Cost relations explored

[OrenGitHub]

Hi @aeflores , the following program returns Asymptotic class: infinity, and we wanted to know if this failure is due to an inherent limitation in the cost relation solving? or other reason? Also, is it possible to extract the cost relations from the web interface of CoFloCo? Thank you very much!

void cex(unsigned int a, unsigned int b)
{
    unsigned int out=1;
    
    while (out)
    {
        if (a > 0)
        {
            a=a-1;
            b=2*b;
        }
        else if (b > 0)
        {
            b=b-1;
        }
        else
        {
            out=0;
        }
    }
}

[aeflores]

Hi @OrenGitHub, Yes, this is a limitation of the current algorithm. If I am not mistaken, in the first phase of the loop, b grows exponentially, which is something that CoFloCo cannot capture.

Regarding your second question, yes, it is possible to print the cost relations in the web interface. Under Settings in the top left corner, there is a checkbox called Print ITS and CRs which will print the ITS (integer transition system), generated from the C code, and the CRs (Cost Relations), generated from the ITS, when you run the analysis.

[OrenGitHub]

Thanks!! I looked at the resulting CRs (pasted below), and understood the following:

• out = V_out_0, a = V__0 and b = V__01
• The CRs are mutually recursive, referring to the five basic blocks of LLVM bitcode.

However, I expected 3 variables handled by each CR, and found 4:

• a, b, out and B

My question is: what is this B?

###### Cost Relations System ####################
input_output_vars(eval_cex_bb0_in(V_a,V_b,B),[V_a,V_b],[B]).
input_output_vars(eval_cex_bb1_in(V_out_0,V__01,V__0,B),[V_out_0,V__01,V__0],[B]).
input_output_vars(eval_cex_bb2_in(V_out_0,V__01,V__0,B),[V_out_0,V__01,V__0],[B]).
input_output_vars(eval_cex_bb3_in(V_out_0,V__01,V__0,B),[V_out_0,V__01,V__0],[B]).
input_output_vars(eval_cex_bb4_in(V_out_0,V__01,V__0,B),[V_out_0,V__01,V__0],[B]).
input_output_vars(eval_cex_bb5_in(B),[],[B]).
input_output_vars(eval_cex_start(V_a,V_b,B),[V_a,V_b],[B]).
eq(eval_cex_start(V_a,V_b,B),0,[eval_cex_bb0_in(V_a,V_b,B)],[]).
eq(eval_cex_bb1_in(V_out_0,V__01,V__0,B),0,[eval_cex_bb2_in(V_out_0,V__01,V__0,B)],[V_out_0<0]).
eq(eval_cex_bb1_in(V_out_0,V__01,V__0,B),0,[eval_cex_bb2_in(V_out_0,V__01,V__0,B)],[V_out_0>0]).
eq(eval_cex_bb1_in(V_out_0,V__01,V__0,2),0,[],[V_out_0=0]).
eq(eval_cex_bb2_in(V_out_0,V__01,V__0,B),0,[eval_cex_bb3_in(V_out_0,V__01,V__0,B)],[V__0>0]).
eq(eval_cex_bb2_in(V_out_0,V__01,V__0,B),0,[eval_cex_bb4_in(V_out_0,V__01,V__0,B)],[V__0=<0]).
eq(eval_cex_bb3_in(V_out_0,V__01,V__0,B),1,[eval_cex_bb1_in(V_out_0,2*V__01,V__0-1,B)],[]).
eq(eval_cex_bb4_in(V_out_0,V__01,V__0,B),1,[eval_cex_bb1_in(V_out_0,V__01-1,V__0,B)],[V__01>0,V__01>0]).
eq(eval_cex_bb4_in(V_out_0,V__01,V__0,B),1,[eval_cex_bb1_in(V_out_0,V__01,V__0,B)],[V__01>0,V__01=<0]).
eq(eval_cex_bb4_in(V_out_0,V__01,V__0,B),1,[eval_cex_bb1_in(0,V__01-1,V__0,B)],[V__01=<0,V__01>0]).
eq(eval_cex_bb4_in(V_out_0,V__01,V__0,B),1,[eval_cex_bb1_in(0,V__01,V__0,B)],[V__01=<0,V__01=<0]).
eq(eval_cex_bb0_in(V_a,V_b,B),1,[eval_cex_bb1_in(1,V_b,V_a,C),loop_cont_eval_cex_bb1_in(C,B)],[]).
eq(eval_cex_bb5_in(B),0,[eval_cex_stop(B)],[]).
eq(loop_cont_eval_cex_bb1_in(2,A),0,[eval_cex_bb5_in(A)],[B=0]).

