From 51265d2a8462b72daed951baf2091d4389567043 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 24 Jan 2022 15:11:13 +0100
Subject: [PATCH] [eacsl] Update sources to support the preprocessing of
labeled statements
---
.../e-acsl/src/analyses/exit_points.ml | 46 +++++++++++--
src/plugins/e-acsl/src/analyses/label.ml | 42 +-----------
src/plugins/e-acsl/src/analyses/label.mli | 6 --
.../e-acsl/src/code_generator/assert.ml | 26 +++----
.../e-acsl/src/code_generator/assert.mli | 21 +++---
.../e-acsl/src/code_generator/contract.ml | 43 ++++--------
src/plugins/e-acsl/src/code_generator/env.ml | 5 +-
src/plugins/e-acsl/src/code_generator/env.mli | 7 +-
.../e-acsl/src/code_generator/injector.ml | 42 +++++-------
src/plugins/e-acsl/src/code_generator/libc.ml | 35 +++++-----
.../e-acsl/src/code_generator/libc.mli | 7 +-
.../e-acsl/src/code_generator/logic_array.ml | 6 +-
.../e-acsl/src/code_generator/loops.ml | 6 +-
.../src/code_generator/memory_observer.ml | 16 ++---
.../src/code_generator/memory_observer.mli | 11 ++-
.../src/code_generator/memory_translate.ml | 1 -
.../e-acsl/src/code_generator/quantif.ml | 4 +-
.../e-acsl/src/code_generator/temporal.ml | 68 +++++++++----------
.../code_generator/translate_predicates.ml | 21 +++---
.../src/code_generator/translate_terms.ml | 40 +++++------
.../src/code_generator/translate_utils.ml | 2 +-
src/plugins/e-acsl/src/main.ml | 5 --
22 files changed, 196 insertions(+), 264 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/exit_points.ml b/src/plugins/e-acsl/src/analyses/exit_points.ml
index c1aec33e33f..be83e43663f 100644
--- a/src/plugins/e-acsl/src/analyses/exit_points.ml
+++ b/src/plugins/e-acsl/src/analyses/exit_points.ml
@@ -20,10 +20,14 @@
(* *)
(**************************************************************************)
+module E_acsl_label = Label
open Cil_types
open Cil_datatype
-module Build_env(X: sig type t end): sig
+module Build_env(X: sig
+ type t
+ val map_opt: (t -> t) option
+ end): sig
val add: stmt -> X.t -> unit
val find: stmt -> X.t (* may raise [Not_found] *)
val get_all: stmt -> X.t list
@@ -32,11 +36,24 @@ module Build_env(X: sig type t end): sig
end = struct
let tbl = Stmt.Hashtbl.create 17
- let add = Stmt.Hashtbl.add tbl
+ let add s x =
+ let s = E_acsl_label.get_first_inner_stmt s in
+ Stmt.Hashtbl.add tbl s x
+
+ let find stmt =
+ let res = Stmt.Hashtbl.find tbl stmt in
+ match X.map_opt with
+ | Some map -> map res
+ | None -> res
+
+ let get_all stmt =
+ let res = try Stmt.Hashtbl.find_all tbl stmt with Not_found -> [] in
+ match X.map_opt with
+ | Some map -> List.map map res
+ | None -> res
- let find stmt = Stmt.Hashtbl.find tbl stmt
- let get_all stmt = try Stmt.Hashtbl.find_all tbl stmt with Not_found -> []
let is_empty () = Stmt.Hashtbl.length tbl = 0
+
let clear () = Stmt.Hashtbl.clear tbl
end
@@ -48,7 +65,10 @@ end
scope variables given by set L', then the goto exists the scopes of
variables given via set G' \ L'. Consequently, if those variables are
tracked, they need to be removed from tracking. *)
-module SLocals = Build_env(struct type t = Varinfo.Set.t end)
+module SLocals = Build_env(struct
+ type t = Varinfo.Set.t
+ let map_opt = None
+ end)
(* Statement to statement mapping indicating source/destination of a jump.
For instance, break statements are mapped to switches or loops they jump
@@ -56,11 +76,23 @@ module SLocals = Build_env(struct type t = Varinfo.Set.t end)
such information does not really be computed for gotos (since they already
capture references to labelled statements they jumps to). Nevertheless it is
done for consistency, so all required information is stored uniformly. *)
-module Exits = Build_env(struct type t = stmt end)
+module Exits = Build_env(struct
+ type t = stmt
+ (* Use [Labeled_stmts.get_first_inner_stmt] so that [find] and [get_all]
+ return the first statement of the labeled block instead of the labeled
+ statement. *)
+ let map_opt = Some E_acsl_label.get_first_inner_stmt
+ end)
(* Map labelled statements back to gotos which lead to them and case statements
back to the corresponding switch *)
-module LJumps = Build_env(struct type t = stmt end)
+module LJumps = Build_env(struct
+ type t = stmt
+ (* Use [Labeled_stmts.get_first_inner_stmt] so that [find] and [get_all]
+ return the first statement of the labeled block instead of the labeled
+ statement. *)
+ let map_opt = Some E_acsl_label.get_first_inner_stmt
+ end)
let clear () =
SLocals.clear ();
diff --git a/src/plugins/e-acsl/src/analyses/label.ml b/src/plugins/e-acsl/src/analyses/label.ml
index d97c60f6628..05f6715748a 100644
--- a/src/plugins/e-acsl/src/analyses/label.ml
+++ b/src/plugins/e-acsl/src/analyses/label.ml
@@ -33,46 +33,6 @@ let get_first_inner_stmt stmt =
(Pretty_utils.pp_list ~sep:"; " Cil_types_debug.pp_label) labels
Printer.pp_stmt stmt
-(* The keys are the stmts which were previously labeled, whereas the associated
- values are the new stmts containing the same labels. *)
-module Labeled_stmts =
- Cil_state_builder.Stmt_hashtbl
- (Cil_datatype.Stmt)
- (struct
- let size = 7
- let dependencies = [] (* delayed *)
- let name = "E-ACSL.Labels"
- end)
-
-let self = Labeled_stmts.self
-
-let move kf ~old new_stmt =
- let labels = old.labels in
- match labels with
- | [] -> ()
- | _ :: _ ->
- old.labels <- [];
- new_stmt.labels <- labels @ new_stmt.labels;
- Labeled_stmts.add old new_stmt;
- (* move annotations from the old labeled stmt to the new one *)
- let l = Annotations.fold_code_annot (fun e ca l -> (e, ca) :: l) old [] in
- List.iter
- (fun (e, ca) ->
- Annotations.remove_code_annot ~kf e old ca;
- Annotations.add_code_annot ~keep_empty:false ~kf e new_stmt ca)
- l;
- (* update the gotos of the function jumping to one of the labels *)
- let f =
- try Kernel_function.get_definition kf
- with Kernel_function.No_Definition -> assert false
- in
- let mv_label s = match s.skind with
- | Goto(s_ref, _) when Cil_datatype.Stmt.equal !s_ref old ->
- s_ref := new_stmt
- | _ -> ()
- in
- List.iter mv_label f.sallstmts
-
let get_stmt kf llabel =
let stmt = match llabel with
| StmtLabel { contents = stmt } -> stmt
@@ -90,7 +50,7 @@ let get_stmt kf llabel =
in
(* the pointed statement has been visited and modified by the injector:
get its new version. *)
- try Labeled_stmts.find stmt with Not_found -> stmt
+ get_first_inner_stmt stmt
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/analyses/label.mli b/src/plugins/e-acsl/src/analyses/label.mli
index 195a0042d63..6244536ac72 100644
--- a/src/plugins/e-acsl/src/analyses/label.mli
+++ b/src/plugins/e-acsl/src/analyses/label.mli
@@ -22,15 +22,9 @@
open Cil_types
-val move: kernel_function -> old:stmt -> stmt -> unit
-(** Move all labels of the [old] stmt onto the new [stmt]. *)
-
val get_stmt: kernel_function -> logic_label -> stmt
(** @return the statement where the logic label points to. *)
-val self: State.t
-(** Internal state *)
-
val get_first_inner_stmt: stmt -> stmt
(** If the given statement has a label, return the first statement of the block.
Otherwise return the given statement. *)
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index c512bfa64bc..2321d56a757 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -84,13 +84,13 @@ let with_data_from ~loc kf env from =
"assert_copy_values"
[ adata.data_ptr; from.data_ptr ]
in
- Env.add_stmt env kf stmt
+ Env.add_stmt env stmt
else env
in
Some { adata with data_registered = from.data_registered }, env
| None -> None, env
-let merge_right ~loc kf env adata1 adata2 =
+let merge_right ~loc env adata1 adata2 =
match adata1, adata2 with
| Some adata1, Some adata2 when adata1.data_registered ->
let stmt =
@@ -103,16 +103,16 @@ let merge_right ~loc kf env adata1 adata2 =
{ adata2 with
data_registered = true }
in
- let env = Env.add_stmt env kf stmt in
+ let env = Env.add_stmt env stmt in
Some adata2, env
| Some _, Some adata | None, Some adata -> Some adata, env
| Some _, None | None, None -> None, env
-let clean ~loc kf env adata =
+let clean ~loc env adata =
match adata with
| Some { data_registered; data_ptr } when data_registered->
let clean_stmt = Smart_stmt.rtl_call ~loc "assert_clean" [ data_ptr ] in
- Env.add_stmt env kf clean_stmt
+ Env.add_stmt env clean_stmt
| Some _ | None ->
env
@@ -130,7 +130,7 @@ let ikind_to_string = function
| ILongLong -> "longlong"
| IULongLong -> "ulonglong"
-let do_register_data ~loc kf env { data_ptr } name e =
+let do_register_data ~loc env { data_ptr } name e =
let ty = Cil.typeOf e in
let fct, args =
if Gmp_types.Z.is_t ty then
@@ -160,9 +160,9 @@ let do_register_data ~loc kf env { data_ptr } name e =
let name = Cil.mkString ~loc name in
let args = data_ptr :: name :: args in
let stmt = Smart_stmt.rtl_call ~loc fct args in
- Env.add_stmt env kf stmt
+ Env.add_stmt env stmt
-let register ~loc kf env ?(force=false) name e adata =
+let register ~loc env ?(force=false) name e adata =
if Options.Assert_print_data.get () then
match adata, e.enode with
| Some adata, Const _ when not force ->
@@ -176,23 +176,23 @@ let register ~loc kf env ?(force=false) name e adata =
Some adata, env
| Some adata, _ ->
let adata = { adata with data_registered = true } in
- Some adata, do_register_data ~loc kf env adata name e
+ Some adata, do_register_data ~loc env adata name e
| None, _ -> None, env
else
adata, env
-let register_term ~loc kf env ?force t e adata =
+let register_term ~loc env ?force t e adata =
let name = Format.asprintf "@[%a@]" Printer.pp_term t in
- register ~loc kf env name ?force e adata
+ register ~loc env name ?force e adata
-let register_pred ~loc kf env ?force p e adata =
+let register_pred ~loc env ?force p e adata =
if Env.annotation_kind env == Smart_stmt.RTE then
(* When translating RTE, we do not want to print the result of the predicate
because they should be the only predicate in an assertion clause. *)
adata, env
else
let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
- register ~loc kf env name ?force e adata
+ register ~loc env name ?force e adata
let kind_to_string loc k =
Cil.mkString
diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli
index 016e4830271..d81ed28c982 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.mli
+++ b/src/plugins/e-acsl/src/code_generator/assert.mli
@@ -46,55 +46,52 @@ val with_data_from: loc:location -> kernel_function -> Env.t -> t -> t * Env.t
If [from] is a "no data" assertion context, then the new context is also a
"no data" assertion context. *)
-val merge_right: loc:location -> kernel_function -> Env.t -> t -> t -> t * Env.t
-(** [merge_right ~loc kf env adata1 adata2] merges the assertion data of
- [adata1] into [adata2] if [adata2] is not a "no data" assertion context. *)
+val merge_right: loc:location -> Env.t -> t -> t -> t * Env.t
+(** [merge_right ~loc env adata1 adata2] merges the assertion data of [adata1]
+ into [adata2] if [adata2] is not a "no data" assertion context. *)
-val clean: loc:location -> kernel_function -> Env.t -> t -> Env.t
-(** [clean ~loc kf env adata] generates a call to the C cleanup function for the
+val clean: loc:location -> Env.t -> t -> Env.t
+(** [clean ~loc env adata] generates a call to the C cleanup function for the
assertion context. This function *must* be used if the assertion context is
not given to [runtime_check] or [runtime_check_with_msg], otherwise the
memory allocated in the C structure will not be freed. *)
val register:
loc:location ->
- kernel_function ->
Env.t ->
?force:bool ->
string ->
exp ->
t ->
t * Env.t
-(** [register ~loc kf env ?force name e adata] registers the data [e]
- corresponding to the name [name] to the assertion context [adata].
+(** [register ~loc env ?force name e adata] registers the data [e] corresponding
+ to the name [name] to the assertion context [adata].
If [force] is false (default), the data is not registered if the expression
is a constant. If [force] is true, the data is registered even if the
expression is a constant. *)
val register_term:
loc:location ->
- kernel_function ->
Env.t ->
?force:bool ->
term ->
exp ->
t ->
t * Env.t
-(** [register_term ~loc kf env ?force t e adata] registers the data [e]
+(** [register_term ~loc env ?force t e adata] registers the data [e]
corresponding to the term [t] to the assertion context [adata]. The
parameter [force] has the same signification than for the function
[register]. *)
val register_pred:
loc:location ->
- kernel_function ->
Env.t ->
?force:bool ->
predicate ->
exp ->
t ->
t * Env.t
-(** [register_pred ~loc kf env ?force p e adata] registers the data [e]
+(** [register_pred ~loc env ?force p e adata] registers the data [e]
corresponding to the predicate [p] to the assertion context [adata]. The
parameter [force] has the same signification than for the function
[register]. *)
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 706c8c69780..69d7b48a5e6 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -38,7 +38,7 @@ module Rtl_call: sig
(** Call the C function [__e_acsl_contract_init] *)
val cleanup:
- loc:location -> Env.t -> kernel_function -> exp -> Env.t
+ loc:location -> Env.t -> exp -> Env.t
(** Call the C function [__e_acsl_contract_cleanup] *)
val set_assumes:
@@ -47,17 +47,15 @@ module Rtl_call: sig
(** Call the C function [__e_acsl_contract_set_behavior_assumes] *)
val get_assumes:
- loc:location -> result:varinfo -> Env.t -> kernel_function -> exp -> int ->
- Env.t
+ loc:location -> result:varinfo -> Env.t -> exp -> int -> Env.t
(** Call the C function [__e_acsl_contract_get_behavior_assumes] *)
val partial_count_behaviors:
- loc:location -> result:varinfo -> Env.t -> kernel_function -> exp ->
- int list -> Env.t
+ loc:location -> result:varinfo -> Env.t -> exp -> int list -> Env.t
(** Call the C function [__e_acsl_contract_partial_count_behaviors] *)
val partial_count_all_behaviors:
- loc:location -> result:varinfo -> Env.t -> kernel_function -> exp -> Env.t
+ loc:location -> result:varinfo -> Env.t -> exp -> Env.t
(** Call the C function [__e_acsl_contract_partial_count_all_behaviors] *)
end = struct
@@ -88,10 +86,9 @@ end = struct
init_function_name
[count_e] ])
- let cleanup ~loc env kf contract =
+ let cleanup ~loc env contract =
Env.add_stmt
env
- kf
(Smart_stmt.rtl_call
~loc
"contract_clean"
@@ -108,25 +105,23 @@ end = struct
in
Env.add_stmt
env
- kf
(Smart_stmt.rtl_call
~loc
"contract_set_behavior_assumes"
[contract; idx_e; assumes_e])
- let get_assumes ~loc ~result env kf contract idx =
+ let get_assumes ~loc ~result env contract idx =
let idx_e = Cil.integer ~loc idx in
let result = Cil.var result in
Env.add_stmt
env
- kf
(Smart_stmt.rtl_call
~loc
~result
"contract_get_behavior_assumes"
[contract; idx_e])
- let partial_count_behaviors ~loc ~result env kf contract idxes =
+ let partial_count_behaviors ~loc ~result env contract idxes =
let idxes, count =
List.fold_right
(fun idx (idxes, count) ->
@@ -137,18 +132,16 @@ end = struct
let result = Cil.var result in
Env.add_stmt
env
- kf
(Smart_stmt.rtl_call
~loc
~result
"contract_partial_count_behaviors"
(contract :: Cil.integer ~loc count :: idxes))
- let partial_count_all_behaviors ~loc ~result env kf contract =
+ let partial_count_all_behaviors ~loc ~result env contract =
let result = Cil.var result in
Env.add_stmt
env
- kf
(Smart_stmt.rtl_call
~loc
~result
@@ -214,12 +207,12 @@ let init kf env contract =
else env
(** Cleanup the C API for the given contract *)
-let cleanup kf env contract =
+let cleanup env contract =
match contract.var with
| None -> env
| Some (_, e) ->
let loc = contract.location in
- Rtl_call.cleanup ~loc env kf e
+ Rtl_call.cleanup ~loc env e
(** Retrieve the behavior index from its name for the given contract *)
let get_bhvr_idx contract bhvr_name =
@@ -422,12 +415,11 @@ let check_other_requires kf env contract =
~loc
~result:assumes_vi
env
- kf
contract_e
idx
in
let stmt = Smart_stmt.if_stmt ~loc ~cond:assumes_e requires_blk in
- Env.add_stmt env kf stmt
+ Env.add_stmt env stmt
in
List.fold_left
do_behavior
@@ -477,7 +469,6 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract
~loc
~result:vi
env
- kf
contract_e
in
let complete_msg = "all behaviors complete" in
@@ -498,7 +489,6 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract
~loc
~result:vi
env
- kf
contract_e
args
in
@@ -520,7 +510,6 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract
let adata, env =
Assert.register
~loc
- kf
env
"number of active behaviors"
active_bhvrs_e
@@ -544,16 +533,15 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract
for the given clause *)
Env.add_stmt
env
- kf
(Smart_stmt.if_stmt
~loc
~cond:(Cil.mkBinOp ~loc Ne active_bhvrs_e (Cil.one ~loc))
(Cil.mkBlock [ assert_complete_stmt; assert_disjoint_stmt ]))
(* Otherwise just get the corresponding assertion *)
else if must_translate_complete then
- Env.add_stmt env kf assert_complete_stmt
+ Env.add_stmt env assert_complete_stmt
else if must_translate_disjoint then
- Env.add_stmt env kf assert_disjoint_stmt
+ Env.add_stmt env assert_disjoint_stmt
else
(* By construction, at least either [must_translate_complete] or
[must_translate_disjoint] is true *)
@@ -754,12 +742,11 @@ let check_post_conds kf env contract =
~loc
~result:assumes_vi
env
- kf
contract_e
idx
in
let stmt = Smart_stmt.if_stmt ~loc ~cond:assumes_e post_cond_blk in
- Env.add_stmt env kf stmt
+ Env.add_stmt env stmt
in
List.fold_left
do_behavior
@@ -795,4 +782,4 @@ let translate_postconditions kf env =
env
in
let env = Env.handle_error do_it env in
- cleanup kf env contract
+ cleanup env contract
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index e7ca3032d40..5abf328e729 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -385,9 +385,7 @@ end
let add_assert kf stmt annot =
Annotations.add_assert Options.emitter ~kf stmt annot
-let add_stmt ?(post=false) ?before env kf stmt =
- if not post then
- Option.iter (fun old -> E_acsl_label.move kf ~old stmt) before;
+let add_stmt ?(post=false) env stmt =
let local_env, tl = top env in
let block = local_env.block_info in
let block =
@@ -400,6 +398,7 @@ let add_stmt ?(post=false) ?before env kf stmt =
{ env with env_stack = local_env :: tl }
let extend_stmt_in_place env stmt ~label block =
+ let stmt = E_acsl_label.get_first_inner_stmt stmt in
let new_stmt = Smart_stmt.block_stmt block in
let sk = stmt.skind in
stmt.skind <- Block (Cil.mkBlock [ new_stmt; Smart_stmt.stmt sk ]);
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 19a5b6f59b4..04117ede82a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -90,12 +90,9 @@ val add_assert: kernel_function -> 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 -> kernel_function -> stmt -> t
+val add_stmt: ?post:bool -> t -> 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]
- indicates that [stmt] should be added after the target statement.
- [before] and [post] are mutually exclusive. *)
+ [post] indicates that [stmt] should be added after the target statement. *)
val extend_stmt_in_place: t -> stmt -> label:logic_label -> block -> t
(** [extend_stmt_in_place env stmt ~label b] modifies [stmt] in place in
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 7c3cba1dbcc..0870eb32d4f 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-module E_acsl_label = Label (* [Label] is hidden when opening [Cil_datatype *)
open Cil_types
open Cil_datatype
module Error = Translation_error
@@ -109,12 +108,12 @@ let rec inject_in_init env kf_opt vi off = function
in
CompoundInit(typ, List.rev l), env
-let inject_in_local_init ~loc ~stmt env kf vi = function
+let inject_in_local_init ~loc env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* add a store statement when creating a variable length array *)
let store = Smart_stmt.store_stmt ~str_size:sz vi in
- let env = Env.add_stmt ~post:true env kf store in
+ let env = Env.add_stmt ~post:true env store in
init, env
| ConsInit (caller, args, kind) ->
@@ -123,7 +122,7 @@ let inject_in_local_init ~loc ~stmt env kf vi = function
let _, env =
if Libc.is_writing_memory caller then begin
let result = Var vi, NoOffset in
- Libc.update_memory_model ~loc ~stmt env kf ~result caller args
+ Libc.update_memory_model ~loc env kf ~result caller args
end else
None, env
in
@@ -146,19 +145,18 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
in
let must_model = Memory_tracking.must_monitor_lval ~stmt ~kf lv in
if not (may_safely_ignore lv) && must_model then
- let before = Cil.mkStmt ~valid_sid:true stmt.skind in
let new_stmt =
(* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *)
if Cil.isBitfield lv then Cil.mkEmptyStmt ()
else Smart_stmt.initialize ~loc lv
in
- let env = Env.add_stmt ~post ~before env kf new_stmt in
+ let env = Env.add_stmt ~post env new_stmt in
let env = match vi with
| None -> env
| Some vi ->
let new_stmt = Smart_stmt.store_stmt vi in
- Env.add_stmt ~post ~before env kf new_stmt
+ Env.add_stmt ~post env new_stmt
in
env
else
@@ -186,7 +184,7 @@ let inject_in_instr env kf stmt = function
let result, env =
match caller.enode with
| Lval (Var cvi, _) when Libc.is_writing_memory cvi ->
- Libc.update_memory_model ~loc ~stmt env kf ?result cvi args
+ Libc.update_memory_model ~loc env kf ?result cvi args
| _ -> result, env
in
(* add statement tracking initialization of return values *)
@@ -203,7 +201,7 @@ let inject_in_instr env kf stmt = function
match args with
| [ { enode = CastE (_, { enode = Lval (Var vi, NoOffset) }) } ] ->
let delete_block = Smart_stmt.delete_stmt ~is_addr:true vi in
- Env.add_stmt env kf delete_block
+ Env.add_stmt env delete_block
| _ -> Options.fatal "The normalization of __fc_vla_free() has changed"
else
env
@@ -213,7 +211,7 @@ let inject_in_instr env kf stmt = function
| Local_init(vi, linit, loc) ->
let lv = Var vi, NoOffset in
let env = add_initializer loc ~vi lv ~post:true stmt env kf in
- let linit, env = inject_in_local_init ~loc ~stmt env kf vi linit in
+ let linit, env = inject_in_local_init ~loc env kf vi linit in
Local_init(vi, linit, loc), env
(* nothing to do: *)
@@ -255,7 +253,7 @@ let add_new_block_in_stmt env kf stmt =
let new_stmt, env =
(* Remove local variables which scopes ended via goto/break/continue. *)
let del_vars = Exit_points.delete_vars stmt in
- let env = Memory_observer.delete_from_set ~before:stmt env kf del_vars in
+ let env = Memory_observer.delete_from_set env kf del_vars in
if Kernel_function.is_return_stmt kf stmt then
let env =
if Functions.check kf then
@@ -280,11 +278,6 @@ let add_new_block_in_stmt env kf stmt =
Env.pop_and_get env new_stmt ~global_clear:true Env.After
in
let new_stmt = Smart_stmt.block stmt b in
- if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
- (* move the labels of the return to the new block in order to
- evaluate the postcondition when jumping to them. *)
- E_acsl_label.move kf stmt new_stmt
- end;
new_stmt, env
else (* i.e. not (is_return stmt) *)
(* must generate [pre_block] which includes [stmt] before generating
@@ -319,8 +312,6 @@ let add_new_block_in_stmt env kf stmt =
else post_block
in
let res = Smart_stmt.block new_stmt post_block in
- if not (Cil_datatype.Stmt.equal new_stmt res) then
- E_acsl_label.move kf new_stmt res;
res, env
in
Options.debug ~level:4
@@ -333,7 +324,7 @@ let add_new_block_in_stmt env kf stmt =
The function [last_stmts] receives an optional argument [?return_stmt] with
the innermost return statement if it exists. In that case the function needs
to return this statement as the last statement. *)
-let insert_as_last_stmts_in_innermost_block ~last_stmts kf outer_block =
+let insert_as_last_stmts_in_innermost_block ~last_stmts outer_block =
(* Retrieve the last innermost block *)
let rec retrieve_innermost_last_return block =
let l = List.rev block.bstmts in
@@ -354,7 +345,6 @@ let insert_as_last_stmts_in_innermost_block ~last_stmts kf outer_block =
| Some return_stmt ->
let b = Cil.mkBlock new_stmts in
let new_stmt = Smart_stmt.block return_stmt b in
- E_acsl_label.move kf return_stmt new_stmt;
[ new_stmt ]
| None -> new_stmts
in
@@ -487,7 +477,7 @@ and inject_in_stmt env kf stmt =
(which adds initializers), otherwise init calls appear before store
calls. *)
let duplicates = Exit_points.store_vars stmt in
- let env = Memory_observer.duplicate_store ~before:stmt env kf duplicates in
+ let env = Memory_observer.duplicate_store env kf duplicates in
let skind, env = inject_in_substmt env kf stmt in
stmt.skind <- skind;
(* building the new block of code *)
@@ -541,7 +531,7 @@ and inject_in_block (env: Env.t) kf blk =
stmts
in
(* select the precise location to inject these pieces of code *)
- insert_as_last_stmts_in_innermost_block ~last_stmts kf blk ;
+ insert_as_last_stmts_in_innermost_block ~last_stmts blk ;
(* allocate the memory blocks observing locals *)
if Functions.instrument kf then
blk.bstmts <-
@@ -672,7 +662,7 @@ let inject_in_global main global =
(* Insert [stmt_begin] as the first statement of [fundec] and insert [stmt_end]
as the last before [return] *)
-let surround_function_with kf fundec stmt_begin stmt_end =
+let surround_function_with fundec stmt_begin stmt_end =
let body = fundec.sbody in
(* Insert last statement *)
Option.iter
@@ -682,7 +672,7 @@ let surround_function_with kf fundec stmt_begin stmt_end =
| Some return_stmt -> [ stmt_end; return_stmt ]
| None -> [ stmt_end]
in
- insert_as_last_stmts_in_innermost_block ~last_stmts kf body)
+ insert_as_last_stmts_in_innermost_block ~last_stmts body)
stmt_end;
(* Insert first statement *)
body.bstmts <- stmt_begin :: body.bstmts
@@ -729,7 +719,7 @@ let inject_global_handler file main =
in
(* Surround the content of main with the calls to
[__e_acsl_globals_init();] and [__e_acsl_globals_delete();] *)
- surround_function_with main main_fundec stmt_init stmt_clean_opt;
+ surround_function_with main_fundec stmt_init stmt_clean_opt;
(* Retrieve all globals except main *)
let main_vi = Globals.Functions.get_vi main in
let new_globals =
@@ -820,7 +810,7 @@ let inject_mtracking_handler main =
let args = args @ [ ptr_size ] in
let init = Smart_stmt.rtl_call loc "memory_init" args in
let clean = Smart_stmt.rtl_call loc "memory_clean" [] in
- surround_function_with main fundec init (Some clean)
+ surround_function_with fundec init (Some clean)
in
Option.iter handle_main main
end
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 8b55699909c..9214791359c 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -224,7 +224,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
Logic_const.prel ~loc (Rge, t, Cil.lzero ~loc ())
in
let adata, env = Assert.empty ~loc kf env in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
let assertion, env =
Assert.runtime_check
~adata
@@ -248,9 +248,9 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
let upper_guard_pp = Logic_const.prel ~loc (Rle, t, sizet_max_t) in
let upper_guard = Cil.mkBinOp ~loc Le e sizet_max_e in
let adata, env = Assert.empty ~loc kf env in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
let adata, env =
- Assert.register ~loc kf env "SIZE_MAX" sizet_max_e adata
+ Assert.register ~loc env "SIZE_MAX" sizet_max_e adata
in
let assertion, env =
Assert.runtime_check
@@ -292,7 +292,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
Printer.pp_term t
(** Code generation of [update_memory_model] for [strcat] and [strncat]. *)
-let process_strcat ~loc ~stmt ?result env kf ?size_e dest_e src_e =
+let process_strcat ~loc ?result env kf ?size_e dest_e src_e =
let src_size_vi, src_size_e, src_size_stmt, env =
strlen ~loc ~name:"strcat_src_size" env kf src_e
in
@@ -341,22 +341,21 @@ let process_strcat ~loc ~stmt ?result env kf ?size_e dest_e src_e =
let initialize_blk = Smart_stmt.block_stmt initialize_blk in
let env =
List.fold_right
- (fun pre_stmt env -> Env.add_stmt ~before:stmt env kf pre_stmt)
+ (fun pre_stmt env -> Env.add_stmt env pre_stmt)
pre_stmts
env
in
- let env = Env.add_stmt ~post:true env kf initialize_blk in
+ let env = Env.add_stmt ~post:true env initialize_blk in
result, env
-let update_memory_model ~loc ~stmt ?result env kf caller args =
+let update_memory_model ~loc ?result env kf caller args =
let name = get_caller_name caller in
let post = true in
- let before = stmt in
match name, args with
| "memset", [ dest_e; _; size_e ] | "memcpy", [ dest_e; _; size_e ]
| "memmove", [ dest_e; _; size_e ] ->
let initialize = Smart_stmt.rtl_call ~loc "initialize" [dest_e; size_e] in
- let env = Env.add_stmt ~post env kf initialize in
+ let env = Env.add_stmt ~post env initialize in
result, env
| "memset", _ | "memcpy", _ | "memmove", _ -> wrong_number_of_arguments name
@@ -396,7 +395,7 @@ let update_memory_model ~loc ~stmt ?result env kf caller args =
Env.pop_and_get env initialize ~global_clear:false Env.Middle
in
let env =
- Env.add_stmt ~post env kf (Smart_stmt.block_stmt initialize_blk)
+ Env.add_stmt ~post env (Smart_stmt.block_stmt initialize_blk)
in
Some result, env
| "fread", _ -> wrong_number_of_arguments name
@@ -420,8 +419,8 @@ let update_memory_model ~loc ~stmt ?result env kf caller args =
Env.pop_and_get env initialize ~global_clear:false Env.Middle
in
let initialize_blk = Smart_stmt.block_stmt initialize_blk in
- let env = Env.add_stmt ~before env kf src_size_stmt in
- let env = Env.add_stmt ~post env kf initialize_blk in
+ let env = Env.add_stmt env src_size_stmt in
+ let env = Env.add_stmt ~post env initialize_blk in
result, env
| "strcpy", _ -> wrong_number_of_arguments name
@@ -429,16 +428,16 @@ let update_memory_model ~loc ~stmt ?result env kf caller args =
let initialize =
Smart_stmt.rtl_call ~loc "initialize" [ dest_e; size_e ]
in
- let env = Env.add_stmt ~post env kf initialize in
+ let env = Env.add_stmt ~post env initialize in
result, env
| "strncpy", _ -> wrong_number_of_arguments name
| "strcat", [ dest_e; src_e ] ->
- process_strcat ~loc ~stmt ?result env kf dest_e src_e
+ process_strcat ~loc ?result env kf dest_e src_e
| "strcat", _ -> wrong_number_of_arguments name
| "strncat", [ dest_e; src_e; size_e ] ->
- process_strcat ~loc ~stmt ?result env kf ~size_e dest_e src_e
+ process_strcat ~loc ?result env kf ~size_e dest_e src_e
| "strncat", _ -> wrong_number_of_arguments name
| "sprintf", buffer_e :: _ :: _ ->
@@ -462,7 +461,7 @@ let update_memory_model ~loc ~stmt ?result env kf caller args =
~cond:(Cil.mkBinOp ~loc Ge result_e (Cil.zero ~loc))
then_blk
in
- let env = Env.add_stmt ~post env kf if_res_pos_stmt in
+ let env = Env.add_stmt ~post env if_res_pos_stmt in
Some result, env
| "sprintf", _ -> wrong_number_of_arguments name
@@ -530,7 +529,7 @@ let update_memory_model ~loc ~stmt ?result env kf caller args =
~cond:(Cil.mkBinOp ~loc LAnd res_pos size_strict_pos)
blk
in
- let env = Env.add_stmt ~post env kf if_res_pos_stmt in
+ let env = Env.add_stmt ~post env if_res_pos_stmt in
Some result, env
| "snprintf", _ ->
wrong_number_of_arguments name
@@ -544,7 +543,7 @@ let update_memory_model ~loc ~stmt ?result env kf caller args =
let unsound =
Smart_stmt.assigns ~loc ~result:(Cil.var sound_verdict_vi) (Cil.zero ~loc)
in
- let env = Env.add_stmt ~post env kf unsound in
+ let env = Env.add_stmt ~post env unsound in
result, env
| _ ->
(* If this error is raised, check that the call to
diff --git a/src/plugins/e-acsl/src/code_generator/libc.mli b/src/plugins/e-acsl/src/code_generator/libc.mli
index 95ef6e79624..a5323906c40 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.mli
+++ b/src/plugins/e-acsl/src/code_generator/libc.mli
@@ -29,16 +29,15 @@ val is_writing_memory: varinfo -> bool
val update_memory_model:
loc:location ->
- stmt:stmt ->
?result:lval ->
Env.t ->
kernel_function ->
varinfo ->
exp list ->
lval option * Env.t
-(** [update_memory_model ~loc ~stmt env kf ?result caller args] generates code
- in [env] to update the memory model after executing the libc function
- [caller] with the given [args].
+(** [update_memory_model ~loc env kf ?result caller args] generates code in
+ [env] to update the memory model after executing the libc function [caller]
+ with the given [args].
@return a tuple [result_opt, env] where [result_opt] is an option with
the lvalue for the result of the function and [env] is the updated
environement. *)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index 13ff7de6305..d9a75dce635 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -243,10 +243,10 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
Typing.preprocess_predicate (Env.Local_vars.get env) p;
let adata, env = Assert.empty ~loc kf env in
let adata, env =
- Assert.register ~loc kf env "destination length" len adata
+ Assert.register ~loc env "destination length" len adata
in
let adata, env =
- Assert.register ~loc kf env "current length" len_orig adata
+ Assert.register ~loc env "current length" len_orig adata
in
let stmt, env =
Assert.runtime_check ~adata ~pred_kind:Assert Smart_stmt.RTE kf env e p
@@ -278,7 +278,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(res_value ~flip:true ()) ])
in
(* Build the statement in the current env *)
- let env = Env.add_stmt env kf stmt in
+ let env = Env.add_stmt env stmt in
(* Return the result expression with the result of the comparison *)
comparison_exp, env
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 39d5e48204f..0166604f9e7 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -134,7 +134,6 @@ let handle_annotations env kf stmt =
let adata, env =
Assert.register
~loc
- kf
env
(Format.asprintf "old %a" Printer.pp_term t_old)
e_old
@@ -143,7 +142,6 @@ let handle_annotations env kf stmt =
let adata, env =
Assert.register
~loc
- kf
env
(Format.asprintf "current %a" Printer.pp_term t)
e
@@ -185,7 +183,6 @@ let handle_annotations env kf stmt =
let adata1, env =
Assert.register
~loc
- kf
env
(Format.asprintf "old %a" Printer.pp_term t)
e_old
@@ -226,7 +223,6 @@ let handle_annotations env kf stmt =
in
Assert.register
~loc
- kf
env
(Format.asprintf "current %a" Printer.pp_term t)
e
@@ -322,7 +318,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let lv_x = var var_x in
let env = match ctx with
| Typing.C_integer _ -> env
- | Typing.Gmpz -> Env.add_stmt env kf (Gmp.init ~loc x)
+ | Typing.Gmpz -> Env.add_stmt env (Gmp.init ~loc x)
| Typing.(C_float _ | Rational | Real | Nan) -> assert false
in
(* build the inner loops and loop body *)
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 03355a4f1cd..758ada02293 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.ml
@@ -22,12 +22,12 @@
open Cil_datatype
-let tracking_stmt ?before fold mk_stmt env kf vars =
+let tracking_stmt fold mk_stmt env kf vars =
if Functions.instrument kf then
fold
(fun vi env ->
if Memory_tracking.must_monitor_vi ~kf vi then
- Env.add_stmt ?before env kf (mk_stmt vi)
+ Env.add_stmt env (mk_stmt vi)
else
env)
vars
@@ -35,36 +35,32 @@ let tracking_stmt ?before fold mk_stmt env kf vars =
else
env
-let store ?before env kf vars =
+let store env kf vars =
tracking_stmt
- ?before
List.fold_right (* small list *)
Smart_stmt.store_stmt
env
kf
vars
-let duplicate_store ?before env kf vars =
+let duplicate_store env kf vars =
tracking_stmt
- ?before
Varinfo.Set.fold
Smart_stmt.duplicate_store_stmt
env
kf
vars
-let delete_from_list ?before env kf vars =
+let delete_from_list env kf vars =
tracking_stmt
- ?before
List.fold_right (* small list *)
Smart_stmt.delete_stmt
env
kf
vars
-let delete_from_set ?before env kf vars =
+let delete_from_set env kf vars =
tracking_stmt
- ?before
Varinfo.Set.fold
Smart_stmt.delete_stmt
env
diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.mli b/src/plugins/e-acsl/src/code_generator/memory_observer.mli
index fad46432acb..216988488b0 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_observer.mli
+++ b/src/plugins/e-acsl/src/code_generator/memory_observer.mli
@@ -26,20 +26,17 @@
open Cil_types
open Cil_datatype
-val store: ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
+val store: Env.t -> kernel_function -> varinfo list -> Env.t
(** For each variable of the given list, if necessary according to the mtracking
analysis, add a call to [__e_acsl_store_block] in the given environment. *)
-val duplicate_store:
- ?before:stmt -> Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
+val duplicate_store: Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
(** Same as [store], with a call to [__e_acsl_duplicate_store_block]. *)
-val delete_from_list:
- ?before:stmt -> Env.t -> kernel_function -> varinfo list -> Env.t
+val delete_from_list: Env.t -> kernel_function -> varinfo list -> Env.t
(** Same as [store], with a call to [__e_acsl_delete_block]. *)
-val delete_from_set:
- ?before:stmt -> Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
+val delete_from_set: Env.t -> kernel_function -> Varinfo.Set.t -> Env.t
(** Same as [delete_from_list] with a set of variables instead of a list. *)
(*
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 08d0fdba873..28c79c7a0fd 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -312,7 +312,6 @@ let term_to_ptr_and_size ~adata ~loc kf env t =
let adata, env =
Assert.register
~loc:t.term_loc
- kf
env
(Format.asprintf "%a" Printer.pp_exp sizeof)
sizeof
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index ed874a35d5e..c1cb81ab441 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -142,7 +142,7 @@ let convert kf env loc ~is_forall quantif =
Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
in
let env =
- Env.add_stmt env kf (Smart_stmt.block_stmt (mkBlock stmts))
+ Env.add_stmt env (Smart_stmt.block_stmt (mkBlock stmts))
in
(* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
@@ -150,7 +150,7 @@ let convert kf env loc ~is_forall quantif =
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 kf end_loop in
+ let env = Env.add_stmt env end_loop in
res, env
end
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index 5964cc63f2a..6635219091e 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -220,10 +220,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 kf =
+let set_instr ?(post=false) loc lhs rhs env kf =
if Memory_tracking.must_monitor_lval ~kf lhs then
Option.fold
- ~some:(fun stmt -> Env.add_stmt ~before:current_stmt ~post env kf stmt)
+ ~some:(fun stmt -> Env.add_stmt ~post env stmt)
~none:env
(mk_stmt_from_assign loc lhs rhs)
else
@@ -237,14 +237,13 @@ let set_instr ?(post=false) current_stmt loc lhs rhs env kf =
module Function_call: sig
(* Top-level handler for Call instructions *)
val instr:
- stmt -> lval option -> exp -> exp list -> location ->
- Env.t -> kernel_function ->
+ 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 kf =
+ let save_params loc args env kf =
let (env, _) = List.fold_left
(fun (env, index) param ->
let lv = Mem(param), NoOffset in
@@ -255,7 +254,7 @@ end = struct
let env =
if Memory_tracking.must_monitor_exp ~kf param then
let stmt = Mk.save_param ~loc flow rhs index in
- Env.add_stmt ~before:current_stmt ~post:false env kf stmt
+ Env.add_stmt ~post:false env stmt
else env
in
(env, index+1))
@@ -267,7 +266,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 kf =
+ let call_with_ret ?(alloc=false) loc ret env =
let rhs = Smart_exp.lval ~loc ret in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
@@ -298,13 +297,13 @@ end = struct
else
Mk.handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
in
- Env.add_stmt ~before:current_stmt ~post:true env kf stmt)
+ Env.add_stmt ~post:true env stmt)
~none: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 kf =
+ let call_memxxx loc args fexp env =
if Libc.is_memcpy fexp || Libc.is_memset fexp then
let prefix = RTL.temporal_prefix in
let name = match fexp.enode with
@@ -314,11 +313,11 @@ end = struct
let stmt =
Smart_stmt.rtl_call ~loc ~prefix name args
in
- Env.add_stmt ~before:current_stmt ~post:false env kf stmt
+ Env.add_stmt ~post:false env stmt
else
env
- let instr current_stmt ret fexp args loc env kf =
+ let instr 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
@@ -331,27 +330,27 @@ end = struct
let name = "reset_parameters" in
Smart_stmt.rtl_call ~loc ~prefix name []
in
- let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
+ let env = Env.add_stmt ~post:false env stmt in
let stmt = Mk.reset_return_referent ~loc in
- let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
+ let env = Env.add_stmt ~post:false env 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 kf
+ save_params loc args env kf
else
env
in
(* Handle special cases of memcpy/memset *)
- let env = call_memxxx current_stmt loc args fexp env kf in
+ let env = call_memxxx loc args fexp env in
(* Memory allocating functions have no definitions so below expression
should capture them *)
let alloc = not has_def in
Option.fold
~some:(fun lhs ->
if Memory_tracking.must_monitor_lval ~kf lhs then
- call_with_ret ~alloc current_stmt loc lhs env kf
+ call_with_ret ~alloc loc lhs env
else env)
~none:env
ret
@@ -364,30 +363,29 @@ end
module Local_init: sig
(* Top-level handler for Local_init instructions *)
val instr:
- stmt -> varinfo -> local_init -> location -> Env.t -> kernel_function ->
- Env.t
+ varinfo -> local_init -> location -> Env.t -> kernel_function -> Env.t
end = struct
- let rec handle_init current_stmt offset loc vi init env kf = match init with
+ let rec handle_init offset loc vi init env kf = match init with
| SingleInit exp ->
- set_instr ~post:true current_stmt loc (Var vi, offset) exp env kf
+ set_instr ~post:true loc (Var vi, offset) exp env kf
| CompoundInit(_, inits) ->
List.fold_left
(fun acc (off, init) ->
let off = Cil.addOffset off offset in
- handle_init current_stmt off loc vi init acc kf)
+ handle_init off loc vi init acc kf)
env
inits
- let instr current_stmt vi li loc env kf =
+ let instr vi li loc env kf =
if Memory_tracking.must_monitor_vi ~kf vi then
match li with
| AssignInit init ->
- handle_init current_stmt NoOffset loc vi init env kf
+ handle_init 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 kf
+ Function_call.instr ret fexp args loc env kf
else
env
end
@@ -399,13 +397,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 kf =
+let track_argument ?(typ) param index env =
let typ = Option.value ~default: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 kf stmt
+ Env.add_stmt ~post:false env stmt
| TInt _ | TFloat _ | TEnum _ | TBuiltin_va_list _ -> env
| TNamed _ -> assert false
| TVoid _ |TArray _ | TFun _ ->
@@ -418,20 +416,20 @@ let track_argument ?(typ) param index env kf =
(* Update local environment [env] with statements tracking return value
of a function. *)
-let handle_return_stmt loc ret env kf =
+let handle_return_stmt loc ret env =
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 kf stmt
+ Env.add_stmt ~post:false env stmt
else
env
| _ -> Options.fatal "Something other than Lval in return"
let handle_return_stmt loc ret env kf =
if Memory_tracking.must_monitor_exp ~kf ret then
- handle_return_stmt loc ret env kf
+ handle_return_stmt loc ret env
else
env
(* }}} *)
@@ -442,14 +440,14 @@ let handle_return_stmt loc ret env kf =
(* Update local environment [env] with statements tracking
instruction [instr] *)
-let handle_instruction current_stmt instr env kf =
+let handle_instruction instr env kf =
match instr with
| Set(lv, exp, loc) ->
- set_instr current_stmt loc lv exp env kf
+ set_instr loc lv exp env kf
| Call(ret, fexp, args, loc) ->
- Function_call.instr current_stmt ret fexp args loc env kf
+ Function_call.instr ret fexp args loc env kf
| Local_init(vi, li, loc) ->
- Local_init.instr current_stmt vi li loc env kf
+ Local_init.instr vi li loc env kf
| Asm _ ->
Options.warning ~once:true ~current:true
"@[Analysis is potentially incorrect in presence of assembly code.@]";
@@ -501,7 +499,7 @@ let handle_function_parameters kf env =
(fun (env, index) param ->
let env =
if Memory_tracking.must_monitor_vi ~kf param
- then track_argument param index env kf
+ then track_argument param index env
else env
in
env, index + 1)
@@ -514,7 +512,7 @@ let handle_function_parameters kf env =
let handle_stmt stmt env kf =
if is_enabled () then begin
match stmt.skind with
- | Instr instr -> handle_instruction stmt instr env kf
+ | Instr instr -> handle_instruction instr env kf
| Return(ret, loc) ->
Option.fold ~some:(fun ret -> handle_return_stmt loc ret env kf) ~none:env ret
| Goto _ | Break _ | Continue _ | If _ | Switch _ | Loop _ | Block _
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index c65609dc83d..b9cc28a77dd 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -78,7 +78,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
| Papp (li, [], args) ->
let e, adata, env =
Logic_functions.app_to_exp ~adata ~loc kf env li args in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pdangling _ -> Env.not_yet env "\\dangling"
| Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
@@ -195,7 +195,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
e, adata, env
| Pforall _ | Pexists _ ->
let e, env = Quantif.quantif_to_exp kf env p in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pat(p, BuiltinLabel Here) ->
to_exp ~adata kf env p
@@ -204,7 +204,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
let pot = PoT_pred p' in
if Lscope.is_used lscope pot then
let e, env = At_with_lscope.to_exp ~loc kf env pot label in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
else begin
(* convert [t'] to [e] in a separated local env *)
@@ -213,7 +213,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
Translate_utils.at_to_exp_no_lscope kf env None label e
in
assert (sty = Typed_number.C_number);
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
end
| Pvalid_read(BuiltinLabel Here, t) as pc
@@ -227,7 +227,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
let e, adata, env =
Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
in
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
@@ -266,7 +266,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
tlist
p
in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pinitialized(BuiltinLabel Here, t) ->
let e, adata, env =
@@ -289,7 +289,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
[ t ]
p
in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env)
in
e, adata, env
@@ -299,7 +299,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
let e, adata, env =
Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
+ let adata, env = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pfreeable _ -> Env.not_yet env "labeled \\freeable"
| Pfresh _ -> Env.not_yet env "\\fresh"
@@ -375,10 +375,7 @@ let do_it ?pred_to_print kf env p =
e
pred_to_print
in
- Env.add_stmt
- env
- kf
- stmt
+ Env.add_stmt env stmt
| Admit -> env
let predicate_to_exp_without_rte ~adata kf env p =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 056ae31da69..c83b2e2ca84 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -255,8 +255,8 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
in
let final_stmt = (Cil.mkBlock [ init_k_stmt; for_stmt ]) in
Env.Logic_binding.remove env k;
- let env = Env.add_stmt env kf (Smart_stmt.block_stmt final_stmt) in
- let adata, env = Assert.register_term ~loc kf env t acc_as_exp adata in
+ let env = Env.add_stmt env (Smart_stmt.block_stmt final_stmt) in
+ let adata, env = Assert.register_term ~loc env t acc_as_exp adata in
acc_as_exp, adata, env, Typed_number.C_number, ""
| _ ->
assert false
@@ -271,29 +271,29 @@ and context_insensitive_term_to_exp ~adata kf env t =
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
let e = Smart_exp.lval ~loc lv in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, name
| TSizeOf ty ->
let e = Cil.sizeOf ~loc ty in
- let adata, env = Assert.register_term ~loc kf env ~force:true t e adata in
+ let adata, env = Assert.register_term ~loc env ~force:true t e adata in
e, adata, env, Typed_number.C_number, "sizeof"
| TSizeOfE t' ->
let e', _, env = to_exp ~adata:Assert.no_data kf env t' in
let e = Cil.sizeOf ~loc (Cil.typeOf e') in
- let adata, env = Assert.register_term ~loc kf env ~force:true t e adata in
+ let adata, env = Assert.register_term ~loc env ~force:true t e adata in
e, adata, env, Typed_number.C_number, "sizeof"
| TSizeOfStr s ->
let e = Cil.new_exp ~loc (SizeOfStr s) in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, "sizeofstr"
| TAlignOf ty ->
let e = Cil.new_exp ~loc (AlignOf ty) in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TAlignOfE t' ->
let e', _, env = to_exp ~adata:Assert.no_data kf env t' in
let e = Cil.new_exp ~loc (AlignOfE e') in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ ~lenv t in
@@ -379,7 +379,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
all data. *)
let adata2, env = Assert.empty ~loc kf env in
let e2, adata2, env = t2_to_exp adata2 env in
- let adata, env = Assert.merge_right ~loc kf env adata2 adata in
+ let adata, env = Assert.merge_right ~loc env adata2 adata in
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
let ctx = Typing.get_number_ty ~lenv t in
@@ -467,8 +467,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
let adata2, env = Assert.empty ~loc kf env in
let e1, adata1, env = t1_to_exp adata1 env in
let e2, adata2, env = t2_to_exp adata2 env in
- let adata, env = Assert.merge_right ~loc kf env adata1 adata in
- let adata, env = Assert.merge_right ~loc kf env adata2 adata in
+ let adata, env = Assert.merge_right ~loc env adata1 adata in
+ let adata, env = Assert.merge_right ~loc env adata2 adata in
(* If the given term is an lvalue variable or a cast from an lvalue
variable, retrieve the name of this variable. Otherwise return
default *)
@@ -618,7 +618,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
else
(* Manual clean because [runtime_check] has not been called on
[adata1]. *)
- let env = Assert.clean ~loc kf env adata1 in
+ let env = Assert.clean ~loc env adata1 in
None, env
in
let mk_stmts _ e =
@@ -746,12 +746,12 @@ and context_insensitive_term_to_exp ~adata kf env t =
| TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
let e = Cil.mkAddrOf ~loc lv in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, "addrof"
| TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
let e = Cil.mkAddrOrStartOf ~loc lv in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, "startof"
| Tapp(li, _, [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ])
when li.l_body = LBnone && (li.l_var_info.lv_name = "\\sum" ||
@@ -763,7 +763,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tapp(li, [], args) ->
let e, adata, env =
Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, "app"
| Tapp(_, _ :: _, _) ->
Env.not_yet env "logic functions with labels"
@@ -807,14 +807,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
let pot = PoT_term t' in
if Lscope.is_used lscope pot then
let e, env = At_with_lscope.to_exp ~loc kf env pot label in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, ""
else
let e, _, env = to_exp ~adata:Assert.no_data kf (Env.push env) t' in
let e, env, sty =
Translate_utils.at_to_exp_no_lscope kf env (Some t) label e
in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, sty, ""
| Tbase_addr(BuiltinLabel Here, t') ->
let name = "base_addr" in
@@ -828,7 +828,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
env
t'
in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, name
| Tbase_addr _ -> Env.not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t') ->
@@ -837,7 +837,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let e, adata, env =
Memory_translate.call ~adata ~loc kf name size_t env t'
in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, name
| Toffset _ -> Env.not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t') ->
@@ -846,7 +846,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let e, adata, env =
Memory_translate.call ~adata ~loc kf name size_t env t'
in
- let adata, env = Assert.register_term ~loc kf env t e adata in
+ let adata, env = Assert.register_term ~loc env t e adata in
e, adata, env, Typed_number.C_number, name
| Tblock_length _ -> Env.not_yet env "labeled \\block_length"
| Tnull ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 318008a35cd..89fe539c7f5 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -290,7 +290,7 @@ let env_of_li ~adata ~loc kf env li =
| Typing.Real ->
Error.not_yet "real number"
in
- adata, Env.add_stmt env kf stmt
+ adata, Env.add_stmt env stmt
| Ltype _ ->
Env.not_yet env "user-defined logic type"
| Lvar _ ->
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 1b18ab669bb..a050b44b6e0 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -30,11 +30,6 @@ module Resulting_projects =
let dependencies = Ast.self :: Options.parameter_states
end)
-let () =
- State_dependency_graph.add_dependencies
- ~from:Resulting_projects.self
- [ Label.self ]
-
let generate_code =
Resulting_projects.memo
(fun name ->
--
GitLab