From af20496514b75df4bb374758a7c5ebdb8a0e5e12 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Tue, 19 May 2026 21:08:48 +0200 Subject: [PATCH 1/2] Fixing some issues to prepare for Z3 4.16 --- .../modules/impls/DefaultHeapModule.scala | 29 ++++++------ .../modules/impls/QuantifiedPermModule.scala | 46 ++++++++++++------- .../carbon/verifier/BoogieInterface.scala | 6 --- src/test/scala/viper/carbon/AllTests.scala | 2 +- 4 files changed, 47 insertions(+), 36 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala index 943b7573..5405e0a8 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala @@ -447,6 +447,8 @@ class DefaultHeapModule(val verifier: Verifier) val pmT = predicateMaskFieldTypeOf(p) val varDecls = p.formalArgs map mainModule.translateLocalVarDecl val vars = varDecls map (_.l) + val predArgGetters = varDecls.map (v => Func(Identifier(f"predicate_${p.name}_arg_${v.name.name}"), Seq(LocalVarDecl(Identifier("pred"), t)), v.typ)) + val predArgGetters2 = varDecls.map (v => Func(Identifier(f"predicate_${p.name}_arg_${v.name.name}_sm"), Seq(LocalVarDecl(Identifier("pred"), pmT)), v.typ)) val predId:BigInt = getPredicateOrWandId(p.name) val f0 = FuncApp(predicate, vars, t) val f1 = predicateMaskField(f0) @@ -454,6 +456,8 @@ class DefaultHeapModule(val verifier: Verifier) TypeDecl(predicateMetaTypeOf(p)) ++ Func(predicate, varDecls, t) ++ Func(pmField, varDecls, pmT) ++ + predArgGetters ++ + predArgGetters2 ++ Axiom(MaybeForall(varDecls, Trigger(f1), f1 === f2)) ++ Axiom(MaybeForall(varDecls, Trigger(f0), isPredicateField(f0))) ++ Axiom(MaybeForall(varDecls, Trigger(f0), getPredicateOrWandId(f0) === IntLit(predId))) ++ @@ -461,21 +465,20 @@ class DefaultHeapModule(val verifier: Verifier) Func(predicateTriggerAnyStateIdentifier(p), Seq(LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++ { // axiom that two predicate identifiers can only be the same, if all arguments - // are the same (e.g., we immediatly know that valid(1) != valid(2)) + // are the same (e.g., we immediately know that valid(1) != valid(2)) if (vars.size == 0) Nil else { - val varDecls2 = varDecls map ( - v => LocalVarDecl(Identifier(v.name.name + "2")(v.name.namespace), v.typ)) - val vars2 = varDecls2 map (_.l) - var varsEqual = All((vars zip vars2) map { - case (v1, v2) => v1 === v2 - }) - val f0_2 = FuncApp(predicate, vars2, t) - val f2_2 = FuncApp(pmField, vars2, t) - Axiom(Forall(varDecls ++ varDecls2, Trigger(Seq(f0, f0_2)), - (f0 === f0_2) ==> varsEqual)) ++ - Axiom(Forall(varDecls ++ varDecls2, Trigger(Seq(f2, f2_2)), - (f2 === f2_2) ==> varsEqual)) + val argGetApply = predArgGetters map (f => FuncApp(f.name, Seq(f0), f.typ)) + val argGetEqual = argGetApply.zip(vars).map { + case (get, v) => get === v + } + val argGetAxiom = Axiom(Forall(varDecls, Trigger(f0), All(argGetEqual))) + val argGetApply2 = predArgGetters2 map (f => FuncApp(f.name, Seq(f2), f.typ)) + val argGetEqual2 = argGetApply2.zip(vars).map { + case (get, v) => get === v + } + val argGetAxiom2 = Axiom(Forall(varDecls, Trigger(f2), All(argGetEqual2))) + argGetAxiom ++ argGetAxiom2 } } } diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 01a20c13..5011f600 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -596,8 +596,8 @@ class QuantifiedPermModule(val verifier: Verifier) //if the permission is a wildcard, we check that we have some permission > 0 for all locations and assume that the permission substracted is smaller than the permission held. val wildcardAssms:Stmt = if(isWildcard) { - (Assert(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (currentPermission(translatedRecv, translatedLocation) > noPerm)), error.dueTo(reasons.InsufficientPermission(fieldAccess))))++ - (Assume(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (wildcard < currentPermission(translatedRecv, translatedLocation))))) + Locally(Assert(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (currentPermission(translatedRecv, translatedLocation) > noPerm)), error.dueTo(reasons.InsufficientPermission(fieldAccess))))++ + (Assume(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(Trigger(currentPermission(translatedRecv, translatedLocation))), translatedCond ==> (wildcard < currentPermission(translatedRecv, translatedLocation))))) } else { Nil } @@ -649,13 +649,18 @@ class QuantifiedPermModule(val verifier: Verifier) CommentBlock("assume permission updates for independent locations", independentLocations) ++ (mask := qpMask) + val inverseAssumptions: Stmt = if (assertReadPermOnly) Nil else + CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) + + val checks = CommentBlock("check that the permission amount is positive", Locally(permPositive)) ++ + CommentBlock("check if receiver " + recv.toString + " is injective", Locally(injectiveAssertion)) ++ + CommentBlock("check if sufficient permission is held", Locally(enoughPerm)) + val res1 = Havoc(qpMask) ++ MaybeComment("wild card assumptions", stmts ++ wildcardAssms) ++ - CommentBlock("check that the permission amount is positive", permPositive) ++ - CommentBlock("check if receiver " + recv.toString + " is injective",injectiveAssertion) ++ - CommentBlock("check if sufficient permission is held", enoughPerm) ++ - CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) ++ + checks ++ + inverseAssumptions ++ maskUpdateStmt vsFresh.foreach(v => env.undefine(v.localVar)) @@ -769,8 +774,8 @@ class QuantifiedPermModule(val verifier: Verifier) //if we exhale a wildcard permission, assert that we hold some permission to all affected locations and restrict the wildcard value val wildcardAssms:Stmt = if(isWildcard) { - Assert(Forall(translatedLocals, Seq(), translatedCond ==> (currentPermission(translateNull, translatedResource) > noPerm)), error.dueTo(reason)) ++ - Assume(Forall(translatedLocals, Seq(), translatedCond ==> (wildcard < currentPermission(translateNull, translatedResource)))) + Locally(Assert(Forall(translatedLocals, Seq(), translatedCond ==> (currentPermission(translateNull, translatedResource) > noPerm)), error.dueTo(reason))) ++ + Assume(Forall(translatedLocals, Seq(Trigger(currentPermission(translateNull, translatedResource))), translatedCond ==> (wildcard < currentPermission(translateNull, translatedResource)))) } else { Nil } @@ -846,13 +851,18 @@ class QuantifiedPermModule(val verifier: Verifier) CommentBlock("assume permission updates for independent locations ", independentLocations) ++ (mask := qpMask) + val inverseAssumptions: Stmt = if (assertReadPermOnly) Nil else + CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) + + val checks = CommentBlock("check that the permission amount is positive", Locally(permPositive)) ++ + CommentBlock("check if receiver " + accPred.toString + " is injective", Locally(injectiveAssertion)) ++ + CommentBlock("check if sufficient permission is held", Locally(enoughPerm)) + val res1 = Havoc(qpMask) ++ MaybeComment("wildcard assumptions", stmts ++ wildcardAssms) ++ - CommentBlock("check that the permission amount is positive", permPositive) ++ - CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion) ++ - CommentBlock("check if sufficient permission is held", enoughPerm) ++ - CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) ++ + checks ++ + inverseAssumptions ++ maskUpdateStmts vsFresh.foreach(vFresh => env.undefine(vFresh.localVar)) @@ -1048,6 +1058,10 @@ class QuantifiedPermModule(val verifier: Verifier) } } + def Locally(s: Stmt): Stmt = { + NondetIf(s ++ Assume(FalseLit())) + } + /* translate inhaling a forall expressions */ @@ -1205,7 +1219,7 @@ class QuantifiedPermModule(val verifier: Verifier) val reas = reasons.QPAssertionNotInjective(fieldAccess) var err = error.dueTo(reas) - val injectiveAssertion = Assert(is_injective, err) + val injectiveAssertion = Locally(Assert(is_injective, err)) val res1 = Havoc(qpMask) ++ stmts ++ @@ -1213,7 +1227,7 @@ class QuantifiedPermModule(val verifier: Verifier) else Nil) ++ CommentBlock("Define Inverse Function", Assume(invAssm1) ++ Assume(invAssm2)) ++ - (if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", permPositive) else Nil) ++ + (if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", Locally(permPositive)) else Nil) ++ CommentBlock("Assume set of fields is nonNull", nonNullAssumptions) ++ // CommentBlock("Assume injectivity", injectiveAssumption) ++ CommentBlock("Define permissions", Assume(Forall(obj, triggerForPermissionUpdateAxiom, condTrueLocations && condFalseLocations)) ++ @@ -1383,7 +1397,7 @@ class QuantifiedPermModule(val verifier: Verifier) } val injectTrigger = Seq(Trigger(Seq(triggerFunApp, triggerFunApp2))) val err = error.dueTo(reasons.QPAssertionNotInjective(accPred.loc)) - val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err) + val injectiveAssertion = Locally(Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err)) val res1 = Havoc(qpMask) ++ @@ -1392,7 +1406,7 @@ class QuantifiedPermModule(val verifier: Verifier) else Nil) ++ CommentBlock("Define Inverse Function", Assume(invAssm1) ++ Assume(invAssm2)) ++ - (if (!isWildcard) (MaybeComment("Check that permission expression is non-negative for all fields", permPositive)) else Nil) ++ + (if (!isWildcard) (MaybeComment("Check that permission expression is non-negative for all fields", Locally(permPositive))) else Nil) ++ CommentBlock("Define updated permissions", permissionsMap) ++ CommentBlock("Define independent locations", (independentLocations ++ independentResource)) ++ diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 2f24baf8..068b1fc7 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -51,16 +51,10 @@ trait BoogieInterface { "/errorTrace:0", "/errorLimit:10000000", "/proverOpt:O:smt.AUTO_CONFIG=false", - "/proverOpt:O:smt.PHASE_SELECTION=0", - "/proverOpt:O:smt.RESTART_STRATEGY=0", - "/proverOpt:O:smt.RESTART_FACTOR=|1.5|", - "/proverOpt:O:smt.ARITH.RANDOM_INITIAL_VALUE=true", "/proverOpt:O:smt.CASE_SPLIT=3", "/proverOpt:O:smt.DELAY_UNITS=true", - "/proverOpt:O:NNF.SK_HACK=true", "/proverOpt:O:smt.MBQI=false", "/proverOpt:O:smt.QI.EAGER_THRESHOLD=100", - "/proverOpt:O:smt.BV.REFLECT=true", "/proverOpt:O:smt.qi.max_multi_patterns=1000", s"/proverOpt:PROVER_PATH=$z3Path") diff --git a/src/test/scala/viper/carbon/AllTests.scala b/src/test/scala/viper/carbon/AllTests.scala index 751558bc..fbf216b8 100644 --- a/src/test/scala/viper/carbon/AllTests.scala +++ b/src/test/scala/viper/carbon/AllTests.scala @@ -40,5 +40,5 @@ class AllTests extends SilSuite { lazy val verifiers = List(verifier) val commandLineArguments: Seq[String] = - Seq() + Seq("--timeout=120") } From 30ee82385972fc5c3d7fe7942a3da868ad35f7ca Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Tue, 19 May 2026 22:20:02 +0200 Subject: [PATCH 2/2] Trying to fix some sequence axiom issues --- .../impls/sequence_axioms/SequenceAxiomatization.scala | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala b/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala index 8ecabfb4..b5d8d605 100644 --- a/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala +++ b/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala @@ -83,7 +83,7 @@ object SequenceAxiomatization { | s0 != Seq#Empty() && s1 != Seq#Empty() && Seq#Length(s0) <= n && n < Seq#Length(Seq#Append(s0,s1)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s0)),Seq#Length(s0)) == n && Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, Seq#Sub(n,Seq#Length(s0)))); |// AS: added "reverse triggering" versions of the axioms |axiom (forall s0: Seq T, s1: Seq T, m: int :: { Seq#Index(s1, m), Seq#Append(s0,s1)} // m == n-|s0|, n == m + |s0| - | s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m)); + | s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) && s1 != Seq#Append(s0,s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m)); | |function Seq#Update(Seq T, int, T): Seq T; |axiom (forall s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } {Seq#Length(s),Seq#Update(s,i,v)} // (diff 4: added trigger) @@ -207,7 +207,7 @@ object SequenceAxiomatization { | |axiom (forall s: Seq T, t: Seq T, n:int :: | { Seq#Drop(Seq#Append(s,t),n) } - | n > 0 && n > Seq#Length(s) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s)))); + | n > 0 && n > Seq#Length(s) && n < Seq#Length(Seq#Append(s,t)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s)))); | |// diff 16: temporarily dropped general case of these |//axiom (forall s: Seq T, t: Seq T, m:int :: @@ -335,11 +335,6 @@ object SequenceAxiomatization { |*/ |// diff 9: skolemise equals (new) |// AS: split axiom - |axiom (forall s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) } - | Seq#Equal(s0,s1) ==> - | Seq#Length(s0) == Seq#Length(s1) && - | (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) } - | 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j))); | |function Seq#SkolemDiff(Seq T, Seq T) : int; // skolem function for Seq#Equals |