diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs index 6f8e33820..3cd06890b 100644 --- a/Source/Core/Xml.cs +++ b/Source/Core/Xml.cs @@ -112,7 +112,7 @@ public void WriteEndMethod(string outcome, DateTime endTime, TimeSpan elapsed, i } public void WriteSplit(int splitNum, int iteration, IEnumerable asserts, DateTime startTime, - string outcome, TimeSpan elapsed, int? resourceCount) + string outcome, TimeSpan elapsed, int? resourceCount, int? smtInputSize) { Contract.Requires(splitNum > 0); Contract.Requires(outcome != null); @@ -145,6 +145,10 @@ public void WriteSplit(int splitNum, int iteration, IEnumerable asser { wr.WriteAttributeString("resourceCount", resourceCount.ToString()); } + if (smtInputSize is not null) + { + wr.WriteAttributeString("smtInputSize", smtInputSize.ToString()); + } wr.WriteEndElement(); // conclusion wr.WriteEndElement(); // assertionBatch diff --git a/Source/ExecutionEngine/ImplementationRunResult.cs b/Source/ExecutionEngine/ImplementationRunResult.cs index bd9c89cfe..b9fe6c7b0 100644 --- a/Source/ExecutionEngine/ImplementationRunResult.cs +++ b/Source/ExecutionEngine/ImplementationRunResult.cs @@ -78,7 +78,7 @@ public void ProcessXml(ExecutionEngine engine) { foreach (var vcResult in RunResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) { engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime, - vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount); + vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount, vcResult.CheckInputs.TotalSize); } engine.Options.XmlSink.WriteEndMethod(VcOutcome.ToString().ToLowerInvariant(), diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index c2beaa48a..d5ec9e33c 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Text; using System.Threading; using System.Threading.Tasks; using Microsoft.Boogie.SMTLib; @@ -21,6 +22,9 @@ public enum SolverOutcome public abstract class ProverInterface { + public int VCExprSize { get; protected set; } + public abstract int CommonSize { get; } + public static ProverInterface CreateProver(SMTLibOptions libOptions, Program prog, string /*?*/ logFilePath, bool appendLogFile, uint timeout, int taskID = -1) diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs index fe172abae..46bd98d75 100644 --- a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs @@ -71,11 +71,9 @@ public override async Task Check(string descriptiveName, VCExpr v SetupProcess(); checkSatSent = false; FullReset(gen); - if (options.LogFilename != null && currentLogFile == null) { currentLogFile = OpenOutputFile(descriptiveName); - await currentLogFile.WriteAsync(common.ToString()); } SendVCOptions(); @@ -84,8 +82,9 @@ public override async Task Check(string descriptiveName, VCExpr v OptimizationRequests.Clear(); - string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + string vcString = "(assert (not\n" + VcExpr2String(vc, 1) + "\n))"; FlushAxioms(); + VCExprSize = vcString.Length; Push(); SendVCId(descriptiveName); @@ -284,7 +283,8 @@ protected override void Send(string s, bool isCommon) // Boogie emits comments after the solver has responded. In batch // mode, sending these to the solver is problematic. But they'll // still get sent to the log below. - if (Process != null && !checkSatSent) { + if (Process != null && !checkSatSent) + { Process.Send(s); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index e58b25eac..6627af0ec 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -46,7 +46,8 @@ private void PossiblyRestart() if (Process != null && processNeedsRestart) { processNeedsRestart = false; SetupProcess(); - Process.Send(common.ToString()); + var c = common.ToString(); + Process.Send(c); } } @@ -63,7 +64,8 @@ public override int FlushAxiomsToTheoremProver() } private bool hasReset = true; - public override async Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) + public override async Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, + int errorLimit, CancellationToken cancellationToken) { currentErrorHandler = handler; try @@ -100,7 +102,8 @@ public override async Task Check(string descriptiveName, VCExpr v SendThisVC("(push 1)"); DeclCollector.Push(); - string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + string vcString = "(assert (not\n" + VcExpr2String(vc, 1) + "\n))"; + VCExprSize = vcString.Length; FlushAxioms(); SendVCId(descriptiveName); SendVCOptions(); @@ -145,7 +148,7 @@ public override async Task Reset(VCExpressionGenerator generator) Process.Send(c); if (currentLogFile != null) { - currentLogFile.WriteLine(c); + await currentLogFile.WriteLineAsync(c); } } @@ -433,7 +436,7 @@ private Task CheckSplit(SortedSet split, uint timeLimit, uin expr = VCExprGen.AndSimp(expr, lit); } - SendThisVC("(assert " + VCExpr2String(expr, 1) + ")"); + SendThisVC("(assert " + VcExpr2String(expr, 1) + ")"); if (options.Solver == SolverKind.Z3) { SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)"); @@ -533,7 +536,7 @@ private async Task CheckSatAndGetResponse(CancellationToken cance public override async Task Evaluate(VCExpr expr) { - string vcString = VCExpr2String(expr, 1); + string vcString = VcExpr2String(expr, 1); var resp = await SendVcRequest($"(get-value ({vcString}))"); if (resp == null) { @@ -697,7 +700,7 @@ public override int GetRCount() nameCounter++; nameToAssumption.Add(name, i); - string vcString = VCExpr2String(vc, 1); + string vcString = VcExpr2String(vc, 1); AssertAxioms(); SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); i++; @@ -748,13 +751,13 @@ public override int GetRCount() var hardAssumptionStrings = new List(); foreach (var a in hardAssumptions) { - hardAssumptionStrings.Add(VCExpr2String(a, 1)); + hardAssumptionStrings.Add(VcExpr2String(a, 1)); } var currAssumptionStrings = new List(); foreach (var a in softAssumptions) { - currAssumptionStrings.Add(VCExpr2String(a, 1)); + currAssumptionStrings.Add(VcExpr2String(a, 1)); } Push(); diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index 16c5cf28e..c35af823b 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -91,11 +91,11 @@ public override void AssertNamed(VCExpr vc, bool polarity, string name) string vcString; if (polarity) { - vcString = VCExpr2String(vc, 1); + vcString = VcExpr2String(vc, 1); } else { - vcString = "(not " + VCExpr2String(vc, 1) + ")"; + vcString = "(not " + VcExpr2String(vc, 1) + ")"; } AssertAxioms(); @@ -149,6 +149,8 @@ protected static string Sanitize(string msg) return msg; } + public override int CommonSize => common.Length; + public override void LogComment(string comment) { SendCommon("; " + comment); @@ -191,63 +193,65 @@ private void FindDependentTypes(Type type, List dependentT private void PrepareDataTypes() { - if (ctx.KnownDatatypes.Count > 0) + if (ctx.KnownDatatypes.Count <= 0) { - GraphUtil.Graph dependencyGraph = new GraphUtil.Graph(); - foreach (var datatype in ctx.KnownDatatypes) + return; + } + + var dependencyGraph = new GraphUtil.Graph(); + foreach (var datatype in ctx.KnownDatatypes) + { + dependencyGraph.AddSource(datatype); + foreach (DatatypeConstructor f in datatype.Constructors) { - dependencyGraph.AddSource(datatype); - foreach (Function f in datatype.Constructors) + var dependentTypes = new List(); + foreach (Variable v in f.InParams) { - var dependentTypes = new List(); - foreach (Variable v in f.InParams) - { - FindDependentTypes(v.TypedIdent.Type, dependentTypes); - } - foreach (var result in dependentTypes) - { - dependencyGraph.AddEdge(datatype, result); - } + FindDependentTypes(v.TypedIdent.Type, dependentTypes); + } + foreach (var result in dependentTypes) + { + dependencyGraph.AddEdge(datatype, result); } } + } - GraphUtil.StronglyConnectedComponents sccs = - new GraphUtil.StronglyConnectedComponents(dependencyGraph.Nodes, dependencyGraph.Predecessors, - dependencyGraph.Successors); - sccs.Compute(); - foreach (GraphUtil.SCC scc in sccs) + var sccs = + new GraphUtil.StronglyConnectedComponents(dependencyGraph.Nodes, dependencyGraph.Predecessors, + dependencyGraph.Successors); + sccs.Compute(); + foreach (var scc in sccs) + { + string datatypesString = ""; + string datatypeConstructorsString = ""; + foreach (var datatype in scc) { - string datatypesString = ""; - string datatypeConstructorsString = ""; - foreach (var datatype in scc) + datatypesString += "(" + new SMTLibExprLineariser(libOptions).TypeToString(new CtorType(Token.NoToken, datatype, new List())) + " 0)"; + string datatypeConstructorString = ""; + foreach (Function f in datatype.Constructors) { - datatypesString += "(" + new SMTLibExprLineariser(libOptions).TypeToString(new CtorType(Token.NoToken, datatype, new List())) + " 0)"; - string datatypeConstructorString = ""; - foreach (Function f in datatype.Constructors) + string quotedConstructorName = Namer.GetQuotedName(f, f.Name); + datatypeConstructorString += "(" + quotedConstructorName + " "; + foreach (Variable v in f.InParams) { - string quotedConstructorName = Namer.GetQuotedName(f, f.Name); - datatypeConstructorString += "(" + quotedConstructorName + " "; - foreach (Variable v in f.InParams) - { - string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name); - datatypeConstructorString += "(" + quotedSelectorName + " " + - DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") "; - } - - datatypeConstructorString += ") "; + string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name); + datatypeConstructorString += "(" + quotedSelectorName + " " + + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") "; } - datatypeConstructorsString += "(" + datatypeConstructorString + ") "; + datatypeConstructorString += ") "; } - List decls = DeclCollector.GetNewDeclarations(); - foreach (string decl in decls) - { - SendCommon(decl); - } + datatypeConstructorsString += "(" + datatypeConstructorString + ") "; + } - SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))"); + List decls = DeclCollector.GetNewDeclarations(); + foreach (string decl in decls) + { + SendCommon(decl); } + + SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))"); } } @@ -318,7 +322,7 @@ private void PrepareFunctionDefinitions() funcDef += ") "; funcDef += new SMTLibExprLineariser(libOptions).TypeToString(defBody[0].Type) + " "; - funcDef += VCExpr2String(defBody[1], -1); + funcDef += VcExpr2String(defBody[1], -1); funcDef += ")"; generatedFuncDefs.Add(funcDef); definitionAdded.Add(f); @@ -402,13 +406,13 @@ private void SetupAxioms() var axioms = ctx.Axioms; if (axioms is VCExprNAry nary && nary.Op == VCExpressionGenerator.AndOp) { foreach (var expr in nary.UniformArguments) { - var str = VCExpr2String(expr, -1); + var str = VcExpr2String(expr, -1); if (str != "true") { AddAxiom(str); } } } else { - AddAxiom(VCExpr2String(axioms, -1)); + AddAxiom(VcExpr2String(axioms, -1)); } AxiomsAreSetup = true; @@ -970,7 +974,7 @@ private void ConvertErrorModel(StringBuilder m) protected readonly IList OptimizationRequests = new List(); - protected string VCExpr2String(VCExpr expr, int polarity) + public string VcExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); Contract.Ensures(Contract.Result() != null); @@ -1101,7 +1105,7 @@ public override VCExpressionGenerator VCExprGen //int numRealPushes; public override string VCExpressionToString(VCExpr vc) { - return VCExpr2String(vc, 1); + return VcExpr2String(vc, 1); } public override void PushVCExpression(VCExpr vc) @@ -1135,7 +1139,7 @@ public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int w assert += "-soft"; } - var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)"; + var expr = polarity ? VcExpr2String(vc, 1) : "(not\n" + VcExpr2String(vc, 1) + "\n)"; if (options.Solver == SolverKind.Z3 && isSoft) { expr += " :weight " + weight; @@ -1157,7 +1161,7 @@ public override void DefineMacro(Macro f, VCExpr vc) string printedName = Namer.GetQuotedName(f, f.Name); var argTypes = string.Join(" ", f.InParams.Select(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type))); string decl = "(define-fun " + printedName + " (" + argTypes + ") " + - DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")"; + DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VcExpr2String(vc, 1) + ")"; AssertAxioms(); SendThisVC(decl); } diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 49f23b1df..4adc5e319 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -19,6 +19,11 @@ enum CheckerStatus } + public record CheckInputs(int VcExprSize, int CommonSize) + { + public int TotalSize => VcExprSize + CommonSize; + } + /// /// Interface to the theorem prover specialized to Boogie. /// @@ -259,12 +264,13 @@ public TimeSpan ProverRunTime get { return proverRunTime; } } + public int SmtInputSize => thmProver.VCExprSize; + public int GetProverResourceCount() { return thmProver.GetRCount(); } - - + private async Task Check(string descriptiveName, VCExpr vc, CancellationToken cancellationToken) { try { outcome = await thmProver.Check(descriptiveName, vc, cce.NonNull(handler), Options.ErrorLimit, @@ -314,7 +320,8 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca proverRunTime = ProverStopwatch.Elapsed; } - public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit, CancellationToken cancellationToken) + public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, + uint timeout, uint rlimit, CancellationToken cancellationToken) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); @@ -333,6 +340,7 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface. ProverStart = DateTime.UtcNow; ProverStopwatch.Restart(); ProverTask = Check(descriptiveName, vc, cancellationToken); + return new CheckInputs(thmProver.VCExprSize, thmProver.CommonSize); } public SolverOutcome ReadOutcome() @@ -383,6 +391,8 @@ public override Task GoBackToIdle() throw new NotImplementedException(); } + public override int CommonSize => throw new NotImplementedException(); + public override Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) { throw new NotImplementedException(); diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 7cf747118..c0a52a9b0 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -38,16 +38,14 @@ public IReadOnlyList PrunedDeclarations { } } - readonly Dictionary /*!*/ - stats = new Dictionary(); + readonly Dictionary /*!*/ stats = new(); static int currentId = -1; Block splitBlock; bool assertToAssume; - List /*!*/ - assumizedBranches = new List(); + List /*!*/ assumizedBranches = new(); double score; bool scoreComputed; @@ -57,8 +55,7 @@ public IReadOnlyList PrunedDeclarations { public Dictionary GotoCmdOrigins { get; } - public readonly VerificationConditionGenerator /*!*/ - parent; + public readonly VerificationConditionGenerator /*!*/ parent; public Implementation /*!*/ Implementation => Run.Implementation; @@ -74,6 +71,7 @@ public readonly VerificationConditionGenerator /*!*/ // async interface public int SplitIndex { get; set; } public VerificationConditionGenerator.ErrorReporter reporter; + public CheckInputs CheckInputs { get; set; } public Split(VCGenOptions options, Func> /*!*/ getBlocks, Dictionary /*!*/ gotoCmdOrigins, @@ -899,6 +897,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie Asserts: Asserts, CoveredElements: CoveredElements, ResourceCount: resourceCount, + CheckInputs, SolverUsed: (Options as SMTLibSolverOptions)?.Solver); callback.OnVCResult(result); @@ -964,7 +963,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions() .Select(kv => new OptionValue(kv.Key, kv.Value))); - await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); + CheckInputs = await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); } public string Description diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index b2566f93e..47b0ee241 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -18,6 +18,7 @@ public record VerificationRunResult List Asserts, IEnumerable CoveredElements, int ResourceCount, + CheckInputs CheckInputs, SolverKind? SolverUsed ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, diff --git a/Test/commandline/xml.bpl b/Test/commandline/xml.bpl index 05ed63232..c66b3e3a5 100644 --- a/Test/commandline/xml.bpl +++ b/Test/commandline/xml.bpl @@ -1,5 +1,5 @@ -// RUN: %parallel-boogie -randomSeed:0 -xml:"%t-1.xml" "%s" -// RUN: %parallel-boogie -randomSeed:0 -xml:"%t-2.xml" "%s" +// RUN: %parallel-boogie -randomSeed:0 -proverLog:%t-1.smt -xml:"%t-1.xml" "%s" +// RUN: %parallel-boogie -randomSeed:0 -proverLog:%t-2.smt -xml:"%t-2.xml" "%s" // RUN: grep -Eo "resourceCount=\"[0-9]+\"" "%t-1.xml" | sort -g > "%t-res1" // RUN: grep -Eo "resourceCount=\"[0-9]+\"" "%t-2.xml" | sort -g > "%t-res2" // RUN: diff "%t-res1" "%t-res2" @@ -11,11 +11,11 @@ // CHECK: \ // CHECK: \ // CHECK: \ -// CHECK: \ +// CHECK: \ // CHECK: \ // CHECK: \ // CHECK: \ -// CHECK: \ +// CHECK: \ // CHECK: \ // CHECK: \ // CHECK: \