identifier __CPROVER_memory not found

[peterschrammel]

Hello,

current CBMC master crashes on the attached Java program (distilled
from production code).

Thanks,

Vladimir Klebanov

---

CBMC version 5.4 64-bit x86_64 linux
Parsing Driver.class
Java main class: Driver
failed to load class java.lang.String' failed to load classjava.lang.Object'
failed to load class java.lang.Class' failed to load classjava.lang.AssertionError'
Converting
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
**** WARNING: no body for function
java::java.lang.Class.desiredAssertionStatus:()Z
**** WARNING: no body for function java::java.lang.Object.:()V
**** WARNING: no body for function java::java.lang.AssertionError.:()V
file Driver.java line 50: identifier __CPROVER_memory not found

public class Driver {

    static byte[] out,in;

    public static void main(String[] argv) {

        X x = new X();
        x.y(out);

    }

}

final class X {

    private static final int DIGEST_SIZE = 20;
    private transient MyMessageDigest digest;
    private byte[] state;

    public X() {
        init(null);
    }

    private void init(byte[] seed) {
        digest = new MyMessageDigest();

        if (seed != null) {
            state = digest.digest(seed);
        }
    }

    public synchronized void y(byte[] result) {
        byte[] output = digest.digest();
    }
}


class MyMessageDigest {

    private byte[] state = null;


    public void update(byte[] input) {
        assert(input.length == 20);
        state = input;
    }


    public byte[] digest() {
        byte[] tmp = state;
        state = null;
        return tmp;
    }

    public byte[] digest(byte[] input) {
        update(input);
        return digest();
    }


}

[vladrich]

Thanks. I now see that this is a duplicate of #161. Sorry about that.

[peterschrammel]

We have a patch that fixes the problem in one of our branches. We'll distil a PR for it asap.

[smowton]

Looks like the principle cause is implicit pointer casting between void* and struct Driver* introducing a byte-extract operation and thus pointer-analysis uncertainty and the possibility that the pointer is an integer address (i.e. something like *(char*)5, which is obviously not possible in Java). I have a patch in my branch that tries to make all pointer casts explicit which I'll try to extract tomorrow.

[smowton]

smowton@5787def fixes this particular case by ensuring all pointer-casting is explicit, and so bytewise reinterpret opcodes are not generated. There may however be other cases where the value set analysis conflates integer and pointer members of the same struct which would lead to the same problem recurring; if that happens we should consider making the pass aware that the source language can't express raw integer addresses, and so in this case anything that would use __CPROVER_memory can be silently discarded.

[vladrich]

Thanks for looking at this, Chris. I grafted your patch onto current master and it does prevent the crash. Verification of the particular benchmark now completes, but the results are surprising to me. At the moment, I cannot say if this is a genuine finding or some misunderstanding of mine. I will investigate the issue.

[vladrich]

The problem no longer occurs with current master (518124c). Thanks.

[smowton]

Per https://github.com/diffblue/verification-engine-utils/issues/173 there are more cases where this can happen; therefore __CPROVER_memory refs are disabled entirely in smowton@733b753

[smowton]

(Just a note this should be review/QA but I don't have the right to do that on the CBMC tracker)

[smowton]

Created #335 to try to get this either integrated or commented upon.