diff --git a/.Makefile.lint b/.Makefile.lint
index 6fbfc24fc477f4a72d46a4c8059501ee61d7951a..8d204ac86b7e088b1d89cb4a304fbe0ab437c21a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -381,4 +381,4 @@ ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.mli
-ML_LINT_KO+=src/plugins/e-acsl/src/project_initializer/dup_functions.ml
+
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9321f0f5a8d863065f3ed19c1ae5b9f884a67f5e..3217ed21a1f00a3ef9700316b40609514416f95e 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -58,8 +58,7 @@ SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# project initializer
SRC_PROJECT_INITIALIZER:= \
keep_status \
- prepare_ast \
- dup_functions
+ prepare_ast
SRC_PROJECT_INITIALIZER:=\
$(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 78572f83775819071f278b22995fe41e269c545c..0fea8bfb71a79a2f880769b7dcd3505a7b13e49a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,8 @@
# configure configure
###############################################################################
+-* E-ACSL [2020/01/06] Fix typing bug in presence of variable-length
+ arrays that may lead to incorrect generated code.
-* E-ACSL [2019/12/04] Fix bug with compiler built-ins.
############################
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index c46a2d297ab13e416ef4b6c0121c958bb318bb32..12ff23ceafff79ebd718dc413e35ed46bd84e492 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -182,42 +182,37 @@ module Memo: sig
val clear: unit -> unit
end = struct
- module H = Hashtbl.Make(struct
- type t = term
- (* The comparison over terms is the physical equality. It cannot be the
- structural one (given by [Cil_datatype.Term.equal]) because the very
- same term can be used in 2 different contexts which lead to different
- casts.
-
- By construction, there are no physically equal terms in the AST
- built by Cil. Consequently the memoisation should be fully
- useless. However the translation of E-ACSL guarded quantification
- generates new terms (see module {!Quantif}) which must be typed. The term
- corresponding to the bound variable [x] is actually used twice: once in
- the guard and once for encoding [x+1] when incrementing it. The
- memoization is only useful here and indeed prevent the generation of
- one extra variable in some cases. *)
- let equal (t1:term) t2 = t1 == t2
- let hash = Cil_datatype.Term.hash
- end)
-
- let tbl = H.create 97
+ (* The comparison over terms is the physical equality. It cannot be the
+ structural one (given by [Cil_datatype.Term.equal]) because the very same
+ term can be used in 2 different contexts which lead to different casts.
+
+ By construction (see prepare_ast.ml), there are no physically equal terms
+ in the E-ACSL's generated AST. Consequently the memoisation should be fully
+ useless. However:
+ - type info of many terms are accessed several times
+ - the translation of E-ACSL guarded quantifications generates
+ new terms (see module {!Quantif}) which must be typed. The term
+ corresponding to the bound variable [x] is actually used twice: once in the
+ guard and once for encoding [x+1] when incrementing it. The memoization is
+ only useful here and indeed prevent the generation of one extra variable in
+ some cases. *)
+ let tbl = Misc.Id_term.Hashtbl.create 97
let get t =
- try H.find tbl t
+ try Misc.Id_term.Hashtbl.find tbl t
with Not_found ->
Options.fatal
"[typing] type of term '%a' was never computed."
Printer.pp_term t
let memo f t =
- try H.find tbl t
+ try Misc.Id_term.Hashtbl.find tbl t
with Not_found ->
let x = f t in
- H.add tbl t x;
+ Misc.Id_term.Hashtbl.add tbl t x;
x
- let clear () = H.clear tbl
+ let clear () = Misc.Id_term.Hashtbl.clear tbl
end
@@ -755,6 +750,6 @@ module Datatype = D
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 7572e09419c0c5db12cf8fee2328507d4018c1df..002f03c504695e951ca0bf74919c0ce7ab3a5f1f 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -160,6 +160,6 @@ val compute_quantif_guards_ref
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 40ddd792664456b4fad05ce76297906aba2e64c7..c49a5317279dc372c18f06fe5d6c6648e17ecf02 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -757,6 +757,7 @@ let reset_all ast =
(* by default, do not run E-ACSL on the generated code *)
Options.Run.off ();
(* reset all the E-ACSL environments to their original states *)
+ Mmodel_analysis.reset ();
Misc.reset ();
Logic_functions.reset ();
Literal_strings.reset ();
@@ -776,6 +777,7 @@ let inject () =
Project.pretty (Project.current ());
Keep_status.before_translation ();
Misc.reorder_ast ();
+ Gmp_types.init ();
let ast = Ast.get () in
inject_in_file ast;
reset_all ast;
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml
index 7ed32f22bda8cf2a429e805c35f87204e2eb1be8..84bbe038d874b982bca2792335ce09ac9fffc956 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.ml
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml
@@ -63,7 +63,7 @@ module Make(X: sig end) = struct
ttype = TArray(
TNamed(!t_struct_torig_ref, []),
Some (Cil.one ~loc:Cil_datatype.Location.unknown),
- {scache = Not_Computed},
+ { scache = Not_Computed },
[]);
treferenced = true;
}
@@ -112,3 +112,9 @@ let init () =
end in
try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.mli b/src/plugins/e-acsl/src/libraries/gmp_types.mli
index c61e8b889d535a6431c25ebbdafe836cad641ed3..560d265d3011ff8ddbdb9094580fe391767f1aa0 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.mli
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.mli
@@ -53,3 +53,9 @@ module Z: S
(** Representation of the rational type at runtime *)
module Q: S
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 872847c39d4d4eb06ef6aa3ba1350146fadec2d3..97b2bea3cfa4b28dcce74f7ed444ef4c563a4ea1 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -219,6 +219,19 @@ let name_of_binop = function
| MinusA -> "sub"
| MinusPP | MinusPI | IndexPI | PlusPI -> assert false
+module Id_term =
+ Datatype.Make_with_collections
+ (struct
+ include Cil_datatype.Term
+ let name = "E_ACSL.Id_term"
+ let compare (t1:term) t2 =
+ if t1 == t2 then 0 else Cil_datatype.Term.compare t1 t2
+ let equal (t1:term) t2 = t1 == t2
+ let structural_descr = Structural_descr.t_abstract
+ let rehash = Datatype.identity
+ let mem_project = Datatype.never_any_project
+ end)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 82d10e9d096b78c3b34aac33e24d6b86777fdba1..0797bc7f8d9a0804373e1b0d1676ba8e9a3e8141 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -30,7 +30,7 @@ open Cil_types
exception Unregistered_library_function of string
val get_lib_fun_vi: string -> varinfo
-(** Return varinfo corresponding to a name of a given library function *)
+(** @return varinfo corresponding to a name of a given library function *)
(* ************************************************************************** *)
(** {2 Handling \result} *)
@@ -80,14 +80,14 @@ val is_set_of_ptr_or_array: logic_type -> bool
(** Checks whether the given logic type is a set of pointers. *)
val is_range_free: term -> bool
-(** Returns [true] iff the given term does not contain any range. *)
+(** @return true iff the given term does not contain any range. *)
val is_bitfield_pointers: logic_type -> bool
-(** Returns [true] iff the given logic type is a bitfield pointer or a
+(** @return true iff the given logic type is a bitfield pointer or a
set of bitfield pointers. *)
val term_has_lv_from_vi: term -> bool
-(** Return [true] iff the given term contains a variables that originates from
+(** @return true iff the given term contains a variables that originates from
a C varinfo, that is a non-purely logic variable. *)
type pred_or_term = PoT_pred of predicate | PoT_term of term
@@ -97,10 +97,13 @@ val mk_ptr_sizeof: typ -> location -> exp
to a [typ] typ and returns [sizeof(typ)]. *)
val name_of_binop: binop -> string
-(** Returns the name of the given binop as a string *)
+(** @return the name of the given binop as a string. *)
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
-(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
+(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds. *)
+
+module Id_term: Datatype.S_with_collections with type t = term
+(** Datatype for terms that relies on physical equality. *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 2a5627276847a8db29b27e54c64d14c185ea4d12..68ae48a0f107699115696f85e44e98702ba1ae18 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -137,42 +137,27 @@ let generate_code =
(fun () ->
Options.feedback "beginning translation.";
Temporal.enable (Options.Temporal_validity.get ());
- let prepared_prj = Prepare_ast.prepare () in
- let res =
- Project.on
- prepared_prj
- (fun () ->
- let dup_prj = Dup_functions.dup () in
- let copied_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 ();
- (* 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 ();
- copied_prj)
- ()
+ let copied_prj =
+ Project.create_by_copy name ~last:true
in
- if Options.Debug.get () = 0 then begin
- Project.remove ~project:prepared_prj ();
- end;
+ Project.on
+ copied_prj
+ (fun () ->
+ Prepare_ast.prepare ();
+ Injector.inject ();
+ (* 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 ())
+ ();
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
- res)
+ copied_prj)
())
let generate_code =
@@ -249,6 +234,6 @@ let () = Db.Main.extend main
(*
Local Variables:
-compile-command: "make -C .."
+compile-command: "make -C ../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 22a51c9286df2825631ab59de445461a2bbe3338..ae196e9bc0748be6ac5115454a851af8a406e3b6 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -166,7 +166,7 @@ let parameter_states =
let must_visit () = Run.get () || Check.get ()
let dkey_analysis = register_category "analysis"
-let dkey_dup = register_category "duplication"
+let dkey_prepare = register_category "preparation"
let dkey_translation = register_category "translation"
let dkey_typing = register_category "typing"
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index cdc235ce85e6f7eeeb29834b7fdc90a68e2de292..cecf66c0d31025e0d4b40104d03e49db80f057f1 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -42,7 +42,7 @@ val parameter_states: State.t list
val must_visit: unit -> bool
val dkey_analysis: category
-val dkey_dup: category
+val dkey_prepare: category
val dkey_translation: category
val dkey_typing: category
diff --git a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml b/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
deleted file mode 100644
index 64fc328a712e224f33e2d6f31fdc0630b825350c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
+++ /dev/null
@@ -1,428 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-let dkey = Options.dkey_dup
-
-(* ********************************************************************** *)
-(* Environment *)
-(* ********************************************************************** *)
-
-let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
-
-let actions = Queue.create ()
-
-module Global: sig
- val add_logic_info: logic_info -> unit
- val mem_logic_info: logic_info -> bool
- val reset: unit -> unit
-end = struct
-
- let tbl = Cil_datatype.Logic_info.Hashtbl.create 7
- let add_logic_info x = Cil_datatype.Logic_info.Hashtbl.add tbl x ()
- let mem_logic_info x = Cil_datatype.Logic_info.Hashtbl.mem tbl x
- let reset () = Cil_datatype.Logic_info.Hashtbl.clear tbl
-
-end
-
-let reset () =
- Kernel_function.Hashtbl.clear fct_tbl;
- Global.reset ();
- Queue.clear actions
-
-(* ********************************************************************** *)
-(* Duplicating functions *)
-(* ********************************************************************** *)
-
-let dup_funspec tbl bhv spec =
- (* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
- let o = object
- inherit Cil.genericCilVisitor bhv
-
- val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7
-
- method !vlogic_info_use li =
- if Global.mem_logic_info li then
- Cil.ChangeDoChildrenPost
- ({ li with l_var_info = li.l_var_info } (* force a copy *),
- Visitor_behavior.Get.logic_info bhv)
- else
- Cil.JustCopy
-
- method !vterm_offset _ =
- Cil.DoChildrenPost
- (function
- (* no way to directly visit fieldinfo and model_info uses *)
- | TField(fi, off) -> TField(Visitor_behavior.Get.fieldinfo bhv fi, off)
- | TModel(mi, off) -> TModel(Visitor_behavior.Get.model_info bhv mi, off)
- | off -> off)
-
- method !vlogic_var_use orig_lvi =
- match orig_lvi.lv_origin with
- | None ->
- Cil.JustCopy
- | Some vi ->
- try
- let new_lvi =
- Cil_datatype.Logic_var.Hashtbl.find already_visited orig_lvi
- in
- Cil.ChangeTo new_lvi
- with Not_found ->
- Cil.ChangeDoChildrenPost
- ({ orig_lvi with lv_id = orig_lvi.lv_id } (* force a copy *),
- fun lvi ->
- (* using [Visitor_behavior.Get.logic_var bhv lvi] is correct only because the
- lv_id used to compare the lvi does not change between the
- original one and this copy *)
- try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find tbl vi in
- Cil_datatype.Logic_var.Hashtbl.add
- already_visited orig_lvi lvi;
- lvi.lv_id <- new_vi.vid;
- lvi.lv_name <- new_vi.vname;
- lvi.lv_origin <- Some new_vi;
- new_vi.vlogic_var_assoc <- Some lvi;
- lvi
- with Not_found ->
- assert vi.vglob;
- Visitor_behavior.Get.logic_var bhv lvi)
-
- method !videntified_term _ =
- Cil.DoChildrenPost Logic_const.refresh_identified_term
-
- method !videntified_predicate _ =
- Cil.DoChildrenPost Logic_const.refresh_predicate
- end in
- Cil.visitCilFunspec o spec
-
-let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
- new_vi.vdefined <- true;
- let formals = Kernel_function.get_formals kf in
- let mk_formal vi =
- let name =
- if vi.vname = "" then
- (* unnamed formal parameter: must generate a fresh name since a fundec
- cannot have unnamed formals (see bts #2303). *)
- Varname.get
- ~scope:Varname.Function
- (Functions.RTL.mk_gen_name "unamed_formal")
- else
- vi.vname
- in
- Cil.copyVarinfo vi name
- in
- let new_formals = List.map mk_formal formals in
- let res =
- let ty = Kernel_function.get_return_type kf in
- if Cil.isVoidType ty then None
- else Some (Cil.makeVarinfo false false ~referenced:true "__retres" ty)
- in
- let return =
- Cil.mkStmt ~valid_sid:true
- (Return(Extlib.opt_map (Cil.evar ~loc) res, loc))
- in
- let stmts =
- let l =
- [ Cil.mkStmtOneInstr ~valid_sid:true
- (Call(Extlib.opt_map Cil.var res,
- Cil.evar ~loc vi,
- List.map (Cil.evar ~loc) new_formals,
- loc));
- return ]
- in
- if Functions.instrument kf then
- l
- else
- (* set the 'unsound_verdict' variable to 'false' whenever required *)
- let unsound =
- Cil.mkStmtOneInstr ~valid_sid:true
- (Set((Var sound_verdict_vi, NoOffset), Cil.zero ~loc, loc))
- in
- unsound :: l
- in
- let locals = match res with None -> [] | Some r -> [ r ] in
- let body = Cil.mkBlock stmts in
- body.blocals <- locals;
- let tbl = Cil_datatype.Varinfo.Hashtbl.create 7 in
- List.iter2 (Cil_datatype.Varinfo.Hashtbl.add tbl) formals new_formals;
- let new_spec = dup_funspec tbl bhv spec in
- { svar = new_vi;
- sformals = new_formals;
- slocals = locals;
- smaxid = List.length new_formals;
- sbody = body;
- smaxstmtid = None;
- sallstmts = [];
- sspec = new_spec }
-
-let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
- let name = vi.vname in
- Options.feedback ~dkey ~level:2 "entering in function %s" name;
- let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi in
- let fct = Definition(fundec, loc) in
- let new_spec = fundec.sspec in
- let new_kf = { fundec = fct; spec = new_spec } in
- Queue.add (fun () ->
- Kernel_function.Hashtbl.add fct_tbl new_kf ();
- Globals.Functions.register new_kf;
- Globals.Functions.replace_by_definition new_spec fundec loc;
- Annotations.register_funspec new_kf)
- actions;
- Options.feedback ~dkey ~level:2 "function %s" name;
- (* remove the specs attached to the previous kf iff it is a definition:
- it is necessary to keep stable the number of annotations in order to get
- [Keep_status] working fine. *)
- let kf = Visitor_behavior.Get.kernel_function bhv kf in
- if Kernel_function.is_definition kf then begin
- Queue.add
- (fun () ->
- let bhvs =
- Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
- in
- List.iter
- (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
- bhvs;
- Annotations.iter_decreases
- (fun e _ -> Annotations.remove_decreases e kf)
- kf;
- Annotations.iter_terminates
- (fun e _ -> Annotations.remove_terminates e kf)
- kf;
- Annotations.iter_complete
- (fun e l -> Annotations.remove_complete e kf l)
- kf;
- Annotations.iter_disjoint
- (fun e l -> Annotations.remove_disjoint e kf l)
- kf)
- actions
- end;
- GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
-
-(* ********************************************************************** *)
-(* Visitor *)
-(* ********************************************************************** *)
-
-type position = Before_gmp | Gmpz | After_gmp | Memory_model | Code
-
-class dup_functions_visitor prj = object (self)
- inherit Visitor.frama_c_copy prj
-
- val unduplicable_functions =
- let white_list =
- [ "__builtin_va_arg";
- "__builtin_va_end";
- "__builtin_va_start";
- "__builtin_va_copy" ]
- in
- List.fold_left
- (fun acc s -> Datatype.String.Set.add s acc)
- Datatype.String.Set.empty
- white_list
-
- val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
- val mutable before_memory_model = Before_gmp
- val mutable new_definitions: global list = []
- (* new definitions of the annotated functions which will contain the
- translation of the E-ACSL contract *)
-
- val mutable sound_verdict_vi =
- let name = Functions.RTL.mk_api_name "sound_verdict" in
- let vi = Project.on prj (Cil.makeGlobalVar name) Cil.intType in
- vi.vstorage <- Extern;
- vi.vreferenced <- true;
- vi
-
- method private before_memory_model = match before_memory_model with
- | Before_gmp | Gmpz | After_gmp -> true
- | Memory_model | Code -> false
-
- method private insert_libc l =
- match new_definitions with
- | [] -> l
- | _ :: _ ->
- (* add the generated definitions of libc at the end of [l]. This way,
- we are sure that they have access to all of it (in particular, the
- memory model, GMP and the soundness variable).
-
- Also add the [__e_acsl_sound_verdict] variable at the beginning *)
- let res =
- GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
- :: l
- @ new_definitions in
- new_definitions <- [];
- res
-
- method private next () =
- match before_memory_model with
- | Before_gmp -> ()
- | Gmpz -> before_memory_model <- After_gmp
- | After_gmp -> ()
- | Memory_model -> before_memory_model <- Code
- | Code -> ()
-
- method !vlogic_info_decl li =
- Global.add_logic_info li;
- Cil.JustCopy
-
- method !vvrbl vi =
- try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
- Cil.ChangeTo new_vi
- with Not_found ->
- Cil.JustCopy
-
- method private is_unvariadic_function vi =
- match Cil.unrollType vi.vtype with
- | TFun(_, _, variadic, _) -> not variadic
- | _ -> false
-
- method !vglob_aux = function
- | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when (* duplicate a function iff: *)
- not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
- (* it is not already duplicated *)
- && not (Datatype.String.Set.mem vi.vname unduplicable_functions)
- (* it is duplicable *)
- && self#is_unvariadic_function vi (* it is not a variadic function *)
- && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
- && not (Misc.is_fc_or_compiler_builtin vi) (* it is not a built-in *)
- &&
- (let kf =
- try Globals.Functions.get vi with Not_found -> assert false
- in
- not (Functions.instrument kf)
- (* either explicitely listed as to be not instrumented *)
- ||
- (* or: *)
- (not (Cil.is_empty_funspec
- (Annotations.funspec ~populate:false
- (Extlib.the self#current_kf)))
- (* it has a function contract *)
- && Functions.check kf
- (* its annotations must be monitored *)))
- ->
- self#next ();
- let name = Functions.RTL.mk_gen_name vi.vname in
- let new_vi =
- Project.on prj (Cil.makeGlobalVar name) vi.vtype
- in
- Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
- Cil.DoChildrenPost
- (fun l -> match l with
- | [ GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
- ->
- (match g with
- | GFunDecl _ ->
- if not (Kernel_function.is_definition (Extlib.the self#current_kf))
- && vi.vname <> "malloc" && vi.vname <> "free"
- then
- Options.warning "@[annotating undefined function `%a':@ \
-the generated program may miss memory instrumentation@ \
-if there are memory-related annotations.@]"
- Printer.pp_varinfo vi
- | GFun _ -> ()
- | _ -> assert false);
- let tmp = vi.vname in
- if tmp = Kernel.MainFunction.get () then begin
- (* the new function becomes the new main: simply swap the name of both
- functions *)
- vi.vname <- new_vi.vname;
- new_vi.vname <- tmp
- end;
- let kf =
- try
- Globals.Functions.get (Visitor_behavior.Get_orig.varinfo self#behavior vi)
- with Not_found ->
- Options.fatal
- "unknown function `%s' while trying to duplicate it"
- vi.vname
- in
- let spec = Annotations.funspec ~populate:false kf in
- let vi_bhv = Visitor_behavior.Get.varinfo self#behavior vi in
- let new_g, new_decl =
- dup_global
- loc
- self#get_filling_actions
- spec
- self#behavior
- sound_verdict_vi
- kf
- vi_bhv
- new_vi
- in
- (* postpone the introduction of the new function definition to the
- end *)
- new_definitions <- new_g :: new_definitions;
- (* put the declaration before the original function in order to solve
- issue with recursive functions *)
- [ new_decl; g ]
- | _ -> assert false)
- | GVarDecl(_, loc) | GFunDecl(_, _, loc) | GFun(_, loc)
- when Misc.is_library_loc loc ->
- (match before_memory_model with
- | Before_gmp -> before_memory_model <- Gmpz
- | Gmpz | Memory_model -> ()
- | After_gmp -> before_memory_model <- Memory_model
- | Code -> () (* still processing the GMP and memory model headers,
- but reading some libc code *));
- Cil.JustCopy
- | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- self#next ();
- Cil.JustCopy
- | _ ->
- self#next ();
- Cil.DoChildren
-
- method !vfile _ =
- Cil.DoChildrenPost
- (fun f ->
- match new_definitions with
- | [] -> f
- | _ :: _ ->
- (* required by the few cases where there is no global tagged as
- [Code] in the file. *)
- f.globals <- self#insert_libc f.globals;
- f)
-
- initializer
- Project.copy ~selection:(Parameter_state.get_selection ()) prj;
- reset ()
-
-end
-
-let dup () =
- Options.feedback ~level:2 "duplicating annotated functions";
- let prj =
- File.create_project_from_visitor
- "e_acsl_dup_functions"
- (new dup_functions_visitor)
- in
- Queue.iter (fun f -> f ()) actions;
- prj
-
-(*
-Local Variables:
-compile-command: "make"
-End:
-*)
diff --git a/src/plugins/e-acsl/src/project_initializer/dup_functions.mli b/src/plugins/e-acsl/src/project_initializer/dup_functions.mli
deleted file mode 100644
index a200772d8d372958433b9bed83f94d5fab270719..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/project_initializer/dup_functions.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-val dup: unit -> Project.t
-
-(*
-Local Variables:
-compile-command: "make"
-End:
-*)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 1eee37987db0534b7caf7f8c7b39660d172e24eb..f73b359eeee82bc6cf905d347208873971dedb3c 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -22,59 +22,328 @@
open Cil_types
-exception Alignment_error of string
-let align_error s = raise (Alignment_error s)
-
-(* Returns true if the list of attributes [attrs] contains an [align]
- * attribute of [algn] or greater. Returns false otherwise.
- * Throws an exception if
- * - [attrs] contains several [align] attributes specifying different
- * alignment
- * - [attrs] has a single align attribute with a value which is less than [algn] *)
-let sufficiently_aligned attrs algn =
- let alignment = List.fold_left (fun acc attr ->
- match attr with
- | Attr("align", [AInt i]) ->
- let alignment = Integer.to_int i in
- if acc <> 0 && acc <> alignment then
- (* Multiple align attributes with different values *)
- align_error "Multiple alignment attributes"
- else if alignment < algn then
- (* If there is an alignment attribute it should be greater
- * or equal to [algn] *)
- align_error "Insufficient alignment"
- else
- alignment
- | Attr("align", _) ->
- (* Align attribute with an argument other than a single number,
- should not happen really *)
- assert false
- | _ -> acc
- ) 0 attrs in alignment > 0
-
-(* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
- * true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
- * of [algn] (i.e., less than [algn] bytes and has no alignment attribute *)
-let require_alignment typ attrs algn =
- Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
-
-class prepare_visitor prj = object (self)
- inherit Visitor.frama_c_copy prj
+let dkey = Options.dkey_prepare
- (* Add align attributes to local variables (required by temporal analysis) *)
- method !vblock _ =
- if Options.Temporal_validity.get () then
- Cil.DoChildrenPost (fun blk ->
- List.iter (fun vi ->
- (* 4 bytes alignment is required to allow sufficient space for storage
- of 32-bit timestamps in a 1:1 shadow. *)
- if require_alignment vi.vtype vi.vattr 4; then begin
- vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
- end)
- blk.blocals;
- blk)
+(* ********************************************************************** *)
+(* Environment *)
+(* ********************************************************************** *)
+
+let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
+
+(* The purpose of [actions] is similar to the Frama-C visitor's
+ [get_filling_actions] but we need to fill it outside the visitor. So it is
+ our own version. *)
+let actions = Queue.create ()
+
+(* global table for ensuring that logic info are not shared between a function
+ definition and its duplicate *)
+module Global: sig
+ val add_logic_info: logic_info -> unit
+ val mem_logic_info: logic_info -> bool
+ val reset: unit -> unit
+end = struct
+
+ let tbl = Cil_datatype.Logic_info.Hashtbl.create 7
+ let add_logic_info x = Cil_datatype.Logic_info.Hashtbl.add tbl x ()
+ let mem_logic_info x = Cil_datatype.Logic_info.Hashtbl.mem tbl x
+ let reset () = Cil_datatype.Logic_info.Hashtbl.clear tbl
+
+end
+
+let reset () =
+ Kernel_function.Hashtbl.clear fct_tbl;
+ Global.reset ();
+ Queue.clear actions
+
+(* ********************************************************************** *)
+(* Duplicating a function *)
+(* ********************************************************************** *)
+
+(* [tbl] associates the old formals to the new ones *)
+let dup_funspec tbl bhv spec =
+ (* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
+ let o = object
+ inherit Cil.genericCilVisitor bhv
+
+ val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7
+
+ method !vlogic_info_use li =
+ if Global.mem_logic_info li then
+ Cil.ChangeDoChildrenPost
+ ({ li with l_var_info = li.l_var_info } (* force a copy *),
+ Visitor_behavior.Get.logic_info bhv)
+ else
+ Cil.JustCopy
+
+ method !vterm_offset _ =
+ Cil.DoChildrenPost
+ (function (* no way to directly visit fieldinfo and model_info uses *)
+ | TField(fi, off) ->
+ TField(Visitor_behavior.Get.fieldinfo bhv fi, off)
+ | TModel(mi, off) ->
+ TModel(Visitor_behavior.Get.model_info bhv mi, off)
+ | off ->
+ off)
+
+ method !vlogic_var_use orig_lvi =
+ match orig_lvi.lv_origin with
+ | None ->
+ Cil.JustCopy
+ | Some vi ->
+ try
+ let new_lvi =
+ Cil_datatype.Logic_var.Hashtbl.find already_visited orig_lvi
+ in
+ Cil.ChangeTo new_lvi
+ with Not_found ->
+ Cil.ChangeDoChildrenPost
+ ({ orig_lvi with lv_id = orig_lvi.lv_id } (* force a copy *),
+ fun lvi ->
+ try
+ let new_vi = Cil_datatype.Varinfo.Hashtbl.find tbl vi in
+ Cil_datatype.Logic_var.Hashtbl.add
+ already_visited orig_lvi lvi;
+ (* [lvi] is the logic counterpart of a formal varinfo that has
+ been replaced by a new one: propagate this change *)
+ lvi.lv_id <- new_vi.vid;
+ lvi.lv_name <- new_vi.vname;
+ lvi.lv_origin <- Some new_vi;
+ new_vi.vlogic_var_assoc <- Some lvi;
+ lvi
+ with Not_found ->
+ assert vi.vglob;
+ (* using [Visitor_behavior.Get.logic_var bhv lvi] is correct
+ only because the lv_id used to compare the lvi does not
+ change between the original one and this copy *)
+ Visitor_behavior.Get.logic_var bhv lvi)
+
+ method !videntified_term _ =
+ Cil.DoChildrenPost Logic_const.refresh_identified_term
+
+ method !videntified_predicate _ =
+ Cil.DoChildrenPost Logic_const.refresh_predicate
+ end in
+ Cil.visitCilFunspec o spec
+
+let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
+ new_vi.vdefined <- true;
+ let formals = Kernel_function.get_formals kf in
+ let mk_formal vi =
+ let name =
+ if vi.vname = "" then
+ (* unnamed formal parameter: must generate a fresh name since a fundec
+ cannot have unnamed formals (see bts #2303). *)
+ Varname.get
+ ~scope:Varname.Function
+ (Functions.RTL.mk_gen_name "unamed_formal")
+ else
+ vi.vname
+ in
+ Cil.copyVarinfo vi name
+ in
+ let new_formals = List.map mk_formal formals in
+ let res =
+ let ty = Kernel_function.get_return_type kf in
+ if Cil.isVoidType ty
+ then None
+ else Some (Cil.makeVarinfo false false ~referenced:true "__retres" ty)
+ in
+ let return =
+ Cil.mkStmt ~valid_sid:true
+ (Return(Extlib.opt_map (Cil.evar ~loc) res, loc))
+ in
+ let stmts =
+ let l =
+ [ Cil.mkStmtOneInstr ~valid_sid:true
+ (Call(Extlib.opt_map Cil.var res,
+ Cil.evar ~loc vi,
+ List.map (Cil.evar ~loc) new_formals,
+ loc));
+ return ]
+ in
+ if Functions.instrument kf then
+ l
else
- Cil.DoChildren
+ (* set the 'sound_verdict' variable to 'false' whenever required *)
+ let unsound =
+ Cil.mkStmtOneInstr ~valid_sid:true
+ (Set((Var sound_verdict_vi, NoOffset), Cil.zero ~loc, loc))
+ in
+ unsound :: l
+ in
+ let locals = match res with None -> [] | Some r -> [ r ] in
+ let body = Cil.mkBlock stmts in
+ body.blocals <- locals;
+ let tbl = Cil_datatype.Varinfo.Hashtbl.create 7 in
+ List.iter2 (Cil_datatype.Varinfo.Hashtbl.add tbl) formals new_formals;
+ let new_spec = dup_funspec tbl bhv spec in
+ let fundec =
+ { svar = new_vi;
+ sformals = new_formals;
+ slocals = locals;
+ smaxid = List.length new_formals;
+ sbody = body;
+ smaxstmtid = None;
+ sallstmts = [];
+ sspec = new_spec }
+ in
+ (* compute the CFG of the new [fundec] *)
+ Cfg.clearCFGinfo ~clear_id:false fundec;
+ Cfg.cfgFun fundec;
+ fundec
+
+let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
+ let name = vi.vname in
+ Options.feedback ~dkey ~level:2 "entering in function %s" name;
+ let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi in
+ let fct = Definition(fundec, loc) in
+ let new_spec = fundec.sspec in
+ let new_kf = { fundec = fct; spec = new_spec } in
+ Queue.add
+ (fun () ->
+ Kernel_function.Hashtbl.add fct_tbl new_kf ();
+ Globals.Functions.register new_kf;
+ Globals.Functions.replace_by_definition new_spec fundec loc;
+ Annotations.register_funspec new_kf;
+ if new_vi.vname = "main" then begin
+ (* recompute the info about the old main since its name has changed;
+ see the corresponding part in the main visitor *)
+ Globals.Functions.remove vi;
+ Globals.Functions.register kf
+ end)
+ actions;
+ (* remove the specs attached to the previous kf iff it is a definition:
+ it is necessary to keep stable the number of annotations in order to get
+ [Keep_status] working fine. *)
+ let kf = Visitor_behavior.Get.kernel_function bhv kf in
+ if Kernel_function.is_definition kf then begin
+ Queue.add
+ (fun () ->
+ let bhvs =
+ Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
+ in
+ List.iter
+ (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
+ bhvs;
+ Annotations.iter_decreases
+ (fun e _ -> Annotations.remove_decreases e kf)
+ kf;
+ Annotations.iter_terminates
+ (fun e _ -> Annotations.remove_terminates e kf)
+ kf;
+ Annotations.iter_complete
+ (fun e l -> Annotations.remove_complete e kf l)
+ kf;
+ Annotations.iter_disjoint
+ (fun e l -> Annotations.remove_disjoint e kf l)
+ kf)
+ actions
+ end;
+ GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
+
+(* ********************************************************************** *)
+(* Alignment *)
+(* ********************************************************************** *)
+
+(* Returns true if the list of attributes [attrs] contains an [align] attribute
+ of [algn] or greater. Returns false otherwise.
+ Throws an exception if
+ - [attrs] contains several [align] attributes specifying different
+ alignments
+ - [attrs] has a single align attribute with a value which is less than
+ [algn] *)
+let sufficiently_aligned vi algn =
+ let alignment =
+ List.fold_left
+ (fun acc attr ->
+ match attr with
+ | Attr("align", [AInt i]) ->
+ let alignment = Integer.to_int i in
+ if acc <> 0 && acc <> alignment then begin
+ (* multiple align attributes with different values *)
+ Options.error
+ "multiple alignment attributes with different values for\
+ variable %a. Keeping the last one."
+ Printer.pp_varinfo vi;
+ alignment
+ end else if alignment < algn then begin
+ (* if there is an alignment attribute it should be greater or equal
+ to [algn] *)
+ Options.error
+ "alignment of variable %a should be greater or equal to %d.@ \
+ Continuing with this value."
+ Printer.pp_varinfo vi
+ algn;
+ algn
+ end else
+ alignment
+ | Attr("align", _) ->
+ (* align attribute with an argument other than a single number,
+ should not happen really *)
+ assert false
+ | _ -> acc)
+ 0
+ vi.vattr
+ in
+ alignment > 0
+
+(* return [true] iff the given [vi] requires to be aligned at the boundary
+ of [algn] (i.e., less than [algn] bytes and has no alignment attribute) *)
+let require_alignment vi algn =
+ Cil.bitsSizeOf vi.vtype < algn*8 && not (sufficiently_aligned vi algn)
+
+(* ********************************************************************** *)
+(* Visitor *)
+(* ********************************************************************** *)
+
+class prepare_visitor = object (self)
+ inherit Visitor.frama_c_inplace
+
+ val mutable has_new_stmt_in_fundec = false
+
+ (* ---------------------------------------------------------------------- *)
+ (* visitor's local variable *)
+ (* ---------------------------------------------------------------------- *)
+
+ val terms = Misc.Id_term.Hashtbl.create 7
+ (* table for ensuring absence of term sharing *)
+
+ val unduplicable_functions =
+ let white_list =
+ [ "__builtin_va_arg";
+ "__builtin_va_end";
+ "__builtin_va_start";
+ "__builtin_va_copy" ]
+ in
+ List.fold_left
+ (fun acc s -> Datatype.String.Set.add s acc)
+ Datatype.String.Set.empty
+ white_list
+
+ val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
+ val mutable new_definitions: global list = []
+ (* new definitions of the annotated functions which will contain the
+ translation of the E-ACSL contract *)
+
+ (* the variable [sound_verdict] belongs to the E-ACSL's RTL and indicates
+ whether the verdict emitted by E-ACSL is sound. It needs to be visible at
+ that point because it is set in all function duplicates
+ (see [dup_fundec]). *)
+ val mutable sound_verdict_vi =
+ let name = Functions.RTL.mk_api_name "sound_verdict" in
+ let vi = Cil.makeGlobalVar name Cil.intType in
+ vi.vstorage <- Extern;
+ vi.vreferenced <- true;
+ vi
+
+ (* ---------------------------------------------------------------------- *)
+ (* visitor's private methods *)
+ (* ---------------------------------------------------------------------- *)
+
+ method private is_variadic_function vi =
+ match Cil.unrollType vi.vtype with
+ | TFun(_, _, variadic, _) -> variadic
+ | _ -> true
(* IMPORTANT: for keeping property statuses, we must preserve the ordering of
translation, see function [Translate.translate_pre_spec] and
@@ -146,7 +415,7 @@ class prepare_visitor prj = object (self)
| AVariant v ->
push kf K_Variant (Property.ip_of_decreases kf (Kstmt stmt) v)
| AAssigns _ ->
- (* TODO: should be a postcondition, but considered as a unhandled
+ (* TODO: should be a postcondition, but considered as an unhandled
precondition in translate.ml right now; and we need to preserve the
same ordering *)
Extlib.may
@@ -156,8 +425,12 @@ class prepare_visitor prj = object (self)
Extlib.may
(push kf K_Allocation)
(Property.ip_of_allocation kf (Kstmt stmt) (Property.Id_loop a) alloc)
- | APragma _ -> () (* not yet translated *)
- | AExtended _ -> () (* never translate extensions *)
+ | APragma _ ->
+ (* not yet translated *)
+ ()
+ | AExtended _ ->
+ (* never translate extensions *)
+ ()
method private push_post_code_annot a = match a.annot_content with
| AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
@@ -169,37 +442,179 @@ class prepare_visitor prj = object (self)
| APragma _
| AExtended _ -> ()
- (* Move variable declared in the body of a switch statement to the outer
- scope *)
- method !vstmt_aux init_stmt =
+ (* ---------------------------------------------------------------------- *)
+ (* visitor's method overloading *)
+ (* ---------------------------------------------------------------------- *)
+
+ method !vlogic_info_decl li =
+ Global.add_logic_info li;
+ Cil.SkipChildren
+
+ method !vvrbl vi =
+ try
+ let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
+ (* replace functions at callsite by its duplicated version *)
+ Cil.ChangeTo new_vi
+ with Not_found ->
+ Cil.SkipChildren
+
+ method !vterm _t =
+ Cil.DoChildrenPost
+ (fun t ->
+ if Misc.Id_term.Hashtbl.mem terms t then
+ (* remove term sharing for soundness of E-ACSL typing
+ (see typing.ml) *)
+ { t with term_node = t.term_node }
+ else begin
+ Misc.Id_term.Hashtbl.add terms t ();
+ t
+ end)
+
+ (* Add align attributes to local variables (required by temporal analysis) *)
+ method !vblock _ =
+ if Options.Temporal_validity.get () then
+ Cil.DoChildrenPost
+ (fun blk ->
+ List.iter
+ (fun vi ->
+ (* 4 bytes alignment is required to allow sufficient space for
+ storage of 32-bit timestamps in a 1:1 shadow. *)
+ if require_alignment vi 4 then
+ vi.vattr <-
+ Attr("aligned", [ AInt Integer.four ]) :: vi.vattr)
+ blk.blocals;
+ blk)
+ else
+ Cil.DoChildren
+
+ method !vstmt_aux stmt =
Annotations.iter_code_annot
(fun _ a -> self#push_pre_code_annot a)
- init_stmt;
+ stmt;
Cil.DoChildrenPost
- (fun stmt ->
+ (fun _ ->
Annotations.iter_code_annot
(fun _ a -> self#push_post_code_annot a)
- init_stmt;
+ stmt;
+ (* move variables declared in the body of a switch statement to the
+ outer scope *)
match stmt.skind with
| Switch(_,sw_blk,_,_) ->
let new_blk = Cil.mkBlock [ stmt ] in
let new_stmt = Cil.mkStmt ~valid_sid:true (Block new_blk) in
new_blk.blocals <- sw_blk.blocals;
sw_blk.blocals <- [];
+ has_new_stmt_in_fundec <- true;
new_stmt
- | _ -> stmt)
+ | _ ->
+ stmt)
- method private is_unvariadic_function vi =
- match Cil.unrollType vi.vtype with
- | TFun(_, _, variadic, _) -> not variadic
- | _ -> false
+ method !vfunc fundec =
+ Cil.DoChildrenPost
+ (fun _ ->
+ if has_new_stmt_in_fundec then begin
+ has_new_stmt_in_fundec <- false;
+ (* recompute the CFG *)
+ Cfg.clearCFGinfo ~clear_id:false fundec;
+ Cfg.cfgFun fundec;
+ end;
+ fundec)
method !vglob_aux = function
+ | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
+ when (* duplicate a function iff: *)
+ (* it is not already duplicated *)
+ not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
+ && (* it is duplicable *)
+ not (Datatype.String.Set.mem vi.vname unduplicable_functions)
+ && (* it is not a variadic function *)
+ not (self#is_variadic_function vi)
+ && (* it is not in the E-ACSL's RTL *)
+ not (Misc.is_library_loc loc)
+ && (* it is not a built-in *)
+ not (Misc.is_fc_or_compiler_builtin vi)
+ &&
+ (let kf =
+ try Globals.Functions.get vi with Not_found -> assert false
+ in
+ (* either explicitely listed as to be not instrumented *)
+ not (Functions.instrument kf)
+ ||
+ (* or: *)
+ ((* it has a function contract *)
+ not (Cil.is_empty_funspec
+ (Annotations.funspec ~populate:false
+ (Extlib.the self#current_kf)))
+ && (* its annotations must be monitored *)
+ Functions.check kf))
+ ->
+ let name = Functions.RTL.mk_gen_name vi.vname in
+ let new_vi = Cil.makeGlobalVar name vi.vtype in
+ Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
+ Cil.DoChildrenPost
+ (fun l -> match l with
+ | [ GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
+ ->
+ let kf = Extlib.the self#current_kf in
+ (match g with
+ | GFunDecl _ ->
+ if not (Kernel_function.is_definition kf)
+ && vi.vname <> "malloc" && vi.vname <> "free"
+ then
+ Options.warning
+ "@[annotating undefined function `%a':@ \
+ the generated program may miss memory instrumentation@ \
+ if there are memory-related annotations.@]"
+ Printer.pp_varinfo vi
+ | GFun _ -> ()
+ | _ -> assert false);
+ let spec = Annotations.funspec ~populate:false kf in
+ self#push_pre_spec spec;
+ self#push_post_spec spec;
+ let tmp = vi.vname in
+ if tmp = "main" then begin
+ (* the new function becomes the new main: *)
+ (* 1. swap the name of both functions *)
+ vi.vname <- new_vi.vname;
+ new_vi.vname <- tmp;
+ (* 2. force recomputation of the entry point if necessary *)
+ if Kernel.MainFunction.get () = tmp then begin
+ let selection =
+ State_selection.with_dependencies Kernel.MainFunction.self
+ in
+ Project.clear ~selection ()
+ end
+ (* 3. recompute what is necessary in [Globals.Functions]:
+ done in [dup_global] *)
+ end;
+ let new_g, new_decl =
+ dup_global
+ loc
+ self#get_filling_actions
+ spec
+ self#behavior
+ sound_verdict_vi
+ kf
+ vi
+ new_vi
+ in
+ (* postpone the introduction of the new function definition to the
+ end *)
+ new_definitions <- new_g :: new_definitions;
+ (* put the declaration before the original function in order to
+ solve issue with recursive functions *)
+ [ new_decl; g ]
+ | _ -> assert false)
+
+ | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
+ when Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi ->
+ Cil.DoChildren
+
| GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when self#is_unvariadic_function vi
- && not (Misc.is_library_loc loc)
- && not (Misc.is_fc_or_compiler_builtin vi)
+ when not (self#is_variadic_function vi)
->
+ assert (* handled by the 2 cases above *)
+ (not (Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi));
let kf = Extlib.the self#current_kf in
let s = Annotations.funspec ~populate:false kf in
Cil.DoChildrenPost
@@ -207,18 +622,39 @@ class prepare_visitor prj = object (self)
self#push_pre_spec s;
self#push_post_spec s;
f)
+
| _ ->
Cil.DoChildren
- initializer Project.copy ~selection:(Parameter_state.get_selection ()) prj
+ method !vfile f =
+ Cil.DoChildrenPost
+ (fun _ ->
+ match new_definitions with
+ | [] -> f
+ | _ :: _ ->
+ (* add the generated definitions of libc at the end of
+ [new_definitions]. This way, we are sure that they have access to
+ all of it (in particular, the memory model, GMP and the soundness
+ variable). Also add the [__e_acsl_sound_verdict] variable at the
+ beginning *)
+ let new_globals =
+ GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
+ :: f.globals
+ @ new_definitions
+ in
+ f.globals <- new_globals;
+ f)
+
+ initializer
+ reset ()
end
let prepare () =
Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
- File.create_project_from_visitor
- "e_acsl_prepare_ast"
- (new prepare_visitor)
+ Visitor.visitFramacFile (new prepare_visitor) (Ast.get ());
+ Queue.iter (fun f -> f ()) actions;
+ Ast.mark_as_grown ()
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index 54e87bf224e2f25d0580dcc9c436002faa8c2221..120e25eba95e287042928d125a18439de12313f2 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -22,15 +22,19 @@
(** Prepare AST for E-ACSL generation.
- So for this module performs two tasks:
- - move declarations of variables declared in the bodies of switch
+ More precisely, this module performs the following tasks:
+ - generating a new definition for functions with contract;
+ - removing term sharing;
+ - moving declarations of variables declared in the bodies of switch
statements to upper scopes;
- - store what is necessary to translate in [Keep_status]. *)
+ - storing what is necessary to translate in [Keep_status];
+ - in case of temporal validity checks, adding the attribute "aligned" to
+ variables that are not sufficiently aligned. *)
-val prepare: unit -> Project.t
+val prepare: unit -> unit
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/tests/memory/vla.c b/src/plugins/e-acsl/tests/memory/vla.c
index 0d2107a0bad4d549fcfa62d1c43b9b98aefd8674..28b41333424bdc50255fde6f48198b70782ce705 100644
--- a/src/plugins/e-acsl/tests/memory/vla.c
+++ b/src/plugins/e-acsl/tests/memory/vla.c
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: Check variable-length arrays
+ COMMENT: check variable-length arrays
*/
int LEN = 10;
@@ -9,9 +9,9 @@ int main(int argc, char **argv) {
int i;
for (i = 0; i <= LEN; i++) {
if (i < LEN) {
- /*@assert \valid(&arr[i]); */
+ /*@ assert \valid(&arr[i]); */
} else {
- /*@assert ! \valid(&arr[i]); */
+ /*@ assert ! \valid(&arr[i]); */
}
}
return 0;