Bug in the desugaring process of `rel()` when using `ghost if`

[AkasakaJelos]

Consider the following example code:

package exercises

// ##(--hyperMode extended --enableExperimentalHyperFeatures)

// @ requires rel(t,0)!= rel(t,1)
func relGhostIf(t uint64) {
	/*@
	ghost if rel(t,0) < rel(t,1){
		assert true
	} else{
		assert true
	}
	@*/
}

When running this code, we will get the following error:

[info] An unknown Exception was thrown.
[info] java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: Unexpected expression rel(t_V0_CN0, 0) cannot be symbolically evaluated
[info] java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: Unexpected expression rel(t_V0_CN0, 0) cannot be symbolically evaluated
[info] 	at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
[info] 	at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
[info] 	at viper.silicon.Silicon.verify(Silicon.scala:205)
[info] 	at viper.silicon.Silicon.verify(Silicon.scala:163)

When looking into the SIF encoding, we can see that the code p1_0 and p3 are not correctly desugared, which leads to the following issues:

p1_0 := p1 && rel(t_V0_CN0, 0) < rel(t_V0_CN0, 1)
p2_0 := p2 && t_V0_CN0 < t_V0_CN0_0
p3 := p1 && !(rel(t_V0_CN0, 0) < rel(t_V0_CN0, 1))
p4 := p2 && !(t_V0_CN0 < t_V0_CN0_0)

The correct workaround consists of the following: we force rel(t, 0) and rel(t, 1) to be desugared first, and then compare them using ghost functions.

package exercises

// ##(--hyperMode extended --enableExperimentalHyperFeatures)

// @ requires rel(t,0)!= rel(t,1)
func relGhostIf(t uint64) {

	/*@
	ghost var t0 uint64 = rel(t,0)
	ghost var t1 uint64 = rel(t,1)
	ghost if t0 < t1{
		assert true
	} else{
		assert true
	}
	@*/

}

[ArquintL]

Note that the description workaround changes the program's semantics as t0 and t1 effectively do not behave like a macro (cf. #993)

[ArquintL]

A semantics preserving work around is the following:

func relGhostIf2(t uint64) {
	/*@
	cond := rel(t, 0) < rel(t, 1)
	ghost if cond {
		assert true
	} else {
		assert true
	}
	@*/
}

[ArquintL]

The same issue is also reproducible when using low:

func lowGhostIf(t uint64) {
	/*@
	ghost if low(t) {
		assert true
	} else {
		assert true
	}
	@*/
}

[ArquintL]

Fixed in Silver #PR 904

[AkasakaJelos]

Additionally, anything compared with rel variables will trigger this issue immediately. A small example would be this:

func test_indexBug(idx2 int) {
	/*@
		ghost if 1 < rel(idx2,0){
			assert true
		}else if 2 > rel(idx2,1){
			assert true
		}
	@*/
}

[ArquintL]

Exactly. The branch condition is not encoded (for the first execution) so any SIF expression in it while result in the exception mentioned above

[ArquintL]

This issue is now fixed on the hyper-rel branch