From 8a99bf321060f700acda5b73ee25219aa72c6ce9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Feb 2022 10:12:06 +0100
Subject: [PATCH] [Eva] New file active_behaviors.
---
Makefile | 6 +-
.../domains/cvalue/cvalue_specification.ml | 6 +-
src/plugins/value/engine/transfer_logic.ml | 80 +++----------------
src/plugins/value/engine/transfer_logic.mli | 17 ++--
src/plugins/value/register.ml | 12 +++
src/plugins/value/utils/active_behaviors.ml | 75 +++++++++++++++++
src/plugins/value/utils/active_behaviors.mli | 29 +++++++
7 files changed, 135 insertions(+), 90 deletions(-)
create mode 100644 src/plugins/value/utils/active_behaviors.ml
create mode 100644 src/plugins/value/utils/active_behaviors.mli
diff --git a/Makefile b/Makefile
index 2f24f05df08..531ba1bf1fa 100644
--- a/Makefile
+++ b/Makefile
@@ -865,7 +865,7 @@ endif
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
utils/eva_audit utils/eva_perf utils/eva_annotations \
utils/eva_dynamic utils/eva_utils utils/red_statuses \
- utils/mark_noresults \
+ utils/active_behaviors utils/mark_noresults \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
partitioning/per_stmt_slevel \
@@ -900,17 +900,17 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
domains/cvalue/builtins_float domains/cvalue/builtins_split \
domains/inout_domain \
legacy/eval_terms legacy/eval_annots \
- domains/powerset engine/transfer_logic \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
domains/cvalue/cvalue_specification \
domains/cvalue/cvalue_domain \
utils/eva_results \
+ domains/powerset \
partitioning/auto_loop_unroll \
partitioning/partition partitioning/partitioning_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/recursion engine/function_calls \
engine/subdivided_evaluation engine/evaluation engine/abstractions \
- engine/transfer_stmt engine/transfer_specification \
+ engine/transfer_logic engine/transfer_stmt engine/transfer_specification \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
domains/taint_domain \
diff --git a/src/plugins/value/domains/cvalue/cvalue_specification.ml b/src/plugins/value/domains/cvalue/cvalue_specification.ml
index 4336ecdaf40..aebbdbd39bc 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -22,8 +22,6 @@
open Cil_types
-module AB = Transfer_logic.ActiveBehaviors
-
(* Eval: under-approximation of the term. Note that ACSL states
that assigns clauses are evaluated in the pre-state.
We skip [\result]: it is meaningless when evaluating the 'assigns' part,
@@ -114,7 +112,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
let link zones = List.fold_left Zone.link Zone.bottom zones in
let outputs = Function_Froms.outputs found_froms in
let check_for_behavior b =
- let activity = AB.is_active ab b in
+ let activity = Active_behaviors.is_active ab b in
match activity with
| False -> ()
| True | Unknown ->
@@ -187,7 +185,7 @@ let verify_assigns_from kf ~pre froms =
| Eval_terms.False -> Alarmset.False
| Eval_terms.Unknown -> Alarmset.Unknown
in
- let ab = AB.create eval_predicate funspec in
+ let ab = Active_behaviors.create eval_predicate funspec in
check_fct_assigns kf ab ~pre_state:pre froms;;
Db.Value.verify_assigns_froms := verify_assigns_from;;
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 124437be116..d56f52ae0bb 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -141,68 +141,6 @@ let create_conjunction l=
in
Logic_const.(List.fold_right (fun p1 p2 -> pand ?loc (p1, p2)) (List.map pred_of_id_pred l) ptrue)
-(* -------------------------- Active behaviors ------------------------------ *)
-
-module ActiveBehaviors = struct
-
- type t = {
- funspec: funspec;
- is_active: funbehavior -> Alarmset.status
- }
-
- module HashBehaviors = Hashtbl.Make(
- struct
- type t = funbehavior
- let equal b1 b2 = b1.b_name = b2.b_name
- let hash b = Hashtbl.hash b.b_name
- end)
-
- let is_active eval_predicate b =
- let assumes = create_conjunction b.b_assumes in
- eval_predicate assumes
-
- let create eval_predicate funspec =
- let h = HashBehaviors.create 3 in
- let is_active = fun b ->
- try HashBehaviors.find h b
- with Not_found ->
- let active = is_active eval_predicate b in
- HashBehaviors.add h b active;
- active
- in
- { is_active; funspec }
-
- let is_active ab behavior = ab.is_active behavior
-
- let active_behaviors ab =
- List.filter
- (fun b -> is_active ab b != Alarmset.False)
- ab.funspec.spec_behavior
-
- let is_active_from_name ab name =
- try
- let list = ab.funspec.spec_behavior in
- let behavior = List.find (fun b' -> b'.b_name = name) list in
- is_active ab behavior
- (* This case happens for behaviors of statement contract, that are not
- handled by this module. *)
- with Not_found -> Alarmset.Unknown
-end
-
-let () =
- Db.Value.valid_behaviors :=
- (fun kf state ->
- let funspec = Annotations.funspec kf in
- let eval_predicate pred =
- match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
- | Eval_terms.True -> Alarmset.True
- | Eval_terms.False -> Alarmset.False
- | Eval_terms.Unknown -> Alarmset.Unknown
- in
- let ab = ActiveBehaviors.create eval_predicate funspec in
- ActiveBehaviors.active_behaviors ab
- )
-
let ip_from_precondition kf call_ki b pre =
let ip_precondition = Property.ip_of_requires kf Kglobal b pre in
match call_ki with
@@ -269,22 +207,22 @@ module type S = sig
type state
type states
- val create: state -> kernel_function -> ActiveBehaviors.t
- val create_from_spec: state -> spec -> ActiveBehaviors.t
+ val create: state -> kernel_function -> Active_behaviors.t
+ val create_from_spec: state -> spec -> Active_behaviors.t
val check_fct_preconditions_for_behaviors:
kinstr -> kernel_function -> behavior list -> Alarmset.status ->
states -> states
val check_fct_preconditions:
- kinstr -> kernel_function -> ActiveBehaviors.t -> state -> states or_bottom
+ kinstr -> kernel_function -> Active_behaviors.t -> state -> states or_bottom
val check_fct_postconditions_for_behaviors:
kernel_function -> behavior list -> Alarmset.status ->
pre_state:state -> post_states:states -> result:varinfo option -> states
val check_fct_postconditions:
- kernel_function -> ActiveBehaviors.t -> termination_kind ->
+ kernel_function -> Active_behaviors.t -> termination_kind ->
pre_state:state -> post_states:states -> result:varinfo option ->
states or_bottom
@@ -292,7 +230,7 @@ module type S = sig
val interp_annot:
limit:int -> record:bool ->
- kernel_function -> ActiveBehaviors.t -> stmt -> code_annotation ->
+ kernel_function -> Active_behaviors.t -> stmt -> code_annotation ->
initial_state:state -> states -> states
end
@@ -344,7 +282,7 @@ module Make
let create_from_spec pre funspec =
let eval_predicate = Domain.evaluate_predicate (pre_env ~pre) pre in
- ActiveBehaviors.create eval_predicate funspec
+ Active_behaviors.create eval_predicate funspec
let create init_state kf =
let funspec = Annotations.funspec kf in
@@ -537,7 +475,7 @@ module Make
to help reduce the final state. *)
let check_fct_postconditions kf ab kind ~pre_state ~post_states ~result =
let behaviors = Annotations.behaviors kf in
- let is_active = ActiveBehaviors.is_active ab in
+ let is_active = Active_behaviors.is_active ab in
let states =
check_fct_postconditions_of_behaviors
kf behaviors is_active kind ~per_behavior:false
@@ -583,7 +521,7 @@ module Make
let check_fct_preconditions call_ki kf ab init_state =
let init_states = States.singleton init_state in
let behaviors = Annotations.behaviors kf in
- let is_active = ActiveBehaviors.is_active ab in
+ let is_active = Active_behaviors.is_active ab in
let states =
check_fct_preconditions_of_behaviors call_ki kf ~per_behavior:false
behaviors is_active init_states
@@ -625,7 +563,7 @@ module Make
| [] -> `True
| behavs ->
let aux acc b =
- match ActiveBehaviors.is_active_from_name ab b with
+ match Active_behaviors.is_active_from_name ab b with
| Alarmset.True -> `True
| Alarmset.Unknown -> if acc = `True then `True else `Unknown
| Alarmset.False -> acc
diff --git a/src/plugins/value/engine/transfer_logic.mli b/src/plugins/value/engine/transfer_logic.mli
index 2512aac64e2..e328d5a9c0b 100644
--- a/src/plugins/value/engine/transfer_logic.mli
+++ b/src/plugins/value/engine/transfer_logic.mli
@@ -23,13 +23,6 @@
open Cil_types
open Eval
-module ActiveBehaviors : sig
- type t
- val is_active: t -> behavior -> Alarmset.status
- val active_behaviors: t -> behavior list
- val create: (predicate -> Alarmset.status) -> spec -> t
-end
-
(* Marks all behaviors of the list as inactive. *)
val process_inactive_behaviors:
kinstr -> kernel_function -> behavior list -> unit
@@ -38,22 +31,22 @@ module type S = sig
type state
type states
- val create: state -> kernel_function -> ActiveBehaviors.t
- val create_from_spec: state -> spec -> ActiveBehaviors.t
+ val create: state -> kernel_function -> Active_behaviors.t
+ val create_from_spec: state -> spec -> Active_behaviors.t
val check_fct_preconditions_for_behaviors:
kinstr -> kernel_function -> behavior list -> Alarmset.status ->
states -> states
val check_fct_preconditions:
- kinstr -> kernel_function -> ActiveBehaviors.t -> state -> states or_bottom
+ kinstr -> kernel_function -> Active_behaviors.t -> state -> states or_bottom
val check_fct_postconditions_for_behaviors:
kernel_function -> behavior list -> Alarmset.status ->
pre_state:state -> post_states:states -> result:varinfo option -> states
val check_fct_postconditions:
- kernel_function -> ActiveBehaviors.t -> termination_kind ->
+ kernel_function -> Active_behaviors.t -> termination_kind ->
pre_state:state -> post_states:states -> result:varinfo option ->
states or_bottom
@@ -61,7 +54,7 @@ module type S = sig
val interp_annot:
limit:int -> record:bool ->
- kernel_function -> ActiveBehaviors.t -> stmt -> code_annotation ->
+ kernel_function -> Active_behaviors.t -> stmt -> code_annotation ->
initial_state:state -> states -> states
end
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index c57f8f46daa..c1e1695ae85 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -140,6 +140,17 @@ let eval_predicate ~pre ~here p =
| False -> Property_status.False_if_reachable
| Unknown -> Property_status.Dont_know
+let valid_behaviors kf state =
+ let funspec = Annotations.funspec kf in
+ let eval_predicate pred =
+ match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
+ | Eval_terms.True -> Alarmset.True
+ | Eval_terms.False -> Alarmset.False
+ | Eval_terms.Unknown -> Alarmset.Unknown
+ in
+ let ab = Active_behaviors.create eval_predicate funspec in
+ Active_behaviors.active_behaviors ab
+
let () =
(* Pretty-printing *)
Db.Value.use_spec_instead_of_definition := use_spec_instead_of_definition;
@@ -150,6 +161,7 @@ let () =
Db.Value.access_location := access_value_of_location;
Db.Value.access_expr := access_value_of_expr;
Db.Value.Logic.eval_predicate := eval_predicate;
+ Db.Value.valid_behaviors := valid_behaviors;
Db.From.find_deps_term_no_transitivity_state :=
find_deps_term_no_transitivity_state;
diff --git a/src/plugins/value/utils/active_behaviors.ml b/src/plugins/value/utils/active_behaviors.ml
new file mode 100644
index 00000000000..bd8599329f8
--- /dev/null
+++ b/src/plugins/value/utils/active_behaviors.ml
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 create_conjunction l =
+ let open Logic_const in
+ let loc = match l with
+ | [] -> None
+ | p :: _ -> Some (pred_of_id_pred p).pred_loc
+ in
+ let predicates = List.map pred_of_id_pred l in
+ List.fold_right (fun p1 p2 -> pand ?loc (p1, p2)) predicates ptrue
+
+type t = {
+ funspec: funspec;
+ is_active: funbehavior -> Alarmset.status
+}
+
+module HashBehaviors = Hashtbl.Make(
+ struct
+ type t = funbehavior
+ let equal b1 b2 = b1.b_name = b2.b_name
+ let hash b = Hashtbl.hash b.b_name
+ end)
+
+let is_active eval_predicate b =
+ let assumes = create_conjunction b.b_assumes in
+ eval_predicate assumes
+
+let create eval_predicate funspec =
+ let h = HashBehaviors.create 3 in
+ let is_active = fun b ->
+ try HashBehaviors.find h b
+ with Not_found ->
+ let active = is_active eval_predicate b in
+ HashBehaviors.add h b active;
+ active
+ in
+ { is_active; funspec }
+
+let is_active ab behavior = ab.is_active behavior
+
+let active_behaviors ab =
+ List.filter
+ (fun b -> is_active ab b != Alarmset.False)
+ ab.funspec.spec_behavior
+
+let is_active_from_name ab name =
+ try
+ let list = ab.funspec.spec_behavior in
+ let behavior = List.find (fun b' -> b'.b_name = name) list in
+ is_active ab behavior
+ (* This case happens for behaviors of statement contract, that are not
+ handled by this module. *)
+ with Not_found -> Alarmset.Unknown
diff --git a/src/plugins/value/utils/active_behaviors.mli b/src/plugins/value/utils/active_behaviors.mli
new file mode 100644
index 00000000000..5ca99b054e5
--- /dev/null
+++ b/src/plugins/value/utils/active_behaviors.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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
+
+type t
+val is_active: t -> behavior -> Alarmset.status
+val is_active_from_name: t -> string -> Alarmset.status
+val active_behaviors: t -> behavior list
+val create: (predicate -> Alarmset.status) -> spec -> t
--
GitLab