C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

Of course... the more that I think about it... :)

You say the "compiler cannot be asked to generate code for the
then-branch".  If the restriction on &x were dynamic, the compiler
could actually assume the code wouldn't be reached.  The compiler
knows that if it COULD be reached, the program would be undefined, so
it's safe to assume it can't be reached.  They could generate no code
whatsoever for this branch.

So maybe it was meant to be a static concept, but it doesn't seem like
it must be.  It certainly isn't clear from the text.  I keep running
into this problem of static vs dynamic trying to figure out exactly
what's undefined.  The same problem crops up all over the place:
6.3.2.2 says "implicit or explicit conversions (except to void) shall
not be applied to such an expression."
if (0) {
    (int)(void)5;
}
Is "applied" static or dynamic?  This /could/ be defined.  Again, when
generating code, an implementation could assume the branch must never
execute.


6.3.2.1:2, says "If the lvalue [to be evaluated] has an incomplete
type and does not have array type, the behavior is undefined."
struct s s0;
int main(void){
        if (0) {
                s0;
        }
}
struct s { int x; };
Same story.


6.3.2.3 says "If a converted pointer is used to call a function whose
type is not compatible with the referenced type, the behavior is
undefined."
int f(void){ return 5; }
int main(void){
        if (0) {
                ((float (*)(void))&f)();
        }
}
Is "is used" static or dynamic?  GCC/Clang/ICC seem to think this
program is valid, while the above two programs are invalid.  I don't
see what makes this one special.


And of course,
if (0) {
    5 / 0;
}
which I assume we would all agree is defined, but Derek tells me there
has been lengthy discussion about even that.


I guess the unwritten intuition is something like the following: given
a questionable piece of C code, if an implementation can compile it
without having to assume anything about program flow, then the code
can only be invalid dynamically.  If an implementation wouldn't be
able to generate code without assuming the code couldn't be reached,
then it is invalid statically.

-Chucky

On Wed, Jan 4, 2012 at 12:34 PM, Chucky Ellison 
<celliso2 AT illinois.edu>
 wrote:
> This makes a ton of sense.  Thanks Pascal!
>
> On Wed, Jan 4, 2012 at 12:19 PM, CUOQ Pascal 
> <Pascal.CUOQ AT cea.fr>
>  wrote:
>>> "register" is [...] used in
>>> 6.3.2.1:2 to identify another very important class of undefined
>>> behaviors, having to do with reading uninitialized values.
>>
>> The rationale for the change is at
>> http://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_338.htm
>>
>>> So in total, we have (in a footnote) "the address ... cannot be
>>> computed" and (in the body) "never had its address taken" used to
>>> describe the restriction on the register storage class.  Are these
>>> static or dynamic concepts?
>>
>> I think the intention was that the restriction was a static notion.
>> This seems to fit both the idea that the compiler cannot be asked
>> to generate code for the then-branch of your if and that the
>> compiler should be allowed to use the register-only NaT value
>> of IA64, that cannot exist in memory, as value of uc in the
>> example of DR 338.
>>
>> Pascal
>>