Reject duplicate mir_points_to statements in a precondition

[RyanGlScott]

The LLVM backend tracks writes in a precondition made through llvm_points_to statements and will throw an error if the same location is written to twice. For example:

// test.c
int f(int* x) {
  return *x;
}

m <- llvm_load_module "test.bc";

let f_spec = do {
  x <- llvm_alloc (llvm_int 32);
  llvm_points_to x (llvm_term {{ 27 : [32] }});
  llvm_points_to x (llvm_term {{ 42 : [32] }});

  llvm_execute_func [x];

  llvm_points_to x (llvm_term {{ 27 : [32] }});
};

llvm_verify m "f" [] false f_spec z3;

When SAW symbolically executes f, should it use 27 or 42 as the argument? It's not clear, as the order in which llvm_points_to statements appear is not supposed to matter. Because of this ambiguity, SAW will reject this specification:

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



[18:11:06.147] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[18:11:06.213] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:13:1-13:12)
"f_spec" (/home/ryanscott/Documents/Hacking/SAW/test.saw:13:28-13:34)
Multiple points-to preconditions on same pointer

The Multiple points-to preconditions on same pointer check is not currently implemented for the MIR backend, however. SAW does verify this program:

// test.rs
pub fn f(x: &u32) -> u32 {
    *x
}

enable_experimental;

m <- mir_load_module "test.linked-mir.json";

let f_spec = do {
  x <- mir_alloc mir_u32;
  mir_points_to x (mir_term {{ 27 : [32] }});
  mir_points_to x (mir_term {{ 42 : [32] }});

  mir_execute_func [x];

  mir_points_to x (mir_term {{ 27 : [32] }});
};

mir_verify m "test::f" [] false f_spec z3;

But this is brittle: the only reason that this works is that SAW just so happens to order the side effectful operations in the precondition such that 27 is the last value written to x before invoking the symbolic simulator. If 42 had instead been the last value written, this this would have failed.

This issue exists to track the idea of porting the LLVM backend's duplicate points_to check over to the MIR backend. Note that we will need to be careful in how this interacts with the mir_ref_value command, as mir_ref_value is meant to allocate and initialize a reference. We want to ensure that the initialization step (1) happens before any mir_points_to statements are executed, and (2) is ignored by the duplicate check.