From f0d090c637feea070cc8966549898955d6dc02bc Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 5 Apr 2022 16:51:26 +0200
Subject: [PATCH] [Eva] Lattice_bounds: open variants for Operators
---
.../abstract_interp/lattice_bounds.ml | 17 -----
.../abstract_interp/lattice_bounds.mli | 75 ++++++++++++-------
src/plugins/value/utils/results.ml | 19 +++--
3 files changed, 58 insertions(+), 53 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
index 349f7d54e3a..3b7fb552f53 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.ml
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -24,17 +24,6 @@ type 'a or_bottom = [ `Value of 'a | `Bottom ]
type 'a or_top = [ `Value of 'a | `Top ]
type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
-module type Operators =
-sig
- type 'a t
- val (>>-) : 'a t -> ('a -> 'b t) -> 'b t
- val (>>-:) : 'a t -> ('a -> 'b) -> 'b t
- val (let+) : 'a t -> ('a -> 'b) -> 'b t
- val (and+) : 'a t -> 'b t -> ('a * 'b) t
- val (let*) : 'a t -> ('a -> 'b t) -> 'b t
- val (and*) : 'a t -> 'b t -> ('a * 'b) t
-end
-
(** Common functions *)
module Common =
@@ -181,8 +170,6 @@ module Bottom = struct
module Operators =
struct
- type 'a t = 'a or_bottom
-
let (>>-) t f = match t with
| `Bottom -> `Bottom
| `Value t -> f t
@@ -278,8 +265,6 @@ struct
(** Operators *)
module Operators = struct
- type 'a t = 'a or_top
-
let (>>-) t f = match t with
| `Top -> `Top
| `Value t -> f t
@@ -325,8 +310,6 @@ struct
(** Operators *)
module Operators = struct
- type 'a t = 'a or_top_bottom
-
let (>>-) t f = match t with
| `Top -> `Top
| `Bottom -> `Bottom
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.mli b/src/kernel_services/abstract_interp/lattice_bounds.mli
index 806c5f73346..1d4ff6f9819 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.mli
+++ b/src/kernel_services/abstract_interp/lattice_bounds.mli
@@ -27,31 +27,26 @@ type 'a or_bottom = [ `Value of 'a | `Bottom ]
type 'a or_top = [ `Value of 'a | `Top ]
type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
-module type Operators =
-sig
- type 'a t
-
- (** This monad propagates `Bottom and or `Top if needed. *)
- val (>>-) : 'a t -> ('a -> 'b t) -> 'b t
-
- (** Use this monad if the following function returns a simple value. *)
- val (>>-:) : 'a t -> ('a -> 'b) -> 'b t
-
- (* Binding operators, applicative syntax *)
- val (let+) : 'a t -> ('a -> 'b) -> 'b t
- val (and+) : 'a t -> 'b t -> ('a * 'b) t
-
- (* Binding operators, monad syntax *)
- val (let*) : 'a t -> ('a -> 'b t) -> 'b t
- val (and*) : 'a t -> 'b t -> ('a * 'b) t
-end
-
module Bottom : sig
type 'a t = 'a or_bottom
(** Operators *)
- module Operators : Operators with type 'a t = 'a or_bottom
+ module Operators : sig
+ (** This monad propagates `Bottom and or `Top if needed. *)
+ val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+
+ (** Use this monad if the following function returns a simple value. *)
+ val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+
+ (* Binding operators, applicative syntax *)
+ val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+ val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+
+ (* Binding operators, monad syntax *)
+ val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+ val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+ end
(** Datatype constructor *)
module Make_Datatype
@@ -113,7 +108,21 @@ module Top : sig
type 'a t = 'a or_top
(** Operators *)
- module Operators : Operators with type 'a t = 'a or_top
+ module Operators : sig
+ (** This monad propagates `Bottom and or `Top if needed. *)
+ val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+
+ (** Use this monad if the following function returns a simple value. *)
+ val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+
+ (* Binding operators, applicative syntax *)
+ val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+ val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+
+ (* Binding operators, monad syntax *)
+ val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+ val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+ end
(** Access *)
val is_top: 'a t -> bool
@@ -147,6 +156,25 @@ end
module TopBottom: sig
type 'a t = 'a or_top_bottom
+ (** Operators *)
+ (* In presence of simultaneous `Bottom and `Top in and+ / and*, everything
+ narrows down to `Bottom *)
+ module Operators : sig
+ (** This monad propagates `Bottom and or `Top if needed. *)
+ val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+
+ (** Use this monad if the following function returns a simple value. *)
+ val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+
+ (* Binding operators, applicative syntax *)
+ val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+ val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+
+ (* Binding operators, monad syntax *)
+ val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+ val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+ end
+
(** Datatype *)
val hash: ('a -> int) -> 'a t -> int
val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
@@ -160,9 +188,4 @@ module TopBottom: sig
(* Lattice operators *)
val join: ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
val narrow: ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
-
- (** Operators *)
- (* In presence of simultaneous `Bottom and `Top in and+ / and*, everything
- narrows down to `Bottom *)
- module Operators : Operators with type 'a t = 'a or_top_bottom
end
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index a348be6a0b9..34883ace8ad 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -174,9 +174,8 @@ struct
let map_join' : type c. ('a -> [< 'b or_top_bottom]) -> ('b -> 'b -> 'b) ->
('a, c) t -> 'b or_top_bottom =
fun map join ->
- let map' x = (map x :> 'b or_top_bottom)
- and join' = TopBottom.join (fun x y -> `Value (join x y)) in
- map_reduce default map' join'
+ let join' = TopBottom.join (fun x y -> `Value (join x y)) in
+ map_reduce default map join'
end
@@ -305,7 +304,7 @@ struct
let join = (@)
and extract state =
let r,_alarms = A.Eval.eval_function_exp exp state in
- (r :> _ or_top_bottom) >>-: List.map fst
+ r >>-: List.map fst
in
get req |> Response.map_join' extract join |> convert |>
Result.map (List.sort_uniq Kernel_function.compare)
@@ -318,11 +317,11 @@ struct
| None -> `Top
| Some get ->
let make_expr (x, _alarms) =
- (x :> _ or_top_bottom) >>-: fun (_valuation, v) ->
+ x >>-: fun (_valuation, v) ->
Cvalue.V_Or_Uninitialized.make ~initialized:true ~escaping:false (get v)
in
let make_lval (x, _alarms) =
- (x :> _ or_top_bottom) >>-: fun (_valuation, v) ->
+ let+ _valuation, v = x in
let Eval.{ v; initialized; escaping } = v in
let v =
match v with
@@ -354,7 +353,7 @@ struct
| Some get ->
let join = Main_values.CVal.join in
let extract value =
- (value :> _ or_top_bottom) >>-: get
+ value >>-: get
in
extract_value res |> Response.map_join' extract join |> convert
@@ -381,7 +380,7 @@ struct
assert (Int_Base.equal loc2.size size);
make_loc loc size
and extract loc =
- (loc :> _ or_top_bottom) >>-: get >>-: Precise_locs.imprecise_location
+ loc >>-: get >>-: Precise_locs.imprecise_location
in
extract_loc res |> fst |> Response.map_join' extract join |> convert
@@ -393,7 +392,7 @@ struct
let response_loc, access = extract_loc res in
let join = Locations.Zone.join
and extract loc =
- (loc :> _ or_top_bottom) >>-: get >>-:
+ loc >>-: get >>-:
Precise_locs.enumerate_valid_bits access
in
response_loc |> Response.map_join' extract join |> convert
@@ -403,7 +402,7 @@ struct
| LValue r ->
let join = (&&)
and extract (x, _alarms) =
- (x :> _ or_top_bottom) >>-: (fun (_valuation,fv) -> fv.Eval.initialized)
+ x >>-: (fun (_valuation,fv) -> fv.Eval.initialized)
in
begin match Response.map_join' extract join r with
| `Bottom | `Top -> false
--
GitLab