Dafny version
4.11.0
Code to produce this issue
This is a language-interface issue, so reproduction requires a Java file and a Dafny file. In BoxPkg/Box.java:
public class Box {
public BigInteger v;
/** Factory: each call allocates a fresh, distinct object. */
public static Box Make(BigInteger v) {
Box b = new Box();
b.v = v;
return b;
}
/** Mutate the wrapped (hash-relevant) value. */
public void setVal(BigInteger v) {
this.v = v;
}
@Override
public boolean equals(Object other) {
return other instanceof Box && this.v.equals(((Box) other).v);
}
@Override
public int hashCode() {
return v.intValue();
}
}And in BoxUnsound.dfy:
module {:compile false} {:extern "BoxPkg"} BoxPkg {
class {:extern "Box"} Box {
static method {:extern "Make"} {:axiom} Make(v: int) returns (b: Box)
ensures fresh(b)
method {:extern "setVal"} SetVal(v: int)
modifies this
}
}
module Repro {
import opened BoxPkg
// BUG 1: structural equals() makes the compiled set identify two physically
// distinct objects, contradicting the verified cardinality.
method DemoCollision() {
var a := Box.Make(1);
var b := Box.Make(1); // distinct object, equal value
assert a != b; // verified: two distinct fresh references
var s := {a, b};
assert |s| == 2; // verified from a != b, false at runtime
print "[collision] verified |s| == 2, but runtime |s| = ", |s|, "\n";
}
// BUG 2: hashCode() tracks the mutable value, so mutating it moves the object
// to a different bucket and the compiled set can no longer find a member the
// model still says is present.
method DemoDiscontinuity() {
var p := Box.Make(1);
var s := { p };
p.SetVal(2); // change the (hash-relevant) value
assert p in s; // verified: the set is keyed by reference
print "[discontinuity] verified (p in s) == true, but runtime = ", p in s, "\n";
}
method Main() {
DemoCollision();
DemoDiscontinuity();
}
}Command to run and resulting output
dafny run BoxUnsound.dfy --target:java --input BoxPkg/Box.java
What happened?
I get this output:
Dafny program verifier finished with 3 verified, 0 errors
[collision] verified |s| == 2, but runtime |s| = 1
[discontinuity] verified (p in s) == true, but runtime = false
It shows that in each demo method in the Dafny source, the verifier proves an expression which is false at runtime.
The extern Java class Box, unbeknownst to Dafny, overrides equals() and hashCode(), rendering Dafny's model of set<Box> unsound.
There should be a way to create a sound model of Box in Dafny without changing the Java source. The default behaviors of equals() and hashCode() are available even for Java classes which override them through == and System.identityHashCode(). If the Java implementation of set<Box> used the latter two, rather than their overridden alternatives, the unsoundness would disappear.
EDIT: admittedly, assuming every generic is a reference type would cause unexpected behavior from, e.g., set<int>, so this is a complicated issue.
What type of operating system are you experiencing the problem on?
Mac
Dafny version
4.11.0
Code to produce this issue
This is a language-interface issue, so reproduction requires a Java file and a Dafny file. In
BoxPkg/Box.java:And in
BoxUnsound.dfy:Command to run and resulting output
What happened?
I get this output:
It shows that in each demo method in the Dafny source, the verifier proves an expression which is false at runtime.
The extern Java class
Box, unbeknownst to Dafny, overridesequals()andhashCode(), rendering Dafny's model ofset<Box>unsound.There should be a way to create a sound model of
Boxin Dafny without changing the Java source. The default behaviors ofequals()andhashCode()are available even for Java classes which override them through==andSystem.identityHashCode(). If the Java implementation ofset<Box>used the latter two, rather than their overridden alternatives, the unsoundness would disappear.EDIT: admittedly, assuming every generic is a reference type would cause unexpected behavior from, e.g.,
set<int>, so this is a complicated issue.What type of operating system are you experiencing the problem on?
Mac