Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands #952

keyboardDrummer · 2024-09-24T14:34:25Z

Changes

Introduce the {:isolate} attribute on AssertCmd and ReturnCmd
Introduce the {:isolate "paths"} attribute on AssertCmd and ReturnCmd
Introduce new tokens that allow precisely describing where a particular Split comes from.
Fix a bug that caused too many VCs to be created when using /vcsSplitOnEveryAssert together with focus
Fix incorrect token bug for VCs originating from focus.

Testing

Created a folder Test/implementationDivision that has tests for {:isolate}, {:isolate "paths"}, {:focus} and {:split_here}

…est work

MikaelMayer

Here are my initial comments. It's nice to see isolate assertions, it's going to be useful.

MikaelMayer · 2024-10-04T14:51:40Z

Source/Core/AST/CallCmd.cs

@@ -882,7 +882,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)

          // Do this after copying the attributes so it doesn't get overwritten
          if (callId is not null) {
-            a.CopyIdWithModificationsFrom(tok, req,
+            (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,


Is this coercion necessary? I seems that AssertCmd always implement this interface, right?

Refactoring from a previous PR that through a git error was reverted in this PR.

That issue happened to me in the past as well 😖

Source/Core/VariableDependenceAnalyser.cs

Source/Directory.Build.props

Source/ExecutionEngine/VerificationTask.cs

Source/Graph/Graph.cs

MikaelMayer · 2024-10-04T15:18:08Z

Source/VCGeneration/Splits/SplitAttributeHandler.cs

+
+namespace VCGeneration;
+
+class SplitAttributeHandler {


Is this file only refactored from somewhere else?

It's part of the old ManualSplitFinder.cs, but it's changed quite a bit.

Source/VCGeneration/VerificationConditionGenerator.cs

MikaelMayer · 2024-10-04T15:23:18Z

Source/VCGeneration/VerificationConditionGenerator.cs

@@ -1445,7 +1430,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options
          {
            Contract.Assert(block != null);
            Contract.Assume(block.TransferCmd != null);
-            returnCmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd);
+            returnCmd = block.TransferCmd.tok is GotoFromReturn gotoFromReturn ? gotoFromReturn.Origin : null;


I now see how you encode meta-data in tokens.
I had launched a discussion about the design of having different tokens vs. flattened tokens here:
dafny-lang/dafny#3354
It all boils down to deciding if you want to encode multiple information using wrapped tokens, where each token provides more information. If that is the case, then a flat token containing everything is more maintainable.
If the cases are truly disjoint, then a hierarchy of tokens is the way to go.
In the light of that, are your new tokens wrapper nestable or not?

IMO the name Token should be reserved for lexical tokens, so data that only describes a source location and a word. However, I think for error reporting purposes, it is useful to track what the origin of nodes in the AST is, that origin might be ParsedFromSource(IToken token) : IOrigin, but it can also be something related to a program transformation. In this case, the origin of the goto jump is the desugaring transformation of a return jump.

I think in the future I would prefer to rename IToken to IOrigin.

Agreed that IToken can be renamed to IOrigin, so that the token part is a sub-part of it, concerns only the lexical token, and not every metadata we don't know otherwise where to store.

In the meantime, if there is a token wrapper, I suggest there is at most one such wrapper that will contain any possible information about the origin. Is it what you did? Or are there at least two token wrapper classes?

Is it what you did? Or are there at least two token wrapper classes?

I think so, if I understand you correctly. Every AST node only has a single origin related field, whether that is a Token or a TokenWrapper.

Source/VCGeneration/VerificationRunResult.cs

MikaelMayer · 2024-10-04T15:24:51Z

Test/civl/regression-tests/non-interference-2.bpl.expect

@@ -2,10 +2,8 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
    non-interference-2.bpl(7,3): anon0
    non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L


I get that (0, 0) is not useful, but what about the label on the right? It looked useful.

Yeah.. that name is still in the codebase, but someone needs to assign a proper token to the generated node that has that name before it will show up in the execution trace. I can't really judge what the civl code is doing and what tokens should be where.

I can pass in a variant of Token.NoToken, and then it would show this exact message again. I'm not sure it's an improvement though. I'd rather leave this as is.

Where is the message stored? If it's not in the token, we should display it without token information. If it was in the token, and is lost because of the new encoding, I'd recommend to revert that change.
I worry about breaking Civi users who relied on the last line being printed.

Okay, I've made it so that nothing changes in the civl tests.

Co-authored-by: Mikaël Mayer <[email protected]>

… isolatePaths

…r assert and return commands (boogie-org#952)" This reverts commit 25160fa.

shazqadeer · 2024-10-22T14:34:54Z

@keyboardDrummer : Thank you for your continued contributions to Boogie. I am adding a late comment to this PR.

I notice that this PR adds a few more attributes related to VC splitting. Perhaps, the Dafny team has added other related attributes in the past also. Could you please make sure that all added attributes are documented in CommandLineOptions.cs? Thanks.

keyboardDrummer · 2024-10-23T13:26:13Z

@keyboardDrummer : Thank you for your continued contributions to Boogie. I am adding a late comment to this PR.

I notice that this PR adds a few more attributes related to VC splitting. Perhaps, the Dafny team has added other related attributes in the past also. Could you please make sure that all added attributes are documented in CommandLineOptions.cs? Thanks.

I've added some small documentation in #970

keyboardDrummer added 22 commits September 24, 2024 15:06

IsolatePaths option seems to work, although it still duplicates errors

576e153

Refactoring

8d0bee6

Finish test and some more refactoring

0465e6e

Refactoring

b451f9f

Refactoring

b016f40

Update version number

0fa1817

Tweaks

4755839

Improve implementation and add tests

23f44ed

More efficient assumed block generation

64b1010

Improvements to splitting, but still need check command to make the t…

bccf0b1

…est work

Some changes

7d5b58f

Remove isolatePaths code

a2f1f76

Add path tokens

9620a3f

Refactoring

c5f13f0

Rename

409cdb8

Refactoring

d4d5db6

Upgrade token

627b42c

Fixes

b6e6dab

Introduce ImplementationPartToken

d08537e

Rename

b46af73

Refactoring

6718564

Refactoring

23a0942

keyboardDrummer changed the title ~~Introduce /isolatePaths option and {:isolate_paths} attribute~~ Improvements to {:focus} Sep 27, 2024

keyboardDrummer marked this pull request as draft September 27, 2024 21:54

keyboardDrummer added 6 commits September 27, 2024 23:59

Fix warnings

2404e95

Draft for isolated assertion

d847412

More progress on the {:isolate} attribute

dea7493

Move some code into DesugarReturns

cf450a1

Work on supporting isolate for return commands

6c8ccaf

Refactoring

5bbe971

keyboardDrummer added 9 commits October 2, 2024 16:43

Fixes

064b44a

Test file fixes

a7ce5e0

Fixes

9a27654

Update tests

43d6824

Fix path isolation error reporting

1a5ff89

Refactoring

be86f19

Refactoring

d91787c

Remove TODO

2e8c8e4

Refactoring

91c304d

keyboardDrummer marked this pull request as ready for review October 3, 2024 10:09

keyboardDrummer added 2 commits October 3, 2024 12:32

Remove TODO

ff1442a

Cleanup

c603cc8

keyboardDrummer added a commit that referenced this pull request Oct 3, 2024

Extract refactorings from #952 (#957)

9a8ce8d

Merge commit '9a8ce8d4c4c' into isolatePaths

e3a6d66

keyboardDrummer force-pushed the isolatePaths branch 2 times, most recently from 0eb1327 to e3a6d66 Compare October 4, 2024 14:52

MikaelMayer reviewed Oct 4, 2024

View reviewed changes

keyboardDrummer and others added 3 commits October 4, 2024 17:32

Update Source/Directory.Build.props

d09374c

Co-authored-by: Mikaël Mayer <[email protected]>

Refactorings

7db5dee

Merge branch 'isolatePaths' of github.com:keyboardDrummer/boogie into…

8ea0f08

… isolatePaths

keyboardDrummer enabled auto-merge (squash) October 4, 2024 16:45

Undo civl test changes

6bff2ff

MikaelMayer approved these changes Oct 7, 2024

View reviewed changes

keyboardDrummer merged commit 25160fa into boogie-org:master Oct 7, 2024
5 checks passed

keyboardDrummer deleted the isolatePaths branch October 7, 2024 11:00

keyboardDrummer restored the isolatePaths branch October 8, 2024 09:29

fabiomadge added a commit to fabiomadge/boogie that referenced this pull request Oct 15, 2024

Revert "Introduce {:isolate} and {:isolate "paths"} attributes fo…

2eb33e2

…r assert and return commands (boogie-org#952)" This reverts commit 25160fa.

keyboardDrummer deleted the isolatePaths branch October 23, 2024 13:22

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands #952

Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands #952

keyboardDrummer commented Sep 24, 2024 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Oct 4, 2024

keyboardDrummer Oct 4, 2024

MikaelMayer Oct 4, 2024

MikaelMayer Oct 4, 2024

keyboardDrummer Oct 4, 2024

MikaelMayer Oct 4, 2024

keyboardDrummer Oct 4, 2024 •

edited

Loading

MikaelMayer Oct 4, 2024

keyboardDrummer Oct 5, 2024

MikaelMayer Oct 4, 2024

keyboardDrummer Oct 4, 2024 •

edited

Loading

MikaelMayer Oct 4, 2024

keyboardDrummer Oct 7, 2024

shazqadeer commented Oct 22, 2024

keyboardDrummer commented Oct 23, 2024


		namespace VCGeneration;

		class SplitAttributeHandler {

Introduce {:isolate} and {:isolate "paths"} attributes for assert and return commands #952

Introduce {:isolate} and {:isolate "paths"} attributes for assert and return commands #952

Conversation

keyboardDrummer commented Sep 24, 2024 • edited Loading

Changes

Testing

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 4, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 4, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shazqadeer commented Oct 22, 2024

keyboardDrummer commented Oct 23, 2024

Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands #952

Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands #952

keyboardDrummer commented Sep 24, 2024 •

edited

Loading

keyboardDrummer Oct 4, 2024 •

edited

Loading

keyboardDrummer Oct 4, 2024 •

edited

Loading