search

gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

VariableResolver in Translator entering infinite loop during Composite gradual verification #50

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

This partial spec for composite: stack_overflow_and_timeout.txt, is exhibiting an infinite loop in the Translator's VariableResolver for the tree_get_parent method.

The symbolic state going into the Translator is correct. It just so happens that the state has enough aliasing to realize an infinite loop in our system. The reason the infinite loop is happening is because the below case of the VariableResolver is setting the translatingVars set to empty rather than removing only what is currently being analyzed. 

      case resolvedVariables => {
        translatingVars = Seq() // is this, but should be translatingVars.filter(v => v != variable)
        resolvedVariables
      }

As a result, the tracking in translatingVars that makes sure the Translator doesn't keep reanalyzing aliases is removed allowing the Translator to keep re-analyzing the same things. Just removing the currently analyzed variable before returning recursively is sufficient to stop the infinite loop and keep the functionality the same/correct. Eventually, the set will become empty when all variables in the recursive stack are resolved, so the set will be ready for the next translation task.

jennalwise commented 2 years ago

Fixed and tested in this commit: https://github.com/gradual-verification/silicon-gv/commit/6e6df0c4fff694e282f37258b4811505a950971d