From b1484e7c6ebf8e64835a081f96ba2fd17d24130f Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 10 Aug 2020 18:28:04 -0700
Subject: [PATCH 1/4] Check for negative integer indices when doing
 indexing-out-of-bounds checks.

Fixes #861
---
 src/Cryptol/Eval/Generic.hs | 26 ++++++++++++++++----------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 95391069..6f242725 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -1407,9 +1407,18 @@ assertIndexInBounds ::
   Either (SInteger sym) (WordValue sym) {- ^ Index value -} ->
   SEval sym ()
 
--- Can't index out of bounds for an infinite sequence
-assertIndexInBounds _sym Inf _ =
-  return ()
+-- Bitvectors can't index out of bounds for an infinite sequence
+assertIndexInBounds _sym Inf (Right _) = return ()
+
+-- All nonnegative integers are in bounds for an infinite sequence
+assertIndexInBounds sym Inf (Left idx) =
+  do ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0
+     assertSideCondition sym ppos (InvalidIndex (integerAsLit sym idx))
+
+-- If the index is concrete, test it directly
+assertIndexInBounds sym (Nat n) (Left idx)
+  | Just i <- integerAsLit sym idx
+  = unless (0 < i && i < n) (raiseError sym (InvalidIndex (Just i)))
 
 -- Can't index out of bounds for a sequence that is
 -- longer than the expressible index values
@@ -1417,21 +1426,18 @@ assertIndexInBounds sym (Nat n) (Right idx)
   | n >= 2^(wordValueSize sym idx)
   = return ()
 
--- If the index is concrete, test it directly
-assertIndexInBounds sym (Nat n) (Left idx)
-  | Just i <- integerAsLit sym idx
-  = unless (i < n) (raiseError sym (InvalidIndex (Just i)))
-
 -- If the index is concrete, test it directly
 assertIndexInBounds sym (Nat n) (Right (WordVal idx))
   | Just (_w,i) <- wordAsLit sym idx
   = unless (i < n) (raiseError sym (InvalidIndex (Just i)))
 
 -- If the index is an integer, test that it
--- is less than the concrete value of n.
+-- is nonnegative and less than the concrete value of n.
 assertIndexInBounds sym (Nat n) (Left idx) =
   do n' <- integerLit sym n
-     p <- intLessThan sym idx n'
+     ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0
+     pn <- intLessThan sym idx n'
+     p <- bitAnd sym ppos pn
      assertSideCondition sym p (InvalidIndex Nothing)
 
 -- If the index is a packed word, test that it

From cfc0f7c6df22f03baf725db66d55c88ce355dd57 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 11 Aug 2020 07:39:53 -0700
Subject: [PATCH 2/4] Fix bounds checking for integer indices to allow 0 and
 other bounds checking fixes.

---
 src/Cryptol/Eval/Generic.hs | 27 +++++++++++----------------
 src/Cryptol/Eval/Value.hs   |  8 ++++----
 2 files changed, 15 insertions(+), 20 deletions(-)

diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 6f242725..3764e0fc 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -1407,18 +1407,22 @@ assertIndexInBounds ::
   Either (SInteger sym) (WordValue sym) {- ^ Index value -} ->
   SEval sym ()
 
--- Bitvectors can't index out of bounds for an infinite sequence
-assertIndexInBounds _sym Inf (Right _) = return ()
-
 -- All nonnegative integers are in bounds for an infinite sequence
 assertIndexInBounds sym Inf (Left idx) =
   do ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0
      assertSideCondition sym ppos (InvalidIndex (integerAsLit sym idx))
 
--- If the index is concrete, test it directly
-assertIndexInBounds sym (Nat n) (Left idx)
-  | Just i <- integerAsLit sym idx
-  = unless (0 < i && i < n) (raiseError sym (InvalidIndex (Just i)))
+-- If the index is an integer, test that it
+-- is nonnegative and less than the concrete value of n.
+assertIndexInBounds sym (Nat n) (Left idx) =
+  do n' <- integerLit sym n
+     ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0
+     pn <- intLessThan sym idx n'
+     p <- bitAnd sym ppos pn
+     assertSideCondition sym p (InvalidIndex (integerAsLit sym idx))
+
+-- Bitvectors can't index out of bounds for an infinite sequence
+assertIndexInBounds _sym Inf (Right _) = return ()
 
 -- Can't index out of bounds for a sequence that is
 -- longer than the expressible index values
@@ -1431,15 +1435,6 @@ assertIndexInBounds sym (Nat n) (Right (WordVal idx))
   | Just (_w,i) <- wordAsLit sym idx
   = unless (i < n) (raiseError sym (InvalidIndex (Just i)))
 
--- If the index is an integer, test that it
--- is nonnegative and less than the concrete value of n.
-assertIndexInBounds sym (Nat n) (Left idx) =
-  do n' <- integerLit sym n
-     ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0
-     pn <- intLessThan sym idx n'
-     p <- bitAnd sym ppos pn
-     assertSideCondition sym p (InvalidIndex Nothing)
-
 -- If the index is a packed word, test that it
 -- is less than the concrete value of n, which
 -- fits into w bits because of the above test.
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
index f4275926..a4ab764c 100644
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -272,21 +272,21 @@ wordValueSize _ (LargeBitsVal n _) = n
 -- | Select an individual bit from a word value
 indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
 indexWordValue sym (WordVal w) idx
-   | idx < wordLen sym w = wordBit sym w idx
+   | 0 <= idx && idx < wordLen sym w = wordBit sym w idx
    | otherwise = invalidIndex sym idx
 indexWordValue sym (LargeBitsVal n xs) idx
