From 14f5a81cd7d0a7e62ea798a3a32a97b173d9fcdd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 7 May 2021 15:31:53 +0200
Subject: [PATCH] [Eva] Dynamic split annotations.
---
src/plugins/value/Eva.mli | 8 ++++++--
src/plugins/value/partitioning/partition.ml | 12 +++++-------
src/plugins/value/partitioning/partition.mli | 4 ++--
.../partitioning/partitioning_parameters.ml | 5 ++---
src/plugins/value/utils/eva_annotations.ml | 16 +++++++++++++---
src/plugins/value/utils/eva_annotations.mli | 4 +++-
6 files changed, 31 insertions(+), 18 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 686e7ab2414..97761d74c25 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -87,10 +87,14 @@ module Eva_annotations: sig
| UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
| UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
+ type split_kind = Static | Dynamic
+
(** Split/merge annotations for value partitioning. *)
type flow_annotation =
- | FlowSplit of Cil_types.term (** Split states according to a term. *)
- | FlowMerge of Cil_types.term (** Merge states separated by a previous split. *)
+ | FlowSplit of Cil_types.term * split_kind
+ (** Split states according to a term. *)
+ | FlowMerge of Cil_types.term
+ (** Merge states separated by a previous split. *)
val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> slevel_annotation -> unit
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index a7138c912d6..2325162fd0c 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -166,7 +166,7 @@ type unroll_limit =
| IntLimit of int
| AutoUnroll of Cil_types.stmt * int * int
-type split_kind = Static | Dynamic
+type split_kind = Eva_annotations.split_kind = Static | Dynamic
type action =
| Enter_loop of unroll_limit
@@ -176,7 +176,7 @@ type action =
| Ration of rationing
| Restrict of Cil_types.exp * Integer.t list
| Split of Cil_types.exp * split_kind * split_monitor
- | Merge of Cil_types.exp * split_kind
+ | Merge of Cil_types.exp
| Update_dynamic_splits
exception InvalidAction
@@ -471,11 +471,9 @@ struct
| Restrict (expr, expected_values) -> fun k s ->
{ k with ration_stamp = stamp_by_value expr expected_values s}
- | Merge (exp, Static) -> fun k _x ->
- { k with static_split = ExpMap.remove exp k.static_split }
-
- | Merge (exp, Dynamic) -> fun k _x ->
- { k with dynamic_split = ExpMap.remove exp k.dynamic_split }
+ | Merge exp -> fun k _x ->
+ { k with static_split = ExpMap.remove exp k.static_split;
+ dynamic_split = ExpMap.remove exp k.dynamic_split }
in
map_keys transfer p
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index a5a3a569b37..1b773efe987 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -92,7 +92,7 @@ type unroll_limit =
split point, and the key is then kept unchanged until a merge.
- dynamic splits are regularly redone: the expression is re-evaluated, and
states are then split or merged accordingly. *)
-type split_kind = Static | Dynamic
+type split_kind = Eva_annotations.split_kind = Static | Dynamic
(** Split monitor: prevents splits from generating too many states. *)
type split_monitor
@@ -145,7 +145,7 @@ type action =
if [exp] evaluates to more than [limit] values, [limit] being the split
limit of the [monitor]. A same monitor can be used for successive splits
on different flows. *)
- | Merge of Cil_types.exp * split_kind
+ | Merge of Cil_types.exp
(** Forgets the split of an expression: states that were kept separate only
by the split of this expression will be joined together. *)
| Update_dynamic_splits
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index d77a88990c7..b3609a90cc6 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -125,14 +125,13 @@ struct
ValuePartitioning.fold add []
let flow_actions stmt =
- let kind = Partition.Static in
let map_annot acc t =
try
let monitor = Partition.new_monitor ~split_limit in
let action =
match t with
- | FlowSplit t -> Partition.Split (term_to_exp t, kind, monitor)
- | FlowMerge t -> Partition.Merge (term_to_exp t, kind)
+ | FlowSplit (t, kind) -> Partition.Split (term_to_exp t, kind, monitor)
+ | FlowMerge t -> Partition.Merge (term_to_exp t)
in
action :: acc
with
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 9cbcd7d3f9d..adaf06945a4 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -33,8 +33,10 @@ type unroll_annotation =
| UnrollAmount of Cil_types.term
| UnrollFull
+type split_kind = Static | Dynamic
+
type flow_annotation =
- | FlowSplit of term
+ | FlowSplit of term * split_kind
| FlowMerge of term
type taint_annotation = Cil_types.term list
@@ -232,6 +234,12 @@ module Merge = Register (struct
let is_loop_annot = false
end)
+module DynamicSplit = Register (struct
+ include SimpleTermAnnotation
+ let name = "dynamic_split"
+ let is_loop_annot = false
+ end)
+
module Taint = Register (struct
include ListTermAnnotation
let name = "taint"
@@ -248,7 +256,8 @@ let get_slevel_annot stmt =
let get_unroll_annot stmt = Unroll.get stmt
let get_flow_annot stmt =
- List.map (fun a -> FlowSplit a) (Split.get stmt) @
+ List.map (fun a -> FlowSplit (a, Static)) (Split.get stmt) @
+ List.map (fun a -> FlowSplit (a, Dynamic)) (DynamicSplit.get stmt) @
List.map (fun a -> FlowMerge a) (Merge.get stmt)
@@ -257,7 +266,8 @@ let add_slevel_annot = Slevel.add
let add_unroll_annot = Unroll.add
let add_flow_annot ~emitter ~loc stmt = function
- | FlowSplit annot -> Split.add ~emitter ~loc stmt annot
+ | FlowSplit (annot, Static) -> Split.add ~emitter ~loc stmt annot
+ | FlowSplit (annot, Dynamic) -> DynamicSplit.add ~emitter ~loc stmt annot
| FlowMerge annot -> Merge.add ~emitter ~loc stmt annot
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 2299ead597d..629f8ffe5ad 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -38,8 +38,10 @@ type unroll_annotation =
| UnrollAmount of Cil_types.term
| UnrollFull
+type split_kind = Static | Dynamic
+
type flow_annotation =
- | FlowSplit of Cil_types.term
+ | FlowSplit of Cil_types.term * split_kind
| FlowMerge of Cil_types.term
type taint_annotation = Cil_types.term list
--
GitLab