llvm dev - Jul 2015 - [LLVMdev] C as used/implemented in practice: analysis of responses

On 07/02/2015 04:44 PM, David Keaton wrote:
> On 07/02/2015 03:17 AM, Kuperstein, Michael M wrote:
>> You want to redefine ["won't break the program"], by
specifying a new
>> abstract machine, which is
>> more conservative than standard C/C++. The proper way to do that would,
>> I believe, be to work towards setting up a working group within the
>> relevant committees, and come up with a uniformly accepted definition
>> for this abstract machine, which could then be implemented (assuming
>> there is, indeed, wide enough agreement in the implementer community –
>> something that does not look at all likely) by next-generation 
>> compilers.
>
>      This work has already been done in Annex L of the C standard, 
> which provides an optional stricter abstract machine.  As far as I 
> know, no implementations have attempted to support Annex L yet.
Do you have a link to the relevant text?  I've never heard of this, and 
a quick google search doesn't turn up anything relevant. Wikipedia knows 
about a set of "analyzability features", but that doesn't sounds
like
what you're talking about?
>
>> Point is – I think you’re barking up the wrong tree.
>>
>> This isn’t an llvm-dev issue, it’s a standards committee issue.
>
>      Because the standards work has been done, the ball is back in the 
> implementations' court.  That doesn't mean Annex L should be the 
> default behavior.  It would be nice to have it as an option, though.
>
>                     David
>
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev

On 07/02/2015 05:30 PM, Philip Reames wrote:
>
>
> On 07/02/2015 04:44 PM, David Keaton wrote:
>> On 07/02/2015 03:17 AM, Kuperstein, Michael M wrote:
>>> You want to redefine ["won't break the program"], by
specifying a new
>>> abstract machine, which is
>>> more conservative than standard C/C++. The proper way to do that
would,
>>> I believe, be to work towards setting up a working group within the
>>> relevant committees, and come up with a uniformly accepted
definition
>>> for this abstract machine, which could then be implemented
(assuming
>>> there is, indeed, wide enough agreement in the implementer
community –
>>> something that does not look at all likely) by next-generation
>>> compilers.
>>
>>      This work has already been done in Annex L of the C standard,
>> which provides an optional stricter abstract machine.  As far as I
>> know, no implementations have attempted to support Annex L yet.
> Do you have a link to the relevant text?  I've never heard of this, and
> a quick google search doesn't turn up anything relevant. Wikipedia
knows
> about a set of "analyzability features", but that doesn't
sounds like
> what you're talking about?
      The relevant text is inside the standard, which is for sale.  The 
cheapest source I know about is this.

http://webstore.ansi.org/RecordDetail.aspx?sku=INCITS%2fISO%2fIEC+9899%3a2011%5b2012%5d

      The title of Annex L is Analyzability, because that was the 
purpose, but the effect was to define a stricter abstract machine in 
which there were no unbounded undefined behaviors except what was 
absolutely necessary.  That does not address every question in the 
questionnaire, but it is a good start, and it has already been 
standardized so there is something concrete to implement.

					David

>      The relevant text is inside the standard, which is for sale.  The
> cheapest source I know about is this.
Or just search for n1570, which I think is the final draft of C11 so
has everything but the rubber stamp.

Tim.

