From 57b73a0744c8c402c4c4544537cc149baae9df1b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 30 Dec 2024 16:18:21 +0100 Subject: [PATCH] Fixing injectivity checks for QPs with multiple quantified variables (#542) --- silver | 2 +- .../modules/impls/QuantifiedPermModule.scala | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/silver b/silver index 7cc30420..65febaeb 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 7cc304207bb95804754e0ac2f0a8bd2f82b43fdd +Subproject commit 65febaeb1be635c4f825d1789e5d0e1809f6ef18 diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index de2a38f3..01a20c13 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -624,7 +624,7 @@ class QuantifiedPermModule(val verifier: Verifier) //injectivity assertion val v2s = translatedLocals.map(translatedLocal => LocalVarDecl(Identifier(translatedLocal.name.name), translatedLocal.typ)) var triggerFunApp2 : FuncApp = triggerFunApp - var notEquals : Exp = TrueLit() + var notEquals : Exp = FalseLit() var translatedPerms2 = translatedPerms var translatedCond2 = translatedCond var translatedRecv2 = translatedRecv @@ -633,7 +633,7 @@ class QuantifiedPermModule(val verifier: Verifier) translatedPerms2 = translatedPerms2.replace(translatedLocals(i).l, v2s(i).l) translatedCond2 = translatedCond2.replace(translatedLocals(i).l, v2s(i).l) translatedRecv2 = translatedRecv2.replace(translatedLocals(i).l, v2s(i).l) - notEquals = notEquals && (translatedLocals(i).l !== v2s(i).l) + notEquals = notEquals || (translatedLocals(i).l !== v2s(i).l) } val is_injective = Forall( translatedLocals++v2s,validateTriggers(translatedLocals++v2s, Seq(Trigger(Seq(triggerFunApp, triggerFunApp2)))),( notEquals && translatedCond && translatedCond2 && permGt(translatedPerms, noPerm) && permGt(translatedPerms2, noPerm)) ==> (translatedRecv !== translatedRecv2)) val reas = reasons.QPAssertionNotInjective(fieldAccess) @@ -811,13 +811,13 @@ class QuantifiedPermModule(val verifier: Verifier) //assert injectivity of inverse function: val translatedLocals2 = translatedLocals.map(translatedLocal => LocalVarDecl(Identifier(translatedLocal.name.name), translatedLocal.typ)) //new varible - var unequalities : Exp = TrueLit() + var unequalities : Exp = FalseLit() var translatedCond2 = translatedCond var translatedPerms2 = translatedPerms var translatedArgs2 = translatedArgs var triggerFunApp2 = triggerFunApp for (i <- 0 until translatedLocals.length) { - unequalities = unequalities && (translatedLocals(i).l.!==(translatedLocals2(i).l)) + unequalities = unequalities || (translatedLocals(i).l.!==(translatedLocals2(i).l)) translatedCond2 = translatedCond2.replace(translatedLocals(i).l, translatedLocals2(i).l) translatedPerms2 = translatedPerms2.replace(translatedLocals(i).l, translatedLocals2(i).l) translatedArgs2 = translatedArgs2.map(a => a.replace(translatedLocals(i).l, translatedLocals2(i).l)) @@ -1190,7 +1190,7 @@ class QuantifiedPermModule(val verifier: Verifier) //injectivity assertion val v2s = translatedLocals.map(translatedLocal => LocalVarDecl(Identifier(translatedLocal.name.name), translatedLocal.typ)) var triggerFunApp2 = FuncApp(triggerFun.name, translatedLocals.map(v => LocalVar(v.name, v.typ)), triggerFun.typ) - var notEquals: Exp = TrueLit() + var notEquals: Exp = FalseLit() var translatedPerms2 = translatedPerms var translatedCond2 = translatedCond var translatedRecv2 = translatedRecv @@ -1199,7 +1199,7 @@ class QuantifiedPermModule(val verifier: Verifier) translatedPerms2 = translatedPerms2.replace(translatedLocals(i).l, v2s(i).l) translatedCond2 = translatedCond2.replace(translatedLocals(i).l, v2s(i).l) translatedRecv2 = translatedRecv2.replace(translatedLocals(i).l, v2s(i).l) - notEquals = notEquals && (translatedLocals(i).l !== v2s(i).l) + notEquals = notEquals || (translatedLocals(i).l !== v2s(i).l) } val is_injective = Forall(translatedLocals ++ v2s, validateTriggers(translatedLocals ++ v2s, Seq(Trigger(Seq(triggerFunApp2)))), (notEquals && translatedCond && translatedCond2 && permGt(translatedPerms, noPerm) && permGt(translatedPerms2, noPerm)) ==> (translatedRecv !== translatedRecv2)) @@ -1361,13 +1361,13 @@ class QuantifiedPermModule(val verifier: Verifier) val triggerFunApp = FuncApp(triggerFun.name, translatedLocals.map(translatedLocal => LocalVar(translatedLocal.name, translatedLocal.typ)), triggerFun.typ) - var unequalities : Exp = TrueLit() + var unequalities : Exp = FalseLit() var translatedCond2 = translatedCond var translatedPerms2 = translatedPerms var translatedArgs2 = translatedArgs var triggerFunApp2 = triggerFunApp for (i <- 0 until translatedLocals.length) { - unequalities = unequalities && (translatedLocals(i).l.!==(translatedLocals2(i).l)) + unequalities = unequalities || (translatedLocals(i).l.!==(translatedLocals2(i).l)) translatedCond2 = translatedCond2.replace(translatedLocals(i).l, translatedLocals2(i).l) translatedPerms2 = translatedPerms2.replace(translatedLocals(i).l, translatedLocals2(i).l) translatedArgs2 = translatedArgs2.map(a => a.replace(translatedLocals(i).l, translatedLocals2(i).l))