merge master

src/main/antlr4/GobraLexer.g4

@@ -20,6 +20,7 @@ DECIMAL_FLOAT_LIT      : DECIMALS ('.'{_input.LA(1) != '.'}? DECIMALS? EXPONENT?
 TRUE        : 'true' -> mode(NLSEMI);
 FALSE       : 'false' -> mode(NLSEMI);
 ASSERT      : 'assert';
+REFUTE      : 'refute';
 ASSUME      : 'assume';
 INHALE      : 'inhale';
 EXHALE      : 'exhale';

src/main/antlr4/GobraParser.g4

@@ -63,7 +63,7 @@ ghostMember: implementationProof
 ghostStatement:
   GHOST statement  #explicitGhostStatement
   | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement
-  | kind=(ASSUME | ASSERT | INHALE | EXHALE) expression #proofStatement
+  | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement
   | matchStmt #matchStmt_
   | OPEN_DUP_SINV #pkgInvStatement
   ;

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -973,6 +973,8 @@ case class PExplicitGhostStatement(actual: PStatement) extends PGhostStatement w
 
 case class PAssert(exp: PExpression) extends PGhostStatement
 
+case class PRefute(exp: PExpression) extends PGhostStatement
+
 case class PAssume(exp: PExpression) extends PGhostStatement
 
 case class PExhale(exp: PExpression) extends PGhostStatement

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -305,6 +305,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case statement: PGhostStatement => statement match {
       case PExplicitGhostStatement(actual) => "ghost" <+> showStmt(actual)
       case PAssert(exp) => "assert" <+> showExpr(exp)
+      case PRefute(exp) => "refute" <+> showExpr(exp)
       case PAssume(exp) => "assume" <+> showExpr(exp)
       case PExhale(exp) => "exhale" <+> showExpr(exp)
       case PInhale(exp) => "inhale" <+> showExpr(exp)

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

@@ -341,6 +341,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
 
     case Return() => "return"
     case Assert(ass) => "assert" <+> showAss(ass)
+    case Refute(ass) => "refute" <+> showAss(ass)
     case Assume(ass) => "assume" <+> showAss(ass)
     case Inhale(ass) => "inhale" <+> showAss(ass)
     case Exhale(ass) => "exhale" <+> showAss(ass)
@@ -791,6 +792,7 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
 
     case Return() => "return"
     case Assert(ass) => "assert" <+> showAss(ass)
+    case Refute(ass) => "refute" <+> showAss(ass)
     case Assume(ass) => "assume" <+> showAss(ass)
     case Inhale(ass) => "inhale" <+> showAss(ass)
     case Exhale(ass) => "exhale" <+> showAss(ass)

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -438,6 +438,7 @@ case class Defer(stmt: Deferrable)(val info: Source.Parser.Info) extends Stmt
 case class Return()(val info: Source.Parser.Info) extends Stmt
 
 case class Assert(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
+case class Refute(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Assume(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Inhale(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Exhale(ass: Assertion)(val info: Source.Parser.Info) extends Stmt

src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala

@@ -135,7 +135,7 @@ object OverflowChecksTransform extends InternalTransform {
       Seqn(genOverflowChecksExprs(Vector(base, idx)) :+ m)(m.info)
 
     // explicitly matches remaining statements to detect non-exhaustive pattern matching if a new statement is added
-    case x@(_: Inhale | _: Exhale | _: Assert | _: Assume
+    case x@(_: Inhale | _: Exhale | _: Assert | _: Refute | _: Assume
             | _: Return | _: Fold | _: Unfold | _: PredExprFold | _: PredExprUnfold | _: Outline
             | _: SafeTypeAssertion | _: SafeReceive | _: Label | _: Initialization | _: PatternMatchStmt) => x
 

src/main/scala/viper/gobra/backend/BackendVerifier.scala

@@ -84,17 +84,18 @@ object BackendVerifier {
   /**
     * Takes a Viper VerificationResult and converts it to a Gobra Result using the provided backtracking information
     */
-  def convertVerificationResult(result: VerificationResult, backTrackInfo: BackTrackInfo): Result = result match {
-    case silver.verifier.Success => Success
-    case failure: silver.verifier.Failure =>
-      val (verificationError, otherError) = failure.errors
-        .partition(_.isInstanceOf[silver.verifier.VerificationError])
-        .asInstanceOf[(Seq[silver.verifier.VerificationError], Seq[silver.verifier.AbstractError])]
+  def convertVerificationResult(result: VerificationResult, backTrackInfo: BackTrackInfo): Result =
+    result match {
+      case silver.verifier.Success => Success
+      case failure: silver.verifier.Failure =>
+        val (verificationError, otherError) = failure.errors
+          .partition(_.isInstanceOf[silver.verifier.VerificationError])
+          .asInstanceOf[(Seq[silver.verifier.VerificationError], Seq[silver.verifier.AbstractError])]
 
-      checkAbstractViperErrors(otherError)
+        checkAbstractViperErrors(otherError)
 
-      Failure(verificationError.toVector, backTrackInfo)
-  }
+        Failure(verificationError.toVector, backTrackInfo)
+    }
 
   @scala.annotation.elidable(scala.annotation.elidable.ASSERTION)
   private def checkAbstractViperErrors(errors: Seq[silver.verifier.AbstractError]): Unit = {

src/main/scala/viper/gobra/backend/Carbon.scala

@@ -7,6 +7,7 @@
 package viper.gobra.backend
 
 import viper.carbon
+import viper.carbon.CarbonFrontendAPI
 import viper.gobra.util.GobraExecutionContext
 import viper.silver.ast.Program
 import viper.silver.reporter._
@@ -20,19 +21,18 @@ class Carbon(commandLineArguments: Seq[String]) extends ViperVerifier {
     // directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
     implicit val _executor: GobraExecutionContext = executor
     Future {
-      val backend: carbon.CarbonVerifier = carbon.CarbonVerifier(reporter, List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}"))
-      backend.parseCommandLine(commandLineArguments ++ Seq("--ignoreFile", "dummy.sil"))
+      val carbonApi: carbon.CarbonFrontendAPI = new CarbonFrontendAPI(reporter)
 
       val startTime = System.currentTimeMillis()
-      backend.start()
-      val result = backend.verify(program)
-      backend.stop()
+      carbonApi.initialize(commandLineArguments ++ Seq("--ignoreFile", "dummy.sil"))
+      val result = carbonApi.verify(program)
+      carbonApi.stop()
 
       result match {
         case Success =>
-          reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime)
+          reporter report OverallSuccessMessage(carbonApi.verifier.name, System.currentTimeMillis() - startTime)
         case f@Failure(_) =>
-          reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f)
+          reporter report OverallFailureMessage(carbonApi.verifier.name, System.currentTimeMillis() - startTime, f)
       }
 
       result

src/main/scala/viper/gobra/backend/Silicon.scala

@@ -19,19 +19,19 @@ class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier {
     // directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
     implicit val _executor: GobraExecutionContext = executor
     Future {
-      val backend: silicon.Silicon = silicon.Silicon.fromPartialCommandLineArguments(commandLineArguments, reporter)
+      val siliconApi: silicon.SiliconFrontendAPI = new silicon.SiliconFrontendAPI(reporter)
 
       val startTime = System.currentTimeMillis()
       try {
-        backend.start()
-        val result = backend.verify(program)
-        backend.stop()
+        siliconApi.initialize(commandLineArguments)
+        val result = siliconApi.verify(program)
+        siliconApi.stop()
 
         result match {
           case Success =>
-            reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime)
+            reporter report OverallSuccessMessage(siliconApi.verifier.name, System.currentTimeMillis() - startTime)
           case f@Failure(_) =>
-            reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f)
+            reporter report OverallFailureMessage(siliconApi.verifier.name, System.currentTimeMillis() - startTime, f)
         }
 
         result

src/main/scala/viper/gobra/backend/ViperBackends.scala

@@ -51,6 +51,9 @@ object ViperBackends {
       // Gobra seems to be much slower with the new silicon axiomatization of collections.
       // For now, we stick to the old one.
       options ++= Vector("--useOldAxiomatization")
+      if (config.respectFunctionPrePermAmounts) {
+        options ++= Vector("--respectFunctionPrePermAmounts")
+      }
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }
@@ -81,6 +84,9 @@ object ViperBackends {
     def create(exePaths: Vector[String], config: Config)(implicit executor: GobraExecutionContext): Carbon = {
       var options: Vector[String] = Vector.empty
       // options ++= Vector("--logLevel", "ERROR")
+      if (config.respectFunctionPrePermAmounts) {
+        options ++= Vector("--respectFunctionPrePermAmounts")
+      }
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }
@@ -154,6 +160,9 @@ object ViperBackends {
         case MCE.OnDemand => "2"
       }
       options ++= Vector(s"--exhaleMode=$mceSiliconOpt")
+      if (config.respectFunctionPrePermAmounts) {
+        options ++= Vector("--respectFunctionPrePermAmounts")
+      }
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }
@@ -172,6 +181,9 @@ object ViperBackends {
     override def getViperVerifierConfig(exePaths: Vector[String], config: Config): ViperVerifierConfig = {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
+      if (config.respectFunctionPrePermAmounts) {
+        options ++= Vector("--respectFunctionPrePermAmounts")
+      }
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }

src/main/scala/viper/gobra/frontend/Config.scala

@@ -78,6 +78,10 @@ object ConfigDefaults {
   val DefaultDisableCheckTerminationPureFns: Boolean = false
   val DefaultUnsafeWildcardOptimization: Boolean = false
   val DefaultMoreJoins: MoreJoins.Mode = MoreJoins.Disabled
+  // TODO: for the time being, we use the old semantics for fractional perms in pure function preconditions,
+  //   as our pre-existing verified codebases use those semantics. In the future, after we have ported our most
+  //   important case studies to the new semantics, we should deprecate the old one and change this default to false.
+  val DefaultRespectFunctionPrePermAmounts: Boolean = true
 }
 
 // More-complete exhale modes
@@ -172,7 +176,7 @@ case class Config(
                    disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                    unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                    moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
-
+                   respectFunctionPrePermAmounts: Boolean = ConfigDefaults.DefaultRespectFunctionPrePermAmounts,
 ) {
 
   def merge(other: Config): Config = {
@@ -226,6 +230,7 @@ case class Config(
       disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
       unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
       moreJoins = MoreJoins.merge(moreJoins, other.moreJoins),
+      respectFunctionPrePermAmounts = respectFunctionPrePermAmounts || other.respectFunctionPrePermAmounts,
     )
   }
 
@@ -283,6 +288,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                       unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                       moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
+                      respectFunctionPrePermAmounts: Boolean = ConfigDefaults.DefaultRespectFunctionPrePermAmounts,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -344,6 +350,7 @@ trait RawConfig {
     disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns,
     unsafeWildcardOptimization = baseConfig.unsafeWildcardOptimization,
     moreJoins = baseConfig.moreJoins,
+    respectFunctionPrePermAmounts = baseConfig.respectFunctionPrePermAmounts,
   )
 }
 
@@ -768,6 +775,16 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     }
   }
 
+  val respectFunctionPrePermAmounts: ScallopOption[Boolean] = toggle(
+    name = "respectFunctionPrePermAmounts",
+    descrYes = s"Respects precise permission amounts in pure function preconditions instead of only checking read access, as done in older versions of Gobra." +
+      "This option should be used for verifying legacy projects written with the old interpretation of fractional permissions." +
+      "New projects are encouraged to set this flag to false.",
+    descrNo = s"Use the default interpretation for fractional permissions in pure function preconditions.",
+    default = Some(ConfigDefaults.DefaultRespectFunctionPrePermAmounts),
+    noshort = true,
+  )
+
   val enableLazyImports: ScallopOption[Boolean] = opt[Boolean](
     name = Config.enableLazyImportOptionName,
     descr = s"Enforces that ${GoVerifier.name} parses depending packages only when necessary. Note that this disables certain language features such as global variables.",
@@ -1031,5 +1048,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     disableCheckTerminationPureFns = disableCheckTerminationPureFns(),
     unsafeWildcardOptimization = unsafeWildcardOptimization(),
     moreJoins = moreJoins(),
+    respectFunctionPrePermAmounts = respectFunctionPrePermAmounts(),
   )
 }

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -4148,6 +4148,7 @@ object Desugar extends LazyLogging {
 
       stmt match {
         case PAssert(exp) => for {e <- goA(exp)} yield in.Assert(e)(src)
+        case PRefute(exp) => for {e <- goA(exp)} yield in.Refute(e)(src)
         case PAssume(exp) => for {e <- goA(exp)} yield in.Assume(e)(src)
         case PInhale(exp) => for {e <- goA(exp)} yield in.Inhale(e)(src)
         case PExhale(exp) => for {e <- goA(exp)} yield in.Exhale(e)(src)

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -2199,6 +2199,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   override def visitProofStatement(ctx: ProofStatementContext): PGhostStatement = super.visitProofStatement(ctx) match {
     case Vector(kind : String, expr : PExpression) => kind match {
       case "assert" => PAssert(expr)
+      case "refute" => PRefute(expr)
       case "assume" => PAssume(expr)
       case "inhale" => PInhale(expr)
       case "exhale" => PExhale(expr)

src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala

@@ -387,7 +387,7 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl =>
 
     def validStatements(stmts: Vector[PStatement]): PropertyResult =
       PropertyResult.bigAnd(stmts.map {
-        case _: PUnfold | _: PFold | _: PAssert | _: PEmptyStmt => successProp
+        case _: PUnfold | _: PFold | _: PAssert | _: PRefute | _: PEmptyStmt => successProp
         case _: PAssume | _: PInhale | _: PExhale => failedProp("Assume, inhale, and exhale are forbidden in implementation proofs")
 
         case b: PBlock => validStatements(b.nonEmptyStmts)

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala

@@ -17,6 +17,7 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl =>
   private[typing] def wellDefGhostStmt(stmt: PGhostStatement): Messages = stmt match {
     case n@PExplicitGhostStatement(s) => error(n, "ghost error: expected ghostifiable statement", !s.isInstanceOf[PGhostifiableStatement])
     case PAssert(exp) => assignableToSpec(exp)
+    case PRefute(exp) => assignableToSpec(exp)
     case PExhale(exp) => assignableToSpec(exp)
     case PAssume(exp) => assignableToSpec(exp)
     case PInhale(exp) => assignableToSpec(exp)