Merges branch 'master' into 'hyperGobra'

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

@@ -60,7 +60,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_
   ;
 

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -1,4 +1,4 @@
-// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -1,4 +1,4 @@
-// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 

src/main/scala/viper/gobra/Gobra.scala

@@ -228,7 +228,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       }
     })
     val (errors, inFileConfigs) = inFileEitherConfigs.partitionMap(identity)
-    if (errors.nonEmpty) Left(errors.map(ConfigError))
+    if (errors.nonEmpty) Left(errors.flatten)
     else {
       // start with original config `config` and merge in every in file config:
       val mergedConfig = inFileConfigs.flatten.foldLeft(config) {
@@ -353,8 +353,8 @@ object GobraRunner extends GobraFrontend with StrictLogging {
       val scallopGobraConfig = new ScallopGobraConfig(args.toSeq)
       val config = scallopGobraConfig.config
       exitCode = config match {
-        case Left(validationError) =>
-          logger.error(validationError)
+        case Left(errors) =>
+          errors.foreach(err => logger.error(err.formattedMessage))
           1
         case Right(config) =>
           // Print copyright report

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

@@ -969,6 +969,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

@@ -284,6 +284,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)
@@ -794,6 +795,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

@@ -432,6 +432,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

@@ -41,14 +41,14 @@ object BackendVerifier {
       case _ =>
     }
 
-    (config.backend, config.boogieExe) match {
+    (config.backendOrDefault, config.boogieExe) match {
       case (Carbon, Some(boogieExe)) =>
         exePaths ++= Vector("--boogieExe", boogieExe)
       case _ =>
     }
 
     val verificationResults: Future[VerificationResult] =  {
-      val verifier = config.backend.create(exePaths, config)
+      val verifier = config.backendOrDefault.create(exePaths, config)
       val reporter = BacktranslatingReporter(config.reporter, task.backtrack, config)
 
       if (!config.shouldChop) {
@@ -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)
+      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

@@ -29,7 +29,6 @@ object ViperBackends {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
       options ++= Vector("--disableCatchingExceptions")
-      options ++= Vector("--respectFunctionPrePermAmounts")
       if (config.conditionalizePermissions) {
         options ++= Vector("--conditionalizePermissions")
       }
@@ -52,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")
       }
@@ -82,10 +84,12 @@ 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")
       }
-      options ++= Vector("--respectFunctionPrePermAmounts")
       options ++= exePaths
 
       new Carbon(options)
@@ -115,7 +119,7 @@ object ViperBackends {
     /** returns an existing ViperCoreServer instance or otherwise creates a new one */
     protected def getOrCreateServer(config: Config)(executionContext: GobraExecutionContext): ViperCoreServer = {
       server.getOrElse({
-        var serverConfig = List("--disablePlugins", "--logLevel", config.logLevel.levelStr)
+        var serverConfig = List("--logLevel", config.logLevel.levelStr)
         if(config.cacheFile.isDefined) {
           serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString))
         }
@@ -137,7 +141,6 @@ object ViperBackends {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
       options ++= Vector("--disableCatchingExceptions")
-      options ++= Vector("--respectFunctionPrePermAmounts")
       // Gobra seems to be much slower with the new silicon axiomatization of collections.
       // For now, we stick to the old one.
       options ++= Vector("--useOldAxiomatization")
@@ -157,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")
       }
@@ -174,8 +180,10 @@ object ViperBackends {
   case class ViperServerWithCarbon(initialServer: Option[ViperCoreServer] = None) extends ViperServerBackend(initialServer) {
     override def getViperVerifierConfig(exePaths: Vector[String], config: Config): ViperVerifierConfig = {
       var options: Vector[String] = Vector.empty
-      options ++= Vector("--logLevel", "ERROR")
-      options ++= Vector("--respectFunctionPrePermAmounts")
+      // options ++= Vector("--logLevel", "ERROR")
+      if (config.respectFunctionPrePermAmounts) {
+        options ++= Vector("--respectFunctionPrePermAmounts")
+      }
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }