3 ms·

Thank you for the write up. I'll be reading up on this more. Do you know if it models the target arch, too? Like, can it account for different architectures ha

Thank you for the write up. I'll be reading up on this more. Do you know if it models the target arch, too? Like, can it account for different architectures having different instruction reordering rules?

dandotway 5y ago
Frama-C doesn't need to know anything about the target arch. It guarantees no undefined / implementation defined behavior on all architectures. You have to prove your code does not cause overflow/underflow (or accounts for it) if you add two integers or cast a uint32_t to an int32_t, etc. Very tedious, but it can and is being done. CompCert, the formally verified C compiler, is a separate thing from Frama-C, but currently supports x86, ARM, RISC-V, and PowerPC. (CompCert is actually mostly programmed in OCaml and the Coq/Gallina proof assistant.) CompCert guarantees that a correct ISO C program (no undefined or implementation defined behavior) is translated into an assembler program with the same semantics, i.e. an assembler program that computes the same results as the C source program. So CompCert for each supported architecture needs a formal semantics for any CPU instructions it generates. CompCert is an optimizing compiler and the optimizer accounts for the delay between when an instruction is issued and when the result is ready, accounts for pipelining and all that if that is what you are asking. But to write verified C programs you don't need to worry about instruction re-ordering happening lower down changing the meaning of your program and all that. That's a deeper layer of the onion, and, as Bjarne Stroustrup said, each time you peel a layer of the onion you cry more.
- KsassPeuk 5y ago
  > Frama-C doesn't need to know anything about the target arch. In fact, it needs some knowledge, but this knowledge can be configured for the project under analysis. This is the reason why the Frama-C kernel provides the `-machdep` option ;) . Then depending on your code, you might need to add particular knowledge according to your target platform. For example validity of some hardware memory location, etc.
  - dandotway 5y ago
    For my use cases thus far, the usual C portability pitfalls haven't applied: whether char is signed or unsigned, the range of 'int', little vs. big endian, etc.
edwcross 5y ago
Frama-C works at the C semantic level, without knowledge about processor instruction-level details (expect for some extended assembly syntax, and a few details here and there). If you are talking about unspecified sequences of C statements, then Frama-C can warn about some situations, as mentioned in the user manual (https://www.frama-c.com/download/frama-c-user-manual.pdf https://www.frama-c.com/download/frama-c-user-manual.pdf): option -unspecified-access may be used to check when the evaluation of an expression depends on the order in which its sub-expressions are evaluated. For instance, this occurs with the following piece of code. int i, j, *p; i = 1; p = &i; j = i++ + (*p)++; In this code, it is unclear in which order the elements of the right-hand side of the last assignment are evaluated. Indeed, the variable j can get any value as i and p are aliased. In some cases, knowing the architecture is essential to get information such as the width of integer types. Ideally, one would like a completely system-independent, portable analysis, but this is extremely hard in C. For instance, the ISO C11 standard, in section 5.2.4.1 Translation limits, states that The implementation shall be able to translate and execute at least one program that contains at least one instance of every one of the following limits [...] 4095 characters in a string literal (after concatenation), 65535 bytes in an object, [...]. It also states that INT_MAX may be, for instance, as low as 32767. So, for a truly portable analysis, one would have to warn whenever any of these limits are reached, leading to an analysis useless except for some toy examples.

dandotway 5y ago

Frama-C doesn't need to know anything about the target arch. It guarantees no undefined / implementation defined behavior on all architectures. You have to prove your code does not cause overflow/underflow (or accounts for it) if you add two integers or cast a uint32_t to an int32_t, etc. Very tedious, but it can and is being done. CompCert, the formally verified C compiler, is a separate thing from Frama-C, but currently supports x86, ARM, RISC-V, and PowerPC. (CompCert is actually mostly programmed in OCaml and the Coq/Gallina proof assistant.) CompCert guarantees that a correct ISO C program (no undefined or implementation defined behavior) is translated into an assembler program with the same semantics, i.e. an assembler program that computes the same results as the C source program. So CompCert for each supported architecture needs a formal semantics for any CPU instructions it generates. CompCert is an optimizing compiler and the optimizer accounts for the delay between when an instruction is issued and when the result is ready, accounts for pipelining and all that if that is what you are asking. But to write verified C programs you don't need to worry about instruction re-ordering happening lower down changing the meaning of your program and all that. That's a deeper layer of the onion, and, as Bjarne Stroustrup said, each time you peel a layer of the onion you cry more.

KsassPeuk 5y ago
> Frama-C doesn't need to know anything about the target arch. In fact, it needs some knowledge, but this knowledge can be configured for the project under analysis. This is the reason why the Frama-C kernel provides the `-machdep` option ;) . Then depending on your code, you might need to add particular knowledge according to your target platform. For example validity of some hardware memory location, etc.
- dandotway 5y ago
  For my use cases thus far, the usual C portability pitfalls haven't applied: whether char is signed or unsigned, the range of 'int', little vs. big endian, etc.

edwcross 5y ago

Frama-C works at the C semantic level, without knowledge about processor instruction-level details (expect for some extended assembly syntax, and a few details here and there). If you are talking about unspecified sequences of C statements, then Frama-C can warn about some situations, as mentioned in the user manual (https://www.frama-c.com/download/frama-c-user-manual.pdf https://www.frama-c.com/download/frama-c-user-manual.pdf): option -unspecified-access may be used to check when the evaluation of an expression depends on the order in which its sub-expressions are evaluated. For instance, this occurs with the following piece of code. int i, j, *p; i = 1; p = &i; j = i++ + (*p)++; In this code, it is unclear in which order the elements of the right-hand side of the last assignment are evaluated. Indeed, the variable j can get any value as i and p are aliased. In some cases, knowing the architecture is essential to get information such as the width of integer types. Ideally, one would like a completely system-independent, portable analysis, but this is extremely hard in C. For instance, the ISO C11 standard, in section 5.2.4.1 Translation limits, states that The implementation shall be able to translate and execute at least one program that contains at least one instance of every one of the following limits [...] 4095 characters in a string literal (after concatenation), 65535 bytes in an object, [...]. It also states that INT_MAX may be, for instance, as low as 32767. So, for a truly portable analysis, one would have to warn whenever any of these limits are reached, leading to an analysis useless except for some toy examples.