Fix inlining of type constraints #753

Dargones · 2023-06-20T01:28:55Z

This PR fixes a bug in which the where type constraint on a variable's declaration is not run through BoundVarAndReplacingOldSubstituter during inlining. Specifically, consider the case of inlining the following procedure:

procedure {:inline 1} b() returns () {
    var v:int where v > 3;
    havoc v;
}

Boogie would previously introduce a new variable into the caller declared as var inline$b$0$v: int where v > 3;, which causes resolution errors upon trying to run Boogie on that procedure, since v is not in scope. Instead, the variable should be declared as var inline$b$0$v: int where inline$b$0$v > 3;. I add this example as a new test case.

As far as I can tell, this bug does not manifest itself during verification phase but it does cause incorrect code being printed, if you use the /printInlined attribute.

This reverts commit 3d3166c.

shazqadeer · 2023-06-20T01:39:10Z

Test/inline/testWhereExpr.bpl.expect

+
+  inline$b$0$Entry:
+    havoc inline$b$0$v /* where inline$b$0$v > 3 */;
+    assume inline$b$0$v > 3;


It seems that this assume is injected automatically by the inlining implementation. Is that correct?

Yes, I think these lines are responsible for doing this. The justification for adding havoc is that the procedure might be invoked in a loop and so the values of its local variables would have to be reset on each iteration. There are FIXME comments surrounding the added assume and I think they might be technically redundant but I am not confident enough in the semantics.

shazqadeer · 2023-06-20T01:39:36Z

Test/inline/testWhereExpr.bpl.expect

+
+  inline$b$0$anon0:
+    havoc inline$b$0$v /* where inline$b$0$v > 3 */;
+    goto inline$b$0$Return;


Strange! Why is an assume not injected here?

I am not sure. My suspicion is that an assumption would be redundant both here and above but I have not fully convinced myself yet. Empirically, it seems that havoc must respect the type constraint by default, e.g. the code below verifies. I will make another PR if I figure it out.

procedure b() { var d:int where d > 3; havoc d; assert d > 3; }

Here is a conjecture.

It is indeed redundant to put the assumes after the havocs in the inlining code because some processing later on (possibly VC generation) takes care of handling the where clauses after havoc appropriately.

The bug in the inlining code you uncovered turned off the treatment above because the where clause was not appropriately substituted.

The bug was discovered by somebody who did not understand the root cause and chose to fix the problem by putting the assumes in the inlining code itself.

If my conjecture is correct, then after your fix has landed, it ought to be possible to delete the assume injection. Of course, we have to make sure that the regression tests are adequate to check the behavior. You might need to add more tests.

I can approve your PR if you are ready to land it.

Thank you, @shazqadeer! I think you are right, let me do some testing to make sure this is the case and then I can make another PR about the assume. I am ready to land this one!

rakamaric

LGTM

rakamaric

LGTM

This PR is a follow up on #753 and removes [redundant assumptions](https://github.com/boogie-org/boogie/blob/f292415255aeff4db8fb1309b92b877cefe07780/Source/Core/Inline.cs#L680-L710) emitted during inlining. The assumptions were meant to ensure the a variable abides by its associated type constraint even after a call to `havoc`. Such assumptions are not necessary, however, since `havoc` is desugared to respect the corresponding type constraint at a later point during VC Generation. [Here is the code](https://github.com/boogie-org/boogie/blob/f292415255aeff4db8fb1309b92b877cefe07780/Source/VCGeneration/ConditionGeneration.cs#L1448) that, if I am correct, is responsible for this desugaring. An additional empirical evidence that `havoc` is supposed to behave in this manner is that the following procedure verifies: ```Boogie procedure p() { var a:int where a > 0; havoc a; assert a > 0; } ``` The historical reason for why these assumptions are present in the code must be that the `where` clauses themselves were not correctly translated prior to #753, so, in particular, this PR adds a test case that would have failed prior to #753 if these redundant assumptions had been removed before fixing the translation of the where clauses. Co-authored-by: Aleksandr Fedchin <fedchina@amazon.com>