[aeflores]

B is a variable added by the transformation. The transformation from ITS to CRs transforms each loop into a recursive definition. But a loop in C/C++ can have multiple exit points e.g. you can have break, return or exit the loop at the loop condition. The variable B is used to match each exit point of the loop (which is a base case of the recursion)

eq(eval_cex_bb1_in(V_out_0,V__01,V__0,2),0,[],[V_out_0=0]).

With the proper continuation after the loop:

eq(eval_cex_bb0_in(V_a,V_b,B),1,[eval_cex_bb1_in(1,V_b,V_a,C),loop_cont_eval_cex_bb1_in(C,B)],[]).
eq(loop_cont_eval_cex_bb1_in(2,A),0,[eval_cex_bb5_in(A)],[B=0]).

In this example B gets the value 2 at the base case. That B corresponds to C in

eq(eval_cex_bb0_in(V_a,V_b,B),1,[eval_cex_bb1_in(1,V_b,V_a,C),loop_cont_eval_cex_bb1_in(C,B)],[]).

Which is passed as the first argument to loop_cont_eval_cex_bb1_in This CR, in turn has a single continuation that requires this argument to be 2.

eq(loop_cont_eval_cex_bb1_in(2,A),0,[eval_cex_bb5_in(A)],[B=0]).

If you have a loop with multiple exits, each one will assign a different value for B. This is not important in your example but it could be important in others. E.g.

void tick(int i);
void cex(unsigned int a, unsigned int b, unsigned int c)
{
    while (a>0) {
        if (b > 0)
            return;
        a--; 
    }
  tick(10);
}

In this example, if the first loop exits with a return, the call to tick will not be executed, but if it exits normally, tick will be called. The corresponding CRs reflect this:

1: eq(eval_cex_bb1_in(V_b,V__0,B),0,[eval_cex_bb2_in(V_b,V__0,B)],[V__0>0]).
2: eq(eval_cex_bb1_in(V_b,V__0,2),0,[],[V__0=<0]).
3: eq(eval_cex_bb2_in(V_b,V__0,3),0,[],[V_b>0]).
4: eq(eval_cex_bb2_in(V_b,V__0,B),0,[eval_cex_bb3_in(V_b,V__0,B)],[V_b=<0]).
5: eq(eval_cex_bb3_in(V_b,V__0,B),0,[eval_cex_bb1_in(V_b,V__0-1,B)],[]).
6: eq(eval_cex_bb0_in(V_a,V_b,B),0,[eval_cex_bb1_in(V_b,V_a,C),loop_cont_eval_cex_bb1_in(C,B)],[]).
7: eq(eval_cex_bb4_in(B),0,[eval_cex_2(B)],[]).
8: eq(eval_cex_bb5_in(B),0,[eval_cex_stop(B)],[]).
9: eq(loop_cont_eval_cex_bb1_in(2,A),0,[eval_cex_bb4_in(A)],[B=<0]).  
10: eq(loop_cont_eval_cex_bb1_in(3,A),0,[eval_cex_bb5_in(A)],[B>0]).
11: eq(eval_cex_2(B),10,[eval_cex_3(B)],[]). 
12: eq(eval_cex_3(B),0,[eval_cex_bb5_in(B)],[]).

There are two loop exits with B=2 and B=3 in Cost Equation (CE) 2 and 3 which correspond to two continuations (CE 9 and 10) which lead to different costs (CE 7 and 11 vs CE 8).