Fix assuming perm bounds in predicates, support flag to get old behavior

viperproject · Oct 15, 2024 · 6048e9e · 6048e9e
1 parent c999815
commit 6048e9e
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 4 deletions.
diff --git a/silver b/silver
diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala
@@ -94,6 +94,12 @@ case class CarbonVerifier(override val reporter: Reporter,
   }
   else false
 
+  def respectFunctionPrecPermAmounts: Boolean = if (config != null) config.respectFunctionPrecPermAmounts.toOption match {
+    case Some(b) => b
+    case None => false
+  }
+  else false
+
   override def usePolyMapsInEncoding =
     if (config != null) {
       config.desugarPolymorphicMaps.toOption match {

diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
@@ -191,7 +191,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     env = Environment(verifier, f)
     ErrorMemberMapping.currentMember = f
 
-    val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(true)
+    val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(!verifier.respectFunctionPrecPermAmounts)
     val res = MaybeCommentedDecl(s"Translation of function ${f.name}",
       MaybeCommentedDecl("Uninterpreted function definitions", functionDefinitions(f), size = 1) ++
         (if (f.isAbstract) Nil else
@@ -668,7 +668,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
     val args = p.formalArgs map translateLocalVarDecl
     val init : Stmt = MaybeCommentBlock("Initializing the state",
-      stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
+      stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
     )
 
     val predicateBody = p.body.get

diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
@@ -198,10 +198,11 @@ class QuantifiedPermModule(val verifier: Verifier)
         Trigger(Seq(staticGoodState)),
         staticGoodState ==> staticGoodMask)) ++ {
       val perm = currentPermission(obj.l, field.l)
+      val shouldAssumePermUpperBound = if (verifier.respectFunctionPrecPermAmounts) TrueLit() else assumePermUpperBound
       Axiom(Forall(staticStateContributions(true, true) ++ obj ++ field,
         Trigger(Seq(staticGoodMask, perm)),
         // permissions are non-negative
-        ((staticGoodMask && assumePermUpperBound) ==> ( perm >= noPerm &&
+        ((staticGoodMask && shouldAssumePermUpperBound) ==> ( perm >= noPerm &&
           // permissions for fields which aren't predicates are smaller than 1
           // permissions for fields which aren't predicates or wands are smaller than 1
           ((staticGoodMask && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm )))

diff --git a/src/main/scala/viper/carbon/verifier/Verifier.scala b/src/main/scala/viper/carbon/verifier/Verifier.scala
@@ -80,4 +80,6 @@ trait Verifier {
 
   def usePolyMapsInEncoding: Boolean
 
+  def respectFunctionPrecPermAmounts: Boolean
+
 }
+7 −0		src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+96 −3		src/test/resources/all/functions/function_precondition_perms.vpr
Original file line number	Diff line number	Diff line change
Expand Up		@@ -80,4 +80,6 @@ trait Verifier {

		def usePolyMapsInEncoding: Boolean

		def respectFunctionPrecPermAmounts: Boolean

		}