Merge pull request #541 from viperproject/option-for-disabling-global…

…-vars

CLI Option for Disabling Support for Global Variables

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

@@ -21,6 +21,7 @@ import viper.gobra.util.{TypeBounds, Violation}
 import viper.silver.ast.SourcePosition
 
 import scala.concurrent.duration.Duration
+import scala.util.matching.Regex
 
 object LoggerDefaults {
   val DefaultLevel: Level = Level.INFO
@@ -62,6 +63,7 @@ object ConfigDefaults {
   lazy val DefaultAssumeInjectivityOnInhale: Boolean = true
   lazy val DefaultParallelizeBranches: Boolean = false
   lazy val DefaultDisableMoreCompleteExhale: Boolean = false
+  lazy val DefaultEnableLazyImports: Boolean = false
 }
 
 case class Config(
@@ -109,6 +111,7 @@ case class Config(
                    // branches will be verified in parallel
                    parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
                    disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale,
+                   enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
 ) {
 
   def merge(other: Config): Config = {
@@ -150,6 +153,7 @@ case class Config(
       assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale,
       parallelizeBranches = parallelizeBranches,
       disableMoreCompleteExhale = disableMoreCompleteExhale,
+      enableLazyImports = enableLazyImports || other.enableLazyImports,
     )
   }
 
@@ -163,10 +167,13 @@ case class Config(
 
 object Config {
   // the header signals that a file should be considered when running on "header-only" mode
-  val header = """\/\/\s*\+gobra""".r
+  val header: Regex = """\/\/\s*\+gobra""".r
   val prettyPrintedHeader = "// +gobra"
   require(header.matches(prettyPrintedHeader))
   def sourceHasHeader(s: Source): Boolean = header.findFirstIn(s.content).nonEmpty
+
+  val enableLazyImportOptionName = "enableLazyImport"
+  val enableLazyImportOptionPrettyPrinted = s"--$enableLazyImportOptionName"
 }
 
 // have a look at `Config` to see an inline description of some of these parameters
@@ -192,6 +199,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale,
                       parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
                       disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale,
+                      enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -242,6 +250,7 @@ trait RawConfig {
     assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale,
     parallelizeBranches = baseConfig.parallelizeBranches,
     disableMoreCompleteExhale = baseConfig.disableMoreCompleteExhale,
+    enableLazyImports = baseConfig.enableLazyImports,
   )
 }
 
@@ -583,6 +592,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     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.",
+    default = Some(ConfigDefaults.DefaultEnableLazyImports),
+    noshort = true,
+  )
+
   /**
     * Exception handling
     */
@@ -715,5 +731,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     assumeInjectivityOnInhale = assumeInjectivityOnInhale(),
     parallelizeBranches = parallelizeBranches(),
     disableMoreCompleteExhale = disableMoreCompleteExhale(),
+    enableLazyImports = enableLazyImports(),
   )
 }

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

@@ -3063,7 +3063,17 @@ object Desugar {
       // As for imported methods, imported packages are not checked to satisfy their specification. In particular,
       // Gobra does not check that the package postconditions are established by the initialization code. Instead,
       // this is assumed. We only generate the proof obligations for the initialization code in the main package.
-      registerPackage(mainPkg, specCollector, generateInitProof = true)(config)
+      // Note that `config.enableLazyImports` disables init blocks, global variables, import preconditions, and init
+      // postconditions in the type checker, which means that we do not have to generate an init proof.
+      registerPackage(mainPkg, specCollector, generateInitProof = !config.enableLazyImports)(config)
+
+      if (config.enableLazyImports) {
+        // early return to not add any proof obligations because we have made sure in the type checker that
+        // there aren't any global variables, init blocks, init postconditions, and import preconditions (in the
+        // packages that have been parsed). Note that packages that have been skipped because of the laziness might
+        // still contain such features.
+        return
+      }
 
       // check that the postconditions of every package are enough to satisfy all of their imports' preconditions
       val src = meta(mainPkg, info)
@@ -3121,8 +3131,9 @@ object Desugar {
         info.context.getTypeInfo(RegularImport(imp.importPath))(config) match {
           case Some(Right(tI)) =>
             val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info))
+            Violation.violation(!config.enableLazyImports || desugaredPre.isEmpty, s"Import precondition found despite running with ${Config.enableLazyImportOptionPrettyPrinted}")
             specCollector.addImportPres(tI.getTypeInfo.tree.originalRoot, desugaredPre)
-          case e => Violation.violation(s"Unexpected value found $e while importing ${imp.importPath}")
+          case e => Violation.violation(config.enableLazyImports, s"Unexpected value found $e while importing ${imp.importPath} - type information is assumed to be available for all packages when Gobra is executed with lazy imports disabled")
         }
       }
 

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

