Infinite loop when resolving variables.

[icmccorm]

During variable resolution in the backend, the following call to foldRight on line 176 of supporters/Translator.scala triggers an infinite loop. This can be replicated using the following program:
err.txt

pcsEquivalentVariables.foldRight[Option[ast.Exp]](None)(
 (term, potentialResolvedVariable) =>
   potentialResolvedVariable match {
     case Some(_) => potentialResolvedVariable
     case None    =>
       // Attempt normal variable resolution (looking in
       // both heaps, followed by the store)
       regularVariableResolver(term) match {
         case Some(resolvedVariable) => Some(resolvedVariable)
         // Attempt regex variable resolution (we only look
         // in the store; the rest is constructed via a regex)
         //
         // Use caution here!
         case None => regexVariableResolver(term)
       }
   }
}

[jennalwise]

Infinite loop is happening in tree_add_right at line 170 where fix_up_ancestors(...) is called. I am not sure why the translator is invoked in this case, but either way this illustrates an issue in the translator.

The heap contains node@2@01.Node$right -> n@11@01 # W, n@11@01.Node$parent -> node@2@01 # W. So when the Translator is trying to resolve node@2@01, it first starts by looking in the heap for node@2@01 and finds n@11@01.Node$parent. Then, the Translator tries to resolve n@11@01 by looking in the heap first and finds node@2@01.Node$right -> n@11@01 # W. So, it then tries to resolve node@2@01 again and so forth. With the changes I needed to make to the translator here: https://github.com/gradual-verification/silicon-gv/commit/aed82926443e2cbfc83f1e55866171e83f76b23b to resolve issue https://github.com/gradual-verification/silicon-gv/issues/29 an infinite loop as described above is created in this case.

My proposed solution is to in the regularVariableResolver look up in the store first before checking either of the heaps. Since store.getKeyForValue has been updated to handle cases like (First: … (Second: …)), this solution should work for those cases as well.

Solution would not work for a heap that looks like this, unless x’.f -> x.f’ is chosen: { x.f’.g -> t’, t’.h -> x.f’ , x’.f -> x.f’ }

The problem here boils down to not dealing with aliasing between the store and heap and within the heap properly. My first proposed solution addresses the problem for aliasing between the store and the heap. To address aliases in the heap (including optimisticHeap) outline of strategy is to:

1. Try to resolve first alias while keeping track of what is being resolved
2. If the verifier repeats resolving a term thanks to recursion, then the verifier should stop the current alias execution.
3. Then, go back and try a different alias,
4. and so forth until one of them resolves (allowing all prior recursive calls to resolve) or no aliases are left to analyze returning None overall

[jennalwise]

Fixed here: https://github.com/gradual-verification/silicon-gv/commit/4432ae2eab18b9193467beda33c0693ea5bc61cc and https://github.com/gradual-verification/silicon-gv/commit/3c948e15eafcba3c8204d1931914a0c59dda9968