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/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/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..361129a8f603d1d4d0544aee9669c6cd85a87d33 100644
--- a/src/plugins/eva/domains/numerors/numerors_domain.ml
+++ b/src/plugins/eva/domains/numerors/numerors_domain.ml
@@ -158,8 +158,12 @@ let () =
in floating-point computations. No support of loops."
and experimental = true
and abstraction =
- { values = Single (module Numerors_value);
- domain = Domain (module Domain); }
+ { key = Domain.key ; domain = (module Domain)
+ ; values = Last Numerors_Value.registered
+ ; locations = Last Main_locations.PLoc.registered
+ }
+ (* { 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);
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..12dc544808c2848075ef0f4ed183726ab41e2487 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.mli
+++ b/src/plugins/eva/domains/numerors/numerors_value.mli
@@ -20,7 +20,9 @@
(* *)
(**************************************************************************)
-include Abstract_value.Leaf
+include Abstract_value.S
+val key : t Abstract_value.key
+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 20d2b3c3a4b4068fb1c15edae9ed19b9bd52004f..5ed7dc50d19f530741bc383290524037a2b6c2be 100644
--- a/src/plugins/eva/engine/abstractions.ml
+++ b/src/plugins/eva/engine/abstractions.ml
@@ -68,14 +68,16 @@ module Value = struct
it interactive. *)
module type Structured = Abstract.Value.Internal
module type Interactive = Abstract.Value.External
- type structured = (module Structured)
- type interactive = (module Interactive)
+ 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 =
- fun (module Structured) ->
- (module struct
+ let make_interactive : structured -> interactive = function
+ | Unit -> Unit
+ | Value (module Structured) ->
+ Value (module struct
include Structured
include Structure.Open (Abstract.Value) (Structured)
end)
@@ -86,23 +88,27 @@ module Value = struct
updating the structure. *)
let add : type v. v registered -> structured -> structured =
fun (key, input) structured ->
- let module Interactive = (val make_interactive structured) in
- if not (Interactive.mem key) then
- (module struct
+ 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 =
- let open Abstract.Value in
- Node (Interactive.structure, Leaf (key, input))
+ let structure = Node (Interactive.structure, Leaf (key, input))
end)
- else structured
+ | _ -> structured
(* The minimal value abstraction to use. It contains the CValue abstraction,
configured depending of the bitwise *)
- let init : structured =
- (module struct
- include Main_values.CVal
- let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
- end)
+ let init : structured = Unit
+
+ 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
@@ -223,34 +229,31 @@ module Location = struct
module Location : Abstract.Location.Internal with type value = value
end
- (* An interactive location is however quite simple, it is simply a location
- with the needed operators. *)
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. *)
- type 'v structured = (module Structured with type value = 'v)
- type 'v interactive = (module Interactive with type value = 'v)
+ 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 *)
- module Init (V : Value.Interactive) : Structured with type value = V.t =
- struct
- module CVal = Main_values.CVal
- let leaf = Abstract.Value.Leaf (CVal.key, (module CVal))
- module From = struct type value = CVal.t let structure = leaf end
- module Converter = Value.Converter (From) (V)
-
- type value = V.t
- module Value = V
- module Location = Location_lift.Make (Main_locations.PLoc) (Converter)
- end
+ let init (value : 'v value) : 'v structured = Unit value
+
+ 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 =
- fun (module Structured) ->
- (module struct
+ 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
@@ -258,6 +261,11 @@ module Location = struct
end)
end)
+ 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. Computing the values dependencies structure.
2. Computing the registered location structure. This steps starts by
@@ -268,37 +276,30 @@ module Location = struct
reduced product with the structured location, except if the last one is
Unit. In that case, we simply use the registered location. *)
let add : type v l. l registered -> v structured -> v structured =
- fun (module Registered) (module Structured) ->
- let dependencies = Value.outline Registered.dependencies in
- let registered : (module Abstract.Location.Internal with type value = v) =
- match Value.dec_eq dependencies Structured.Value.structure with
- | Some Eq ->
- (module struct
- include Registered
- let structure = Registered.structure
- end)
- | None ->
- let module From = struct
- type value = Registered.value
- let structure = dependencies
- end in
- let module Converter = Value.Converter (From) (Structured.Value) in
- (module Location_lift.Make (Registered) (Converter))
+ 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 location : (module Abstract.Location.Internal with type value = v) =
- let open Locations_product in
- let module Val = Structured.Value in
- let module Loc = Structured.Location in
- match Structured.Location.structure with
- | Unit -> registered
- | _ -> (module Same_value (Val) (val registered) (Loc))
+ 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
- (module struct
- type value = Structured.value
- module Value = Structured.Value
- module Location = (val location)
+ 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
@@ -502,9 +503,24 @@ module Domain = struct
with type value = value and type location = location
end
- type ('v, 'l) structured =
+ 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
+
+ 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))
+
+ 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 =
@@ -520,88 +536,93 @@ module Domain = struct
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. *)
- let add (type v l) (registered, mode) (structured : (v, l) 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 module Structured = (val structured) in
- let module Loc = Structured.Location in
- let module Val = Structured.Value in
- let module Dom = Structured.Domain in
- let domain : (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))
+ 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
- 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 registered.name in
- register_global_state (storage && not no_results) state
- end
- end in
- (* Restricts the domain according to [mode]. *)
- let domain : (v, l) structured_domain =
- match mode with
- | None -> (module Domain)
- | Some kf_modes ->
- let module Scope = struct let functions = kf_modes end in
- (module Domain_builder.Restrict (Val) (Domain) (Scope))
- in
- let domain : (v, l) structured_domain =
- match Abstract.Domain.(eq_structure Structured.Domain.structure Unit) with
- | Some Eq -> 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 (Val) ((val domain)) (Dom))
- in
- (module struct
- include Structured
- module Domain = (val domain)
- end : Structured with type value = v and type location = l)
+ 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
@@ -620,9 +641,9 @@ module Domain = struct
List.fold_left add_values Value.init domains |>
Value.make_interactive
in
- let module V = (val values) in
+ let module V = (val Value.assert_not_unit values) in
let locations =
- let init : V.t Location.structured = (module Location.Init (V)) in
+ 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
@@ -632,19 +653,12 @@ module Domain = struct
List.fold_left add_locations init domains |>
Location.make_interactive
in
- let module L = (val locations) in
- let domain : (V.t, L.location) structured_domain =
- (module Unit_domain.Make (V) (L))
+ 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 : (V.t, L.location) structured = (module struct
- type value = V.t
- type location = L.location
- module Value = V
- module Location = L
- module Domain = (val domain)
- end) in
let structured = List.fold_left (fun s d -> add d s) structured domains in
- let module Structured : Structured = (val structured) in
+ let module Structured : Structured = (val assert_not_unit structured) in
(module Structured)
end
@@ -652,7 +666,7 @@ end
(* --- Configuration -------------------------------------------------------- *)
-module Configuration = struct
+module Config = struct
module Mode = Datatype.Option (Domain_mode)
include Set.Make (struct
@@ -666,11 +680,16 @@ module Configuration = struct
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)
+
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 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
@@ -732,6 +751,15 @@ module type S = sig
with type value = Val.t and type location = Loc.location
end
+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
+
module Hooks = struct
let hooks = ref []
type hook = (module S) -> (module S)
@@ -745,33 +773,12 @@ module Open (Structured : Domain.Structured) : S = struct
module Dom = struct
include Structured.Domain
include Structure.Open (Abstract.Domain) (Structured.Domain)
-
- let get_cvalue = match get Cvalue_domain.State.key with
- | None -> None
- | Some get -> Some (fun s -> fst (get s))
-
- let get_cvalue_or_top = match get Cvalue_domain.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
end
-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
-end
-
let make config =
- let abstractions = Configuration.elements config |> Domain.build in
+ let abstractions = Config.elements config |> Domain.build in
let abstractions = (module Open (val abstractions) : S) in
Hooks.apply abstractions
-module Default = (val make (Configuration.configure ()))
+(* module Default = (val make (Config.configure ())) *)
diff --git a/src/plugins/eva/engine/abstractions.mli b/src/plugins/eva/engine/abstractions.mli
index 755e771a05094249fa2a75b9c937f40eace47109..0bc1abe9fc42815f36569bc71b60c5bfb24e8774 100644
--- a/src/plugins/eva/engine/abstractions.mli
+++ b/src/plugins/eva/engine/abstractions.mli
@@ -108,6 +108,15 @@ end
+module Config : sig
+ type t
+ val equal : t -> t -> bool
+ val singleton : string -> Domain.registered -> t
+ val configure : unit -> t
+end
+
+
+
module Reducer : sig
module type S = sig
include Abstract.Value.External
@@ -129,21 +138,22 @@ module type S = sig
with type value = Val.t and type location = Loc.location
end
-module Hooks : sig
- type hook = (module S) -> (module S)
- val register : hook -> unit
-end
-
-module type Eva = sig
+module type S_with_evaluation = sig
include S
- module Eval: Evaluation.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
-module Default : S
+module Hooks : sig
+ type hook = (module S) -> (module S)
+ val register : hook -> unit
+end
+
+(* module Default : S *)
+val make : Config.t -> (module S)
(*
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..115d2eb0169f07d589d7b91c9db68091d9259be8 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
@@ -1691,6 +1661,15 @@ module Make
| _ -> assert false
end
+module type Eva = sig
+ include Abstractions.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
+
(*
Local Variables:
diff --git a/src/plugins/eva/engine/evaluation.mli b/src/plugins/eva/engine/evaluation.mli
index 6197f1d07fb23dae081e2cb38e226c17dbb3148e..0f8e50d01d1483a104423c9bbae909671a2d53ed 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,12 +41,11 @@ 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
+ : 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:
compile-command: "make -C ../../../.."
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..981568f2b5654ce45a422962ffd3eb28a0d1e979 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,10 +273,11 @@ 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 Domain.get Cvalue_domain.State.key with
| None -> Self.abort "Function Db.Value.fun_set_args cannot be \
used without the Cvalue domain"
| Some get_cvalue ->
+ let get_cvalue s = get_cvalue s |> fst in
let formals = Kernel_function.get_formals kf in
if (List.length formals) <> List.length actuals then
raise Db.Value.Incorrect_number_of_arguments;
@@ -366,7 +368,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/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/locations/locations_product.ml b/src/plugins/eva/locations/locations_product.ml
index 02e1ff617796be86a55b852bbc34dd1a2917973a..4d6ca1c1f83407e5f7ea1daf814d492bff4425f0 100644
--- a/src/plugins/eva/locations/locations_product.ml
+++ b/src/plugins/eva/locations/locations_product.ml
@@ -23,8 +23,15 @@
open Eval
-module Common (Left: Abstract_location.S) (Right: Abstract_location.S) = struct
- (* TODO: maybe wrong if left and right use the same offset *)
+
+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
@@ -48,17 +55,34 @@ module Common (Left: Abstract_location.S) (Right: Abstract_location.S) = struct
let replace_base subst (l, r) =
Left.replace_base subst l, Right.replace_base subst r
- let assume_no_overlap ~partial (l, r) (l', r') =
- let left = Left.assume_no_overlap ~partial l l' in
- let right = Right.assume_no_overlap ~partial r r' in
- (* TODO: don't known how to combine *)
- assert false
+ (* 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_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
+ let combine (l1, l2) (r1, r2) = (l1, r1), (l2, r2) in
+ narrow_any_truth combine ((l1, l2), l_truth) ((r1, r2), r_truth)
let assume_valid_location ~for_writing ~bitfield (l, r) =
- let left = Left.assume_valid_location ~for_writing ~bitfield l in
- let right = Right.assume_valid_location ~for_writing ~bitfield r in
- (* TODO: don't known how to combine *)
- assert false
+ let l_truth = Left.assume_valid_location ~for_writing ~bitfield l in
+ let r_truth = Right.assume_valid_location ~for_writing ~bitfield r in
+ narrow_truth (l, l_truth) (r, r_truth)
let no_offset = Left.no_offset, Right.no_offset
@@ -81,44 +105,6 @@ module Common (Left: Abstract_location.S) (Right: Abstract_location.S) = struct
let* lo = Left.backward_field typ info lo in
let* ro = Right.backward_field typ info ro in
`Value (lo, ro)
-end
-
-
-
-module Make (Left: Abstract_location.S) (Right: Abstract_location.S) = struct
- include Common (Left) (Right)
- type value = Left.value * Right.value
-
- let to_value (l, r) = Left.to_value l, Right.to_value r
-
- let forward_index typ (lv, rv) (l, r) =
- Left.forward_index typ lv l, Right.forward_index typ rv r
-
- let forward_pointer typ (lv, rv) (lo, ro) =
- let* l = Left.forward_pointer typ lv lo in
- let* r = Right.forward_pointer typ rv ro in
- `Value (l, r)
-
- let backward_pointer (lv, rv) (lo, ro) (l, r) =
- let* (lv, lo) = Left.backward_pointer lv lo l in
- let* (rv, ro) = Right.backward_pointer rv ro r in
- `Value ((lv, rv), (lo, ro))
-
- let backward_index typ ~index:(li, ri) ~remaining:(lrem, rrem) (lo, ro) =
- let* (lv, lo) = Left.backward_index typ ~index:li ~remaining:lrem lo in
- let* (rv, ro) = Right.backward_index typ ~index:ri ~remaining:rrem ro in
- `Value ((lv, rv), (lo, ro))
-end
-
-
-
-module Same_value
- (Value: Abstract_value.S)
- (Left: Abstract_location.S with type value = Value.t)
- (Right: Abstract_location.S with type value = Value.t)
-= struct
- include Common (Left) (Right)
- type value = Value.t
(* TODO: ??? *)
let to_value (l, r) = Value.join (Left.to_value l) (Right.to_value r)
diff --git a/src/plugins/eva/locations/locations_product.mli b/src/plugins/eva/locations/locations_product.mli
index d8279dfb0b368200272d46049a69cca8719cf662..b79029fcf775daa6ccb0a792d3c82d8ba9881732 100644
--- a/src/plugins/eva/locations/locations_product.mli
+++ b/src/plugins/eva/locations/locations_product.mli
@@ -20,18 +20,10 @@
(* *)
(**************************************************************************)
-module Make (Left : Abstract_location.S) (Right : Abstract_location.S) :
- Abstract_location.S
- with type value = Left.value * Right.value
- and type location = Left.location * Right.location
- and type offset = Left.offset * Right.offset
-
-
-
-module Same_value
+module Make
(Value: Abstract_value.S)
- (Left: Abstract_location.S with type value = Value.t)
- (Right: Abstract_location.S with type value = Value.t)
+ (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
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..b2cfb4e471ccc1dc5ab6fe57ba064996c1a6c090 100644
--- a/src/plugins/eva/utils/abstract.ml
+++ b/src/plugins/eva/utils/abstract.ml
@@ -81,8 +81,8 @@ module Domain = struct
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
+ (* 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..504dc52a92fafd68e053c81cdc8ea38ad4776197 100644
--- a/src/plugins/eva/utils/abstract.mli
+++ b/src/plugins/eva/utils/abstract.mli
@@ -92,8 +92,8 @@ module Domain : sig
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
+ (* 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/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/main_locations.ml b/src/plugins/eva/values/main_locations.ml
index 92d31c7f54b1baeaaf2723e373815aef3cd9bfc3..dedbd3e8209e8d9e9e6e37aa25735b828da0693b 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
@@ -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..109cfdbf18ba1a63e1ca8332fd06fcb0f0a55c5b 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -369,116 +369,114 @@ 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))))
+module CvalueOffsm = struct
+ type t = Main_values.CVal.t * Offsm.t
let size typ = Integer.of_int (Cil.bitsSizeOf typ)
@@ -507,37 +505,60 @@ module CvalueOffsm : Abstract.Value.Internal with type t = V.t * offsm_or_top
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
-
+ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
+ let module Value = struct
+ include Abstraction.Val
+ let (let*) = (>>-)
+
+ let get_product =
+ match get Main_values.CVal.key, get Offsm.key with
+ | Some cval, Some offsm -> Some (fun p -> (cval p, offsm p))
+ | _, _ -> None
+
+ let set_product =
+ let set_cval = set Main_values.CVal.key in
+ let set_offsm = set Offsm.key in
+ fun (cval, offsm) p -> set_cval cval p |> set_offsm offsm
+
+ let forward_unop =
+ match get_product with
+ | None -> Abstraction.Val.forward_unop
+ | Some get_product -> fun typ op p ->
+ let p' = set_product (strengthen_offsm typ (get_product p)) p in
+ let* p'' = Abstraction.Val.forward_unop typ op p' in
+ let* reduced = strengthen_v typ (get_product p'') in
+ `Value (set_product reduced p'')
+
+ let forward_binop =
+ match get_product with
+ | None -> Abstraction.Val.forward_binop
+ | Some get_product -> fun typ op l r ->
+ match op with
+ | BAnd | BOr | BXor ->
+ let l' = set_product (strengthen_offsm typ (get_product l)) l in
+ let r' = set_product (strengthen_offsm typ (get_product r)) r in
+ let* p = Abstraction.Val.forward_binop typ op l' r' in
+ let* reduced = strengthen_v typ (get_product p) in
+ `Value (set_product reduced p)
+ | Shiftlt | Shiftrt ->
+ let l' = get_product l in
+ let (r_val, _) = get_product r in
+ let* p = Abstraction.Val.forward_binop typ op l r in
+ begin
+ try
+ let i = V.project_ival r_val |> 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
+ let (v, _) = get_product p in
+ `Value (set_product (v, O offsm) p)
+ with V.Not_based_on_null | Ival.Not_Singleton_Int -> `Value p
+ end
+ | _ -> Abstraction.Val.forward_binop typ op l r
+ end in
+ (module struct
+ include Abstraction
+ module Val = Value
+ end)
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