From 1b7f90a6529fc5ad5c7a5b157da424b35b386b13 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 19 Feb 2020 10:12:41 +0100
Subject: [PATCH] [Eva] Abstract domains: changes the signature of
[logic_assign].
The logical clause and the pre-state are now optional. The function can now
be used to remove from a state all inferred properties that depend on a given
memory location.
This only impacts the cvalue domain, which is the only one to use the assign
clause.
---
src/plugins/value/domains/abstract_domain.mli | 13 +++++++------
src/plugins/value/domains/apron/apron_domain.ml | 2 +-
src/plugins/value/domains/cvalue/cvalue_domain.ml | 10 +++++++---
src/plugins/value/domains/domain_builder.ml | 4 ++--
src/plugins/value/domains/domain_lift.ml | 4 ++--
src/plugins/value/domains/domain_product.ml | 11 ++++++++---
.../value/domains/equality/equality_domain.ml | 2 +-
src/plugins/value/domains/gauges/gauges_domain.ml | 2 +-
src/plugins/value/domains/inout_domain.ml | 2 +-
src/plugins/value/domains/octagons.ml | 2 +-
src/plugins/value/domains/offsm_domain.ml | 2 +-
src/plugins/value/domains/simple_memory.ml | 2 +-
src/plugins/value/domains/symbolic_locs.ml | 2 +-
src/plugins/value/domains/traces_domain.ml | 2 +-
src/plugins/value/domains/unit_domain.ml | 2 +-
src/plugins/value/engine/transfer_specification.ml | 2 +-
16 files changed, 37 insertions(+), 27 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index b1b06f70f1d..cc7d69a289e 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -358,12 +358,13 @@ module type S = sig
(** Logical evaluation. This API is subject to changes. *)
(* TODO: cooperative evaluation of predicates in the engine. *)
- (** [logic_assign from loc_asgn pre state] applies the effect of the
- [assigns ... \from ...] clause [from] to [state]. [pre] is the state
- before the assign clauses, in which the terms of the clause are evaluated.
- [loc_asgn] is the result of the evaluation of the [assigns] part of [from]
- in [pre]. *)
- val logic_assign: logic_assign -> location -> pre:state -> state -> state
+ (** [logic_assign None loc state] removes from [state] all inferred properties
+ that depend on the memory location [loc].
+ If the first argument is not None, it contains the logical clause being
+ interpreted and the pre-state in which the terms of the clause are
+ evaluated. The clause can be an \assign, \allocated or \free clause.
+ [loc] is then the memory location concerned by the clause. *)
+ val logic_assign: (logic_assign * state) option -> location -> state -> state
(** Evaluates a [predicate] to a logical status in the current [state].
The [logic_environment] contains the states at some labels and the
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index c9fd86075f1..c21820f2b2d 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -673,7 +673,7 @@ module Make (Man : Input) = struct
let show_expr _valuation _state _fmt _expr = ()
- let logic_assign _assigns location ~pre:_ state = kill_bases location state
+ let logic_assign _assigns location state = kill_bases location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index b5a165f3189..5257e966b87 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -308,15 +308,19 @@ module State = struct
Printer.pp_from assign pp_eval_error e;
Cvalue.V.top
- let logic_assign logic_assign location ~pre:(pre_state, _) (state, sclob) =
+ let logic_assign logic_assign location (state, sclob) =
match logic_assign with
- | Assigns assign ->
+ | None ->
+ let location = Precise_locs.imprecise_location location
+ and value = Cvalue.V.top in
+ Cvalue.Model.add_binding ~exact:false state location value, sclob
+ | Some (Assigns assign, (pre_state, _)) ->
let location = Precise_locs.imprecise_location location in
let env = Eval_terms.env_assigns pre_state in
let value = evaluate_from_clause env assign in
Locals_scoping.remember_if_locals_in_value sclob location value;
Cvalue.Model.add_binding ~exact:false state location value, sclob
- | Frees _ | Allocates _ -> state, sclob
+ | Some ((Frees _ | Allocates _), _) -> state, sclob
(* ------------------------------------------------------------------------ *)
(* Initialization *)
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 4be9203e8c2..a574d3a3c4a 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -102,7 +102,7 @@ module Make_Minimal
let lval = Cil.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
- let logic_assign _assigns _location ~pre:_ _state = top
+ let logic_assign _assigns _location _state = top
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ t _ _ = `Value t
@@ -239,7 +239,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let lval = Cil.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
- let logic_assign _assigns _location ~pre:_ _state = top
+ let logic_assign _assigns _location _state = top
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ t _ _ = `Value t
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0e8d958ef1d..46331911138 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -123,8 +123,8 @@ module Make
let show_expr valuation = Domain.show_expr (lift_valuation valuation)
- let logic_assign assigns location ~pre state =
- Domain.logic_assign assigns (Convert.restrict_loc location) ~pre state
+ let logic_assign assigns location state =
+ Domain.logic_assign assigns (Convert.restrict_loc location) state
let evaluate_predicate = Domain.evaluate_predicate
let reduce_by_predicate = Domain.reduce_by_predicate
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index e9894fa2f06..06574e327e6 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -227,9 +227,14 @@ module Make
print_one_side fmt right_log Right.name Right.pretty right)
- let logic_assign assign location ~pre:(left_pre, right_pre) (left, right) =
- Left.logic_assign assign location ~pre:left_pre left,
- Right.logic_assign assign location ~pre:right_pre right
+ let logic_assign assign location (left, right) =
+ let left_assign, right_assign =
+ match assign with
+ | None -> None, None
+ | Some (assign, (left, right)) -> Some (assign, left), Some (assign, right)
+ in
+ Left.logic_assign left_assign location left,
+ Right.logic_assign right_assign location right
let lift_logic_env f logic_env =
Abstract_domain.{ states = (fun label -> f (logic_env.states label));
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index f78930c6d92..b04cd0ffa19 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -503,7 +503,7 @@ module Make
| Some equality -> Equality.Equality.pretty fmt equality
| None -> ()
- let logic_assign _assigns location ~pre:_ state =
+ let logic_assign _assigns location state =
let loc = Precise_locs.imprecise_location location in
let zone = Locations.(enumerate_valid_bits Write loc) in
kill Hcexprs.Modified zone state
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 3b60576b815..4c8dec87e1e 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1296,7 +1296,7 @@ module D_Impl : Abstract_domain.S
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
- let logic_assign _assigns location ~pre:_ state = kill location state
+ let logic_assign _assigns location state = kill location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index da068efc2f9..5bbf25ba1ff 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -261,7 +261,7 @@ module Internal
let initialize_variable_using_type _ _ state = state
(* TODO *)
- let logic_assign _assign _location ~pre:_ _state = top
+ let logic_assign _assign _location _state = top
(* Logic *)
let evaluate_predicate _ _ _ = Alarmset.Unknown
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 853183f0d39..b1faca4b4d6 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1235,7 +1235,7 @@ module Domain = struct
let show_expr _valuation _state _fmt _expr = ()
- let logic_assign _logic_assign location ~pre:_ state =
+ let logic_assign _logic_assign location state =
let loc = Precise_locs.imprecise_location location in
let zone = Locations.(enumerate_valid_bits Write loc) in
let state = kill zone state in
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 4d8a15d53eb..cb7c583d9e8 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -216,7 +216,7 @@ module Internal : Domain_builder.InputDomain
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
- let logic_assign _assign location ~pre:_ state =
+ let logic_assign _assign location state =
let loc = Precise_locs.imprecise_location location in
kill loc state
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 20f91dc4a99..f2e84f2c345 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -300,7 +300,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let incr_loop_counter _ state = state
let leave_loop _ state = state
- let logic_assign _assign location ~pre:_ state = remove location state
+ let logic_assign _assign location state = remove location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 91b53803645..9464308a6e2 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -631,7 +631,7 @@ module Internal : Domain_builder.InputDomain
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
- let logic_assign _assigns location ~pre:_ state =
+ let logic_assign _assigns location state =
let loc = Precise_locs.imprecise_location location in
Memory.kill loc state
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 4c533c30c2c..de5887617b6 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -931,7 +931,7 @@ module Internal = struct
Traces.add_trans state (Msg msg)
(* TODO *)
- let logic_assign _assign _location ~pre:_ state =
+ let logic_assign _assign _location state =
Traces.add_trans state (Msg "logic assign")
(* Logic *)
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5d1a5594218..c12cdfc9f3c 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -67,7 +67,7 @@ module Make
let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
let show_expr _ _ _ _ = ()
- let logic_assign _ _ ~pre:_ _ = ()
+ let logic_assign _ _ _ = ()
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ _ _ _ = `Value ()
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index d84a01a562d..4521648ffbb 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -267,7 +267,7 @@ module Make
let env = make_env state in
let assigns_with_locations = evaluate_locations env retres_loc assigns in
let transfer state (logic_assign, location) =
- Domain.logic_assign logic_assign location ~pre state
+ Domain.logic_assign (Some (logic_assign, pre)) location state
in
List.fold_left transfer state assigns_with_locations
--
GitLab