Skip to content

GitLab

Commit 15aaf8d3 authored by Julien Signoles's avatar Julien Signoles
Browse files

[archi] visitor rewritten up to blocks (included)

parent ef532a0b
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/Makefile.in
View file @ 15aaf8d3
......@@ -79,7 +79,6 @@ SRC_CODE_GENERATOR:= \
memory_observer \
literal_observer \
global_observer \
visit \
injector
SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))
......
src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
View file @ 15aaf8d3
......@@ -710,11 +710,7 @@ if there are memory-related annotations.@]"
Env.consolidated_mem vi
end
let must_model_vi bhv ?kf ?stmt vi =
let vi = match bhv with
| None -> vi
| Some bhv -> Visitor_behavior.Get_orig.varinfo bhv vi
in
let must_model_vi ?kf ?stmt vi =
let _kf = match kf, stmt with
| None, None | Some _, _ -> kf
| None, Some stmt -> Some (Kernel_function.find_englobing_kf stmt)
......@@ -743,19 +739,19 @@ consolidated_must_model_vi vi
false
*)
let rec apply_on_vi_base_from_lval f bhv ?kf ?stmt = function
| Var vi, _ -> f bhv ?kf ?stmt vi
| Mem e, _ -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
let rec apply_on_vi_base_from_lval f ?kf ?stmt = function
| Var vi, _ -> f ?kf ?stmt vi
| Mem e, _ -> apply_on_vi_base_from_exp f ?kf ?stmt e
and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
and apply_on_vi_base_from_exp f ?kf ?stmt e = match e.enode with
| Lval lv | AddrOf lv | StartOf lv ->
apply_on_vi_base_from_lval f bhv ?kf ?stmt lv
apply_on_vi_base_from_lval f ?kf ?stmt lv
| BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) ->
apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
apply_on_vi_base_from_exp f ?kf ?stmt e1
| BinOp(MinusPP, e1, e2, _) ->
apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
|| apply_on_vi_base_from_exp f bhv ?kf ?stmt e2
| Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
apply_on_vi_base_from_exp f ?kf ?stmt e1
|| apply_on_vi_base_from_exp f ?kf ?stmt e2
| Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f ?kf ?stmt e
| BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
| Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
| Const _ -> (* possible in case of static address *) false
......@@ -765,18 +761,16 @@ and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
let must_model_lval = apply_on_vi_base_from_lval must_model_vi
let must_model_exp = apply_on_vi_base_from_exp must_model_vi
let must_never_monitor_lval bhv ?kf ?stmt lv =
let must_never_monitor_lval ?kf ?stmt lv =
apply_on_vi_base_from_lval
(fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
bhv
(fun ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
?kf
?stmt
lv
let must_never_monitor_exp bhv ?kf ?stmt lv =
let must_never_monitor_exp ?kf ?stmt lv =
apply_on_vi_base_from_exp
(fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
bhv
(fun ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
?kf
?stmt
lv
......@@ -785,23 +779,23 @@ let must_never_monitor_exp bhv ?kf ?stmt lv =
(** {1 Public API} *)
(* ************************************************************************** *)
let must_model_vi ?bhv ?kf ?stmt vi =
let must_model_vi ?kf ?stmt vi =
not (must_never_monitor vi)
&&
(Options.Full_mmodel.get ()
|| Error.generic_handle (must_model_vi bhv ?kf ?stmt) false vi)
|| Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
let must_model_lval ?bhv ?kf ?stmt lv =
not (must_never_monitor_lval bhv ?kf ?stmt lv)
let must_model_lval ?kf ?stmt lv =
not (must_never_monitor_lval ?kf ?stmt lv)
&&
(Options.Full_mmodel.get ()
|| Error.generic_handle (must_model_lval bhv ?kf ?stmt) false lv)
|| Error.generic_handle (must_model_lval ?kf ?stmt) false lv)
let must_model_exp ?bhv ?kf ?stmt exp =
not (must_never_monitor_exp bhv ?kf ?stmt exp)
let must_model_exp ?kf ?stmt exp =
not (must_never_monitor_exp ?kf ?stmt exp)
&&
(Options.Full_mmodel.get ()
|| Error.generic_handle (must_model_exp bhv ?kf ?stmt) false exp)
|| Error.generic_handle (must_model_exp ?kf ?stmt) false exp)
let use_model () =
not (Env.is_empty ())
......@@ -810,6 +804,6 @@ let use_model () =
(*
Local Variables:
compile-command: "make"
compile-command: "make -C ../.."
End:
*)
src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
View file @ 15aaf8d3
......@@ -31,19 +31,15 @@ val reset: unit -> unit
val use_model: unit -> bool
(** Is one variable monitored (at least)? *)
val must_model_vi: ?bhv:Visitor_behavior.t -> ?kf:kernel_function
-> ?stmt:stmt -> varinfo -> bool
val must_model_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
(** [must_model_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
[stmt] in the given function [kf] must be tracked by the memory model
library. If behavior [bhv] is specified then assume that [vi] is part
of the new project generated by the given copy behavior [bhv] *)
library. *)
val must_model_lval: ?bhv:Visitor_behavior.t -> ?kf:kernel_function
-> ?stmt:stmt -> lval -> bool
val must_model_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
(** Same as {!must_model_vi}, for left-values *)
val must_model_exp: ?bhv:Visitor_behavior.t -> ?kf:kernel_function
-> ?stmt:stmt -> exp -> bool
val must_model_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
(** Same as {!must_model_vi}, for expressions *)
(*
......
src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
View file @ 15aaf8d3
......@@ -204,7 +204,7 @@ let index_from_sizes_and_shifts ~loc sizes_and_shifts =
sum
let put_block_at_label env block label =
let stmt = Label.get_stmt (Env.get_visitor env) label in
let stmt = Label.get_stmt label in
let env_ref = ref env in
let o = object
inherit Visitor.frama_c_inplace
......@@ -214,8 +214,7 @@ let put_block_at_label env block label =
Cil.ChangeTo stmt
end
in
let bhv = Env.get_behavior env in
ignore(Visitor.visitFramacStmt o (Visitor_behavior.Get.stmt bhv stmt));
ignore (Visitor.visitFramacStmt o stmt);
!env_ref
let to_exp ~loc kf env pot label =
......@@ -244,6 +243,7 @@ let to_exp ~loc kf env pot label =
~name:"at"
~scope:Varname.Function
env
kf
None
ty_ptr
(fun vi e ->
......
src/plugins/e-acsl/src/code_generator/env.ml
View file @ 15aaf8d3
......@@ -54,7 +54,6 @@ type local_env = {
}
type t = {
visitor: Visitor.frama_c_visitor;
lscope: Lscope.t;
lscope_reset: bool;
annotation_kind: Misc.annotation_kind;
......@@ -86,21 +85,8 @@ let empty_local_env =
mp_tbl = empty_mp_tbl;
rte = true }
let dummy =
{ visitor = new Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ());
lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mp_tbl = empty_mp_tbl;
env_stack = [];
var_mapping = Logic_var.Map.empty;
loop_invariants = [];
cpt = 0; }
let empty v =
{ visitor = v;
lscope = Lscope.empty;
let empty =
{ lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
......@@ -118,19 +104,6 @@ let has_no_new_stmt env =
let local, _ = top env in
local.block_info = empty_block
let current_kf env =
let v = env.visitor in
match v#current_kf with
| None -> None
| Some kf -> Some (Visitor_behavior.Get.kernel_function v#behavior kf)
let set_current_kf env kf =
let v = env.visitor in
v#set_current_kf kf
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
(* ************************************************************************** *)
(** {2 Loop invariants} *)
(* ************************************************************************** *)
......@@ -163,7 +136,7 @@ let generate_rte env =
(* eta-expansion required for typing generalisation *)
let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
let local_env, tl_env = top env in
let local_block = local_env.block_info in
let is_z_t = Gmp_types.Z.is_t ty in
......@@ -183,8 +156,8 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
v.vreferenced <- true;
let lscope = match scope with
| Varname.Global -> LGlobal
| Varname.Function -> LFunction (Extlib.the (current_kf env))
| Varname.Block -> LLocal_block (Extlib.the (current_kf env))
| Varname.Function -> LFunction kf
| Varname.Block -> LLocal_block kf
in
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let e = Cil.evar v in
......@@ -246,7 +219,7 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
exception No_term
let new_var ~loc ?(scope=Varname.Block) ?name env t ty mk_stmts =
let new_var ~loc ?(scope=Varname.Block) ?name env kf t ty mk_stmts =
let local_env, _ = top env in
let memo tbl =
try
......@@ -256,18 +229,19 @@ let new_var ~loc ?(scope=Varname.Block) ?name env t ty mk_stmts =
let v, e = Term.Map.find t tbl.new_exps in
if Typ.equal ty v.vtype then v, e, env else raise No_term
with Not_found | No_term ->
do_new_var ~loc ~scope ?name env t ty mk_stmts
do_new_var ~loc ~scope ?name env kf t ty mk_stmts
in
match scope with
| Varname.Global | Varname.Function -> memo env.global_mp_tbl
| Varname.Block -> memo local_env.mp_tbl
let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
let new_var_and_mpz_init ~loc ?scope ?name env kf t mk_stmts =
new_var
~loc
?scope
?name
env
kf
t
(Gmp_types.Z.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
......@@ -285,7 +259,7 @@ module Logic_binding = struct
let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
{ env with var_mapping = var_mapping }
let add ?ty env logic_v =
let add ?ty env kf logic_v =
let ty = match ty with
| Some ty -> ty
| None -> match logic_v.lv_type with
......@@ -303,6 +277,7 @@ module Logic_binding = struct
new_var
~loc:Location.unknown
env
kf
~name:logic_v.lv_name
None
ty
......@@ -336,23 +311,27 @@ module Logic_scope = struct
else env
end
let emitter =
let _emitter = (* [TODO ARCHI] *)
Emitter.create
"E_ACSL"
[ Emitter.Code_annot ]
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
let add_assert env stmt annot = match current_kf env with
(* [TODO ARCHI] to be reimplemented *)
let add_assert _env _stmt _annot = assert false
(*match current_kf env with
| None -> assert false
| Some kf ->
Queue.add
| Some _kf ->
(* Queue.add
(fun () -> Annotations.add_assert emitter ~kf stmt annot)
env.visitor#get_filling_actions
*)*)
let add_stmt ?(post=false) ?before env stmt =
let add_stmt ?(post=false) ?before env kf stmt =
if not post then
Extlib.may (fun old -> E_acsl_label.move env.visitor ~old stmt) before;
Extlib.may (fun old -> E_acsl_label.move kf ~old stmt) before;
let local_env, tl = top env in
let block = local_env.block_info in
let block =
......@@ -491,15 +470,16 @@ module Context = struct
if !ctx <> [] then begin
let vars = env.new_global_vars in
let env =
{ env with new_global_vars =
List.filter
{ env with
new_global_vars =
List.filter
(fun (v, scope) ->
(match scope with
| LGlobal | LFunction _ -> true
| LLocal_block _ -> false)
&& List.for_all (fun (v', _) -> v != v') vars)
!ctx
@ vars }
(match scope with
| LGlobal | LFunction _ -> true
| LLocal_block _kf -> false)
&& List.for_all (fun (v', _) -> v != v') vars)
!ctx
@ vars }
in
ctx := [];
env
......
src/plugins/e-acsl/src/code_generator/env.mli
View file @ 15aaf8d3
......@@ -22,15 +22,14 @@
open Cil_types
(** Environments.
(** Environments.
Environments handle all the new C constructs (variables, statements and
annotations. *)
annotations. *)
type t
val dummy: t
val empty: Visitor.frama_c_visitor -> t
val empty: t
val has_no_new_stmt: t -> bool
(** Assume that a local context has been previously pushed.
......@@ -43,8 +42,8 @@ type localized_scope =
val new_var:
loc:location -> ?scope:Varname.scope -> ?name:string ->
t -> term option -> typ ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
t -> kernel_function -> term option -> typ ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
(** [new_var env t ty mk_stmts] extends [env] with a fresh variable of type
[ty] corresponding to [t]. [scope] is the scope of the new variable (default
......@@ -54,14 +53,14 @@ val new_var:
val new_var_and_mpz_init:
loc:location -> ?scope:Varname.scope -> ?name:string ->
t -> term option ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
t -> kernel_function -> term option ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
(** Same as [new_var], but dedicated to mpz_t variables initialized by
(** Same as [new_var], but dedicated to mpz_t variables initialized by
{!Mpz.init}. *)
module Logic_binding: sig
val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
val add: ?ty:typ -> t -> kernel_function -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
val add_binding: t -> logic_var -> varinfo -> t
......@@ -80,7 +79,7 @@ val add_assert: t -> stmt -> predicate -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
val add_stmt: ?post:bool -> ?before:stmt -> t -> stmt -> t
val add_stmt: ?post:bool -> ?before:stmt -> t -> kernel_function -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s].
[before] may define which stmt the new one is included before. This is to
say that any labels attached to [before] are moved to [stmt]. [post]
......@@ -115,11 +114,6 @@ val transfer: from:t -> t -> t
val get_generated_variables: t -> (varinfo * localized_scope) list
(** All the new variables local to the visited function. *)
val get_visitor: t -> Visitor.generic_frama_c_visitor
val get_behavior: t -> Visitor_behavior.t
val current_kf: t -> kernel_function option
(** Kernel function currently visited in the new project. *)
module Logic_scope: sig
val get: t -> Lscope.t
(** Return the logic scope associated to the environment. *)
......@@ -141,9 +135,6 @@ module Logic_scope: sig
reset at next call to [reset]. *)
end
val set_current_kf: t -> kernel_function -> unit
(* Set current kf of the environment *)
(* ************************************************************************** *)
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
......
src/plugins/e-acsl/src/code_generator/global_observer.ml
View file @ 15aaf8d3
......@@ -38,6 +38,9 @@ let reset () = Varinfo.Hashtbl.reset tbl
let is_empty () = Varinfo.Hashtbl.length tbl = 0
(* Make a unique mapping for each global variable omitting initializers.
Initializers (used to capture literal strings) are added through
[add_initializer] below. *)
let add vi =
if Mmodel_analysis.must_model_vi vi then
Varinfo.Hashtbl.replace tbl vi (ref [])
......@@ -50,12 +53,12 @@ let add_initializer vi offset init =
with Not_found ->
assert false
let rec literal_in_initializer env = function
| SingleInit exp -> snd (Literal_observer.exp_in_depth env exp)
let rec literal_in_initializer env kf = function
| SingleInit exp -> snd (Literal_observer.exp_in_depth env kf exp)
| CompoundInit (_, l) ->
List.fold_left (fun env (_, i) -> literal_in_initializer env i) env l
List.fold_left (fun env (_, i) -> literal_in_initializer env kf i) env l
let mk_init bhv env =
let mk_init_function env =
(* Create [__e_acsl_globals_init] function with definition
for initialization of global variables *)
let vi =
......@@ -82,9 +85,7 @@ let mk_init bhv env =
let fct = Definition(fundec, Location.unknown) in
(* Create and register [__e_acsl_globals_init] as kernel
function *)
let kf =
{ fundec = fct; spec = spec }
in
let kf = { fundec = fct; spec = spec } in
Globals.Functions.register kf;
Globals.Functions.replace_by_definition spec fundec Location.unknown;
(* Now generate the statements. The generation is done only now because it
......@@ -95,12 +96,11 @@ let mk_init bhv env =
after generating observers of **all** globals *)
let env, stmts =
Varinfo.Hashtbl.fold_sorted
(fun old_vi l stmts ->
let new_vi = Visitor_behavior.Get.varinfo bhv old_vi in
(fun vi l stmts ->
List.fold_left
(fun (env, stmts) (off, init) ->
let env = literal_in_initializer env init in
let stmt = Temporal.generate_global_init new_vi off init env in
let env = literal_in_initializer env kf init in
let stmt = Temporal.generate_global_init vi off init in
env, match stmt with None -> stmts | Some stmt -> stmt :: stmts)
stmts
!l)
......@@ -110,11 +110,10 @@ let mk_init bhv env =
(* allocation and initialization of globals *)
let stmts =
Varinfo.Hashtbl.fold_sorted
(fun old_vi _ stmts ->
let new_vi = Visitor_behavior.Get.varinfo bhv old_vi in
(fun vi _ stmts ->
(* a global is both allocated and initialized *)
Misc.mk_store_stmt new_vi
:: Misc.mk_initialize ~loc:Location.unknown (Cil.var new_vi)
Misc.mk_store_stmt vi
:: Misc.mk_initialize ~loc:Location.unknown (Cil.var vi)
:: stmts)
tbl
stmts
......@@ -171,11 +170,10 @@ let mk_init bhv env =
blk.bstmts <- stmts;
vi, fundec, env
let mk_delete bhv stmts =
let mk_delete_stmts stmts =
Varinfo.Hashtbl.fold_sorted
(fun old_vi _l acc ->
let new_vi = Visitor_behavior.Get.varinfo bhv old_vi in
Misc.mk_delete_stmt new_vi :: acc)
(fun vi _l acc ->
Misc.mk_delete_stmt vi :: acc)
tbl
stmts
......
src/plugins/e-acsl/src/code_generator/global_observer.mli
View file @ 15aaf8d3
......@@ -36,11 +36,11 @@ val add: varinfo -> unit
val add_initializer: varinfo -> offset -> init -> unit
(** add the initializer for the given observed variable *)
val mk_init: Visitor_behavior.t -> Env.t -> varinfo * fundec * Env.t
val mk_init_function: Env.t -> varinfo * fundec * Env.t
(** generates a new C function containing the observers for global variable
declaration and initialization *)
val mk_delete: Visitor_behavior.t -> stmt list -> stmt list
val mk_delete_stmts: stmt list -> stmt list
(** generates the observers for global variable de-allocation *)
(*
......
src/plugins/e-acsl/src/code_generator/injector.ml
View file @ 15aaf8d3
......@@ -20,6 +20,284 @@
(* *)
(**************************************************************************)
open Cil_types
open Cil_datatype
let dkey = Options.dkey_translation
let is_main kf =
try
let main, _ = Globals.entry_point () in
Kernel_function.equal kf main
with Globals.No_such_entry_point _s ->
false
(* ************************************************************************** *)
(* Code *)
(* ************************************************************************** *)
let inject_in_block _env _main kf blk =
(* [TODO ARCHI] HERE recursive call *)
let free_stmts = At_with_lscope.Free.find_all kf in
match blk.blocals, free_stmts with
| [], [] ->
()
| [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
let add_locals stmts =
if Functions.instrument kf then
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi ~kf vi then
Misc.mk_delete_stmt vi :: acc
else
acc)
stmts
blk.blocals
else
stmts
in
let rec insert_in_innermost_last_block blk = function
| { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
(* keep the return (enclosed in a generated block) at the end;
preceded by clean if any *)
let init, tl =
if is_main kf && Mmodel_analysis.use_model () then
free_stmts @ [ potential_clean; ret ], tl
else
free_stmts @ [ ret ], l
in
(* now that [free] stmts for [kf] have been inserted,
there is no more need to keep the corresponding entries in the
table managing them. *)
At_with_lscope.Free.remove_all kf;
blk.bstmts <-
List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
| { skind = Block b } :: _ ->
insert_in_innermost_last_block b (List.rev b.bstmts)
| l ->
blk.bstmts <- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
in
insert_in_innermost_last_block blk (List.rev blk.bstmts);
if Functions.instrument kf then
blk.bstmts <-
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi vi && not vi.vdefined
then Misc.mk_store_stmt vi :: acc
else acc)
blk.bstmts
blk.blocals
(* ************************************************************************** *)
(* Function definition *)
(* ************************************************************************** *)