Update indexing primitives to remove troublesome corner cases.

Previously, when indexing into a sequence, there were code paths
in both the SBV and What4 backends where an if/then/else tree
would be built to compute the value of a symbolic lookup, with one
branch for each valid sequence index.  They differed, however, in
what value they would comute for out-of-bound indices.  For SBV,
we would compute a `zero` value, whereas for What4 we would
raise an error.  For What4, this resulted in unfortunate and redundant
proof obligations, as we elsewhere add a test for in-bounds contditions
to the safety predicate.  Moreover, the strategy of returning a
`zero` value could panic in some situations, as not every type
has a `zero` value anymore (e.g., newtypes).

In both cases, we now do the same thing, which is not to have a case
of the if/then/else tree for out-of-bounds indices; the final element
of the sequence will simply be returned instead.  We will only raise
an out of bounds error in this code path if the sequence is actually
empty.

Fixes #1239

src/Cryptol/Eval/SBV.hs

@@ -29,7 +29,7 @@ import qualified Data.Text as T
 import Data.SBV.Dynamic as SBV
 
 import Cryptol.Backend
-import Cryptol.Backend.Monad (Unsupported(..) )
+import Cryptol.Backend.Monad (Unsupported(..), EvalError(..) )
 import Cryptol.Backend.SBV
 import Cryptol.Backend.SeqMap
 import Cryptol.Backend.WordValue
@@ -81,25 +81,32 @@ indexFront sym mblen a xs _ix idx
          Just ws ->
            do z <- wordLit sym wlen 0
               return $ VWord wlen $ wordVal $ SBV.svSelect ws z idx
-         Nothing -> folded
+         Nothing -> folded'
+
+  | otherwise = folded'
 
-  | otherwise
-  = folded
 
  where
     k = SBV.kindOf idx
-    def = zeroV sym a
-    f n y = iteValue sym (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y
+
+    f n (Just y) = Just $ iteValue sym (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y
+    f n Nothing  = Just $ lookupSeqMap xs n
+
+    folded' =
+      case folded of
+        Nothing -> raiseError sym (InvalidIndex Nothing)
+        Just m  -> m
+
     folded =
       case k of
         KBounded _ w ->
           case mblen of
-            Nat n | n < 2^w -> foldr f def [0 .. n-1]
-            _ -> foldr f def [0 .. 2^w - 1]
+            Nat n | n < 2^w -> foldr f Nothing [0 .. n-1]
+            _ -> foldr f Nothing [0 .. 2^w - 1]
         _ ->
           case mblen of
-            Nat n -> foldr f def [0 .. n-1]
-            Inf -> liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))
+            Nat n -> foldr f Nothing [0 .. n-1]
+            Inf -> Just (liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing")))
 
 indexFront_segs ::
   SBV ->

src/Cryptol/Eval/What4.hs

@@ -510,19 +510,20 @@ indexFront_int sym mblen _a xs ix idx
   = lookupSeqMap xs i
 
   | (lo, Just hi) <- bounds
-  = foldr f def [lo .. hi]
+  = case foldr f Nothing [lo .. hi] of
+      Nothing -> raiseError sym (InvalidIndex Nothing)
+      Just m  -> m
 
   | otherwise
   = liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))
 
  where
     w4sym = w4 sym
 
-    def = raiseError sym (InvalidIndex Nothing)
-
-    f n y =
+    f n (Just y) = Just $
        do p <- liftIO (W4.intEq w4sym idx =<< W4.intLit w4sym n)
           iteValue sym p (lookupSeqMap xs n) y
+    f n Nothing = Just $ lookupSeqMap xs n
 
     bounds =
       (case W4.rangeLowBound (W4.integerBounds idx) of
@@ -559,17 +560,19 @@ indexFront_segs sym mblen _a xs _ix _idx_bits [WordIndexSegment idx]
   = lookupSeqMap xs i
 
   | otherwise
-  = foldr f def idxs
+  = case foldr f Nothing idxs of
+      Nothing -> raiseError sym (InvalidIndex Nothing)
+      Just m  -> m
 
  where
     w4sym = w4 sym
 
     w = SW.bvWidth idx
-    def = raiseError sym (InvalidIndex Nothing)
 
-    f n y =
+    f n (Just y) = Just $
        do p <- liftIO (SW.bvEq w4sym idx =<< SW.bvLit w4sym w n)
           iteValue sym p (lookupSeqMap xs n) y
+    f n Nothing = Just $ lookupSeqMap xs n
 
     -- maximum possible in-bounds index given the bitwidth
     -- of the index value and the length of the sequence