8 ms·

A semantic model for a substantial fragment of C

97 points by edwintorok 10y ago

gravypod 10y ago
I've heard many "real" computer scientists say the "C remains central to our computing infrastructure but still lacks a clear and complete semantics" line but I have no idea what they mean. Can someone explain to me what this means to the academic-CS type? How can something with a parser & lexer not have "clear and complete semantics". If you have a computer language which has defined elements of the syntax how can you not have clearly defined meanings of combinations of the syntax? Does someone have an example of a piece of C that is not "deterministic" (best word I have for this) to a lexer & parser?
- brianberns 10y ago
  Example of undefined behavior: What arguments will f be called with? int i = 0; f(i++, i++); More examples here: https://www.cl.cam.ac.uk/teaching/1415/CandC++/lecture10.pdf https://www.cl.cam.ac.uk/teaching/1415/CandC++/lecture10.pdf
  - gravypod 10y ago
    I'd assume it would be f(1, 0); Because function arguments are pushed in reverse order in C and funnily enough, GCC actually does that even though that's crazy. But clang catches it as an "unsequenced modification". I don't think that's a good example. The C standards make no guarantees about unsequenced modifications so relying on them is the programmer not using C, it's the programmer using a language derivative implemented by their compiler. Why do people say "C remains central to our computing infrastructure but still lacks a clear and complete semantics" when the standards are very clear about what it allows? If you use something it doesn't allow you can't blame the spec for that.
    - brianberns 10y ago
      I don't understand why you say that it's not a good example. It's legal C that has undefined semantics, which is what you were asking for.
      - gravypod 10y ago
        > It's legal C No it's not. It's undefined behavior meaning, by definition, it's not C. It's not defined in C. If I had an list of all definitions, would an undefined item be in my list? No. When you are using Undefined Behavior, you are not using C. You're using a C-extension that a compiler designer has implemented. This was done because there is no sane operation to do in these UB cases for one reason or another. Either it would not be portable or it wouldn't make sense. If there was a standard that implemented standards for UB cases it would not be portable.
        brianberns 10y ago
        OK, so to paraphrase your position: C has clear and complete semantics because anything written in C that doesn't have clear and complete semantics is, by definition, not actually written in C. Yes? To me, that's like saying the tax code doesn't contain any loopholes, because any loopholes that it contains are, by definition, not actually part of the tax code. While amusing, I don't think this is a fruitful way to look at the problem. :)
        loeg 10y ago
        You can write things that look like C, but that doesn't make them valid C. Invalid code is just a collection of ASCII characters, I guess.
        pasquinelli 10y ago
        Does the parser reject it? That's the test for syntactically valid c.
        10y ago
    - CalChris 10y ago
      What if f is a macro. Then it has a lexically determined meaning. What if f is a function. Then it has a parsing determined meaning. What if the ++ operator has been redefined. Et cetera.
      - gravypod 10y ago
        If F is a macro then it will just be expanded. Lets say F was #define f(a, b) printf("%d %d\n", a, b); This would change absolutely nothing. A macro is just a piece of code that is expanded. It still follows all of the rules (and disallowances) of C.
        foota 10y ago
        Fairly certain you can have compound statements as the result of the macro. e.g., the macro could expand to if(a) {printf("%d\n", b);} for example
        Normal_gaussian 10y ago
        You can. Of course you don't even need the logical connector #define f(a,b) \ f_var1 = a; \ f_var2 = b Equally you could use macros to make it a whole lot worse #define f(a,b) \ f_arr[a][b] += f_arr[b][a]
        snovv_crash 10y ago
        What if the macro uses a and/or b more than once?
      - loeg 10y ago
        At least, the ++ operator cannot be redefined in C.
        tathougies 10y ago
        The ability to redefine the ++ operator would not alone make it difficult to add proper semantics to the C language. What is preventing that is that no one can really describe how function application truly works in C (in terms of operation ordering), except that we all have an idea similar enough that our systems seem to work together in practice. For all the criticism Haskell gets over the purported difficulty on describing sequential computation, at least the order of monadic operations is clearly captured by the requirements to be a monad. There is no such concept for C, except that each compiler mostly seems to perform operations sequentially.
    - laughinghan 10y ago
      You're missing the point. Can we agree that people are learning a programming language that they call "C", and writing text files in that language and running programs that they call "C compilers" such as gcc on those text files to produce binary executables? You are correct to note that the programming language I'm describing does not perfectly conform to any of the documents that are ever called a "C standard". But that programming language is central to our computing infrastructure, and whether you or C standard authors like it or not that programming language is widely called "C". That language's semantics are unclear and incomplete---even though both gcc and clang are commonly called "C compilers", they have differing behavior on `f(i++, i++)` as you found; reportedly, there's code on which gcc behaves differently depending on the optimization level option.
      - zodiac 10y ago
        > You are correct to note that the programming language I'm describing does not perfectly conform to any of the documents that are ever called a "C standard". But that programming language is central to our computing infrastructure I don't agree with this. Yes, people often write code that unintentionally rely on UB/implementation-specific behavior; but are there important projects that do this intentionally? In any case, compiler authors are going to follow the C standards, not you hypothetical "C-in-practice" standards, so what good does it do to for formalize or clearly specify the latter?
        naasking 10y ago
        > I don't agree with this. Yes, people often write code that unintentionally rely on UB/implementation-specific behavior; but are there important projects that do this intentionally? The Linux kernel.
        gravypod 10y ago
        I thought staging was the only folder with UB code.
        10y ago
    - jabot 10y ago
      > Because function arguments are pushed in reverse order in C and funnily enough, GCC actually does that even though that's crazy. Actually, pushing function arguments right-to-left means that the first argument ends up on top of the stack - and that makes vararg-style functions possible. Think about it - a called vararg method must be able find the fixed arguments to figure out how many arguments it actually gets.
      - gravypod 10y ago
        That's what I mean by "Pushed in reverse order"
    - nickpsecurity 10y ago
      While people are arguing it's syntax, you all might enjoy this parody that's a good example of Poe's Law due to C's horrid (i.e. lack of a) design: https://www.gnu.org/fun/jokes/unix-hoax.html https://www.gnu.org/fun/jokes/unix-hoax.html
  - danieltillett 10y ago
    Is this example non-deterministic or just undefined? Sure you should not rely on this code to give you consistent results between compilers and even optimisation levels, but what ever happens should be consistent between runs.
    - gravypod 10y ago
      This is UB and it's caught by both GCC and Clang: $ gcc -Wall test.c test.c: In function ‘main’: test.c:12:13: warning: operation on ‘a’ may be undefined [-Wsequence-point] test(a++, a++); ~^~ $ clang test.c test.c:12:8: warning: multiple unsequenced modifications to 'a' [-Wunsequenced] test(a++, a++); ^ ~~ 1 warning generated.
      - danieltillett 10y ago
        Exactly. The OP asked for an example of a non- deterministic function not UB.
        fmap 10y ago
        I'm not sure about non-deterministic behavior without looking it up, but you can fix this example to be implementation defined, rather than undefined like this: #include <stdio.h> int postincrement(int *x) { int y = *x; *x = y + 1; return y; } int main(int argc, char **argv) { int i = 0; printf("%d, %d\n", postincrement(&i), postincrement(&i)); return 0; } The point is that function arguments introduce sequence points, but the specification for i++ is weaker than what you get for a function call. C is full of gotchas like this...
        pasquinelli 10y ago
        Their term was non-deterministic, but they asked for undefined behavior, because they were asking for examples of course being not fully defined semantically.
      - Keyframe 10y ago
        Exactly! Without sequence-point error, output is 1,0 on GCC6, 0,1 with CLang.
  - agumonkey 10y ago
    I'm dumbfounded by all the operators of C that enable all this confusion. About the potential order of evaluation, it's not limited to C, but at least it's clearly and dilligently explained even in tiny standards like Scheme.
    - Johnny_Brahms 10y ago
      The scheme standard actually bit my sorry behind recently. I was porting a small library between scheme implementations, and my tests were failing. I had always thought it was evaluated left->right (which it was in the first scheme implementation), but it is in fact standardised as "The order of evaluation is unspecified". The reason I hadn't noticed before was that most my code is rather functional. Now I was reading a char from a file handle, and peeking it as the other argument. It failed because read-char is destructive (it changes the position of the file pointer), and since the order was the other way around in the scheme I was porting to, all the procedures relying on my "read-until" method started failing left and right. It just took me ~20 years to figure it out...
      - agumonkey 10y ago
        ouch.
        sigjuice 10y ago
        Would this be an issue in Common Lisp? I believe CL function arguments are evaluated left-to-right.
        lispm 10y ago
        That's right. The standard says left to right. It's not good style to exploit that, but you can.
        fiddlerwoaroof 10y ago
        It is undefined in Common Lisp whether or not the car of a form is resolved to a function before or after the other arguments, iirc
