Skip to content

Various updates in preparation for Z3 version update #585

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

Draft
marcoeilers wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Various updates in preparation for Z3 version update #585

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
af20496
Fixing some issues to prepare for Z3 4.16
marcoeilers May 19, 2026
30ee823
Trying to fix some sequence axiom issues
marcoeilers May 19, 2026
1d537fd
Merge branch 'master' into meilers_z3_416
marcoeilers May 20, 2026
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
29 changes: 16 additions & 13 deletions src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -447,35 +447,38 @@ 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)
val f2 = FuncApp(pmField, vars, pmT)
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))) ++
Func(predicateTriggerIdentifier(p), Seq(LocalVarDecl(heapName, heapTyp), LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
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
}
}
}
Expand Down
46 changes: 30 additions & 16 deletions src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -1048,6 +1058,10 @@ class QuantifiedPermModule(val verifier: Verifier)
}
}

def Locally(s: Stmt): Stmt = {
NondetIf(s ++ Assume(FalseLit()))
}

/*
translate inhaling a forall expressions
*/
Expand Down Expand Up @@ -1205,15 +1219,15 @@ 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 ++
(if (!verifier.assumeInjectivityOnInhale) injectiveAssertion
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)) ++
Expand Down Expand Up @@ -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) ++
Expand All @@ -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)) ++
Expand Down
9 changes: 2 additions & 7 deletions src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<T> 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));

@alexanderjsummers alexanderjsummers Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's move this to before the inequalities (two conjuncts earlier); I think (heuristically) it can be useful to put the first-to-be-ruled-out cases first.

Also, although I don't think it's relevant for what this axiom does directly, adding s0 != Seq#Append(s0,s1) && before it should be fine and I think it might be easier to get this consistent if we follow this pattern everywhere: rule out the cases where the operator doesn't actually create new sequences, and only add the index terms under these conditions. I didn't think about it that way when making the previous changes, but I think this fits well how to make this more methodical.

|
|function Seq#Update<T>(Seq T, int, T): Seq T;
|axiom (forall<T> 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)
Expand Down Expand Up @@ -207,7 +207,7 @@ object SequenceAxiomatization {
|
|axiom (forall<T> 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<T> s: Seq T, t: Seq T, m:int ::
Expand Down Expand Up @@ -335,11 +335,6 @@ object SequenceAxiomatization {
|*/
|// diff 9: skolemise equals (new)
|// AS: split axiom
|axiom (forall<T> 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<T>(Seq T, Seq T) : int; // skolem function for Seq#Equals
|
Expand Down
6 changes: 0 additions & 6 deletions src/main/scala/viper/carbon/verifier/BoogieInterface.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,16 +51,10 @@ trait BoogieInterface {
"/errorTrace:0",
"/errorLimit:10000000",
"/proverOpt:O:smt.AUTO_CONFIG=false",
"/proverOpt:O:smt.PHASE_SELECTION=0",

@alexanderjsummers alexanderjsummers Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the rationale for removing these three? It might be a good thing to do, but presumably has some chance of non-trivial performance impact (maybe in either direction?)

"/proverOpt:O:smt.RESTART_STRATEGY=0",
"/proverOpt:O:smt.RESTART_FACTOR=|1.5|",
"/proverOpt:O:smt.ARITH.RANDOM_INITIAL_VALUE=true",

@alexanderjsummers alexanderjsummers Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looking at the docs, I'm surprised we had this one - seems good to get rid of anyway

"/proverOpt:O:smt.CASE_SPLIT=3",
"/proverOpt:O:smt.DELAY_UNITS=true",
"/proverOpt:O:NNF.SK_HACK=true",

@alexanderjsummers alexanderjsummers Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume this option has gone? Not sure what it did, to be honest

"/proverOpt:O:smt.MBQI=false",
"/proverOpt:O:smt.QI.EAGER_THRESHOLD=100",
"/proverOpt:O:smt.BV.REFLECT=true",

@alexanderjsummers alexanderjsummers Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this option no longer exist? It seems like one that could have quite significant effects on performance but only for problems using bitvectors + quantifiers

"/proverOpt:O:smt.qi.max_multi_patterns=1000",
s"/proverOpt:PROVER_PATH=$z3Path")

Expand Down
2 changes: 1 addition & 1 deletion src/test/scala/viper/carbon/AllTests.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,5 +40,5 @@ class AllTests extends SilSuite {
lazy val verifiers = List(verifier)

val commandLineArguments: Seq[String] =
Seq()
Seq("--timeout=120")
}
Loading