Bug: unnecessary UNKNOWN for bitwiseAnd/bitwiseOr

[FahrJo]

Basic Info

• Version: 0.2.3-dev-625b118-m
• (Optional) Java Version: 11.0.21
• Input file:

extern int __VERIFIER_nondet_int(void);
void main(void) {
    int data1 = 0;
    int data2 = 0;
    int test = 0;

    /* In the following, the issue is broken down to minimal test cases. */
    /* This bitwise OR is okay... */
    data1 |= 1;
    data2 &= 1;

    /* But as soon as the right side is larger then 1, Ultimate will return UNKNOWN */
    data1 |= 2;
    data2 &= 2;

    if(__VERIFIER_nondet_int()) test = 1;
    //@ assert (test == 1);
}

• Settings & Toolchain: Archiv.zip

Description

Ultimate fails to prove the program to be incorrect and returns unknown:

Unable to prove that assertion always holds
 Reason: overapproximation of bitwiseOr at line 13, overapproximation of bitwiseAnd at line 14.

I cannot explain myself, why those simple bitwise AND/OR operations should cause a problem. Is this reasonable?

[schuessf]

This is expected. We can model the C-program by using mathematical and unbounded integers (integer translation), but then we loose the bitprecise information. Therefore we cannot handle bitwise precisely in general, but we have try to be as precise as possible for several cases. For example data2 &= 1 is equivalent to data2 %= 2 (which we can handle precisely), so we model it similarly. data2 &= 2 cannot be handled in such a simple way, so we just overapproximate it, i.e. we don't model the precise value. To keep our analysis sound, we say unknown, if the counterexample contains an overapproximation, because the error might only be reached with our imprecise handling. However, there is also a setting to translate bitprecise using bitvectors.

But you are right in the way that this overapproximation here is unnecessary. The error found is an actual error, because it does not even use the possibly imprecise value of the bitprecise operations. In general this detection might be slightly more complicated, but this is someting we are currently working on.

[FahrJo]

Alright, thanks for clarification.

[danieldietsch]

@FahrJo Did you try it with bitvector translation?

[FahrJo]

@FahrJo Did you try it with bitvector translation?

I just tried with the cacsl2boogietranslator setting /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Bitprecise\ bitfields=true but it still fails (see ultimate.log)

[schuessf]

This is not the correct setting, use /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ bitvectors\ instead\ of\ ints=true instead.

[FahrJo]

I just found this, @schuessf. Unfortunately this throws an exception:

 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - ExceptionOrErrorResult: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Unsupported internal sort: (_ BitVec 32)
    de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Unsupported internal sort: (_ BitVec 32): de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.TraceCheck.<init>(TraceCheck.java:236)
RESULT: Ultimate could not prove your program: Toolchain returned no result.

[schuessf]

Oh, yes, this requires to change some other settings as well. I think the best idea is just to load predefined settings (for example examples/settings/default/automizer/svcomp-Reach-32bit-Automizer_Bitvector.epf) and adapt them to your needs.

[FahrJo]

Ok, after adding the suggested settings for the traceabstraction, everything works. I leave the issue open though, since the overapproximation here is unnecessary anyways. I adjusted the issue title.