- cmrx64 10y ago
  The parser/lexer consider the syntax of the language. Syntax is easy. Semantics is about meaning. It's quite easy to have non-clearly-defined meanings of syntactic constructs! Just write some vague language in the specification. Don't confuse the semantics of the language with the behavior of a particular implementation (eg, GCC). It's important for the language to have clear, well-defined semantics so that implementations can be compatible and programmers, compilers, analysis tools, etc can all agree on the meaning of a program. Follow some links from the page for concrete examples: https://www.cl.cam.ac.uk/~pes20/cerberus/n2090.html https://www.cl.cam.ac.uk/~pes20/cerberus/n2090.html https://www.cl.cam.ac.uk/~pes20/cerberus/n2089.html https://www.cl.cam.ac.uk/~pes20/cerberus/n2089.html And, of course, their paper, which has examples and explanations: https://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf https://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf
  - gravypod 10y ago
    My question was "If you have a computer language which has defined elements of the syntax how can you not have clearly defined meanings of combinations of the syntax?" Also, these links don't have anything that is defined in C that isn't "deterministic". I can look at all of these pieces of code and see what is happening and it's all stemming from a misinterpretation of what the standards specify, not from what a "lack of aclear and complete semantics". Some of these are also not issues at all. I have no idea what they mean to show with provenance_equality_global_yx.c. They take two pointers, change one of the values, and see if the two different pointers are equal. It's obvious in most cases this will be faults but its not an invariant. First of all, there is no guarantee for layout/ordering of data in the binary. Secondly, a pointer is a memory address. A Memory Address + 1 is just 1 sizeof(int) (in this case). If you're on a system that needs specific aligning and special datatype sizes it might even be impossible to have two ints 1 sizeof(int) away. There's no reason to think you'd be able to get the same output from that code from multiple architectures because 1) it may be impossible on some hardware and 2) it's not specified in the spec that that will work.
    - cmrx64 10y ago
      > If you're on a system that needs specific aligning and special datatype sizes it might even be impossible to have two ints 1 sizeof(int) away In this case, you're right about that, since these aren't arrays being considered. But if p is pointing to an array object of length n, with i <= n - 2, you must have &p[i] + 1 == p[i + 1], from the definition of array indexing in 6.5.2.1.2 of N1570. So, it must always be possible to have two ints 1 sizeof(int) away, otherwise it's not C. ---- The entire Cerberus research project is about finding inconsistencies between the spec, compiler implementations, and human understanding, and creating an accurate formal specification of C. They have found numerous of these. N2090 is about a spec bug, inconsistent with another WG document, and inconsistent with practice.
