4 ms·

I wonder why he mentions this TIS interpreter but not the development of complete semantics for C and specifically the k framework (https://github.com/kframewor

by jpfr 9y ago

I wonder why he mentions this TIS interpreter but not the development of complete semantics for C and specifically the k framework (https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics). Afaik, kcc is also really good at finding undefined behavior. Regehr even wrote about it in the past (https://blog.regehr.org/archives/523 https://blog.regehr.org/archives/523).

tom_mellior 9y ago
AFAIR from the last presentation on the K framework I attended (a year ago), the publicly available version of their C interpreter is incomplete: It only runs programs that don't need the standard library. That's pretty great for many things! But it's not a turnkey solution for analyzing real applications. For that they had a proprietary commercial version. (Again, this is from memory, and it may have changed.) Another reason to mention TIS-interpreter specially is that Pascal Cuoq (the co-author of this blog post) is one of its developers, and his livelihood depends on it being used.
- ellisonch 9y ago
  Original developer of the C semantics in K here! I just wanted to add a pedantic clarification (since pedantry is what semantics is all about). The semantics of the language itself is more or less complete. On top of that, a sizable portion of the standard library is given semantics directly (e.g, malloc, setjmp, stdargs, I/O including input/output to FILEs, much of printf, etc. are all formalized in the semantics). There's even basic C11 thread support. All of this runs and can be reasoned about formally. I tried to give direct semantics to the things that couldn't be (easily) written in C, because much of the standard library CAN be written in C and so it isn't so critical that it's formalized. To round out the library you can provide provide C implementations of any missing library functions at compile time (we provide some by default), and it will KCC those just like any other code. The resulting system is pretty good at catching undefined behavior, but it is super slow. I'm not involved with the commercial version, but they offer a trade off: don't do any semantic checking inside standard library calls in exchange for faster execution times. My understanding is that instead of chugging through the semantics of printf for every bottle of beer on the wall, they just call out to a native of printf. This makes things a lot faster, but it's possible you won't catch as many problems. In general, the commercial version is trying to make using the semantics practical instead of "academically slow", which was all I managed :) Any questions welcome.
  - tom_mellior 9y ago
    Thanks for the clarification! That's kind of what I remembered, but you explained it much better.

by jpfr 9y ago

tom_mellior 9y ago

AFAIR from the last presentation on the K framework I attended (a year ago), the publicly available version of their C interpreter is incomplete: It only runs programs that don't need the standard library. That's pretty great for many things! But it's not a turnkey solution for analyzing real applications. For that they had a proprietary commercial version. (Again, this is from memory, and it may have changed.) Another reason to mention TIS-interpreter specially is that Pascal Cuoq (the co-author of this blog post) is one of its developers, and his livelihood depends on it being used.

ellisonch 9y ago
Original developer of the C semantics in K here! I just wanted to add a pedantic clarification (since pedantry is what semantics is all about). The semantics of the language itself is more or less complete. On top of that, a sizable portion of the standard library is given semantics directly (e.g, malloc, setjmp, stdargs, I/O including input/output to FILEs, much of printf, etc. are all formalized in the semantics). There's even basic C11 thread support. All of this runs and can be reasoned about formally. I tried to give direct semantics to the things that couldn't be (easily) written in C, because much of the standard library CAN be written in C and so it isn't so critical that it's formalized. To round out the library you can provide provide C implementations of any missing library functions at compile time (we provide some by default), and it will KCC those just like any other code. The resulting system is pretty good at catching undefined behavior, but it is super slow. I'm not involved with the commercial version, but they offer a trade off: don't do any semantic checking inside standard library calls in exchange for faster execution times. My understanding is that instead of chugging through the semantics of printf for every bottle of beer on the wall, they just call out to a native of printf. This makes things a lot faster, but it's possible you won't catch as many problems. In general, the commercial version is trying to make using the semantics practical instead of "academically slow", which was all I managed :) Any questions welcome.
- tom_mellior 9y ago
  Thanks for the clarification! That's kind of what I remembered, but you explained it much better.