Translate quantifier weights to Boogie

[fpoli]

With this PR Carbon translates quantifier weights (added in viperproject/silver#633, used in viperproject/silicon#674) to Boogie. I added a test to show how to set the weight in the AST.

[fpoli]

The following test fails in CI, even after restarting the job two times. It seems deterministic.

[info] - wands/examples/list_insert_tmp.vpr [carbon-Silver] *** FAILED *** (25 minutes, 46 seconds)
[info]   5 errors
[info]   
[info]   The following output occurred during testing, but should not have according to the test annotations:
[info]     [internal:internal] [internal:internal] An internal error occurred. Found 2 errors, but there should be 0. The output was: Boogie program verifier version 1.0.0.0, Copyright (c) 2003-2014, Microsoft.
[info]   Advisory: insert SKIPPED because of internal error: unexpected prover output: Broken pipe
[info]   /tmp/carbon8032009235638965007.bpl(956,11): Verification inconclusive (insert)
[info]   
[info]   Boogie program verifier finished with 3 verified, 0 errors, 1 inconclusive
[info]    (<no position>)
[info]     [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: /tmp/carbon8032009235638965007.bpl(956,11): Verification inconclusive (insert) (<no position>)
[info]     [internal:internal] [internal:internal] An internal error occurred. Found an unparsable output from Boogie: Advisory: insert SKIPPED because of internal error: unexpected prover output: Broken pipe (<no position>)
[info]   
[info]   The following outputs was specified to occur erroneously (UnexpectedOutput) according to the test annotations, but did not occur during testing:
[info]     assert.failed:assertion.false (list_insert_tmp.vpr:132)
[info]     apply.failed:assertion.false (list_insert_tmp.vpr:90) (AnnotationBasedTestSuite.scala:63)
[info]   + Verifier used: carbon 1.0. 
[info]   + Time required: 73 msec (Parsing), 53 msec (Semantic Analysis), 19 msec (Translation), 87 msec (Consistency Check), 1545.99 sec (Verification). 

I failed to reprodue this error. Even when using the exact same Docker image gobraverifier/gobra-base:v5_z3_4.8.7, Boogie version bae82d3, and Z3 version 4.8.7 as used in CI, sbt test runs fine and reports the following CANCELED message:

[info] - wands/examples/list_insert_tmp.vpr [carbon-Silver] !!! CANCELED !!! (16 seconds, 592 milliseconds)
[info]   2 ignored errors
[info]   apply.failed:assertion.false, issue 290
[info]   assert.failed:assertion.false, issue 290 (AnnotationBasedTestSuite.scala:81)
[info]   + Verifier used: carbon 1.0. 
[info]   + Time required: 1.29 sec (Parsing), 126 msec (Semantic Analysis), 180 msec (Translation), 310 msec (Consistency Check), 14.43 sec (Verification). 

Strangely, running Carbon with sbt run fails for a completely different reason, related to macro expansion:

> sbt "run silver/src/test/resources/wands/examples/list_insert_tmp.vpr"
[info] welcome to sbt 1.6.2 (Private Build Java 17.0.5)
[info] loading global plugins from /home/fpoli/.sbt/1.0/plugins
[info] loading settings for project carbon-build from plugins.sbt ...
[info] loading project definition from /home/fpoli/src/carbon/project
[info] loading settings for project carbon from build.sbt ...
[info] loading settings for project silver from build.sbt ...
[info] set current project to Carbon (in build file:/home/fpoli/src/carbon/)
[warn] Compile / run / javaOptions will be ignored, Compile / run / fork is set to false
[info] running viper.carbon.Carbon silver/src/test/resources/wands/examples/list_insert_tmp.vpr
carbon 1.0
carbon found 1 error in 1.39s:
  [0] Parse error: Macro expansion would result in invalid code (encountered ParseTreeDuplicationError:)
Cannot duplicate PAccPred(PCall(PIdnUse(List),List(PIdnUse(crt)),None),PFullPerm()) with new children List(PCall(PIdnUse(List),List(PIdnUse(crt)),None), PFullPerm()) (list_insert_tmp.vpr@57.11)

The ./carbon.sh script runs fine and reports the same (canceled) verification errors reported by sbt test.

[fpoli]

The failing test is in the wands folder. By removing other test folders the failing test passes.

My current best guess is that there is a deterministic memory leak in Carbon or in the test suite. When the CI runs out of memory, it might be that Z3 or Boogie is killed, which would explain the "broken pipe" error message. Then, Carbon or Boogie restarts the killed process and the remaining tests work fine.

I'm trying to identify the memory leak.

[gauravpartha]

As discussed in the meeting, we will look into merging this PR after the January 2022 release.