diff --git a/src/plugins/eva/contexts/abstract_context.ml b/src/plugins/eva/contexts/abstract_context.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b93d201dfe43afc4f24b1af9968e75c19e4766e1
--- /dev/null
+++ b/src/plugins/eva/contexts/abstract_context.ml
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** An abstract context can be used to transfer information from the state of
+ an abstract domain, in which an expression or lvalue is evaluated, to a
+ value abstraction, which interprets operations during this evaluation.
+ The context is built by the function [build_context] of abstract domains,
+ and passed as argument of most transfer functions from {!Abstract_value}. *)
+
+open Eval
+
+module type S = sig
+ type t
+
+ (** The default context used in a top abstract state, or if no domain has been
+ enabled — or no domain providing this context. *)
+ val top : t
+
+ (** In a product of abstract domains, merges the context provided by the
+ abstract state of each domain. *)
+ val narrow : t -> t -> t or_bottom
+end
+
+(** Keys used to identify context modules. *)
+type 'c key = 'c Structure.Key_Context.key
+
+(** Signature for a leaf module of context. *)
+module type Leaf = sig
+ include S
+
+ (** The key identifies the module and the type [t] of context. *)
+ val key : t key
+end
+
+(** Eva abstractions are divided between contexts, values, locations and domains.
+ Values and domains depend on contexts, and use this type to declare such
+ dependencies. In the standard case, a value or domain depends on a single
+ context module [Ctx] and uses [Leaf (module Ctx)] to declare this dependency. *)
+type 'c dependencies =
+ | Leaf : (module Leaf with type t = 'c) -> 'c dependencies
+ | Node : 'l dependencies * 'r dependencies -> ('l * 'r) dependencies
diff --git a/src/plugins/eva/contexts/context_product.ml b/src/plugins/eva/contexts/context_product.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4ca41b8fdc1ce92d1c2531b5afcd4dfade1ba9a6
--- /dev/null
+++ b/src/plugins/eva/contexts/context_product.ml
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Make (L : Abstract_context.S) (R : Abstract_context.S) = struct
+ type t = L.t * R.t
+ let top = (L.top, R.top)
+ let narrow (l, r) (l', r') =
+ Lattice_bounds.Bottom.zip (L.narrow l l') (R.narrow r r')
+end
diff --git a/src/plugins/eva/contexts/context_product.mli b/src/plugins/eva/contexts/context_product.mli
new file mode 100644
index 0000000000000000000000000000000000000000..abbd6bfc9a965d81773516d727701b5480dcf799
--- /dev/null
+++ b/src/plugins/eva/contexts/context_product.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Cartesian product of two context abstractions. *)
+
+module Make (L : Abstract_context.S) (R : Abstract_context.S)
+ : Abstract_context.S with type t = L.t * R.t
diff --git a/src/plugins/eva/contexts/unit_context.ml b/src/plugins/eva/contexts/unit_context.ml
new file mode 100644
index 0000000000000000000000000000000000000000..86669eb7cde87661606d07dcea04d6b8780c0e7f
--- /dev/null
+++ b/src/plugins/eva/contexts/unit_context.ml
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type t = unit
+let top = ()
+let narrow () () = `Value ()
+let key = Structure.Key_Context.create_key "Unit context"
diff --git a/src/plugins/eva/contexts/unit_context.mli b/src/plugins/eva/contexts/unit_context.mli
new file mode 100644
index 0000000000000000000000000000000000000000..908e1f44c9645649be7b02488c667b29b49013a0
--- /dev/null
+++ b/src/plugins/eva/contexts/unit_context.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Abstract_context.Leaf with type t = unit
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 36b5e3125468a73ddcba0d75fb9e485f776189b1..9f359ed133e988bd3e1197fa4af26eb9ef2668d3 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -127,6 +127,11 @@ module type Queries = sig
(** Domain state. *)
type state
+ (** Domains can optionally provide a context to be used by value abstractions
+ when evaluating expressions. This can be safely ignored for most domains.
+ Defined as unit (no context) by {!Domain_builder.Complete}. *)
+ type context
+
(** Numerical values to which the expressions are evaluated. *)
type value
@@ -188,6 +193,11 @@ module type Queries = sig
Defined by {!Domain_builder.Complete} with no reduction. *)
val reduce_further : state -> exp -> value -> (exp * value) list
+ (** Returns the current context to be used by value abstractions for the
+ evaluation of expressions or lvalues.
+ Defined by {!Domain_builder.Complete} with no context. *)
+ val build_context : state -> context or_bottom
+
end
(** Results of an evaluation: the results of all intermediate calculation (the
@@ -511,6 +521,11 @@ module type Leaf = sig
Automatically created by {!Domain_builder.Complete}. *)
val key: t key
+ (** The abstract context used by the domain.
+ It carries the [context] type used by the domain.
+ Defined by {!Domain_builder.Complete} for the unit context. *)
+ val context_dependencies : context Abstract_context.dependencies
+
(** The abstract value used by the domain.
It carries the [value] type used by the domain.
See {!Main_values} for some abstract values available in Eva. *)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 3e59910211ace4eaa373a09edd2c98fabb3868a6..4a28b113809f6fdad73dd42a4abf5a66f3eb3e74 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -33,6 +33,9 @@ module State = struct
let value_dependencies = Main_values.cval
let location_dependencies = Main_locations.ploc
+ type context = unit
+ let context_dependencies = Abstract_context.Leaf (module Unit_context)
+
let log_category = Self.dkey_cvalue_domain
include Datatype.Make_with_collections (
@@ -83,6 +86,8 @@ module State = struct
let reduce_further (state, _) expr value =
Cvalue_queries.reduce_further state expr value
+ let build_context (state, _) = Cvalue_queries.build_context state
+
(* ------------------------------------------------------------------------ *)
(* Transfer Functions *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index 7aacb74f3eaf7971c466af16ef5a5f79db9149cc..f6a375c1366fc68c9e6f2f931e357e0ba9c1acfc 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -23,6 +23,7 @@
module Queries = struct
type state = Cvalue.Model.t
+ type context = unit
type value = Main_values.CVal.t
type location = Main_locations.PLoc.location
@@ -158,6 +159,7 @@ module Queries = struct
`Value (Precise_locs.make_precise_loc loc ~size, value)
let reduce_further _state _expr _value = []
+ let build_context _ = `Value ()
end
include Queries
@@ -181,7 +183,7 @@ module Domain = struct
include Queries
end
-include Evaluation.Make (Value) (Main_locations.PLoc) (Domain)
+include Evaluation.Make (Unit_context) (Value) (Main_locations.PLoc) (Domain)
let lval_to_loc state lval =
let eval, _alarms = lvaluate ~for_writing:false state lval in
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.mli b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
index 3d907cf50e529ff3f26ac568c181da57cef0ea79..f2b03356ad70e9052684db92e1b327b88e9e4c71 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
@@ -23,12 +23,14 @@
(** Implementation of domain queries for the cvalue domain. *)
include Abstract_domain.Queries
with type state = Cvalue.Model.t
+ and type context = unit
and type value = Main_values.CVal.t
and type location = Main_locations.PLoc.location
and type origin = Main_values.CVal.t
(** Evaluation engine specific to the cvalue domain. *)
include Evaluation_sig.S with type state := state
+ and type context := unit
and type value := value
and type loc := location
and type origin := origin
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index fbe4083c00fc595f526d8e696ba82ce98e329f6b..76daf8972998165baf7faed8160bbb9787b3f371 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -23,15 +23,23 @@
open Cil_types
open Eval
+
+
module type InputDomain = sig
include Datatype.S
val top: t
val join: t -> t -> t
end
+
+
module type LeafDomain = sig
type t
+ type context = unit
+ val context_dependencies: context Abstract_context.dependencies
+ val build_context: t -> context or_bottom
+
val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
@@ -61,8 +69,13 @@ module type LeafDomain = sig
val key: t Abstract_domain.key
end
+
module Complete (Domain: InputDomain) = struct
+ type context = unit
+ let context_dependencies = Abstract_context.Leaf (module Unit_context)
+ let build_context _ = `Value ()
+
let backward_location _state _lval _typ loc value = `Value (loc, value)
let reduce_further _state _expr _value = []
@@ -88,6 +101,8 @@ module Complete (Domain: InputDomain) = struct
Structure.Key_Domain.create_key Domain.name
end
+
+
open Simpler_domains
let simplify_argument argument =
@@ -100,6 +115,8 @@ let simplify_call call =
rest = List.map fst call.Eval.rest;
return = call.Eval.return; }
+
+
module Make_Minimal
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
@@ -157,6 +174,7 @@ module Make_Minimal
end
+
module Complete_Minimal
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
@@ -298,8 +316,11 @@ let unique_name =
name ^ string_of_int !counter
module Restrict
- (Value: Abstract_value.S)
- (Domain: Abstract.Domain.Internal with type value = Value.t)
+ (Context: Abstract_context.S)
+ (Value: Abstract_value.S with type context = Context.t)
+ (Domain: Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t)
(Scope: sig val functions: Domain_mode.function_mode list end)
= struct
@@ -348,10 +369,15 @@ module Restrict
Abstract.Domain.(Option ((Node (Domain.structure, Void)), default))
type state = t
+ type context = Domain.context
type value = Domain.value
type location = Domain.location
type origin = Domain.origin
+ let build_context = function
+ | None -> `Value Context.top
+ | Some (state, _mode) -> Domain.build_context state
+
let get_state = function
| None -> Domain.top
| Some (state, _mode) -> state
diff --git a/src/plugins/eva/domains/domain_builder.mli b/src/plugins/eva/domains/domain_builder.mli
index 6b6f560b5f741dcb3c7e4075fef3a950582c2b89..a78eeeee2204b958d359ff56ac10ad5cdd533fe2 100644
--- a/src/plugins/eva/domains/domain_builder.mli
+++ b/src/plugins/eva/domains/domain_builder.mli
@@ -40,6 +40,10 @@ end
module type LeafDomain = sig
type t
+ type context = unit
+ val context_dependencies: context Abstract_context.dependencies
+ val build_context: t -> context or_bottom
+
val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
@@ -76,7 +80,8 @@ module Complete_Minimal
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
- : Abstract_domain.Leaf with type value = Value.t
+ : Abstract_domain.Leaf with type context = unit
+ and type value = Value.t
and type location = Location.location
and type state = Domain.t
@@ -84,13 +89,15 @@ module Complete_Minimal_with_datatype
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal_with_datatype)
- : Abstract_domain.Leaf with type value = Value.t
+ : Abstract_domain.Leaf with type context = unit
+ and type value = Value.t
and type location = Location.location
and type state = Domain.t
module Complete_Simple_Cvalue
(Domain: Simpler_domains.Simple_Cvalue)
- : Abstract_domain.Leaf with type value = Cvalue.V.t
+ : Abstract_domain.Leaf with type context = unit
+ and type value = Cvalue.V.t
and type location = Precise_locs.precise_location
and type state = Domain.t
@@ -100,8 +107,13 @@ module Complete_Simple_Cvalue
in the current function and in all functions called from it.
See {!Domain_mode} for more details. *)
module Restrict
- (Value: Abstract_value.S)
- (Domain: Abstract.Domain.Internal with type value = Value.t)
+ (Context: Abstract_context.S)
+ (Value: Abstract_value.S with type context = Context.t)
+ (Domain: Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t)
(_: sig val functions: Domain_mode.function_mode list end)
- : Abstract.Domain.Internal with type value = Value.t
- and type location = Domain.location
+ : Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t
+ and type location = Domain.location
diff --git a/src/plugins/eva/domains/domain_lift.ml b/src/plugins/eva/domains/domain_lift.ml
index f409b0c43035b84479a27b53d2dd34b5d574f38a..90f11ac2bcafacdc3c32f0758a155db6e7ee8a32 100644
--- a/src/plugins/eva/domains/domain_lift.ml
+++ b/src/plugins/eva/domains/domain_lift.ml
@@ -36,6 +36,7 @@ end
module Make
(Domain: Input_Domain)
+ (Ctx: Conversion with type internal := Domain.context)
(Val: Conversion with type internal := Domain.value)
(Loc: Conversion with type internal := Domain.location)
= struct
@@ -47,6 +48,7 @@ module Make
let log_category = Domain.log_category
+ type context = Ctx.extended
type value = Val.extended
type location = Loc.extended
type origin = Domain.origin
@@ -73,6 +75,10 @@ module Make
let list = Domain.reduce_further state expr (Val.restrict value) in
List.map (fun (e, v) -> e, Val.extend v) list
+ let build_context state =
+ let open Bottom.Operators in
+ let+ context = Domain.build_context state in
+ Ctx.extend context
let lift_left left = { left with lloc = Loc.restrict left.lloc }
let lift_flagged_value value =
diff --git a/src/plugins/eva/domains/domain_lift.mli b/src/plugins/eva/domains/domain_lift.mli
index 6ece7d2d6063da1a3de053f58c09b2fb23e91d41..21989482d579856ac2a2c77e43de03a4a26cace1 100644
--- a/src/plugins/eva/domains/domain_lift.mli
+++ b/src/plugins/eva/domains/domain_lift.mli
@@ -34,9 +34,11 @@ end
module Make
(Domain: Input_Domain)
+ (Ctx: Conversion with type internal := Domain.context)
(Val: Conversion with type internal := Domain.value)
(Loc: Conversion with type internal := Domain.location)
: Abstract.Domain.Internal with type state = Domain.state
+ and type context = Ctx.extended
and type value = Val.extended
and type location = Loc.extended
and type origin = Domain.origin
diff --git a/src/plugins/eva/domains/domain_product.ml b/src/plugins/eva/domains/domain_product.ml
index e5b59aa7da99961802d1ee6910509abbae7643cf..fdf4ab1eeeaf75c7d6dd588a4d5bb32573f9701a 100644
--- a/src/plugins/eva/domains/domain_product.ml
+++ b/src/plugins/eva/domains/domain_product.ml
@@ -27,14 +27,22 @@ let counter = ref 0
let product_category = Self.register_category "domain_product"
module Make
- (Value: Abstract_value.S)
- (Left: Abstract.Domain.Internal with type value = Value.t)
- (Right: Abstract.Domain.Internal with type value = Left.value
- and type location = Left.location)
+ (Context : Abstract_context.S)
+ (Value : Abstract_value.S with type context = Context.t)
+ (Location : Abstract_location.S with type value = Value.t)
+ (Left : Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t
+ and type location = Location.location)
+ (Right : Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t
+ and type location = Location.location)
= struct
- type value = Left.value
- type location = Left.location
+ type context = Context.t
+ type value = Value.t
+ type location = Location.location
type origin = {
left: reductness * Left.origin option;
@@ -112,6 +120,12 @@ module Make
(Left.reduce_further left expr value)
(Right.reduce_further right expr value)
+ let build_context (left, right) =
+ let open Lattice_bounds.Bottom.Operators in
+ let* left = Left.build_context left in
+ let* right = Right.build_context right in
+ Context.narrow left right
+
let lift_record side record =
let origin = Option.map side record.origin in
let reductness =
diff --git a/src/plugins/eva/domains/domain_product.mli b/src/plugins/eva/domains/domain_product.mli
index 712050901420e432a212cccf8094fa3dd7166156..7456288492853772fff15bf172a9c16a8beba271 100644
--- a/src/plugins/eva/domains/domain_product.mli
+++ b/src/plugins/eva/domains/domain_product.mli
@@ -23,13 +23,22 @@
val product_category: Self.category
module Make
- (Value: Abstract_value.S)
- (Left: Abstract.Domain.Internal with type value = Value.t)
- (Right: Abstract.Domain.Internal with type value = Left.value
- and type location = Left.location)
- : Abstract.Domain.Internal with type value = Value.t
- and type location = Left.location
- and type state = Left.state * Right.state
+ (Context : Abstract_context.S)
+ (Value : Abstract_value.S with type context = Context.t)
+ (Location : Abstract_location.S with type value = Value.t)
+ (Left : Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t
+ and type location = Location.location)
+ (Right : Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t
+ and type location = Location.location)
+ : Abstract.Domain.Internal
+ with type context = Context.t
+ and type value = Value.t
+ and type location = Location.location
+ and type state = Left.state * Right.state
(*
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 53477de6050e7067164ba5b6d1aafb8d9e49ac39..680f09fd4ec955d1b4a65f64c33b6505f3c68da6 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -127,7 +127,7 @@ module Internal = struct
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
- let pretty_debug fmt (eqs, deps, modified) =
+ let _pretty_debug fmt (eqs, deps, modified) =
Format.fprintf fmt
"@[<v>@[<hov 2>Eqs: %a@]@.@[<hov 2>Deps: %a@]@.@[<hov 2>Changed: %a@]@]"
Equality.Set.pretty eqs Deps.pretty deps
@@ -176,19 +176,24 @@ let project (t, _, _) = t
(* ------------------------- Abstract Domain -------------------------------- *)
-module Make
- (Value : Abstract.Value.External)
-= struct
+module type Context = Abstract.Context.External
+module type Value = Abstract.Value.External
+
+module Make (Context : Context) (Value : Value with type context = Context.t) =
+struct
include Internal
include Store
let get_cvalue = Value.get Main_values.CVal.key
+ type context = Context.t
type value = Value.t
type location = Precise_locs.precise_location
type origin
+ let build_context _ = `Value Context.top
+
let reduce_further (equalities, _, _) expr value =
let atom = HCE.of_exp expr in
match Equality.Set.find_option atom equalities with
@@ -534,7 +539,7 @@ end
module Functor = struct
type location = Precise_locs.precise_location
let location_dependencies = Main_locations.ploc
- module Make (V : Abstract.Value.External) = Make (V)
+ module Make (C : Context) (V : Value with type context = C.t) = Make (C) (V)
end
let registered =
diff --git a/src/plugins/eva/domains/equality/equality_domain.mli b/src/plugins/eva/domains/equality/equality_domain.mli
index 3a6bb3f81ce89184de7c6aa56ccfc66229c4c48f..aa35a9e332641fc8cfafabdfbb903fee8caa6aed 100644
--- a/src/plugins/eva/domains/equality/equality_domain.mli
+++ b/src/plugins/eva/domains/equality/equality_domain.mli
@@ -35,12 +35,13 @@ type t
val key: t Abstract_domain.key
val project: t -> Equality.Set.t
-module Make (Value : Abstract.Value.External) : sig
- include Abstract_domain.S with type value = Value.t
- and type location = Precise_locs.precise_location
- and type state = t
+module type Context = Abstract.Context.External
+module type Value = Abstract.Value.External
- val pretty_debug : Format.formatter -> t -> unit
-end
+module Make (Context : Context) (Value : Value with type context = Context.t) :
+ Abstract_domain.S with type context = Context.t
+ and type value = Value.t
+ and type location = Precise_locs.precise_location
+ and type state = t
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 31bed46e08b5149ca5c2c63e6cd9bcb76379c033..c34c84acc994dd8348aba9af923a7058a7d03efb 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -931,7 +931,7 @@ let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
| _, None -> (module Abstract)
| Some get_cval, Some get_multidim ->
let module Eval =
- Evaluation.Make (Abstract.Val) (Abstract.Loc) (Abstract.Dom)
+ Evaluation.Make (Abstract.Ctx) (Abstract.Val) (Abstract.Loc) (Abstract.Dom)
in
let module Dom = struct
include Abstract.Dom
@@ -960,6 +960,7 @@ let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
end
in
(module struct
+ module Ctx = Abstract.Ctx
module Val = Abstract.Val
module Loc = Abstract.Loc
module Dom = Dom
diff --git a/src/plugins/eva/domains/numerors/numerors_domain.ml b/src/plugins/eva/domains/numerors/numerors_domain.ml
index 0ad9d3cbf7ee95d1b3143745fd62791385b36d94..bde3d56c0ef99c7a0937a4dd427bc60df05278b9 100644
--- a/src/plugins/eva/domains/numerors/numerors_domain.ml
+++ b/src/plugins/eva/domains/numerors/numerors_domain.ml
@@ -125,8 +125,8 @@ let reduce_cast (module Abstract: Abstractions.S) =
| Some get_cvalue, true ->
(* Otherwise, applies the [forward_cast] function, but updates the
numerors component of the result. *)
- fun ~src_type ~dst_type value ->
- forward_cast ~src_type ~dst_type value >>-: fun result ->
+ fun context ~src_type ~dst_type value ->
+ forward_cast context ~src_type ~dst_type value >>-: fun result ->
match src_type, dst_type with
| Eval_typ.TSInt _, Eval_typ.TSFloat fkind ->
begin
@@ -146,6 +146,7 @@ let reduce_cast (module Abstract: Abstractions.S) =
| _, _ -> result
end in
(module struct
+ module Ctx = Abstract.Ctx
module Val = Val
module Loc = Abstract.Loc
module Dom = Abstract.Dom
diff --git a/src/plugins/eva/domains/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
index a92622dea5caf862a68fb058829f2f3b8a22d169..41380d779b7f4a475eb6dbe88c05ae52412594ac 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.ml
+++ b/src/plugins/eva/domains/numerors/numerors_value.ml
@@ -116,6 +116,9 @@ include Datatype.Make(T)
let pretty_debug = pretty
let pretty_typ _ = pretty
+type context = unit
+let context = Abstract_context.Leaf (module Unit_context)
+
(*-----------------------------------------------------------------------------
* Constructors
@@ -156,7 +159,7 @@ module Rel_Err = Arith.Rel_Err
(*-----------------------------------------------------------------------------
* Numerors value of a constant
*---------------------------------------------------------------------------*)
-let constant _ = function
+let constant _ _ = function
| CReal (r, fkind, opt) ->
let prec = Precisions.of_fkind fkind in
let exact =
@@ -177,7 +180,7 @@ let constant _ = function
(*-----------------------------------------------------------------------------
* Forward unary operations on Numerors value
*---------------------------------------------------------------------------*)
-let forward_unop _typ op v =
+let forward_unop _context _typ op v =
match v, op with
| Elt v, Neg ->
let exact , approx = Exact.Forward.neg v, Approx.Forward.neg v in
@@ -194,7 +197,7 @@ let forward_unop _typ op v =
* 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
+let forward_cast _context ~src_type ~dst_type = function
| Top -> `Value Top
| Zero -> `Value Zero
| Elt t ->
@@ -207,7 +210,7 @@ let forward_cast ~src_type ~dst_type = function
(*-----------------------------------------------------------------------------
* Forward binary operations on Numerors values
*---------------------------------------------------------------------------*)
-let forward_binop _typ op x y =
+let forward_binop _context _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
@@ -234,7 +237,7 @@ let forward_binop _typ op x y =
(*-----------------------------------------------------------------------------
* Backward unary operations on Numerors values
*---------------------------------------------------------------------------*)
-let backward_unop ~typ_arg:_ op ~arg ~res =
+let backward_unop _context ~typ_arg:_ op ~arg ~res =
match arg, res, op with
| Elt x, Elt r, Neg ->
Exact.Backward.neg x r >>- fun exact ->
@@ -248,7 +251,7 @@ let backward_unop ~typ_arg:_ op ~arg ~res =
(*-----------------------------------------------------------------------------
* Backward binary operations on Numerors values
*---------------------------------------------------------------------------*)
-let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
+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 ) ->
@@ -313,8 +316,8 @@ 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 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
diff --git a/src/plugins/eva/domains/numerors/numerors_value.mli b/src/plugins/eva/domains/numerors/numerors_value.mli
index a93772408e7e568eb970eba400dd8c273d3e6e5d..4814acb57a0edd21e9225483776dff5eb02dd811 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.mli
+++ b/src/plugins/eva/domains/numerors/numerors_value.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-include Abstract_value.Leaf
+include Abstract_value.Leaf with type context = unit
val pretty_debug : t Pretty_utils.formatter
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 07efff330ecd3703d8cc3bee513f6e93aff94885..33be2920a29172dabe0ebf5c32eec98d07df2b46 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1604,7 +1604,6 @@ module Domain = struct
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin
-
let value_dependencies = Main_values.cval
let location_dependencies = Main_locations.ploc
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index 9876dd9c550bb03b53124416668cbb006715550a..d20a13adf8ab68cf6ef4181c5b0d7bfe835b93a0 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -585,6 +585,7 @@ let interpret_taint_logic
end
in
(module struct
+ module Ctx = Abstract.Ctx
module Val = Abstract.Val
module Loc = Abstract.Loc
module Dom = Dom
diff --git a/src/plugins/eva/domains/unit_domain.mli b/src/plugins/eva/domains/unit_domain.mli
index d23039ef5c05823dd373d143c2ee551269039a96..e8334fa3e505f0964372ecaf3a299a916a4f8a83 100644
--- a/src/plugins/eva/domains/unit_domain.mli
+++ b/src/plugins/eva/domains/unit_domain.mli
@@ -23,7 +23,8 @@
module Make
(Value: Abstract_value.S)
(Loc: Abstract_location.S)
- : Abstract.Domain.Internal with type state = unit
+ : Abstract.Domain.Internal with type context = unit
+ and type state = unit
and type value = Value.t
and type location = Loc.location
diff --git a/src/plugins/eva/engine/abstractions.ml b/src/plugins/eva/engine/abstractions.ml
index 1e16ee9bc641ea2f12feed2a5a859aae39836131..3e02c2c85e63c3656b4869637a547a7c2bceee67 100644
--- a/src/plugins/eva/engine/abstractions.ml
+++ b/src/plugins/eva/engine/abstractions.ml
@@ -22,6 +22,118 @@
+(* --- Contexts abstraction ------------------------------------------------- *)
+
+module Context = struct
+ type 'c structure = 'c Abstract.Context.structure
+ type 'c dependencies = 'c Abstract_context.dependencies
+ let dec_eq = Abstract.Context.eq_structure
+
+ type 'c context = (module Abstract_context.Leaf with type t = 'c)
+
+ (* When building the abstraction, we will need to compare the dependencies
+ structure with the structured values. *)
+ let rec outline : type v. v dependencies -> v structure = function
+ | Leaf context ->
+ let module C = (val context) in
+ Abstract.Context.Leaf (C.key, (module C))
+ | Node (l, r) -> Abstract.Context.(Node (outline l, outline r))
+
+ (* Folding over contexts dependencies *)
+ type 'a folder = { folder : 'c. 'c context -> 'a -> 'a }
+ let rec fold : type c. 'a folder -> c dependencies -> 'a -> 'a =
+ fun folder dependencies acc ->
+ match dependencies with
+ | Leaf leaf -> folder.folder leaf acc
+ | Node (l, r) -> fold folder l (fold folder r acc)
+
+ (* The context abstraction build consists of accumulating registered contexts
+ into a structured context and then adding the needed operators, thus making
+ it interactive. A [Unit] structured abstraction is used for the initial
+ state and is discarded as soon as a real context abstraction is added. *)
+ module type Structured = Abstract.Context.Internal
+ module type Interactive = Abstract.Context.External
+ type 'a or_unit = Unit | Context of 'a
+ type structured = (module Structured) or_unit
+ type interactive = (module Interactive) or_unit
+
+ let init : structured = Unit
+
+ (* During the complete abstraction build, we need to verify that there is at
+ least one context in the computed abstraction.
+ TODO: better error handling. *)
+ let assert_not_unit = function
+ | Unit -> Self.fatal "The built context cannot be unit."
+ | Context interactive -> interactive
+
+ (* Making a structured context interactive simply consists of adding the
+ needed operations using the Structure.Open functor.*)
+ let make_interactive : structured -> interactive = function
+ | Unit -> Unit
+ | Context (module Structured) ->
+ Context (module struct
+ include Structured
+ include Structure.Open (Abstract.Context) (Structured)
+ end)
+
+ (* Adding a registered context into a structured one consists of deciding if
+ a product is needed (which comes down to checking if the registered
+ context key we want to add is not in the structure), computing it, and
+ updating the structure. *)
+ let add : type c. c context -> structured -> structured =
+ fun (module Ctx) structured ->
+ let leaf = Abstract.Context.Leaf (Ctx.key, (module Ctx)) in
+ match make_interactive structured with
+ | Unit ->
+ Context (module struct
+ include Ctx
+ let structure = leaf
+ end)
+ | Context (module Interactive) when not (Interactive.mem Ctx.key) ->
+ Context (module struct
+ include Context_product.Make (Interactive) (Ctx)
+ let structure = Abstract.Context.Node (Interactive.structure, leaf)
+ end)
+ | _ -> structured
+
+
+ (* When building the complete abstraction, we need to trick values and domains
+ into thinking that their context dependencies are there, even if the
+ structured context type is not the good one. This is done through a
+ lift that requires conversion operations to interact with the subpart
+ of the structured context that matters for the value or the domain.
+ This functor is responsible of building such conversion operations. *)
+ module type From = sig type context val structure : context structure end
+ module Converter (From : From) (To : Interactive) = struct
+ type internal = From.context
+ type extended = To.t
+ let structure = From.structure
+
+ let void_context () =
+ Self.fatal "Cannot register a context module from a Void structure."
+
+ let rec set : type v. v structure -> v -> extended -> extended = function
+ | Leaf (key, _) -> To.set key
+ | Node (s1, s2) -> fun (v1, v2) ext -> set s2 v2 ext |> set s1 v1
+ | Option (s, default) -> fun v -> set s (Option.value ~default v)
+ | Unit -> fun () value -> value
+ | Void -> void_context ()
+
+ let rec get : type v. v structure -> extended -> v = function
+ | Leaf (key, _) -> Option.get (To.get key)
+ | Node (s1, s2) -> fun v -> get s1 v, get s2 v
+ | Option (s, _) -> fun v -> Some (get s v)
+ | Unit -> fun _ -> ()
+ | Void -> void_context ()
+
+ let replace = set structure
+ let extend v = replace v To.top
+ let restrict = get structure
+ end
+end
+
+
+
(* --- Values abstraction --------------------------------------------------- *)
module Value = struct
@@ -48,55 +160,101 @@ module Value = struct
| Leaf leaf -> folder.folder leaf acc
| Node (l, r) -> fold folder l (fold folder r acc)
- (* The value abstraction build consists of accumulating registered values
- into a structured value and then adding the needed operators, thus making
- it interactive. A [Unit] structured abstraction is used for the initial
- state and is discarded as soon as a real value abstraction is added. *)
- module type Structured = Abstract.Value.Internal
+ (* Folding over contexts dependencies of a value. *)
+ let rec fold_contexts : type v. 'a Context.folder -> v dependencies -> 'a -> 'a =
+ fun folder dependencies acc ->
+ match dependencies with
+ | Leaf (module V) -> Context.fold folder V.context acc
+ | Node (l, r) -> fold_contexts folder l (fold_contexts folder r acc)
+
+
+ (* As for the context abstraction, building the value abstraction consists
+ of structuring the needed registered values and then adding the needed
+ operators to make it interactive. However, a structured value is not
+ as simple as a structured context, as it needs to keep track of the
+ context abstraction it is based on. This context is supposed to be the
+ complete aggregation of all the contexts that are needed by the
+ requested domains. *)
+ module type Structured = sig
+ type context
+ module Context : Context.Interactive with type t = context
+ module Value : Abstract.Value.Internal with type context = context
+ end
+
+ (* We expose the type of the structured context we are based on to statically
+ ensure that we do not temper with it. As for the context abstractions, a
+ [Unit] structured abstraction is used for the initial state and is
+ discarded as soon as a value is added. *)
+ type ('c, 'v) or_unit = Unit of 'c | Value of 'v
+ type 'c context = (module Context.Interactive with type t = 'c)
+ type 'c structured_module = (module Structured with type context = 'c)
+ type 'c structured = ('c context, 'c structured_module) or_unit
+
module type Interactive = Abstract.Value.External
- type 'a or_unit = Unit | Value of 'a
- type structured = (module Structured) or_unit
- type interactive = (module Interactive) or_unit
+ type 'c interactive_module = (module Interactive with type context = 'c)
+ type 'c interactive = ('c context, 'c interactive_module) or_unit
+
+
+ (* Initial value builder *)
+ let init (context : 'c context) : 'c structured = Unit context
+
+ (* During the complete abstraction build, we need to verify that there is at
+ least one value in the computed abstraction.
+ TODO: better error handling. *)
+ let assert_not_unit = function
+ | Unit _ -> Self.fatal "The built value cannot be unit."
+ | Value interactive -> interactive
+
(* Making a structured value interactive simply consists of adding the
- needed operations using the Structure.Open functor.*)
- let make_interactive : structured -> interactive = function
- | Unit -> Unit
+ needed operations using the Structure.Open functor. *)
+ let make_interactive : type c. c structured -> c interactive = function
+ | Unit context -> Unit context
| Value (module Structured) ->
Value (module struct
- include Structured
- include Structure.Open (Abstract.Value) (Structured)
+ include Structured.Value
+ include Structure.Open (Abstract.Value) (Structured.Value)
end)
+ (* Retrieves the context contained in a structured value. *)
+ let get_context : type c. c structured -> c context = function
+ | Unit context -> context
+ | Value (module V) -> (module V.Context)
+
+
(* Adding a registered value into a structured one consists of deciding if
a product is needed (which comes down to checking if the registered
value key we want to add is not in the structure), computing it, and
updating the structure. *)
- let add : type v. v value -> structured -> structured =
- fun (module Val) structured ->
- let leaf = Abstract.Value.Leaf (Val.key, (module Val)) in
- match make_interactive structured with
- | Unit ->
- Value (module struct
- include Val
- let structure = leaf
- end)
- | Value (module Interactive) when not (Interactive.mem Val.key) ->
- Value (module struct
- include Value_product.Make (Interactive) (Val)
- let structure = Abstract.Value.Node (Interactive.structure, leaf)
- end)
- | _ -> structured
-
- (* The minimal value abstraction to use. *)
- let init : structured = Unit
-
- (* During the complete abstraction build, we need to verify that there is at
- least one value in the computed abstraction.
- TODO: better error handling. *)
- let assert_not_unit = function
- | Unit -> Self.fatal "The built value cannot be unit."
- | Value interactive -> interactive
+ let add : type c v. v value -> c structured -> c structured =
+ fun (module Leaf) structured ->
+ let leaf_context_structure = Context.outline Leaf.context in
+ let module To = (val get_context structured) in
+ let lifted_leaf : (module Abstract.Value.Internal with type context = c) =
+ match Context.dec_eq leaf_context_structure To.structure with
+ | Some Eq ->
+ let leaf = Abstract.Value.Leaf (Leaf.key, (module Leaf)) in
+ (module struct include Leaf let structure = leaf end)
+ | None ->
+ let module From = struct
+ type context = Leaf.context
+ let structure = leaf_context_structure
+ end in
+ let module Converter = Context.Converter (From) (To) in
+ (module Value_lift.Make (Leaf) (Converter))
+ in
+ let combined : (module Abstract.Value.Internal with type context = c) =
+ match make_interactive structured with
+ | Unit _ -> lifted_leaf
+ | Value (module Val) when Val.mem Leaf.key -> (module Val)
+ | Value (module Val) ->
+ (module Value_product.Make (To) (val lifted_leaf) (Val))
+ in
+ Value (module struct
+ type context = c
+ module Context = To
+ module Value = (val combined)
+ end)
(* When building the complete abstraction, we need to trick locations and
@@ -107,6 +265,7 @@ module Value = struct
This functor is responsible of building such conversion operations. *)
module type From = sig type value val structure : value structure end
module Converter (From : From) (To : Interactive) = struct
+ type internal = From.value
type extended = To.t
let structure = From.structure
@@ -154,19 +313,27 @@ module Location = struct
(* Folding over values dependencies *)
type 'a folder = { folder : 'l. 'l location -> 'a -> 'a }
- let rec fold : type v. 'a folder -> v dependencies -> 'a -> 'a =
+ let rec fold : type l. 'a folder -> l dependencies -> 'a -> 'a =
fun folder dependencies acc ->
match dependencies with
| Leaf leaf -> folder.folder leaf acc
| Node (l, r) -> fold folder l (fold folder r acc)
(* Folding over the values dependencies of some locations dependencies. *)
- let rec fold_values : type v. 'a Value.folder -> v dependencies -> 'a -> 'a =
+ let rec fold_values : type l. 'a Value.folder -> l dependencies -> 'a -> 'a =
fun folder dependencies acc ->
match dependencies with
- | Leaf (module R) -> Value.fold folder R.value acc
+ | Leaf (module Loc) -> Value.fold folder Loc.value acc
| Node (l, r) -> fold_values folder l (fold_values folder r acc)
+ (* Folding over contexts dependencies of the value dependencies of some
+ locations dependencies. *)
+ let rec fold_contexts : type l. 'a Context.folder -> l dependencies -> 'a -> 'a =
+ fun folder dependencies acc ->
+ match dependencies with
+ | Leaf (module Loc) -> Value.fold_contexts folder Loc.value acc
+ | Node (l, r) -> fold_contexts folder l (fold_contexts folder r acc)
+
(* As for the value abstraction, building the location abstraction consists
of structuring the needed registered locations and then adding the needed
@@ -269,6 +436,7 @@ module Location = struct
responsible of building such conversion operations. *)
module type From = sig type location val structure : location structure end
module Converter (From : From) (To : Interactive) = struct
+ type internal = From.location
type extended = To.location
let structure = From.structure
@@ -301,15 +469,19 @@ end
module Domain = struct
module type S = Abstract_domain.S
+ module type Context = Abstract.Context.External
+ module type Value = Abstract.Value.External
(** Functor domain which can be built over any value abstractions, but with
fixed locations dependencies. *)
module type Functor = sig
type location
val location_dependencies: location Abstract_location.dependencies
- module Make (V : Abstract.Value.External) : sig
+ module Make (C : Context) (V : Value with type context = C.t) : sig
include Abstract_domain.S
- with type value = V.t and type location = location
+ with type context = C.t
+ and type value = V.t
+ and type location = location
val key : state Abstract_domain.key
end
end
@@ -366,36 +538,59 @@ module Domain = struct
let make () = { name ; experimental ; priority ; abstraction = make () } in
dynamic_domains := (name, make) :: !dynamic_domains
+
(* Building the domain abstraction consists of structuring the requested
registered domains. To do so, we need to keep track of the values and
locations abstraction on which the structured domain will rely. Those
abstractions are supposed to be the complete aggregations of all the
values (resp locations) that are needed by the requested domains. *)
module type Structured = sig
+ type context
type value
type location
- module Value : Value.Interactive with type t = value
+ module Context : Context.Interactive
+ with type t = context
+ module Value : Value.Interactive
+ with type context = context
+ and type t = value
module Location : Location.Interactive
- with type value = value and type location = location
+ with type value = value
+ and type location = location
module Domain : Abstract.Domain.Internal
- with type value = value and type location = location
+ with type context = context
+ and type value = value
+ and type location = location
end
- (* As for the value and location abstractions, a [Unit] structured domain is
- used for the initial state. *)
- type ('v, 'l, 's) or_unit = Unit of 'v * 'l | State of 's
- type 'v value = (module Value.Interactive with type t = 'v)
+ type 'c context =
+ (module Context.Interactive with type t = 'c)
+
+ type ('c, 'v) value =
+ (module Value.Interactive with type context = 'c and type t = 'v)
+
type ('v, 'l) location =
(module Location.Interactive with type value = 'v and type location = 'l)
- type ('v, 'l) structured_module =
- (module Structured with type value = 'v and type location = 'l)
- type ('v, 'l) structured =
- ('v value, ('v, 'l) location, ('v, 'l) structured_module) or_unit
- (* Recovers the value and location abstractions of a structured domain. *)
- let get : type v l. (v, l) structured -> v value * (v, l) location = function
- | Unit (value, location) -> (value, location)
- | State (module S) -> ((module S.Value), (module S.Location))
+ type ('c, 'v, 'l) state =
+ (module Structured
+ with type context = 'c
+ and type value = 'v
+ and type location = 'l)
+
+ type ('c, 'v, 'l, 's) or_unit = Unit of 'c * 'v * 'l | State of 's
+
+ type ('c, 'v, 'l) structured =
+ ('c context, ('c, 'v) value, ('v, 'l) location, ('c, 'v, 'l) state) or_unit
+
+ (* Internal type used for intermediate results of the add procedure. *)
+ type ('c, 'v, 'l) structured_domain =
+ (module Abstract.Domain.Internal
+ with type context = 'c
+ and type value = 'v
+ and type location = 'l)
+
+
+ let init c v l : ('c, 'v, 'l) structured = Unit (c, v, l)
(* During the complete abstraction build, we need to verify that there is at
least one domain in the computed abstraction.
@@ -404,100 +599,124 @@ module Domain = struct
| Unit _ -> Self.fatal "The built domain cannot be unit."
| State structured -> structured
+ module type Typ = sig type t [@@warning "-34"] end
+ type 't typ = (module Typ with type t = 't)
- (* Internal type used for intermediate results of the add procedure. *)
- type ('v, 'l) structured_domain =
- (module Abstract.Domain.Internal with type value = 'v and type location = 'l)
+ type ('internal, 'extended) conversion =
+ (module Domain_lift.Conversion
+ with type extended = 'extended
+ and type internal = 'internal)
- (* Utility function used to create an identity converter. *)
- module type Typ = sig type t end
- let conversion_id (type t) (module T: Typ with type t = t) =
+ let conversion_id (type t) (_ : t typ) : (t, t) conversion =
(module struct
- type extended = T.t
- type internal = T.t
+ type extended = t
+ type internal = t
let extend x = x
let restrict x = x
- end: Domain_lift.Conversion with type extended = t and type internal = t)
+ end)
+
+ let context : type c v l. (c, v, l) structured -> c context = function
+ | Unit (context, _, _) -> context
+ | State (module S) -> (module S.Context)
+
+ let value : type c v l. (c, v, l) structured -> (c, v) value = function
+ | Unit (_, value, _) -> value
+ | State (module S) -> (module S.Value)
+
+ let location : type c v l. (c, v, l) structured -> (v, l) location = function
+ | Unit (_, _, location) -> location
+ | State (module S) -> (module S.Location)
+
+ type 'a identity = 'a -> 'a
+ type ('c, 'v, 'l) name = string -> ('c, 'v, 'l) structured_domain identity
+
+ (* Change [Domain.register_global_state] to take -eva-no-results-domain into
+ account, according to the domain name. Need to be applied after the domain
+ has been built, in case of a domain functor. *)
+ let use_no_results : type c v l. (c, v, l) name = fun name (module D) ->
+ let register = D.Store.register_global_state in
+ let results () = not (Parameters.NoResultsDomains.mem name) in
+ let f storage state = register (storage && results ()) state in
+ let module S = struct include D.Store let register_global_state = f end in
+ (module struct include D module Store = S end)
+
(* Adding a registered domain into a structured one consists of performing a
lifting of the registered one if needed before performing the product,
configuring the name and restricting the domain depending of the mode. *)
- type add_input = registered_with_mode
- let add : type v l. add_input -> (v, l) structured -> (v, l) structured =
- fun (registered, mode) structured ->
+ type input = registered_with_mode
+ type ('c, 'v, 'l) add = input -> ('c, 'v, 'l) structured identity
+ let add : type c v l. (c, v, l) add = 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 =
+ let module Ctx = (val context structured) in
+ let module Val = (val value structured) in
+ let module Loc = (val location structured) in
+ let lifted : (c, v, l) structured_domain =
match registered.abstraction with
| Functor (module Functor) ->
let locs = Location.outline Functor.location_dependencies in
let eq_loc = Location.dec_eq locs Loc.structure in
- let module D = Functor.Make (Val) in
+ let module D = Functor.Make (Ctx) (Val) in
begin match eq_loc with
| Some Eq ->
- (module struct
- include D
- let structure = Abstract.Domain.Leaf (D.key, (module D))
- end)
+ let structure = Abstract.Domain.Leaf (D.key, (module D)) in
+ (module struct include D let structure = structure end)
| None ->
+ let module Ctx = (val conversion_id (module Ctx)) in
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))
+ (module Domain_lift.Make (D) (Ctx) (Val) (Loc))
end
| Domain (module D) ->
- let loc_deps = Location.outline D.location_dependencies in
+ let ctx_deps = Context.outline D.context_dependencies in
let val_deps = Value.outline D.value_dependencies in
- let eq_loc = Location.dec_eq loc_deps Loc.structure in
+ let loc_deps = Location.outline D.location_dependencies in
+ let eq_ctx = Context.dec_eq ctx_deps Ctx.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 struct
- include D
- let structure = Abstract.Domain.Leaf (D.key, (module D))
- end)
- | 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
+ let eq_loc = Location.dec_eq loc_deps Loc.structure in
+ match eq_ctx, eq_val, eq_loc with
+ | Some Eq, Some Eq, Some Eq ->
+ let structure = Abstract.Domain.Leaf (D.key, (module D)) in
+ (module struct include D let structure = structure end)
+ | _ ->
+ let ctx_converter : (D.context, Ctx.t) conversion =
+ match eq_ctx with
+ | Some Eq -> conversion_id (module Ctx)
+ | None ->
+ let module From = struct include D let structure = ctx_deps end in
+ (module Context.Converter (From) (Ctx))
+ in
+ let val_converter : (D.value, Val.t) conversion =
+ match eq_val with
+ | Some Eq -> conversion_id (module Val)
+ | None ->
+ let module From = struct include D let structure = val_deps end in
+ (module Value.Converter (From) (Val))
+ in
+ let loc_converter : (D.location, Loc.location) conversion =
+ match eq_loc with
+ | Some Eq -> conversion_id (module (struct type t = Loc.location end))
+ | None ->
+ let module From = struct include D let structure = loc_deps end in
+ (module Location.Converter (From) (Loc))
+ in
+ (module Domain_lift.Make (D)
+ (val ctx_converter) (val val_converter) (val loc_converter))
in
- (* Set the name of the domain. *)
- let module Named = struct
- include (val lifted)
- module Store = struct
- include Store
- let register_global_state storage state =
- let no_results = Parameters.NoResultsDomains.mem registered.name in
- register_global_state (storage && not no_results) state
- end
- end in
+ (* Take -eva-no-results-domain into account for this domain. *)
+ let lifted = use_no_results registered.name lifted in
(* Restricts the domain according to [mode]. *)
- let restricted : (v, l) structured_domain =
+ let restricted : (c, v, l) structured_domain =
match mode with
- | None -> (module Named)
+ | None -> lifted
| Some kf_modes ->
let module Scope = struct let functions = kf_modes end in
- (module Domain_builder.Restrict (Val) (Named) (Scope))
+ (module Domain_builder.Restrict (Ctx) (Val) (val lifted) (Scope))
in
- let combined : (v, l) structured_domain =
+ let combined : (c, v, l) structured_domain =
match structured with
| Unit _ -> restricted
| State (module Structured) ->
@@ -505,52 +724,65 @@ module Domain = struct
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))
+ (module Domain_product.Make (Ctx) (Val) (Loc) (val restricted) (Dom))
in
State (module struct
+ type context = c
type value = v
type location = l
+ module Context = Ctx
module Value = Val
module Location = Loc
module Domain = (val combined)
end)
- (* Build a complete abstraction based on a list of registered domains and a
- value initial configuration. *)
- let build domains : (module Structured) =
- let values =
- let add_value = Value.{ folder = add } in
- let add_values values (registered, _) =
- match registered.abstraction with
- | Domain (module Domain) ->
- Value.fold add_value Domain.value_dependencies values |>
- Location.fold_values add_value Domain.location_dependencies
- | Functor (module F) ->
- Location.fold_values add_value F.location_dependencies values
- in
- List.fold_left add_values Value.init domains |>
- Value.make_interactive
- in
- let module V = (val Value.assert_not_unit values) in
- let locations =
- let init : V.t Location.structured = Location.init (module V) in
- let add = Location.{ folder = add } in
- let add_locations locs (registered, _) =
- match registered.abstraction with
- | Domain (module D) -> Location.fold add D.location_dependencies locs
- | Functor (module D) -> Location.fold add D.location_dependencies locs
- in
- List.fold_left add_locations init domains |>
- Location.make_interactive
- in
- let module L = (val Location.assert_not_unit locations) in
- let structured : (V.t, L.location) structured =
- Unit ((module V), (module L))
- in
- let structured = List.fold_left (fun s d -> add d s) structured domains in
- let module Structured : Structured = (val assert_not_unit structured) in
- (module Structured)
+
+ let add_contexts contexts (registered, _mode) =
+ let add_context = Context.{ folder = add } in
+ match registered.abstraction with
+ | Domain (module Domain) ->
+ Context.fold add_context Domain.context_dependencies contexts |>
+ Value.fold_contexts add_context Domain.value_dependencies |>
+ Location.fold_contexts add_context Domain.location_dependencies
+ | Functor (module F) ->
+ Location.fold_contexts add_context F.location_dependencies contexts
+
+ let add_values values (registered, _) =
+ let add_value = Value.{ folder = add } in
+ match registered.abstraction with
+ | Domain (module Domain) ->
+ Value.fold add_value Domain.value_dependencies values |>
+ Location.fold_values add_value Domain.location_dependencies
+ | Functor (module F) ->
+ Location.fold_values add_value F.location_dependencies values
+
+ let add_locations locs (registered, _) =
+ let add = Location.{ folder = add } in
+ match registered.abstraction with
+ | Domain (module D) -> Location.fold add D.location_dependencies locs
+ | Functor (module D) -> Location.fold add D.location_dependencies locs
+
+ let build domains =
+ (* Build the contexts *)
+ let contexts = List.fold_left add_contexts Context.init domains in
+ let interactive_ctx c = Context.(make_interactive c |> assert_not_unit) in
+ let module Contexts = (val interactive_ctx contexts) in
+ (* Build the values *)
+ let init_values = Value.init (module Contexts) in
+ let values = List.fold_left add_values init_values domains in
+ let interactive_value v = Value.(make_interactive v |> assert_not_unit) in
+ let module Values = (val interactive_value values) in
+ (* Build the locations *)
+ let init_locations = Location.init (module Values) in
+ let locations = List.fold_left add_locations init_locations domains in
+ let interactive_loc l = Location.(make_interactive l |> assert_not_unit) in
+ let module Locs = (val interactive_loc locations) in
+ (* Build the domains *)
+ let init_domain = init (module Contexts) (module Values) (module Locs) in
+ let structured = List.fold_left (fun s d -> add d s) init_domain domains in
+ let module Structured = (val assert_not_unit structured) in
+ (module Structured : Structured)
end
@@ -631,16 +863,20 @@ end
(* --- Finalizing abstractions build ---------------------------------------- *)
module type S = sig
- module Val : Value_with_reduction
+ module Ctx : Abstract.Context.External
+ module Val : Value_with_reduction with type context = Ctx.t
module Loc : Abstract.Location.External with type value = Val.t
module Dom : Abstract.Domain.External
- with type value = Val.t and type location = Loc.location
+ with type value = Val.t
+ and type location = Loc.location
+ and type context = Ctx.t
end
module type S_with_evaluation = sig
include S
module Eval : Evaluation_sig.S
with type state = Dom.t
+ and type context = Ctx.t
and type value = Val.t
and type loc = Loc.location
and type origin = Dom.origin
@@ -654,6 +890,7 @@ module Hooks = struct
end
module Open (Structured : Domain.Structured) : S = struct
+ module Ctx = Structured.Context
module Val = Reducer.Make (Structured.Value)
module Loc = Structured.Location
module Dom = struct
diff --git a/src/plugins/eva/engine/abstractions.mli b/src/plugins/eva/engine/abstractions.mli
index 7fb32c594d3358ae92c8efeb172c29ac5d3a1e7f..482ba65653723a6e2e7bd07bd95083c5b1c8052d 100644
--- a/src/plugins/eva/engine/abstractions.mli
+++ b/src/plugins/eva/engine/abstractions.mli
@@ -49,14 +49,19 @@ module Domain : sig
name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
(unit -> (module Abstract_domain.Leaf)) -> unit
+ module type Context = Abstract.Context.External
+ module type Value = Abstract.Value.External
+
(** Functor domain which can be built over any value abstractions, but with
fixed locations dependencies. *)
module type Functor = sig
type location
val location_dependencies: location Abstract_location.dependencies
- module Make (V : Abstract.Value.External) : sig
+ module Make (C : Context) (V : Value with type context = C.t) : sig
include Abstract_domain.S
- with type value = V.t and type location = location
+ with type context = C.t
+ and type value = V.t
+ and type location = location
val key : state Abstract_domain.key
end
end
@@ -114,12 +119,15 @@ module type Value_with_reduction = sig
val reduce : t -> t
end
-(** The three abstractions used in an Eva analysis. *)
+(** The four abstractions used in an Eva analysis. *)
module type S = sig
- module Val : Value_with_reduction
+ module Ctx : Abstract.Context.External
+ module Val : Value_with_reduction with type context = Ctx.t
module Loc : Abstract.Location.External with type value = Val.t
module Dom : Abstract.Domain.External
- with type value = Val.t and type location = Loc.location
+ with type value = Val.t
+ and type location = Loc.location
+ and type context = Ctx.t
end
(* The three abstractions plus an evaluation engine for these abstractions. *)
@@ -127,6 +135,7 @@ module type S_with_evaluation = sig
include S
module Eval : Evaluation_sig.S
with type state = Dom.t
+ and type context = Ctx.t
and type value = Val.t
and type loc = Loc.location
and type origin = Dom.origin
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 1fcd2719a6da58bb0e18f9d222dd10cae7b3a1e1..d680a534eb411d4cc9bde1aba46812e5671f3e16 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -95,7 +95,7 @@ module Make (Abstract: Abstractions.S) = struct
module Abstract = struct
include Abstract
- module Eval = Evaluation.Make (Val) (Loc) (Dom)
+ module Eval = Evaluation.Make (Ctx) (Val) (Loc) (Dom)
end
include Abstract
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index d89980278d86653f087e450f4438c63a65305994..81ac423fadbe17a0c3e6b94375473d531ba40f3d 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -242,13 +242,16 @@ module type Queries = sig
end
module Make
- (Value : Value)
+ (Context : Abstract_context.S)
+ (Value : Value with type context = Context.t)
(Loc : Abstract_location.S with type value = Value.t)
- (Domain : Queries with type value = Value.t
+ (Domain : Queries with type context = Context.t
+ and type value = Value.t
and type location = Loc.location)
= struct
type state = Domain.state
+ type context = Context.t
type value = Value.t
type origin = Domain.origin
type loc = Loc.location
@@ -418,18 +421,18 @@ module Make
truncate_lower_bound overflow_kind expr range value >>= fun value ->
truncate_upper_bound overflow_kind expr range value
- let handle_integer_overflow expr range value =
+ let handle_integer_overflow context expr range value =
let signed = range.Eval_typ.i_signed in
- if (signed && Kernel.SignedOverflow.get ()) ||
- (not signed && Kernel.UnsignedOverflow.get ())
- then
+ let signed_overflow = signed && Kernel.SignedOverflow.get () in
+ let unsigned_overflow = not signed && Kernel.UnsignedOverflow.get () in
+ if signed_overflow || unsigned_overflow then
let overflow_kind = if signed then Alarms.Signed else Alarms.Unsigned in
truncate_integer overflow_kind expr range value
else
- let v = Value.rewrap_integer range value in
- if range.Eval_typ.i_signed && not (Value.equal value v)
- then Self.warning ~wkey:Self.wkey_signed_overflow
- ~current:true ~once:true "2's complement assumed for overflow";
+ let v = Value.rewrap_integer context range value in
+ if range.Eval_typ.i_signed && not (Value.equal value v) then
+ Self.warning ~wkey:Self.wkey_signed_overflow
+ ~current:true ~once:true "2's complement assumed for overflow" ;
return v
let restrict_float ?(reduce=false) ~assume_finite expr fkind value =
@@ -450,10 +453,10 @@ module Make
| "non-finite" -> restrict_float ~assume_finite:true expr fk value
| _ -> assert false
- let assume_pointer expr value =
- let value, alarms =
- if Kernel.InvalidPointer.get ()
- then
+ let assume_pointer context expr value =
+ let open Evaluated.Operators in
+ let+ value =
+ if Kernel.InvalidPointer.get () then
let truth = Value.assume_pointer value in
let alarm () = Alarms.Invalid_pointer expr in
interpret_truth ~alarm value truth
@@ -462,9 +465,9 @@ module Make
(* Rewrap absolute addresses of pointer values, seen as unsigned
integers, to ensure a consistent representation of pointers. *)
let range = Eval_typ.pointer_range () in
- value >>-: Value.rewrap_integer range, alarms
+ Value.rewrap_integer context range value
- let handle_overflow ~may_overflow expr typ value =
+ let handle_overflow ~may_overflow context expr typ value =
match Eval_typ.classify_as_scalar typ with
| Some (Eval_typ.TSInt range) ->
(* If the operation cannot overflow, truncates the abstract value to the
@@ -474,80 +477,80 @@ module Make
the parameters of the analysis. *)
if not may_overflow
then fst (truncate_integer Alarms.Signed expr range value), Alarmset.none
- else handle_integer_overflow expr range value
+ else handle_integer_overflow context expr range value
| Some (Eval_typ.TSFloat fk) -> remove_special_float expr fk value
- | Some (Eval_typ.TSPtr _) -> assume_pointer expr value
+ | Some (Eval_typ.TSPtr _) -> assume_pointer context expr value
| None -> return value
(* Assumes that [res] is a valid result for the lvalue [lval] of type [typ].
Removes NaN and infinite floats and trap representations of bool values. *)
- let assume_valid_value typ lval res =
+ let assume_valid_value context typ lval res =
+ let open Evaluated.Operators in
+ let* value, origin = res in
match typ with
| TFloat (fkind, _) ->
- res >>= fun (value, origin) ->
let expr = Eva_utils.lval_to_exp lval in
- remove_special_float expr fkind value >>=: fun new_value ->
+ let+ new_value = remove_special_float expr fkind value in
+ new_value, origin
+ | TInt (IBool, _) when Kernel.InvalidBool.get () ->
+ let one = Abstract_value.Int Integer.one in
+ let truth = Value.assume_bounded Alarms.Upper_bound one value in
+ let alarm () = Alarms.Invalid_bool lval in
+ let+ new_value = interpret_truth ~alarm value truth in
new_value, origin
- | TInt (IBool, _) ->
- if Kernel.InvalidBool.get () then
- res >>= fun (value, origin) ->
- let one = Abstract_value.Int Integer.one in
- let truth = Value.assume_bounded Alarms.Upper_bound one value in
- let alarm () = Alarms.Invalid_bool lval in
- interpret_truth ~alarm value truth >>=: fun new_value ->
- new_value, origin
- else res
| TPtr _ ->
- res >>= fun (value, origin) ->
let expr = Eva_utils.lval_to_exp lval in
- assume_pointer expr value >>=: fun new_value ->
+ let+ new_value = assume_pointer context expr value in
new_value, origin
| _ -> res
(* Reduce the rhs argument of a shift so that it fits inside [size] bits. *)
let reduce_shift_rhs typ expr value =
+ let open Evaluated.Operators in
let size = Cil.bitsSizeOf typ in
let size_int = Abstract_value.Int (Integer.of_int (size - 1)) in
let zero_int = Abstract_value.Int Integer.zero in
let alarm () = Alarms.Invalid_shift (expr, Some size) in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int value in
- reduce_by_truth ~alarm (expr, value) truth >>= fun value ->
+ let* value = reduce_by_truth ~alarm (expr, value) truth in
let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
reduce_by_truth ~alarm (expr, value) truth
(* Reduces the right argument of a shift, and if [warn_negative] is true,
also reduces its left argument to a positive value. *)
let reduce_shift ~warn_negative typ (e1, v1) (e2, v2) =
- reduce_shift_rhs typ e2 v2 >>= fun v2 ->
- if warn_negative && Bit_utils.is_signed_int_enum_pointer typ
- then
+ let open Evaluated.Operators in
+ let* v2 = reduce_shift_rhs typ e2 v2 in
+ if warn_negative && Bit_utils.is_signed_int_enum_pointer typ then
(* Cannot shift a negative value *)
let zero_int = Abstract_value.Int Integer.zero in
let alarm () = Alarms.Invalid_shift (e1, None) in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int v1 in
- reduce_by_truth ~alarm (e1, v1) truth >>=: fun v1 ->
+ let+ v1 = reduce_by_truth ~alarm (e1, v1) truth in
v1, v2
else return (v1, v2)
(* Emits alarms for an index out of bound, and reduces its value. *)
let assume_valid_index ~size ~size_expr ~index_expr value =
+ let open Evaluated.Operators in
let size_int = Abstract_value.Int (Integer.pred size) in
let zero_int = Abstract_value.Int Integer.zero in
let alarm () = Alarms.Index_out_of_bound (index_expr, None) in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int value in
- reduce_by_truth ~alarm (index_expr, value) truth >>= fun value ->
+ let* value = reduce_by_truth ~alarm (index_expr, value) truth in
let alarm () = Alarms.Index_out_of_bound (index_expr, Some size_expr) in
let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
reduce_by_truth ~alarm (index_expr, value) truth
let assume_valid_binop typ (e1, v1 as arg1) op (e2, v2 as arg2) =
- if Cil.isIntegralType typ
- then
+ let open Evaluated.Operators in
+ if Cil.isIntegralType typ then
match op with
| Div | Mod ->
let truth = Value.assume_non_zero v2 in
let alarm () = Alarms.Division_by_zero e2 in
- reduce_by_truth ~alarm arg2 truth >>=: fun v2 -> v1, v2
+ let+ v2 = reduce_by_truth ~alarm arg2 truth in
+ v1, v2
| Shiftrt ->
let warn_negative = Kernel.RightShiftNegative.get () in
reduce_shift ~warn_negative typ arg1 arg2
@@ -566,25 +569,23 @@ module Make
(* Pretty prints the result of a comparison independently of the value
abstractions used. *)
let pretty_zero_or_one fmt v =
- let str =
- if Value.(equal v zero) then "{0}"
- else if Value.(equal v one) then "{1}"
- else "{0; 1}"
- in
- Format.fprintf fmt "%s" str
+ let print = Format.pp_print_string fmt in
+ if Value.(equal v zero) then print "{0}"
+ else if Value.(equal v one) then print "{1}"
+ else print "{0; 1}"
let forward_comparison ~compute typ kind (e1, v1) (e2, v2) =
let truth = Value.assume_comparable kind v1 v2 in
let alarm () = Alarms.Pointer_comparison (e1, e2) in
let propagate_all = propagate_all_pointer_comparison typ in
let args, alarms =
- if warn_pointer_comparison typ
- then if propagate_all
+ if warn_pointer_comparison typ then
+ if propagate_all
then `Value (v1, v2), snd (interpret_truth ~alarm (v1, v2) truth)
else reduce_by_double_truth ~alarm (e1, v1) (e2, v2) truth
else `Value (v1, v2), Alarmset.none
in
- let result = args >>- fun (v1, v2) -> compute v1 v2 in
+ let result = let* v1, v2 = args in compute v1 v2 in
let value =
if is_true truth || not propagate_all
then result
@@ -600,26 +601,26 @@ module Make
in
value, alarms
- let forward_binop typ (e1, v1 as arg1) op arg2 =
+ let forward_binop context typ (e1, v1 as arg1) op arg2 =
+ let open Evaluated.Operators in
let typ_e1 = Cil.unrollType (Cil.typeOf e1) in
match comparison_kind op with
| Some kind ->
- let compute v1 v2 = Value.forward_binop typ_e1 op v1 v2 in
+ let compute v1 v2 = Value.forward_binop context typ_e1 op v1 v2 in
(* Detect zero expressions created by the evaluator *)
let e1 = if Eva_utils.is_value_zero e1 then None else Some e1 in
forward_comparison ~compute typ_e1 kind (e1, v1) arg2
| None ->
- assume_valid_binop typ arg1 op arg2 >>=. fun (v1, v2) ->
- Value.forward_binop typ_e1 op v1 v2
+ let& v1, v2 = assume_valid_binop typ arg1 op arg2 in
+ Value.forward_binop context typ_e1 op v1 v2
- let forward_unop unop (e, v as arg) =
+ let forward_unop context unop (e, v as arg) =
let typ = Cil.unrollType (Cil.typeOf e) in
- if unop = LNot
- then
+ if unop = LNot then
let kind = Abstract_value.Equality in
- let compute _ v = Value.forward_unop typ unop v in
+ let compute _ v = Value.forward_unop context typ unop v in
forward_comparison ~compute typ kind (None, Value.zero) arg
- else Value.forward_unop typ unop v, Alarmset.none
+ else Value.forward_unop context typ unop v, Alarmset.none
(* ------------------------------------------------------------------------
Casts
@@ -628,12 +629,12 @@ module Make
type integer_range = Eval_typ.integer_range = { i_bits: int; i_signed: bool }
let cast_integer overflow_kind expr ~src ~dst value =
- let value =
+ let open Evaluated.Operators in
+ let* value =
if Eval_typ.(Integer.lt (range_lower_bound src) (range_lower_bound dst))
then truncate_lower_bound overflow_kind expr dst value
else return value
in
- value >>= fun value ->
if Eval_typ.(Integer.gt (range_upper_bound src) (range_upper_bound dst))
then truncate_upper_bound overflow_kind expr dst value
else return value
@@ -642,24 +643,23 @@ module Make
first converts the value to the signed counterpart of the source type, and
then downcasts it into the signed destination type. Emits only alarms for
the second cast. *)
- let relaxed_signed_downcast expr ~src ~dst value =
+ let relaxed_signed_downcast context expr ~src ~dst value =
let expr, src, value =
- if not src.i_signed
- then
+ if not src.i_signed then
let signed_src = { src with i_signed = true } in
- let signed_v = Value.rewrap_integer signed_src value in
+ let signed_v = Value.rewrap_integer context signed_src value in
let signed_exp = exp_alarm_signed_converted_downcast expr in
signed_exp, signed_src, signed_v
else expr, src, value
in
cast_integer Alarms.Signed_downcast expr ~src ~dst value
- let cast_int_to_int expr ~ptr ~src ~dst value =
+ let cast_int_to_int context expr ~ptr ~src ~dst value =
(* Regain some precision in case a transfer function was imprecise.
This should probably be done in the transfer function, though. *)
let value =
if Value.(equal top_int value)
- then Value.rewrap_integer src value
+ then Value.rewrap_integer context src value
else value
in
if Eval_typ.range_inclusion src dst
@@ -675,8 +675,8 @@ module Make
if warn ()
then cast_integer overflow_kind expr ~src ~dst value
else if dst.i_signed && Parameters.WarnSignedConvertedDowncast.get ()
- then relaxed_signed_downcast expr ~src ~dst value
- else return (Value.rewrap_integer dst value)
+ then relaxed_signed_downcast context expr ~src ~dst value
+ else return (Value.rewrap_integer context dst value)
(* Re-export type here *)
type scalar_typ = Eval_typ.scalar_typ =
@@ -706,43 +706,48 @@ module Make
reduce_by_truth ~alarm (expr, value) truth
let truncate_float fkind dst_range expr value =
+ let open Evaluated.Operators in
let max_bound = Eval_typ.range_upper_bound dst_range in
let bound_kind = Alarms.Upper_bound in
- truncate_float_bound fkind max_bound bound_kind expr value >>= fun value ->
+ let* value = truncate_float_bound fkind max_bound bound_kind expr value in
let min_bound = Eval_typ.range_lower_bound dst_range in
let bound_kind = Alarms.Lower_bound in
truncate_float_bound fkind min_bound bound_kind expr value
- let forward_cast ~dst expr value =
+ let forward_cast context ~dst expr value =
+ let open Evaluated.Operators in
let src = Cil.typeOf expr in
match Eval_typ.(classify_as_scalar src, classify_as_scalar dst) with
| None, _ | _, None -> return value (* Unclear whether this happens. *)
| Some src_type, Some dst_type ->
- let value, alarms =
+ let& value =
match src_type, dst_type with
| TSPtr src, TSInt dst ->
- cast_int_to_int ~ptr:true ~src ~dst expr value
+ cast_int_to_int context ~ptr:true ~src ~dst expr value
| TSInt src, (TSInt dst | TSPtr dst) ->
- cast_int_to_int ~ptr:false ~src ~dst expr value
+ cast_int_to_int context ~ptr:false ~src ~dst expr value
| TSFloat src, (TSInt dst | TSPtr dst) ->
- restrict_float ~reduce:true ~assume_finite:true expr src value >>=
- truncate_float src dst expr
+ let reduce = true and assume_finite = true in
+ let* value = restrict_float ~reduce ~assume_finite expr src value in
+ truncate_float src dst expr value
| (TSInt _ | TSPtr _), TSFloat _ ->
(* Cannot overflow with 32 bits float. *)
return value
| TSFloat _, TSFloat _ | TSPtr _, TSPtr _ -> return value
in
- value >>- Value.forward_cast ~src_type ~dst_type, alarms
+ Value.forward_cast context ~src_type ~dst_type value
(* ------------------------------------------------------------------------
Forward Evaluation
------------------------------------------------------------------------ *)
- (* The forward evaluation context: arguments that must be passed through
+ (* The forward evaluation environment: arguments that must be passed through
the mutually recursive evaluation functions without being modified. *)
- type context =
+ type recursive_environment =
{ (* The abstract domain state in which the evaluation takes place. *)
state: Domain.t;
+ (* The abstract context in which the evaluation takes place. *)
+ context: Context.t Abstract_value.enriched;
(* Is the expression currently processed the "root" expression being
evaluated, or is it a sub-expression? Useful for domain queries. *)
root: bool;
@@ -756,27 +761,27 @@ module Make
remaining_fuel: int;
(* The oracle which can be used by abstract domains to get a value for
some expressions. *)
- oracle: context -> exp -> Value.t evaluated;
+ oracle: recursive_environment -> exp -> Value.t evaluated;
}
- (* Builds the query to the domain from the context. *)
- let make_domain_query query context =
- let { state; oracle; root; subdivision; subdivided; } = context in
- let oracle = oracle context in
- let domain_context = Abstract_domain.{ root; subdivision; subdivided; } in
- query ~oracle domain_context state
+ (* Builds the query to the domain from the environment. *)
+ let make_domain_query query env =
+ let { state; oracle; root; subdivision; subdivided; } = env in
+ let oracle = oracle env in
+ let domain_env = Abstract_domain.{ root; subdivision; subdivided; } in
+ query ~oracle domain_env state
(* Returns the cached value and alarms for the evaluation if it exists;
call [coop_forward_eval] and caches its result otherwise.
Also returns a boolean indicating whether the expression is volatile. *)
- let rec root_forward_eval context expr =
+ let rec root_forward_eval env expr =
(* Search in the cache for the result of a previous computation. *)
try
let record, report = Cache.find' !cache expr in
(* If the record was computed with more fuel than [fuel], return it. *)
if report.fuel = Loop then fuel_consumed := true;
- if less_fuel_than context.remaining_fuel report.fuel
- then (record.value.v >>-: fun v -> v, report.volatile), record.val_alarms
+ if less_fuel_than env.remaining_fuel report.fuel
+ then (let+ v = record.value.v in v, report.volatile), record.val_alarms
else raise Not_found
(* If no result found, evaluate the expression. *)
with Not_found ->
@@ -786,25 +791,25 @@ module Make
(* Fill the cache to avoid loops in the use of the oracle. *)
cache := Cache.add' !cache expr top_entry;
(* Evaluation of [expr]. *)
- let result, alarms = coop_forward_eval context expr in
+ let result, alarms = coop_forward_eval env expr in
let value =
- result >>- fun (record, reduction, volatile) ->
+ let* record, reduction, volatile = result in
(* Put the alarms in the record. *)
let record = { record with val_alarms = alarms } in
(* Inter-reduction of the value (in case of a reduced product). *)
let record = reduce_value record in
(* Cache the computed result with an appropriate report. *)
- let fuel = context.remaining_fuel in
+ let fuel = env.remaining_fuel in
let fuel = if !fuel_consumed then Finite fuel else Infty in
let report = {fuel; reduction; volatile} in
cache := Cache.add' !cache expr (record, report);
- record.value.v >>-: fun v -> v, volatile
+ let+ v = record.value.v in v, volatile
in
(* Reset the flag fuel_consumed. *)
fuel_consumed := previous_fuel_consumed || !fuel_consumed;
value, alarms
- and forward_eval context expr = root_forward_eval context expr >>=: fst
+ and forward_eval env expr = root_forward_eval env expr >>=: fst
(* The functions below returns, along with the computed value (when it is not
bottom):
@@ -815,26 +820,26 @@ module Make
(* Asks the abstract domain for abstractions (value and alarms) of [expr],
and performs the narrowing with the abstractions computed by
[internal_forward_eval]. *)
- and coop_forward_eval context expr =
+ and coop_forward_eval env expr =
match expr.enode with
- | Lval lval -> eval_lval context lval
- | BinOp _ | UnOp _ | CastE _ -> begin
- let domain_query = make_domain_query Domain.extract_expr context in
- let context = { context with root = false } in
- let intern_value, alarms = internal_forward_eval context expr in
- let domain_value, alarms' = domain_query expr in
- (* Intersection of alarms, as each sets of alarms are correct
- and "complete" for the evaluation of [expr]. *)
- match Alarmset.inter alarms alarms' with
+ | Lval lval -> eval_lval env lval
+ | BinOp _ | UnOp _ | CastE _ ->
+ let domain_query = make_domain_query Domain.extract_expr env in
+ let env = { env with root = false } in
+ let intern_value, alarms = internal_forward_eval env expr in
+ let domain_value, alarms' = domain_query expr in
+ (* Intersection of alarms, as each sets of alarms are correct
+ and "complete" for the evaluation of [expr]. *)
+ begin match Alarmset.inter alarms alarms' with
| `Inconsistent ->
(* May happen for a product of states with no concretization. Such
cases are reported to the user by transfer_stmt. *)
`Bottom, Alarmset.none
| `Value alarms ->
let v =
- intern_value >>- fun (intern_value, reduction, volatile) ->
- domain_value >>- fun (domain_value, origin) ->
- Value.narrow intern_value domain_value >>-: fun result ->
+ let* intern_value, reduction, volatile = intern_value in
+ let* domain_value, origin = domain_value in
+ let+ result = Value.narrow intern_value domain_value in
let reductness =
if Value.equal domain_value result then Unreduced
else if Value.(equal domain_value top) then Created else Reduced
@@ -849,53 +854,51 @@ module Make
v, alarms
end
| _ ->
- internal_forward_eval context expr
- >>=: fun (value, reduction, volatile) ->
- let value = define_value value
- and origin = None
- and reductness = Dull in
- {value; origin; reductness; val_alarms = Alarmset.all},
- reduction, volatile
+ let open Evaluated.Operators in
+ let+ value, reduction, volatile = internal_forward_eval env expr in
+ let value = define_value value and origin = None in
+ let reductness = Dull and val_alarms = Alarmset.all in
+ { value; origin; reductness; val_alarms }, reduction, volatile
(* Recursive descent in the sub-expressions. *)
- and internal_forward_eval context expr =
+ and internal_forward_eval env expr =
+ let open Evaluated.Operators in
let compute_reduction (v, a) volatile =
- (v, a) >>=: fun v ->
+ let+ v = (v, a) in
let reduction = if Alarmset.is_empty a then Neither else Forward in
v, reduction, volatile
in
match expr.enode with
- | Const constant -> internal_forward_eval_constant context expr constant
+ | Const constant -> internal_forward_eval_constant env expr constant
| Lval _lval -> assert false
| AddrOf v | StartOf v ->
- lval_to_loc context ~for_writing:false ~reduction:false v
- >>= fun (loc, _, _) ->
- (Loc.to_value loc, Alarmset.none) >>= fun value ->
- let v = assume_pointer expr value in
+ let* loc, _, _ = lval_to_loc env ~for_writing:false ~reduction:false v in
+ let* value = Loc.to_value loc, Alarmset.none in
+ let v = assume_pointer env.context expr value in
compute_reduction v false
| UnOp (op, e, typ) ->
- root_forward_eval context e >>= fun (v, volatile) ->
- forward_unop op (e, v) >>= fun v ->
+ let* v, volatile = root_forward_eval env e in
+ let* v = forward_unop env.context op (e, v) in
let may_overflow = op = Neg in
- let v = handle_overflow ~may_overflow expr typ v in
+ let v = handle_overflow ~may_overflow env.context expr typ v in
compute_reduction v volatile
| BinOp (op, e1, e2, typ) ->
- root_forward_eval context e1 >>= fun (v1, volatile1) ->
- root_forward_eval context e2 >>= fun (v2, volatile2) ->
- forward_binop typ (e1, v1) op (e2, v2) >>= fun v ->
+ let* v1, volatile1 = root_forward_eval env e1 in
+ let* v2, volatile2 = root_forward_eval env e2 in
+ let* v = forward_binop env.context typ (e1, v1) op (e2, v2) in
let may_overflow = may_overflow op in
- let v = handle_overflow ~may_overflow expr typ v in
+ let v = handle_overflow ~may_overflow env.context expr typ v in
compute_reduction v (volatile1 || volatile2)
| CastE (dst, e) ->
- root_forward_eval context e >>= fun (value, volatile) ->
- let v = forward_cast ~dst e value in
+ let* value, volatile = root_forward_eval env e in
+ let v = forward_cast env.context ~dst e value in
let v = match Cil.unrollType dst with
- | TFloat (fkind, _) -> v >>= remove_special_float expr fkind
- | TPtr _ -> v >>= assume_pointer expr
+ | TFloat (fkind, _) -> let* v in remove_special_float expr fkind v
+ | TPtr _ -> let* v in assume_pointer env.context expr v
| _ -> v
in
compute_reduction v volatile
@@ -905,17 +908,19 @@ module Make
| Some v -> return (Value.inject_int (Cil.typeOf expr) v, Neither, false)
| _ -> return (Value.top_int, Neither, false)
- and internal_forward_eval_constant context expr constant =
- let eval = match constant with
- | CEnum {eival = e} -> forward_eval context e
+ and internal_forward_eval_constant env expr constant =
+ let open Evaluated.Operators in
+ let+ value =
+ match constant with
+ | CEnum {eival = e} -> forward_eval env e
| CReal (_f, fkind, _fstring) ->
- let value = Value.constant expr constant in
+ let value = Value.constant env.context expr constant in
remove_special_float expr fkind value
(* Integer constants never overflow, because the front-end chooses a
suitable type. *)
- | _ -> return (Value.constant expr constant)
+ | _ -> return (Value.constant env.context expr constant)
in
- eval >>=: fun value -> value, Neither, false
+ value, Neither, false
(* ------------------------------------------------------------------------
@@ -930,14 +935,12 @@ module Make
If the location is not bottom, the function also returns the typ of the
lvalue, and a boolean indicating that the lvalue contains a sub-expression
with volatile qualifier (in its host or offset). *)
- and lval_to_loc context ~for_writing ~reduction lval =
+ and lval_to_loc env ~for_writing ~reduction lval =
let compute () =
- let res, alarms =
- reduced_lval_to_loc context ~for_writing ~reduction lval
- in
+ let res, alarms = reduced_lval_to_loc env ~for_writing ~reduction lval in
let res =
- res >>-: fun (loc, typ_offs, red, volatile) ->
- let fuel = context.remaining_fuel in
+ let+ loc, typ_offs, red, volatile = res in
+ let fuel = env.remaining_fuel in
let record = { loc; typ = typ_offs; loc_alarms = alarms }
and report = { fuel = Finite fuel; reduction = red; volatile }
and loc_report = { for_writing; with_reduction = reduction } in
@@ -946,79 +949,74 @@ module Make
in
res, alarms
in
+ let already_precise = already_precise_loc_report ~for_writing ~reduction in
+ let not_enough_fuel = less_fuel_than env.remaining_fuel in
match Cache.find_loc' !cache lval with
| `Value (record, (report, loc_report)) ->
- if
- already_precise_loc_report ~for_writing ~reduction loc_report
- && less_fuel_than context.remaining_fuel report.fuel
+ if already_precise loc_report && not_enough_fuel report.fuel
then `Value (record.loc, record.typ, report.volatile), record.loc_alarms
else compute ()
| `Top -> compute ()
(* If [reduction] is false, don't reduce the location and the offset by their
valid parts, and don't emit alarms about their validity. *)
- and reduced_lval_to_loc context ~for_writing ~reduction lval =
- internal_lval_to_loc context ~for_writing ~reduction lval
- >>= fun (loc, typ, volatile) ->
- if not reduction
- then `Value (loc, typ, Neither, volatile), Alarmset.none
- else
+ and reduced_lval_to_loc env ~for_writing ~reduction lval =
+ let open Evaluated.Operators in
+ let lval_to_loc = internal_lval_to_loc env ~for_writing ~reduction in
+ let* loc, typ, volatile = lval_to_loc lval in
+ if reduction then
let bitfield = Cil.isBitfield lval in
let truth = Loc.assume_valid_location ~for_writing ~bitfield loc in
- let alarm () =
- let access_kind =
- if for_writing then Alarms.For_writing else Alarms.For_reading
- in
- Alarms.Memory_access (lval, access_kind)
- in
- interpret_truth ~alarm loc truth >>=: fun valid_loc ->
+ let access = Alarms.(if for_writing then For_writing else For_reading) in
+ let alarm () = Alarms.Memory_access (lval, access) in
+ let+ valid_loc = interpret_truth ~alarm loc truth in
let reduction = if Loc.equal_loc valid_loc loc then Neither else Forward in
valid_loc, typ, reduction, volatile
+ else `Value (loc, typ, Neither, volatile), Alarmset.none
(* Internal evaluation of a lvalue to an abstract location.
Combination of the evaluation of the right part of an lval (an host) with
an offset, to obtain a location *)
- and internal_lval_to_loc context ~for_writing ~reduction lval =
+ and internal_lval_to_loc env ~for_writing ~reduction lval =
+ let open Evaluated.Operators in
let host, offset = lval in
- let typ = match host with
- | Var host -> host.vtype
- | Mem x -> Cil.typeOf_pointed (Cil.typeOf x)
- in
- eval_offset context ~reduce_valid_index:reduction typ offset
- >>= fun (offs, typ_offs, offset_volatile) ->
- if for_writing && Eva_utils.is_const_write_invalid typ_offs
- then
- `Bottom,
- Alarmset.singleton ~status:Alarmset.False
- (Alarms.Memory_access (lval, Alarms.For_writing))
+ let typ = Cil.typeOfLhost host in
+ let evaluated = eval_offset env ~reduce_valid_index:reduction typ offset in
+ let* (offs, typ_offs, offset_volatile) = evaluated in
+ if for_writing && Eva_utils.is_const_write_invalid typ_offs then
+ let alarm = Alarms.(Memory_access (lval, For_writing)) in
+ `Bottom, Alarmset.singleton ~status:Alarmset.False alarm
else
- eval_host context typ_offs offs host >>=: fun (loc, host_volatile) ->
+ let+ loc, host_volatile = eval_host env typ_offs offs host in
loc, typ_offs, offset_volatile || host_volatile
(* Host evaluation. Also returns a boolean which is true if the host
contains a volatile sub-expression. *)
- and eval_host context typ_offset offs = function
+ and eval_host env typ_offset offs = function
| Var host ->
- (Loc.forward_variable typ_offset host offs >>-: fun loc -> loc, false),
- Alarmset.none
+ let loc = Loc.forward_variable typ_offset host offs in
+ (let+ loc in loc, false), Alarmset.none
| Mem x ->
- root_forward_eval context x >>=. fun (loc_lv, volatile) ->
- Loc.forward_pointer typ_offset loc_lv offs >>-: fun loc ->
+ let open Evaluated.Operators in
+ let& loc_lv, volatile = root_forward_eval env x in
+ let open Bottom.Operators in
+ let+ loc = Loc.forward_pointer typ_offset loc_lv offs in
loc, volatile
(* Offset evaluation. Also returns a boolean which is true if the offset
contains a volatile sub-expression. *)
- and eval_offset context ~reduce_valid_index typ = function
+ and eval_offset env ~reduce_valid_index typ = function
| NoOffset -> return (Loc.no_offset, typ, false)
| Index (index_expr, remaining) ->
- let typ_pointed, array_size = match Cil.unrollType typ with
+ let open Evaluated.Operators in
+ let typ_pointed, array_size =
+ match Cil.unrollType typ with
| TArray (t, size, _) -> t, size
- | t -> Self.fatal ~current:true
- "Got type '%a'" Printer.pp_typ t
+ | t -> Self.fatal ~current:true "Got type '%a'" Printer.pp_typ t
in
- eval_offset context ~reduce_valid_index typ_pointed remaining >>=
- fun (roffset, typ_offs, remaining_volatile) ->
- root_forward_eval context index_expr >>= fun (index, volatile) ->
+ let eval = eval_offset env ~reduce_valid_index typ_pointed remaining in
+ let* roffset, typ_offs, remaining_volatile = eval in
+ let* index, volatile = root_forward_eval env index_expr in
let valid_index =
if not (Kernel.SafeArrays.get ()) || not reduce_valid_index
then `Value index, Alarmset.none
@@ -1033,26 +1031,27 @@ module Make
else
let size_expr = Option.get array_size in (* array_size exists *)
assume_valid_index ~size ~size_expr ~index_expr index
- with
- | Cil.LenOfArray _ -> `Value index, Alarmset.none (* unknown array size *)
+ with Cil.LenOfArray _ -> `Value index, Alarmset.none (* unknown array size *)
in
- valid_index >>=: fun index ->
+ let+ index = valid_index in
Loc.forward_index typ_pointed index roffset, typ_offs,
remaining_volatile || volatile
| Field (fi, remaining) ->
+ let open Evaluated.Operators in
let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
let typ_fi = Cil.typeAddAttributes attrs fi.ftype in
- eval_offset context ~reduce_valid_index typ_fi remaining
- >>=: fun (r, typ_res, volatile) ->
+ let evaluated = eval_offset env ~reduce_valid_index typ_fi remaining in
+ let+ r, typ_res, volatile = evaluated in
let off = Loc.forward_field typ fi r in
off, typ_res, volatile
- and eval_lval ?(indeterminate=false) context lval =
- let domain_query = make_domain_query Domain.extract_lval context in
- let context = { context with root = false } in
+ and eval_lval ?(indeterminate=false) env lval =
+ let open Evaluated.Operators in
+ let domain_query = make_domain_query Domain.extract_lval env in
+ let env = { env with root = false } in
(* Computes the location of [lval]. *)
- lval_to_loc context ~for_writing:false ~reduction:true lval
- >>= fun (loc, typ_lv, volatile_expr) ->
+ let evaluated = lval_to_loc env ~for_writing:false ~reduction:true lval in
+ let* loc, typ_lv, volatile_expr = evaluated in
let typ_lv = Cil.unrollType typ_lv in
(* the lvalue is volatile:
- if it has qualifier volatile (lval_to_loc propagates qualifiers
@@ -1063,19 +1062,18 @@ module Make
(* Find the value of the location, if not bottom. *)
let v, alarms = domain_query lval typ_lv loc in
let alarms = close_dereference_alarms lval alarms in
- if indeterminate
- then
+ if indeterminate then
let record, alarms = indeterminate_copy lval v alarms in
`Value (record, Neither, volatile), alarms
else
- let v, alarms = assume_valid_value typ_lv lval (v, alarms) in
- (v, alarms) >>=: fun (value, origin) ->
- let value = define_value value
- and reductness, reduction =
+ let v, alarms = assume_valid_value env.context typ_lv lval (v, alarms) in
+ let+ value, origin = v, alarms in
+ let value = define_value value in
+ let reductness, reduction =
if Alarmset.is_empty alarms then Unreduced, Neither else Reduced, Forward
in
(* The proper alarms will be set in the record by forward_eval. *)
- {value; origin; reductness; val_alarms = Alarmset.all},
+ { value; origin; reductness; val_alarms = Alarmset.all },
reduction, volatile
(* ------------------------------------------------------------------------
@@ -1085,32 +1083,29 @@ module Make
(* These two modules could be implemented as mutually recursive, to avoid
the reference for the oracle given to the domains. *)
module Forward_Evaluation = struct
- type nonrec context = context
- let evaluate ~subdivided context valuation expr =
+ type environment = recursive_environment
+ let evaluate ~subdivided environment valuation expr =
+ let open Evaluated.Operators in
cache := valuation;
- let context =
- if subdivided
- then { context with root = false; subdivided }
- else context
- in
- root_forward_eval context expr >>=: fun (value, _) ->
+ let root = not subdivided && environment.root in
+ let subdivided = subdivided || environment.subdivided in
+ let environment = { environment with root ; subdivided } in
+ let+ value, _ = root_forward_eval environment expr in
!cache, value
end
module Subdivided_Evaluation =
Subdivided_evaluation.Make (Value) (Loc) (Cache) (Forward_Evaluation)
- let oracle context =
- let remaining_fuel = pred context.remaining_fuel in
- if remaining_fuel > 0
- then
+ let oracle env =
+ let remaining_fuel = pred env.remaining_fuel in
+ if remaining_fuel > 0 then
fun expr ->
let valuation = !cache in
- let context = { context with remaining_fuel } in
- let subdivnb = context.subdivision in
- let eval, alarms =
- Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
- in
+ let env = { env with remaining_fuel } in
+ let subdivnb = env.subdivision in
+ let evaluate = Subdivided_Evaluation.evaluate env valuation in
+ let eval, alarms = evaluate ~subdivnb expr in
(* Always reset the reference to the cached valuation after a subdivided
evaluation (as the multiple evaluations modify the cache). *)
match eval with
@@ -1123,36 +1118,39 @@ module Make
| `Value (valuation, value) ->
cache := valuation;
`Value value, alarms
- else
- fun _ -> fuel_consumed := true; `Value Value.top, Alarmset.all
+ else fun _ -> fuel_consumed := true; `Value Value.top, Alarmset.all
+
+ (* Context from state [state]. *)
+ let get_context state =
+ let+ from_domains = Domain.build_context state in
+ Abstract_value.{ from_domains }
- (* Context for the forward evaluation of a root expression in state [state]
+ (* Environment for the forward evaluation of a root expression in state [state]
with maximal precision. *)
- let root_context ?subdivnb state =
+ let root_environment ?subdivnb state =
+ let+ context = get_context state in
+ let subdivided = false and root = true in
let remaining_fuel = root_fuel () in
(* By default, use the number of subdivision defined by the global option
-eva-subdivide-non-linear. *)
- let subdivision =
- match subdivnb with
- | None -> Parameters.LinearLevel.get ()
- | Some n -> n
- in
- let subdivided = false in
- { state; root = true; subdivision; subdivided; remaining_fuel; oracle }
+ let default () = Parameters.LinearLevel.get () in
+ let subdivision = match subdivnb with None -> default () | Some n -> n in
+ { state; context; root; subdivision; subdivided; remaining_fuel; oracle }
- (* Context for a fast forward evaluation with minimal precision:
+ (* Environment for a fast forward evaluation with minimal precision:
no subdivisions, no calls to the oracle, and the expression is not
considered as a "root" expression. *)
- let fast_eval_context state =
- let remaining_fuel = no_fuel in
- let subdivision = 0 in
- let subdivided = false in
- { state; root = false; subdivision; subdivided; remaining_fuel; oracle }
+ let fast_eval_environment state =
+ let+ context = get_context state in
+ let remaining_fuel = no_fuel and root = false in
+ let subdivision = 0 and subdivided = false in
+ { state; context; root; subdivision; subdivided; remaining_fuel; oracle }
let subdivided_forward_eval valuation ?subdivnb state expr =
- let context = root_context ?subdivnb state in
- let subdivnb = context.subdivision in
- Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
+ let open Evaluated.Operators in
+ let* env = root_environment ?subdivnb state, Alarmset.none in
+ let subdivnb = env.subdivision in
+ Subdivided_Evaluation.evaluate env valuation ~subdivnb expr
(* ------------------------------------------------------------------------
Backward Evaluation
@@ -1167,16 +1165,14 @@ module Make
(* Find the record computed for an lvalue.
Return None if no reduction can be performed. *)
let find_loc_for_reduction lval =
- if not (may_be_reduced_lval lval)
- then None
- else
- let record, report = match Cache.find_loc' !cache lval with
+ if may_be_reduced_lval lval then
+ let record, report =
+ match Cache.find_loc' !cache lval with
| `Value all -> all
| `Top -> assert false
in
- if (snd report).with_reduction
- then Some (record, report)
- else None
+ if (snd report).with_reduction then Some (record, report) else None
+ else None
(* Evaluate an expression before any reduction, if needed. Also return the
report indicating if a forward reduction during the forward evaluation may
@@ -1184,7 +1180,8 @@ module Make
let evaluate_for_reduction state expr =
try `Value (Cache.find' !cache expr)
with Not_found ->
- fst (forward_eval (fast_eval_context state) expr) >>-: fun _ ->
+ let* env = fast_eval_environment state in
+ let+ _ = forward_eval env expr |> fst in
try Cache.find' !cache expr
with Not_found -> assert false
@@ -1197,13 +1194,13 @@ module Make
the reduction is propagated but the value of the current expression is
unchanged. *)
let backward_reduction old_value latter_reduction value =
- let propagate_forward_reduction () =
- if latter_reduction = Forward then Some (old_value, Neither) else None
- in
+ let forward = latter_reduction = Forward in
+ let neither () = Some (old_value, Neither) in
+ let propagate_forward_reduction () = if forward then neither () else None in
match value with
| None -> `Value (propagate_forward_reduction ())
| Some new_value ->
- Value.narrow old_value new_value >>-: fun value ->
+ let+ value = Value.narrow old_value new_value in
if Value.is_included old_value value
then propagate_forward_reduction ()
else Some (value, Backward)
@@ -1214,36 +1211,39 @@ module Make
abstract domains) are propagated backward to the subexpressions;
- if [value = Some v], then [expr] is assumed to evaluate to [v] (and is
reduced accordingly). *)
- let rec backward_eval fuel state expr value =
+ let rec backward_eval fuel context state expr value =
(* Evaluate the expression if needed. *)
- evaluate_for_reduction state expr >>- fun (record, report) ->
+ let* record, report = evaluate_for_reduction state expr in
(* Reduction of [expr] by [value]. Also performs further reductions
requested by the domains. Returns Bottom if one of these reductions
leads to bottom. *)
let reduce kind value =
let continue = `Value () in
(* Avoids reduction of volatile expressions. *)
- if report.volatile then continue
- else
+ if not report.volatile then
let value = Value.reduce value in
- reduce_expr_recording kind expr (record, report) value;
+ reduce_expr_recording kind expr (record, report) value ;
(* If enough fuel, asks the domain for more reductions. *)
- if fuel > 0
- then
+ if fuel > 0 then
(* The reductions requested by the domains. *)
let reductions_list = Domain.reduce_further state expr value in
- let reduce acc (expr, v) =
- acc >>- fun () -> backward_eval (pred fuel) state expr (Some v)
+ (* Reduces [expr] to value [v]. *)
+ let reduce acc (expr, value) =
+ (* If a previous reduction has returned bottom, return bottom. *)
+ let* () = acc in
+ backward_eval (pred fuel) context state expr (Some value)
in
List.fold_left reduce continue reductions_list
else continue
+ else continue
in
- record.value.v >>- fun old_value ->
+ let* old_value = record.value.v in
(* Determines the need of a backward reduction. *)
- backward_reduction old_value report.reduction value >>- function
+ let* reduced = backward_reduction old_value report.reduction value in
+ match reduced with
| None ->
(* If no reduction to be propagated, just visit the subterms. *)
- recursive_descent fuel state expr
+ recursive_descent fuel context state expr
| Some (value, kind) ->
(* Otherwise, backward propagation to the subterms. *)
match expr.enode with
@@ -1252,95 +1252,92 @@ module Make
(* For a lvalue, we try to reduce its location according to the value;
this operation may lead to a more precise value for this lvalue,
which is then reduced accordingly. *)
- backward_loc state lval value >>- function
+ let* reduced_loc = backward_loc state lval value in
+ match reduced_loc with
| None ->
- reduce kind value >>- fun () ->
- recursive_descent_lval fuel state lval
+ let* () = reduce kind value in
+ recursive_descent_lval fuel context state lval
| Some (loc, new_value) ->
- let kind =
- if Value.is_included old_value new_value then Neither else Backward
- in
- reduce kind new_value >>- fun () ->
- internal_backward_lval fuel state loc lval
+ let included = Value.is_included old_value new_value in
+ let kind = if included then Neither else Backward in
+ let* () = reduce kind new_value in
+ internal_backward_lval fuel context state loc lval
end
| _ ->
- reduce kind value >>- fun () ->
- internal_backward fuel state expr value
+ let* () = reduce kind value in
+ internal_backward fuel context state expr value
(* Backward propagate the reduction [expr] = [value] to the subterms of the
compound expression [expr]. *)
- and internal_backward fuel state expr value =
+ and internal_backward fuel context state expr value =
match expr.enode with
| Lval _lv -> assert false
| UnOp (LNot, e, _) ->
let cond = Eva_utils.normalize_as_cond e false in
(* TODO: should we compute the meet with the result of the call to
Value.backward_unop? *)
- backward_eval fuel state cond (Some value)
+ backward_eval fuel context state cond (Some value)
| UnOp (op, e, _typ) ->
- let typ_e = Cil.unrollType (Cil.typeOf e) in
- find_val e >>- fun v ->
- Value.backward_unop ~typ_arg:typ_e op ~arg:v ~res:value
- >>- fun v ->
- backward_eval fuel state e v
+ let typ_arg = Cil.unrollType (Cil.typeOf e) in
+ let* arg = find_val e in
+ let* v = Value.backward_unop context ~typ_arg op ~arg ~res:value in
+ backward_eval fuel context state e v
| BinOp (binop, e1, e2, typ) ->
- let typ_res = Cil.unrollType typ
- and typ_e1 = Cil.typeOf e1 in
- find_val e1 >>- fun v1 ->
- find_val e2 >>- fun v2 ->
- Value.backward_binop
- ~input_type:typ_e1
- ~resulting_type:typ_res
- binop ~left:v1 ~right:v2 ~result:value
- >>- fun (v1, v2) ->
- backward_eval fuel state e1 v1 >>- fun () ->
- backward_eval fuel state e2 v2
+ let resulting_type = Cil.unrollType typ in
+ let input_type = Cil.typeOf e1 in
+ let* left = find_val e1
+ and* right = find_val e2 in
+ let backward = Value.backward_binop context ~input_type ~resulting_type in
+ let* v1, v2 = backward binop ~left ~right ~result:value in
+ let* () = backward_eval fuel context state e1 v1 in
+ backward_eval fuel context state e2 v2
| CastE (typ, e) ->
begin
let dst_typ = Cil.unrollType typ in
let src_typ = Cil.unrollType (Cil.typeOf e) in
- find_val e >>- fun src_val ->
- Value.backward_cast ~src_typ ~dst_typ ~src_val ~dst_val:value
- >>- function v -> backward_eval fuel state e v
+ let* src_val = find_val e in
+ let backward = Value.backward_cast context ~src_typ ~dst_typ in
+ let* v = backward ~src_val ~dst_val:value in
+ backward_eval fuel context state e v
end
| _ -> `Value ()
- and recursive_descent fuel state expr =
+ and recursive_descent fuel context state expr =
match expr.enode with
- | Lval lval -> backward_lval fuel state lval
+ | Lval lval -> backward_lval fuel context state lval
| UnOp (_, e, _)
- | CastE (_, e) ->
- backward_eval fuel state e None
+ | CastE (_, e) -> backward_eval fuel context state e None
| BinOp (_binop, e1, e2, _typ) ->
- backward_eval fuel state e1 None >>- fun () ->
- backward_eval fuel state e2 None
+ let* () = backward_eval fuel context state e1 None in
+ backward_eval fuel context state e2 None
| _ -> `Value ()
- and recursive_descent_lval fuel state (host, offset) =
- recursive_descent_host fuel state host >>- fun () ->
- recursive_descent_offset fuel state offset
+ and recursive_descent_lval fuel context state (host, offset) =
+ let* () = recursive_descent_host fuel context state host in
+ recursive_descent_offset fuel context state offset
- and recursive_descent_host fuel state = function
+ and recursive_descent_host fuel context state = function
| Var _ -> `Value ()
- | Mem expr -> backward_eval fuel state expr None >>-: fun _ -> ()
+ | Mem expr -> backward_eval fuel context state expr None
- and recursive_descent_offset fuel state = function
+ and recursive_descent_offset fuel context state = function
| NoOffset -> `Value ()
- | Field (_, remaining) -> recursive_descent_offset fuel state remaining
+ | Field (_, remaining) ->
+ recursive_descent_offset fuel context state remaining
| Index (exp, remaining) ->
- backward_eval fuel state exp None >>- fun __ ->
- recursive_descent_offset fuel state remaining
+ let* _ = backward_eval fuel context state exp None in
+ recursive_descent_offset fuel context state remaining
(* Even if the value of an lvalue has not been reduced, its memory location
could have been, and this can be propagated backward. Otherwise, continue
the recursive descent. *)
- and backward_lval fuel state lval =
+ and backward_lval fuel context state lval =
match find_loc_for_reduction lval with
- | None -> recursive_descent_lval fuel state lval
+ | None -> recursive_descent_lval fuel context state lval
| Some (record, report) ->
if (fst report).reduction = Forward
- then internal_backward_lval fuel state record.loc lval
- else recursive_descent_lval fuel state lval
+ then internal_backward_lval fuel context state record.loc lval
+ else recursive_descent_lval fuel context state lval
(* [backward_loc state lval value] tries to reduce the memory location of the
lvalue [lval] according to its value [value] in the state [state]. *)
@@ -1348,13 +1345,12 @@ module Make
match find_loc_for_reduction lval with
| None -> `Value None
| Some (record, report) ->
- Domain.backward_location state lval record.typ record.loc value
- >>- fun (loc, new_value) ->
- Value.narrow new_value value >>-: fun value ->
+ let backward_location = Domain.backward_location state lval in
+ let* loc, new_value = backward_location record.typ record.loc value in
+ let+ value = Value.narrow new_value value in
let b = not (Loc.equal_loc record.loc loc) in
(* Avoids useless reductions and reductions of volatile expressions. *)
- if b && not (fst report).volatile
- then
+ if b && not (fst report).volatile then
let record = { record with loc } in
let report = { (fst report) with reduction = Backward }, snd report in
cache := Cache.add_loc' !cache lval (record, report);
@@ -1363,43 +1359,46 @@ module Make
then Some (loc, value)
else None
- and internal_backward_lval fuel state location = function
+ and internal_backward_lval fuel context state location = function
| Var host, offset ->
- Loc.backward_variable host location >>- fun loc_offset ->
- backward_offset fuel state host.vtype offset loc_offset
+ let* loc_offset = Loc.backward_variable host location in
+ backward_offset fuel context state host.vtype offset loc_offset
| Mem expr, offset ->
match offset with
| NoOffset ->
- Loc.to_value location >>- fun loc_value ->
- backward_eval fuel state expr (Some loc_value) >>-: fun _ -> ()
+ let* loc_value = Loc.to_value location in
+ backward_eval fuel context state expr (Some loc_value)
| _ ->
let reduce_valid_index = true in
let typ_lval = Cil.typeOf_pointed (Cil.typeOf expr) in
- let context = fast_eval_context state in
- fst (eval_offset context ~reduce_valid_index typ_lval offset)
- >>- fun (loc_offset, _, _) ->
- find_val expr >>- fun value ->
- Loc.backward_pointer value loc_offset location
- >>- fun (pointer_value, loc_offset) ->
- backward_eval fuel state expr (Some pointer_value) >>- fun _ ->
- backward_offset fuel state typ_lval offset loc_offset
-
- and backward_offset fuel state typ offset loc_offset = match offset with
- | NoOffset -> `Value ()
+ let* env = fast_eval_environment state in
+ let eval = eval_offset env ~reduce_valid_index typ_lval offset in
+ let* loc_offset, _, _ = fst eval in
+ let* value = find_val expr in
+ let pointer = Loc.backward_pointer value loc_offset location in
+ let* pointer_value, loc_offset = pointer in
+ let* () = backward_eval fuel context state expr (Some pointer_value) in
+ backward_offset fuel context state typ_lval offset loc_offset
+
+ and backward_offset fuel context state typ offset loc_offset =
+ match offset with
+ | NoOffset -> `Value ()
| Field (field, remaining) ->
- Loc.backward_field typ field loc_offset >>- fun rem ->
- backward_offset fuel state field.ftype remaining rem
+ let* rem = Loc.backward_field typ field loc_offset in
+ backward_offset fuel context state field.ftype remaining rem
| Index (exp, remaining) ->
- find_val exp >>- fun v ->
+ let* v = find_val exp in
let typ_pointed = Cil.typeOf_array_elem typ in
- let context = fast_eval_context state in
- fst (eval_offset context ~reduce_valid_index:true typ_pointed remaining)
- >>- fun (rem, _, _) ->
- Loc.backward_index typ_pointed ~index:v ~remaining:rem loc_offset >>-
- fun (v', rem') ->
+ let* env = fast_eval_environment state in
+ let* rem, _, _ =
+ eval_offset env ~reduce_valid_index:true typ_pointed remaining |> fst
+ in
+ let* v', rem' =
+ Loc.backward_index ~index:v ~remaining:rem typ_pointed loc_offset
+ in
let reduced_v = if Value.is_included v v' then None else Some v' in
- backward_eval fuel state exp reduced_v >>- fun _ ->
- backward_offset fuel state typ_pointed remaining rem'
+ let* () = backward_eval fuel context state exp reduced_v in
+ backward_offset fuel context state typ_pointed remaining rem'
(* ------------------------------------------------------------------------
@@ -1422,72 +1421,65 @@ module Make
to a less precise value than the one stored after the backward evaluation.
This means that the backward propagation has not been precise enough. *)
let rec second_forward_eval state expr =
- let record, report =
- try Cache.find' !cache expr
- with Not_found -> assert false
- in
- if report.reduction <> Backward then `Value ()
- else
- record.value.v >>- fun value ->
- recursive_descent state expr >>- fun () ->
+ let find e = try Cache.find' !cache e with Not_found -> assert false in
+ let record, report = find expr in
+ if report.reduction == Backward then
+ let* value = record.value.v in
+ let* () = recursive_descent state expr in
let new_value =
match expr.enode with
| Lval lval -> second_eval_lval state lval value
| _ ->
- fst (internal_forward_eval (fast_eval_context state) expr)
- >>-: fun (v, _, _) -> v
+ let* env = fast_eval_environment state in
+ let+ v, _, _ = fst (internal_forward_eval env expr) in v
in
- new_value >>- fun evaled ->
+ let* evaled = new_value in
let evaled = Value.reduce evaled in
- Value.narrow value evaled >>-: fun new_value ->
- if not (Value.is_included evaled value)
- then raise Not_Exact_Reduction
- else
+ let+ new_value = Value.narrow value evaled in
+ if Value.is_included evaled value then
let kind = if Value.equal value new_value then Neither else Forward in
reduce_expr_value kind expr new_value
+ else raise Not_Exact_Reduction
+ else `Value ()
and second_eval_lval state lval value =
- if not (may_be_reduced_lval lval)
- then `Value value
- else
- let record, report = match Cache.find_loc' !cache lval with
+ if may_be_reduced_lval lval then
+ let record, report =
+ match Cache.find_loc' !cache lval with
| `Value all -> all
| `Top -> assert false
in
- let evaloc =
- if (fst report).reduction = Backward
- then
- let for_writing = false
- and reduction = true
- and context = fast_eval_context state in
- fst (reduced_lval_to_loc context ~for_writing ~reduction lval)
- >>-: fun (loc, _, _, _) ->
+ let* env = fast_eval_environment state in
+ let* () =
+ if (fst report).reduction = Backward then
+ let for_writing = false and reduction = true in
+ let+ loc, _, _, _ =
+ reduced_lval_to_loc ~for_writing ~reduction env lval |> fst
+ in
(* TODO: Loc.narrow *)
let record = { record with loc } in
- let reduction =
- if Loc.equal_loc record.loc loc then Neither else Forward
- in
+ let in_record loc = Loc.equal_loc record.loc loc in
+ let reduction = if in_record loc then Neither else Forward in
let report = { (fst report) with reduction }, snd report in
cache := Cache.add_loc' !cache lval (record, report);
else `Value ()
in
- evaloc >>- fun () ->
- fst (eval_lval (fast_eval_context state) lval) >>- fun (record, _, _) ->
+ let* record, _, _ = eval_lval env lval |> fst in
record.value.v
+ else `Value value
and recursive_descent state expr =
match expr.enode with
| Lval lval -> recursive_descent_lval state lval
| UnOp (_, e, _)
- | CastE (_, e) ->
- second_forward_eval state e
- | BinOp (_binop, e1, e2, _typ) ->
- second_forward_eval state e1 >>- fun () ->
+ | CastE (_, e) -> second_forward_eval state e
+ | BinOp (_, e1, e2, _) ->
+ let* () = second_forward_eval state e1 in
second_forward_eval state e2
| _ -> `Value ()
and recursive_descent_lval state (host, offset) =
- recursive_descent_host state host >>- fun () ->
+ let* () = recursive_descent_host state host in
recursive_descent_offset state offset
and recursive_descent_host state = function
@@ -1498,7 +1490,7 @@ module Make
| NoOffset -> `Value ()
| Field (_, remaining) -> recursive_descent_offset state remaining
| Index (exp, remaining) ->
- second_forward_eval state exp >>- fun () ->
+ let* () = second_forward_eval state exp in
recursive_descent_offset state remaining
(* ------------------------------------------------------------------------
@@ -1508,40 +1500,42 @@ module Make
module Valuation = Cache
let to_domain_valuation valuation =
- Abstract_domain.{ find = Valuation.find valuation;
- fold = (fun f acc -> Valuation.fold f valuation acc);
- find_loc = Valuation.find_loc valuation; }
+ let find = Valuation.find valuation in
+ let fold f acc = Valuation.fold f valuation acc in
+ let find_loc = Valuation.find_loc valuation in
+ Abstract_domain.{ find ; fold ; find_loc }
let evaluate ?(valuation=Cache.empty) ?(reduction=true) ?subdivnb state expr =
let eval, alarms = subdivided_forward_eval valuation ?subdivnb state expr in
let result =
- if not reduction || Alarmset.is_empty alarms
- then eval
- else
- eval >>- fun (valuation, value) ->
+ if reduction && not (Alarmset.is_empty alarms) then
+ let open Bottom.Operators in
+ let* valuation, value = eval in
cache := valuation;
- backward_eval (backward_fuel ()) state expr None >>-: fun _ ->
+ let fuel = backward_fuel () in
+ let* context = get_context state in
+ let+ () = backward_eval fuel context state expr None in
!cache, value
+ else eval
in
result, alarms
let copy_lvalue ?(valuation=Cache.empty) ?subdivnb state lval =
- let expr = Eva_utils.lval_to_exp lval
- and context = root_context ?subdivnb state in
+ let open Evaluated.Operators in
+ let expr = Eva_utils.lval_to_exp lval in
+ let* env = root_environment ?subdivnb state, Alarmset.none in
try
let record, report = Cache.find' valuation expr in
- if less_fuel_than context.remaining_fuel report.fuel
+ if less_fuel_than env.remaining_fuel report.fuel
then `Value (valuation, record.value), record.val_alarms
else raise Not_found
with Not_found ->
cache := valuation;
- eval_lval context ~indeterminate:true lval
- >>=: fun (record, _, volatile) ->
+ let+ record, _, volatile = eval_lval env ~indeterminate:true lval in
let record = reduce_value record in
(* Cache the computed result with an appropriate report. *)
- let report =
- { fuel = Finite (root_fuel ()); reduction = Neither; volatile }
- in
+ let fuel = Finite (root_fuel ()) in
+ let report = { fuel; reduction = Neither; volatile } in
let valuation = Cache.add' !cache expr (record, report) in
valuation, record.value
@@ -1551,55 +1545,61 @@ module Make
| NoOffset -> `Value valuation, Alarmset.none
| Field (_, offset) -> evaluate_offsets valuation ?subdivnb state offset
| Index (expr, offset) ->
- subdivided_forward_eval valuation ?subdivnb state expr
- >>= fun (valuation, _value) ->
+ let open Evaluated.Operators in
+ let* valuation, _ =
+ subdivided_forward_eval valuation ?subdivnb state expr
+ in
evaluate_offsets valuation ?subdivnb state offset
let evaluate_host valuation ?subdivnb state = function
- | Var _ -> `Value valuation, Alarmset.none
- | Mem expr ->
- subdivided_forward_eval valuation ?subdivnb state expr >>=: fst
+ | Var _ -> `Value valuation, Alarmset.none
+ | Mem e -> subdivided_forward_eval valuation ?subdivnb state e >>=: fst
let lvaluate ?(valuation=Cache.empty) ?subdivnb ~for_writing state lval =
+ let open Evaluated.Operators in
(* If [for_writing] is true, the location of [lval] is reduced by removing
const bases. Use [for_writing:false] if const bases can be written
through a mutable field or an initializing function. *)
let for_writing = for_writing && not (Cil.is_mutable_or_initialized lval) in
let host, offset = lval in
- evaluate_host valuation ?subdivnb state host >>= fun valuation ->
- evaluate_offsets valuation ?subdivnb state offset >>= fun valuation ->
+ let* valuation = evaluate_host valuation ?subdivnb state host in
+ let* valuation = evaluate_offsets valuation ?subdivnb state offset in
cache := valuation;
- let context = root_context ?subdivnb state in
- lval_to_loc context ~for_writing ~reduction:true lval
- >>=. fun (_, typ, _) ->
- backward_lval (backward_fuel ()) state lval >>-: fun _ ->
+ let* env = root_environment ?subdivnb state, Alarmset.none in
+ let& _, typ, _ = lval_to_loc env ~for_writing ~reduction:true lval in
+ let open Bottom.Operators in
+ let+ () = backward_lval (backward_fuel ()) env.context state lval in
match Cache.find_loc !cache lval with
| `Value record -> !cache, record.loc, typ
| `Top -> assert false
let reduce ?valuation:(valuation=Cache.empty) state expr positive =
+ let open Evaluated.Operators in
(* Generate [e == 0] *)
let expr = Eva_utils.normalize_as_cond expr (not positive) in
cache := valuation;
(* Currently, no subdivisions are performed during the forward evaluation
in this function, which is used to evaluate the conditions of if(…)
statements in the analysis. *)
- let context = root_context ~subdivnb:0 state in
- root_forward_eval context expr >>=. fun (_v, volatile) ->
+ let* env = root_environment ~subdivnb:0 state, Alarmset.none in
+ let& _, volatile = root_forward_eval env expr in
+ let open Bottom.Operators in
(* Reduce by [(e == 0) == 0] *)
- backward_eval (backward_fuel ()) state expr (Some Value.zero)
- >>- fun () ->
- try second_forward_eval state expr >>-: fun () -> !cache
+ let fuel = backward_fuel () in
+ let* () = backward_eval fuel env.context state expr (Some Value.zero) in
+ try let+ () = second_forward_eval state expr in !cache
with Not_Exact_Reduction ->
- (* Avoids reduce_by_cond_enumerate on volatile expressions. *)
- if volatile then `Value !cache
- else
- let context = fast_eval_context state in
- Subdivided_Evaluation.reduce_by_enumeration context !cache expr false
+ (* Avoids reduce_by_enumeration on volatile expressions. *)
+ if not volatile then
+ let* env = fast_eval_environment state in
+ Subdivided_Evaluation.reduce_by_enumeration env !cache expr false
+ else `Value !cache
let assume ?valuation:(valuation=Cache.empty) state expr value =
cache := valuation;
- backward_eval (backward_fuel ()) state expr (Some value) >>-: fun _ ->
+ let fuel = backward_fuel () in
+ let* context = get_context state in
+ let+ () = backward_eval fuel context state expr (Some value) in
!cache
@@ -1638,11 +1638,11 @@ module Make
let eval_function_exp ?subdivnb funcexp ?args state =
match funcexp.enode with
| Lval (Var vinfo, NoOffset) ->
- `Value [Globals.Functions.get vinfo, Valuation.empty],
- Alarmset.none
+ `Value [Globals.Functions.get vinfo, Valuation.empty], Alarmset.none
| Lval (Mem v, NoOffset) ->
begin
- evaluate ?subdivnb state v >>= fun (valuation, value) ->
+ let open Evaluated.Operators in
+ let* valuation, value = evaluate ?subdivnb state v in
let kfs, alarm = Value.resolve_functions value in
match kfs with
| `Top -> top_function_pointer funcexp
diff --git a/src/plugins/eva/engine/evaluation.mli b/src/plugins/eva/engine/evaluation.mli
index c7585a1acabb9d60f84da1b27285668ab5c9d870..09b69cae530f5b514249b98b1e9555ef60b8cff9 100644
--- a/src/plugins/eva/engine/evaluation.mli
+++ b/src/plugins/eva/engine/evaluation.mli
@@ -37,11 +37,14 @@ end
(** Generic functor. *)
module Make
- (Value : Value)
+ (Context : Abstract_context.S)
+ (Value : Value with type context = Context.t)
(Loc : Abstract_location.S with type value = Value.t)
- (Domain : Queries with type value = Value.t
+ (Domain : Queries with type context = Context.t
+ and type value = Value.t
and type location = Loc.location)
: Evaluation_sig.S with type state = Domain.state
+ and type context = Context.t
and type value = Value.t
and type origin = Domain.origin
and type loc = Loc.location
diff --git a/src/plugins/eva/engine/evaluation_sig.ml b/src/plugins/eva/engine/evaluation_sig.ml
index 79d7e214e912dce3ee0532960b243f8e383ff72f..7fc600378d24d8109417522ec39c3eb0fc71b4e7 100644
--- a/src/plugins/eva/engine/evaluation_sig.ml
+++ b/src/plugins/eva/engine/evaluation_sig.ml
@@ -30,6 +30,9 @@ module type S = sig
(** State of abstract domain. *)
type state
+ (** Context *)
+ type context
+
(** Numeric values to which the expressions are evaluated. *)
type value
diff --git a/src/plugins/eva/engine/subdivided_evaluation.ml b/src/plugins/eva/engine/subdivided_evaluation.ml
index 2745ee14214a021292ab57156a3cec97cbb237c7..e4a15fdbfa44f8fc1f284c57ba4de2e36b6fb612 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.ml
+++ b/src/plugins/eva/engine/subdivided_evaluation.ml
@@ -359,8 +359,8 @@ end
module type Forward_Evaluation = sig
type value
type valuation
- type context
- val evaluate: subdivided:bool -> context -> valuation ->
+ type environment
+ val evaluate: subdivided:bool -> environment -> valuation ->
exp -> (valuation * value) evaluated
end
@@ -649,7 +649,7 @@ module Make
The function returns the alarms and the valuation resulting from the
subdivided evaluation. In the resulting valuation, the values of [expr],
[subexpr] and of the lvalues in [lvals] have been reduced. *)
- let subdivide_lvals context valuation subdivnb ~expr ~subexpr lvals =
+ let subdivide_lvals env valuation subdivnb ~expr ~subexpr lvals =
let Hypotheses.L variables = Hypotheses.from_list lvals in
(* Split function for the subvalues of [lvals]. *)
let split = make_split valuation variables in
@@ -664,7 +664,7 @@ module Make
(* Updates [variables] with their new [subvalues]. *)
let valuation = update_variables cleared_valuation variables subvalues in
(* Evaluates [expr] with this new valuation. *)
- let eval, alarms = Eva.evaluate ~subdivided:true context valuation expr in
+ let eval, alarms = Eva.evaluate ~subdivided:true env valuation expr in
let result = eval >>-: snd in
(* Optimization if [subexpr] = [expr]. *)
if eq_equal_subexpr
@@ -707,12 +707,12 @@ module Make
eval_result, alarms
(* Builds the information for an lvalue. *)
- let get_info context valuation lval =
+ let get_info environment valuation lval =
let lv_expr = Eva_utils.lval_to_exp lval in
(* Reevaluates the lvalue in the initial state, as its value could have
been reduced in the evaluation of the complete expression, and we cannot
omit the alarms for the removed values. *)
- fst (Eva.evaluate ~subdivided:true context valuation lv_expr)
+ fst (Eva.evaluate ~subdivided:true environment valuation lv_expr)
>>- fun (valuation, _) ->
let lv_record = find_val valuation lv_expr in
lv_record.value.v >>-: fun lv_value ->
@@ -721,8 +721,8 @@ module Make
(* Makes a list of lvalue information from a list of lvalues. Removes lvalues
whose cvalue is singleton or contains addresses, as we cannot subdivide on
such values. *)
- let make_info_list context valuation lvals =
- let get_info = get_info context valuation in
+ let make_info_list environment valuation lvals =
+ let get_info = get_info environment valuation in
let get_info acc lval = Bottom.add_to_list (get_info lval) acc in
let list = List.fold_left get_info [] lvals in
List.filter (fun info -> can_be_subdivided (get_cval info.lv_value)) list
@@ -736,10 +736,10 @@ module Make
| `Value (valuation, result) -> f valuation result alarms
(* Subdivided evaluation of [expr] in state [state]. *)
- let subdivide_evaluation context initial_valuation subdivnb expr =
+ let subdivide_evaluation environment initial_valuation subdivnb expr =
(* Evaluation of [expr] without subdivision. *)
let subdivided = false in
- let default = Eva.evaluate ~subdivided context initial_valuation expr in
+ let default = Eva.evaluate ~subdivided environment initial_valuation expr in
default >>> fun valuation result alarms ->
(* Do not try to subdivide if the result is singleton or contains some
pointers: the better_bound heuristic only works on numerical values. *)
@@ -751,7 +751,7 @@ module Make
let vars = compute_non_linear expr in
(* Compute necessary information about the lvalues to be subdivided.
Also remove lvalues with pointer or singleton values. *)
- let make_info = make_info_list context initial_valuation in
+ let make_info = make_info_list environment initial_valuation in
let vars_info = List.map (fun (e, lvals) -> e, make_info lvals) vars in
let vars_info = List.filter (fun (_, infos) -> infos <> []) vars_info in
let rec subdivide_subexpr vars valuation result alarms =
@@ -775,7 +775,7 @@ module Make
"subdividing on %a"
(Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lvals;
let subdivide =
- subdivide_lvals context valuation subdivnb lvals_info
+ subdivide_lvals environment valuation subdivnb lvals_info
in
(* If there are no other variables to subdivide, stops the
subdivision as soon as they can no longer improve the value
@@ -793,15 +793,15 @@ module Make
let valuation =
Clear.clear_englobing_exprs valuation ~expr ~subexpr
in
- Eva.evaluate ~subdivided:true context valuation expr >>>
+ Eva.evaluate ~subdivided:true environment valuation expr >>>
subdivide_subexpr tail
in
subdivide_subexpr vars_info valuation result alarms
- let evaluate context valuation ~subdivnb expr =
+ let evaluate environment valuation ~subdivnb expr =
if subdivnb = 0 || not activated
- then Eva.evaluate ~subdivided:false context valuation expr
- else subdivide_evaluation context valuation subdivnb expr
+ then Eva.evaluate ~subdivided:false environment valuation expr
+ else subdivide_evaluation environment valuation subdivnb expr
(* ---------------------- Reduction by enumeration ------------------------ *)
@@ -890,13 +890,13 @@ module Make
let get_influential_exprs valuation expr =
get_influential_vars valuation expr []
- let reduce_by_cond_enumerate context valuation cond positive influentials =
+ let reduce_by_cond_enumerate env valuation cond positive influentials =
(* Test whether the condition [expr] may still be true when the
sub-expression [e] has the value [v]. *)
let condition_may_still_be_true valuation expr record value =
let value = { record.value with v = `Value value } in
let valuation = Valuation.add valuation expr { record with value } in
- let eval = fst (Eva.evaluate ~subdivided:true context valuation cond) in
+ let eval = fst (Eva.evaluate ~subdivided:true env valuation cond) in
match eval with
| `Bottom -> false
| `Value (_valuation, value) ->
@@ -940,11 +940,11 @@ module Make
(* If the value module contains no cvalue component, this function is
inoperative. Otherwise, it calls reduce_by_cond_enumerate with the
value accessor for the cvalue component. *)
- let reduce_by_enumeration context valuation expr positive =
+ let reduce_by_enumeration env valuation expr positive =
if activated && Parameters.EnumerateCond.get ()
then
get_influential_exprs valuation expr >>- fun split_on ->
- reduce_by_cond_enumerate context valuation expr positive split_on
+ reduce_by_cond_enumerate env valuation expr positive split_on
else `Value valuation
end
diff --git a/src/plugins/eva/engine/subdivided_evaluation.mli b/src/plugins/eva/engine/subdivided_evaluation.mli
index fbfc6ea6f8e6f5350d1e76c5c9f4788e4809788e..a0fb79f594e37349401e516a37205eb864d49c09 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.mli
+++ b/src/plugins/eva/engine/subdivided_evaluation.mli
@@ -30,8 +30,8 @@ open Eval
module type Forward_Evaluation = sig
type value
type valuation
- type context
- val evaluate: subdivided:bool -> context -> valuation ->
+ type environment
+ val evaluate: subdivided:bool -> environment -> valuation ->
exp -> (valuation * value) evaluated
end
@@ -45,11 +45,11 @@ module Make
: sig
val evaluate:
- Eva.context -> Valuation.t -> subdivnb:int ->
+ Eva.environment -> Valuation.t -> subdivnb:int ->
exp -> (Valuation.t * Value.t) evaluated
val reduce_by_enumeration:
- Eva.context -> Valuation.t -> exp -> bool -> Valuation.t or_bottom
+ Eva.environment -> Valuation.t -> exp -> bool -> Valuation.t or_bottom
end
diff --git a/src/plugins/eva/eval.ml b/src/plugins/eva/eval.ml
index 464adad0ba009b58bb40600f0f2db88495f1ad4c..3aa5c768e8eab5bee45d6f12f9f86e63baeafba0 100644
--- a/src/plugins/eva/eval.ml
+++ b/src/plugins/eva/eval.ml
@@ -56,6 +56,15 @@ let (>>=.) (t, a) f = match t with
| `Bottom -> `Bottom, a
| `Value t -> let t' = f t in t', a
+module Evaluated = struct
+ type 'a t = 'a evaluated
+ module Operators = struct
+ let ( let* ) evaluated f = evaluated >>= f
+ let ( let+ ) evaluated f = evaluated >>=: f
+ let ( let& ) evaluated f = evaluated >>=. f
+ end
+end
+
(* Backward evaluation. *)
type 'a reduced = [ `Bottom | `Unreduced | `Value of 'a ]
diff --git a/src/plugins/eva/eval.mli b/src/plugins/eva/eval.mli
index 5a070232b736d033017abae28b9273c031da8f0a..91acacbbd63d9a3ed265eff60f59bdc8c4eeeab2 100644
--- a/src/plugins/eva/eval.mli
+++ b/src/plugins/eva/eval.mli
@@ -59,6 +59,15 @@ val (>>=.) : 'a evaluated -> ('a -> 'b or_bottom) -> 'b evaluated
val (>>=:) : 'a evaluated -> ('a -> 'b) -> 'b evaluated
+module Evaluated : sig
+ type 'a t = 'a evaluated
+ module Operators : sig
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( let& ) : 'a t -> ('a -> 'b or_bottom) -> 'b t
+ end
+end
+
(** Most backward evaluation function returns `Bottom if the reduction leads to
an invalid state, `Unreduced if no reduction can be performed, or the
reduced value. *)
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 0675ae74772688f2e65bc585ccb50321f6754bbe..7fa874f64bd0a34625c0b16633be632466eedb51 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -349,19 +349,18 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Adds or subtracts the integer value of [expr] to the current increment
[acc.delta], according to [binop] which can be PlusA or MinusA.
Raises NoIncrement if [expr] is not a constant integer expression. *)
- let add_to_delta binop acc expr =
+ let add_to_delta context binop acc expr =
let typ = Cil.typeOf expr in
match Cil.constFoldToInt expr with
| None -> raise NoIncrement
| Some i ->
- let add_to v =
- v >>- fun v -> Val.forward_binop typ binop v (Val.inject_int typ i)
- in
- { value = add_to acc.value; delta = add_to acc.delta; }
+ let inject i = Val.inject_int typ i in
+ let add v = let* v in Val.forward_binop context typ binop v (inject i) in
+ { value = add acc.value; delta = add acc.delta; }
(* Adds to [acc] the increment from the assignement of [lval] to the value
of [expr]. Raises NoIncrement if this is not an increment of [lval]. *)
- let rec delta_assign lval expr acc =
+ let rec delta_assign context lval expr acc =
(* Is the expression [e] equal to the lvalue [lval] (modulo cast)? *)
let rec is_lval e = match e.enode with
| Lval lv -> Cil_datatype.LvalStructEq.equal lval lv
@@ -376,11 +375,12 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
match expr.enode with
| BinOp ((PlusA | MinusA) as binop, e1, e2, _) ->
if is_lval e1
- then add_to_delta binop acc e2
+ then add_to_delta context binop acc e2
else if is_lval e2 && binop = PlusA
- then add_to_delta binop acc e1
+ then add_to_delta context binop acc e1
else raise NoIncrement
- | CastE (typ, e) when Cil.isIntegralType typ -> delta_assign lval e acc
+ | CastE (typ, e) when Cil.isIntegralType typ ->
+ delta_assign context lval e acc
| _ -> raise NoIncrement
(* Computes an over-approximation of the increment of [lval] in the [loop].
@@ -388,8 +388,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
should be a direct access to a variable whose address is not taken,
and which should not be global if the loop contains function calls.
Returns None if no increment can be computed. *)
- let compute_delta lval loop =
- let transfer = transfer_assign lval NoIncrement (delta_assign lval) in
+ let compute_delta ctx lval loop =
+ let transfer = transfer_assign lval NoIncrement (delta_assign ctx lval) in
let join t1 t2 =
{ value = Bottom.join Val.join t1.value t2.value;
delta = Bottom.join Val.join t1.delta t2.delta; }
@@ -517,7 +517,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Is the number of iterations of a loop bounded by [limit]?
[state] is the loop entry state, and [loop_block] the block of the loop. *)
- let is_bounded_loop kf stmt loop state limit =
+ let is_bounded_loop kf stmt loop context state limit =
(* Computes the effect of the loop. Stops if it contains assembly code. *)
compute_loop_effect loop >>: fun loop_effect ->
(* Finds loop exit conditions. *)
@@ -540,9 +540,10 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
evaluate_lvalue state lval >>: fun v_init ->
(* Computes an over-approximation [v_incr] of the value update of [lval]
in one iteration of the loop. *)
- compute_delta lval loop >>: fun v_incr ->
+ compute_delta context lval loop >>: fun v_incr ->
let typ = Cil.typeOfLval lval in
- let binop op v1 v2 = Bottom.non_bottom (Val.forward_binop typ op v1 v2) in
+ let forward_binop op v1 v2 = Val.forward_binop context typ op v1 v2 in
+ let binop op v1 v2 = Bottom.non_bottom (forward_binop op v1 v2) in
(* Computes the possible values of [lval] after n loop iterations. *)
let value =
(* [delta] is the possible increments of [lval] in one iteration. *)
@@ -578,10 +579,12 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Computes an automatic loop unrolling for statement [stmt] in state [state],
with a maximum limit. Returns None for no automatic loop unrolling. *)
let compute ~max_unroll state stmt =
+ let open Option.Operators in
+ let* from_domains = Dom.build_context state |> Bottom.to_option in
try
let kf = Kernel_function.find_englobing_kf stmt in
let loop = Graph.find_loop kf stmt in
- if is_bounded_loop kf stmt loop state max_unroll
+ if is_bounded_loop kf stmt loop { from_domains } state max_unroll
then Some max_unroll
else None
with Not_found -> None
diff --git a/src/plugins/eva/utils/abstract.ml b/src/plugins/eva/utils/abstract.ml
index d9d06c86b9f781d2da2fbdab62c0593f76fa37ab..2db761536bf7bc22383fdd4d95c12220cedaf84c 100644
--- a/src/plugins/eva/utils/abstract.ml
+++ b/src/plugins/eva/utils/abstract.ml
@@ -20,6 +20,28 @@
(* *)
(**************************************************************************)
+module Context = struct
+
+ type 'a context = (module Abstract_context.S with type t = 'a)
+ module C = struct type 'a t = 'a context end
+ include Structure.Shape (Structure.Key_Context) (C)
+
+ module type Internal = sig
+ include Abstract_context.S
+ val structure : t structure
+ end
+
+ module type External = sig
+ include Internal
+ include Structure.External
+ with type t := t
+ and type 'a key := 'a key
+ and type 'a data := 'a data
+ end
+
+end
+
+
module Value = struct
module V = struct
diff --git a/src/plugins/eva/utils/abstract.mli b/src/plugins/eva/utils/abstract.mli
index 75e6f15198fff73dc9cf2bb05322570f8ff9ee8f..6ced511c6f1121f03803f40e03c476e33c541d67 100644
--- a/src/plugins/eva/utils/abstract.mli
+++ b/src/plugins/eva/utils/abstract.mli
@@ -33,6 +33,26 @@
Note that their behavior is undefined if an abstraction contains
several times the same leaf module. *)
+(** Key and structure for abstract contexts.
+ See {!Structure} for more details. *)
+module Context : sig
+ include Structure.Shape
+ with type 'a key = 'a Structure.Key_Context.key
+ and type 'a data = (module Abstract_context.S with type t = 'a)
+
+ module type Internal = sig
+ include Abstract_context.S
+ val structure: t structure
+ end
+
+ module type External = sig
+ include Internal
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ and type 'a data := 'a data
+ end
+end
+
(** Key and structure for abstract values.
See {!Structure} for more details. *)
module Value : sig
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index 551d6460b61c6192f9cf75c8feca0566660bb243..dd3d5c7c6d70b84f617c202e693bbf962b92b797 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
module Abstract_domain = Abstract_domain
+module Abstract_context = Abstract_context
module Abstract_value = Abstract_value
module Abstract_location = Abstract_location
module Abstract = Abstract
@@ -30,6 +31,7 @@ module Alarmset = Alarmset
module Analysis = Analysis
module Assigns = Assigns
module Callstack = Callstack
+module Unit_context = Unit_context
module Cvalue_domain = Cvalue_domain
module Cvalue_results = Cvalue_results
module Domain_builder = Domain_builder
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index b28740b076b493187fb4cb1ae56b630de09a9451..a00af9b2d37525e367ddedfb7549a967ed2b14bc 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -25,6 +25,7 @@
to the internal modules of Eva they need. *)
module Abstract_domain = Abstract_domain
+module Abstract_context = Abstract_context
module Abstract_value = Abstract_value
module Abstract_location = Abstract_location
module Abstract = Abstract
@@ -34,6 +35,7 @@ module Alarmset = Alarmset
module Analysis = Analysis
module Assigns = Assigns
module Callstack = Callstack
+module Unit_context = Unit_context
module Cvalue_domain = Cvalue_domain
module Cvalue_results = Cvalue_results
module Domain_builder = Domain_builder
diff --git a/src/plugins/eva/utils/structure.ml b/src/plugins/eva/utils/structure.ml
index 93fa44dd8379a6426895f4bcc1335783e2c7d070..f04b8bebb148ead1868c1aa21c11a94c0ca0ebe4 100644
--- a/src/plugins/eva/utils/structure.ml
+++ b/src/plugins/eva/utils/structure.ml
@@ -87,6 +87,7 @@ module Make () = struct
let print fmt x = Format.pp_print_string fmt x.name
end
+module Key_Context = Make ()
module Key_Value = Make ()
module Key_Location = Make ()
module Key_Domain = Make ()
diff --git a/src/plugins/eva/utils/structure.mli b/src/plugins/eva/utils/structure.mli
index f10a3edc9fcb659e0e0ad3cbd9fd7be1ffd99dc7..ad2a55a7c37dabf150755b94b04d6a1731aafd92 100644
--- a/src/plugins/eva/utils/structure.mli
+++ b/src/plugins/eva/utils/structure.mli
@@ -44,6 +44,9 @@ end
module Make () : Key
+(** Keys module for the abstract contexts of Eva. *)
+module Key_Context : Key
+
(** Keys module for the abstract values of Eva. *)
module Key_Value : Key
diff --git a/src/plugins/eva/utils/unit_tests.ml b/src/plugins/eva/utils/unit_tests.ml
index 1e2e0647403006e650a0d4ecddf146825cb738e8..2b3ab6fc5273e0dc3223c8cee2fba39485846e1b 100644
--- a/src/plugins/eva/utils/unit_tests.ml
+++ b/src/plugins/eva/utils/unit_tests.ml
@@ -94,8 +94,9 @@ module Sign = struct
let test_unop unop typ values =
let test (cval, sign) =
- let cval_res = Cval.forward_unop typ unop cval in
- let sign_res = Sign.forward_unop typ unop sign in
+ let context = Abstract_value.{ from_domains = Unit_context.top } in
+ let cval_res = Cval.forward_unop context typ unop cval in
+ let sign_res = Sign.forward_unop context typ unop sign in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a = %a while %a %a = %a"
Printer.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
@@ -105,8 +106,9 @@ module Sign = struct
let test_binop binop typ values =
let test (cval1, sign1) (cval2, sign2) =
- let cval_res = Cval.forward_binop typ binop cval1 cval2 in
- let sign_res = Sign.forward_binop typ binop sign1 sign2 in
+ let context = Abstract_value.{ from_domains = Unit_context.top } in
+ let cval_res = Cval.forward_binop context typ binop cval1 cval2 in
+ let sign_res = Sign.forward_binop context typ binop sign1 sign2 in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a %a = %a while %a %a %a = %a"
Cval.pretty cval1 Printer.pp_binop binop Cval.pretty cval2
diff --git a/src/plugins/eva/values/abstract_value.ml b/src/plugins/eva/values/abstract_value.ml
index 4070f3d9efe1a65d6949c30dd78081807c5281bf..2f82d4852466d2fa7bb47e4a50974f7a5fc5bd59 100644
--- a/src/plugins/eva/values/abstract_value.ml
+++ b/src/plugins/eva/values/abstract_value.ml
@@ -46,10 +46,23 @@ type bound = Int of Integer.t | Float of float * fkind
type pointer_comparison = Equality | Relation | Subtraction
+(** Enriched context.
+ This record could easily be extended to contain more information about the
+ context in which an evaluation takes place, if the need arises. *)
+type 'a enriched = { from_domains : 'a }
+
(** Signature of abstract numerical values. *)
module type S = sig
include Datatype.S
+ (** A numerical value abstraction can optionally require some context from
+ abstract domains. Most transfer functions take the context as argument;
+ it is provided by the abstract state in which operations are performed.
+ See {!Abstract_context} for more details about contexts.
+ For values that don't need context, this type can be defined as unit
+ and the context argument can be safely ignored. *)
+ type context
+
val pretty_typ: typ option -> t Pretty_utils.formatter
(** Pretty the abstract value assuming it has the type given as argument. *)
@@ -120,25 +133,26 @@ module type S = sig
(** Embeds C constants into value abstractions: returns an abstract value
for the given constant. The constant cannot be an enumeration constant. *)
- val constant : exp -> constant -> t
+ val constant : context enriched -> exp -> constant -> t
(** [forward_unop typ unop v] evaluates the value [unop v], resulting from the
application of the unary operator [unop] to the value [v]. [typ] is the
type of [v]. *)
- val forward_unop : typ -> unop -> t -> t or_bottom
+ val forward_unop : context enriched -> typ -> unop -> t -> t or_bottom
(** [forward_binop typ binop v1 v2] evaluates the value [v1 binop v2],
resulting from the application of the binary operator [binop] to the
values [v1] and [v2]. [typ] is the type of [v1]. *)
- val forward_binop : typ -> binop -> t -> t -> t or_bottom
+ val forward_binop : context enriched -> typ -> binop -> t -> t -> t or_bottom
(** [rewrap_integer irange t] wraps around the abstract value [t] to fit the
integer range [irange], assuming 2's complement. Also used on absolute
addresses for pointer values, seen as unsigned integers. *)
- val rewrap_integer: Eval_typ.integer_range -> t -> t
+ val rewrap_integer: context enriched -> Eval_typ.integer_range -> t -> t
(** Abstract evaluation of casts operators from [src_type] to [dst_type]. *)
val forward_cast :
+ context enriched ->
src_type: Eval_typ.scalar_typ -> dst_type: Eval_typ.scalar_typ ->
t -> t or_bottom
@@ -164,19 +178,23 @@ module type S = sig
(** Backward evaluation of the binary operation [left binop right = result];
tries to reduce the argument [left] and [right] according to [result].
[input_type] is the type of [left], [resulting_type] the type of [result]. *)
- val backward_binop : input_type:typ -> resulting_type:typ ->
- binop -> left:t -> right:t -> result:t -> (t option * t option) or_bottom
+ val backward_binop :
+ context enriched -> input_type:typ -> resulting_type:typ ->
+ binop -> left:t -> right:t -> result:t ->
+ (t option * t option) or_bottom
(** Backward evaluation of the unary operation [unop arg = res];
tries to reduce the argument [arg] according to [res].
[typ_arg] is the type of [arg]. *)
val backward_unop :
- typ_arg:typ -> unop -> arg:t -> res:t -> t option or_bottom
+ context enriched -> typ_arg:typ -> unop ->
+ arg:t -> res:t -> t option or_bottom
(** Backward evaluation of the cast of the value [src_val] of type [src_typ]
into the value [dst_val] of type [dst_typ]. Tries to reduce [scr_val]
according to [dst_val]. *)
val backward_cast:
+ context enriched ->
src_typ: typ ->
dst_typ: typ ->
src_val: t ->
@@ -205,6 +223,9 @@ module type Leaf = sig
(** The key identifies the module and the type [t] of abstract values. *)
val key: t key
+
+ (** The abstract context on which this value depends. *)
+ val context : context Abstract_context.dependencies
end
(** Eva abstractions are divided between values, locations and domains.
diff --git a/src/plugins/eva/values/main_values.ml b/src/plugins/eva/values/main_values.ml
index bfdb787b8aa0416d9fb95b67cc0ba0fef6d2a3f6..d2602ce3480a3dc14e00bbea9e43d7477c5ea7cc 100644
--- a/src/plugins/eva/values/main_values.ml
+++ b/src/plugins/eva/values/main_values.ml
@@ -25,6 +25,9 @@ open Cil_types
module CVal = struct
include Cvalue.V
+ type context = unit
+ let context = Abstract_context.Leaf (module Unit_context)
+
let zero = Cvalue.V.singleton_zero
let one = Cvalue.V.singleton_one
@@ -47,7 +50,7 @@ module CVal = struct
let assume_pointer = Cvalue_forward.assume_pointer
let assume_comparable = Cvalue_forward.assume_comparable
- let constant exp = function
+ let constant _context 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
@@ -55,12 +58,12 @@ module CVal = struct
Cvalue_forward.eval_float_constant f fkind fstring
| CEnum _ -> assert false
- let forward_unop typ unop value =
+ let forward_unop _context 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 forward_binop _context typ binop v1 v2 =
let value =
match typ with
| TFloat (fkind, _) ->
@@ -72,16 +75,16 @@ module CVal = struct
then `Bottom
else `Value value
- let rewrap_integer = Cvalue_forward.rewrap_integer
+ let rewrap_integer _context = Cvalue_forward.rewrap_integer
- let forward_cast ~src_type ~dst_type v =
+ let forward_cast _context ~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 backward_binop _ctx ~input_type ~resulting_type op ~left ~right ~result =
let reduction =
Cvalue_backward.backward_binop
- ~typ_res:resulting_type ~res_value:result ~typ_e1:input_type left binop right
+ ~typ_res:resulting_type ~res_value:result ~typ_e1:input_type left op right
in
match reduction with
| None -> `Value (None, None)
@@ -90,7 +93,7 @@ module CVal = struct
then `Bottom
else `Value (Some v1, Some v2)
- let backward_unop ~typ_arg op ~arg ~res =
+ let backward_unop _context ~typ_arg op ~arg ~res =
let reduction = Cvalue_backward.backward_unop ~typ_arg op ~arg ~res in
match reduction with
| None -> `Value None
@@ -99,7 +102,7 @@ module CVal = struct
then `Bottom
else `Value r
- let backward_cast ~src_typ ~dst_typ ~src_val ~dst_val =
+ let backward_cast _context ~src_typ ~dst_typ ~src_val ~dst_val =
let reduction =
Cvalue_backward.backward_cast ~src_typ ~dst_typ ~src_val ~dst_val
in
@@ -142,6 +145,9 @@ let cval = Abstract_value.Leaf (module CVal)
module Interval = struct
include Datatype.Option (Ival)
+ type context = unit
+ let context = Abstract_context.Leaf (module Unit_context)
+
let pretty_typ _ = pretty
let top = None
@@ -172,15 +178,15 @@ module Interval = struct
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 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 =
+ let rewrap_integer _ range value =
match value with
| None -> value
| Some value ->
@@ -188,10 +194,10 @@ module Interval = struct
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:_ =
+ 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:_ =
+ let backward_cast _ ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
`Value None
let key = Structure.Key_Value.create_key "interval"
diff --git a/src/plugins/eva/values/main_values.mli b/src/plugins/eva/values/main_values.mli
index 942c9dcbacbeb507fadc254a1f9976471ab88286..daec5ef3c6c16add4c4e4bdef255f04fb8f6c136 100644
--- a/src/plugins/eva/values/main_values.mli
+++ b/src/plugins/eva/values/main_values.mli
@@ -23,16 +23,19 @@
(** Main numeric values of Eva that can be used by abstract domains. *)
(** Main abstract values built over Cvalue.V, used by most domains. *)
-module CVal: Abstract_value.Leaf with type t = Cvalue.V.t
+module CVal: Abstract_value.Leaf
+ with type t = Cvalue.V.t and type context = unit
val cval: CVal.t Abstract_value.dependencies
(** Dummy intervals: no forward nor backward propagations,
only used as a reduced product with CVal above. [None] is top. *)
-module Interval: Abstract_value.Leaf with type t = Ival.t option
+module Interval: Abstract_value.Leaf
+ with type t = Ival.t option and type context = unit
val ival: Interval.t Abstract_value.dependencies
(** Simple sign values, used by the sign domain. *)
-module Sign: Abstract_value.Leaf with type t = Sign_value.t
+module Sign: Abstract_value.Leaf
+ with type t = Sign_value.t and type context = unit
val sign: Sign.t Abstract_value.dependencies
(*
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index 38f2cef9b17fc67ef9d4ff431d0166150ce997bc..0ce2bed1fc5bade5c7b8a5b059df7989d9ae1e6b 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -369,9 +369,14 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
end)
-module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
+module Offsm
+ : Abstract_value.Leaf with type t = offsm_or_top and type context = unit
+= struct
include Datatype_Offsm_or_top
+ type context = unit
+ let context = Abstract_context.Leaf (module Unit_context)
+
let pretty_typ typ fmt = function
| Top as o -> pretty fmt o
| O o ->
@@ -412,7 +417,7 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
- let constant e _c =
+ let constant _context e _c =
if store_redundant then
match Cil.constFoldToInt e with
| Some i -> inject_int (Cil.typeOf e) i
@@ -426,14 +431,14 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
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 forward_unop _context _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 forward_binop _context _typ op o1 o2 =
let o' =
match o1, o2, op with
| O _o1, O _o2, (Shiftlt | Shiftrt) ->
@@ -447,17 +452,18 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
in
`Value o'
- let backward_binop ~input_type:_ ~resulting_type:_ _op ~left:_ ~right:_ ~result:_ =
+ let backward_binop _context ~input_type:_ ~resulting_type:_
+ _op ~left:_ ~right:_ ~result:_ =
`Value (None, None)
- let backward_unop ~typ_arg:_ _unop ~arg:_ ~res:_ = `Value None
+ let backward_unop _context ~typ_arg:_ _unop ~arg:_ ~res:_ = `Value None
- let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
+ let backward_cast _context ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
`Value None
- let rewrap_integer _range o = o
+ let rewrap_integer _context _range o = o
- let forward_cast ~src_type ~dst_type o =
+ let forward_cast _context ~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) ->
@@ -515,23 +521,23 @@ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
let* v = strengthen_v typ (get_cvalue t) o in
`Value (set_cvalue v t)
- let forward_unop typ op t =
+ let forward_unop context typ op t =
match op with
| BNot ->
let t = strengthen_offsm typ t in
- let* t = forward_unop typ op t in
+ let* t = forward_unop context typ op t in
strengthen_v typ t
- | _ -> forward_unop typ op t
+ | _ -> forward_unop context typ op t
- let forward_binop typ op l r =
+ let forward_binop context typ op l r =
match op with
| BAnd | BOr | BXor ->
let l = strengthen_offsm typ l
and r = strengthen_offsm typ r in
- let* t = forward_binop typ op l r in
+ let* t = forward_binop context typ op l r in
strengthen_v typ t
| Shiftlt | Shiftrt ->
- let* p = forward_binop typ op l r in
+ let* p = forward_binop context typ op l r in
begin
try
let i = get_cvalue r |> V.project_ival |> Ival.project_int in
@@ -542,7 +548,7 @@ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
`Value (set_offsm (O offsm) p)
with V.Not_based_on_null | Ival.Not_Singleton_Int -> `Value p
end
- | _ -> forward_binop typ op l r
+ | _ -> forward_binop context typ op l r
end in
(module struct
include Abstraction
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index 8cdc4014a403cb51914b91f2da7fa7b3becd5afb..89371844af7776c2bf9b786112fe302605c6d5a7 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -68,6 +68,9 @@ include Datatype.Make(struct
let pretty_debug = pretty
let pretty_typ _ = pretty
+type context = unit
+let context = Abstract_context.Leaf (module Unit_context)
+
(* Inclusion: test inclusion of each field. *)
let is_included v1 v2 =
let bincl b1 b2 = (not b1) || b2 in
@@ -99,7 +102,7 @@ let inject_int _ i =
else if Integer.gt i Integer.zero then pos
else zero
-let constant _ = function
+let constant _context _expr = function
| CInt64 (i, _, _) -> inject_int () i
| _ -> top
@@ -144,7 +147,7 @@ let bitwise_not typ v =
let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
-let forward_unop typ op v =
+let forward_unop _context typ op v =
match op with
| Neg -> `Value (neg_unop v)
| BNot -> `Value (bitwise_not typ v)
@@ -223,7 +226,7 @@ let logical_or v1 v2 =
let zero = v1.zero && v2.zero in
{ pos; neg; zero }
-let forward_binop _ op v1 v2 =
+let forward_binop _context _typ op v1 v2 =
match op with
| PlusA -> `Value (plus v1 v2)
| MinusA -> `Value (plus v1 (neg_unop v2))
@@ -236,13 +239,13 @@ let forward_binop _ op v1 v2 =
| LOr -> `Value (logical_or v1 v2)
| _ -> `Value top
-let rewrap_integer range v =
+let rewrap_integer _context 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 forward_cast _context ~src_type ~dst_type v =
let open Eval_typ in
match src_type, dst_type with
| TSInt range_src, TSInt range_dst ->
@@ -312,7 +315,7 @@ let backward_comp_right op ~left ~right =
(* 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 =
+let backward_binop _ctx ~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
@@ -334,9 +337,12 @@ let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
| _ -> `Value (None, None)
(* Not implemented precisely *)
-let backward_unop ~typ_arg:_ _op ~arg:_ ~res:_ = `Value None
+let backward_unop _context ~typ_arg:_ _op ~arg:_ ~res:_ =
+ `Value None
+
(* Not implemented precisely *)
-let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
+let backward_cast _context ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ =
+ `Value None
(* Eva boilerplate, used to retrieve the domain. *)
let key = Structure.Key_Value.create_key "sign_values"
diff --git a/src/plugins/eva/values/sign_value.mli b/src/plugins/eva/values/sign_value.mli
index 9bf0bd1cc32f0877a2a8ac8fe5e46e23945e5276..7fadfe569703267e5dede1c083937d92099ea031 100644
--- a/src/plugins/eva/values/sign_value.mli
+++ b/src/plugins/eva/values/sign_value.mli
@@ -28,5 +28,5 @@ type signs = {
neg: bool; (** true: maybe negative, false: never negative *)
}
-include Abstract_value.Leaf with type t = signs
+include Abstract_value.Leaf with type t = signs and type context = unit
val pretty_debug: t Pretty_utils.formatter
diff --git a/src/plugins/eva/values/value_lift.ml b/src/plugins/eva/values/value_lift.ml
new file mode 100644
index 0000000000000000000000000000000000000000..08d29c185bad5f4445d713dd5b25b8e344ebc4b8
--- /dev/null
+++ b/src/plugins/eva/values/value_lift.ml
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module type Conversion = sig
+ type extended
+ type internal
+ val restrict : extended -> internal
+end
+
+module Make
+ (Val: Abstract_value.Leaf)
+ (Convert : Conversion with type internal := Val.context)
+= struct
+
+ (* Import most of [Val] *)
+ include (Val: Abstract_value.S
+ with type context := Val.context (* we are converting this type *)
+ and type t = Val.t)
+ type context = Convert.extended
+
+ let structure = Abstract.Value.Leaf (Val.key, (module Val))
+
+ let restrict context =
+ let open Abstract_value in
+ { from_domains = Convert.restrict context.from_domains }
+
+ (* Now lift the functions that contain {!context} in their type. *)
+
+ let constant context exp constant =
+ Val.constant (restrict context) exp constant
+
+ let forward_unop context typ unop value =
+ Val.forward_unop (restrict context) typ unop value
+
+ let forward_binop context typ binop left right =
+ Val.forward_binop (restrict context) typ binop left right
+
+ let rewrap_integer context range value =
+ Val.rewrap_integer (restrict context) range value
+
+ let forward_cast context ~src_type ~dst_type value =
+ Val.forward_cast (restrict context) ~src_type ~dst_type value
+
+ let backward_binop context ~input_type ~resulting_type binop ~left ~right ~result =
+ Val.backward_binop (restrict context) ~input_type ~resulting_type binop ~left ~right ~result
+
+ let backward_unop context ~typ_arg unop ~arg ~res =
+ Val.backward_unop (restrict context) ~typ_arg unop ~arg ~res
+
+ let backward_cast context ~src_typ ~dst_typ ~src_val ~dst_val =
+ Val.backward_cast (restrict context) ~src_typ ~dst_typ ~src_val ~dst_val
+
+end
diff --git a/src/plugins/eva/values/value_lift.mli b/src/plugins/eva/values/value_lift.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a706eb89ea344f6d0028a3d5bc04d2add39c8271
--- /dev/null
+++ b/src/plugins/eva/values/value_lift.mli
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module type Conversion = sig
+ type extended
+ type internal
+ val restrict : extended -> internal
+end
+
+module Make
+ (Val: Abstract_value.Leaf)
+ (Convert : Conversion with type internal := Val.context)
+ : Abstract.Value.Internal with type t = Val.t
+ and type context = Convert.extended
diff --git a/src/plugins/eva/values/value_product.ml b/src/plugins/eva/values/value_product.ml
index 1ad09d002d82a6ab8546f26074554f6d38e7e0af..0cfbe6e78b6af8861d9a89b6c430ef53ec9022ed 100644
--- a/src/plugins/eva/values/value_product.ml
+++ b/src/plugins/eva/values/value_product.ml
@@ -45,82 +45,90 @@ let narrow_truth_pair x y =
narrow_any_truth combine x y
module Make
- (Left: Abstract_value.S)
- (Right: Abstract_value.S)
+ (Context : Abstract_context.S)
+ (Left : Abstract.Value.Internal with type context = Context.t)
+ (Right : Abstract.Value.Internal with type context = Context.t)
= struct
include Datatype.Pair (Left) (Right)
+ type context = Context.t
+ let structure = Abstract.Value.Node (Left.structure, Right.structure)
let pretty_typ typ =
Pretty_utils.pp_pair ~pre:"@[" ~sep:",@ " ~suf:"@]"
(Left.pretty_typ typ) (Right.pretty_typ typ)
let top = Left.top, Right.top
+
let is_included (l1, r1) (l2, r2) =
Left.is_included l1 l2 && Right.is_included r1 r2
+
let join (l1, r1) (l2, r2) =
Left.join l1 l2, Right.join r1 r2
+
let narrow (l1, r1) (l2, r2) =
- Left.narrow l1 l2 >>- fun left ->
- Right.narrow r1 r2 >>-: fun right ->
+ let+ left = Left.narrow l1 l2
+ and+ right = Right.narrow r1 r2 in
left, right
let zero = Left.zero, Right.zero
- let one = Left.one, Right.one
+ let one = Left.one , Right.one
let top_int = Left.top_int, Right.top_int
let inject_int typ i = Left.inject_int typ i, Right.inject_int typ i
let assume_non_zero (left, right) =
- let left_truth = Left.assume_non_zero left
+ let left_truth = Left.assume_non_zero left
and right_truth = Right.assume_non_zero right in
narrow_truth (left, left_truth) (right, right_truth)
let assume_bounded kind bound (left, right) =
- let left_truth = Left.assume_bounded kind bound left
+ let left_truth = Left.assume_bounded kind bound left
and right_truth = Right.assume_bounded kind bound right in
narrow_truth (left, left_truth) (right, right_truth)
let assume_not_nan ~assume_finite fkind (left, right) =
- let left_truth = Left.assume_not_nan ~assume_finite fkind left
+ let left_truth = Left.assume_not_nan ~assume_finite fkind left
and right_truth = Right.assume_not_nan ~assume_finite fkind right in
narrow_truth (left, left_truth) (right, right_truth)
let assume_pointer (left, right) =
- let left_truth = Left.assume_pointer left
+ let left_truth = Left.assume_pointer left
and right_truth = Right.assume_pointer right in
narrow_truth (left, left_truth) (right, right_truth)
let assume_comparable op (l1, r1) (l2, r2) =
- let left_truth = Left.assume_comparable op l1 l2
+ let left_truth = Left.assume_comparable op l1 l2
and right_truth = Right.assume_comparable op r1 r2 in
narrow_truth_pair ((l1, l2), left_truth) ((r1, r2), right_truth)
- let constant expr constant =
- let left = Left.constant expr constant
- and right = Right.constant expr constant in
+ let constant context expr constant =
+ let left = Left.constant context expr constant
+ and right = Right.constant context expr constant in
left, right
- let forward_unop typ unop (left, right) =
- Left.forward_unop typ unop left >>- fun left ->
- Right.forward_unop typ unop right >>-: fun right ->
+ let forward_unop context typ unop (left, right) =
+ let+ left = Left.forward_unop context typ unop left
+ and+ right = Right.forward_unop context typ unop right in
left, right
- let forward_binop typ binop (l1, r1) (l2, r2) =
- Left.forward_binop typ binop l1 l2 >>- fun left ->
- Right.forward_binop typ binop r1 r2 >>-: fun right ->
+ let forward_binop context typ binop (l1, r1) (l2, r2) =
+ let+ left = Left.forward_binop context typ binop l1 l2
+ and+ right = Right.forward_binop context typ binop r1 r2 in
left, right
- let rewrap_integer range (left, right) =
- Left.rewrap_integer range left, Right.rewrap_integer range right
+ let rewrap_integer context range (left, right) =
+ let left = Left.rewrap_integer context range left
+ and right = Right.rewrap_integer context range right in
+ left, right
- let forward_cast ~src_type ~dst_type (left, right) =
- Left.forward_cast ~src_type ~dst_type left >>- fun left ->
- Right.forward_cast ~src_type ~dst_type right >>-: fun right ->
+ let forward_cast context ~src_type ~dst_type (left, right) =
+ let+ left = Left.forward_cast context ~src_type ~dst_type left
+ and+ right = Right.forward_cast context ~src_type ~dst_type right in
left, right
let resolve_functions (left, right) =
- let list1, b1 = Left.resolve_functions left
- and list2, b2 = Right.resolve_functions right in
+ let list1, b1 = Left.resolve_functions left in
+ let list2, b2 = Right.resolve_functions right in
let list = match list1, list2 with
| `Top, _ -> list2
| _, `Top -> list1
@@ -129,8 +137,7 @@ module Make
list, b1 && b2
let replace_base substitution (left, right) =
- Left.replace_base substitution left,
- Right.replace_base substitution right
+ Left.replace_base substitution left, Right.replace_base substitution right
let reduce (orig_left, orig_right) left right = match left, right with
| None, None -> None
@@ -138,25 +145,25 @@ module Make
| None, Some right -> Some (orig_left, right)
| Some left, Some right -> Some (left, right)
- let backward_unop ~typ_arg unop ~arg:(arg_l, arg_r as arg) ~res:(res_l, res_r) =
- Left.backward_unop ~typ_arg unop ~arg:arg_l ~res:res_l >>- fun left ->
- Right.backward_unop ~typ_arg unop ~arg:arg_r ~res:res_r >>-: fun right ->
+ let backward_unop context ~typ_arg unop ~arg ~res =
+ let on_left = Left.backward_unop context ~typ_arg unop in
+ let on_right = Right.backward_unop context ~typ_arg unop in
+ let+ left = on_left ~arg:(fst arg) ~res:(fst res)
+ and+ right = on_right ~arg:(snd arg) ~res:(snd res) in
reduce arg left right
- let backward_binop ~input_type ~resulting_type binop ~left ~right ~result =
- let l1, r1 = left and l2, r2 = right and l3, r3 = result in
- Left.backward_binop ~input_type ~resulting_type
- binop ~left:l1 ~right:l2 ~result:l3
- >>- fun (l1, l2) ->
- Right.backward_binop ~input_type ~resulting_type
- binop ~left:r1 ~right:r2 ~result:r3
- >>-: fun (r1, r2) ->
+ let backward_binop ctx ~input_type ~resulting_type binop ~left ~right ~result:res =
+ let on_left = Left.backward_binop ctx ~input_type ~resulting_type binop in
+ let on_right = Right.backward_binop ctx ~input_type ~resulting_type binop in
+ let+ l1, l2 = on_left ~left:(fst left) ~right:(fst right) ~result:(fst res)
+ and+ r1, r2 = on_right ~left:(snd left) ~right:(snd right) ~result:(snd res) in
reduce left l1 r1, reduce right l2 r2
- let backward_cast ~src_typ ~dst_typ ~src_val ~dst_val =
- let l1, r1 = src_val and l2, r2 = dst_val in
- Left.backward_cast ~src_typ ~dst_typ ~src_val:l1 ~dst_val:l2 >>- fun left ->
- Right.backward_cast ~src_typ ~dst_typ ~src_val:r1 ~dst_val:r2 >>-: fun right ->
+ let backward_cast context ~src_typ ~dst_typ ~src_val ~dst_val =
+ let on_left = Left.backward_cast context ~src_typ ~dst_typ in
+ let on_right = Right.backward_cast context ~src_typ ~dst_typ in
+ let+ left = on_left ~src_val:(fst src_val) ~dst_val:(fst dst_val)
+ and+ right = on_right ~src_val:(snd src_val) ~dst_val:(snd dst_val) in
reduce src_val left right
end
diff --git a/src/plugins/eva/values/value_product.mli b/src/plugins/eva/values/value_product.mli
index 4139bed2c33e2d05151b888c2f2639983d798bc1..dd4e6e528750d561e19b5651afe1501922acfd0e 100644
--- a/src/plugins/eva/values/value_product.mli
+++ b/src/plugins/eva/values/value_product.mli
@@ -35,9 +35,12 @@ val narrow_truth_pair:
(('a * 'b) * ('a * 'b)) truth
module Make
- (Left: Abstract_value.S)
- (Right: Abstract_value.S)
- : Abstract_value.S with type t = Left.t * Right.t
+ (Context : Abstract_context.S)
+ (Left : Abstract.Value.Internal with type context = Context.t)
+ (Right : Abstract.Value.Internal with type context = Context.t)
+ : Abstract.Value.Internal
+ with type t = Left.t * Right.t
+ and type context = Context.t
(*