Converting SV-COMP (complexity competition) programs.

[ishimwed]

Converting 2019 Complexity competition programs to recursive structure.

There are around 500 imperative programs with nontrivial loops in the complexity competition. We want to convert these iterative programs to recursive programs.
Most of these functions with loops have the following structure:

foo_iterative(params){
    header
    while(condition){
        loop_body
    }
    return tail
}

1. the header: statements before the loop. This may declare some new variables

2. the loop condition: which indicates when to stop the loop

3. the loop body: which changes some header variables and/or function parameters. This is the main part we want to eliminate or convert into recursion.

4. the tail; statements after the loop.

We transform the above foo_iterative function to recursion as follows:

foo_recursive(params){
    header
    return foo_recursion(params, header_vars)
}

foo_recursion(params, header_vars){
    if(!condition){
        return tail
    }

    loop_body
    return foo_recursion(params, modified_header_vars)
}

Example: Bangalore_v4_true-termination.c

int foo(int x, int y){
if (y > x) {
	while (x >= 0) {
	    	x = x - y;
    	}
	}
return 0;
}

Converting foo() into a recursive function:

1. header: if (y > x)
2. loop condition: (x >= 0)
3. loop body: x = x - y;
4. tail: return 0;

Resulting recursive foo program:

int foo(int x, int y){
    if (y > x){
      return rec_foo(x, y);
    }
    return 0;
}

int rec_foo(int x, int y){
  rec_trace(x);
  if(!(x >= 0)){
      return 0;
  }
  x = x - y;
  return rec_foo(x, y);
}

Remarks:
Although these steps help to transform a lot of iterative functions into recursion it is not comprehensive. There are examples where it would be difficult to follow the above steps. Fortunately, termination competition have a lot of programs and many of them can be converted by just using the above technique. We want to start with those easier programs. We are not trying to remove all loops, just the main loops. For example, in case of nested loops we want to transform the outer loop and consider the inner loop as loop body (step 3). More examples are given in recursive_programs/c (dev branch); the file names matches the file names given in the complexity termination to avoid confusion.
Note: I haven't figured out how to handle sequential loops. Do not commit any changes to the master branch.

[nguyenthanhvuh]

@ishimwed , turn this into smaller tasks. Let's start with say 20 programs first.

[ishimwed]

I selected 20 programs to start with. Selection criteria: randomly picked programs for which I couldn't compute complexity in less than 20 seconds. I also selected programs for which AProVE and CoFloCo did not compute the same upper bound. I tried to have all complexity classes (n, n^2, n^3, n^4, \inf) represented.
The programs selected are:

1. t11.c
2. speed_popl10_nested_multiple.c
3. speed_pldi10_ex1.c
4. speed_pldi09_fig1.c
5. svcomp_c.01_assume.c
6. gcd1_true-termination.c
7. cBench_hc_compute.c
8. realshellsort.c
9. Masse-VMCAI2014-Fig1a_true-termination.c
10. aaron3.c
11. rank2.c
12. Loopus2011_ex2.c
13. ex_paper1.c
14. Nested.c
15. PastaA10.c
16. Masse-VMCAI2014-Fig1a_true-termination.c
17. CookSeeZuleger-TACAS2013-Fig8a_true-termination.c
18. svcomp_a.10.c
19. ChenFlurMukhopadhyay-SAS2012-Ex2.22_true-termination.c
20. HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_true-termination.c

[nguyenthanhvuh]

@ishimwed thanks, can you also select about 10 "easy" programs so that the undergraduate students can try them first?

[ishimwed]

Let's start with the programs from the list above. The two programs converted could lead to non-terminating executions. We will avoid such programs since their worst case complexity is infinite and dynaplex cannot handle such programs.
The conversion looked correct. To simplify the task we can avoid using pointers unless necessary.

[hyunsoo3075]

Did you want us to create our own branches to try some examples?
I'm not much experienced with github but I didn't want to make any changes to master.
I did try out PastaA10.c as an example please let me know if it's correct! thank you

[ishimwed]

You can create your own branches. We will merge the results once we are done. I checked PastaA10.c and it looks good. I would change one thing in rec_foo() for better readability: move the two recursive calls at the end since they are similar in both branches.

int rec_foo(int x, int y)
{
	if(x>y)
	{
		y = y+1;
	}	
	else if(y > x)
	{
		x = x + 1;
	}
        return rec_foo(x,y);
}

[hyunsoo3075]

Great, Thanks for the feedback! will fix with the suggestions.