…geted (#4326) This PR changes what coverage criteria a user of test generation may target. - Path coverage: Dafny will now attempt complete path coverage of the (inlined part of the) program as oppose to covering paths through each method in isolation. As a means of dealing with path explosion, Dafny will now try generating tests for increasingly longer paths, skipping over any paths whose subpaths have been found to be infeasible. - Branch coverage: As an middle ground between path coverage and block coverage, Dafny can now attempt call-graph-sensitive version of block coverage (i.e. it tries to cover every block in the program for every path through the call graph that can lead to that block). I call this "call-graph" coverage but am not sure this is the best way to call it - would be grateful for any suggestions. This PR relies on a [recent change](boogie-org/boogie#753) in Boogie that fixes a bug in how inlined programs are printed to a file. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <fedchina@amazon.com> Co-authored-by: Aaron Tomb <aarontomb@gmail.com>

…geted (dafny-lang#4326) This PR changes what coverage criteria a user of test generation may target. - Path coverage: Dafny will now attempt complete path coverage of the (inlined part of the) program as oppose to covering paths through each method in isolation. As a means of dealing with path explosion, Dafny will now try generating tests for increasingly longer paths, skipping over any paths whose subpaths have been found to be infeasible. - Branch coverage: As an middle ground between path coverage and block coverage, Dafny can now attempt call-graph-sensitive version of block coverage (i.e. it tries to cover every block in the program for every path through the call graph that can lead to that block). I call this "call-graph" coverage but am not sure this is the best way to call it - would be grateful for any suggestions. This PR relies on a [recent change](boogie-org/boogie#753) in Boogie that fixes a bug in how inlined programs are printed to a file. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <fedchina@amazon.com> Co-authored-by: Aaron Tomb <aarontomb@gmail.com>

…geted (#4326) This PR changes what coverage criteria a user of test generation may target. - Path coverage: Dafny will now attempt complete path coverage of the (inlined part of the) program as oppose to covering paths through each method in isolation. As a means of dealing with path explosion, Dafny will now try generating tests for increasingly longer paths, skipping over any paths whose subpaths have been found to be infeasible. - Branch coverage: As an middle ground between path coverage and block coverage, Dafny can now attempt call-graph-sensitive version of block coverage (i.e. it tries to cover every block in the program for every path through the call graph that can lead to that block). I call this "call-graph" coverage but am not sure this is the best way to call it - would be grateful for any suggestions. This PR relies on a [recent change](boogie-org/boogie#753) in Boogie that fixes a bug in how inlined programs are printed to a file. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <fedchina@amazon.com> Co-authored-by: Aaron Tomb <aarontomb@gmail.com>

Aleksandr Fedchin added 5 commits June 19, 2023 17:52

Run tests

3d3166c

Introduce fix

c202c8b

Test the fix

3ca078a

Revert "Run tests"

e21309a

This reverts commit 3d3166c.

Simplify test case

67eebb5

shazqadeer reviewed Jun 20, 2023

View reviewed changes

shazqadeer previously approved these changes Jun 20, 2023

View reviewed changes

rakamaric previously approved these changes Jun 22, 2023

View reviewed changes

Dargones added 2 commits June 22, 2023 09:33

Merge branch 'master' into InliningFix

a635d36

Dummy Commit to Rerun Tests

0d31eff

Dargones dismissed stale reviews from rakamaric and shazqadeer via 0d31eff June 22, 2023 17:04

rakamaric approved these changes Jun 22, 2023

View reviewed changes

rakamaric merged commit 66e8869 into boogie-org:master Jun 22, 2023

Dargones mentioned this pull request Jul 3, 2023

Remove redundant assumptions in inlining #761

Merged

Dargones mentioned this pull request Jul 24, 2023

[Test Generation] Change the set of coverage criteria that can be targeted dafny-lang/dafny#4326

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix inlining of type constraints #753

Fix inlining of type constraints #753

Dargones commented Jun 20, 2023 •

edited by shazqadeer

Loading

shazqadeer Jun 20, 2023

Dargones Jun 20, 2023

shazqadeer Jun 20, 2023

Dargones Jun 20, 2023

shazqadeer Jun 20, 2023

Dargones Jun 20, 2023 •

edited

Loading

rakamaric left a comment

rakamaric left a comment

Fix inlining of type constraints #753

Fix inlining of type constraints #753

Conversation

Dargones commented Jun 20, 2023 • edited by shazqadeer Loading

shazqadeer Jun 20, 2023

Choose a reason for hiding this comment

Dargones Jun 20, 2023

Choose a reason for hiding this comment

shazqadeer Jun 20, 2023

Choose a reason for hiding this comment

Dargones Jun 20, 2023

Choose a reason for hiding this comment

shazqadeer Jun 20, 2023

Choose a reason for hiding this comment

Dargones Jun 20, 2023 • edited Loading

Choose a reason for hiding this comment

rakamaric left a comment

Choose a reason for hiding this comment

rakamaric left a comment

Choose a reason for hiding this comment

Dargones commented Jun 20, 2023 •

edited by shazqadeer

Loading

Dargones Jun 20, 2023 •

edited

Loading