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,151 @@
+// 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))
+  }
+
+  /**
+    * get all variables that are assigned to inside the block and take intersection with universal introduction
+    * variables. If they are contained throw error since these 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))
+      }
+  }
+
+  private def specifiesLemma(m: Method): Boolean = (m.pres ++ m.posts).exists {
+    case _: Lemma => true
+    case _ => false
+  }
+
+  /** check if isLemma precondition is correct */
+  def checkLemma(input: Program, reportError: AbstractError => Unit): Unit = {
+    input.methods.foreach(method => {
+      val containsLemma = specifiesLemma(method)
+      val (containsDecreases, containsDecreasesStar) = AnalysisUtils.containsDecreasesAnnotations(method)
+
+      if (containsLemma) {
+        /** report error if there is no decreases clause or specification */
+        if(!containsDecreases) {
+          reportError(ConsistencyError(s"method ${method.name} marked lemma might not contain decreases clause", method.pos))
+        }
+
+        /** report error if the decreases statement might not prove termination */
+        if (containsDecreasesStar) {
+          reportError(ConsistencyError("decreases statement might not prove termination", method.pos))
+        }
+
+        /** check method body for impure statements */
+        checkBodyPure(method.body.getOrElse(Seqn(Seq(), Seq())()), method, input, reportError)
+      }
+    })
+  }
+
+  /** checks whether the body is pure, reports error if impure operation found */
+  def checkBodyPure(stmt: Stmt, method: Method, prog: Program, reportError: AbstractError => Unit): Boolean = {
+    var pure: Boolean = true
+    stmt match {
+      case Seqn(ss, _) =>
+        ss.foreach(s => {
+          pure = pure && checkBodyPure(s, method, prog, reportError)
+        })
+        pure
+
+        /** 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 containsLemma = specifiesLemma(mc)
+
+        /** if called method is not a lemma report error */
+        if (!containsLemma) {
+          reportError(ConsistencyError(s"method ${method.name} marked lemma might contain call to method ${m}", m.pos))
+          false
+        } else {
+          pure
+        }
+      case _ =>
+        pure
+    }
+  }
+
+  /** checks that influences by annotations 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.AssumeNode(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 variables can be influenced. ${targetVarDecl.name} is not be a return variable.", v.pos))
+          }
+          if (seenVars.contains(targetVarDecl)) {
+            reportError(ConsistencyError(s"Only one influenced by expression per return variable 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 arguments can influence a return variable. ${argVarDecl.name} is not be a method argument.", 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 quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++
+    (if (varList.isEmpty) Seq(ConsistencyError("Quantifier 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 space <> 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], exp1: Exp, exp2: 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 (!(exp1 isSubtype Bool)) Seq(ConsistencyError(s"Body of universal quantifier must be of Bool type, but found ${exp1.typ}", exp1.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(exp1) <+>
+      text("implies") <+> toParenDoc(exp2) <+>
+      showBlock(block)
+  }
+
+  override val extensionSubnodes: Seq[Node] = varList ++ triggers ++ Seq(exp1, exp2, 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)))
+  }
+}
+
+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 FlowVar {
+  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 FlowVar {
+  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[FlowVar])(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 _ => 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] = {
+    var s = Seq.empty[ConsistencyError]
+    if (!Consistency.noResult(this))
+      s :+= ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)
+    if (!Consistency.noDuplicates(rets))
+      s :+= ConsistencyError("Targets are not allowed to have duplicates", rets.head.pos)
+    s ++= args.flatMap(Consistency.checkPure)
+    s
+  }
+
+  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,40 @@
+// 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 = " no witness could be found."
+
+  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 = " not true for all vars."
+
+  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 FlowAnalysisFailed(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
+  override val id = "flow analysis.failed"
+  override val text = " ."
+
+  override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): FlowAnalysisFailed =
+    FlowAnalysisFailed(this.offendingNode, this.reason, this.cached)
+
+  override def withReason(r: ErrorReason): FlowAnalysisFailed = FlowAnalysisFailed(offendingNode, r, cached)
+}