From 94b2be7d36128adb33910666c137cfa0320605a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Mon, 20 Nov 2023 13:01:06 -0500
Subject: [PATCH] smt: ensure that updates are properly overwritten

---
 src/mc/smt.rs   | 9 ++++++---
 src/mc/types.rs | 9 +++++++++
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/mc/smt.rs b/src/mc/smt.rs
index 3c4011c..63725e5 100644
--- a/src/mc/smt.rs
+++ b/src/mc/smt.rs
@@ -250,7 +250,7 @@ fn parse_smt_store(
     let mut inner = parse_smt_array(smt_ctx, array)?;
     let (index_val, _) = parse_smt_bit_vec(smt_ctx, index)?;
     let (data_val, _) = parse_smt_bit_vec(smt_ctx, value)?;
-    inner.updates.push((index_val, data_val));
+    inner.add_update(index_val, data_val);
     Some(inner)
 }
 
@@ -708,11 +708,13 @@ mod tests {
         let default = ctx.binary(data_width, default_value);
 
         // check the base expression
+        // ((as const (Array (_ BitVec 5) (_ BitVec 32))) #b00000000000000000000000000110011)
         let base = ctx.const_array(tpe, default);
         let base_val = parse_smt_array(&ctx, base).unwrap();
         assert_eq!(base_val.default, Some(BigUint::from(default_value)));
 
         // store
+        // (store <base> #b01110 #x00000000)
         let store_index: usize = 14;
         let store_data: usize = 0;
         let store = ctx.store(
@@ -728,8 +730,9 @@ mod tests {
         );
 
         // two stores
+        // (store <store> #b01110 #x00000011)
         let store2_index: usize = 14;
-        let store2_data: usize = 0;
+        let store2_data: usize = 3;
         let store2 = ctx.store(
             store,
             ctx.binary(index_width, store2_index),
@@ -740,7 +743,7 @@ mod tests {
         assert_eq!(
             store2_val.updates,
             vec![
-                (BigUint::from(store_index), BigUint::from(store_data)),
+                // should be overwritten
                 (BigUint::from(store2_index), BigUint::from(store2_data))
             ]
         );
diff --git a/src/mc/types.rs b/src/mc/types.rs
index c70b118..9bf57ba 100644
--- a/src/mc/types.rs
+++ b/src/mc/types.rs
@@ -49,6 +49,15 @@ pub struct WitnessArray {
     pub updates: Vec<(BigUint, BigUint)>,
 }
 
+impl WitnessArray {
+    pub fn add_update(&mut self, index: BigUint, value: BigUint) {
+        // delete any previous update that mapped to the same index
+        self.updates.retain(|(i, _)| !i.eq(&index));
+        // add new update
+        self.updates.push((index, value));
+    }
+}
+
 pub fn parse_big_uint_from_bit_string(value: &str) -> (BigUint, WidthInt) {
     let int_val = BigUint::from_str_radix(value, 2).unwrap();
     (int_val, value.len() as WidthInt)