On Thu, Jul 2, 2015 at 5:43 PM, David Keaton <dmk at dmk.com> wrote:
> On 07/02/2015 05:30 PM, Philip Reames wrote:
>
>>
>>
>> On 07/02/2015 04:44 PM, David Keaton wrote:
>>
>>> On 07/02/2015 03:17 AM, Kuperstein, Michael M wrote:
>>>
>>>> You want to redefine ["won't break the program"],
by specifying a new
>>>> abstract machine, which is
>>>> more conservative than standard C/C++. The proper way to do
that would,
>>>> I believe, be to work towards setting up a working group within
the
>>>> relevant committees, and come up with a uniformly accepted
definition
>>>> for this abstract machine, which could then be implemented
(assuming
>>>> there is, indeed, wide enough agreement in the implementer
community –
>>>> something that does not look at all likely) by next-generation
>>>> compilers.
>>>>
>>>
>>>      This work has already been done in Annex L of the C standard,
>>> which provides an optional stricter abstract machine.  As far as I
>>> know, no implementations have attempted to support Annex L yet.
>>>
>> Do you have a link to the relevant text?  I've never heard of this,
and
>> a quick google search doesn't turn up anything relevant. Wikipedia
knows
>> about a set of "analyzability features", but that doesn't
sounds like
>> what you're talking about?
>>
>
>      The relevant text is inside the standard, which is for sale.  The
> cheapest source I know about is this.
>
>
>
http://webstore.ansi.org/RecordDetail.aspx?sku=INCITS%2fISO%2fIEC+9899%3a2011%5b2012%5d

"Final draft" is available at
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf

-- Sean Silva

>
>
>      The title of Annex L is Analyzability, because that was the purpose,
> but the effect was to define a stricter abstract machine in which there
> were no unbounded undefined behaviors except what was absolutely
> necessary.  That does not address every question in the questionnaire, but
> it is a good start, and it has already been standardized so there is
> something concrete to implement.
>
>
>                                         David
>
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150702/90235520/attachment.html>

On 07/02/2015 05:43 PM, David Keaton wrote:
> On 07/02/2015 05:30 PM, Philip Reames wrote:
>>
>>
>> On 07/02/2015 04:44 PM, David Keaton wrote:
>>> On 07/02/2015 03:17 AM, Kuperstein, Michael M wrote:
>>>> You want to redefine ["won't break the program"],
by specifying a new
>>>> abstract machine, which is
>>>> more conservative than standard C/C++. The proper way to do
that
>>>> would,
>>>> I believe, be to work towards setting up a working group within
the
>>>> relevant committees, and come up with a uniformly accepted
definition
>>>> for this abstract machine, which could then be implemented
(assuming
>>>> there is, indeed, wide enough agreement in the implementer
community –
>>>> something that does not look at all likely) by next-generation
>>>> compilers.
>>>
>>>      This work has already been done in Annex L of the C standard,
>>> which provides an optional stricter abstract machine.  As far as I
>>> know, no implementations have attempted to support Annex L yet.
>> Do you have a link to the relevant text?  I've never heard of this,
and
>> a quick google search doesn't turn up anything relevant. Wikipedia
knows
>> about a set of "analyzability features", but that doesn't
sounds like
>> what you're talking about?
>
>      The relevant text is inside the standard, which is for sale. The 
> cheapest source I know about is this.
>
>
http://webstore.ansi.org/RecordDetail.aspx?sku=INCITS%2fISO%2fIEC+9899%3a2011%5b2012%5d
>
I found a draft version which appears to have been
complete.
>
>      The title of Annex L is Analyzability, because that was the 
> purpose, but the effect was to define a stricter abstract machine in 
> which there were no unbounded undefined behaviors except what was 
> absolutely necessary.  That does not address every question in the 
> questionnaire, but it is a good start, and it has already been 
> standardized so there is something concrete to implement.
IMHO, the Annex completely fails to be useful for the purpose you 
intend.  The definition of "bounded undefined behavior" is phrased in 
terms of "may", not "must".  The wording doesn't appear
to require a
choice from the list; it merely states some possible implementations.  
Unless I'm reading it wrong, the only real restriction is against out of 
bounds stores.  On the surface, it doesn't even seem to prevent out of 
bounds stores in the program being exposed by a transformation.  It only 
prevents an out of bounds store in the undefined operation itself.  That 
really doesn't get you much of anything.

Consider:
y is positive
a = x + y (signed overflow, wrapping "expected")
if (a >= x)
   store out of bounds
===>
store out of bounds

Philip



Philip