JBMC cant handle aliasing

[JonasKlamroth]

JBMC version: 5.32.1 (cbmc-5.32.1-10-gb84b37dea)
Operating system: Ubuntu 20.04.2 LTS
Exact command line resulting in the issue: ./jbmc Test --function Test.test
What behaviour did you expect: Verification should fail because of the "assert false"
What happened instead: Verification was sucessful

Above information are the result given the following content of Test.java:

import org.cprover.CProver;
 
public class Test {
    private void test(Object o1, Object o2) {
        CProver.assume(o1 == o2 && o1 != null);
        assert false;
    }
}

I assume this is the result of non deterministic objects being treated as new objects with nondeterministic fields, which is implicitly makes the assumption that those objects cannot alias. Is there a way to prevent this behavior? Are there plans to implement this in the future?

[NlightNFotis]

Paging @tautschnig @kroening who might know more about this.

[peterschrammel]

This is a known issue, and there are currently no concrete plans to fix this.
In the meanwhile, you can work around it by encoding the desired behavior yourself, e.g.

import org.cprover.CProver;
 
public class Test {
    private void entryPoint(Object o1, Object o2, boolean equal) {
      if (equal) {
        o2 = o1;
      }
      test(o1, o2);
    }

    private void test(Object o1, Object o2) {
        CProver.assume(o1 == o2 && o1 != null);
        assert false;
    }
}

and then run jbmc Test.entryPoint.

[JonasKlamroth]

Thank you for the workaround.

I thought about trying to implement this myself. Can you estimate the complexity of this endeavor? If you think it can be done with reasonable effort: Can you point me to a good place to start?

[martin-cs]

Complexity : Assuming you have a reasonable level of familiarity with the code / this kind of tool then the changes are not actually that difficult in this case but the general case is probably a bit harder. Configuring it could be a little tricky.

Plan of attack...

1. Get comfortable building cbmc from source. export CXXFLAGS="-O0 -g"; export LINKFLAGS=-rdynamic; is your friend. So is rr.
2. Run the regression and unit tests so you know when you have broken things.
3. Do 1 and 2 for jbmc as well.
4. Use --show-goto-functions to show you the calling context that is auto-generated. This should give you a way of seeing what the effect of your changes are.
5. Compile up what you want your auto-generated calling context to be and use --show-goto-functions to look at the differences between the two.
6. Write a bunch of test cases and integrate them into the test suite.
7. Aim your debugger here

   cbmc/src/goto-programs/initialize_goto_model.cpp

   Line 36 in 2e3ba57

   static bool generate_entry_point_for_function(

8. You might want to experiment with the C entry point code first https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/ansi_c_entry_point.cpp see if you can just add some instructions or spurious variables. Changes should be visible via --show-goto-functions
9. Then have a go with

   cbmc/jbmc/src/java_bytecode/java_bytecode_language.cpp

   Line 1056 in 2e3ba57

   bool java_bytecode_languaget::generate_support_functions(

HTH

[JonasKlamroth]

Thank you. I will take a look at it.