@@ -7,20 +7,26 @@
 package viper.gobra.frontend.info.implementation.typing
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{message, noMessages}
+import viper.gobra.GoVerifier
 import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PImplicitQualifiedImport, PImport, PNode, PUnqualifiedImport}
+import viper.gobra.frontend.Config
 import viper.gobra.frontend.PackageResolver.RegularImport
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 trait ImportTyping extends BaseTyping { this: TypeInfoImpl =>
 
   lazy val wellDefImport: WellDefinedness[PImport] = createWellDef { imp =>
-    forceNonLazyImport(imp.importPath, imp)
-    imp match {
+    (if (config.enableLazyImports) {
+      imp.importPres.flatMap(importPre => message(importPre, s"Import preconditions are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}"))
+    } else {
+      forceNonLazyImport(imp.importPath, imp)
+      noMessages
+    }) ++ (imp match {
       case _: PExplicitQualifiedImport => noMessages
       case _: PUnqualifiedImport => noMessages
       // this case should never occur as these nodes should get converted in the parse postprocessing step
       case n: PImplicitQualifiedImport => message(n, s"Explicit qualifier could not be derived")
-    }
+    })
   }
 
   // This method forces a package to be processed non-lazily - every import can cause side effects,

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

@@ -7,7 +7,9 @@
 package viper.gobra.frontend.info.implementation.typing
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages}
+import viper.gobra.GoVerifier
 import viper.gobra.ast.frontend._
+import viper.gobra.frontend.Config
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.Constants
 
@@ -26,19 +28,23 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
     case b: PConstDecl =>
       b.specs.flatMap(wellDefConstSpec)
     case g: PVarDecl if isGlobalVarDeclaration(g) =>
