Merge branch 'master' into add-test-report

annotation/Terms.example.scala

@@ -842,49 +842,6 @@ object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Te
   }
 }
 
-/*
-  Helper class for permissions
- */
-
-final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
-  require(d != 0, "Denominator of Rational must not be 0.")
-
-  private val g = n.gcd(d)
-  val numerator: BigInt = n / g * d.signum
-  val denominator: BigInt = d.abs / g
-
-  def +(that: Rational): Rational = {
-    val newNum = this.numerator * that.denominator + that.numerator * this.denominator
-    val newDen = this.denominator * that.denominator
-    Rational(newNum, newDen)
-  }
-  def -(that: Rational): Rational = this + (-that)
-  def unary_- = Rational(-numerator, denominator)
-  def abs = Rational(numerator.abs, denominator)
-  def signum = Rational(numerator.signum, 1)
-
-  def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)
-  def /(that: Rational): Rational = this * that.inverse
-  def inverse = Rational(denominator, numerator)
-
-  def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum
-
-  override def equals(obj: Any) = obj match {
-    case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
-    case _ => false
-  }
-
-  override lazy val toString = s"$numerator/$denominator"
-}
-
-object Rational extends ((BigInt, BigInt) => Rational) {
-  val zero = Rational(0, 1)
-  val one = Rational(1, 1)
-
-  def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)
-  def unapply(r: Rational) = Some(r.numerator, r.denominator)
-}
-
 /*
  * Permissions
  */

project/plugins.sbt

@@ -4,5 +4,5 @@
 //
 // Copyright (c) 2011-2019 ETH Zurich.
 
-addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.15.0")
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.10.0")
+addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.0.0")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.11.0")

src/main/resources/dafny_axioms/sequences.vpr

