[Termtools] Complexity of C programs: some issues

[Michael Schaper]

Hi all,

we agreed to have a *complexity of integer C programs* category. I 
missed that we have already fixed the details of the input format and 
the benchmark.

The TPDB/C_Integer benchmark has been established for termination 
analysis. Though I do not know the details it seems that the entry point 
for the problems is fixed to `int main()` and as mentioned by Antonio 
most programs use a non-deterministic assignment to initialise variables.

For complexity it would make sense to have `int main(int x1, ... int 
xn)` or more generally `int someFunction(int x1, ..., int xn)` and take 
the last function declaration. This clarifies the input. Moreover, 
non-deterministic assignments may also be introduced during program 
abstractions and we would have to distinguish input and non-input variables.

On the other hand, we want to automate as much as possible. We should 
take into consideration the input and output format of tools that 
perform the necessary transformations from/to C, integer C, ITS, CES,...

Best,
michi



On 08/17/2016 02:16 PM, aeflores wrote:
> Dear all,
>
> I noticed some of the benchmarks for the complexity of C programs have a
> single function with no parameters. Instead, the "parameters" are
> assigned with a call to the function __VERIFIER_nondet_int(). The
> simplest example of this is *test/C_Integer/Stroeder_15/WhileDecr.c:*
>
> typedef enum {false,true} bool;
>
> extern int __VERIFIER_nondet_int(void);
>
> int main() {
>     int i;
>     i = __VERIFIER_nondet_int();
>
>     while (i > 5) {
>         i = i-1;
>     }
>
>     return 0;
> }
>
> I imagine that these examples come from the termination benchmarks where
> this is irrelevant, but I believe that the complexity of a function
> should be in terms of the input parameters, shouldn't it? As it is, the
> complexity of *WhileDecr.c *in terms of the input parameters is not defined.
>
> Surprisingly, Loopus finds assigns a linear complexity to this example.
> I guess it assumes the return of __VERIFIER_nondet_int() as an input
> parameter...
>
> We could adapt these examples for complexity by adding the relevant
> variables as parameters: "int main(int i)...". Other examples in which I
> noticed this  (there might be more) are:
>
> AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination.c
> CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination.c
> NoriSharma-FSE2013-Fig7_true-termination.c
> svcomp_b.18.c
>
> Best regards,
>
>
> Antonio
>
>
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>