Chopper: More fine grained dependency analysis for domain axioms

[Felalolf]

This PR makes two changes to the chopper that I explain below:

Changes the dependency analysis for domain axioms

The PR changes how dependencies for domain axioms are defined. Before, for an axiom A, we added dependencies from all uses in A to A and from A to all uses in A. These dependencies have two issues:

1) If the uses of A include the domain that A is defined in, then A and all its uses are always included when the domain is included. 2) A is always included if any expression in A is required, even if that expression is guarded by a trigger that is not included, i.e. never triggered.

The PR does the following changes:

1) Dependencies that have A's domain as source are removed from axiom dependencies. 2) As before, the axiom has a dependency to all uses in its body. Conversely, all uses outside of quantified expressions and uses in triggers have a dependency to the axiom.

Consider the following domain:

domain D {
  func foo(x: Int): Int
  func bar(x: Int): Int
  func baz(x: Int): Int
  axiom A { forall x: Int :: {bar(x)} bar(x) > baz(x) }
}

Previously, the dependencies were (omitting dependencies to D): A -> bar, A -> baz, bar -> A, baz -> A With the PR the dependencies are instead: A -> bar, A -> baz, bar -> A

Makes the chopper extendable

In short, the PR changes all objects to traits. To avoid polluting the namespace, I moved the chopper into a separate package.

Changes to the code

Unfortunately, Github does not recognize that the new Chopper file is based on the previous one. Below, I give a list of all code changes without changes to signatures (to replace objects with traits):

1) I introduce a Edges.directUsages method. The method is a non-transitive version of Edges.usages. 2) I changed the ast.Domain case of the Edges.dependencies method. This case implements the change to the logic as described above.

[marcoeilers]

I have a question about the axiom dependencies based on triggers: If an axiom has any trigger that does not require a specific domain function to be used, then... what are the dependencies? E.g. in your example axiom A { forall x: Int :: {bar(x)} { Seq(x) } bar(x) > baz(x) }

[Felalolf]

@marcoeilers I assume you meant the axiom axiom A { forall x: Int :: { Seq(x) } bar(x) > baz(x) }. At the time of your review, the dependencies would have been A -> bar, A -> baz and indeed the axiom would have never been included in the final Viper program. I changed the logic such that all usages occurring in a quantified expression are included if there is no use in one trigger. With my change, the dependencies for the example are A -> bar, A -> baz, bar -> A, baz -> A.

For the axiom axiom A { forall x: Int :: {bar(x) }{ Seq(x) } bar(x) > baz(x) } the dependencies were A -> bar, A -> baz, bar -> A before my change and are now A -> bar, A -> baz, bar -> A, baz -> A.