Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unfold, fold, and unfolding must have a strictly positive permission amount #754

Merged
merged 6 commits into from
Oct 9, 2023
Merged

Unfold, fold, and unfolding must have a strictly positive permission amount #754

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e957272
Unfold, unfolding and fold no longer allowed with none-permission
marcoeilers Oct 4, 2023
904f7ae
Merge branch 'master' into meilers_unfold_none
marcoeilers Oct 4, 2023
987be74
Updated silver version
marcoeilers Oct 4, 2023
d3f5d84
Updated silver version
marcoeilers Oct 4, 2023
fab9efe
Updated silver version
marcoeilers Oct 4, 2023
ace7052
Merge branch 'master' into meilers_unfold_none
marcoeilers Oct 9, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Submodule silver updated 5 files
+8 −0 src/main/scala/viper/silver/verifier/VerificationError.scala
+5 −5 src/test/resources/all/issues/carbon/0125.vpr
+5 −5 src/test/resources/all/issues/silver/0072.vpr
+52 −0 src/test/resources/all/issues/silver/0444.vpr
+1 −1 src/test/resources/all/issues/silver/0522.vpr
4 changes: 2 additions & 2 deletions src/main/scala/rules/Evaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/rules/Executor.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)})))

Expand All @@ -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)
})
Expand Down
19 changes: 17 additions & 2 deletions src/main/scala/rules/PermissionSupporter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
}
}
}
}
Loading