Issue with backend VSWITHSILICON

[jcp19]

As of recently, Gobra runs into an exception whenever it verifies a file with the Viper server with silicon. This seems to be a problem caused by the interaction of the viperserver and the PredicateInstancePlugin. In the future, we should run the tests against all backends that we want to support, otherwise these errors might fall through the cracks. I guess that PR #818 might be the culprit, but we need to do more debugging to figure this out.

Example:

package test

pure
requires acc(x)
decreases _
func getVal(x *int) int {
	return *x
}

Error:

[info] Writing [level:INFO] logs into (default) journal: /var/folders/4s/59ywvwc566j0cj10rn6bjcdr0000gn/T/viperserver_journal_173714098439911452264655554032242.log
[info] An unknown Exception was thrown.
[info] java.lang.RuntimeException: Unexpected expression decreases ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf) cannot be symbolically evaluated
[info] java.util.concurrent.ExecutionException: java.lang.RuntimeException: Unexpected expression decreases ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf) 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)
[info] 	at viper.server.core.ViperBackend.verification(VerificationWorker.scala:254)
[info] 	at viper.server.core.ViperBackend.$anonfun$execute$3(VerificationWorker.scala:164)
[info] 	at scala.util.Either.flatMap(Either.scala:352)
[info] 	at viper.server.core.ViperBackend.$anonfun$execute$1(VerificationWorker.scala:156)
[info] 	at scala.util.Either.flatMap(Either.scala:352)
[info] 	at viper.server.core.ViperBackend.execute(VerificationWorker.scala:155)
[info] 	at viper.server.core.VerificationWorker.run(VerificationWorker.scala:68)
[info] 	at viper.server.core.VerificationWorker.call(VerificationWorker.scala:109)
[info] 	at viper.server.core.VerificationWorker.call(VerificationWorker.scala:32)
[info] 	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[info] 	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[info] 	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[info] 	at java.base/java.lang.Thread.run(Thread.java:829)
[info] Caused by: java.lang.RuntimeException: Unexpected expression decreases ErrorMem_ad177c4e_SY$db8f20c_ad177c4e_(thisItf) cannot be symbolically evaluated
[info] 	at scala.sys.package$.error(package.scala:27)
[info] 	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:1287)
[info] 	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
[info] 	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
[info] 	at viper.silicon.rules.producer$.produceTlc(Producer.scala:549)
[info] 	at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:200)
[info] 	at viper.silicon.rules.producer$.produceTlcs(Producer.scala:149)
[info] 	at viper.silicon.rules.producer$.$anonfun$produceTlcs$1(Producer.scala:161)
[info] 	at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:202)
[info] 	at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:217)
[info] 	at viper.silicon.rules.producer$.$anonfun$produceTlc$48(Producer.scala:374)
[info] 	at viper.silicon.rules.chunkSupporter$.produce(ChunkSupporter.scala:221)
[info] 	at viper.silicon.rules.producer$.$anonfun$produceTlc$42(Producer.scala:367)
[info] 	at viper.silicon.rules.permissionSupporter$.assertNotNegative(PermissionSupporter.scala:24)
[info] 	at viper.silicon.rules.producer$.$anonfun$produceTlc$41(Producer.scala:350)
[info] 	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
[info] 	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)

[ArquintL]

I noticed this today too and reverting #818 "fixes" the problem

[ArquintL]

@jcp19 do you have any idea what the issue could be? I haven't dived deep yet but I can neither spot an obvious change in #818 nor did removing --disablePlugins in ViperBackends.scala help

[jcp19]

I did not look at the problem, but, from the exception we get, I would speculate that either the TerminationPlugin or the PredicateInstancePlugin are not running, or running at the wrong time, given that the error is about us using a predicate instance (ErrorMem()) as a termination measure in the error interface in builtin.gobra. If that is the case, passing --disablePlugins to the backends would probably not change the behaviour of Gobra

I don't know if we ever tested the SiliconFrontendAPI together with ViperServer in the group, so these errors could have gone unnoticed.