Fix bounds checking for integer indices to allow 0 and other

bounds checking fixes.

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.

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