Allow keeping SMT commands unchanged when Boogie identifiers are renamed #452

keyboardDrummer · 2021-11-11T11:47:24Z

Related Dafny issue: dafny-lang/dafny#1585

This PR includes changes #453

SMT solvers in practice can show significantly different behavior in terms of total runtime and check-sat result when identifiers in the input are renamed. Such changes in solver output are often surprising to the Boogie programmer, so this PR introduces an option to normalize names in the Boogie program.

Changes

Enables normalizing any names that occur in the Boogie program when translating it into SMT commands.
Remove unused code that was in SMTLibNamer and UniqueNamer

Testing

Add a test that checks that renaming various elements in a Boogie program does not effect the solver input.
Add the /normalizeNames:1 option to all tests that inspect the SMT model, to verify that names in the parsed SMT model are correctly translated back to their original name.

Source/Provers/SMTLib/SmtLibNameUtils.cs

Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs

Source/VCGeneration/Checker.cs

MikaelMayer

Just minor changes.

shazqadeer · 2021-11-11T22:58:07Z

@MikaelMayer : Removing a lock does not appear a minor change to me.

shazqadeer · 2021-11-11T23:00:47Z

This PR enables discarding any names that occur in the Boogie program when translating it into SMT commands.

I could not understand the sentence above in the PR description. Perhaps use extra sentences.

shazqadeer · 2021-11-11T23:01:13Z

@RustanLeino : I would appreciate your input on this PR.

keyboardDrummer · 2021-11-12T10:39:11Z

This PR enables discarding any names that occur in the Boogie program when translating it into SMT commands.

I could not understand the sentence above in the PR description. Perhaps use extra sentences.

Done.

shazqadeer · 2021-11-12T18:11:13Z

The PR title talks about renaming which is an accurate description of the goals of the PR. However, the PR description talks about discarding which is misleading and confusing.
The option name DiscardNames is confusing and should be renamed to something that indicates that variables in the input are being renamed according to some scheme to product the SMT output.

I see that you are renaming names as n0, n1, ... Did I get that right? Is it still possible that a minor change to an input file would cause the names assigned to variables x and y to shift? I imagine that the actual assignment of names to x and y would depend on some iteration order. Changes to names other than x and y could cause the iteration order to change.

keyboardDrummer · 2021-11-14T21:30:19Z

The PR title talks about renaming which is an accurate description of the goals of the PR. However, the PR description talks about discarding which is misleading and confusing.

The option name DiscardNames is confusing and should be renamed to something that indicates that variables in the input are being renamed according to some scheme to product the SMT output.

I see that you are renaming names as n0, n1, ... Did I get that right? Is it still possible that a minor change to an input file would cause the names assigned to variables x and y to shift? I imagine that the actual assignment of names to x and y would depend on some iteration order. Changes to names other than x and y could cause the iteration order to change.

Good callout. The steps I'm adding to Boogie are these:

Remove top level declarations that aren't used for the verification condition that's about to be verified. Introduce aggressive pruning and the related 'uses' keyword for constants and functions #450
Reorder top level axioms based on a content hash. Content hash based reordering #454
[Optionally] Rename top level declarations based on their order. Allow keeping SMT commands unchanged when Boogie identifiers are renamed #452

The combination of these allows solver input to remain unchanged, when changes unrelated to the verification condition being solved are made, and when declarations are reordered or renamed.

However, you are right that adding something that isn't pruned away might change the names of all the other declarations in the program, due to the naming by order system. One question is whether we should always try to minimise the amount of changes in solver input, or focus solely on providing zero solver input changes when possible. I'm doing the latter since that's the only thing which guarantees no change in solver behavior.

If you're adding something that cannot be pruned away, then a small change to solver input is unavoidable. That the renaming scheme makes this a bigger change is something I'm accepting, given the benefit of getting zero solver input changes when only doing a rename.

Another reason I'm adding the renaming scheme is because it's useful for Dafny. Dafny names some of the Boogie declarations it compiles to using a global counter, so changes to one proof can effect the names generated for another proof. Renaming those declarations after pruning and reordering in Boogie makes the names only depend on the current proof again. Another way of solving this problem would be for Dafny to generate one Boogie program per verification condition, but that's a big change for us.

An improvement to this order based renaming scheme could be to choose a base-name based on a content hash instead having it fixed, but I'm leaving that for another PR since it requires significantly more changes and I saw good results for verification stability in Dafny with the PRs that are published now.

RustanLeino · 2021-11-16T00:38:21Z

I think

focus solely on providing zero solver input changes when possible

is a good goal to focus on.

RustanLeino

I like this option. I have some questions that the code I read didn't answer for me:

