Need to catch logical conditionals with impure conditions in frontend and produce error message

[jennalwise]

In my case study, I wrote a loop invariant: tokenListSeg(gv_tok, tok) && gv_beforeloop == true ? true : gv_tok != tok

which is ambiguous and with conditional priority makes sense to translate into: (tokenListSeg(gv_tok,tok) && gv_beforeloop == true ? true : gv_tok != tok) which interprets tokenListSeg(gv_tok,tok) as being in the condition of the logical conditional. This is not my intention, and I'm okay with having to adjust my specification. However, the error I got due to the 'bad' spec was a Scala Match error from the silicon backend:

[info] welcome to sbt 1.5.3 (Ubuntu Java 11.0.20.1)
[info] loading settings for project gvc0-build from plugins.sbt ...
[info] loading project definition from /home/jenna/Desktop/gvc0/project
[info] loading settings for project gvc from build.sbt ...
[info] loading settings for project silicon from build.sbt ...
[info] loading settings for project silver from build.sbt ...
[info] set current project to gvc0 (in build file:/home/jenna/Desktop/gvc0/)
[info] running (fork) gvc.Main -c src/test/resources/case-study-2023/cparser.c0
[info] Verifying 'src/test/resources/case-study-2023/cparser.c0' and gathering data.
[info] Outputting collected data to /home/jenna/Desktop/gvc0/cparser-2023-09-28T16:48:19.046199/
[info] [*] — Thu Sep 28 16:48:19 EDT 2023
[info] Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: scala.MatchError: acc(tokenListSeg(gv_tok, tok2), write) (of class viper.silver.ast.PredicateAccessPredicate)
[info]   Cause: java.util.concurrent.ExecutionException: scala.MatchError: acc(tokenListSeg(gv_tok, tok2), write) (of class viper.silver.ast.PredicateAccessPredicate)
[error] Exception in thread "main" gvc.VerificationException: Verification aborted exceptionally: acc(tokenListSeg(gv_tok, tok2), write) (of class viper.silver.ast.PredicateAccessPredicate)
[error]     at gvc.Main$.verifySiliconProvided(main.scala:401)
[error]     at gvc.Main$.verify(main.scala:359)
[error]     at gvc.Main$.run(main.scala:200)
[error]     at gvc.Main$.delayedEndpoint$gvc$Main$1(main.scala:77)
[error]     at gvc.Main$delayedInit$body.apply(main.scala:44)
[error]     at scala.Function0.apply$mcV$sp(Function0.scala:39)
[error]     at scala.Function0.apply$mcV$sp$(Function0.scala:39)
[error]     at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:17)
[error]     at scala.App.$anonfun$main$1$adapted(App.scala:80)
[error]     at scala.collection.immutable.List.foreach(List.scala:431)
[error]     at scala.App.main(App.scala:80)
[error]     at scala.App.main$(App.scala:78)
[error]     at gvc.Main$.main(main.scala:44)
[error]     at gvc.Main.main(main.scala)
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1
[error] Total time: 46 s, completed Sep 28, 2023, 4:49:02 PM

At the very least this should not happen, because the only way I was able to figure out that my specification was bad was from putting the .vpr file in silicon-gv directly which utilizes the silver-gv parser and catches my bad spec as a consistency error:

jenna@ubuntu-2023:~/Desktop/silicon-gv$ sbt "testOnly -- -n cparser.vpr -Dsilicon:includeMethods=parse"
[info] welcome to sbt 1.6.2 (Ubuntu Java 11.0.20.1)
[info] loading settings for project silicon-gv-build from metals.sbt,plugins.sbt ...
[info] loading project definition from /home/jenna/Desktop/silicon-gv/project
[info] loading settings for project silicon from build.sbt ...
[info] loading settings for project silver from build.sbt ...
[info] set current project to Silicon (in build file:/home/jenna/Desktop/silicon-gv/)
[warn] javaOptions will be ignored, fork is set to false
[info] Passed: Total 0, Failed 0, Errors 0, Passed 0
[info] No tests to run for common / Test / testOnly
[info] SimpleArithmeticTermSolverTests:
[info] SiliconTests:
[info] - gradual/cparser.vpr [Silicon-Silver] *** FAILED *** (4 seconds, 851 milliseconds)
[info]   1 errors
[info]   
[info]   The following output occurred during testing, but should not have according to the test annotations:
[info]     [consistency.error] Consistency error: acc(tokenListSeg(gv_tok, tok2), write) && gv_beforeloop == true is non pure and appears where only pure expressions are allowed. (cparser.vpr@4255.103) (AnnotationBasedTestSuite.scala:63)
[info]   + Verifier used: Silicon 1.1-SNAPSHOT (4445a121+). 
[info]   + Time required: 2.84 sec (Parsing), 828 msec (Semantic Analysis), 483 msec (Translation), 405 msec (Consistency Check), 0 msec (Verification). 
[info] TriggerRewriterTests:
[info] TriggerGeneratorTests:
[info] NodeBacktranslationTests:
[info] ConcurrentInstantiationTests:
[info] MemoryTests:
[info] Run completed in 8 seconds, 472 milliseconds.
[info] Total number of tests run: 1
[info] Suites: completed 7, aborted 0
[info] Tests: succeeded 0, failed 1, canceled 0, ignored 0, pending 0
[info] *** 1 TEST FAILED ***
[error] Failed tests:
[error]         viper.silicon.tests.SiliconTests
[error] (Test / testOnly) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 12 s, completed Sep 28, 2023, 7:03:53 PM

At minimum, Gradual C0 should produce the same error. But, maybe we could do better in some way?

[jennalwise]

Along a similar vain, if you have your specs split across two clauses, like two ensures clauses, conditionals still take precedence. For example, I expected

//@ ensures ? && acc(*rest) && acc(\result->name) && (\result->name == NULL ? true : *rest != gv_tok);
//@ ensures tokenListSeg(gv_tok, *rest) && tokenListSeg(*rest, NULL);

to join into:

//@ ensures ? && acc(*rest) && acc(\result->name) && (\result->name == NULL ? true : *rest != gv_tok) && tokenListSeg(gv_tok, *rest) && tokenListSeg(*rest, NULL);

But, in reality the frontend turned it into:

//@ ensures ? && acc(*rest) && acc(\result->name) && (\result->name == NULL ? true : *rest != gv_tok && tokenListSeg(gv_tok, *rest) && tokenListSeg(*rest, NULL));

for the backend.

If what Gradual C0 is doing here is the right thing, then we need to probably warn or make it clear to the user that this isn't the intention. Otherwise, we should probably fix the behavior here to match my expected version (especially since I include parentheses around the conditional).