Don't warn about unresolved expressions in functions if they are unreachable/dead code

[viper-admin]

Created by @marcoeilers on 2016-12-13 21:26 Last updated on 2018-08-26 09:54

For functions containing unreachable expressions, like the following:

function f(): Int
{ (true ? f1() : f2()) }
   
function f1(): Int
function f2(): Int

Silicon warns that it could not resolve f2() ([email protected]) during the axiomatisation of function f, which makes it seem as if there is a problem to the user, even though there isn't.

In cases like this, Silicon should remember that some code is unreachable and not emit the warning.

[viper-admin]

@mschwerhoff on 2017-03-17 10:14:

• changed component from (none) to Logging, Reporting, IDE

[viper-admin]

@mschwerhoff commented on 2018-08-22 16:24

Duplicate of https://github.com/viperproject/silicon/issues/352.

[viper-admin]

@mschwerhoff on 2018-08-22 16:24:

• changed state from new to duplicate

[viper-admin]

@mschwerhoff commented on 2018-08-25 10:06

Reopened this issue, since emitting the warning ("Could not resolve ...") in cases where the unsolved expression is on an infeasible is still potentially confusing.

[viper-admin]

@mschwerhoff on 2018-08-25 10:06:

• changed state from duplicate to open

[viper-admin]

@mschwerhoff commented on 2018-08-25 11:12

The warning has been changed to be more helpful:

Could not resolve expression f2() ([email protected]) during the axiomatisation of function f. 
This typically happens if the expression is on an infeasible path, i.e. is dead code. 
The unresolved expression will be replaced by a fresh symbol, i.e. an arbitrary value.

That is still not ideal, however: if an expression is unreachable, Silicon should at most emit a warning explicitly stating that there is dead code (or not emit a warning at all).

This is not easy, however, due to how the Viper AST is currently implemented. Consider the Viper expression

b ? f1() : (b ? f1() : f2())

where the second (or inner-most) application f1() is unreachable. A straight-forward approach would be the following:

1. In Silicon's first phase of function axiomatisation — in which Silicon symbolically explores the function body and records which hap-dependent expression has which snapshot — record (e.g. in a set) which expressions Silicon actually reached.

2. In the second phase — in which Silicon translates the function body into an axiom while replacing heap-dependent expressions with previously recorded snapshots — the previously recorded reachability information could be used to decide when to emit a "resolution failure" and when to omit it (the failure is meant to indicate that no snapshot was recorded for a particular heap-dependent expression, which could indicate a bug in Silicon).

The problem is that both applications of f1() are equal in the sense of AST node equality because the nodes have no unique ID and because positional information is not considered when determining equality (see also Silver issue #94. Since positional information, or any other meta data, is optional, it can also not reliably be included in equality checks at use-site, e.g. by recording reached expressions in a set of pairs <expression, position>. Identity (reference equality) could theoretically be used, but would practically quickly fail to work since we routinely duplicate AST nodes, e.g. during AST transformations.

Contextual information, e.g. under which conditionals an expression is nested, or how deeply nested it is (for a suitable definition of depth), could be used, but this would require not only more bookkeeping, but also threading such contextual information through Silicon.

[viper-admin]

@mschwerhoff on 2018-08-25 11:12:

• changed kind from bug to enhancement
• edited the title
• edited the description

[viper-admin]

@mschwerhoff commented on 2018-08-26 09:54

Silver issue #245 is an enhancement request for being able to conveniently and reliably identify AST nodes.

[fpoli]

I observe that this message is printed to stdout. Is there a way to avoid that? It pollutes Prusti's output.

[mschwerhoff]

Since the message is a logger warning, you could set Silicon's log level to error (--logLevel ERROR), which should suppress any message of lower severity.

[fpoli]

Since the message is a logger warning, you could set Silicon's log level to error (--logLevel ERROR), which should suppress any message of lower severity.

Thanks!