Redundant arguments in constructor of FuncApp class

[viper-admin]

Created by @fpoli on 2018-07-23 14:25
Last updated on 2019-05-14 08:55

When building a function application, the FuncApp class requires:

• the name of the function,
• the expression of the arguments,
• the return type of the function, and
• the formal arguments of the function's declaration.

The first two arguments make sense, but the last two look like a duplication of the declaration of the function. Isn't something that should already be accessible in the program with a lookup on the function name?

For comparison, the MethodCall class does not require to specify the formal arguments or formal returns of the method's declaration, but just:

• the name of the method,
• the expression of the arguments, and
• the target variables that go on the lhs of the assignment.

[viper-admin]

@alexanderjsummers on 2018-10-15 15:36:

• changed the assignee from (none) to @fpoli

[viper-admin]

@fpoli commented on 2019-05-03 15:06

I thought a bit more about this. The proper consistency check for the FuncAppAST node should lookup by name the function from the verified program, and check the type of the expressions of the arguments against it, not against the formal arguments provided in the constructor.

For example, the current checks can not detect inconsistencies if a frontend builds FuncApp using the wrong return type or formal arguments with the wrong type. The same goes for DomainFuncApp.

My proposal is to turn checkand checkTransitivelyinto methods, with a Program parameter. This way the checks can lookup and use the definition of functions, domains and so on.

Any strong opinion about this? Does this work against any other implementation plan that I am not aware of?

[viper-admin]

@mschwerhoff commented on 2019-05-03 15:11

@fpoli I'm not sure the additional argument is necessary (it would also look odd for Program.check/checkTransitively, and it would make it possible to pass the wrong program). As you mentioned, some checks, in particular those that reference symbols (variables, functions, predicates, ...) from a surrounding scope, require "looking up". However, instead of doing that, such checks can be made at the top, i.e. when callin `Program.check. Isn’t that currently done already (but maybe not for function applications)?

[viper-admin]

@fpoli commented on 2019-05-03 15:49

I see. I'll check how to do the checks at the top. If such checks are already done in Program I can remove them from FuncApp

[viper-admin]

@fabiopakk commented on 2019-05-14 08:55

I guess checkTransitively is the right place to do such check. However, after producing the Parse AST, there’s a semantic check which currently is performing name and type check. I’m not sure if they test for such type compatibility between a method/function definition and their respective call, but I suppose so. Which brings the question: why do we have a P_AST → AST translation? Maybe this question is not completely related with the present issue, since frontends produce an AST directly, but that seems to be repeated code. In a sense checkTransitively is doing what’s already been done in semantic analysis (when not skipped by giving an AST directly). As the question of why P_AST → AST is a deeper one, I suggest that, if possible, produce a code that can work with both Parse AST and AST. For example, some of the strategies for rewriting trees accepts both PNodes and Node. But that’s just a suggestion and it is up to you to evaluate whether it is worth the effort.