From cf5609ff05e8168ff7a7362b8b3002961c72f704 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 8 Mar 2024 11:57:35 -0800 Subject: [PATCH] Added quantifier instantiation option (#857) Added option ```/keepQuantifier``` which allows the original quantifier to be kept along with the instances. By default, the original quantifier is dropped if any instances are found. More hints had to be added to a few Civl benchmarks. Co-authored-by: Shaz Qadeer --- Source/Core/CoreOptions.cs | 1 + Source/ExecutionEngine/CommandLineOptions.cs | 16 ++++++++-- Source/Provers/SMTLib/SMTLibOptions.cs | 1 - Source/VCExpr/NormalizeNamer.cs | 4 --- .../VCExpr/QuantifierInstantiationEngine.cs | 29 +++++++++++++++---- Source/VCExpr/RandomiseNamer.cs | 1 - Source/VCGeneration/Checker.cs | 1 - Source/VCGeneration/ConditionGeneration.cs | 2 -- Source/VCGeneration/Counterexample.cs | 1 - Source/VCGeneration/ModelViewInfo.cs | 2 -- Source/VCGeneration/Split.cs | 1 - Source/VCGeneration/StratifiedVC.cs | 2 -- Source/VCGeneration/VCGenOptions.cs | 2 -- Source/VCGeneration/Wlp.cs | 2 -- .../ChangRoberts.bpl | 4 +-- .../inductive-sequentialization/PingPong.bpl | 6 ++-- .../ProducerConsumer.bpl | 2 +- Test/civl/paxos/PaxosActions.bpl | 2 +- Test/inst/ying_sort.bpl | 2 +- 19 files changed, 45 insertions(+), 36 deletions(-) diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index d60f52230..4e91977a2 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -107,6 +107,7 @@ public enum VerbosityLevel bool ConcurrentHoudini { get; } double VcsPathJoinMult { get; } bool VerifySeparately { get; } + bool KeepQuantifier { get; } public enum ProverWarnings { diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index ff4755836..06653bfe9 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -1,11 +1,9 @@ using System; using System.Collections.Generic; using System.Collections.Specialized; -using System.Diagnostics; using System.Diagnostics.Contracts; using System.IO; using Microsoft.Boogie.SMTLib; -using VC; namespace Microsoft.Boogie { @@ -519,6 +517,11 @@ public bool PrintInlined { public int LiveVariableAnalysis { get; set; } = 1; + public bool KeepQuantifier { + get => keepQuantifier; + set => keepQuantifier = value; + } + public HashSet Libraries { get; set; } = new HashSet(); // Note that procsToCheck stores all patterns

supplied with /proc:

@@ -568,6 +571,7 @@ void ObjectInvariant5() private bool emitDebugInformation = true; private bool normalizeNames; private bool normalizeDeclarationOrder = true; + private bool keepQuantifier = false; public List Cho { get; set; } = new(); @@ -1322,7 +1326,8 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("trustSequentialization", x => trustSequentialization = x) || ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) || ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) || - ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) + ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) || + ps.CheckBooleanFlag("keepQuantifier", x => keepQuantifier = x) ) { // one of the boolean flags matched @@ -1933,6 +1938,11 @@ Track and report which program elements labeled with an report. This generalizes and replaces the previous (undocumented) `/printNecessaryAssertions` option. + /keepQuantifier + If pool-based quantifier instantiation creates instances of a quantifier + then keep the quantifier along with the instances. By default, the quantifier + is dropped if any instances are created. + ---- Verification-condition splitting -------------------------------------- /vcsMaxCost: diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs index 354c91979..af4100123 100644 --- a/Source/Provers/SMTLib/SMTLibOptions.cs +++ b/Source/Provers/SMTLib/SMTLibOptions.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Generic; using Microsoft.Boogie.SMTLib; namespace Microsoft.Boogie diff --git a/Source/VCExpr/NormalizeNamer.cs b/Source/VCExpr/NormalizeNamer.cs index 8f0ebb0c1..b371210ba 100644 --- a/Source/VCExpr/NormalizeNamer.cs +++ b/Source/VCExpr/NormalizeNamer.cs @@ -1,7 +1,3 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; - namespace Microsoft.Boogie.VCExprAST { public class NormalizeNamer : ScopedNamer diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index 1bae1b1cc..1f062ba91 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -374,17 +374,34 @@ private VCExpr LetConvert(VCExpr vcExpr) private VCExpr AugmentWithInstances(VCExprQuantifier quantifierExpr) { + var instances = quantifierInstantiationInfo[quantifierExpr].instances; + if (instances.Count == 0) + { + return quantifierExpr; + } if (quantifierExpr.Quan == Quantifier.ALL) { - return vcExprGen.And(quantifierExpr, - vcExprGen.NAry(VCExpressionGenerator.AndOp, - quantifierInstantiationInfo[quantifierExpr].instances.Values.ToList())); + var instantiatedConjuncts = vcExprGen.NAry(VCExpressionGenerator.AndOp, instances.Values.ToList()); + if (exprTranslator.GenerationOptions.Options.KeepQuantifier) + { + return vcExprGen.And(quantifierExpr, instantiatedConjuncts); + } + else + { + return instantiatedConjuncts; + } } else { - return vcExprGen.Or(quantifierExpr, - vcExprGen.NAry(VCExpressionGenerator.OrOp, - quantifierInstantiationInfo[quantifierExpr].instances.Values.ToList())); + var instantiatedDisjuncts = vcExprGen.NAry(VCExpressionGenerator.OrOp, instances.Values.ToList()); + if (exprTranslator.GenerationOptions.Options.KeepQuantifier) + { + return vcExprGen.Or(quantifierExpr, instantiatedDisjuncts); + } + else + { + return instantiatedDisjuncts; + } } } diff --git a/Source/VCExpr/RandomiseNamer.cs b/Source/VCExpr/RandomiseNamer.cs index 4a85f3ff4..6fe1ad021 100644 --- a/Source/VCExpr/RandomiseNamer.cs +++ b/Source/VCExpr/RandomiseNamer.cs @@ -1,5 +1,4 @@ using System; -using System.Diagnostics.Contracts; namespace Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index b0f145e5e..195361cfd 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -6,7 +6,6 @@ using Microsoft.Boogie.VCExprAST; using System.Diagnostics; using System.Threading.Tasks; -using Microsoft.Boogie.SMTLib; using VC; namespace Microsoft.Boogie diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a4ac161a4..46fe6b792 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -8,9 +8,7 @@ using Microsoft.Boogie.GraphUtil; using System.Diagnostics.Contracts; using System.IO; -using System.Runtime.CompilerServices; using System.Threading.Tasks; -using VC; using Set = Microsoft.Boogie.GSet; namespace VC diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs index 11e5ff3d9..31cafb18c 100644 --- a/Source/VCGeneration/Counterexample.cs +++ b/Source/VCGeneration/Counterexample.cs @@ -7,7 +7,6 @@ using Microsoft.Boogie.VCExprAST; using VC; using VCGeneration; -using Set = Microsoft.Boogie.GSet; namespace Microsoft.Boogie { diff --git a/Source/VCGeneration/ModelViewInfo.cs b/Source/VCGeneration/ModelViewInfo.cs index 8aedd87bd..2e9d547ed 100644 --- a/Source/VCGeneration/ModelViewInfo.cs +++ b/Source/VCGeneration/ModelViewInfo.cs @@ -1,8 +1,6 @@ using System.Collections.Generic; using Microsoft.Boogie; -using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts; -using Set = Microsoft.Boogie.GSet; namespace VC { diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index aba8e05df..7b397fa0b 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -9,7 +9,6 @@ using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; -using VCGeneration; using System.Threading.Tasks; namespace VC diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 5a296ffc4..19cfe5426 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2,10 +2,8 @@ using System.Collections; using System.Collections.Generic; using System.Diagnostics; -using System.Linq; using System.IO; using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; using System.Diagnostics.Contracts; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/VCGenOptions.cs b/Source/VCGeneration/VCGenOptions.cs index 765e1772b..6fc1ca5f5 100644 --- a/Source/VCGeneration/VCGenOptions.cs +++ b/Source/VCGeneration/VCGenOptions.cs @@ -1,5 +1,3 @@ -using VC; - namespace Microsoft.Boogie; public interface VCGenOptions : SMTLibOptions diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 67d8b54f4..e26ed57c7 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -2,8 +2,6 @@ using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using System.Diagnostics.Contracts; -using System.Collections.Generic; -using System.Runtime.CompilerServices; using Microsoft.BaseTypes; namespace VC diff --git a/Test/civl/inductive-sequentialization/ChangRoberts.bpl b/Test/civl/inductive-sequentialization/ChangRoberts.bpl index 61d4b8a4a..bc2174aaf 100644 --- a/Test/civl/inductive-sequentialization/ChangRoberts.bpl +++ b/Test/civl/inductive-sequentialization/ChangRoberts.bpl @@ -115,10 +115,10 @@ modifies channel; assume {:add_to_pool "INV2", Next(Max(id))} true; havoc channel; - assume (forall i:int :: 1 <= i && i <= n ==> channel[Next(i)] == EmptyChannel()[id[i] := 1 ]); + assume (forall i:int :: {:add_to_pool "CHANNEL_INV", i} 1 <= i && i <= n ==> channel[Next(i)] == EmptyChannel()[id[i] := 1 ]); assume (forall i:int :: i < 1 || i > n ==> channel[i] == EmptyChannel()); call create_asyncs((lambda pa:P :: Pid(pa->pid->val))); - assume (forall i:int, msg:int :: Pid(i) && channel[i][msg] > 0 ==> msg == id[Prev(i)]); + assume (forall i:int, msg:int :: {:add_to_pool "CHANNEL_INV", Prev(i)} Pid(i) && channel[i][msg] > 0 ==> msg == id[Prev(i)]); } action {:layer 2} diff --git a/Test/civl/inductive-sequentialization/PingPong.bpl b/Test/civl/inductive-sequentialization/PingPong.bpl index 13031a2ef..1cf3f53ba 100644 --- a/Test/civl/inductive-sequentialization/PingPong.bpl +++ b/Test/civl/inductive-sequentialization/PingPong.bpl @@ -49,7 +49,7 @@ modifies channel; assert handles == BothHandles(cid); assert channel[cid] == ChannelPair(EmptyChannel(), EmptyChannel()); - assume {:add_to_pool "INV", c, c+1} 0 < c; + assume {:add_to_pool "INV", 0, c, c+1} 0 < c; if (*) { channel[cid] := ChannelPair(EmptyChannel(), EmptyChannel()[c := 1]); call create_async(PONG(c, One(Right(cid)))); @@ -75,7 +75,7 @@ action {:layer 2} PING' (x: int, {:linear_in} p: One ChannelHandle) creates PING; modifies channel; { - assert (exists {:pool "INV"} m:int :: channel[p->val->cid]->left[m] > 0); + assert (exists {:pool "INV"} m:int :: {:add_to_pool "INV", m} channel[p->val->cid]->left[m] > 0); assert (forall m:int :: channel[p->val->cid]->right[m] == 0); call PING(x, p); } @@ -84,7 +84,7 @@ action {:layer 2} PONG' (y: int, {:linear_in} p: One ChannelHandle) creates PONG; modifies channel; { - assert (exists {:pool "INV"} m:int :: channel[p->val->cid]->right[m] > 0); + assert (exists {:pool "INV"} m:int :: {:add_to_pool "INV", m} channel[p->val->cid]->right[m] > 0); assert (forall m:int :: channel[p->val->cid]->left[m] == 0); call PONG(y, p); } diff --git a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl index 7e16dc255..8a8832875 100644 --- a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl +++ b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl @@ -57,7 +57,7 @@ modifies channels; C := channel->C; head := channel->head; tail := channel->tail; - assume {:add_to_pool "INV1", c} 0 < c; + assume {:add_to_pool "INV1", c, c+1} 0 < c; if (*) { assume head == tail; call create_async(PRODUCER(c, One(Send(cid)))); diff --git a/Test/civl/paxos/PaxosActions.bpl b/Test/civl/paxos/PaxosActions.bpl index a1f3cbb78..44c72dcc3 100644 --- a/Test/civl/paxos/PaxosActions.bpl +++ b/Test/civl/paxos/PaxosActions.bpl @@ -56,7 +56,7 @@ modifies decision; assert voteInfo[r] is Some; assert voteInfo[r]->t->value == v; - assume {:add_to_pool "Round", r} true; + assume {:add_to_pool "Round", r} {:add_to_pool "NodeSet", q} true; if (*) { assume IsSubset(q, voteInfo[r]->t->ns) && IsQuorum(q); diff --git a/Test/inst/ying_sort.bpl b/Test/inst/ying_sort.bpl index 263007517..4c148955b 100644 --- a/Test/inst/ying_sort.bpl +++ b/Test/inst/ying_sort.bpl @@ -7,7 +7,7 @@ function {:inline} InOrder(x: int, y: int, z: int): bool { function {:inline} Permutation(A: Vec E, B: Vec E): bool { Vec_Len(A) == Vec_Len(B) && - (forall {:pool "A"} k: int :: {:add_to_pool "A", k} InOrder(0, k, Vec_Len(A)) ==> + (forall {:pool "A"} k: int :: {:add_to_pool "A", k} {:add_to_pool "B", k} InOrder(0, k, Vec_Len(A)) ==> (exists {:pool "B"} k': int :: {:add_to_pool "B", k'} InOrder(0, k', Vec_Len(B)) ==> Vec_Nth(A, k) == Vec_Nth(B, k'))) }