Advanced logical proofs

src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala

@@ -133,7 +133,7 @@ object ImpureAssumeRewriter {
       assert(conds.isEmpty)
       assert(cond.isEmpty)
 
-      PermGeCmp(permLoc, perm)()
+      PermGeCmp(permLoc, perm)(permLoc.pos, permLoc.info, permLoc.errT)
     } else {
       val perms: Seq[Exp] = (contextWithoutRcv map (_._2)) :+ perm
 
@@ -146,7 +146,7 @@ object ImpureAssumeRewriter {
       val func = funcs(contextWithoutRcv.length-1)
       val funcApp = DomainFuncApp(func, conds ++ perms, Map[TypeVar, Type]())()
 
-      PermGeCmp(permLoc, funcApp)()
+      PermGeCmp(permLoc, funcApp)(permLoc.pos, permLoc.info, permLoc.errT)
     }
   }
 

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -107,6 +107,7 @@ trait SilFrontend extends DefaultFrontend {
     "viper.silver.plugin.standard.adt.AdtPlugin",
     "viper.silver.plugin.standard.termination.TerminationPlugin",
     "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin",
+    "viper.silver.plugin.standard.reasoning.ReasoningPlugin",
     refutePlugin
   )
 

src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala

@@ -0,0 +1,146 @@
+// 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-2024 ETH Zurich.
+
+package viper.silver.plugin.standard.reasoning
+
+
+import viper.silver.ast.utility.Expressions
+import viper.silver.ast.{Apply, Declaration, Exhale, Exp, FieldAssign, Fold, Inhale, LocalVarDecl, Method, MethodCall, Package, Program, Seqn, Stmt, Unfold}
+import viper.silver.verifier.{AbstractError, ConsistencyError}
+import viper.silver.plugin.standard.reasoning.analysis.AnalysisUtils
+
+import scala.collection.mutable
+
+trait BeforeVerifyHelper {
+  /** methods to rename variables for the encoding of the new syntax */
+  def uniqueName(name: String, usedNames: mutable.Set[String]): String = {
+    var i = 1
+    var newName = name
+    while (usedNames.contains(newName)) {
+      newName = name + i
+      i += 1
+    }
+    usedNames.add(newName)
+    newName
+  }
+
+  def substituteWithFreshVars[E <: Exp](vars: Seq[LocalVarDecl], exp: E, usedNames: mutable.Set[String]): (Seq[(LocalVarDecl, LocalVarDecl)], E) = {
+    val declMapping = vars.map(oldDecl =>
+      oldDecl -> LocalVarDecl(uniqueName(oldDecl.name, usedNames), oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT))
+    val transformedExp = applySubstitution(declMapping, exp)
+    (declMapping, transformedExp)
+  }
+
+  def applySubstitution[E <: Exp](mapping: Seq[(LocalVarDecl, LocalVarDecl)], exp: E): E = {
+    Expressions.instantiateVariables(exp, mapping.map(_._1.localVar), mapping.map(_._2.localVar))
+  }
+
+  def applySubstitutionWithExp[E <: Exp](mapping: Seq[(LocalVarDecl, Exp)], exp: E): E = {
+    Expressions.instantiateVariables(exp, mapping.map(_._1.localVar), mapping.map(_._2))
+  }
+
+  /**
+    * check that all variables (`modified_vars`) that are assigned to inside a universal introduction `u`'s block are
+    * distinct from the universal introduction `u`'s quantified variables `quantified_vars`. Otherwise, an error is
+    * reported via `reportError` since these quantified variables should be immutable.
+    *
+    * @param modified_vars: set of variables that were modified in a given statement
+    * @param quantified_vars: set of quantified variables in the universal introduction statement.
+    * @param reportError: Method to report the error when a qunatified variable was modified
+    * @param u: universal introduction statement, used for details in error message
+    */
+  def checkReassigned(modified_vars: Set[LocalVarDecl], quantified_vars: Seq[LocalVarDecl], reportError: AbstractError => Unit, u: UniversalIntro): Unit = {
+      val reassigned_vars: Set[LocalVarDecl] = modified_vars.intersect(quantified_vars.toSet)
+      if (reassigned_vars.nonEmpty) {
+        val reassigned_names: String = reassigned_vars.mkString(", ")
+        val reassigned_pos: String = reassigned_vars.map(_.pos).mkString(", ")
+        reportError(ConsistencyError("Universal Introduction variable(s) (" + reassigned_names + ") might have been reassigned at position(s) (" + reassigned_pos + ")", u.pos))
+      }
+  }
+
+  /** returns true if method `m` is annotated to be a lemma */
+ def specifiesLemma(m: Method): Boolean = (m.pres ++ m.posts).exists {
+    case _: Lemma => true
+    case _ => false
+  }
+
+  /** Checks that all lemmas in `input` satisfy the syntactical restrictions and, otherwise, reports errors by invoking `reportError`.  */
+  def checkLemmas(input: Program, reportError: AbstractError => Unit): Unit = {
+    input.methods.foreach(method => {
+      val containsLemma = specifiesLemma(method)
+      val (containsDecreases, containsDecreasesStar) = AnalysisUtils.specifiesTermination(method)
+
+      if (containsLemma) {
+        /** report error if there is no decreases clause or specification */
+        if(!containsDecreases) {
+          reportError(ConsistencyError(s"Lemmas must terminate but method ${method.name} marked lemma does not specify any termination measures", method.pos))
+        }
+
+        /** report error if the decreases statement might not prove termination */
+        if (containsDecreasesStar) {
+          reportError(ConsistencyError("Lemmas must terminate but method ${method.name} marked lemma specifies only incomplete termination measures", method.pos))
+        }
+
+        /** check method body for impure statements */
+        checkStmtPure(method.body.getOrElse(Seqn(Seq(), Seq())()), method, input, reportError)
+      }
+    })
+  }
+
+  /** checks whether a statement `stmt` is pure, reports error if impure operation found */
+  def checkStmtPure(stmt: Stmt, method: Method, prog: Program, reportError: AbstractError => Unit): Boolean = {
+    stmt match {
+      case Seqn(ss, _) =>
+        ss.forall(s => checkStmtPure(s, method, prog, reportError))
+
+        /** case for statements considered impure */
+      case ie@(Inhale(_) | Exhale(_) | FieldAssign(_, _) | Fold(_) | Unfold(_) | Apply(_) | Package(_, _)) =>
+        reportError(ConsistencyError(s"method ${method.name} marked lemma might contain impure statement $ie", ie.pos))
+        false
+      case m@MethodCall(methodName, _, _) =>
+        val mc = prog.findMethod(methodName)
+        val isLemmaCall = specifiesLemma(mc)
+
+        /** if called method is not a lemma report error */
+        if (!isLemmaCall) {
+          reportError(ConsistencyError(s"method ${method.name} marked lemma might contain call to method $m", m.pos))
+        }
+        isLemmaCall
+      case _ => true
+    }
+  }
+
+  /** checks that all influences by annotations in `input` are used correctly. */
+  def checkInfluencedBy(input: Program, reportError: AbstractError => Unit): Unit = {
+    input.methods.foreach(method => {
+      val argVars = method.formalArgs.toSet + AnalysisUtils.heapVertex
+      val retVars = method.formalReturns.toSet.asInstanceOf[Set[Declaration]] + AnalysisUtils.heapVertex + AnalysisUtils.AssumeMethodNode(method.pos)
+
+      val seenVars: mutable.Set[Declaration] = mutable.Set()
+      /** iterate through method postconditions to find flow annotations */
+      method.posts.foreach {
+        case v@FlowAnnotation(target, args) =>
+          val targetVarDecl = AnalysisUtils.getDeclarationFromFlowVar(target, method)
+
+          if (!retVars.contains(targetVarDecl)) {
+            reportError(ConsistencyError(s"Only return parameters, the heap or assumes can be influenced. ${targetVarDecl.name} is not be a return parameter.", v.pos))
+          }
+          if (seenVars.contains(targetVarDecl)) {
+            reportError(ConsistencyError(s"Only one influenced by expression per return parameter can exist. ${targetVarDecl.name} is used several times.", v.pos))
+          }
+          seenVars.add(targetVarDecl)
+
+          args.foreach(arg => {
+            val argVarDecl = AnalysisUtils.getLocalVarDeclFromFlowVar(arg)
+            if (!argVars.contains(argVarDecl)) {
+              reportError(ConsistencyError(s"Only method input parameters or the heap can influence a return parameter. ${argVarDecl.name} is not be a method input parameter.", v.pos))
+            }
+          })
+        case _ =>
+      }
+    })
+  }
+}

