From e9d9cb9c96a8878dc3978b24dcc4b9eedd896c53 Mon Sep 17 00:00:00 2001 From: Yushuo Xiao Date: Thu, 31 Jul 2025 10:36:19 +0800 Subject: [PATCH 1/2] set known-folded permission mask to empty if an unfold statement unfolds all permissions of a predicate --- .../scala/viper/carbon/modules/impls/DefaultHeapModule.scala | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala index 943b7573..c4239be5 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala @@ -640,6 +640,9 @@ class DefaultHeapModule(val verifier: Verifier) If(UnExp(Not,hasDirectPerm(loc)), resetPredicateInfo, Nil) ++ addPermissionToPMask(loc) ++ stateModule.assumeGoodState} ) + case sil.Unfold(sil.PredicateAccessPredicate(loc@sil.PredicateAccess(_, _), _)) => + val knownfolded_update: Stmt = curHeapAssignUpdatePredWandMask(predicateMask(loc).maskField, zeroPMask) + stmt ++ If(UnExp(Not,hasDirectPerm(loc)), knownfolded_update, Nil) case sil.FieldAssign(lhs, rhs) => if(usingOldState) sys.error("heap module: field is assigned while using old state") stmt ++ (currentHeapAssignUpdate(lhs, translateExp(rhs))) // after all checks From b73b9d8fefaf6f49f1632eef24cc81725636ea5d Mon Sep 17 00:00:00 2001 From: Yushuo Xiao Date: Mon, 15 Dec 2025 16:53:49 +0100 Subject: [PATCH 2/2] change to an alternative (simplified) encoding (known-folded mask update in unfold) --- .../scala/viper/carbon/modules/impls/DefaultHeapModule.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala index c4239be5..dd1999e0 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala @@ -642,7 +642,7 @@ class DefaultHeapModule(val verifier: Verifier) addPermissionToPMask(loc) ++ stateModule.assumeGoodState} ) case sil.Unfold(sil.PredicateAccessPredicate(loc@sil.PredicateAccess(_, _), _)) => val knownfolded_update: Stmt = curHeapAssignUpdatePredWandMask(predicateMask(loc).maskField, zeroPMask) - stmt ++ If(UnExp(Not,hasDirectPerm(loc)), knownfolded_update, Nil) + stmt ++ knownfolded_update case sil.FieldAssign(lhs, rhs) => if(usingOldState) sys.error("heap module: field is assigned while using old state") stmt ++ (currentHeapAssignUpdate(lhs, translateExp(rhs))) // after all checks