Commit a1a09d0a authored by Julien Signoles's avatar Julien Signoles
Browse files

[E-ACSL] faster initialization of the dataflow analysis

[E-ACSL] fixed bug with global declarations involved in the memory model (btw fixed but #1392)
[E-ACSL] additional feedback messages
parent fbbd4716
################
# NEXT RELEASE #
################
##################
# FEATURE WISHES #
##################
- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
à appeler dès qu'un behavior est activé
- [Yannick] Logic functions
#####################
# E-ACSL CONSTRUCTS #
#####################
- predicates
- logic functions
- disjoint and complete behaviors (cf. Bernard's feature wish)
- loop invariant
########
# CODE #
########
- grep TODO *.ml*
- Gestion du mode -lib-entry
- Gestion du mode -lib-entry et/ou pas de main
- variable GMP potentiellement initialisé mais non utilisé en présence de \at
(voir test result.i, cas -e-acsl-gmp-only)
- générer les delete des globals dans une fonction séparée, comme pour les init.
- do not analyse library function in pre-analysis
- variadic functions are not yet duplicated
- generate guard for \offset & co (\offset(p) must ensures that p is valid)
- improve computation of the initial state of the dataflow analysis
- don't generate code for properties with status valid_under_hyp when we know
that the hyp will be generated
- use value analysis whenever possible instead of our own imprecise analysis
- use checked assigns whenever possible in the analysis
checked property = valid property or property for which code will be generated
##############
# KNOWN BUGS #
......@@ -37,6 +52,14 @@
(voir aussi result.i et ./at_stmt_contract.i)
- interprétation des tableaux
- \valid (or other memory-model constructs) in ensures of functions without code
- function pointers
(in case of the pointing function has a behavior like in test ptr_init.c)
#######
# DOC #
#######
- writing user manual
#########
# TESTS #
......
......@@ -53,6 +53,7 @@ module Extended_ast =
let unmemoized_extend_ast () =
let extend () =
Options.feedback ~level:3 "setting kernel options for E-ACSL.";
Kernel.CppExtraArgs.add
(Pretty_utils.sfprintf " -DE_ACSL_MACHDEP=%s -I%s/libc"
(Kernel.Machdep.get ())
......@@ -71,6 +72,8 @@ let unmemoized_extend_ast () =
if Ast.is_computed () then begin
(* do not modify the existing project: work on a copy.
Must also extend the current AST with the E-ACSL's library files. *)
Options.feedback ~level:2 "AST already computed: \
E-ACSL is going to work on a copy.";
let name = Project.get_name (Project.current ()) in
let tmpfile =
Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
......@@ -123,6 +126,7 @@ let generate_code =
(fun name ->
apply_on_e_acsl_ast
(fun () ->
Options.feedback "beginning translation.";
let dup_prj = Pre_visit.dup_functions () in
let res =
Project.on
......@@ -137,6 +141,8 @@ let generate_code =
()
in
Project.remove ~project:dup_prj ();
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
res)
())
......
......@@ -105,6 +105,11 @@ let () = Cmdline.run_after_configuring_stage version
let must_visit () = Run.get () || Check.get ()
let dkey_analysis = register_category "analysis"
let dkey_dup = register_category "duplication"
let dkey_translation = register_category "translation"
let dkey_typing = register_category "typing"
(*
Local Variables:
compile-command: "make"
......
......@@ -34,6 +34,11 @@ module Project_name: String
val must_visit: unit -> bool
val dkey_analysis: category
val dkey_dup: category
val dkey_translation: category
val dkey_typing: category
(*
Local Variables:
compile-command: "make"
......
......@@ -24,6 +24,7 @@ open Cil_types
open Cil_datatype
let init_mpz () =
Options.feedback ~level:2 "initializing GMP type.";
let set_mpzt = object
inherit Cil.nopCilVisitor
method vglob = function
......@@ -40,6 +41,8 @@ let init_mpz () =
left-values must be tracked by the memory model library *)
(* ********************************************************************** *)
let dkey = Options.dkey_analysis
let get_rte_by_stmt =
Misc.rte2
"stmt_annotations"
......@@ -109,7 +112,9 @@ end = struct
end
let reset = Env.clear
let reset () =
Options.feedback ~dkey ~level:2 "clearing environment.";
Env.clear ()
module rec Transfer
: Dataflow.BackwardsTransfer with type t = Varinfo.Set.t option
......@@ -442,28 +447,26 @@ end = struct
module D = Dataflow.Backwards(Transfer)
let compute init_set kf =
Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
assert (not (Misc.is_library_loc (Kernel_function.get_location kf)));
let tbl = Stmt.Hashtbl.create 17 in
(* Options.feedback "ANALYSING %a" Kernel_function.pretty kf;*)
Env.add kf tbl;
try
let init = object
inherit Visitor.frama_c_inplace
method vstmt_aux stmt =
Stmt.Hashtbl.add tbl stmt None;
Cil.DoChildren
method vinst _ = Cil.SkipChildren
method vexpr _ = Cil.SkipChildren
end
in
(try
let fundec = Kernel_function.get_definition kf in
let stmt = Kernel_function.find_return kf in
ignore (Visitor.visitFramacFunction init fundec);
Extlib.may (fun set -> Stmt.Hashtbl.replace tbl stmt (Some set)) init_set;
D.compute [ stmt ];
tbl
let stmts, returns = Dataflow.find_stmts fundec in
List.iter (fun s -> Stmt.Hashtbl.add tbl s None) stmts;
Extlib.may
(fun set ->
List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
init_set;
D.compute returns
with Kernel_function.No_Definition | Kernel_function.No_Statement ->
tbl
());
Options.feedback ~dkey ~level:2 "function %a done."
Kernel_function.pretty kf;
tbl
let get ?init kf =
if Misc.is_library_loc (Kernel_function.get_location kf) then
......@@ -490,14 +493,17 @@ let consolidated_must_model_vi vi =
if Env.is_consolidated () then
Env.consolidated_mem vi
else begin
Options.feedback ~level:2 "performing pre-analysis for minimal memory \
instrumentation.";
(try
let main, _ = Globals.entry_point () in
let set = Compute.get main in
Env.consolidate set
with Globals.No_such_entry_point s ->
Options.warning ~once:true "%s@ \
@[The generated program may be incomplete.@]"
@[The generated program may miss memory instrumentation.@]"
s);
Options.feedback ~level:2 "pre-analysis done.";
Env.consolidated_mem vi
end
......
......@@ -22,6 +22,8 @@
open Cil_types
let dkey = Options.dkey_dup
(* ********************************************************************** *)
(* Environment *)
(* ********************************************************************** *)
......@@ -66,11 +68,6 @@ let copy_ppt old_prj new_prj old_ppt new_ppt =
(fun s ->
let e = match l with [] -> assert false | e :: _ -> e in
let emitter = Emitter.Usable_emitter.get e.P.emitter in
Options.feedback "%a: %a --> %a (%d)"
Emitter.pretty emitter
Property.pretty new_ppt
Property_status.Emitted_status.pretty s
(List.length e.P.properties);
match s with
| P.True | P.False_and_reachable | P.Dont_know ->
P.emit emitter ~hyps:e.P.properties new_ppt s
......@@ -198,7 +195,8 @@ let dup_fundec loc spec bhv kf vi new_vi =
return
let dup_global loc old_prj spec bhv kf vi new_vi =
(* Options.feedback "DUP GLOBAL %s" vi.vname;*)
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
let fundec, return = dup_fundec loc spec bhv kf vi new_vi in
let fct = Definition(fundec, loc) in
let new_spec = fundec.sspec in
......@@ -208,6 +206,7 @@ let dup_global loc old_prj spec bhv kf vi new_vi =
Globals.Functions.replace_by_definition new_spec fundec loc;
Annotations.register_funspec new_kf;
dup_spec_status old_prj kf new_kf spec new_spec;
Options.feedback ~dkey ~level:2 "function %s" name;
GFun(fundec, loc)
(* ********************************************************************** *)
......@@ -352,6 +351,7 @@ class dup_functions_visitor prj = object (self)
end
let dup_functions () =
Options.feedback ~level:2 "duplicating annotated functions";
let prj =
File.create_project_from_visitor
"e_acsl_dup_functions"
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -5,10 +5,12 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -5,8 +5,10 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,8 +4,10 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
tests/e-acsl-runtime/bts1324.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
tests/e-acsl-runtime/bts1324.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
......@@ -4,6 +4,8 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment