diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 1e109a39629a2e95115db3b403be1112542972ba..d810aa0d99919467335cedb4939e4c56408bd45a 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -360,6 +360,8 @@ end
module Proxy(A : Analysis.S) : EvaProxy = struct
+ include Cvalue_domain.Getters (A.Dom)
+
open Eval
type dstate = A.Dom.state or_top_bottom
@@ -448,7 +450,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
(* --- Evaluates an expression or lvalue into an evaluation [result]. ----- *)
let lval_to_offsetmap lval state =
- let cvalue_state = A.Dom.get_cvalue_or_top state in
+ let cvalue_state = get_cvalue_or_top state in
match lval with
| Var vi, NoOffset ->
let r = extract_single_var vi cvalue_state in
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index ff4d21571c61738d0be479e498f7f7f60ca32cfa..19a6077e455b005d09948033cac317b0808b6a88 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -714,16 +714,16 @@ let () = Floating_point.set_round_nearest_even ()
let make name (module Man: Input) =
let module Domain = Make (Man) in
+ let name = "apron-" ^ name and experimental = true and priority = 1 in
let descr =
"Binding to the " ^ name ^ " domain of the Apron library. " ^
"See http://apron.cri.ensmp.fr/library for more details."
in
- let name = "apron-" ^ name in
- let abstraction =
- Abstractions.{ values = Single (module Main_values.Interval);
- domain = Domain (module Domain); }
- in
- Abstractions.register ~name ~descr ~experimental:true ~priority:1 abstraction
+ Abstractions.Domain.register ~name ~descr ~experimental ~priority @@ Domain
+ { key = Domain.key ; domain = (module Domain)
+ ; values = Last Main_values.Interval.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
let octagon = make "octagon" (module Apron_Octagon)
let box = make "box" (module Apron_Box)
@@ -731,6 +731,32 @@ let polka_loose = make "polka-loose" (module Apron_Polka_Loose)
let polka_strict = make "polka-strict" (module Apron_Polka_Strict)
let polka_equality = make "polka-equality" (module Apron_Polka_Equalities)
+(* When the value abstraction contains both a cvalue and an interval
+ component (coming currently from an Apron domain), reduce them from each
+ other. If the Cvalue is not a scalar do nothing, because we do not
+ currently use Apron for pointer offsets. *)
+let reduce_apron_itv cvalue ival =
+ match ival with
+ | None -> begin
+ try cvalue, Some (Cvalue.V.project_ival cvalue)
+ with Cvalue.V.Not_based_on_null -> cvalue, ival
+ end
+ | Some ival ->
+ try
+ let ival' = Cvalue.V.project_ival cvalue in
+ if Ival.is_int ival'
+ then
+ let reduced_ival = Ival.narrow ival ival' in
+ let cvalue = Cvalue.V.inject_ival reduced_ival in
+ cvalue, Some reduced_ival
+ else cvalue, Some ival
+ with Cvalue.V.Not_based_on_null -> cvalue, Some ival
+
+let () =
+ Abstractions.Reducer.register
+ Main_values.CVal.key Main_values.Interval.key reduce_apron_itv
+
+
(*
Local Variables:
compile-command: "make -C ../../../../.. -j"
diff --git a/src/plugins/eva/domains/apron/apron_domain.mli b/src/plugins/eva/domains/apron/apron_domain.mli
index ede77986e150365603b0a878d6a84296bc42c17e..fb06185c0fa58124d767e27515907ea33a980230 100644
--- a/src/plugins/eva/domains/apron/apron_domain.mli
+++ b/src/plugins/eva/domains/apron/apron_domain.mli
@@ -24,11 +24,11 @@
the APRON library: http://apron.cri.ensmp.fr/library
For now, this binding only processes scalar integer variables. *)
-val octagon: Abstractions.flag
-val box: Abstractions.flag
-val polka_loose: Abstractions.flag
-val polka_strict: Abstractions.flag
-val polka_equality: Abstractions.flag
+val octagon: Abstractions.Domain.registered
+val box: Abstractions.Domain.registered
+val polka_loose: Abstractions.Domain.registered
+val polka_strict: Abstractions.Domain.registered
+val polka_equality: Abstractions.Domain.registered
(*
Local Variables:
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 6dca30d2ccbd4b4f031acc222c6c5018ed26f9de..53d65ab877e8d114d209cfa9c88ba52b20a301f7 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -585,6 +585,18 @@ end
let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
+let registered =
+ let name = "cvalue" and priority = 9 in
+ let descr =
+ "Main analysis domain, enabled by default. Should not be disabled."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Domain
+ { key = State.key ; domain = (module State)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
+
+
type prefix = Hptmap.prefix
module Subpart = struct
type t = Model.subtree
@@ -598,6 +610,23 @@ let distinct_subpart (a, _) (b, _) =
with Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
let find_subpart (s, _) prefix = Model.find_prefix s prefix
+
+module Getters (Dom : Abstract.Domain.External) = struct
+ let get_cvalue =
+ match Dom.get State.key with
+ | None -> None
+ | Some get -> Some (fun s -> fst (get s))
+
+ let get_cvalue_or_top =
+ match Dom.get State.key with
+ | None -> fun _ -> Cvalue.Model.top
+ | Some get -> fun s -> fst (get s)
+
+ let get_cvalue_or_bottom = function
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value state -> get_cvalue_or_top state
+end
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.mli b/src/plugins/eva/domains/cvalue/cvalue_domain.mli
index 9c603e71b66e274c0befb703affd35767f17c8ac..c1b6c225d789b44de7cee952f2fa1f3dd9f923d8 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.mli
@@ -27,6 +27,8 @@ module State : Abstract_domain.Leaf
and type location = Main_locations.PLoc.location
and type state = Cvalue.Model.t * Locals_scoping.clobbered_set
+val registered : Abstractions.Domain.registered
+
(** Specific functions for partitioning optimizations. *)
type prefix
@@ -35,6 +37,13 @@ val distinct_subpart :
State.t -> State.t -> (prefix * Subpart.t * Subpart.t) option
val find_subpart : State.t -> prefix -> Subpart.t option
+(** Special getters. *)
+
+module Getters (Dom : Abstract.Domain.External) : sig
+ val get_cvalue : (Dom.t -> Cvalue.Model.t) option
+ val get_cvalue_or_top : Dom.t -> Cvalue.Model.t
+ val get_cvalue_or_bottom : Dom.t Lattice_bounds.or_bottom -> Cvalue.Model.t
+end
(*
diff --git a/src/plugins/eva/domains/domain_lift.ml b/src/plugins/eva/domains/domain_lift.ml
index d527ada3927f690d19a2051d03b999c474e899ca..892db6b19f7783c5c9f6eb39d8d1325283c0ac4c 100644
--- a/src/plugins/eva/domains/domain_lift.ml
+++ b/src/plugins/eva/domains/domain_lift.ml
@@ -23,23 +23,16 @@
open Eval
module type Conversion = sig
- type extended_value
- type extended_location
- type internal_value
- type internal_location
-
- val extend_val : internal_value -> extended_value
- val restrict_val : extended_value -> internal_value
-
- val extend_loc : internal_location -> extended_location
- val restrict_loc : extended_location -> internal_location
+ type extended
+ type internal
+ val extend: internal -> extended
+ val restrict: extended -> internal
end
-
module Make
(Domain: Abstract_domain.Leaf)
- (Convert : Conversion with type internal_value := Domain.value
- and type internal_location := Domain.location)
+ (Val: Conversion with type internal := Domain.value)
+ (Loc: Conversion with type internal := Domain.location)
= struct
include (Domain : Datatype.S_with_collections with type t = Domain.t)
@@ -49,38 +42,38 @@ module Make
let log_category = Domain.log_category
- type value = Convert.extended_value
- type location = Convert.extended_location
+ type value = Val.extended
+ type location = Loc.extended
type origin = Domain.origin
let extract_expr ~oracle context state exp =
- let oracle exp = oracle exp >>=: Convert.restrict_val in
+ let oracle exp = oracle exp >>=: Val.restrict in
Domain.extract_expr ~oracle context state exp >>=: fun (value, origin) ->
- Convert.extend_val value, origin
+ Val.extend value, origin
let extract_lval ~oracle context state lval typ loc =
- let oracle exp = oracle exp >>=: Convert.restrict_val in
- let loc = Convert.restrict_loc loc in
+ let oracle exp = oracle exp >>=: Val.restrict in
+ let loc = Loc.restrict loc in
Domain.extract_lval ~oracle context state lval typ loc
>>=: fun (value, origin) ->
- Convert.extend_val value, origin
+ Val.extend value, origin
let backward_location state lval typ loc value =
Domain.backward_location
- state lval typ (Convert.restrict_loc loc) (Convert.restrict_val value)
+ state lval typ (Loc.restrict loc) (Val.restrict value)
>>-: fun (loc, value) ->
- Convert.extend_loc loc, Convert.extend_val value
+ Loc.extend loc, Val.extend value
let reduce_further state expr value =
- let list = Domain.reduce_further state expr (Convert.restrict_val value) in
- List.map (fun (e, v) -> e, Convert.extend_val v) list
+ let list = Domain.reduce_further state expr (Val.restrict value) in
+ List.map (fun (e, v) -> e, Val.extend v) list
- let lift_left left = { left with lloc = Convert.restrict_loc left.lloc }
+ let lift_left left = { left with lloc = Loc.restrict left.lloc }
let lift_flagged_value value =
- { value with v = value.v >>-: Convert.restrict_val }
+ { value with v = value.v >>-: Val.restrict }
let lift_assigned = function
- | Assign value -> Assign (Convert.restrict_val value)
+ | Assign value -> Assign (Val.restrict value)
| Copy (lval, value) -> Copy (lift_left lval, lift_flagged_value value)
let lift_argument arg = { arg with avalue = lift_assigned arg.avalue }
@@ -98,7 +91,7 @@ module Make
| `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 lift_loc_record r = { r with loc = Loc.restrict 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
@@ -126,7 +119,7 @@ module Make
let show_expr valuation = Domain.show_expr (lift_valuation valuation)
let lift_logic_dep dep =
- let location = Option.map Convert.restrict_loc dep.location in
+ let location = Option.map Loc.restrict dep.location in
{ dep with location }
let lift_logic_assigns = function
@@ -135,7 +128,7 @@ module Make
let logic_assign assigns location state =
let assigns = Option.map (fun (a, s) -> lift_logic_assigns a, s) assigns in
- Domain.logic_assign assigns (Convert.restrict_loc location) state
+ Domain.logic_assign assigns (Loc.restrict location) state
let evaluate_predicate = Domain.evaluate_predicate
let reduce_by_predicate = Domain.reduce_by_predicate
@@ -150,7 +143,7 @@ module Make
let empty = Domain.empty
let initialize_variable lval loc ~initialized init_value state =
- let loc = Convert.restrict_loc loc in
+ let loc = Loc.restrict loc in
Domain.initialize_variable lval loc ~initialized init_value state
let initialize_variable_using_type = Domain.initialize_variable_using_type
diff --git a/src/plugins/eva/domains/domain_lift.mli b/src/plugins/eva/domains/domain_lift.mli
index a1f2fba0a689502ef007bf109e27bdda7e67d7a0..1630af2e95f852715ecb83e93548c442d29bc10e 100644
--- a/src/plugins/eva/domains/domain_lift.mli
+++ b/src/plugins/eva/domains/domain_lift.mli
@@ -20,28 +20,20 @@
(* *)
(**************************************************************************)
-
module type Conversion = sig
- type extended_value
- type extended_location
- type internal_value
- type internal_location
-
- val extend_val : internal_value -> extended_value
- val restrict_val : extended_value -> internal_value
-
- val extend_loc : internal_location -> extended_location
- val restrict_loc : extended_location -> internal_location
+ type extended
+ type internal
+ val extend: internal -> extended
+ val restrict: extended -> internal
end
-
module Make
(Domain: Abstract_domain.Leaf)
- (Convert : Conversion with type internal_value := Domain.value
- and type internal_location := Domain.location)
+ (Val: Conversion with type internal := Domain.value)
+ (Loc: Conversion with type internal := Domain.location)
: Abstract.Domain.Internal with type state = Domain.state
- and type value = Convert.extended_value
- and type location = Convert.extended_location
+ and type value = Val.extended
+ and type location = Loc.extended
and type origin = Domain.origin
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 9c3d309cafddc1127bb56bd9fe631cdc0823da08..514bcc6815da9a3d4360beee7b4fc5c2e33f367e 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -528,3 +528,22 @@ module Make
| ISEmpty | ISFormals -> Base.SetLattice.empty
| ISCaller -> Base.SetLattice.top
end
+
+
+
+module Register = struct
+ type location = Precise_locs.precise_location
+ module Make (V : Abstract.Value.External) = Make (V)
+end
+
+let registered =
+ let name = "equality" and priority = 8 in
+ let descr =
+ "Infers equalities between syntactic C expressions. \
+ Makes the analysis less dependent on temporary variables and \
+ intermediate computations."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Functor
+ { domain = (module Register)
+ ; locations = Last Main_locations.PLoc.registered
+ }
diff --git a/src/plugins/eva/domains/equality/equality_domain.mli b/src/plugins/eva/domains/equality/equality_domain.mli
index 56a182e4a562bc10ba07cb09b6d82a8dc5b2827b..f01057153ea6a01cd5f76c60ad819a72688bf687 100644
--- a/src/plugins/eva/domains/equality/equality_domain.mli
+++ b/src/plugins/eva/domains/equality/equality_domain.mli
@@ -42,3 +42,5 @@ module Make (Value : Abstract.Value.External) : sig
val pretty_debug : Format.formatter -> t -> unit
end
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 4906186a931315ff8a6ad691b4846240d0630b35..4214218302687d1d33e43d2c81f84bfcaf1dd968 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1288,3 +1288,15 @@ module D : Abstract_domain.Leaf
let top = G.empty (* must not be used, not neutral w.r.t. join (because
join crashes...)!! *)
end
+
+let registered =
+ let name = "gauges" and priority = 6 in
+ let descr =
+ "Infers linear inequalities between the variables modified within a loop \
+ and a special loop counter."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Domain
+ { key = D.key ; domain = (module D)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.mli b/src/plugins/eva/domains/gauges/gauges_domain.mli
index d268a29ab40632c4c2a0108e27baba86158db861..8a9636ef90e32912238fb6807137068f5f903565 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.mli
+++ b/src/plugins/eva/domains/gauges/gauges_domain.mli
@@ -26,3 +26,5 @@
module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index fce469fb49423b4973d549844d795b42ded00e54..04e59101a87a7347786c15ef0cdf1668c11a9c9c 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -267,6 +267,16 @@ module D
let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
end
+let registered =
+ let name = "inout" and priority = 5 and experimental = true in
+ let descr = "Infers the inputs and outputs of each function." in
+ Abstractions.Domain.register ~name ~priority ~experimental ~descr @@ Domain
+ { key = D.key ; domain = (module D)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
+
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/eva/domains/inout_domain.mli b/src/plugins/eva/domains/inout_domain.mli
index a224b7ec61a763fcaabbb16c53f27b55bb8e1d12..282d599008c19fdbc76034752474275216ea206a 100644
--- a/src/plugins/eva/domains/inout_domain.mli
+++ b/src/plugins/eva/domains/inout_domain.mli
@@ -25,3 +25,5 @@
module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 4d2cf0c8a9bad96390659645499ac1f0575017fe..96d084d7ff1514b9c6cb4561930a47175e304ecd 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -941,15 +941,16 @@ let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
end)
(* Registers the domain. *)
-let flag =
+let registered =
let name = "multidim"
and descr = "Improve the precision over arrays of structures \
or multidimensional arrays."
and experimental = true
- and abstraction =
- Abstractions.{ values = Single (module Main_values.CVal);
- domain = Domain (module Domain); }
in
- Abstractions.register ~name ~descr ~experimental abstraction
+ Abstractions.Domain.register ~name ~descr ~experimental @@ Domain
+ { key = Domain.key ; domain = (module Domain)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
-let () = Abstractions.register_hook multidim_hook
+let () = Abstractions.Hooks.register multidim_hook
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.mli b/src/plugins/eva/domains/multidim/multidim_domain.mli
index 5df3635d248f49ca8d75027a40dd28a28303ed1f..ce8f376e509af1586a9c62aca8961812da09b2c6 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.mli
+++ b/src/plugins/eva/domains/multidim/multidim_domain.mli
@@ -24,4 +24,4 @@ include Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
-val flag: Abstractions.flag
+val registered: Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/numerors/numerors_domain.ml b/src/plugins/eva/domains/numerors/numerors_domain.ml
index ec40528a61bead026670aee4fa5c71375fd94195..de24c17397dd96f4e478461ca0490e0d14974d91 100644
--- a/src/plugins/eva/domains/numerors/numerors_domain.ml
+++ b/src/plugins/eva/domains/numerors/numerors_domain.ml
@@ -151,17 +151,19 @@ let reduce_cast (module Abstract: Abstractions.S) =
end: Abstractions.S)
(* Register the domain as an Eva abstractions. *)
+let registered =
+ let name = "numerors" and experimental = true in
+ let descr =
+ "Infers ranges for the absolute and relative errors \
+ in floating-point computations. No support of loops."
+ in
+ Abstractions.Domain.register ~name ~experimental ~descr @@ Domain
+ { key = Domain.key ; domain = (module Domain)
+ ; values = Last Numerors_Value.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
+
let () =
let open Abstractions in
- let name = "numerors"
- and descr = "Infers ranges for the absolute and relative errors \
- in floating-point computations. No support of loops."
- and experimental = true
- and abstraction =
- { values = Single (module Numerors_value);
- domain = Domain (module Domain); }
- in
- let reduced_product = Main_values.CVal.key, Numerors_value.key, reduce_error in
- ignore (register ~name ~descr ~experimental abstraction);
- register_value_reduction reduced_product;
- register_hook reduce_cast
+ Reducer.register Main_values.CVal.key Numerors_Value.key reduce_error ;
+ Hooks.register reduce_cast
diff --git a/src/plugins/eva/domains/numerors/numerors_domain.mli b/src/plugins/eva/domains/numerors/numerors_domain.mli
index 707b9094300b0f0f16d9f5c235924e2fea512815..184f827d6225b2022c452269ed95f3785c6122aa 100644
--- a/src/plugins/eva/domains/numerors/numerors_domain.mli
+++ b/src/plugins/eva/domains/numerors/numerors_domain.mli
@@ -24,3 +24,5 @@
of floating-point computations.
Nothing is exported: the domain is registered as an analysis abstraction
in the Eva engine, enabled by the -eva-domains numerors option. *)
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
index 574087982663173f898299f30c7dc913dcb07f8d..6fcf0148880d9328523238309e2b6a4ae5bee494 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.ml
+++ b/src/plugins/eva/domains/numerors/numerors_value.ml
@@ -29,369 +29,375 @@ module P = Precisions
module Arith = Numerors_arithmetics
+module Value = struct
+
+ (*-----------------------------------------------------------------------------
+ * Abstract value for numerical errors estimation
+ *-----------------------------------------------------------------------------
+ * The abstract value is a record with four fields :
+ * - exact : interval abstraction of the real value
+ * - approx : interval abstraction of the float value
+ * - abs_err : interval abstraction of the absolute error value
+ * - rel_err : interval abstraction of the relative error value
+ * A zonotope abstraction for each of those fields may be added
+ *---------------------------------------------------------------------------*)
+ type err = Top | Zero | Elt of Arith.t
+
+
+ (*-----------------------------------------------------------------------------
+ * Pretty printer
+ *---------------------------------------------------------------------------*)
+ let pp_print fmt = function
+ | Elt t -> Arith.pretty fmt t
+ | Zero -> Format.fprintf fmt "{ZERO}"
+ | Top -> Format.fprintf fmt "{TOP}"
+
+
+ (*-----------------------------------------------------------------------------
+ * Set errors to top
+ *---------------------------------------------------------------------------*)
+ let set_absolute_to_top = function
+ | Elt e -> Elt { e with Arith.abs_err = I.top ~prec:P.Real }
+ | err -> err
+
+ let set_relative_to_top = function
+ | Elt e -> Elt { e with Arith.rel_err = I.top ~prec:P.Real }
+ | err -> err
+
+
+ (*-----------------------------------------------------------------------------
+ * Lattice structure
+ *---------------------------------------------------------------------------*)
+ let top = Top
+
+ let is_included x y =
+ match x, y with
+ | Zero, Zero | _, Top -> true
+ | Zero, Elt t -> Arith.is_included (Arith.zero t) t
+ | Elt a, Elt b -> Arith.is_included a b
+ | Elt _, Zero | Top, _ -> false
-(*-----------------------------------------------------------------------------
- * Abstract value for numerical errors estimation
- *-----------------------------------------------------------------------------
- * The abstract value is a record with four fields :
- * - exact : interval abstraction of the real value
- * - approx : interval abstraction of the float value
- * - abs_err : interval abstraction of the absolute error value
- * - rel_err : interval abstraction of the relative error value
- * A zonotope abstraction for each of those fields may be added
- *---------------------------------------------------------------------------*)
-type err = Top | Zero | Elt of Arith.t
-
-
-(*-----------------------------------------------------------------------------
- * Pretty printer
- *---------------------------------------------------------------------------*)
-let pp_print fmt = function
- | Elt t -> Arith.pretty fmt t
- | Zero -> Format.fprintf fmt "{ZERO}"
- | Top -> Format.fprintf fmt "{TOP}"
-
-
-(*-----------------------------------------------------------------------------
- * Set errors to top
- *---------------------------------------------------------------------------*)
-let set_absolute_to_top = function
- | Elt e -> Elt { e with Arith.abs_err = I.top ~prec:P.Real }
- | err -> err
-
-let set_relative_to_top = function
- | Elt e -> Elt { e with Arith.rel_err = I.top ~prec:P.Real }
- | err -> err
-
-
-(*-----------------------------------------------------------------------------
- * Lattice structure
- *---------------------------------------------------------------------------*)
-let top = Top
-
-let is_included x y =
- match x, y with
- | Zero, Zero | _, Top -> true
- | Zero, Elt t -> Arith.is_included (Arith.zero t) t
- | Elt a, Elt b -> Arith.is_included a b
- | Elt _, Zero | Top, _ -> false
-
-let join x y =
- match x, y with
- | Zero, Zero -> Zero
- | Top, _ | _, Top -> Top
- | Elt a, Zero | Zero, Elt a -> Elt (Arith.join (Arith.zero a) a)
- | Elt a, Elt b -> Elt (Arith.join a b)
-
-let narrow x y =
- match x, y with
- | Zero, Zero -> `Value Zero
- | Top, t | t, Top -> `Value t
- | Elt a, Zero | Zero, Elt a ->
- Arith.narrow (Arith.zero a) a >>- fun t -> `Value (Elt t)
- | Elt a, Elt b -> Arith.narrow a b >>- fun t -> `Value (Elt t)
-
-let reduce _ t = `Value t
-
-
-(*-----------------------------------------------------------------------------
- * Elements needed for Eva core
- *---------------------------------------------------------------------------*)
-module T = struct
- type t = err
- include Datatype.Undefined
- let structural_descr = Structural_descr.t_unknown
- let compare x y =
+ let join x y =
match x, y with
- | Elt a, Elt b -> Arith.compare a b
- | Top, Top | Zero, Zero -> 0
- | Top, _ | _, Zero -> 1
- | _, Top | Zero, _ -> -1
- let equal = Datatype.from_compare
- let hash = Hashtbl.hash
- let reprs = [top]
- let name = "Value.Numerors_values.Numerors"
- let pretty = pp_print
-end
-include Datatype.Make(T)
-let pretty_debug = pretty
-let pretty_typ _ = pretty
-let key = Structure.Key_Value.create_key "numerors_values"
+ | Zero, Zero -> Zero
+ | Top, _ | _, Top -> Top
+ | Elt a, Zero | Zero, Elt a -> Elt (Arith.join (Arith.zero a) a)
+ | Elt a, Elt b -> Elt (Arith.join a b)
+ let narrow x y =
+ match x, y with
+ | Zero, Zero -> `Value Zero
+ | Top, t | t, Top -> `Value t
+ | Elt a, Zero | Zero, Elt a ->
+ Arith.narrow (Arith.zero a) a >>- fun t -> `Value (Elt t)
+ | Elt a, Elt b -> Arith.narrow a b >>- fun t -> `Value (Elt t)
+
+ let reduce _ t = `Value t
+
+
+ (*-----------------------------------------------------------------------------
+ * Elements needed for Eva core
+ *---------------------------------------------------------------------------*)
+ module T = struct
+ type t = err
+ include Datatype.Undefined
+ let structural_descr = Structural_descr.t_unknown
+ let compare x y =
+ match x, y with
+ | Elt a, Elt b -> Arith.compare a b
+ | Top, Top | Zero, Zero -> 0
+ | Top, _ | _, Zero -> 1
+ | _, Top | Zero, _ -> -1
+ let equal = Datatype.from_compare
+ let hash = Hashtbl.hash
+ let reprs = [top]
+ let name = "Value.Numerors_values.Numerors"
+ let pretty = pp_print
+ end
+ include Datatype.Make(T)
+ let pretty_debug = pretty
+ let pretty_typ _ = pretty
+
+
+ (*-----------------------------------------------------------------------------
+ * Constructors
+ *---------------------------------------------------------------------------*)
+ let zero = Zero
+ let one = top
+ let top_int = top
+ let inject_int _ _ = top
+
+ let create exact approx abs_err rel_err =
+ Elt (Arith.create exact approx abs_err rel_err)
+
+ let of_ints ~prec min max =
+ let exact = I.of_ints ~prec:P.Real (min, max) in
+ let approx = I.of_ints ~prec:prec (min, max) in
+ let abs_err = I.zero ~prec:P.Real in
+ let rel_err = I.zero ~prec:P.Real in
+ create exact approx abs_err rel_err
+
+
+ (*-----------------------------------------------------------------------------
+ * Miscellaneous
+ *---------------------------------------------------------------------------*)
+
+ (* Handle the computation mode for the forward operations *)
+ let mode_on_errors exact approx abs_err rel_err =
+ Elt (Arith.forward_interaction (Arith.create exact approx abs_err rel_err))
+
+ (*-----------------------------------------------------------------------------
+ * Arithmetic import
+ *---------------------------------------------------------------------------*)
+ module Exact = Arith.Exact
+ module Approx = Arith.Approx
+ module Abs_Err = Arith.Abs_Err
+ module Rel_Err = Arith.Rel_Err
+
+
+ (*-----------------------------------------------------------------------------
+ * Numerors value of a constant
+ *---------------------------------------------------------------------------*)
+ let constant _ = function
+ | CReal (r, fkind, opt) ->
+ let prec = Precisions.of_fkind fkind in
+ let exact =
+ match opt with
+ | Some s -> I.of_strings ~prec:Precisions.Real (s, s)
+ | None -> I.of_floats ~prec:Precisions.Real (r, r)
+ in
+ let approx = I.of_floats_without_rounding ~prec (r, r) in
+ let abs_err = I.sub approx exact in
+ let rel_err =
+ if I.is_zero exact then I.of_floats ~prec:P.Real (0.0, 0.0)
+ else I.div abs_err exact
+ in
+ mode_on_errors exact approx abs_err rel_err
+ | _ -> top
+
+
+ (*-----------------------------------------------------------------------------
+ * Forward unary operations on Numerors value
+ *---------------------------------------------------------------------------*)
+ let forward_unop _typ op v =
+ match v, op with
+ | Elt v, Neg ->
+ let exact , approx = Exact.Forward.neg v, Approx.Forward.neg v in
+ let abs_err = Abs_Err.Forward.neg v ~exact ~approx in
+ let rel_err = Rel_Err.Forward.neg v ~exact ~abs_err in
+ `Value (mode_on_errors exact approx abs_err rel_err)
+ | Zero, Neg -> `Value zero
+ | _, LNot | _, BNot | Top, _ -> `Value top
+
+
+ (*-----------------------------------------------------------------------------
+ * Forward cast on Numerors value
+ *-----------------------------------------------------------------------------
+ * The cast of integers into floats is actually handled by the Numerors
+ * domain in the module <MakeNumerorsCValuesProduct>.
+ *---------------------------------------------------------------------------*)
+ let forward_cast ~src_type ~dst_type = function
+ | Top -> `Value Top
+ | Zero -> `Value Zero
+ | Elt t ->
+ match src_type, dst_type with
+ | Eval_typ.TSFloat _, Eval_typ.TSFloat fk ->
+ `Value (Elt (Arith.change_prec (Precisions.of_fkind fk) t))
+ | _, _ -> `Value top
+
+
+ (*-----------------------------------------------------------------------------
+ * Forward binary operations on Numerors values
+ *---------------------------------------------------------------------------*)
+ let forward_binop _typ op x y =
+ match x, y, op with
+ | Elt x, Elt y, PlusA ->
+ let exact , approx = Exact.Forward.add x y, Approx.Forward.add x y in
+ let abs_err = Abs_Err.Forward.add x y ~exact ~approx in
+ let rel_err = Rel_Err.Forward.add x y ~exact ~abs_err in
+ `Value (mode_on_errors exact approx abs_err rel_err)
+ | Elt x, Elt y, MinusA ->
+ let exact , approx = Exact.Forward.sub x y, Approx.Forward.sub x y in
+ let abs_err = Abs_Err.Forward.sub x y ~exact ~approx in
+ let rel_err = Rel_Err.Forward.sub x y ~exact ~abs_err in
+ `Value (mode_on_errors exact approx abs_err rel_err)
+ | Elt x, Elt y, Mult ->
+ let exact , approx = Exact.Forward.mul x y, Approx.Forward.mul x y in
+ let abs_err = Abs_Err.Forward.mul x y ~exact ~approx in
+ let rel_err = Rel_Err.Forward.mul x y ~exact ~abs_err in
+ `Value (mode_on_errors exact approx abs_err rel_err)
+ | Elt x, Elt y, Div ->
+ let exact , approx = Exact.Forward.div x y, Approx.Forward.div x y in
+ let abs_err = Abs_Err.Forward.div x y ~exact ~approx in
+ let rel_err = Rel_Err.Forward.div x y ~exact ~abs_err in
+ `Value (mode_on_errors exact approx abs_err rel_err)
+ | _, _, _ -> `Value top
+
+ (*-----------------------------------------------------------------------------
+ * Backward unary operations on Numerors values
+ *---------------------------------------------------------------------------*)
+ let backward_unop ~typ_arg:_ op ~arg ~res =
+ match arg, res, op with
+ | Elt x, Elt r, Neg ->
+ Exact.Backward.neg x r >>- fun exact ->
+ Approx.Backward.neg x r >>- fun approx ->
+ Abs_Err.Backward.neg x r >>- fun abs_err ->
+ Rel_Err.Backward.neg x r >>- fun rel_err ->
+ `Value (Some (create exact approx abs_err rel_err))
+ | _, _, _ -> `Value None
+
+
+ (*-----------------------------------------------------------------------------
+ * Backward binary operations on Numerors values
+ *---------------------------------------------------------------------------*)
+ let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
+ match left, right, result, op with
+ | Elt x, Elt y, Elt r, PlusA ->
+ Exact.Backward.add x y r >>- fun (x_exact , y_exact ) ->
+ Approx.Backward.add x y r >>- fun (x_approx , y_approx ) ->
+ Abs_Err.Backward.add x y r >>- fun (x_abs_err , y_abs_err ) ->
+ Rel_Err.Backward.add x y r >>- fun (x_rel_err , y_rel_err ) ->
+ let x = create x_exact x_approx x_abs_err x_rel_err in
+ let y = create y_exact y_approx y_abs_err y_rel_err in
+ `Value (Some x, Some y)
+ | Elt x, Elt y, Elt r, MinusA ->
+ Exact.Backward.sub x y r >>- fun (x_exact , y_exact ) ->
+ Approx.Backward.sub x y r >>- fun (x_approx , y_approx ) ->
+ Abs_Err.Backward.sub x y r >>- fun (x_abs_err , y_abs_err ) ->
+ Rel_Err.Backward.sub x y r >>- fun (x_rel_err , y_rel_err ) ->
+ let x = create x_exact x_approx x_abs_err x_rel_err in
+ let y = create y_exact y_approx y_abs_err y_rel_err in
+ `Value (Some x, Some y)
+ | Elt x, Elt y, Elt r, Mult ->
+ Exact.Backward.mul x y r >>- fun (x_exact , y_exact ) ->
+ Approx.Backward.mul x y r >>- fun (x_approx , y_approx ) ->
+ Abs_Err.Backward.mul x y r >>- fun (x_abs_err , y_abs_err ) ->
+ Rel_Err.Backward.mul x y r >>- fun (x_rel_err , y_rel_err ) ->
+ let x = create x_exact x_approx x_abs_err x_rel_err in
+ let y = create y_exact y_approx y_abs_err y_rel_err in
+ `Value (Some x, Some y)
+ | Elt x, Elt y, Elt r, Div ->
+ Exact.Backward.div x y r >>- fun (x_exact , y_exact ) ->
+ Approx.Backward.div x y r >>- fun (x_approx , y_approx ) ->
+ Abs_Err.Backward.div x y r >>- fun (x_abs_err , y_abs_err ) ->
+ Rel_Err.Backward.div x y r >>- fun (x_rel_err , y_rel_err ) ->
+ let x = create x_exact x_approx x_abs_err x_rel_err in
+ let y = create y_exact y_approx y_abs_err y_rel_err in
+ `Value (Some x, Some y)
+ (* x == y *)
+ | _, _, Zero, Ne -> narrow left right >>-: fun t -> Some t, Some t
+ (* x < y *)
+ | Elt x, Elt y, Zero, Ge ->
+ Arith.Backward_Comparisons.lt x y >>-: fun (x, y) ->
+ Some (Elt x), Some (Elt y)
+ (* x <= y *)
+ | Elt x, Elt y, Zero, Gt -> (* x >= y *)
+ Arith.Backward_Comparisons.le x y >>-: fun (x, y) ->
+ Some (Elt x), Some (Elt y)
+ (* x >= y *)
+ | Elt x, Elt y, Zero, Lt ->
+ Arith.Backward_Comparisons.ge x y >>-: fun (x, y) ->
+ Some (Elt x), Some (Elt y)
+ (* x > y *)
+ | Elt x, Elt y, Zero, Le ->
+ Arith.Backward_Comparisons.gt x y >>-: fun (x, y) ->
+ Some (Elt x), Some (Elt y)
+ | _ -> `Value (None, None)
+
+
+ (*-----------------------------------------------------------------------------
+ * Operations not handled on Numerors values
+ *---------------------------------------------------------------------------*)
+
+ let assume_non_zero v = `Unknown v
+ let assume_bounded _kind _bound v = `Unknown v
+ let assume_not_nan ~assume_finite:_ _fkind v = `Unknown v
+ let assume_pointer v = `Unknown v
+ let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
+
+ let rewrap_integer _ _ = top
+ let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
+ let resolve_functions _ = `Top, true
+ let replace_base _substitution t = t
+
+
+ (*-----------------------------------------------------------------------------
+ * Built-in to create values in a interval
+ *---------------------------------------------------------------------------*)
+ let dbetween min max =
+ match min, max with
+ | Elt min, Elt max ->
+ let z = I.zero ~prec:P.Real in
+ let f = I.join min.Arith.approx max.Arith.approx in
+ let r = I.mul f (I.of_ints ~prec:P.Real (1, 1)) in
+ let r = { Arith.exact = r
+ ; Arith.approx = f
+ ; Arith.abs_err = z
+ ; Arith.rel_err = z
+ }
+ in `Value (Elt r)
+ | _, _ -> `Value top
-(*-----------------------------------------------------------------------------
- * Constructors
- *---------------------------------------------------------------------------*)
-let zero = Zero
-let one = top
-let top_int = top
-let inject_int _ _ = top
-
-let create exact approx abs_err rel_err =
- Elt (Arith.create exact approx abs_err rel_err)
-
-let of_ints ~prec min max =
- let exact = I.of_ints ~prec:P.Real (min, max) in
- let approx = I.of_ints ~prec:prec (min, max) in
- let abs_err = I.zero ~prec:P.Real in
- let rel_err = I.zero ~prec:P.Real in
- create exact approx abs_err rel_err
-
-
-(*-----------------------------------------------------------------------------
- * Miscellaneous
- *---------------------------------------------------------------------------*)
-
-(* Handle the computation mode for the forward operations *)
-let mode_on_errors exact approx abs_err rel_err =
- Elt (Arith.forward_interaction (Arith.create exact approx abs_err rel_err))
-
-(*-----------------------------------------------------------------------------
- * Arithmetic import
- *---------------------------------------------------------------------------*)
-module Exact = Arith.Exact
-module Approx = Arith.Approx
-module Abs_Err = Arith.Abs_Err
-module Rel_Err = Arith.Rel_Err
-
-
-(*-----------------------------------------------------------------------------
- * Numerors value of a constant
- *---------------------------------------------------------------------------*)
-let constant _ = function
- | CReal (r, fkind, opt) ->
- let prec = Precisions.of_fkind fkind in
- let exact =
- match opt with
- | Some s -> I.of_strings ~prec:Precisions.Real (s, s)
- | None -> I.of_floats ~prec:Precisions.Real (r, r)
- in
- let approx = I.of_floats_without_rounding ~prec (r, r) in
- let abs_err = I.sub approx exact in
- let rel_err =
- if I.is_zero exact then I.of_floats ~prec:P.Real (0.0, 0.0)
- else I.div abs_err exact
- in
- mode_on_errors exact approx abs_err rel_err
- | _ -> top
-
-
-(*-----------------------------------------------------------------------------
- * Forward unary operations on Numerors value
- *---------------------------------------------------------------------------*)
-let forward_unop _typ op v =
- match v, op with
- | Elt v, Neg ->
- let exact , approx = Exact.Forward.neg v, Approx.Forward.neg v in
- let abs_err = Abs_Err.Forward.neg v ~exact ~approx in
- let rel_err = Rel_Err.Forward.neg v ~exact ~abs_err in
- `Value (mode_on_errors exact approx abs_err rel_err)
- | Zero, Neg -> `Value zero
- | _, LNot | _, BNot | Top, _ -> `Value top
-
-
-(*-----------------------------------------------------------------------------
- * Forward cast on Numerors value
- *-----------------------------------------------------------------------------
- * The cast of integers into floats is actually handled by the Numerors
- * domain in the module <MakeNumerorsCValuesProduct>.
- *---------------------------------------------------------------------------*)
-let forward_cast ~src_type ~dst_type = function
- | Top -> `Value Top
- | Zero -> `Value Zero
- | Elt t ->
- match src_type, dst_type with
- | Eval_typ.TSFloat _, Eval_typ.TSFloat fk ->
- `Value (Elt (Arith.change_prec (Precisions.of_fkind fk) t))
+ let rbetween min max =
+ match min, max with
+ | Elt min, Elt max ->
+ let approx = I.join min.Arith.approx max.Arith.approx in
+ let exact = I.mul approx (I.of_ints ~prec:P.Real (1, 1)) in
+ let rel_err = I.epsilon (I.prec min.Arith.approx) in
+ let abs_err = I.mul rel_err exact in
+ let res = { Arith.exact = exact
+ ; Arith.approx = approx
+ ; Arith.abs_err = abs_err
+ ; Arith.rel_err = rel_err
+ }
+ in `Value (Elt res)
| _, _ -> `Value top
-(*-----------------------------------------------------------------------------
- * Forward binary operations on Numerors values
- *---------------------------------------------------------------------------*)
-let forward_binop _typ op x y =
- match x, y, op with
- | Elt x, Elt y, PlusA ->
- let exact , approx = Exact.Forward.add x y, Approx.Forward.add x y in
- let abs_err = Abs_Err.Forward.add x y ~exact ~approx in
- let rel_err = Rel_Err.Forward.add x y ~exact ~abs_err in
- `Value (mode_on_errors exact approx abs_err rel_err)
- | Elt x, Elt y, MinusA ->
- let exact , approx = Exact.Forward.sub x y, Approx.Forward.sub x y in
- let abs_err = Abs_Err.Forward.sub x y ~exact ~approx in
- let rel_err = Rel_Err.Forward.sub x y ~exact ~abs_err in
- `Value (mode_on_errors exact approx abs_err rel_err)
- | Elt x, Elt y, Mult ->
- let exact , approx = Exact.Forward.mul x y, Approx.Forward.mul x y in
- let abs_err = Abs_Err.Forward.mul x y ~exact ~approx in
- let rel_err = Rel_Err.Forward.mul x y ~exact ~abs_err in
- `Value (mode_on_errors exact approx abs_err rel_err)
- | Elt x, Elt y, Div ->
- let exact , approx = Exact.Forward.div x y, Approx.Forward.div x y in
- let abs_err = Abs_Err.Forward.div x y ~exact ~approx in
- let rel_err = Rel_Err.Forward.div x y ~exact ~abs_err in
- `Value (mode_on_errors exact approx abs_err rel_err)
- | _, _, _ -> `Value top
-
-(*-----------------------------------------------------------------------------
- * Backward unary operations on Numerors values
- *---------------------------------------------------------------------------*)
-let backward_unop ~typ_arg:_ op ~arg ~res =
- match arg, res, op with
- | Elt x, Elt r, Neg ->
- Exact.Backward.neg x r >>- fun exact ->
- Approx.Backward.neg x r >>- fun approx ->
- Abs_Err.Backward.neg x r >>- fun abs_err ->
- Rel_Err.Backward.neg x r >>- fun rel_err ->
- `Value (Some (create exact approx abs_err rel_err))
- | _, _, _ -> `Value None
-
-
-(*-----------------------------------------------------------------------------
- * Backward binary operations on Numerors values
- *---------------------------------------------------------------------------*)
-let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
- match left, right, result, op with
- | Elt x, Elt y, Elt r, PlusA ->
- Exact.Backward.add x y r >>- fun (x_exact , y_exact ) ->
- Approx.Backward.add x y r >>- fun (x_approx , y_approx ) ->
- Abs_Err.Backward.add x y r >>- fun (x_abs_err , y_abs_err ) ->
- Rel_Err.Backward.add x y r >>- fun (x_rel_err , y_rel_err ) ->
- let x = create x_exact x_approx x_abs_err x_rel_err in
- let y = create y_exact y_approx y_abs_err y_rel_err in
- `Value (Some x, Some y)
- | Elt x, Elt y, Elt r, MinusA ->
- Exact.Backward.sub x y r >>- fun (x_exact , y_exact ) ->
- Approx.Backward.sub x y r >>- fun (x_approx , y_approx ) ->
- Abs_Err.Backward.sub x y r >>- fun (x_abs_err , y_abs_err ) ->
- Rel_Err.Backward.sub x y r >>- fun (x_rel_err , y_rel_err ) ->
- let x = create x_exact x_approx x_abs_err x_rel_err in
- let y = create y_exact y_approx y_abs_err y_rel_err in
- `Value (Some x, Some y)
- | Elt x, Elt y, Elt r, Mult ->
- Exact.Backward.mul x y r >>- fun (x_exact , y_exact ) ->
- Approx.Backward.mul x y r >>- fun (x_approx , y_approx ) ->
- Abs_Err.Backward.mul x y r >>- fun (x_abs_err , y_abs_err ) ->
- Rel_Err.Backward.mul x y r >>- fun (x_rel_err , y_rel_err ) ->
- let x = create x_exact x_approx x_abs_err x_rel_err in
- let y = create y_exact y_approx y_abs_err y_rel_err in
- `Value (Some x, Some y)
- | Elt x, Elt y, Elt r, Div ->
- Exact.Backward.div x y r >>- fun (x_exact , y_exact ) ->
- Approx.Backward.div x y r >>- fun (x_approx , y_approx ) ->
- Abs_Err.Backward.div x y r >>- fun (x_abs_err , y_abs_err ) ->
- Rel_Err.Backward.div x y r >>- fun (x_rel_err , y_rel_err ) ->
- let x = create x_exact x_approx x_abs_err x_rel_err in
- let y = create y_exact y_approx y_abs_err y_rel_err in
- `Value (Some x, Some y)
- (* x == y *)
- | _, _, Zero, Ne -> narrow left right >>-: fun t -> Some t, Some t
- (* x < y *)
- | Elt x, Elt y, Zero, Ge ->
- Arith.Backward_Comparisons.lt x y >>-: fun (x, y) ->
- Some (Elt x), Some (Elt y)
- (* x <= y *)
- | Elt x, Elt y, Zero, Gt -> (* x >= y *)
- Arith.Backward_Comparisons.le x y >>-: fun (x, y) ->
- Some (Elt x), Some (Elt y)
- (* x >= y *)
- | Elt x, Elt y, Zero, Lt ->
- Arith.Backward_Comparisons.ge x y >>-: fun (x, y) ->
- Some (Elt x), Some (Elt y)
- (* x > y *)
- | Elt x, Elt y, Zero, Le ->
- Arith.Backward_Comparisons.gt x y >>-: fun (x, y) ->
- Some (Elt x), Some (Elt y)
- | _ -> `Value (None, None)
-
-
-(*-----------------------------------------------------------------------------
- * Operations not handled on Numerors values
- *---------------------------------------------------------------------------*)
-
-let assume_non_zero v = `Unknown v
-let assume_bounded _kind _bound v = `Unknown v
-let assume_not_nan ~assume_finite:_ _fkind v = `Unknown v
-let assume_pointer v = `Unknown v
-let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
-
-let rewrap_integer _ _ = top
-let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
-let resolve_functions _ = `Top, true
-let replace_base _substitution t = t
-
-
-(*-----------------------------------------------------------------------------
- * Built-in to create values in a interval
- *---------------------------------------------------------------------------*)
-let dbetween min max =
- match min, max with
- | Elt min, Elt max ->
- let z = I.zero ~prec:P.Real in
- let f = I.join min.Arith.approx max.Arith.approx in
- let r = I.mul f (I.of_ints ~prec:P.Real (1, 1)) in
- let r = { Arith.exact = r
- ; Arith.approx = f
- ; Arith.abs_err = z
- ; Arith.rel_err = z
- }
- in `Value (Elt r)
- | _, _ -> `Value top
-
-let rbetween min max =
- match min, max with
- | Elt min, Elt max ->
- let approx = I.join min.Arith.approx max.Arith.approx in
- let exact = I.mul approx (I.of_ints ~prec:P.Real (1, 1)) in
- let rel_err = I.epsilon (I.prec min.Arith.approx) in
- let abs_err = I.mul rel_err exact in
- let res = { Arith.exact = exact
- ; Arith.approx = approx
- ; Arith.abs_err = abs_err
- ; Arith.rel_err = rel_err
- }
- in `Value (Elt res)
- | _, _ -> `Value top
-
-
-(*-----------------------------------------------------------------------------
- * Built-in for square root
- *---------------------------------------------------------------------------*)
-let sqrt = function
- | Elt x ->
- let exact = Exact.Forward.sqrt x in
- let approx = Approx.Forward.sqrt x in
- let abs_err = Abs_Err.Forward.sqrt x ~exact ~approx in
- let rel_err = Rel_Err.Forward.sqrt x ~exact ~abs_err in
- `Value (create exact approx abs_err rel_err)
- | _ -> `Value top
-
-
-(*-----------------------------------------------------------------------------
- * Built-in for transcendental functions
- *---------------------------------------------------------------------------*)
-let log = function
- | Elt x ->
- let exact = Exact.Forward.log x in
- let approx = Approx.Forward.log x in
- let abs_err = Abs_Err.Forward.log x ~exact ~approx in
- let rel_err = Rel_Err.Forward.log x ~exact ~abs_err in
- `Value (create exact approx abs_err rel_err)
- | _ -> `Value top
-
-let exp = function
- | Elt x ->
- let exact = Exact.Forward.exp x in
- let approx = Approx.Forward.exp x in
- let abs_err = Abs_Err.Forward.exp x ~exact ~approx in
- let rel_err = Rel_Err.Forward.exp x ~exact ~abs_err in
- `Value (create exact approx abs_err rel_err)
- | _ -> `Value top
-
-let get_max_absolute_error = function
- | Elt x -> Some (snd (I.get_bounds (I.abs (x.Arith.abs_err))))
- | _ -> None
-
-let get_max_relative_error = function
- | Elt x -> Some (snd (I.get_bounds (I.abs (x.Arith.rel_err))))
- | _ -> None
+ (*-----------------------------------------------------------------------------
+ * Built-in for square root
+ *---------------------------------------------------------------------------*)
+ let sqrt = function
+ | Elt x ->
+ let exact = Exact.Forward.sqrt x in
+ let approx = Approx.Forward.sqrt x in
+ let abs_err = Abs_Err.Forward.sqrt x ~exact ~approx in
+ let rel_err = Rel_Err.Forward.sqrt x ~exact ~abs_err in
+ `Value (create exact approx abs_err rel_err)
+ | _ -> `Value top
+
+
+ (*-----------------------------------------------------------------------------
+ * Built-in for transcendental functions
+ *---------------------------------------------------------------------------*)
+ let log = function
+ | Elt x ->
+ let exact = Exact.Forward.log x in
+ let approx = Approx.Forward.log x in
+ let abs_err = Abs_Err.Forward.log x ~exact ~approx in
+ let rel_err = Rel_Err.Forward.log x ~exact ~abs_err in
+ `Value (create exact approx abs_err rel_err)
+ | _ -> `Value top
+
+ let exp = function
+ | Elt x ->
+ let exact = Exact.Forward.exp x in
+ let approx = Approx.Forward.exp x in
+ let abs_err = Abs_Err.Forward.exp x ~exact ~approx in
+ let rel_err = Rel_Err.Forward.exp x ~exact ~abs_err in
+ `Value (create exact approx abs_err rel_err)
+ | _ -> `Value top
+
+ let get_max_absolute_error = function
+ | Elt x -> Some (snd (I.get_bounds (I.abs (x.Arith.abs_err))))
+ | _ -> None
+
+ let get_max_relative_error = function
+ | Elt x -> Some (snd (I.get_bounds (I.abs (x.Arith.rel_err))))
+ | _ -> None
+end
+
+
+let key = Structure.Key_Value.create_key "numerors_values"
+let registered = Abstractions.Value.register { key ; value = (module Value) }
+include Value
diff --git a/src/plugins/eva/domains/numerors/numerors_value.mli b/src/plugins/eva/domains/numerors/numerors_value.mli
index 8d860a502b5a92ef31b5d45afd60d74e036d6b24..bb489ae9797b42c3a5d0811e9a5aeab44ab9e83c 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.mli
+++ b/src/plugins/eva/domains/numerors/numerors_value.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
include Abstract_value.Leaf
+val registered : t Abstractions.Value.registered
val pretty_debug : t Pretty_utils.formatter
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 00adb0b62fdff9fa42f670690688e674271b7a16..c1533364c88daa1d6795fcbae654b169177207e0 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1953,3 +1953,15 @@ module Domain = struct
end
include Domain
+
+let registered =
+ let name = "octagon" and priority = 6 in
+ let descr =
+ "Infers relations between scalar variables of the form b ≤ ±X ± Y ≤ e, \
+ where X, Y are program variables and b, e are constants."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Domain
+ { key ; domain = (module Domain)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
diff --git a/src/plugins/eva/domains/octagons.mli b/src/plugins/eva/domains/octagons.mli
index 2625b8b6b75f0296d68e8cdb9082babcf40cc8d0..9968be3051ef9e9e5adaa30003203acfa8788553 100644
--- a/src/plugins/eva/domains/octagons.mli
+++ b/src/plugins/eva/domains/octagons.mli
@@ -23,3 +23,5 @@
include Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 26aad6c665b306b8e84a9c2d55e5eba8f38fa08d..49f49c3548fd46687442dc2ef19b663eb49924a5 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -224,3 +224,15 @@ module D : Abstract_domain.Leaf
let loc = Precise_locs.imprecise_location location in
kill loc state
end
+
+
+let registered =
+ let name = "bitwise" and priority = 3 in
+ let descr =
+ "Infers bitwise information to interpret more precisely bitwise operators."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Domain
+ { key = D.key ; domain = (module D)
+ ; values = Last Offsm_value.Offsm.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
diff --git a/src/plugins/eva/domains/offsm_domain.mli b/src/plugins/eva/domains/offsm_domain.mli
index 9b69966616999b75f6208ea619504e1f0a25246b..ed4bee0dda7010e6221b57052a540b7f436f44cb 100644
--- a/src/plugins/eva/domains/offsm_domain.mli
+++ b/src/plugins/eva/domains/offsm_domain.mli
@@ -23,3 +23,5 @@
module D : Abstract_domain.Leaf
with type value = Offsm_value.offsm_or_top
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/printer_domain.ml b/src/plugins/eva/domains/printer_domain.ml
index 270925f3ad699eca48fa9607b75ac758a012320f..0e04039aa556fb0a8b6216d4b19d34f15110bbd4 100644
--- a/src/plugins/eva/domains/printer_domain.ml
+++ b/src/plugins/eva/domains/printer_domain.ml
@@ -125,4 +125,19 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
state
end
-include Domain_builder.Complete_Simple_Cvalue (Simple)
+module Domain = Domain_builder.Complete_Simple_Cvalue (Simple)
+include Domain
+
+let registered =
+ let name = "printer" in
+ let priority = 2 in
+ let descr =
+ "Debug domain, only useful for developers. Prints the transfer functions \
+ used during the analysis."
+ in
+ Abstractions.Domain.register ~name ~descr ~priority @@ Domain
+ { key ; domain = (module Domain)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
+
diff --git a/src/plugins/eva/domains/printer_domain.mli b/src/plugins/eva/domains/printer_domain.mli
index c23cfc215f0c44367b4d2d17f0b68f16352ebf7a..2aa295d606ca971fde616646e8ab90559ef68c78 100644
--- a/src/plugins/eva/domains/printer_domain.mli
+++ b/src/plugins/eva/domains/printer_domain.mli
@@ -25,3 +25,5 @@
during an analysis. *)
include Abstract_domain.Leaf with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/sign_domain.ml b/src/plugins/eva/domains/sign_domain.ml
index ab0ce64335e51ca7b7f010faa459f30a07a2cc94..e2f073cb88412dc93fd51a58b0fae5d7edf62cb9 100644
--- a/src/plugins/eva/domains/sign_domain.ml
+++ b/src/plugins/eva/domains/sign_domain.ml
@@ -34,4 +34,15 @@ module Sign_Value = struct
let builtins = []
end
-include Simple_memory.Make_Domain (struct let name = "sign" end) (Sign_Value)
+module Name = struct let name = "sign" end
+module D = Simple_memory.Make_Domain (Name) (Sign_Value)
+include D
+
+let registered =
+ let name = Name.name and priority = 4 in
+ let descr = "Infers the sign of program variables." in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Domain
+ { key ; domain = (module D)
+ ; values = Last Sign_value.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
diff --git a/src/plugins/eva/domains/sign_domain.mli b/src/plugins/eva/domains/sign_domain.mli
index e8d8622c30a537200663fd9190a61f77582cf456..b5d5dfcd333eb039b8bb5dc9bd558c424b766d92 100644
--- a/src/plugins/eva/domains/sign_domain.mli
+++ b/src/plugins/eva/domains/sign_domain.mli
@@ -24,3 +24,5 @@
include Abstract_domain.Leaf with type value = Sign_value.t
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 8dd06c85fa33a88e13d6daed4daddeee7173870f..319966cb259b3fe0488773d8df4ba298e356fc12 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -637,3 +637,17 @@ module D : Abstract_domain.Leaf
let loc = Precise_locs.imprecise_location location in
Memory.kill loc state
end
+
+
+
+let registered =
+ let name = "symbolic-locations" and priority = 7 in
+ let descr =
+ "Infers values of symbolic locations represented by imprecise lvalues, \
+ such as t[i] or *p when the possible values of [i] or [p] are imprecise."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr @@ Domain
+ { key = D.key ; domain = (module D)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
diff --git a/src/plugins/eva/domains/symbolic_locs.mli b/src/plugins/eva/domains/symbolic_locs.mli
index dba5b5878f7b7b7aaf2bc76f1a7b0e28b120fd0d..0c7e8d5f52f3dc6210d777456e327fe5c84c6170 100644
--- a/src/plugins/eva/domains/symbolic_locs.mli
+++ b/src/plugins/eva/domains/symbolic_locs.mli
@@ -26,3 +26,5 @@
module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index 6abf186ae3fd6e7b52aa9c261fb0cabfa20b769f..a5ed670f5cd7464c64dcb0546a79a3849a40149d 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -582,17 +582,18 @@ let interpret_taint_logic
end)
(* Registers the domain. *)
-let flag =
+let registered =
let name = "taint"
and descr = "Taint analysis"
and experimental = true
- and abstraction =
- Abstractions.{ values = Single (module Main_values.CVal);
- domain = Domain (module TaintDomain); }
in
- Abstractions.register ~name ~descr ~experimental abstraction
+ Abstractions.Domain.register ~name ~descr ~experimental @@ Domain
+ { key = TaintDomain.key ; domain = (module TaintDomain)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
-let () = Abstractions.register_hook interpret_taint_logic
+let () = Abstractions.Hooks.register interpret_taint_logic
type taint = Direct | Indirect | Untainted
diff --git a/src/plugins/eva/domains/taint_domain.mli b/src/plugins/eva/domains/taint_domain.mli
index fa31e885b038f02c351fa5b87c073a8b4e5b8c44..2b26fa23af604b9eeb6ce7ff3274a226beee2957 100644
--- a/src/plugins/eva/domains/taint_domain.mli
+++ b/src/plugins/eva/domains/taint_domain.mli
@@ -26,7 +26,7 @@ include Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
-val flag: Abstractions.flag
+val registered: Abstractions.Domain.registered
type taint = | Direct | Indirect | Untainted
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index 396d0cfca6bc06b4a58a60255cb599cc4b1f58eb..e759bbfd3259161b7d79f3a27b0739df65c241b4 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1260,6 +1260,16 @@ module D = struct
then project_of_cfg return_exp state
end
+let registered =
+ let name = "traces" and priority = 2 and experimental = true in
+ let descr =
+ "Builds an over-approximation of all the traces that lead to a statement."
+ in
+ Abstractions.Domain.register ~name ~priority ~descr ~experimental @@ Domain
+ { key = D.key ; domain = (module D)
+ ; values = Last Main_values.CVal.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
(*
Local Variables:
diff --git a/src/plugins/eva/domains/traces_domain.mli b/src/plugins/eva/domains/traces_domain.mli
index 7e13fe9d4212dcdf761de59c8329580c06090f56..6c05df34c29aa6ed9c385bba763238016d4fb7d4 100644
--- a/src/plugins/eva/domains/traces_domain.mli
+++ b/src/plugins/eva/domains/traces_domain.mli
@@ -76,3 +76,5 @@ module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
and type state = state
+
+val registered : Abstractions.Domain.registered
diff --git a/src/plugins/eva/engine/abstractions.ml b/src/plugins/eva/engine/abstractions.ml
index 573457ba34d0d5877b5bc14e9c3250c314e523c7..f1e303a997477f45319baa16127df886550e2702 100644
--- a/src/plugins/eva/engine/abstractions.ml
+++ b/src/plugins/eva/engine/abstractions.ml
@@ -20,527 +20,786 @@
(* *)
(**************************************************************************)
-(* --- Registration types --------------------------------------------------- *)
-type 'v value =
- | Single of (module Abstract_value.Leaf with type t = 'v)
- | Struct of 'v Abstract.Value.structure
-type precise_loc = Precise_locs.precise_location
-
-module type leaf_domain = Abstract_domain.Leaf with type location = precise_loc
-
-module type domain_functor =
- functor (Value: Abstract.Value.External) ->
- (leaf_domain with type value = Value.t)
-
-type 'v domain =
- | Domain: (module leaf_domain with type value = 'v) -> 'v domain
- | Functor: (module domain_functor) -> _ domain
+(* --- Values abstraction --------------------------------------------------- *)
+
+module Value = struct
+ type 'v structure = 'v Abstract.Value.structure
+ type 'v key = 'v Abstract.Value.key
+ let dec_eq = Abstract.Value.eq_structure
+
+ type 'v value = (module Abstract_value.S with type t = 'v)
+
+
+ (* Value registration *)
+ type 'v register = { key : 'v key ; value : 'v value }
+ type 'v registered = 'v key * 'v value
+ let register : type v. v register -> v registered =
+ fun { key ; value } -> (key, value)
+
+
+ (* When registering a location or a domain, the user has to declare its
+ values dependencies, i.e the values it uses during its computations. To
+ simplify the abstraction build and the dependencies declaration, they
+ are handled as a simple list. Arguably not so simple as it is
+ heterogenous, but it is still a list. *)
+ type 'v dependencies =
+ | Last : 'v registered -> 'v dependencies
+ | (::) : 'a registered * 'b dependencies -> ('a * 'b) dependencies
+
+ (* When building the abstraction, we will need to compare the dependencies
+ structure with the structured values. *)
+ let rec outline : type v. v dependencies -> v structure = function
+ | Last (key, value) -> Abstract.Value.Leaf (key, value)
+ | (k, v) :: tl -> Abstract.Value.(Node (Leaf (k, v), outline tl))
+
+ (* Folding over values dependencies *)
+ type 'a folder = { folder : 'v. 'v registered -> 'a -> 'a }
+ let rec fold : type v. 'a folder -> v dependencies -> 'a -> 'a =
+ fun { folder } dependencies acc ->
+ match dependencies with
+ | Last registered -> folder registered acc
+ | hd :: tl -> fold { folder } tl (folder hd acc)
+
+
+ (* The value abstraction build consists of accumulating registered values
+ into a structured value and then adding the needed operators, thus making
+ it interactive. A [Unit] structured abstraction is used for the initial
+ state and is discarded as soon as a real value abstraction is added. *)
+ module type Structured = Abstract.Value.Internal
+ module type Interactive = Abstract.Value.External
+ type 'a or_unit = Unit | Value of 'a
+ type structured = (module Structured) or_unit
+ type interactive = (module Interactive) or_unit
+
+ (* Making a structured value interactive simply consists of adding the
+ needed operations using the Structure.Open functor.*)
+ let make_interactive : structured -> interactive = function
+ | Unit -> Unit
+ | Value (module Structured) ->
+ Value (module struct
+ include Structured
+ include Structure.Open (Abstract.Value) (Structured)
+ end)
-type 'v abstraction =
- { values: 'v value;
- domain: 'v domain; }
+ (* Adding a registered value into a structured one consists of deciding if
+ a product is needed (which comes down to checking if the registered
+ value key we want to add is not in the structure), computing it, and
+ updating the structure. *)
+ let add : type v. v registered -> structured -> structured =
+ fun (key, input) structured ->
+ let open Abstract.Value in
+ match make_interactive structured with
+ | Unit ->
+ Value (module struct
+ include (val input)
+ let structure = Leaf (key, input)
+ end)
+ | Value (module Interactive) when not (Interactive.mem key) ->
+ Value (module struct
+ include Value_product.Make (Interactive) (val input)
+ let structure = Node (Interactive.structure, Leaf (key, input))
+ end)
+ | _ -> structured
+
+ (* The minimal value abstraction to use. *)
+ let init : structured = Unit
+
+ (* During the complete abstraction build, we need to verify that there is at
+ least one value in the computed abstraction.
+ TODO: better error handling. *)
+ let assert_not_unit = function
+ | Unit -> Self.fatal "The built value cannot be unit."
+ | Value interactive -> interactive
+
+
+ (* When building the complete abstraction, we need to trick locations and
+ domains into thinking that their value dependencies are there, even if
+ the structured value type is not the good one. This is done through a
+ lift that requires conversion operations to interact with the subpart
+ of the structured value that matters for the location or the domain.
+ This functor is responsible of building such conversion operations. *)
+ module type From = sig type value val structure : value structure end
+ module Converter (From : From) (To : Interactive) = struct
+ type extended = To.t
+ let structure = From.structure
+
+ let void_value () =
+ Self.fatal "Cannot register a value module from a Void structure."
+
+ let rec set : type v. v structure -> v -> extended -> extended = function
+ | Leaf (key, _) -> To.set key
+ | Node (s1, s2) -> fun (v1, v2) ext -> set s2 v2 ext |> set s1 v1
+ | Option (s, default) -> fun v -> set s (Option.value ~default v)
+ | Unit -> fun () value -> value
+ | Void -> void_value ()
+
+ let rec get : type v. v structure -> extended -> v = function
+ | Leaf (key, _) -> Option.get (To.get key)
+ | Node (s1, s2) -> fun v -> get s1 v, get s2 v
+ | Option (s, _) -> fun v -> Some (get s v)
+ | Unit -> fun _ -> ()
+ | Void -> void_value ()
+
+ let replace = set structure
+ let extend v = replace v To.top
+ let restrict = get structure
+ end
+end
-type 't with_info =
- { name: string;
- experimental: bool;
- priority: int;
- abstraction: 't; }
-type flag = Flag: 'v abstraction with_info -> flag
-(* --- Config and registration ---------------------------------------------- *)
+(* --- Locations abstraction ------------------------------------------------ *)
-module Config = struct
- module OptMode = Datatype.Option (Domain_mode)
- module Element = struct
- type t = flag * Domain_mode.t option
-
- (* Flags are sorted by increasing priority order, and then by name. *)
- let compare (Flag f1, mode1) (Flag f2, mode2) =
- let c = Datatype.Int.compare f1.priority f2.priority in
- if c <> 0 then c else
- let c = Datatype.String.compare f1.name f2.name in
- if c <> 0 then c else
- OptMode.compare mode1 mode2
- end
+module Location = struct
+ type 'l structure = 'l Abstract.Location.structure
+ type 'l key = 'l Abstract.Location.key
+ let dec_eq = Abstract.Location.eq_structure
- include Set.Make (Element)
+ type ('v, 'l) location =
+ (module Abstract_location.S with type value = 'v and type location = 'l)
- let mem (Flag domain) =
- exists (fun (Flag flag, _mode) -> flag.name = domain.name)
- let abstractions = ref []
- let dynamic_abstractions = ref []
+ (* When registering a location, we also need its key and its values
+ dependencies. *)
+ type ('v, 'l) register =
+ { key: 'l key
+ ; location : ('v, 'l) location
+ ; dependencies : 'v Value.dependencies
+ }
- let register_domain_option ~name ~experimental ~descr =
- let descr = if experimental then "Experimental. " ^ descr else descr in
- Parameters.register_domain ~name ~descr
+ (* A registered location is simply a location with its key and its values
+ dependencies. *)
+ module type Registered = sig
+ include Abstract_location.S
+ val key : location key
+ val structure : location structure
+ val dependencies : value Value.dependencies
+ end
+ type 'l registered = (module Registered with type location = 'l)
- let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
- register_domain_option ~name ~experimental ~descr;
- let flag = Flag { name; experimental; priority; abstraction } in
- abstractions := flag :: !abstractions;
- flag
+ (* Location registration. *)
+ let register : type v l. (v, l) register -> l registered =
+ fun { key ; location ; dependencies } ->
+ (module struct
+ module Location = (val location)
+ include Location
+ let key = key
+ let structure = Abstract.Location.Leaf (key, (module Location))
+ let dependencies = dependencies
+ end)
+
+
+ (* When registering a domain, the user has to declare its locations
+ dependencies, i.e the locations it uses during its computations. As
+ for the values, they are handled as a simple heterogenous list. *)
+ type 'l dependencies =
+ | Last : 'l registered -> 'l dependencies
+ | (::) : 'a registered * 'b dependencies -> ('a * 'b) dependencies
+
+ (* When building the abstraction, we will need to compare dependencies
+ with the structured locations. *)
+ let rec outline : type l. l dependencies -> l structure = function
+ | Last (module R) -> R.structure
+ | (module R) :: tl -> Abstract.Location.Node (R.structure, outline tl)
+
+ (* Folding over locations dependencies *)
+ type 'a folder = { folder : 'v. 'v registered -> 'a -> 'a }
+ let rec fold : type v. 'a folder -> v dependencies -> 'a -> 'a =
+ fun { folder } dependencies acc ->
+ match dependencies with
+ | Last registered -> folder registered acc
+ | hd :: tl -> fold { folder } tl (folder hd acc)
+
+ (* Folding over the values dependencies of some locations dependencies. *)
+ let rec fold_values : type v. 'a Value.folder -> v dependencies -> 'a -> 'a =
+ fun folder dependencies acc ->
+ match dependencies with
+ | Last (module R) -> Value.fold folder R.dependencies acc
+ | (module R) :: tl ->
+ fold_values folder tl (Value.fold folder R.dependencies acc)
+
+
+ (* As for the value abstraction, building the location abstraction consists
+ of structuring the needed registered locations and then adding the needed
+ operators to make it interactive. However, a structured location is not
+ as simple as a structured value, as it needs to keep track of the value
+ abstraction it is based on. This value is supposed to be the complete
+ aggregation of all the values that are needed by the requested domains. *)
+ module type Structured = sig
+ type value
+ module Value : Value.Interactive with type t = value
+ module Location : Abstract.Location.Internal with type value = value
+ end
- let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make =
- register_domain_option ~name ~experimental ~descr;
- let make' () : flag =
- Flag { name; experimental; priority; abstraction = make () }
- in
- dynamic_abstractions := (name,make') :: !dynamic_abstractions
+ module type Interactive = Abstract.Location.External
+
+ (* We expose the type of the structured value we are based on to statically
+ ensure that we do not temper with it. As for the value abstractions, a
+ [Unit] structured abstraction is used for the initial state and is
+ discarded as soon as a location is added. *)
+ type ('u, 'l) or_unit = Unit of 'u | Location of 'l
+ type 'v value = (module Value.Interactive with type t = 'v)
+ type 'v structured_module = (module Structured with type value = 'v)
+ type 'v structured = ('v value, 'v structured_module) or_unit
+ type 'v interactive_module = (module Interactive with type value = 'v)
+ type 'v interactive = ('v value, 'v interactive_module) or_unit
+
+ (* Initial location builder *)
+ let init (value : 'v value) : 'v structured = Unit value
+
+ (* During the complete abstraction build, we need to verify that there is at
+ least one location in the computed abstraction.
+ TODO: better error handling. *)
+ let assert_not_unit = function
+ | Unit _ -> Self.fatal "The built location cannot be unit."
+ | Location interactive -> interactive
+
+
+ (* Making a structured value interactive simply consists of adding the
+ needed operations using the Structure.Open functor.*)
+ let make_interactive : type v. v structured -> v interactive = function
+ | Unit value -> Unit value
+ | Location (module Structured) ->
+ Location (module struct
+ include Structured.Location
+ include Structure.Open (Abstract.Location) (struct
+ include Structured.Location
+ type t = location
+ end)
+ end)
- let configure () =
- let add_main_mode mode =
- let main, _ = Globals.entry_point () in
- (main, Domain_mode.Mode.all) :: mode
- in
- let add config (name, make) =
- let enabled = Parameters.Domains.mem name in
- try
- let mode = Parameters.DomainsFunction.find name in
- let mode = if enabled then add_main_mode mode else mode in
- add (make (), Some mode) config
- with Not_found ->
- if enabled then add (make (), None) config else config
- in
- let aux config (Flag domain as flag) =
- add config (domain.name, (fun () -> flag))
+ (* Retrieves the value contained in a structured location. *)
+ let get_value : type v. v structured -> v value = function
+ | Unit value -> value
+ | Location (module S) -> (module S.Value)
+
+
+ (* Adding a registered location into a structured one is done in three steps:
+ 1. Lifting the location abstraction we want to add to match the value
+ abstraction contained in the structured abstraction.
+ 2. Combine the given location abstraction with the one contained in the
+ structured abstraction. It comes down to decide if a reduced product is
+ needed.
+ 3. Rebuild a structured abstraction with the new location abstraction. *)
+ let add : type v l. l registered -> v structured -> v structured =
+ fun (module Registered) structured ->
+ let deps = Value.outline Registered.dependencies in
+ let module To = (val get_value structured) in
+ let module From = struct include Registered let structure = deps end in
+ let module Converter = Value.Converter (From) (To) in
+ let lifted : (module Abstract.Location.Internal with type value = v) =
+ match Value.dec_eq deps To.structure with
+ | Some Eq -> (module Registered)
+ | None -> (module Location_lift.Make (Registered) (Converter))
in
- let config = List.fold_left aux empty !abstractions in
- List.fold_left add config !dynamic_abstractions
-
- (* --- Register default abstractions -------------------------------------- *)
-
- let create_domain ?experimental priority name descr values domain =
- let abstraction = { values = Single values; domain = Domain domain } in
- register ~name ~descr ~priority ?experimental abstraction
-
- (* Register standard domains over cvalues. *)
- let make ?experimental rank name descr =
- create_domain ?experimental rank name descr (module Main_values.CVal)
-
- let cvalue =
- make 9 "cvalue"
- "Main analysis domain, enabled by default. Should not be disabled."
- (module Cvalue_domain.State)
-
- let symbolic_locations =
- make 7 "symbolic-locations"
- "Infers values of symbolic locations represented by imprecise lvalues, \
- such as t[i] or *p when the possible values of [i] or [p] are imprecise."
- (module Symbolic_locs.D)
-
- let equality =
- let descr = "Infers equalities between syntactic C expressions. \
- Makes the analysis less dependent on temporary variables and \
- intermediate computations."
- and abstraction =
- { values = Struct Abstract.Value.Unit;
- domain = Functor (module Equality_domain.Make); }
+ let combined : (module Abstract.Location.Internal with type value = v) =
+ match make_interactive structured with
+ | Unit _ -> lifted
+ | Location (module Loc) when Loc.mem Registered.key -> (module Loc)
+ | Location (module Loc) ->
+ (module Locations_product.Make (To) (val lifted) (Loc))
in
- register ~name:"equality" ~descr ~priority:8 abstraction
-
- let gauges =
- make 6 "gauges"
- "Infers linear inequalities between the variables modified within a loop \
- and a special loop counter."
- (module Gauges_domain.D)
-
- let octagon =
- make 6 "octagon"
- "Infers relations between scalar variables of the form b ≤ ±X ± Y ≤ e, \
- where X, Y are program variables and b, e are constants."
- (module Octagons)
-
- let bitwise =
- create_domain 3 "bitwise"
- "Infers bitwise information to interpret more precisely bitwise operators."
- (module Offsm_value.Offsm) (module Offsm_domain.D)
-
- let sign =
- create_domain 4 "sign"
- "Infers the sign of program variables."
- (module Sign_value) (module Sign_domain)
-
- let inout = make 5 "inout" ~experimental:true
- "Infers the inputs and outputs of each function."
- (module Inout_domain.D)
-
- let traces =
- make 2 "traces" ~experimental:true
- "Builds an over-approximation of all the traces that lead \
- to a statement."
- (module Traces_domain.D)
-
- let printer =
- make 2 "printer"
- "Debug domain, only useful for developers. Prints the transfer functions \
- used during the analysis."
- (module Printer_domain)
-
- (* --- Default and legacy configurations ---------------------------------- *)
-
- let default = configure ()
- let legacy = singleton (cvalue, None)
+ Location (module struct
+ type value = v
+ module Value = To
+ module Location = (val combined)
+ end)
+
+
+ (* When building the complete abstraction, we need to trick domains into
+ thinking that their locations dependencies are there, even if the
+ structured location type is not the good one. This is done through a
+ lift that requires conversion operations to interact with the subpart
+ of the structured location that matters for the domains. This functor is
+ responsible of building such conversion operations. *)
+ module type From = sig type location val structure : location structure end
+ module Converter (From : From) (To : Interactive) = struct
+ type extended = To.location
+ let structure = From.structure
+
+ let void_location () =
+ Self.fatal "Cannot register a location module from a Void structure."
+
+ let rec set : type l. l structure -> l -> extended -> extended = function
+ | Leaf (key, _) -> To.set key
+ | Node (s1, s2) -> fun (l1, l2) ext -> set s2 l2 ext |> set s1 l1
+ | Option (s, default) -> fun l -> set s (Option.value ~default l)
+ | Unit -> fun () loc -> loc
+ | Void -> void_location ()
+
+ let rec get : type l. l structure -> extended -> l = function
+ | Leaf (key, _) -> Option.get (To.get key)
+ | Node (s1, s2) -> fun l -> get s1 l, get s2 l
+ | Option (s, _) -> fun l -> Some (get s l)
+ | Unit -> fun _ -> ()
+ | Void -> void_location ()
+
+ let replace = set structure
+ let extend l = replace l To.top
+ let restrict = get structure
+ end
end
-let register = Config.register
-let dynamic_register = Config.dynamic_register
-(* --- Building value abstractions ------------------------------------------ *)
-module Leaf_Value (V: Abstract_value.Leaf) = struct
- include V
- let structure = Abstract.Value.Leaf (V.key, (module V))
-end
+(* --- Domains abstraction -------------------------------------------------- *)
-module Leaf_Location (Loc: Abstract_location.Leaf) = struct
- include Loc
- let structure = Abstract.Location.Leaf (Loc.key, (module Loc))
-end
+module Domain = struct
+ type 's structure = 's Abstract.Domain.structure
+ type 's key = 's Abstract.Domain.key
+ module type S = Abstract_domain.S
-module Leaf_Domain (D: Abstract_domain.Leaf) = struct
- include D
- let structure = Abstract.Domain.Leaf (D.key, (module D))
-end
-module type Acc = sig
- module Val : Abstract.Value.External
- module Loc : Abstract.Location.Internal with type value = Val.t
- and type location = precise_loc
- module Dom : Abstract.Domain.Internal with type value = Val.t
- and type location = Loc.location
-end
+ (* Registration of leaf domains, i.e simple domain with a fixed value. *)
+ module Leaf = struct
+ type ('v, 'l, 's) domain =
+ (module S with type value = 'v and type location = 'l and type state = 's)
+
+ (* We need the values and locations dependendies to register a domain. *)
+ type ('v, 'l, 's) register =
+ { key : 's key
+ ; domain : ('v, 'l, 's) domain
+ ; values : 'v Value.dependencies
+ ; locations : 'l Location.dependencies
+ }
-module Internal_Value = struct
- open Abstract.Value
+ (* As for the locations, a registered domain is a simple module that
+ contains all the information given during the register along with
+ the domain structure (which is a leaf). *)
+ module type Registered = sig
+ include Abstract_domain.S
+ val key : state key
+ val structure : state structure
+ val values : value Value.dependencies
+ val locations : location Location.dependencies
+ end
- type value_key_module = V : 'v key * 'v data -> value_key_module
+ (* Registration procedure. *)
+ type 's registered = (module Registered with type state = 's)
+ let register : type v l s. (v, l, s) register -> s registered =
+ fun { key ; domain ; values ; locations } ->
+ (module struct
+ module Domain = (val domain)
+ include Domain
+ let key = key
+ let structure = Abstract.Domain.Leaf (key, (module Domain))
+ let values = values
+ let locations = locations
+ end)
+ end
- let open_value_abstraction (module Value : Internal) =
- (module struct
- include Value
- include Structure.Open (Abstract.Value) (Value)
- end : Abstract.Value.External)
- let add_value_leaf value (V (key, v)) =
- let module Value = (val open_value_abstraction value) in
- if Value.mem key then value else
+ (* Registration of a functor domain, i.e a domain that can be built on top of
+ any value. *)
+ module Functor = struct
+
+ (* A functor domain is declared as an existantiel. This module type has to
+ be read as: there exists a type <location> such as, given any Value, we
+ can build a domain using this Value and relying on a Location of type
+ <location>. *)
+ module type Domain = sig
+ type location
+ module Make (V : Value.Interactive) : sig
+ include Abstract_domain.S
+ with type value = V.t
+ and type location = location
+ val key : state key
+ end
+ end
+ type 'l domain = (module Domain with type location = 'l)
+
+ (* As a functor domain can be instanciated for any value, we only need
+ locations dependencies to register it. *)
+ type 'l register =
+ { domain : 'l domain
+ ; locations : 'l Location.dependencies
+ }
+
+ (* Once registered, a functor domain builds a domain along with its
+ structure and its key. *)
+ module type RegisteredLeaf = sig
+ include Abstract.Domain.Internal
+ val key : state key
+ end
+
+ (* A registered functor domain contains its locations dependencies and a
+ functor that builds a domain along its structure and its key. *)
+ module type Registered = sig
+ type location
+ val locations : location Location.dependencies
+ module Make (V : Value.Interactive) :
+ RegisteredLeaf with type value = V.t and type location = location
+ end
+
+ (* Registration procedure. *)
+ type registered = (module Registered)
+ let register : type l. l register -> registered =
+ fun { domain ; locations } ->
+ let module Domain = (val domain) in
(module struct
- include Value_product.Make (Value) (val v)
- let structure = Node (Value.structure, Leaf (key, v))
+ type location = Domain.location
+ let locations = locations
+ module Make (V : Value.Interactive) = struct
+ module Result = Domain.Make (V)
+ include Result
+ let structure = Abstract.Domain.Leaf (key, (module Result))
+ end
end)
+ end
- let void_value () =
- Self.fatal
- "Cannot register a value module from a Void structure."
-
- let add_value_structure value internal =
- let rec aux: type v. (module Internal) -> v structure -> (module Internal) =
- fun value -> function
- | Option (s, _) -> aux value s
- | Leaf (key, v) -> add_value_leaf value (V (key, v))
- | Node (s1, s2) -> aux (aux value s1) s2
- | Unit -> value
- | Void -> void_value ()
- in
- aux value internal
- let build_values config initial_value =
- let build (Flag flag, _) acc =
- match flag.abstraction.values with
- | Struct structure -> add_value_structure acc structure
- | Single (module V) -> add_value_leaf acc (V (V.key, (module V)))
- in
- let value = Config.fold build config initial_value in
- open_value_abstraction value
-
-
- module Convert
- (Value: Abstract.Value.External)
- (Struct: sig type v val s : v value end)
- = struct
-
- let structure = match Struct.s with
- | Single (module V) -> Abstract.Value.Leaf (V.key, (module V))
- | Struct s -> s
-
- type extended_value = Value.t
-
- let replace_val =
- let rec set: type v. v structure -> v -> Value.t -> Value.t =
- function
- | Leaf (key, _) -> Value.set key
- | Node (s1, s2) ->
- let set1 = set s1 and set2 = set s2 in
- fun (v1, v2) value -> set1 v1 (set2 v2 value)
- | Option (s, default) -> fun v -> set s (Option.value ~default:default v)
- | Unit -> fun () value -> value
- | Void -> void_value ()
- in
- set structure
-
- let extend_val v = replace_val v Value.top
-
- let restrict_val =
- let rec get: type v. v structure -> Value.t -> v = function
- | Leaf (key, _) -> Option.get (Value.get key)
- | Node (s1, s2) ->
- let get1 = get s1 and get2 = get s2 in
- fun v -> get1 v, get2 v
- | Option (s, _) -> fun v -> Some (get s v)
- | Unit -> fun _ -> ()
- | Void -> void_value ()
- in
- get structure
+ (* To simplify the domain registration procedure, we provide common types.
+ However, the code above is still useful to prove some properties, mainly
+ that we do not temper with the dependencies. *)
+ type register =
+ | Domain : ('v, 'l, 's) Leaf.register -> register
+ | Functor : 'l Functor.register -> register
+
+ type registered =
+ | RegisteredDomain : 's Leaf.registered -> registered
+ | RegisteredFunctor : Functor.registered -> registered
+
+ (* Registered domain are saved in mutable lists along with there information,
+ i.e. there name, there experimental and there priority flags. *)
+ type 't with_info =
+ { name : string
+ ; experimental : bool
+ ; priority : int
+ ; abstraction : 't
+ }
- type extended_location = Main_locations.PLoc.location
+ (* The configuration of an analysis contains a set of domains along with their
+ mode. *)
+ type 't with_mode = 't * Domain_mode.t option
- let restrict_loc = fun x -> x
- let extend_loc = fun x -> x
+
+ (* Mutable lists containing statically and dynamically registered domains. *)
+ let static_domains = ref []
+ let dynamic_domains = ref []
+
+ (* Helper function used to register the parameters of a domain. *)
+ let register_domain_option ~name ~experimental ~descr =
+ let descr = if experimental then "Experimental. " ^ descr else descr in
+ Parameters.register_domain ~name ~descr
+
+ (* Helper function used to dispatch the registration process to the good
+ registration process depending of the domain kind. *)
+ let register_abstraction = function
+ | Domain register -> RegisteredDomain (Leaf.register register)
+ | Functor register -> RegisteredFunctor (Functor.register register)
+
+ (* Registration of a static domain. *)
+ let register ~name ~descr ?(experimental=false) ?(priority=0) register =
+ register_domain_option ~name ~descr ~experimental ;
+ let abstraction = register_abstraction register in
+ let registered = { name ; experimental ; priority ; abstraction } in
+ static_domains := registered :: !static_domains ;
+ abstraction
+
+ (* Registration of a dynamic domain. *)
+ let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make =
+ register_domain_option ~name ~descr ~experimental ;
+ let make () = make () |> register_abstraction in
+ let make () = { name ; experimental ; priority ; abstraction = make () } in
+ dynamic_domains := (name, make) :: !dynamic_domains
+
+
+ (* Building the domain abstraction consists of structuring the requested
+ registered domains. To do so, we need to keep track of the values and
+ locations abstraction on which the structured domain will rely. Those
+ abstractions are supposed to be the complete aggregations of all the
+ values (resp locations) that are needed by the requested domains. *)
+ module type Structured = sig
+ type value
+ type location
+ module Value : Value.Interactive with type t = value
+ module Location : Location.Interactive
+ with type value = value and type location = location
+ module Domain : Abstract.Domain.Internal
+ with type value = value and type location = location
end
-end
-(* --- Building domain abstractions ----------------------------------------- *)
-
-module type internal_loc =
- Abstract.Location.Internal with type location = precise_loc
-module type internal_domain =
- Abstract.Domain.Internal with type location = precise_loc
-
-let eq_value:
- type a b. a Abstract.Value.structure -> b value -> (a,b) Structure.eq option
- = fun structure -> function
- | Struct s -> Abstract.Value.eq_structure structure s
- | Single (module V) ->
- match structure with
- | Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
- | _ -> None
-
-let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc) =
- let domain : (module internal_domain with type value = Acc.Val.t) =
- match abstraction.domain with
- | Functor make ->
- let module Make = (val make: domain_functor) in
- (module Leaf_Domain (Make (Acc.Val)))
- | Domain domain ->
- match eq_value Acc.Val.structure abstraction.values with
- | Some Structure.Eq ->
- let module Domain = (val domain) in
- (module Leaf_Domain (Domain))
- | None ->
- let module Domain = (val domain : leaf_domain with type value = v) in
- let module Struct = struct
- type v = Domain.value
- let s = abstraction.values
- end in
- let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
- (module Domain_lift.Make (Domain) (Convert))
- in
- (* Set the name of the domain. *)
- let module Domain = struct
- include (val domain)
- module Store = struct
- include Store
- let register_global_state storage state =
- let no_results = Parameters.NoResultsDomains.mem dname in
- register_global_state (storage && not no_results) state
- end
- end in
- (* Restricts the domain according to [mode]. *)
- let domain : (module internal_domain with type value = Acc.Val.t) =
- match mode with
- | None -> (module Domain)
- | Some kf_modes ->
- let module Scope = struct let functions = kf_modes end in
- let module Domain =
- Domain_builder.Restrict
- (Acc.Val)
- (Domain)
- (Scope)
+ (* As for the value and location abstractions, a [Unit] structured domain is
+ used for the initial state. *)
+ type ('v, 'l, 's) or_unit = Unit of 'v * 'l | State of 's
+ type 'v value = (module Value.Interactive with type t = 'v)
+ type ('v, 'l) location =
+ (module Location.Interactive with type value = 'v and type location = 'l)
+ type ('v, 'l) structured_module =
+ (module Structured with type value = 'v and type location = 'l)
+ type ('v, 'l) structured =
+ ('v value, ('v, 'l) location, ('v, 'l) structured_module) or_unit
+
+ (* Recovers the value and location abstractions of a structured domain. *)
+ let get : type v l. (v, l) structured -> v value * (v, l) location = function
+ | Unit (value, location) -> (value, location)
+ | State (module S) -> ((module S.Value), (module S.Location))
+
+ (* During the complete abstraction build, we need to verify that there is at
+ least one domain in the computed abstraction.
+ TODO: better error handling. *)
+ let assert_not_unit = function
+ | Unit _ -> Self.fatal "The built domain cannot be unit."
+ | State structured -> structured
+
+
+ (* Internal type used for intermediate results of the add procedure. *)
+ type ('v, 'l) structured_domain =
+ (module Abstract.Domain.Internal with type value = 'v and type location = 'l)
+
+ (* Utility function used to create an identity converter. *)
+ module type Typ = sig type t end
+ let conversion_id (type t) (module T: Typ with type t = t) =
+ (module struct
+ type extended = T.t
+ type internal = T.t
+ let extend x = x
+ let restrict x = x
+ end: Domain_lift.Conversion with type extended = t and type internal = t)
+
+ (* Adding a registered domain into a structured one consists of performing a
+ lifting of the registered one if needed before performing the product,
+ configuring the name and restricting the domain depending of the mode. *)
+ type add_input = registered with_info with_mode
+ let add : type v l. add_input -> (v, l) structured -> (v, l) structured =
+ fun (registered, mode) structured ->
+ let wkey = Self.wkey_experimental in
+ let { experimental = exp ; name } = registered in
+ if exp then Self.warning ~wkey "The %s domain is experimental." name ;
+ let value, location = get structured in
+ let module Val = (val value) in
+ let module Loc = (val location) in
+ let lifted : (v, l) structured_domain =
+ match registered.abstraction with
+ | RegisteredFunctor (module Functor) ->
+ let locs = Location.outline Functor.locations in
+ let eq_loc = Location.dec_eq locs Loc.structure in
+ let module D = Functor.Make (Val) in
+ begin match eq_loc with
+ | Some Eq -> (module D)
+ | None ->
+ let module Val = (val conversion_id (module Val)) in
+ let module From = struct include D let structure = locs end in
+ let module Loc = Location.Converter (From) (Loc) in
+ (module Domain_lift.Make (D) (Val) (Loc))
+ end
+ | RegisteredDomain (module D) ->
+ let loc_deps = Location.outline D.locations in
+ let val_deps = Value.outline D.values in
+ let eq_loc = Location.dec_eq loc_deps Loc.structure in
+ let eq_val = Value.dec_eq val_deps Val.structure in
+ begin match eq_val, eq_loc with
+ | Some Eq, Some Eq -> (module D)
+ | Some Eq, None ->
+ let module Val = (val conversion_id (module Val)) in
+ let module From = struct include D let structure = loc_deps end in
+ let module Loc = Location.Converter (From) (Loc) in
+ (module Domain_lift.Make (D) (Val) (Loc))
+ | None, Some Eq ->
+ let module From = struct include D let structure = val_deps end in
+ let module Val = Value.Converter (From) (Val) in
+ let module LocTyp = struct type t = Loc.location end in
+ let module Loc = (val conversion_id (module LocTyp)) in
+ (module Domain_lift.Make (D) (Val) (Loc))
+ | _, _ ->
+ let module From = struct include D let structure = val_deps end in
+ let module Val = Value.Converter (From) (Val) in
+ let module From = struct include D let structure = loc_deps end in
+ let module Loc = Location.Converter (From) (Loc) in
+ (module Domain_lift.Make (D) (Val) (Loc))
+ end
+ in
+ (* Set the name of the domain. *)
+ let module Named = struct
+ include (val lifted)
+ module Store = struct
+ include Store
+ let register_global_state storage state =
+ let no_results = Parameters.NoResultsDomains.mem registered.name in
+ register_global_state (storage && not no_results) state
+ end
+ end in
+ (* Restricts the domain according to [mode]. *)
+ let restricted : (v, l) structured_domain =
+ match mode with
+ | None -> (module Named)
+ | Some kf_modes ->
+ let module Scope = struct let functions = kf_modes end in
+ (module Domain_builder.Restrict (Val) (Named) (Scope))
+ in
+ let combined : (v, l) structured_domain =
+ match structured with
+ | Unit _ -> restricted
+ | State (module Structured) ->
+ (* The new [domain] becomes the left leaf of the domain product, and
+ will be processed before the domains from [Acc.Dom] during the
+ analysis. *)
+ let module Dom = Structured.Domain in
+ (module Domain_product.Make (Val) (val restricted) (Dom))
+ in
+ State (module struct
+ type value = v
+ type location = l
+ module Value = Val
+ module Location = Loc
+ module Domain = (val combined)
+ end)
+
+
+ (* Build a complete abstraction based on a list of registered domains and a
+ value initial configuration. *)
+ let build domains : (module Structured) =
+ let values =
+ let add_value = Value.{ folder = add } in
+ let add_values values (registered, _) =
+ match registered.abstraction with
+ | RegisteredDomain (module Domain) ->
+ Value.fold add_value Domain.values values |>
+ Location.fold_values add_value Domain.locations
+ | RegisteredFunctor (module F) ->
+ Location.fold_values add_value F.locations values
+ in
+ List.fold_left add_values Value.init domains |>
+ Value.make_interactive
+ in
+ let module V = (val Value.assert_not_unit values) in
+ let locations =
+ let init : V.t Location.structured = Location.init (module V) in
+ let add_loc = Location.{ folder = add } in
+ let add_locations locs (registered, _) =
+ match registered.abstraction with
+ | RegisteredDomain (module D) -> Location.fold add_loc D.locations locs
+ | RegisteredFunctor (module D) -> Location.fold add_loc D.locations locs
in
- (module Domain)
- in
- let domain : (module internal_domain with type value = Acc.Val.t) =
- match Abstract.Domain.(eq_structure Acc.Dom.structure Unit) with
- | Some _ -> domain
- | None ->
- (* The new [domain] becomes the left leaf of the domain product, and will
- be processed before the domains from [Acc.Dom] during the analysis. *)
- (module Domain_product.Make (Acc.Val) ((val domain)) (Acc.Dom))
- in
- (module struct
- module Val = Acc.Val
- module Loc = Acc.Loc
- module Dom = (val domain)
- end : Acc)
-
-let warn_experimental flag =
- if flag.experimental then
- Self.(warning ~wkey:wkey_experimental
- "The %s domain is experimental." flag.name)
-
-let build_domain config abstract =
- let build (Flag flag, mode) acc =
- warn_experimental flag;
- add_domain flag.name mode flag.abstraction acc
- in
- (* Domains in the [config] are sorted by increasing priority: domains with
- higher priority are added last: they will be at the top of the domains
- tree, and thus will be processed first during the analysis. *)
- Config.fold build config abstract
+ List.fold_left add_locations init domains |>
+ Location.make_interactive
+ in
+ let module L = (val Location.assert_not_unit locations) in
+ let structured : (V.t, L.location) structured =
+ Unit ((module V), (module L))
+ in
+ let structured = List.fold_left (fun s d -> add d s) structured domains in
+ let module Structured : Structured = (val assert_not_unit structured) in
+ (module Structured)
+end
-(* --- Value reduced product ----------------------------------------------- *)
-module type Value = sig
- include Abstract.Value.External
- val reduce : t -> t
-end
+(* --- Configuration -------------------------------------------------------- *)
-module type S = sig
- module Val : Value
- module Loc : Abstract.Location.External with type value = Val.t
- module Dom : Abstract.Domain.External with type value = Val.t
- and type location = Loc.location
-end
+module Config = struct
+ module Mode = Datatype.Option (Domain_mode)
+
+ include Set.Make (struct
+ open Domain
+ type t = registered with_info with_mode
+ let compare (d1, m1) (d2, m2) =
+ let c = Datatype.Int.compare d1.priority d2.priority in
+ if c = 0 then
+ let c = Datatype.String.compare d1.name d2.name in
+ if c = 0 then Mode.compare m1 m2 else c
+ else c
+ end)
+
+ let singleton name abstraction =
+ let experimental = false and priority = 9 in
+ let abstraction = Domain.{ name ; priority ; experimental ; abstraction } in
+ singleton (abstraction, None)
-module type Eva = sig
- include S
- module Eval: Evaluation.S with type state = Dom.t
- and type value = Val.t
- and type loc = Loc.location
- and type origin = Dom.origin
+ let configure () =
+ let find = Parameters.DomainsFunction.find in
+ let find name = try Some (find name) with Not_found -> None in
+ let main () = Globals.entry_point () |> fst in
+ let add_main_mode modes = (main (), Domain_mode.Mode.all) :: modes in
+ let dynamic (name, make) config =
+ let enabled = Parameters.Domains.mem name in
+ let enable modes = if enabled then add_main_mode modes else modes in
+ match find name with
+ | None -> if enabled then add (make (), None) config else config
+ | Some modes -> add (make (), Some (enable modes)) config
+ in
+ let static d = dynamic (d.Domain.name, fun () -> d) in
+ let fold f xs acc = List.fold_left (fun acc x -> f x acc) acc xs in
+ fold static !Domain.static_domains empty |>
+ fold dynamic !Domain.dynamic_domains
end
-type ('a, 'b) value_reduced_product =
- 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b)
-type v_reduced_product = R: ('a, 'b) value_reduced_product -> v_reduced_product
+(* --- Value reduced product ----------------------------------------------- *)
-let value_reduced_product = ref []
+module Reducer = struct
+ type 'a key = 'a Value.key
+ type ('a, 'b) reducer = 'a -> 'b -> 'a * 'b
+ type action = Action : 'a key * 'b key * ('a, 'b) reducer -> action
-let register_value_reduction reduced_product =
- value_reduced_product := (R reduced_product) :: !value_reduced_product
+ let actions = ref []
-(* When the value abstraction contains both a cvalue and an interval
- component (coming currently from an Apron domain), reduce them from each
- other. If the Cvalue is not a scalar do nothing, because we do not
- currently use Apron for pointer offsets. *)
-let reduce_apron_itv cvalue ival =
- match ival with
- | None -> begin
- try cvalue, Some (Cvalue.V.project_ival cvalue)
- with Cvalue.V.Not_based_on_null -> cvalue, ival
- end
- | Some ival ->
- try
- let ival' = Cvalue.V.project_ival cvalue in
- if Ival.is_int ival'
- then
- let reduced_ival = Ival.narrow ival ival' in
- let cvalue = Cvalue.V.inject_ival reduced_ival in
- cvalue, Some reduced_ival
- else cvalue, Some ival
- with Cvalue.V.Not_based_on_null -> cvalue, Some ival
-
-let () =
- register_value_reduction
- (Main_values.CVal.key, Main_values.Interval.key, reduce_apron_itv)
-
-module Reduce (Value : Abstract.Value.External) = struct
- include Value
-
- let make_reduction acc (R (key1, key2, f)) =
- match Value.get key1, Value.get key2 with
- | Some get1, Some get2 ->
- let set1 = Value.set key1
- and set2 = Value.set key2 in
- let reduce v = let v1, v2 = f (get1 v) (get2 v) in set1 v1 (set2 v2 v) in
- reduce :: acc
- | _, _ -> acc
-
- let reduce =
- let list = List.fold_left make_reduction [] !value_reduced_product in
- fun v -> List.fold_left (fun v reduce -> reduce v) v list
-end
+ let register left right reducer =
+ actions := (Action (left, right, reducer)) :: !actions
-(* --- Final hook ----------------------------------------------------------- *)
+ module type Value = sig
+ include Abstract.Value.External
+ val reduce : t -> t
+ end
-let final_hooks = ref []
+ module Make (Value : Abstract.Value.External) = struct
+ include Value
+
+ let make_reduction acc (Action (key1, key2, f)) =
+ match Value.get key1, Value.get key2 with
+ | Some get1, Some get2 ->
+ let set1 = Value.set key1 and set2 = Value.set key2 in
+ let reduce v = f (get1 v) (get2 v) in
+ let reducer v = let v1, v2 = reduce v in set1 v1 (set2 v2 v) in
+ reducer :: acc
+ | _, _ -> acc
+
+ let reduce =
+ let list = List.fold_left make_reduction [] !actions in
+ fun v -> List.fold_left (fun v reduce -> reduce v) v list
+ end
+end
-let register_hook f =
- final_hooks := f :: !final_hooks
-let apply_final_hooks abstractions =
- List.fold_left (fun acc f -> f acc) abstractions !final_hooks
-(* --- Building abstractions ------------------------------------------------ *)
+(* --- Finalizing abstractions build ---------------------------------------- *)
-module Open (Acc: Acc) : S = struct
- module Val = Reduce (Acc.Val)
- module Loc = struct
- include Acc.Loc
- include Structure.Open (Abstract.Location)
- (struct include Acc.Loc type t = location end)
- end
- module Dom = struct
- include Acc.Dom
- include Structure.Open (Abstract.Domain) (Acc.Dom)
+module type S = sig
+ module Val : Reducer.Value
+ module Loc : Abstract.Location.External with type value = Val.t
+ module Dom : Abstract.Domain.External
+ with type value = Val.t and type location = Loc.location
+end
- let get_cvalue = match get Cvalue_domain.State.key with
- | None -> None
- | Some get -> Some (fun s -> fst (get s))
+module type S_with_evaluation = sig
+ include S
+ module Eval : Evaluation_sig.S
+ with type state = Dom.t
+ and type value = Val.t
+ and type loc = Loc.location
+ and type origin = Dom.origin
+end
- let get_cvalue_or_top = match get Cvalue_domain.State.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun s -> fst (get s)
+module Hooks = struct
+ let hooks = ref []
+ type hook = (module S) -> (module S)
+ let register (f : hook) = hooks := f :: !hooks
+ let apply abst = List.fold_left (fun acc f -> f acc) abst !hooks
+end
- let get_cvalue_or_bottom = function
- | `Bottom -> Cvalue.Model.bottom
- | `Value state -> get_cvalue_or_top state
+module Open (Structured : Domain.Structured) : S = struct
+ module Val = Reducer.Make (Structured.Value)
+ module Loc = Structured.Location
+ module Dom = struct
+ include Structured.Domain
+ include Structure.Open (Abstract.Domain) (Structured.Domain)
end
end
-module CVal = Leaf_Value (Main_values.CVal)
-
-let unit_acc (module Value: Abstract.Value.External) =
- let loc : (module internal_loc with type value = Value.t) =
- match Abstract.Value.eq_structure Value.structure CVal.structure with
- | Some Structure.Eq -> (module Leaf_Location (Main_locations.PLoc))
- | _ ->
- let module Struct = struct
- type v = Cvalue.V.t
- let s = Single (module Main_values.CVal)
- end in
- let module Conv = Internal_Value.Convert (Value) (Struct) in
- (module Location_lift.Make (Main_locations.PLoc) (Conv))
- in
- (module struct
- module Val = Value
- module Loc = (val loc)
- module Dom = Unit_domain.Make (Val) (Loc)
- end : Acc)
-
-let build_abstractions config =
- let initial_value : (module Abstract.Value.Internal) =
- if Config.mem Config.bitwise config
- then (module Offsm_value.CvalueOffsm)
- else (module CVal)
- in
- let value = Internal_Value.build_values config initial_value in
- let acc = unit_acc value in
- build_domain config acc
-
-let configure = Config.configure
-
let make config =
- let abstractions = build_abstractions config in
- let abstractions = (module Open (val abstractions): S) in
- apply_final_hooks abstractions
-
-module Default = (val make Config.default)
-module Legacy = (val make Config.legacy)
+ let abstractions = Config.elements config |> Domain.build in
+ let abstractions = (module Open (val abstractions) : S) in
+ Hooks.apply abstractions
diff --git a/src/plugins/eva/engine/abstractions.mli b/src/plugins/eva/engine/abstractions.mli
index be3c32e05155142ce18afb9f54512883ffc30a6e..21a16ba10c30c3748980237edaa2ac7dc21fba63 100644
--- a/src/plugins/eva/engine/abstractions.mli
+++ b/src/plugins/eva/engine/abstractions.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+
+
(** Registration and building of the analysis abstractions. *)
(** {2 Registration of abstractions.} *)
@@ -30,152 +32,198 @@
- state abstractions, or abstract domains, detailed in {!Abstract_domain}.
*)
-(** Module types of value abstractions: either a single leaf module, or
- a compound of several modules described by a structure. In this last case,
- the structure must not contain the Void constructor. *)
-type 'v value =
- | Single of (module Abstract_value.Leaf with type t = 'v)
- | Struct of 'v Abstract.Value.structure
-
-(** For the moment, all domains must use [precise_loc] as their location
- abstraction, and no new location abstraction can be registered for an
- analysis.
- If you need to build a new location abstraction, please contact us. *)
-type precise_loc = Precise_locs.precise_location
-
-(** Module type of a leaf domain over precise_loc abstraction. *)
-module type leaf_domain = Abstract_domain.Leaf with type location = precise_loc
-
-(** Module type of a functor building a leaf domain from a value abstraction.
- The resulting domain must use the input value as value abstraction. *)
-module type domain_functor = functor
- (Value: Abstract.Value.External) -> (leaf_domain with type value = Value.t)
-
-(** Type of domain to be registered: either a leaf module with ['v] as value
- abstraction, or a functor building a domain from any value abstraction. *)
-type 'v domain =
- | Domain: (module leaf_domain with type value = 'v) -> 'v domain
- | Functor: (module domain_functor) -> _ domain
-
-(** Abstraction to be registered. *)
-type 'v abstraction =
- { values: 'v value; (** The value abstraction. *)
- domain: 'v domain ; (** The domain over the value abstraction. *)
- }
-
-(** Information about a registered abstraction. *)
-type 't with_info =
- { name: string; (** Name of the domain. Must be unique. *)
- experimental: bool; (** Is the domain experimental? *)
- priority: int; (** Domains with higher priority are processed first. *)
- abstraction: 't; (** The abstract value and the domain. *)
- }
-
-(** Flag for an abstract domain. A domain can be programmatically enabled via
- its flag. See module {!Config} for more details. *)
-type flag = Flag: 'v abstraction with_info -> flag
-
-(** Registers an abstract domain. Returns a flag for the given domain.
- - [name] must be unique. The domain is used if the -eva-domains option
- has been set to [name].
- - [descr] is a description printed in the help message of -eva-domains.
- - [experimental] is false by default. If set to true, a warning is emitted
- when the domain is enabled.
- - [priority] can be any integer; domains with higher priority are always
- processed first. The domains currently provided by Eva have priority
- ranging between 1 and 19, so a priority of 0 (respectively 20) ensures
- that a new domain is processed after (respectively before) the classic
- Eva domains. The default priority is 0. *)
-val register:
- name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
- 'v abstraction -> flag
-
-(** Register a dynamic abstraction: the abstraction is built by applying
- the last argument when starting an analysis, if the -eva-domains option
- has been set to [name]. See function {!register} for more details. *)
-val dynamic_register:
- name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
- (unit -> 'v abstraction) -> unit
-
-(** Reduced product between two value abstractions, identified by their keys. *)
-type ('a, 'b) value_reduced_product =
- 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b)
-
-(** Register a reduction function for a value reduced product. *)
-val register_value_reduction: ('a, 'b) value_reduced_product -> unit
-
-
-(** {2 Types used in the engine.} *)
-
-(** The external signature of value abstractions, plus the reduction function
- of the reduced product. *)
-module type Value = sig
- include Abstract.Value.External
- val reduce : t -> t
+(** Value abstractions registration. *)
+module Value : sig
+ type 'v key = 'v Abstract.Value.key
+ type 'v value = (module Abstract_value.S with type t = 'v)
+
+ (** Registering a value abstraction requires a single module and a key. The
+ returned [`v registered] is a witness of the registration process and is
+ used by the location and domain abstractions registration to declare their
+ value dependencies. *)
+ type 'v register = { key : 'v key ; value : 'v value }
+ type 'v registered
+ val register : 'v register -> 'v registered
+
+ (** Other abstractions need to declare their value dependencies, i.e. the
+ value abstractions they rely on to perform their computations. Those
+ dependencies are declared as a heterogenous list containing at least one
+ element. *)
+ type 'v dependencies =
+ | Last : 'v registered -> 'v dependencies
+ | (::) : 'a registered * 'b dependencies -> ('a * 'b) dependencies
end
-(** The three abstractions used in an Eva analysis. *)
-module type S = sig
- module Val : Value
- module Loc : Abstract.Location.External with type value = Val.t
- module Dom : Abstract.Domain.External with type value = Val.t
- and type location = Loc.location
+
+(** Location abstractions registration. *)
+module Location : sig
+ type 'l key = 'l Abstract.Location.key
+ type ('v, 'l) location =
+ (module Abstract_location.S with type value = 'v and type location = 'l)
+
+ (** Registering a location abstraction requires a single module, a key and the
+ registered value abstractions needed to perform the computations. The
+ returned [`l registered] is a witness of the registration process and is
+ used by the domain abstractions registration to declare their location
+ dependencies. *)
+ type ('v, 'l) register =
+ { key : 'l key
+ ; location : ('v, 'l) location
+ ; dependencies : 'v Value.dependencies
+ }
+ type 'l registered
+ val register : ('v, 'l) register -> 'l registered
+
+ (** Domain abstractions need to declare their location dependencies. As for
+ the value dependencies, they are declared as a heterogenous list. *)
+ type 'l dependencies =
+ | Last : 'l registered -> 'l dependencies
+ | (::) : 'a registered * 'b dependencies -> ('a * 'b) dependencies
end
-(** The three abstractions plus an evaluation engine for these abstractions. *)
-module type Eva = sig
- include S
- module Eval: Evaluation.S with type state = Dom.t
- and type value = Val.t
- and type loc = Loc.location
- and type origin = Dom.origin
+
+(** Domain abstractions registration. *)
+module Domain : sig
+ type 's key = 's Abstract.Domain.key
+
+ (** Leaf domain abstraction, i.e. a simple domain with fixed values and
+ locations dependencies. The registration of such domains requires a
+ key, a single module and values and locations dependencies. *)
+ module Leaf : sig
+ type ('v, 'l, 's) domain =
+ (module Abstract_domain.S
+ with type value = 'v and type location = 'l and type state = 's)
+
+ type ('v, 'l, 's) register =
+ { key : 's key
+ ; domain : ('v, 'l, 's) domain
+ ; values : 'v Value.dependencies
+ ; locations : 'l Location.dependencies
+ }
+ end
+
+ (** Functor domain abstraction, i.e. a domain that can be built over any value
+ abstractions, but with fixed locations dependencies. The registraction of
+ such domains requires only the location dependencies, as the abstraction
+ produced by the functor cannot rely on any particular value and the key
+ can depend on the value abstractions used. *)
+ module Functor : sig
+ module type Domain = sig
+ type location
+ module Make (V : Abstract.Value.External) : sig
+ include Abstract_domain.S
+ with type value = V.t and type location = location
+ val key : state key
+ end
+ end
+ type 'l domain = (module Domain with type location = 'l)
+
+ type 'l register =
+ { domain : 'l domain
+ ; locations : 'l Location.dependencies
+ }
+ end
+
+ (** Registration of both kind of domain abstractions is done using the same
+ functions. The two kind of registration information are thus regrouped
+ under the same type. The returned [registered] is a witness of the
+ registration process and can be used to programmatically enable the
+ domain. *)
+ type register =
+ | Domain : ('v, 'l, 's) Leaf.register -> register
+ | Functor : 'l Functor.register -> register
+ type registered
+
+ (** Registers an abstract domain. Returns a flag for the given domain.
+ - [name] must be unique. The domain is used if the -eva-domains option
+ has been set to [name].
+ - [descr] is a description printed in the help message of -eva-domains.
+ - [experimental] is false by default. If set to true, a warning is emitted
+ when the domain is enabled.
+ - [priority] can be any integer; domains with higher priority are always
+ processed first. The domains currently provided by Eva have priority
+ ranging between 1 and 19, so a priority of 0 (respectively 20) ensures
+ that a new domain is processed after (respectively before) the classic
+ Eva domains. The default priority is 0. *)
+ val register :
+ name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
+ register -> registered
+
+ (** Register a dynamic abstraction: the abstraction is built by applying
+ the last argument when starting an analysis, if the -eva-domains option
+ has been set to [name]. See function {!register} for more details. *)
+ val dynamic_register :
+ name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
+ (unit -> register) -> unit
+end
+
+
+(** Value reduced product registration. Registering a value reduced product
+ requires the keys of each value abstractions involved along with a reducer,
+ i.e. a function that perform the reduction. *)
+module Reducer : sig
+ type ('a, 'b) reducer = 'a -> 'b -> 'a * 'b
+ val register : 'a Value.key -> 'b Value.key -> ('a, 'b) reducer -> unit
+
+ (** The value abstractions signature used in the engine. It is composed of the
+ external signature of value abstractions, plus the reduction function of
+ the reduced product. *)
+ module type Value = sig
+ include Abstract.Value.External
+ val reduce : t -> t
+ end
end
-(** Register a hook modifying the three abstractions after their building by
- the engine, before the start of each analysis. *)
-val register_hook: ((module S) -> (module S)) -> unit
+
(** {2 Configuration of an analysis.} *)
-(** Configuration defining the abstractions to be used in an analysis.
- A configuration is a set of flags, i.e. a set of abstract domains. Each flag
- comes with an optional mode. None is the default mode: the given domain is
- enabled for the whole analysis. See {!Domain_mode} for more details. *)
+(** Configuration defining the abstractions to be used in an analysis. A
+ configuration can either be built from a given domain along with its
+ name or can be built based on the command line parameters. The first
+ approach relies on the [singleton] function and is mainly used to
+ build a default abstraction during the engine initialization. The
+ second one relies on the [configure] function. *)
module Config : sig
- include Set.S with type elt = flag * Domain_mode.t option
-
- (** Returns true if the given flag is in the configuration. *)
- val mem: flag -> t -> bool
-
- (** Flags for the standard domains currently provided in Eva. *)
-
- val cvalue: flag
- val equality: flag
- val symbolic_locations: flag
- val gauges: flag
- val octagon: flag
- val bitwise: flag
- val inout: flag
- val sign: flag
- val traces: flag
- val printer: flag
-
- val default: t
- (** The default configuration of Eva. *)
-
- val legacy: t
- (** The configuration corresponding to the old "Value" analysis,
- with only the cvalue domain enabled. *)
+ type t
+ val equal : t -> t -> bool
+ val singleton : string -> Domain.registered -> t
+ val configure : unit -> t
end
-(** Creates the configuration according to the analysis parameters. *)
-val configure: unit -> Config.t
+
+
+(** {2 Types and functions used in the engine.} *)
+
+(** The three abstractions used in an Eva analysis. *)
+module type S = sig
+ module Val : Reducer.Value
+ module Loc : Abstract.Location.External with type value = Val.t
+ module Dom : Abstract.Domain.External
+ with type value = Val.t and type location = Loc.location
+end
+
+(* The three abstractions plus an evaluation engine for these abstractions. *)
+module type S_with_evaluation = sig
+ include S
+ module Eval : Evaluation_sig.S
+ with type state = Dom.t
+ and type value = Val.t
+ and type loc = Loc.location
+ and type origin = Dom.origin
+end
(** Builds the abstractions according to a configuration. *)
-val make: Config.t -> (module S)
+val make : Config.t -> (module S)
-(** Two abstractions are instantiated at compile time for the default and legacy
- configurations (which may be the same). *)
-module Legacy : S
-module Default : S
+
+(** {2 Analysis low level modifications.} *)
+
+(** Registration of a hook, i.e. a function that modifies directly the three
+ abstractions after their building by the engine and before the start of
+ each analysis. *)
+module Hooks : sig
+ type hook = (module S) -> (module S)
+ val register : hook -> unit
+end
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index a390c9398cfd06d88ea2a8f813466d6d78b4b143..c6fe1ee2bc3103382d5a897c99b89f4434bd8c89 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -72,7 +72,7 @@ module type Results = sig
end
module type S = sig
- include Abstractions.Eva
+ include Abstractions.S_with_evaluation
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
@@ -81,7 +81,7 @@ end
module type Analyzer = sig
include S
val compute_from_entry_point : kernel_function -> lib_entry:bool -> unit
- val compute_from_init_state: kernel_function -> Dom.t -> unit
+ (* val compute_from_init_state: kernel_function -> Dom.t -> unit *)
val initial_state: lib_entry:bool -> Dom.t or_bottom
end
@@ -90,7 +90,7 @@ module Make (Abstract: Abstractions.S) = struct
module Abstract = struct
include Abstract
- module Eval = Evaluation.Make (Abstract.Val) (Abstract.Loc) (Abstract.Dom)
+ module Eval = Evaluation.Make (Val) (Loc) (Dom)
end
include Abstract
@@ -149,20 +149,15 @@ module Make (Abstract: Abstractions.S) = struct
end
-module Legacy = Make (Abstractions.Legacy)
-module Default =
- (val
- (if Abstractions.Config.(equal default legacy)
- then (module Legacy)
- else (module Make (Abstractions.Default)))
- : Analyzer)
+let default = Abstractions.Config.singleton "cvalue" Cvalue_domain.registered
+module Default : Analyzer = Make (val Abstractions.make default)
+
(* Reference to the current configuration (built by Abstractions.configure from
the parameters of Eva regarding the abstractions used in the analysis) and
the current Analyzer module. *)
-let ref_analyzer =
- ref (Abstractions.Config.default, (module Default : Analyzer))
+let ref_analyzer = ref (default, (module Default : Analyzer))
(* Returns the current Analyzer module. *)
let current_analyzer () = (module (val (snd !ref_analyzer)): S)
@@ -182,15 +177,15 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
let cvalue_initial_state () =
let module A = (val snd !ref_analyzer) in
+ let module G = (Cvalue_domain.Getters (A.Dom)) in
let _, lib_entry = Globals.entry_point () in
- A.Dom.get_cvalue_or_bottom (A.initial_state ~lib_entry)
+ G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
let analyzer =
- if Abstractions.Config.(equal config legacy) then (module Legacy: Analyzer)
- else if Abstractions.Config.(equal config default) then (module Default)
+ if Abstractions.Config.(equal config default) then (module Default : Analyzer)
else
let module Abstract = (val Abstractions.make config) in
let module Analyzer = Make (Abstract) in
@@ -200,7 +195,7 @@ let make_analyzer config =
(* Builds the analyzer according to the parameters of Eva. *)
let reset_analyzer () =
- let config = Abstractions.configure () in
+ let config = Abstractions.Config.configure () in
(* If the configuration has not changed, do not reset the Analyzer but uses
the reference instead. *)
if not (Abstractions.Config.equal config (fst !ref_analyzer))
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 3cb30baf2214b8afd75d27e8ef5fed42b9d88798..dc017343ef221e88d4369946e52ffc6463218251 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -60,7 +60,7 @@ end
module type S = sig
- include Abstractions.Eva
+ include Abstractions.S_with_evaluation
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 5e913a57d2c6738e82bcb20c861fa11a0cbc8177..11a90011b3aec48f415ac7bc8bfc4059ac70d5f4 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -141,7 +141,7 @@ let register_signal_handler () =
let restore_sigint = register_handler Sys.sigint interrupt in
fun () -> restore_sigusr1 (); restore_sigint ()
-module Make (Abstract: Abstractions.Eva) = struct
+module Make (Abstract: Abstractions.S_with_evaluation) = struct
module PowersetDomain = Powerset.Make (Abstract.Dom)
@@ -154,6 +154,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Iterator.Computer
(Abstract) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
+ include Cvalue_domain.Getters (Abstract.Dom)
+
let initial_state = Init.initial_state
let get_cval =
@@ -185,7 +187,7 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
+ let cvalue = get_cvalue_or_top init_state in
Cvalue_callbacks.apply_call_hooks call.callstack call.kf `Memexec cvalue;
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
@@ -240,7 +242,7 @@ module Make (Abstract: Abstractions.Eva) = struct
"@[computing for function %a.@\nCalled from %a.@]"
Value_types.Callstack.pretty_short call.callstack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
- let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
+ let cvalue_state = get_cvalue_or_top state in
let compute, kind =
match target with
| `Def (fundec, save_results) ->
@@ -290,7 +292,7 @@ module Make (Abstract: Abstractions.Eva) = struct
in
Locations.Location_Bytes.do_track_garbled_mix true;
let final_state = join_states states in
- let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
+ let cvalue_state = get_cvalue_or_top state in
match final_state with
| `Bottom ->
let kind = `Spec spec in
@@ -299,7 +301,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
let cvalue_call = get_cvalue_call call in
- let post = Abstract.Dom.get_cvalue_or_top final_state in
+ let post = get_cvalue_or_top final_state in
let cvalue_states =
Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
in
@@ -344,7 +346,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let store_initial_state kf init_state =
Abstract.Dom.Store.register_initial_state (Eva_utils.call_stack ()) init_state;
- let cvalue_state = Abstract.Dom.get_cvalue_or_top init_state in
+ let cvalue_state = get_cvalue_or_top init_state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
let compute kf init_state =
diff --git a/src/plugins/eva/engine/compute_functions.mli b/src/plugins/eva/engine/compute_functions.mli
index 2eea8219cdbbf5e9a8a7c664e4640155da7d6919..28f78965dbb2d54008aabe51674bbf084a49f3d8 100644
--- a/src/plugins/eva/engine/compute_functions.mli
+++ b/src/plugins/eva/engine/compute_functions.mli
@@ -25,7 +25,7 @@
open Cil_types
open Eval
-module Make (Abstract: Abstractions.Eva)
+module Make (Abstract: Abstractions.S_with_evaluation)
: sig
(** Compute a call to the main function. *)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index fa55a38798a0e020a7e632e9aa39de4bbd4712c3..7a58005d92be8f394687268b4a7f44a76084b3e7 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -183,36 +183,6 @@ let exp_alarm_signed_converted_downcast =
let signed_exp = Cil.new_exp ~loc:exp.eloc (CastE (signed_typ, exp)) in
signed_exp)
-module type S = sig
- type state
- type value
- type origin
- type loc
- module Valuation : Valuation with type value = value
- and type origin = origin
- and type loc = loc
- val to_domain_valuation:
- Valuation.t -> (value, loc, origin) Abstract_domain.valuation
- val evaluate :
- ?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
- state -> exp -> (Valuation.t * value) evaluated
- val copy_lvalue :
- ?valuation:Valuation.t -> ?subdivnb:int ->
- state -> lval -> (Valuation.t * value flagged_value) evaluated
- val lvaluate :
- ?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
- state -> lval -> (Valuation.t * loc * typ) evaluated
- val reduce:
- ?valuation:Valuation.t -> state -> exp -> bool -> Valuation.t evaluated
- val assume:
- ?valuation:Valuation.t -> state -> exp -> value -> Valuation.t or_bottom
- val eval_function_exp:
- ?subdivnb:int -> exp -> ?args:exp list -> state ->
- (Kernel_function.t * Valuation.t) list evaluated
- val interpret_truth:
- alarm:(unit -> Alarms.t) -> 'a -> 'a Abstract_value.truth -> 'a evaluated
-end
-
let return t = `Value t, Alarmset.none
(* Intersects [alarms] with the only possible alarms from the dereference of
@@ -895,7 +865,7 @@ module Make
| AddrOf v | StartOf v ->
lval_to_loc context ~for_writing:false ~reduction:false v
>>= fun (loc, _, _) ->
- let value = Loc.to_value loc in
+ (Loc.to_value loc, Alarmset.none) >>= fun value ->
let v = assume_pointer expr value in
compute_reduction v false
@@ -1394,7 +1364,7 @@ module Make
| Mem expr, offset ->
match offset with
| NoOffset ->
- let loc_value = Loc.to_value location in
+ Loc.to_value location >>- fun loc_value ->
backward_eval fuel state expr (Some loc_value) >>-: fun _ -> ()
| _ ->
let reduce_valid_index = true in
@@ -1691,7 +1661,6 @@ module Make
| _ -> assert false
end
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/eva/engine/evaluation.mli b/src/plugins/eva/engine/evaluation.mli
index 6197f1d07fb23dae081e2cb38e226c17dbb3148e..ff7487ecf1bfdbf17609864a1cd00161b3329066 100644
--- a/src/plugins/eva/engine/evaluation.mli
+++ b/src/plugins/eva/engine/evaluation.mli
@@ -20,111 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
-open Eval
-
-(** Generic evaluation and reduction of expressions and left values. *)
-
-module type S = sig
-
- (** State of abstract domain. *)
- type state
-
- (** Numeric values to which the expressions are evaluated. *)
- type value
-
- (** Origin of values. *)
- type origin
-
- (** Location of an lvalue. *)
- type loc
-
- (** Results of an evaluation: the results of all intermediate calculation (the
- value of each expression and the location of each lvalue) are cached here.
- See {!Eval} for more details. *)
- module Valuation : Valuation with type value = value
- 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 from [Abstract_domain.valuation]
- records. This function converts the former into the latter. *)
- val to_domain_valuation:
- 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;
- - [result] is either `Bottom if the evaluation leads to an error,
- or `Value (valuation, value), where [value] is the numeric value computed
- for the expression [expr], and [valuation] contains all the intermediate
- results of the evaluation.
-
- Optional arguments are:
- - [valuation] is a cache of already computed expressions; empty by default.
- - [reduction] allows the deactivation of the backward reduction performed
- after the forward evaluation; true by default.
- - [subdivnb] is the maximum number of subdivisions performed on non-linear
- sub-expressions of [expr]. If a lvalue occurs several times in [expr],
- its value can be split up to [subdivnb] times to gain more precision.
- Set to the value of the option -eva-subdivide-non-linear by default. *)
- val evaluate :
- ?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
- state -> exp -> (Valuation.t * value) evaluated
-
- (** Computes the value of a lvalue, with possible indeterminateness: the
- returned value may be uninitialized, or contain escaping addresses.
- Also returns the alarms resulting of the evaluation of the lvalue location,
- and a valuation containing all the intermediate results of the evaluation.
- The [valuation] argument is a cache of already computed expressions.
- It is empty by default.
- [subdivnb] is the maximum number of subdivisions performed on non-linear
- expressions. *)
- val copy_lvalue :
- ?valuation:Valuation.t -> ?subdivnb:int ->
- state -> lval -> (Valuation.t * value flagged_value) evaluated
-
- (** [lvaluate ~valuation ~for_writing state lval] evaluates the left value
- [lval] in the state [state]. Same general behavior as [evaluate] above
- but evaluates the lvalue into a location and its type.
- The boolean [for_writing] indicates whether the lvalue is evaluated to be
- read or written. It is useful for the emission of the alarms, and for the
- reduction of the location.
- [subdivnb] is the maximum number of subdivisions performed on non-linear
- expressions (including the possible pointer and offset of the lvalue). *)
- val lvaluate :
- ?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
- state -> lval -> (Valuation.t * loc * typ) evaluated
-
- (** [reduce ~valuation state expr positive] evaluates the expression [expr]
- in the state [state], and then reduces the [valuation] such that
- the expression [expr] evaluates to a zero or a non-zero value, according
- to [positive]. By default, the empty valuation is used. *)
- val reduce:
- ?valuation:Valuation.t ->
- state -> exp -> bool -> Valuation.t evaluated
-
- (** [assume ~valuation state expr value] assumes in the [valuation] that
- the expression [expr] has the value [value] in the state [state],
- and backward propagates this information to the subterm of [expr].
- If [expr] has not been already evaluated in the [valuation], its forward
- evaluation takes place first, but the alarms are dismissed. By default,
- the empty valuation is used.
- The function returns the updated valuation, or bottom if it discovers
- a contradiction. *)
- val assume:
- ?valuation:Valuation.t ->
- state -> exp -> value -> Valuation.t or_bottom
-
- val eval_function_exp:
- ?subdivnb:int -> exp -> ?args:exp list -> state ->
- (Kernel_function.t * Valuation.t) list evaluated
- (** Evaluation of the function argument of a [Call] constructor *)
-
- val interpret_truth:
- alarm:(unit -> Alarms.t) -> 'a -> 'a Abstract_value.truth -> 'a evaluated
-end
-
module type Value = sig
include Abstract.Value.External
@@ -146,11 +41,10 @@ module Make
(Loc : Abstract_location.S with type value = Value.t)
(Domain : Queries with type value = Value.t
and type location = Loc.location)
- : S with type state = Domain.state
- and type value = Value.t
- and type origin = Domain.origin
- and type loc = Loc.location
-
+ : Evaluation_sig.S with type state = Domain.state
+ and type value = Value.t
+ and type origin = Domain.origin
+ and type loc = Loc.location
(*
Local Variables:
diff --git a/src/plugins/eva/engine/evaluation_sig.ml b/src/plugins/eva/engine/evaluation_sig.ml
new file mode 100644
index 0000000000000000000000000000000000000000..75673541afa231aa24ae910d904560b2e69cafd4
--- /dev/null
+++ b/src/plugins/eva/engine/evaluation_sig.ml
@@ -0,0 +1,126 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Eval
+
+(** Generic evaluation and reduction of expressions and left values. *)
+
+module type S = sig
+
+ (** State of abstract domain. *)
+ type state
+
+ (** Numeric values to which the expressions are evaluated. *)
+ type value
+
+ (** Origin of values. *)
+ type origin
+
+ (** Location of an lvalue. *)
+ type loc
+
+ (** Results of an evaluation: the results of all intermediate calculation (the
+ value of each expression and the location of each lvalue) are cached here.
+ See {!Eval} for more details. *)
+ module Valuation : Valuation with type value = value
+ 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 from [Abstract_domain.valuation]
+ records. This function converts the former into the latter. *)
+ val to_domain_valuation:
+ 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;
+ - [result] is either `Bottom if the evaluation leads to an error,
+ or `Value (valuation, value), where [value] is the numeric value computed
+ for the expression [expr], and [valuation] contains all the intermediate
+ results of the evaluation.
+
+ Optional arguments are:
+ - [valuation] is a cache of already computed expressions; empty by default.
+ - [reduction] allows the deactivation of the backward reduction performed
+ after the forward evaluation; true by default.
+ - [subdivnb] is the maximum number of subdivisions performed on non-linear
+ sub-expressions of [expr]. If a lvalue occurs several times in [expr],
+ its value can be split up to [subdivnb] times to gain more precision.
+ Set to the value of the option -eva-subdivide-non-linear by default. *)
+ val evaluate :
+ ?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
+ state -> exp -> (Valuation.t * value) evaluated
+
+ (** Computes the value of a lvalue, with possible indeterminateness: the
+ returned value may be uninitialized, or contain escaping addresses.
+ Also returns the alarms resulting of the evaluation of the lvalue location,
+ and a valuation containing all the intermediate results of the evaluation.
+ The [valuation] argument is a cache of already computed expressions.
+ It is empty by default.
+ [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions. *)
+ val copy_lvalue :
+ ?valuation:Valuation.t -> ?subdivnb:int ->
+ state -> lval -> (Valuation.t * value flagged_value) evaluated
+
+ (** [lvaluate ~valuation ~for_writing state lval] evaluates the left value
+ [lval] in the state [state]. Same general behavior as [evaluate] above
+ but evaluates the lvalue into a location and its type.
+ The boolean [for_writing] indicates whether the lvalue is evaluated to be
+ read or written. It is useful for the emission of the alarms, and for the
+ reduction of the location.
+ [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions (including the possible pointer and offset of the lvalue). *)
+ val lvaluate :
+ ?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
+ state -> lval -> (Valuation.t * loc * typ) evaluated
+
+ (** [reduce ~valuation state expr positive] evaluates the expression [expr]
+ in the state [state], and then reduces the [valuation] such that
+ the expression [expr] evaluates to a zero or a non-zero value, according
+ to [positive]. By default, the empty valuation is used. *)
+ val reduce:
+ ?valuation:Valuation.t ->
+ state -> exp -> bool -> Valuation.t evaluated
+
+ (** [assume ~valuation state expr value] assumes in the [valuation] that
+ the expression [expr] has the value [value] in the state [state],
+ and backward propagates this information to the subterm of [expr].
+ If [expr] has not been already evaluated in the [valuation], its forward
+ evaluation takes place first, but the alarms are dismissed. By default,
+ the empty valuation is used.
+ The function returns the updated valuation, or bottom if it discovers
+ a contradiction. *)
+ val assume:
+ ?valuation:Valuation.t ->
+ state -> exp -> value -> Valuation.t or_bottom
+
+ val eval_function_exp:
+ ?subdivnb:int -> exp -> ?args:exp list -> state ->
+ (Kernel_function.t * Valuation.t) list evaluated
+ (** Evaluation of the function argument of a [Call] constructor *)
+
+ val interpret_truth:
+ alarm:(unit -> Alarms.t) -> 'a -> 'a Abstract_value.truth -> 'a evaluated
+end
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index 7cccb65020e25018c7191d12951acd08ca77ffc8..ba5c5ea1c1539b2d72543981a0f827cab92722e1 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -82,8 +82,8 @@ let counter = ref 0
module Make
(Domain: Abstract.Domain.External)
- (Eva: Evaluation.S with type state = Domain.state
- and type loc = Domain.location)
+ (Eva: Evaluation_sig.S with type state = Domain.state
+ and type loc = Domain.location)
(Transfer: Transfer_stmt.S with type state = Domain.t)
= struct
@@ -95,6 +95,7 @@ module Make
fst (Eva.lvaluate ~for_writing:false Domain.top lval)
>>> fun (_valuation, loc, _typ) -> loc
+ include Cvalue_domain.Getters (Domain)
(* ------------------------- Apply initializer ---------------------------- *)
@@ -272,7 +273,7 @@ module Make
(* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *)
let add_supplied_main_formals kf actuals state =
- match Domain.get_cvalue with
+ match get_cvalue with
| None -> Self.abort "Function Db.Value.fun_set_args cannot be \
used without the Cvalue domain"
| Some get_cvalue ->
@@ -366,7 +367,7 @@ module Make
else global_state ~lib_entry
let print_initial_cvalue_state state =
- let cvalue_state = Domain.get_cvalue_or_bottom state in
+ let cvalue_state = get_cvalue_or_bottom state in
(* Do not show variables from the frama-c libc specifications. *)
let print_base base =
try
diff --git a/src/plugins/eva/engine/initialization.mli b/src/plugins/eva/engine/initialization.mli
index 9012946abe082baf204f551152efae99468bb9da..872206abe61796ac482a107efdd3d344668ca87b 100644
--- a/src/plugins/eva/engine/initialization.mli
+++ b/src/plugins/eva/engine/initialization.mli
@@ -45,8 +45,8 @@ end
module Make
(Domain: Abstract.Domain.External)
- (Eva: Evaluation.S with type state = Domain.state
- and type loc = Domain.location)
+ (Eva: Evaluation_sig.S with type state = Domain.state
+ and type loc = Domain.location)
(Transfer: Transfer_stmt.S with type state = Domain.t)
: S with type state := Domain.t
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 2a0c7af021ac216b6eae8cea7f8315e3604f3ece..7979fd721696059972af7faf81b24327e98c4c0f 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -45,7 +45,7 @@ let blocks_share_locals b1 b2 =
| _, _ -> false
module Make_Dataflow
- (Abstract : Abstractions.Eva)
+ (Abstract : Abstractions.S_with_evaluation)
(States : Powerset.S with type state = Abstract.Dom.t)
(Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
(Init: Initialization.S with type state := Abstract.Dom.t)
@@ -63,6 +63,7 @@ module Make_Dataflow
= struct
module Domain = Abstract.Dom
+ include Cvalue_domain.Getters (Domain)
(* --- Analysis parameters --- *)
@@ -441,7 +442,7 @@ module Make_Dataflow
edge_info.fireable <- true;
flow
- let gather_cvalues states = match Domain.get_cvalue with
+ let gather_cvalues states = match get_cvalue with
| Some get -> List.map get states
| None -> []
@@ -681,7 +682,7 @@ module Make_Dataflow
then VertexTable.memo merged_states v get_smashed_store
else `Bottom
and lift_to_cvalues table =
- StmtTable.map (fun _ s -> Domain.get_cvalue_or_top s) (Lazy.force table)
+ StmtTable.map (fun _ s -> get_cvalue_or_top s) (Lazy.force table)
in
let merged_pre_states = lazy
(StmtTable.map' (fun s (v,_) -> get_merged_states ~all:true s v) automaton.stmt_table)
@@ -696,7 +697,7 @@ module Make_Dataflow
(StmtTable.map (fun _stmt (v,_) ->
let store = get_vertex_store v in
let states = Partitioning.expanded store in
- List.map (fun (_k,x) -> Domain.get_cvalue_or_top x) states)
+ List.map (fun (_k,x) -> get_cvalue_or_top x) states)
automaton.stmt_table)
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
@@ -744,7 +745,7 @@ end
module Computer
- (Abstract : Abstractions.Eva)
+ (Abstract : Abstractions.S_with_evaluation)
(States : Powerset.S with type state = Abstract.Dom.t)
(Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
(Init: Initialization.S with type state := Abstract.Dom.t)
diff --git a/src/plugins/eva/engine/iterator.mli b/src/plugins/eva/engine/iterator.mli
index 1c70fd4b0e17a75e7454e721b731edd3b606a829..0d1f9944063057b116f95a53af45b2766169cd64 100644
--- a/src/plugins/eva/engine/iterator.mli
+++ b/src/plugins/eva/engine/iterator.mli
@@ -27,7 +27,7 @@ val signal_abort: unit -> unit
module Computer
(* Abstractions with the evaluator. *)
- (Abstract: Abstractions.Eva)
+ (Abstract: Abstractions.S_with_evaluation)
(* Set of states of abstract domain. *)
(States : Powerset.S with type state = Abstract.Dom.t)
(* Transfer functions for statement on the abstract domain. *)
diff --git a/src/plugins/eva/engine/subdivided_evaluation.ml b/src/plugins/eva/engine/subdivided_evaluation.ml
index 5e0ea2abac87900a9cc23b77e0e8cf90000a6bcd..60949a0ef0a7ade04b1e9f198791293a5ef1029c 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.ml
+++ b/src/plugins/eva/engine/subdivided_evaluation.ml
@@ -856,8 +856,8 @@ module Make
| Lval (host, off as lval) ->
if Cil.typeHasQualifier "volatile" (Cil.typeOfLval lval) then `Value acc
else
- let loc = find_loc valuation lval in
- if Cvalue.V.cardinal_zero_or_one (get_cval (Loc.to_value loc))
+ Loc.to_value (find_loc valuation lval) >>- fun value ->
+ if Cvalue.V.cardinal_zero_or_one (get_cval value)
then
(* no variable in the host or in the offset can be influential. Check
the contents of the location, on which we might want to enumerate*)
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 0821c12b0356dc91faf181ece6239c65c245c2d8..ebde0b8888044622355b7b71954dc3915149f5b7 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -179,6 +179,7 @@ module Make
module Domain = Abstract.Dom
module Location = Abstract.Loc
+ include Cvalue_domain.Getters (Domain)
(* Most transfer functions about logic return a set of states instead of a
single state, and States.empty instead of bottom. We thus use this monad
@@ -239,7 +240,7 @@ module Make
let set_location loc = set_ploc (Main_locations.PLoc.make loc)
let make_env state =
- Eval_terms.env_assigns ~pre:(Domain.get_cvalue_or_top state)
+ Eval_terms.env_assigns ~pre:(get_cvalue_or_top state)
(* Evaluates the location affected by an assigns, allocates, frees or \from
clause. Returns None if the clause cannot be interpreted. *)
@@ -322,7 +323,7 @@ module Make
end
in
let check_one_state state =
- let cvalue_state = Domain.get_cvalue_or_top state in
+ let cvalue_state = get_cvalue_or_top state in
List.iter (check_one_assign cvalue_state) assigns
in
States.iter check_one_state states
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 71042b2b2e41baab8d8f7d0c49e811f686231910..3d17e1177e9756eeeafe100a238db064756dc675 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -114,12 +114,13 @@ let substitution_visitor table = object
| Some vi -> Cil.ChangeTo vi
end
-module Make (Abstract: Abstractions.Eva) = struct
+module Make (Abstract: Abstractions.S_with_evaluation) = struct
module Value = Abstract.Val
module Location = Abstract.Loc
module Domain = Abstract.Dom
module Eval = Abstract.Eval
+ include Cvalue_domain.Getters (Domain)
type state = Domain.t
type value = Value.t
@@ -633,7 +634,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* For non scalar expressions, prints the offsetmap of the cvalue domain. *)
let show_offsm =
- match Domain.get_cvalue, Location.get Main_locations.PLoc.key with
+ match get_cvalue, Location.get Main_locations.PLoc.key with
| None, _ | _, None ->
fun fmt _ _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cvalue, Some get_ploc ->
@@ -729,7 +730,7 @@ module Make (Abstract: Abstractions.Eva) = struct
{Cvalue_transfer.start_call}. *)
let apply_cvalue_callback kf ki_call state =
let stack_with_call = (kf, ki_call) :: Eva_utils.call_stack () in
- let cvalue_state = Domain.get_cvalue_or_top state in
+ let cvalue_state = get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
let kind = `Builtin None in
Cvalue_callbacks.apply_call_hooks stack_with_call kf kind cvalue_state
diff --git a/src/plugins/eva/engine/transfer_stmt.mli b/src/plugins/eva/engine/transfer_stmt.mli
index a54bfe15b9cc5b7b6849a5cabfaeba4c9674ede0..7da3e2be794787a059471923e14b7d7bdacf7260 100644
--- a/src/plugins/eva/engine/transfer_stmt.mli
+++ b/src/plugins/eva/engine/transfer_stmt.mli
@@ -58,7 +58,7 @@ module type S = sig
(stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
end
-module Make (Abstract: Abstractions.Eva)
+module Make (Abstract: Abstractions.S_with_evaluation)
: S with type state = Abstract.Dom.t
and type value = Abstract.Val.t
and type loc = Abstract.Loc.location
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 8dd3dbd6d1682d60541f7e119ebd035cfda7470d..25d985d9e4d77693633421bc8e3567105bd11f26 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -139,6 +139,7 @@ end
module Make (X: Analysis.S) = struct
module Analysis = X
+ include Cvalue_domain.Getters (X.Dom)
let get_precise_loc =
match X.Loc.get Main_locations.PLoc.key with
@@ -202,7 +203,7 @@ module Make (X: Analysis.S) = struct
let lval_to_offsetmap state lv =
let loc, alarms = X.eval_lval_to_loc state lv in
let ok = Alarmset.is_empty alarms in
- let state = X.Dom.get_cvalue_or_top state in
+ let state = get_cvalue_or_top state in
let aux loc (acc_res, acc_ok) =
let res, ok =
match lv with (* catch simplest pattern *)
@@ -265,7 +266,7 @@ module Make (X: Analysis.S) = struct
}
let null_to_offsetmap state (_:unit) =
- let state = X.Dom.get_cvalue_or_top state in
+ let state = get_cvalue_or_top state in
match Cvalue.Model.find_base_or_default Base.null state with
| `Bottom -> GO_InvalidLoc, false, false
| `Top -> GO_Top, false, false
@@ -327,17 +328,17 @@ module Make (X: Analysis.S) = struct
let env_here kf here callstack =
let pre = pre_kf kf callstack in
- let here = X.Dom.get_cvalue_or_top here in
+ let here = get_cvalue_or_top here in
let c_labels = Eval_annots.c_labels kf callstack in
Eval_terms.env_annot ~c_labels ~pre ~here ()
let env_pre _kf here _callstack =
- let here = X.Dom.get_cvalue_or_top here in
+ let here = get_cvalue_or_top here in
Eval_terms.env_pre_f ~pre:here ()
let env_post kf post callstack =
let pre = pre_kf kf callstack in
- let post = X.Dom.get_cvalue_or_top post in
+ let post = get_cvalue_or_top post in
let result =
if Function_calls.use_spec_instead_of_definition kf then
None
diff --git a/src/plugins/eva/gui/gui_types.ml b/src/plugins/eva/gui/gui_types.ml
index e52339afa5e8918bdbd00c42cb15234e8671064b..94f675343aa8ecb17515ad6137ae9596a5a033d3 100644
--- a/src/plugins/eva/gui/gui_types.ml
+++ b/src/plugins/eva/gui/gui_types.ml
@@ -135,7 +135,7 @@ module type S = sig
val equal_gui_after : value gui_after -> value gui_after -> bool
end
-module Make (V: Abstractions.Value) = struct
+module Make (V: Abstract.Value.External) = struct
let pretty_gui_res fmt = function
| GR_Empty -> ()
diff --git a/src/plugins/eva/gui/gui_types.mli b/src/plugins/eva/gui/gui_types.mli
index fdc05aa6401b9103a1521c7ff6974bf902535ace..e4d5018d9c10a678c9a4c719d470f9280ff5d719 100644
--- a/src/plugins/eva/gui/gui_types.mli
+++ b/src/plugins/eva/gui/gui_types.mli
@@ -99,7 +99,7 @@ module type S = sig
end
(** The types below depend on the abstract values currently available. *)
-module Make (V : Abstractions.Value) : sig
+module Make (V : Abstract.Value.External) : sig
include S with type value := V.t
val get_cvalue : (V.t -> Main_values.CVal.t) option
diff --git a/src/plugins/eva/locations/locations_product.ml b/src/plugins/eva/locations/locations_product.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e6fad814205d20093d00dd1ced03c3f8c47ece82
--- /dev/null
+++ b/src/plugins/eva/locations/locations_product.ml
@@ -0,0 +1,125 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Eval
+
+
+
+module Make
+ (Value: Abstract_value.S)
+ (Left: Abstract.Location.Internal with type value = Value.t)
+ (Right: Abstract.Location.Internal with type value = Value.t)
+= struct
+ type value = Value.t
+ let structure = Abstract.Location.Node (Left.structure, Right.structure)
+
+ type offset = Left.offset * Right.offset
+ type location = Left.location * Right.location
+
+ let top = Left.top, Right.top
+
+ let equal_loc (l, r) (l', r') =
+ Left.equal_loc l l' && Right.equal_loc r r'
+ let pretty_loc =
+ Pretty_utils.pp_pair Left.pretty_loc Right.pretty_loc
+
+ let equal_offset (l, r) (l', r') =
+ Left.equal_offset l l' && Right.equal_offset r r'
+ let pretty_offset =
+ Pretty_utils.pp_pair Left.pretty_offset Right.pretty_offset
+
+ (* TODO: don't know what to do, used max by default *)
+ let size (l, r) =
+ match Left.size l, Right.size r with
+ | Int_Base.Top, size
+ | size, Int_Base.Top -> size
+ | Int_Base.Value lsize as size, Int_Base.Value rsize ->
+ if Integer.equal lsize rsize then size else
+ Self.fatal
+ "Location product: inconsistent size of the same location \
+ represented by %a (size %a) and %a (size %a)."
+ Left.pretty_loc l Integer.pretty lsize
+ Right.pretty_loc r Integer.pretty rsize
+
+ let replace_base subst (l, r) =
+ Left.replace_base subst l, Right.replace_base subst r
+
+ let assume_no_overlap ~partial (l1, r1) (l2, r2) =
+ let l_truth = Left.assume_no_overlap ~partial l1 l2 in
+ let r_truth = Right.assume_no_overlap ~partial r1 r2 in
+ Value_product.narrow_truth_pair ((l1, l2), l_truth) ((r1, r2), r_truth)
+
+ let assume_valid_location ~for_writing ~bitfield (l, r) =
+ let l_truth = Left.assume_valid_location ~for_writing ~bitfield l in
+ let r_truth = Right.assume_valid_location ~for_writing ~bitfield r in
+ Value_product.narrow_truth (l, l_truth) (r, r_truth)
+
+ let no_offset = Left.no_offset, Right.no_offset
+
+ let forward_field typ varinfo (l, r) =
+ Left.forward_field typ varinfo l, Right.forward_field typ varinfo r
+
+ let forward_variable typ varinfo (l, r) =
+ let* l = Left.forward_variable typ varinfo l in
+ let* r = Right.forward_variable typ varinfo r in
+ `Value (l, r)
+
+ let eval_varinfo varinfo =
+ Left.eval_varinfo varinfo, Right.eval_varinfo varinfo
+
+ let backward_variable varinfo (l, r) =
+ let* l = Left.backward_variable varinfo l in
+ let* r = Right.backward_variable varinfo r in
+ `Value (l, r)
+
+ let backward_field typ varinfo (lo, ro) =
+ let* lo = Left.backward_field typ varinfo lo in
+ let* ro = Right.backward_field typ varinfo ro in
+ `Value (lo, ro)
+
+ (** Both value abstractions produce a sound value abstraction for the same
+ location, so we can narrow their results. *)
+ let to_value (l, r) =
+ let* vleft = Left.to_value l
+ and* vright = Right.to_value r in
+ Value.narrow vleft vright
+
+ let forward_index typ v (l, r) =
+ Left.forward_index typ v l, Right.forward_index typ v r
+
+ let forward_pointer typ v (lo, ro) =
+ let* l = Left.forward_pointer typ v lo in
+ let* r = Right.forward_pointer typ v ro in
+ `Value (l, r)
+
+ let backward_pointer v (lo, ro) (l, r) =
+ let* (lv, lo) = Left.backward_pointer v lo l in
+ let* (rv, ro) = Right.backward_pointer v ro r in
+ let* v = Value.narrow lv rv in
+ `Value (v, (lo, ro))
+
+ let backward_index typ ~index ~remaining:(lrem, rrem) (lo, ro) =
+ let* (lv, lo) = Left.backward_index typ ~index ~remaining:lrem lo in
+ let* (rv, ro) = Right.backward_index typ ~index ~remaining:rrem ro in
+ let* v = Value.narrow lv rv in
+ `Value (v, (lo, ro))
+end
diff --git a/src/plugins/eva/locations/locations_product.mli b/src/plugins/eva/locations/locations_product.mli
new file mode 100644
index 0000000000000000000000000000000000000000..150c21c89eba0fca1c895b2b9fc553e7e4a02392
--- /dev/null
+++ b/src/plugins/eva/locations/locations_product.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Make
+ (Value: Abstract_value.S)
+ (Left: Abstract.Location.Internal with type value = Value.t)
+ (Right: Abstract.Location.Internal with type value = Value.t)
+ : Abstract.Location.Internal
+ with type value = Value.t
+ and type location = Left.location * Right.location
+ and type offset = Left.offset * Right.offset
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 3df1e5d6b2efb702367092fb9854ffc779d43ad5..58b52807752271e0a9c58bb69d832deeb6f78844 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -323,7 +323,7 @@ let cross_equality loop lval =
| Some lval -> lval
| None | exception No_equality -> lval
-module Make (Abstract: Abstractions.Eva) = struct
+module Make (Abstract: Abstractions.S_with_evaluation) = struct
open Eval
open Abstract
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.mli b/src/plugins/eva/partitioning/auto_loop_unroll.mli
index 4bbc478a68584f5c3bcf6543c41883006692d528..1922eb815dfc850ff97e624f4730ff9c58444028 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.mli
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.mli
@@ -22,7 +22,7 @@
(** Heuristic for automatic loop unrolling. *)
-module Make (Abstract: Abstractions.Eva) : sig
+module Make (Abstract: Abstractions.S_with_evaluation) : sig
val compute:
max_unroll:int -> Abstract.Dom.t -> Cil_types.stmt -> int option
diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index 14723800087101c1b1049d3fd7a0b910ff631278..a994030d11119fdf8254e9cde51a4d6962fca531 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -322,7 +322,7 @@ exception InvalidAction
(* --- Flows --- *)
-module MakeFlow (Abstract: Abstractions.Eva) =
+module MakeFlow (Abstract: Abstractions.S_with_evaluation) =
struct
type state = Abstract.Dom.t
type t = (key * state) list
diff --git a/src/plugins/eva/partitioning/partition.mli b/src/plugins/eva/partitioning/partition.mli
index caf4e08c2487c27dba54be9916b43945669c14d4..18256b222e2249af59dc67eef3c5128956a6b4f4 100644
--- a/src/plugins/eva/partitioning/partition.mli
+++ b/src/plugins/eva/partitioning/partition.mli
@@ -175,7 +175,7 @@ exception InvalidAction
(** Flows are used to transfer states from one partition to another, by
applying transfer functions and partitioning actions. They do not enforce
the unicity of keys. *)
-module MakeFlow (Abstract: Abstractions.Eva) :
+module MakeFlow (Abstract: Abstractions.S_with_evaluation) :
sig
type state = Abstract.Dom.t
type t
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index 2e38c548ff027ad0587432d265d6e0beaff02f6a..ae449dc72983922a90d7215ed43e9f298d7935db 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -26,7 +26,7 @@ open Partition
let stat_max_widenings = Statistics.register_statement_stat "max-widenings"
module Make
- (Abstract: Abstractions.Eva)
+ (Abstract: Abstractions.S_with_evaluation)
(Kf : sig val kf: kernel_function end) =
struct
module Partition_parameters = Partitioning_parameters.Make (Kf)
diff --git a/src/plugins/eva/partitioning/trace_partitioning.mli b/src/plugins/eva/partitioning/trace_partitioning.mli
index dd8cade8865e1ec7ae490547566e411efb46b588..d6e22fb5345a33f170950df629cd0b38f6b495d1 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.mli
+++ b/src/plugins/eva/partitioning/trace_partitioning.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
module Make
- (Abstract : Abstractions.Eva)
+ (Abstract : Abstractions.S_with_evaluation)
(Kf : sig val kf: Cil_types.kernel_function end) :
sig
(** The states being partitioned *)
diff --git a/src/plugins/eva/utils/abstract.ml b/src/plugins/eva/utils/abstract.ml
index 11c54bedde65a23402bffb172c8168234f2f42cb..1ef84e43b66b2516ada82693c6488252cb76a5d8 100644
--- a/src/plugins/eva/utils/abstract.ml
+++ b/src/plugins/eva/utils/abstract.ml
@@ -80,9 +80,5 @@ module Domain = struct
include Structure.External with type t := t
and type 'a key := 'a key
and type 'a data := 'a data
-
- val get_cvalue: (t -> Cvalue.Model.t) option
- val get_cvalue_or_top: t -> Cvalue.Model.t
- val get_cvalue_or_bottom: t Lattice_bounds.or_bottom -> Cvalue.Model.t
end
end
diff --git a/src/plugins/eva/utils/abstract.mli b/src/plugins/eva/utils/abstract.mli
index d3d5e3a3a62a07f60af87054df0a7ac32f00e57f..399aac89323e8e0d894e720a5c4d5ee4e9cc6329 100644
--- a/src/plugins/eva/utils/abstract.mli
+++ b/src/plugins/eva/utils/abstract.mli
@@ -90,10 +90,5 @@ module Domain : sig
include Structure.External with type t := t
and type 'a key := 'a key
and type 'a data := 'a data
-
- (** Special accessors for the main cvalue domain. *)
- val get_cvalue: (t -> Cvalue.Model.t) option
- val get_cvalue_or_top: t -> Cvalue.Model.t
- val get_cvalue_or_bottom: t Lattice_bounds.or_bottom -> Cvalue.Model.t
end
end
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index 3c28cfb69da993bfc8f99d62ffb18c3c4647359f..2994cdfb8d21cf96fd800f045be6b6982b9bd780 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -22,10 +22,12 @@
module Abstract_domain = Abstract_domain
module Abstract_value = Abstract_value
+module Abstract = Abstract
module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Cvalue_domain = Cvalue_domain
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
module Eva_results = Eva_results
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index 2012d89d2920890ab2e46f43185c330c2c050d7f..41ab31a858140a4854d048dd62d190a8bf6b02b0 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -26,10 +26,12 @@
module Abstract_domain = Abstract_domain
module Abstract_value = Abstract_value
+module Abstract = Abstract
module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Cvalue_domain = Cvalue_domain
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
module Eva_results = Eva_results
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 6133518219ca79430760b556261fb28f1329b98c..2d048a8995e6b381a6c223c74ea543cf108c16be 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -314,10 +314,11 @@ struct
convert r
let get_cvalue_model req =
- match A.Dom.get_cvalue with
+ match A.Dom.get Cvalue_domain.State.key with
| None ->
Result.error DisabledDomain
| Some extract ->
+ let extract s = extract s |> fst in
convert (Response.map_join extract Cvalue.Model.join (get req))
let get_state req key join =
diff --git a/src/plugins/eva/values/abstract_location.ml b/src/plugins/eva/values/abstract_location.ml
index 1cbc439a1f8dbd7e5dc4b23904dc88ff6ded3d36..e4b18564d97f0099492b1a3890670da1a8ffcab5 100644
--- a/src/plugins/eva/values/abstract_location.ml
+++ b/src/plugins/eva/values/abstract_location.ml
@@ -44,7 +44,7 @@ module type S = sig
val pretty_loc: Format.formatter -> location -> unit
val pretty_offset : Format.formatter -> offset -> unit
- val to_value : location -> value
+ val to_value : location -> value or_bottom
val size : location -> Int_Base.t
(** [replace_base substitution location] replaces the variables represented
diff --git a/src/plugins/eva/values/location_lift.ml b/src/plugins/eva/values/location_lift.ml
index 5aaee286c0d3d1178a417fcd8e8d7663883e6e7b..769faab7a8c797b552699a8a3ea996bee1c9812c 100644
--- a/src/plugins/eva/values/location_lift.ml
+++ b/src/plugins/eva/values/location_lift.ml
@@ -23,17 +23,16 @@
open Eval
module type Conversion = sig
- type extended_value
- type internal_value
-
- val extend_val : internal_value -> extended_value
- val replace_val : internal_value -> extended_value -> extended_value
- val restrict_val : extended_value -> internal_value
+ type extended
+ type internal
+ val extend : internal -> extended
+ val replace : internal -> extended -> extended
+ val restrict : extended -> internal
end
module Make
(Loc: Abstract_location.Leaf)
- (Convert : Conversion with type internal_value := Loc.value)
+ (Convert : Conversion with type internal := Loc.value)
= struct
(* Import most of [Loc] *)
@@ -41,29 +40,29 @@ module Make
with type value := Loc.value (* we are converting this type *)
and type location = Loc.location
and type offset = Loc.offset)
- type value = Convert.extended_value
+ type value = Convert.extended
let structure = Abstract.Location.Leaf (Loc.key, (module Loc))
(* Now lift the functions that contain {!value} in their type. *)
- let to_value loc = Convert.extend_val (Loc.to_value loc)
+ let to_value loc = Loc.to_value loc >>-: Convert.extend
let forward_index typ value offset =
- Loc.forward_index typ (Convert.restrict_val value) offset
+ Loc.forward_index typ (Convert.restrict value) offset
let forward_pointer typ value offset =
- Loc.forward_pointer typ (Convert.restrict_val value) offset
+ Loc.forward_pointer typ (Convert.restrict value) offset
let backward_pointer value offset loc =
- let v = Convert.restrict_val value in
+ let v = Convert.restrict value in
Loc.backward_pointer v offset loc >>-: fun (v, off) ->
- Convert.replace_val v value, off
+ Convert.replace v value, off
let backward_index typ ~index:value ~remaining offset =
- let index = Convert.restrict_val value in
+ let index = Convert.restrict value in
Loc.backward_index typ ~index ~remaining offset >>-: fun (v, off) ->
- Convert.replace_val v value, off
+ Convert.replace v value, off
end
diff --git a/src/plugins/eva/values/location_lift.mli b/src/plugins/eva/values/location_lift.mli
index 34b80aaa11daac14e7796e10184b66b6bd645e1d..d66d68fb6ca44873bbf1c31eb0ce6943bad92227 100644
--- a/src/plugins/eva/values/location_lift.mli
+++ b/src/plugins/eva/values/location_lift.mli
@@ -21,20 +21,19 @@
(**************************************************************************)
module type Conversion = sig
- type extended_value
- type internal_value
-
- val extend_val : internal_value -> extended_value
- val replace_val : internal_value -> extended_value -> extended_value
- val restrict_val : extended_value -> internal_value
+ type extended
+ type internal
+ val extend : internal -> extended
+ val replace : internal -> extended -> extended
+ val restrict : extended -> internal
end
module Make
(Loc: Abstract_location.Leaf)
- (Convert : Conversion with type internal_value := Loc.value)
+ (Convert : Conversion with type internal := Loc.value)
: Abstract.Location.Internal with type location = Loc.location
and type offset = Loc.offset
- and type value = Convert.extended_value
+ and type value = Convert.extended
(*
diff --git a/src/plugins/eva/values/main_locations.ml b/src/plugins/eva/values/main_locations.ml
index 92d31c7f54b1baeaaf2723e373815aef3cd9bfc3..f74e3799a852ab747d9494b98fb2f10edbd6cedd 100644
--- a/src/plugins/eva/values/main_locations.ml
+++ b/src/plugins/eva/values/main_locations.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-module PLoc = struct
+module Location = struct
type value = Cvalue.V.t
type location = Precise_locs.precise_location
@@ -28,8 +28,6 @@ module PLoc = struct
| Precise of Precise_locs.precise_offset
| Imprecise of Cvalue.V.t (* when the offset contains addresses *)
- let key = Structure.Key_Location.create_key "precise_locs"
-
let equal_loc = Precise_locs.equal_loc
let equal_offset o1 o2 = match o1, o2 with
| Precise o1, Precise o2 -> Precise_locs.equal_offset o1 o2
@@ -43,7 +41,7 @@ module PLoc = struct
let to_value t =
let loc = Precise_locs.imprecise_location t in
- Locations.loc_to_loc_without_size loc
+ `Value (Locations.loc_to_loc_without_size loc)
let size loc = Precise_locs.loc_size loc
@@ -235,10 +233,18 @@ module PLoc = struct
`Value (index, rem)
(* No reduction if the offsets are not arithmetics. *)
with Cvalue.V.Not_based_on_null -> `Value (index, remaining)
-
end
+module PLoc = struct
+ include Location
+ let key = Structure.Key_Location.create_key "precise_locs"
+ let registered = Abstractions.Location.register
+ { key ; location = (module Location)
+ ; dependencies = Last Main_values.CVal.registered
+ }
+end
+
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/eva/values/main_locations.mli b/src/plugins/eva/values/main_locations.mli
index 4d95a9933e380e44166fae2d006cc0ce957b77a8..7349704d2bb1910d67e730d711ad688d349b70fe 100644
--- a/src/plugins/eva/values/main_locations.mli
+++ b/src/plugins/eva/values/main_locations.mli
@@ -24,13 +24,14 @@
(** Abstract locations built over Precise_locs. *)
module PLoc : sig
-
- include Abstract_location.Leaf
+ include Abstract_location.S
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
val make: Locations.location -> location
+ val key : location Abstract_location.key
+ val registered : location Abstractions.Location.registered
end
(*
diff --git a/src/plugins/eva/values/main_values.ml b/src/plugins/eva/values/main_values.ml
index fdd47e5052ce7028de7f6f1cb341b4fc0f9a0012..909106265a10f2c9c85f583b4a67be4301decdf6 100644
--- a/src/plugins/eva/values/main_values.ml
+++ b/src/plugins/eva/values/main_values.ml
@@ -23,175 +23,184 @@
open Cil_types
module CVal = struct
- include Cvalue.V
-
- let key = Structure.Key_Value.create_key "cvalue"
-
- let zero = Cvalue.V.singleton_zero
- let one = Cvalue.V.singleton_one
-
- let top = Cvalue.V.top
- let top_int = Cvalue.V.top_int
- let inject_int _typ = Cvalue.V.inject_int
-
- let equal = Cvalue.V.equal
- let is_included = Cvalue.V.is_included
- let join = Cvalue.V.join
- let narrow a b =
- let n = Cvalue.V.narrow a b in
- if Cvalue.V.is_bottom n
- then `Bottom
- else `Value n
-
- let assume_non_zero = Cvalue_forward.assume_non_zero
- let assume_bounded = Cvalue_forward.assume_bounded
- let assume_not_nan = Cvalue_forward.assume_not_nan
- let assume_pointer = Cvalue_forward.assume_pointer
- let assume_comparable = Cvalue_forward.assume_comparable
-
- let constant exp = function
- | CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
- | CChr c -> Cvalue.V.inject_int (Cil.charConstToInt c)
- | CWStr _ | CStr _ -> Cvalue.V.inject (Base.of_string_exp exp) Ival.zero
- | CReal (f, fkind, fstring) ->
- Cvalue_forward.eval_float_constant f fkind fstring
- | CEnum _ -> assert false
-
- let forward_unop typ unop value =
- let value = Cvalue_forward.forward_unop typ unop value in
- (* TODO: `Bottom must be in CValue and Cvalue_forward. *)
- if Cvalue.V.is_bottom value then `Bottom else `Value value
-
- let forward_binop typ binop v1 v2 =
- let value =
- match typ with
- | TFloat (fkind, _) ->
- Cvalue_forward.forward_binop_float (Fval.kind fkind) v1 binop v2
- | TInt _ | TPtr _ | _ as typ ->
- Cvalue_forward.forward_binop_int ~typ v1 binop v2
- in
- if Cvalue.V.is_bottom value
- then `Bottom
- else `Value value
-
- let rewrap_integer = Cvalue_forward.rewrap_integer
-
- let forward_cast ~src_type ~dst_type v =
- let v = Cvalue_forward.forward_cast ~src_type ~dst_type v in
- if Cvalue.V.is_bottom v then `Bottom else `Value v
-
- let backward_binop ~input_type ~resulting_type binop ~left ~right ~result =
- let reduction =
- Cvalue_backward.backward_binop
- ~typ_res:resulting_type ~res_value:result ~typ_e1:input_type left binop right
- in
- match reduction with
- | None -> `Value (None, None)
- | Some (v1, v2) ->
- if Cvalue.V.is_bottom v1 || Cvalue.V.is_bottom v2
- then `Bottom
- else `Value (Some v1, Some v2)
-
- let backward_unop ~typ_arg op ~arg ~res =
- let reduction = Cvalue_backward.backward_unop ~typ_arg op ~arg ~res in
- match reduction with
- | None -> `Value None
- | Some v as r ->
- if Cvalue.V.is_bottom v
+ module Value = struct
+ include Cvalue.V
+
+ let zero = Cvalue.V.singleton_zero
+ let one = Cvalue.V.singleton_one
+
+ let top = Cvalue.V.top
+ let top_int = Cvalue.V.top_int
+ let inject_int _typ = Cvalue.V.inject_int
+
+ let equal = Cvalue.V.equal
+ let is_included = Cvalue.V.is_included
+ let join = Cvalue.V.join
+ let narrow a b =
+ let n = Cvalue.V.narrow a b in
+ if Cvalue.V.is_bottom n
then `Bottom
- else `Value r
-
- let backward_cast ~src_typ ~dst_typ ~src_val ~dst_val =
- let reduction =
- Cvalue_backward.backward_cast ~src_typ ~dst_typ ~src_val ~dst_val
- in
- match reduction with
- | None -> `Value None
- | Some v ->
- if Cvalue.V.is_bottom v
+ else `Value n
+
+ let assume_non_zero = Cvalue_forward.assume_non_zero
+ let assume_bounded = Cvalue_forward.assume_bounded
+ let assume_not_nan = Cvalue_forward.assume_not_nan
+ let assume_pointer = Cvalue_forward.assume_pointer
+ let assume_comparable = Cvalue_forward.assume_comparable
+
+ let constant exp = function
+ | CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
+ | CChr c -> Cvalue.V.inject_int (Cil.charConstToInt c)
+ | CWStr _ | CStr _ -> Cvalue.V.inject (Base.of_string_exp exp) Ival.zero
+ | CReal (f, fkind, fstring) ->
+ Cvalue_forward.eval_float_constant f fkind fstring
+ | CEnum _ -> assert false
+
+ let forward_unop typ unop value =
+ let value = Cvalue_forward.forward_unop typ unop value in
+ (* TODO: `Bottom must be in CValue and Cvalue_forward. *)
+ if Cvalue.V.is_bottom value then `Bottom else `Value value
+
+ let forward_binop typ binop v1 v2 =
+ let value =
+ match typ with
+ | TFloat (fkind, _) ->
+ Cvalue_forward.forward_binop_float (Fval.kind fkind) v1 binop v2
+ | TInt _ | TPtr _ | _ as typ ->
+ Cvalue_forward.forward_binop_int ~typ v1 binop v2
+ in
+ if Cvalue.V.is_bottom value
then `Bottom
- else if Cvalue.V.is_included src_val v
- then `Value None
- else `Value (Some v)
-
- let resolve_functions v =
- let aux base offs (acc, alarm) =
- match base with
- | Base.String (_,_) | Base.Null | Base.CLogic_Var _ | Base.Allocated _ ->
- acc, true
- | Base.Var (v,_) ->
- if Cil.isFunctionType v.vtype then
- let alarm = alarm || Ival.contains_non_zero offs in
- let kf = Globals.Functions.get v in
- let list = if Ival.contains_zero offs then kf :: acc else acc in
- list, alarm
- else acc, true
- in
- try
- let init = [], false in
- let kfs, alarm = Locations.Location_Bytes.fold_topset_ok aux v init in
- `Value kfs, alarm
- with Abstract_interp.Error_Top -> `Top, true
-
- let replace_base substitution t = snd (Cvalue.V.replace_base substitution t)
+ else `Value value
+
+ let rewrap_integer = Cvalue_forward.rewrap_integer
+
+ let forward_cast ~src_type ~dst_type v =
+ let v = Cvalue_forward.forward_cast ~src_type ~dst_type v in
+ if Cvalue.V.is_bottom v then `Bottom else `Value v
+
+ let backward_binop ~input_type ~resulting_type binop ~left ~right ~result =
+ let reduction =
+ Cvalue_backward.backward_binop
+ ~typ_res:resulting_type ~res_value:result ~typ_e1:input_type left binop right
+ in
+ match reduction with
+ | None -> `Value (None, None)
+ | Some (v1, v2) ->
+ if Cvalue.V.is_bottom v1 || Cvalue.V.is_bottom v2
+ then `Bottom
+ else `Value (Some v1, Some v2)
+
+ let backward_unop ~typ_arg op ~arg ~res =
+ let reduction = Cvalue_backward.backward_unop ~typ_arg op ~arg ~res in
+ match reduction with
+ | None -> `Value None
+ | Some v as r ->
+ if Cvalue.V.is_bottom v
+ then `Bottom
+ else `Value r
+
+ let backward_cast ~src_typ ~dst_typ ~src_val ~dst_val =
+ let reduction =
+ Cvalue_backward.backward_cast ~src_typ ~dst_typ ~src_val ~dst_val
+ in
+ match reduction with
+ | None -> `Value None
+ | Some v ->
+ if Cvalue.V.is_bottom v
+ then `Bottom
+ else if Cvalue.V.is_included src_val v
+ then `Value None
+ else `Value (Some v)
+
+ let resolve_functions v =
+ let aux base offs (acc, alarm) =
+ match base with
+ | Base.String (_,_) | Base.Null | Base.CLogic_Var _ | Base.Allocated _ ->
+ acc, true
+ | Base.Var (v,_) ->
+ if Cil.isFunctionType v.vtype then
+ let alarm = alarm || Ival.contains_non_zero offs in
+ let kf = Globals.Functions.get v in
+ let list = if Ival.contains_zero offs then kf :: acc else acc in
+ list, alarm
+ else acc, true
+ in
+ try
+ let init = [], false in
+ let kfs, alarm = Locations.Location_Bytes.fold_topset_ok aux v init in
+ `Value kfs, alarm
+ with Abstract_interp.Error_Top -> `Top, true
+
+ let replace_base substitution t = snd (Cvalue.V.replace_base substitution t)
+ end
+
+ let key = Structure.Key_Value.create_key "cvalue"
+ let registered = Abstractions.Value.register { key ; value = (module Value) }
+ include Value
end
+
module Interval = struct
+ module Value = struct
+ include Datatype.Option (Ival)
+
+ let pretty_typ _ = pretty
+
+ let top = None
+
+ let is_included a b = match a, b with
+ | _, None -> true
+ | None, _ -> false
+ | Some a, Some b -> Ival.is_included a b
+
+ let join a b = match a, b with
+ | None, _ | _, None -> None
+ | Some a, Some b -> Some (Ival.join a b)
+
+ let narrow a b = match a, b with
+ | None, x | x, None -> `Value x
+ | Some a, Some b ->
+ let res = Ival.narrow a b in
+ if Ival.is_bottom res then `Bottom else `Value (Some res)
+
+ let zero = None
+ let one = None
+ let top_int = None
+ let inject_int _typ i = Some (Ival.inject_singleton i)
+
+ let assume_non_zero v = `Unknown v
+ let assume_bounded _ _ v = `Unknown v
+ let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
+ let assume_comparable _ v1 v2 = `Unknown (v1, v2)
+
+ let constant _ _ = top
+ let forward_unop _ _ _ = `Value top
+ let forward_binop _ _ _ _ = `Value top
+ let forward_cast ~src_type:_ ~dst_type:_ _ = `Value top
+
+ let resolve_functions _ = `Top, true
+ let replace_base _substitution t = t
+
+ let rewrap_integer range value =
+ match value with
+ | None -> value
+ | Some value ->
+ let size = Integer.of_int range.Eval_typ.i_bits in
+ let signed = range.Eval_typ.i_signed in
+ Some (Ival.cast_int_to_int ~signed ~size value)
+
+ let backward_unop ~typ_arg:_ _unop ~arg:_ ~res:_ = `Value None
+ let backward_binop ~input_type:_ ~resulting_type:_ _binop ~left:_ ~right:_ ~result:_ =
+ `Value (None, None)
+ let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
+ `Value None
+ end
- include Datatype.Option (Ival)
let key = Structure.Key_Value.create_key "interval"
-
- let pretty_typ _ = pretty
-
- let top = None
-
- let is_included a b = match a, b with
- | _, None -> true
- | None, _ -> false
- | Some a, Some b -> Ival.is_included a b
-
- let join a b = match a, b with
- | None, _ | _, None -> None
- | Some a, Some b -> Some (Ival.join a b)
-
- let narrow a b = match a, b with
- | None, x | x, None -> `Value x
- | Some a, Some b ->
- let res = Ival.narrow a b in
- if Ival.is_bottom res then `Bottom else `Value (Some res)
-
- let zero = None
- let one = None
- let top_int = None
- let inject_int _typ i = Some (Ival.inject_singleton i)
-
- let assume_non_zero v = `Unknown v
- let assume_bounded _ _ v = `Unknown v
- let assume_not_nan ~assume_finite:_ _ v = `Unknown v
- let assume_pointer v = `Unknown v
- let assume_comparable _ v1 v2 = `Unknown (v1, v2)
-
- let constant _ _ = top
- let forward_unop _ _ _ = `Value top
- let forward_binop _ _ _ _ = `Value top
- let forward_cast ~src_type:_ ~dst_type:_ _ = `Value top
-
- let resolve_functions _ = `Top, true
- let replace_base _substitution t = t
-
- let rewrap_integer range value =
- match value with
- | None -> value
- | Some value ->
- let size = Integer.of_int range.Eval_typ.i_bits in
- let signed = range.Eval_typ.i_signed in
- Some (Ival.cast_int_to_int ~signed ~size value)
-
- let backward_unop ~typ_arg:_ _unop ~arg:_ ~res:_ = `Value None
- let backward_binop ~input_type:_ ~resulting_type:_ _binop ~left:_ ~right:_ ~result:_ =
- `Value (None, None)
- let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
- `Value None
+ let registered = Abstractions.Value.register { key ; value = (module Value) }
+ include Value
end
(*
diff --git a/src/plugins/eva/values/main_values.mli b/src/plugins/eva/values/main_values.mli
index dc71abad115a51b916cab31f719006fe27921f29..e203d3b8f217a0c9fd1a154271777c44cf6298e4 100644
--- a/src/plugins/eva/values/main_values.mli
+++ b/src/plugins/eva/values/main_values.mli
@@ -23,11 +23,19 @@
(** Main numeric values of Eva. *)
(** Abstract values built over Cvalue.V *)
-module CVal : Abstract_value.Leaf with type t = Cvalue.V.t
+module CVal : sig
+ include Abstract_value.S with type t = Cvalue.V.t
+ val key : t Abstract_value.key
+ val registered : t Abstractions.Value.registered
+end
(** Dummy interval: no forward nor backward propagations.
[None] is top. *)
-module Interval : Abstract_value.Leaf with type t = Ival.t option
+module Interval : sig
+ include Abstract_value.S with type t = Ival.t option
+ val key : t Abstract_value.key
+ val registered : t Abstractions.Value.registered
+end
(*
Local Variables:
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index 35ddb8f38afc8051fb2a606e551258c3ab7753b8..c4b990bf6d8ca67d25b339c0fbb72853c911a55d 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -369,175 +369,186 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
end)
-module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
- include Datatype_Offsm_or_top
+module Offsm = struct
+ module Value : Abstract_value.S with type t = offsm_or_top = struct
+ include Datatype_Offsm_or_top
+
+ let pretty_typ typ fmt = function
+ | Top as o -> pretty fmt o
+ | O o ->
+ Format.fprintf fmt "O @[%a@]"
+ (V_Offsetmap.pretty_generic ?typ ()) o
+
+ let top = Top
+
+ let is_included o1 o2 = match o1, o2 with
+ | _, Top -> true
+ | O o1, O o2 -> V_Offsetmap.is_included o1 o2
+ | Top, O _ -> false
+
+ let join o1 o2 = match o1, o2 with
+ | Top, _ | _, Top -> Top
+ | O o1, O o2 -> O (V_Offsetmap.join o1 o2)
+
+ let narrow o1 o2 = match o1, o2 with
+ | Top, o | o, Top -> `Value o
+ | O o1, O o2 ->
+ V_Offsetmap.narrow_reinterpret o1 o2 >>-: (fun o -> O o)
+
+ (* Simple values cannot be injected because we do not known their type
+ (hence size in bits *)
+ let zero = Top
+ let one = Top
+ let top_int = Top
+
+ let inject_int typ i =
+ try
+ let size = Integer.of_int (Cil.bitsSizeOf typ) in
+ O (inject ~size (V.inject_int i))
+ with Cil.SizeOfError _ -> Top
+
+ let assume_non_zero v = `Unknown v
+ let assume_bounded _ _ v = `Unknown v
+ let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
+ let assume_comparable _ v1 v2 = `Unknown (v1, v2)
+
+ let constant e _c =
+ if store_redundant then
+ match Cil.constFoldToInt e with
+ | Some i -> inject_int (Cil.typeOf e) i
+ | None -> Top
+ else Top
+
+ let resolve_functions _ = `Top, true (* TODO: extract value *)
+ let replace_base substitution = function
+ | Top -> Top
+ | O offsm ->
+ let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
+ O (Cvalue.V_Offsetmap.map_on_values f offsm)
+
+ let forward_unop _typ op o =
+ let o' = match o, op with
+ | Top, _ | _, (Neg | LNot) -> Top
+ | O o, BNot -> O (bnot o)
+ in
+ `Value o'
+
+ let forward_binop _typ op o1 o2 =
+ let o' =
+ match o1, o2, op with
+ | O _o1, O _o2, (Shiftlt | Shiftrt) ->
+ (* It is inconvenient to handle shift here, because we need a
+ constant for o2 *)
+ Top
+ | O o1, O o2, BAnd -> O (bitwise_and o1 o2)
+ | O o1, O o2, BOr -> O (bitwise_or o1 o2)
+ | O o1, O o2, BXor -> O (bitwise_xor o1 o2)
+ | _ -> Top
+ in
+ `Value o'
+
+ let backward_binop ~input_type:_ ~resulting_type:_ _op ~left:_ ~right:_ ~result:_ =
+ `Value (None, None)
+
+ let backward_unop ~typ_arg:_ _unop ~arg:_ ~res:_ = `Value None
+
+ let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
+ `Value None
+
+ let rewrap_integer _range o = o
+
+ let forward_cast ~src_type ~dst_type o =
+ let open Eval_typ in
+ match o, src_type, dst_type with
+ | O o, (TSInt src | TSPtr src), (TSInt dst | TSPtr dst) ->
+ let old_size = Int.of_int src.i_bits in
+ let new_size = Int.of_int dst.i_bits in
+ let signed = src.i_signed in
+ `Value (O (cast ~old_size ~new_size ~signed o))
+ | _ -> `Value Top
+ end
let key = Structure.Key_Value.create_key "offsetmap_value"
-
- let pretty_typ typ fmt = function
- | Top as o -> pretty fmt o
- | O o ->
- Format.fprintf fmt "O @[%a@]"
- (V_Offsetmap.pretty_generic ?typ ()) o
-
- let top = Top
-
- let is_included o1 o2 = match o1, o2 with
- | _, Top -> true
- | O o1, O o2 -> V_Offsetmap.is_included o1 o2
- | Top, O _ -> false
-
- let join o1 o2 = match o1, o2 with
- | Top, _ | _, Top -> Top
- | O o1, O o2 -> O (V_Offsetmap.join o1 o2)
-
- let narrow o1 o2 = match o1, o2 with
- | Top, o | o, Top -> `Value o
- | O o1, O o2 ->
- V_Offsetmap.narrow_reinterpret o1 o2 >>-: (fun o -> O o)
-
- (* Simple values cannot be injected because we do not known their type
- (hence size in bits *)
- let zero = Top
- let one = Top
- let top_int = Top
-
- let inject_int typ i =
- try
- let size = Integer.of_int (Cil.bitsSizeOf typ) in
- O (inject ~size (V.inject_int i))
- with Cil.SizeOfError _ -> Top
-
- let assume_non_zero v = `Unknown v
- let assume_bounded _ _ v = `Unknown v
- let assume_not_nan ~assume_finite:_ _ v = `Unknown v
- let assume_pointer v = `Unknown v
- let assume_comparable _ v1 v2 = `Unknown (v1, v2)
-
- let constant e _c =
- if store_redundant then
- match Cil.constFoldToInt e with
- | Some i -> inject_int (Cil.typeOf e) i
- | None -> Top
- else Top
-
- let resolve_functions _ = `Top, true (* TODO: extract value *)
- let replace_base substitution = function
- | Top -> Top
- | O offsm ->
- let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
- O (Cvalue.V_Offsetmap.map_on_values f offsm)
-
- let forward_unop _typ op o =
- let o' = match o, op with
- | Top, _ | _, (Neg | LNot) -> Top
- | O o, BNot -> O (bnot o)
- in
- `Value o'
-
- let forward_binop _typ op o1 o2 =
- let o' =
- match o1, o2, op with
- | O _o1, O _o2, (Shiftlt | Shiftrt) ->
- (* It is inconvenient to handle shift here, because we need a
- constant for o2 *)
- Top
- | O o1, O o2, BAnd -> O (bitwise_and o1 o2)
- | O o1, O o2, BOr -> O (bitwise_or o1 o2)
- | O o1, O o2, BXor -> O (bitwise_xor o1 o2)
- | _ -> Top
- in
- `Value o'
-
- let backward_binop ~input_type:_ ~resulting_type:_ _op ~left:_ ~right:_ ~result:_ =
- `Value (None, None)
-
- let backward_unop ~typ_arg:_ _unop ~arg:_ ~res:_ = `Value None
-
- let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
- `Value None
-
- let rewrap_integer _range o = o
-
- let forward_cast ~src_type ~dst_type o =
- let open Eval_typ in
- match o, src_type, dst_type with
- | O o, (TSInt src | TSPtr src), (TSInt dst | TSPtr dst) ->
- let old_size = Int.of_int src.i_bits in
- let new_size = Int.of_int dst.i_bits in
- let signed = src.i_signed in
- `Value (O (cast ~old_size ~new_size ~signed o))
- | _ -> `Value Top
-
+ let registered = Abstractions.Value.register { key ; value = (module Value) }
+ include Value
end
-
-module CvalueOffsm : Abstract.Value.Internal with type t = V.t * offsm_or_top
-= struct
- include Value_product.Make (Main_values.CVal) (Offsm)
-
- let structure =
- Abstract.Value.(Node (Leaf (Main_values.CVal.key, (module Main_values.CVal)),
- Leaf (Offsm.key, (module Offsm))))
-
- let size typ = Integer.of_int (Cil.bitsSizeOf typ)
-
- (* Extract an offsetmap from a pair, by converting the value when needed. *)
- let to_offsm typ (v, o : t) =
- match o with
- | Top -> inject ~size:(size typ) v
- | O o -> o
-
- (* Ensure that the offsetmap component is not empty *)
- let strengthen_offsm typ (v, o as p : t) : t =
- if o = Top then
- (v, O (to_offsm typ p))
- else p
-
- (* Refine the value component according to the contents of the offsetmap *)
- let strengthen_v typ (v, o as p : t) : t or_bottom =
- match o with
- | Top -> `Value p
- | O o' ->
- let size = size typ in
- (* TODO: this should be done by the transfer function itself... *)
- let v = Cvalue_forward.reinterpret typ v in
- let v_o = V_Or_Uninitialized.get_v (basic_find ~size o') in
- let v_o = Cvalue_forward.reinterpret typ v_o in
- let v = V.narrow v v_o in
- if V.is_bottom v then `Bottom else `Value (v, o)
-
- let forward_unop typ op p =
- match op with
- | BNot ->
- let p' = strengthen_offsm typ p in
- forward_unop typ op p' >>- fun p'' ->
- strengthen_v typ p''
- | _ -> forward_unop typ op p
-
- let forward_binop typ op l r =
- match op with
- | BAnd | BOr | BXor ->
- let l = strengthen_offsm typ l in
- let r = strengthen_offsm typ r in
- forward_binop typ op l r >>- fun p ->
- strengthen_v typ p
- | Shiftlt | Shiftrt ->
- let (v_r, _) = r in
- let (v_l, _) = l in
- begin
- try
- let i = V.project_ival v_r in
- let i = Ival.project_int i in
- let size = size typ in
- let signed = Bit_utils.is_signed_int_enum_pointer typ in
- let dir = if op = Shiftlt then Left else Right in
- let o = shift ~size ~signed (to_offsm typ l) dir i in
- Main_values.CVal.forward_binop typ op v_l v_r >>-: fun v ->
- v, O o
- with V.Not_based_on_null | Ival.Not_Singleton_Int ->
- forward_binop typ op l r
- end
- | _ -> forward_binop typ op l r
-
-end
+(* -------------------------------------------------------------------------- *)
+(* Reduced product between Cvalues and Offsetmaps values *)
+(* -------------------------------------------------------------------------- *)
+
+let size typ = Integer.of_int (Cil.bitsSizeOf typ)
+
+(* Extract an offsetmap from a pair, by converting the value when needed. *)
+let to_offsm typ v = function
+ | Top -> inject ~size:(size typ) v
+ | O o -> o
+
+(* Refine the cvalue according to the contents of the offsetmap. *)
+let strengthen_v typ v offsm : Cvalue.V.t or_bottom =
+ let size = size typ in
+ (* TODO: this should be done by the transfer function itself... *)
+ let v = Cvalue_forward.reinterpret typ v in
+ let v_o = V_Or_Uninitialized.get_v (basic_find ~size offsm) in
+ let v_o = Cvalue_forward.reinterpret typ v_o in
+ let v = V.narrow v v_o in
+ if V.is_bottom v then `Bottom else `Value v
+
+let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
+ let module Val = Abstraction.Val in
+ match Val.get Main_values.CVal.key, Val.get Offsm.key with
+ | None, _ | _, None -> (module Abstraction)
+ | Some get_cvalue, Some get_offsm ->
+ let module Value = struct
+ include Abstraction.Val
+
+ let set_cvalue = set Main_values.CVal.key
+ let set_offsm = set Offsm.key
+
+ let to_offsm typ t = to_offsm typ (get_cvalue t) (get_offsm t)
+
+ (* Ensure that the offsetmap component is not empty. *)
+ let strengthen_offsm typ t = set_offsm (O (to_offsm typ t)) t
+
+ (* Refine the cvalue component according to the offsetmap component. *)
+ let strengthen_v typ t =
+ match get_offsm t with
+ | Top -> `Value t
+ | O o ->
+ let* v = strengthen_v typ (get_cvalue t) o in
+ `Value (set_cvalue v t)
+
+ let forward_unop typ op t =
+ match op with
+ | BNot ->
+ let t = strengthen_offsm typ t in
+ let* t = forward_unop typ op t in
+ strengthen_v typ t
+ | _ -> forward_unop typ op t
+
+ let forward_binop typ op l r =
+ match op with
+ | BAnd | BOr | BXor ->
+ let l = strengthen_offsm typ l
+ and r = strengthen_offsm typ r in
+ let* t = forward_binop typ op l r in
+ strengthen_v typ t
+ | Shiftlt | Shiftrt ->
+ let* p = forward_binop typ op l r in
+ begin
+ try
+ let i = get_cvalue r |> V.project_ival |> Ival.project_int in
+ let size = size typ in
+ let signed = Bit_utils.is_signed_int_enum_pointer typ in
+ let dir = if op = Shiftlt then Left else Right in
+ let offsm = shift ~size ~signed (to_offsm typ l) dir i in
+ `Value (set_offsm (O offsm) p)
+ with V.Not_based_on_null | Ival.Not_Singleton_Int -> `Value p
+ end
+ | _ -> forward_binop typ op l r
+ end in
+ (module struct
+ include Abstraction
+ module Val = Value
+ end)
diff --git a/src/plugins/eva/values/offsm_value.mli b/src/plugins/eva/values/offsm_value.mli
index cae5bd0efeec1484b5605279916b1ab56403e7c5..2cf4b088ae641e81addd04b0c3311f4a23ae4704 100644
--- a/src/plugins/eva/values/offsm_value.mli
+++ b/src/plugins/eva/values/offsm_value.mli
@@ -26,6 +26,8 @@ val cast :
old_size: Integer.t -> new_size: Integer.t -> signed: bool ->
Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.t
-module Offsm : Abstract_value.Leaf with type t = offsm_or_top
-
-module CvalueOffsm : Abstract.Value.Internal with type t = Cvalue.V.t * offsm_or_top
+module Offsm : sig
+ include Abstract_value.S with type t = offsm_or_top
+ val key : t Abstract_value.key
+ val registered : t Abstractions.Value.registered
+end
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index d60458ec1e0ed6eeb36d4bb26b0b54476b6ad2d8..9ac0956e0dd4343e5b369f0bb60f928b848f40ea 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -25,321 +25,326 @@ open Eval
open Abstract_interp
(** Sign domain: abstraction of integer numerical values by their signs. *)
-
-type signs = {
- pos: bool; (** true: maybe positive, false: never positive *)
- zero: bool; (** true: maybe zero, false: never zero *)
- neg: bool; (** true: maybe negative, false: never negative *)
-}
-
-let top = { pos = true; zero = true; neg = true }
-let pos_or_zero = { pos = true; zero = true; neg = false }
-let pos = { pos = true; zero = false; neg = false }
-let neg_or_zero = { pos = false; zero = true; neg = true }
-let neg = { pos = false; zero = false; neg = true }
-let zero = { pos = false; zero = true; neg = false }
-let one = { pos = true; zero = false; neg = false }
-let non_zero = { pos = true; zero = false; neg = true }
-let ge_zero v = not v.neg
-let le_zero v = not v.pos
-
-(* Bottom is a special value (`Bottom) in Eva, and need not be part of
- the lattice. Here, we have a value which is equivalent to it, defined
- there only for commodity. *)
-let empty = { pos = false; zero = false; neg = false }
-
-(* Datatypes are Frama-C specific modules used among other things for
- serialization. There is no need to understand them in detail.
- They are created mostly via copy/paste of templates. *)
-include Datatype.Make(struct
- type t = signs
- include Datatype.Serializable_undefined
- let compare = Stdlib.compare
- let equal = Datatype.from_compare
- let hash = Hashtbl.hash
- let reprs = [top]
- let name = "Value.Sign_values.signs"
- let pretty fmt v =
- Format.fprintf fmt "%s%s%s"
- (if v.neg then "-" else "")
- (if v.zero then "0" else "")
- (if v.pos then "+" else "")
- end)
-let pretty_debug = pretty
-let pretty_typ _ = pretty
-
-(* Inclusion: test inclusion of each field. *)
-let is_included v1 v2 =
- let bincl b1 b2 = (not b1) || b2 in
- bincl v1.pos v2.pos && bincl v1.zero v2.zero && bincl v1.neg v2.neg
-
-(* Join of the lattice: pointwise logical or. *)
-let join v1 v2 = {
- pos = v1.pos || v2.pos;
- zero = v1.zero || v2.zero;
- neg = v1.neg || v2.neg;
-}
-
-(* Meet of the lattice (called 'narrow' in Eva for historical reasons).
- We detect the case where the values have incompatible concretization,
- and report this as `Bottom. *)
-let narrow v1 v2 =
- let r = {
- pos = v1.pos && v2.pos;
- zero = v1.zero && v2.zero;
- neg = v1.neg && v2.neg;
- } in
- if r = empty then `Bottom else `Value r
-
-let top_int = top
-
-(* [inject_int] creates an abstract value corresponding to the singleton [i]. *)
-let inject_int _ i =
- if Integer.lt i Integer.zero then neg
- else if Integer.gt i Integer.zero then pos
- else zero
-
-let constant _ = function
- | CInt64 (i, _, _) -> inject_int () i
- | _ -> top
-
-(* Extracting function pointers from an abstraction. Not implemented
- precisely *)
-let resolve_functions _ = `Top, true
-
-let replace_base _substitution t = t
-
-(** {2 Alarms} *)
-
-let assume_non_zero v =
- if equal v zero
- then `False
- else if v.zero
- then `Unknown {v with zero = false}
- else `True
-
-(* TODO: use the bound to reduce the value when possible. *)
-let assume_bounded _ _ v = `Unknown v
-
-let assume_not_nan ~assume_finite:_ _ v = `Unknown v
-let assume_pointer v = `Unknown v
-let assume_comparable _ v1 v2 = `Unknown (v1, v2)
-
-(** {2 Forward transfer functions} *)
-
-(* Functions [neg_unop], [plus], [mul] and [div] below are forward transformers
- for the mathematical operations -, +, *, /. The potential overflows and
- wrappings for the operations on machine integers are taken into account by
- the functions [truncate_integer] and [rewrap_integer]. *)
-
-let neg_unop v = { v with neg = v.pos; pos = v.neg }
-
-let bitwise_not typ v =
- match Cil.unrollType typ with
- | TInt (ikind, _) | TEnum ({ekind=ikind}, _) ->
- if Cil.isSigned ikind
- then { pos = v.neg; neg = v.pos || v.zero; zero = v.neg }
- else { pos = v.pos || v.zero; neg = false; zero = v.pos }
- | _ -> top
-
-let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
-
-let forward_unop typ op v =
- match op with
- | Neg -> `Value (neg_unop v)
- | BNot -> `Value (bitwise_not typ v)
- | LNot -> `Value (logical_not v)
-
-let plus v1 v2 =
- let neg = v1.neg || v2.neg in
- let pos = v1.pos || v2.pos in
- let same_sign v1 v2 =
- (le_zero v1 && le_zero v2) || (ge_zero v1 && ge_zero v2)
- in
- let zero = not (same_sign v1 v2) || (v1.zero && v2.zero) in
- { neg; pos; zero }
-
-let mul v1 v2 =
- let pos = (v1.pos && v2.pos) || (v1.neg && v2.neg) in
- let neg = (v1.pos && v2.neg) || (v1.neg && v2.pos) in
- let zero = v1.zero || v2.zero in
- { neg; pos; zero }
-
-let div v1 v2 =
- let pos = (v1.pos && v2.pos) || (v1.neg && v2.neg) in
- let neg = (v1.pos && v2.neg) || (v1.neg && v2.pos) in
- let zero = true in (* zero can appear with large enough v2 *)
- { neg; pos; zero }
-
-(* The implementation of the bitwise operators below relies on this table
- giving the sign of the result according to the sign of both operands.
-
- v1 v2 v1&v2 v1|v2 v1^v2
- -----------------------------------
- | + + +0 + +0
- | + 0 0 + +
- | + - +0 - -
- | 0 + 0 + +
- | 0 0 0 0 0
- | 0 - 0 - -
- | - + +0 - -
- | - 0 0 - -
- | - - - - +0
-*)
-
-let bitwise_and v1 v2 =
- let pos = (v1.pos && (v2.pos || v2.neg)) || (v2.pos && v1.neg) in
- let neg = v1.neg && v2.neg in
- let zero = v1.zero || v1.pos || v2.zero || v2.pos in
- { neg; pos; zero }
-
-let bitwise_or v1 v2 =
- let pos = (v1.pos && (v2.pos || v2.zero)) || (v1.zero && v2.pos) in
- let neg = v1.neg || v2.neg in
- let zero = v1.zero && v2.zero in
- { neg; pos; zero }
-
-let bitwise_xor v1 v2 =
- let pos =
- (v1.pos && v2.pos) || (v1.pos && v2.zero) || (v1.zero && v2.pos)
- || (v1.neg && v2.neg)
- in
- let neg =
- (v1.neg && (v2.pos || v2.zero)) ||
- (v2.neg && (v1.pos || v1.zero))
- in
- let zero = (v1.zero && v2.zero) || (v1.pos && v2.pos) || (v1.neg && v2.neg) in
- { neg; pos; zero }
-
-let logical_and v1 v2 =
- let pos = (v1.pos || v1.neg) && (v2.pos || v2.neg) in
- let neg = false in
- let zero = v1.zero || v2.zero in
- { pos; neg; zero }
-
-let logical_or v1 v2 =
- let pos = v1.pos || v1.neg || v2.pos || v2.neg in
- let neg = false in
- let zero = v1.zero && v2.zero in
- { pos; neg; zero }
-
-let forward_binop _ op v1 v2 =
- match op with
- | PlusA -> `Value (plus v1 v2)
- | MinusA -> `Value (plus v1 (neg_unop v2))
- | Mult -> `Value (mul v1 v2)
- | Div -> if equal zero v2 then `Bottom else `Value (div v1 v2)
- | BAnd -> `Value (bitwise_and v1 v2)
- | BOr -> `Value (bitwise_or v1 v2)
- | BXor -> `Value (bitwise_xor v1 v2)
- | LAnd -> `Value (logical_and v1 v2)
- | LOr -> `Value (logical_or v1 v2)
- | _ -> `Value top
-
-let rewrap_integer range v =
- if equal v zero then v
- else if range.Eval_typ.i_signed then top else pos_or_zero
-
-(* Casts from type [src_typ] to type [dst_typ]. As downcasting can wrap,
- we only handle upcasts precisely *)
-let forward_cast ~src_type ~dst_type v =
- let open Eval_typ in
- match src_type, dst_type with
- | TSInt range_src, TSInt range_dst ->
- if equal v zero then `Value v else
- if range_inclusion range_src range_dst then
- `Value v (* upcast *)
- else if range_dst.i_signed then
- `Value top (*dst_typ is signed, return all possible values*)
- else
- `Value pos_or_zero (* dst_typ is unsigned *)
- | _ ->
- (* at least one non-integer type. not handled precisely. *)
- `Value top
-
-
-(** {2 Backward transfer functions} *)
-
-(* Backward transfer functions are used to reduce the abstraction of a value,
- knowing other information. For example '[0+] > [0]' means that the
- first value can only be [+].
-
- In the OCaml signatures, 'None' means 'I cannot reduce'. *)
-
-(* Value to return when no reduction is possible *)
-let unreduced = `Value None
-(* Function to use when a reduction is possible *)
-let reduced v = `Value (Some v)
-
-(* This function must reduce the value [right] assuming that the
- comparison [left op right] holds. *)
-let backward_comp_right op ~left ~right =
- let open Abstract_interp.Comp in
- match op with
- | Eq ->
- narrow left right >>- reduced
- | Ne ->
- if equal left zero then
- narrow right non_zero >>- reduced
- else unreduced
- | Le ->
- if ge_zero left then
- (* [left] is positive or zero. Hence, [right] is at least also positive
- or zero. *)
- if left.zero then
- (* [left] may be zero, [right] is positive or zero *)
- narrow right pos_or_zero >>- reduced
+module Value = struct
+
+ type signs = {
+ pos: bool; (** true: maybe positive, false: never positive *)
+ zero: bool; (** true: maybe zero, false: never zero *)
+ neg: bool; (** true: maybe negative, false: never negative *)
+ }
+
+ let top = { pos = true; zero = true; neg = true }
+ let pos_or_zero = { pos = true; zero = true; neg = false }
+ let pos = { pos = true; zero = false; neg = false }
+ let neg_or_zero = { pos = false; zero = true; neg = true }
+ let neg = { pos = false; zero = false; neg = true }
+ let zero = { pos = false; zero = true; neg = false }
+ let one = { pos = true; zero = false; neg = false }
+ let non_zero = { pos = true; zero = false; neg = true }
+ let ge_zero v = not v.neg
+ let le_zero v = not v.pos
+
+ (* Bottom is a special value (`Bottom) in Eva, and need not be part of
+ the lattice. Here, we have a value which is equivalent to it, defined
+ there only for commodity. *)
+ let empty = { pos = false; zero = false; neg = false }
+
+ (* Datatypes are Frama-C specific modules used among other things for
+ serialization. There is no need to understand them in detail.
+ They are created mostly via copy/paste of templates. *)
+ include Datatype.Make(struct
+ type t = signs
+ include Datatype.Serializable_undefined
+ let compare = Stdlib.compare
+ let equal = Datatype.from_compare
+ let hash = Hashtbl.hash
+ let reprs = [top]
+ let name = "Value.Sign_values.signs"
+ let pretty fmt v =
+ Format.fprintf fmt "%s%s%s"
+ (if v.neg then "-" else "")
+ (if v.zero then "0" else "")
+ (if v.pos then "+" else "")
+ end)
+ let pretty_debug = pretty
+ let pretty_typ _ = pretty
+
+ (* Inclusion: test inclusion of each field. *)
+ let is_included v1 v2 =
+ let bincl b1 b2 = (not b1) || b2 in
+ bincl v1.pos v2.pos && bincl v1.zero v2.zero && bincl v1.neg v2.neg
+
+ (* Join of the lattice: pointwise logical or. *)
+ let join v1 v2 = {
+ pos = v1.pos || v2.pos;
+ zero = v1.zero || v2.zero;
+ neg = v1.neg || v2.neg;
+ }
+
+ (* Meet of the lattice (called 'narrow' in Eva for historical reasons).
+ We detect the case where the values have incompatible concretization,
+ and report this as `Bottom. *)
+ let narrow v1 v2 =
+ let r = {
+ pos = v1.pos && v2.pos;
+ zero = v1.zero && v2.zero;
+ neg = v1.neg && v2.neg;
+ } in
+ if r = empty then `Bottom else `Value r
+
+ let top_int = top
+
+ (* [inject_int] creates an abstract value corresponding to the singleton [i]. *)
+ let inject_int _ i =
+ if Integer.lt i Integer.zero then neg
+ else if Integer.gt i Integer.zero then pos
+ else zero
+
+ let constant _ = function
+ | CInt64 (i, _, _) -> inject_int () i
+ | _ -> top
+
+ (* Extracting function pointers from an abstraction. Not implemented
+ precisely *)
+ let resolve_functions _ = `Top, true
+
+ let replace_base _substitution t = t
+
+ (** {2 Alarms} *)
+
+ let assume_non_zero v =
+ if equal v zero
+ then `False
+ else if v.zero
+ then `Unknown {v with zero = false}
+ else `True
+
+ (* TODO: use the bound to reduce the value when possible. *)
+ let assume_bounded _ _ v = `Unknown v
+
+ let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
+ let assume_comparable _ v1 v2 = `Unknown (v1, v2)
+
+ (** {2 Forward transfer functions} *)
+
+ (* Functions [neg_unop], [plus], [mul] and [div] below are forward transformers
+ for the mathematical operations -, +, *, /. The potential overflows and
+ wrappings for the operations on machine integers are taken into account by
+ the functions [truncate_integer] and [rewrap_integer]. *)
+
+ let neg_unop v = { v with neg = v.pos; pos = v.neg }
+
+ let bitwise_not typ v =
+ match Cil.unrollType typ with
+ | TInt (ikind, _) | TEnum ({ekind=ikind}, _) ->
+ if Cil.isSigned ikind
+ then { pos = v.neg; neg = v.pos || v.zero; zero = v.neg }
+ else { pos = v.pos || v.zero; neg = false; zero = v.pos }
+ | _ -> top
+
+ let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
+
+ let forward_unop typ op v =
+ match op with
+ | Neg -> `Value (neg_unop v)
+ | BNot -> `Value (bitwise_not typ v)
+ | LNot -> `Value (logical_not v)
+
+ let plus v1 v2 =
+ let neg = v1.neg || v2.neg in
+ let pos = v1.pos || v2.pos in
+ let same_sign v1 v2 =
+ (le_zero v1 && le_zero v2) || (ge_zero v1 && ge_zero v2)
+ in
+ let zero = not (same_sign v1 v2) || (v1.zero && v2.zero) in
+ { neg; pos; zero }
+
+ let mul v1 v2 =
+ let pos = (v1.pos && v2.pos) || (v1.neg && v2.neg) in
+ let neg = (v1.pos && v2.neg) || (v1.neg && v2.pos) in
+ let zero = v1.zero || v2.zero in
+ { neg; pos; zero }
+
+ let div v1 v2 =
+ let pos = (v1.pos && v2.pos) || (v1.neg && v2.neg) in
+ let neg = (v1.pos && v2.neg) || (v1.neg && v2.pos) in
+ let zero = true in (* zero can appear with large enough v2 *)
+ { neg; pos; zero }
+
+ (* The implementation of the bitwise operators below relies on this table
+ giving the sign of the result according to the sign of both operands.
+
+ v1 v2 v1&v2 v1|v2 v1^v2
+ -----------------------------------
+ | + + +0 + +0
+ | + 0 0 + +
+ | + - +0 - -
+ | 0 + 0 + +
+ | 0 0 0 0 0
+ | 0 - 0 - -
+ | - + +0 - -
+ | - 0 0 - -
+ | - - - - +0
+ *)
+
+ let bitwise_and v1 v2 =
+ let pos = (v1.pos && (v2.pos || v2.neg)) || (v2.pos && v1.neg) in
+ let neg = v1.neg && v2.neg in
+ let zero = v1.zero || v1.pos || v2.zero || v2.pos in
+ { neg; pos; zero }
+
+ let bitwise_or v1 v2 =
+ let pos = (v1.pos && (v2.pos || v2.zero)) || (v1.zero && v2.pos) in
+ let neg = v1.neg || v2.neg in
+ let zero = v1.zero && v2.zero in
+ { neg; pos; zero }
+
+ let bitwise_xor v1 v2 =
+ let pos =
+ (v1.pos && v2.pos) || (v1.pos && v2.zero) || (v1.zero && v2.pos)
+ || (v1.neg && v2.neg)
+ in
+ let neg =
+ (v1.neg && (v2.pos || v2.zero)) ||
+ (v2.neg && (v1.pos || v1.zero))
+ in
+ let zero = (v1.zero && v2.zero) || (v1.pos && v2.pos) || (v1.neg && v2.neg) in
+ { neg; pos; zero }
+
+ let logical_and v1 v2 =
+ let pos = (v1.pos || v1.neg) && (v2.pos || v2.neg) in
+ let neg = false in
+ let zero = v1.zero || v2.zero in
+ { pos; neg; zero }
+
+ let logical_or v1 v2 =
+ let pos = v1.pos || v1.neg || v2.pos || v2.neg in
+ let neg = false in
+ let zero = v1.zero && v2.zero in
+ { pos; neg; zero }
+
+ let forward_binop _ op v1 v2 =
+ match op with
+ | PlusA -> `Value (plus v1 v2)
+ | MinusA -> `Value (plus v1 (neg_unop v2))
+ | Mult -> `Value (mul v1 v2)
+ | Div -> if equal zero v2 then `Bottom else `Value (div v1 v2)
+ | BAnd -> `Value (bitwise_and v1 v2)
+ | BOr -> `Value (bitwise_or v1 v2)
+ | BXor -> `Value (bitwise_xor v1 v2)
+ | LAnd -> `Value (logical_and v1 v2)
+ | LOr -> `Value (logical_or v1 v2)
+ | _ -> `Value top
+
+ let rewrap_integer range v =
+ if equal v zero then v
+ else if range.Eval_typ.i_signed then top else pos_or_zero
+
+ (* Casts from type [src_typ] to type [dst_typ]. As downcasting can wrap,
+ we only handle upcasts precisely *)
+ let forward_cast ~src_type ~dst_type v =
+ let open Eval_typ in
+ match src_type, dst_type with
+ | TSInt range_src, TSInt range_dst ->
+ if equal v zero then `Value v else
+ if range_inclusion range_src range_dst then
+ `Value v (* upcast *)
+ else if range_dst.i_signed then
+ `Value top (*dst_typ is signed, return all possible values*)
else
- (* [left] is strictly positive, hence so is [right] *)
+ `Value pos_or_zero (* dst_typ is unsigned *)
+ | _ ->
+ (* at least one non-integer type. not handled precisely. *)
+ `Value top
+
+
+ (** {2 Backward transfer functions} *)
+
+ (* Backward transfer functions are used to reduce the abstraction of a value,
+ knowing other information. For example '[0+] > [0]' means that the
+ first value can only be [+].
+
+ In the OCaml signatures, 'None' means 'I cannot reduce'. *)
+
+ (* Value to return when no reduction is possible *)
+ let unreduced = `Value None
+ (* Function to use when a reduction is possible *)
+ let reduced v = `Value (Some v)
+
+ (* This function must reduce the value [right] assuming that the
+ comparison [left op right] holds. *)
+ let backward_comp_right op ~left ~right =
+ let open Abstract_interp.Comp in
+ match op with
+ | Eq ->
+ narrow left right >>- reduced
+ | Ne ->
+ if equal left zero then
+ narrow right non_zero >>- reduced
+ else unreduced
+ | Le ->
+ if ge_zero left then
+ (* [left] is positive or zero. Hence, [right] is at least also positive
+ or zero. *)
+ if left.zero then
+ (* [left] may be zero, [right] is positive or zero *)
+ narrow right pos_or_zero >>- reduced
+ else
+ (* [left] is strictly positive, hence so is [right] *)
+ narrow right pos >>- reduced
+ else unreduced
+ | Lt ->
+ if ge_zero left then
narrow right pos >>- reduced
- else unreduced
- | Lt ->
- if ge_zero left then
- narrow right pos >>- reduced
- else unreduced
- | Ge ->
- if le_zero left then
- if left.zero then
- narrow right neg_or_zero >>- reduced
- else
+ else unreduced
+ | Ge ->
+ if le_zero left then
+ if left.zero then
+ narrow right neg_or_zero >>- reduced
+ else
+ narrow right neg >>- reduced
+ else unreduced
+ | Gt ->
+ if le_zero left then
narrow right neg >>- reduced
- else unreduced
- | Gt ->
- if le_zero left then
- narrow right neg >>- reduced
- else unreduced
-
-(* This functions must reduce the values [left] and [right], assuming
- that [left op right == result] holds. Currently, it is only implemented
- for comparison operators. *)
-let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
- match op with
- | Ne | Eq | Le | Lt | Ge | Gt ->
- let op = Eva_utils.conv_comp op in
- if equal zero result then
- (* The comparison is false, as it always evaluate to false. Reduce by the
- fact that the inverse comparison is true. *)
- let op = Comp.inv op in
- backward_comp_right op ~left ~right >>- fun right' ->
- backward_comp_right (Comp.sym op) ~left:right ~right:left >>- fun left' ->
- `Value (left', right')
- else if not result.zero then
- (* The comparison always hold, as it never evaluates to false. *)
- backward_comp_right op ~left ~right >>- fun right' ->
- backward_comp_right (Comp.sym op) ~left:right ~right:left >>- fun left' ->
- `Value (left', right')
- else
- (* The comparison may or may not hold, it is not possible to reduce *)
- `Value (None, None)
- | _ -> `Value (None, None)
-
-(* Not implemented precisely *)
-let backward_unop ~typ_arg:_ _op ~arg:_ ~res:_ = `Value None
-(* Not implemented precisely *)
-let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
+ else unreduced
+
+ (* This functions must reduce the values [left] and [right], assuming
+ that [left op right == result] holds. Currently, it is only implemented
+ for comparison operators. *)
+ let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
+ match op with
+ | Ne | Eq | Le | Lt | Ge | Gt ->
+ let op = Eva_utils.conv_comp op in
+ if equal zero result then
+ (* The comparison is false, as it always evaluate to false. Reduce by the
+ fact that the inverse comparison is true. *)
+ let op = Comp.inv op in
+ backward_comp_right op ~left ~right >>- fun right' ->
+ backward_comp_right (Comp.sym op) ~left:right ~right:left >>- fun left' ->
+ `Value (left', right')
+ else if not result.zero then
+ (* The comparison always hold, as it never evaluates to false. *)
+ backward_comp_right op ~left ~right >>- fun right' ->
+ backward_comp_right (Comp.sym op) ~left:right ~right:left >>- fun left' ->
+ `Value (left', right')
+ else
+ (* The comparison may or may not hold, it is not possible to reduce *)
+ `Value (None, None)
+ | _ -> `Value (None, None)
+
+ (* Not implemented precisely *)
+ let backward_unop ~typ_arg:_ _op ~arg:_ ~res:_ = `Value None
+ (* Not implemented precisely *)
+ let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
+
+end
(** {2 Misc} *)
(* Eva boilerplate, used to retrieve the domain. *)
let key = Structure.Key_Value.create_key "sign_values"
+let registered = Abstractions.Value.register { key ; value = (module Value) }
+include Value
diff --git a/src/plugins/eva/values/sign_value.mli b/src/plugins/eva/values/sign_value.mli
index aa4030e1e386fdf7d2ee8e05e1f65fdbd6d63d85..7c8853fbd1c253af2702d31751aa0746714b5c0e 100644
--- a/src/plugins/eva/values/sign_value.mli
+++ b/src/plugins/eva/values/sign_value.mli
@@ -28,6 +28,7 @@ type signs = {
neg: bool; (** true: maybe negative, false: never negative *)
}
-include Abstract_value.Leaf with type t = signs
-
+include Abstract_value.S with type t = signs
+val key : t Abstract_value.key
val pretty_debug: t Pretty_utils.formatter
+val registered : t Abstractions.Value.registered
diff --git a/src/plugins/eva/values/value_product.ml b/src/plugins/eva/values/value_product.ml
index d0f99098c43092082b9c585ceebec1623ca6ba34..8f2101a68cd756802b98f379afae7fbefb4d47f9 100644
--- a/src/plugins/eva/values/value_product.ml
+++ b/src/plugins/eva/values/value_product.ml
@@ -22,6 +22,28 @@
open Eval
+(* Intersects the truth values [t1] and [t2] coming from [assume_] functions
+ from both abstract values. [v1] and [v2] are the initial values leading to
+ these truth values, that may be reduced by the assumption. [combine]
+ combines values from both abstract values into values of the product. *)
+let narrow_any_truth combine (v1, t1) (v2, t2) = match t1, t2 with
+ | `Unreachable, _ | _, `Unreachable
+ | (`True | `TrueReduced _), `False
+ | `False, (`True | `TrueReduced _) -> `Unreachable
+ | `False, _ | _, `False -> `False
+ | `Unknown v1, `Unknown v2 -> `Unknown (combine v1 v2)
+ | (`Unknown v1 | `TrueReduced v1), `True -> `TrueReduced (combine v1 v2)
+ | `True, (`Unknown v2 | `TrueReduced v2) -> `TrueReduced (combine v1 v2)
+ | (`Unknown v1 | `TrueReduced v1),
+ (`Unknown v2 | `TrueReduced v2) -> `TrueReduced (combine v1 v2)
+ | `True, `True -> `True
+
+let narrow_truth x y = narrow_any_truth (fun left right -> left, right) x y
+
+let narrow_truth_pair x y =
+ let combine (l1, l2) (r1, r2) = (l1, r1), (l2, r2) in
+ narrow_any_truth combine x y
+
module Make
(Left: Abstract_value.S)
(Right: Abstract_value.S)
@@ -48,24 +70,6 @@ module Make
let top_int = Left.top_int, Right.top_int
let inject_int typ i = Left.inject_int typ i, Right.inject_int typ i
- (* Intersects the truth values [t1] and [t2] coming from [assume_] functions
- from both abstract values. [v1] and [v2] are the initial values leading to
- these truth values, that may be reduced by the assumption. [combine]
- combines values from both abstract values into values of the product. *)
- let narrow_any_truth combine (v1, t1) (v2, t2) = match t1, t2 with
- | `Unreachable, _ | _, `Unreachable
- | (`True | `TrueReduced _), `False
- | `False, (`True | `TrueReduced _) -> `Unreachable
- | `False, _ | _, `False -> `False
- | `Unknown v1, `Unknown v2 -> `Unknown (combine v1 v2)
- | (`Unknown v1 | `TrueReduced v1), `True -> `TrueReduced (combine v1 v2)
- | `True, (`Unknown v2 | `TrueReduced v2) -> `TrueReduced (combine v1 v2)
- | (`Unknown v1 | `TrueReduced v1),
- (`Unknown v2 | `TrueReduced v2) -> `TrueReduced (combine v1 v2)
- | `True, `True -> `True
-
- let narrow_truth = narrow_any_truth (fun left right -> left, right)
-
let assume_non_zero (left, right) =
let left_truth = Left.assume_non_zero left
and right_truth = Right.assume_non_zero right in
@@ -89,8 +93,7 @@ module Make
let assume_comparable op (l1, r1) (l2, r2) =
let left_truth = Left.assume_comparable op l1 l2
and right_truth = Right.assume_comparable op r1 r2 in
- let combine (l1, l2) (r1, r2) = (l1, r1), (l2, r2) in
- narrow_any_truth combine ((l1, l2), left_truth) ((r1, r2), right_truth)
+ narrow_truth_pair ((l1, l2), left_truth) ((r1, r2), right_truth)
let constant expr constant =
let left = Left.constant expr constant
diff --git a/src/plugins/eva/values/value_product.mli b/src/plugins/eva/values/value_product.mli
index 43aca79e8140ec25f9c5ea50b33a68ba157a42f8..f53f265b25b1670f777045be22892c8f096c665b 100644
--- a/src/plugins/eva/values/value_product.mli
+++ b/src/plugins/eva/values/value_product.mli
@@ -22,6 +22,18 @@
(** Cartesian product of two value abstractions. *)
+type 'v truth := 'v Abstract_value.truth
+
+(** [narrow_truth (v1, t1) (v2, t2)] intersects the truth values [t1] and [t2]
+ resulting from [assume_] functions for abstract values [v1] and [v2]
+ (that may be reduced by the assumption). *)
+val narrow_truth: 'a * 'a truth -> 'b * 'b truth -> ('a * 'b) truth
+
+(** Same as narrow_truth for truth values involving pairs of abstract values. *)
+val narrow_truth_pair:
+ ('a * 'a) * ('a * 'a) truth -> ('b * 'b) * ('b * 'b) truth ->
+ (('a * 'b) * ('a * 'b)) truth
+
module Make
(Left: Abstract_value.S)
(Right: Abstract_value.S)
diff --git a/tests/value/oracle_bitwise/addition.res.oracle b/tests/value/oracle_bitwise/addition.res.oracle
index 5bf7aa4f39c61e0f2a36094f97327d3f11610ef7..729310a2affcab008aba9cbf34a61e8629f09d58 100644
--- a/tests/value/oracle_bitwise/addition.res.oracle
+++ b/tests/value/oracle_bitwise/addition.res.oracle
@@ -4,9 +4,9 @@
< The imprecision originates from Arithmetic {addition.i:52}
---
> [eva] addition.i:52: Assigning imprecise value to p10.
-163a162
+162a161
> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
-165a165
+163a163
> {{ garbled mix of &{p2} (origin: Misaligned {addition.i:56}) }}
186c186
< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}