- zodiac 10y ago
  Unlike the other replies, I don't think they are talking about undefined behavior, I think they mean "formal semantics". The C standard documents are written in English, which might leave room for ambiguities (logical or linguistic), underspecification or inconsistencies. You can search for formal semantics (or "operational semantics", or "denotational semantics") of other languages for examples. And what the C standard calls "undefined behavior" can in theory be formalized in a very clear way (so I think it was a bad choice for them to call it "undefined behavior")
  - pandaman 10y ago
    Indeed, semantics has nothing to do with undefined behavior. Claiming that undefined behavior in C is what prevents us from defining its semantics is quite similar to the assertion that the fact that the division by 0 is not defined is the reason we cannot obtain semantics for the arithmetic notation.
- jabot 10y ago
  int f(int x, int y) { return x << y; } This is undefined for SOME values of y, namely those bigger than 31 (on platforms where int is 32 bit; adjust where different). This is caused by two facts: a) The arithmetic operation should be compiled to a hardware shift instruction where possible b) Different architectures do different things when shifting by an amount bigger than the word size: - on ARM, the "y" operand is evaluated mod 32 - on x86, if y is greater than 31, the result is 0
  - wott 10y ago
    > - on ARM, the "y" operand is evaluated mod 32 > - on x86, if y is greater than 31, the result is 0 You mixed them up, didn't you ? AFAIK, ARM does set all bits to 0 if the shift if greater than 31, but it only uses the lowest byte of the shift amount register, so it feels like a mod 256. x86[^1] does mask the lower 5 bits of the shift amount, so it feels like a mod 32. And the amount can only be 8 bits, so a 32-bit C variable must be truncated somehow. [1] except on 8086, there is no mask there, so no modulo.
