From 501b9bd40ea396a099e70fad5a4924e07e10d518 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 Oct 2021 10:04:59 +0200
Subject: [PATCH] [Eva] Adds function [call_return] to trace_partitioning.ml
Called from the iterator; removes [call_return_policy] from iterator.ml.
In partition.ml, renames [recombine] to [combine].
---
src/plugins/value/engine/iterator.ml | 8 +++-----
src/plugins/value/partitioning/partition.ml | 2 +-
src/plugins/value/partitioning/partition.mli | 4 ++--
src/plugins/value/partitioning/trace_partitioning.ml | 4 ++++
src/plugins/value/partitioning/trace_partitioning.mli | 6 ++++++
5 files changed, 16 insertions(+), 8 deletions(-)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 31bf7543394..773be0b00ab 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -88,10 +88,9 @@ module Make_Dataflow
(* Ideally, the slevel parameter should not be used anymore in this file
but it is still required for logic interpretation *)
- let slevel, call_return_policy =
+ let slevel =
let module P = Partitioning_parameters.Make (AnalysisParam) in
- P.slevel,
- P.call_return_policy
+ P.slevel
(* --- Abstract values storage --- *)
@@ -282,8 +281,7 @@ module Make_Dataflow
(* Propagate info that the current call cannot be cached either *)
cacheable := Eval.NoCacheCallers;
(* Recombine callee partitioning keys with caller key *)
- let recombine = Partition.Key.recombine ~policy:call_return_policy in
- List.map (fun (k, s) -> recombine ~caller:key ~callee:k, s) result
+ Partitioning.call_return ~caller:key result
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 7ff3a9f7843..91f40d87ad3 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -247,7 +247,7 @@ struct
let exceed_rationing key = key.ration_stamp = None
- let recombine ~policy ~caller ~callee =
+ let combine ~policy ~caller ~callee =
let keep_second _ v1 v2 =
match v1, v2 with
| None, None -> None
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index 7ef819e2a77..8ac9926955e 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -52,8 +52,8 @@ module Key : sig
include Datatype.S_with_collections with type t = key
val zero : t (** Initial key: no partitioning. *)
val exceed_rationing: t -> bool
- val recombine : policy:call_return_policy ->
- caller:t -> callee:t -> t (** Recombinaison of keys after a call *)
+ val combine : policy:call_return_policy -> caller:t -> callee:t -> t
+ (** Recombinaison of keys after a call *)
end
(** Collection of states, each identified by a unique key. *)
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index b07eaa7ca62..61f2b7a458f 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -175,6 +175,10 @@ struct
then apply (Restrict (return_exp, i))
else apply (Ration empty_rationing)
+ let call_return ~caller result =
+ let combine = Partition.Key.combine ~policy:call_return_policy in
+ List.map (fun (k, s) -> combine ~caller ~callee:k, s) result
+
(* Reset state (for hierchical convergence) *)
let reset_store (s : store) : unit =
diff --git a/src/plugins/value/partitioning/trace_partitioning.mli b/src/plugins/value/partitioning/trace_partitioning.mli
index 5c208d99b80..dbdd548600b 100644
--- a/src/plugins/value/partitioning/trace_partitioning.mli
+++ b/src/plugins/value/partitioning/trace_partitioning.mli
@@ -81,6 +81,12 @@ sig
val next_loop_iteration : flow -> Cil_types.stmt -> flow
val split_return : flow -> Cil_types.exp option -> flow
+ (** After the analysis of a function call, recombines callee partitioning keys
+ with the caller key. *)
+ val call_return:
+ caller:Partition.key ->
+ (Partition.key * state) list -> (Partition.key * state) list
+
(* --- Operators --- *)
(** Remove all states from the tank, leaving it empty as if it was just
--
GitLab