From 8ef8e80a4a3676a6d4ffd3be6b337a2e2eb22a7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 21 Oct 2019 16:51:06 +0200
Subject: [PATCH] [Kernel] Interpreted_automata: comments the dataflow functor.
---
.../analysis/interpreted_automata.mli | 22 ++++++++++++++++---
tests/misc/interpreted_automata_dataflow.i | 3 +++
tests/misc/interpreted_automata_dataflow.ml | 2 +-
3 files changed, 23 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index dec17586091..e939c4cf6c4 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/src/kernel_services/analysis/interpreted_automata.mli
@@ -246,17 +246,33 @@ module UnrollUnnatural : sig
end
-(* Dataflow computation *)
+(** Dataflow computation: simple data-flow analysis using interpreted automata.
+ This is mostly intended as an example for using interpreted automata;
+ see also tests/misc/interpreted_automata_dataflow.ml for a complete example
+ using this dataflow. *)
+(** Input domain for a simple dataflow analysis. *)
module type Domain =
sig
- type t
+ type t (** States propagated by the dataflow analysis. *)
+ (** Merges two states coming from different paths. *)
val join : t -> t -> t
- val widen : t -> t -> t option (* returns None when inclusion *)
+
+ (** [widen v1 v2] must returns None if [v2] is included in [v1].
+ Otherwise, over-approximates 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.
+ Called on loop heads to ensure the analysis termination. *)
+ val widen : t -> t -> t option
+
+ (** Transfer function for transitions: computes the state after the transition
+ from the state before. Returns None if the end of the transition is not
+ reachable from the given state. *)
val transfer : vertex transition -> t -> t option
end
+(** Builds a simple dataflow analysis over an input domain. *)
module Dataflow (D : Domain) :
sig
val fixpoint : Cil_types.kernel_function -> D.t -> D.t Vertex.Hashtbl.t
diff --git a/tests/misc/interpreted_automata_dataflow.i b/tests/misc/interpreted_automata_dataflow.i
index 0dbe0d14845..9446609755e 100644
--- a/tests/misc/interpreted_automata_dataflow.i
+++ b/tests/misc/interpreted_automata_dataflow.i
@@ -2,6 +2,9 @@
OPT: -load-script tests/misc/interpreted_automata_dataflow.ml
*/
+/* Tests the dataflow functor of interpreted automata via a caml script
+ implementing a propagation of constants. */
+
void main(int x)
{
int y = 3;
diff --git a/tests/misc/interpreted_automata_dataflow.ml b/tests/misc/interpreted_automata_dataflow.ml
index b23a0a3cd8d..04843ba93f6 100644
--- a/tests/misc/interpreted_automata_dataflow.ml
+++ b/tests/misc/interpreted_automata_dataflow.ml
@@ -33,7 +33,7 @@ struct
exception Not_constant
- let rec eval v exp =
+ let rec eval v exp =
match exp.enode with
| Const (CInt64 (i,_,_)) ->
(try Integer.to_int i with _ -> raise Not_constant)
--
GitLab