Counterexamples (WIP)

.gitignore

@@ -10,6 +10,29 @@ silver
 silicon
 viperserver
 logger.log
-
+*.log
 *.go.*
-*.gobra.*
+*.gobra.*
+
+playground
+.metals
+.vscode
+.vscode/launch.json
+.metals/metals.lock.db
+.metals/readonly/scala/package.scala
+.metals/metals.h2.db
+.metals/metals.log
+.vscode/settings.json
+project/.bloop
+project/.bloop/*
+fvf_finder.sh
+.gitignore
+csv
+warmup
+congregated_date.ods
+.~lock.congregated_date.ods#
+asserionerrors
+eval_nErrors
+n_Errors_2
+replicateFile.sh
+numars

README.md

@@ -1,5 +1,3 @@
-<img src=".github/docs/gobra.png" height="250">
-
 [![Test Status](https://github.com/viperproject/gobra/workflows/test/badge.svg?branch=master)](https://github.com/viperproject/gobra/actions?query=workflow%3Atest+branch%3Amaster)
 [![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](./LICENSE)
 

project/.bloop/bloop.settings.json

@@ -0,0 +1,18 @@
+{
+    "semanticDBVersion": "4.4.13",
+    "supportedScalaVersions": [
+        "2.13.5",
+        "2.12.13",
+        "2.12.12",
+        "2.12.11",
+        "2.12.10",
+        "2.13.3",
+        "2.13.4",
+        "2.11.12",
+        "2.12.8",
+        "2.12.9",
+        "2.13.0",
+        "2.13.1",
+        "2.13.2"
+    ]
+}

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

@@ -14,6 +14,7 @@ import viper.gobra.ast.frontend.PPackage
 import viper.gobra.ast.internal.Program
 import viper.gobra.ast.internal.transform.OverflowChecksTransform
 import viper.gobra.backend.BackendVerifier
+import viper.gobra.reporting.BackTranslator.VerificationBackTrackInfo
 import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.frontend.{Config, Desugar, Parser, ScallopGobraConfig}
 import viper.gobra.reporting.{AppliedInternalTransformsMessage, BackTranslator, CopyrightReport, VerifierError, VerifierResult}
@@ -77,8 +78,20 @@ class Gobra extends GoVerifier with GoIdeVerifier {
         typeInfo <- performTypeChecking(parsedPackage, finalConfig)
         program <- performDesugaring(parsedPackage, typeInfo, finalConfig)
         program <- performInternalTransformations(program, finalConfig)
-        viperTask <- performViperEncoding(program, finalConfig)
-      } yield (viperTask, finalConfig)
+        programWithBackInfo <- performViperEncoding(program, finalConfig,typeInfo)
+
+       (encodedProgram, encodingBackInfo) = (programWithBackInfo.program,programWithBackInfo.backtrack)
+       task = BackendVerifier.Task(
+         encodedProgram,
+         BackTranslator.BackTrackInfo(
+           encodingBackInfo.errorT,
+           encodingBackInfo.reasonT,
+           encodedProgram,
+           typeInfo,
+           config
+         )
+       )
+     } yield (task, finalConfig)
     }
 
     task.flatMap{
@@ -183,9 +196,9 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     }
   }
 
-  private def performViperEncoding(program: Program, config: Config): Either[Vector[VerifierError], BackendVerifier.Task] = {
+  private def performViperEncoding(program: Program, config: Config,typeInfo:viper.gobra.frontend.info.TypeInfo): Either[Vector[VerifierError], BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
-      Right(Translator.translate(program)(config))
+      Right(Translator.translate(program)(config,typeInfo))
     } else {
       Left(Vector())
     }

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

@@ -41,6 +41,10 @@ object BackendVerifier {
       case _ =>
     }
 
+    if(config.counterexample.isDefined){
+      exePaths ++= Vector("--counterexample", "mapped")
+    }
+
     (config.backend, config.boogieExe) match {
       case (Carbon, Some(boogieExe)) =>
         exePaths ++= Vector("--boogieExe", boogieExe)

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

@@ -16,10 +16,12 @@ object ViperBackends {
     def create(exePaths: Vector[String]): Silicon = {
 
       var options: Vector[String] = Vector.empty
+
       options ++= Vector("--logLevel", "ERROR")
       options ++= Vector("--disableCatchingExceptions")
       options ++= Vector("--enableMoreCompleteExhale")
       options ++= exePaths
+
 
       new Silicon(options)
     }

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

@@ -17,8 +17,10 @@ import org.slf4j.LoggerFactory
 import viper.gobra.backend.{ViperBackend, ViperBackends, ViperVerifierConfig}
 import viper.gobra.GoVerifier
 import viper.gobra.frontend.PackageResolver.{FileResource, RegularImport}
-import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter}
+import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter,CounterexampleConfigs}
 import viper.gobra.util.{TypeBounds, Violation}
+import org.scalactic.Bool
+import _root_.viper.gobra.reporting.CounterexampleConfig
 
 
 object LoggerDefaults {
@@ -41,10 +43,12 @@ case class Config(
                  checkOverflows: Boolean = false,
                  checkConsistency: Boolean = false,
                  shouldVerify: Boolean = true,
+
                  // The go language specification states that int and uint variables can have either 32bit or 64, as long
                  // as they have the same size. This flag allows users to pick the size of int's and uints's: 32 if true,
                  // 64 bit otherwise.
-                 int32bit: Boolean = false
+                 int32bit: Boolean = false,
+                 counterexample :Option[CounterexampleConfig] = None
             ) {
   def merge(other: Config): Config = {
     // this config takes precedence over other config
@@ -63,7 +67,8 @@ case class Config(
       shouldViperEncode = shouldViperEncode,
       checkOverflows = checkOverflows || other.checkOverflows,
       shouldVerify = shouldVerify,
-      int32bit = int32bit || other.int32bit
+      int32bit = int32bit || other.int32bit,
+      counterexample=counterexample
     )
   }
 
@@ -207,6 +212,20 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = false
   )
 
+  val counterexample:ScallopOption[CounterexampleConfig] = opt[CounterexampleConfig](
+    name = "counterexample",
+    descr = "Adds counterexamples to output can be run with: mapped, native, reduced, extended (default: no counterexample)"
+              +"curently works witch SILICON as a backend",
+    default = None,
+    noshort = false
+  )(singleArgConverter({ 
+    case "mapped" => CounterexampleConfigs.MappedCounterexamples
+    case "native" => CounterexampleConfigs.NativeCounterexamples
+    case "reduced" => CounterexampleConfigs.ReducedCounterexamples 
+    case "extended" => CounterexampleConfigs.ExtendedCounterexamples 
+    case _ => CounterexampleConfigs.MappedCounterexamples
+  }))
+
 
   /**
     * Exception handling
@@ -379,6 +398,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     shouldViperEncode = shouldViperEncode,
     checkOverflows = checkOverflows(),
     int32bit = int32Bit(),
-    shouldVerify = shouldVerify
+    shouldVerify = shouldVerify,
+    counterexample=counterexample.toOption
   )
 }

src/main/scala/viper/gobra/reporting/BackTranslator.scala

@@ -5,10 +5,13 @@
 // Copyright (c) 2011-2020 ETH Zurich.
 
 package viper.gobra.reporting
+import viper.gobra.ast.frontend._
+import viper.gobra.frontend.info.TypeInfo
 import viper.gobra.backend.BackendVerifier
-import viper.gobra.frontend.Config
+import viper.gobra.frontend.{Config,Parser}
 import viper.silver.{ast => vpr}
 import viper.silver
+import java.nio.file.{Path,Paths}
 
 import scala.annotation.unused
 
@@ -18,20 +21,27 @@ object BackTranslator {
     def translate(error: silver.verifier.VerificationError): VerificationError
     def translate(reason: silver.verifier.ErrorReason): VerificationErrorReason
   }
-
-  case class BackTrackInfo(
+ case class VerificationBackTrackInfo(
                             errorT: Seq[BackTranslator.ErrorTransformer],
                             reasonT: Seq[BackTranslator.ReasonTransformer]
                           )
+  case class BackTrackInfo(
+                            errorT: Seq[BackTranslator.ErrorTransformer],
+                            reasonT: Seq[BackTranslator.ReasonTransformer],
+                            viperprogram:vpr.Program,
+                            typeInfo:TypeInfo,
+                            config:Config
+                          )
 
   type ErrorTransformer = PartialFunction[silver.verifier.VerificationError, VerificationError]
   type ReasonTransformer = PartialFunction[silver.verifier.ErrorReason, VerificationErrorReason]
 
-  def backTranslate(result: BackendVerifier.Result)(@unused config: Config): VerifierResult = result match {
+  def backTranslate(result: BackendVerifier.Result)(/* @unused */ config: Config): VerifierResult = 
+  result match {
     case BackendVerifier.Success => VerifierResult.Success
-    case BackendVerifier.Failure(errors, backtrack) =>
-      val errorTranslator = new DefaultErrorBackTranslator(backtrack)
-      VerifierResult.Failure(errors map errorTranslator.translate)
+    case BackendVerifier.Failure(errors, backtrack) => 
+      val errorTranslator =  new DefaultErrorBackTranslator(backtrack.copy(config=config)) //TODO make this more clean e.g. remove config from backtrack Info
+      VerifierResult.Failure(errors map  errorTranslator.translate)
   }
 
   implicit class RichErrorMessage(error: silver.verifier.ErrorMessage) {