From 6048e9e2636c395ffdbd875509028536cfd936a0 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 15 Oct 2024 15:30:08 +0200
Subject: [PATCH] Fix assuming perm bounds in predicates, support flag to get
 old behavior

---
 silver                                                      | 2 +-
 src/main/scala/viper/carbon/CarbonVerifier.scala            | 6 ++++++
 .../viper/carbon/modules/impls/DefaultFuncPredModule.scala  | 4 ++--
 .../viper/carbon/modules/impls/QuantifiedPermModule.scala   | 3 ++-
 src/main/scala/viper/carbon/verifier/Verifier.scala         | 2 ++
 5 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/silver b/silver
index 89dce6fd..626437b0 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 89dce6fde51d0a9bebf6db83c8968a5778be5a1f
+Subproject commit 626437b04aaa354061246f8d07831ad8effdeb93
diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala
index fc33d06a..8632851e 100644
--- 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
index f4a60265..4b3dd2c8 100644
--- 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
index 78ae7892..9af96186 100644
--- 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
index ac28846b..9af97523 100644
--- 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
+
 }