Support for rel Expressions

[ArquintL]

This PR adds support for rel(e, i) expressions, where e is an arbitrary expression and i is an int literal (either 0 or 1), which denotes one of the two executions when reasoning hyper properties in which e should be evaluated.
Since Viper's rel expression is hidden behind a feature flag, Gobra also requires --enableExperimentalHyperFeatures as well as the extended hyper mode.

@jcp19 I've started implementing rel for the non-extended hyper mode as supporting this expressions in that mode should technically be possible. However, it wasn't immediately clear to me how to make it fit into the current implementation as the implementation requires, e.g., expressing a transformation to turn a hyper assertion into a unary assertion. For now, support in the extended hyper mode seems sufficient but please let me know if you have thoughts on supporting the non-extended hyper mode.

This PR now also removes the deprecated silver-sif-extension dependency and instead uses the SIF plugin that is now part of silver. The changes to the Dockerfile also resolve the warnings we have observed in the GitHub CI.

[ArquintL]

The unit tests are currently failing as the tests do not seem to correctly pick up the in-file configurations

[jcp19]

Maybe we can have a more informative error saying that rel expressions are still not supported by the LowGuardTransformer?

[ArquintL]

GhostExprTyping already creates a type error for rel expressions so this error is basically dead code

[jcp19]

However, it wasn't immediately clear to me how to make it fit into the current implementation as the implementation requires, e.g., expressing a transformation to turn a hyper assertion into a unary assertion. For now, support in the extended hyper mode seems sufficient but please let me know if you have thoughts on supporting the non-extended hyper mode.

Can you provide more details on the problem here?

[ArquintL]

Can you provide more details on the problem here?

There are several problems, such as:

• If the hyperMode is set to off, then we remove all hyper assertions in members that do not have proof obligations removeLow. rel(e,i) could simply be turned into e to preserve well-typedness of the expression but this might introduce an unsoundness, as illustrated by the following example:

  ensures rel(b, 0) && !rel(b, 1)
  func unsoundTransformation() (b bool)
  

• Similarly, runExp removes the minor execution if onlyMajor is desired
• And lastly, assertion performs the actual encoding of an expression e. However, my intuition is not good enough about what a "positive" or "negative unary" is supposed to be to extend the encoding. In particular, it seems that I'd have to add additional cases to support, e.g., rel(i_V0, 0) < rel(i_V0, 1), which currently results in the error "Encountered unexpected node during product-program transformation of assertions" (which btw also occurs if a program contains the expression !low(e))

[jcp19]

Hmm, I see. Regarding the first two problems, I think we could be conservative and produce an error in the cases where there is no obvious translation. The example you provide is pretty illustrative and I think it shows why we should generate an error rather than trying to translate this expression in a way that may be surprising to the user. Likewise, I would produce an error in the second problem if we use the rel operator to evaluate an expression in the minor execution.

I guess an alternative to this could be to generate a precondition false for all methods that contain relational specifications when hyperMode is off and generate a warning for those methods. The advantage of this would be that, if we try to verify a package that depends on another where only a part of its functions with relational spec, we could still verify that package with hyperMode off if it never uses relational specs or never calls functions with relational specs from another package.

As for the third problem, I need to think some more about it.