Merge pull request #1361 from GaloisInc/T1359

Fix off-by-one error in What4 implementation of `(@)`

CHANGES.md

@@ -1,3 +1,10 @@
+# next
+
+## Bug fixes
+
+* Fix a bug in the What4 backend that could cause applications of `(@)` with
+  symbolic `Integer` indices to become out of bounds (#1359).
+
 # 2.13.0
 
 ## Language changes

src/Cryptol/Eval/What4.hs

@@ -505,7 +505,7 @@ indexFront_int ::
   TValue ->
   SInteger (What4 sym) ->
   SEval (What4 sym) (Value sym)
-indexFront_int sym mblen _a xs ix idx
+indexFront_int sym mblen _a xs _ix idx
   | Just i <- W4.asInteger idx
   = lookupSeqMap xs i
 
@@ -535,16 +535,13 @@ indexFront_int sym mblen _a xs ix idx
           _                        -> Nothing
       )
 
-    -- Maximum possible in-bounds index given `Z m`
-    -- type information and the length
-    -- of the sequence. If the sequences is infinite and the
-    -- integer is unbounded, there isn't much we can do.
+    -- Maximum possible in-bounds index given the length
+    -- of the sequence. If the sequence is infinite, there
+    -- isn't much we can do.
     maxIdx =
-      case (mblen, ix) of
-        (Nat n, TVIntMod m)  -> Just (min (toInteger n) (toInteger m))
-        (Nat n, _)           -> Just n
-        (_    , TVIntMod m)  -> Just m
-        _                    -> Nothing
+      case mblen of
+        Nat n -> Just (n - 1)
+        Inf   -> Nothing
 indexFront_segs ::
   W4.IsSymExprBuilder sym =>
   What4 sym ->

tests/issues/issue1359.icry

@@ -0,0 +1,7 @@
+:set prover=sbv-z3
+:safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)
+:safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))
+
+:set prover=w4-z3
+:safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)
+:safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))

tests/issues/issue1359.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Safe
+Safe
+Safe
+Safe