Are only top-level declarations renamed? Or does the renaming also apply to local variables, quantified variables, and incarnation variables?
Boogie performs "lambda lifting", where it creates a function for each lambda binder in the given program. Do these play a part of the renaming?
Under the renaming option, is the output affected? That is, will Boogie rename things back before given back any results to its callers? For example, if you want to use the counterexample display in the Dafny IDE, then will it still know what variables to ask for value for? (If the output is affected, then I have doubts about how useful this PR actually is to Boogie clients.)

RustanLeino · 2021-11-16T00:44:06Z

Source/Provers/SMTLib/SmtLibNameUtils.cs

- var allGood = true;
-
- foreach (char ch in s)
+ validIdChar = new bool[255];


Why 255? I'm guessing it has to do with 255 being close to 2^8. But then, why not use all 256? Or is 255 just an arbitrary "pretty small" number?

I don't know, I didn't write this code, just moved it.

Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs

Source/Core/CommandLineOptions.cs

…itDebugInformation as a command line option

RustanLeino · 2021-11-17T18:13:36Z

I could look into why those names are maintained, but we can also leave it for later.

Don't worry about the types T@T and T@U and the function tickleBool, etc. These are always added by Boogie, so they will be the same for any input.

RustanLeino · 2021-11-17T18:34:58Z

The output was effected but I've since changed the ModelParser so it automatically reverts the renaming when recovering a model from Z3, this makes the counterexample display unchanged by this PR.

Excellent! Thanks.

shazqadeer · 2021-11-21T23:43:34Z

Source/Core/CommandLineOptions.cs

+ ps.GetNumericArgument(ref emitDebugInformation);
+ return true;
+
+ case "discardNames":


I find the option name "discardNames" confusing. I have indicated several times before in my feedback that the verb "discard" is inappropriate for what this PR is trying to achieve.

Hey, sorry for not responding to your earlier comment.

Do you have a suggestion for a different name? Your earlier comment seems to indicate something with rename, but I find that renameNames does not say enough about what the option does.

The goal of the option is to get verification output that does not depend on the original identifier names and is deterministic. I picked discardNames to indicate that the original program names are not used, leaving the reader to conclude that they must be replaced using some fixed naming scheme.

Here are some ideas for other names:
replaceNames, discardAndReplaceNames, ignoreNames, or renameBasedOnContent

Do you have a preference or suggestion?

Maybe normalizeNames?

normalizeNames appears to be the best option so far.

Great, changed it to normalizeNames.

