From 339a9066b316970d777b569d084d2435d7605652 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Sat, 3 Dec 2022 12:15:32 -0500
Subject: [PATCH] saw-core: Fix handling of atWithDefault for infinite bit
 sequences

When calling `atWithDefault n d v i`, `d` should be returned if `i` is greater
than or equal to `n`. `atWithDefault` is implemented as a primitive, so we must
ensure that this is done in `saw-core`'s `atWithDefaultOp` function. While
`atWithDefaultOp` was handling this correctly for generic infinite sequences, it
was _not_ correctly handling the special case of infinite bit sequences. This
led to the issues reported in #1768.

This patch fixes #1768 by introducing a `bpBvAtWithDefault` combinator that
implements the defaulting behavior above in terms of `bpBvAt`. I've added a test
case to demonstrate that the test case from #1768 now works as expected.
---
 intTests/test1768/test.cry                   |  4 ++++
 intTests/test1768/test.saw                   |  5 +++++
 intTests/test1768/test.sh                    |  3 +++
 saw-core/src/Verifier/SAW/Simulator/Prims.hs | 21 ++++++++++++++++++--
 4 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100644 intTests/test1768/test.cry
 create mode 100644 intTests/test1768/test.saw
 create mode 100755 intTests/test1768/test.sh

diff --git a/intTests/test1768/test.cry b/intTests/test1768/test.cry
new file mode 100644
index 0000000000..4937a4a585
--- /dev/null
+++ b/intTests/test1768/test.cry
@@ -0,0 +1,4 @@
+f : [2] -> [10]
+f x = take y
+  where
+    y = x # y
diff --git a/intTests/test1768/test.saw b/intTests/test1768/test.saw
new file mode 100644
index 0000000000..ecd792ad8e
--- /dev/null
+++ b/intTests/test1768/test.saw
@@ -0,0 +1,5 @@
+import "test.cry";
+print {{ f 0b11 }};
+print {{ f 0b10 }};
+print {{ f 0b00 }};
+sat z3 {{ \x -> f x == zero }};
diff --git a/intTests/test1768/test.sh b/intTests/test1768/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1768/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
index 444685f616..a226e66e30 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
@@ -769,7 +769,7 @@ atWithDefaultOp bp =
       VNat i ->
         case x of
           VVector xv -> lift (force (vecIdx d xv (fromIntegral i))) -- FIXME dangerous fromIntegral
-          VWord xw -> lift (VBool <$> bpBvAt bp xw (fromIntegral i)) -- FIXME dangerous fromIntegral
+          VWord xw -> lift (bpBvAtWithDefault bp (fromIntegral n) (force d) xw (fromIntegral i)) -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
       VBVToNat _sz i | bpIsSymbolicEvaluator bp -> do
         iv <- lift (toBits (bpUnpack bp) i)
@@ -777,13 +777,30 @@ atWithDefaultOp bp =
           VVector xv ->
             lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (force . vecIdx d xv) iv -- FIXME dangerous fromIntegral
           VWord xw ->
-            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (liftM VBool . bpBvAt bp xw) iv -- FIXME dangerous fromIntegral
+            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (bpBvAtWithDefault bp (fromIntegral n) (force d) xw) iv -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
 
       VIntToNat _i | bpIsSymbolicEvaluator bp -> panic "atWithDefault: symbolic integer TODO"
 
       _ -> throwE $ "atOp: expected Nat, got " <> Text.pack (show idx)
 
+-- | @bpBvAtWithDefault bp w d vw i@ returns @bpBvAt bp vw i@ if @i@ is between
+-- @0@ (inclusive) and @w@ (exclusive), the bit width of @vw@. Otherwise, it
+-- returns @d@.
+bpBvAtWithDefault ::
+  VMonad l =>
+  BasePrims l ->
+  Int ->
+  MValue l ->
+  VWord l ->
+  Int ->
+  MValue l
+bpBvAtWithDefault bp w d vw i
+  | 0 <= i && i < w
+  = VBool <$> bpBvAt bp vw i
+  | otherwise
+  = d
+
 -- upd :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> a -> Vec n a;
 updOp :: (VMonadLazy l, Show (Extra l)) => BasePrims l -> Prim l
 updOp bp =