From b010834c8d2abff62c590b684631cb728e047ea9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 6 Sep 2019 10:05:28 +0200
Subject: [PATCH] [Eva] Fixes the traces domain for the memexec cache.

---
 src/plugins/value/domains/traces/traces_domain.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 87057cd9b91..5bc65500f86 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -309,8 +309,15 @@ module Internal = struct
   end
 
   (* Memexec *)
-  let filter_by_bases _bases state = state
-  let reuse ~current_input:state ~previous_output:_ = state
+  (* This domains infers no relation between variables. *)
+  let relate _kf _bases _state = Base.SetLattice.bottom
+  (* Do not filter the state: the memexec cache will be applied only on function
+     calls for which the entry states are equal. This almost completely
+     disable memexec, but is always sound. *)
+  let filter _kf _kind _bases state = state
+  (* As memexec cache is only applied on equal entry states, the previous
+     output state is a correct output for the current input state. *)
+  let reuse _kf _bases ~current_input:_ ~previous_output:state = state
 
   let empty () = Traces.empty
   let introduce_globals _vars state = state
-- 
GitLab