qznc 10y ago
There is also the K framework, where C semantics were specified and an interpreter is generated. http://www.kframework.org/index.php/Chucky_Ellison http://www.kframework.org/index.php/Chucky_Ellison
- mafribe 10y ago
  Does this handles concurrency properly?
- nickpsecurity 10y ago
  I didn't even see you beat me to it. You should also link to KCC when you bring it up. Developers love practical stuff they can download and use to their benefit. :) https://news.ycombinator.com/item?id=14012891 https://news.ycombinator.com/item?id=14012891
JoelJacobson 10y ago
"Its front-end is written from scratch to closely follow the C11 standard, including a parser that follows the C11 standard grammar, and a typechecker." C front-end written from scratch sounds interesting. I cannot find the code for this front-end anywhere. Has anyone found it somewhere or maybe it's not released yet?
nickpsecurity 10y ago
Also see the work done in the under-utilized K Framework which captures & rejects undefined behavior as well: http://fsl.cs.illinois.edu/index.php/Defining_the_Undefinedness_of_C http://fsl.cs.illinois.edu/index.php/Defining_the_Undefinedn... Since it's K, they were able to turn it into a GCC-like compiler for you verifying things about your application. If it even compiles, you have no undefined behavior. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics On concurrency side, it's built on top of Maude tool that an inexperienced student was able to use to find errors in Eiffel's SCOOP model for concurrency. So, it can probably handle that aspect as well.
- fiddlerwoaroof 10y ago
  Any write up about the errors they found? Are they a problem with SCOOP as such or an implementation issue?
  - nickpsecurity 10y ago
    My memory is hazy but the abstract suggests this is the one I read before: http://se.ethz.ch/~meyer/publications/concurrency/scoop_maude.pdf http://se.ethz.ch/~meyer/publications/concurrency/scoop_maud... The good thing about SCOOP particularly is there was a lot of CompSci work improving on it in many ways. Most of the safer, concurrency models didn't get such attention. Example: http://cme.ethz.ch/publications/ http://cme.ethz.ch/publications/

97 points by edwintorok 10y ago

I've heard many "real" computer scientists say the "C remains central to our computing infrastructure but still lacks a clear and complete semantics" line but I have no idea what they mean. Can someone explain to me what this means to the academic-CS type? How can something with a parser & lexer not have "clear and complete semantics". If you have a computer language which has defined elements of the syntax how can you not have clearly defined meanings of combinations of the syntax? Does someone have an example of a piece of C that is not "deterministic" (best word I have for this) to a lexer & parser?