src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningASTExtension.scala

@@ -0,0 +1,173 @@
+// 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-2024 ETH Zurich.
+
+package viper.silver.plugin.standard.reasoning
+
+import viper.silver.ast._
+import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, brackets, char, defaultIndent, group, line, nest, nil, parens, show, showBlock, showVars, space, ssep, text, toParenDoc}
+import viper.silver.ast.pretty.PrettyPrintPrimitives
+import viper.silver.ast.utility.Consistency
+import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult}
+
+
+case object ReasoningInfo extends FailureExpectedInfo
+
+case class ExistentialElim(varList: Seq[LocalVarDecl], trigs: Seq[Trigger], exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt {
+  override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(exp) ++
+    (if (!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of existential elimination must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++
+    (if (varList.isEmpty) Seq(ConsistencyError("Existential elimination must have at least one quantified variable.", pos)) else Seq())
+
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = {
+    text("obtain") <+> showVars(varList) <+>
+      text("where") <+> (if (trigs.isEmpty) nil else ssep(trigs map show, space)) <+>
+      toParenDoc(exp)
+  }
+
+  override val extensionSubnodes: Seq[Node] = varList ++ trigs ++ Seq(exp)
+
+  /** declarations contributed by this statement that should be added to the parent scope */
+  override def declarationsInParentScope: Seq[Declaration] = varList
+}
+
+case class UniversalIntro(varList: Seq[LocalVarDecl], triggers: Seq[Trigger], assumingExp: Exp, implyingExp: Exp, block: Seqn)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt with Scope {
+  // See also Expression Line 566
+  override lazy val check: Seq[ConsistencyError] =
+    (if (!(assumingExp isSubtype Bool)) Seq(ConsistencyError(s"Assume expression of universal introduction must be of Bool type, but found ${assumingExp.typ}", assumingExp.pos)) else Seq()) ++
+    (if (!(implyingExp isSubtype Bool)) Seq(ConsistencyError(s"Implies expression of universal introduction must be of Bool type, but found ${implyingExp.typ}", implyingExp.pos)) else Seq()) ++
+    (if (varList.isEmpty) Seq(ConsistencyError("Quantifier must have at least one quantified variable.", pos)) else Seq()) ++
+    Consistency.checkAllVarsMentionedInTriggers(varList, triggers)
+
+  override val scopedDecls: Seq[Declaration] = varList
+
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = {
+    text("prove forall") <+> showVars(varList) <+>
+      text("assuming") <+>
+      toParenDoc(assumingExp) <+>
+      text("implies") <+> toParenDoc(implyingExp) <+>
+      showBlock(block)
+  }
+
+  override val extensionSubnodes: Seq[Node] = varList ++ triggers ++ Seq(assumingExp, implyingExp, block)
+}
+
+sealed trait FlowVar extends ExtensionExp {
+  override def extensionIsPure: Boolean = true
+
+  override def verifyExtExp(): VerificationResult = {
+    assert(assertion = false, "FlowAnalysis: verifyExtExp has not been implemented.")
+    Failure(Seq(ConsistencyError("FlowAnalysis: verifyExtExp has not been implemented.", pos)))
+  }
+}
+
+trait FlowVarOrHeap extends FlowVar
+
+case class Assumes()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVar {
+  override val extensionSubnodes: Seq[Node] = Seq.empty
+  override def typ: Type = InternalType
+  override def prettyPrint: PrettyPrintPrimitives#Cont = PAssumesKeyword.keyword
+}
+
+case class Heap()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVarOrHeap {
+  override val extensionSubnodes: Seq[Node] = Seq.empty
+  override def typ: Type = InternalType
+  override def prettyPrint: PrettyPrintPrimitives#Cont = PHeapKeyword.keyword
+}
+
+case class Var(decl: LocalVar)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVarOrHeap {
+  override val extensionSubnodes: Seq[Node] = Seq(decl)
+  override def typ: Type = decl.typ
+  override def prettyPrint: PrettyPrintPrimitives#Cont = show(decl)
+}
+
+case class NoAssumeAnnotation()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionExp with Node {
+  override def extensionIsPure: Boolean = true
+
+  override def extensionSubnodes: Seq[Node] = Seq()
+
+  override def typ: Type = Bool
+
+  override def verifyExtExp(): VerificationResult = {
+    assert(assertion = false, "FlowAnalysis: verifyExtExp has not been implemented.")
+    Failure(Seq(ConsistencyError("FlowAnalysis: verifyExtExp has not been implemented.", pos)))
+  }
+
+  /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter.
+   * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */
+  override def prettyPrint: PrettyPrintPrimitives#Cont = {
+    text("assumes nothing")
+  }
+}
+
+case class FlowAnnotation(v: FlowVar, varList: Seq[FlowVarOrHeap])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionExp with Node with Scope {
+  override def extensionIsPure: Boolean = true
+
+  override val scopedDecls: Seq[Declaration] = Seq()
+
+  override def typ: Type = Bool
+
+  override def verifyExtExp(): VerificationResult = {
+    assert(assertion = false, "FlowAnalysis: verifyExtExp has not been implemented.")
+    Failure(Seq(ConsistencyError("FlowAnalysis: verifyExtExp has not been implemented.", pos)))
+  }
+
+  override def extensionSubnodes: Seq[Node] = Seq(v) ++ varList
+
+  /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter.
+    * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */
+  override def prettyPrint: PrettyPrintPrimitives#Cont = {
+    text("influenced") <+> (v match {
+      case value: Var => show(value.decl)
+      case _: Assumes => text("assumes")
+      case _: Heap => text("heap")
+    })  <+>
+      text("by") <+>
+      ssep(varList.map {
+        case value: Var => show(value.decl)
+        case _ => text("heap")
+      }, group(char(',') <> line(" ")))
+  }
+}
+
+case class Lemma()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionExp with Node with Scope {
+  override def extensionIsPure: Boolean = true
+
+  override val scopedDecls: Seq[Declaration] = Seq()
+
+  override def typ: Type = Bool
+
+  override def verifyExtExp(): VerificationResult = {
+    assert(assertion = false, "Lemma: verifyExtExp has not been implemented.")
+    Failure(Seq(ConsistencyError("Lemma: verifyExtExp has not been implemented.", pos)))
+  }
+
+  override def extensionSubnodes: Seq[Node] = Seq()
+
+  /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter.
+    * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */
+  override def prettyPrint: PrettyPrintPrimitives#Cont = {
+    text("isLemma")
+  }
+}
+
+case class OldCall(methodName: String, args: Seq[Exp], rets: Seq[LocalVar], oldLabel: String)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt with Scope {
+  override val scopedDecls: Seq[Declaration] = Seq()
+
+  override lazy val check: Seq[ConsistencyError] = {
+    (if (Consistency.noResult(this)) Seq.empty else Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos))) ++
+    (if (Consistency.noDuplicates(rets)) Seq.empty else Seq(ConsistencyError("Targets are not allowed to have duplicates", rets.head.pos))) ++
+    args.flatMap(Consistency.checkPure)
+  }
+
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = {
+    val call = text("oldCall") <> brackets(text(oldLabel)) <> text(methodName) <> nest(defaultIndent, parens(ssep(args map show, group(char(',') <> line))))
+    rets match {
+      case Nil => call
+      case _ => ssep(rets map show, char(',') <> space) <+> ":=" <+> call
+    }
+  }
+
+  override val extensionSubnodes: Seq[Node] = args ++ rets
+}

