Merge pull request #862 from GaloisInc/issue861

Check for negative integer indices when doing indexing-out-of-bounds checks

src/Cryptol/Eval/Generic.hs

@@ -1407,9 +1407,22 @@ assertIndexInBounds ::
   Either (SInteger sym) (WordValue sym) {- ^ Index value -} ->
   SEval sym ()
 
--- Can't index out of bounds for an infinite sequence
-assertIndexInBounds _sym Inf _ =
-  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 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
@@ -1417,23 +1430,11 @@ 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.
-assertIndexInBounds sym (Nat n) (Left idx) =
-  do n' <- integerLit sym n
-     p <- intLessThan sym idx n'
-     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
 

tests/issues/issue861.icry

@@ -0,0 +1,26 @@
+
+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

tests/issues/issue861.icry.stdout

@@ -0,0 +1,29 @@
+Loading module Cryptol
+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