-      // HACK: without this explicit check, Gobra does not find repeated declarations
-      //       of global variables. This has to do with the changes introduced in PR #186.
-      //       We need this check nonetheless because the checks performed in the "true" branch
-      //       assume that the ids are well-defined.
-      val idsOkMsgs = g.left.flatMap(l => wellDefID(l).out)
-      if (idsOkMsgs.isEmpty) {
-        val isGhost = isEnclosingGhost(g)
-        g.right.flatMap(isExpr(_).out) ++
-          declarableTo.errors(g.right map exprType, g.typ map typeSymbType, g.left map idType)(g) ++
-          error(g, s"Currently, global variables cannot be made ghost", isGhost) ++
-          acyclicGlobalDeclaration.errors(g)(g)
+      if (config.enableLazyImports) {
+        error(g, s"Global variables are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}")
       } else {
-        idsOkMsgs
+        // HACK: without this explicit check, Gobra does not find repeated declarations
+        //       of global variables. This has to do with the changes introduced in PR #186.
+        //       We need this check nonetheless because the checks performed in the "true" branch
+        //       assume that the ids are well-defined.
+        val idsOkMsgs = g.left.flatMap(l => wellDefID(l).out)
+        if (idsOkMsgs.isEmpty) {
+          val isGhost = isEnclosingGhost(g)
+          g.right.flatMap(isExpr(_).out) ++
+            declarableTo.errors(g.right map exprType, g.typ map typeSymbType, g.left map idType)(g) ++
+            error(g, s"Currently, global variables cannot be made ghost", isGhost) ++
+            acyclicGlobalDeclaration.errors(g)(g)
+        } else {
+          idsOkMsgs
+        }
       }
     case s: PActualStatement =>
       wellDefStmt(s).out
@@ -68,7 +74,9 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private def wellDefIfInitBlock(n: PFunctionDecl): Messages = {
     val isInitFunc = n.id.name == Constants.INIT_FUNC_NAME
-    if (isInitFunc) {
+    if (isInitFunc && config.enableLazyImports) {
+      error(n, s"Init functions are not supported when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}")
+    } else if (isInitFunc) {
       val errorMsgEmptySpec =
         s"Currently, ${Constants.INIT_FUNC_NAME} blocks cannot have specification. Instead, use package postconditions and import preconditions."
       val errorMsgNoInOut = s"func ${Constants.INIT_FUNC_NAME} must have no arguments and no return values"

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

@@ -7,8 +7,10 @@
 package viper.gobra.frontend.info.implementation.typing
 
 import org.bitbucket.inkytonik.kiama.util.Entity
-import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error}
+import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message}
+import viper.gobra.GoVerifier
 import viper.gobra.ast.frontend.{PExpression, POld, PPackage, PProgram, PVarDecl}
+import viper.gobra.frontend.Config
 import viper.gobra.frontend.info.base.{SymbolTable => st}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode}
@@ -18,30 +20,34 @@ trait ProgramTyping extends BaseTyping { this: TypeInfoImpl =>
 
   lazy val wellDefProgram: WellDefinedness[PProgram] = createWellDef {
     case PProgram(_, posts, imports, members) =>
-      // Obtains global variable declarations sorted by the order in which they appear in the file
-      val sortedByPosDecls: Vector[PVarDecl] = {
-        val unsortedDecls: Vector[PVarDecl] = members.collect{ case d: PVarDecl => d }
-        // we require a package to be able to obtain position information
-        val pkgOpt: Option[PPackage] = unsortedDecls.headOption.flatMap(tryEnclosingPackage)
-        // sort declarations by the order in which they appear in the program
-        unsortedDecls.sortBy{ decl =>
-          pkgOpt.get.positions.positions.getStart(decl) match {
-            case Some(pos) => (pos.line, pos.column)
-            case _ => Violation.violation(s"Could not find position information of $decl.")
+      if (config.enableLazyImports) {
+        posts.flatMap(post => message(post, s"Init postconditions are not allowed when executing ${GoVerifier.name} with ${Config.enableLazyImportOptionPrettyPrinted}"))
+      } else {
+        // Obtains global variable declarations sorted by the order in which they appear in the file
+        val sortedByPosDecls: Vector[PVarDecl] = {
+          val unsortedDecls: Vector[PVarDecl] = members.collect{ case d: PVarDecl => d }
+          // we require a package to be able to obtain position information
+          val pkgOpt: Option[PPackage] = unsortedDecls.headOption.flatMap(tryEnclosingPackage)
+          // sort declarations by the order in which they appear in the program
+          unsortedDecls.sortBy{ decl =>
+            pkgOpt.get.positions.positions.getStart(decl) match {
+              case Some(pos) => (pos.line, pos.column)
+              case _ => Violation.violation(s"Could not find position information of $decl.")
+            }
           }
         }
-      }
-      // HACK: without this explicit check, Gobra does not find repeated declarations
-      //       of global variables. This has to do with the changes introduced in PR #186.
-      //       We need this check nonetheless because the checks performed in the "true" branch
-      //       assume that the ids are well-defined.
-      val idsOkMsgs = sortedByPosDecls.flatMap(d => d.left).flatMap(l => wellDefID(l).out)
-      if (idsOkMsgs.isEmpty) {
-        globalDeclSatisfiesDepOrder(sortedByPosDecls) ++
-          hasOldExpression(posts) ++
-          hasOldExpression(imports.flatMap(_.importPres))
-      } else {
-        idsOkMsgs
+        // HACK: without this explicit check, Gobra does not find repeated declarations
+        //       of global variables. This has to do with the changes introduced in PR #186.
+        //       We need this check nonetheless because the checks performed in the "true" branch
+        //       assume that the ids are well-defined.
+        val idsOkMsgs = sortedByPosDecls.flatMap(d => d.left).flatMap(l => wellDefID(l).out)
+        if (idsOkMsgs.isEmpty) {
+          globalDeclSatisfiesDepOrder(sortedByPosDecls) ++
+            hasOldExpression(posts) ++
+            hasOldExpression(imports.flatMap(_.importPres))
+        } else {
+          idsOkMsgs
+        }
       }
   }
 

src/test/resources/regressions/features/globals/globals-disabled-fail01.gobra

@@ -0,0 +1,58 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this is the same file as `globals-simple01.gobra` but additionally provides the `--disableGlobalVars` flag to Gobra.
+// ##(--enableLazyImport)
+
+//:: ExpectedOutput(type_error)
+initEnsures acc(&A) && acc(&B) && acc(&C, 1/2)
+package pkg
+
+//:: ExpectedOutput(type_error)
+importRequires true
+import "fmt"
+
+import (
+    //:: ExpectedOutput(type_error)
+	importRequires true
+	//:: ExpectedOutput(type_error)
+	importRequires true
+	"bytes"
+	//:: ExpectedOutput(type_error)
+	importRequires true
+	"sync"
+)
+
+
+//:: ExpectedOutput(type_error)
+var A int = 0
+//:: ExpectedOutput(type_error)
+var B, C = f()
+//:: ExpectedOutput(type_error)
+var _ = g()
+//:: ExpectedOutput(type_error)
+var D struct{}
+
+decreases
+func f() (int, bool)
+
+decreases
+func g() interface{}
+
+requires acc(&A, 1/2) && A == 1
+ensures  acc(&A, 1/2)
+func testRead() {
+	var v1 int = A
+	assert v1 == 1
+}
+
+requires acc(&C) && C
+func testWrite() {
+	C = false
+}
+
+// Variable hiding works correctly, as in Go
+func tesVarHiding() {
+	var A int = 0
+	assert A == 0
+}