From 7b4bf2bd14cae99a4d8086a0b66d9875be1acbab Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 21 May 2019 17:31:13 +0100
Subject: SMT: Use a separate constructor for memory read variables

We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
---
 src/jib/jib_smt.ml | 4 ++--
 src/smtlib.ml      | 6 ++++--
 2 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 7420707c..0d6f42fe 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1044,7 +1044,7 @@ let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
   let name = "R" ^ string_of_int !reads in
   [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk,
              smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
-  Var (name ^ "_ret")
+  Read_res name
 
 let excl_results = ref (-1)
 
@@ -1626,7 +1626,7 @@ module Make_optimizer(S : Sequence) = struct
          | Some n -> Hashtbl.replace uses var (n + 1)
          | None -> Hashtbl.add uses var 1
          end
-      | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
+      | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
       | Fn (_, exps) | Ctor (_, exps) ->
          List.iter uses_in_exp exps
       | Ite (cond, t, e) ->
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 5de13bdb..b90f33a7 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -94,6 +94,7 @@ type smt_exp =
   | Real_lit of string
   | String_lit of string
   | Var of string
+  | Read_res of string
   | Enum of string
   | Fn of string * smt_exp list
   | Ctor of string * smt_exp list
@@ -109,7 +110,7 @@ let rec fold_smt_exp f = function
   | SignExtend (n, exp) -> f (SignExtend (n, fold_smt_exp f exp))
   | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp))
   | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp))
-  | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Enum _ as exp) -> f exp
+  | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Read_res _ | Enum _ as exp) -> f exp
 
 let smt_conj = function
   | [] -> Bool_lit true
@@ -204,7 +205,7 @@ let rec simp_smt_exp vars kinds = function
      | Some exp -> simp_smt_exp vars kinds exp
      | None -> Var v
      end
-  | (Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | (Read_res _ | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
   | Fn (f, exps) ->
      let exps = List.map (simp_smt_exp vars kinds) exps in
      simp_fn (Fn (f, exps))
@@ -330,6 +331,7 @@ let rec pp_smt_exp =
   | Hex str -> string ("#x" ^ str)
   | Bin str -> string ("#b" ^ str)
   | Var str -> string str
+  | Read_res str -> string (str ^ "_ret")
   | Enum str -> string str
   | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
   | Ctor (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
-- 
cgit v1.2.3