Merge pull request #1254 from GaloisInc/issue1239

Fix issue 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

tests/regression/ignore-safe.icry

@@ -10,7 +10,6 @@
 :prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
 
 :prove (\ (x:Integer) -> [0,0,0]@x == 0 )
-:prove (\ (x:Integer) -> []@x == 0 )
 :prove (\ (x:[8]) -> [0,0,0]@x == 0 )
 
 :set ignore-safety = on
@@ -22,5 +21,4 @@
 :prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
 
 :prove (\ (x:Integer) -> [0,0,0]@x == 0 )
-:prove (\ (x:Integer) -> []@x == 0 )
 :prove (\ (x:[8]) -> [0,0,0]@x == 0 )

tests/regression/ignore-safe.icry.stdout

@@ -11,5 +11,3 @@ Q.E.D.
 Q.E.D.
 Q.E.D.
 Q.E.D.
-Q.E.D.
-Q.E.D.