State merging failed due to inequal `quantifiedVariables` with `--conditionalizePermissions`
pieter-bos opened this issue · 3 comments
pieter-bos commented
In this example:
field int: Int
field unrelated: Int
method conv_layer(a: Set[Ref])
requires (forall r: Ref :: r in a ==> acc(r.int, write))
{
label beforeFrame
while (true)
invariant true ==>
(forall r: Ref :: r in a ==> acc(r.int, write)) &&
[
// on inhale
(forperm
obj: Ref [obj.unrelated] :: obj.unrelated ==
old[beforeFrame](obj.unrelated)) &&
(forperm
obj: Ref [obj.int] :: obj.int == old[beforeFrame](obj.int)),
// on exhale
true
]
{ inhale false }
}
Silicon normally reports:
$ ./bin/silicon ~/viper/conditionalize-bug.vpr
silicon 1.1-SNAPSHOT (fe9222fb269d41ab94e642c2ab89e8ceae1903b1@(detached))
silicon finished verification successfully in 3.68s.
But with --conditionalizePermissions
:
$ ./bin/silicon --conditionalizePermissions ~/viper/conditionalize-bug.vpr
silicon 1.1-SNAPSHOT (fe9222fb269d41ab94e642c2ab89e8ceae1903b1@(detached))
Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states:
- Field index quantifiedVariables not equal.
java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states:
- Field index quantifiedVariables not equal.
at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
(...)
at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1622)
at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:165)
Cause: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states:
- Field index quantifiedVariables not equal.
silicon found 1 error in 3.58s:
[0] Verification aborted exceptionally
pieter-bos commented
Don't know if it's useful, but I toyed a bit with the output of --printTranslatedProgram --conditionalizePermissions
, to the point where I un-encoded the conditionalized permissions, and the error is the same (i.e. without --conditionalizePermissions
) -- it thus appears it is not necessarily related to the conditionalized permissions.
field int: Int
field unrelated: Int
method conv_layer(a: Set[Ref])
requires (forall r: Ref :: r in a ==> acc(r.int, write))
{
label beforeFrame
while (true)
invariant
(forall r: Ref :: r in a ==> acc(r.int, write)) &&
(true ==>
[
// on inhale
(forperm obj: Ref [obj.unrelated] ::
obj.unrelated == old[beforeFrame](obj.unrelated)) &&
(forperm obj: Ref [obj.int] ::
obj.int == old[beforeFrame](obj.int)),
// on exhale
true
])
{ inhale false }
}
marcoeilers commented
Thanks for reporting this!
--conditionalizePermissions
only rewrites the AST, so any issue that you get with that option you can also get without.
The same problem can also happen with conditional expressions:
field int: Int
field unrelated: Int
method conv_layer_and(a: Set[Ref])
requires (forall r: Ref :: r in a ==> acc(r.int, write))
{
var x: Int
inhale (forall r: Ref :: r in a ==> acc(r.int, write)) &&
(true ==>
(x > 12) &&
(forperm obj: Ref [obj.int] ::
obj.int == 4)
)
}
method conv_layer_ite(a: Set[Ref])
requires (forall r: Ref :: r in a ==> acc(r.int, write))
{
var x: Int
var y: Int
inhale (forall r: Ref :: r in a ==> acc(r.int, write)) &&
(true ==>
y > 2 ? (x > 12) :
(forperm obj: Ref [obj.int] ::
obj.int == 4)
)
}
marcoeilers commented
Fixed in PR #714