From e957272d696ef46fdd29c531660f933e93912a34 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 4 Oct 2023 23:44:10 +0200 Subject: [PATCH 1/4] Unfold, unfolding and fold no longer allowed with none-permission --- src/main/scala/rules/Evaluator.scala | 4 ++-- src/main/scala/rules/Executor.scala | 4 ++-- .../scala/rules/PermissionSupporter.scala | 19 +++++++++++++++++-- 3 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 610cc514e..a8be60cf4 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -791,7 +791,7 @@ object evaluator extends EvaluationRules { if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) { evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, ePerm, pve, v1)((s2, tPerm, v2) => - v2.decider.assert(IsNonNegative(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative + v2.decider.assert(IsPositive(tPerm)) { case true => joiner.join[Term, Term](s2, v2)((s3, v3, QB) => { val s4 = s3.incCycleCounter(predicate) @@ -832,7 +832,7 @@ object evaluator extends EvaluationRules { eval(s10, eIn, pve, v5)(QB)})}) })(join(v2.symbolConverter.toSort(eIn.typ), "joined_unfolding", s2.relevantQuantifiedVariables, v2))(Q) case false => - createFailure(pve dueTo NegativePermission(ePerm), v2, s2)})) + createFailure(pve dueTo NonPositivePermission(ePerm), v2, s2)})) } else { val unknownValue = v.decider.appliedFresh("recunf", v.symbolConverter.toSort(eIn.typ), s.relevantQuantifiedVariables) Q(s, unknownValue, v) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 24d2c602d..33abac61b 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -507,7 +507,7 @@ object executor extends ExecutionRules { val pve = FoldFailed(fold) evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, ePerm, pve, v1)((s2, tPerm, v2) => - permissionSupporter.assertNotNegative(s2, tPerm, ePerm, pve, v2)((s3, v3) => { + permissionSupporter.assertPositive(s2, tPerm, ePerm, pve, v2)((s3, v3) => { val wildcards = s3.constrainableARPs -- s1.constrainableARPs predicateSupporter.fold(s3, predicate, tArgs, tPerm, wildcards, pve, v3)(Q)}))) @@ -529,7 +529,7 @@ object executor extends ExecutionRules { s2.smCache } - permissionSupporter.assertNotNegative(s2, tPerm, ePerm, pve, v2)((s3, v3) => { + permissionSupporter.assertPositive(s2, tPerm, ePerm, pve, v2)((s3, v3) => { val wildcards = s3.constrainableARPs -- s1.constrainableARPs predicateSupporter.unfold(s3.copy(smCache = smCache1), predicate, tArgs, tPerm, wildcards, pve, v3, pa)(Q) }) diff --git a/src/main/scala/rules/PermissionSupporter.scala b/src/main/scala/rules/PermissionSupporter.scala index 63cd54194..1dd0daae1 100644 --- a/src/main/scala/rules/PermissionSupporter.scala +++ b/src/main/scala/rules/PermissionSupporter.scala @@ -10,9 +10,9 @@ import viper.silver.ast import viper.silver.verifier.PartialVerificationError import viper.silicon.interfaces.VerificationResult import viper.silicon.state.State -import viper.silicon.state.terms.{Term, perms, Var} +import viper.silicon.state.terms.{Term, Var, perms} import viper.silicon.verifier.Verifier -import viper.silver.verifier.reasons.NegativePermission +import viper.silver.verifier.reasons.{NegativePermission, NonPositivePermission} object permissionSupporter extends SymbolicExecutionRules { def assertNotNegative(s: State, tPerm: Term, ePerm: ast.Exp, pve: PartialVerificationError, v: Verifier) @@ -29,4 +29,19 @@ object permissionSupporter extends SymbolicExecutionRules { } } } + + def assertPositive(s: State, tPerm: Term, ePerm: ast.Exp, pve: PartialVerificationError, v: Verifier) + (Q: (State, Verifier) => VerificationResult) + : VerificationResult = { + + tPerm match { + case k: Var if s.constrainableARPs.contains(k) => + Q(s, v) + case _ => + v.decider.assert(perms.IsPositive(tPerm)) { + case true => Q(s, v) + case false => createFailure(pve dueTo NonPositivePermission(ePerm), v, s) + } + } + } } From 987be744b9ed09307e9f6f6b532c9ba6610bffd7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 4 Oct 2023 23:56:58 +0200 Subject: [PATCH 2/4] Updated silver version --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 65ec3412b..e678cd731 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4 +Subproject commit e678cd731b4bc7dd7e9f79ae7627d08891158f2c From d3f5d84379051dbe81c9204445015a239ffb7b0b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 4 Oct 2023 23:58:10 +0200 Subject: [PATCH 3/4] Updated silver version --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index e678cd731..67fa15588 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit e678cd731b4bc7dd7e9f79ae7627d08891158f2c +Subproject commit 67fa155884a51d17d25a496bda73d76b31a5c889 From fab9efe45076832265d59d3fa8ee6b801ed441d7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 5 Oct 2023 00:40:27 +0200 Subject: [PATCH 4/4] Updated silver version --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 67fa15588..820db76e9 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 67fa155884a51d17d25a496bda73d76b31a5c889 +Subproject commit 820db76e92646c57b180c7ccdc8dee0465118e62