Add option to disable set axiomatization (#708)

* Add disableSetAxiomatization to Config

* Add noaxioms/sets.vpr to resources

* Pass noaxiom version of sets.vpr to Silicon

* Clarify README.md

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Remove newline
---------

Co-authored-by: Daniel Nezamabadi <dnezamabadi@ethz.ch>

src/main/resources/README.md

@@ -20,3 +20,8 @@ import stubAssert "github.com/scionproto/scion/go/lib/assert"
 Note that the import path directly corresponds to the directory structure in `stubs`.
 As `assert` is a reserved keyword in Gobra and the implicit qualifier would be `assert`, the library is imported with the qualifier `stubAssert`.
 The implicit qualifier corresponds to the last path component (here `assert`) and is not related to the package clause used in Gobra files located in the `assert` folder.
+
+## noaxioms
+The `.vpr` files in the `noaxioms` folder contain minimal definitions of operations on the various built-in Viper types. These files are used when we disable the built-in axiomatisation of the Viper files.
+`sets.vpr` for example is used when the flag `--disableSetAxiomatization` is passed to Gobra, which in turn is useful if the user
+wants to manually prove obligations using the standard library.

src/main/resources/noaxioms/sets.vpr

@@ -0,0 +1,19 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2023 ETH Zurich.
+
+domain $Set[E] {
+  function Set_in(e: E, s: $Set[E]): Bool
+  function Set_card(s: $Set[E]): Int
+  function Set_empty(): $Set[E]
+  function Set_singleton(e: E): $Set[E]
+  function Set_unionone(s: $Set[E], e: E): $Set[E]
+  function Set_union(s1: $Set[E], s2: $Set[E]): $Set[E]
+  function Set_disjoint(s1: $Set[E], s2: $Set[E]): Bool
+  function Set_difference(s1: $Set[E], s2: $Set[E]): $Set[E]
+  function Set_intersection(s1: $Set[E], s2: $Set[E]): $Set[E]
+  function Set_subset(s1: $Set[E], s2: $Set[E]): Bool
+  function Set_equal(s1: $Set[E], s2: $Set[E]): Bool
+}

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

@@ -13,6 +13,10 @@ import viper.server.core.ViperCoreServer
 import viper.silicon.decider.Z3ProverAPI
 import viper.server.vsi.DefaultVerificationServerStart
 
+import java.nio.file.{Files, Paths}
+import scala.io.Source
+import scala.util.Using
+
 trait ViperBackend {
   def create(exePaths: Vector[String], config: Config)(implicit executor: GobraExecutionContext): ViperVerifier
 }
@@ -47,6 +51,20 @@ object ViperBackends {
         options ++= Vector("--parallelizeBranches")
       }
       options ++= exePaths
+      if (config.disableSetAxiomatization) {
+        // Since resources are stored within the .jar archive, we cannot
+        // directly pass the axiom file to Silicon.
+        val tmpPath = Paths.get("gobra_tmp")
+        val axiomTmpPath = tmpPath.resolve("noaxioms_sets.vpr")
+        val axiom: Source = Source.fromResource("noaxioms/sets.vpr")
+
+        Files.createDirectories(tmpPath)
+        Using(axiom) { source =>
+          Files.write(axiomTmpPath, source.mkString.getBytes)
+        }
+
+        options ++= Vector("--setAxiomatizationFile", axiomTmpPath.toString())
+      }
 
       new Silicon(options)
     }

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

@@ -73,6 +73,7 @@ object ConfigDefaults {
   lazy val DefaultNoStreamErrors: Boolean = false
   lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
   lazy val DefaultRequireTriggers: Boolean = false
+  lazy val DefaultDisableSetAxiomatization: Boolean = false
 }
 
 // More-complete exhale modes
@@ -139,6 +140,7 @@ case class Config(
                    parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
                    // when enabled, all quantifiers without triggers are rejected
                    requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
+                   disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
 ) {
 
   def merge(other: Config): Config = {
@@ -188,7 +190,8 @@ case class Config(
       noVerify = noVerify || other.noVerify,
       noStreamErrors = noStreamErrors || other.noStreamErrors,
       parseAndTypeCheckMode = parseAndTypeCheckMode,
-      requireTriggers = requireTriggers || other.requireTriggers
+      requireTriggers = requireTriggers || other.requireTriggers,
+      disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization,
     )
   }
 
@@ -243,6 +246,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
                       parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
                       requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
+                      disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -301,6 +305,7 @@ trait RawConfig {
     noStreamErrors = baseConfig.noStreamErrors,
     parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode,
     requireTriggers = baseConfig.requireTriggers,
+    disableSetAxiomatization = baseConfig.disableSetAxiomatization,
   )
 }
 
@@ -718,6 +723,12 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     case _ => ConfigDefaults.DefaultParseAndTypeCheckMode
   }
 
+  val disableSetAxiomatization: ScallopOption[Boolean] = opt[Boolean](
+    name = "disableSetAxiomatization",
+    descr = s"Disables set axiomatization in Silicon.",
+    default = Some(ConfigDefaults.DefaultDisableSetAxiomatization),
+    noshort = true,
+  )
   /**
     * Exception handling
     */
@@ -782,6 +793,18 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
       Right(())
     }
   }
+
+  // `disableSetAxiomatization` can only be provided when using a silicon-based backend
+  // since, at the time of writing, we rely on Silicon's setAxiomatizationFile for the
+  // implementation
+  addValidation {
+    val disableSetAxiomatizationOn = disableSetAxiomatization.toOption.contains(true)
+    if (disableSetAxiomatizationOn && !isSiliconBasedBackend) {
+      Left("The selected backend does not support --disableSetAxiomatization.")
+    } else {
+      Right(())
+    }
+  }
 
   addValidation {
     if (!disableNL.toOption.contains(true) || isSiliconBasedBackend) {
@@ -885,5 +908,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noStreamErrors = noStreamErrors(),
     parseAndTypeCheckMode = parseAndTypeCheckMode(),
     requireTriggers = requireTriggers(),
+    disableSetAxiomatization = disableSetAxiomatization(),
   )
 }

src/test/resources/regressions/features/sets/set-disable-axioms-fail1.gobra

@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+// ##(--disableSetAxiomatization)
+
+// From set-union-simple1.gobra, example 10
+func foo(ghost s set[int], ghost t set[int]) {
+	// fails: set axioms disabled (including commutativity)
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert s union t == t union s
+}