Could not match specified value with actual value

[weaversa]

could not match specified value with actual value:
  actual (simulator) value: [{literal integer: unsigned value = 3, signed value =  3, width = 32
                             ;{literal integer: unsigned value = 1, signed value =  1, width = 64
                              ;literal integer: unsigned value = 1, signed value =  1, width = 64
                              ;concrete pointer: allocation = 110, offset = 0}}]
  specified value:          [{Cryptol.ecNumber
                                (Cryptol.TCNum 3)
                                (Prelude.Vec 32 Prelude.Bool)
                                (Cryptol.PLiteralSeqBool
                                   (Cryptol.TCNum
                                      32)) : [32], {Cryptol.ecNumber
                                                      (Cryptol.TCNum 1)
                                                      (Prelude.Vec 64
                                                         Prelude.Bool)
                                                      (Cryptol.PLiteralSeqBool
                                                         (Cryptol.TCNum
                                                            64)) : [64], sequence.pList.nLength_max : [64], @AllocIndex 3}}]
  type of actual value:    [1 x { i32, { i64, i64, [1 x i64]* } }]
  type of specified value: [1 x { i32, { i64, i64, [1 x i64]* } }]

Maybe related to #519 ?

[weaversa]

701.tar.gz

[weaversa]

I've boiled this down to an issue with crucible_array. Using crucible_array in a prestate seems fine, but using it in a poststate gives could not match specified value with actual value. Simple example attached at the bottom.

#include <stdint.h>

uint32_t *f(uint32_t *x) {
  return x;
}

let f_pre_spec = do {
  x0 <- crucible_fresh_var "x0" (llvm_int 32);
  let x = crucible_array [crucible_term x0];
  xp <- crucible_alloc (llvm_array 1 (llvm_int 32));
  crucible_points_to xp x;

  crucible_execute_func [xp];

  x' <- crucible_fresh_var "x'" (llvm_array 1 (llvm_int 32));
  crucible_points_to xp (crucible_term x');

  crucible_return (xp);
};

let f_post_spec = do {
  x <- crucible_fresh_var "x" (llvm_array 1 (llvm_int 32));
  xp <- crucible_alloc (llvm_array 1 (llvm_int 32));
  crucible_points_to xp (crucible_term x);

  crucible_execute_func [xp];

  x0' <- crucible_fresh_var "x0'" (llvm_int 32);
  let x' = crucible_array [crucible_term x0'];
  crucible_points_to xp x';

  crucible_return (xp);
};

m <- llvm_load_module "test.bc";

f_pre_result <- crucible_llvm_verify m "f" [] true f_pre_spec z3;
f_post_result <- crucible_llvm_verify m "f" [] true f_post_spec z3;

$ saw test.saw
[18:52:28.530] Loading file "701_simple/test.saw"
[18:52:28.536] Verifying f ...
[18:52:28.536] Simulating f ...
[18:52:28.540] Checking proof obligations f ...
[18:52:28.540] Proof succeeded! f
[18:52:28.541] Verifying f ...
[18:52:28.541] Simulating f ...
[18:52:28.545] "crucible_llvm_verify" (701_simple/test.saw:32:18-32:38):
at 701_simple/test.saw:32:18
could not match specified value with actual value:
  actual (simulator) value: [symbolic integer:  width = 32]
  specified value:          [x0' : [32]]
  type of actual value:    [1 x i32]
  type of specified value: [1 x i32]

701_simple.tar.gz

[atomb]

One thing that's going on here that makes it hard to debug is that the "actual (simulator) value" printouts describe symbolic values as just "symbolic integer" or something similar, which makes it hard to tell where they're coming from. One first step would be to change those to be sure to include their names.

[atomb]

Having looked at this a little more careful, I think it's something that should work but doesn't right now. I suspect it may be due to unfortunate interactions between two different term representations (SAWCore and What4). I wonder if @brianhuffman has any thoughts about this. Could it be due to a difference in the translation of a single integer from SAWCore to What4 vs. a vector of one integer?

[weaversa]

@atomb I hope you're not stuck on the specific message (copied below). crucible_array doesn't work in the poststate for any type (at least, I have never been able to get it to work). The example above was just something small to demonstrate that it's broken.

could not match specified value with actual value:
  actual (simulator) value: [symbolic integer:  width = 32]
  specified value:          [x0' : [32]]
  type of actual value:    [1 x i32]
  type of specified value: [1 x i32]

[brianhuffman]

The case for array values was simply missing from the matchArg function in the SAWScript.Crucible.LLVM.Override module. PR #717 now includes a patch to fix it.

As of 32f53e2, the 701_simple test completes successfully:

[05:07:59.105] Loading file "/Users/huffman/Documents/saw/701/701_simple/test.saw"
[05:07:59.110] Verifying f ...
[05:07:59.111] Simulating f ...
[05:07:59.114] Checking proof obligations f ...
[05:07:59.114] Proof succeeded! f
[05:07:59.114] Verifying f ...
[05:07:59.115] Simulating f ...
[05:07:59.117] Checking proof obligations f ...
[05:07:59.117] Proof succeeded! f