From 8d63ea228c7d46b7aeee4620f596293ee1dc8892 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 31 Mar 2022 17:51:42 +0200
Subject: [PATCH] [Eva] add support for Top polymorphic variant
---
Makefile | 1 +
headers/header_spec.txt | 2 +
src/kernel_services/abstract_interp/top.ml | 68 +++++++++++++++++++++
src/kernel_services/abstract_interp/top.mli | 56 +++++++++++++++++
4 files changed, 127 insertions(+)
create mode 100644 src/kernel_services/abstract_interp/top.ml
create mode 100644 src/kernel_services/abstract_interp/top.mli
diff --git a/Makefile b/Makefile
index bc1699b5bd8..bebbcfb5d81 100644
--- a/Makefile
+++ b/Makefile
@@ -587,6 +587,7 @@ KERNEL_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/top.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 45b246e8a48..ce43c75a366 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -525,6 +525,8 @@ src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli: CEA_LGP
src/kernel_services/abstract_interp/offsetmap_sig.mli: CEA_LGPL
src/kernel_services/abstract_interp/origin.ml: CEA_LGPL
src/kernel_services/abstract_interp/origin.mli: CEA_LGPL
+src/kernel_services/abstract_interp/top.ml: CEA_LGPL
+src/kernel_services/abstract_interp/top.mli: CEA_LGPL
src/kernel_services/abstract_interp/tr_offset.ml: CEA_LGPL
src/kernel_services/abstract_interp/tr_offset.mli: CEA_LGPL
src/kernel_services/analysis/README.md: .ignore
diff --git a/src/kernel_services/abstract_interp/top.ml b/src/kernel_services/abstract_interp/top.ml
new file mode 100644
index 00000000000..e9cefd2c8df
--- /dev/null
+++ b/src/kernel_services/abstract_interp/top.ml
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(* *)
+(* 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_top = [ `Value of 'a | `Top ]
+
+(** Combination *)
+
+let zip x y =
+ match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Value x, `Value y -> `Value (x,y)
+
+(** Operators *)
+
+module Type = struct
+ type 'a or_top = [ `Value of 'a | `Top ]
+
+ 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
+
+(** Conversion. *)
+
+let of_option = function
+ | None -> `Top
+ | Some x -> `Value x
+
+let to_option = function
+ | `Top -> None
+ | `Value x -> Some x
+
+(** Pretty printing. *)
+
+let pretty_top fmt =
+ Format.pp_print_string fmt (Unicode.top_string ())
+
+let pretty pp fmt = function
+ | `Top -> pretty_top fmt
+ | `Value v -> pp fmt v
diff --git a/src/kernel_services/abstract_interp/top.mli b/src/kernel_services/abstract_interp/top.mli
new file mode 100644
index 00000000000..1f9245dc8d7
--- /dev/null
+++ b/src/kernel_services/abstract_interp/top.mli
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(* *)
+(* 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 top is
+ managed separately from other values. *)
+
+module Type : sig
+ type 'a or_top = [ `Value of 'a | `Top ]
+
+ (** This monad propagates the `Bottom value if needed. *)
+ val (>>-) : 'a or_top -> ('a -> 'b or_top) -> 'b or_top
+
+ (** Use this monad if the following function returns a simple value. *)
+ val (>>-:) : 'a or_top -> ('a -> 'b) -> 'b or_top
+
+ (** Binding operators, applicative syntax *)
+ val (let+) : 'a or_top -> ('a -> 'b) -> 'b or_top
+ val (and+) : 'a or_top -> 'b or_top -> ('a * 'b) or_top
+
+ (** Binding operators, monad syntax *)
+ val (let*) : 'a or_top -> ('a -> 'b or_top) -> 'b or_top
+ val (and*) : 'a or_top -> 'b or_top -> ('a * 'b) or_top
+end
+
+type 'a or_top = 'a Type.or_top
+
+(** Combination, if one is `Top, the combination is `Top *)
+val zip : 'a or_top -> 'b or_top -> ('a * 'b) or_top
+
+(** Conversion. *)
+val to_option : 'a or_top -> 'a option
+val of_option : 'a option -> 'a or_top
+
+(** Pretty printing. *)
+val pretty_top : Format.formatter -> unit (* for %t specifier *)
+val pretty : (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a or_top -> unit
--
GitLab