src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningErrors.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-2024 ETH Zurich.
+
+package viper.silver.plugin.standard.reasoning
+
+import viper.silver.verifier._
+import viper.silver.verifier.reasons.ErrorNode
+
+case class ExistentialElimFailed(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
+  override val id = "existential.elimination.failed"
+  override val text = "Existentially quantified formula might not hold."
+
+  override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): ExistentialElimFailed =
+    ExistentialElimFailed(this.offendingNode, this.reason, this.cached)
+
+  override def withReason(r: ErrorReason): ExistentialElimFailed = ExistentialElimFailed(offendingNode, r, cached)
+}
+
+case class UniversalIntroFailed(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
+  override val id = "universal.introduction.failed"
+  override val text = "Specified property might not hold."
+
+  override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): UniversalIntroFailed =
+    UniversalIntroFailed(this.offendingNode, this.reason, this.cached)
+
+  override def withReason(r: ErrorReason): UniversalIntroFailed = UniversalIntroFailed(offendingNode, r, cached)
+}
+
+case class PreconditionInLemmaCallFalse(offendingNode: OldCall, reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
+  val id = "lemma.call.precondition"
+  val text = s"The precondition of lemma ${offendingNode.methodName} might not hold."
+
+  def withNode(offendingNode: errors.ErrorNode = this.offendingNode): PreconditionInLemmaCallFalse = PreconditionInLemmaCallFalse(offendingNode.asInstanceOf[OldCall], this.reason, this.cached)
+
+  def withReason(r: ErrorReason): PreconditionInLemmaCallFalse = PreconditionInLemmaCallFalse(offendingNode, r, cached)
+}