Clarify the semantics of AST-to-CFG transformation and how to handle irreducible CFGs

[viper-admin]

Created by @gauravpartha on 2019-07-15 08:14 Last updated on 2019-07-23 13:05

Consider the following example

method minimal()
{
  goto loopHead

  while(true) {
    label loopHead
    invariant true 
    assert false /*unexpected: verifies currently*/
  }
}

The loop head is at the label on line 9. Silicon currently verifies “false” on line 11 which should not be the case, since line 11 can clearly be reached. An extended version of the program which contains traces after the loop is given by

method extended_after_loop(n: Int) 
{
  var i:Int := 0

  goto loopHead

  while(i < n) {
    i := i+1
    label loopHead
    invariant true
    assert false /*unexpected: verifies currently*/
  }

  assert false /*unexpected: verifies currently*/
}

Here “false” is also verified on line 14 after the loop, even though line 14 can be reached.

When one encodes the while loop using gotos, then the issue does not arise:

method loop_label(n:Int) 
{
  var i:Int := 0
  goto loopHead

  label cond
  if(i >= n) {
    goto exit
  }

  i := i+1
  label loopHead
  invariant true
  assert false /* expected: does not verify */
  goto cond

  label exit
  assert false
}

---

Attachments:

• goto_while_loop_issue_392.vpr

[viper-admin]

@gauravpartha on 2019-07-15 08:15:

• changed attachment from (none) to goto_while_loop_issue_392.vpr

[viper-admin]

@gauravpartha on 2019-07-15 08:16:

• changed attachment from (none) to goto_while_loop_issue_392.vpr
• edited the description

[viper-admin]

@mschwerhoff commented on 2019-07-15 08:28

Jumping into a loop results in a irreducible CFG, which isn’t supported. The program should be rejected by Viper. If you agree that the CFG is irreducible, please close the issue as “invalid” and file a corresponding Silver issue (if non already exists).

[viper-admin]

@gauravpartha commented on 2019-07-15 08:34

In my opinion this is a reducible CFG (correct me if I am wrong). The node at label loopHead dominates the backedge from i := i+1 to label loopHead. I think as long as there is a single entry point to the loop, then the CFG is still reducible. In this case the unique entry point is at label loopHead. My phrasing "jumping into the loop" is not ideal, because here one actually does not jump into the loop because the loop starts at label loopHead, but one jumps into the syntactic construct that defines the while loop.

[viper-admin]

@alexanderjsummers commented on 2019-07-15 08:42

Is it possible to check the cfg which is actually generated (and that it is indeed reducible)? Whether this is the case or not seems to depend on whether the AST to CFG transformation treats blocks containing a manual goto specially (avoiding introducing an edge from the end of the block, in such cases). Is that the case?

We should also document this design at some point, since it will be part of what is allowed in Viper (do we have anything about gotos/cfgs in the tutorial?)

[viper-admin]

Bitbucket user Fedux commented on 2019-07-15 08:47

Silicon has a --printMethodCFGscommand line flag that can be used to dump the CFG as a .dot file in the viper tmp folder.

[viper-admin]

@gauravpartha commented on 2019-07-15 09:22

Thanks for the information. I used --printMethodCFGs and this is the output. The minimal method has CFG

‌

This is strange, because there are no loops at all. So, I guess this is a Silver issue @mschwerhoff ? If so, then I would close this issue and create a Silver issue. Although it’s not clear to me why this CFG leads to “assert false” going through.

For completeness sake, here are the CFGs for extended_after_loop (which is again not of the expected shape) and only_labels:

‌

‌

The version which does not use while loops (only_labels) at all contains the CFG which I expect and I would say it is reducible (Silicon handles it correctly).

[viper-admin]

@alexanderjsummers commented on 2019-07-15 09:39

Hi Gaurav,

Thanks for the extra information - that’s very useful. I wonder whether there could be an issue with the CFG visualisation itself, in the case of an unexpected (perhaps irreducible) CFG. It certainly seems surprising that the first CFG would be the result of the program you explained. There is definitely at least a Silver issue there - do please file it. Maybe we can keep this one on hold for now, and link them?

Is there a more raw (less pretty) way to dump the CFG, e.g. as text, to compare? Maybe we should add that to Viper eventually.

[viper-admin]

@mschwerhoff commented on 2019-07-15 10:38

@gauravpartha Maybe there’s no loop in the CFG generated for minimal because the AST-to-CFG code cannot handle such a case, but instead of rejecting the program it computes a wrong result. Did you already ask Jerome about that?

[viper-admin]

@dohrau commented on 2019-07-15 11:37

The AST-to-CFG transformation should be able to handle any kind of code with GOTOs. There is probably a bug in the transformation. I can have a look.

[viper-admin]

@mschwerhoff on 2019-07-23 13:05:

• changed kind from bug to task
• edited the title