Issue 903

[ArquintL]

Fixes #903

[ArquintL]

As expected, CI fails for the first commit and succeeds for the second

[marcoeilers]

I had thought that we check that if-conditions don't contain relational expressions and reject programs in which they do, but apparently not.

Allowing this is a bit tricky semantically, because it means that it is no longer the case that there are two independent executions with their own control flow. So the idea would be that 1) if both executions reach the if, then both executions take the same branch here, because the relational expression evaluates to the same value for both of them, and 2) if only one execution reaches the if, then it takes the true-branch, because low-expressions are trivially true unless both executions are active. If that's what we want, it'd be great to add another test or two that checks that the encoding does the right thing. And then we should probably do the same for loops, too, and make sure that the semantics is clear for those as well.

If you only need this to conditionally check assertions, you could also just write assert e ==> A instead of if (e) { assert A }. And we could add a consistency check that makes sure that branch conditions are not relational.

[ArquintL]

I don’t fully know whether branching on a SIF expression is strictly necessary or more like a convenience feature to case split and “debug” where the SMT solver gets stuck.
From a frontend’s perspective, this would always be a ghost if statement (hopefully we classify SIF expressions as being ghost).

but speaking of consistency checks: I tried to find the consistency check for making sure that no SIF expressions appear in triggers but couldn’t find it. Do you happen to know where they are implemented?

[marcoeilers]

The check is called here:

silver/src/main/scala/viper/silver/parser/Translator.scala

Line 68 in ac67f4f

case trig: Trigger => Consistency.checkTriggers(trig, finalProgram)

(only checked directly after translation from the PAst, therefore not checked when the AST comes from a frontend, as I wrote in the other issue).
And the AST nodes for low etc. don't override the default for

silver/src/main/scala/viper/silver/ast/Expression.scala

Line 1311 in ac67f4f

def extensionIsForbiddenInTrigger(): Boolean = true

[ArquintL]

@marcoeilers I've just added additional testcases demonstrating the semantics you've outlined above. In addition, !lowEvent seemed to not have been supported yet, which is not fixed too

[ArquintL]

The check is called here:

silver/src/main/scala/viper/silver/parser/Translator.scala

Line 68 in ac67f4f

case trig: Trigger => Consistency.checkTriggers(trig, finalProgram)

(only checked directly after translation from the PAst, therefore not checked when the AST comes from a frontend, as I wrote in the other issue).
And the AST nodes for low etc. don't override the default for

silver/src/main/scala/viper/silver/ast/Expression.scala

Line 1311 in ac67f4f

def extensionIsForbiddenInTrigger(): Boolean = true

@marcoeilers Since the check is performed on the AST (instead of the PAST) level, is there a reason this is done in translate as opposed to during consistency checking (i.e., AST.checkTransitively)?

[marcoeilers]

No, I don't know why this is not done as part of the normal consistency checks, it probably should be.
But moving it to the consistency checks would almost certainly break some frontend stuff (since the consistency check would then reject the bad triggers they sometimes generate).