Verifying the termination of programs with value analysis option -obviously-terminates

What's old about option -obviously-terminates

Option -obviously-terminates is a value analysis option, new in Nitrogen, with some of the same effects as using an infinite slevel. This option also disables fixpoint detection and the statement-wise memorisation of analysis results.

I briefly described this option in a previous post in section “Trying to improve results by doing things differently”. This option was originally intended for the interpretation of Csmith-generated programs. Csmith-generated programs are executable and it is possible to make sure that they terminate by simply letting them run for a few milliseconds. Once it is known that a Csmith-generated program terminates then the value analysis' job interpreting the program is much easier with option -obviously-terminates. This option tells it not to waste time looking for a fixpoint since in this case it could only find one if the program looped which we know it doesn't.

What's new about option -obviously-terminates

Option -obviously-terminates can be used to verify the termination of C programs.

Used this way it is sound—when it diagnoses the program as terminating then the program always terminates. It is not complete: it may fail to answer for programs that terminate. Actually it always either diagnoses the program as terminating or fails to answer: it must be used with a timeout. It tries to make the program terminate until the timeout and the timeout being reached must be interpreted as the answer “I don't know”.

This new insight into an existing option is as new for me as it is for you: I genuinely did not realize that this option could do this until this morning's shower. I was close because in the previously linked blog post I had written:

“[Option -obviously-terminates] makes [the value analysis] loop forever on C programs that loop forever — like an interpreter does”

But it did not occur to me to contrapose the above statement until I tried a few examples into the web interface for sett Germán Vidal's symbolic execution-based termination tool. I am extremely thankful to him for making this web interface available.

Examples

Here is a first example with non-obvious termination:

char x  y; 
main() 
{ 
  x = input(); 
  y = input(); 
  while (x>0 && y>0) 
    { 
      if (input() == 1) 
	{ 
	  x = x - 1; 
	  y = input(); 
	} 
      else 
	y = y - 1; 
    } 
} 

Note the use of the (signed) type char for variables x and y to limit combinatorial explosion.

$ frama-c -obviously-terminates -val t1.c 
[kernel] preprocessing with "gcc -C -E -I.  t1.c" 
[value] Analyzing a complete application starting at main 
[value] Computing initial state 
[value] Initial state computed 
[value] Values of globals at initialization 
        x ∈ {0} 
        y ∈ {0} 
[value] computing for function input <- main. 
        Called from t1.c:5. 
... 
   (several seconds here) 
... 
[value] Semantic level unrolling superposing up to 48100 states 
... 
[value] Done for function input 
[value] Recording results for main 
[value] done for function main 
[value] ====== VALUES COMPUTED ====== 

Frama-C's value analysis with option -obviously-terminates was able to finish its analysis of this example. This means that the program terminates for all possible integers returned by input().

Another example:

char x  y; 
main() 
{ 
  x = input(); 
  y = input(); 
  while (x>0 && y>0) 
    { 
      // Frama_C_dump_each(); 
      if (input()) 
        { 
          x = x - 1; 
          y = x; 
        } 
      else 
        { 
          x = y - 2; 
          y = x + 1; 
        } 
    } 
} 

$ frama-c -obviously-terminates -val t2.c  
... 
[value] ====== VALUES COMPUTED ====== 

This means once again that the program terminates for all possible integers returned by input().

I couldn't believe how fast the analysis of this second example was so I inserted the Frama_C_dump_each(); call. If you uncomment it you can see the abstract states that have been considered during the analysis and how they become smaller and smaller until it becomes obvious that all execution paths eventually exit the loop.

The two above examples were taken from the sett website. They can be found in the sett input language syntax inside the PDF description of the tool. Here is a third example invented by me:

char x; 
main(){ 
  x = input(); 
  while (x > 0) 
    { 
      Frama_C_dump_each(); 
      if (x > 11) 
        x = x - 12; 
      else 
        x = x + 1; 
    } 
} 

Again frama-c -obviously-terminates -val shows the termination of this program. It is very quick in this case since the interval for variable x is initially reduced by slices of 12 values at a time and then the value analysis carefully analyzes the tricky part which takes most of the time.