rtc failure of CursorList

[markro49]

From email of 5/8/2015:

Mark-

The original invariant (in daikon format) is:
DataStructures.CursorList.cursorSpace[0..return].next elements <
size(DataStructures.CursorList.cursorSpace[..])-1

This invariant has 3 parts: 2 expressions and a relationship between them. (Just like "a > b+1" has two expressions and a relationship between them -- but more complicated.)

For this invariant, we have:

expr1 = DataStructures.CursorList.cursorSpace[0..return].next
relation = elements <
expr2 = size(DataStructures.CursorList.cursorSpace[..])-1

Here is what expr1 means:

Consider the array DataStructures.CursorList.cursorSpace[0..return].
Let's call it "a". It has return+1 elements. Each of those elements is of type CursorNode.

Now, consider a new array that is constructed by taking the .next field of each of the CursorNode elements of a. You could make it thus:
nextarray = new int[return+1];
for (int i=0; i<=return; i++)
nextarray[i] = a.next;
but we will just call it "a.next" for brevity, even though of course an array doesn't have a "next" field.

I think expr2 is clear.

Here is what the relation "elements <" means:

The relation takes two arguments: one is an array and one is an int (or float, or whatever).
The relation is true if every element of the array is less than the int. In other words, "a elements < b" can be implemented this way:
for (int i=0; i<a.length; i++)
if (! (a[i] < b))
return false;
return true;

(It is implemented by SeqIntLessThan.)

All of the above should perhaps be better documented in the Daikon manual.
Can you think about whether doing so would improve the manual?

I think I have identified the source of one part of the error. The
method daikon.derive.binary.SequenceSubsequence.jml_name() is being
called on the term "DataStructures.CursorList.cursorSpace[..].next"
and there is no code in the routine to deal with/parse the ".next" term.

JML contains set comprehensions, but it does not contain array comprehensions, which it would need in order to literally translate the Daikon invariant. However, JML can express the invariant in a different syntax that is semantically equivalent:

a.next elements < b

would be expressed in JML as

(\forall int i; 0 < i && i < a.size();
a.get(i).next < b)

This works if you drop off the .next or if you stack more field accesses onto the array.

So, you could use this as the JML translation of the eltsLT invariant.

But there is another problem: what happened to the "elements" part of
the invariant? I am unable to locate any code that scans this term.
I assume it needs to be converted to a "size()" call? Also, does this
mean it should not have been classified as a sequence? In the end, it
is just comparing two integers.

I tried to clarify these issues above. It's all integer comparisons, but multiple of them. Let me know if I should clarify some parts, though.

As an additional note, I am unable to locate any use of
"Quant.collectint" as an output expression.

Do you mean that you don't see how Chicory is producing code that calls it? Or that Daikon doesn't use it? Or that it doesn't appear in the printed representations of any invariants? (It could have been used in the Java-format printed representation of the invariant, I suppose.)

I hope I have gotten at at least some of the confusion; please let me know where I should dig deeper.

Thanks!

                 -Mike

Subject: RE: rtc failure of CursorList
From: "Mark Roberts" markro@cs.washington.edu
To: "'Michael Ernst'" mernst@cs.washington.edu
Date: Thu, 7 May 2015 10:17:04 -0700

I am getting confused and bogged down on this problem.

The original invariant (in daikon format) is:
DataStructures.CursorList.cursorSpace[0..return].next elements <
size(DataStructures.CursorList.cursorSpace[..])-1

It is stored as type daikon.inv.binary.sequenceScalar.SeqIntLessThan
and the first step of outputting the "eltsLT" looks ok.

I think I have identified the source of one part of the error. The
method daikon.derive.binary.SequenceSubsequence.jml_name() is being
called on the term "DataStructures.CursorList.cursorSpace[..].next"
and there is no code in the routine to deal with/parse the ".next" term.

But there is another problem: what happened to the "elements" part of
the invariant? I am unable to locate any code that scans this term.
I assume it needs to be converted to a "size()" call? Also, does this
mean it should not have been classified as a sequence? In the end, it
is just comparing two integers.

As an additional note, I am unable to locate any use of
"Quant.collectint" as an output expression.

Any light you can shed on this would be much appreciated.

Thank you,
Mark

-----Original Message-----
From: Michael Ernst [mailto:mernst@cs.washington.edu]
Sent: Thursday, April 30, 2015 3:54 PM
To: Mark Roberts
Subject: Re: rtc failure of CursorList

Mark-

Thanks for debugging this, and for the clear questions.

The compiler error is that there is no version of eltsLT that accepts
an object array. My thought is the “.next” got lost – that is, the
slice should not be of the Node objects, but of the Node member ‘next’.

I think your analysis is exactly right.

So my question(s): Is the original invariant ok?

Yes, I think it's a correct invariant and Daikon is correct to report it.

When you have an array of objects, is there a way to generate a slice
array of a particular element of that object? What should the
generated code look like?

The produced invariant shows how to do it in Daikon syntax.
For Java syntax, use the Quant.collectInt routine, something like this:
Quant.collectInt(myObjectArray, "next") whose result is of type int[].

Or, I notice that runtimechecker skips a lot of the invariants,
should it be skipping this one?

I think that we can check this one.

I'm not sure why the next field is being skipped (with no call to
collectInt) -- that looks like a bug to me.

                  Thanks,

                 -Mike

Subject: rtc failure of CursorList
From: "Mark Roberts" markro@cs.washington.edu
To: "Michael Ernst " mernst@cs.washington.edu
Date: Thu, 30 Apr 2015 11:33:20 -0700

Hopefully, my explanation will be clear enough that you won’t need
the attached files, but I’ve included them for completeness. Packing list:

CursorList.java – the original source file

Invl1 – the output of PrintInvariants on the generated inv.gz file

Rtc_CursorList.java – the output of the runtimechecker tool

The failure is a compilation error(s) on rtc_CursorList.java. (will
get to the actual error in a bit.)

This is the alloc() method in CursorList:

private static int alloc( )

{

int p = cursorSpace[ 0 ].next;

cursorSpace[ 0 ].next = cursorSpace[ p ].next;

if( p == 0 )

  throw new OutOfMemoryError( );

return p;

}

Here is a section of the discovered invariants:

DataStructures.CursorList.alloc():::EXIT

…

DataStructures.CursorList.cursorSpace[0..return].next elements <
size(DataStructures.CursorList.cursorSpace[])-1

…

Here is the relevant generated code from rtc_CursorList.java:

if (
!(daikon.Quant.eltsLT(daikon.Quant.slice(DataStructures.CursorList.cu
r
sorSpace,
0, retval_instrument),
daikon.Quant.size(DataStructures.CursorList.cursorSpace) - 1)) ). . .

The compiler error is that there is no version of eltsLT that accepts
an object array. My thought is the “.next” got lost – that is, the
slice should not be of the Node objects, but of the Node member ‘next’.

So my question(s): Is the original invariant ok? When you have an
array of objects, is there a way to generate a slice array of a
particular element of that object? What should the generated code
look like? Or, I notice that runtimechecker skips a lot of the
invariants, should it be skipping this one?

Thank you,

Mark