From b782ca9ced30f0c3ba71aaae2e2fd1369c41626a Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 01:51:48 -0800 Subject: [PATCH] Allow `/prune:0` to disable pruning (#848) Add a `/noprune` flag to turn off pruning. It's off by default, but this can be convenient if a) it's turned on earlier on the command line, or b) Boogie is being used from another system like Dafny. I would have made it `/prune:{1,0}`, but it's harder to make that backward compatible with the current behavior. --- Source/Directory.Build.props | 2 +- Source/ExecutionEngine/CommandLineOptions.cs | 19 ++++++++++++------- Test/commandline/noprune.bpl | 12 ++++++++++++ Test/coverage/verificationCoverage.bpl | 8 ++++---- Test/dafny/dafny-issue-4804.bpl | 2 +- Test/pruning/IncludeDep.bpl | 2 +- Test/pruning/MonomorphicSplit.bpl | 2 +- Test/pruning/NonmonomorphicSplit.bpl | 2 +- Test/pruning/Triggers.bpl | 4 ++-- Test/pruning/UsesClauses.bpl | 2 +- Test/test15/CommonVariablesPruning.bpl | 2 +- 11 files changed, 37 insertions(+), 20 deletions(-) create mode 100644 Test/commandline/noprune.bpl diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index f1d97551a..cbc7f6511 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.0.11 + 3.0.12 net6.0 false Boogie diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index faf89dc7b..ff4755836 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -1257,6 +1257,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.GetIntArgument(x => normalizeDeclarationOrder = x); return true; + case "prune": + ps.GetIntArgument(x => Prune = x); + return true; + default: bool optionValue = false; if (ps.CheckBooleanFlag("printUnstructured", x => optionValue = x)) @@ -1318,7 +1322,6 @@ 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("prune", x => Prune = x) || ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) ) { @@ -1889,12 +1892,14 @@ Boogie automatically detects monomorphic programs and enables the SMT theory of arrays. This option allows the use of axioms instead. /reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined to be +, instead of +. - /prune - Turn on pruning. Pruning will remove any top-level Boogie declarations - that are not accessible by the implementation that is about to be verified. - Without pruning, due to the unstable nature of SMT solvers, - a change to any part of a Boogie program has the potential - to affect the verification of any other part of the program. + /prune: + 0 - Turn off pruning. + 1 - Turn on pruning (default). Pruning will remove any top-level + Boogie declarations that are not accessible by the implementation + that is about to be verified. Without pruning, due to the unstable + nature of SMT solvers, a change to any part of a Boogie program + has the potential to affect the verification of any other part of + the program. Only use this if your program contains uses clauses where required, otherwise pruning will break your program. diff --git a/Test/commandline/noprune.bpl b/Test/commandline/noprune.bpl new file mode 100644 index 000000000..cf6e4ba4f --- /dev/null +++ b/Test/commandline/noprune.bpl @@ -0,0 +1,12 @@ +// RUN: %parallel-boogie -quiet -prune:0 -normalizeNames:0 -proverLog:"%t.noprune.smt2" "%s" +// RUN: %OutputCheck --file-to-check "%t.noprune.smt2" "%s" +// CHECK: ThisIsAFunction + +function ThisIsAFunction(): int uses { + axiom ThisIsAFunction() == 2; +} + +procedure P() +{ + assert 1 == 1; +} diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index 850c6b833..8fbc5a243 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -91,13 +91,13 @@ // CHECK: xy_sum // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage" // RUN: %diff "%s.expect" "%t.coverage" -// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a" +// RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune:1 "%s" > "%t.coverage-a" // RUN: %diff "%s.expect" "%t.coverage-a" -// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune "%s" > "%t.coverage-p" +// RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune:1 "%s" > "%t.coverage-p" // RUN: %diff "%s.expect" "%t.coverage-p" -// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d" +// RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune:1 "%s" > "%t.coverage-d" // RUN: %diff "%s.expect" "%t.coverage-d" -// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n" +// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune:1 "%s" > "%t.coverage-n" // RUN: %diff "%s.expect" "%t.coverage-n" procedure testRequiresAssign(n: int) diff --git a/Test/dafny/dafny-issue-4804.bpl b/Test/dafny/dafny-issue-4804.bpl index 747c9b313..2aa0b4b46 100644 --- a/Test/dafny/dafny-issue-4804.bpl +++ b/Test/dafny/dafny-issue-4804.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 /prune "%s" > "%t" +// RUN: %parallel-boogie /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 /prune:1 "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t" // CHECK: Boogie program verifier finished with 3 verified, 0 errors, 1 out of resource // dafny 4.3.0.0 diff --git a/Test/pruning/IncludeDep.bpl b/Test/pruning/IncludeDep.bpl index 69f33e240..f800b6528 100644 --- a/Test/pruning/IncludeDep.bpl +++ b/Test/pruning/IncludeDep.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" function f1 (x: int) : int; diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 956498d8c..56a21f196 100644 --- a/Test/pruning/MonomorphicSplit.bpl +++ b/Test/pruning/MonomorphicSplit.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /errorTrace:0 /printPruned:"%t" "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /errorTrace:0 /printPruned:"%t" "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t-after-monomorphicSplit.bpl" // The following checks are a bit simplistic, but this is diff --git a/Test/pruning/NonmonomorphicSplit.bpl b/Test/pruning/NonmonomorphicSplit.bpl index 17fbb7df6..0e61a7065 100644 --- a/Test/pruning/NonmonomorphicSplit.bpl +++ b/Test/pruning/NonmonomorphicSplit.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /trace /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /trace /errorTrace:0 "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t" // Related PR #767. diff --git a/Test/pruning/Triggers.bpl b/Test/pruning/Triggers.bpl index 966b28cb2..e1116afe7 100644 --- a/Test/pruning/Triggers.bpl +++ b/Test/pruning/Triggers.bpl @@ -1,4 +1,4 @@ - // RUN: %parallel-boogie /prune /errorTrace:0 "%s" > "%t" + // RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" function f1 (x: int) : bool; @@ -32,4 +32,4 @@ axiom (forall x: int :: {f5(f4(x)), f4(x)} f4(x)); procedure twoTriggers(x : int) ensures f4(x); { -} \ No newline at end of file +} diff --git a/Test/pruning/UsesClauses.bpl b/Test/pruning/UsesClauses.bpl index 0ec5f06c5..0ebe6cfe8 100644 --- a/Test/pruning/UsesClauses.bpl +++ b/Test/pruning/UsesClauses.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /prune /printPruned:"%tpruned" /errorTrace:0 "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /printPruned:"%tpruned" /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // UNSUPPORTED: batch_mode diff --git a/Test/test15/CommonVariablesPruning.bpl b/Test/test15/CommonVariablesPruning.bpl index 513c4c6c5..0cec41d8b 100644 --- a/Test/test15/CommonVariablesPruning.bpl +++ b/Test/test15/CommonVariablesPruning.bpl @@ -1,6 +1,6 @@ // VcsCores:1 means we only use a single solver for both procedures in this Boogie program. // Prune triggers a full reset after using the solver on one problem -// RUN: %boogie "%s" -typeEncoding:p -vcsCores:1 -normalizeNames:1 -prune -mv:- > "%t" +// RUN: %boogie "%s" -typeEncoding:p -vcsCores:1 -normalizeNames:1 -prune:1 -mv:- > "%t" // RUN: %diff "%s.expect" "%t" --ignore-matching-lines='else ->' // Part of the MultiDimArray test from Dafny: https://github.com/dafny-lang/dafny/blob/cc913d9159ded2ad131c048135f817e49f500e50/Test/dafny0/MultiDimArray.dfy