From 6121a9b4523d86ce788045dd997bfe2db534c5e5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 19 Feb 2019 10:44:02 +0100
Subject: [PATCH] new option -e-acsl-functions
---
src/plugins/e-acsl/dup_functions.ml | 16 ++--
src/plugins/e-acsl/env.ml | 24 +++---
src/plugins/e-acsl/functions.ml | 14 ++++
src/plugins/e-acsl/functions.mli | 4 +
src/plugins/e-acsl/mmodel_analysis.ml | 64 +++++++++-------
src/plugins/e-acsl/options.ml | 9 +++
src/plugins/e-acsl/options.mli | 2 +
src/plugins/e-acsl/visit.ml | 101 +++++++++++++++++---------
8 files changed, 152 insertions(+), 82 deletions(-)
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index a4a7c550087..fb7067d7a67 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -263,13 +263,15 @@ class dup_functions_visitor prj = object (self)
method !vglob_aux = function
| GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
when self#is_unvariadic_function vi
- && not (Misc.is_library_loc loc)
- && not (Cil.is_builtin vi)
- && not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
- && not (Cil.is_empty_funspec
- (Annotations.funspec ~populate:false
- (Extlib.the self#current_kf)))
- ->
+ && not (Misc.is_library_loc loc)
+ && not (Cil.is_builtin vi)
+ && not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
+ && not (Cil.is_empty_funspec
+ (Annotations.funspec ~populate:false
+ (Extlib.the self#current_kf)))
+ && Functions.check
+ (try Globals.Functions.get vi with Not_found -> assert false)
+ ->
self#next ();
let name = Functions.RTL.mk_gen_name vi.vname in
let new_vi =
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index c23b7089391..9b7748f17f8 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -93,7 +93,7 @@ end = struct
end
-let empty_block =
+let empty_block =
{ new_block_vars = [];
new_stmts = [];
pre_stmts = [];
@@ -104,19 +104,19 @@ let empty_mpz_tbl =
{ new_exps = Term.Map.empty;
clear_stmts = [] }
-let empty_local_env =
- { block_info = empty_block;
+let empty_local_env =
+ { block_info = empty_block;
mpz_tbl = empty_mpz_tbl;
rte = true }
-let dummy =
+let dummy =
{ visitor = new Visitor.generic_frama_c_visitor (Cil.inplace_visit ());
lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
- global_mpz_tbl = empty_mpz_tbl;
- env_stack = [];
+ global_mpz_tbl = empty_mpz_tbl;
+ env_stack = [];
var_mapping = Logic_var.Map.empty;
loop_invariants = [];
cpt = 0; }
@@ -127,15 +127,15 @@ let empty v =
lscope_reset = true;
annotation_kind = Misc.Assertion;
new_global_vars = [];
- global_mpz_tbl = empty_mpz_tbl;
- env_stack = [];
+ global_mpz_tbl = empty_mpz_tbl;
+ env_stack = [];
var_mapping = Logic_var.Map.empty;
loop_invariants = [];
cpt = 0 }
-
-let top env =
- match env.env_stack with [] -> assert false | hd :: tl -> hd, tl
+let top env = match env.env_stack with
+ | [] -> Options.fatal "Empty environment. That is unexpected."
+ | hd :: tl -> hd, tl
let has_no_new_stmt env =
let local, _ = top env in
@@ -145,7 +145,7 @@ let has_no_new_stmt env =
(** {2 Loop invariants} *)
(* ************************************************************************** *)
-let push_loop env =
+let push_loop env =
{ env with loop_invariants = [] :: env.loop_invariants }
let add_loop_invariant env inv = match env.loop_invariants with
diff --git a/src/plugins/e-acsl/functions.ml b/src/plugins/e-acsl/functions.ml
index 22c8f1cd994..489cbbc03f4 100644
--- a/src/plugins/e-acsl/functions.ml
+++ b/src/plugins/e-acsl/functions.ml
@@ -212,3 +212,17 @@ module Libc = struct
Cil.mkString ~loc param_str
end
+
+let check kf =
+ (* [kf] is monitored iff all functions must be monitored or [kf] belongs to
+ the white list *)
+ Options.Functions.is_empty ()
+ || Options.Functions.mem kf
+ ||
+ (* also check if [kf] is a duplicate of a monitored function *)
+ let s = RTL.get_original_name kf in
+ try
+ let gen_kf = Globals.Functions.find_by_name s in
+ Options.Functions.mem gen_kf
+ with Not_found ->
+ false
diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli
index 7c65ec95fd4..6798b215f89 100644
--- a/src/plugins/e-acsl/functions.mli
+++ b/src/plugins/e-acsl/functions.mli
@@ -26,6 +26,10 @@ val has_fundef: exp -> bool
(** @return [true] if a function whose name is given via [exp] is defined and
[false] otherwise *)
+val check: kernel_function -> bool
+(** @return [true] iff code must be generated for annotations of the given
+ function. *)
+
(* ************************************************************************** *)
(** {2 RTL} Operations on function belonging to the runtime library of E-ACSL *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml
index e5c3136060f..6bd1ce2b1d1 100644
--- a/src/plugins/e-acsl/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/mmodel_analysis.ml
@@ -453,35 +453,43 @@ let register_predicate kf pred state =
(fun state ->
let state = Env.default_varinfos state in
let state =
- if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
- Annotations.fold_behaviors
- (fun _ bhv s ->
- let handle_annot test f s =
- if test then
- f (fun _ p s -> register_predicate kf p s) kf bhv.b_name s
- else
- s
- in
- let s = handle_annot is_first Annotations.fold_requires s in
- let s = handle_annot is_first Annotations.fold_assumes s in
- handle_annot
- is_last
- (fun f -> Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
- kf
+ if Functions.check kf then
+ let state =
+ if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
+ Annotations.fold_behaviors
+ (fun _ bhv s ->
+ let handle_annot test f s =
+ if test then
+ f
+ (fun _ p s -> register_predicate kf p s)
+ kf
+ bhv.b_name
+ s
+ else
+ s
+ in
+ let s = handle_annot is_first Annotations.fold_requires s in
+ let s = handle_annot is_first Annotations.fold_assumes s in
+ handle_annot
+ is_last
+ (fun f ->
+ Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
+ kf
+ state
+ else
+ state
+ in
+ let state =
+ Annotations.fold_code_annot
+ (fun _ -> register_code_annot kf) stmt state
+ in
+ if stmt.ghost then
+ let rtes = Rte.stmt kf stmt in
+ List.fold_left
+ (fun state a -> register_code_annot kf a state) state rtes
+ else
state
- else
- state
- in
- let state =
- Annotations.fold_code_annot
- (fun _ -> register_code_annot kf) stmt state
- in
- let state =
- if stmt.ghost then
- let rtes = Rte.stmt kf stmt in
- List.fold_left
- (fun state a -> register_code_annot kf a state) state rtes
- else
+ else (* not (Options.Functions.check kf): do not monitor [kf] *)
state
in
let state =
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index 93797ae0bde..c7fd1214917 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -114,6 +114,15 @@ module Builtins =
let help = "C functions which can be used in the E-ACSL specifications"
end)
+module Functions =
+ Kernel_function_set
+ (struct
+ let option_name = "-e-acsl-functions"
+ let arg_name ="f1, ..., fn"
+ let help = "only annotations in functions f1, ..., fn are checked at \
+runtime"
+ end)
+
let () = Parameter_customize.set_group help
module Version =
False
diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli
index 6e1347e43d7..628234584f1 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -34,6 +34,8 @@ module Temporal_validity: Parameter_sig.Bool
module Validate_format_strings: Parameter_sig.Bool
module Replace_libc_functions: Parameter_sig.Bool
+module Functions: Parameter_sig.Kernel_function_set
+
val parameter_states: State.t list
val must_visit: unit -> bool
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 031004a66a1..c30617569d2 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -643,25 +643,31 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
env
in
(* translate the precondition of the function *)
- Project.on prj (Translate.translate_pre_spec kf env) !funspec
+ if Functions.check kf then
+ Project.on prj (Translate.translate_pre_spec kf env) !funspec
+ else
+ env
else
env
in
let env, new_annots =
- Annotations.fold_code_annot
- (fun _ old_a (env, new_annots) ->
- let a =
- (* [VP] Don't use Visitor here, as it will fill the queue in the
- middle of the computation... *)
- Cil.visitCilCodeAnnotation (self :> Cil.cilVisitor) old_a
- in
- let env =
- Project.on prj (Translate.translate_pre_code_annotation kf env) a
- in
- env, a :: new_annots)
- (Cil.get_original_stmt self#behavior stmt)
- (env, [])
+ if Functions.check kf then
+ Annotations.fold_code_annot
+ (fun _ old_a (env, new_annots) ->
+ let a =
+ (* [VP] Don't use Visitor here, as it will fill the queue in the
+ middle of the computation... *)
+ Cil.visitCilCodeAnnotation (self :> Cil.cilVisitor) old_a
+ in
+ let env =
+ Project.on prj (Translate.translate_pre_code_annotation kf env) a
+ in
+ env, a :: new_annots)
+ (Cil.get_original_stmt self#behavior stmt)
+ (env, [])
+ else
+ env, []
in
(* Add [__e_acsl_store_duplicate] calls for local variables which
@@ -686,18 +692,32 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let env = Temporal.handle_stmt stmt env in
(* Add initialization statements and store_block statements stemming
from Local_init *)
- self#handle_instructions stmt env kf
+ self#handle_instructions stmt env kf
else
env
in
- let env =
- if stmt.ghost && generate then begin
- stmt.ghost <- false;
- (* translate potential RTEs of ghost code *)
- let rtes = Rte.stmt ~warn:false kf stmt in
- Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
- end else
- env
+ let new_stmt, env, must_mv =
+ if Functions.check kf then
+ let env =
+ (* handle ghost statement *)
+ if stmt.ghost then begin
+ stmt.ghost <- false;
+ (* translate potential RTEs of ghost code *)
+ let rtes = Rte.stmt ~warn:false kf stmt in
+ Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
+ end else
+ env
+ in
+ (* handle loop invariants *)
+ let new_stmt, env, must_mv =
+ Loops.preserve_invariant prj env kf stmt
+ in
+ let orig = Cil.get_original_stmt self#behavior stmt in
+ Cil.set_orig_stmt self#behavior new_stmt orig;
+ Cil.set_stmt self#behavior orig new_stmt;
+ new_stmt, env, must_mv
+ else
+ stmt, env, false
in
let mk_post_env env =
(* [fold_right] to preserve order of generation of pre_conditions *)
@@ -708,11 +728,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
new_annots)
env
in
- (* handle loop invariants *)
- let new_stmt, env, must_mv = Loops.preserve_invariant prj env kf stmt in
- let orig = Cil.get_original_stmt self#behavior stmt in
- Cil.set_orig_stmt self#behavior new_stmt orig;
- Cil.set_stmt self#behavior orig new_stmt;
let new_stmt, env =
(* Remove local variables which scopes ended via goto/break/continue. *)
let del_vars = Exit_points.delete_vars stmt in
@@ -721,13 +736,20 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
else env
in
if self#is_return kf stmt then
- (* must generate the post_block before including [stmt] (the 'return')
- since no code is executed after it. However, since this statement
- is pure (Cil invariant), that is semantically correct. *)
- let env = mk_post_env env in
- (* also handle the postcondition of the function and clear the env *)
let env =
- Project.on prj (Translate.translate_post_spec kf env) !funspec
+ if Functions.check kf then
+ (* must generate the post_block before including [stmt] (the
+ 'return') since no code is executed after it. However, since
+ this statement is pure (Cil invariant), that is semantically
+ correct. *)
+ (* [JS 2019/2/19] TODO: what about the other ways of early exiting
+ a block? *)
+ let env = mk_post_env env in
+ (* also handle the postcondition of the function and clear the
+ env *)
+ Project.on prj (Translate.translate_post_spec kf env) !funspec
+ else
+ env
in
(* de-allocating memory previously allocating by the kf *)
(* JS: should be done in the new project? *)
@@ -778,7 +800,15 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
~global_clear:false
Env.After
in
- let env = mk_post_env (Env.push env) in
+ let env =
+ (* if [kf] is not monitored, do not translate any postcondition,
+ but still push an empty environment consumed by
+ [Env.pop_and_get] below. This [Env.pop_and_get] call is always
+ required in order to generate the code not directly related to
+ the annotations of the current stmt in anycase. *)
+ if Functions.check kf then mk_post_env (Env.push env)
+ else Env.push env
+ in
let post_block, env =
Env.pop_and_get
env
@@ -795,6 +825,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if not (Cil_datatype.Stmt.equal new_stmt res) then
E_acsl_label.move (self :> Visitor.generic_frama_c_visitor)
new_stmt res;
+ let orig = Cil.get_original_stmt self#behavior stmt in
Cil.set_stmt self#behavior orig res;
Cil.set_orig_stmt self#behavior res orig;
res, env
--
GitLab