From 4fe8dab8fb5e578bb38b569250f8880356d9edfe Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 9 Jul 2024 11:40:15 +0200
Subject: [PATCH] [kernel] Dataflow analyses with interpreted automata now
requires widen to return a more explicit type
---
.../analysis/interpreted_automata.ml | 8 +++++---
.../analysis/interpreted_automata.mli | 16 +++++++++++-----
.../interpreted_automata_dataflow_backward.ml | 4 ++--
.../interpreted_automata_dataflow_forward.ml | 4 ++--
4 files changed, 20 insertions(+), 12 deletions(-)
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 6e6d3de14c2..a9534ac4395 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -1213,12 +1213,14 @@ end
(* --- Dataflow computation --- *)
(* ---------------------------------------------------------------------- *)
+type 'a widening = Fixpoint | Widening of 'a
+
module type Domain =
sig
type t
val join : t -> t -> t
- val widen : t -> t -> t option (* returns None when inclusion *)
+ val widen : t -> t -> t widening
val transfer : vertex -> vertex edge -> t -> t option
end
@@ -1292,8 +1294,8 @@ struct
| None, _ -> true (* Previous was bottom *)
| Some v1, Some v2 ->
match D.widen v1 v2 with
- | None -> false (* End of iteration *)
- | Some value -> (* new value *)
+ | Fixpoint -> false (* End of iteration *)
+ | Widening value -> (* new value *)
States.replace results v value;
true
in
diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index 0fe34c38337..939a7929c58 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/src/kernel_services/analysis/interpreted_automata.mli
@@ -310,6 +310,12 @@ end
See tests/misc/interpreted_automata_dataflow.ml for a complete example
using this dataflow computation. *)
+type 'a widening =
+ | Fixpoint (** The analysis have reached a fixpoint *)
+ | Widening of 'a (** The analysis have not reached a fixpoint and must
+ continue with the provided state, widened if termination
+ requires it. *)
+
(** Input domain for a simple dataflow analysis. *)
module type Domain =
sig
@@ -321,15 +327,15 @@ sig
(** [widen v1 v2] is called on loop heads after each iteration of the
analysis on the loop body: [v1] is the previous state before the
iteration, and [v2] the new state after the iteration.
- The function must return None if the analysis has reached a fixpoint for
- the loop: this is the case if [join v1 v2] is equivalent to [v1], as a new
- iteration would have the same entry state as the last one.
+ The function must return [Fixpoint] if the analysis has reached a fixpoint
+ for the loop: this is the case if [join v1 v2] is equivalent to [v1], as a
+ new iteration would have the same entry state as the last one.
Otherwise, it must return the new entry state for the next iteration,
by over-approximating the join between [v1] and [v2] such that
any sequence of successive widenings is ultimately stationary,
- i.e. […widen (widen (widen x0 x1) x2) x3…] eventually returns None.
+ i.e. […widen (widen (widen x0 x1) x2) x3…] eventually returns [Fixpoint].
This ensures the analysis termination. *)
- val widen : t -> t -> t option
+ val widen : t -> t -> t widening
(** Transfer function for edges: computes the state after the transition
from the state before. Returns None if the end of the transition is not
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index 444b362690d..c2a29ac70d6 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -16,9 +16,9 @@ struct
let widen v1 v2 =
if Set.subset v2 v1 then
- None (* Inclusion *)
+ Interpreted_automata.Fixpoint (* Inclusion *)
else
- Some v2 (* No widening necessary *)
+ Interpreted_automata.Widening v2 (* No widening necessary *)
let rec vars exp =
match exp.enode with
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 017d2f638d0..922109a7ec9 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -25,9 +25,9 @@ struct
Map.find_opt vi v2 = Some x
in
if Map.for_all same_entry v1 then
- None (* Inclusion *)
+ Interpreted_automata.Fixpoint (* Inclusion *)
else
- Some v2 (* No widening necessary *)
+ Interpreted_automata.Widening v2 (* No widening necessary *)
exception Not_constant
--
GitLab