brianberns 10y ago
Example of undefined behavior: What arguments will f be called with? int i = 0; f(i++, i++); More examples here: https://www.cl.cam.ac.uk/teaching/1415/CandC++/lecture10.pdf https://www.cl.cam.ac.uk/teaching/1415/CandC++/lecture10.pdf
- gravypod 10y ago
  I'd assume it would be f(1, 0); Because function arguments are pushed in reverse order in C and funnily enough, GCC actually does that even though that's crazy. But clang catches it as an "unsequenced modification". I don't think that's a good example. The C standards make no guarantees about unsequenced modifications so relying on them is the programmer not using C, it's the programmer using a language derivative implemented by their compiler. Why do people say "C remains central to our computing infrastructure but still lacks a clear and complete semantics" when the standards are very clear about what it allows? If you use something it doesn't allow you can't blame the spec for that.
  - brianberns 10y ago
    I don't understand why you say that it's not a good example. It's legal C that has undefined semantics, which is what you were asking for.
    - gravypod 10y ago
      > It's legal C No it's not. It's undefined behavior meaning, by definition, it's not C. It's not defined in C. If I had an list of all definitions, would an undefined item be in my list? No. When you are using Undefined Behavior, you are not using C. You're using a C-extension that a compiler designer has implemented. This was done because there is no sane operation to do in these UB cases for one reason or another. Either it would not be portable or it wouldn't make sense. If there was a standard that implemented standards for UB cases it would not be portable.
      - brianberns 10y ago
        OK, so to paraphrase your position: C has clear and complete semantics because anything written in C that doesn't have clear and complete semantics is, by definition, not actually written in C. Yes? To me, that's like saying the tax code doesn't contain any loopholes, because any loopholes that it contains are, by definition, not actually part of the tax code. While amusing, I don't think this is a fruitful way to look at the problem. :)
        loeg 10y ago
        You can write things that look like C, but that doesn't make them valid C. Invalid code is just a collection of ASCII characters, I guess.
        pasquinelli 10y ago
        Does the parser reject it? That's the test for syntactically valid c.
        10y ago
  - CalChris 10y ago
    What if f is a macro. Then it has a lexically determined meaning. What if f is a function. Then it has a parsing determined meaning. What if the ++ operator has been redefined. Et cetera.
    - gravypod 10y ago
      If F is a macro then it will just be expanded. Lets say F was #define f(a, b) printf("%d %d\n", a, b); This would change absolutely nothing. A macro is just a piece of code that is expanded. It still follows all of the rules (and disallowances) of C.
      - foota 10y ago
        Fairly certain you can have compound statements as the result of the macro. e.g., the macro could expand to if(a) {printf("%d\n", b);} for example
        Normal_gaussian 10y ago
        You can. Of course you don't even need the logical connector #define f(a,b) \ f_var1 = a; \ f_var2 = b Equally you could use macros to make it a whole lot worse #define f(a,b) \ f_arr[a][b] += f_arr[b][a]
      - snovv_crash 10y ago
        What if the macro uses a and/or b more than once?
    - loeg 10y ago
      At least, the ++ operator cannot be redefined in C.
      - tathougies 10y ago
        The ability to redefine the ++ operator would not alone make it difficult to add proper semantics to the C language. What is preventing that is that no one can really describe how function application truly works in C (in terms of operation ordering), except that we all have an idea similar enough that our systems seem to work together in practice. For all the criticism Haskell gets over the purported difficulty on describing sequential computation, at least the order of monadic operations is clearly captured by the requirements to be a monad. There is no such concept for C, except that each compiler mostly seems to perform operations sequentially.
  - laughinghan 10y ago
    You're missing the point. Can we agree that people are learning a programming language that they call "C", and writing text files in that language and running programs that they call "C compilers" such as gcc on those text files to produce binary executables? You are correct to note that the programming language I'm describing does not perfectly conform to any of the documents that are ever called a "C standard". But that programming language is central to our computing infrastructure, and whether you or C standard authors like it or not that programming language is widely called "C". That language's semantics are unclear and incomplete---even though both gcc and clang are commonly called "C compilers", they have differing behavior on `f(i++, i++)` as you found; reportedly, there's code on which gcc behaves differently depending on the optimization level option.
    - zodiac 10y ago
      > You are correct to note that the programming language I'm describing does not perfectly conform to any of the documents that are ever called a "C standard". But that programming language is central to our computing infrastructure I don't agree with this. Yes, people often write code that unintentionally rely on UB/implementation-specific behavior; but are there important projects that do this intentionally? In any case, compiler authors are going to follow the C standards, not you hypothetical "C-in-practice" standards, so what good does it do to for formalize or clearly specify the latter?
      - naasking 10y ago
        > I don't agree with this. Yes, people often write code that unintentionally rely on UB/implementation-specific behavior; but are there important projects that do this intentionally? The Linux kernel.
        gravypod 10y ago
        I thought staging was the only folder with UB code.
        10y ago
  - jabot 10y ago
    > Because function arguments are pushed in reverse order in C and funnily enough, GCC actually does that even though that's crazy. Actually, pushing function arguments right-to-left means that the first argument ends up on top of the stack - and that makes vararg-style functions possible. Think about it - a called vararg method must be able find the fixed arguments to figure out how many arguments it actually gets.
    - gravypod 10y ago
      That's what I mean by "Pushed in reverse order"
  - nickpsecurity 10y ago
    While people are arguing it's syntax, you all might enjoy this parody that's a good example of Poe's Law due to C's horrid (i.e. lack of a) design: https://www.gnu.org/fun/jokes/unix-hoax.html https://www.gnu.org/fun/jokes/unix-hoax.html
