Adding a Viper plugin

build.sbt

@@ -4,6 +4,29 @@
 //
 // Copyright (c) 2011-2020 ETH Zurich.
 
+ThisBuild / scalaVersion := "2.13.10"
+ThisBuild / scalacOptions ++= Seq(
+    "-encoding", "UTF-8",               // Enforce UTF-8, instead of relying on properly set locales
+    "-deprecation",                     // Warn when using deprecated language features
+    "-unchecked",                       // Warn on generated code assumptions
+    "-feature",                         // Warn on features that requires explicit import
+    "-Wunused",                         // Warn on unused imports
+    "-Ypatmat-exhaust-depth", "40",     // Increase depth of pattern matching analysis
+    // "-Xfatal-warnings",                 // Treat Warnings as errors to guarantee code quality in future changes
+)
+
+// Enforce UTF-8, instead of relying on properly set locales
+ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8", "-charset", "UTF-8", "-docencoding", "UTF-8")
+ThisBuild / javaOptions  ++= Seq("-Dfile.encoding=UTF-8")
+
+// Publishing settings
+
+// Allows 'publishLocal' SBT command to include test artifacts in a dedicated JAR file
+// (whose name is postfixed by 'test-source') and publish it in the local Ivy repository.
+// This JAR file contains all classes and resources for testing and projects like Carbon
+// and Silicon can rely on it to access the test suit implemented in Silver.
+ThisBuild / Test / publishArtifact := true
+
 // Import general settings from Silver
 lazy val silver = project in file("silver")
 

project/build.properties

@@ -1,2 +1,2 @@
-sbt.version=1.4.4
+sbt.version=1.6.2
 

src/main/scala/SIFAstExtensions.scala

@@ -125,6 +125,21 @@ case class SIFLowExp(exp: Exp, comparator: Option[String] = None, typVarMap: Map
   override val extensionIsPure: Boolean = exp.isPure
 }
 