…tion behavior of the proof (#1612) In DafnyOptions.cs, turn on Boogie's `Prune` and `NormaliseNames` option, and turn off `EmitDebugInformation`, to increase verification stability. Use `uses` clauses on constants and functions, both in DafnyPrelude.bpl and in generated Boogie declarations, and the `include_dep` attribute on axioms, to ensure not too much is pruned. More information on these Boogie features can be found in the PRs that introduce them: boogie-org/boogie#450, boogie-org/boogie#452, boogie-org/boogie#453, boogie-org/boogie#454, boogie-org/boogie#464 In follow-up PRs, we will replace all `include_dep` with `uses` clauses, since they allow more but still correct pruning. This PR also updates the test `SchorrWaite.dfy` to make it more stable. Changes stolen from #1620

Enable turning off skolimid

427842a

keyboardDrummer force-pushed the thrashingNamer branch 2 times, most recently from 665b2fa to e0cc6f1 Compare November 11, 2021 11:49

keyboardDrummer mentioned this pull request Nov 11, 2021

Verification behavior changes when making unrelated changes dafny-lang/dafny#1585

Closed

keyboardDrummer marked this pull request as ready for review November 11, 2021 13:27

Add tests for EmitSkolimIdAndQId

4b80306

MikaelMayer approved these changes Nov 11, 2021

View reviewed changes

MikaelMayer requested changes Nov 11, 2021

View reviewed changes

Correct spelling of skolem

d085aa4

keyboardDrummer changed the title ~~Enable discarding names when translating to SMT~~ Enable keeping SMT commands constant when Boogie identifiers are renamed Nov 12, 2021

keyboardDrummer changed the title ~~Enable keeping SMT commands constant when Boogie identifiers are renamed~~ Allow keeping SMT commands constant when Boogie identifiers are renamed Nov 12, 2021

keyboardDrummer requested a review from RustanLeino November 12, 2021 10:37

keyboardDrummer mentioned this pull request Nov 14, 2021

Content hash based reordering #454

Merged

RustanLeino requested changes Nov 16, 2021

View reviewed changes

Remy Willems added 9 commits November 17, 2021 11:16

Also don't emit :boogie-vc-id, perform some refactoring and expose em…

b361dda

…itDebugInformation as a command line option

Rename UniqueNamer file

ec6cf6a

Add missing using

8a9272a

Make SMTLibNamer obsolete

af1f8db

Remove SMTLibNamer

3bf6828

Rename UniqueNamer

81fba48

Remove unused code

5733338

Enable trashing names

dc3cc00

Rename

1092937

Remy Willems added 10 commits November 17, 2021 15:47

Remove accidentaly added file, and update .gitignore

dfee172

Move class into separate file

6a2b790

Merge branch 'master' into thrashingNamer

4c4f0f4

Fix big related to duplicate renames

a890180

Turn on discardNames for an extra test

2e1bc91

Turn on more discard names in model tests

d63f139

Slightly different naming scheme

c3b16a4

Fix clone

1dd3d0c

Use a less colliding base name

42a5124

Update else clause in ControlFlow test

8f57127

keyboardDrummer requested review from shazqadeer and RustanLeino November 17, 2021 18:32

RustanLeino previously approved these changes Nov 17, 2021

View reviewed changes

keyboardDrummer requested a review from MikaelMayer November 17, 2021 20:35

MikaelMayer previously approved these changes Nov 17, 2021

View reviewed changes

shazqadeer changed the title ~~Allow keeping SMT commands constant when Boogie identifiers are renamed~~ Allow keeping SMT commands unchanged when Boogie identifiers are renamed Nov 21, 2021

shazqadeer requested changes Nov 21, 2021

View reviewed changes

Merge remote-tracking branch 'origin/master' into thrashingNamer

df888b3

keyboardDrummer dismissed stale reviews from MikaelMayer and RustanLeino via df888b3 November 22, 2021 14:08

keyboardDrummer requested a review from shazqadeer November 22, 2021 14:21

Rename discardNames to normalizeNames

2c2f651

shazqadeer approved these changes Nov 22, 2021

View reviewed changes

keyboardDrummer merged commit 9f53039 into boogie-org:master Nov 22, 2021

keyboardDrummer deleted the thrashingNamer branch November 22, 2021 17:44

keyboardDrummer mentioned this pull request Dec 8, 2021

feat: Prevent changes unrelated to a proof from changing the verification behavior of the proof dafny-lang/dafny#1612

Merged

jcp19 mentioned this pull request Mar 9, 2022

Whitespace-dependent bug: "Assertion unknown might not hold" viperproject/gobra#418

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow keeping SMT commands unchanged when Boogie identifiers are renamed #452

Allow keeping SMT commands unchanged when Boogie identifiers are renamed #452

keyboardDrummer commented Nov 11, 2021 •

edited by shazqadeer

Loading

MikaelMayer left a comment

shazqadeer commented Nov 11, 2021

shazqadeer commented Nov 11, 2021

shazqadeer commented Nov 11, 2021

keyboardDrummer commented Nov 12, 2021

shazqadeer commented Nov 12, 2021

keyboardDrummer commented Nov 14, 2021 •

edited

Loading

RustanLeino commented Nov 16, 2021

RustanLeino left a comment

RustanLeino Nov 16, 2021

keyboardDrummer Nov 17, 2021

RustanLeino commented Nov 17, 2021

RustanLeino commented Nov 17, 2021

shazqadeer Nov 21, 2021

keyboardDrummer Nov 22, 2021 •

edited

Loading

bkragl Nov 22, 2021

shazqadeer Nov 22, 2021

keyboardDrummer Nov 22, 2021 •

edited

Loading

Allow keeping SMT commands unchanged when Boogie identifiers are renamed #452

Allow keeping SMT commands unchanged when Boogie identifiers are renamed #452

Conversation

keyboardDrummer commented Nov 11, 2021 • edited by shazqadeer Loading

Changes

Testing

MikaelMayer left a comment

Choose a reason for hiding this comment

shazqadeer commented Nov 11, 2021

shazqadeer commented Nov 11, 2021

shazqadeer commented Nov 11, 2021

keyboardDrummer commented Nov 12, 2021

shazqadeer commented Nov 12, 2021

keyboardDrummer commented Nov 14, 2021 • edited Loading

RustanLeino commented Nov 16, 2021

RustanLeino left a comment

Choose a reason for hiding this comment

RustanLeino Nov 16, 2021

Choose a reason for hiding this comment

keyboardDrummer Nov 17, 2021

Choose a reason for hiding this comment

RustanLeino commented Nov 17, 2021

RustanLeino commented Nov 17, 2021

shazqadeer Nov 21, 2021

Choose a reason for hiding this comment

keyboardDrummer Nov 22, 2021 • edited Loading

Choose a reason for hiding this comment

bkragl Nov 22, 2021

Choose a reason for hiding this comment

shazqadeer Nov 22, 2021

Choose a reason for hiding this comment

keyboardDrummer Nov 22, 2021 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer commented Nov 11, 2021 •

edited by shazqadeer

Loading

keyboardDrummer commented Nov 14, 2021 •

edited

Loading

keyboardDrummer Nov 22, 2021 •

edited

Loading

keyboardDrummer Nov 22, 2021 •

edited

Loading