- danieltillett 10y ago
  Is this example non-deterministic or just undefined? Sure you should not rely on this code to give you consistent results between compilers and even optimisation levels, but what ever happens should be consistent between runs.
  - gravypod 10y ago
    This is UB and it's caught by both GCC and Clang: $ gcc -Wall test.c test.c: In function ‘main’: test.c:12:13: warning: operation on ‘a’ may be undefined [-Wsequence-point] test(a++, a++); ~^~ $ clang test.c test.c:12:8: warning: multiple unsequenced modifications to 'a' [-Wunsequenced] test(a++, a++); ^ ~~ 1 warning generated.
    - danieltillett 10y ago
      Exactly. The OP asked for an example of a non- deterministic function not UB.
      - fmap 10y ago
        I'm not sure about non-deterministic behavior without looking it up, but you can fix this example to be implementation defined, rather than undefined like this: #include <stdio.h> int postincrement(int *x) { int y = *x; *x = y + 1; return y; } int main(int argc, char **argv) { int i = 0; printf("%d, %d\n", postincrement(&i), postincrement(&i)); return 0; } The point is that function arguments introduce sequence points, but the specification for i++ is weaker than what you get for a function call. C is full of gotchas like this...
      - pasquinelli 10y ago
        Their term was non-deterministic, but they asked for undefined behavior, because they were asking for examples of course being not fully defined semantically.
    - Keyframe 10y ago
      Exactly! Without sequence-point error, output is 1,0 on GCC6, 0,1 with CLang.
- agumonkey 10y ago
  I'm dumbfounded by all the operators of C that enable all this confusion. About the potential order of evaluation, it's not limited to C, but at least it's clearly and dilligently explained even in tiny standards like Scheme.
  - Johnny_Brahms 10y ago
    The scheme standard actually bit my sorry behind recently. I was porting a small library between scheme implementations, and my tests were failing. I had always thought it was evaluated left->right (which it was in the first scheme implementation), but it is in fact standardised as "The order of evaluation is unspecified". The reason I hadn't noticed before was that most my code is rather functional. Now I was reading a char from a file handle, and peeking it as the other argument. It failed because read-char is destructive (it changes the position of the file pointer), and since the order was the other way around in the scheme I was porting to, all the procedures relying on my "read-until" method started failing left and right. It just took me ~20 years to figure it out...
    - agumonkey 10y ago
      ouch.
      - sigjuice 10y ago
        Would this be an issue in Common Lisp? I believe CL function arguments are evaluated left-to-right.
        lispm 10y ago
        That's right. The standard says left to right. It's not good style to exploit that, but you can.
        fiddlerwoaroof 10y ago
        It is undefined in Common Lisp whether or not the car of a form is resolved to a function before or after the other arguments, iirc
cmrx64 10y ago
The parser/lexer consider the syntax of the language. Syntax is easy. Semantics is about meaning. It's quite easy to have non-clearly-defined meanings of syntactic constructs! Just write some vague language in the specification. Don't confuse the semantics of the language with the behavior of a particular implementation (eg, GCC). It's important for the language to have clear, well-defined semantics so that implementations can be compatible and programmers, compilers, analysis tools, etc can all agree on the meaning of a program. Follow some links from the page for concrete examples: https://www.cl.cam.ac.uk/~pes20/cerberus/n2090.html https://www.cl.cam.ac.uk/~pes20/cerberus/n2090.html https://www.cl.cam.ac.uk/~pes20/cerberus/n2089.html https://www.cl.cam.ac.uk/~pes20/cerberus/n2089.html And, of course, their paper, which has examples and explanations: https://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf https://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf
- gravypod 10y ago
  My question was "If you have a computer language which has defined elements of the syntax how can you not have clearly defined meanings of combinations of the syntax?" Also, these links don't have anything that is defined in C that isn't "deterministic". I can look at all of these pieces of code and see what is happening and it's all stemming from a misinterpretation of what the standards specify, not from what a "lack of aclear and complete semantics". Some of these are also not issues at all. I have no idea what they mean to show with provenance_equality_global_yx.c. They take two pointers, change one of the values, and see if the two different pointers are equal. It's obvious in most cases this will be faults but its not an invariant. First of all, there is no guarantee for layout/ordering of data in the binary. Secondly, a pointer is a memory address. A Memory Address + 1 is just 1 sizeof(int) (in this case). If you're on a system that needs specific aligning and special datatype sizes it might even be impossible to have two ints 1 sizeof(int) away. There's no reason to think you'd be able to get the same output from that code from multiple architectures because 1) it may be impossible on some hardware and 2) it's not specified in the spec that that will work.
  - cmrx64 10y ago
    > If you're on a system that needs specific aligning and special datatype sizes it might even be impossible to have two ints 1 sizeof(int) away In this case, you're right about that, since these aren't arrays being considered. But if p is pointing to an array object of length n, with i <= n - 2, you must have &p[i] + 1 == p[i + 1], from the definition of array indexing in 6.5.2.1.2 of N1570. So, it must always be possible to have two ints 1 sizeof(int) away, otherwise it's not C. ---- The entire Cerberus research project is about finding inconsistencies between the spec, compiler implementations, and human understanding, and creating an accurate formal specification of C. They have found numerous of these. N2090 is about a spec bug, inconsistent with another WG document, and inconsistent with practice.
