From b1c416b1d51ef5e3dfb4fd0eaff136438a3b2b5a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 20 Jun 2024 09:33:34 +0200
Subject: [PATCH] [kernel] Pass vertex and edge instead of edge_transition in
transfer function
---
src/kernel_services/analysis/interpreted_automata.ml | 4 ++--
src/kernel_services/analysis/interpreted_automata.mli | 10 +++++-----
tests/misc/interpreted_automata_dataflow_backward.ml | 4 ++--
tests/misc/interpreted_automata_dataflow_forward.ml | 4 ++--
4 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 4330418f551..29f82f78abe 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -1206,7 +1206,7 @@ sig
val join : t -> t -> t
val widen : t -> t -> t option (* returns None when inclusion *)
- val transfer : vertex transition -> t -> t option
+ val transfer : vertex -> vertex edge -> t -> t option
end
module type DataflowAnalysis =
@@ -1254,7 +1254,7 @@ struct
let process_edge v e acc =
(* Retrieve origin value *)
let value = States.find_opt results v in
- let result = Option.bind value (D.transfer e.edge_transition) in
+ let result = Option.bind value (D.transfer v e) in
Option.to_list result @ acc
in
diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index 9f7eb9bd812..e751f86f751 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/src/kernel_services/analysis/interpreted_automata.mli
@@ -52,9 +52,9 @@ type 'a control =
the given cases and default vertices. *)
(** Vertices are control points. When a vertice is the *start* of a statement,
- this statement is kept in vertex_stmt. Currently, this statement is kept for
- two reasons: to know when callbacks should be called and when annotations
- should be read. *)
+ this statement is kept in [vertex_start_of]. Currently, this statement is
+ kept for two reasons: to know when callbacks should be called and when
+ annotations should be read. *)
type vertex = private {
vertex_kf : Cil_types.kernel_function;
@@ -325,10 +325,10 @@ sig
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
+ (** Transfer function for edges: 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
+ val transfer : vertex -> vertex edge -> t -> t option
end
(** Simple dataflow analysis *)
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index dce5e8cfc2b..444b362690d 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -34,9 +34,9 @@ struct
| Lval (Var vi, _) -> Set.singleton vi
| Lval (Mem e, _) -> vars e
- let transfer t v =
+ let transfer _ e v =
let open Interpreted_automata in
- let r = match t with
+ let r = match e.edge_transition with
| Skip | Prop _ | Leave _ | Return (None,_) ->
v (* Nothing to do *)
| Enter b ->
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 97678ef9abb..017d2f638d0 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -83,9 +83,9 @@ struct
with Not_constant ->
Map.remove vi v
- let transfer t v =
+ let transfer _ e v =
let open Interpreted_automata in
- match t with
+ match e.edge_transition with
| Skip | Return _ | Prop _ | Enter _ | Leave _ -> Some v
| Guard (exp, kind, _) -> assume v exp kind
| Instr (Set ((Var vi, NoOffset), exp, _), _) -> Some (assign v vi exp)
--
GitLab