General

This site provides supporting material for the paper Loop Detection by Logically Constrained Term Rewriting by Naoki Nishida and Sarah Winkler, submitted to VSTTE 2018.

Abstract. Logically constrained rewrite systems constitute a very general rewriting formalism that can capture simplification processes in various domains as well as computation in imperative programs. In both of these contexts, nontermination is a critical source of errors. We present new criteria to find loops in logically constrained rewrite systems which are implemented in the tool Ctrl. We illustrate the usefulness of these criteria in three example applications: to find loops of LLVM peephole optimizations, to detect looping program executions of C programs, and to establish nontermination of integer transition systems.

Examples

The following input files for Ctrl correspond to examples mentioned in the paper:

• Instcombine simplifications: alive_loops.ctrs, shift.ctrs, andorxor.ctrs, select.ctrs, addsub.ctrs, muldivrem.ctrs
• integer rewrite systems: Velroyen08-alternKonv.jar-obl-8.ctrs, alternKonv.ctrs
• C programs: bsearch.ctrs

Tool

The new version of Ctrl with loop support is on github. (For the original version of the tool by Cynthia Kop, check out this website.)

The code can be compiled via make (please see the README file for details). Then Ctrl is simply invoked by
./ctrl input.ctrs
Following the conventions of the termination competition, it will output NO if a loop was found, hence termination was refuted. If this is the case, it will moreover show one loop to justify its answer. The dependency graph decomposition is output as well. In order to see all loops, the --debug option can be used.