From 3236acfeef939a21aa01f2d95dc8b51f57b35199 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 29 May 2024 15:03:40 +0200
Subject: [PATCH] [Eva] Comments abstract contexts, and removes unused
functions.
---
src/plugins/eva/contexts/abstract_context.ml | 24 +++++++++++++++++---
src/plugins/eva/contexts/context_product.ml | 4 +---
src/plugins/eva/contexts/unit_context.ml | 4 +---
src/plugins/eva/values/abstract_value.ml | 9 ++++++++
4 files changed, 32 insertions(+), 9 deletions(-)
diff --git a/src/plugins/eva/contexts/abstract_context.ml b/src/plugins/eva/contexts/abstract_context.ml
index 19ba4b09d2e..b93d201dfe4 100644
--- a/src/plugins/eva/contexts/abstract_context.ml
+++ b/src/plugins/eva/contexts/abstract_context.ml
@@ -20,23 +20,41 @@
(* *)
(**************************************************************************)
+(** An abstract context can be used to transfer information from the state of
+ an abstract domain, in which an expression or lvalue is evaluated, to a
+ value abstraction, which interprets operations during this evaluation.
+ The context is built by the function [build_context] of abstract domains,
+ and passed as argument of most transfer functions from {!Abstract_value}. *)
+
open Eval
module type S = sig
- include Datatype.S
+ type t
+
+ (** The default context used in a top abstract state, or if no domain has been
+ enabled — or no domain providing this context. *)
val top : t
- val is_included : t -> t -> bool
- val join : t -> t -> t
+
+ (** In a product of abstract domains, merges the context provided by the
+ abstract state of each domain. *)
val narrow : t -> t -> t or_bottom
end
+(** Keys used to identify context modules. *)
type 'c key = 'c Structure.Key_Context.key
+(** Signature for a leaf module of context. *)
module type Leaf = sig
include S
+
+ (** The key identifies the module and the type [t] of context. *)
val key : t key
end
+(** Eva abstractions are divided between contexts, values, locations and domains.
+ Values and domains depend on contexts, and use this type to declare such
+ dependencies. In the standard case, a value or domain depends on a single
+ context module [Ctx] and uses [Leaf (module Ctx)] to declare this dependency. *)
type 'c dependencies =
| Leaf : (module Leaf with type t = 'c) -> 'c dependencies
| Node : 'l dependencies * 'r dependencies -> ('l * 'r) dependencies
diff --git a/src/plugins/eva/contexts/context_product.ml b/src/plugins/eva/contexts/context_product.ml
index b1478d207f6..ad934208e87 100644
--- a/src/plugins/eva/contexts/context_product.ml
+++ b/src/plugins/eva/contexts/context_product.ml
@@ -21,9 +21,7 @@
(**************************************************************************)
module Make (L : Abstract_context.S) (R : Abstract_context.S) = struct
- include Datatype.Pair (L) (R)
+ type t = L.t * R.t
let top = (L.top, R.top)
- let join (l, r) (l', r') = (L.join l l', R.join r r')
- let is_included (l, r) (l', r') = L.is_included l l' && R.is_included r r'
let narrow (l, r) (l', r') = Eval.Bottom.zip (L.narrow l l') (R.narrow r r')
end
diff --git a/src/plugins/eva/contexts/unit_context.ml b/src/plugins/eva/contexts/unit_context.ml
index d0039a3004f..86669eb7cde 100644
--- a/src/plugins/eva/contexts/unit_context.ml
+++ b/src/plugins/eva/contexts/unit_context.ml
@@ -20,9 +20,7 @@
(* *)
(**************************************************************************)
-include Datatype.Unit
+type t = unit
let top = ()
-let is_included () () = true
-let join () () = ()
let narrow () () = `Value ()
let key = Structure.Key_Context.create_key "Unit context"
diff --git a/src/plugins/eva/values/abstract_value.ml b/src/plugins/eva/values/abstract_value.ml
index ab72e136ec9..2f82d485246 100644
--- a/src/plugins/eva/values/abstract_value.ml
+++ b/src/plugins/eva/values/abstract_value.ml
@@ -46,12 +46,21 @@ type bound = Int of Integer.t | Float of float * fkind
type pointer_comparison = Equality | Relation | Subtraction
+(** Enriched context.
+ This record could easily be extended to contain more information about the
+ context in which an evaluation takes place, if the need arises. *)
type 'a enriched = { from_domains : 'a }
(** Signature of abstract numerical values. *)
module type S = sig
include Datatype.S
+ (** A numerical value abstraction can optionally require some context from
+ abstract domains. Most transfer functions take the context as argument;
+ it is provided by the abstract state in which operations are performed.
+ See {!Abstract_context} for more details about contexts.
+ For values that don't need context, this type can be defined as unit
+ and the context argument can be safely ignored. *)
type context
val pretty_typ: typ option -> t Pretty_utils.formatter
--
GitLab