Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Defining the Undefinedness of C (2015) [pdf]

fsl.cs.illinois.edu

Post reply on HN
Print view View original

21–30 of 91 posts

Re: Defining the Undefinedness of C (2015) [pdf]

#21

Post by masklinn »

iainmerrick wrote: post #11
xrange wrote: post #5

Earlier quoted context omitted.

>Here's something I'd love to know about undefined behavior in C: is this something specific to C, or is it something that any similar language would have to contend with? How similar is similar? Pascal? Ada? Spark Ada? Rust? Friendly C ( https://blog.regehr.org/archives/1180 )?

Yes, I'd say those are similar. Systems languages, no mandatory GC. That Friendly C proposal is terrific, I'd dearly love to use that. Basically, use sane and conservative optimizations for most code, with the option of using aggressive optimizations for hotspots. Kind of similar to Rust -- mostly safe by default, more dangerous stuff available when you need it.

IIRC Safe Rust has no UB, `unsafe` does, according to the Nomicon:

* Dereferencing null or dangling pointers

* Reading uninitialized memory

* Breaking the pointer aliasing rules

* Producing invalid primitive values:

- dangling/null references

- a bool that isn't 0 or 1

- an undefined enum discriminant

- a char outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF]

- A non-utf8 str

* Unwinding into another language

* Causing a data race

These are all guarantees unsafe code must uphold or there are no guarantees anymore.

IIRC LLVM IR also has UBs.

Re: Defining the Undefinedness of C (2015) [pdf]

#22

Post by nickpsecurity »

That team’s awesome. One of few groups in formal methods using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. They also build their own modified logic called matching logic on top that they claim is better than separation logic.

http://www.kframework.org/index.php/Main_Page

More interesting, their use of these tools allowed them to make their C semantics executable in a style similar to GCC:

https://github.com/kframework/c-semantics

I want this group to do one for Rust and SPARK as a reference spec for certifying compilers for those. Also useful for the diverse compilation concept to counter Karger's compiler/compiler subversion. On a side note, they also have a company that they use to fund and apply their work:

https://runtimeverification.com/

Re: Defining the Undefinedness of C (2015) [pdf]

#23

Post by iainmerrick »

masklinn wrote: post #21
iainmerrick wrote: post #11

Earlier quoted context omitted.

Yes, I'd say those are similar. Systems languages, no mandatory GC. That Friendly C proposal is terrific, I'd dearly love to use that. Basically, use sane and conservative optimizations for most code, with the option of using aggressive optimizations for hotspots. Kind of similar to Rust -- mostly safe by default, more dangerous stuff available when you need it.

IIRC Safe Rust has no UB, `unsafe` does, according to the Nomicon: * Dereferencing null or dangling pointers * Reading uninitialized memory * Breaking the pointer aliasing rules * Producing invalid primitive values: - dangling/null references - a bool that isn't 0 or 1 - an undefined enum discriminant - a char outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] - A non-utf8 str * Unwinding into another language *…

I wonder if it's possible to sneak UB into normal "safe" Rust code, by leveraging LLVM optimizations?

Re: Defining the Undefinedness of C (2015) [pdf]

#24

Post by simias »

iainmerrick wrote: post #20
simias wrote: post #12

Earlier quoted context omitted.

