From 84d892b5ba5645b55d5bfdc7a80b9ab006a501de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 31 Jan 2020 17:27:35 +0100
Subject: [PATCH] [Eva] Removes the [Transfer] functor from abstract domains.
For abstract domains, the valuation is now a record of three functions:
[find], [fold] and [find_loc].
Adds a function in the evaluation engine to convert Valuation maps into
these records.
---
src/plugins/value/domains/abstract_domain.mli | 41 +-
.../value/domains/apron/apron_domain.ml | 227 +++++----
.../value/domains/cvalue/cvalue_domain.ml | 61 ++-
.../value/domains/cvalue/cvalue_transfer.ml | 416 ++++++++---------
.../value/domains/cvalue/cvalue_transfer.mli | 20 +-
src/plugins/value/domains/domain_builder.ml | 81 ++--
src/plugins/value/domains/domain_lift.ml | 71 +--
src/plugins/value/domains/domain_product.ml | 181 ++++----
.../value/domains/equality/equality_domain.ml | 435 +++++++++---------
.../value/domains/gauges/gauges_domain.ml | 193 ++++----
src/plugins/value/domains/inout_domain.ml | 63 +--
src/plugins/value/domains/octagons.ml | 246 +++++-----
src/plugins/value/domains/offsm_domain.ml | 100 ++--
src/plugins/value/domains/simple_memory.ml | 178 ++++---
src/plugins/value/domains/symbolic_locs.ml | 168 ++++---
src/plugins/value/domains/traces_domain.ml | 105 ++---
src/plugins/value/domains/unit_domain.ml | 19 +-
src/plugins/value/engine/evaluation.ml | 6 +
src/plugins/value/engine/evaluation.mli | 5 +
src/plugins/value/engine/transfer_stmt.ml | 26 +-
src/plugins/value/partitioning/partition.ml | 5 +-
src/plugins/value/register.ml | 4 +-
22 files changed, 1236 insertions(+), 1415 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 1b8ed544fad..16a7dc6c6d7 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -164,21 +164,26 @@ module type Queries = sig
end
(** Results of an evaluation: the results of all intermediate calculation (the
- value of each expression and the location of each lvalue) are cached in a
- map. *)
-module type Valuation = sig
- type t
- type value (** Abstract value. *)
- type origin (** Origin of abstract values. *)
- type loc (** Abstract memory location. *)
- val find : t -> exp -> (value, origin) record_val or_top
- val fold : (exp -> (value, origin) record_val -> 'a -> 'a) -> t -> 'a -> 'a
- val find_loc : t -> lval -> loc record_loc or_top
-end
+ value of each expression and the location of each lvalue) are available for
+ the domain. *)
+type ('value, 'location, 'origin) valuation =
+ {
+ find: exp -> ('value, 'origin) record_val or_top;
+ (** Finds the value computed for an expression. The returned record also
+ contains the origin given by the domain for this expression, the alarms
+ emitted by its evaluation, and whether its value has been reduced.
+ Returns `Top if the expression has not been evaluated. *)
+ fold: 'a. (exp -> ('value, 'origin) record_val -> 'a -> 'a) -> 'a -> 'a;
+ (** [fold f e] applies [f expr record] to any expression [expr] evaluated
+ to [record], which contains its value, reduction, origin, and alarms. *)
+ find_loc: lval -> 'location record_loc or_top
+ (** Finds the location computed for an lvalue. The returned record also
+ contains the lvalue type and the alarms emitted by its evaluation.
+ Returns `Top if the lvalue has not been evaluated. *)
+ }
(** Transfer function of the domain. *)
module type Transfer = sig
-
type state
type value
type location
@@ -324,14 +329,10 @@ module type S = sig
(** Transfer functions from the result of evaluations.
See {eval.mli} for more details about valuation. *)
- module Transfer
- (Valuation: Valuation with type value = value
- and type origin = origin
- and type loc = location)
- : Transfer with type state := t
- and type value := value
- and type location := location
- and type valuation := Valuation.t
+ include Transfer with type state := t
+ and type value := value
+ and type location := location
+ and type valuation := (value, location, origin) valuation
(** {3 Logic } *)
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 15035124c40..22cd1448509 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -360,6 +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
let man = Man.manager
let log_category = dkey
@@ -427,8 +428,6 @@ module Make (Man : Input) = struct
let s = Abstract1.meet man s1 s2 in
if Abstract1.is_bottom man s then `Bottom else `Value s
- type origin = unit
-
let make_eval state =
let env = Abstract1.env state in
fun e ->
@@ -555,130 +554,124 @@ module Make (Man : Input) = struct
let incr_loop_counter _ state = state
let leave_loop _ state = state
- module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type loc = location)
- = struct
-
- (* make an oracle for the translation Cil->Apron, using the valuation.
- Translate integer expressions that have been evaluated (which should
- be all of them if the translation is called on a source expression!)
- into Apron intervals. *)
- let make_oracle valuation =
- fun exp exn ->
- if Cil.isIntegralType (Cil.typeOf exp) then
- match Valuation.find valuation exp with
- | `Value { value = { v = `Value itv } } ->
- let interval = ival_to_interval itv in
- Texpr1.Cst (Coeff.Interval interval)
- | _ -> raise exn
- else raise exn
-
- let update valuation state =
- let eval = make_eval state in
- let oracle = make_oracle valuation in
- let env = Abstract1.env state in
- (* Makes a list of apron constraints from a valuation:
- for each value marked as Reduced for an expression, creates the
- apron constraint [expression = value]. *)
- let gather_constraints exp record acc =
- if record.reductness = Reduced
- then
- try
- let expr = translate_expr_linearize eval oracle exp in
- let expr = coerce eval (Cil.typeOf exp) expr in
- (* When the value is top or bottom, no constraint is expressible. *)
- let cons = record.value.v >>- fun ival ->
- let interval = ival_to_interval ival in
- if Interval.is_top interval
- then `Bottom
- else `Value (constraint_reduction env expr interval)
- in
- Bottom.add_to_list cons acc
- with Out_of_Scope _ -> acc
- else acc
+ (* make an oracle for the translation Cil->Apron, using the valuation.
+ Translate integer expressions that have been evaluated (which should
+ be all of them if the translation is called on a source expression!)
+ into Apron intervals. *)
+ let make_oracle valuation =
+ fun exp exn ->
+ if Cil.isIntegralType (Cil.typeOf exp) then
+ match valuation.Abstract_domain.find exp with
+ | `Value { value = { v = `Value itv } } ->
+ let interval = ival_to_interval itv in
+ Texpr1.Cst (Coeff.Interval interval)
+ | _ -> raise exn
+ else raise exn
+
+ let update valuation state =
+ let eval = make_eval state in
+ let oracle = make_oracle valuation in
+ let env = Abstract1.env state in
+ (* Makes a list of apron constraints from a valuation:
+ for each value marked as Reduced for an expression, creates the
+ apron constraint [expression = value]. *)
+ let gather_constraints exp record acc =
+ if record.reductness = Reduced
+ then
+ try
+ let expr = translate_expr_linearize eval oracle exp in
+ let expr = coerce eval (Cil.typeOf exp) expr in
+ (* When the value is top or bottom, no constraint is expressible. *)
+ let cons = record.value.v >>- fun ival ->
+ let interval = ival_to_interval ival in
+ if Interval.is_top interval
+ then `Bottom
+ else `Value (constraint_reduction env expr interval)
+ in
+ Bottom.add_to_list cons acc
+ with Out_of_Scope _ -> acc
+ else acc
+ in
+ let constraints = valuation.Abstract_domain.fold gather_constraints [] in
+ if constraints = []
+ then `Value state
+ else meet_with_constraints env state constraints
+
+ let assign _stmt lvalue expr _value valuation state =
+ update valuation state >>- fun state ->
+ try
+ let state =
+ try
+ let eval = make_eval state in
+ let oracle = make_oracle valuation in
+ let var = translate_lval lvalue.lval in
+ let expr = expr in
+ let exp = translate_expr_linearize eval oracle expr in
+ let exp = coerce eval lvalue.ltyp exp in
+ let exp = Texpr1.of_expr (Abstract1.env state) exp in
+ (* TODO: currently, all variables are present in the environment
+ at all times. Change to a dynamic environment, in which new
+ variables are added here, and removed when the scope changes. *)
+ Abstract1.assign_texpr man state var exp None
+ with
+ | Out_of_Scope _ -> kill_bases lvalue.lloc state
in
- let constraints = Valuation.fold gather_constraints valuation [] in
- if constraints = []
- then `Value state
- else meet_with_constraints env state constraints
+ maybe_bottom state
+ with Manager.Error exclog -> abort exclog
- let assign _stmt lvalue expr _value valuation state =
- update valuation state >>- fun state ->
- try
- let state =
- try
- let eval = make_eval state in
- let oracle = make_oracle valuation in
- let var = translate_lval lvalue.lval in
- let expr = expr in
- let exp = translate_expr_linearize eval oracle expr in
- let exp = coerce eval lvalue.ltyp exp in
- let exp = Texpr1.of_expr (Abstract1.env state) exp in
- (* TODO: currently, all variables are present in the environment
- at all times. Change to a dynamic environment, in which new
- variables are added here, and removed when the scope changes. *)
- Abstract1.assign_texpr man state var exp None
- with
- | Out_of_Scope _ -> kill_bases lvalue.lloc state
- in
- maybe_bottom state
- with Manager.Error exclog -> abort exclog
+ let assume _stmt exp bool valuation state =
+ update valuation state >>- fun state ->
+ try
+ let env = Abstract1.env state in
+ let eval = make_eval state in
+ let oracle = make_oracle valuation in
+ let cons = constraint_expr eval oracle env exp bool in
+ let array = Tcons1.array_make env 1 in
+ Tcons1.array_set array 0 cons;
+ let state = Abstract1.meet_tcons_array man state array in
+ maybe_bottom state
+ with
+ | Out_of_Scope _ -> `Value state
- let assume _stmt exp bool valuation state =
- update valuation state >>- fun state ->
+ let start_call _stmt call valuation state =
+ update valuation state >>- fun state ->
+ let eval = make_eval state in
+ let oracle = make_oracle valuation in
+ let process_argument (vars, acc) arg =
try
let env = Abstract1.env state in
- let eval = make_eval state in
- let oracle = make_oracle valuation in
- let cons = constraint_expr eval oracle env exp bool in
- let array = Tcons1.array_make env 1 in
- Tcons1.array_set array 0 cons;
- let state = Abstract1.meet_tcons_array man state array in
- maybe_bottom state
+ let var = translate_varinfo arg.formal in
+ let vars = var :: vars in
+ let acc =
+ try
+ let exp = translate_expr_linearize eval oracle arg.concrete in
+ let texp = Texpr1.of_expr env exp in
+ (var, texp) :: acc
+ with Out_of_Scope _ -> acc
+ in
+ vars, acc
with
- | Out_of_Scope _ -> `Value state
-
- let start_call _stmt call valuation state =
- update valuation state >>- fun state ->
- let eval = make_eval state in
- let oracle = make_oracle valuation in
- let process_argument (vars, acc) arg =
- try
- let env = Abstract1.env state in
- let var = translate_varinfo arg.formal in
- let vars = var :: vars in
- let acc =
- try
- let exp = translate_expr_linearize eval oracle arg.concrete in
- let texp = Texpr1.of_expr env exp in
- (var, texp) :: acc
- with Out_of_Scope _ -> acc
- in
- vars, acc
- with
- | Out_of_Scope _ -> (vars, acc)
- in
- let vars, list = List.fold_left process_argument ([], []) call.arguments in
- let env = Abstract1.env state in
- let vars_array = Array.of_list vars in
- let env = Environment.add env vars_array [||] in
- let vars, texprs = List.split list in
- let vars_array = Array.of_list vars
- and texprs_array = Array.of_list texprs in
- let state = Abstract1.change_environment man state env false in
- let state =
- Abstract1.assign_texpr_array man state vars_array texprs_array None
- in
- if Abstract1.is_bottom man state
- then `Bottom
- else `Value state
+ | Out_of_Scope _ -> (vars, acc)
+ in
+ let vars, list = List.fold_left process_argument ([], []) call.arguments in
+ let env = Abstract1.env state in
+ let vars_array = Array.of_list vars in
+ let env = Environment.add env vars_array [||] in
+ let vars, texprs = List.split list in
+ let vars_array = Array.of_list vars
+ and texprs_array = Array.of_list texprs in
+ let state = Abstract1.change_environment man state env false in
+ let state =
+ Abstract1.assign_texpr_array man state vars_array texprs_array None
+ in
+ if Abstract1.is_bottom man state
+ then `Bottom
+ else `Value state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call ~pre:_ ~post = `Value post
- let show_expr _valuation _state _fmt _expr = ()
- end
+ let show_expr _valuation _state _fmt _expr = ()
let logic_assign _assigns location ~pre:_ state = kill_bases location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index cf96cb4f363..13142d74dcb 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -208,45 +208,40 @@ module State = struct
Model.backward_location state lval typ precise_loc value
let reduce_further _ _ _ = []
+ (* ------------------------------------------------------------------------ *)
+ (* Transfer Functions *)
+ (* ------------------------------------------------------------------------ *)
- module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = location)
- = struct
-
- module T = Cvalue_transfer.Transfer (Valuation)
-
- let update valuation (s, clob) = T.update valuation s >>-: fun s -> s, clob
+ let update valuation (s, clob) =
+ Cvalue_transfer.update valuation s >>-: fun s -> s, clob
- let assign stmt lv expr assigned valuation (s, clob) =
- T.assign stmt lv expr assigned valuation s >>-: fun s ->
- (* TODO: use the value in assignment *)
- let _ =
- Eval.value_assigned assigned >>-: fun value ->
- let location = Precise_locs.imprecise_location lv.lloc in
- Locals_scoping.remember_if_locals_in_value clob location value
- in
- s, clob
+ let assign stmt lv expr assigned valuation (s, clob) =
+ Cvalue_transfer.assign stmt lv expr assigned valuation s >>-: fun s ->
+ (* TODO: use the value in assignment *)
+ let _ =
+ Eval.value_assigned assigned >>-: fun value ->
+ let location = Precise_locs.imprecise_location lv.lloc in
+ Locals_scoping.remember_if_locals_in_value clob location value
+ in
+ s, clob
- let assume stmt expr positive valuation (s, clob) =
- T.assume stmt expr positive valuation s >>-: fun s ->
- s, clob
+ let assume stmt expr positive valuation (s, clob) =
+ Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
+ s, clob
- let start_call stmt call valuation (s, _clob) =
- T.start_call stmt call valuation s >>-: fun state ->
- state, Locals_scoping.bottom ()
+ let start_call stmt call valuation (s, _clob) =
+ Cvalue_transfer.start_call stmt call valuation s >>-: fun state ->
+ state, Locals_scoping.bottom ()
- let finalize_call stmt call ~pre ~post =
- let (post_state, post_clob) = post
- and pre_state, clob = pre in
- Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
- T.finalize_call stmt call ~pre:pre_state ~post:post_state
- >>-: fun state ->
- state, clob
+ let finalize_call stmt call ~pre ~post =
+ let (post_state, post_clob) = post
+ and pre_state, clob = pre in
+ Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
+ Cvalue_transfer.finalize_call stmt call ~pre:pre_state ~post:post_state
+ >>-: fun state ->
+ state, clob
- let show_expr valuation (state, _) = T.show_expr valuation state
- end
+ let show_expr valuation (state, _) = Cvalue_transfer.show_expr valuation state
(* ------------------------------------------------------------------------ *)
(* Mem Exec *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 1e9065ac7f3..a0f76b6a4a5 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -22,230 +22,220 @@
open Cil_types
open Eval
-
open Cvalue.Model
type value = Main_values.CVal.t
+type origin = value option
type location = Main_locations.PLoc.location
-
let unbottomize = function
| `Bottom -> Cvalue.V.bottom
| `Value v -> v
-module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type origin = value option
- and type loc = location)
-= struct
-
- type state = Cvalue.Model.t
-
- (* ---------------------------------------------------------------------- *)
- (* Assumptions *)
- (* ---------------------------------------------------------------------- *)
-
- let reduce valuation lval value t =
- let typ = Cil.typeOfLval lval in
+(* ---------------------------------------------------------------------- *)
+(* Assumptions *)
+(* ---------------------------------------------------------------------- *)
+
+let reduce valuation lval value t =
+ let typ = Cil.typeOfLval lval in
+ if Cil.typeHasQualifier "volatile" typ
+ then t
+ else
+ match valuation.Abstract_domain.find_loc lval with
+ | `Value record ->
+ let loc = Precise_locs.imprecise_location record.loc in
+ if Locations.cardinal_zero_or_one loc
+ then reduce_indeterminate_binding t loc value
+ else t
+ | `Top -> t (* Cannot reduce without the location of the lvalue. *)
+
+let is_smaller_value typ v1 v2 =
+ let size = Integer.of_int (Cil.bitsSizeOf typ) in
+ let card1 = Cvalue.V.cardinal_estimate v1 ~size
+ and card2 = Cvalue.V.cardinal_estimate v2 ~size in
+ Integer.lt card1 card2
+
+(* Update the state according to a Valuation. *)
+let update valuation t =
+ let process exp record t =
+ match exp.enode with
+ | Lval lv ->
+ if record.reductness = Reduced
+ then
+ let {v; initialized; escaping} = record.value in
+ let v = unbottomize v in
+ let v =
+ (* The origin contains the value already stored in the state, when
+ its type is incompatible with the lvalue [lv]. The precision of
+ this previous value and [v] are then incomparable (none is
+ 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) ->
+ let typ = Cil.typeOfLval lv in
+ if is_smaller_value typ v previous_v then v else previous_v
+ | _ -> v
+ in
+ let value = Cvalue.V_Or_Uninitialized.make ~initialized ~escaping v in
+ reduce valuation lv value t
+ else t
+ | _ -> t
+ in
+ valuation.Abstract_domain.fold process t
+
+(* ---------------------------------------------------------------------- *)
+(* Assignments *)
+(* ---------------------------------------------------------------------- *)
+
+let write_abstract_value state (lval, loc, typ) assigned_value =
+ let {v; initialized; escaping} = assigned_value in
+ let value = unbottomize v in
+ Warn.warn_right_exp_imprecision lval loc value;
+ let value =
if Cil.typeHasQualifier "volatile" typ
- then t
- else
- match Valuation.find_loc valuation lval with
- | `Value record ->
- let loc = Precise_locs.imprecise_location record.loc in
- if Locations.cardinal_zero_or_one loc
- then reduce_indeterminate_binding t loc value
- else t
- | `Top -> t (* Cannot reduce without the location of the lvalue. *)
-
- let is_smaller_value typ v1 v2 =
- let size = Integer.of_int (Cil.bitsSizeOf typ) in
- let card1 = Cvalue.V.cardinal_estimate v1 ~size
- and card2 = Cvalue.V.cardinal_estimate v2 ~size in
- Integer.lt card1 card2
-
- (* Update the state according to a Valuation. *)
- let update valuation t =
- let process exp record t =
- match exp.enode with
- | Lval lv ->
- if record.reductness = Reduced
- then
- let {v; initialized; escaping} = record.value in
- let v = unbottomize v in
- let v =
- (* The origin contains the value already stored in the state, when
- its type is incompatible with the lvalue [lv]. The precision of
- this previous value and [v] are then incomparable (none is
- 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) ->
- let typ = Cil.typeOfLval lv in
- if is_smaller_value typ v previous_v then v else previous_v
- | _ -> v
- in
- let value = Cvalue.V_Or_Uninitialized.make ~initialized ~escaping v in
- reduce valuation lv value t
- else t
- | _ -> t
- in
- Valuation.fold process valuation t
-
- (* ---------------------------------------------------------------------- *)
- (* Assignments *)
- (* ---------------------------------------------------------------------- *)
-
- let write_abstract_value state (lval, loc, typ) assigned_value =
- let {v; initialized; escaping} = assigned_value in
- let value = unbottomize v in
- Warn.warn_right_exp_imprecision lval loc value;
+ then Cvalue_forward.make_volatile value
+ else value
+ in
+ match loc.Locations.loc with
+ | Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
+ Value_parameters.result
+ "State before degeneration:@\n======%a@\n======="
+ Cvalue.Model.pretty state;
+ Value_util.warning_once_current
+ "writing at a completely unknown address@[%a@].@\nAborting."
+ Origin.pretty_as_reason orig;
+ raise Db.Value.Aborted
+ | _ ->
+ let exact = Locations.cardinal_zero_or_one loc in
let value =
- if Cil.typeHasQualifier "volatile" typ
- then Cvalue_forward.make_volatile value
- else value
- in
- match loc.Locations.loc with
- | Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
- Value_parameters.result
- "State before degeneration:@\n======%a@\n======="
- Cvalue.Model.pretty state;
- Value_util.warning_once_current
- "writing at a completely unknown address@[%a@].@\nAborting."
- Origin.pretty_as_reason orig;
- raise Db.Value.Aborted
- | _ ->
- let exact = Locations.cardinal_zero_or_one loc in
- let value =
- Cvalue.V_Or_Uninitialized.make ~initialized ~escaping value in
- (* let value = Cvalue.V_Or_Uninitialized.initialized value in *)
- add_indeterminate_binding ~exact state loc value
-
- exception Do_assign_imprecise_copy
-
- let copy_one_loc state left_lv right_lv =
- let left_lval, left_loc, left_typ = left_lv
- and right_lval, right_loc, right_typ = right_lv in
- (* Warn if right_loc is imprecise *)
- Warn.warn_imprecise_lval_read right_lval right_loc Cvalue.V.bottom;
- (* top size is tested before this function is called, in which case
- the imprecise copy mode is used. *)
- let size = Int_Base.project right_loc.Locations.size in
- let offsetmap = copy_offsetmap right_loc.Locations.loc size state in
- let make_volatile =
- Cil.typeHasQualifier "volatile" left_typ ||
- Cil.typeHasQualifier "volatile" right_typ
- in
- match offsetmap with
- | `Bottom -> `Bottom
- | `Value offsm ->
- (* TODO: this is the good place to handle partially volatile
- struct, whether as source or destination *)
- let offsetmap =
- if make_volatile then
- Cvalue.V_Offsetmap.map_on_values
- (Cvalue.V_Or_Uninitialized.map Cvalue_forward.make_volatile) offsm
- else offsm
- in
- if not (Eval_typ.offsetmap_matches_type left_typ offsetmap) then
- raise Do_assign_imprecise_copy;
- Cvalue_offsetmap.warn_right_imprecision left_lval left_loc offsetmap;
- `Value
- (paste_offsetmap ~exact:true
- ~from:offsetmap ~dst_loc:left_loc.Locations.loc ~size state)
-
- let make_determinate value =
- { v = `Value value; initialized = true; escaping = false }
-
- let copy_right_lval state left_lv right_lv copied_value =
- let lval, loc, typ = left_lv in
- (* Size mismatch between left and right size, or imprecise size.
- This cannot be done by copies, but require a conversion *)
- let right_size = Main_locations.PLoc.size right_lv.lloc
- and left_size = Main_locations.PLoc.size loc in
- if not (Int_Base.equal left_size right_size) || Int_Base.is_top right_size
- then
- fun loc -> write_abstract_value state (lval, loc, typ) copied_value
- else
- fun loc ->
- try
- let process right_loc acc =
- let left_lv = lval, loc, typ
- and right_lv = right_lv.lval, right_loc, right_lv.ltyp in
- match copy_one_loc state left_lv right_lv with
- | `Bottom -> acc
- | `Value state -> join acc state
- in
- Precise_locs.fold process right_lv.lloc bottom
- with
- Do_assign_imprecise_copy ->
- write_abstract_value state (lval, loc, typ) copied_value
-
- let assign _stmt { lval; ltyp; lloc } _expr assigned valuation state =
- let state = update valuation state in
- let assign_one_loc =
- match assigned with
- | Assign value ->
- let assigned_value = make_determinate value in
- fun loc -> write_abstract_value state (lval, loc, ltyp) assigned_value
- | Copy (right_lv, copied_value) ->
- copy_right_lval state (lval, lloc, ltyp) right_lv copied_value
- in
- let aux_loc loc acc_state =
- let s = assign_one_loc loc in
- join acc_state s
+ Cvalue.V_Or_Uninitialized.make ~initialized ~escaping value in
+ (* let value = Cvalue.V_Or_Uninitialized.initialized value in *)
+ add_indeterminate_binding ~exact state loc value
+
+exception Do_assign_imprecise_copy
+
+let copy_one_loc state left_lv right_lv =
+ let left_lval, left_loc, left_typ = left_lv
+ and right_lval, right_loc, right_typ = right_lv in
+ (* Warn if right_loc is imprecise *)
+ Warn.warn_imprecise_lval_read right_lval right_loc Cvalue.V.bottom;
+ (* top size is tested before this function is called, in which case
+ the imprecise copy mode is used. *)
+ let size = Int_Base.project right_loc.Locations.size in
+ let offsetmap = copy_offsetmap right_loc.Locations.loc size state in
+ let make_volatile =
+ Cil.typeHasQualifier "volatile" left_typ ||
+ Cil.typeHasQualifier "volatile" right_typ
+ in
+ match offsetmap with
+ | `Bottom -> `Bottom
+ | `Value offsm ->
+ (* TODO: this is the good place to handle partially volatile
+ struct, whether as source or destination *)
+ let offsetmap =
+ if make_volatile then
+ Cvalue.V_Offsetmap.map_on_values
+ (Cvalue.V_Or_Uninitialized.map Cvalue_forward.make_volatile) offsm
+ else offsm
in
- let state = Precise_locs.fold aux_loc lloc bottom in
- if not (is_reachable state)
- then `Bottom
- else `Value state
-
- (* ---------------------------------------------------------------------- *)
- (* Function Calls *)
- (* ---------------------------------------------------------------------- *)
-
- let actualize_formals state arguments =
- let treat_one_formal state arg =
- let offsm =
- Cvalue_offsetmap.offsetmap_of_assignment state arg.concrete arg.avalue
- in
- Cvalue.Model.add_base (Base.of_varinfo arg.formal) offsm state
+ if not (Eval_typ.offsetmap_matches_type left_typ offsetmap) then
+ raise Do_assign_imprecise_copy;
+ Cvalue_offsetmap.warn_right_imprecision left_lval left_loc offsetmap;
+ `Value
+ (paste_offsetmap ~exact:true
+ ~from:offsetmap ~dst_loc:left_loc.Locations.loc ~size state)
+
+let make_determinate value =
+ { v = `Value value; initialized = true; escaping = false }
+
+let copy_right_lval state left_lv right_lv copied_value =
+ let lval, loc, typ = left_lv in
+ (* Size mismatch between left and right size, or imprecise size.
+ This cannot be done by copies, but require a conversion *)
+ let right_size = Main_locations.PLoc.size right_lv.lloc
+ and left_size = Main_locations.PLoc.size loc in
+ if not (Int_Base.equal left_size right_size) || Int_Base.is_top right_size
+ then
+ fun loc -> write_abstract_value state (lval, loc, typ) copied_value
+ else
+ fun loc ->
+ try
+ let process right_loc acc =
+ let left_lv = lval, loc, typ
+ and right_lv = right_lv.lval, right_loc, right_lv.ltyp in
+ match copy_one_loc state left_lv right_lv with
+ | `Bottom -> acc
+ | `Value state -> join acc state
+ in
+ Precise_locs.fold process right_lv.lloc bottom
+ with
+ Do_assign_imprecise_copy ->
+ write_abstract_value state (lval, loc, typ) copied_value
+
+let assign _stmt { lval; ltyp; lloc } _expr assigned valuation state =
+ let state = update valuation state in
+ let assign_one_loc =
+ match assigned with
+ | Assign value ->
+ let assigned_value = make_determinate value in
+ fun loc -> write_abstract_value state (lval, loc, ltyp) assigned_value
+ | Copy (right_lv, copied_value) ->
+ copy_right_lval state (lval, lloc, ltyp) right_lv copied_value
+ in
+ let aux_loc loc acc_state =
+ let s = assign_one_loc loc in
+ join acc_state s
+ in
+ let state = Precise_locs.fold aux_loc lloc bottom in
+ if not (is_reachable state)
+ then `Bottom
+ else `Value state
+
+(* ---------------------------------------------------------------------- *)
+(* Function Calls *)
+(* ---------------------------------------------------------------------- *)
+
+let actualize_formals state arguments =
+ let treat_one_formal state arg =
+ let offsm =
+ Cvalue_offsetmap.offsetmap_of_assignment state arg.concrete arg.avalue
in
- List.fold_left treat_one_formal state arguments
-
- let start_call _stmt call valuation state =
- let state = update valuation state in
- let with_formals = actualize_formals state call.arguments in
- let stack_with_call = Value_util.call_stack () in
- Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
- `Value with_formals
-
- let finalize_call stmt call ~pre:_ ~post:state =
- (* Deallocate memory allocated via alloca().
- To minimize computations, only do it for function definitions. *)
- let state' =
- if Kernel_function.is_definition call.kf then
- let stack = (call.kf, Kstmt stmt) :: (Value_util.call_stack ()) in
- Builtins_malloc.free_automatic_bases stack state
- else state
+ Cvalue.Model.add_base (Base.of_varinfo arg.formal) offsm state
+ in
+ List.fold_left treat_one_formal state arguments
+
+let start_call _stmt call valuation state =
+ let state = update valuation state in
+ let with_formals = actualize_formals state call.arguments in
+ let stack_with_call = Value_util.call_stack () in
+ Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
+ `Value with_formals
+
+let finalize_call stmt call ~pre:_ ~post:state =
+ (* Deallocate memory allocated via alloca().
+ To minimize computations, only do it for function definitions. *)
+ let state' =
+ if Kernel_function.is_definition call.kf then
+ let stack = (call.kf, Kstmt stmt) :: (Value_util.call_stack ()) in
+ Builtins_malloc.free_automatic_bases stack state
+ else state
+ in
+ `Value state'
+
+let show_expr valuation state fmt expr =
+ match expr.enode with
+ | Lval lval ->
+ let record = match valuation.Abstract_domain.find_loc lval with
+ | `Value record -> record
+ | `Top -> assert false
in
- `Value state'
-
- let show_expr valuation state fmt expr =
- match expr.enode with
- | Lval lval ->
- let record = match Valuation.find_loc valuation lval with
- | `Value record -> record
- | `Top -> assert false
- in
- let offsm = Cvalue_offsetmap.offsetmap_of_lval state lval record.loc in
- let typ = Cil.typeOf expr in
- Eval_op.pretty_offsetmap typ fmt offsm
- | _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
-
-
- (* ----------------- Export assumption functions -------------------------- *)
-
- let update valuation state = `Value (update valuation state)
- let assume _stmt _expr _positive = update
-end
+ let offsm = Cvalue_offsetmap.offsetmap_of_lval state lval record.loc in
+ let typ = Cil.typeOf expr in
+ Eval_op.pretty_offsetmap typ fmt offsm
+ | _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
+
+
+(* ----------------- Export assumption functions -------------------------- *)
+
+let update valuation state = `Value (update valuation state)
+let assume _stmt _expr _positive = update
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.mli b/src/plugins/value/domains/cvalue/cvalue_transfer.mli
index a2bff4ae04a..62ce0a5523c 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.mli
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.mli
@@ -23,22 +23,14 @@
(** Transfer functions for the main domain of the Value analysis. *)
type value = Main_values.CVal.t
+type origin = value option
type location = Main_locations.PLoc.location
-module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type origin = value option
- and type loc = location)
- : sig
-
- include Abstract_domain.Transfer
- with type state = Cvalue.Model.t
- and type value := value
- and type location := location
- and type valuation := Valuation.t
-
- end
-
+include Abstract_domain.Transfer
+ with type state := Cvalue.Model.t
+ and type value := value
+ and type location := location
+ and type valuation := (value, location, origin) Abstract_domain.valuation
(*
Local Variables:
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index fa69cac6e2a..ae604a6b2b0 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -75,28 +75,21 @@ module Make_Minimal
let backward_location _state _lval _typ location value = `Value (location, value)
let reduce_further _sttae _expr _value = []
- module Transfer
- (_: Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = location)
- = struct
+ let update _valuation state = `Value state
- let update _valuation state = `Value state
+ let assign kinstr lv expr _value _valuation state =
+ Domain.assign kinstr lv.Eval.lval expr state
- let assign kinstr lv expr _value _valuation state =
- Domain.assign kinstr lv.Eval.lval expr state
+ let assume stmt expr positive _valuation state =
+ Domain.assume stmt expr positive state
- let assume stmt expr positive _valuation state =
- Domain.assume stmt expr positive state
+ let start_call stmt call _valuation state =
+ `Value (Domain.start_call stmt (simplify_call call) state)
- let start_call stmt call _valuation state =
- `Value (Domain.start_call stmt (simplify_call call) state)
+ let finalize_call stmt call ~pre ~post =
+ Domain.finalize_call stmt (simplify_call call) ~pre ~post
- let finalize_call stmt call ~pre ~post =
- Domain.finalize_call stmt (simplify_call call) ~pre ~post
-
- let show_expr _valuation = Domain.show_expr
- end
+ let show_expr _valuation = Domain.show_expr
let enter_loop _stmt state = state
let incr_loop_counter _stmt state = state
@@ -209,37 +202,29 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let reduce_further _state _expr _value = []
- module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = location)
- = struct
-
- let find valuation expr =
- match Valuation.find valuation expr with
- | `Top -> `Top
- | `Value record -> `Value record.value
-
- let find_loc valuation lval =
- match Valuation.find_loc valuation lval with
- | `Top -> `Top
- | `Value record -> `Value record.loc
-
- let record valuation = { find = find valuation;
- find_loc = find_loc valuation; }
-
- let update _valuation state = `Value state
- let assign kinstr lv expr value valuation state =
- Domain.assign kinstr lv expr value (record valuation) state
- let assume stmt expr positive valuation state =
- Domain.assume stmt expr positive (record valuation) state
- let start_call stmt call valuation state =
- `Value (Domain.start_call stmt call (record valuation) state)
- let finalize_call = Domain.finalize_call
-
- let show_expr _valuation = Domain.show_expr
-
- end
+ let find valuation expr =
+ match valuation.Abstract_domain.find expr with
+ | `Top -> `Top
+ | `Value record -> `Value record.value
+
+ let find_loc valuation lval =
+ match valuation.Abstract_domain.find_loc lval with
+ | `Top -> `Top
+ | `Value record -> `Value record.loc
+
+ let record valuation = { find = find valuation;
+ find_loc = find_loc valuation; }
+
+ let update _valuation state = `Value state
+ let assign kinstr lv expr value valuation state =
+ Domain.assign kinstr lv expr value (record valuation) state
+ let assume stmt expr positive valuation state =
+ Domain.assume stmt expr positive (record valuation) state
+ let start_call stmt call valuation state =
+ `Value (Domain.start_call stmt call (record valuation) state)
+ let finalize_call = Domain.finalize_call
+
+ let show_expr _valuation = Domain.show_expr
let enter_loop _stmt state = state
let incr_loop_counter _stmt state = state
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0256e97c80d..4aff7889345 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -51,7 +51,6 @@ module Make
type value = Convert.extended_value
type location = Convert.extended_location
-
type origin = Domain.origin
let extract_expr oracle state exp =
@@ -92,57 +91,37 @@ module Make
in
{ call with arguments; rest }
- module Transfer
- (Valuation:
- Abstract_domain.Valuation with type value = Convert.extended_value
- and type origin = Domain.origin
- and type loc = Convert.extended_location)
- = struct
-
- module Internal_Valuation = struct
- type t = Valuation.t
- type value = Domain.value
- type origin = Domain.origin
- type loc = Domain.location
-
- let lift_record record =
- { record with value = lift_flagged_value record.value }
-
- let find valuation expr = match Valuation.find valuation expr with
- | `Value record -> `Value (lift_record record)
- | `Top -> `Top
-
- let fold f valuation acc =
- Valuation.fold
- (fun exp record acc -> f exp (lift_record record) acc)
- valuation acc
-
- let find_loc valuation loc = match Valuation.find_loc valuation loc with
- | `Value r -> `Value {r with loc = Convert.restrict_loc r.loc}
- | `Top -> `Top
-
- end
-
- module Internal_Transfer = Domain.Transfer (Internal_Valuation)
+ let lift_valuation valuation =
+ let (>>>) v f = match v with
+ | `Value v -> `Value (f v)
+ | `Top -> `Top
+ in
+ let lift_record r = { r with value = lift_flagged_value r.value } in
+ let lift_loc_record r = { r with loc = Convert.restrict_loc r.loc } in
+ let open Abstract_domain in
+ let find expr = valuation.find expr >>> lift_record in
+ let find_loc lval = valuation.find_loc lval >>> lift_loc_record in
+ let fold f acc =
+ valuation.fold (fun exp record acc -> f exp (lift_record record) acc) acc
+ in
+ { find; fold; find_loc; }
- let update = Internal_Transfer.update
+ let update valuation = Domain.update (lift_valuation valuation)
- let assign stmt lv expr value valuation state =
- Internal_Transfer.assign stmt
- (lift_left lv) expr (lift_assigned value) valuation state
+ let assign stmt lv expr value valuation state =
+ Domain.assign stmt
+ (lift_left lv) expr (lift_assigned value) (lift_valuation valuation) state
- let assume = Internal_Transfer.assume
+ let assume stmt expr positive valuation state =
+ Domain.assume stmt expr positive (lift_valuation valuation) state
- let start_call stmt call valuation state =
- let call = lift_call call in
- Internal_Transfer.start_call stmt call valuation state
+ let start_call stmt call valuation state =
+ Domain.start_call stmt (lift_call call) (lift_valuation valuation) state
- let finalize_call stmt call ~pre ~post =
- let call = lift_call call in
- Internal_Transfer.finalize_call stmt call ~pre ~post
+ let finalize_call stmt call ~pre ~post =
+ Domain.finalize_call stmt (lift_call call) ~pre ~post
- let show_expr = Internal_Transfer.show_expr
- end
+ 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
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 1985b6c173a..5f9d14b4397 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -111,115 +111,94 @@ module Make
(Left.reduce_further left expr value)
(Right.reduce_further right expr value)
- module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = location)
- = struct
-
- module type Lift = sig
- type o
- val side : origin -> reductness * o
- end
-
- module Lift_Valuation (Lift: Lift) = struct
- type t = Valuation.t
- type value = Value.t
- type origin = Lift.o
- type loc = Valuation.loc
-
- let lift_record record =
- let origin = Extlib.opt_map Lift.side record.origin in
- let reductness =
- match record.reductness, origin with
- | Unreduced, Some (reduced, _) -> reduced
- | Unreduced, None -> Unreduced (* This case should not happen. *)
- | Reduced, Some (Created, _) -> Created
- | _ as x, _ -> x
- in
- let origin = Extlib.opt_map snd origin in
- { record with origin; reductness }
-
- let find valuation expr = match Valuation.find valuation expr with
- | `Value record -> `Value (lift_record record)
- | `Top -> `Top
-
- let fold f valuation acc =
- Valuation.fold
- (fun exp record acc -> f exp (lift_record record) acc)
- valuation acc
-
- let find_loc = Valuation.find_loc
- end
+ let lift_record side record =
+ let origin = Extlib.opt_map side record.origin in
+ let reductness =
+ match record.reductness, origin with
+ | Unreduced, Some (reduced, _) -> reduced
+ | Unreduced, None -> Unreduced (* This case should not happen. *)
+ | Reduced, Some (Created, _) -> Created
+ | _ as x, _ -> x
+ in
+ let origin = Extlib.opt_map snd origin in
+ { record with origin; reductness }
+
+ let lift_valuation side valuation =
+ let find expr =
+ match valuation.Abstract_domain.find expr with
+ | `Value record -> `Value (lift_record side record)
+ | `Top -> `Top
+ in
+ let fold f acc =
+ valuation.Abstract_domain.fold
+ (fun expr record acc -> f expr (lift_record side record) acc)
+ acc
+ in
+ Abstract_domain.{ find; fold; find_loc = valuation.find_loc }
- module Left_Valuation =
- Lift_Valuation (struct type o = Left.origin let side o = o.left end)
- module Right_Valuation =
- Lift_Valuation (struct type o = Right.origin let side o = o.right end)
+ let left_val = lift_valuation (fun o -> o.left)
+ let right_val = lift_valuation (fun o -> o.right)
- module Left_Transfer = Left.Transfer (Left_Valuation)
- module Right_Transfer = Right.Transfer (Right_Valuation)
- let update valuation (left, right) =
- Left_Transfer.update valuation left >>- fun left ->
- Right_Transfer.update valuation right >>-: fun right ->
- left, right
+ let update valuation (left, right) =
+ Left.update (left_val valuation) left >>- fun left ->
+ Right.update (right_val valuation) right >>-: fun right ->
+ left, right
- let assign stmt lv expr value valuation (left, right) =
- Left_Transfer.assign stmt lv expr value valuation left >>- fun left ->
- Right_Transfer.assign stmt lv expr value valuation right >>-: fun right ->
- left, right
+ let assign stmt lv expr value valuation (left, right) =
+ Left.assign stmt lv expr value (left_val valuation) left >>- fun left ->
+ Right.assign stmt lv expr value (right_val valuation) right >>-: fun right ->
+ left, right
- let assume stmt expr positive valuation (left, right) =
- Left_Transfer.assume stmt expr positive valuation left >>- fun left ->
- Right_Transfer.assume stmt expr positive valuation right >>-: fun right ->
- left, right
+ let assume stmt expr positive valuation (left, right) =
+ Left.assume stmt expr positive (left_val valuation) left >>- fun left ->
+ Right.assume stmt expr positive (right_val valuation) right >>-: fun right ->
+ left, right
- let finalize_call stmt call ~pre ~post =
- let pre_left, pre_right = pre
- and left_state, right_state = post in
- Left_Transfer.finalize_call stmt call ~pre:pre_left ~post:left_state
- >>- fun left ->
- Right_Transfer.finalize_call stmt call ~pre:pre_right ~post:right_state
- >>-: fun right ->
- left, right
+ let finalize_call stmt call ~pre ~post =
+ let pre_left, pre_right = pre
+ and left_state, right_state = post in
+ Left.finalize_call stmt call ~pre:pre_left ~post:left_state
+ >>- fun left ->
+ Right.finalize_call stmt call ~pre:pre_right ~post:right_state
+ >>-: fun right ->
+ left, right
- let start_call stmt call valuation (left, right) =
- Left_Transfer.start_call stmt call valuation left >>- fun left ->
- Right_Transfer.start_call stmt call valuation right >>-: fun right ->
- left, right
+ let start_call stmt call valuation (left, right) =
+ Left.start_call stmt call (left_val valuation) left >>- fun left ->
+ Right.start_call stmt call (right_val valuation) right >>-: fun right ->
+ left, right
- let show_expr =
- let (|-) f g = fun fmt exp -> f fmt exp; g fmt exp in
- let show_expr_one_side category name show_expr = fun fmt exp ->
- if Value_parameters.is_debug_key_enabled category
- then Format.fprintf fmt "@,@]@[<v># %s: @[<hov>%a@]" name show_expr exp
- in
- let right_log = Right.log_category
- and left_log = Left.log_category in
- match left_log = product_category,
- right_log = product_category with
- | true, true ->
- (fun valuation (left, right) ->
- Left_Transfer.show_expr valuation left |-
- Right_Transfer.show_expr valuation right)
- | true, false ->
- (fun valuation (left, right) ->
- Left_Transfer.show_expr valuation left |-
- show_expr_one_side right_log Right.name
- (Right_Transfer.show_expr valuation right))
- | false, true ->
- (fun valuation (left, right) ->
- show_expr_one_side left_log Left.name
- (Left_Transfer.show_expr valuation left) |-
- Right_Transfer.show_expr valuation right)
- | false, false ->
- (fun valuation (left, right) ->
- show_expr_one_side left_log Left.name
- (Left_Transfer.show_expr valuation left) |-
- show_expr_one_side right_log Right.name
- (Right_Transfer.show_expr valuation right))
- end
+ let show_expr =
+ let (|-) f g = fun fmt exp -> f fmt exp; g fmt exp in
+ let show_expr_one_side category name show_expr = fun fmt exp ->
+ if Value_parameters.is_debug_key_enabled category
+ then Format.fprintf fmt "@,@]@[<v># %s: @[<hov>%a@]" name show_expr exp
+ in
+ let right_log = Right.log_category
+ and left_log = Left.log_category in
+ match left_log = product_category,
+ right_log = product_category with
+ | true, true ->
+ (fun valuation (left, right) ->
+ Left.show_expr (left_val valuation) left |-
+ Right.show_expr (right_val valuation) right)
+ | true, false ->
+ (fun valuation (left, right) ->
+ Left.show_expr (left_val valuation) left |-
+ show_expr_one_side right_log Right.name
+ (Right.show_expr (right_val valuation) right))
+ | false, true ->
+ (fun valuation (left, right) ->
+ show_expr_one_side left_log Left.name
+ (Left.show_expr (left_val valuation) left) |-
+ Right.show_expr (right_val valuation) right)
+ | false, false ->
+ (fun valuation (left, right) ->
+ show_expr_one_side left_log Left.name
+ (Left.show_expr (left_val valuation) left) |-
+ show_expr_one_side right_log Right.name
+ (Right.show_expr (right_val valuation) right))
let pretty =
let print_one_side fmt category name dump state =
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 7186aaebe57..9407df3145a 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -281,234 +281,227 @@ module Make
let zone = List.fold_left aux_vi Locations.Zone.bottom vars in
kill Hcexprs.Deleted zone state
- module Transfer
- (Valuation: Abstract_domain.Valuation
- with type value = Value.t
- and type loc = Precise_locs.precise_location)
- = struct
-
- let find_val valuation expr =
- match Valuation.find valuation expr with
- | `Top -> Value.top
- | `Value record -> Bottom.non_bottom record.value.v
-
- let minus_zero = Cvalue.V.inject_float Fval.minus_zero
- let plus_zero = Cvalue.V.inject_float Fval.plus_zero
-
- let incompatible_zeros v1 v2 =
- let aux v1 v2 =
- Cvalue.V.(is_included minus_zero v1 && is_included plus_zero v2)
+ let find_val valuation expr =
+ match valuation.Abstract_domain.find expr with
+ | `Top -> Value.top
+ | `Value record -> Bottom.non_bottom record.value.v
+
+ let minus_zero = Cvalue.V.inject_float Fval.minus_zero
+ let plus_zero = Cvalue.V.inject_float Fval.plus_zero
+
+ let incompatible_zeros v1 v2 =
+ let aux v1 v2 =
+ Cvalue.V.(is_included minus_zero v1 && is_included plus_zero v2)
+ in
+ aux v1 v2 || aux v2 v1
+
+ (* Does the equality between two expressions imply they have the same
+ object representation, allowing the narrow of their abstract values? *)
+ let is_safe_equality =
+ match get_cvalue with
+ | None -> fun _ _ _ -> false
+ | Some get_cvalue ->
+ fun valuation e1 e2 ->
+ let cval1 = get_cvalue (find_val valuation e1)
+ and cval2 = get_cvalue (find_val valuation e2) in
+ Cvalue_forward.are_comparable Abstract_interp.Comp.Eq cval1 cval2
+ && not (incompatible_zeros cval1 cval2)
+
+ exception Top_location
+
+ let find_loc valuation = fun lval ->
+ match valuation.Abstract_domain.find_loc lval with
+ | `Top -> raise Top_location
+ | `Value record -> record.loc
+
+ let add_one_dep valuation lval deps =
+ match HCE.get lval with
+ | E _ -> assert false
+ | LV lv ->
+ let zone =
+ match lv with
+ | Var vi, NoOffset -> Locations.zone_of_varinfo vi
+ | _ ->
+ let expr = Cil.dummy_exp (Lval lv) in
+ Value_util.zone_of_expr (find_loc valuation) expr
in
- aux v1 v2 || aux v2 v1
-
- (* Does the equality between two expressions imply they have the same
- object representation, allowing the narrow of their abstract values? *)
- let is_safe_equality =
- match get_cvalue with
- | None -> fun _ _ _ -> false
- | Some get_cvalue ->
- fun valuation e1 e2 ->
- let cval1 = get_cvalue (find_val valuation e1)
- and cval2 = get_cvalue (find_val valuation e2) in
- Cvalue_forward.are_comparable Abstract_interp.Comp.Eq cval1 cval2
- && not (incompatible_zeros cval1 cval2)
-
- exception Top_location
-
- let find_loc valuation = fun lval ->
- match Valuation.find_loc valuation lval with
- | `Top -> raise Top_location
- | `Value record -> record.loc
-
- let add_one_dep valuation lval deps =
- match HCE.get lval with
- | E _ -> assert false
- | LV lv ->
- let zone =
- match lv with
- | Var vi, NoOffset -> Locations.zone_of_varinfo vi
- | _ ->
- let expr = Cil.dummy_exp (Lval lv) in
- Value_util.zone_of_expr (find_loc valuation) expr
- in
- Deps.add lval zone deps
-
- let add_deps valuation lvalues deps =
- let deps = HCESet.fold (add_one_dep valuation) lvalues.read deps in
- HCESet.fold (add_one_dep valuation) lvalues.addr deps
-
- let update _valuation state = `Value state
-
- let is_singleton = match get_cvalue with
- | None -> fun _ -> false
- | Some get ->
- function
- | `Bottom -> true
- | `Value v -> Cvalue.V.cardinal_zero_or_one (get v)
-
- let expr_cardinal_zero_or_one valuation e =
- match Valuation.find valuation e with
- | `Top -> false (* should not happen *)
- | `Value { value = { v } } -> is_singleton v
-
- let expr_is_cardinal_zero_or_one_loc valuation e =
- match e.enode with
- | Lval lv -> begin
- let loc = Valuation.find_loc valuation lv in
- match loc with
- | `Top -> false (* should not happen *)
- | `Value loc -> Precise_locs.cardinal_zero_or_one loc.loc
- end
- | _ -> false (* TODO: handle upcasts *)
-
-
- let register expr valuation deps =
- let term = HCE.of_exp expr in
- if HCE.is_lval term
- then
- let deps = add_one_dep valuation term deps in
- term, Hcexprs.empty_lvalues, deps
- else
- let lvalues = Hcexprs.syntactic_lvalues expr in
- term, lvalues, add_deps valuation lvalues deps
-
- let indeterminate_copy = function
- | Assign _ -> false
- | Copy (_loc, value) -> not value.initialized || value.escaping
-
- (* Auxiliary function for [assign]. The equality is inferred, unless:
- - some of the expressions involved are volatile
- - the value has an aggregate type (as the current Eva values have no
- meaning for such type, the equality would be useless or misleading).
- - it is an assignment by copy, and the copied value is possibly
- unitialized or escaping. In this case, when using the equality later,
- the reevaluation of [right_expr] would reduce it incorrectly, by
- removing indeterminate flags without emitting alarms. *)
- let assign_eq left_lval right_expr value valuation state =
- if Eval_typ.lval_contains_volatile left_lval ||
- Eval_typ.expr_contains_volatile right_expr ||
- not (Cil.isArithmeticOrPointerType (Cil.typeOfLval left_lval)) ||
- indeterminate_copy value
- then state
+ Deps.add lval zone deps
+
+ let add_deps valuation lvalues deps =
+ let deps = HCESet.fold (add_one_dep valuation) lvalues.read deps in
+ HCESet.fold (add_one_dep valuation) lvalues.addr deps
+
+ let update _valuation state = `Value state
+
+ let is_singleton = match get_cvalue with
+ | None -> fun _ -> false
+ | Some get ->
+ function
+ | `Bottom -> true
+ | `Value v -> Cvalue.V.cardinal_zero_or_one (get v)
+
+ let expr_cardinal_zero_or_one valuation e =
+ match valuation.Abstract_domain.find e with
+ | `Top -> false (* should not happen *)
+ | `Value { value = { v } } -> is_singleton v
+
+ let expr_is_cardinal_zero_or_one_loc valuation e =
+ match e.enode with
+ | Lval lv -> begin
+ let loc = valuation.Abstract_domain.find_loc lv in
+ match loc with
+ | `Top -> false (* should not happen *)
+ | `Value loc -> Precise_locs.cardinal_zero_or_one loc.loc
+ end
+ | _ -> false (* TODO: handle upcasts *)
+
+
+ let register expr valuation deps =
+ let term = HCE.of_exp expr in
+ if HCE.is_lval term
+ then
+ let deps = add_one_dep valuation term deps in
+ term, Hcexprs.empty_lvalues, deps
+ else
+ let lvalues = Hcexprs.syntactic_lvalues expr in
+ term, lvalues, add_deps valuation lvalues deps
+
+ let indeterminate_copy = function
+ | Assign _ -> false
+ | Copy (_loc, value) -> not value.initialized || value.escaping
+
+ (* Auxiliary function for [assign]. The equality is inferred, unless:
+ - some of the expressions involved are volatile
+ - the value has an aggregate type (as the current Eva values have no
+ meaning for such type, the equality would be useless or misleading).
+ - it is an assignment by copy, and the copied value is possibly
+ unitialized or escaping. In this case, when using the equality later,
+ the reevaluation of [right_expr] would reduce it incorrectly, by
+ removing indeterminate flags without emitting alarms. *)
+ let assign_eq left_lval right_expr value valuation state =
+ if Eval_typ.lval_contains_volatile left_lval ||
+ Eval_typ.expr_contains_volatile right_expr ||
+ not (Cil.isArithmeticOrPointerType (Cil.typeOfLval left_lval)) ||
+ indeterminate_copy value
+ then state
+ else
+ let (equalities, deps, modified_zone: t) = state in
+ let lterm = HCE.of_lval left_lval in
+ let lterm_lvals = Hcexprs.empty_lvalues in
+ let deps = add_one_dep valuation lterm deps in
+ let rterm, rterm_lvals, deps = register right_expr valuation deps in
+ let equalities =
+ Equality.Set.unite
+ (lterm, lterm_lvals) (rterm, rterm_lvals) equalities
+ in
+ (equalities, deps, modified_zone: t)
+
+ let assign _stmt left_value right_expr value valuation state =
+ let open Locations in
+ let left_loc = Precise_locs.imprecise_location left_value.lloc in
+ let direct_left_zone = Locations.(enumerate_valid_bits Write left_loc) in
+ let state = kill Hcexprs.Modified direct_left_zone state in
+ let right_expr = Cil.constFold true right_expr in
+ try
+ let indirect_left_zone =
+ Value_util.indirect_zone_of_lval (find_loc valuation) left_value.lval
+ and right_zone =
+ Value_util.zone_of_expr (find_loc valuation) right_expr
+ in
+ (* After an assignment lv = e, the equality [lv == eq] holds iff the value
+ of [e] and the location of [lv] are not modified by the assignment,
+ i.e. iff the dependencies of [e] and of the lhost and offset of [lv]
+ do not intersect the assigned location.
+ Moreover, the domain do not store the equality when the abstract
+ location of [lv] and the abstract value of [e] are singleton, as in
+ this case, the main cvalue domain is able to infer the equality. *)
+ if (Zone.intersects direct_left_zone right_zone) ||
+ (Zone.intersects direct_left_zone indirect_left_zone) ||
+ (is_singleton (Eval.value_assigned value) &&
+ Locations.cardinal_zero_or_one left_loc)
+ then `Value state
+ else `Value (assign_eq left_value.lval right_expr value valuation state)
+ with Top_location -> `Value state
+
+ (* Add the equalities between the formals of a function and the actuals
+ at the call. *)
+ let assign_formals valuation call state =
+ let assign_formal state arg =
+ if is_singleton (Eval.value_assigned arg.avalue) then
+ state
else
- let (equalities, deps, modified_zone: t) = state in
- let lterm = HCE.of_lval left_lval in
- let lterm_lvals = Hcexprs.empty_lvalues in
- let deps = add_one_dep valuation lterm deps in
- let rterm, rterm_lvals, deps = register right_expr valuation deps in
- let equalities =
- Equality.Set.unite
- (lterm, lterm_lvals) (rterm, rterm_lvals) equalities
- in
- (equalities, deps, modified_zone: t)
-
- let assign _stmt left_value right_expr value valuation state =
- let open Locations in
- let left_loc = Precise_locs.imprecise_location left_value.lloc in
- let direct_left_zone = Locations.(enumerate_valid_bits Write left_loc) in
- let state = kill Hcexprs.Modified direct_left_zone state in
- let right_expr = Cil.constFold true right_expr in
- try
- let indirect_left_zone =
- Value_util.indirect_zone_of_lval (find_loc valuation) left_value.lval
- and right_zone =
- Value_util.zone_of_expr (find_loc valuation) right_expr
- in
- (* After an assignment lv = e, the equality [lv == eq] holds iff the value
- of [e] and the location of [lv] are not modified by the assignment,
- i.e. iff the dependencies of [e] and of the lhost and offset of [lv]
- do not intersect the assigned location.
- Moreover, the domain do not store the equality when the abstract
- location of [lv] and the abstract value of [e] are singleton, as in
- this case, the main cvalue domain is able to infer the equality. *)
- if (Zone.intersects direct_left_zone right_zone) ||
- (Zone.intersects direct_left_zone indirect_left_zone) ||
- (is_singleton (Eval.value_assigned value) &&
- Locations.cardinal_zero_or_one left_loc)
+ try
+ let left_value = Var arg.formal, NoOffset in
+ assign_eq left_value arg.concrete arg.avalue valuation state
+ with Top_location -> state
+ in
+ List.fold_left assign_formal state call.arguments
+
+ (* The domain infers equalities [e1 = e2] stemming from assignments,
+ meaning that e1 and e2 have not only the same value, but also the same
+ object representation — their values can thus be safely narrowed,
+ which is used by the domain to regain precision when possible.
+ The domain can also infer equalities from conditions, but C values
+ with different object representations may be equal, invalidating this
+ reasoning. This is the case for equalities between 0. and -0., and
+ between non-comparable pointers, so we need to skip such equalities. *)
+ let assume _stmt expr positive valuation (eqs, deps, modified_zone as state) =
+ match positive, expr.enode with
+ | true, BinOp (Eq, e1, e2, _)
+ | false, BinOp (Ne, e1, e2, _) ->
+ begin
+ if not (is_safe_equality valuation e1 e2)
then `Value state
- else `Value (assign_eq left_value.lval right_expr value valuation state)
- with Top_location -> `Value state
-
- (* Add the equalities between the formals of a function and the actuals
- at the call. *)
- let assign_formals valuation call state =
- let assign_formal state arg =
- if is_singleton (Eval.value_assigned arg.avalue) then
- state
else
- try
- let left_value = Var arg.formal, NoOffset in
- assign_eq left_value arg.concrete arg.avalue valuation state
- with Top_location -> state
- in
- List.fold_left assign_formal state call.arguments
-
- (* The domain infers equalities [e1 = e2] stemming from assignments,
- meaning that e1 and e2 have not only the same value, but also the same
- object representation — their values can thus be safely narrowed,
- which is used by the domain to regain precision when possible.
- The domain can also infer equalities from conditions, but C values
- with different object representations may be equal, invalidating this
- reasoning. This is the case for equalities between 0. and -0., and
- between non-comparable pointers, so we need to skip such equalities. *)
- let assume _stmt expr positive valuation (eqs, deps, modified_zone as state) =
- match positive, expr.enode with
- | true, BinOp (Eq, e1, e2, _)
- | false, BinOp (Ne, e1, e2, _) ->
- begin
- if not (is_safe_equality valuation e1 e2)
+ let e1 = Cil.constFold true e1
+ and e2 = Cil.constFold true e2 in
+ if Eval_typ.expr_contains_volatile e1
+ || Eval_typ.expr_contains_volatile e2
+ || not (Cil.isArithmeticOrPointerType (Cil.typeOf e1))
+ || (expr_is_cardinal_zero_or_one_loc valuation e1 &&
+ expr_cardinal_zero_or_one valuation e2)
+ || (expr_is_cardinal_zero_or_one_loc valuation e2 &&
+ expr_cardinal_zero_or_one valuation e1)
then `Value state
else
- let e1 = Cil.constFold true e1
- and e2 = Cil.constFold true e2 in
- if Eval_typ.expr_contains_volatile e1
- || Eval_typ.expr_contains_volatile e2
- || not (Cil.isArithmeticOrPointerType (Cil.typeOf e1))
- || (expr_is_cardinal_zero_or_one_loc valuation e1 &&
- expr_cardinal_zero_or_one valuation e2)
- || (expr_is_cardinal_zero_or_one_loc valuation e2 &&
- expr_cardinal_zero_or_one valuation e1)
- then `Value state
- else
- try
- let a1, a1_lvals, deps = register e1 valuation deps in
- let a2, a2_lvals, deps = register e2 valuation deps in
- let eqs = Equality.Set.unite (a1, a1_lvals) (a2, a2_lvals) eqs in
- `Value (eqs, deps, modified_zone)
- with Top_location -> `Value state
- end
- | _ -> `Value state
-
- let start_call _stmt call valuation state =
- let state =
- match call_init_state call.kf with
- | ISCaller -> assign_formals valuation call state
- | ISFormals -> assign_formals valuation call empty
- | ISEmpty -> empty
- in
- `Value state
+ try
+ let a1, a1_lvals, deps = register e1 valuation deps in
+ let a2, a2_lvals, deps = register e2 valuation deps in
+ let eqs = Equality.Set.unite (a1, a1_lvals) (a2, a2_lvals) eqs in
+ `Value (eqs, deps, modified_zone)
+ with Top_location -> `Value state
+ end
+ | _ -> `Value state
+
+ let start_call _stmt call valuation state =
+ let state =
+ match call_init_state call.kf with
+ | ISCaller -> assign_formals valuation call state
+ | ISFormals -> assign_formals valuation call empty
+ | ISEmpty -> empty
+ in
+ `Value state
- let finalize_call _stmt call ~pre ~post =
- if call_init_state call.kf = ISCaller then
- `Value post (* [pre] was the state inferred in the caller, and it
- has been updated during the analysis of [kf] into
- [post]. Send all the equalities back to the caller. *)
- else
- (* [pre] contains the equalities from the caller, but [post] was
- computed starting from an essentially empty state. We must
- restore the equalities of [pre]. *)
- let (_, _, modif) = post in
- (* Invalidate the equalities that are no longer true. *)
- let pre' = kill Hcexprs.Modified modif pre in
- (* then merge the two sets of equalities *)
- `Value (concat pre' post)
-
- let show_expr _valuation (equalities, _, _) fmt expr =
- let atom = Hcexprs.HCE.of_exp expr in
- match Equality.Set.find_option atom equalities with
- | Some equality -> Equality.Equality.pretty fmt equality
- | None -> ()
- end
+ let finalize_call _stmt call ~pre ~post =
+ if call_init_state call.kf = ISCaller then
+ `Value post (* [pre] was the state inferred in the caller, and it
+ has been updated during the analysis of [kf] into
+ [post]. Send all the equalities back to the caller. *)
+ else
+ (* [pre] contains the equalities from the caller, but [post] was
+ computed starting from an essentially empty state. We must
+ restore the equalities of [pre]. *)
+ let (_, _, modif) = post in
+ (* Invalidate the equalities that are no longer true. *)
+ let pre' = kill Hcexprs.Modified modif pre in
+ (* then merge the two sets of equalities *)
+ `Value (concat pre' post)
+
+ let show_expr _valuation (equalities, _, _) fmt expr =
+ let atom = Hcexprs.HCE.of_exp expr in
+ match Equality.Set.find_option atom equalities with
+ | Some equality -> Equality.Equality.pretty fmt equality
+ | None -> ()
let logic_assign _assigns location ~pre:_ state =
let loc = Precise_locs.imprecise_location location in
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 62ce07b51b9..5c892c9e225 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1130,6 +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
include G
@@ -1151,8 +1152,6 @@ module D_Impl : Abstract_domain.S
(* reverts implicitly to Top *)
remove_variables vars state
- type origin = unit
-
let kill loc state =
let loc = Precise_locs.imprecise_location loc in
let loc = loc.Locations.loc in
@@ -1163,108 +1162,96 @@ module D_Impl : Abstract_domain.S
let vars = Locations.Location_Bits.fold_topset_ok aux_base loc [] in
remove_variables vars state
- module Transfer (Valuation:
- Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = location)
- : Abstract_domain.Transfer
- with type state := state
- and type value := value
- and type location := location
- and type valuation := Valuation.t
- = struct
-
- let assume_exp valuation e r state =
- if r.reductness = Created || r.reductness = Reduced then
- match e.enode with
- | Lval lv -> begin
- match Valuation.find_loc valuation lv with
- | `Top -> `Value state
- | `Value {loc} ->
- let loc = Precise_locs.imprecise_location loc in
- try
- let b = loc_to_base loc (Cil.typeOfLval lv) in
- match r.value.v with
- | `Bottom -> `Value state
- | `Value v ->
- match backward_loop state b v with
- | Some `Bottom -> `Bottom
- | Some (`Value _ as s) -> s
- | None -> `Value state
- with Untranslatable -> `Value state
- end
- | _ -> `Value state
- else `Value state
-
- let assume_exp_bot valuation e r state =
- state >>- assume_exp valuation e r
-
- let update valuation state =
- let assume_one = assume_exp_bot valuation in
- Valuation.fold assume_one valuation (`Value state)
-
- let assume _ _ _ = update
-
- exception Unassignable
-
- let assign _kinstr lv e _assignment valuation (state:state) =
- update valuation state >>- fun state ->
- let to_loc lv =
- match Valuation.find_loc valuation lv with
- | `Value r -> Precise_locs.imprecise_location r.loc
- | `Top -> raise Unassignable
- in
- let to_val e =
- match Valuation.find valuation e with
- | `Top -> raise Unassignable
- | `Value v ->
- match v.value.initialized, v.value.escaping, v.value.v with
- | true, false, `Value v -> v
- | _ -> raise Unassignable
- in
- try `Value (G.assign to_loc to_val lv.lval e state)
- with Unassignable -> `Value (kill lv.lloc state)
-
- let finalize_call _stmt _call ~pre ~post =
- let state =
- match function_calls_handling with
- | FullInterprocedural -> post
- | IntraproceduralNonReferenced -> pre
- | IntraproceduralAll -> pre (* unsound here *)
- in
- `Value state
-
- let start_call _stmt call valuation state =
- let state =
- match function_calls_handling with
- | FullInterprocedural -> update valuation state
- | IntraproceduralAll
- | IntraproceduralNonReferenced -> `Value G.empty
- in
- state >>- fun state ->
- (* track [arg.formal] into [state]. Important for functions that
- receive a size as argument. *)
- let aux_arg state arg =
- try
- let vi = arg.formal in
- if not (tracked_variable vi) then raise Untranslatable;
- let b = Base.of_varinfo vi in
- let v = match arg.avalue with
- | Assign v -> v
- | Copy (_, v) ->
- match v.initialized, v.escaping, v.v with
- | true, false, `Value v -> v
- | _ -> raise Untranslatable
- in
- let g = Gauge.ct v in
- store_gauge b g state
- with Untranslatable -> state
- in
- let state = List.fold_left aux_arg state call.arguments in
- `Value state
+ let assume_exp valuation e r state =
+ if r.reductness = Created || r.reductness = Reduced then
+ match e.enode with
+ | Lval lv -> begin
+ match valuation.Abstract_domain.find_loc lv with
+ | `Top -> `Value state
+ | `Value {loc} ->
+ let loc = Precise_locs.imprecise_location loc in
+ try
+ let b = loc_to_base loc (Cil.typeOfLval lv) in
+ match r.value.v with
+ | `Bottom -> `Value state
+ | `Value v ->
+ match backward_loop state b v with
+ | Some `Bottom -> `Bottom
+ | Some (`Value _ as s) -> s
+ | None -> `Value state
+ with Untranslatable -> `Value state
+ end
+ | _ -> `Value state
+ else `Value state
+
+ let assume_exp_bot valuation e r state =
+ state >>- assume_exp valuation e r
+
+ let update valuation state =
+ let assume_one = assume_exp_bot valuation in
+ valuation.Abstract_domain.fold assume_one (`Value state)
+
+ let assume _ _ _ = update
+
+ exception Unassignable
+
+ let assign _kinstr lv e _assignment valuation (state:state) =
+ update valuation state >>- fun state ->
+ let to_loc lv =
+ match valuation.Abstract_domain.find_loc lv with
+ | `Value r -> Precise_locs.imprecise_location r.loc
+ | `Top -> raise Unassignable
+ in
+ let to_val e =
+ match valuation.Abstract_domain.find e with
+ | `Top -> raise Unassignable
+ | `Value v ->
+ match v.value.initialized, v.value.escaping, v.value.v with
+ | true, false, `Value v -> v
+ | _ -> raise Unassignable
+ in
+ try `Value (G.assign to_loc to_val lv.lval e state)
+ with Unassignable -> `Value (kill lv.lloc state)
+
+ let finalize_call _stmt _call ~pre ~post =
+ let state =
+ match function_calls_handling with
+ | FullInterprocedural -> post
+ | IntraproceduralNonReferenced -> pre
+ | IntraproceduralAll -> pre (* unsound here *)
+ in
+ `Value state
+
+ let start_call _stmt call valuation state =
+ let state =
+ match function_calls_handling with
+ | FullInterprocedural -> update valuation state
+ | IntraproceduralAll
+ | IntraproceduralNonReferenced -> `Value G.empty
+ in
+ state >>- fun state ->
+ (* track [arg.formal] into [state]. Important for functions that
+ receive a size as argument. *)
+ let aux_arg state arg =
+ try
+ let vi = arg.formal in
+ if not (tracked_variable vi) then raise Untranslatable;
+ let b = Base.of_varinfo vi in
+ let v = match arg.avalue with
+ | Assign v -> v
+ | Copy (_, v) ->
+ match v.initialized, v.escaping, v.v with
+ | true, false, `Value v -> v
+ | _ -> raise Untranslatable
+ in
+ let g = Gauge.ct v in
+ store_gauge b g state
+ with Untranslatable -> state
+ in
+ let state = List.fold_left aux_arg state call.arguments in
+ `Value state
- let show_expr _valuation _state _fmt _expr = ()
- end
+ let show_expr _valuation _state _fmt _expr = ()
let enter_loop = G.enter_loop
let incr_loop_counter _ = G.inc
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 1a5a4888c93..b34535306a3 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -213,6 +213,7 @@ module Internal
type state = inout
type value = Cvalue.V.t
type location = Precise_locs.precise_location
+ type origin = unit
include (LatticeInout: sig
include Datatype.S_with_collections with type t = state
@@ -225,47 +226,29 @@ module Internal
let enter_scope _kf _vars state = state
let leave_scope _kf vars state = Transfer.remove_variables vars state
- type origin = unit
+ let to_z valuation lv =
+ match valuation.Abstract_domain.find_loc lv with
+ | `Value loc -> loc.Eval.loc
+ | `Top -> Precise_locs.loc_top (* should not occur *)
+
+ let assign _ki lv e _v valuation state =
+ let to_z = to_z valuation in
+ let effects = Transfer.effects_assign to_z lv e in
+ `Value (Transfer.catenate state effects)
+
+ let assume _stmt e _pos valuation state =
+ let to_z = to_z valuation in
+ let effects = Transfer.effects_assume to_z e in
+ `Value (Transfer.catenate state effects)
+
+ let start_call _stmt _call _valuation _state = `Value LatticeInout.empty
+
+ let finalize_call _stmt _call ~pre ~post =
+ `Value (Transfer.catenate pre post)
+
+ let update _valuation state = `Value state
- module Transfer (Valuation: Abstract_domain.Valuation
- with type value = value
- and type origin = origin
- and type loc = Precise_locs.precise_location)
- : Abstract_domain.Transfer
- with type state = state
- and type value = Cvalue.V.t
- and type location = Precise_locs.precise_location
- and type valuation = Valuation.t
- = struct
- type value = Cvalue.V.t
- type state = inout
- type location = Precise_locs.precise_location
- type valuation = Valuation.t
-
- let to_z valuation lv =
- match Valuation.find_loc valuation lv with
- | `Value loc -> loc.Eval.loc
- | `Top -> Precise_locs.loc_top (* should not occur *)
-
- let assign _ki lv e _v valuation state =
- let to_z = to_z valuation in
- let effects = Transfer.effects_assign to_z lv e in
- `Value (Transfer.catenate state effects)
-
- let assume _stmt e _pos valuation state =
- let to_z = to_z valuation in
- let effects = Transfer.effects_assume to_z e in
- `Value (Transfer.catenate state effects)
-
- let start_call _stmt _call _valuation _state = `Value LatticeInout.empty
-
- let finalize_call _stmt _call ~pre ~post =
- `Value (Transfer.catenate pre post)
-
- let update _valuation state = `Value state
-
- let show_expr _valuation _state _fmt _expr = ()
- end
+ let show_expr _valuation _state _fmt _expr = ()
(* Memexec *)
let relate _kf _bases _state = Base.SetLattice.empty
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index c5a14838419..fae7d982ebc 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1037,8 +1037,8 @@ module Domain = struct
type value = Cvalue.V.t
type location = Precise_locs.precise_location
-
type origin = unit
+
let top_value = `Value (Cvalue.V.top, ()), Alarmset.all
let extract_expr oracle state expr =
@@ -1108,138 +1108,132 @@ module Domain = struct
let state = Zone.fold_bases kill_base zone state in
{ state with modified }
- module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type loc = location)
- = struct
-
- (* Evaluation function of expressions to ival, from a [valuation]. *)
- let evaluation_function valuation = fun expr ->
- match Valuation.find valuation expr with
- | `Top -> `Top
- | `Value record ->
- match record.Eval.value.v with
- | `Bottom -> `Top (* TODO: why this keeps happening? *)
- | `Value cvalue ->
- try `Value (Cvalue.V.project_ival cvalue)
- with Cvalue.V.Not_based_on_null -> `Top
-
- exception EBottom
-
- let infer_octagons evaluate expr ival state =
- let octagons = Rewriting.make_octagons evaluate expr ival in
- let add_octagon state octagon =
- match State.add_octagon state octagon with
- | `Bottom -> raise EBottom
- | `Value state -> state
- in
- List.fold_left add_octagon state octagons
+ (* Evaluation function of expressions to ival, from a [valuation]. *)
+ let evaluation_function valuation = fun expr ->
+ match valuation.Abstract_domain.find expr with
+ | `Top -> `Top
+ | `Value record ->
+ match record.Eval.value.v with
+ | `Bottom -> `Top (* TODO: why this keeps happening? *)
+ | `Value cvalue ->
+ try `Value (Cvalue.V.project_ival cvalue)
+ with Cvalue.V.Not_based_on_null -> `Top
- let infer_interval expr ival state =
- if not infer_intervals
- then state
- else
- match expr.enode with
- | Lval (Var varinfo, NoOffset)
- when Cil.isIntegralType varinfo.vtype ->
- let intervals = Intervals.add varinfo ival state.intervals in
- { state with intervals }
- | _ -> state
-
- let update valuation state =
- let evaluate = evaluation_function valuation in
- let aux expr record state =
- let value = record.Eval.value in
- match record.reductness, value.v, value.initialized, value.escaping with
- | (Created | Reduced), `Value cvalue, true, false ->
- begin
- try
- let ival = Cvalue.V.project_ival cvalue in
- let state = infer_octagons evaluate expr ival state in
- infer_interval expr ival state
- with Cvalue.V.Not_based_on_null -> state
- end
- | _ -> state
- in
- try `Value (check "update" (Valuation.fold aux valuation state))
- with EBottom -> `Bottom
+ exception EBottom
- let assign_interval varinfo assigned state =
- if not infer_intervals
- then state
- else
- match assigned with
- | Assign v
- | Copy (_, { v = `Value v; initialized = true; escaping = false }) ->
- begin
- try
- let ival = Cvalue.V.project_ival v in
- let intervals = Intervals.add varinfo ival state.intervals in
- { state with intervals }
- with Cvalue.V.Not_based_on_null -> state
- end
- | _ -> state
-
- let assign_variable varinfo expr assigned valuation state =
- let evaluate = evaluation_function valuation in
- (* TODO: redundant with rewrite_binop below. *)
- let vars = Rewriting.rewrite evaluate expr in
- let equal_varinfo v = Variable.equal varinfo v.Rewriting.varinfo in
- let state =
- try
- let var = List.find equal_varinfo vars in
- let inverse = not var.Rewriting.sign in
- State.sub_delta ~inverse state varinfo var.Rewriting.coeff
- with Not_found -> State.remove state varinfo
- in
- let state = assign_interval varinfo assigned state in
- let enode = Lval (Var varinfo, NoOffset) in
- let left_expr = Cil.new_exp ~loc:expr.eloc enode in
- (* On the assignment X = E; if X-E can be rewritten as ±(X±Y-v),
- then the octagonal constraint [X±Y ∈ v] holds. *)
- let octagons = Rewriting.rewrite_binop evaluate left_expr Sub expr in
- let state =
- List.fold_left
- (fun acc (_sign, octagon) ->
- acc >>- fun state -> State.add_octagon state octagon)
- (`Value state) octagons
+ let infer_octagons evaluate expr ival state =
+ let octagons = Rewriting.make_octagons evaluate expr ival in
+ let add_octagon state octagon =
+ match State.add_octagon state octagon with
+ | `Bottom -> raise EBottom
+ | `Value state -> state
+ in
+ List.fold_left add_octagon state octagons
+
+ let infer_interval expr ival state =
+ if not infer_intervals
+ then state
+ else
+ match expr.enode with
+ | Lval (Var varinfo, NoOffset)
+ when Cil.isIntegralType varinfo.vtype ->
+ let intervals = Intervals.add varinfo ival state.intervals in
+ { state with intervals }
+ | _ -> state
+
+ let update valuation state =
+ let evaluate = evaluation_function valuation in
+ let aux expr record state =
+ let value = record.Eval.value in
+ match record.reductness, value.v, value.initialized, value.escaping with
+ | (Created | Reduced), `Value cvalue, true, false ->
+ begin
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ let state = infer_octagons evaluate expr ival state in
+ infer_interval expr ival state
+ with Cvalue.V.Not_based_on_null -> state
+ end
+ | _ -> state
+ in
+ try `Value (check "update" (valuation.Abstract_domain.fold aux state))
+ with EBottom -> `Bottom
+
+ let assign_interval varinfo assigned state =
+ if not infer_intervals
+ then state
+ else
+ match assigned with
+ | Assign v
+ | Copy (_, { v = `Value v; initialized = true; escaping = false }) ->
+ begin
+ try
+ let ival = Cvalue.V.project_ival v in
+ let intervals = Intervals.add varinfo ival state.intervals in
+ { state with intervals }
+ with Cvalue.V.Not_based_on_null -> state
+ end
+ | _ -> state
+
+ let assign_variable varinfo expr assigned valuation state =
+ let evaluate = evaluation_function valuation in
+ (* TODO: redundant with rewrite_binop below. *)
+ let vars = Rewriting.rewrite evaluate expr in
+ let equal_varinfo v = Variable.equal varinfo v.Rewriting.varinfo in
+ let state =
+ try
+ let var = List.find equal_varinfo vars in
+ let inverse = not var.Rewriting.sign in
+ State.sub_delta ~inverse state varinfo var.Rewriting.coeff
+ with Not_found -> State.remove state varinfo
+ in
+ let state = assign_interval varinfo assigned state in
+ let enode = Lval (Var varinfo, NoOffset) in
+ let left_expr = Cil.new_exp ~loc:expr.eloc enode in
+ (* On the assignment X = E; if X-E can be rewritten as ±(X±Y-v),
+ then the octagonal constraint [X±Y ∈ v] holds. *)
+ let octagons = Rewriting.rewrite_binop evaluate left_expr Sub expr in
+ let state =
+ List.fold_left
+ (fun acc (_sign, octagon) ->
+ acc >>- fun state -> State.add_octagon state octagon)
+ (`Value state) octagons
+ in
+ state >>-: check "precise assign"
+
+ let assign _kinstr left_value expr assigned valuation state =
+ update valuation state >>- fun state ->
+ match left_value.lval with
+ | Var varinfo, NoOffset when Cil.isIntegralType varinfo.vtype ->
+ assign_variable varinfo expr assigned valuation state
+ | _ ->
+ let written_loc = Precise_locs.imprecise_location left_value.lloc in
+ let written_zone =
+ Locations.(enumerate_valid_bits Write written_loc)
in
- state >>-: check "precise assign"
-
- let assign _kinstr left_value expr assigned valuation state =
- update valuation state >>- fun state ->
- match left_value.lval with
- | Var varinfo, NoOffset when Cil.isIntegralType varinfo.vtype ->
- assign_variable varinfo expr assigned valuation state
- | _ ->
- let written_loc = Precise_locs.imprecise_location left_value.lloc in
- let written_zone =
- Locations.(enumerate_valid_bits Write written_loc)
- in
- let state = kill written_zone state in
- `Value (check "imprecise assign" state)
+ let state = kill written_zone state in
+ `Value (check "imprecise assign" state)
- let assume _stmt _exp _bool = update
+ let assume _stmt _exp _bool = update
- let start_call _stmt call valuation state =
- if intraprocedural ()
- then `Value (empty ())
- else
- let state = { state with modified = Locations.Zone.bottom } in
- let assign_formal state { formal; concrete; avalue } =
- state >>- assign_variable formal concrete avalue valuation
- in
- List.fold_left assign_formal (`Value state) call.arguments
+ let start_call _stmt call valuation state =
+ if intraprocedural ()
+ then `Value (empty ())
+ else
+ let state = { state with modified = Locations.Zone.bottom } in
+ let assign_formal state { formal; concrete; avalue } =
+ state >>- assign_variable formal concrete avalue valuation
+ in
+ List.fold_left assign_formal (`Value state) call.arguments
- let finalize_call _stmt _call ~pre ~post =
- if intraprocedural ()
- then `Value (kill post.modified pre)
- else
- let modified = Locations.Zone.join post.modified pre.modified in
- `Value { post with modified }
+ let finalize_call _stmt _call ~pre ~post =
+ if intraprocedural ()
+ then `Value (kill post.modified pre)
+ else
+ let modified = Locations.Zone.join post.modified pre.modified in
+ `Value { post with modified }
- let show_expr _valuation _state _fmt _expr = ()
- end
+ let show_expr _valuation _state _fmt _expr = ()
let logic_assign _logic_assign location ~pre:_ state =
let loc = Precise_locs.imprecise_location location in
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index f491384582b..2809ade3ffa 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -97,6 +97,8 @@ module Internal : Domain_builder.InputDomain
type value = offsm_or_top
type state = Memory.t
type location = Precise_locs.precise_location
+ type origin = unit (* ???? *)
+
include (Memory: sig
include Datatype.S_with_collections with type t = state
include Abstract_domain.Lattice with type state := state
@@ -115,65 +117,51 @@ module Internal : Domain_builder.InputDomain
let incr_loop_counter _ state = state
let leave_loop _ state = state
- type origin = unit (* ???? *)
-
let kill loc state =
Memory.add_binding ~exact:true state loc V_Or_Uninitialized.top
- module Transfer (Valuation:
- Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = Precise_locs.precise_location)
- : Abstract_domain.Transfer
- with type state := state
- and type value := offsm_or_top
- and type location := Precise_locs.precise_location
- and type valuation := Valuation.t
- = struct
-
- let update _valuation st = `Value st (* TODO? *)
-
- let store loc state v =
- let state' =
- match v with
- | Top -> kill loc state
- | O o ->
- if not store_redundant && V_Offsetmap.is_single_interval o then
- kill loc state
- else
- match loc.Locations.size with
- | Int_Base.Top -> assert false
- | Int_Base.Value size ->
- Memory.paste_offsetmap
- ~from:o ~dst_loc:loc.Locations.loc ~size ~exact:true state
- in
- match state' with
- | Memory.Bottom -> `Bottom
- | _ -> `Value state'
-
- let generic_assign lv value state =
- let loc = Precise_locs.imprecise_location lv.lloc in
- let v = Eval.value_assigned value in
- let v = match v with
- | `Value v -> v
- (* Copy of fully indeterminate bits. We could store an uninitialized
- bottom, or something like that. Since this would be redundant
- with the legacy domain, we just drop the value. *)
- | `Bottom -> Top
- in
- store loc state v
-
- let assign _kinstr lv _e assignment _valuation state =
- generic_assign lv assignment state
-
- let assume _ _ _ _ state = `Value state
-
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
-
- let start_call _stmt _call valuation state = update valuation state
-
- let show_expr _valuation _state _fmt _expr = ()
- end
+ let update _valuation st = `Value st (* TODO? *)
+
+ let store loc state v =
+ let state' =
+ match v with
+ | Top -> kill loc state
+ | O o ->
+ if not store_redundant && V_Offsetmap.is_single_interval o then
+ kill loc state
+ else
+ match loc.Locations.size with
+ | Int_Base.Top -> assert false
+ | Int_Base.Value size ->
+ Memory.paste_offsetmap
+ ~from:o ~dst_loc:loc.Locations.loc ~size ~exact:true state
+ in
+ match state' with
+ | Memory.Bottom -> `Bottom
+ | _ -> `Value state'
+
+ let generic_assign lv value state =
+ let loc = Precise_locs.imprecise_location lv.lloc in
+ let v = Eval.value_assigned value in
+ let v = match v with
+ | `Value v -> v
+ (* Copy of fully indeterminate bits. We could store an uninitialized
+ bottom, or something like that. Since this would be redundant
+ with the legacy domain, we just drop the value. *)
+ | `Bottom -> Top
+ in
+ store loc state v
+
+ let assign _kinstr lv _e assignment _valuation state =
+ generic_assign lv assignment state
+
+ let assume _ _ _ _ state = `Value state
+
+ let finalize_call _stmt _call ~pre:_ ~post = `Value post
+
+ let start_call _stmt _call valuation state = update valuation state
+
+ let show_expr _valuation _state _fmt _expr = ()
let extract_expr _oracle _state _exp =
`Value (Offsm_value.Offsm.top, ()), Alarmset.all
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index ea175768582..97eed460437 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -187,6 +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
let log_category = Value_parameters.register_category ("d-" ^ Info.name)
@@ -207,99 +208,90 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let reduce_further _state _expr _value = []
- type origin = unit
-
- module Transfer
- (Valuation: Abstract_domain.Valuation with type value := value
- and type origin := origin
- and type loc := location)
- = struct
-
- (* This function binds [loc] to [v], of type [typ], in [state].
- [v] can be [`Bottom], which means that its contents are guaranteed
- to be indeterminate (e.g. unitialized data). *)
- let bind_loc loc typ v state =
- match v with
- (* We are adding a "good" value. Store it in the state. *)
- | `Value v -> add loc typ v state
- (* Indeterminate value. Drop the information known for loc. *)
- | `Bottom -> remove loc state
-
- (* This function updates [state] with information for [expr], only possible
- when it is an lvalue. In this case, we can update the corresponding
- location with the result of the evaluation of [exp]. Both the value and
- the location are found in the [valuation]. *)
- let assume_exp valuation expr record state =
- match expr.enode with
- | Lval lv -> begin
- match Valuation.find_loc valuation lv with
- | `Top -> state
- | `Value {loc; typ} ->
- if Precise_locs.cardinal_zero_or_one loc
- then bind_loc loc typ record.value.v state
- else state
- end
- | _ -> state
-
- (* This function fills [state] according to the information available
- in [valuation]. This information is computed by Eva's engine for
- all the expressions involved in the current statement. *)
- let assume_valuation valuation state =
- Valuation.fold (assume_exp valuation) valuation state
-
- (* Abstraction of an assignment. *)
- let assign _kinstr lv _expr value valuation state =
- (* Update the state with the information obtained from evaluating
- [lv] and [e] *)
- let state = assume_valuation valuation state in
- (* Extract the abstract value *)
- let value = Eval.value_assigned value in
- (* Store the information [lv = e;] in the state *)
- let state = bind_loc lv.lloc lv.ltyp value state in
- `Value state
-
- let update valuation state = `Value (assume_valuation valuation state)
-
- (* Abstraction of a conditional. All information inferred by the engine
- is present in the valuation, and must be stored in the memory
- abstraction of the domain itself. *)
- let assume _stmt _expr _pos = update
-
- let start_call _stmt call _valuation state =
- let bind_argument state argument =
- let typ = argument.formal.vtype in
- let loc = Main_locations.PLoc.eval_varinfo argument.formal in
- let value = Eval.value_assigned argument.avalue in
- bind_loc loc typ value state
- in
- let state = List.fold_left bind_argument state call.arguments in
- `Value state
-
- let finalize_call _stmt call ~pre:_ ~post =
- let kf_name = Kernel_function.get_name call.kf in
- match find_builtin kf_name, call.return with
- | None, _ | _, None -> `Value post
- | Some f, Some return ->
- let extract_value arg = Eval.value_assigned arg.avalue in
- let args = List.map extract_value call.arguments in
- if List.exists (function `Bottom -> true | `Value _ -> false) args
- then `Bottom
- else
- let args = List.map Bottom.non_bottom args in
- f args >>-: fun result ->
- let return_loc = Main_locations.PLoc.eval_varinfo return in
- bind_loc return_loc return.vtype (`Value result) post
-
- let show_expr valuation state fmt expr =
- match expr.enode with
- | Lval lval ->
- begin
- match Valuation.find_loc valuation lval with
- | `Top -> ()
- | `Value {loc; typ} -> Value.pretty fmt (find loc typ state)
- end
- | _ -> ()
- end
+ (* This function binds [loc] to [v], of type [typ], in [state].
+ [v] can be [`Bottom], which means that its contents are guaranteed
+ to be indeterminate (e.g. unitialized data). *)
+ let bind_loc loc typ v state =
+ match v with
+ (* We are adding a "good" value. Store it in the state. *)
+ | `Value v -> add loc typ v state
+ (* Indeterminate value. Drop the information known for loc. *)
+ | `Bottom -> remove loc state
+
+ (* This function updates [state] with information for [expr], only possible
+ when it is an lvalue. In this case, we can update the corresponding
+ location with the result of the evaluation of [exp]. Both the value and
+ the location are found in the [valuation]. *)
+ let assume_exp valuation expr record state =
+ match expr.enode with
+ | Lval lv -> begin
+ match valuation.Abstract_domain.find_loc lv with
+ | `Top -> state
+ | `Value {loc; typ} ->
+ if Precise_locs.cardinal_zero_or_one loc
+ then bind_loc loc typ record.value.v state
+ else state
+ end
+ | _ -> state
+
+ (* This function fills [state] according to the information available
+ in [valuation]. This information is computed by Eva's engine for
+ all the expressions involved in the current statement. *)
+ let assume_valuation valuation state =
+ valuation.Abstract_domain.fold (assume_exp valuation) state
+
+ (* Abstraction of an assignment. *)
+ let assign _kinstr lv _expr value valuation state =
+ (* Update the state with the information obtained from evaluating
+ [lv] and [e] *)
+ let state = assume_valuation valuation state in
+ (* Extract the abstract value *)
+ let value = Eval.value_assigned value in
+ (* Store the information [lv = e;] in the state *)
+ let state = bind_loc lv.lloc lv.ltyp value state in
+ `Value state
+
+ let update valuation state = `Value (assume_valuation valuation state)
+
+ (* Abstraction of a conditional. All information inferred by the engine
+ is present in the valuation, and must be stored in the memory
+ abstraction of the domain itself. *)
+ let assume _stmt _expr _pos = update
+
+ let start_call _stmt call _valuation state =
+ let bind_argument state argument =
+ let typ = argument.formal.vtype in
+ let loc = Main_locations.PLoc.eval_varinfo argument.formal in
+ let value = Eval.value_assigned argument.avalue in
+ bind_loc loc typ value state
+ in
+ let state = List.fold_left bind_argument state call.arguments in
+ `Value state
+
+ let finalize_call _stmt call ~pre:_ ~post =
+ let kf_name = Kernel_function.get_name call.kf in
+ match find_builtin kf_name, call.return with
+ | None, _ | _, None -> `Value post
+ | Some f, Some return ->
+ let extract_value arg = Eval.value_assigned arg.avalue in
+ let args = List.map extract_value call.arguments in
+ if List.exists (function `Bottom -> true | `Value _ -> false) args
+ then `Bottom
+ else
+ let args = List.map Bottom.non_bottom args in
+ f args >>-: fun result ->
+ let return_loc = Main_locations.PLoc.eval_varinfo return in
+ bind_loc return_loc return.vtype (`Value result) post
+
+ let show_expr valuation state fmt expr =
+ match expr.enode with
+ | Lval lval ->
+ begin
+ match valuation.Abstract_domain.find_loc lval with
+ | `Top -> ()
+ | `Value {loc; typ} -> Value.pretty fmt (find loc typ state)
+ end
+ | _ -> ()
let enter_scope _kf _vars state = state
let leave_scope _kf vars state = remove_variables vars state
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 00220370476..f325e2a7148 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -466,6 +466,8 @@ module Internal : Domain_builder.InputDomain
type state = Memory.t
type value = V.t
type location = Precise_locs.precise_location
+ type origin = unit
+
include (Memory: sig
include Datatype.S_with_collections with type t = state
include Abstract_domain.Lattice with type state := state
@@ -485,101 +487,87 @@ module Internal : Domain_builder.InputDomain
let incr_loop_counter _ state = state
let leave_loop _ state = state
- type origin = unit
-
- module Transfer (Valuation: Abstract_domain.Valuation
- with type value = value
- and type origin = origin
- and type loc = Precise_locs.precise_location)
- : Abstract_domain.Transfer
- with type state := state
- and type value := V.t
- and type location := Precise_locs.precise_location
- and type valuation := Valuation.t
- = struct
-
- (* build a [get_locs] function from a valuation *)
- let get_locs valuation =
- fun lv ->
- let r =
- match Valuation.find_loc valuation lv with
- | `Top -> Precise_locs.loc_top
- | `Value loc -> loc.Eval.loc
- in
- if Precise_locs.(equal_loc loc_top r) then
- Value_parameters.fatal "Unknown location for %a" Printer.pp_lval lv
- else r
-
- (* update the state according to the information known in the valuation.
- Important, because on statements such as [if (t[i] + j <= 3)], the
- interesting information on [t[i]] is only in the valuation. *)
- let update valuation state =
- let aux e r state =
- let v = r.value in
- (* TODO: incorporate DB criterion: only expressions that are immediate
- lvalues, or that embed two non-singleton lvalues for the first
- time. *)
- match r.reductness, v.v, v.initialized, v.escaping with
- | (Created | Reduced), `Value v, true, false ->
- if not (is_cond e) && multiple_loc_exp (get_locs valuation) e then
- begin
- let k = K.HCE.of_exp e in
- (* remove the existing binding: the key may already be in
- the state, and [add_exp] assumes it is not the case.
- The new dependencies may not be the same (in rare cases
- where one dependency has disappeared by reduction), so
- we need to update the dependency inverse maps. *)
- (* TODO: it would be more efficient to use a function that
- compares the previous and current dependencies, and update
- the inverse maps accordingly. *)
- let state = Memory.remove_key k state in
- Memory.add_exp state (get_locs valuation) e v
- end
- else
- state
- | _ -> state
- in
- `Value (Valuation.fold aux valuation state)
-
- let store_value valuation lv loc state v =
- let loc = Precise_locs.imprecise_location loc in
- (* Remove the keys that are overwritten because [loc] is written *)
- let state = Memory.kill loc state in
- if Locations.cardinal_zero_or_one loc then
- (* Stored by the standard domain. Skip *)
- `Value state
- else
- (* Add the new binding *)
- `Value (Memory.add_lv state (get_locs valuation) lv v)
-
- (* Assume we may be copying indeterminate bits. Kill existing information *)
- let store_indeterminate state loc =
- let loc = Precise_locs.imprecise_location loc in
- `Value (Memory.kill loc state)
-
- let store_copy valuation lv loc state fv =
- if Cil.isArithmeticOrPointerType lv.ltyp then
- match fv.v, fv.initialized, fv.escaping with
- | `Value v, true, false -> store_value valuation lv.lval loc state v
- | _ -> store_indeterminate state loc
- else
- store_indeterminate state loc
+ (* build a [get_locs] function from a valuation *)
+ let get_locs valuation =
+ fun lv ->
+ let r =
+ match valuation.Abstract_domain.find_loc lv with
+ | `Top -> Precise_locs.loc_top
+ | `Value loc -> loc.Eval.loc
+ in
+ if Precise_locs.(equal_loc loc_top r) then
+ Value_parameters.fatal "Unknown location for %a" Printer.pp_lval lv
+ else r
+
+ (* update the state according to the information known in the valuation.
+ Important, because on statements such as [if (t[i] + j <= 3)], the
+ interesting information on [t[i]] is only in the valuation. *)
+ let update valuation state =
+ let aux e r state =
+ let v = r.value in
+ (* TODO: incorporate DB criterion: only expressions that are immediate
+ lvalues, or that embed two non-singleton lvalues for the first
+ time. *)
+ match r.reductness, v.v, v.initialized, v.escaping with
+ | (Created | Reduced), `Value v, true, false ->
+ if not (is_cond e) && multiple_loc_exp (get_locs valuation) e then
+ begin
+ let k = K.HCE.of_exp e in
+ (* remove the existing binding: the key may already be in
+ the state, and [add_exp] assumes it is not the case.
+ The new dependencies may not be the same (in rare cases
+ where one dependency has disappeared by reduction), so
+ we need to update the dependency inverse maps. *)
+ (* TODO: it would be more efficient to use a function that
+ compares the previous and current dependencies, and update
+ the inverse maps accordingly. *)
+ let state = Memory.remove_key k state in
+ Memory.add_exp state (get_locs valuation) e v
+ end
+ else
+ state
+ | _ -> state
+ in
+ `Value (valuation.Abstract_domain.fold aux state)
+
+ let store_value valuation lv loc state v =
+ let loc = Precise_locs.imprecise_location loc in
+ (* Remove the keys that are overwritten because [loc] is written *)
+ let state = Memory.kill loc state in
+ if Locations.cardinal_zero_or_one loc then
+ (* Stored by the standard domain. Skip *)
+ `Value state
+ else
+ (* Add the new binding *)
+ `Value (Memory.add_lv state (get_locs valuation) lv v)
+
+ (* Assume we may be copying indeterminate bits. Kill existing information *)
+ let store_indeterminate state loc =
+ let loc = Precise_locs.imprecise_location loc in
+ `Value (Memory.kill loc state)
+
+ let store_copy valuation lv loc state fv =
+ if Cil.isArithmeticOrPointerType lv.ltyp then
+ match fv.v, fv.initialized, fv.escaping with
+ | `Value v, true, false -> store_value valuation lv.lval loc state v
+ | _ -> store_indeterminate state loc
+ else
+ store_indeterminate state loc
- (* perform [lv = e] in [state] *)
- let assign _kinstr lv _e v valuation state =
- update valuation state >>- fun state ->
- match v with
- | Copy (_, vc) -> store_copy valuation lv lv.lloc state vc
- | Assign v -> store_value valuation lv.lval lv.lloc state v
+ (* perform [lv = e] in [state] *)
+ let assign _kinstr lv _e v valuation state =
+ update valuation state >>- fun state ->
+ match v with
+ | Copy (_, vc) -> store_copy valuation lv lv.lloc state vc
+ | Assign v -> store_value valuation lv.lval lv.lloc state v
- let assume _stmt _exp _pos valuation state = update valuation state
+ let assume _stmt _exp _pos valuation state = update valuation state
- let start_call _stmt _call valuation state = update valuation state
+ let start_call _stmt _call valuation state = update valuation state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call ~pre:_ ~post = `Value post
- let show_expr _valuation _state _fmt _expr = ()
- end
+ let show_expr _valuation _state _fmt _expr = ()
let top_query = `Value (V.top, ()), Alarmset.all
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index c22c8bcfd19..771c2220a59 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -848,6 +848,7 @@ module Internal = struct
type nonrec state = state
type value = Cvalue.V.t
type location = Precise_locs.precise_location
+ type origin = unit
include (Traces: sig
include Datatype.S_with_collections with type t = state
@@ -856,68 +857,50 @@ module Internal = struct
let log_category = Value_parameters.register_category "d-traces"
- type origin = unit
+ let assign ki lv e _v _valuation state =
+ let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
+ `Value (Traces.add_trans state trans)
+
+ let assume stmt e pos _valuation state =
+ let trans = Assume (stmt, e, pos) in
+ `Value (Traces.add_trans state trans)
+
+ let start_call stmt call _valuation state =
+ let kf = call.Eval.kf in
+ if Kernel_function.is_definition kf then
+ let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
+ (Kernel_function.is_definition call.Eval.kf) in
+ let state = Traces.add_trans state (Msg msg) in
+ let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
+ let state = Traces.add_trans state (EnterScope (kf, formals)) in
+ let state = List.fold_left (fun state arg ->
+ Traces.add_trans state
+ (Assign (Kstmt stmt, Cil.var arg.Eval.formal,
+ arg.Eval.formal.Cil_types.vtype,
+ arg.Eval.concrete))) state call.Eval.arguments in
+ `Value state
+ else
+ (** enter the scope of the dumb result variable *)
+ let var = call.Eval.return in
+ let state = match var with
+ | Some var -> Traces.add_trans state (EnterScope (kf, [var]))
+ | None -> state in
+ let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
+ let state = Traces.add_trans state
+ (CallDeclared (call.Eval.kf, exps, Extlib.opt_map Cil.var var))
+ in `Value {state with call_declared_function = true}
+
+ let finalize_call _stmt call ~pre:_ ~post =
+ if post.call_declared_function
+ then `Value {post with call_declared_function = false}
+ else
+ let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
+ let state = Traces.add_trans post (Msg msg) in
+ `Value state
- module Transfer (Valuation: Abstract_domain.Valuation
- with type value = value
- and type origin = origin
- and type loc = Precise_locs.precise_location)
- : Abstract_domain.Transfer
- with type state = state
- and type value = Cvalue.V.t
- and type location = Precise_locs.precise_location
- and type valuation = Valuation.t
- = struct
- type value = Cvalue.V.t
- type state = t
- type location = Precise_locs.precise_location
- type valuation = Valuation.t
-
- let assign ki lv e _v _valuation state =
- let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
- `Value (Traces.add_trans state trans)
-
- let assume stmt e pos _valuation state =
- let trans = Assume (stmt, e, pos) in
- `Value (Traces.add_trans state trans)
-
- let start_call stmt call _valuation state =
- let kf = call.Eval.kf in
- if Kernel_function.is_definition kf then
- let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
- (Kernel_function.is_definition call.Eval.kf) in
- let state = Traces.add_trans state (Msg msg) in
- let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
- let state = Traces.add_trans state (EnterScope (kf, formals)) in
- let state = List.fold_left (fun state arg ->
- Traces.add_trans state
- (Assign (Kstmt stmt, Cil.var arg.Eval.formal,
- arg.Eval.formal.Cil_types.vtype,
- arg.Eval.concrete))) state call.Eval.arguments in
- `Value state
- else
- (** enter the scope of the dumb result variable *)
- let var = call.Eval.return in
- let state = match var with
- | Some var -> Traces.add_trans state (EnterScope (kf, [var]))
- | None -> state in
- let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
- let state = Traces.add_trans state
- (CallDeclared (call.Eval.kf, exps, Extlib.opt_map Cil.var var))
- in `Value {state with call_declared_function = true}
-
- let finalize_call _stmt call ~pre:_ ~post =
- if post.call_declared_function
- then `Value {post with call_declared_function = false}
- else
- let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
- let state = Traces.add_trans post (Msg msg) in
- `Value state
-
- let update _valuation state = `Value state
-
- let show_expr _valuation state fmt _expr = Traces.pretty fmt state
- end
+ let update _valuation state = `Value state
+
+ let show_expr _valuation state fmt _expr = Traces.pretty fmt state
(* Memexec *)
(* This domains infers no relation between variables. *)
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index bbc3d74c956..8fd5df76754 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -52,7 +52,6 @@ module Make
include Static
type value = Value.t
type location = Loc.location
-
type origin = unit
let eval_top = `Value (Value.top, ()), Alarmset.all
@@ -61,18 +60,12 @@ module Make
let backward_location _ _ _ loc value = `Value (loc, value)
let reduce_further _ _ _ = []
- module Transfer
- (_: Abstract_domain.Valuation with type value = value
- and type loc = location)
- = struct
-
- let update _ _ = `Value ()
- let assign _ _ _ _ _ _ = `Value ()
- let assume _ _ _ _ _ = `Value ()
- let start_call _ _ _ _ = `Value ()
- let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
- let show_expr _ _ _ _ = ()
- end
+ let update _ _ = `Value ()
+ let assign _ _ _ _ _ _ = `Value ()
+ let assume _ _ _ _ _ = `Value ()
+ let start_call _ _ _ _ = `Value ()
+ let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
+ let show_expr _ _ _ _ = ()
let logic_assign _ _ ~pre:_ _ = ()
let evaluate_predicate _ _ _ = Alarmset.Unknown
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index c9ecc4766a4..63be1240664 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -195,6 +195,7 @@ module type S = sig
module Valuation : Valuation with type value = value
and type origin = origin
and type loc = loc
+ val record: Valuation.t -> (value, loc, origin) Abstract_domain.valuation
val evaluate :
?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
state -> exp -> (Valuation.t * value) evaluated
@@ -1483,6 +1484,11 @@ module Make
module Valuation = Cache
+ let record valuation =
+ Abstract_domain.{ find = Valuation.find valuation;
+ fold = (fun f acc -> Valuation.fold f valuation acc);
+ find_loc = Valuation.find_loc valuation; }
+
let evaluate ?(valuation=Cache.empty) ?(reduction=true) ?subdivnb state expr =
let eval, alarms = subdivided_forward_eval valuation ?subdivnb state expr in
let result =
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index 258657a0c58..ad36f758101 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -39,6 +39,11 @@ module type S = sig
and type origin = origin
and type loc = loc
+ (** Evaluation functions store the results of an evaluation into [Valuation.t]
+ maps. Abstract domains read these results in [Abstract_domain.valuation]
+ records. This function converts the former into the latter. *)
+ val record: Valuation.t -> (value, loc, origin) Abstract_domain.valuation
+
(** [evaluate ~valuation state expr] evaluates the expression [expr] in the
state [state], and returns the pair [result, alarms], where:
- [alarms] are the set of alarms ensuring the soundness of the evaluation;
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index b0ffc5fa32a..3e821a34907 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -116,9 +116,6 @@ module Make (Abstract: Abstractions.Eva) = struct
type value = Value.t
type location = Location.location
- (* Transfer functions. *)
- module TF = Domain.Transfer (Eval.Valuation)
-
(* When using a product of domains, a product of states may have no
concretization (if the domains have inferred incompatible properties)
without being bottom (if the inter-reduction between domains are
@@ -267,7 +264,8 @@ module Make (Abstract: Abstractions.Eva) = struct
if is_ret then assert (Alarmset.is_empty alarms);
Alarmset.emit kinstr alarms;
eval >>- fun (assigned, valuation) ->
- TF.assign kinstr {lval; ltyp; lloc} expr assigned valuation state
+ let valuation = Eval.record valuation in
+ Domain.assign kinstr {lval; ltyp; lloc} expr assigned valuation state
let assign = assign_lv_or_ret ~is_ret:false
let assign_ret = assign_lv_or_ret ~is_ret:true
@@ -282,7 +280,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* TODO: check not comparable. *)
Alarmset.emit (Kstmt stmt) alarms;
eval >>- fun valuation ->
- TF.assume stmt expr positive valuation state
+ Domain.assume stmt expr positive (Eval.record valuation) state
(* ------------------------------------------------------------------------ *)
@@ -312,7 +310,7 @@ module Make (Abstract: Abstractions.Eva) = struct
try
let res =
(* Process the call according to the domain decision. *)
- match TF.start_call stmt call valuation state with
+ match Domain.start_call stmt call (Eval.record valuation) state with
| `Value state ->
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
!compute_call_ref stmt call state
@@ -418,7 +416,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Eval.assume ~valuation state argument.concrete post_value
in
List.fold_left reduce_one_argument valuation reductions >>- fun valuation ->
- TF.update valuation state
+ Domain.update (Eval.record valuation) state
(* -------------------- Treat the results of a call ----------------------- *)
@@ -474,7 +472,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let post = Domain.leave_scope kf_callee leaving_vars state in
(* Computes the state after the call, from the post state at the end of
the called function, and the pre state at the call site. *)
- TF.finalize_call stmt call ~pre ~post >>- fun state ->
+ Domain.finalize_call stmt call ~pre ~post >>- fun state ->
(* Backward propagates the [reductions] on the concrete arguments. *)
reduce_arguments reductions state >>- fun state ->
treat_return ~kf_callee lv call.return stmt state
@@ -483,7 +481,7 @@ module Make (Abstract: Abstractions.Eva) = struct
domains. Do not reduce them, and more importantly, do not remove
them from the scope. (Because the instance from the initial,
non-recursive, call are still present.) *)
- TF.finalize_call stmt call ~pre ~post:state >>- fun state ->
+ Domain.finalize_call stmt call ~pre ~post:state >>- fun state ->
treat_return ~kf_callee lv call.return stmt state
in
let states =
@@ -590,12 +588,12 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Idem as for [print_state]. *)
let show_expr =
if Domain.log_category = Domain_product.product_category
- then TF.show_expr
+ then Domain.show_expr
else if Value_parameters.is_debug_key_enabled Domain.log_category
then
fun valuation state fmt exp ->
Format.fprintf fmt "# %s: @[<hov>%a@]"
- Domain.name (TF.show_expr valuation state) exp
+ Domain.name (Domain.show_expr valuation state) exp
else fun _ _ _ _ -> ()
(* Frama_C_domain_show_each functions. *)
@@ -603,8 +601,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let pretty fmt expr =
let pp fmt =
match fst (Eval.evaluate ~subdivnb state expr) with
- | `Bottom -> Format.fprintf fmt "%s" (Unicode.bottom_string ())
- | `Value (valuation, _value) -> show_expr valuation state fmt expr
+ | `Bottom ->
+ Format.fprintf fmt "%s" (Unicode.bottom_string ())
+ | `Value (valuation, _v) ->
+ show_expr (Eval.record valuation) state fmt expr
in
Format.fprintf fmt "%a : @[<h>%t@]" Printer.pp_exp expr pp
in
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 87940525f00..1d16932e3d9 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -226,9 +226,6 @@ struct
(* --- Evaluation and split functions ------------------------------------- *)
- (* Domains transfer functions. *)
- module TF = Abstract.Dom.Transfer (Abstract.Eval.Valuation)
-
(* Evaluation with no reduction and no subdivision. *)
let evaluate = Abstract.Eval.evaluate ~reduction:false ~subdivnb:0
@@ -278,7 +275,7 @@ struct
let state =
Abstract.Eval.assume ~valuation state exp value >>- fun valuation ->
(* Check the reduction *)
- TF.update valuation state
+ Abstract.Dom.update (Abstract.Eval.record valuation) state
in
match state with
| `Value state ->
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 0181dc86435..638dffd79ca 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -186,8 +186,6 @@ module Eva =
(Main_locations.PLoc)
(Cvalue_domain.State)
-module Transfer = Cvalue_domain.State.Transfer (Eva.Valuation)
-
let inject_cvalue state = state, Locals_scoping.bottom ()
let bot_value = function
@@ -199,7 +197,7 @@ let bot_state = function
| `Value s -> s
let update valuation state =
- bot_state (Transfer.update valuation state >>-: fst)
+ bot_state (Cvalue_domain.State.update (Eva.record valuation) state >>-: fst)
let rec eval_deps state e =
match e.enode with
--
GitLab