From 55e9427a2986b40d19bbd511d06545e86b196894 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2019 14:51:12 +0200
Subject: [PATCH] [Eva] Trace_partitioning: removes already propagated states
only at statements.
Restores a previous optimization.
This is a useful optimization, as the inclusion tests between incoming states
and already propagated states are very costly.
---
src/plugins/value/engine/trace_partitioning.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 2a63927373b..063afad6c95 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -288,8 +288,10 @@ struct
dest.store_partition <- Partition.replace key s dest.store_partition;
in
Extlib.may add state;
- (* Filter out already propagated states *)
- Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
+ (* Filter out already propagated states (only at statements). *)
+ if dest.store_stmt = None
+ then state
+ else Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
in
let flow = Flow.join_duplicate_keys flow_states in
let flow = Flow.filter_map update flow in
--
GitLab