Merge pull request #392 from viperproject/silver-issue-522

Silver issue 522

build.sbt

@@ -22,6 +22,8 @@ lazy val carbon = (project in file("."))
         Test / fork := true,
         Test / testOptions += Tests.Argument(TestFrameworks.ScalaTest, "-u", "target/test-reports", "-oD"),
 
+		Compile / fork := true,
+
         // Assembly settings
         assembly / assemblyJarName := "carbon.jar",             // JAR filename
         assembly / mainClass := Some("viper.carbon.Carbon"),    // Define JAR's entry point

src/main/scala/viper/carbon/CarbonVerifier.scala

@@ -87,6 +87,13 @@ case class CarbonVerifier(override val reporter: Reporter,
     case None => z3Default
   } else z3Default
 
+  def checkInjectivity = if (config != null) config.checkInjectivity.toOption match {
+    case Some(b) => b
+    case None => false
+  }
+  else false
+
+
   def name: String = "carbon"
   def version: String = "1.0"
   def buildVersion = version

src/main/scala/viper/carbon/modules/InhaleModule.scala

@@ -9,6 +9,7 @@ package viper.carbon.modules
 import components.{ComponentRegistry, InhaleComponent}
 import viper.silver.{ast => sil}
 import viper.carbon.boogie.Stmt
+import viper.silver.verifier.PartialVerificationError
 
 /**
  * A module for translating inhale statements.  The module takes care of the basic
@@ -28,5 +29,5 @@ trait InhaleModule extends Module with InhaleComponent with ComponentRegistry[In
     * The 'statesStackForPackageStmt' and 'insidePackageStmt' are used when translating statements during packaging a wand.
     * For more details refer to the general note in 'wandModule'.
     */
-  def inhale(exp: Seq[sil.Exp], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
+  def inhale(exp: Seq[(sil.Exp, PartialVerificationError)], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
 }

src/main/scala/viper/carbon/modules/components/InhaleComponent.scala

@@ -7,6 +7,7 @@
 package viper.carbon.modules.components
 
 import viper.carbon.boogie.Stmt
+import viper.silver.verifier.PartialVerificationError
 import viper.silver.{ast => sil}
 
 /**
@@ -18,5 +19,5 @@ trait InhaleComponent extends Component {
   /**
    * Inhale a single expression.
    */
-  def inhaleExp(exp: sil.Exp): Stmt
+  def inhaleExp(exp: sil.Exp, error: PartialVerificationError): Stmt
 }

src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala

@@ -533,7 +533,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
       //      case [email protected](vars, triggers, expr) => // NOTE: there's no need for a special case for QPs, since these are desugared, introducing conjunctions
         case _ =>
           checkDefinedness(e, error, duringPackageStmt = duringPackageStmt) ++
-            inhale(e, statesStack, duringPackageStmt)
+            inhale(Seq((e, error)), statesStack, duringPackageStmt)
       }
     }
 

src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala

@@ -828,7 +828,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     foldInfo = acc
     val stmt = exhale(Seq((Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error)), havocHeap = false,
       statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) ++
-      inhale(acc, statesStackForPackageStmt, insidePackageStmt)
+      inhale(Seq((acc, error)), statesStackForPackageStmt, insidePackageStmt)
     val stmtLast =  Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++ {
       val location = acc.loc
       val predicate = verifier.program.findPredicate(location.predicateName)
@@ -873,7 +873,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
       } ++
       (if(exhaleUnfoldedPredicate)
           exhale(Seq((acc, error)), havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)
-      else Nil) ++ inhale(Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)
+      else Nil) ++ inhale(Seq((Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error)), statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)
     unfoldInfo = oldUnfoldInfo
     duringUnfold = oldDuringUnfold
     duringFold = oldDuringFold
@@ -937,7 +937,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
   var exhaleTmpStateId = -1
   var extraUnfolding = false
