[Termtools] TPDB -- C-Integer Complexity

[Florian Frohn]

Good point. Indeed, I found some mails on this subject, but as far as I
can see we didn't agree on a definition (true?). Thus we should probably
try to fix the fragment of C which is in scope. How about the following:

* one and only one defined function, which is the starting point
* all types occurring in function-signatures must be integer-types
* all variables have to have some integer-type
* no pointers / arrays / dereferencing / address-operator (&)
* no bitwise operations
* no structs / unions
* no function calls except for calls to declared, but undefined
functions (which are used to model nondeterminism)
* no sizeof
* no programs which might have undefined behavior (e.g., no division by
zero)

plus the following rules from http://termination-portal.org/wiki/C_Programs:

* functions which are only declared, but not defined, are considered to
be terminating, have no side effects, and return a non-deterministic
value according to the function's return type
* programs where the evaluation order of operations is not defined
according to the C standard and where different execution orders of the
operations lead to different resulting states are not allowed
* we assume integers to be mathematical integers
* integer division by negative numbers is assumed to be done by
truncation towards zero

I think this includes most (probably all) programs from the current
benchmark set.

Best
Florian


On 08/03/2017 03:48 PM, aeflores wrote:
> The problem with that definition is that the main function does not
> receive any parameters so the complexity of the program cannot be
> defined in terms of the input parameters.
> I believe we ran into the same problem last year.
>
> I think we could adopt a similar definition that allows parameters and
> collect new examples (points 1 and 2) but I do not think we can use
> the examples from the termination category
> (point 3) for the same reason (maybe some can be adapted).
> Best,
>
> Antonio
>
>
> On 07/31/2017 11:02 AM, Florian Frohn wrote:
>> Dear all,
>>
>> during the preparations for the upcoming TermComp I came across some
>> oddities regarding the category "C-Integer Complexity". First of all,
>> the TPDB contains just 26 examples for this category, but according to
>> the Call for Participation at least 40 examples are required. More
>> importantly, they do not conform to the TermComp definition of C-Integer
>> programs (http://www.termination-portal.org/wiki/C_Integer_Programs).
>> E.g., cBench_bin_search_StepSize2.c uses "nondet" instead of
>> "__VERIFIER_nondet_int" for nondeterminism and it uses division, which
>> is not allowed by the definition.
>>
>> Assuming that we agree on the definition from
>> http://www.termination-portal.org/wiki/C_Integer_Programs (which was
>> discussed when the category "C-Integer Termination" was introduced), I
>> propose to
>>
>> 1. remove all examples that do not conform to the definition,
>> 2. collect new examples, and
>> 3. use the examples from "C-Integer Termination" as fallback (i.e., if
>> less than 40 examples are submitted), even though some of them might be
>> uninteresting for complexity analysis.
>>
>> What do the other participants of this category think?
>>
>> Best
>> Florian
>>
>>
>> PS: Sorry if you received multiple copies of this mail, there were some
>> technical issues.
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools