IndexOutOfBounds triggered by Translator.selectShortestField

[icmccorm]

When running the following two permutations (example 1, example 2) of List, an IndexOutOfBoundsException is thrown. The source of the exception is in Translator. It occurs on line 169 when an empty candidateFields is indexed into:

    } else {
      // in this case, we only have a list of receivers, so we select one
      // (they should all be equal in length!)
      Some(candidateFields(0))
    }

Returning None if the list is empty triggers an additional exception on lines 575-578 of Consumer:

tArgs.map(tArg => new Translator(s5.copy(g = g), v4.decider.pcs).translate(tArg) match {
  case None => sys.error("Error translating! Exiting safely.")
  case Some(expr) => expr
})

[jennalwise]

I did some more debugging on this, and the problem is that the regexVariableResolver is correctly receiving an argument to resolve that is not of the type terms.Var(identifier: Identifier, termType), because it is a receiver from a heap chunk. I have dealt with this in other places in the code, so I will borrow the logic from there and apply it in regexVariableResolver.

[jennalwise]

Pushed fix to issue38 branch for testing: https://github.com/gradual-verification/silicon-gv/tree/issue38

[jennalwise]

Fixed in commit https://github.com/gradual-verification/silicon-gv/commit/17bdfbf2ed43042df66e994764b56b4bbfeeb47d .