Sound trigger-independent function encoding

src/main/scala/rules/Consumer.scala

@@ -474,7 +474,14 @@ object consumer extends ConsumptionRules {
 
     executionFlowController.tryOrFail0(s1, v)((s2, v1, QS) => {
       eval(s2, e, pve, v1)((s3, t, v2) => {
-        v2.decider.assert(t) {
+        val termToAssert = t match {
+          case Quantification(q, vars, body, trgs, name, isGlob) =>
+            val transformed = FunctionPreconditionTransformer.transform(body, s3.program)
+            v2.decider.assume(Quantification(q, vars, transformed, trgs, name+"_precondition", isGlob))
+            Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob)
+          case _ => t
+        }
+        v2.decider.assert(termToAssert) {
           case true =>
             v2.decider.assume(t)
             QS(s3, v2)

src/main/scala/rules/Evaluator.scala

@@ -728,6 +728,10 @@ object evaluator extends EvaluationRules {
                              smDomainNeeded = true)
             consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.convert(sorts.Snap)
+              if (func.pres.nonEmpty) {
+                val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
+                v3.decider.assume(preFApp)
+              }
               val tFApp = App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
               val fr5 =
                 s4.functionRecorder.changeDepthBy(-1)

src/main/scala/rules/FunctionSupporter.scala

@@ -19,4 +19,9 @@ object functionSupporter {
     val id = function.id.withSuffix("%", "stateless")
     Fun(id, function.argSorts.tail, terms.sorts.Bool)
   }
+
+  def preconditionVersion(function: HeapDepFun): HeapDepFun = {
+    val id = function.id.withSuffix("%", "precondition")
+    HeapDepFun(id, function.argSorts, terms.sorts.Bool)
+  }
 }

src/main/scala/rules/Joiner.scala

@@ -11,6 +11,7 @@ import viper.silicon.interfaces.{Success, VerificationResult}
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.logger.records.structural.JoiningRecord
 import viper.silicon.state.State
+import viper.silicon.state.terms.{And, Or, Term}
 import viper.silicon.verifier.Verifier
 
 case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathConditions)
@@ -64,11 +65,16 @@ object joiner extends JoiningRules {
       } else {
         val (sJoined, dataJoined) = merge(entries)
 
+        var feasibleBranches: List[Term] = Nil
+
         entries foreach (entry => {
           val pcs = entry.pathConditions.conditionalized
           v.decider.prover.comment("Joined path conditions")
           v.decider.assume(pcs)
+          feasibleBranches = And(entry.pathConditions.branchConditions) :: feasibleBranches
         })
+        // Assume we are in a feasible branch
+        v.decider.assume(Or(feasibleBranches))
 
         Q(sJoined, dataJoined, v)
       }

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -142,7 +142,8 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
                        perms: Term,
                        arguments: Seq[Term],
                        triggers: Seq[Trigger],
-                       qidPrefix: String)
+                       qidPrefix: String,
+                       program: ast.Program)
                       : Quantification
 
   def createSingletonQuantifiedChunk(codomainQVars: Seq[Var],
@@ -847,8 +848,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         vars = effectiveTriggersQVars,
         triggers = effectiveTriggers)))
 
+    val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
+    val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
     // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
-    v.decider.assert(Forall(qvars, Implies(tCond, perms.IsNonNegative(tPerm)), Nil)) {
+    v.decider.assert(nonNegTerm) {
       case true =>
 
         /* TODO: Can we omit/simplify the injectivity check in certain situations? */
@@ -861,18 +864,21 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               perms     = tPerm,
               arguments = tArgs,
               triggers  = Nil,
-              qidPrefix = qid)
+              qidPrefix = qid,
+              program   = s.program)
           } else {
             True()
           }
         v.decider.prover.comment("Check receiver injectivity")
+        v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program))
         v.decider.assert(receiverInjectivityCheck) {
           case true =>
             val ax = inverseFunctions.axiomInversesOfInvertibles
             val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers))
 
             v.decider.prover.comment("Definitional axioms for inverse functions")
             val definitionalAxiomMark = v.decider.setPathConditionMark()
+            v.decider.assume(inv.definitionalAxioms.map(a => FunctionPreconditionTransformer.transform(a, s.program)))
             v.decider.assume(inv.definitionalAxioms)
             val conservedPcs =
               if (s.recordPcs) (s.conservedPcs.head :+ v.decider.pcs.after(definitionalAxiomMark)) +: s.conservedPcs.tail
@@ -1046,8 +1052,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         /* Explicit triggers were provided. */
         v.decider.assume(auxNonGlobals)
     }
+
+    val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
+    val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
     // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
