Commit 42748391 authored by Michele Alberti's avatar Michele Alberti
Browse files

Merge branch 'julien/e-acsl/feature/rewrite-project-initializers' into 'master'

[e-acsl] remove copy-visitors from E-ACSL pre-stages

See merge request frama-c/frama-c!2492
parents 221abc36 027b0d44
......@@ -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
......@@ -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))
......
......@@ -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.
############################
......
......@@ -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:
*)
......@@ -160,6 +160,6 @@ val compute_quantif_guards_ref
(*
Local Variables:
compile-command: "make -C ../.."
compile-command: "make -C ../../../../.."
End:
*)
......@@ -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;
......
......@@ -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:
*)
......@@ -53,3 +53,9 @@ module Z: S
(** Representation of the rational type at runtime *)
module Q: S
(*
Local Variables:
compile-command: "make -C ../../../../.."
End:
*)
......@@ -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 ../../../../.."
......
......@@ -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:
......
......@@ -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:
*)
......@@ -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"
......
......@@ -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
......
<
(**************************************************************************)
(* *)
(* 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 =