From d0006075ae55bcc17e3a359094fa80393b1a379f Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 30 Sep 2021 17:19:13 +0200
Subject: [PATCH] [Eva] Parametrize interprocedural trace partitioning
---
src/plugins/value/engine/iterator.ml | 8 ++---
src/plugins/value/partitioning/partition.ml | 31 ++++++++++++++-----
src/plugins/value/partitioning/partition.mli | 11 +++++--
.../partitioning/partitioning_parameters.ml | 9 ++++++
.../partitioning/partitioning_parameters.mli | 1 +
src/plugins/value/value_parameters.ml | 20 ++++++++++++
src/plugins/value/value_parameters.mli | 2 ++
tests/value/partitioning-interproc.c | 4 +--
8 files changed, 70 insertions(+), 16 deletions(-)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 8300fb92d13..df784153c29 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -88,10 +88,10 @@ 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, history_size =
+ let slevel, call_return_policy =
let module P = Partitioning_parameters.Make (AnalysisParam) in
P.slevel,
- P.history_size
+ P.call_return_policy
(* --- Abstract values storage --- *)
@@ -282,8 +282,8 @@ 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 ~history_size in
- List.map (fun (k,s) -> recombine key k, s) result
+ let recombine = Partition.Key.recombine ~policy:call_return_policy in
+ List.map (fun (k,s) -> recombine ~caller:key ~callee:k, s) 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 49a4ef331b8..32ea6246dbd 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -161,6 +161,13 @@ type key = {
dynamic_splits : split_monitor SplitMap.t; (* term -> monitor *)
}
+type call_return_policy = {
+ policy_keep_callee_splits: bool;
+ policy_keep_callee_history: bool;
+ policy_keep_caller_history: bool;
+ policy_history_size: int;
+}
+
module Key =
struct
open Datatype
@@ -243,19 +250,27 @@ struct
let exceed_rationing key = key.ration_stamp = None
- let recombine ~history_size k1 k2 =
- let merge_split _ v1 v2 =
+ let recombine ~policy ~caller ~callee =
+ let keep_second _ v1 v2 =
match v1, v2 with
| None, None -> None
- | Some v, None | None, Some v -> Some v
- | Some _v1, Some v2 -> Some v2 (* Keep the newest split value *)
+ | Some x, None | (Some _ | None), Some x -> Some x
in {
ration_stamp = None;
- branches = Extlib.list_first_n history_size (k2.branches @ k1.branches);
- loops = k1.loops;
- splits = SplitMap.merge merge_split k1.splits k2.splits;
+ branches =
+ Extlib.list_first_n policy.policy_history_size (
+ (if policy.policy_keep_callee_history then callee.branches else []) @
+ (if policy.policy_keep_caller_history then caller.branches else [])
+ );
+ loops = caller.loops;
+ splits =
+ if policy.policy_keep_callee_splits
+ then SplitMap.merge keep_second caller.splits callee.splits
+ else caller.splits;
dynamic_splits =
- SplitMap.merge merge_split k1.dynamic_splits k2.dynamic_splits;
+ if policy.policy_keep_callee_splits
+ then SplitMap.merge keep_second caller.dynamic_splits callee.dynamic_splits
+ else caller.dynamic_splits;
}
end
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index d894e23fc84..7ef819e2a77 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -41,12 +41,19 @@
(** Partitioning keys attached to states. *)
type key
+type call_return_policy = {
+ policy_keep_callee_splits: bool;
+ policy_keep_callee_history: bool;
+ policy_keep_caller_history: bool;
+ policy_history_size: int;
+}
+
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 : history_size:int ->
- t -> t -> t (** Recombinaison of keys after a call *)
+ val recombine : 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/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 4ddcf183521..60f8b52616c 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -139,4 +139,13 @@ struct
acc (* Impossible to convert term to lval *)
in
List.fold_left map_annot [] (get_flow_annot stmt)
+
+ let call_return_policy = {
+ Partition.policy_keep_callee_splits =
+ Value_parameters.InterproceduralPartitioningKeepSplits.get ();
+ policy_keep_callee_history =
+ Value_parameters.InterproceduralPartitioningKeepHistory.get ();
+ policy_keep_caller_history = true;
+ policy_history_size = history_size;
+ }
end
diff --git a/src/plugins/value/partitioning/partitioning_parameters.mli b/src/plugins/value/partitioning/partitioning_parameters.mli
index 891a2b72b6f..636eabc5bcf 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.mli
+++ b/src/plugins/value/partitioning/partitioning_parameters.mli
@@ -31,4 +31,5 @@ module Make (Kf : sig val kf: kernel_function end) : sig
val history_size : int
val universal_splits : Partition.action list
val flow_actions : stmt -> Partition.action list
+ val call_return_policy : Partition.call_return_policy
end
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index c1a44a5949f..324cb0f02f9 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -791,6 +791,26 @@ module SplitLimit =
let () = add_precision_dep SplitLimit.parameter
let () = SplitLimit.set_range 0 max_int
+let () = Parameter_customize.set_group precision_tuning
+let () = Parameter_customize.is_invisible ()
+module InterproceduralPartitioningKeepSplits =
+ False
+ (struct
+ let option_name = "-eva-interprocedural-partitioning-keep-splits"
+ let help = "Keep partitioning splits through function returns"
+ end)
+let () = add_precision_dep InterproceduralPartitioningKeepSplits.parameter
+
+let () = Parameter_customize.set_group precision_tuning
+let () = Parameter_customize.is_invisible ()
+module InterproceduralPartitioningKeepHistory =
+ False
+ (struct
+ let option_name = "-eva-interprocedural-partitioning-keep-history"
+ let help = "Keep partitioning history through function returns"
+ end)
+let () = add_precision_dep InterproceduralPartitioningKeepHistory.parameter
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module SplitReturnFunction =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 0442dbcc0bb..dca2eb22108 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -79,6 +79,8 @@ module DefaultLoopUnroll : Parameter_sig.Int
module HistoryPartitioning : Parameter_sig.Int
module ValuePartitioning : Parameter_sig.String_set
module SplitLimit : Parameter_sig.Int
+module InterproceduralPartitioningKeepSplits : Parameter_sig.Bool
+module InterproceduralPartitioningKeepHistory : Parameter_sig.Bool
module ArrayPrecisionLevel: Parameter_sig.Int
diff --git a/tests/value/partitioning-interproc.c b/tests/value/partitioning-interproc.c
index 1b42df1bfba..7cb9dc220aa 100644
--- a/tests/value/partitioning-interproc.c
+++ b/tests/value/partitioning-interproc.c
@@ -1,7 +1,7 @@
/* run.config*
GCC:
- STDOPT: #"-main cassign_test -eva-partition-history 1"
- STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality"
+ STDOPT: #"-main cassign_test -eva-partition-history 1 -eva-interprocedural-partitioning-keep-history"
+ STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-partitioning-keep-history"
*/
#include "__fc_builtin.h"
--
GitLab