saw-core: Fix bug involving incorrect maximum values in selectV

[RyanGlScott]

The selectV function had a maxValue argument that, in principle, was supposed to represent the largest possible value of the index argument (treated as a big-endian list of bits). In practice, however, this was always given the length of the vector being indexed into minus 1! This led to subtle issues where indexing vectors with seemingly out-of-bounds indices would succeed, since the index value would be clamped to the length of the vector minus 1, which is always in bounds.

This patch fixes the bug. Moreover, it turns out that the maxValue argument is not actually needed to do selectV's job, as its implementation always upholds the invariant that the bitmask that it computes never exceeds the largest possible value of the index argument. To make the code simpler, I have removed the maxValue argument entirely, and I have added some more comments in selectV in saw-core, as well as its cousins in saw-core-sbv and saw-core-what4, to explain why this works.

Fixes #1807.

[RyanGlScott]

It looks like this isn't quite right, as there are now some integration tests that are failing, e.g.,

[19:31:08.418] Loading file "/home/runner/work/saw-script/saw-script/examples/llvm/safety/set.saw"
[19:31:08.495] Verifying set ...
[19:31:08.496] Simulating set ...
[19:31:08.501] Checking proof obligations set ...
[19:31:08.875] ./Data/Vector/Generic/Mutable.hs:991 (update): index out of bounds (4294967295,10)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.3.1-f40fd5e4ddcae7f360ed2e694ddb273592b4e91964bfc7c2f37e468bf1577be7:Data.Vector.Internal.Check

FAIL (46.21s)
    intTests/IntegrationTest.hs:170:
    expected: ExitSuccess
     but got: ExitFailure 2
    Use -p '/test_examples/' to rerun this test only.

I will mark this as a draft until I figure out what is going on.

[RyanGlScott]

Here is a relatively small example of the bug, which has been extracted from examples/llvm/safety:

// set.c
void set(int *a, int i, int v) {
    a[i] = v;
}

// set.saw
let alloc_init ty v = do {
    p <- llvm_alloc ty;
    llvm_points_to p v;
    return p;
};

let ptr_to_fresh n ty = do {
    x <- llvm_fresh_var n ty;
    p <- alloc_init ty (llvm_term x);
    return (x, p);
};

let set_spec n = do {
    (a, ap) <- ptr_to_fresh "a" (llvm_array n (llvm_int 32));
    i <- llvm_fresh_var "i" (llvm_int 32);
    v <- llvm_fresh_var "v" (llvm_int 32);

    // The ` in the following is to convert an unbounded integer into a
    // fixed-size bit vector.
    llvm_precond {{ i < (`n : [32]) }};

    llvm_execute_func [ap, llvm_term i, llvm_term v];

    llvm_points_to ap (llvm_term {{ update a i v }});
};

m <- llvm_load_module "set.bc";

llvm_verify m "set" [] false (set_spec 10) abc;

$ clang -g -emit-llvm -c set.c
$ ~/Software/saw-0.9/bin/saw set.saw # Using saw-0.9


[13:27:44.025] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/set.saw"
[13:27:44.118] Verifying set ...
[13:27:44.119] Simulating set ...
[13:27:44.122] Checking proof obligations set ...
[13:27:47.159] Proof succeeded! set

$ ./bin/saw set.saw # Using the changes from this PR



[13:28:04.382] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/set.saw"
[13:28:04.449] Verifying set ...
[13:28:04.450] Simulating set ...
[13:28:04.453] Checking proof obligations set ...
[13:28:04.701] ./Data/Vector/Generic/Mutable.hs:991 (update): index out of bounds (4294967295,10)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.3.1-f40fd5e4ddcae7f360ed2e694ddb273592b4e91964bfc7c2f37e468bf1577be7:Data.Vector.Internal.Check

[RyanGlScott]

Another bug (which I suspect is unrelated to the one in #1808 (comment)) is taken from intTests/test0063_polyarith:

// polyarith.saw
let {{

thm : {n,m} (fin n, fin m, n > m, m >= 1) => [n] -> [m] -> Bit
thm x y = y != 0 ==>
    pmult y (pdiv x y) ^ (zero # pmod x y) == zero`{[m-1]}#x

}};

print_term (rewrite (cryptol_ss ())
  (unfold_term ["thm"] {{ thm`{16,4} }}));

prove_print rme {{ thm`{16,8} }};

$ ~/Software/saw-0.9/bin/saw polyarith.saw # Using saw-0.9


[15:39:00.864] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/polyarith.saw"
[15:39:01.040] let { x@1 = TCNum 16
      x@2 = Vec 4 Bool
      x@3 = TCNum 3
    }
 in \(x : Vec 16 Bool) ->
      \(y : x@2) ->
        ==> (not (ecEq x@2 (PEqWord 4) y (bvNat 4 0)))
          (ecEq (Vec 19 Bool) (PEqWord 19)
             (bvXor 19
                (Cryptol::pmult x@3 (TCNum 15) y
                   (Cryptol::pdiv x@1 (TCNum 4) x y))
                (append 16 3 Bool (bvNat 16 0) (Cryptol::pmod x@1 x@3 x y)))
             (append 3 16 Bool (bvNat 3 0) x))

$ ./bin/saw polyarith.saw # Using the changes from this PR



[15:39:08.879] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/polyarith.saw"
[15:39:09.045] let { x@1 = TCNum 16
      x@2 = Vec 4 Bool
      x@3 = TCNum 3
    }
 in \(x : Vec 16 Bool) ->
      \(y : x@2) ->
        ==> (not (ecEq x@2 (PEqWord 4) y (bvNat 4 0)))
          (ecEq (Vec 19 Bool) (PEqWord 19)
             (bvXor 19
                (Cryptol::pmult x@3 (TCNum 15) y
                   (Cryptol::pdiv x@1 (TCNum 4) x y))
                (append 16 3 Bool (bvNat 16 0) (Cryptol::pmod x@1 x@3 x y)))
             (append 3 16 Bool (bvNat 3 0) x))
[15:39:09.088] Run-time error: at: index out of bounds

There is another occurrence of this Run-time error: at: index out of bounds error in the ecdsa example, but that one is much, much more complicated. I am going to hope that fixing the bug in polyarith.saw will also fix the bug in the ecdsa example by extension.

[RyanGlScott]

This has ended up being a much deeper rabbit-hole than I expected. After looking further, I think that the implementation in this PR is actually correct, but implementing it has expected an entirely different bug in #1820. I've left some commentary on that issue about how it related to the main issue at hand, namely #1807. I'm not sure of how we can fix these issues without first addressing #1820.