Idea : Connecting up producers and consumers of knowledge about termination

[martin-cs]

1. There are various things we do that can be improved by having even crude information about loop and function termination and non-termination.

2. For example, I think that slicing can be improved with a small amount of information about termination so that irrelevant loops and functions can be removed. This can also remove control dependencies on loop control variables. In the past when I have used slicing this was one of the key limitations. @marek-trtik and @lucasccordeiro might care.

3. Another example, in goto-analyze, we can only show that an assertion is false "if reachable", termination and non-termination can give us a crude reachability analysis which may be enough to give a definitive false in some cases. @danpoe and @thk123 might care.

4. Various people have termination and non-termination analyses of varying weights in various branches. I know @cristina-david and @pkesseli have some very cool things. I know @peterschrammel and @steffan711 are building something. I know @danpoe has built a loop bound computation in goto-analyze. I wouldn't be surprised if @tautschnig has something up his sleeve.

5. Could we provide an API for accessing / using this information:

loop_id -> TERMINATE & NON_TERMINATE & UNKNOWN
function_name -> TERMINATE & NON_TERMINATE & UNKNOWN

(i.e. a bit-wise combination of which cases are possible)

with a trivial default implementation (for loops, check if the guard is false, for functions check all loops) and then have a task to connect up more sophisticated analyses as they are merge-able / in branches that they exist?

What do people think?

[mgudemann]

I think it's a good idea.

Not sure if that counts, but we have --java-unwind-enum-static in CBMC/Java which unrolls any loop it finds in the static initalization context of Java enumerations. The unwind parameter k is exactly the number of elements in the enumeration. The reasoning is that as there's no input parameter to <clinit>, the unwinding that makes most sense is k.

This is a heuristic, but could be worth a try to assume <clinit> loops to terminate in presence of the above option. In particular as enums with user-defined static init are often used in the Java benchmarks we have looked at.

[martin-cs]

1. The unwind analysis in goto-analyze should be able to do this soundly. 2. Maybe the interface should be extended to also return a bound on the number of iterations if it returns TERMINATE | !NON_TERMINATE | !UNKNOWN

[tautschnig]

Couldn't we use custom_bit_vector_domaint for this purpose?

[martin-cs]

On Thu, 2017-03-09 at 07:17 -0800, Michael Tautschnig wrote: Couldn't we use custom_bit_vector_domaint for this purpose?

There are many ways of implementing the API and many ways of using it. I don't think we should restrict ourselves to just one implementation; hence suggesting an interface of some kind.

[martin-cs]

There seem to actually be several bits of information this interface could give (per function / loop):

1. Condition for traces guaranteed to terminate : true == all, false == none known
2. Conditions for traces guaranteed to non-terminate : true == all, false == none known
3. Upper and lower bounds on iterations (exact if equal).

If the static unwinder and symex can be optionally aware of this interface then we can switch no information, hints from the language, info from a full analysis, etc. depending on what is needed.

(@smowton and @peterschrammel possibly @mgu ).

[TGWDB]

Closing due to detail in #6284