[Termtools] TPDB -- C-Integer Complexity

[aeflores]

Dear all,

I agree with Florian's proposal for the fragment of C in the C integer 
complexity category.
Best,

Antonio



On 08/03/2017 05:02 PM, Florian Frohn wrote:
> 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
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools