MIR/JVM: Enforce disjointness of postcondition allocations from precondition allocations and statics

[qsctr]

The MIR backend has the same unsoundness issues for allocations as the LLVM backend did in #641 and #642.

A MIR port of the unsound example in #641:

pub fn foo(x: *const u64) -> *const u64 {
    x
}

pub fn bar(x: *const u64) -> bool {
    x == foo(x)
}

enable_experimental;

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

let foo_spec = do {
    x <- mir_alloc_raw_ptr_const mir_u64;
    mir_execute_func [x];
    y <- mir_alloc_raw_ptr_const mir_u64;
    mir_return y;
};

foo_ov <- mir_verify m "test::foo" [] false foo_spec z3;

let bar_spec0 = do {
    x <- mir_alloc_raw_ptr_const mir_u64;
    mir_execute_func [x];
    mir_return (mir_term {{ False }});
};

mir_verify m "test::bar" [foo_ov] false bar_spec0 z3;

let bar_spec1 = do {
    x <- mir_alloc_raw_ptr_const mir_u64;
    mir_execute_func [x];
    mir_return (mir_term {{ True }});
};

mir_verify m "test::bar" [] false bar_spec1 z3;

A MIR port of the unsound example in #642 using mutable statics, by @RyanGlScott:

// test.rs
static mut GLOB: u32 = 0;

pub fn foo(x: *mut u32) -> bool {
 x == &raw mut GLOB
}

pub fn bar() -> bool {
 foo(&raw mut GLOB)
}

// test.saw
enable_experimental;

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

foo_ov <-
  mir_verify m "test::foo" [] false
    do {
      glob_contents <- mir_fresh_var "GLOB" mir_u32;
      mir_points_to (mir_static "test::GLOB") (mir_term glob_contents);
      x <- mir_alloc_raw_ptr_mut mir_u32;
      x_contents <- mir_fresh_var "x" mir_u32;
      mir_points_to x (mir_term x_contents);

      mir_execute_func [x];

      mir_points_to (mir_static "test::GLOB") (mir_term glob_contents);
      mir_points_to x (mir_term x_contents);
      mir_return (mir_term {{ False }});
    }
    z3;

bar_ov0 <-
  mir_verify m "test::bar" [foo_ov] false
    do {
      glob_contents <- mir_fresh_var "GLOB" mir_u32;
      mir_points_to (mir_static "test::GLOB") (mir_term glob_contents);

      mir_execute_func [];

      mir_points_to (mir_static "test::GLOB") (mir_term glob_contents);
      mir_return (mir_term {{ False }});
    }
    z3;

bar_ov1 <-
  mir_verify m "test::bar" [] false
    do {
      glob_contents <- mir_fresh_var "GLOB" mir_u32;
      mir_points_to (mir_static "test::GLOB") (mir_term glob_contents);

      mir_execute_func [];

      mir_points_to (mir_static "test::GLOB") (mir_term glob_contents);
      mir_return (mir_term {{ True }});
    }
    z3;

The same thing but with immutable statics:

// test.rs
static GLOB: u32 = 0;

pub fn foo(x: *const u32) -> bool {
 x == &raw const GLOB
}

pub fn bar() -> bool {
 foo(&raw const GLOB)
}

// test.saw
enable_experimental;

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

foo_ov <-
  mir_verify m "test::foo" [] false
    do {
      x <- mir_alloc_raw_ptr_const mir_u32;
      x_contents <- mir_fresh_var "x" mir_u32;
      mir_points_to x (mir_term x_contents);

      mir_execute_func [x];

      mir_return (mir_term {{ False }});
    }
    z3;

bar_ov0 <-
  mir_verify m "test::bar" [foo_ov] false
    do {
      mir_execute_func [];

      mir_return (mir_term {{ False }});
    }
    z3;

bar_ov1 <-
  mir_verify m "test::bar" [] false
    do {
      mir_execute_func [];

      mir_return (mir_term {{ True }});
    }
    z3;

All three of these examples are currently successfully verified by SAW, but prove different results for bar with and without the override for foo.

This can be fixed by doing a similar thing for MIR as was done for LLVM in #752 and #826: make sure that each postcondition allocation is disjoint from the precondition allocations and static allocations, in addition to each other postcondition allocation. Note that according to #641 (comment) it seems like the LLVM backend did not face this issue for const globals due to how the crucible-llvm memory model works; however, as shown by the third test case above, fixing this for the MIR backend would require handing both mutable and immutable statics.

The JVM backend also lacks these additional disjointness checks, so it might be affected by this as well, but I haven't investigated this.

[RyanGlScott]

The JVM backend also lacks these additional disjointness checks, so it might be affected by this as well, but I haven't investigated this.

Some investigation reveals that unlike the LLVM and MIR backends, the JVM backend doesn't have distinct notions of global allocations versus input allocations. For instance, I attempted to adapt the test case from #642 to use the JVM backend:

// Bug2.java
public class Bug2 {
    static class C {}

    static C GLOB;

    public static boolean foo(C x) {
        return x.equals(GLOB);
    }

    public static boolean bar() {
        return foo(GLOB);
    }
}

// bug2.saw
cls <- java_load_class "Bug2";

let foo_spec = do {
    c <- jvm_alloc_object "Bug2$C";
    jvm_static_field_is "GLOB" c;
    x <- jvm_alloc_object "Bug2$C";

    jvm_execute_func [x];

    jvm_static_field_is "GLOB" c;
    jvm_return (jvm_term {{ False }});
};

foo_ov <- jvm_verify cls "foo" [] false foo_spec z3;

let bar_spec0 = do {
    c <- jvm_alloc_object "Bug2$C";
    jvm_static_field_is "GLOB" c;

    jvm_execute_func [];

    jvm_static_field_is "GLOB" c;
    jvm_return (jvm_term {{ False }});
};

jvm_verify cls "bar" [foo_ov] false bar_spec0 z3;

let bar_spec1 = do {
    c <- jvm_alloc_object "Bug2$C";
    jvm_static_field_is "GLOB" c;

    jvm_execute_func [];

    jvm_static_field_is "GLOB" c;
    jvm_return (jvm_term {{ True }});
};

jvm_verify cls "bar" [] false bar_spec1 z3;

Fortunately, the JVM backend rejects this:

$ javac Bug2.java
$ saw bug2.saw
[12:34:42.639] Loading file "/home/rscott/Documents/Hacking/Java/bug2.saw"
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[12:34:42.758] Proof succeeded! foo
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[12:34:42.886] Stack trace:
"jvm_verify" (/home/rscott/Documents/Hacking/Java/bug2.saw:27:1-27:11)
Symbolic execution failed.
Abort due to assertion failure:
  /home/rscott/Documents/Hacking/Java/bug2.saw:27:1: error: in overrideBranches
  no override specification applies for foo

On the other hand, the JVM backend is susceptible to the same bug seen in #641. Here is a variant of the test case from #641 that uses the JVM backend:

// Bug1.java
public class Bug1 {
    static class C {}

    static C foo(C x) {
        return x;
    }

    static boolean bar(C x) {
        return x.equals(foo(x));
    }
}

// bug1.saw
cls <- java_load_class "Bug1";

let foo_spec = do {
    x <- jvm_alloc_object "Bug1$C";
    jvm_execute_func [x];
    y <- jvm_alloc_object "Bug1$C";
    jvm_return y;
};

foo_ov <- jvm_verify cls "foo" [] false foo_spec z3;

let bar_spec0 = do {
    x <- jvm_alloc_object "Bug1$C";
    jvm_execute_func [x];
    jvm_return (jvm_term {{ False }});
};

jvm_verify cls "bar" [foo_ov] false bar_spec0 z3;

let bar_spec1 = do {
    x <- jvm_alloc_object "Bug1$C";
    jvm_execute_func [x];
    jvm_return (jvm_term {{ True }});
};

jvm_verify cls "bar" [] false bar_spec1 z3;

SAW currently accepts this, but it shouldn't:

$ javac Bug1.java
$ saw bug1.saw
[12:36:44.453] Loading file "/home/rscott/Documents/Hacking/Java/bug1.saw"
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[12:36:44.520] Proof succeeded! foo
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[12:36:44.640] Proof succeeded! bar
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[12:36:44.713] Proof succeeded! bar

As such, the JVM backend needs a similar fix as well.