Commit a2c983f1 authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Eva] In abstract domains, slightly changes the queries signature.

Queries return an origin option instead of an origin.
Domains not using the origin simply return None, and no longer need to define
the origin type.
parent 9f68b5c3
......@@ -134,7 +134,8 @@ module type Queries = sig
- a value for the expression, which can be:
– `Bottom if its evaluation is infeasible;
– `Value (v, o) where [v] is an over-approximation of the abstract
value of the expression [exp], and [o] is the origin of the value. *)
value of the expression [exp], and [o] is the origin of the value,
which can be None. *)
(** Query function for compound expressions:
[eval oracle t exp] returns the known value of [exp] by the state [t].
......@@ -143,14 +144,14 @@ module type Queries = sig
No recursive evaluation should be done by this function. *)
val extract_expr :
(exp -> value evaluated) ->
state -> exp -> (value * origin) evaluated
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) ->
state -> lval -> typ -> location -> (value * origin) evaluated
state -> lval -> typ -> location -> (value * origin option) evaluated
(** [backward_location state lval typ loc v] reduces the location [loc] of the
lvalue [lval] of type [typ], so that only the locations that may have value
......
......@@ -360,7 +360,7 @@ module Make (Man : Input) = struct
type state = Man.t Abstract1.t
type value = Main_values.Interval.t
type location = Precise_locs.precise_location
type origin = unit
type origin
let man = Man.manager
let log_category = dkey
......@@ -463,7 +463,7 @@ module Make (Man : Input) = struct
let dummy_oracle _ exn = raise exn
let compute state expr typ =
let top = `Value (None, ()), Alarmset.all in
let top = `Value (None, None), Alarmset.all in
if not (is_relevant expr)
then top
else
......@@ -476,7 +476,7 @@ module Make (Man : Input) = struct
let value =
if Interval.is_bottom interval
then `Bottom
else `Value (interval_to_ival interval, ())
else `Value (interval_to_ival interval, None)
in
(* TODO: remove alarms if computation does not overflow *)
value, Alarmset.all
......
......@@ -38,7 +38,7 @@ module Model = struct
lvalue can be incomparable. The origin is then used to store the value from
the state, to later choose which value to keep. This is done by the update
function in cvalue_transfer. *)
type origin = value option
type origin = value
let extract_expr _ _ _ = `Value (Cvalue.V.top, None), Alarmset.all
......
......@@ -25,7 +25,7 @@ open Eval
open Cvalue.Model
type value = Main_values.CVal.t
type origin = value option
type origin = value
type location = Main_locations.PLoc.location
let unbottomize = function
......@@ -71,7 +71,7 @@ let update valuation t =
included in the other). We use some notion of cardinality of
abstract values to choose the best value to keep. *)
match record.origin with
| Some (Some previous_v) ->
| Some previous_v ->
let typ = Cil.typeOfLval lv in
if is_smaller_value typ v previous_v then v else previous_v
| _ -> v
......
......@@ -23,7 +23,7 @@
(** Transfer functions for the main domain of the Value analysis. *)
type value = Main_values.CVal.t
type origin = value option
type origin = value
type location = Main_locations.PLoc.location
include Abstract_domain.Transfer
......
......@@ -65,11 +65,11 @@ module Make_Minimal
type value = Value.t
type location = Location.location
type state = Domain.t
type origin = unit
type origin
let narrow x _y = `Value x
let top_answer = `Value (Value.top, ()), Alarmset.all
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 backward_location _state _lval _typ location value = `Value (location, value)
......@@ -184,16 +184,19 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type state = Domain.t
type origin = unit
type origin
let narrow x _y = `Value x
let extract_expr _oracle state expr =
let v = Domain.extract_expr state expr >>-: fun v -> v, () in
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, () in
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 =
......
......@@ -37,8 +37,8 @@ module Make
type location = Left.location
type origin = {
left: reductness * Left.origin;
right: reductness * Right.origin;
left: reductness * Left.origin option;
right: reductness * Right.origin option;
}
let () = incr counter
......@@ -85,7 +85,7 @@ module Make
else if Value.equal v2 Value.top then Created else Reduced
in
let origin = {left = left, o1; right = right, o2} in
value, origin
value, Some origin
in
value, alarms
......@@ -120,7 +120,7 @@ module Make
| Reduced, Some (Created, _) -> Created
| _ as x, _ -> x
in
let origin = Extlib.opt_map snd origin in
let origin = Extlib.may_map snd ~dft:None origin in
{ record with origin; reductness }
let lift_valuation side valuation =
......
......@@ -189,7 +189,7 @@ module Make
type value = Value.t
type location = Precise_locs.precise_location
type origin = unit
type origin
let reduce_further (equalities, _, _) expr value =
let atom = HCE.of_exp expr in
......@@ -232,12 +232,12 @@ module Make
in
let v = Equality.Equality.fold aux_eq equality (`Value Value.top) in
(* Remove the 'origin' information of garbled mixes. *)
let v = v >>-: fun v -> imprecise_origin v, () in
let v = v >>-: fun v -> imprecise_origin v, None in
(* All expressions used by the equality domain have already been evaluated
before during the analysis; alarms about those expressions have already
been emitted. *)
v, Alarmset.none
| None -> `Value (Value.top, ()), Alarmset.all
| None -> `Value (Value.top, None), Alarmset.all
let extract_expr (oracle: exp -> Value.t evaluated) (equalities, _, _) expr =
let expr = Cil.constFold true expr in
......
......@@ -1130,7 +1130,7 @@ module D_Impl : Abstract_domain.S
type value = Cvalue.V.t
type state = G.t
type location = Precise_locs.precise_location
type origin = unit
type origin
include G
......@@ -1260,7 +1260,7 @@ 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 =
`Value (Cvalue.V.top, ()), Alarmset.all
`Value (Cvalue.V.top, None), Alarmset.all
let extract_lval _oracle state _lv typ loc =
let v =
......@@ -1274,7 +1274,7 @@ module D_Impl : Abstract_domain.S
(* We can probably return an empty set of alarms when the value is known,
but the only possible alarms on lvalues are about indeterminateness,
and it is not clear that we know more than the Cvalue domain. *)
`Value (v, ()), Alarmset.all
`Value (v, None), Alarmset.all
let backward_location _state _lval _typ loc value = `Value (loc, value)
......
......@@ -213,7 +213,7 @@ module Internal
type state = inout
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin = unit
type origin
include (LatticeInout: sig
include Datatype.S_with_collections with type t = state
......@@ -269,7 +269,7 @@ module Internal
let storage () = true
let top_query = `Value (Cvalue.V.top, ()), Alarmset.all
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
......
......@@ -1037,9 +1037,9 @@ module Domain = struct
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin = unit
type origin
let top_value = `Value (Cvalue.V.top, ()), Alarmset.all
let top_value = `Value (Cvalue.V.top, None), Alarmset.all
let extract_expr oracle state expr =
let evaluate_expr expr =
......@@ -1057,7 +1057,7 @@ module Domain = struct
then top_value
else if Ival.is_bottom ival
then `Bottom, Alarmset.all
else `Value (Cvalue.V.inject_ival ival, ()), alarms
else `Value (Cvalue.V.inject_ival ival, None), alarms
let extract_lval _oracle _t _lval _typ _loc = top_value
......
......@@ -97,7 +97,7 @@ module Internal : Domain_builder.InputDomain
type value = offsm_or_top
type state = Memory.t
type location = Precise_locs.precise_location
type origin = unit (* ???? *)
type origin
include (Memory: sig
include Datatype.S_with_collections with type t = state
......@@ -164,7 +164,7 @@ module Internal : Domain_builder.InputDomain
let show_expr _valuation _state _fmt _expr = ()
let extract_expr _oracle _state _exp =
`Value (Offsm_value.Offsm.top, ()), Alarmset.all
`Value (Offsm_value.Offsm.top, None), Alarmset.all
(* Basic 'find' on a location *)
let find_loc state loc =
......@@ -181,7 +181,7 @@ module Internal : Domain_builder.InputDomain
if Cil.typeHasQualifier "volatile" typ ||
not (Cil.isArithmeticOrPointerType typ)
then
`Value (Top, ())
`Value (Top, None)
else
try
let aux_loc loc o =
......@@ -189,8 +189,8 @@ module Internal : Domain_builder.InputDomain
Bottom.join Offsm_value.Offsm.join o o'
in
Precise_locs.fold aux_loc locs `Bottom >>-: fun v ->
v, ()
with Abstract_interp.Error_Top -> `Value (Top, ())
v, None
with Abstract_interp.Error_Top -> `Value (Top, None)
in
o, Alarmset.all
......
......@@ -187,7 +187,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
type state = t
type value = Value.t
type location = Precise_locs.precise_location
type origin = unit
type origin
let log_category = Value_parameters.register_category ("d-" ^ Info.name)
......@@ -198,9 +198,9 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
evaluation. *)
let extract_lval _oracle state _lv typ loc =
let v = find loc typ state in
`Value (v, ()), Alarmset.all
`Value (v, None), Alarmset.all
let extract_expr _oracle _state _expr = `Value (Value.top, ()), Alarmset.all
let extract_expr _oracle _state _expr = `Value (Value.top, None), Alarmset.all
let backward_location state _lval typ loc _value =
let new_value = find loc typ state in
......
......@@ -466,7 +466,7 @@ module Internal : Domain_builder.InputDomain
type state = Memory.t
type value = V.t
type location = Precise_locs.precise_location
type origin = unit
type origin
include (Memory: sig
include Datatype.S_with_collections with type t = state
......@@ -569,7 +569,7 @@ module Internal : Domain_builder.InputDomain
let show_expr _valuation _state _fmt _expr = ()
let top_query = `Value (V.top, ()), Alarmset.all
let top_query = `Value (V.top, None), Alarmset.all
(* For extraction functions, if we have an information about the value,
this means that the key has been evaluated in all the paths that reach
......@@ -579,12 +579,12 @@ module Internal : Domain_builder.InputDomain
let extract_expr _oracle state expr =
match Memory.find_expr expr state with
| None -> top_query
| Some v -> `Value (v, ()), Alarmset.none
| Some v -> `Value (v, None), Alarmset.none
let extract_lval _oracle state lv _typ _locs =
match Memory.find_lval lv state with
| None -> top_query
| Some v -> `Value (v, ()), Alarmset.none
| Some v -> `Value (v, None), Alarmset.none
let backward_location _state _lval _typ loc value =
(* Nothing to do. We could check if [[lval]] intersects [value] and
......
......@@ -848,7 +848,7 @@ module Internal = struct
type nonrec state = state
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin = unit
type origin
include (Traces: sig
include Datatype.S_with_collections with type t = state
......@@ -940,7 +940,7 @@ module Internal = struct
let storage () = true
let top_query = `Value (Cvalue.V.top, ()), Alarmset.all
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
......
......@@ -52,9 +52,9 @@ module Make
include Static
type value = Value.t
type location = Loc.location
type origin = unit
type origin
let eval_top = `Value (Value.top, ()), Alarmset.all
let eval_top = `Value (Value.top, None), Alarmset.all
let extract_expr _ _ _ = eval_top
let extract_lval _ _ _ _ _ = eval_top
let backward_location _ _ _ loc value = `Value (loc, value)
......
......@@ -258,7 +258,7 @@ let indeterminate_copy lval result alarms =
let reductness = Unreduced in
let v, origin = match result with
| `Bottom -> `Bottom, None
| `Value (v, origin) -> `Value v, Some origin
| `Value (v, origin) -> `Value v, origin
in
let value = { v; initialized; escaping } in
let record = { value; origin; reductness; val_alarms = alarms} in
......@@ -853,7 +853,6 @@ module Make
in
let reduction =
update_reduction reduction (Value.equal intern_value result)
and origin = Some origin
and value = define_value result in
(* The proper alarms will be set in the record by forward_eval. *)
{value; origin; reductness; val_alarms = Alarmset.all},
......@@ -1084,7 +1083,6 @@ module Make
let v, alarms = assume_valid_value typ_lv lval (v, alarms) in
(v, alarms) >>=: fun (value, origin) ->
let value = define_value value
and origin = Some origin
and reductness, reduction =
if Alarmset.is_empty alarms then Unreduced, Neither else Reduced, Forward
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment