Commit 29d304c2 authored by Julien Signoles's avatar Julien Signoles

[e-acsl:archi] merge stages 'prepare_ast' and 'dup_functions'

parent d7616871
......@@ -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))
......
......@@ -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
......
......@@ -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
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:
*)
(**************************************************************************)
(* *)
(* 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:
*)
......@@ -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