Flatten macro expansions

[viper-admin]

Created by @fabiopakk on 2019-07-02 11:17
Last updated on 2019-07-10 11:33

Whenever a macro is expanded in the body of a method, a new Seqn node (AST) is generally created as a placeholder for all statements from the macro. As a result the body of the method is a Seqn containing another Seqn. Worse, in cases of multiply nested macro expansions as in nestedBlocks.sil (in attachment), we can have multiple layers of Seqn composed of Seqn.

A side effect of such nesting can be seen in the transformation framework, particularly when neighbor nodes are used as a context for detecting when to rewrite a statement. For an example, refer to ManyToOneAssert test case in RewriterTest.scala.

Currently, the AST is left as is after nested macro expansions and it is the job of the rewriter framework to tackle nested statements and linearize them prior to rewriting.

This should be reverted: the rewriter framework should be agnostic to macro expansions that might have taken place previously. And the macro expansion should deliver a linearized sequence of statements (Seqn) without unnecessary nesting.

---

Attachments:

• nestedBlocks.sil

[viper-admin]

@mschwerhoff commented on 2019-07-02 11:32

Quick note: Since front-ends can create arbitrary ASTs, the transformation framework must still be able to handle nested Seqn nodes, regardless of how macro expansion is implemented.

[viper-admin]

@fpoli commented on 2019-07-02 11:38

I confirm that in Prusti we generate nested Seqn nodes; it's quite convenient for us.

[viper-admin]

@mschwerhoff commented on 2019-07-02 11:40

Voila generates nested Seqn as well.

[viper-admin]

@fabiopakk commented on 2019-07-03 07:03

It is not a problem to generate nested Seqn, as long as they are equivalent to their flattened versions.

The issue is that the transformation framework has a cumbersome code just to make the context’s successors and predecessors work, when in presence of nested Seqn. One has to decide if successors, for example, mean a nested Seqn or the statements in its flattened version.

However, the scope of this task is macro expansion. But it can easily be adopted for every situation. Would you see any consequences in flattening all nested Seqn prior to any processing? This could be done in another task.

[viper-admin]

@mschwerhoff commented on 2019-07-04 10:09

Flattening Seqn by default might surprise users. Using nested Seqn can be convenient for front-end developers, e.g. to structure the AST they create. If they create an AST val ast = Seqn(Seqn(...), Seqn(...)), then replace all variables x instead ast with some y and then pattern-match on the AST via val Seqn(left, right) = ast, they’ll most likely won’t expect a pattern match failure.

In my opinion, flattening is an AST optimisation, and as such should be explicitly performed by users, not automatically for technical reasons.

[viper-admin]

@fabiopakk commented on 2019-07-08 14:20

I see. I’ll deploy the solution to this issue (limited to the scope of macro expansions). And then lets check if there’s any interference with the frontends. The effects should be perpendicular.

[viper-admin]

@fabiopakk commented on 2019-07-10 11:32

Indeed, this example is what is described in the description of this issue, only the other way around. So this discussion is very good, since the issue seems to make sense particularly after macro expansions but not generally. So I’ll make sure it is restricted.

[viper-admin]

@fabiopakk commented on 2019-07-10 11:33

Issue fixed in branch fabiopakk_issue_279_flatten_macro_expansions, already merged into default branch.

[viper-admin]

@fabiopakk on 2019-07-10 11:33:

• changed state from new to resolved