Chopper

[Felalolf]

Adds the chop function, which splits an input Viper program into several Viper programs.

[Felalolf]

@mschwerhoff I do not know who usually reviews silver PRs, so for now I just added you as a reviewer.

[Aurel300]

@Felalolf @mschwerhoff What is the status of this? Can this make it for the July release?

[mschwerhoff]

I don't have time for a thorough review, but stumbled over a few things:

• The formatting of method and class signatures doesn't seem consistent, if it spans multiple lines: indentation, and whether or not the opening/closing parentheses are on the same line as the first/last parameter
• I saw what looked like a depth-first search, and we already have

  silver/src/main/scala/viper/silver/cfg/utility/Dominators.scala

  Line 85 in 6428d2d

  def dfs(block: Block[S, E], index: Int = 0): Int = {

  . Maybe factor out an unify?
• I saw what looked like a stronges connected component algorithm, and we already have a library for that -

  silver/build.sbt

  Line 53 in 6428d2d

  libraryDependencies += "org.jgrapht" % "jgrapht-core" % "1.5.0", // Graphs

  - which is used to identify SCCs in function call graphs. Would be nice to reuse the former.
• I didn't see any high-level description of the chopper. Would be great to have more documentation, to avoid creating another "type checker & resolver" that nobody except Uri understands ... who left a while ago.

However, if the majority feels adding the chopper to the next release is important, I won't object.

[Felalolf]

@mschwerhoff I tried to make the formatting more consistent. Furthermore, I added a high-level description of the chopper. I do not think that I can just use the existing DFS algorithm because the chopper always computes additional information on top of the dfs traversal order. The strongly connected component algorithm can probably be replaced. However, I would first want to evaluate performance differences since my implementation should be rather optimized as it exploits details of the specific domain. Furthermore, such a refactoring would require quite some time that I do not have available right now.

[marcoeilers]

LGTM, just added some comments/questions about the documentation.