It could let the compiler get rid of entire branches if it can statically assert than an overflow or other UB is guaranteed (assuming that it's not a coding error but that the check is done somewhere upstream and the branch would be unreachable). That might seem a bit aggressive and risky but it's not rare to write funky macro code where you hope the compiler will be clever enough to get rid of the cruft. One case I…

So that "next = a + 1" is essentially a note to the compiler, promising that "++a" won't overflow? To me that seems really reckless! If you need that note, make it a compiler pragma or something, rather than trying to sneak it in by repurposing some existing code. Now if overflow were implementation-defined, the compiler would have to assume that INT_MAX + 1 wraps to INT_MIN (say). So as written, the "if (a == INT_MA…

I wouldn't write code like this on purpose, rather I'd genuinely need "next" for some other computation and the compiler could then use that to infer that I know "a" not to overflow. If I wanted to make it an "annotation" then I'd use "assert(a This is a very simple example of course, but maybe this "increment" code is actually used in many other parts of the codebase where the test actually makes sense.

It's not rare for instance to start a C function with "if (param == NULL) return;", just in case. If the compiler inlines the function and sees that the caller dereferences "param" it can assume that it's not null and remove the test.

But you're right that it makes it easy to shoot yourself in the foot. I remember a strange bug in the linux kernel source that was "hidden" by such an optimization, the code looked something like that:

    int bar(somestruct *ptr) {
        int somevalue = ptr->val;

        if (ptr == NULL) {
            return -EINVAL;
        }

        // Rest of the function here
    }
The real code was a little more complicated than that obviously, but at a glance it might look that the function won't run if "ptr" is NULL. GCC however noticed the dereference before the test and happily decided that "of course this coder knows what they're doing, ptr can't be NULL!" and removed it.

It can take a while to debug code like that.

Re: Defining the Undefinedness of C (2015) [pdf]

#25

Post by littlestymaar »

iainmerrick wrote: post #7
simias wrote: post #4

Earlier quoted context omitted.

Any language which allows unprotected memory access will potentially have "undefined behaviour" if you start plowing through random addresses. Things like divisions by 0 are also commonly UB. Some CPU ABI even have instructions which, when used with certain operands, are undefined. For instance the ARM Thumb "BL" instruction is encoded as two successive "pseudo-instructions", IIRC if you break the pair the behaviour…

Yeah, it's not at all clear to me why so many things need to be undefined rather than implementation-defined.

Undefined means : the compiler can omit this case and assume it never happens. Take integer overflow for instance: an implementation-defined behavior means in case of overflow the compiler can either wrap, crash, or have a saturation at max value. Undefined behavior means the compiler can assume it doesn't happen and optimize with this information in mind.

For instance, the following code :

    for(i = 0; i
With the undefined behavior, the compiler assume that j will never overflow, which means it can re-order the loops if he wants, or unfold it, or any other optimization if he desires so. But if it takes the possible overflow into account, it cannot optimize anything since the inner loop could be an infinite loop if `max` is big enough.

Re: Defining the Undefinedness of C (2015) [pdf]

#27

Post by simias »

kps wrote: post #9
iainmerrick wrote: post #2

Here's something I'd love to know about undefined behavior in C: is this something specific to C, or is it something that any similar language would have to contend with? It seems like problems crop up when you combine a fairly low-level language with an emphasis on performance, a specification that explicitly calls out implementation-defined and undefined semantics, and very highly optimizing compilers. None of the…

I think it was an unintended consequence of the wording chosen by the ANSI C89 committee. The reality of pre-ANSI C was that if you wrote ‘+’, the expectation was that you'd get the target machine's ‘add’ instruction, no more and no less. It might overflow, it might not; it might crash or hang your machine on overflow or trap values — but that is all your problem, not the language's or compiler's. I worked on a comme…

That's a good explanation for invalid memory accesses and divisions by zero but I'm not aware of many architectures where addition overflow traps (it can trap on MIPS but there's an other instruction that simply wraps around). That being said I don't have an encyclopedic knowledge of instruction sets.

I could be wrong though, after all compilers back then were a lot less clever than now so maybe they couldn't really make use of this information. I'd be curious to get a first hand testimony as to why certain UB exist in the first place.

Re: Defining the Undefinedness of C (2015) [pdf]

#28

Post by bbatha »

kps wrote: post #9
iainmerrick wrote: post #2

Here's something I'd love to know about undefined behavior in C: is this something specific to C, or is it something that any similar language would have to contend with? It seems like problems crop up when you combine a fairly low-level language with an emphasis on performance, a specification that explicitly calls out implementation-defined and undefined semantics, and very highly optimizing compilers. None of the…

I think it was an unintended consequence of the wording chosen by the ANSI C89 committee. The reality of pre-ANSI C was that if you wrote ‘+’, the expectation was that you'd get the target machine's ‘add’ instruction, no more and no less. It might overflow, it might not; it might crash or hang your machine on overflow or trap values — but that is all your problem, not the language's or compiler's. I worked on a comme…

I've never really understood why this couldn't be slotted in as "implementation defined behavior". `add` has a well defined meaning on every platform just because it differs shouldn't give the compiler license to change the meaning of my program for that platform. It should however platform specific optimizations based on overflow, etc.

Could somebody provide me with an example of truly undefinable behavior? (Perhaps data races?)

Re: Defining the Undefinedness of C (2015) [pdf]

#29

Post by bbatha »

iainmerrick wrote: post #23
masklinn wrote: post #21

Earlier quoted context omitted.

IIRC Safe Rust has no UB, `unsafe` does, according to the Nomicon: * Dereferencing null or dangling pointers * Reading uninitialized memory * Breaking the pointer aliasing rules * Producing invalid primitive values: - dangling/null references - a bool that isn't 0 or 1 - an undefined enum discriminant - a char outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] - A non-utf8 str * Unwinding into another language *…

I wonder if it's possible to sneak UB into normal "safe" Rust code, by leveraging LLVM optimizations?

Its totally possible, but its considered a compiler bug if it does happen. In the same way that its possible to segfault java if there's a bug in the jit. There's an on going project to verify the semantics of the Rust language and its safe abstractions[0] which should make it easier to choose which optimizations are legal.

0: http://plv.mpi-sws.org/rustbelt/

Re: Defining the Undefinedness of C (2015) [pdf]

#30

Post by Manishearth »

iainmerrick wrote: post #23
masklinn wrote: post #21

Earlier quoted context omitted.

IIRC Safe Rust has no UB, `unsafe` does, according to the Nomicon: * Dereferencing null or dangling pointers * Reading uninitialized memory * Breaking the pointer aliasing rules * Producing invalid primitive values: - dangling/null references - a bool that isn't 0 or 1 - an undefined enum discriminant - a char outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] - A non-utf8 str * Unwinding into another language *…

I wonder if it's possible to sneak UB into normal "safe" Rust code, by leveraging LLVM optimizations?

Assuming no compiler bugs, no.

UB isn't something "caused" by optimizations, it's something that exists in the code before optimizations, optimizations can just trigger nasal demons. So you shouldn't be able to write UB in safe Rust assuming no compiler bugs.

(And assuming that any unsafe libraries being leveraged are bug free)

Post reply on HN