diff --git a/Makefile b/Makefile
index bc1699b5bd89bed03d5b51c0c53d5372c69b24f1..57d5264ffe28ef9639bb5d1b5c0a3d74b6c9f7c2 100644
--- a/Makefile
+++ b/Makefile
@@ -586,7 +586,7 @@ KERNEL_CMO=\
src/kernel_services/ast_printing/description.cmo \
src/kernel_services/abstract_interp/lattice_messages.cmo \
src/kernel_services/abstract_interp/abstract_interp.cmo \
- src/kernel_services/abstract_interp/bottom.cmo \
+ src/kernel_services/abstract_interp/lattice_bounds.cmo \
src/kernel_services/abstract_interp/int_Base.cmo \
src/kernel_services/analysis/bit_utils.cmo \
src/kernel_services/abstract_interp/fc_float.cmo \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 45b246e8a48c7dbc258e0e48b73df33a5c0b1046..46728f67158b574cdc4d57a131dabe62f6f58a01 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -480,8 +480,6 @@ src/kernel_services/abstract_interp/abstract_offset.ml: CEA_LGPL
src/kernel_services/abstract_interp/abstract_offset.mli: CEA_LGPL
src/kernel_services/abstract_interp/base.ml: CEA_LGPL
src/kernel_services/abstract_interp/base.mli: CEA_LGPL
-src/kernel_services/abstract_interp/bottom.ml: CEA_LGPL
-src/kernel_services/abstract_interp/bottom.mli: CEA_LGPL
src/kernel_services/abstract_interp/eva_lattice_type.mli: CEA_LGPL
src/kernel_services/abstract_interp/fc_float.ml: CEA_LGPL
src/kernel_services/abstract_interp/fc_float.mli: CEA_LGPL
@@ -504,6 +502,8 @@ src/kernel_services/abstract_interp/int_val.ml: CEA_LGPL
src/kernel_services/abstract_interp/int_val.mli: CEA_LGPL
src/kernel_services/abstract_interp/ival.ml: CEA_LGPL
src/kernel_services/abstract_interp/ival.mli: CEA_LGPL
+src/kernel_services/abstract_interp/lattice_bounds.ml: CEA_LGPL
+src/kernel_services/abstract_interp/lattice_bounds.mli: CEA_LGPL
src/kernel_services/abstract_interp/lattice_messages.ml: CEA_LGPL
src/kernel_services/abstract_interp/lattice_messages.mli: CEA_LGPL
src/kernel_services/abstract_interp/lattice_type.mli: CEA_LGPL
diff --git a/src/kernel_services/abstract_interp/bottom.ml b/src/kernel_services/abstract_interp/bottom.ml
deleted file mode 100644
index b420661b852603263dd60a303203bd1f345ceab3..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/bottom.ml
+++ /dev/null
@@ -1,186 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* 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 = struct
-
- type 'a or_bottom = [ `Value of 'a | `Bottom ]
-
- (* This monad propagates the `Bottom value if needed. *)
- let (>>-) t f = match t with
- | `Bottom -> `Bottom
- | `Value t -> f t
-
- (* Use this monad if the following function returns a simple value. *)
- let (>>-:) t f = match t with
- | `Bottom -> `Bottom
- | `Value t -> `Value (f t)
-
-end
-
-include Type
-
-let is_bottom = function
- | `Bottom -> true
- | `Value _ -> false
-
-let non_bottom = function
- | `Value v -> v
- | `Bottom -> assert false
-
-let value ~bottom = function
- | `Value v -> v
- | `Bottom -> bottom
-
-let equal equal x y = match x, y with
- | `Bottom, `Bottom -> true
- | `Value vx, `Value vy -> equal vx vy
- | _ -> false
-
-let compare compare a b = match a, b with
- | `Bottom, `Bottom -> 0
- | `Bottom, _ -> -1
- | _, `Bottom -> 1
- | `Value v, `Value w -> compare v w
-
-let is_included is_included x y = match x, y with
- | `Bottom, _ -> true
- | _, `Bottom -> false
- | `Value vx, `Value vy -> is_included 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
- | `Bottom, `Value _
- | `Value _, `Bottom
- | `Bottom, `Bottom -> `Bottom
-
-let pretty pretty fmt = function
- | `Bottom -> Format.fprintf fmt "Bottom"
- | `Value v -> pretty fmt v
-
-let iter f = function
- | `Bottom -> ()
- | `Value v -> f v
-
-let fold ~bottom f = function
- | `Bottom -> bottom
- | `Value v -> f v
-
-let counter = ref 0
-
-module Make_Datatype
- (Domain: Datatype.S)
- =
- Datatype.Make (
- struct
- include Datatype.Serializable_undefined
- type t = Domain.t or_bottom
- let () = incr counter
- let name = Domain.name ^ "+bottom(" ^ string_of_int !counter ^ ")"
- let reprs = [`Bottom; `Value (List.hd Domain.reprs)]
- let structural_descr = Structural_descr.t_unknown
- (* Structural_descr.t_sum [| [| Domain.packed_descr |] |] *)
-
- let equal a b = match a, b with
- | `Bottom, `Bottom -> true
- | `Value v, `Value w -> Domain.equal v w
- | _, _ -> false
-
- let compare a b = match a, b with
- | `Bottom, `Bottom -> 0
- | `Bottom, _ -> -1
- | _, `Bottom -> 1
- | `Value v, `Value w -> Domain.compare v w
-
- let hash = function
- | `Bottom -> 0
- | `Value v -> Domain.hash v
-
- let rehash = Datatype.identity
-
- let copy = function
- | `Bottom -> `Bottom
- | `Value v -> `Value (Domain.copy v)
-
- let pretty fmt = function
- | `Bottom -> Format.fprintf fmt "Bottom"
- | `Value v -> Domain.pretty fmt v
-
- let mem_project = Datatype.never_any_project
- end)
-
-
-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
-
-let to_option = function
- | `Bottom -> None
- | `Value v -> Some v
-
-let to_list = function
- | `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
- | `Bottom -> list
- | `Value elt -> elt :: list
-
-let all l =
- List.fold_left (fun l elt -> add_to_list elt l) [] l
-
-module Top = struct
-
- type 'a or_top_bottom = [ 'a or_bottom | `Top ]
-
- let join vjoin x y = match x, y with
- | `Top, _ | _, `Top -> `Top
- | (#or_bottom as x), (#or_bottom as y) -> join vjoin x y
-
- let narrow vnarrow x y = match x, y with
- | `Top, v | v, `Top -> v
- | (#or_bottom as x), (#or_bottom as y) ->
- (narrow vnarrow x y :> _ or_top_bottom)
-
-end
diff --git a/src/kernel_services/abstract_interp/bottom.mli b/src/kernel_services/abstract_interp/bottom.mli
deleted file mode 100644
index fad87be41a342bee62ce8fe041c9ba0e4aa7c0ca..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/bottom.mli
+++ /dev/null
@@ -1,98 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Types, monads and utilitary functions for lattices in which the bottom is
- managed separately from other values. *)
-
-module Type : sig
-
- type 'a or_bottom = [ `Value of 'a | `Bottom ]
-
- (** This monad propagates the `Bottom value if needed. *)
- val (>>-) : 'a or_bottom -> ('a -> 'b or_bottom) -> 'b or_bottom
-
- (** Use this monad if the following function returns a simple value. *)
- val (>>-:) : 'a or_bottom -> ('a -> 'b) -> 'b or_bottom
-
-end
-
-include module type of Type
-
-val is_bottom: 'a or_bottom -> bool
-val non_bottom: 'a or_bottom -> 'a
-val value: bottom: 'a -> 'a or_bottom -> 'a
-
-val equal: ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
-val compare: ('a -> 'a -> int) -> 'a or_bottom -> 'a or_bottom -> int
-val is_included: ('a -> 'b -> bool) -> 'a or_bottom -> 'b or_bottom -> bool
-val join: ('a -> 'a -> 'a) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
-val join_list: ('a -> 'a -> 'a) -> 'a or_bottom list -> 'a or_bottom
-val narrow: ('a -> 'a -> 'a or_bottom) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
-
-val pretty :
- (Format.formatter -> 'a -> unit) ->
- Format.formatter -> 'a or_bottom -> unit
-
-val iter: ('a -> unit) -> 'a or_bottom -> unit
-val fold: bottom: 'b -> ('a -> 'b) -> 'a or_bottom -> 'b
-
-(** Datatype constructor. *)
-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
-
-
-
-(** In a lattice where the elements are lists of non-bottom values,
- the empty list is the bottom case. *)
-
-(** Conversion functions. *)
-val to_option : 'a or_bottom -> 'a option
-val to_list: 'a or_bottom -> 'a list
-val bot_of_list: 'a list -> 'a list or_bottom
-val list_of_bot: 'a list or_bottom -> 'a list
-val all: 'a or_bottom list -> 'a list
-
-(** [elt >:: list] adds [elt] to the [list] if it is not bottom. *)
-val add_to_list : 'a or_bottom -> 'a list -> 'a list
-
-
-(** Lattices in which both top and bottom are managed separately *)
-module Top: sig
-
- type 'a or_top_bottom = [ 'a or_bottom | `Top ]
-
- val join:
- ('a -> 'a -> 'a) ->
- 'a or_top_bottom -> 'a or_top_bottom -> 'a or_top_bottom
-
- val narrow:
- ('a -> 'a -> 'a or_bottom) ->
- 'a or_top_bottom -> 'a or_top_bottom -> 'a or_top_bottom
-
-end
diff --git a/src/kernel_services/abstract_interp/eva_lattice_type.mli b/src/kernel_services/abstract_interp/eva_lattice_type.mli
index 8c5e10c62fded3e273207b4d847b732420cc76eb..e05c1ee9c49e5d9c7de08120923ecea494ddbe53 100644
--- a/src/kernel_services/abstract_interp/eva_lattice_type.mli
+++ b/src/kernel_services/abstract_interp/eva_lattice_type.mli
@@ -25,7 +25,7 @@
when needed. Except that, they are identical to the module signatures in
{!Lattice_type}. *)
-open Bottom.Type
+open Lattice_bounds
module type Join_Semi_Lattice = Lattice_type.Join_Semi_Lattice
module type With_Top = Lattice_type.With_Top
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index aa8216f716a3171f1d8bcc34d6a8d022487179d0..1f5d34a2f4a01a74a6e140559324e5f234011673 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -21,7 +21,8 @@
(**************************************************************************)
module Comp = Abstract_interp.Comp
-open Bottom.Type
+open Lattice_bounds
+open Bottom.Operators
type round = Float_sig.round = Up | Down | Near | Zero
type prec = Float_sig.prec = Single | Double | Long_Double | Real
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index 560d6f692d142bc05a396c2256a84eac6920c4ec..b1b3561dcee85cc4f0c706bf3d67bd6c25607dee 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -22,7 +22,7 @@
(** Signature for the floating-point interval semantics. *)
-open Bottom.Type
+open Lattice_bounds
(** Precision of the intervals. *)
type prec = Float_sig.prec
@@ -116,7 +116,7 @@ module type S = sig
[f1] into [f1'] so that the relation [f1' op f2] holds.
[prec] is the precision of [f1] and [f1'], but not necessarily of [f2]. *)
val backward_comp_left_true:
- Abstract_interp.Comp.t -> prec -> t -> t -> t Bottom.or_bottom
+ Abstract_interp.Comp.t -> prec -> t -> t -> t or_bottom
(** [backward_comp_left_false op prec f1 f2] attempts to reduce
[f1] into [f1'] so that the relation [f1' op f2] doesn't holds.
diff --git a/src/kernel_services/abstract_interp/fval.mli b/src/kernel_services/abstract_interp/fval.mli
index 93aa5e24a914d858537e5e50fe84b9615fbac907..30e3e709536d52435094415029b9b94166a53bab 100644
--- a/src/kernel_services/abstract_interp/fval.mli
+++ b/src/kernel_services/abstract_interp/fval.mli
@@ -89,7 +89,7 @@ val e: t (** Real representation of \e. *)
val contains_plus_zero : t -> bool
-val meet: t -> t -> t Bottom.or_bottom
+val meet: t -> t -> t Lattice_bounds.or_bottom
val is_singleton : t -> bool
(** Returns [true] on NaN. We expect this function to be e.g. to perform
@@ -134,7 +134,7 @@ val ceil: kind -> t -> t
val trunc: kind -> t -> t
val fround: kind -> t -> t
-val backward_cast_float_to_double: t -> t Bottom.or_bottom
+val backward_cast_float_to_double: t -> t Lattice_bounds.or_bottom
(** [backward_cast_float_to_double d] return all possible float32 [f] such that
[(double)f = d]. The double of [d] that have no float32 equivalent are
discarded. *)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 9d72418a04c039447427c931d35c7881e5f5ff35..f1eb54dada1209a83225a2b0b5017fb34e7be71b 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -699,7 +699,7 @@ let div x y =
`Value (div_range x min gneg)
else `Bottom
in
- Bottom.join join result_neg result_pos
+ Lattice_bounds.Bottom.join join result_neg result_pos
(* ----------------------------------- Misc --------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
index dbdbcba5db2233ff1e0d29f7e973a8ce13689c09..1e52aa926a144e2311b8f68fc4ed9e86ab4e8da1 100644
--- a/src/kernel_services/abstract_interp/int_interval.mli
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -26,7 +26,7 @@
A value of [None] for [min] (resp. [max]) represents -infinity
(resp. +infinity). [modu] is > 0, and [0 <= rem < modu]. *)
-open Bottom.Type
+open Lattice_bounds
include Datatype.S_with_collections
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 72ad214057be997c0278b060c33c9a04dda5588e..1d5a7fad690e76287ed21e296371fcd9b25df308 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Abstract_interp
-open Bottom.Type
+open Lattice_bounds
(* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index 0eab36f019c0ff870f1a29e5f7618144a8c61383..d3aac28587ccc2bf78c127d5710a0a4cc4501fba 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -30,7 +30,7 @@
Sets are always non-empty. The functions reducing the sets returns a
[set or_bottom] type: either the result is non-empty, or it is `Bottom. *)
-open Bottom.Type
+open Lattice_bounds
(** Returns the limit above which integer sets are converted into intervals. *)
val get_small_cardinal: unit -> int
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 5cade9d5c4948b35ff016ea83e86dfbed557a055..6e661036c0cc91facfb7fc2c1d62a1e384b8146e 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -21,7 +21,8 @@
(**************************************************************************)
open Abstract_interp
-open Bottom.Type
+open Lattice_bounds
+open Bottom.Operators
let small_cardinal = Int_set.get_small_cardinal
let small_cardinal_Int () = Int.of_int (small_cardinal ())
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 47b23b1d145c9f366da0773fbd2d2071dca790e1..86b7f208542a3b944d820a41f48a214d18ddba55 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -26,7 +26,7 @@
(** Abstractions do not represent the empty set. Instead, operations creating
empty sets return `Bottom. *)
-open Bottom.Type
+open Lattice_bounds
include Datatype.S_with_collections
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index c6495c9d001045a770e8dc1b0e7d4d880b6712c1..5022d6fd6adde061e50d9b15851be9c0391ad98c 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -21,7 +21,8 @@
(**************************************************************************)
open Abstract_interp
-open Bottom.Type
+open Lattice_bounds
+open Bottom.Operators
let emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
@@ -1031,7 +1032,6 @@ let reinterpret_as_float kind i =
then [`Value Fval.nan]
else []
in
- let open Bottom in
let range mn mx = Fval.inject kind (conv mn) (conv mx) in
(* convert positive floats; increasing on positive range *)
let pos = bounds_narrow f_pos >>-: (fun (b, e) -> range b e) in
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index 5e072bc1ecb175e16a86eaeb73675f3a214517e4..82740fff771c53814b332b5658c12f92214bba01 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -272,7 +272,7 @@ val create_all_values: signed:bool -> size:int -> t
representable in [size] bits. *)
val all_values: size:Integer.t -> t -> bool
-val backward_mult_int_left: right:t -> result:t -> t option Bottom.or_bottom
+val backward_mult_int_left: right:t -> result:t -> t option Lattice_bounds.or_bottom
val backward_comp_int_left : Comp.t -> t -> t -> t
(** [backward_comp_int op l r] reduces [l] into [l'] so that
@@ -319,7 +319,7 @@ val reinterpret_as_int: size:Integer.t -> signed:bool -> t -> t
(** Bitwise reinterpretation of the given value, of size [size], as an integer
of the given signedness (and size). *)
-val complement_int_under: size:int -> signed:bool -> t -> t Bottom.or_bottom
+val complement_int_under: size:int -> signed:bool -> t -> t Lattice_bounds.or_bottom
(** Returns an under-approximation of the integers of the given size and
signedness that are *not* represented by the given ival. *)
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3b7fb552f534d8b9ec6c53b4d6fbc7ef19be2367
--- /dev/null
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -0,0 +1,328 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 '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
+
+ (* Pretty-printing *)
+
+ let pretty_top fmt =
+ Format.pp_print_string fmt (Unicode.top_string ())
+
+ let pretty_bottom fmt =
+ Format.pp_print_string fmt (Unicode.bottom_string ())
+
+ let pretty pretty_value fmt = function
+ | `Bottom -> pretty_bottom fmt
+ | `Top -> pretty_top fmt
+ | `Value v -> pretty_value fmt v
+
+ (* Datatype *)
+
+ let hash hash_value = function
+ | `Bottom -> 7
+ | `Top -> 13
+ | `Value v -> hash_value v
+
+ let equal equal_value x y =
+ match x, y with
+ | `Bottom, `Bottom -> true
+ | `Top, `Top -> true
+ | `Value vx, `Value vy -> equal_value vx vy
+ | (`Value _ | `Bottom | `Top), (`Value _ | `Bottom | `Top) -> false
+
+ let compare compare_value a b = match a, b with
+ | `Bottom, `Bottom -> 0
+ | `Bottom, (`Top | `Value _) -> -1
+ | (`Top | `Value _), `Bottom -> 1
+ | `Top, `Top -> 0
+ | `Top, `Value _ -> -1
+ | `Value _, `Top -> 1
+ | `Value vx, `Value vy -> compare_value vx vy
+
+ (* Tests *)
+
+ let is_bottom = function
+ | `Bottom -> true
+ | `Value _ | `Top -> false
+
+ let is_top = function
+ | `Top -> true
+ | `Value _ | `Bottom -> false
+
+ let is_included is_included x y =
+ match x, y with
+ | `Bottom, _ | _, `Top -> true
+ | _, `Bottom | `Top, _ -> false
+ | `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
+
+ (** Access *)
+
+ let non_bottom = function
+ | `Value v -> v
+ | `Bottom -> assert false
+
+ let value ~bottom = function
+ | `Value v -> v
+ | `Bottom -> bottom
+
+ (* Lattice operators *)
+
+ 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
+ | `Bottom, `Value _
+ | `Value _, `Bottom
+ | `Bottom, `Bottom -> `Bottom
+
+ (* Iterators *)
+
+ let fold ~bottom f = function
+ | `Bottom -> bottom
+ | `Value v -> f v
+
+ let map f = function
+ | `Bottom -> `Bottom
+ | `Value v -> `Value (f v)
+
+ (* Combination *)
+
+ let zip x y =
+ match x, y with
+ | `Bottom, _ | _, `Bottom -> `Bottom
+ | `Value x, `Value y -> `Value (x,y)
+
+ (** Conversion *)
+
+ let of_option = function
+ | None -> `Bottom
+ | Some v -> `Value v
+
+ let to_list = function
+ | `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
+ | `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 (>>-) t f = match t with
+ | `Bottom -> `Bottom
+ | `Value t -> f t
+
+ let (>>-:) t f = match t with
+ | `Bottom -> `Bottom
+ | `Value t -> `Value (f t)
+
+ let (let+) = (>>-:)
+ let (and+) = zip
+ let (let*) = (>>-)
+ let (and*) = zip
+ 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_bottom
+ let () = incr counter
+ let name = Domain.name ^ "+bottom(" ^ string_of_int !counter ^ ")"
+ let reprs = `Bottom :: (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)
+
+ (* Bound lattice *)
+
+ 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
+
+ include Common
+
+ (** Access *)
+
+ let non_top = function
+ | `Value v -> v
+ | `Top -> assert false
+
+ let value ~top = function
+ | `Value v -> v
+ | `Top -> top
+
+ (** Lattice *)
+
+ let join join_value x y =
+ match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Value vx, `Value vy -> join_value vx vy
+
+ let narrow narrow_value x y =
+ match x, y with
+ | `Top, v | v, `Top -> v
+ | `Value vx, `Value vy -> `Value (narrow_value vx vy)
+
+ (** Combination *)
+
+ let zip x y =
+ match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Value x, `Value y -> `Value (x,y)
+
+ (** Conversion. *)
+
+ let of_option = function
+ | None -> `Top
+ | Some x -> `Value x
+
+ (** Operators *)
+
+ module Operators = struct
+ let (>>-) t f = match t with
+ | `Top -> `Top
+ | `Value t -> f t
+
+ let (>>-:) t f = match t with
+ | `Top -> `Top
+ | `Value t -> `Value (f t)
+
+ let (let+) = (>>-:)
+ let (and+) = zip
+ let (let*) = (>>-)
+ let (and*) = zip
+ end
+end
+
+
+module TopBottom =
+struct
+ type 'a t = 'a or_top_bottom
+
+ include Common
+
+ (* Lattice operators *)
+
+ let join join_value x y = match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Bottom, x | x, `Bottom -> x
+ | `Value vx, `Value vy -> (join_value vx vy :> 'a t)
+
+ let narrow narrow_value x y = match x, y with
+ | `Top, v | v, `Top -> v
+ | `Bottom, _ | _, `Bottom -> `Bottom
+ | `Value vx, `Value vy -> (narrow_value vx vy :> 'a t)
+
+ (** Combination *)
+
+ let zip x y =
+ match x, y with
+ | `Bottom, _ | _, `Bottom -> `Bottom
+ | `Top, _ | _, `Top -> `Top
+ | `Value x, `Value y -> `Value (x,y)
+
+ (** Operators *)
+
+ module Operators = struct
+ let (>>-) t f = match t with
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value t -> f t
+
+ let (>>-:) t f = match t with
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value t -> `Value (f t)
+
+ let (let+) = (>>-:)
+ let (and+) = zip
+ let (let*) = (>>-)
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..1d4ff6f981953528b5ca07ac081628344cf9e855
--- /dev/null
+++ b/src/kernel_services/abstract_interp/lattice_bounds.mli
@@ -0,0 +1,191 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Types, monads and utilitary functions for lattices in which the bottom
+ and/or the top are managed separately from other values. *)
+
+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 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
+
+ (** Datatype constructor *)
+ 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
+
+ (** Access *)
+ 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
+
+ (** Pretty-printing *)
+ 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
+
+ (* Iterators *)
+ val iter: ('a -> unit) -> 'a t -> unit
+ val fold: bottom: 'b -> ('a -> 'b) -> 'a t -> 'b
+ val map: ('a -> 'b) -> 'a t -> 'b t
+
+ (* Combination *)
+ 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
+
+ (** [elt >:: list] adds [elt] to the [list] if it is not bottom. *)
+ 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
+
+ (** 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
+ 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
+
+ (** Pretty-printing *)
+ 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
+
+ (** Combination *)
+ 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
+
+ (** 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
+ val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+
+ (** Pretty-printing *)
+ 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 t]) -> 'a t -> 'a t -> 'a t
+end
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index c4d22d71789d1efdfa1a53cf9e892ff226eb35ad..afe85f50c5b901176bd733b5884258627c85ea3e 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -22,6 +22,7 @@
open Abstract_interp
open Locations
+open Lattice_bounds
let msg_emitter = Lattice_messages.register "Lmap";;
@@ -41,7 +42,7 @@ module Make_LOffset
and type widen_hint = V.numerical_widen_hint)
(Default_offsetmap: sig
val name: string
- val default_offsetmap : Base.t -> Offsetmap.t Bottom.or_bottom
+ val default_offsetmap : Base.t -> Offsetmap.t or_bottom
val default_contents: V.t default_contents
end)
=
@@ -631,7 +632,7 @@ struct
let find_base_or_default b = function
| Bottom -> `Bottom
| Top -> `Top
- | Map m -> (M.find_or_default b m :> _ Bottom.Top.or_top_bottom)
+ | Map m -> (M.find_or_default b m :> _ or_top_bottom)
let remove_base b = function
| Bottom -> Bottom
diff --git a/src/kernel_services/abstract_interp/lmap.mli b/src/kernel_services/abstract_interp/lmap.mli
index 0d2068a665479c7c61e385117913e26859100e7d..5eb0e0b0e2aa6283397122fe4bda0581ef19657a 100644
--- a/src/kernel_services/abstract_interp/lmap.mli
+++ b/src/kernel_services/abstract_interp/lmap.mli
@@ -44,7 +44,7 @@ module Make_LOffset
val name: string
(** Used to create different datatypes each time the functor is applied *)
- val default_offsetmap : Base.t -> Offsetmap.t Bottom.or_bottom
+ val default_offsetmap : Base.t -> Offsetmap.t Lattice_bounds.or_bottom
(** Value returned when a map is queried, and the base is not present.
[`Bottom] indicates that the base is never bound in such a map. *)
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index 850a0189bba8890801e0300f1edb7607fa1bdbee..ee6e25cad0d1d230c328933d10ed64192b07ae5e 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Locations
+open Lattice_bounds
exception Bitwise_cannot_copy
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index 00164382ae2f4fce610c6188eecb566fdd125a7e..2636e657c17e6994dbbc9ad21a0bad5d07643beb 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.mli
+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
@@ -94,7 +94,7 @@ val find: ?conflate_bottom:bool -> t -> location -> v
is no Top value in the type {!v}. *)
val copy_offsetmap :
- Location_Bits.t -> Integer.t -> t -> offsetmap Bottom.or_bottom
+ Location_Bits.t -> Integer.t -> t -> offsetmap Lattice_bounds.or_bottom
(** [copy_offsetmap alarms loc size m] returns the superposition of the
ranges of [size] bits starting at [loc] within [m]. [size] must be
strictly greater than zero. Return [None] if all pointed addresses are
@@ -103,10 +103,10 @@ val copy_offsetmap :
@raise Error_Top when the location or the state are Top, and there
is no Top value in the type {!v}. *)
-val find_base : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom
+val find_base : Base.t -> t -> offsetmap Lattice_bounds.or_top_bottom
(** @raise Not_found if the varid is not present in the map. *)
-val find_base_or_default : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom
+val find_base_or_default : Base.t -> t -> offsetmap Lattice_bounds.or_top_bottom
(** Same as [find_base], but return the default values for bases
that are not currently present in the map. Prefer the use of this function
to [find_base], unless you explicitly want to see if the base is bound. *)
diff --git a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
index de3bb300395095518239e2e3f1bd4e4fefa68f3d..d70edcda7c0a9e9e7f69f9c51989d30f633c98e0 100644
--- a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
+++ b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
@@ -67,11 +67,11 @@ val find_iset : validity:Base.validity -> intervals -> t -> v
val add_binding_intervals :
validity:Base.validity ->
- exact:bool -> intervals -> v -> t -> t Bottom.or_bottom
+ exact:bool -> intervals -> v -> t -> t Lattice_bounds.or_bottom
val add_binding_ival :
validity:Base.validity ->
- exact:bool -> Ival.t -> size:Int_Base.t -> v -> t -> t Bottom.or_bottom
+ exact:bool -> Ival.t -> size:Int_Base.t -> v -> t -> t Lattice_bounds.or_bottom
(** {2 Creating an offsetmap} *)
@@ -83,7 +83,7 @@ val empty: t
(** offsetmap containing no interval. *)
val size_from_validity:
- Base.validity -> Integer.t Bottom.or_bottom
+ Base.validity -> Integer.t Lattice_bounds.or_bottom
(** [size_from_validity v] returns the size to be used when creating a
new offsetmap for a base with validity [v]. This is a convention that
should be shared by all modules that create offsetmaps.
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.mli b/src/kernel_services/abstract_interp/offsetmap_sig.mli
index 172a935d91313ae582f3be2daea2c1f30b9246bc..c653a13f9a4b79ff887e126d661f2b13bf0595fc 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.mli
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.mli
@@ -63,7 +63,7 @@ val of_list: ((t -> v -> t) -> t -> 'l -> t) -> 'l -> Int.t -> t
val empty: t
(** offsetmap containing no interval. *)
-val size_from_validity: Base.validity -> Integer.t Bottom.or_bottom
+val size_from_validity: Base.validity -> Integer.t Lattice_bounds.or_bottom
(** [size_from_validity v] returns the size to be used when creating a
new offsetmap for a base with validity [v]. This is a convention that
must be shared by all modules that create offsetmaps, because operations
@@ -196,7 +196,7 @@ val find_imprecise_everywhere: t -> v
val copy_slice:
validity:Base.validity ->
offsets:Ival.t -> size:Integer.t ->
- t -> t Bottom.or_bottom
+ t -> t Lattice_bounds.or_bottom
(** [copy_slice ~validity ~offsets ~size m] copies and merges the slices of
[m] starting at offsets [offsets] and of size [size]. Offsets invalid
according to [validity] are removed. [size] must be strictly greater
@@ -220,7 +220,7 @@ val update :
offsets:Ival.t ->
size:Int.t ->
v ->
- t -> t Bottom.or_bottom
+ t -> t Lattice_bounds.or_bottom
(** [update ?origin ~validity ~exact ~offsets ~size v m] writes [v],
of size [size], each [offsets] in [m]; [m] must be of the size implied by
[validity]. [~exact=true] results in a strong update, while
@@ -235,7 +235,7 @@ val update_under :
offsets:Ival.t ->
size:Int.t ->
v ->
- t -> t Bottom.or_bottom
+ t -> t Lattice_bounds.or_bottom
(** Same as {!update}, except that no over-approximation on the set
of offsets or on the value written occurs. In case of imprecision,
[m] is not updated. *)
@@ -244,7 +244,7 @@ val update_under :
val update_imprecise_everywhere:
validity:Base.validity ->
Origin.t -> v ->
- t -> t Bottom.or_bottom
+ t -> t Lattice_bounds.or_bottom
(** [update_everywhere ~validity o v m] computes the offsetmap resulting
from imprecisely writing [v] potentially anywhere where [m] is valid
according to [validity]. If a value becomes too imprecise, [o] is used
@@ -256,7 +256,7 @@ val paste_slice:
from:t ->
size:Int.t ->
offsets:Ival.t ->
- t -> t Bottom.or_bottom
+ t -> t Lattice_bounds.or_bottom
(** {2 Shape} *)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 784b1a0fa9ad832637b2d1a9d7f761b8f95e8b2f..8714daa8f222455631017568fc60ce4afdd39618 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -337,7 +337,7 @@ end
module Proxy(A : Analysis.S) : EvaProxy = struct
open Eval
- type dstate = A.Dom.state or_top_or_bottom
+ type dstate = A.Dom.state or_top_bottom
let get_precise_loc =
let default = fun _ -> Precise_locs.loc_top in
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index a6145775c9145c21dbb1136ee66ab61136a8e44d..c29b62c4e48ea5ddbec3b8c669f8021cee8b0e97 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -24,6 +24,7 @@ open Cil_types
open Abstract_interp
open Locations
open Cvalue
+open Lattice_bounds
let dkey = Self.register_category "malloc"
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 3c434d03e0633706083da76f9238596280e8f101..141c643cc703d84b082afa5a7af9e5b6355a0b92 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -52,7 +52,7 @@ module type LeafDomain = sig
current_input:t -> previous_output:t -> t
val show_expr: 'a -> t -> Format.formatter -> exp -> unit
- val post_analysis: t Bottom.or_bottom -> unit
+ val post_analysis: t Lattice_bounds.or_bottom -> unit
module Store: Domain_store.S with type t := t
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index 9be07c5c74e3d39836cbcf98dc05317445ebe381..bf3c05b8f0cc79efed1e2e4ec30131f737bd49df 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -58,7 +58,7 @@ module type LeafDomain = sig
current_input:t -> previous_output:t -> t
val show_expr: 'a -> t -> Format.formatter -> exp -> unit
- val post_analysis: t Bottom.or_bottom -> unit
+ val post_analysis: t Lattice_bounds.or_bottom -> unit
module Store: Domain_store.S with type t := t
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 426f36a687d6e3b13010d9ca067d8b2f7b1e7c58..5692678cb22ce05a3e3932e157d225b667c02ed4 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -42,12 +42,12 @@ module type S = sig
val get_initial_state: kernel_function -> t or_bottom
val get_initial_state_by_callstack:
?selection:callstack list ->
- kernel_function -> t Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ kernel_function -> t Value_types.Callstack.Hashtbl.t or_top_bottom
val get_stmt_state: after:bool -> stmt -> t or_bottom
val get_stmt_state_by_callstack:
?selection:callstack list ->
- after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_bottom
val mark_as_computed: unit -> unit
val is_computed: unit -> bool
diff --git a/src/plugins/value/domains/domain_store.mli b/src/plugins/value/domains/domain_store.mli
index 97260867803e6f922f12c44d2bf2853dff4d67f4..e4d70dce5e61b1fbaf5cbb3e98f006153d557bc2 100644
--- a/src/plugins/value/domains/domain_store.mli
+++ b/src/plugins/value/domains/domain_store.mli
@@ -49,12 +49,12 @@ module type S = sig
val get_initial_state: kernel_function -> t or_bottom
val get_initial_state_by_callstack:
?selection:callstack list ->
- kernel_function -> t Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ kernel_function -> t Value_types.Callstack.Hashtbl.t or_top_bottom
val get_stmt_state: after:bool -> stmt -> t or_bottom
val get_stmt_state_by_callstack:
?selection:callstack list ->
- after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_bottom
val mark_as_computed: unit -> unit
val is_computed: unit -> bool
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 27188a34302751add35377747f6ad6027edb0f48..7a91a6af3f8e2dc22c04e88287d12316f2853dd0 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -108,7 +108,7 @@ module G = struct
let join = lift Integer.min Integer.max
let add = lift Integer.add Integer.add
- let narrow (min1, max1: t) (min2, max2: t) : t Bottom.or_bottom =
+ let narrow (min1, max1: t) (min2, max2: t) : t or_bottom =
let minb = match min1, min2 with
| Some i1, Some i2 -> Some (Integer.max i1 i2)
| None, i | i, None -> i
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 6341124d00598a7fec90ff64b3811920abe18d20..52e14219be6b7f3d87404deb6e778f55890cc0a2 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -30,6 +30,7 @@ module OCamlGraph = Graph
module Frama_c_File = File
open Cil_types
open Cil_datatype
+open Lattice_bounds
module Node : sig
include Datatype.S_with_collections
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 25fabab93298489eec675318ab166eaca0afa0dd..ca4771584258e22ee4118a368c3cbd5e4366acf8 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -38,12 +38,12 @@ module type Results = sig
val get_stmt_state : after:bool -> stmt -> state or_bottom
val get_stmt_state_by_callstack:
?selection:callstack list ->
- after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_bottom
val get_initial_state:
kernel_function -> state or_bottom
val get_initial_state_by_callstack:
?selection:callstack list ->
- kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_bottom
val eval_expr : state -> exp -> value evaluated
val copy_lvalue: state -> lval -> value flagged_value evaluated
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 92dfdb74955a4ac80169393ca2738ec52269ad2e..510972db9184b41e85601f6ef1c11cb2f390482c 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -32,12 +32,12 @@ module type Results = sig
val get_stmt_state : after:bool -> stmt -> state or_bottom
val get_stmt_state_by_callstack:
?selection:callstack list ->
- after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_bottom
val get_initial_state:
kernel_function -> state or_bottom
val get_initial_state_by_callstack:
?selection:callstack list ->
- kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_bottom
val eval_expr : state -> exp -> value evaluated
val copy_lvalue: state -> lval -> value flagged_value evaluated
diff --git a/src/plugins/value/engine/initialization.mli b/src/plugins/value/engine/initialization.mli
index 3aa3687606e2a9d575bbd24bc00832f97dbdb3ce..cef8e46011c16f8e0bc83ebe4f0f6ccda44a999f 100644
--- a/src/plugins/value/engine/initialization.mli
+++ b/src/plugins/value/engine/initialization.mli
@@ -23,7 +23,7 @@
(** Creation of the initial state of abstract domain. *)
open Cil_types
-open Bottom.Type
+open Lattice_bounds
module type S = sig
type state
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index e728a44c4444f1673af2e72bda889435fdf25643..d9d50612ebb06d92a81cf5218fdffdb626428c9e 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -22,7 +22,8 @@
open Cil_types
open Interpreted_automata
-open Bottom.Type
+open Lattice_bounds
+open Bottom.Operators
let check_signals, signal_abort =
let signal_emitted = ref false in
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index dcc295fcd5bb4ef154823a35e86800bd23a7eb0d..8e3c04f6d31f20deb9bbaf4aa09966db3482974d 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -272,7 +272,7 @@ module Make (Abstract: Abstractions.Eva) = struct
in
if is_ret then assert (Alarmset.is_empty alarms);
Alarmset.emit kinstr alarms;
- eval >>- fun (assigned, valuation) ->
+ let* assigned, valuation = eval in
let domain_valuation = Eval.to_domain_valuation valuation in
let lvalue = { lval; ltyp; lloc } in
Domain.assign kinstr lvalue expr assigned domain_valuation state
@@ -289,7 +289,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let eval, alarms = Eval.reduce state expr positive in
(* TODO: check not comparable. *)
Alarmset.emit (Kstmt stmt) alarms;
- eval >>- fun valuation ->
+ let* valuation = eval in
Domain.assume stmt expr positive (Eval.to_domain_valuation valuation) state
@@ -394,7 +394,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let safe_arguments = filter_safe_arguments valuation call in
let empty = Eval.Valuation.empty in
let reduce_one_argument acc argument =
- acc >>- fun acc ->
+ let* acc = acc in
let pre_value = match argument.avalue with
| Assign pre_value -> `Value pre_value
| Copy (_lv, pre_value) -> pre_value.v
@@ -407,8 +407,8 @@ module Make (Abstract: Abstractions.Eva) = struct
If the call has copied the argument, it may be uninitialized. Thus,
we also avoid the backward propagation if the formal is uninitialized
here. This should not happen in the Assign case above. *)
- fst (Eval.copy_lvalue ~valuation:empty ~subdivnb:0 state lval)
- >>- fun (_valuation, post_value) ->
+ let* _valuation, post_value =
+ fst (Eval.copy_lvalue ~valuation:empty ~subdivnb:0 state lval) in
if
Bottom.is_included Value.is_included pre_value post_value.v
|| post_value.escaping || not post_value.initialized
@@ -423,10 +423,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let reduce_arguments reductions state =
let valuation = `Value Eval.Valuation.empty in
let reduce_one_argument valuation (argument, post_value) =
- valuation >>- fun valuation ->
+ let* valuation = valuation in
Eval.assume ~valuation state argument.concrete post_value
in
- List.fold_left reduce_one_argument valuation reductions >>- fun valuation ->
+ let* valuation = List.fold_left reduce_one_argument valuation reductions in
Domain.update (Eval.to_domain_valuation valuation) state
(* -------------------- Treat the results of a call ----------------------- *)
@@ -441,8 +441,8 @@ module Make (Abstract: Abstractions.Eva) = struct
| Some _, None -> assert false
| Some lval, Some vi_ret ->
let exp_ret_caller = Eva_utils.lval_to_exp (Var vi_ret, NoOffset) in
- assign_ret state (Kstmt stmt) lval exp_ret_caller
- >>-: fun state -> Domain.leave_scope kf_callee [vi_ret] state
+ let+ state = assign_ret state (Kstmt stmt) lval exp_ret_caller in
+ Domain.leave_scope kf_callee [vi_ret] state
(* ---------------------- Make a one function call ------------------------ *)
@@ -475,16 +475,15 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Gathers the possible reductions on the value of the concrete arguments
at the call site, according to the value of the formals at the post
state of the called function. *)
- gather_reduced_arguments call valuation state
- >>- fun reductions ->
+ let* reductions = gather_reduced_arguments call valuation state in
(* The formals (and the locals) of the called function leave scope. *)
let post = Domain.leave_scope kf_callee leaving_vars state in
let recursion = Option.map Recursion.revert recursion in
(* Computes the state after the call, from the post state at the end of
the called function, and the pre state at the call site. *)
- Domain.finalize_call stmt call recursion ~pre ~post >>- fun state ->
+ let* state = Domain.finalize_call stmt call recursion ~pre ~post in
(* Backward propagates the [reductions] on the concrete arguments. *)
- reduce_arguments reductions state >>- fun state ->
+ let* state = reduce_arguments reductions state in
treat_return ~kf_callee lv call.return stmt state
in
let states =
@@ -640,8 +639,8 @@ module Make (Abstract: Abstractions.Eva) = struct
fun fmt subdivnb lval state ->
try
let offsm =
- fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval)
- >>- fun (_, loc, _) ->
+ let* (_, loc, _) =
+ fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval) in
Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
in
let typ = Cil.typeOfLval lval in
@@ -748,7 +747,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Alarmset.emit ki_call alarms;
let cacheable = ref Cacheable in
let eval =
- functions >>-: fun functions ->
+ let+ functions = functions in
let current_kf = Eva_utils.current_kf () in
let process_one_function kf valuation =
(* The special Frama_C_ functions to print states are handled here. *)
@@ -761,7 +760,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let eval, alarms = make_call ~subdivnb kf args valuation state in
Alarmset.emit ki_call alarms;
let states =
- eval >>-: fun (call, recursion, valuation) ->
+ let+ call, recursion, valuation = eval in
(* Register the call. *)
Eva_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
(* Do the call. *)
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 24ec7fe01dffd408fcba0df899feca82fe44891b..c59224b89441c60ae40a58ebccd11d2990879a3d 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -28,10 +28,9 @@ open Cil_types
(** {2 Lattice structure } *)
(* -------------------------------------------------------------------------- *)
-include Bottom.Type
+include Lattice_bounds
+include Bottom.Operators
-type 'a or_top = [ `Value of 'a | `Top ]
-type 'a or_top_or_bottom = [ `Value of 'a | `Top | `Bottom ]
(* -------------------------------------------------------------------------- *)
(** {2 Types for the evaluations } *)
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index f1220412daae8394c2042f5b4dbc1353220f8a89..76f96cf20bc10c0f141cb2ac03e1448bd620c1b8 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -31,13 +31,8 @@ open Cil_types
(** {2 Lattice structure } *)
(* -------------------------------------------------------------------------- *)
-include module type of Bottom.Type
-
-(** For some functions, the special value top (denoting no information)
- is managed separately. *)
-type 'a or_top = [ `Value of 'a | `Top ]
-
-type 'a or_top_or_bottom = [ `Value of 'a | `Top | `Bottom ]
+include module type of Lattice_bounds
+include module type of Bottom.Operators
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index c97449d1778ea9b41e420a52dff7b64f476b9649..05ca7822f598f6266d533fc24a0ec3495b52da7a 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -22,6 +22,7 @@
open Cil_types
open Gui_types
+open Lattice_bounds
let results_kf_computed kf =
Analysis.is_computed () &&
@@ -107,7 +108,7 @@ module type S = sig
val lval_as_offsm_ev: (Analysis.Dom.t, lval, gui_offsetmap_res) evaluation_functions
val lval_zone_ev: (Analysis.Dom.t, lval, Locations.Zone.t) evaluation_functions
val null_ev: (Analysis.Dom.t, unit, gui_offsetmap_res) evaluation_functions
- val exp_ev: (Analysis.Dom.t, exp, Analysis.Val.t Bottom.or_bottom) evaluation_functions
+ val exp_ev: (Analysis.Dom.t, exp, Analysis.Val.t or_bottom) evaluation_functions
val lval_ev: (Analysis.Dom.t, lval, Analysis.Val.t Eval.flagged_value) evaluation_functions
val tlval_ev:
@@ -116,20 +117,20 @@ module type S = sig
gui_loc -> (Eval_terms.eval_env, term, Locations.Zone.t) evaluation_functions
val term_ev:
gui_loc ->
- (Eval_terms.eval_env, term, Analysis.Val.t Bottom.or_bottom) evaluation_functions
+ (Eval_terms.eval_env, term, Analysis.Val.t or_bottom) evaluation_functions
val predicate_ev:
gui_loc ->
(Eval_terms.eval_env,
predicate,
- Eval_terms.predicate_status Bottom.or_bottom
+ Eval_terms.predicate_status or_bottom
) evaluation_functions
val predicate_with_red:
gui_loc ->
(Eval_terms.eval_env * (kinstr * Value_types.callstack),
Red_statuses.alarm_or_property * predicate,
- Eval_terms.predicate_status Bottom.or_bottom
+ Eval_terms.predicate_status or_bottom
) evaluation_functions
@@ -357,8 +358,8 @@ module Make (X: Analysis.S) = struct
(* Maps from callstacks to Value states before and after a GUI location.
The 'after' map is not always available. *)
type states_by_callstack = {
- states_before: X.Dom.t Value_types.Callstack.Hashtbl.t Eval.or_top_or_bottom;
- states_after: X.Dom.t Value_types.Callstack.Hashtbl.t Eval.or_top_or_bottom;
+ states_before: X.Dom.t Value_types.Callstack.Hashtbl.t or_top_bottom;
+ states_after: X.Dom.t Value_types.Callstack.Hashtbl.t or_top_bottom;
}
let top_states_by_callstacks = { states_before = `Top; states_after = `Top }
diff --git a/src/plugins/value/gui_files/gui_eval.mli b/src/plugins/value/gui_files/gui_eval.mli
index 9b2686313a76f88cc70636ac761f18c253b299fd..8ee4a20c0c50d5a36d3a2f032aa980a39e5d8cf7 100644
--- a/src/plugins/value/gui_files/gui_eval.mli
+++ b/src/plugins/value/gui_files/gui_eval.mli
@@ -79,7 +79,7 @@ module type S = sig
(Analysis.Dom.t, unit, gui_offsetmap_res) evaluation_functions
val exp_ev:
- (Analysis.Dom.t, exp, Analysis.Val.t Bottom.or_bottom) evaluation_functions
+ (Analysis.Dom.t, exp, Analysis.Val.t Lattice_bounds.or_bottom) evaluation_functions
val lval_ev:
(Analysis.Dom.t, lval, Analysis.Val.t Eval.flagged_value) evaluation_functions
@@ -97,20 +97,20 @@ module type S = sig
val term_ev:
gui_loc ->
- (Eval_terms.eval_env, term, Analysis.Val.t Bottom.or_bottom) evaluation_functions
+ (Eval_terms.eval_env, term, Analysis.Val.t Lattice_bounds.or_bottom) evaluation_functions
val predicate_ev:
gui_loc ->
(Eval_terms.eval_env,
predicate,
- Eval_terms.predicate_status Bottom.or_bottom
+ Eval_terms.predicate_status Lattice_bounds.or_bottom
) evaluation_functions
val predicate_with_red:
gui_loc ->
(Eval_terms.eval_env * (kinstr * Value_types.callstack),
Red_statuses.alarm_or_property * predicate,
- Eval_terms.predicate_status Bottom.or_bottom
+ Eval_terms.predicate_status Lattice_bounds.or_bottom
) evaluation_functions
val make_data_all_callstacks:
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index dc71060c5f2182ada0acb15ebdbb0cbd789654c0..8c83557fd2a766d1dde996152ae20a256e009ece 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -22,6 +22,7 @@
open Cil_types
open Eval_terms
+open Lattice_bounds
let has_requires spec =
let behav_has_requires b = b.b_requires <> [] in
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 439c086ede5ca6e4061fc8e24cd76528efb0d559..8168a495b7df1f845cbfc59216cdd068bb68ea99 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -24,6 +24,7 @@ open Cvalue
open Cil_types
open Abstract_interp
+open Lattice_bounds
let offsetmap_of_v ~typ v =
let size = Int.of_int (Cil.bitsSizeOf typ) in
diff --git a/src/plugins/value/legacy/function_args.ml b/src/plugins/value/legacy/function_args.ml
index 30b612bb2d4de720e67d7f65ae1c750aa65b239b..876450c09b1f91f7154d6289cde1a2bc51ca0988 100644
--- a/src/plugins/value/legacy/function_args.ml
+++ b/src/plugins/value/legacy/function_args.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Lattice_bounds
exception Actual_is_bottom
exception WrongFunctionType (* at a call through a pointer *)
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index f06b5022fa1ba45f47947b5aa225f2424fb8441b..b1c1c6f7e2444d0c53b2ea3cd6f2f3b7e1c0d8b3 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -20,7 +20,8 @@
(* *)
(**************************************************************************)
-open Bottom.Type
+open Lattice_bounds
+open Bottom.Operators
(* --- Split monitors --- *)
@@ -411,7 +412,7 @@ struct
let build i acc =
let value = Abstract.Val.inject_int (Cil.typeOf exp) i in
let state =
- Abstract.Eval.assume ~valuation state exp value >>- fun valuation ->
+ let* valuation = Abstract.Eval.assume ~valuation state exp value in
(* Check the reduction *)
Abstract.Dom.update (Abstract.Eval.to_domain_valuation valuation) state
in
@@ -471,8 +472,8 @@ struct
in
let source = fst (predicate.Cil_types.pred_loc) in
let aux positive =
- Abstract.Dom.reduce_by_predicate env state predicate positive
- >>-: fun state' ->
+ let+ state' =
+ Abstract.Dom.reduce_by_predicate env state predicate positive in
let x = Abstract.Dom.evaluate_predicate env state' predicate in
if x == Unknown
then
@@ -482,7 +483,7 @@ struct
let value = if positive then Integer.one else Integer.zero in
value, state'
in
- Bottom.all [ aux true; aux false ]
+ Bottom.list_values [ aux true; aux false ]
(* --- Applying partitioning actions onto flows --------------------------- *)
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index e1cc4261b38c25a272a04e2733484fc60dc67d2d..14df177983377e98e48733c679bbab5c6ea77a07 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Bottom.Type
open Partition
module Make
@@ -115,7 +114,7 @@ struct
let expanded (s : store) : (key * state) list =
Partition.to_list s.store_partition
- let smashed (s : store) : state or_bottom =
+ let smashed (s : store) : state Lattice_bounds.or_bottom =
match expanded s with
| [] -> `Bottom
| (_k, v1) :: l -> `Value (List.fold_left Domain.join v1 (List.map snd l))
diff --git a/src/plugins/value/partitioning/trace_partitioning.mli b/src/plugins/value/partitioning/trace_partitioning.mli
index c4d4d76cd11713c881842c50b387094a43874314..a21dc1af6723be80131a88ac289a7c8dbf00c3c9 100644
--- a/src/plugins/value/partitioning/trace_partitioning.mli
+++ b/src/plugins/value/partitioning/trace_partitioning.mli
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-open Bottom.Type
-
module Make
(Abstract : Abstractions.Eva)
(Kf : sig val kf: Cil_types.kernel_function end) :
@@ -59,7 +57,7 @@ sig
(* --- Accessors --- *)
val expanded : store -> (Partition.key * state) list
- val smashed : store -> state or_bottom
+ val smashed : store -> state Lattice_bounds.or_bottom
val contents : flow -> state list
val is_empty_store : store -> bool
val is_empty_flow : flow -> bool
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index 4fe15353218c9fdb8c59b69eb3dd9c2474c61dad..1b5be7c02b3367f62d1077fdaf654a2e5ce0cff3 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -89,6 +89,6 @@ module Domain = struct
val get_cvalue: (t -> Cvalue.Model.t) option
val get_cvalue_or_top: t -> Cvalue.Model.t
- val get_cvalue_or_bottom: t Bottom.or_bottom -> Cvalue.Model.t
+ val get_cvalue_or_bottom: t Lattice_bounds.or_bottom -> Cvalue.Model.t
end
end
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 6ef4a4e9132c93783c5756dffb51acef1b6b8b46..087cae69ffcb7aed9c473009cd4b25e244b5a41c 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -113,6 +113,6 @@ module Domain : sig
(** Special accessors for the main cvalue domain. *)
val get_cvalue: (t -> Cvalue.Model.t) option
val get_cvalue_or_top: t -> Cvalue.Model.t
- val get_cvalue_or_bottom: t Bottom.or_bottom -> Cvalue.Model.t
+ val get_cvalue_or_bottom: t Lattice_bounds.or_bottom -> Cvalue.Model.t
end
end
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 25e8a8c1001b93eacfccdd75029beba110a02e30..34883ace8adb8f69fb01045657630c21715090d6 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -20,14 +20,7 @@
(* *)
(**************************************************************************)
-open Bottom.Type
-
-type 'a or_top_bottom = 'a Bottom.Top.or_top_bottom
-
-let (>>>-:) t f = match t with
- | `Top -> `Top
- | `Bottom -> `Bottom
- | `Value t -> `Value (f t)
+open Lattice_bounds
module Callstack = Value_types.Callstack
@@ -174,13 +167,15 @@ struct
let map_join : type c.
('a -> 'b) -> ('b -> 'b -> 'b) -> ('a, c) t -> 'b or_top_bottom =
fun map join ->
- let map' x = `Value (map x) in
- map_reduce default map' (Bottom.Top.join join)
+ let map' x = `Value (map x)
+ and join' = TopBottom.join (fun x y -> `Value (join x y)) in
+ map_reduce default map' join'
- let map_join' : type c. ('a -> 'b or_top_bottom) -> ('b -> 'b -> 'b) ->
+ let map_join' : type c. ('a -> [< 'b or_top_bottom]) -> ('b -> 'b -> 'b) ->
('a, c) t -> 'b or_top_bottom =
fun map join ->
- map_reduce default map (Bottom.Top.join join)
+ let join' = TopBottom.join (fun x y -> `Value (join x y)) in
+ map_reduce default map join'
end
@@ -191,6 +186,8 @@ type address
module Make () =
struct
+ open TopBottom.Operators
+
module A = (val Analysis.current_analyzer ())
module EvalTypes =
@@ -307,7 +304,7 @@ struct
let join = (@)
and extract state =
let r,_alarms = A.Eval.eval_function_exp exp state in
- r >>>-: List.map fst
+ r >>-: List.map fst
in
get req |> Response.map_join' extract join |> convert |>
Result.map (List.sort_uniq Kernel_function.compare)
@@ -320,11 +317,11 @@ struct
| None -> `Top
| Some get ->
let make_expr (x, _alarms) =
- x >>>-: 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 >>>-: fun (_valuation, v) ->
+ let+ _valuation, v = x in
let Eval.{ v; initialized; escaping } = v in
let v =
match v with
@@ -340,6 +337,7 @@ struct
let extract_value :
type c. (value, c) evaluation -> (A.Val.t or_bottom, c) Response.t =
+ let open Bottom.Operators in
function
| LValue r ->
let extract (x, _alarms) = x >>- (fun (_valuation,fv) -> fv.Eval.v) in
@@ -355,7 +353,7 @@ struct
| Some get ->
let join = Main_values.CVal.join in
let extract value =
- value >>>-: get
+ value >>-: get
in
extract_value res |> Response.map_join' extract join |> convert
@@ -364,7 +362,10 @@ struct
(A.Loc.location or_bottom, c) Response.t * Locations.access =
function
| Address (r, access) ->
- let extract (x, _alarms) = x >>-: (fun (_valuation,loc,_typ) -> loc) in
+ let extract (x, _alarms) =
+ let open Bottom.Operators in
+ let+ _valuation,loc,_typ = x in loc
+ in
Response.map extract r, access
let as_location res =
@@ -379,7 +380,7 @@ struct
assert (Int_Base.equal loc2.size size);
make_loc loc size
and extract loc =
- loc >>>-: get >>>-: Precise_locs.imprecise_location
+ loc >>-: get >>-: Precise_locs.imprecise_location
in
extract_loc res |> fst |> Response.map_join' extract join |> convert
@@ -391,7 +392,8 @@ struct
let response_loc, access = extract_loc res in
let join = Locations.Zone.join
and extract loc =
- loc >>>-: get >>>-: Precise_locs.enumerate_valid_bits access
+ loc >>-: get >>-:
+ Precise_locs.enumerate_valid_bits access
in
response_loc |> Response.map_join' extract join |> convert
@@ -400,7 +402,7 @@ struct
| LValue r ->
let join = (&&)
and extract (x, _alarms) =
- x >>>-: (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
diff --git a/src/plugins/value/utils/unit_tests.ml b/src/plugins/value/utils/unit_tests.ml
index 78f38064bd355e254d02e8a9b39fe6a24173fdac..bfa09e7c518d259f23e17d5da0c5b3a5a057356c 100644
--- a/src/plugins/value/utils/unit_tests.ml
+++ b/src/plugins/value/utils/unit_tests.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Lattice_bounds
(* If true, prints each operation performed for the tests. Otherwise, only
prints wrong operations. *)
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index b1a91b8758b3ce1425776f7ae3cec963bcca1c49..550be0376e2a9b0f0a7ad39175b9e3de699d1ad9 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -23,6 +23,7 @@
open Cvalue
open Cil_types
open Abstract_value
+open Lattice_bounds
(* --------------------------------------------------------------------------
Comparison
diff --git a/src/plugins/value/values/numerors/numerors_interval.ml b/src/plugins/value/values/numerors/numerors_interval.ml
index ded1e62a5ae622753371d86bda765221ad9f8ca4..9858daa14af736aab130686424b9fd01bd78bf9e 100644
--- a/src/plugins/value/values/numerors/numerors_interval.ml
+++ b/src/plugins/value/values/numerors/numerors_interval.ml
@@ -462,7 +462,7 @@ let backward_op (op : operator) fnan ?(prec = Precisions.Real) value result () =
let x = op ~rnd:Rounding.Near ~prec xres yval in
let y = op ~rnd:Rounding.Near ~prec yres xval in
`Value (make ~nan:false x y)
- in Bottom.join join reduced_for_nan reduced_for_finite
+ in Lattice_bounds.Bottom.join join reduced_for_nan reduced_for_finite
[@@inline]
let synthetize left right =
diff --git a/src/plugins/value/values/numerors/numerors_interval.mli b/src/plugins/value/values/numerors/numerors_interval.mli
index 8ec3edb9281a04cb0b8df6dbb2ae70e42841fb75..395d5c54fe829e2e1a59cd8b32a2690ac61113fe 100644
--- a/src/plugins/value/values/numerors/numerors_interval.mli
+++ b/src/plugins/value/values/numerors/numerors_interval.mli
@@ -175,17 +175,17 @@ val exp : ?prec:Precisions.t -> t -> t
(** These functions perform backward propagation on intervals using the
precision <prec> *)
-val backward_le : ?prec:Precisions.t -> t -> t -> t Bottom.or_bottom
-val backward_lt : ?prec:Precisions.t -> t -> t -> t Bottom.or_bottom
-val backward_ge : ?prec:Precisions.t -> t -> t -> t Bottom.or_bottom
-val backward_gt : ?prec:Precisions.t -> t -> t -> t Bottom.or_bottom
+val backward_le : ?prec:Precisions.t -> t -> t -> t Lattice_bounds.or_bottom
+val backward_lt : ?prec:Precisions.t -> t -> t -> t Lattice_bounds.or_bottom
+val backward_ge : ?prec:Precisions.t -> t -> t -> t Lattice_bounds.or_bottom
+val backward_gt : ?prec:Precisions.t -> t -> t -> t Lattice_bounds.or_bottom
(** These functions perform backward propagation for arithmetic *)
val backward_add : ?prec:Precisions.t -> left:t -> right:t ->
- result:t -> unit -> (t * t) Bottom.or_bottom
+ result:t -> unit -> (t * t) Lattice_bounds.or_bottom
val backward_sub : ?prec:Precisions.t -> left:t -> right:t ->
- result:t -> unit -> (t * t) Bottom.or_bottom
+ result:t -> unit -> (t * t) Lattice_bounds.or_bottom
val backward_mul : ?prec:Precisions.t -> left:t -> right:t ->
- result:t -> unit -> (t * t) Bottom.or_bottom
+ result:t -> unit -> (t * t) Lattice_bounds.or_bottom
val backward_div : ?prec:Precisions.t -> left:t -> right:t ->
- result:t -> unit -> (t * t) Bottom.or_bottom
+ result:t -> unit -> (t * t) Lattice_bounds.or_bottom
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 6a236513097a604c4fe7822cde08b948cc6370c5..61fc238db742832bc5ad2a2a42e13f2acd0cfbb8 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -259,7 +259,7 @@ module V = struct
(** Comparisons *)
- open Bottom.Type
+ open Lattice_bounds.Bottom.Operators
let backward_mult_int_left ~right ~result =
try
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index 4573934e9929fa74a5a135571d8077c983a0f15e..06768eed07afa94a17c98874bd19959a3aeb5cec 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -81,7 +81,7 @@ module V : sig
val of_char : char -> t
val of_int64: int64 -> t
- val backward_mult_int_left: right:t -> result:t -> t option Bottom.or_bottom
+ val backward_mult_int_left: right:t -> result:t -> t option Lattice_bounds.or_bottom
val backward_comp_int_left: Comp.t -> t -> t -> t
val backward_comp_float_left_true: Comp.t -> Fval.kind -> t -> t -> t
@@ -241,15 +241,15 @@ module V_Offsetmap: sig
with type v = V_Or_Uninitialized.t
and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
- val narrow: t -> t -> t Bottom.Type.or_bottom
- val narrow_reinterpret: t -> t -> t Bottom.Type.or_bottom
+ val narrow: t -> t -> t Lattice_bounds.or_bottom
+ val narrow_reinterpret: t -> t -> t Lattice_bounds.or_bottom
(** See the corresponding functions in {!Offsetmap_sig}. *)
end
(** Values bound by default to a variable. *)
module Default_offsetmap: sig
- val default_offsetmap : Base.t -> V_Offsetmap.t Bottom.or_bottom
+ val default_offsetmap : Base.t -> V_Offsetmap.t Lattice_bounds.or_bottom
end
(** Memories. They are maps from bases to memory slices *)
diff --git a/tests/builtins/oracle/allocated.0.res.oracle b/tests/builtins/oracle/allocated.0.res.oracle
index 78bb3d8a95aaf2d0c061cd1d62396def409a63f0..25fe2055044456adf9034cd035c16e7f9f692ce9 100644
--- a/tests/builtins/oracle/allocated.0.res.oracle
+++ b/tests/builtins/oracle/allocated.0.res.oracle
@@ -16,7 +16,7 @@
[eva] allocated.c:31: Call to builtin free
[eva] allocated.c:31: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:31: strong free on bases: {__malloc_main_l25}
-[eva] allocated.c:32: Frama_C_show_each_p_after_free: Bottom
+[eva] allocated.c:32: Frama_C_show_each_p_after_free: ⊥
[eva] allocated.c:36: Call to builtin malloc
[eva] allocated.c:36: allocating variable __malloc_main_l36
[eva] allocated.c:36: assertion got status valid.
@@ -149,7 +149,7 @@
[eva] allocated.c:120: Call to builtin malloc
[eva] allocated.c:120: allocating variable __malloc_main_l120
[eva] allocated.c:120: Frama_C_show_each: {{ &__malloc_main_l120 }}
-[eva] allocated.c:123: Frama_C_show_each: Bottom
+[eva] allocated.c:123: Frama_C_show_each: ⊥
[eva] allocated.c:125: Call to builtin free
[eva] allocated.c:125: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:125: strong free on bases: {__malloc_main_l120}
diff --git a/tests/builtins/oracle/allocated.1.res.oracle b/tests/builtins/oracle/allocated.1.res.oracle
index ebfce7b0022a825db7b9d5c25a7faa4881e77c96..a944c57c4e6c64a80c7f9f266b7ee9c6ba157289 100644
--- a/tests/builtins/oracle/allocated.1.res.oracle
+++ b/tests/builtins/oracle/allocated.1.res.oracle
@@ -16,7 +16,7 @@
[eva] allocated.c:31: Call to builtin free
[eva] allocated.c:31: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:31: strong free on bases: {__malloc_main_l25}
-[eva] allocated.c:32: Frama_C_show_each_p_after_free: Bottom
+[eva] allocated.c:32: Frama_C_show_each_p_after_free: ⊥
[eva] allocated.c:36: Call to builtin malloc
[eva] allocated.c:36: allocating variable __malloc_main_l36
[eva] allocated.c:36: assertion got status valid.
@@ -636,7 +636,7 @@
[eva] allocated.c:120: Call to builtin malloc
[eva] allocated.c:120: allocating variable __malloc_main_l120
[eva] allocated.c:120: Frama_C_show_each: {{ &__malloc_main_l120 }}
-[eva] allocated.c:123: Frama_C_show_each: Bottom
+[eva] allocated.c:123: Frama_C_show_each: ⊥
[eva] allocated.c:125: Call to builtin free
[eva] allocated.c:125: function free: precondition 'freeable' got status valid.
[eva:malloc] allocated.c:125: strong free on bases: {__malloc_main_l120}
diff --git a/tests/float/oracle/conv.res.oracle b/tests/float/oracle/conv.res.oracle
index daa38ec7a842f43d823967175d5234eb55af4312..dea66da8e28d30a16b7a97441834f0ffc96b50ff 100644
--- a/tests/float/oracle/conv.res.oracle
+++ b/tests/float/oracle/conv.res.oracle
@@ -38,16 +38,16 @@
[eva] conv.i:69: Frama_C_show_each: [4.94065645841e-322 .. 9.22442153475e+159]
[eva] conv.i:73: Frama_C_show_each: {1.79769313486e+308}
[eva] conv.i:74: assertion got status valid.
-[eva] conv.i:77: Frama_C_show_each: Bottom
-[eva] conv.i:80: Frama_C_show_each: Bottom
+[eva] conv.i:77: Frama_C_show_each: ⊥
+[eva] conv.i:80: Frama_C_show_each: ⊥
[eva] conv.i:84: Frama_C_show_each: {-1.79769313486e+308}
[eva] conv.i:85: assertion got status valid.
-[eva] conv.i:88: Frama_C_show_each: Bottom
+[eva] conv.i:88: Frama_C_show_each: ⊥
[eva] conv.i:91: Frama_C_show_each: [0. .. 4.94065645841e-324]
[eva:alarm] conv.i:94: Warning: assertion got status unknown.
-[eva] conv.i:95: Frama_C_show_each: Bottom
+[eva] conv.i:95: Frama_C_show_each: ⊥
[eva] conv.i:98: Frama_C_show_each: {0}
-[eva] conv.i:101: Frama_C_show_each: Bottom
+[eva] conv.i:101: Frama_C_show_each: ⊥
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index 55c450297df40885a409f0f701b45ffd30284441..a9944c463d097f25c3d87b231526dd26e7f0ce46 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -76,8 +76,7 @@
[eva] partitioning-annots.c:100: Frama_C_show_each_split_with_uninit: {2}, {2}
[eva] partitioning-annots.c:100: Frama_C_show_each_split_with_uninit: {1}, {1}
[eva] partitioning-annots.c:100: Frama_C_show_each_split_with_uninit: {0}, {0}
-[eva] partitioning-annots.c:100:
- Frama_C_show_each_split_with_uninit: Bottom, Bottom
+[eva] partitioning-annots.c:100: Frama_C_show_each_split_with_uninit: ⊥, ⊥
[eva] partitioning-annots.c:102: Frama_C_show_each_no_split: {0}, {0; 1; 2}
[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
Called from partitioning-annots.c:103.