Also test parameters of a functoin

[Johanvdberg]

Modify the dot product example so that the x parameter is set to zero after the function call. How does you tell saw to also test the x parameters. My attempt is

xs <- fresh_symbolic "xs" {| [12][32] |};
ys <- fresh_symbolic "ys" {| [12][32] |};
let allocs = [ ("x", 12), ("y", 12) ];
let inputs = [ ("*x", xs, 12) , ("*y", ys, 12) , ("size", {{ 12:[32] }}, 1) ];
let outputs_and_in = [("return", 1), ("*x", 12)];

t <- llvm_symexec m "mod_dotprod" allocs inputs outputs true;
thm1 <- abstract_symbolic {{ t == mod_dotprod xs ys }};
prove_print abc thm1;

the C code:

uint32_t mod_dotprod(uint32_t *x, uint32_t *y, uint32_t size)
{
    uint32_t res = 0;
    for(size_t i = 0; i < size; i++) {
        res += x[i] * y[i];
    }
	memset(x, 0, size*sizeof(uint32_t));
    return res;
}

[Johanvdberg]

Update the saw script to use commands like llvm_verify:

llvm_verify m "mod_dotprod" [] do {
  llvm_ptr "x" (llvm_array  12 (llvm_int 8));
  x <- llvm_var "*x" (llvm_array  12 (llvm_int 8));
  llvm_ptr "y" (llvm_array  12 (llvm_int 8));
  y <- llvm_var "*y" (llvm_array  12 (llvm_int 8));

  size <- llvm_var "size" (llvm_int 32);
  llvm_assert {{size == 12}};


  let res = {{ mod_dotprod x y }};

  llvm_ensure_eq "*return" {{ res.0 }};   <<<<<<<< line 28
  llvm_ensure_eq "*x" {{ res.1 }};

  llvm_verify_tactic abc;
};

I get the error:

Loading module Cryptol
Loading file "....saw"
Loading module Main
Valid
saw: user error ("llvm_verify" (....saw:16:1):
"llvm_ensure_eq" (.....saw:28:3):
LLVM name *return has not been declared.)

According to the documentation "*return" need not be defined as it is already defined.

[atomb]

The return value of mod_dotprod is an integer, so you don't need the * on *return. I haven't tried it yet, but I think it should work without that.

In the long run, I should mention that the llvm_verify and llvm_symexec commands are likely to be deprecated (and eventually removed), in favor of crucible_llvm_verify and a new crucible_llvm_extract (which we haven't yet written).

See here for more information about using crucible_llvm_verify.

[TomMD]

@atomb Is it not the plan to deprecate the current llvm_verify and rename crucible_llvm_verify to llvm_verify? Keeping the crucible* names around just seems like pollution.

[atomb]

Yes, I think that's what we'll do. I had in mind the functionality and style of verification, rather than the function names, but didn't make that explicit. Thanks for clarifying.

[Johanvdberg]

Using return instead of *return I get the error

saw: user error ("llvm_verify" (.../dotprod.saw:16:1):
"llvm_ensure_eq" (.../dotprod.saw:29:3):
LLVM name return has not been declared.)

If I un-comment the line

llvm_ensure_eq "return" {{ res.0 }};

ending with:

Base memory
  Allocations:
    HeapAlloc lss__alloc1 Prelude.bvNat
                            64
                            144
    HeapAlloc lss__alloc0 Prelude.bvNat
                            64
                            144
  Writes:

--
--------------------------------------------------------------------------------
saw: user error ("llvm_verify" (/media/sf_cryptol/code/dotprod.saw:16:1):
Pattern match failure in do expression at src/Verifier/LLVM/Simulator/Internals.hs:1182:3-10)

The files I used ('.txt' was added at the end to github to accept the files):
dotprod.cry.txt
dotprod.saw.txt
dotprod.c.txt

[weaversa]

Is this issue still relevant now that we have crucible? Things have changed quite a bit in the last 3 years.

[atomb]

Yep, these functions no longer exist. Closing!