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/src/main.ml b/src/plugins/e-acsl/src/main.ml
index f8053f3dc74882f6be00928cd1561831d84fa855..c7546057321970e52c9e8e5c0bfa557c0964e0d5 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -144,7 +144,6 @@ let generate_code =
copied_prj
(fun () ->
Prepare_ast.prepare ();
- Dup_functions.dup ();
Injector.inject ();
(* remove the RTE's results computed from E-ACSL: they are
partial and associated with the wrong kernel function (the
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 c8e395c43fbc6f5c8138d1f2c9d8e35c8a0cb23a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
+++ /dev/null
@@ -1,438 +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
- 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;
- 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 = object (self)
- inherit Visitor.frama_c_inplace
-
- 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 = 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 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.SkipChildren
-
- method !vvrbl vi =
- try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
- Cil.ChangeTo new_vi
- with Not_found ->
- Cil.SkipChildren
-
- method private is_variadic_function vi =
- match Cil.unrollType vi.vtype with
- | TFun(_, _, variadic, _) -> variadic
- | _ -> true
-
- 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 *)
- && not (self#is_variadic_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 = 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 _ ->
- let kf = Extlib.the self#current_kf in
- 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 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 kf =
- try
- Globals.Functions.get 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 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(_, 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.DoChildren
- | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- self#next ();
- Cil.DoChildren
- | _ ->
- self#next ();
- Cil.DoChildren
-
- method !vfile f =
- Cil.DoChildrenPost
- (fun _ ->
- match new_definitions with
- | [] -> f
- | _ :: _ ->
- (* 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 new_globals =
- GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
- :: f.globals
- @ new_definitions
- in
- f.globals <- new_globals;
- f)
-
- initializer
- reset ()
-
-end
-
-let dup () =
- Options.feedback ~level:2 "duplicating annotated functions";
- Visitor.visitFramacFile (new dup_functions_visitor) (Ast.get ());
- Queue.iter (fun f -> f ()) actions;
- Ast.mark_as_grown ()
-
-(*
-Local Variables:
-compile-command: "make -C ../../../../.."
-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 2d8dfd48d782fd2ff6f4592487099279928fe554..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 -> unit
-
-(*
-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 d015c335f8d801fc8a70bf8d108e3ff5ecb2eae5..cf20d89e609c207bc514010d6301a8963b83f973 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -22,6 +22,222 @@
open Cil_types
+let dkey = Options.dkey_prepare
+
+(* ********************************************************************** *)
+(* Environment *)
+(* ********************************************************************** *)
+
+let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
+
+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 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
+ 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;
+ 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)
+
+(* ********************************************************************** *)
+(* Alignment *)
+(* ********************************************************************** *)
+
exception Alignment_error of string
let align_error s = raise (Alignment_error s)
@@ -64,39 +280,69 @@ let sufficiently_aligned attrs algn =
let require_alignment typ attrs algn =
Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
+(* ********************************************************************** *)
+(* Visitor *)
+(* ********************************************************************** *)
+
+type position = Before_gmp | Gmpz | After_gmp | Memory_model | Code
+
class prepare_visitor = object (self)
inherit Visitor.frama_c_inplace
val mutable has_new_stmt_in_fundec = false
- val mutable has_new_stmt = false
+
+ (* ---------------------------------------------------------------------- *)
+ (* visitor's local variable *)
+ (* ---------------------------------------------------------------------- *)
+
val terms = Misc.Id_term.Hashtbl.create 7
+ (* table for ensuring absence of term sharing *)
- 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
- t)
+ 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
- (* 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)
- else
- Cil.DoChildren
+ 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 = 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
+
+ method private before_memory_model = match before_memory_model with
+ | Before_gmp | Gmpz | After_gmp -> true
+ | Memory_model | Code -> false
+
+ 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 -> ()
(* IMPORTANT: for keeping property statuses, we must preserve the ordering of
translation, see function [Translate.translate_pre_spec] and
@@ -195,6 +441,51 @@ class prepare_visitor = object (self)
| APragma _
| AExtended _ -> ()
+ (* ---------------------------------------------------------------------- *)
+ (* 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.vtype vi.vattr 4 then begin
+ vi.vattr <- Attr("aligned", [ AInt Integer.four ]) :: vi.vattr
+ end)
+ blk.blocals;
+ blk)
+ else
+ Cil.DoChildren
+
method !vstmt_aux stmt =
Annotations.iter_code_annot
(fun _ a -> self#push_pre_code_annot a)
@@ -221,7 +512,6 @@ class prepare_visitor = object (self)
Cil.DoChildrenPost
(fun _ ->
if has_new_stmt_in_fundec then begin
- has_new_stmt <- true;
has_new_stmt_in_fundec <- false;
(* recompute the CFG *)
Cfg.clearCFGinfo ~clear_id:false fundec;
@@ -229,38 +519,152 @@ class prepare_visitor = object (self)
end;
fundec)
- 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 *)
+ && not (self#is_variadic_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 = 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(_, 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.DoChildren
+
+ | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
+ when Misc.is_fc_or_compiler_builtin vi ->
+ self#next ();
+ 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 (* handle 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
+ self#next ();
Cil.DoChildrenPost
(fun f ->
self#push_pre_spec s;
self#push_post_spec s;
f)
+
| _ ->
+ self#next ();
Cil.DoChildren
- method !vfile _ =
+ method !vfile f =
Cil.DoChildrenPost
- (fun f ->
- if has_new_stmt then Ast.mark_as_grown ();
- f)
+ (fun _ ->
+ match new_definitions with
+ | [] -> f
+ | _ :: _ ->
+ (* 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 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";
- Visitor.visitFramacFileSameGlobals (new prepare_visitor) (Ast.get ())
+ 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 b23a84d6295060acf5d0d6e10fbf0dab760d033a..f9739a57ffa76851d44680d227dc146fff7bc05c 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -23,11 +23,12 @@
(** Prepare AST for E-ACSL generation.
So for this module performs the following tasks:
- - remove term sharing
- - move declarations of variables declared in the bodies of switch
+ - 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]
- - in case of temporal validity checks, add the attribute "aligned" to
+ - 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 -> unit