Incorrect bounds checking for LLVM array functions

[RyanGlScott]

While browsing the code in the SAW LLVM backend recently, I noticed a couple of array bounds checks that look suspicious:

• saw-script/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

  Lines 500 to 506 in 4c0985c

  	Crucible.ArrayType n memTy''
  	| fromIntegral i <= n -> return (Crucible.PtrType (Crucible.MemType memTy''))
  	| otherwise -> throwError $ unwords $
  	[ "typeOfSetupValue: array type index out of bounds"
  	, "(index: " ++ show i ++ ")"
  	, "(array length: " ++ show n ++ ")"
  	]

• saw-script/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

  Lines 572 to 573 in 4c0985c

  	Crucible.ArrayType n memTy''
  	| fromIntegral i <= n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')

Since i is zero-indexed, I believe these should be fromIntegral i < n, not fromIntegral i <= n.

I don't believe this is a source of unsoundness, since I think the worst that can happen from this code is that you might try to write to an uninitialized part of Crucible memory, which will cause Crucible to throw an error message. That being said, the error message you'd get in this situation would be suboptimal. When you run SAW on the this program, which writes to an array index equal to the length of the array:

#include <stdint.h>

uint32_t f(uint32_t x[2]) {
  return x[1];
}

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 "test.bc";
llvm_verify m "f" [] false f_spec z3;

Then SAW will produce this error:

$ ~/Software/saw-1.0/bin/saw test.saw



[12:23:31.271] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[12:23:31.274] Verifying f ...
[12:23:31.274] Simulating f ...
[12:23:31.275] Checking proof obligations f ...
[12:23:31.281] Subgoal failed: f internal: error: in _SAW_verify_prestate
Memory store failed
Details:
  The region wasn't allocated, wasn't large enough, or was marked as readonly
[12:23:31.281] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 29}
[12:23:31.281] ----------Counterexample----------
[12:23:31.281] <<All settings of the symbolic variables constitute a counterexample>>
[12:23:31.281] ----------------------------------
[12:23:31.281] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:15:1-15:12)
Proof failed.

If you made one minor change to this program, however:

-    llvm_points_to (llvm_elem x 2) (llvm_term a);
+    llvm_points_to (llvm_elem x 3) (llvm_term a);

Then the error message becomes much more understandable:

$ ~/Software/saw-1.0/bin/saw test.saw



[12:25:11.936] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[12:25:11.939] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:15:1-15:12)
"f_spec" (/home/ryanscott/Documents/Hacking/SAW/test.saw:15:28-15:34)
"llvm_points_to" (/home/ryanscott/Documents/Hacking/SAW/test.saw:7:5-7:19)
typeOfSetupValue: array type index out of bounds (index: 3) (array length: 2)

I believe that if we fixed the bounds checks above to be fromIntegral i < n, then we would get the more understandable error message in both cases. This issue tracks implementing this idea.

[RyanGlScott]

Fixed in #1949.