-    v.decider.assert(Forall(qvars, Implies(tCond, perms.IsNonNegative(tPerm)), Nil)) {
+    v.decider.assert(nonNegTerm) {
       case true =>
         val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs)
         val chunkOrderHeuristics =
@@ -1077,7 +1086,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             perms     = tPerm,
             arguments = tArgs,
             triggers  = Nil,
-            qidPrefix = qid)
+            qidPrefix = qid,
+            program = s.program)
         v.decider.prover.comment("Check receiver injectivity")
         v.decider.assert(receiverInjectivityCheck) {
           case true =>
@@ -1086,6 +1096,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             val lossOfInvOfLoc = loss.replace(qvarsToInvOfLoc)
 
             v.decider.prover.comment("Definitional axioms for inverse functions")
+            v.decider.assume(inverseFunctions.definitionalAxioms.map(a => FunctionPreconditionTransformer.transform(a, s.program)))
             v.decider.assume(inverseFunctions.definitionalAxioms)
 
             if (s.heapDependentTriggers.contains(resourceIdentifier)){
@@ -1510,7 +1521,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                        perms: Term,
                        arguments: Seq[Term],
                        triggers: Seq[Trigger],
-                       qidPrefix: String)
+                       qidPrefix: String,
+                       program: ast.Program)
                       : Quantification = {
 
     val qvars1 = qvars.map(x => x.copy(id = x.id.rename(id => s"${id}1")))
@@ -1546,9 +1558,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           argsEqual),
         varsEqual)
 
+    val functionPres = FunctionPreconditionTransformer.transform(implies, program)
+
     Forall(
       qvars1 ++ qvars2,
-      implies,
+      Implies(functionPres, implies),
       triggers,
       s"$qidPrefix-rcvrInj")
   }

src/main/scala/state/FunctionPreconditionTransformer.scala

@@ -0,0 +1,52 @@
+package viper.silicon.state
+
+import viper.silicon.rules.functionSupporter
+import viper.silicon.state.terms.{And, App, HeapDepFun, Implies, Ite, Let, Literal, Not, Or, Quantification, Term, True}
+import viper.silver.ast
+
+
+/**
+  * Given a term t, returns a new term tr(t) that expresses that all applications of heap-dependent functions are
+  * well-defined (in particular, that the abstract functions that represent their preconditions hold).
+  * In general, after checking that t is well-defined, it is sound to assume tr(t).
+  *
+  * I.e., given
+  *   fun(e1, ..., en)
+  * where fun is a heap-dependent function with a precondition, it returns
+  *   tr(e1) && ... && tr(en) && fun%precondition(e1, ..., en)
+  * where the tr(ei) terms express that all function applications in the argument terms are well-defined.
+  *
+  * For &&, ||, and ==>, the transformation takes into account short-circuit semantics:
+  * If A && B is well-defined, that means that A is well-defined, and if A is true, then B is well-defined as well.
+  * Thus, the transformation of A && B is tr(A) && (A ==> tr(B)).
+  */
+object FunctionPreconditionTransformer {
+  def transform(t: Term, p: ast.Program): Term = {
+    val res = t match {
+      case _:Literal => True()
+      case And(ts) => And(transform(ts.head, p), Implies(ts.head, transform(And(ts.tail), p)))
+      case Or(ts) => And(transform(ts.head, p), Implies(Not(ts.head), transform(Or(ts.tail), p)))
+      case Implies(t0, t1) => And(transform(t0, p), Implies(t0, transform(t1, p)))
+      case Ite(t, t1, t2) => And(transform(t, p), Ite(t, transform(t1, p), transform(t2, p)))
+      case Let(bindings, body) => Let(bindings, transform(body, p))
+      case Quantification(q, vars, body, triggers, name, isGlobal) =>
+        val tBody = transform(body, p)
+        if (tBody == True())
+          tBody
+        else
+          Quantification(q, vars, tBody, triggers, name, isGlobal)
+      case App(hdf@HeapDepFun(id, _, _), args)  =>
+        val funcName = id match {
+          case SuffixedIdentifier(prefix, _, _) => prefix.name
+          case _ => id.name
+        }
+        if (p.findFunction(funcName).pres.nonEmpty)
+          And(args.map(transform(_, p)) :+ App(functionSupporter.preconditionVersion(hdf), args))
+        else
+          And(args.map(transform(_, p)))
+      case other => And(other.subterms.map(transform(_, p)))
+    }
+    res
+  }
+
+}

src/main/scala/supporters/functions/FunctionData.scala

@@ -8,6 +8,7 @@ package viper.silicon.supporters.functions
 
 import scala.annotation.unused
 import com.typesafe.scalalogging.LazyLogging