@@ -123,7 +123,7 @@ domain $Seq[E] {
     axiom {
         forall s: $Seq[E], t: $Seq[E], n: Int ::
         { Seq_take(Seq_append(s, t), n) }
-        n > 0 && n > Seq_length(s) ==> Seq_add(Seq_sub(n, Seq_length(s)), Seq_length(s)) == n && Seq_take(Seq_append(s, t), n) == Seq_append(s, Seq_take(t, Seq_sub(n, Seq_length(s))))
+        n > 0 && n > Seq_length(s) && n < Seq_length(Seq_append(s, t)) ==> Seq_add(Seq_sub(n, Seq_length(s)), Seq_length(s)) == n && Seq_take(Seq_append(s, t), n) == Seq_append(s, Seq_take(t, Seq_sub(n, Seq_length(s))))
     }
     axiom {
         forall s: $Seq[E], t: $Seq[E], n: Int ::

src/main/resources/magic_wand_snap_functions_declarations.smt2

@@ -0,0 +1 @@
+(declare-fun MWSF_apply ($MWSF $Snap) $Snap)

src/main/scala/Config.scala

@@ -818,6 +818,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val enableDebugging: ScallopOption[Boolean] = opt[Boolean]("enableDebugging",
+    descr = "Enable debugging mode",
+    default = Some(false),
+    noshort = true
+  )
+
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {

src/main/scala/Utils.scala

@@ -6,20 +6,23 @@
 
 package viper.silicon
 
-import scala.annotation.implicitNotFound
-import scala.collection.immutable.ArraySeq
+import viper.silicon.state.terms._
+import viper.silicon.verifier.Verifier
 import viper.silver
+import viper.silver.ast.utility.Triggers.TriggerGenerationWithAddAndSubtract
+import viper.silver.ast.utility.rewriter.Traverse
+import viper.silver.ast.SourcePNodeInfo
 import viper.silver.components.StatefulComponent
-import viper.silver.verifier.{VerificationError, errors}
+import viper.silver.parser.{PExp, PType, PUnknown, PUnnamedTypedDeclaration}
 import viper.silver.verifier.errors.Internal
 import viper.silver.verifier.reasons.{FeatureUnsupported, UnexpectedNode}
-import viper.silver.ast.utility.rewriter.Traverse
-import viper.silicon.state.terms.{Sort, Term, Var}
-import viper.silicon.verifier.Verifier
-import viper.silver.ast.utility.Triggers.TriggerGenerationWithAddAndSubtract
+import viper.silver.verifier.{VerificationError, errors}
+
+import scala.annotation.implicitNotFound
+import scala.collection.immutable.ArraySeq
 
 package object utils {
-  def freshSnap: (Sort, Verifier) => Var = (sort, v) => v.decider.fresh(sort)
+  def freshSnap: (Sort, Verifier) => Var = (sort, v) => v.decider.fresh(sort, Option.when(Verifier.config.enableDebugging())(PUnknown()))
   def toSf(t: Term): (Sort, Verifier) => Term = (sort, _) => t.convert(sort)
 
   def mapReduceLeft[E](it: Iterable[E], f: E => E, op: (E, E) => E, unit: E): E =
@@ -131,6 +134,59 @@ package object utils {
                     (e0: silver.ast.Exp, e1: silver.ast.Exp) => silver.ast.Or(e0, e1)(e0.pos, e0.info),
                      silver.ast.FalseLit()(emptyPos))
 
+    def removeKnownToBeTrueExp(exps: List[silver.ast.Exp], terms: List[Term]): List[silver.ast.Exp] = {
+      exps.zip(terms).filter(t => t._2 != True).map(e => e._1)
+    }
+
+    def simplifyVariableName(str: String) : String = {
+      str.substring(0, str.lastIndexOf("@"))
+    }
+
+    def replaceVarsInExp(e: silver.ast.Exp, varNames: Seq[String], replacements: Seq[silver.ast.Exp]): silver.ast.Exp = {
+      silver.utility.Sanitizer.replaceFreeVariablesInExpression(e, varNames.zip(replacements).toMap, Set())
+    }
+
+    def extractPTypeFromStmt(stmt: silver.ast.Stmt): PType = {
+      stmt.info.getUniqueInfo[SourcePNodeInfo] match {
+        case Some(info) =>
+          val sourceNode = info.sourcePNode
+          sourceNode match {
+            case decl: PUnnamedTypedDeclaration => decl.typ
+            case _ => PUnknown()
+          }
+        case _ => PUnknown()
+      }
+    }
+
+    def extractPTypeFromExp(exp: silver.ast.Exp): PType = {
+      exp.info.getUniqueInfo[SourcePNodeInfo] match {
+        case Some(info) =>
+          val sourceNode = info.sourcePNode
+          sourceNode match {
+            case e: PExp => e.typ
+            case d: PUnnamedTypedDeclaration => d.typ
+            case _ => PUnknown()
+          }
+        case _ => PUnknown()
+      }
+    }
+
+    def buildMinExp(exps: Seq[silver.ast.Exp], typ: silver.ast.Type): silver.ast.Exp = {
+      exps match {
+        case Seq(e) => e
+        case Seq(e0, e1) => silver.ast.DebugPermMin(e0, e1)(e0.pos, e0.info)
+        case exps if exps.length > 2 => silver.ast.DebugPermMin(exps.head, buildMinExp(exps.tail, typ))(exps.head.pos, exps.head.info)
+      }
+    }
+
+    def buildQuantExp(quantifier: Quantifier, vars: Seq[silver.ast.LocalVarDecl], eBody: silver.ast.Exp, eTrigger: Seq[silver.ast.Trigger]): silver.ast.Exp = {
+      quantifier match {
+        case Forall => silver.ast.Forall(vars, eTrigger, eBody)(eBody.pos, eBody.info, eBody.errT)
+        case Exists => silver.ast.Exists(vars, eTrigger, eBody)(eBody.pos, eBody.info, eBody.errT)
+      }
+    }
+
+
     /** Note: be aware of Silver issue #95!*/
     def rewriteRangeContains(program: silver.ast.Program): silver.ast.Program =
       program.transform({
@@ -211,7 +267,7 @@ package object utils {
     def toUnambiguousShortString(resource: silver.ast.Resource): String = {
       resource match {
         case l: silver.ast.Location => l.name
-        case m: silver.ast.MagicWand => m.toString()
+        case m: silver.ast.MagicWand => m.toString
         case m@silver.ast.MagicWandOp => s"${silver.ast.MagicWandOp.op}@${sourceLineColumn(m)}"
       }
     }
@@ -222,6 +278,7 @@ package object utils {
     case class ViperEmbedding(embeddedSort: Sort) extends silver.ast.ExtensionType {
       def substitute(typVarsMap: Predef.Map[silver.ast.TypeVar, silver.ast.Type]): silver.ast.Type = this
       def isConcrete: Boolean = true
+      override def toString: String = s"ViperEmbedding(sorts.$embeddedSort)"
     }
   }