Array copy set prep

[andreistefanescu]

No description provided.

[robdockins]

Some minor comments on the code. Let's add changelogs and documentation and such for these new options.

[robdockins]

Let's open ticket about plumbing this new option through the RPC server.

[RyanGlScott]

For what it's worth, it's fairly easy to add support for toggling options like this in saw-remote-api. You basically just add a new constructor here, and then update the code in setOption, parseOption, and instance Doc.DescribedMethod SetOptionParams OK accordingly.

[RyanGlScott]

For what it's worth, it's fairly easy to add support for toggling options like this in saw-remote-api. You basically just add a new constructor here, and then update the code in setOption, parseOption, and instance Doc.DescribedMethod SetOptionParams OK accordingly.

[RyanGlScott]

I'm curious: does this work in practice when you apply in an a specification that is assumed with llvm_unsafe_assume_spec? The reason I ask is that I'm doing something quite similar to this as part of ongoing work in #1461, and I couldn't make it work without making some nontrivial changes to the way doInvalidate works in crucible.

I suppose this is a long-winded way of asking for some more test cases using llvm_alloc_sym_init. I'm not sure if you plan to do this as part of this PR or as part of a later PR, however.

[robdockins]

I think we need to fix this case; or perhaps the proper fix is elsewhere, I'm not sure exactly.

At any rate, if we assume in a specification that an allocation is backed by symbolic bytes, then that incurs a proof obligation at call sites to ensure that the affected memory can actually be read, and I don't see where that is being checked.

[andreistefanescu]

This is by design. Similar to what @RyanGlScott is working on, this changes the semantics of memory reads such that there are always some bytes. This is not the same as the combination of llvm_alloc and llvm_points_to_array_prefix. I will update the description to make it more clear.

[robdockins]

That doesn't seem right. This isn't a global option, it's a per-spec and per-allocation. I can use llvm_alloc in some places and llvm_alloc_sym_init in some other places, right?

In that case, llvm_alloc_sym_init incurs an obligation we have to check for, because it isn't universal.

[robdockins]

Consider the following program:

#include <stdlib.h>

int g (int* x) {
  return *x;
}

int f (void)  {
  int *x = (int*) malloc( sizeof(int) );
  return g(x);
}

And the following script:

enable_experimental;

m <- llvm_load_module "syminit.bc";

let f_spec = do {
  llvm_execute_func[];
  v <- llvm_fresh_var "v" (llvm_int 32);
  llvm_return (crucible_term v);
};


let g_spec = do {
  x <- llvm_alloc_sym_init (llvm_int 32);
  llvm_execute_func [x];
  v <- llvm_fresh_var "v" (llvm_int 32);
  llvm_return (crucible_term v);
};

g_thm <- llvm_verify m "g" [] false g_spec z3;

llvm_verify m "f" [g_thm] false f_spec z3;
llvm_verify m "f" [] false f_spec z3;

On this branch, the verification of f properly fails if given no overrides; it claims that there is no write that satisfies the read in line 4 of this program, as it should.

However, if I pass it the g_thm, which was proved assuming that the input to g has backing symbolic bytes, the verification goes through, and this represents a soundess bug.

[robdockins]

Latest patch addresses my soundness concern; the user must take deliberate action to weaken the check.

I'd like to see a little more information in the documentation about what disabling that check means, but otherwise I am happy.