From a8f27afcda45c1c794bd08ddb076eee7784232a7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Feb 2021 15:19:30 +0100
Subject: [PATCH] [Eva] The evaluation engine gives a context record to domain
queries.
The context currently contains the fields:
- root: is the queried expression the root expression being evaluated, or is it
a subexpression?
- sudivision: the maximum number of subdivisions for the current evaluation.
- subdivided: is the evaluation being subdivided?
[root] is always set to false for subdivided evaluations.
---
src/plugins/value/domains/abstract_domain.mli | 32 +++++++++++++------
.../value/domains/apron/apron_domain.ml | 4 +--
.../value/domains/cvalue/cvalue_domain.ml | 4 +--
src/plugins/value/domains/domain_builder.ml | 16 +++++-----
src/plugins/value/domains/domain_lift.ml | 8 ++---
src/plugins/value/domains/domain_product.ml | 12 +++----
.../value/domains/equality/equality_domain.ml | 4 +--
.../value/domains/gauges/gauges_domain.ml | 4 +--
src/plugins/value/domains/inout_domain.ml | 4 +--
src/plugins/value/domains/octagons.ml | 4 +--
src/plugins/value/domains/offsm_domain.ml | 4 +--
src/plugins/value/domains/simple_memory.ml | 4 +--
src/plugins/value/domains/symbolic_locs.ml | 4 +--
src/plugins/value/domains/traces_domain.ml | 4 +--
src/plugins/value/domains/unit_domain.ml | 4 +--
src/plugins/value/engine/evaluation.ml | 10 +++---
16 files changed, 68 insertions(+), 54 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index fa7ff77ac1f..0e7d17f7ccc 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -112,6 +112,15 @@ module type Lattice = sig
without impeding the analysis: [meet x y = `Value x] is always sound. *)
end
+(** Context from the engine evaluation about a domain query. *)
+type evaluation_context = {
+ root: bool;
+ (** Is the queried expression the "root" expression being evaluated, or is it
+ a sub-expression? *)
+ subdivision: int;
+ (** Maximum number of subdivisions for the current evaluation.
+ See {!Subdivided_evaluation} for more details. *)
+}
(** Extraction of information: queries for values or locations inferred by a
domain about expressions and lvalues.
@@ -140,23 +149,26 @@ module type Queries = sig
(** When evaluating an expression, the evaluation engine asks the domains
for abstract values and alarms at each lvalue (via [extract_lval]) and
each sub-expressions (via [extract_expr]).
- In these queries, the [root] boolean is true for the root expression
- being evaluated, and false for all its sub-terms. *)
+ In these queries:
+ - [oracle] is an evaluation function and can be used to find the answer
+ by evaluating some others expressions, especially by relational domain.
+ No recursive evaluation should be done by this function.
+ - [context] record gives some information about
+ the current evaluation. *)
(** Query function for compound expressions:
- [eval oracle t exp] returns the known value of [exp] by the state [t].
- [oracle] is an evaluation function and can be used to find the answer
- by evaluating some others expressions, especially by relational domain.
- No recursive evaluation should be done by this function. *)
+ [extract_expr ~oracle context t exp] returns the known value of [exp]
+ by the state [t]. See above for more details on queries. *)
val extract_expr :
- oracle:(exp -> value evaluated) -> root:bool ->
+ oracle:(exp -> value evaluated) -> evaluation_context ->
state -> exp -> (value * origin option) evaluated
(** Query function for lvalues:
- [find oracle t lval typ loc] returns the known value stored at
- the location [loc] of the left value [lval] of type [typ]. *)
+ [extract_lval ~oracle context t lval typ loc] returns the known value
+ stored at the location [loc] of the left value [lval] of type [typ].
+ See above for more details on queries. *)
val extract_lval :
- oracle:(exp -> value evaluated) -> root:bool ->
+ oracle:(exp -> value evaluated) -> evaluation_context ->
state -> lval -> typ -> location -> (value * origin option) evaluated
(** [backward_location state lval typ loc v] reduces the location [loc] of the
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 0e8d896ce66..9c2d3e85184 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -487,10 +487,10 @@ module Make (Man : Input) = struct
apron state, whose environment raises the Failure exception. *)
| Z.Overflow | Failure _ -> top
- let extract_expr ~oracle:_ ~root:_ state expr =
+ let extract_expr ~oracle:_ _context state expr =
compute state expr (Cil.typeOf expr)
- let extract_lval ~oracle:_ ~root:_ state lval typ _loc =
+ let extract_lval ~oracle:_ _context state lval typ _loc =
let expr = Value_util.lval_to_exp lval in
compute state expr typ
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 3aa03b76dd4..efcf6121cb5 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -201,9 +201,9 @@ module State = struct
type origin = Model.origin
- let extract_expr ~oracle:_ ~root:_ (s, _) expr =
+ let extract_expr ~oracle:_ _context (s, _) expr =
Model.extract_expr s expr
- let extract_lval ~oracle:_ ~root:_ (s, _) lval typ loc =
+ let extract_lval ~oracle:_ _context (s, _) lval typ loc =
Model.extract_lval s lval typ loc
let backward_location (state, _) lval typ precise_loc value =
Model.backward_location state lval typ precise_loc value
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 9c69420202f..f19b48efa12 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -69,8 +69,8 @@ module Make_Minimal
let narrow x _y = `Value x
let top_answer = `Value (Value.top, None), Alarmset.all
- let extract_expr ~oracle:_ ~root:_ _state _expr = top_answer
- let extract_lval ~oracle:_ ~root:_ _state _lval _typ _location = top_answer
+ let extract_expr ~oracle:_ _context _state _expr = top_answer
+ let extract_lval ~oracle:_ _context _state _lval _typ _location = top_answer
let backward_location _state _lval _typ location value = `Value (location, value)
let reduce_further _state _expr _value = []
@@ -187,11 +187,11 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let narrow x _y = `Value x
- let extract_expr ~oracle:_ ~root:_ state expr =
+ let extract_expr ~oracle:_ _context state expr =
let v = Domain.extract_expr state expr >>-: fun v -> v, None in
v, Alarmset.all
- let extract_lval ~oracle:_ ~root:_ state lval typ location =
+ let extract_lval ~oracle:_ _context state lval typ location =
let v = Domain.extract_lval state lval typ location >>-: fun v -> v, None in
v, Alarmset.all
@@ -369,14 +369,14 @@ module Restrict
let default_query = `Value (Value.top, None), Alarmset.all
- let extract_expr ~oracle ~root state expr =
+ let extract_expr ~oracle context state expr =
make_query default_query
- (fun s -> Domain.extract_expr ~oracle ~root s expr) state
+ (fun s -> Domain.extract_expr ~oracle context s expr) state
- let extract_lval ~oracle ~root state lval typ location =
+ let extract_lval ~oracle context state lval typ location =
make_query
default_query
- (fun s -> Domain.extract_lval ~oracle ~root s lval typ location)
+ (fun s -> Domain.extract_lval ~oracle context s lval typ location)
state
let backward_location state lval typ location value =
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index a2fd37480d5..e93db09c859 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -53,15 +53,15 @@ module Make
type location = Convert.extended_location
type origin = Domain.origin
- let extract_expr ~oracle ~root state exp =
+ let extract_expr ~oracle context state exp =
let oracle exp = oracle exp >>=: Convert.restrict_val in
- Domain.extract_expr ~oracle ~root state exp >>=: fun (value, origin) ->
+ Domain.extract_expr ~oracle context state exp >>=: fun (value, origin) ->
Convert.extend_val value, origin
- let extract_lval ~oracle ~root state lval typ loc =
+ let extract_lval ~oracle context state lval typ loc =
let oracle exp = oracle exp >>=: Convert.restrict_val in
let loc = Convert.restrict_loc loc in
- Domain.extract_lval ~oracle ~root state lval typ loc
+ Domain.extract_lval ~oracle context state lval typ loc
>>=: fun (value, origin) ->
Convert.extend_val value, origin
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 43c9f9ec3dd..683892ef2dc 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -89,15 +89,15 @@ module Make
in
value, alarms
- let extract_expr ~oracle ~root (left, right) expr =
+ let extract_expr ~oracle context (left, right) expr =
merge
- (Left.extract_expr ~oracle ~root left expr)
- (Right.extract_expr ~oracle ~root right expr)
+ (Left.extract_expr ~oracle context left expr)
+ (Right.extract_expr ~oracle context right expr)
- let extract_lval ~oracle ~root (left, right) lval typ location =
+ let extract_lval ~oracle context (left, right) lval typ location =
merge
- (Left.extract_lval ~oracle ~root left lval typ location)
- (Right.extract_lval ~oracle ~root right lval typ location)
+ (Left.extract_lval ~oracle context left lval typ location)
+ (Right.extract_lval ~oracle context right lval typ location)
let backward_location (left, right) lval typ loc value =
(* TODO: Loc.narrow *)
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index d616ee51836..2849ec1f6f3 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -239,12 +239,12 @@ module Make
v, Alarmset.none
| None -> `Value (Value.top, None), Alarmset.all
- let extract_expr ~oracle ~root:_ (equalities, _, _) expr =
+ let extract_expr ~oracle _context (equalities, _, _) expr =
let expr = Cil.constFold true expr in
let atom_e = HCE.of_exp expr in
coop_eval oracle equalities atom_e
- let extract_lval ~oracle ~root:_ (equalities, _, _) lval _typ _location =
+ let extract_lval ~oracle _context (equalities, _, _) lval _typ _location =
let atom_lv = HCE.of_lval lval in
coop_eval oracle equalities atom_lv
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 9ffa7ce932c..0e41b58d91d 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1259,10 +1259,10 @@ module D_Impl : Abstract_domain.S
(* TODO: it would be interesting to return something here, but we
currently need a valuation to perform the translation. *)
- let extract_expr ~oracle:_ ~root:_ _state _exp =
+ let extract_expr ~oracle:_ _context _state _exp =
`Value (Cvalue.V.top, None), Alarmset.all
- let extract_lval ~oracle:_ ~root:_ state _lv typ loc =
+ let extract_lval ~oracle:_ _context state _lv typ loc =
let v =
try
let b = loc_to_base (Precise_locs.imprecise_location loc) typ in
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 4167145500e..a51098e16eb 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -271,8 +271,8 @@ module Internal
let top_query = `Value (Cvalue.V.top, None), Alarmset.all
- let extract_expr ~oracle:_ ~root:_ _state _expr = top_query
- let extract_lval ~oracle:_ ~root:_ _state _lv _typ _locs = top_query
+ let extract_expr ~oracle:_ _context _state _expr = top_query
+ let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
let backward_location _state _lval _typ loc value =
`Value (loc, value)
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index f8149f17cf6..2be0ff0dfa9 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1041,7 +1041,7 @@ module Domain = struct
let top_value = `Value (Cvalue.V.top, None), Alarmset.all
- let extract_expr ~oracle ~root:_ state expr =
+ let extract_expr ~oracle _context state expr =
let evaluate_expr expr =
match fst (oracle expr) with
| `Bottom -> `Top (* should not happen *)
@@ -1059,7 +1059,7 @@ module Domain = struct
then `Bottom, Alarmset.all
else `Value (Cvalue.V.inject_ival ival, None), alarms
- let extract_lval ~oracle:_ ~root:_ _t _lval _typ _loc = top_value
+ let extract_lval ~oracle:_ _context _t _lval _typ _loc = top_value
let backward_location _t _lval _typ loc value = `Value (loc, value)
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 236c27fe02a..a2d8355c3e2 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -163,7 +163,7 @@ module Internal : Domain_builder.InputDomain
let show_expr _valuation _state _fmt _expr = ()
- let extract_expr ~oracle:_ ~root:_ _state _exp =
+ let extract_expr ~oracle:_ _context _state _exp =
`Value (Offsm_value.Offsm.top, None), Alarmset.all
(* Basic 'find' on a location *)
@@ -176,7 +176,7 @@ module Internal : Domain_builder.InputDomain
then Offsm_value.Offsm.top
else O o
- let extract_lval ~oracle:_ ~root:_ state _lv typ locs =
+ let extract_lval ~oracle:_ _context state _lv typ locs =
let o =
if Cil.typeHasQualifier "volatile" typ ||
not (Cil.isArithmeticOrPointerType typ)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 97cb3f3e296..94a2f4c5f6c 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -196,11 +196,11 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
(* This function returns the information known about the location
corresponding to [_lv], so that it may be used by the engine during
evaluation. *)
- let extract_lval ~oracle:_ ~root:_ state _lv typ loc =
+ let extract_lval ~oracle:_ _context state _lv typ loc =
let v = find loc typ state in
`Value (v, None), Alarmset.all
- let extract_expr ~oracle:_ ~root:_ _state _expr =
+ let extract_expr ~oracle:_ _context _state _expr =
`Value (Value.top, None), Alarmset.all
let backward_location state _lval typ loc _value =
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index c56c7a592d1..2c2f51d88a2 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -576,12 +576,12 @@ module Internal : Domain_builder.InputDomain
this point. Hence, the alarms have already been emitted, and we can
return [Alarmset.none]. *)
- let extract_expr ~oracle:_ ~root:_ state expr =
+ let extract_expr ~oracle:_ _context state expr =
match Memory.find_expr expr state with
| None -> top_query
| Some v -> `Value (v, None), Alarmset.none
- let extract_lval ~oracle:_ ~root:_ state lv _typ _locs =
+ let extract_lval ~oracle:_ _context state lv _typ _locs =
match Memory.find_lval lv state with
| None -> top_query
| Some v -> `Value (v, None), Alarmset.none
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 408b6f10f97..ce718b03ee1 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -942,8 +942,8 @@ module Internal = struct
let top_query = `Value (Cvalue.V.top, None), Alarmset.all
- let extract_expr ~oracle:_ ~root:_ _state _expr = top_query
- let extract_lval ~oracle:_ ~root:_ _state _lv _typ _locs = top_query
+ let extract_expr ~oracle:_ _context _state _expr = top_query
+ let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
let backward_location _state _lval _typ loc value =
`Value (loc, value)
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 0460e6201db..5633d599dd5 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -55,8 +55,8 @@ module Make
type origin
let eval_top = `Value (Value.top, None), Alarmset.all
- let extract_expr ~oracle:_ ~root:_ _ _ = eval_top
- let extract_lval ~oracle:_ ~root:_ _ _ _ _ = eval_top
+ let extract_expr ~oracle:_ _ _ _ = eval_top
+ let extract_lval ~oracle:_ _ _ _ _ _ = eval_top
let backward_location _ _ _ loc value = `Value (loc, value)
let reduce_further _ _ _ = []
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 52d993be37b..477dee8f4e8 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -834,12 +834,13 @@ module Make
match expr.enode with
| Lval lval -> eval_lval context lval
| BinOp _ | UnOp _ | CastE _ -> begin
- let { state; root } = context in
+ let { state; root; subdivision } = context in
let context = { context with root = false } in
let oracle = make_oracle context in
let intern_value, alarms = internal_forward_eval context expr in
+ let eval_context = Abstract_domain.{ root; subdivision } in
let domain_value, alarms' =
- Domain.extract_expr ~oracle ~root state expr
+ Domain.extract_expr ~oracle eval_context state expr
in
(* Intersection of alarms, as each sets of alarms are correct
and "complete" for the evaluation of [expr]. *)
@@ -1067,7 +1068,7 @@ module Make
off, typ_res, volatile
and eval_lval ?(indeterminate=false) context lval =
- let { state; root } = context in
+ let { state; root; subdivision } = context in
let context = { context with root = false } in
let oracle = make_oracle context in
(* Computes the location of [lval]. *)
@@ -1081,7 +1082,8 @@ module Make
*)
let volatile = volatile_expr || Cil.typeHasQualifier "volatile" typ_lv in
(* Find the value of the location, if not bottom. *)
- let v, alarms = Domain.extract_lval ~oracle ~root state lval typ_lv loc in
+ let context = Abstract_domain.{ root; subdivision } in
+ let v, alarms = Domain.extract_lval ~oracle context state lval typ_lv loc in
let alarms = close_dereference_alarms lval alarms in
if indeterminate
then
--
GitLab