Verification fails with java.util.NoSuchElementException: head of empty list

[viper-admin]

Created by @fpoli on 2018-05-31 16:31 Last updated on 2019-07-29 14:43

The attached program passes the consistency checks, but causes a java.util.NoSuchElementException: head of empty list during the verification.

Part of the stacktrace:

java.util.NoSuchElementException: head of empty list
	at scala.collection.immutable.Nil$.head(List.scala:420)
	at scala.collection.immutable.Nil$.head(List.scala:417)
	at viper.silicon.rules.executor$.viper$silicon$rules$executor$$follow(Executor.scala:54)
	at viper.silicon.rules.executor$$anonfun$viper$silicon$rules$executor$$follows$1.apply(Executor.scala:89)
	at viper.silicon.rules.executor$$anonfun$viper$silicon$rules$executor$$follows$1.apply(Executor.scala:87)
	at scala.collection.LinearSeqOptimized$class.foldLeft(LinearSeqOptimized.scala:124)
	at scala.collection.immutable.List.foldLeft(List.scala:84)
	at viper.silicon.rules.executor$.viper$silicon$rules$executor$$follows(Executor.scala:87)
	at viper.silicon.rules.executor$$anonfun$exec$1.apply(Executor.scala:107)
	at viper.silicon.rules.executor$$anonfun$exec$1.apply(Executor.scala:106)
	at viper.silicon.rules.executor$.execs(Executor.scala:206)
	at viper.silicon.rules.executor$$anonfun$execs$1.apply(Executor.scala:204)
	at viper.silicon.rules.executor$$anonfun$execs$1.apply(Executor.scala:203)
	at viper.silicon.rules.executor$$anonfun$exec$7.apply(Executor.scala:214)
	at viper.silicon.rules.executor$$anonfun$exec$7.apply(Executor.scala:212)
	at viper.silicon.rules.executor$$anonfun$5.apply(Executor.scala:223)
	at viper.silicon.rules.executor$$anonfun$5.apply(Executor.scala:222)
	at viper.silicon.rules.executor$$anonfun$6.apply(Executor.scala:253)
	at viper.silicon.rules.executor$$anonfun$6.apply(Executor.scala:251)
        ...

Silicon build that I'm using: Silicon version 1.1-SNAPSHOT <https://github.com/viperproject/silicon/commit/aa2bfca33b4181126d0626cf4809d8d5ce40d76a> default 2018/05/30 01:48:53

---

Attachments:

• program.vpr
• check.dot.pdf

[viper-admin]

@fpoli on 2018-05-31 16:34:

• changed attachment from (none) to program.vpr

[viper-admin]

@fpoli commented on 2018-05-31 16:35

I'll try minimizing the program

[viper-admin]

@mschwerhoff commented on 2018-06-01 07:29

That would be great! It currently looks somewhat ... insane ;-)

[viper-admin]

@fpoli commented on 2018-06-01 09:30

It was fun :D Here is the minimized program:

method check(b: Bool)
{
  if (b) {
    goto bb6
  }
  assume false
  
  label bb1
  assume false
  
  label bb6
  goto bb1
}

[viper-admin]

@fpoli commented on 2018-06-01 09:34

Here is another version, full of assume false:

method check(b: Bool)
{
  if (b) {
    assume false
    goto bb6
  }
  assume false
  
  label bb1
  assume false
  
  label bb6
  assume false
  goto bb1
}

[viper-admin]

@mschwerhoff commented on 2018-06-01 20:49

That's quite the simplification :-) Thanks a lot!

[viper-admin]

@mschwerhoff commented on 2019-03-02 21:45

@fpoli I've attached the CFG generated for the first simplification. The exception happens when Silicon leaves StatementBlock(1) via the b (out) edge: since it is labelled as an edge going out of a loop, Silicon tries to merge the invariant context, i.e. the part of the state framed around a loop, back in. However, since Silicon did not previously traverse an in-edge, no such context exists.

@dohrau This looks like a bug in the CFG generation code. Can you please have a look?

[viper-admin]

@mschwerhoff on 2019-03-02 21:45:

• changed attachment from (none) to check.dot.pdf

[viper-admin]

@dohrau commented on 2019-03-03 17:08

Will do!

[viper-admin]

@dohrau on 2019-07-29 14:43:

• changed the assignee from (none) to @dohrau

[mschwerhoff]

@dohrau Any progress on this?