+case class SIFRelExp(exp: Exp, i: IntLit)
+                    (val pos: Position = NoPosition,
+                     val info: Info = NoInfo,
+                     val errT: ErrorTrafo = NoTrafos) extends ExtensionExp {
+  override def extensionSubnodes: Seq[Node] = Seq(exp, i)
+
+  override def typ: Type = exp.typ
+
+  override def verifyExtExp(): VerificationResult = ???
+
+  override def prettyPrint: PrettyPrintPrimitives#Cont = (text("rel") <> parens(show(exp) <> "," <+> show(i)))
+
+  override val extensionIsPure: Boolean = exp.isPure
+}
+
 case class SIFLowEventExp()(val pos: Position = NoPosition,
                             val info: Info = NoInfo,
                             val errT: ErrorTrafo = NoTrafos) extends ExtensionExp {

src/main/scala/SIFError.scala

@@ -12,7 +12,7 @@ import viper.silver.verifier._
 
 
 case class SIFTerminationChannelCheckFailed(offendingNode: ErrorNode, reason: ErrorReason,
-                                            override val cached: Boolean = false) extends AbstractVerificationError {
+                                            override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
   val id: String = "termination_channel_check.failed"
   val text: String = "Termination channel might exist."
   override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
@@ -21,31 +21,31 @@ case class SIFTerminationChannelCheckFailed(offendingNode: ErrorNode, reason: Er
   override def withReason(r: ErrorReason): AbstractVerificationError = SIFTerminationChannelCheckFailed(offendingNode, r)
 }
 
-case class SIFFoldNotLow(offendingNode: Fold) extends AbstractErrorReason {
+case class SIFFoldNotLow(offendingNode: Fold) extends ExtensionAbstractErrorReason {
   val id: String = "sif.fold"
   val readableMessage: String = s"The low parts of predicate ${offendingNode.acc.loc.predicateName} might not hold."
 
   override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
     SIFFoldNotLow(offendingNode.asInstanceOf[Fold])
 }
 
-case class SIFUnfoldNotLow(offendingNode: Unfold) extends AbstractErrorReason {
+case class SIFUnfoldNotLow(offendingNode: Unfold) extends ExtensionAbstractErrorReason {
   val id: String = "sif.unfold"
   val readableMessage: String = s"The low parts of predicate ${offendingNode.acc.loc.predicateName} might not hold."
 
   override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
     SIFUnfoldNotLow(offendingNode.asInstanceOf[Unfold])
 }
 
-case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
+case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
   val id: String = "sif_termination.condition_not_low"
   val readableMessage: String = s"Termination condition ${offendingNode.cond} might not be low."
 
   override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
     SIFTermCondNotLow(offendingNode.asInstanceOf[SIFTerminatesExp])
 }
 
-case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
+case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
   val id: String = "sif_termination.not_lowevent"
   val readableMessage: String =
     s"Termination condition ${offendingNode.cond} evaluating to false might not imply both executions don't terminate."
@@ -54,7 +54,7 @@ case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends Abstract
     SIFTermCondLowEvent(offendingNode.asInstanceOf[SIFTerminatesExp])
 }
 
-case class SIFTermCondNotTight(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
+case class SIFTermCondNotTight(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
   val id: String = "sif_termination.condition_not_tight"
   val readableMessage: String = s"Termination condition ${offendingNode.cond} might not be tight."
 

src/main/scala/SIFExtendedTransformer.scala

@@ -134,8 +134,9 @@ trait SIFExtendedTransformer {
       p.methods.map(m => translateMethod(m))
     }
 
-    p.copy(domains = newDomains, fields = newFields, functions = newFunctions, predicates = newPredicates,
+    val res = p.copy(domains = newDomains, fields = newFields, functions = newFunctions, predicates = newPredicates,
       methods = newMethods)(p.pos, p.info, p.errT)
+    res
   }
 
   def getName(orig: String) : String = {
@@ -1271,7 +1272,9 @@ trait SIFExtendedTransformer {
     val relVars = e.filter{
       case _: SIFLowExp => true
       case _: SIFLowEventExp => true
-      case f@DomainFuncApp("Low", args, _) => true
+      case _: SIFRelExp => true
+      case f@DomainFuncApp("Low", _, _) => true
+      case f@DomainFuncApp("LowEvent", Seq(), _) => true
       case _ => false
     }
     relVars.isEmpty
@@ -1395,6 +1398,8 @@ trait SIFExtendedTransformer {
       // for the domain method low, used e.g. for list resource
       case f@DomainFuncApp("Low", args, _) => translateSIFAss(
         SIFLowExp(args.head, None)(f.pos, f.info, f.errT), ctx, relAssertCtx)
+      case f@DomainFuncApp("LowEvent", Seq(), _) => translateSIFAss(
+        SIFLowEventExp()(f.pos, f.info, f.errT), ctx, relAssertCtx)
       case pap@PredicateAccessPredicate(pred, _) =>
         val (lowFunc, lhs) = getPredicateLowFuncExp(pred.predicateName, ctx, Some((p1, p2)))
         lowFunc match {
@@ -1450,7 +1455,9 @@ trait SIFExtendedTransformer {
       case pa@PredicateAccess(args, name) => PredicateAccess(args.map(a => translatePrime(a, p1, p2)),
         primedNames(name))(pa.pos, pa.info, pa.errT)
       case l: SIFLowExp => Implies(And(p1, p2)(), translateSIFLowExpComparison(l, p1, p2))()
+      case SIFRelExp(e, i) => if(i.i == BigInt.int2bigInt(1)) translatePrime(e, p1, p2) else translateNormal(e, p1, p2)
       case f@DomainFuncApp("Low", args, _) => TrueLit()()
+      case f@DomainFuncApp("LowEvent", Seq(), _) => TrueLit()()
       case f@ForPerm(vars, location, body) => ForPerm(vars,
         translateResourceAccess(location),
         translatePrime(body, p1, p2))(f.pos, f.info, f.errT)
@@ -1460,6 +1467,7 @@ trait SIFExtendedTransformer {
   def translateNormal[T <: Exp](e: T, p1: Exp, p2: Exp): T = {
     e.transform{
       case l: SIFLowExp => Implies(And(p1, p2)(), translateSIFLowExpComparison(l, p1, p2))()
+      case SIFRelExp(e, i) => if(i.i == BigInt.int2bigInt(1)) translatePrime(e, p1, p2) else translateNormal(e, p1, p2)
       case f@DomainFuncApp("Low", args, _) => Implies(And(p1, p2)(), translateSIFLowExpComparison(SIFLowExp(args.head)(), p1, p2))()
     }
   }
@@ -1475,7 +1483,8 @@ trait SIFExtendedTransformer {
   def translateToUnary(e: Exp): Exp = {
     val transformed = e.transform{
       case _: SIFLowExp => TrueLit()()
-      case f@DomainFuncApp("Low", args, _) => TrueLit()()
+      case DomainFuncApp("Low", args, _) => TrueLit()()
+      case DomainFuncApp("LowEvent", Seq(), _) => TrueLit()()
       case Implies(_: SIFLowExp, _: SIFLowExp) => TrueLit()()
       case i@Implies(lhs, rhs) => Implies(lhs, translateToUnary(rhs))(i.pos, i.info, i.errT)
     }

src/main/scala/SIFPAstExtensions.scala

@@ -0,0 +1,101 @@
+// 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-2020 ETH Zurich.
+
+package viper.silver.sif
+
+import viper.silver.ast.{ExtensionExp, IntLit, NoPosition, Position}
+import viper.silver.parser.{NameAnalyser, PExp, PExtender, PIntLit, PNode, PType, PTypeSubstitution, Translator, TypeChecker, TypeHelper}
+
+case class PLowExp(e: PExp)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PExp {
+  typ = TypeHelper.Bool
+
+  override def typeSubstitutions = e.typeSubstitutions
+
+  override def forceSubstitution(ts: PTypeSubstitution): Unit = {
+    e.forceSubstitution(ts)
+  }
+
+  override val getSubnodes: Seq[PNode] = Seq(e)
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = {
+    t.checkTopTyped(e, None)
+    if (expected == TypeHelper.Bool)
+      None
+    else
+      Some(Seq(s"Expected type ${expected}, but got Bool"))
+  }
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
+    t.checkTopTyped(e, None)
+    None
+  }
+
+  override def translateExp(t: Translator): ExtensionExp = {
+    SIFLowExp(t.exp(e))(t.liftPos(this))
+  }
+}
+
+case class PLowEventExp()(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PExp {
+  typ = TypeHelper.Bool
+
+  override def typeSubstitutions = Seq()
+
+  override def forceSubstitution(ts: PTypeSubstitution): Unit = {}
+
+  override val getSubnodes: Seq[PNode] = Seq()
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = None
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = {
+    if (expected == TypeHelper.Bool)
+      None
+    else
+      Some(Seq(s"Expected type ${expected}, but got Bool"))
+  }
+
+  override def translateExp(t: Translator): ExtensionExp = {
+    SIFLowEventExp()(t.liftPos(this))
+  }
+}
+
+case class PRelExp(e: PExp, i: PIntLit)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PExp {
+
+  override def typeSubstitutions = e.typeSubstitutions
+
+  override def forceSubstitution(ts: PTypeSubstitution): Unit = {
+    e.forceSubstitution(ts)
+  }
+
+  override val getSubnodes: Seq[PNode] = Seq(e, i)
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
+    t.checkTopTyped(e, None)
+    t.checkTopTyped(i, Some(TypeHelper.Int))
+    typ = e.typ
+    if (i.i == BigInt.int2bigInt(0) || i.i == BigInt.int2bigInt(1))
+      None
+    else
+      Some(Seq(s"Second argument of rel must be 0 or 1, but is ${i.i}"))
+  }
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = {
+    t.checkTopTyped(e, None)
+    t.checkTopTyped(i, Some(TypeHelper.Int))
+    typ = e.typ
+    if (i.i == BigInt.int2bigInt(0) || i.i == BigInt.int2bigInt(1)) {
+      if (expected == e.typ)
+        None
+      else
+        Some(Seq(s"Expected type ${expected}, but got ${e.typ}"))
+    } else {
+      Some(Seq(s"Second argument of rel must be 0 or 1, but is ${i.i}"))
+    }
+  }
+
+  override def translateExp(t: Translator): ExtensionExp = {
+    SIFRelExp(t.exp(e), t.exp(i).asInstanceOf[IntLit])(t.liftPos(this))
+  }
+}

src/main/scala/SIFPlugin.scala

@@ -0,0 +1,39 @@
+// 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-2020 ETH Zurich.
+
+
+package viper.silver.sif
+
+import fastparse._
+import viper.silver.ast.Program
+import viper.silver.parser.FastParser
+import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
+import viper.silver.parser.FastParserCompanion.whitespace
+
+import scala.annotation.unused
+
+class SIFPlugin(@unused reporter: viper.silver.reporter.Reporter,
+                @unused logger: ch.qos.logback.classic.Logger,
+                config: viper.silver.frontend.SilFrontendConfig,
+                fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+  import fp.{FP, exp, integer, ParserExtension}
+
+  def low[$: P]: P[PLowExp] = FP("low" ~ "(" ~ exp ~ ")").map { case (pos, e) => PLowExp(e)(pos) }
+  def rel[$: P]: P[PRelExp] = FP("rel" ~ "(" ~ exp ~ "," ~ integer ~ ")").map { case (pos, (e, i)) => PRelExp(e, i)(pos) }
+  def lowEvent[$: P]: P[PLowEventExp] = FP("lowEvent").map { case (pos, _) => PLowEventExp()(pos) }
+
+  override def beforeParse(input: String, isImported: Boolean): String = {
+    ParserExtension.addNewKeywords(Set[String]("low", "lowEvent", "rel"))
+    ParserExtension.addNewExpAtEnd(low(_))
+    ParserExtension.addNewExpAtEnd(rel(_))
+    ParserExtension.addNewExpAtEnd(lowEvent(_))
+    input
+  }
+
+  override def beforeVerify(input: Program): Program = {
+    SIFExtendedTransformer.transform(input, false)
+  }
+}