Termination Plugin: undefined error locations prevent caching

[aterga]

The termination plugin implicitly creates methods that perform termination checks for functions, e.g., in the following scenario:

import <decreases/int.vpr>
function bar(x: Int): Bool
    decreases x
{
    bar(x)
}

Since these auxiliary method's do not correspond to any source code, the positions for them (and the verification errors that might occur inside) are set to NoPosition. This prevents us from being able to soundly cache anything in the current file. The reason is that caching must associate each error with one method, and this happens based on the position of the error. It would be unsound to cache any method that verified successfully if some errors are potentially not cacheable. Therefore, the only sound solution right now seems to be to discard all verification results if at least one of them is lacking position info.

@marcoeilers and I are proposing a lightweight solution: we can add the following field to class AbstractError:

val scope: Option[Node] = None

This would give the plugin the opportunity to associate an error with an internal method and would enable caching. In future, Silicon and Carbon could also be adapted to set the scope of errors that they generate, avoiding the need to recompute this relation in the caching mechanism, which is fragile.

Conceptually, I think that such a field would make sense, as it is often important to see the associativity of errors to AST nodes even, e.g., in a scenario where the verifiers are invoked from the command line.