iss-1932

intTests/test_llvm_bound_check/Makefile

@@ -0,0 +1,2 @@
+bound.bc : bound.c
+	clang -c -emit-llvm -o bound.bc bound.c

intTests/test_llvm_bound_check/bound.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t f(uint32_t x[2]) {
+  return x[1];
+}

intTests/test_llvm_bound_check/bound.saw

@@ -0,0 +1,15 @@
+let f_spec = do {
+    x <- llvm_alloc (llvm_array 2 (llvm_int 32));
+    a <- llvm_fresh_var "a" (llvm_int 32);
+    llvm_points_to (llvm_elem x 1) (llvm_term a);
+
+    // BAD: Out-of-bounds write
+    llvm_points_to (llvm_elem x 2) (llvm_term a);
+
+    llvm_execute_func [x];
+
+    llvm_return (llvm_term a);
+};
+
+m <- llvm_load_module "bound.bc";
+llvm_verify m "f" [] false f_spec z3;

intTests/test_llvm_bound_check/test.sh

@@ -0,0 +1,10 @@
+#!/bin/sh
+
+set -e
+
+# We want to ensure there isn't a memory store failure and this is caught during type checking of Setup Value
+if $SAW bound.saw | grep -q "Memory store failed"; then
+    exit 1
+else
+    exit 0
+fi

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -502,7 +502,7 @@ typeOfSetupValue cc env nameEnv val =
                Right memTy' ->
                  case memTy' of
                    Crucible.ArrayType n memTy''
-                     | fromIntegral i <= n -> return (Crucible.PtrType (Crucible.MemType memTy''))
+                     | fromIntegral i < n -> return (Crucible.PtrType (Crucible.MemType memTy''))
                      | otherwise -> throwError $ unwords $
                          [ "typeOfSetupValue: array type index out of bounds"
                          , "(index: " ++ show i ++ ")"
@@ -574,7 +574,7 @@ resolveSetupElemOffset cc env nameEnv v i = do
            Right memTy' ->
              case memTy' of
                Crucible.ArrayType n memTy''
-                 | fromIntegral i <= n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
+                 | fromIntegral i < n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
                Crucible.StructType si ->
                  case Crucible.siFieldOffset si i of
                    Just d -> return d