From fa84420e5cd21a4279fbb56ce410cce474842395 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 4 Jan 2024 16:20:33 +0000 Subject: [PATCH] Added more verbose lines to strategies --- .../src/main/java/quickcheck/QuickCheck.java | 12 ++++++++-- .../strategies/DirectQCStrategy.java | 23 +++++++++++++++---- .../quickcheck/visitors/TrivialQCVisitor.java | 10 +++++++- 3 files changed, 37 insertions(+), 8 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index efa286bf4..010492ab1 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -29,6 +29,7 @@ import static quickcheck.commands.QCConsole.infof; import static quickcheck.commands.QCConsole.infoln; import static quickcheck.commands.QCConsole.verbose; +import static quickcheck.commands.QCConsole.verboseln; import java.lang.reflect.Constructor; import java.util.HashMap; @@ -181,6 +182,8 @@ public boolean initStrategies(long timeoutSecs) for (QCStrategy strategy: strategies) { + verbose("------------------------ Initializing %s strategy\n", strategy.getName()); + doChecks = doChecks && strategy.init(this); if (strategy.hasErrors()) @@ -193,6 +196,7 @@ public boolean initStrategies(long timeoutSecs) } } + verbose("------------------------ Initialized\n"); return doChecks; } @@ -321,12 +325,12 @@ public StrategyResults getValues(ProofObligation po) for (QCStrategy strategy: strategies) { - verbose("Invoking %s strategy\n", strategy.getName()); + verbose("------------------------ Invoking %s strategy on PO #%d\n", strategy.getName(), po.number); StrategyResults sresults = strategy.getValues(po, binds, ictxt); if (sresults.provedBy != null || sresults.disprovedBy != null) // No need to go further { - verbose("Obligation (dis)proved by %s\n", strategy.getName()); + verbose("Obligation resolved by %s\n", strategy.getName()); sresults.setDuration(System.currentTimeMillis() - before); sresults.setBinds(binds); sresults.setInExpression(poexp); @@ -359,6 +363,8 @@ public StrategyResults getValues(ProofObligation po) hasAllValues = hasAllValues || sresults.hasAllValues; // At least one has all values } + + verboseln("-------------------------"); } for (INBindingOverride bind: binds) @@ -383,6 +389,8 @@ public StrategyResults getValues(ProofObligation po) public void checkObligation(ProofObligation po, StrategyResults sresults) { + verbose("------------------------ Checking PO #%d\n", po.number); + try { resetErrors(); // Only flag fatal errors diff --git a/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java index c09c4fb27..e9ff7e3ec 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java @@ -25,7 +25,8 @@ package quickcheck.strategies; import static com.fujitsu.vdmj.plugins.PluginConsole.println; -import static com.fujitsu.vdmj.plugins.PluginConsole.verboseln; +import static quickcheck.commands.QCConsole.verbose; +import static quickcheck.commands.QCConsole.verboseln; import java.util.HashSet; import java.util.List; @@ -127,9 +128,9 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po) try { long before = System.currentTimeMillis(); - Context ctxt = Interpreter.getInstance().getInitialContext(); - LexLocation loc = po.exp.location; Interpreter in = Interpreter.getInstance(); + Context ctxt = in.getInitialContext(); + LexLocation loc = po.exp.location; INExpressionList list = in.findExpressions(loc.file, loc.startLine); INCasesExpression cases = null; @@ -150,6 +151,8 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po) ValueList values = po.exp.expType.apply(new INGetAllValuesVisitor(), ctxt); long timeout = INBindingGlobals.getInstance().getTimeout(); + verbose("Checking %d values of type %s\n", values.size(), po.exp.expType); + for (Value value: values) { boolean matched = false; @@ -170,6 +173,8 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po) if (!matched) { + verbose("Value %s does not match any case patterns\n", value); + TCNameToken name = new TCNameToken(po.location, po.location.module, po.exp.exp.toString()); Context cex = new Context(po.location, "Counterexample", Interpreter.getInstance().getInitialContext()); cex.put(name, value); @@ -230,24 +235,32 @@ private StrategyResults directTotalObligation(TotalFunctionObligation po) if (exdef.bodyObligationCount > 0) { - return new StrategyResults(); // Body can fail in principle, so not definitely total + verboseln("Function body raises some proof obligations, so not total"); + return new StrategyResults(); } + + verboseln("Function body does not raise any obligations"); if (exdef.isUndefined || !TypeComparator.isSubType(exdef.actualResult, exdef.expectedResult)) { - return new StrategyResults(); // Body may not be the right type, so not definitely total + verboseln("But function body type is not a subtype of the return type, so not total"); + return new StrategyResults(); } + verboseln("Function body type always matches the return type"); + long before = System.currentTimeMillis(); exdef.body.apply(visitor, null); if (visitor.isTotal()) { + verboseln("Function body has no partial operators"); return new StrategyResults(getName(), "(body is total)", null, System.currentTimeMillis() - before); } else { + verboseln("But function body contains some partial operators"); return new StrategyResults(); } } diff --git a/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java b/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java index fcee029b5..28d976032 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java +++ b/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java @@ -24,6 +24,8 @@ package quickcheck.visitors; +import static quickcheck.commands.QCConsole.verbose; + import java.util.List; import java.util.Stack; import java.util.Vector; @@ -276,8 +278,14 @@ else if (node.left instanceof TCIntegerLiteralExpression && @Override public Boolean caseExpression(TCExpression node, Stack truths) { - if (truths.contains(node)) + int idx = truths.indexOf(node); + + if (idx >= 0) { + TCExpression original = truths.get(idx); + verbose("Expression %s defined at line %d\n", original, original.location.startLine); + verbose("Expression %s true at line %d\n", node, node.location.startLine); + evaluated.add(Utils.deBracketed(node)); // This truth was used return true; }