4 ms·

I never see anyone do this, but it doesn't seem like a bad idea to run a program through a C interpreter and see if it ever triggers undefined behavior. As I un

I never see anyone do this, but it doesn't seem like a bad idea to run a program through a C interpreter and see if it ever triggers undefined behavior. As I understand it, the C standard is written so that all undefined behavior is able to be caught in this manner. I could even see something like gcc coming with a 'create an interpreted executable for debugging purposes' flag. It wouldn't constitute a formal proof or anything, but it would solve the problem of people leaving overflow and null pointer checks in plain sight expecting them to be hit.

eloff 11y ago
There's also ubsan: http://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html http://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html
throwaway2048 11y ago
Undefined behaviour isn't a set of checks the compiler goes through before deciding to call invoke_nasal_demons() which you can then just replace with yell_loudly_about_UB(). Undefined behaviour is a set of conditions that the standard says they can pretend do not occur, ever, so certain results are easier to obtain because the UB is never checked for and assumed to have not occurred. UB is fundamentally not a well defined condition because it is the absence of knowledge about the state of a program, and many UB conditions are very very hard to detect if not actually impossible (cf Turing) which is why the standard says the compiler doesn't have to care to begin with. Its very nature means detecting UB in anything approaching a reliable way is impossible, the C standard is not remotely compatable with such an idea.
- deleted 11y ago
  [deleted]
zodiac 11y ago
But while running your C program through the C interpreter, what user input would you give your C program?
- MichaelBurge 11y ago
  If it's easy, then you could just run the program as normal with a few test cases. If you're a web browser for example, use it to browse some web pages. If you're a BitTorrent client, use it to download some Linux ISOs. If the interpreter limits the external resources available[1], then you'd have to rephrase the guts of your C program as a pure computation. Then if you had a program for rendering HTML files into BMP files, I would collect a couple examples and run it with them as input. If necessary, you could embed the test data into a .c file that exercises the rendering code and remove any dependency on user input. "Just run the program" doesn't constitute a correctness proof. And if you have access to kernel functions at all, I'm sure there's a way to rewrite your own code at runtime while not invoking undefined behavior. It looks like CompCert C's formally verified C Interpreter[1] only allows print, free, and malloc as external resources. [1] http://compcert.inria.fr/man/manual004.html http://compcert.inria.fr/man/manual004.html
  - zodiac 11y ago
    But if the test cases you run it on are not comprehensive enough, the behavior of your program might be undefined when run on user input, but not be undefined when run on your test cases.

eloff 11y ago

There's also ubsan: http://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html http://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html

throwaway2048 11y ago

Undefined behaviour isn't a set of checks the compiler goes through before deciding to call invoke_nasal_demons() which you can then just replace with yell_loudly_about_UB(). Undefined behaviour is a set of conditions that the standard says they can pretend do not occur, ever, so certain results are easier to obtain because the UB is never checked for and assumed to have not occurred. UB is fundamentally not a well defined condition because it is the absence of knowledge about the state of a program, and many UB conditions are very very hard to detect if not actually impossible (cf Turing) which is why the standard says the compiler doesn't have to care to begin with. Its very nature means detecting UB in anything approaching a reliable way is impossible, the C standard is not remotely compatable with such an idea.

deleted 11y ago
[deleted]

zodiac 11y ago

But while running your C program through the C interpreter, what user input would you give your C program?

MichaelBurge 11y ago
If it's easy, then you could just run the program as normal with a few test cases. If you're a web browser for example, use it to browse some web pages. If you're a BitTorrent client, use it to download some Linux ISOs. If the interpreter limits the external resources available[1], then you'd have to rephrase the guts of your C program as a pure computation. Then if you had a program for rendering HTML files into BMP files, I would collect a couple examples and run it with them as input. If necessary, you could embed the test data into a .c file that exercises the rendering code and remove any dependency on user input. "Just run the program" doesn't constitute a correctness proof. And if you have access to kernel functions at all, I'm sure there's a way to rewrite your own code at runtime while not invoking undefined behavior. It looks like CompCert C's formally verified C Interpreter[1] only allows print, free, and malloc as external resources. [1] http://compcert.inria.fr/man/manual004.html http://compcert.inria.fr/man/manual004.html
- zodiac 11y ago
  But if the test cases you run it on are not comprehensive enough, the behavior of your program might be undefined when run on user input, but not be undefined when run on your test cases.