From 15aaf8d330b6743d0e279f9d4c2c3d2c6f78b75a Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 27 Sep 2019 15:11:35 +0200
Subject: [PATCH] [archi] visitor rewritten up to blocks (included)
---
src/plugins/e-acsl/Makefile.in | 1 -
.../e-acsl/src/analyses/mmodel_analysis.ml | 52 ++-
.../e-acsl/src/analyses/mmodel_analysis.mli | 12 +-
.../src/code_generator/at_with_lscope.ml | 6 +-
src/plugins/e-acsl/src/code_generator/env.ml | 80 ++---
src/plugins/e-acsl/src/code_generator/env.mli | 29 +-
.../src/code_generator/global_observer.ml | 36 +-
.../src/code_generator/global_observer.mli | 4 +-
.../e-acsl/src/code_generator/injector.ml | 278 +++++++++++++++
.../e-acsl/src/code_generator/injector.mli | 2 +
.../e-acsl/src/code_generator/label.ml | 27 +-
.../e-acsl/src/code_generator/label.mli | 4 +-
.../src/code_generator/literal_observer.ml | 11 +-
.../src/code_generator/literal_observer.mli | 4 +-
.../src/code_generator/logic_functions.ml | 15 +-
.../src/code_generator/logic_functions.mli | 3 +-
.../e-acsl/src/code_generator/loops.ml | 37 +-
.../e-acsl/src/code_generator/loops.mli | 2 +-
.../src/code_generator/memory_observer.ml | 3 +-
.../src/code_generator/mmodel_translate.ml | 11 +
.../e-acsl/src/code_generator/quantif.ml | 7 +-
.../e-acsl/src/code_generator/rational.ml | 28 +-
.../e-acsl/src/code_generator/rational.mli | 23 +-
.../e-acsl/src/code_generator/temporal.ml | 132 ++++---
.../e-acsl/src/code_generator/temporal.mli | 11 +-
.../e-acsl/src/code_generator/translate.ml | 90 ++---
.../e-acsl/src/code_generator/visit.ml | 322 ------------------
src/plugins/e-acsl/src/main.ml | 64 ++--
28 files changed, 607 insertions(+), 687 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c4f3be570ff..797036119ec 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -79,7 +79,6 @@ SRC_CODE_GENERATOR:= \
memory_observer \
literal_observer \
global_observer \
- visit \
injector
SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index b0600493ae0..70451b51a11 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
@@ -710,11 +710,7 @@ if there are memory-related annotations.@]"
Env.consolidated_mem vi
end
-let must_model_vi bhv ?kf ?stmt vi =
- let vi = match bhv with
- | None -> vi
- | Some bhv -> Visitor_behavior.Get_orig.varinfo bhv vi
- in
+let must_model_vi ?kf ?stmt vi =
let _kf = match kf, stmt with
| None, None | Some _, _ -> kf
| None, Some stmt -> Some (Kernel_function.find_englobing_kf stmt)
@@ -743,19 +739,19 @@ consolidated_must_model_vi vi
false
*)
-let rec apply_on_vi_base_from_lval f bhv ?kf ?stmt = function
- | Var vi, _ -> f bhv ?kf ?stmt vi
- | Mem e, _ -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
+let rec apply_on_vi_base_from_lval f ?kf ?stmt = function
+ | Var vi, _ -> f ?kf ?stmt vi
+ | Mem e, _ -> apply_on_vi_base_from_exp f ?kf ?stmt e
-and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
+and apply_on_vi_base_from_exp f ?kf ?stmt e = match e.enode with
| Lval lv | AddrOf lv | StartOf lv ->
- apply_on_vi_base_from_lval f bhv ?kf ?stmt lv
+ apply_on_vi_base_from_lval f ?kf ?stmt lv
| BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) ->
- apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
+ apply_on_vi_base_from_exp f ?kf ?stmt e1
| BinOp(MinusPP, e1, e2, _) ->
- apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
- || apply_on_vi_base_from_exp f bhv ?kf ?stmt e2
- | Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
+ apply_on_vi_base_from_exp f ?kf ?stmt e1
+ || apply_on_vi_base_from_exp f ?kf ?stmt e2
+ | Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f ?kf ?stmt e
| BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
| Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
| Const _ -> (* possible in case of static address *) false
@@ -765,18 +761,16 @@ and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
let must_model_lval = apply_on_vi_base_from_lval must_model_vi
let must_model_exp = apply_on_vi_base_from_exp must_model_vi
-let must_never_monitor_lval bhv ?kf ?stmt lv =
+let must_never_monitor_lval ?kf ?stmt lv =
apply_on_vi_base_from_lval
- (fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
- bhv
+ (fun ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
?kf
?stmt
lv
-let must_never_monitor_exp bhv ?kf ?stmt lv =
+let must_never_monitor_exp ?kf ?stmt lv =
apply_on_vi_base_from_exp
- (fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
- bhv
+ (fun ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
?kf
?stmt
lv
@@ -785,23 +779,23 @@ let must_never_monitor_exp bhv ?kf ?stmt lv =
(** {1 Public API} *)
(* ************************************************************************** *)
-let must_model_vi ?bhv ?kf ?stmt vi =
+let must_model_vi ?kf ?stmt vi =
not (must_never_monitor vi)
&&
(Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_vi bhv ?kf ?stmt) false vi)
+ || Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
-let must_model_lval ?bhv ?kf ?stmt lv =
- not (must_never_monitor_lval bhv ?kf ?stmt lv)
+let must_model_lval ?kf ?stmt lv =
+ not (must_never_monitor_lval ?kf ?stmt lv)
&&
(Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_lval bhv ?kf ?stmt) false lv)
+ || Error.generic_handle (must_model_lval ?kf ?stmt) false lv)
-let must_model_exp ?bhv ?kf ?stmt exp =
- not (must_never_monitor_exp bhv ?kf ?stmt exp)
+let must_model_exp ?kf ?stmt exp =
+ not (must_never_monitor_exp ?kf ?stmt exp)
&&
(Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_exp bhv ?kf ?stmt) false exp)
+ || Error.generic_handle (must_model_exp ?kf ?stmt) false exp)
let use_model () =
not (Env.is_empty ())
@@ -810,6 +804,6 @@ let use_model () =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
index f091021b51c..bf50f714e48 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
@@ -31,19 +31,15 @@ val reset: unit -> unit
val use_model: unit -> bool
(** Is one variable monitored (at least)? *)
-val must_model_vi: ?bhv:Visitor_behavior.t -> ?kf:kernel_function
- -> ?stmt:stmt -> varinfo -> bool
+val must_model_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
(** [must_model_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
[stmt] in the given function [kf] must be tracked by the memory model
- library. If behavior [bhv] is specified then assume that [vi] is part
- of the new project generated by the given copy behavior [bhv] *)
+ library. *)
-val must_model_lval: ?bhv:Visitor_behavior.t -> ?kf:kernel_function
- -> ?stmt:stmt -> lval -> bool
+val must_model_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
(** Same as {!must_model_vi}, for left-values *)
-val must_model_exp: ?bhv:Visitor_behavior.t -> ?kf:kernel_function
- -> ?stmt:stmt -> exp -> bool
+val must_model_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
(** Same as {!must_model_vi}, for expressions *)
(*
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index 93075f36f5b..c9b710bc924 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -204,7 +204,7 @@ let index_from_sizes_and_shifts ~loc sizes_and_shifts =
sum
let put_block_at_label env block label =
- let stmt = Label.get_stmt (Env.get_visitor env) label in
+ let stmt = Label.get_stmt label in
let env_ref = ref env in
let o = object
inherit Visitor.frama_c_inplace
@@ -214,8 +214,7 @@ let put_block_at_label env block label =
Cil.ChangeTo stmt
end
in
- let bhv = Env.get_behavior env in
- ignore(Visitor.visitFramacStmt o (Visitor_behavior.Get.stmt bhv stmt));
+ ignore (Visitor.visitFramacStmt o stmt);
!env_ref
let to_exp ~loc kf env pot label =
@@ -244,6 +243,7 @@ let to_exp ~loc kf env pot label =
~name:"at"
~scope:Varname.Function
env
+ kf
None
ty_ptr
(fun vi e ->
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index ca90454b2a7..b6c1f7742c8 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -54,7 +54,6 @@ type local_env = {
}
type t = {
- visitor: Visitor.frama_c_visitor;
lscope: Lscope.t;
lscope_reset: bool;
annotation_kind: Misc.annotation_kind;
@@ -86,21 +85,8 @@ let empty_local_env =
mp_tbl = empty_mp_tbl;
rte = true }
-let dummy =
- { visitor = new Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ());
- lscope = Lscope.empty;
- lscope_reset = true;
- annotation_kind = Misc.Assertion;
- new_global_vars = [];
- global_mp_tbl = empty_mp_tbl;
- env_stack = [];
- var_mapping = Logic_var.Map.empty;
- loop_invariants = [];
- cpt = 0; }
-
-let empty v =
- { visitor = v;
- lscope = Lscope.empty;
+let empty =
+ { lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
@@ -118,19 +104,6 @@ let has_no_new_stmt env =
let local, _ = top env in
local.block_info = empty_block
-let current_kf env =
- let v = env.visitor in
- match v#current_kf with
- | None -> None
- | Some kf -> Some (Visitor_behavior.Get.kernel_function v#behavior kf)
-
-let set_current_kf env kf =
- let v = env.visitor in
- v#set_current_kf kf
-
-let get_visitor env = env.visitor
-let get_behavior env = env.visitor#behavior
-
(* ************************************************************************** *)
(** {2 Loop invariants} *)
(* ************************************************************************** *)
@@ -163,7 +136,7 @@ let generate_rte env =
(* eta-expansion required for typing generalisation *)
let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
-let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
+let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
let local_env, tl_env = top env in
let local_block = local_env.block_info in
let is_z_t = Gmp_types.Z.is_t ty in
@@ -183,8 +156,8 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
v.vreferenced <- true;
let lscope = match scope with
| Varname.Global -> LGlobal
- | Varname.Function -> LFunction (Extlib.the (current_kf env))
- | Varname.Block -> LLocal_block (Extlib.the (current_kf env))
+ | Varname.Function -> LFunction kf
+ | Varname.Block -> LLocal_block kf
in
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let e = Cil.evar v in
@@ -246,7 +219,7 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
exception No_term
-let new_var ~loc ?(scope=Varname.Block) ?name env t ty mk_stmts =
+let new_var ~loc ?(scope=Varname.Block) ?name env kf t ty mk_stmts =
let local_env, _ = top env in
let memo tbl =
try
@@ -256,18 +229,19 @@ let new_var ~loc ?(scope=Varname.Block) ?name env t ty mk_stmts =
let v, e = Term.Map.find t tbl.new_exps in
if Typ.equal ty v.vtype then v, e, env else raise No_term
with Not_found | No_term ->
- do_new_var ~loc ~scope ?name env t ty mk_stmts
+ do_new_var ~loc ~scope ?name env kf t ty mk_stmts
in
match scope with
| Varname.Global | Varname.Function -> memo env.global_mp_tbl
| Varname.Block -> memo local_env.mp_tbl
-let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
+let new_var_and_mpz_init ~loc ?scope ?name env kf t mk_stmts =
new_var
~loc
?scope
?name
env
+ kf
t
(Gmp_types.Z.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
@@ -285,7 +259,7 @@ module Logic_binding = struct
let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
{ env with var_mapping = var_mapping }
- let add ?ty env logic_v =
+ let add ?ty env kf logic_v =
let ty = match ty with
| Some ty -> ty
| None -> match logic_v.lv_type with
@@ -303,6 +277,7 @@ module Logic_binding = struct
new_var
~loc:Location.unknown
env
+ kf
~name:logic_v.lv_name
None
ty
@@ -336,23 +311,27 @@ module Logic_scope = struct
else env
end
-let emitter =
+let _emitter = (* [TODO ARCHI] *)
Emitter.create
"E_ACSL"
[ Emitter.Code_annot ]
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
-let add_assert env stmt annot = match current_kf env with
+(* [TODO ARCHI] to be reimplemented *)
+let add_assert _env _stmt _annot = assert false
+(*match current_kf env with
| None -> assert false
- | Some kf ->
- Queue.add
+ | Some _kf ->
+(* Queue.add
(fun () -> Annotations.add_assert emitter ~kf stmt annot)
env.visitor#get_filling_actions
+ *)*)
+
-let add_stmt ?(post=false) ?before env stmt =
+let add_stmt ?(post=false) ?before env kf stmt =
if not post then
- Extlib.may (fun old -> E_acsl_label.move env.visitor ~old stmt) before;
+ Extlib.may (fun old -> E_acsl_label.move kf ~old stmt) before;
let local_env, tl = top env in
let block = local_env.block_info in
let block =
@@ -491,15 +470,16 @@ module Context = struct
if !ctx <> [] then begin
let vars = env.new_global_vars in
let env =
- { env with new_global_vars =
- List.filter
+ { env with
+ new_global_vars =
+ List.filter
(fun (v, scope) ->
- (match scope with
- | LGlobal | LFunction _ -> true
- | LLocal_block _ -> false)
- && List.for_all (fun (v', _) -> v != v') vars)
- !ctx
- @ vars }
+ (match scope with
+ | LGlobal | LFunction _ -> true
+ | LLocal_block _kf -> false)
+ && List.for_all (fun (v', _) -> v != v') vars)
+ !ctx
+ @ vars }
in
ctx := [];
env
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 8789e0f8d18..bfc4a75da8c 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -22,15 +22,14 @@
open Cil_types
-(** Environments.
+(** Environments.
Environments handle all the new C constructs (variables, statements and
- annotations. *)
+ annotations. *)
type t
-val dummy: t
-val empty: Visitor.frama_c_visitor -> t
+val empty: t
val has_no_new_stmt: t -> bool
(** Assume that a local context has been previously pushed.
@@ -43,8 +42,8 @@ type localized_scope =
val new_var:
loc:location -> ?scope:Varname.scope -> ?name:string ->
- t -> term option -> typ ->
- (varinfo -> exp (* the var as exp *) -> stmt list) ->
+ t -> kernel_function -> term option -> typ ->
+ (varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
(** [new_var env t ty mk_stmts] extends [env] with a fresh variable of type
[ty] corresponding to [t]. [scope] is the scope of the new variable (default
@@ -54,14 +53,14 @@ val new_var:
val new_var_and_mpz_init:
loc:location -> ?scope:Varname.scope -> ?name:string ->
- t -> term option ->
- (varinfo -> exp (* the var as exp *) -> stmt list) ->
+ t -> kernel_function -> term option ->
+ (varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
-(** Same as [new_var], but dedicated to mpz_t variables initialized by
+(** Same as [new_var], but dedicated to mpz_t variables initialized by
{!Mpz.init}. *)
module Logic_binding: sig
- val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
+ val add: ?ty:typ -> t -> kernel_function -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
val add_binding: t -> logic_var -> varinfo -> t
@@ -80,7 +79,7 @@ val add_assert: t -> stmt -> predicate -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
-val add_stmt: ?post:bool -> ?before:stmt -> t -> stmt -> t
+val add_stmt: ?post:bool -> ?before:stmt -> t -> kernel_function -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s].
[before] may define which stmt the new one is included before. This is to
say that any labels attached to [before] are moved to [stmt]. [post]
@@ -115,11 +114,6 @@ val transfer: from:t -> t -> t
val get_generated_variables: t -> (varinfo * localized_scope) list
(** All the new variables local to the visited function. *)
-val get_visitor: t -> Visitor.generic_frama_c_visitor
-val get_behavior: t -> Visitor_behavior.t
-val current_kf: t -> kernel_function option
-(** Kernel function currently visited in the new project. *)
-
module Logic_scope: sig
val get: t -> Lscope.t
(** Return the logic scope associated to the environment. *)
@@ -141,9 +135,6 @@ module Logic_scope: sig
reset at next call to [reset]. *)
end
-val set_current_kf: t -> kernel_function -> unit
-(* Set current kf of the environment *)
-
(* ************************************************************************** *)
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 4fffa4ab20a..d4ad9545a64 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -38,6 +38,9 @@ let reset () = Varinfo.Hashtbl.reset tbl
let is_empty () = Varinfo.Hashtbl.length tbl = 0
+(* Make a unique mapping for each global variable omitting initializers.
+ Initializers (used to capture literal strings) are added through
+ [add_initializer] below. *)
let add vi =
if Mmodel_analysis.must_model_vi vi then
Varinfo.Hashtbl.replace tbl vi (ref [])
@@ -50,12 +53,12 @@ let add_initializer vi offset init =
with Not_found ->
assert false
-let rec literal_in_initializer env = function
- | SingleInit exp -> snd (Literal_observer.exp_in_depth env exp)
+let rec literal_in_initializer env kf = function
+ | SingleInit exp -> snd (Literal_observer.exp_in_depth env kf exp)
| CompoundInit (_, l) ->
- List.fold_left (fun env (_, i) -> literal_in_initializer env i) env l
+ List.fold_left (fun env (_, i) -> literal_in_initializer env kf i) env l
-let mk_init bhv env =
+let mk_init_function env =
(* Create [__e_acsl_globals_init] function with definition
for initialization of global variables *)
let vi =
@@ -82,9 +85,7 @@ let mk_init bhv env =
let fct = Definition(fundec, Location.unknown) in
(* Create and register [__e_acsl_globals_init] as kernel
function *)
- let kf =
- { fundec = fct; spec = spec }
- in
+ let kf = { fundec = fct; spec = spec } in
Globals.Functions.register kf;
Globals.Functions.replace_by_definition spec fundec Location.unknown;
(* Now generate the statements. The generation is done only now because it
@@ -95,12 +96,11 @@ let mk_init bhv env =
after generating observers of **all** globals *)
let env, stmts =
Varinfo.Hashtbl.fold_sorted
- (fun old_vi l stmts ->
- let new_vi = Visitor_behavior.Get.varinfo bhv old_vi in
+ (fun vi l stmts ->
List.fold_left
(fun (env, stmts) (off, init) ->
- let env = literal_in_initializer env init in
- let stmt = Temporal.generate_global_init new_vi off init env in
+ let env = literal_in_initializer env kf init in
+ let stmt = Temporal.generate_global_init vi off init in
env, match stmt with None -> stmts | Some stmt -> stmt :: stmts)
stmts
!l)
@@ -110,11 +110,10 @@ let mk_init bhv env =
(* allocation and initialization of globals *)
let stmts =
Varinfo.Hashtbl.fold_sorted
- (fun old_vi _ stmts ->
- let new_vi = Visitor_behavior.Get.varinfo bhv old_vi in
+ (fun vi _ stmts ->
(* a global is both allocated and initialized *)
- Misc.mk_store_stmt new_vi
- :: Misc.mk_initialize ~loc:Location.unknown (Cil.var new_vi)
+ Misc.mk_store_stmt vi
+ :: Misc.mk_initialize ~loc:Location.unknown (Cil.var vi)
:: stmts)
tbl
stmts
@@ -171,11 +170,10 @@ let mk_init bhv env =
blk.bstmts <- stmts;
vi, fundec, env
-let mk_delete bhv stmts =
+let mk_delete_stmts stmts =
Varinfo.Hashtbl.fold_sorted
- (fun old_vi _l acc ->
- let new_vi = Visitor_behavior.Get.varinfo bhv old_vi in
- Misc.mk_delete_stmt new_vi :: acc)
+ (fun vi _l acc ->
+ Misc.mk_delete_stmt vi :: acc)
tbl
stmts
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.mli b/src/plugins/e-acsl/src/code_generator/global_observer.mli
index 6b1ce04936a..e0098a5ae8a 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.mli
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.mli
@@ -36,11 +36,11 @@ val add: varinfo -> unit
val add_initializer: varinfo -> offset -> init -> unit
(** add the initializer for the given observed variable *)
-val mk_init: Visitor_behavior.t -> Env.t -> varinfo * fundec * Env.t
+val mk_init_function: Env.t -> varinfo * fundec * Env.t
(** generates a new C function containing the observers for global variable
declaration and initialization *)
-val mk_delete: Visitor_behavior.t -> stmt list -> stmt list
+val mk_delete_stmts: stmt list -> stmt list
(** generates the observers for global variable de-allocation *)
(*
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 6cc68db52cf..ef8f10fbf54 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -20,6 +20,284 @@
(* *)
(**************************************************************************)
+open Cil_types
+open Cil_datatype
+
+let dkey = Options.dkey_translation
+
+let is_main kf =
+ try
+ let main, _ = Globals.entry_point () in
+ Kernel_function.equal kf main
+ with Globals.No_such_entry_point _s ->
+ false
+
+(* ************************************************************************** *)
+(* Code *)
+(* ************************************************************************** *)
+
+let inject_in_block _env _main kf blk =
+ (* [TODO ARCHI] HERE recursive call *)
+ let free_stmts = At_with_lscope.Free.find_all kf in
+ match blk.blocals, free_stmts with
+ | [], [] ->
+ ()
+ | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
+ let add_locals stmts =
+ if Functions.instrument kf then
+ List.fold_left
+ (fun acc vi ->
+ if Mmodel_analysis.must_model_vi ~kf vi then
+ Misc.mk_delete_stmt vi :: acc
+ else
+ acc)
+ stmts
+ blk.blocals
+ else
+ stmts
+ in
+ let rec insert_in_innermost_last_block blk = function
+ | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
+ (* keep the return (enclosed in a generated block) at the end;
+ preceded by clean if any *)
+ let init, tl =
+ if is_main kf && Mmodel_analysis.use_model () then
+ free_stmts @ [ potential_clean; ret ], tl
+ else
+ free_stmts @ [ ret ], l
+ in
+ (* now that [free] stmts for [kf] have been inserted,
+ there is no more need to keep the corresponding entries in the
+ table managing them. *)
+ At_with_lscope.Free.remove_all kf;
+ blk.bstmts <-
+ List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
+ | { skind = Block b } :: _ ->
+ insert_in_innermost_last_block b (List.rev b.bstmts)
+ | l ->
+ blk.bstmts <- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
+ in
+ insert_in_innermost_last_block blk (List.rev blk.bstmts);
+ if Functions.instrument kf then
+ blk.bstmts <-
+ List.fold_left
+ (fun acc vi ->
+ if Mmodel_analysis.must_model_vi vi && not vi.vdefined
+ then Misc.mk_store_stmt vi :: acc
+ else acc)
+ blk.bstmts
+ blk.blocals
+
+(* ************************************************************************** *)
+(* Function definition *)
+(* ************************************************************************** *)
+
+let add_generated_variables_in_function env fundec =
+ let vars = Env.get_generated_variables env in
+ let locals, blocks =
+ List.fold_left
+ (fun (local_vars, block_vars as acc) (v, scope) -> match scope with
+ (* TODO: [kf] assumed to be consistent. Should be asserted. *)
+ (* TODO: actually, is the kf as constructor parameter useful? *)
+ | Env.LFunction _kf -> v :: local_vars, v :: block_vars
+ | Env.LLocal_block _kf -> v :: local_vars, block_vars
+ | _ -> acc)
+ (fundec.slocals, fundec.sbody.blocals)
+ vars
+ in
+ fundec.slocals <- locals;
+ fundec.sbody.blocals <- blocks
+
+(* Memory management for \at on purely logic variables: put [malloc] stmts at
+ proper locations *)
+let add_malloc_and_free_stmts kf fundec =
+ let malloc_stmts = At_with_lscope.Malloc.find_all kf in
+ let fstmts = malloc_stmts @ fundec.sbody.bstmts in
+ fundec.sbody.bstmts <- fstmts;
+ (* now that [malloc] stmts for [kf] have been inserted, there is no more need
+ to keep the corresponding entries in the table managing them. *)
+ At_with_lscope.Malloc.remove_all kf
+
+let inject_in_fundec env main fundec =
+ let vi = fundec.svar in
+ let kf = try Globals.Functions.get vi with Not_found -> assert false in
+ (* convert ghost variables *)
+ vi.vghost <- false;
+ List.iter (fun vi -> vi.vghost <- false) fundec.slocals;
+ (* update environments *)
+ Builtins.update vi.vname vi;
+ if is_main kf then Global_observer.add vi;
+ (* exit point computations *)
+ if Functions.instrument kf then Exit_points.generate fundec;
+ Options.feedback ~dkey ~level:2 "entering in function %a."
+ Kernel_function.pretty kf;
+ (* recursive visit *)
+ inject_in_block env main kf fundec.sbody;
+ Exit_points.clear ();
+ add_generated_variables_in_function env fundec;
+ add_malloc_and_free_stmts kf fundec;
+ (* setting main if necessary *)
+ let main = if is_main kf then Some fundec else main in
+ Options.feedback ~dkey ~level:2 "function %a done."
+ Kernel_function.pretty kf;
+ env, main
+
+(* ************************************************************************** *)
+(* The whole AST *)
+(* ************************************************************************** *)
+
+let inject_in_global (env, main) = function
+ (* library functions and built-ins *)
+ | GVarDecl(vi, _) | GVar(vi, _, _)
+ | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
+ when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
+ Misc.register_library_function vi;
+ if Builtins.mem vi.vname then Builtins.update vi.vname vi;
+ env, main
+
+ (* Cil built-ins and other library globals: nothing to do *)
+ | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
+ when Cil.is_builtin vi ->
+ env, main
+ | g when Misc.is_library_loc (Global.loc g) ->
+ env, main
+
+ (* variables and functions declarations *)
+ | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
+ (* do not convert extern ghost variables, because they can't be linked,
+ see bts #1392 *)
+ if vi.vstorage <> Extern then vi.vghost <- false;
+ env, main
+
+ (* variable definition *)
+ | GVar(vi, _initinfo, _) ->
+ vi.vghost <- false;
+ (* [TODO ARCHI] init_info *)
+ env, main
+
+ (* function definition *)
+ | GFun(fundec, _) ->
+ inject_in_fundec env main fundec
+
+ (* other globals: nothing to do *)
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ | GAnnot _ (* do never read annotation from sources *)
+ ->
+ env, main
+
+(* TODO: what about using [file.globalinit]? *)
+let inject_global_initializer env file main =
+ Options.feedback ~dkey ~level:2 "building global initializer.";
+ (* [TODO ARCHI] is env really useless? *)
+ let vi, fundec, _env = Global_observer.mk_init_function env in
+ let cil_fct = GFun(fundec, Location.unknown) in
+ if Mmodel_analysis.use_model () then begin
+ match main with
+ | Some main ->
+ let exp = Cil.evar ~loc:Location.unknown vi in
+ (* Create [__e_acsl_globals_init();] call *)
+ let stmt =
+ Cil.mkStmtOneInstr ~valid_sid:true
+ (Call(None, exp, [], Location.unknown))
+ in
+ vi.vreferenced <- true;
+ (* insert [__e_acsl_globals_init ();] as first statement of
+ [main] *)
+ main.sbody.bstmts <- stmt :: main.sbody.bstmts;
+ let new_globals =
+ List.fold_right
+ (fun g acc -> match g with
+ | GFun({ svar = vi }, _)
+ when Varinfo.equal vi main.svar ->
+ acc
+ | _ -> g :: acc)
+ file.globals
+ [ cil_fct; GFun(main, Location.unknown) ]
+ in
+ (* add the literal string varinfos as the very first
+ globals *)
+ let new_globals =
+ Literal_strings.fold
+ (fun _ vi l ->
+ GVar(vi, { init = None }, Location.unknown) :: l)
+ new_globals
+ in
+ file.globals <- new_globals
+ | None ->
+ Kernel.warning "@[no entry point specified:@ \
+ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
+ Global_observer.function_name;
+ file.globals <- file.globals @ [ cil_fct ]
+ end
+
+(* Add a call to [__e_acsl_memory_init] that initializes memory storage and
+ potentially records program arguments. Parameters to [__e_acsl_memory_init]
+ are addresses of program arguments or NULLs if [main] is declared without
+ arguments. *)
+let inject_mmodel_initializer main =
+ let loc = Location.unknown in
+ let nulls = [ Cil.zero loc ; Cil.zero loc ] in
+ let handle_main main =
+ let args =
+ (* record arguments only if the second has a pointer type, so a argument
+ strings can be recorded. This is sufficient to capture C99 compliant
+ arguments and GCC extensions with environ. *)
+ match main.sformals with
+ | [] ->
+ (* no arguments to main given *)
+ nulls
+ | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
+ (* grab addresses of arguments for a call to the main initialization
+ function, i.e., [__e_acsl_memory_init] *)
+ List.map Cil.mkAddrOfVi main.sformals;
+ | _ :: _ ->
+ (* some non-standard arguments. *)
+ nulls
+ in
+ let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
+ let args = args @ [ ptr_size ] in
+ let name = Functions.RTL.mk_api_name "memory_init" in
+ let init = Misc.mk_call loc name args in
+ main.sbody.bstmts <- init :: main.sbody.bstmts
+ in
+ Extlib.may handle_main main
+
+let inject_in_file file =
+ let env, main =
+ List.fold_left inject_in_global (Env.empty, None) file.globals
+ in
+ (* post-treatment *)
+ (* extend [main] with forward initialization and put it at end *)
+ if not (Global_observer.is_empty () && Literal_strings.is_empty ()) then
+ inject_global_initializer env file main;
+ file.globals <- Logic_functions.add_generated_functions file.globals;
+ inject_mmodel_initializer main
+
+let reset_all () =
+ Misc.reset ();
+ Logic_functions.reset ();
+ Literal_strings.reset ();
+ Global_observer.reset ();
+ Keep_status.before_translation ()
+
+let inject () =
+ Options.feedback ~level:2
+ "injecting annotations as code in project %a"
+ Project.pretty (Project.current ());
+ reset_all ();
+ Misc.reorder_ast ();
+ let ast = Ast.get () in
+ inject_in_file ast;
+ (* [TODO ARCHI] not consistent with the [reset_all] strategy: *)
+ Typing.clear ()
+
(*
Local Variables:
compile-command: "make -C ../.."
diff --git a/src/plugins/e-acsl/src/code_generator/injector.mli b/src/plugins/e-acsl/src/code_generator/injector.mli
index 6cc68db52cf..6c382503b25 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.mli
+++ b/src/plugins/e-acsl/src/code_generator/injector.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+val inject: unit -> unit
+
(*
Local Variables:
compile-command: "make -C ../.."
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index 4a2b857694e..f6638213b5a 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -37,14 +37,13 @@ let self = Labeled_stmts.self
let new_labeled_stmt stmt = try Labeled_stmts.find stmt with Not_found -> stmt
-let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
+let move kf ~old new_stmt =
let labels = old.labels in
match labels with
| [] -> ()
| _ :: _ ->
old.labels <- [];
new_stmt.labels <- labels @ new_stmt.labels;
- let old = Visitor_behavior.Get_orig.stmt vis#behavior old in
Labeled_stmts.add old new_stmt;
(* update the gotos of the function jumping to one of the labels *)
let o orig_stmt = object
@@ -63,28 +62,30 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
method !vexpr _ = Cil.SkipChildren
method !vlval _ = Cil.SkipChildren
end in
- let f = Extlib.the vis#current_func in
- let mv_labels s =
- ignore (Visitor.visitFramacStmt (o s) (Visitor_behavior.Memo.stmt vis#behavior s))
+ let mv_labels s = ignore (Visitor.visitFramacStmt (o s) s) in
+ let f =
+ try Kernel_function.get_definition kf
+ with Kernel_function.No_Definition -> assert false
in
List.iter mv_labels f.sallstmts
-let get_stmt vis = function
+(* [TODO ARCHI] reimplement it *)
+let get_stmt = function
| StmtLabel { contents = stmt } -> stmt
| BuiltinLabel Here ->
- (match vis#current_stmt with
+(* (match vis#current_stmt with
| None -> Error.not_yet "label \"Here\" in function contract"
- | Some s -> s)
+ | Some s -> s)*) assert false
| BuiltinLabel(Old | Pre) ->
- (try Kernel_function.find_first_stmt (Extlib.the vis#current_kf)
- with Kernel_function.No_Statement -> assert false)
+(* (try Kernel_function.find_first_stmt (Extlib.the vis#current_kf)
+ with Kernel_function.No_Statement -> assert false)*)assert false
| BuiltinLabel(Post) ->
- (try Kernel_function.find_return (Extlib.the vis#current_kf)
- with Kernel_function.No_Statement -> assert false)
+(* (try Kernel_function.find_return (Extlib.the vis#current_kf)
+ with Kernel_function.No_Statement -> assert false)*) assert false
| BuiltinLabel _ | FormalLabel _ -> assert false
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/label.mli b/src/plugins/e-acsl/src/code_generator/label.mli
index 994d7831f94..194e2d2589e 100644
--- a/src/plugins/e-acsl/src/code_generator/label.mli
+++ b/src/plugins/e-acsl/src/code_generator/label.mli
@@ -22,11 +22,11 @@
open Cil_types
-val move: Visitor.generic_frama_c_visitor -> old:stmt -> stmt -> unit
+val move: kernel_function -> old:stmt -> stmt -> unit
(** Move all labels of the [old] stmt onto the new [stmt].
Both stmts must be in the new project. *)
-val get_stmt: Visitor.generic_frama_c_visitor -> logic_label -> stmt
+val get_stmt: logic_label -> stmt
(** @return the statement where the logic label points to. *)
val new_labeled_stmt: stmt -> stmt
diff --git a/src/plugins/e-acsl/src/code_generator/literal_observer.ml b/src/plugins/e-acsl/src/code_generator/literal_observer.ml
index 2be3b192a55..147f9baa6d9 100644
--- a/src/plugins/e-acsl/src/code_generator/literal_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/literal_observer.ml
@@ -22,7 +22,7 @@
open Cil_types
-let literal loc env s =
+let literal loc env kf s =
try
let vi = Literal_strings.find s in
(* if the literal string was already created, just get it. *)
@@ -35,6 +35,7 @@ let literal loc env s =
~scope:Varname.Global
~name:"literal_string"
env
+ kf
None
Cil.charPtrType
(fun _ _ -> [] (* done in the initializer, see {!vglob_aux} *))
@@ -42,14 +43,14 @@ let literal loc env s =
Literal_strings.add s vi;
exp, env
-let exp env e = match e.enode with
+let exp env kf e = match e.enode with
(* the guard below could be optimized: if no annotation **depends on this
string**, then it is not required to monitor it.
(currently, the guard says: "no annotation uses the memory model" *)
- | Const (CStr s) when Mmodel_analysis.use_model () -> literal e.eloc env s
+ | Const (CStr s) when Mmodel_analysis.use_model () -> literal e.eloc env kf s
| _ -> e, env
-let exp_in_depth env e =
+let exp_in_depth env kf e =
let env_ref = ref env in
let o = object
inherit Cil.genericCilVisitor (Visitor_behavior.copy (Project.current ()))
@@ -58,7 +59,7 @@ let exp_in_depth env e =
string**, then it is not required to monitor it.
(currently, the guard says: "no annotation uses the memory model" *)
| Const (CStr s) when Mmodel_analysis.use_model () ->
- let e, env = literal e.eloc !env_ref s in
+ let e, env = literal e.eloc !env_ref kf s in
env_ref := env;
Cil.ChangeTo e
| _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/literal_observer.mli b/src/plugins/e-acsl/src/code_generator/literal_observer.mli
index f5cea67adfe..a196bf1d0d9 100644
--- a/src/plugins/e-acsl/src/code_generator/literal_observer.mli
+++ b/src/plugins/e-acsl/src/code_generator/literal_observer.mli
@@ -24,10 +24,10 @@
open Cil_types
-val exp: Env.t -> exp -> exp * Env.t
+val exp: Env.t -> kernel_function -> exp -> exp * Env.t
(** replace the given exp by an observed variable if it is a literal string *)
-val exp_in_depth: Env.t -> exp -> exp * Env.t
+val exp_in_depth: Env.t -> kernel_function -> exp -> exp * Env.t
(** replace any sub-expression of the given exp that is a literal string by an
observed variable *)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 41bf5a276e0..8ac2421c992 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -177,9 +177,10 @@ let generate_kf ~loc fname env ret_ty params_ty li =
in
Cil.setMaxId fundec;
let spec = Cil.empty_funspec () in
- Queue.add
+ (*[TODO ARCHI] reimplement *)
+(* Queue.add
(fun () -> Globals.Functions.replace_by_definition spec fundec loc)
- (Env.get_visitor env)#get_filling_actions;
+ (Env.get_visitor env)#get_filling_actions;*)
(* create the kernel function itself *)
let kf = { fundec = Definition(fundec, loc); spec } in
(* closure generating the function's body.
@@ -187,8 +188,6 @@ let generate_kf ~loc fname env ret_ty params_ty li =
of recursive function calls) *)
let gen_body () =
let env = Env.push env in
- let old_kf = Extlib.the (Env.current_kf env) in
- Env.set_current_kf env kf;
(* fill the typing environment with the function's parameters
before generating the code (code generation invokes typing) *)
let env =
@@ -225,10 +224,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
(fun lvi ->
Interval.Env.remove lvi;
ignore (Env.Logic_binding.remove env lvi))
- li.l_profile;
- Env.set_current_kf
- env
- (Visitor_behavior.Get_orig.kernel_function (Env.get_behavior env) old_kf)
+ li.l_profile
in
vi, kf, gen_body
@@ -286,7 +282,7 @@ let add_generated_functions globals =
in
List.rev rev_globals
-let tapp_to_exp ~loc fname env t li params_ty args =
+let tapp_to_exp ~loc fname env kf t li params_ty args =
let ret_ty = Typing.get_typ t in
let gen tbl =
let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
@@ -340,6 +336,7 @@ let tapp_to_exp ~loc fname env t li params_ty args =
~loc
~name:li.l_var_info.lv_name
env
+ kf
(Some t)
ret_ty
(fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.mli b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
index 4a9a4c02ce9..8392275833a 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.mli
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
@@ -38,7 +38,8 @@ val reset: unit -> unit
val tapp_to_exp:
loc:location ->
- string -> Env.t -> term -> logic_info -> Typing.number_ty list -> exp list ->
+ string -> Env.t -> kernel_function ->
+ term -> logic_info -> Typing.number_ty list -> exp list ->
varinfo * exp * Env.t
val add_generated_functions: global list -> global list
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 05f89c24ee7..e9849e324dc 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -48,25 +48,22 @@ module Loop_invariants_actions = Hook.Make(struct end)
let apply_after_transformation prj =
Project.on prj Loop_invariants_actions.apply ()
-let mv_invariants env ~old stmt =
+let mv_invariants kf ~old stmt =
Options.feedback ~current:true ~level:3
"keep loop invariants attached to its loop";
- match Env.current_kf env with
- | None -> assert false
- | Some kf ->
- let filter _ ca = match ca.annot_content with
- | AInvariant(_, b, _) -> b
- | _ -> false
- in
- let l = Annotations.code_annot_emitter ~filter stmt in
- if l != [] then
- Loop_invariants_actions.extend
- (fun () ->
- List.iter
- (fun (ca, e) ->
- Annotations.remove_code_annot e ~kf old ca;
- Annotations.add_code_annot e ~kf stmt ca)
- l)
+ let filter _ ca = match ca.annot_content with
+ | AInvariant(_, b, _) -> b
+ | _ -> false
+ in
+ let l = Annotations.code_annot_emitter ~filter stmt in
+ if l != [] then
+ Loop_invariants_actions.extend
+ (fun () ->
+ List.iter
+ (fun (ca, e) ->
+ Annotations.remove_code_annot e ~kf old ca;
+ Annotations.add_code_annot e ~kf stmt ca)
+ l)
let preserve_invariant prj env kf stmt = match stmt.skind with
| Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
@@ -219,11 +216,11 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
with Typing.Not_a_number -> assert false
in
(* loop counter corresponding to the quantified variable *)
- let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
+ let var_x, x, env = Env.Logic_binding.add ~ty env kf logic_x in
let lv_x = var var_x in
let env = match ctx_one with
| Typing.C_integer _ -> env
- | Typing.Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
+ | Typing.Gmpz -> Env.add_stmt env kf (Gmp.init ~loc x)
| Typing.(C_float _ | Rational | Real | Nan) -> assert false
in
(* build the inner loops and loop body *)
@@ -301,7 +298,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
[ start ; stmt ], env
| Lscope.Lvs_let(lv, t) :: lscope_vars' ->
let ty = Typing.get_typ t in
- let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env lv in
+ let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
let e, env = term_to_exp kf env t in
let ty = Cil.typeOf e in
let init_set =
diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
index ffe13fb4af4..a55e09d7a65 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.mli
+++ b/src/plugins/e-acsl/src/code_generator/loops.mli
@@ -30,7 +30,7 @@ open Cil_types
val apply_after_transformation: Project.t -> unit
-val mv_invariants: Env.t -> old:stmt -> stmt -> unit
+val mv_invariants: kernel_function -> old:stmt -> stmt -> unit
(** Transfer the loop invariants from the [old] loop to the new one.
Both statements must be loops. *)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.ml b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
index 2004c9a510e..f3a3805994a 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
@@ -27,8 +27,7 @@ let tracking_stmt ?before fold mk_stmt env kf vars =
fold
(fun vi env ->
if Mmodel_analysis.must_model_vi ~kf vi then
- let vi = Visitor_behavior.Get.varinfo (Env.get_behavior env) vi in
- Env.add_stmt ?before env (mk_stmt vi)
+ Env.add_stmt ?before env kf (mk_stmt vi)
else
env)
vars
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index 036b3089c25..4d80c4d8cc2 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -121,6 +121,7 @@ let call ~loc kf name ctx env t =
~loc
~name
env
+ kf
None
ctx
(fun v _ ->
@@ -154,6 +155,7 @@ let gmp_to_sizet ~loc kf env size p =
~loc
~name:"size"
env
+ kf
None
sizet
(fun vi _ ->
@@ -230,6 +232,7 @@ let call_memory_block ~loc kf name ctx env ptr r p =
~loc
~name
env
+ kf
None
ctx
(fun v _ ->
@@ -337,6 +340,7 @@ let call_with_size ~loc kf name ctx env t p =
~loc
~name
env
+ kf
None
ctx
(fun v _ ->
@@ -374,6 +378,7 @@ let call_valid ~loc kf name ctx env t p =
~loc
~name
env
+ kf
None
ctx
(fun v _ ->
@@ -394,3 +399,9 @@ let call_valid ~loc kf name ctx env t p =
t
p
call_for_unsupported_constructs
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 4a618c5b806..2ad62b7b950 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -169,6 +169,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
~loc
~name
env
+ kf
None
intType
(fun v _ ->
@@ -204,7 +205,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
in
let env =
- Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
+ Env.add_stmt env kf (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
in
(* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
@@ -212,7 +213,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let label = Label(label_name, loc, false) in
end_loop.labels <- label :: end_loop.labels;
end_loop_ref := end_loop;
- let env = Env.add_stmt env end_loop in
+ let env = Env.add_stmt env kf end_loop in
res, env
end
@@ -229,6 +230,6 @@ let quantif_to_exp kf env p =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 427e9ef5650..8145541f8c0 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -30,7 +30,7 @@ let init_set ~loc lval vi_e e =
[ Gmp.init ~loc vi_e ;
Gmp.affect ~loc lval vi_e e ]))
-let create ~loc ?name e env t_opt =
+let create ~loc ?name e env kf t_opt =
let ty = Cil.typeOf e in
if Gmp_types.Z.is_t ty then
(* GMPQ has no builtin for creating Q from Z. Hence:
@@ -45,6 +45,7 @@ let create ~loc ?name e env t_opt =
~loc
?name
env
+ kf
t_opt
(Gmp_types.Q.t ())
(fun vi vi_e ->
@@ -138,7 +139,7 @@ let cast_to_z ~loc:_ ?name:_ e _env =
assert (Gmp_types.Q.is_t (Cil.typeOf e));
Error.not_yet "reals: cast from R to Z"
-let add_cast ~loc ?name e env ty =
+let add_cast ~loc ?name e env kf ty =
(* TODO: The best solution would actually be to directly write all the needed
functions as C builtins then just call them here depending on the situation
at hand. *)
@@ -149,6 +150,7 @@ let add_cast ~loc ?name e env ty =
~loc
?name
env
+ kf
None
Cil.doubleType
(fun v _ ->
@@ -182,15 +184,18 @@ let add_cast ~loc ?name e env ty =
| _ ->
Error.not_yet "R to <typ>"
-let cmp ~loc bop e1 e2 env t_opt =
+let cmp ~loc bop e1 e2 env kf t_opt =
let fname = "__gmpq_cmp" in
let name = Misc.name_of_binop bop in
- let e1, env = create ~loc e1 env None (* TODO: t1_opt could be provided *) in
- let e2, env = create ~loc e2 env None (* TODO: t2_opt could be provided *) in
+ (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
+ [e2] *)
+ let e1, env = create ~loc e1 env kf None in
+ let e2, env = create ~loc e2 env kf None in
let _, e, env =
Env.new_var
~loc
env
+ kf
t_opt
~name
Cil.intType
@@ -198,12 +203,13 @@ let cmp ~loc bop e1 e2 env t_opt =
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
-let new_var_and_init ~loc ?scope ?name env t_opt mk_stmts =
+let new_var_and_init ~loc ?scope ?name env kf t_opt mk_stmts =
Env.new_var
~loc
?scope
?name
env
+ kf
t_opt
(Gmp_types.Q.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
@@ -216,13 +222,15 @@ let name_arith_bop = function
| Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
| Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
-let binop ~loc bop e1 e2 env t_opt =
+let binop ~loc bop e1 e2 env kf t_opt =
let name = name_arith_bop bop in
- let e1, env = create ~loc e1 env None (* TODO: t1_opt could be provided *) in
- let e2, env = create ~loc e2 env None (* TODO: t2_opt could be provided *) in
+ (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
+ [e2] *)
+ let e1, env = create ~loc e1 env kf None in
+ let e2, env = create ~loc e2 env kf None in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
- let _, e, env = new_var_and_init ~loc ~name env t_opt mk_stmts in
+ let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
e, env
(*
diff --git a/src/plugins/e-acsl/src/code_generator/rational.mli b/src/plugins/e-acsl/src/code_generator/rational.mli
index c85f97de2b3..e326fb18f9b 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.mli
+++ b/src/plugins/e-acsl/src/code_generator/rational.mli
@@ -22,12 +22,18 @@
(** Generation of rational numbers. *)
+(* [TODO ARCHI]: change the call convention in the whole module *)
+
open Cil_types
-val create: loc:location -> ?name:string -> exp -> Env.t -> term option ->
+(* TODO: change the call convention *)
+val create:
+ loc:location -> ?name:string -> exp -> Env.t -> kernel_function ->
+ term option ->
exp * Env.t
(** Create a real *)
+(* TODO: change the call convention *)
val init_set: loc:location -> lval -> exp -> exp -> stmt
(** [init_set lval lval_as_exp exp] sets [lval] to [exp] while guranteeing that
[lval] is properly initialized wrt the underlying real library. *)
@@ -39,20 +45,29 @@ val normalize_str: string -> string
decimal expansion. In order to make `libgmp` consider it to be a rational,
it must be converted into "1/10". *)
+(* TODO: change the call convention *)
val cast_to_z: loc:location -> ?name:string -> exp -> Env.t -> exp * Env.t
(** Assumes that the given exp is of real type and casts it into Z *)
-val add_cast: loc:location -> ?name:string -> exp -> Env.t -> typ ->
+(* TODO: change the call convention *)
+val add_cast:
+ loc:location -> ?name:string -> exp -> Env.t -> kernel_function -> typ ->
exp * Env.t
(** Assumes that the given exp is of real type and casts it into
the given typ *)
-val binop: loc:location -> binop -> exp -> exp -> Env.t -> term option ->
+(* TODO: change the call convention --> exp at the end *)
+val binop:
+ loc:location -> binop -> exp -> exp -> Env.t -> kernel_function ->
+ term option ->
exp * Env.t
(** Applies [binop] to the given expressions. The optional term
indicates whether the comparison has a correspondance in the logic. *)
-val cmp: loc:location -> binop -> exp -> exp -> Env.t -> term option ->
+(* TODO: change the call convention --> exp at the end *)
+val cmp:
+ loc:location -> binop -> exp -> exp -> Env.t -> kernel_function ->
+ term option ->
exp * Env.t
(** Compares two expressions according to the given [binop]. The optional term
indicates whether the comparison has a correspondance in the logic. *)
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index 1d27b2046c5..9e49453af8a 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -45,25 +45,6 @@ type flow =
| Copy (* Copy shadow from RHS to LHS *)
(* }}} *)
-(* ************************************************************************** *)
-(* Miscellaneous {{{ *)
-(* ************************************************************************** *)
-
-(* Shortcuts for SA in Mmodel_analysis *)
-let must_model_exp exp env =
- let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
- Mmodel_analysis.must_model_exp ~bhv ~kf exp
-
-let must_model_lval lv env =
- let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
- Mmodel_analysis.must_model_lval ~bhv ~kf lv
-
-let must_model_vi vi env =
- let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
- Mmodel_analysis.must_model_vi ~bhv ~kf vi
-
-(* }}} *)
-
(* ************************************************************************* *)
(* Generate analysis function calls {{{ *)
(* ************************************************************************** *)
@@ -233,10 +214,10 @@ let mk_stmt_from_assign loc lhs rhs =
(* ************************************************************************** *)
(* Top-level handler for Set instructions *)
-let set_instr ?(post=false) current_stmt loc lhs rhs env =
- if must_model_lval lhs env then
+let set_instr ?(post=false) current_stmt loc lhs rhs env kf =
+ if Mmodel_analysis.must_model_lval ~kf lhs then
Extlib.may_map
- (fun stmt -> Env.add_stmt ~before:current_stmt ~post env stmt)
+ (fun stmt -> Env.add_stmt ~before:current_stmt ~post env kf stmt)
~dft:env
(mk_stmt_from_assign loc lhs rhs)
else
@@ -249,12 +230,15 @@ let set_instr ?(post=false) current_stmt loc lhs rhs env =
module Function_call: sig
(* Top-level handler for Call instructions *)
- val instr: stmt -> lval option -> exp -> exp list -> location -> Env.t -> Env.t
+ val instr:
+ stmt -> lval option -> exp -> exp list -> location ->
+ Env.t -> kernel_function ->
+ Env.t
end = struct
(* Track function arguments: export referents of arguments to a global
structure so they can be retrieved once that function is called *)
- let save_params current_stmt loc args env =
+ let save_params current_stmt loc args env kf =
let (env, _) = List.fold_left
(fun (env, index) param ->
let lv = Mem(param), NoOffset in
@@ -263,9 +247,9 @@ end = struct
Extlib.may_map
(fun (_, rhs, flow) ->
let env =
- if must_model_exp param env then
+ if Mmodel_analysis.must_model_exp ~kf param then
let stmt = Mk.save_param ~loc flow rhs index in
- Env.add_stmt ~before:current_stmt ~post:false env stmt
+ Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else env
in
(env, index+1))
@@ -277,7 +261,7 @@ end = struct
(* Update local environment with a statement tracking temporal metadata
associated with assignment [ret] = [func(args)]. *)
- let call_with_ret ?(alloc=false) current_stmt loc ret env =
+ let call_with_ret ?(alloc=false) current_stmt loc ret env kf =
let rhs = Cil.new_exp ~loc (Lval ret) in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
@@ -308,24 +292,24 @@ end = struct
else
Mk.handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
in
- Env.add_stmt ~before:current_stmt ~post:true env stmt)
+ Env.add_stmt ~before:current_stmt ~post:true env kf stmt)
~dft:env
vals
(* Update local environment with a statement tracking temporal metadata
associated with memcpy/memset call *)
- let call_memxxx current_stmt loc args fexp env =
+ let call_memxxx current_stmt loc args fexp env kf =
if Libc.is_memcpy fexp || Libc.is_memset fexp then
let name = match fexp.enode with
| Lval(Var vi, _) -> vi.vname
| _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
in
let stmt = Misc.mk_call ~loc (RTL.mk_temporal_name name) args in
- Env.add_stmt ~before:current_stmt ~post:false env stmt
+ Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else
env
- let instr current_stmt ret fexp args loc env =
+ let instr current_stmt ret fexp args loc env kf =
(* Add function calls to reset_parameters and reset_return before each
function call regardless. They are not really required, as if the
instrumentation is correct then the right parameters will be saved
@@ -335,27 +319,27 @@ end = struct
be able to optimize that code out. *)
let name = (RTL.mk_temporal_name "reset_parameters") in
let stmt = Misc.mk_call ~loc name [] in
- let env = Env.add_stmt ~before:current_stmt ~post:false env stmt in
+ let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
let stmt = Mk.reset_return_referent ~loc in
- let env = Env.add_stmt ~before:current_stmt ~post:false env stmt in
+ let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
(* Push parameters with either a call to a function pointer or a function
definition otherwise there is no point. *)
let has_def = Functions.has_fundef fexp in
let env =
if Cil.isFunctionType (Cil.typeOf fexp) || has_def then
- save_params current_stmt loc args env
+ save_params current_stmt loc args env kf
else
env
in
(* Handle special cases of memcpy/memset *)
- let env = call_memxxx current_stmt loc args fexp env in
+ let env = call_memxxx current_stmt loc args fexp env kf in
(* Memory allocating functions have no definitions so below expression
should capture them *)
let alloc = not has_def in
Extlib.may_map
(fun lhs ->
- if must_model_lval lhs env then
- call_with_ret ~alloc current_stmt loc lhs env
+ if Mmodel_analysis.must_model_lval ~kf lhs then
+ call_with_ret ~alloc current_stmt loc lhs env kf
else env)
~dft:env
ret
@@ -367,30 +351,33 @@ end
(* ************************************************************************** *)
module Local_init: sig
(* Top-level handler for Local_init instructions *)
- val instr: stmt -> varinfo -> local_init -> location -> Env.t -> Env.t
+ val instr:
+ stmt -> varinfo -> local_init -> location -> Env.t -> kernel_function ->
+ Env.t
end = struct
- let rec handle_init current_stmt offset loc vi init env =
- match init with
+ let rec handle_init current_stmt offset loc vi init env kf = match init with
| SingleInit exp ->
- set_instr ~post:true current_stmt loc (Var vi, offset) exp env
+ set_instr ~post:true current_stmt loc (Var vi, offset) exp env kf
| CompoundInit(_, inits) ->
List.fold_left
(fun acc (off, init) ->
- handle_init current_stmt (Cil.addOffset off offset) loc vi init acc)
+ let off = Cil.addOffset off offset in
+ handle_init current_stmt off loc vi init acc kf)
env
inits
- let instr current_stmt vi li loc env =
- if must_model_vi vi env then
+ let instr current_stmt vi li loc env kf =
+ if Mmodel_analysis.must_model_vi ~kf vi then
match li with
| AssignInit init ->
- handle_init current_stmt NoOffset loc vi init env
+ handle_init current_stmt NoOffset loc vi init env kf
| ConsInit(fexp, args, _) ->
let ret = Some (Cil.var vi) in
let fexp = Cil.evar ~loc fexp in
- Function_call.instr current_stmt ret fexp args loc env
- else env
+ Function_call.instr current_stmt ret fexp args loc env kf
+ else
+ env
end
(* }}} *)
@@ -400,13 +387,13 @@ end
(* Update local environment with a statement tracking temporal metadata
associated with adding a function argument to a stack frame *)
-let track_argument ?(typ) param index env =
+let track_argument ?(typ) param index env kf =
let typ = Extlib.opt_conv param.vtype typ in
match Cil.unrollType typ with
| TPtr _
| TComp _ ->
let stmt = Mk.pull_param ~loc:Location.unknown param index in
- Env.add_stmt ~post:false env stmt
+ Env.add_stmt ~post:false env kf stmt
| TInt _ | TFloat _ | TEnum _ | TBuiltin_va_list _ -> env
| TNamed _ -> assert false
| TVoid _ |TArray _ | TFun _ ->
@@ -419,20 +406,20 @@ let track_argument ?(typ) param index env =
(* Update local environment [env] with statements tracking return value
of a function. *)
-let handle_return_stmt loc ret env =
+let handle_return_stmt loc ret env kf =
match ret.enode with
| Lval lv ->
if Cil.isPointerType (Cil.typeOfLval lv) then
let exp = Cil.mkAddrOf ~loc lv in
let stmt = Mk.handle_return_referent ~loc ~save:true exp in
- Env.add_stmt ~post:false env stmt
+ Env.add_stmt ~post:false env kf stmt
else
env
| _ -> Options.fatal "Something other than Lval in return"
-let handle_return_stmt loc ret env =
- if must_model_exp ret env then
- handle_return_stmt loc ret env
+let handle_return_stmt loc ret env kf =
+ if Mmodel_analysis.must_model_exp ~kf ret then
+ handle_return_stmt loc ret env kf
else
env
(* }}} *)
@@ -443,14 +430,18 @@ let handle_return_stmt loc ret env =
(* Update local environment [env] with statements tracking
instruction [instr] *)
-let handle_instruction current_stmt instr env =
+let handle_instruction current_stmt instr env kf =
match instr with
- | Set(lv, exp, loc) -> set_instr current_stmt loc lv exp env
+ | Set(lv, exp, loc) ->
+ set_instr current_stmt loc lv exp env kf
| Call(ret, fexp, args, loc) ->
- Function_call.instr current_stmt ret fexp args loc env
- | Local_init(vi, li, loc) -> Local_init.instr current_stmt vi li loc env
- | Asm _ -> Options.warning ~once:true ~current:true "@[Analysis is\
-potentially incorrect in presence of assembly code.@]"; env
+ Function_call.instr current_stmt ret fexp args loc env kf
+ | Local_init(vi, li, loc) ->
+ Local_init.instr current_stmt vi li loc env kf
+ | Asm _ ->
+ Options.warning ~once:true ~current:true
+ "@[Analysis is potentially incorrect in presence of assembly code.@]";
+ env
| Skip _ | Code_annot _ -> env
(* }}} *)
@@ -462,7 +453,7 @@ potentially incorrect in presence of assembly code.@]"; env
at offset [off] return [Some stmt], where [stmt] is a statement
tracking that initialization. If [init] does not need to be tracked than
the return value is [None] *)
-let mk_global_init ~loc vi off init env =
+let mk_global_init ~loc vi off init =
let exp = match init with
| SingleInit e -> e
(* Compound initializers should have been thrown away at this point *)
@@ -484,7 +475,6 @@ let mk_global_init ~loc vi off init env =
in
(* The input [vi] is from the old project, so get the corresponding variable
from the new one, otherwise AST integrity is violated *)
- let vi = Visitor_behavior.Get.varinfo (Env.get_behavior env) vi in
let lv = Var vi, off in
mk_stmt_from_assign loc lv exp
(* }}} *)
@@ -497,33 +487,33 @@ let handle_function_parameters kf env =
if is_enabled () then
let env, _ = List.fold_left
(fun (env, index) param ->
- let param = Visitor_behavior.Get.varinfo (Env.get_behavior env) param in
let env =
- if Mmodel_analysis.must_model_vi ~kf param then
- track_argument param index env
+ if Mmodel_analysis.must_model_vi ~kf param
+ then track_argument param index env kf
else env
- in env, index + 1)
+ in
+ env, index + 1)
(env, 0)
(Kernel_function.get_formals kf)
in env
else
env
-let handle_stmt stmt env =
+let handle_stmt stmt env kf =
if is_enabled () then begin
match stmt.skind with
- | Instr instr -> handle_instruction stmt instr env
+ | Instr instr -> handle_instruction stmt instr env kf
| Return(ret, loc) -> Extlib.may_map
- (fun ret -> handle_return_stmt loc ret env) ~dft:env ret
+ (fun ret -> handle_return_stmt loc ret env kf) ~dft:env ret
| Goto _ | Break _ | Continue _ | If _ | Switch _ | Loop _ | Block _
| UnspecifiedSequence _ | Throw _ | TryCatch _ | TryFinally _
| TryExcept _ -> env
end else
env
-let generate_global_init vi off init env =
+let generate_global_init vi off init =
if is_enabled () then
- mk_global_init ~loc:vi.vdecl vi off init env
+ mk_global_init ~loc:vi.vdecl vi off init
else
None
(* }}} *)
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.mli b/src/plugins/e-acsl/src/code_generator/temporal.mli
index d996adf9d51..cf0f41843d5 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.mli
+++ b/src/plugins/e-acsl/src/code_generator/temporal.mli
@@ -23,23 +23,26 @@
(** Transformations to detect temporal memory errors (e.g., dereference of
stale pointers). *)
+open Cil_types
+
+(* [TODO ARCHI]: change the call convention in this module *)
+
val enable: bool -> unit
(** Enable/disable temporal transformations *)
val is_enabled: unit -> bool
(** Return a boolean value indicating whether temporal analysis is enabled *)
-val handle_function_parameters: Cil_types.kernel_function -> Env.t -> Env.t
+val handle_function_parameters: kernel_function -> Env.t -> Env.t
(** [handle_function_parameters kf env] updates the local environment [env],
according to the parameters of [kf], with statements allowing to track
referent numbers across function calls. *)
-val handle_stmt: Cil_types.stmt -> Env.t -> Env.t
+val handle_stmt: stmt -> Env.t -> kernel_function -> Env.t
(** Update local environment ([Env.t]) with statements tracking temporal
properties of memory blocks *)
-val generate_global_init: Cil_types.varinfo -> Cil_types.offset ->
- Cil_types.init -> Env.t -> Cil_types.stmt option
+val generate_global_init: varinfo -> offset -> init -> stmt option
(** Generate [Some s], where [s] is a statement tracking global initializer
or [None] if there is no need to track it *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index b981e283a8d..9433bd739e7 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -69,13 +69,14 @@ type strnum =
| C_number (* integers and floats included *)
(* convert [e] in a way that it is compatible with the given typing context. *)
-let add_cast ~loc ?name env ctx strnum t_opt e =
+let add_cast ~loc ?name env kf ctx strnum t_opt e =
let mk_mpz e =
let _, e, env =
Env.new_var
~loc
?name
env
+ kf
t_opt
(Gmp_types.Z.t ())
(fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
@@ -84,7 +85,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
in
let e, env = match strnum with
| Str_Z -> mk_mpz e
- | Str_R -> Rational.create ~loc ?name e env t_opt
+ | Str_R -> Rational.create ~loc ?name e env kf t_opt
| C_number -> e, env
in
match ctx with
@@ -115,8 +116,10 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
mk_mpz e
| _, false ->
if Gmp_types.Q.is_t ctx then
- if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *) e, env
- else (* C integer or Z --> R *) Rational.create ~loc ?name e env t_opt
+ if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *)
+ e, env
+ else (* C integer or Z --> R *)
+ Rational.create ~loc ?name e env kf t_opt
else if Gmp_types.Z.is_t ty || strnum = Str_Z then
(* Z --> C type or the integer is represented by a string:
anyway, it fits into a C integer: convert it *)
@@ -129,6 +132,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
~loc
?name
env
+ kf
None
new_ty
(fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e ] ])
@@ -136,7 +140,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
e, env
else if Gmp_types.Q.is_t ty || strnum = Str_R then
(* R --> C type or the real is represented by a string *)
- Rational.add_cast ~loc ?name e env ctx
+ Rational.add_cast ~loc ?name e env kf ctx
else
(* C type --> another C type *)
Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
@@ -183,7 +187,7 @@ let constant_to_exp ~loc t c =
else mk_real lr.r_literal
| LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), C_number
-let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
+let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
let env = Env.pop (Env.pop env3) in
match e1.enode with
| Const(CInt64(n, _, _)) when Integer.is_zero n ->
@@ -200,6 +204,7 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
~loc
~name
env
+ kf
t_opt
ty
(fun v ev ->
@@ -224,19 +229,14 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
let rec thost_to_host kf env th = match th with
| TVar { lv_origin = Some v } ->
- let v' = Visitor_behavior.Get.varinfo (Env.get_behavior env) v in
- Var v', env, v.vname
+ Var v, env, v.vname
| TVar ({ lv_origin = None } as logic_v) ->
let v' = Env.Logic_binding.get env logic_v in
Var v', env, logic_v.lv_name
| TResult _typ ->
- let vis = Env.get_visitor env in
- let kf = Extlib.the vis#current_kf in
let lhost = Misc.result_lhost kf in
(match lhost with
- | Var v ->
- let v' = Visitor_behavior.Get.varinfo (Env.get_behavior env) v in
- Var v', env, "result"
+ | Var v -> Var v, env, "result"
| _ -> assert false)
| TMem t ->
let e, env = term_to_exp kf env t in
@@ -294,6 +294,7 @@ and context_insensitive_term_to_exp kf env t =
Env.new_var_and_mpz_init
~loc
env
+ kf
~name:vname
(Some t)
(fun _ ev -> [ Misc.mk_call ~loc name [ ev; e ] ])
@@ -328,11 +329,11 @@ and context_insensitive_term_to_exp kf env t =
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env =
- Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
+ Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
- let e, env = Rational.binop ~loc bop e1 e2 env (Some t) in
+ let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
e, env, C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
@@ -361,8 +362,6 @@ and context_insensitive_term_to_exp kf env t =
in
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
- let vis = Env.get_visitor env in
- let kf = Extlib.the vis#current_kf in
let cond =
Misc.mk_e_acsl_guard
(Env.annotation_kind env)
@@ -375,10 +374,10 @@ and context_insensitive_term_to_exp kf env t =
[ cond; instr ]
in
let name = Misc.name_of_binop bop in
- let _, e, env = Env.new_var_and_mpz_init ~loc ~name env t mk_stmts in
+ let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
- let e, env = Rational.binop ~loc bop e1 e2 env (Some t) in
+ let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
e, env, C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
@@ -399,7 +398,7 @@ and context_insensitive_term_to_exp kf env t =
let env' = Env.push env1 in
let res2 = term_to_exp kf (Env.push env') t2 in
let e, env =
- conditional_to_exp ~name:"or" loc (Some t) e1 (Cil.one loc, env') res2
+ conditional_to_exp ~name:"or" loc kf (Some t) e1 (Cil.one loc, env') res2
in
e, env, C_number, ""
| TBinOp(LAnd, t1, t2) ->
@@ -408,7 +407,8 @@ and context_insensitive_term_to_exp kf env t =
let _, env2 as res2 = term_to_exp kf (Env.push env1) t2 in
let env3 = Env.push env2 in
let e, env =
- conditional_to_exp ~name:"and" loc (Some t) e1 res2 (Cil.zero loc, env3)
+ conditional_to_exp
+ ~name:"and" loc kf (Some t) e1 res2 (Cil.zero loc, env3)
in
e, env, C_number, ""
| TBinOp((BOr | BXor | BAnd), _, _) ->
@@ -443,7 +443,7 @@ and context_insensitive_term_to_exp kf env t =
| TCastE(ty, t') ->
let e, env = term_to_exp kf env t' in
let e, env =
- add_cast ~loc ~name:"cast" env (Some ty) C_number (Some t) e
+ add_cast ~loc ~name:"cast" env kf (Some ty) C_number (Some t) e
in
e, env, C_number, ""
| TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
@@ -477,6 +477,7 @@ and context_insensitive_term_to_exp kf env t =
~loc
~name:(fname ^ "_app")
env
+ kf
(Some t)
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
@@ -491,7 +492,7 @@ and context_insensitive_term_to_exp kf env t =
let e, env =
try
let ty = Typing.typ_of_number_ty param_ty in
- add_cast loc env (Some ty) C_number (Some targ) e
+ add_cast loc env kf (Some ty) C_number (Some targ) e
with Typing.Not_a_number ->
e, env
in
@@ -502,7 +503,7 @@ and context_insensitive_term_to_exp kf env t =
let gen_fname =
Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
in
- Logic_functions.tapp_to_exp ~loc gen_fname env t li params_ty args
+ Logic_functions.tapp_to_exp ~loc gen_fname env kf t li params_ty args
in
e, env, C_number, "app"
| Tapp(_, _ :: _, _) ->
@@ -513,7 +514,7 @@ and context_insensitive_term_to_exp kf env t =
let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
let (_, env2 as res2) = term_to_exp kf (Env.push env1) t2 in
let res3 = term_to_exp kf (Env.push env2) t3 in
- let e, env = conditional_to_exp loc (Some t) e1 res2 res3 in
+ let e, env = conditional_to_exp loc kf (Some t) e1 res2 res3 in
e, env, C_number, ""
| Tat(t, BuiltinLabel Here) ->
let e, env = term_to_exp kf env t in
@@ -526,7 +527,7 @@ and context_insensitive_term_to_exp kf env t =
e, env, C_number, ""
else
let e, env = term_to_exp kf (Env.push env) t' in
- let e, env, sty = at_to_exp_no_lscope env (Some t) label e in
+ let e, env, sty = at_to_exp_no_lscope env kf (Some t) label e in
e, env, sty, ""
| Tbase_addr(BuiltinLabel Here, t) ->
let name = "base_addr" in
@@ -580,6 +581,7 @@ and term_to_exp kf env t =
~loc:t.term_loc
?name
env
+ kf
cast
sty
(Some t)
@@ -603,6 +605,7 @@ and comparison_to_exp
let _, e, env = Env.new_var
~loc
env
+ kf
t_opt
~name
Cil.intType
@@ -611,12 +614,12 @@ and comparison_to_exp
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
| Typing.Rational ->
- Rational.cmp ~loc bop e1 e2 env t_opt
+ Rational.cmp ~loc bop e1 e2 env kf t_opt
| Typing.Real ->
Error.not_yet "comparison involving real numbers"
-and at_to_exp_no_lscope env t_opt label e =
- let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
+and at_to_exp_no_lscope env kf t_opt label e =
+ let stmt = E_acsl_label.get_stmt label in
(* generate a new variable denoting [\at(t',label)].
That is this variable which is the resulting expression.
ACSL typing rule ensures that the type of this variable is the same as
@@ -628,6 +631,7 @@ and at_to_exp_no_lscope env t_opt label e =
~name:"at"
~scope:Varname.Function
env
+ kf
t_opt
(Cil.typeOf e)
(fun _ _ -> [])
@@ -656,17 +660,15 @@ and at_to_exp_no_lscope env t_opt label e =
Cil.ChangeTo stmt
end
in
- let bhv = Env.get_behavior new_env in
- let new_stmt =
- Visitor.visitFramacStmt o (Visitor_behavior.Get.stmt bhv stmt)
- in
- Visitor_behavior.Set.stmt bhv stmt new_stmt;
+ let _new_stmt = Visitor.visitFramacStmt o stmt in
+ (* [TODO ARCHI] reimplement *)
+ (*Visitor_behavior.Set.stmt bhv stmt new_stmt;*)
res, !env_ref, C_number
and env_of_li li kf env loc =
let t = Misc.term_of_li li in
let ty = Typing.get_typ t in
- let vi, vi_e, env = Env.Logic_binding.add ~ty env li.l_var_info in
+ let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
@@ -678,7 +680,7 @@ and env_of_li li kf env loc =
| Typing.Real ->
Error.not_yet "real number"
in
- Env.add_stmt env stmt
+ Env.add_stmt env kf stmt
(* Convert an ACSL named predicate into a corresponding C expression (if
any) in the given environment. Also extend this environment which includes
@@ -715,14 +717,14 @@ and named_predicate_content_to_exp ?name kf env p =
named_predicate_to_exp kf (Env.push env1) p2 in
let env3 = Env.push env2 in
let name = match name with None -> "and" | Some n -> n in
- conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
+ conditional_to_exp ~name loc kf None e1 res2 (Cil.zero loc, env3)
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
let env' = Env.push env1 in
let res2 = named_predicate_to_exp kf (Env.push env') p2 in
let name = match name with None -> "or" | Some n -> n in
- conditional_to_exp ~name loc None e1 (Cil.one loc, env') res2
+ conditional_to_exp ~name loc kf None e1 (Cil.one loc, env') res2
| Pxor _ -> not_yet env "xor"
| Pimplies(p1, p2) ->
(* (p1 ==> p2) <==> !p1 || p2 *)
@@ -748,7 +750,7 @@ and named_predicate_content_to_exp ?name kf env p =
let (_, env2 as res2) =
named_predicate_to_exp kf (Env.push env1) p2 in
let res3 = named_predicate_to_exp kf (Env.push env2) p3 in
- conditional_to_exp loc None e1 res2 res3
+ conditional_to_exp loc kf None e1 res2 res3
| Plet(li, p) ->
let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
@@ -767,7 +769,7 @@ and named_predicate_content_to_exp ?name kf env p =
else begin
(* convert [t'] to [e] in a separated local env *)
let e, env = named_predicate_to_exp kf (Env.push env) p' in
- let e, env, sty = at_to_exp_no_lscope env None label e in
+ let e, env, sty = at_to_exp_no_lscope env kf None label e in
assert (sty = C_number);
e, env
end
@@ -835,6 +837,7 @@ and named_predicate_to_exp ?name kf ?rte env p =
~loc:p.pred_loc
?name
env
+ kf
cast
C_number
None
@@ -885,6 +888,7 @@ and translate_named_predicate kf env p =
let env = Env.Logic_scope.reset env in
Env.add_stmt
env
+ kf
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) kf e p)
let named_predicate_to_exp ?name kf env p =
@@ -906,8 +910,7 @@ let () =
However, it is correct to use it only in specific contexts. *)
let predicate_to_exp kf p =
Typing.type_named_predicate ~must_clear:true p;
- let empty_env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
- let e, _ = named_predicate_to_exp kf empty_env p in
+ let e, _ = named_predicate_to_exp kf Env.empty p in
assert (Typ.equal (Cil.typeOf e) Cil.intType);
e
@@ -927,8 +930,7 @@ let term_to_exp typ t =
in
let ctx = Extlib.opt_map ctx_of_typ typ in
Typing.type_term ~use_gmp_opt:true ?ctx t;
- let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
- let env = Env.push env in
+ let env = Env.push Env.empty in
let env = Env.rte env false in
let e, env =
try term_to_exp (Kernel_function.dummy ()) env t
diff --git a/src/plugins/e-acsl/src/code_generator/visit.ml b/src/plugins/e-acsl/src/code_generator/visit.ml
index d220b15715e..0083db8f3a0 100644
--- a/src/plugins/e-acsl/src/code_generator/visit.ml
+++ b/src/plugins/e-acsl/src/code_generator/visit.ml
@@ -21,17 +21,12 @@
(**************************************************************************)
module E_acsl_label = Label
-open Cil_types
-open Cil_datatype
-
-let dkey = Options.dkey_translation
(* ************************************************************************** *)
(* Visitor *)
(* ************************************************************************** *)
(* local references to the below visitor and to [do_visit] *)
-let function_env = ref Env.dummy
let dft_funspec = Cil.empty_funspec ()
let funspec = ref dft_funspec
@@ -41,194 +36,10 @@ class e_acsl_visitor prj generate = object (self)
inherit Visitor.generic_frama_c_visitor
(if generate then Visitor_behavior.copy prj else Visitor_behavior.inplace ())
- val mutable main_fct = None
- (* fundec of the main entry point, in the new project [prj].
- [None] while the global corresponding to this fundec has not been
- visited *)
-
val mutable is_initializer = false
(* Global flag set to [true] if a currently visited node
belongs to a global initializer and set to [false] otherwise *)
- method private reset_env () =
- function_env := Env.empty (self :> Visitor.frama_c_visitor)
-
- method !vfile _f =
- (* copy the options used during the visit in the new project: it is the
- right place to do this: it is still before visiting, but after
- that the visitor internals reset all of them :-(. *)
- let cur = Project.current () in
- let selection =
- State_selection.of_list
- [ Options.Gmp_only.self; Options.Check.self; Options.Full_mmodel.self;
- Kernel.SignedOverflow.self; Kernel.UnsignedOverflow.self;
- Kernel.SignedDowncast.self; Kernel.UnsignedDowncast.self;
- Kernel.Machdep.self ]
- in
- if generate then Project.copy ~selection ~src:cur prj;
- Cil.DoChildrenPost
- (fun f ->
- (* extend [main] with forward initialization and put it at end *)
- if generate then begin
- if not (Global_observer.is_empty () && Literal_strings.is_empty ())
- then begin
- let build_initializer () =
- Options.feedback ~dkey ~level:2 "building global initializer.";
- let vi, fundec, env =
- Global_observer.mk_init self#behavior !function_env
- in
- function_env := env;
- let cil_fct = GFun(fundec, Location.unknown) in
- if Mmodel_analysis.use_model () then
- match main_fct with
- | Some main ->
- let exp = Cil.evar ~loc:Location.unknown vi in
- (* Create [__e_acsl_globals_init();] call *)
- let stmt =
- Cil.mkStmtOneInstr ~valid_sid:true
- (Call(None, exp, [], Location.unknown))
- in
- vi.vreferenced <- true;
- (* insert [__e_acsl_globals_init ();] as first statement of
- [main] *)
- main.sbody.bstmts <- stmt :: main.sbody.bstmts;
- let new_globals =
- List.fold_right
- (fun g acc -> match g with
- | GFun({ svar = vi }, _)
- when Varinfo.equal vi main.svar ->
- acc
- | _ -> g :: acc)
- f.globals
- [ cil_fct; GFun(main, Location.unknown) ]
- in
- (* add the literal string varinfos as the very first
- globals *)
- let new_globals =
- Literal_strings.fold
- (fun _ vi l ->
- GVar(vi, { init = None }, Location.unknown) :: l)
- new_globals
- in
- f.globals <- new_globals
- | None ->
- Kernel.warning "@[no entry point specified:@ \
-you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
- Global_observer.function_name;
- f.globals <- f.globals @ [ cil_fct ]
- in
- Project.on prj build_initializer ()
- end; (* must_init *)
- (* Add a call to [__e_acsl_memory_init] that initializes memory
- storage and potentially records program arguments. Parameters to
- [__e_acsl_memory_init] are addresses of program arguments or
- NULLs if [main] is declared without arguments. *)
- let build_mmodel_initializer () =
- let loc = Location.unknown in
- let nulls = [ Cil.zero loc ; Cil.zero loc ] in
- let handle_main main =
- let args =
- (* record arguments only if the second has a pointer type, so a
- argument strings can be recorded. This is sufficient to
- capture C99 compliant arguments and GCC extensions with
- environ. *)
- match main.sformals with
- | [] ->
- (* no arguments to main given *)
- nulls
- | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
- (* grab addresses of arguments for a call to the main
- initialization function, i.e., [__e_acsl_memory_init] *)
- List.map Cil.mkAddrOfVi main.sformals;
- | _ :: _ ->
- (* some non-standard arguments. *)
- nulls
- in
- let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
- let args = args @ [ ptr_size ] in
- let name = Functions.RTL.mk_api_name "memory_init" in
- let init = Misc.mk_call loc name args in
- main.sbody.bstmts <- init :: main.sbody.bstmts
- in
- Extlib.may handle_main main_fct
- in
- Project.on
- prj
- (fun () ->
- f.globals <- Logic_functions.add_generated_functions f.globals;
- build_mmodel_initializer ())
- ();
- (* reset copied states at the end to be observationally
- equivalent to a standard visitor. *)
- Project.clear ~selection ~project:prj ();
- end; (* generate *)
- f)
-
- method !vglob_aux = function
- | GVarDecl(vi, _) | GVar(vi, _, _)
- | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
- when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
- if generate then
- Cil.JustCopyPost
- (fun l ->
- let new_vi = Visitor_behavior.Get.varinfo self#behavior vi in
- if Misc.is_library_loc vi.vdecl then
- Misc.register_library_function new_vi;
- if Builtins.mem vi.vname then Builtins.update vi.vname new_vi;
- l)
- else begin
- Misc.register_library_function vi;
- Cil.SkipChildren
- end
- | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
- when Cil.is_builtin vi ->
- if generate then Cil.JustCopy else Cil.SkipChildren
- | g when Misc.is_library_loc (Global.loc g) ->
- if generate then Cil.JustCopy else Cil.SkipChildren
- | g ->
- let unghost_vi vi =
- vi.vghost <- false ;
- vi.vtype <- match vi.vtype with
- | TFun(res, Some l, va, attr) ->
- let retype (n, t, a) =
- (n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a)
- in
- TFun(res, Some (List.map retype l), va, attr)
- | _ ->
- vi.vtype
- in
- let do_it = function
- | GVar(vi, _, _) ->
- unghost_vi vi
- | GFun({ svar = vi } as fundec, _) ->
- unghost_vi vi ;
- Builtins.update vi.vname vi;
- (* remember that we have to remove the main later (see method
- [vfile]); do not use the [vorig_name] since both [main] and
- [__e_acsl_main] have the same [vorig_name]. *)
- if vi.vname = Kernel.MainFunction.get () then
- main_fct <- Some fundec
- | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
- (* do not convert extern ghost variables, because they can't be linked,
- see bts #1392 *)
- if vi.vstorage <> Extern then
- unghost_vi vi
- | _ ->
- ()
- in
- (match g with
- | GVar(vi, _, _) | GVarDecl(vi, _) | GFun({ svar = vi }, _)
- (* Track function addresses but the main function that is tracked
- internally via RTL *)
- when vi.vorig_name <> Kernel.MainFunction.get () ->
- (* Make a unique mapping for each global variable omitting initializers.
- Initializers (used to capture literal strings) are added to
- [global_vars] via the [vinit] visitor method (see comments below). *)
- Global_observer.add (Visitor_behavior.Get_orig.varinfo self#behavior vi)
- | _ -> ());
- if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
- else Cil.DoChildren
-
(* Add mappings from global variables to their initializers in [global_vars].
Note that the below function captures only [SingleInit]s. All compound
initializers containing SingleInits (except for empty compound
@@ -270,57 +81,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
());
Cil.SkipChildren
- method private add_generated_variables_in_function f =
- assert generate;
- let vars = Env.get_generated_variables !function_env in
- self#reset_env ();
- let locals, blocks =
- List.fold_left
- (fun (local_vars, block_vars as acc) (v, scope) -> match scope with
- (* TODO: [kf] assumed to be consistent. Should be asserted. *)
- | Env.LFunction _kf -> v :: local_vars, v :: block_vars
- | Env.LLocal_block _kf -> v :: local_vars, block_vars
- | _ -> acc)
- (f.slocals, f.sbody.blocals)
- vars
- in
- f.slocals <- locals;
- f.sbody.blocals <- blocks
-
- (* Memory management for \at on purely logic variables:
- Put [malloc] stmts at proper locations *)
- method private insert_malloc_and_free_stmts kf f =
- let malloc_stmts = At_with_lscope.Malloc.find_all kf in
- let fstmts = malloc_stmts @ f.sbody.bstmts in
- f.sbody.bstmts <- fstmts;
- (* Now that [malloc] stmts for [kf] have been inserted,
- there is no more need to keep the corresponding entries in the
- table managing them. *)
- At_with_lscope.Malloc.remove_all kf
-
- method !vfunc f =
- if generate then begin
- let kf = Extlib.the self#current_kf in
- if Functions.instrument kf then Exit_points.generate f;
- Options.feedback ~dkey ~level:2 "entering in function %a."
- Kernel_function.pretty kf;
- let unghost_formal vi =
- vi.vghost <- false ;
- vi.vattr <- Cil.dropAttribute Cil.frama_c_ghost_formal vi.vattr
- in
- List.iter (fun vi -> vi.vghost <- false) f.slocals;
- List.iter unghost_formal f.sformals;
- Cil.DoChildrenPost
- (fun f ->
- Exit_points.clear ();
- self#add_generated_variables_in_function f;
- self#insert_malloc_and_free_stmts kf f;
- Options.feedback ~dkey ~level:2 "function %a done."
- Kernel_function.pretty kf;
- f)
- end else
- Cil.DoChildren
-
method private is_return old_kf stmt =
let old_ret =
try Kernel_function.find_return old_kf
@@ -672,63 +432,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| _ -> env)
| _ -> env
- method !vblock blk =
- let handle_memory new_blk =
- let kf = Extlib.the self#current_kf in
- let free_stmts = At_with_lscope.Free.find_all kf in
- match new_blk.blocals, free_stmts with
- | [], [] ->
- new_blk
- | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
- let add_locals stmts =
- if Functions.instrument kf then
- List.fold_left
- (fun acc vi ->
- if Mmodel_analysis.must_model_vi ~bhv:self#behavior ~kf vi then
- Misc.mk_delete_stmt vi :: acc
- else
- acc)
- stmts
- new_blk.blocals
- else
- stmts
- in
- let rec insert_in_innermost_last_block blk = function
- | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
- (* keep the return (enclosed in a generated block) at the end;
- preceded by clean if any *)
- let init, tl =
- if self#is_main kf && Mmodel_analysis.use_model () then
- free_stmts @ [ potential_clean; ret ], tl
- else
- free_stmts @ [ ret ], l
- in
- (* Now that [free] stmts for [kf] have been inserted,
- there is no more need to keep the corresponding entries in the
- table managing them. *)
- At_with_lscope.Free.remove_all kf;
- blk.bstmts <-
- List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
- | { skind = Block b } :: _ ->
- insert_in_innermost_last_block b (List.rev b.bstmts)
- | l -> blk.bstmts <-
- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
- in
- insert_in_innermost_last_block new_blk (List.rev new_blk.bstmts);
- if Functions.instrument kf then
- new_blk.bstmts <-
- List.fold_left
- (fun acc vi ->
- if Mmodel_analysis.must_model_vi vi && not vi.vdefined then
- let vi = Visitor_behavior.Get.varinfo self#behavior vi in
- Misc.mk_store_stmt vi :: acc
- else acc)
- new_blk.bstmts
- blk.blocals;
- new_blk
- in
- if generate then Cil.DoChildrenPost handle_memory else Cil.DoChildren
-
(* Processing expressions for the purpose of replacing literal strings found
in the code with variables generated by E-ACSL. *)
method !vexpr _ =
@@ -746,33 +449,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
end else
Cil.SkipChildren
- initializer
- Misc.reset ();
- Logic_functions.reset ();
- Literal_strings.reset ();
- Global_observer.reset ();
- Keep_status.before_translation ();
- self#reset_env ()
-
end
-let do_visit ?(prj=Project.current ()) generate =
- (* The main visitor proceeds by tracking declarations belonging to the
- E-ACSL runtime library and then using these declarations to generate
- statements used in instrumentation. The following code reorders AST
- so declarations belonging to E-ACSL library appear atop of any location
- requiring instrumentation. *)
- Misc.reorder_ast ();
- Options.feedback ~level:2 "%s annotations in %a."
- (if generate then "translating" else "checking")
- Project.pretty prj;
- let vis =
- Extlib.try_finally ~finally:Typing.clear (new e_acsl_visitor prj) generate
- in
- (* explicit type annotation in order to check that no new method is
- introduced by error *)
- (vis : Visitor.frama_c_visitor)
-
(*
Local Variables:
compile-command: "make -C ../.."
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index d638cb7357f..4b0ccaabdf1 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -20,20 +20,7 @@
(* *)
(**************************************************************************)
-let check () =
- Visitor.visitFramacFileSameGlobals (Visit.do_visit false) (Ast.get ());
- let t = Error.nb_untypable () in
- let n = Error.nb_not_yet () in
- let print msg n =
- Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
- n
- (if n > 1 then "s" else "")
- (if n > 1 then "were" else "was")
- msg
- in
- print "untypable" t;
- print "unsupported" n;
- n + t = 0
+let check () = assert false (* [TODO ARCHI] kill check *)
let check =
Dynamic.register
@@ -155,39 +142,30 @@ let generate_code =
Project.on prepared_prj
(fun () ->
let dup_prj = Dup_functions.dup () in
- let cname = Project.get_name dup_prj ^ " (copy)" in
let copied_prj =
- Project.create_by_copy cname ~last:true ~src:dup_prj
- in
- let res =
- Project.on
- copied_prj
- (fun () ->
- Gmp_types.init ();
- Mmodel_analysis.reset ();
- let visit prj = Visit.do_visit ~prj true in
- let prj =
- File.create_project_from_visitor name visit
- in
- Loops.apply_after_transformation prj;
- (* remove the RTE's results computed from E-ACSL:
- they are partial and associated with the wrong
- kernel function (the one of the old project). *)
- let selection =
- State_selection.with_dependencies !Db.RteGen.self
- in
- Project.clear ~selection ~project:prj ();
- Resulting_projects.mark_as_computed ();
- let selection =
- State_selection.singleton Kernel.Files.self
- in
- Project.copy ~selection prj;
- prj)
- ()
+ Project.create_by_copy name ~last:true ~src:dup_prj
in
+ Project.on
+ copied_prj
+ (fun () ->
+ Gmp_types.init ();
+ Mmodel_analysis.reset ();
+ Injector.inject ();
+ (* [TODO ARCHI] remove the project as arguments *)
+ Loops.apply_after_transformation copied_prj;
+ (* remove the RTE's results computed from E-ACSL:
+ they are partial and associated with the wrong
+ kernel function (the one of the old project). *)
+ (* [TODO ARCHI] what if RTE was already computed? *)
+ let selection =
+ State_selection.with_dependencies !Db.RteGen.self
+ in
+ Project.clear ~selection ~project:copied_prj ();
+ Resulting_projects.mark_as_computed ())
+ ();
if Options.Debug.get () = 0 then
Project.remove ~project:dup_prj ();
- res)
+ copied_prj)
()
in
if Options.Debug.get () = 0 then begin
--
GitLab