-  override def inhaleExp(e: sil.Exp): Stmt = {
+  override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = {
     e match {
       case sil.Unfolding(acc, _) => if (duringUnfoldingExtraUnfold) Nil else // execute the unfolding, since this may gain information
       {

src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala

@@ -14,6 +14,7 @@ import viper.carbon.boogie._
 import viper.carbon.boogie.Implicits._
 import viper.carbon.verifier.Verifier
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
+import viper.silver.verifier.PartialVerificationError
 
 /**
  * The default implementation of a [[viper.carbon.modules.HeapModule]].
@@ -740,7 +741,7 @@ class DefaultHeapModule(val verifier: Verifier)
     else Nil
   }
 
-  override def inhaleExp(e: sil.Exp): Stmt = {
+  override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = {
     e match {
       case sil.Unfolding(sil.PredicateAccessPredicate(loc, perm), exp) =>
         addPermissionToPMask(loc)

src/main/scala/viper/carbon/modules/impls/DefaultInhaleModule.scala

@@ -11,6 +11,7 @@ import viper.silver.{ast => sil}
 import viper.carbon.boogie._
 import viper.carbon.verifier.Verifier
 import viper.carbon.boogie.Implicits._
+import viper.silver.verifier.PartialVerificationError
 
 /**
  * The default implementation of a [[viper.carbon.modules.InhaleModule]].
@@ -29,17 +30,17 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat
     register(this)
   }
 
-  override def inhale(exps: Seq[sil.Exp], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
+  override def inhale(exps: Seq[(sil.Exp, PartialVerificationError)], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
     val current_state = stateModule.state
     if(insidePackageStmt){ // replace currentState with the correct state in which the inhale occurs during packaging the wand
       stateModule.replaceState(statesStackForPackageStmt(0).asInstanceOf[StateRep].state)
     }
 
 
     val stmt =
-        (exps map (e => inhaleConnective(e.whenInhaling))) ++
+        (exps map (e => inhaleConnective(e._1.whenInhaling, e._2))) ++
           MaybeCommentBlock("Free assumptions",
-            exps map (e => allFreeAssumptions(e))) ++
+            exps map (e => allFreeAssumptions(e._1))) ++
           assumeGoodState
 
     if(insidePackageStmt) { // all the assumption made during packaging a wand (except assumptions about the global state before the package statement)
@@ -62,29 +63,29 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat
    * Inhales Viper expression connectives (such as logical and/or) and forwards the
    * translation of other expressions to the inhale components.
    */
-  private def inhaleConnective(e: sil.Exp): Stmt = {
+  private def inhaleConnective(e: sil.Exp, error: PartialVerificationError): Stmt = {
     e match {
       case sil.And(e1, e2) =>
-        inhaleConnective(e1) ::
-          inhaleConnective(e2) ::
+        inhaleConnective(e1, error) ::
+          inhaleConnective(e2, error) ::
           Nil
       case sil.Implies(e1, e2) =>
-        If(translateExp(e1), inhaleConnective(e2), Statements.EmptyStmt)
+        If(translateExp(e1), inhaleConnective(e2, error), Statements.EmptyStmt)
       case sil.CondExp(c, e1, e2) =>
-        If(translateExp(c), inhaleConnective(e1), inhaleConnective(e2))
+        If(translateExp(c), inhaleConnective(e1, error), inhaleConnective(e2, error))
       case sil.Let(declared,boundTo,body) if !body.isPure =>
       {
         val u = env.makeUniquelyNamed(declared) // choose a fresh binder
         env.define(u.localVar)
         Assign(translateLocalVar(u.localVar),translateExp(boundTo)) ::
-          inhaleConnective(body.replace(declared.localVar, u.localVar)) ::
+          inhaleConnective(body.replace(declared.localVar, u.localVar), error) ::
           {
             env.undefine(u.localVar)
             Nil
           }
       }
       case _ =>
-        val stmt = components map (_.inhaleExp(e))
+        val stmt = components map (_.inhaleExp(e, error))
         if (stmt.children.isEmpty)
           sys.error(s"missing translation for inhaling of $e")
         val retStmt = (if (containsFunc(e)) Seq(assumeGoodState) else Seq()) ++ stmt ++ (if (e.isPure) Seq() else Seq(assumeGoodState))
@@ -95,7 +96,7 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat
     }
   }
 
-  override def inhaleExp(e: sil.Exp): Stmt = {
+  override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = {
     if (e.isPure) {
       Assume(translateExp(e))
     } else {

src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala

@@ -437,7 +437,7 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp
         MaybeCommentBlock("Check the loop body", NondetIf({
           val (freshStateStmt, prevState) = stateModule.freshTempState("loop")
           val stmts = MaybeComment("Reset state", freshStateStmt ++ stateModule.initBoogieState) ++
-            MaybeComment("Inhale invariant", inhale(invs) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++
+            MaybeComment("Inhale invariant", inhale(invs map (x => (x, errors.WhileFailed(x)))) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++
             Comment("Check and assume guard") ++
             checkDefinedness(w.cond, errors.WhileFailed(w.cond)) ++
             Assume(guard) ++ stateModule.assumeGoodState ++
@@ -450,7 +450,7 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp
         )) ++
         MaybeCommentBlock("Inhale loop invariant after loop, and assume guard",
           Assume(guard.not) ++ stateModule.assumeGoodState ++
-            inhale(invs) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))
+            inhale(invs map (x => (x, errors.WhileFailed(x)))) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))
         )
   }
 
@@ -536,7 +536,7 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp
             As long as modules the state at this point refers to the original state, this is fine.
          */
           MaybeComment("Reset state", stateModule.initBoogieState) ++
-          MaybeComment("Inhale invariant", inhale(invs) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++
+          MaybeComment("Inhale invariant", inhale(invs map (x => (x, errors.WhileFailed(x)))) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++
           stateModule.assumeGoodState
       )
     )

src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala

@@ -189,7 +189,8 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt
           MaybeCommentBlock("Exhaling precondition", executeUnfoldings(pres, (pre => errors.PreconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))) ++
             exhale(pres map (e => (e, errors.PreconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))), statesStackForPackageStmt = statesStack, insidePackageStmt = insidePackageStmt)) ++ {
           stateModule.replaceOldState(preCallState)
-          val res = MaybeCommentBlock("Inhaling postcondition", inhale(posts, statesStack, insidePackageStmt) ++
+          val res = MaybeCommentBlock("Inhaling postcondition",
+            inhale(posts map (e => (e, errors.CallFailed(mc).withReasonNodeTransformed(renamingArguments))), statesStack, insidePackageStmt) ++
             executeUnfoldings(posts, (post => errors.Internal(post).withReasonNodeTransformed(renamingArguments))))
           stateModule.replaceOldState(oldState)
           toUndefine map mainModule.env.undefine

src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala

@@ -216,7 +216,7 @@ DefaultWandModule(val verifier: Verifier) extends WandModule with StmtComponent
             val oldOps = OPS
 
             currentWand = w
-            val addWand = inhaleModule.inhale(w, statesStack, inWand)
+            val addWand = inhaleModule.inhale(Seq((w, error)), statesStack, inWand)
 
             val currentState = stateModule.state
 
@@ -692,7 +692,7 @@ case class PackageSetup(hypState: StateRep, usedState: StateRep, initStmt: Stmt)
       (if(inWand) exchangeAssumesWithBoolean(stateModule.assumeGoodState, OPS.boolVar) else stateModule.assumeGoodState) ++
       CommentBlock("check if LHS holds and remove permissions ", exhaleModule.exhale((w.left, error), false, insidePackageStmt = inWand, statesStackForPackageStmt = statesStack)) ++
       (if(inWand) exchangeAssumesWithBoolean(stateModule.assumeGoodState, OPS.boolVar) else stateModule.assumeGoodState) ++
-      CommentBlock("inhale the RHS of the wand",inhaleModule.inhale(w.right, statesStackForPackageStmt = statesStack, insidePackageStmt = inWand)) ++
+      CommentBlock("inhale the RHS of the wand",inhaleModule.inhale(Seq((w.right, error)), statesStackForPackageStmt = statesStack, insidePackageStmt = inWand)) ++
       heapModule.beginExhale ++ heapModule.endExhale ++
       (if(inWand) exchangeAssumesWithBoolean(stateModule.assumeGoodState, OPS.boolVar) else stateModule.assumeGoodState)
     //GP: using beginExhale, endExhale works now, but isn't intuitive, maybe should duplicate code to avoid this breaking