diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
index 6ca6bc1eb377457d9fb5e89cab584196cc3a6f82..646ba8975ae5ac8eb5285c10c85f1b670ec7a63e 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.ml
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -20,14 +20,19 @@
(* *)
(**************************************************************************)
+
+
+(** Types definitions *)
+
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 ]
+
+
(** Common functions *)
-module Common =
-struct
+module Common = struct
(* Pretty-printing *)
@@ -82,19 +87,22 @@ struct
| `Value vx, `Value vy -> is_included vx vy
(* Iterator *)
+
let iter f = function
| `Bottom | `Top -> ()
| `Value v -> f v
(* Conversion *)
+
let to_option = function
| `Bottom | `Top -> None
| `Value x -> Some x
end
+
+
module Bottom = struct
- type 'a t = 'a or_bottom
include Common
@@ -110,41 +118,38 @@ module Bottom = struct
(* Lattice operators *)
- let join join x y = match x, y with
- | `Value vx, `Value vy -> `Value (join vx vy)
+ let join join x y =
+ match x, y with
+ | `Value vx, `Value vy -> `Value (join vx vy)
| `Bottom, (`Value _ as v)
| (`Value _ as v), `Bottom
| (`Bottom as v), `Bottom -> v
- let join_list j l = List.fold_left (join j) `Bottom l
-
- let narrow narrow x y = match x, y with
- | `Value vx, `Value vy -> narrow vx vy
+ let narrow narrow x y =
+ match x, y with
+ | `Value vx, `Value vy -> narrow vx vy
| `Bottom, `Value _
| `Value _, `Bottom
| `Bottom, `Bottom -> `Bottom
- (* Iterators *)
-
- let bind f = function
- | `Bottom -> `Bottom
- | `Value v -> f v
-
- let fold ~bottom f = function
- | `Bottom -> bottom
- | `Value v -> f v
-
- let map f = function
- | `Bottom -> `Bottom
- | `Value v -> `Value (f v)
+ let join_list f = List.fold_left (join f) `Bottom
(* Combination *)
let zip x y =
match x, y with
- | `Bottom, #t | #t, `Bottom -> `Bottom
+ | `Bottom, _ | _, `Bottom -> `Bottom
| `Value x, `Value y -> `Value (x,y)
+ (* Monadic operations *)
+
+ include Monad.Extend_Kleisli_with_product (struct
+ type 'a t = 'a or_bottom
+ let return x = `Value x
+ let bind f = function `Bottom -> `Bottom | `Value x -> f x
+ let product l r = zip l r
+ end)
+
(** Conversion *)
let of_option = function
@@ -155,41 +160,19 @@ module Bottom = struct
| `Bottom -> []
| `Value v -> [v]
- let bot_of_list = function
- | [] -> `Bottom
- | l -> `Value l
-
- let list_of_bot = function
- | `Bottom -> []
- | `Value l -> l
-
- let add_to_list elt list = match elt with
+ let add_to_list elt list =
+ match elt with
| `Bottom -> list
| `Value elt -> elt :: list
let list_values l =
List.fold_left (fun l elt -> add_to_list elt l) [] l
- (** Operators *)
-
- module Operators =
- struct
- let (>>-) x f = bind f x
- let (>>-:) x f = map f x
- let (let+) x f = map f x
- let (and+) = zip
- let (let*) x f = bind f x
- let (and*) = zip
- end
-
(** Datatype construction *)
+
let counter = ref 0
- module Make_Datatype
- (Domain: Datatype.S)
- =
- Datatype.Make (
- struct
+ module Make_Datatype (Domain: Datatype.S) = Datatype.Make (struct
include Datatype.Serializable_undefined
type t = Domain.t or_bottom
let () = incr counter
@@ -207,21 +190,18 @@ module Bottom = struct
(* Bound lattice *)
- module Bound_Lattice
- (Lattice: Lattice_type.Join_Semi_Lattice)
- = struct
+ module Bound_Lattice (Lattice: Lattice_type.Join_Semi_Lattice) = struct
include Make_Datatype (Lattice)
-
let bottom = `Bottom
let join = join Lattice.join
let is_included = is_included Lattice.is_included
end
+
end
-module Top =
-struct
- type 'a t = 'a or_top
+
+module Top = struct
include Common
@@ -235,6 +215,12 @@ struct
| `Value v -> v
| `Top -> top
+ (** Conversion. *)
+
+ let of_option = function
+ | None -> `Top
+ | Some x -> `Value x
+
(** Lattice *)
let join join_value x y =
@@ -247,52 +233,88 @@ struct
| `Top, v | v, `Top -> v
| `Value vx, `Value vy -> `Value (narrow_value vx vy)
- (* Iterators *)
+ (** Combination *)
- let bind f = function
- | `Top -> `Top
- | `Value v -> f v
+ let zip x y =
+ match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Value x, `Value y -> `Value (x,y)
- let fold ~top f = function
- | `Top -> top
- | `Value v -> f v
+ (** Monadic operators *)
- let map f = function
- | `Top -> `Top
- | `Value v -> `Value (f v)
+ include Monad.Extend_Kleisli_with_product (struct
+ type 'a t = 'a or_top
+ let return x = `Value x
+ let bind f = function `Top -> `Top | `Value x -> f x
+ let product l r = zip l r
+ end)
+
+ (** Datatype construction *)
+
+ let counter = ref 0
+
+ module Make_Datatype (Domain: Datatype.S) = Datatype.Make (struct
+ include Datatype.Serializable_undefined
+ type t = Domain.t or_top
+ let () = incr counter
+ let name = Domain.name ^ "+top(" ^ string_of_int !counter ^ ")"
+ let reprs = `Top :: (List.map (fun v -> `Value v) Domain.reprs)
+ let structural_descr = Structural_descr.t_unknown
+ let hash = Common.hash Domain.hash
+ let equal = (Common.equal Domain.equal :> t -> t -> bool)
+ let compare = Common.compare Domain.compare
+ let rehash = Datatype.identity
+ let copy = map Domain.copy
+ let pretty = Common.pretty Domain.pretty
+ let mem_project = Datatype.never_any_project
+ end)
+
+end
+
+
+
+module TopBottom = struct
+
+ type 'a t = 'a or_top_bottom
+ include Common
(** Combination *)
let zip x y =
match x, y with
+ | `Bottom, #t | #t, `Bottom -> `Bottom
| `Top, #t | #t, `Top -> `Top
| `Value x, `Value y -> `Value (x,y)
- (** Conversion. *)
+ (** Monadic operators. We have to redefines every operators to ensure
+ subtyping properties. *)
- let of_option = function
- | None -> `Top
- | Some x -> `Value x
+ let return x = `Value x
+ let product l r = zip l r
- (** Operators *)
+ let bind f = function
+ | `Bottom -> `Bottom
+ | `Top -> `Top
+ | `Value x -> f x
- module Operators =
- struct
- let (>>-) x f = bind f x
- let (>>-:) x f = map f x
- let (let+) x f = map f x
- let (and+) = zip
- let (let*) x f = bind f x
- let (and*) = zip
+ let map f = function
+ | `Bottom -> `Bottom
+ | `Top -> `Top
+ | `Value x -> `Value (f x)
+
+ let flatten = function
+ | `Bottom | `Value `Bottom -> `Bottom
+ | `Top | `Value `Top -> `Top
+ | `Value `Value x -> `Value x
+
+ module Operators = struct
+ let ( >>- ) (m : [< 'a t]) (f : 'a -> ([> 'b t] as 'c)) : 'c = bind f m
+ let ( let* ) (m : [< 'a t]) (f : 'a -> ([> 'b t] as 'c)) : 'c = bind f m
+ let ( and* ) (l : [< 'a t]) (r : [< 'b t]) : [> ('a * 'b) t] = product l r
+ let ( >>-: ) (m : [< 'a t]) (f : 'a -> 'b) : [> 'b t] = map f m
+ let ( let+ ) (m : [< 'a t]) (f : 'a -> 'b) : [> 'b t] = map f m
+ let ( and+ ) (l : [< 'a t]) (r : [< 'b t]) : [> ('a * 'b) t] = product l r
end
-end
-
-
-module TopBottom =
-struct
- type 'a t = 'a or_top_bottom
-
- include Common
(* Lattice operators *)
@@ -306,40 +328,24 @@ struct
| `Bottom, _ | _, `Bottom -> `Bottom
| `Value vx, `Value vy -> (narrow_value vx vy :> 'a t)
- (* Iterators *)
-
- let bind f = function
- | `Top -> `Top
- | `Bottom -> `Bottom
- | `Value v -> f v
-
- let fold ~top ~bottom f = function
- | `Top -> top
- | `Bottom -> bottom
- | `Value v -> f v
-
- let map f = function
- | `Top -> `Top
- | `Bottom -> `Bottom
- | `Value v -> `Value (f v)
-
- (** Combination *)
+ (** Datatype construction *)
- let zip x y =
- match x, y with
- | `Bottom, #t | #t, `Bottom -> `Bottom
- | `Top, #t | #t, `Top -> `Top
- | `Value x, `Value y -> `Value (x,y)
+ let counter = ref 0
- (** Operators *)
+ module Make_Datatype (Domain: Datatype.S) = Datatype.Make (struct
+ include Datatype.Serializable_undefined
+ type t = Domain.t or_top_bottom
+ let () = incr counter
+ let name = Domain.name ^ "+top_bottom(" ^ string_of_int !counter ^ ")"
+ let reprs = `Bottom :: `Top :: (List.map (fun v -> `Value v) Domain.reprs)
+ let structural_descr = Structural_descr.t_unknown
+ let hash = Common.hash Domain.hash
+ let equal = (Common.equal Domain.equal :> t -> t -> bool)
+ let compare = Common.compare Domain.compare
+ let rehash = Datatype.identity
+ let copy = map Domain.copy
+ let pretty = Common.pretty Domain.pretty
+ let mem_project = Datatype.never_any_project
+ end)
- module Operators =
- struct
- let (>>-) x f = bind f x
- let (>>-:) x f = map f x
- let (let+) x f = map f x
- let (and+) = zip
- let (let*) x f = bind f x
- let (and*) = zip
- end
end
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.mli b/src/kernel_services/abstract_interp/lattice_bounds.mli
index 903fec7a1db3058103e5c6156cffcb759e4af295..9b444d32611eef76632a75e2d37034436c38384a 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.mli
+++ b/src/kernel_services/abstract_interp/lattice_bounds.mli
@@ -29,163 +29,129 @@ type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
module Bottom : sig
- type 'a t = 'a or_bottom
- (** Operators *)
- 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
+ include Monad.S_with_product with type 'a t = 'a or_bottom
(** Datatype constructor *)
- module Make_Datatype
- (Domain: Datatype.S)
- : Datatype.S with type t = Domain.t or_bottom
+ module Make_Datatype (Domain: Datatype.S) :
+ Datatype.S with type t = Domain.t or_bottom
(** Bounds a semi-lattice *)
- module Bound_Lattice
- (Lattice: Lattice_type.Join_Semi_Lattice)
- : Lattice_type.Bounded_Join_Semi_Lattice with type t = Lattice.t or_bottom
+ module Bound_Lattice (Lattice: Lattice_type.Join_Semi_Lattice) :
+ Lattice_type.Bounded_Join_Semi_Lattice with type t = Lattice.t or_bottom
(** Access *)
- val is_bottom: 'a t -> bool
- val non_bottom: 'a t -> 'a
- val value: bottom: 'a -> 'a t -> 'a
+ val is_bottom : 'a t -> bool
+ val non_bottom : 'a t -> 'a
+ val value : bottom:'a -> 'a t -> 'a
(** Datatype *)
- val hash: ('a -> int) -> 'a t -> int
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val hash : ('a -> int) -> 'a t -> int
+ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Pretty-printing *)
- val pretty_bottom :Format.formatter -> unit (* for %t specifier *)
- val pretty :
- (Format.formatter -> 'a -> unit) ->
- Format.formatter -> 'a t -> unit
+ val pretty_bottom : Format.formatter -> unit (* for %t specifier *)
+ val pretty : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
(* Lattice operators *)
- val is_included: ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
- val join: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
- val join_list: ('a -> 'a -> 'a) -> 'a t list -> 'a t
- val narrow: ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+ val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+ val join : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+ val narrow : ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+ val join_list : ('a -> 'a -> 'a) -> 'a t list -> 'a t
(* Iterators *)
- val iter: ('a -> unit) -> 'a t -> unit
- val bind: ('a -> 'b t) -> 'a t -> 'b t
- val fold: bottom:'b -> ('a -> 'b) -> 'a t -> 'b
- val map: ('a -> 'b) -> 'a t -> 'b t
+ val iter : ('a -> unit) -> 'a t -> unit
(* Combination *)
- val zip: 'a t -> 'b t -> ('a * 'b) t (* `Bottom if any is `Bottom *)
+ val zip : 'a t -> 'b t -> ('a * 'b) t (* `Bottom if any is `Bottom *)
(** In a lattice where the elements are lists of non-bottom values,
the empty list is the bottom case. *)
(** Conversion *)
- val to_option: 'a t -> 'a option
- val of_option: 'a option -> 'a t
- val to_list: 'a t -> 'a list
- val bot_of_list: 'a list -> 'a list t
- val list_of_bot: 'a list t -> 'a list
- val list_values: 'a t list -> 'a list
+ val to_option : 'a t -> 'a option
+ val of_option : 'a option -> 'a t
+ val to_list : 'a t -> 'a list
+ val list_values : 'a t list -> 'a list
(** [elt >:: list] adds [elt] to the [list] if it is not bottom. *)
- val add_to_list: 'a t -> 'a list -> 'a list
+ val add_to_list : 'a t -> 'a list -> 'a list
+
end
module Top : sig
- type 'a t = 'a or_top
- (** Operators *)
- module Operators : sig
- (** This monad propagates `Bottom and or `Top if needed. *)
- val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+ include Monad.S_with_product with type 'a t = 'a or_top
- (** 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 (Domain: Datatype.S) :
+ Datatype.S with type t = Domain.t or_top
(** Access *)
- val is_top: 'a t -> bool
- val non_top: 'a t -> 'a
- val value: top: 'a -> 'a t -> 'a
+ val is_top : 'a t -> bool
+ val non_top : 'a t -> 'a
+ val value : top:'a -> 'a t -> 'a
(** Datatype *)
- val hash: ('a -> int) -> 'a t -> int
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val hash : ('a -> int) -> 'a t -> int
+ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Pretty-printing *)
- val pretty_top :Format.formatter -> unit (* for %t specifier *)
+ val pretty_top : Format.formatter -> unit (* for %t specifier *)
val pretty :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a t -> unit
(** Lattice operators *)
- val join: ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
- val narrow: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+ val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+ val join : ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+ val narrow : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
(* Iterators *)
- val iter: ('a -> unit) -> 'a t -> unit
- val bind: ('a -> 'b t) -> 'a t -> 'b t
- val fold: top:'b -> ('a -> 'b) -> 'a t -> 'b
- val map: ('a -> 'b) -> 'a t -> 'b t
+ val iter : ('a -> unit) -> 'a t -> unit
(** Combination *)
- val zip: 'a t -> 'b t -> ('a * 'b) t (* `Top if any is `Top *)
+ val zip : 'a t -> 'b t -> ('a * 'b) t (* `Top if any is `Top *)
(** Conversion *)
val to_option : 'a t -> 'a option
val of_option : 'a option -> 'a t
+
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
+ include Monad.S_with_product with type 'a t = 'a or_top_bottom
- (** Use this monad if the following function returns a simple value. *)
- val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+ (** Datatype constructor *)
+ module Make_Datatype (Domain: Datatype.S) :
+ Datatype.S with type t = Domain.t or_top_bottom
+
+ (** Operators. In presence of simultaneous `Bottom and `Top in and+ / and*,
+ everything narrows down to `Bottom. Every operators is redefined to
+ ensure subtyping properties. *)
+ module Operators : sig
(* Binding operators, applicative syntax *)
+ val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
(* Binding operators, monad syntax *)
+ val (>>- ) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
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
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val hash : ('a -> int) -> 'a t -> int
+ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Pretty-printing *)
val pretty :
@@ -193,12 +159,8 @@ module TopBottom: sig
Format.formatter -> 'a t -> unit
(* 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
+ val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+ val join : ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
+ val narrow : ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
- (* Iterators *)
- val iter: ('a -> unit) -> 'a t -> unit
- val bind: ('a -> 'b t) -> 'a t -> 'b t
- val fold: top:'b -> bottom:'b -> ('a -> 'b) -> 'a t -> 'b
- val map: ('a -> 'b) -> 'a t -> 'b t
end
diff --git a/src/libraries/monads/monad.ml b/src/libraries/monads/monad.ml
new file mode 100644
index 0000000000000000000000000000000000000000..61099357703f0429a7066e09247dbaf5ca82f980
--- /dev/null
+++ b/src/libraries/monads/monad.ml
@@ -0,0 +1,157 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+
+
+(* Kleisli triple minimal signature *)
+module type Kleisli = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+end
+
+(* Categoric minimal signature *)
+module type Categoric = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val map : ('a -> 'b) -> 'a t -> 'b t
+ val flatten : 'a t t -> 'a t
+end
+
+(* Complete signature *)
+module type S = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ end
+end
+
+(** Extend a Kleisli triple monad *)
+module Extend_Kleisli (M : Kleisli) = struct
+ type 'a t = 'a M.t
+ let return x = M.return x
+ let bind f m = M.bind f m
+ let flatten m = bind (fun x -> x) m
+ let map f m = bind (fun x -> return (f x)) m
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( >>-: ) m f = map f m
+ let ( let+ ) m f = map f m
+ end
+end
+
+(** Extend a categoric monad *)
+module Extend_Categoric (M : Categoric) = struct
+ type 'a t = 'a M.t
+ let return x = M.return x
+ let map f m = M.map f m
+ let flatten m = M.flatten m
+ let bind f m = flatten (map f m)
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( >>-: ) m f = map f m
+ let ( let+ ) m f = map f m
+ end
+end
+
+
+
+(* Product on monads *)
+module type Product = sig
+ type 'a t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+end
+
+(* Kleisli triple with a product *)
+module type Kleisli_with_product = sig
+ include Kleisli
+ include Product with type 'a t := 'a t
+end
+
+(* Categoric monad with a product *)
+module type Categoric_with_product = sig
+ include Categoric
+ include Product with type 'a t := 'a t
+end
+
+(* Complete signature with a product *)
+module type S_with_product = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( and* ) : 'a t -> 'b t -> ('a * '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
+ end
+end
+
+(** Extend a Kleisli triple monad with a product *)
+module Extend_Kleisli_with_product (M : Kleisli_with_product) = struct
+ type 'a t = 'a M.t
+ let return x = M.return x
+ let bind f m = M.bind f m
+ let flatten m = bind (fun x -> x) m
+ let map f m = bind (fun x -> return (f x)) m
+ let product l r = M.product l r
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( let+ ) m f = map f m
+ let ( >>-: ) m f = map f m
+ let ( and* ) l r = product l r
+ let ( and+ ) l r = product l r
+ end
+end
+
+(** Extend a categoric monad with a product *)
+module Extend_Categoric_with_product (M : Categoric_with_product) = struct
+ type 'a t = 'a M.t
+ let return x = M.return x
+ let map f m = M.map f m
+ let flatten m = M.flatten m
+ let bind f m = flatten (map f m)
+ let product l r = M.product l r
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( let+ ) m f = map f m
+ let ( >>-: ) m f = map f m
+ let ( and* ) l r = product l r
+ let ( and+ ) l r = product l r
+ end
+end
diff --git a/src/libraries/monads/monad.mli b/src/libraries/monads/monad.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a31294b6e49cdab9f3ac85c4ad58a418bc8f3eb9
--- /dev/null
+++ b/src/libraries/monads/monad.mli
@@ -0,0 +1,264 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+
+
+(** {2 Kleisli triple signature for a monadic type constructor ['a t]}
+
+ This is the usual minimal definition of a monadic type constructor.
+ The [return] function embeds a value {m x} in the monad. The [bind]
+ function, also called the "combinator", corresponds to the idea of
+ "sequence" in the monadic world, i.e the call [bind f m] comes down
+ to performing the computation [m] before applying the next computation
+ step, represented by the function [f], to the resulting value.
+
+ To fully qualify as a monad, these three parts must respect the three
+ following laws :
+
+ 1. [return] is a left-identity for [bind] :
+ ∀f:('a -> 'b t), ∀x:'a, [bind f (return x) ≣ return (f x)]
+
+ 2. [return] is a right-identity for [bind] :
+ ∀m:'a t, [bind return m ≣ m]
+
+ 3. [bind] is associative :
+ ∀m:'a t, ∀f:('a -> 'b t), ∀g:('b -> 'c t),
+ [bind (fun x -> bind g (f x)) m ≣ bind g (bind f m)]
+
+ As there is no way in the OCaml type system to enforce those properties,
+ users have to trust the implemented monad when using it, and developpers
+ have to manually check that they are respected. *)
+module type Kleisli = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+end
+
+
+
+(** {2 Categoric signature for a monadic type constructor ['a t]}
+
+ In a computer science context, this is a rarer definition of a monadic
+ type constructor. It is however equivalent to the Kleisli triple one,
+ and may be simpler to use for certain monads, such as the [list] one.
+
+ To be pedantic, this approach defines a monad as a categoric functor
+ equipped with two natural transformations. This does sounds frightening
+ but this breaks down to rather simple concepts.
+
+ Let's start at the beginning. A category is just a collection of objets
+ and arrows (or morphisms) between those objets that satisfies two
+ properties: there exists a morphism from all objects to themselves, i.e
+ an identity, and if there is a morphism between objects [a] and [b] and
+ a morphism between objects [b] and [c], then there must be a morphism
+ between [a] and [c], i.e morphisms are associative.
+
+ There is a strong parallel between categories and type systems. Indeed,
+ if one uses the collection of all types as objects, then for all types
+ ['a] and ['b], the function [f : 'a -> 'b] can be seen as a morphism
+ between the objets ['a] and ['b]. As functions are naturally associative
+ and, for any type ['a], one can trivially defines the identity function
+ ['a -> 'a], one can conclude that types along with all functions of
+ arithy one forms a category.
+
+ Next, there is the idea of functors. In the category theory, a functor
+ is a mapping between categories. That means that, given two categories
+ [A] and [B], a functor maps all objects of [A] to an object of [B] and
+ maps all morphisms of [A] into a morphims of [B]. But, not all mappings
+ are functors. Indeed, to be a valid functor, one as to preserve the
+ identity morphisms and the composition of morphims.
+
+ The idea of functors can also be seen in a type systems. At least, the
+ more restricted but enough here of an endofunctor, a functor from a
+ category to itself. Indeed, for any type [v] and for any parametric
+ type ['a t], the type [v t] can be seen as a mapping from values of
+ type [v] to values of type [v t]. Thus the type ['a t] encodes the first
+ part of what a functor is, a mapping from objects of the Type category
+ to objects of the Type category. For the second part, we need a way to
+ transform morphisms of the Type category, i.e functions of type ['a -> 'b],
+ in a way that preserves categoric properties. Expressed as a type, this
+ transformation can be seen as a higher-order function [map] with the
+ type [map : ('a -> 'b) -> ('a t -> 'b t)].
+
+ Finally, this definition of a monad requires two natural transformations.
+ Simply put, a natural transformation is a mapping between functors that
+ preserves the structures of all the underlying categories (mathematicians
+ and naming conventions...). That may be quite complicated to grasp, but in
+ this case, the two required transformations are quite simple and intuitive.
+
+ The first one, as in a Kleisli triple, is a [return] function that embeds
+ values {m x} of type [v] into the monad. This function must satisfies
+ similar laws than in a Kleisli triple, but expressed in terms of [map] :
+
+ 1. ∀x:'a, ∀f:('a -> 'b), [return (f x) ≣ map f (return x)]
+
+ The second one is called [flatten], and can be seen as a way to "flatten"
+ nested applications of the monad. It must also satisfy some laws :
+
+ 2. ∀m:('a t t t), [map flatten (flatten m) ≣ flatten (flatten m)]
+ 3. ∀m:('a t), [flatten (map return m) ≣ flatten (return m) ≣ m]
+ 4. ∀m:('a t t), ∀f: ('a -> 'b), [flatten (map (map f) m) ≣ map f (flatten m)]
+
+ As there is no way in the OCaml type system to enforce those properties,
+ users have to trust the implemented monad when using it, and developpers
+ have to manually check that they are respected. *)
+module type Categoric = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val map : ('a -> 'b) -> 'a t -> 'b t
+ val flatten : 'a t t -> 'a t
+end
+
+
+
+(** {2 Extended signature with let-bindings}
+
+ The minimal definitions of a monad are not that useful when one tries to
+ develop clean monadic code. To help alleviate this, one should instead
+ uses monads respecting this extended signature, that combines both the
+ Kleisli triple and categoric definitions and provides two let-binding
+ operators. The operator [let*] corresponds to the [bind] function
+ while the operator [let+] corresponds to the [map]. *)
+module type S = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ end
+end
+
+
+
+(** {2 Extend minimal signature}
+
+ Those functors provide a way to extend a minimal signature into a full
+ monad that satisfies the signature defined above. This is possible
+ because one can defines operations from one monadic definition
+ using the operations required by the others. Indeed :
+
+ 1. ∀m:('a t), ∀f:('a -> 'b), [map f m ≣ bind (fun x -> return (f x)) m]
+ 2. ∀m:('a t t), [flatten m ≣ bind identity m]
+ 3. ∀m:('a t), ∀f:('a -> 'b t), [bind f m ≣ flatten (map f m)]
+
+ All required laws expressed in both minimal signatures are respected
+ using those definitions. *)
+
+(** Extend a Kleisli triple monad *)
+module Extend_Kleisli (M : Kleisli) : S with type 'a t = 'a M.t
+
+(** Extend a categoric monad *)
+module Extend_Categoric (M : Categoric) : S with type 'a t = 'a M.t
+
+
+
+(** {2 Product on monads}
+
+ In a computational point of view, a monad is an abstraction of a sequence
+ of operations. But sometimes, one may need to specify that two operations
+ can be perform in *any* order, for instance when dealing with concurrency
+ or generic errors handling using the [option] type. To do so, one needs
+ to specify a *product* on monadic values, i.e a way to combine two monads
+ into a new one. The concept of a product has also deep roots in category
+ theory, but there is no need to dive into this for the purpose of this
+ module. *)
+module type Product = sig
+ type 'a t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+end
+
+
+
+(** {3 Product on Kleisli triple monads}
+
+ When combined with a Kleisli triple monad, the product should respect
+ the following property if one wants it to truly encode that computations
+ can be performed in *any* order :
+
+ 1. ∀l:('a t), ∀r:('b t), ∀f:(('a * 'b) -> 'c t),
+ [bind f (product l r) ≣ bind (fun (b, a) -> f (a, b)) (product r l)]
+
+ However, in some cases, this property is not feasible. In those cases, it
+ should be explicitly stated. *)
+module type Kleisli_with_product = sig
+ include Kleisli
+ include Product with type 'a t := 'a t
+end
+
+
+
+(** {3 Product on Categoric monads}
+
+ When combined with a Categoric monad, the product should respect the
+ following property if one wants it to truly encode that computations
+ can be performed in *any* order :
+
+ 1. ∀l:('a t), ∀r:('b t), ∀f:(('a * 'b) -> 'c),
+ [map f (product l r) ≣ map (fun (b, a) -> f (a, b)) (product r l)]
+
+ However, in some cases, this property is not feasible. In those cases, it
+ should be explicitly stated.*)
+module type Categoric_with_product = sig
+ include Categoric
+ include Product with type 'a t := 'a t
+end
+
+
+
+(** {3 Extended monads with product}
+
+ Extended monads that provides a product also provides two and-binding
+ operators implementing it, the [and*] and [and+] operators.
+
+ Take note that a generic implementation of the product can be given
+ as [bind (fun a -> map (fun b -> (a, b)) r) l]. However, this
+ definition may not be symmetric, which is why one is required to
+ provide a custom product. *)
+module type S_with_product = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( and* ) : 'a t -> 'b t -> ('a * '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
+ end
+end
+
+(** Extend a Kleisli triple monad with product *)
+module Extend_Kleisli_with_product (M : Kleisli_with_product) :
+ S_with_product with type 'a t = 'a M.t
+
+(** Extend a categoric monad *)
+module Extend_Categoric_with_product (M : Categoric_with_product) :
+ S_with_product with type 'a t = 'a M.t
diff --git a/src/libraries/utils/option.ml b/src/libraries/monads/option.ml
similarity index 86%
rename from src/libraries/utils/option.ml
rename to src/libraries/monads/option.ml
index dc7cf73b39f51f4cb9c2912f4ce5ce1acf34bada..beb92fc126b85fca0c40e97dbcce914714e933d7 100644
--- a/src/libraries/utils/option.ml
+++ b/src/libraries/monads/option.ml
@@ -22,11 +22,12 @@
include Stdlib.Option
-let zip l r = match l, r with Some l, Some r -> Some (l, r) | _ -> None
-
-module Operators = struct
- let ( let* ) m f = bind m f
- let ( let+ ) m f = map f m
- let ( and* ) l r = zip l r
- let ( and+ ) l r = zip l r
+module Minimal = struct
+ type 'a t = 'a option
+ let return v = Some v
+ let bind f m = bind m f
+ let product l r = match l, r with Some l, Some r -> Some (l, r) | _ -> None
end
+
+include Monad.Extend_Kleisli_with_product (Minimal)
+let bind m f = bind f m
diff --git a/src/libraries/utils/option.mli b/src/libraries/monads/option.mli
similarity index 78%
rename from src/libraries/utils/option.mli
rename to src/libraries/monads/option.mli
index 2f8cbed250f26dd3e4d3ae08c808f396c3d51642..f671ec61e15af5105bd69592bbdeabd39f8f0a21 100644
--- a/src/libraries/utils/option.mli
+++ b/src/libraries/monads/option.mli
@@ -20,16 +20,9 @@
(* *)
(**************************************************************************)
-(* Adding let binding operators to the Option module. See
- https://v2.ocaml.org/manual/bindingops.html for more information. *)
-
+(* Extend the [option] type to a full fleshed monad. *)
include module type of Stdlib.Option
+include Monad.S_with_product with type 'a t = 'a option
-val zip : 'a option -> 'b option -> ('a * 'b) option
-
-module Operators : sig
- val ( let* ) : 'a option -> ('a -> 'b option) -> 'b option
- val ( let+ ) : 'a option -> ('a -> 'b) -> 'b option
- val ( and* ) : 'a option -> 'b option -> ('a * 'b) option
- val ( and+ ) : 'a option -> 'b option -> ('a * 'b) option
-end
+(* The bind is reversed for retrocompatibility reasons. *)
+val bind : 'a t -> ('a -> 'b t) -> 'b t
diff --git a/src/libraries/utils/result.ml b/src/libraries/monads/result.ml
similarity index 100%
rename from src/libraries/utils/result.ml
rename to src/libraries/monads/result.ml
diff --git a/src/libraries/utils/result.mli b/src/libraries/monads/result.mli
similarity index 100%
rename from src/libraries/utils/result.mli
rename to src/libraries/monads/result.mli
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 07440aa5df998418c374ab4fd13264237c756b5f..a5bcb30055223b72a780bdb78f8195ac3772fe77 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -417,7 +417,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
| Status truth -> Alarmset.Status.pretty fmt truth
let get_pointed_bases = function
- | Value v -> get_bases (Bottom.fold ~bottom:Cvalue.V.bottom get_cvalue v.v)
+ | Value v -> get_bases Bottom.(map get_cvalue v.v |> value ~bottom:Cvalue.V.bottom)
| Offsetmap offsm -> get_pointed_bases offsm
| Status _ -> Base.Hptset.empty
@@ -445,7 +445,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let pretty_eval = Bottom.pretty (pp_result typ) in
let value = Pretty_utils.to_string pretty_eval result in
let pointed_markers = get_pointed_markers eval_point in
- let pointed_vars = Bottom.fold ~bottom:[] pointed_markers result in
+ let pointed_vars = Bottom.(map pointed_markers result |> value ~bottom:[]) in
{ value; alarms; pointed_vars }
(* --- Evaluates an expression or lvalue into an evaluation [result]. ----- *)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 2d21392330438f3e357ebf4b8d659f4ba8e85c17..5e3ddcabfbca7b8a2b95528bb39e4a96fc0ad19e 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1277,8 +1277,9 @@ module State = struct
let mk_variable_builder (eval : evaluator) (_: t) =
let (let*) x f = Option.bind (Top.to_option x) f in
(* Is the interval computed for a variable a singleton? *)
- let is_singleton =
- Top.fold ~top:false Cvalue.V.cardinal_zero_or_one
+ let is_singleton v =
+ Top.map Cvalue.V.cardinal_zero_or_one v
+ |> Top.value ~top:false
in
fun exp ->
match exp.node with
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index 06c1daa44ce5840a433e7793feb222aa697d56a2..e1e64a105b104b64e1fdc4d68cf94570dc8f64f7 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -1742,7 +1742,7 @@ module Make
let cil_args = Option.map (List.map Eva_ast.to_cil_exp) args in
let alarm = Alarms.Function_pointer (cil_v, cil_args) in
let alarms = Alarmset.singleton ~status alarm in
- Bottom.bot_of_list list, alarms
+ Bottom.return list, alarms
end
| _ -> assert false
end
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 839d17ea3a3b7461da610afb861ccae1477ac1d2..b768b4fa11a0665901f757d825845801aac7b15e 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -735,7 +735,7 @@ module Make (Engine: Engine_sig.S) = struct
cacheable := NoCacheCallers;
states
in
- Bottom.list_of_bot states
+ Bottom.value ~bottom:[] states
in
(* Process each possible function apart, and append the result list. *)
let process acc (kf, valuation) =
@@ -743,7 +743,7 @@ module Make (Engine: Engine_sig.S) = struct
in
List.fold_left process [] functions
in
- Bottom.list_of_bot eval, !cacheable
+ Bottom.value ~bottom:[] eval, !cacheable
(* ------------------------------------------------------------------------ *)
(* Unspecified Sequence *)