-   | idx < n   = fromVBit <$> lookupSeqMap xs idx
+   | 0 <= idx && idx < n = fromVBit <$> lookupSeqMap xs idx
    | otherwise = invalidIndex sym idx
 
 -- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the
 --   given bit value.
 updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
 updateWordValue sym (WordVal w) idx b 
-   | idx >= wordLen sym w = invalidIndex sym idx
+   | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx
    | isReady sym b = WordVal <$> (wordUpdate sym w idx =<< b)
 
 updateWordValue sym wv idx b
-   | idx < wordValueSize sym wv =
+   | 0 <= idx && idx < wordValueSize sym wv =
         pure $ LargeBitsVal (wordValueSize sym wv) $ updateSeqMap (asBitsMap sym wv) idx (VBit <$> b)
    | otherwise = invalidIndex sym idx
 

From 06aca879f00c231273a3634e3a833ab26b64fec9 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 11 Aug 2020 09:28:13 -0700
Subject: [PATCH 3/4] Test case for issue 861

---
 tests/issues/issue861.cry         |  6 ++++++
 tests/issues/issue861.icry        | 31 +++++++++++++++++++++++++++++
 tests/issues/issue861.icry.stdout | 33 +++++++++++++++++++++++++++++++
 3 files changed, 70 insertions(+)
 create mode 100644 tests/issues/issue861.cry
 create mode 100644 tests/issues/issue861.icry
 create mode 100644 tests/issues/issue861.icry.stdout

diff --git a/tests/issues/issue861.cry b/tests/issues/issue861.cry
new file mode 100644
index 00000000..7a510e00
--- /dev/null
+++ b/tests/issues/issue861.cry
@@ -0,0 +1,6 @@
+atXis0:
+    {n, a, w}
+    (fin n, Eq a, Zero a, Cmp w, Integral w, Literal n w) =>
+    [n]a -> w -> Bit
+property atXis0 seq i =
+    zero == seq ==> i < `n ==> seq @ i == zero
diff --git a/tests/issues/issue861.icry b/tests/issues/issue861.icry
new file mode 100644
index 00000000..58351af3
--- /dev/null
+++ b/tests/issues/issue861.icry
@@ -0,0 +1,31 @@
+:l issue861.cry
+
+:set tests=1000
+
+:check atXis0`{4, Char, Integer}
+
+let xs = [0,1,2] : [3]Integer
+
+xs@0
+xs@1
+xs@2
+xs@3
+xs@(-1)
+
+xs!0
+xs!1
+xs!2
+xs!3
+xs!(-1)
+
+update xs 0 5
+update xs 1 5
+update xs 2 5
+update xs 3 5
+update xs (-1) 5
+
+updateEnd xs 0 5
+updateEnd xs 1 5
+updateEnd xs 2 5
+updateEnd xs 3 5
+updateEnd xs (-1) 5
diff --git a/tests/issues/issue861.icry.stdout b/tests/issues/issue861.icry.stdout
new file mode 100644
index 00000000..18a13e4a
--- /dev/null
+++ b/tests/issues/issue861.icry.stdout
@@ -0,0 +1,33 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Using random testing.
+Testing... Passed 1000 tests.
+0
+1
+2
+
+invalid sequence index: 3
+
+invalid sequence index: -1
+2
+1
+0
+
+invalid sequence index: 3
+
+invalid sequence index: -1
+[5, 1, 2]
+[0, 5, 2]
+[0, 1, 5]
+
+invalid sequence index: 3
+
+invalid sequence index: -1
+[0, 1, 5]
+[0, 5, 2]
+[5, 1, 2]
+
+invalid sequence index: 3
+
+invalid sequence index: -1

From af94423b48f28e71e6cc8151193fc78dff164d0d Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 11 Aug 2020 11:06:59 -0700
Subject: [PATCH 4/4] Remove the `atXis0` test.  I couldn't think of a way to
 make it determinsitic enough for a regression test.

---
 tests/issues/issue861.cry         | 6 ------
 tests/issues/issue861.icry        | 5 -----
 tests/issues/issue861.icry.stdout | 4 ----
 3 files changed, 15 deletions(-)
 delete mode 100644 tests/issues/issue861.cry

diff --git a/tests/issues/issue861.cry b/tests/issues/issue861.cry
deleted file mode 100644
index 7a510e00..00000000
--- a/tests/issues/issue861.cry
+++ /dev/null
@@ -1,6 +0,0 @@
-atXis0:
-    {n, a, w}
-    (fin n, Eq a, Zero a, Cmp w, Integral w, Literal n w) =>
-    [n]a -> w -> Bit
-property atXis0 seq i =
-    zero == seq ==> i < `n ==> seq @ i == zero
diff --git a/tests/issues/issue861.icry b/tests/issues/issue861.icry
index 58351af3..30185602 100644
--- a/tests/issues/issue861.icry
+++ b/tests/issues/issue861.icry
@@ -1,8 +1,3 @@
-:l issue861.cry
-
-:set tests=1000
-
-:check atXis0`{4, Char, Integer}
 
 let xs = [0,1,2] : [3]Integer
 
diff --git a/tests/issues/issue861.icry.stdout b/tests/issues/issue861.icry.stdout
index 18a13e4a..6fc0462b 100644
--- a/tests/issues/issue861.icry.stdout
+++ b/tests/issues/issue861.icry.stdout
@@ -1,8 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
-Loading module Main
-Using random testing.
-Testing... Passed 1000 tests.
 0
 1
 2