zodiac 10y ago
Unlike the other replies, I don't think they are talking about undefined behavior, I think they mean "formal semantics". The C standard documents are written in English, which might leave room for ambiguities (logical or linguistic), underspecification or inconsistencies. You can search for formal semantics (or "operational semantics", or "denotational semantics") of other languages for examples. And what the C standard calls "undefined behavior" can in theory be formalized in a very clear way (so I think it was a bad choice for them to call it "undefined behavior")
- pandaman 10y ago
  Indeed, semantics has nothing to do with undefined behavior. Claiming that undefined behavior in C is what prevents us from defining its semantics is quite similar to the assertion that the fact that the division by 0 is not defined is the reason we cannot obtain semantics for the arithmetic notation.
jabot 10y ago
int f(int x, int y) { return x << y; } This is undefined for SOME values of y, namely those bigger than 31 (on platforms where int is 32 bit; adjust where different). This is caused by two facts: a) The arithmetic operation should be compiled to a hardware shift instruction where possible b) Different architectures do different things when shifting by an amount bigger than the word size: - on ARM, the "y" operand is evaluated mod 32 - on x86, if y is greater than 31, the result is 0
- wott 10y ago
  > - on ARM, the "y" operand is evaluated mod 32 > - on x86, if y is greater than 31, the result is 0 You mixed them up, didn't you ? AFAIK, ARM does set all bits to 0 if the shift if greater than 31, but it only uses the lowest byte of the shift amount register, so it feels like a mod 256. x86[^1] does mask the lower 5 bits of the shift amount, so it feels like a mod 32. And the amount can only be 8 bits, so a 32-bit C variable must be truncated somehow. [1] except on 8086, there is no mask there, so no modulo.

qznc 10y ago

There is also the K framework, where C semantics were specified and an interpreter is generated. http://www.kframework.org/index.php/Chucky_Ellison http://www.kframework.org/index.php/Chucky_Ellison

mafribe 10y ago
Does this handles concurrency properly?
nickpsecurity 10y ago
I didn't even see you beat me to it. You should also link to KCC when you bring it up. Developers love practical stuff they can download and use to their benefit. :) https://news.ycombinator.com/item?id=14012891 https://news.ycombinator.com/item?id=14012891

JoelJacobson 10y ago

"Its front-end is written from scratch to closely follow the C11 standard, including a parser that follows the C11 standard grammar, and a typechecker." C front-end written from scratch sounds interesting. I cannot find the code for this front-end anywhere. Has anyone found it somewhere or maybe it's not released yet?

nickpsecurity 10y ago

Also see the work done in the under-utilized K Framework which captures & rejects undefined behavior as well: http://fsl.cs.illinois.edu/index.php/Defining_the_Undefinedness_of_C http://fsl.cs.illinois.edu/index.php/Defining_the_Undefinedn... Since it's K, they were able to turn it into a GCC-like compiler for you verifying things about your application. If it even compiles, you have no undefined behavior. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics On concurrency side, it's built on top of Maude tool that an inexperienced student was able to use to find errors in Eiffel's SCOOP model for concurrency. So, it can probably handle that aspect as well.

fiddlerwoaroof 10y ago
Any write up about the errors they found? Are they a problem with SCOOP as such or an implementation issue?
- nickpsecurity 10y ago
  My memory is hazy but the abstract suggests this is the one I read before: http://se.ethz.ch/~meyer/publications/concurrency/scoop_maude.pdf http://se.ethz.ch/~meyer/publications/concurrency/scoop_maud... The good thing about SCOOP particularly is there was a lot of CompSci work improving on it in many ways. Most of the safer, concurrency models didn't get such attention. Example: http://cme.ethz.ch/publications/ http://cme.ethz.ch/publications/