State merging failed due to inequal `quantifiedVariables` with `--conditionalizePermissions`

[pieter-bos]

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]

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]

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]

Fixed in PR #714