injectivity test moved to checkDefinednessImpl

viperproject · Jul 10, 2016 · 5c159a1 · 5c159a1
1 parent a436316
commit 5c159a1
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 23 deletions.
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala
@@ -8,14 +8,19 @@ package viper.carbon.modules.impls
 
 import viper.carbon.modules.{StatelessComponent, ExpModule}
 import viper.silver.{ast => sil}
-import viper.carbon.boogie._
 import viper.carbon.verifier.Verifier
 import viper.silver.verifier.{reasons, PartialVerificationError}
 import viper.carbon.boogie.Implicits._
 import viper.carbon.modules.components.DefinednessComponent
 import viper.silver.ast.{LocationAccess, QuantifiedExp}
 import viper.silver.ast.utility.Expressions
 
+import viper.carbon.boogie._
+import viper.carbon.boogie.LocalVarDecl
+import viper.carbon.boogie.Forall
+import viper.carbon.boogie.Assert
+import viper.carbon.boogie.Identifier
+
 /**
  * The default implementation of [[viper.carbon.modules.ExpModule]].
  */
@@ -31,7 +36,6 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
   import inhaleModule._
   import funcPredModule._
   import exhaleModule._
-  import stateModule.StateSnapshot
 
   override def start() {
     register(this)
@@ -300,23 +304,39 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
           stmt ++ stmt2 ++ stmt3 ++
             MaybeCommentBlock("Free assumptions", allFreeAssumptions(e))
         }
-        
+
         if (e.isInstanceOf[sil.QuantifiedExp]) {
           val bound_vars  = e.asInstanceOf[sil.QuantifiedExp].variables
-	  bound_vars map (v => env.define(v.localVar))
-	  val res = if(e.isInstanceOf[sil.ForPerm]) {
-      val eAsForallRef = e.asInstanceOf[sil.ForPerm]
-      val bound_var = eAsForallRef.variable
-      val perLocFilter : sil.Location => LocationAccess = loc => loc match {
-          case f: sil.Field => sil.FieldAccess(bound_var.localVar, f)(loc.pos, loc.info)
-          case p: sil.Predicate => sil.PredicateAccess(Seq(bound_var.localVar), p)(loc.pos, loc.info)
-        }
-      val filter : Exp = eAsForallRef.accessList.foldLeft[Exp](BoolLit(false))((soFar,loc) => BinExp(soFar,Or,hasDirectPerm(perLocFilter(loc))))
+	        bound_vars map (v => env.define(v.localVar))
+          //check injectivity
+          val injectivity_check:Stmt = e match  {
+            case qp@sil.utility.QuantifiedPermissions.QPForall(v_orig, cond_orig, recv_orig, field, exp, forall, fieldAccess) =>
+                val namespace = verifier.freshNamespace("perm")
+                val v = translateLocalVarDecl(v_orig)
+                val cond = translateExp(cond_orig)
+                val recv = translateExp(recv_orig)
+                val v1 = LocalVarDecl(Identifier("v")(namespace), v.typ)
+                val v2 = LocalVarDecl(Identifier("v2")(namespace),v.typ)
+                MaybeCommentBlock("Check if receiver " + recv_orig.toString() + " is injective", Assert(Forall( v1++v2, Seq(), ((v1.l !== v2.l) &&  cond.replace(v.l, v1.l) && cond.replace(v.l, v2.l) ) ==> (recv.replace(v.l, v1.l) !== recv.replace(v.l, v2.l)) ),
+                          error.dueTo(reasons.ReceiverNotInjective(fieldAccess))))
+
+            case _ => Nil
+          }
+
+
+          val res:Stmt = if(e.isInstanceOf[sil.ForPerm]) {
+            val eAsForallRef = e.asInstanceOf[sil.ForPerm]
+            val bound_var = eAsForallRef.variable
+            val perLocFilter : sil.Location => LocationAccess = loc => loc match {
+                case f: sil.Field => sil.FieldAccess(bound_var.localVar, f)(loc.pos, loc.info)
+                case p: sil.Predicate => sil.PredicateAccess(Seq(bound_var.localVar), p)(loc.pos, loc.info)
+              }
+            val filter : Exp = eAsForallRef.accessList.foldLeft[Exp](BoolLit(false))((soFar,loc) => BinExp(soFar,Or,hasDirectPerm(perLocFilter(loc))))
 
-      handleQuantifiedLocals(bound_vars, If(filter, translate, Nil))
-    }else handleQuantifiedLocals(bound_vars,translate)
-	  bound_vars map (v => env.undefine(v.localVar))
-          res        
+            handleQuantifiedLocals(bound_vars, If(filter, translate, Nil))
+          } else handleQuantifiedLocals(bound_vars,translate)
+              bound_vars map (v => env.undefine(v.localVar))
+              injectivity_check ++  res
         } else e match {
           case sil.Old(_) =>
             val prevState = stateModule.state
@@ -331,7 +351,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
             stateModule.replaceState(prevState)
             res
           case _ =>
-          translate
+            translate
         }
     }
   }

diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
@@ -394,14 +394,12 @@ class QuantifiedPermModule(val verifier: Verifier)
 
 
         val ts = Seq(Trigger(curPerm),Trigger(currentPermission(qpMask,obj.l,translatedLocation)),Trigger(invFunApp))
-        val injectiveAssertion = Assert(isInjective(qpComp), error.dueTo(reasons.ReceiverNotInjective(fieldAccess)))
 
         val res = Havoc(qpMask) ++
           stmts ++
           wildcardAssms ++
           // notNull ++ // subsumed by permission check
           permPositive ++
-          CommentBlock("check if receiver " + recv.toString() + " is injective",injectiveAssertion) ++
           enoughPerm ++
           CommentBlock("assumptions for inverse of receiver " + recv.toString(), Assume(invAssm1)++Assume(invAssm2)) ++
           Assume(Forall(obj,ts, condTrueLocations&&condFalseLocations )) ++
@@ -518,16 +516,12 @@ class QuantifiedPermModule(val verifier: Verifier)
         val ts = Seq(Trigger(curPerm),Trigger(currentPermission(qpMask,obj.l,translatedLocation)),Trigger(invFunApp)) //triggers TODO
 
 
-        val injectiveAssumption = assmsToStmt(isInjective(qpComp))
-
-
         val res = Havoc(qpMask) ++
           stmts ++
           assmsToStmt(invAssm1) ++
           assmsToStmt(invAssm2) ++
           nonNullAssumptions ++
           permPositive ++
-          injectiveAssumption ++
           assmsToStmt(Forall(obj,ts, condTrueLocations&&condFalseLocations )) ++
           independentLocations ++
           (mask := qpMask)