+import viper.silicon.state.FunctionPreconditionTransformer
 import viper.silver.ast
 import viper.silver.ast.utility.Functions
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
@@ -51,6 +52,7 @@ class FunctionData(val programFunction: ast.Function,
   val function: HeapDepFun = symbolConverter.toFunction(programFunction)
   val limitedFunction = functionSupporter.limitedVersion(function)
   val statelessFunction = functionSupporter.statelessVersion(function)
+  val preconditionFunction = functionSupporter.preconditionVersion(function)
 
   val formalArgs: Map[ast.AbstractLocalVar, Var] = toMap(
     for (arg <- programFunction.formalArgs;
@@ -67,6 +69,7 @@ class FunctionData(val programFunction: ast.Function,
   val functionApplication = App(function, `?s` +: formalArgs.values.toSeq)
   val limitedFunctionApplication = App(limitedFunction, `?s` +: formalArgs.values.toSeq)
   val triggerFunctionApplication = App(statelessFunction, formalArgs.values.toSeq)
+  val preconditionFunctionApplication = App(preconditionFunction, `?s` +: formalArgs.values.toSeq)
 
   val limitedAxiom =
     Forall(arguments,
@@ -175,15 +178,21 @@ class FunctionData(val programFunction: ast.Function,
     expressionTranslator.translatePrecondition(program, programFunction.pres, this)
   }
 
+  lazy val translatedPosts = {
+    assert(phase == 1, s"Postcondition axiom must be generated in phase 1, current phase is $phase")
+    if (programFunction.posts.nonEmpty) {
+      expressionTranslator.translatePostcondition(program, programFunction.posts, this)
+    }else{
+      Seq()
+    }
+  }
+
   lazy val postAxiom: Option[Term] = {
     assert(phase == 1, s"Postcondition axiom must be generated in phase 1, current phase is $phase")
 
     if (programFunction.posts.nonEmpty) {
-      val posts =
-        expressionTranslator.translatePostcondition(program, programFunction.posts, this)
-
-      val pre = And(translatedPres)
-      val innermostBody = And(generateNestedDefinitionalAxioms ++ List(Implies(pre, And(posts))))
+      val pre = if (programFunction.pres.nonEmpty) preconditionFunctionApplication else True()
+      val innermostBody = And(generateNestedDefinitionalAxioms ++ List(Implies(pre, And(translatedPosts))))
       val bodyBindings: Map[Var, Term] = Map(formalResult -> limitedFunctionApplication)
       val body = Let(toMap(bodyBindings), innermostBody)
 
@@ -237,13 +246,17 @@ class FunctionData(val programFunction: ast.Function,
     }))
   }
 
-  lazy val definitionalAxiom: Option[Term] = {
+  lazy val optBody: Option[Term] = {
     assert(phase == 2, s"Definitional axiom must be generated in phase 2, current phase is $phase")
 
-    val optBody = expressionTranslator.translate(program, programFunction, this)
+    expressionTranslator.translate(program, programFunction, this)
+  }
+
+  lazy val definitionalAxiom: Option[Term] = {
+    assert(phase == 2, s"Definitional axiom must be generated in phase 2, current phase is $phase")
 
     optBody.map(translatedBody => {
-      val pre = And(translatedPres)
+      val pre = if (programFunction.pres.nonEmpty) preconditionFunctionApplication else True()
       val nestedDefinitionalAxioms = generateNestedDefinitionalAxioms
       val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(functionApplication === translatedBody))))
       val allTriggers = (
@@ -252,4 +265,18 @@ class FunctionData(val programFunction: ast.Function,
 
       Forall(arguments, body, allTriggers)})
   }
+
+  lazy val preconditionPropagationAxiom: Seq[Term] = {
+    val pre = if (programFunction.pres.nonEmpty) preconditionFunctionApplication else True()
+    val bodyPreconditions = if (programFunction.body.isDefined) optBody.map(translatedBody => {
+      val body = Implies(pre, FunctionPreconditionTransformer.transform(translatedBody, program))
+      Forall(arguments, body, Seq(Trigger(functionApplication)))
+    }) else None
+    val postPreconditions = if (programFunction.posts.nonEmpty) {
+      val bodyBindings: Map[Var, Term] = Map(formalResult -> limitedFunctionApplication)
+      val bodies = translatedPosts.map(tPost => Let(bodyBindings, Implies(pre, FunctionPreconditionTransformer.transform(tPost, program))))
+      bodies.map(b => Forall(arguments, b, Seq(Trigger(limitedFunctionApplication))))
+    } else Seq()
+    bodyPreconditions.toSeq ++ postPreconditions
+  }
 }

src/main/scala/supporters/functions/FunctionVerificationUnit.scala

@@ -111,7 +111,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
     private def generateFunctionSymbolsAfterAnalysis: Iterable[Either[String, Decl]] = (
          Seq(Left("Declaring symbols related to program functions (from program analysis)"))
       ++ functionData.values.flatMap(data =>
-            Seq(data.function, data.limitedFunction, data.statelessFunction).map(FunctionDecl)
+            Seq(data.function, data.limitedFunction, data.statelessFunction, data.preconditionFunction).map(FunctionDecl)
          ).map(Right(_))
     )
 
@@ -175,9 +175,10 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
           emitAndRecordFunctionAxioms(data.postAxiom.toSeq: _*)
           this.postConditionAxioms = this.postConditionAxioms ++ data.postAxiom.toSeq
 
-          if (function.body.isEmpty)
+          if (function.body.isEmpty) {
+            emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*)
             result1
-          else {
+          } else {
             /* Phase 2: Verify the function's postcondition */
             val result2 = verify(function, phase1data)
 
@@ -186,6 +187,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
                 data.verificationFailures = data.verificationFailures :+ fatalResult
               case _ =>
                 emitAndRecordFunctionAxioms(data.definitionalAxiom.toSeq: _*)
+                emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*)
             }
 
             result1 && result2