diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli index d45f5d4a2dbeeafe55f6acadc9af88fd7dee4a24..fa7ff77ac1f2868434ea60420c65c3826254026c 100644 --- a/src/plugins/value/domains/abstract_domain.mli +++ b/src/plugins/value/domains/abstract_domain.mli @@ -137,20 +137,26 @@ module type Queries = sig value of the expression [exp], and [o] is the origin of the value, which can be None. *) + (** 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. *) + (** 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. *) val extract_expr : - (exp -> value evaluated) -> + oracle:(exp -> value evaluated) -> root:bool -> 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]. *) val extract_lval : - (exp -> value evaluated) -> + oracle:(exp -> value evaluated) -> root:bool -> 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 3e3fb679f2888aeaa05d88ff27636c648b649703..0e8d896ce6685acc2f77cd89f79781949fc887ce 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 state expr = + let extract_expr ~oracle:_ ~root:_ state expr = compute state expr (Cil.typeOf expr) - let extract_lval _oracle state lval typ _loc = + let extract_lval ~oracle:_ ~root:_ 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 bc7868a1f805d6190468624a1ef56e91f041df07..3aa03b76dd440c601e6a60351904a7820bb89b4f 100644 --- a/src/plugins/value/domains/cvalue/cvalue_domain.ml +++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml @@ -40,7 +40,7 @@ module Model = struct function in cvalue_transfer. *) type origin = value - let extract_expr _ _ _ = `Value (Cvalue.V.top, None), Alarmset.all + let extract_expr _state _expr = `Value (Cvalue.V.top, None), Alarmset.all let indeterminate_alarms lval v = let open Cvalue.V_Or_Uninitialized in @@ -112,7 +112,7 @@ module Model = struct let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in v, alarms - let extract_lval _oracle state lval typ loc = + let extract_lval state lval typ loc = if Cil.isArithmeticOrPointerType typ then extract_scalar_lval state lval typ loc else extract_aggregate_lval state lval typ loc @@ -201,9 +201,10 @@ module State = struct type origin = Model.origin - let extract_expr evaluate (s, _) expr = Model.extract_expr evaluate s expr - let extract_lval oracle (s, _) lval typ loc = - Model.extract_lval oracle s lval typ loc + let extract_expr ~oracle:_ ~root:_ (s, _) expr = + Model.extract_expr s expr + let extract_lval ~oracle:_ ~root:_ (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 let reduce_further _ _ _ = [] diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml index 090ec84a602a7c9abc8082d368c70d16c1738105..9c69420202f21f768258d175a9aede0fc5b408e0 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 _state _expr = top_answer - let extract_lval _oracle _state _lval _typ _location = top_answer + let extract_expr ~oracle:_ ~root:_ _state _expr = top_answer + let extract_lval ~oracle:_ ~root:_ _state _lval _typ _location = top_answer let backward_location _state _lval _typ location value = `Value (location, value) let reduce_further _state _expr _value = [] @@ -187,15 +187,12 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue) let narrow x _y = `Value x - let extract_expr _oracle state expr = + let extract_expr ~oracle:_ ~root:_ state expr = let v = Domain.extract_expr state expr >>-: fun v -> v, None in v, Alarmset.all - let extract_lval _oracle state lval typ location = - let v = - Domain.extract_lval state lval typ location >>-: fun v -> - v, None - in + let extract_lval ~oracle:_ ~root:_ state lval typ location = + let v = Domain.extract_lval state lval typ location >>-: fun v -> v, None in v, Alarmset.all let backward_location _state _lval _typ location value = @@ -372,13 +369,14 @@ module Restrict let default_query = `Value (Value.top, None), Alarmset.all - let extract_expr oracle state expr = - make_query default_query (fun s -> Domain.extract_expr oracle s expr) state + let extract_expr ~oracle ~root state expr = + make_query default_query + (fun s -> Domain.extract_expr ~oracle ~root s expr) state - let extract_lval oracle state lval typ location = + let extract_lval ~oracle ~root state lval typ location = make_query default_query - (fun s -> Domain.extract_lval oracle s lval typ location) + (fun s -> Domain.extract_lval ~oracle ~root 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 1b0b7938ca82df8cea92695051efbf27b1d3babd..a2fd37480d59d073c6f9a941be300fcb09f519d4 100644 --- a/src/plugins/value/domains/domain_lift.ml +++ b/src/plugins/value/domains/domain_lift.ml @@ -53,15 +53,16 @@ module Make type location = Convert.extended_location type origin = Domain.origin - let extract_expr oracle state exp = + let extract_expr ~oracle ~root state exp = let oracle exp = oracle exp >>=: Convert.restrict_val in - Domain.extract_expr oracle state exp >>=: fun (value, origin) -> + Domain.extract_expr ~oracle ~root state exp >>=: fun (value, origin) -> Convert.extend_val value, origin - let extract_lval oracle state lval typ loc = + let extract_lval ~oracle ~root state lval typ loc = let oracle exp = oracle exp >>=: Convert.restrict_val in let loc = Convert.restrict_loc loc in - Domain.extract_lval oracle state lval typ loc >>=: fun (value, origin) -> + Domain.extract_lval ~oracle ~root state lval typ loc + >>=: fun (value, origin) -> Convert.extend_val value, origin let backward_location state lval typ loc value = diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml index 875cf9c4b655252059f607be6aed23572e7388e7..43c9f9ec3ddbba80b73130c1d1e4194552c42b81 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 (left, right) expr = + let extract_expr ~oracle ~root (left, right) expr = merge - (Left.extract_expr oracle left expr) - (Right.extract_expr oracle right expr) + (Left.extract_expr ~oracle ~root left expr) + (Right.extract_expr ~oracle ~root right expr) - let extract_lval oracle (left, right) lval typ location = + let extract_lval ~oracle ~root (left, right) lval typ location = merge - (Left.extract_lval oracle left lval typ location) - (Right.extract_lval oracle right lval typ location) + (Left.extract_lval ~oracle ~root left lval typ location) + (Right.extract_lval ~oracle ~root 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 45d2dd6562d0c784db4f6980fae40aae866ea40c..d616ee5183669465db21b1e08a2032d7878f1ebf 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: exp -> Value.t evaluated) (equalities, _, _) expr = + let extract_expr ~oracle ~root:_ (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 (equalities, _, _) lval _typ _location = + let extract_lval ~oracle ~root:_ (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 2617cd55e4d2209f8ba7f71db8b619a5832baf30..9ffa7ce932cc1ba134b47dafeb6660b914368b82 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 _state _exp = + let extract_expr ~oracle:_ ~root:_ _state _exp = `Value (Cvalue.V.top, None), Alarmset.all - let extract_lval _oracle state _lv typ loc = + let extract_lval ~oracle:_ ~root:_ 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 15e5f00ee7c0766b97dfdb24037f082111de299c..4167145500eec004412d373397eba6d991cd6004 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 _state _expr = top_query - let extract_lval _oracle _state _lv _typ _locs = top_query + let extract_expr ~oracle:_ ~root:_ _state _expr = top_query + let extract_lval ~oracle:_ ~root:_ _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 efce9ddb734dfa03ed131be2f42a91678b8b9243..f8149f17cf631d41850cade793c9143b6c18e562 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 state expr = + let extract_expr ~oracle ~root:_ 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 _t _lval _typ _loc = top_value + let extract_lval ~oracle:_ ~root:_ _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 2a4d4854be35e24a2e61f2971f7871f7c3996e9e..236c27fe02acde09ac02c2f5982deda3e7579f4d 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 _state _exp = + let extract_expr ~oracle:_ ~root:_ _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 state _lv typ locs = + let extract_lval ~oracle:_ ~root:_ 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 6cabd4da3f2b5a85ee3fc9759ee9b3e4bae2ba1c..97cb3f3e29637be412a46e6cd238a60144224468 100644 --- a/src/plugins/value/domains/simple_memory.ml +++ b/src/plugins/value/domains/simple_memory.ml @@ -196,11 +196,12 @@ 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 state _lv typ loc = + let extract_lval ~oracle:_ ~root:_ state _lv typ loc = let v = find loc typ state in `Value (v, None), Alarmset.all - let extract_expr _oracle _state _expr = `Value (Value.top, None), Alarmset.all + let extract_expr ~oracle:_ ~root:_ _state _expr = + `Value (Value.top, None), Alarmset.all let backward_location state _lval typ loc _value = let new_value = find loc typ state in diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml index 61a33252c51d31025f65854ce43d425e7979d5cd..c56c7a592d1102f9e40ec3ea1fb91233b6c2a8b5 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 state expr = + let extract_expr ~oracle:_ ~root:_ state expr = match Memory.find_expr expr state with | None -> top_query | Some v -> `Value (v, None), Alarmset.none - let extract_lval _oracle state lv _typ _locs = + let extract_lval ~oracle:_ ~root:_ 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 5dd2ac5bb9d925a853d14ac89d3c1fdb904bed86..408b6f10f97894ef91ef0a0d1863eead6e87ac8a 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 _state _expr = top_query - let extract_lval _oracle _state _lv _typ _locs = top_query + let extract_expr ~oracle:_ ~root:_ _state _expr = top_query + let extract_lval ~oracle:_ ~root:_ _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 75a3db212865817be796939c17f668328012e533..0460e6201db94376deaefffcafe460f362c9e82e 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 _ _ _ = eval_top - let extract_lval _ _ _ _ _ = eval_top + let extract_expr ~oracle:_ ~root:_ _ _ = eval_top + let extract_lval ~oracle:_ ~root:_ _ _ _ _ = 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 5e0eee53d7c87d3dd5bdff036883af2071653046..52d993be37bb5e68d7cfc1d8c39d68eaf8d2e65f 100644 --- a/src/plugins/value/engine/evaluation.ml +++ b/src/plugins/value/engine/evaluation.ml @@ -764,6 +764,9 @@ module Make type context = { (* The abstract domain state in which the evaluation takes place. *) state: Domain.t; + (* Is the expression currently processed the "root" expression being + evaluated, or is it a sub-expression? Useful for domain queries. *) + root: bool; (* Maximum number of subdivisions. See {!Subdivided_evaluation} for more details. *) subdivision: int; @@ -831,10 +834,13 @@ module Make match expr.enode with | Lval lval -> eval_lval context lval | BinOp _ | UnOp _ | CastE _ -> begin - let intern_value, alarms = internal_forward_eval context expr in - let state = context.state in + let { state; root } = context in + let context = { context with root = false } in let oracle = make_oracle context in - let domain_value, alarms' = Domain.extract_expr oracle state expr in + let intern_value, alarms = internal_forward_eval context expr in + let domain_value, alarms' = + Domain.extract_expr ~oracle ~root state expr + in (* Intersection of alarms, as each sets of alarms are correct and "complete" for the evaluation of [expr]. *) match Alarmset.inter alarms alarms' with @@ -1061,6 +1067,9 @@ module Make off, typ_res, volatile and eval_lval ?(indeterminate=false) context lval = + let { state; root } = context in + let context = { context with root = false } in + let oracle = make_oracle context in (* Computes the location of [lval]. *) lval_to_loc context ~for_writing:false ~reduction:true lval >>= fun (loc, typ_lv, volatile_expr) -> @@ -1072,8 +1081,7 @@ module Make *) let volatile = volatile_expr || Cil.typeHasQualifier "volatile" typ_lv in (* Find the value of the location, if not bottom. *) - let oracle = make_oracle context in - let v, alarms = Domain.extract_lval oracle context.state lval typ_lv loc in + let v, alarms = Domain.extract_lval ~oracle ~root state lval typ_lv loc in let alarms = close_dereference_alarms lval alarms in if indeterminate then @@ -1133,14 +1141,15 @@ module Make | None -> Value_parameters.LinearLevel.get () | Some n -> n in - { state; subdivision; remaining_fuel; oracle } + { state; root = true; subdivision; remaining_fuel; oracle } (* Context for a fast forward evaluation with minimal precision: - no subdivisions and no calls to the oracle. *) + no subdivisions, no calls to the oracle, and the expression is not + considered as a "root" expression. *) let fast_eval_context state = let remaining_fuel = no_fuel in let subdivision = 0 in - { state; subdivision; remaining_fuel; oracle } + { state; root = false; subdivision; remaining_fuel; oracle } let subdivided_forward_eval valuation ?subdivnb state expr = let context = root_context ?subdivnb state in