Java: invariant masked by overflow condition (no exceptions) ?

[wilsondy]

java version "1.8.0_131" Java(TM) SE Runtime Environment (build 1.8.0_131-b11) Java HotSpot(TM) 64-Bit Server VM (build 25.131-b11, mixed mode)
Darwin Dylans-MBP.localdomain 19.6.0 Darwin Kernel Version 19.6.0: Mon Aug 31 22:12:52 PDT 2020; root:xnu-6153.141.2~1/RELEASE_X86_64 x86_64
Compile per your preference...

java -cp target/classes:target/test-classes:$DAIKONDIR/daikon.jar daikon.Chicory --daikon --ppt-select-pattern=org\.joda\.time\.field\.FieldUtils org.junit.runner.JUnitCore org.joda.time.field.TestFieldUtils

0
0
0
0
letting overflow go... 
0
0
letting overflow go... 
0
0
0
0
0
0
0
0
letting overflow go... 
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
letting overflow go... 
0
0
0
0
0
0
0
0
0
0
Count: 20
Chicory warning: ClassFile: org.junit.runner.notification.RunNotifier$9 - classfile version (49) is out of date and may not be processed correctly.
Chicory warning: ClassFile: org.junit.runner.notification.RunNotifier$4 - classfile version (49) is out of date and may not be processed correctly.
Chicory warning: ClassFile: org.junit.runner.notification.RunNotifier$2 - classfile version (49) is out of date and may not be processed correctly.

Time: 0.086

OK (1 test)


Daikon version 5.8.5, released July 22, 2020; http://plse.cs.washington.edu/daikon.
Reading declaration files Processing trace data; reading 1 dtrace file:

===========================================================================
org.joda.time.field.FieldUtils.safeAdd(long, long):::ENTER
val1 != val2
===========================================================================
org.joda.time.field.FieldUtils.safeAdd(long, long):::EXIT
return != orig(val1)
return != orig(val2)
===========================================================================
org.joda.time.field.FieldUtils.safeAdd2(long,long):::ENTER
val1 != val2
===========================================================================
org.joda.time.field.FieldUtils.safeAdd2(long, long):::EXIT
return != orig(val1)
return != orig(val2)
return - orig(val1) - orig(val2) == 0
Exiting Daikon.

What you expected to happen:
testSafeAdd Invariant should equal testSafeAdd2 (particularly return - orig(val1) - orig(val2) == 0
as we see no indication this invariant was violated even in the overflow conditions...

Source attached SOURCE.zip
Thank you!

[mernst]

I cannot compile the files you provided, because they use libraries you have not provided.

In particular, I ran these commands:

wget https://github.com/codespecs/daikon/files/5557337/SOURCE.zip
unzip SOURCE.zip
javac time93b/src/main/java/org/joda/time/field/FieldUtils.java time93b/src/test/java/org/joda/time/field/TestFieldUtils.java

The result is a torrent of compilation errors such as

time93b/src/main/java/org/joda/time/field/FieldUtils.java:18: error: cannot find symbol
import org.joda.time.DateTimeField;
                    ^
  symbol:   class DateTimeField
  location: package org.joda.time

I could guess at what command you ran, and guess at what jar files you used, but I might end up doing something differently than you did.

Can you please provide the missing files and the missing commands?
If you can provide a set of commands that can be pasted into a shell, that would be most useful and reproducible.
Thanks!

[mernst]

By the way, this is just a guess, but maybe this issue is actually a feature request for a mode in which integer overflow is ignored. Daikon does all computation in long values. Thus, even though Java might output true for Integer.MIN_VALUE = Integer.MAX_VALUE + 1, it is not true (in reality, nor in the longs where Daikon operates) that 2147483647 + 1 = -2147483648.

[mernst]

Ping: could you please provide the missing files and the missing commands?
Thanks!

[wilsondy]

Here's a simplified test case. Covers both longs and ints and has exact same code where we trigger and don't trigger overflow and see the differences in invariants discovered.
I guess it comes down to what the invariant is speaking to: the mathematical definition or the java execution reality. In the overflow case, in Java, the invariant is still true. Perhaps it's fine as is, but it limits the invariants you can discover with the tool and creates (for me) an unintuitive gap based solely on the input values and not the source code.
Main.java.zip
javac Main.java
java -cp .:$DAIKONDIR/daikon.jar daikon.Chicory --daikon Main

Latest output

entered daikon.chicory.Runtime.setDtrace(./Main.dtrace.gz, false)...
0
0
0
0
0
0
0
0
letting int overflow go... 
------ Even with overflow, invariant holds
0
0
0
0
letting int overflow go... 
------ Even with overflow, invariant holds
0
0
letting long overflow go... 
------ Even with overflow, invariant holds
letting int overflow go... 
------ Even with overflow, invariant holds
0
0
0
0
letting long overflow go... 
------ Even with overflow, invariant holds
0
0
letting long overflow go... 
------ Even with overflow, invariant holds
letting int overflow go... 
------ Even with overflow, invariant holds
0
0
0
0
letting long overflow go... 
------ Even with overflow, invariant holds
0
0
letting long overflow go... 
------ Even with overflow, invariant holds
letting int overflow go... 
------ Even with overflow, invariant holds
0
0
0
0
0
0
0
0
0
0
0
0
0
0
Count: 20
Daikon version 5.8.5, released July 22, 2020; http://plse.cs.washington.edu/daikon.
Reading declaration files Processing trace data; reading 1 dtrace file:

===========================================================================
Main.main(java.lang.String[]):::ENTER
args has only one value
args.getClass().getName() == java.lang.String[].class
args[] == []
args[].toString == []
===========================================================================
Main.main(java.lang.String[]):::EXIT
args[] == orig(args[])
args[] == []
args[].toString == []
===========================================================================
Main.safeAddInts(int, int):::ENTER
val1 != val2
===========================================================================
Main.safeAddInts(int, int):::EXIT
return != orig(val1)
return != orig(val2)
===========================================================================
Main.safeAddIntsNoOverflowTriggered(int, int):::ENTER
val1 != val2
===========================================================================
Main.safeAddIntsNoOverflowTriggered(int, int):::EXIT
return != orig(val1)
return != orig(val2)
return - orig(val1) - orig(val2) == 0
===========================================================================
Main.safeAddLong(long, long):::ENTER
val1 != val2
===========================================================================
Main.safeAddLong(long, long):::EXIT
return != orig(val1)
return != orig(val2)
===========================================================================
Main.safeAddLongNoOverflowTriggered(long, long):::ENTER
val1 != val2
===========================================================================
Main.safeAddLongNoOverflowTriggered(long, long):::EXIT
return != orig(val1)
return != orig(val2)
return - orig(val1) - orig(val2) == 0
Exiting Daikon.