Non-Determinism for Java objects in JBMC

20 views
Skip to first unread message

Michael

unread,
Dec 16, 2019, 7:34:23 AM12/16/19
to CProver Support
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

unread,
Dec 16, 2019, 12:35:30 PM12/16/19
to cprover...@googlegroups.com
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


Reply all
Reply to author
Forward
0 new messages