Non-Determinism for Java objects in JBMC

[Michael]

Hi there,

I have a question regarding the semantics of non-determinism in JBMC.
I understood that the API methods

nondetWithNull()

and

nondetWithoutNull()

non-deterministically initialize object references that may or may not be null.

However, it seems that this non-determinism does not cover references of
objects that were created before the call of such API methods.

So my question(s) is/are the following:
Is this the intended behaviour or rather not? If this is intended, is there also a way
to model non-determinism that includes objects that were created beforehand?

As an example, in the following there are two assertions for which JBMC does not seem to find any violating traces

(i.e., JBMC outputs "VERIFICATION SUCCESSFUL"), however I would like to be able to make use of

non-determinism that allows traces violating both assertions.

import org.cprover.CProver;

public class JbmcTests {
    JbmcTests t = null;
    JbmcTests t2 = null;

    public void test2(){
        JbmcTests local = new jbmcTests();
        t = CProver.nondetWithNull();
        assert local != t;
    }

    public void test3(){
        t = new JbmcTests();
        t2 = CProver.nondetWithNull();
        assert t2 != t;
    }
}

Thank you and best regards,

Michael

[Martin Nyx Brain]

On Mon, 2019-12-16 at 04:34 -0800, Michael wrote:
> Hi there,
>
> I have a question regarding the semantics of non-determinism in JBMC.
> I understood that the API methods
> nondetWithNull()
> and
> nondetWithoutNull()
> non-deterministically initialize object references that may or may
> not be
> null.

I have not had too much to do with the internals of the JVM front-end
but from what I know it creates a new object, non-deterministically
"assigns" fields and returns the reference to that object (or null).

> However, it seems that this non-determinism does not cover references
> of
> objects that were created before the call of such API methods.

As I understand it, yes, it creates a new object rather than non-
determinism over existing objects of the correct type.

> So my question(s) is/are the following:
> Is this the intended behaviour or rather not?

I suspect it is the intended behaviour. It would be the nearest analog
of how non-determinism is introduced in the C front-end.

> If this is intended, is there
> also a way
> to model non-determinism that includes objects that were created
> beforehand?

Not that I am aware of. You could model it by collecting the
previously allocated objects in an array and then nondeterministically
calling nondetWith*Null() or using the object at a nondeterministic
index.

> As an example, in the following there are two assertions for which
> JBMC
> does not seem to find any violating traces
> (i.e., JBMC outputs "VERIFICATION SUCCESSFUL"), however I would like
> to be
> able to make use of
> non-determinism that allows traces violating both assertions.
>
> import org.cprover.CProver;
>
> public class JbmcTests {
> JbmcTests t = null;
> JbmcTests t2 = null;
>
> public void test2(){
> JbmcTests local = new jbmcTests();
> t = CProver.nondetWithNull();
> assert local != t;
> }
>
> public void test3(){
> t = new JbmcTests();
> t2 = CProver.nondetWithNull();
> assert t2 != t;
> }
> }

Thank you for the code examples; these are always helpful.

public void test3() {
t = new JbmcTests();

t2 = (CProver.nondetBoolean()) ? t : CProver.nondetWithNull();
assert t2 != t;
}

might do what you want.

Cheers,
- Martin