State-of-art in correctness made by compilers

4 min readAug 29, 2022

"I reject beauty, I want formalism!" Kevin Buzzard about the future of mathematics with Proof assistants.

Nobody wants to bring out bad software, even though it results in a lot of complexity. But in real-life, this is a cost-benefit trade-off between going into the market and proof-making time [4]. Maybe your killer dating app doesn’t need it, but nuclear power plants have to.

Since your software must be free of defects and compilers have shown like a tool that sheds out static and dynamic bugs from program analysis, your modern compiler plays a critical role in automatic program verification and correctness in order to be free of defects [1].

Debugger, unit testing, and similar techniques have been helpful techniques. However, they are not enough, instead one should prove it by specifications and it checked by a computer program.

Compiler verification

You have to prove your high-level system works but who verifies your compiler? must you trust it?

This was set out by Jonh McCarthy and James Painter, so it is an old problem [9]. Today, applied research is about using Proof assistants such as Coq or Lean Prover in order to check semantics preservation, equivalence preservation, and full abstraction by two approaches: logical relations and bisimulation [10]. For instance, the closed-world project CompCert is a particular subset of C and was entirely proved within the Coq proof assistant based on constructive type theory from axiomatic semantics [8]. Others used the interactive theorem prover Lean and Concrete Semantics [11].

On the other hand, security concerns about compiler correctness, have you asked yourself if your compiler is secure? In other words, is your compiler introducing security errors by optimizations?. This situation is called the correctness-security gap, which formally means that a compiler optimization introduces security errors, indeed not by source code, but compiler itself [3].

Frama-C [12]

Assuming your compiler has been proven and is secure, can your compiler verify your critical software?

We introduce you to an open-source C compiler called Frama-C that makes your software safer analyzing your code by Why3; it helps you to prove your software’s correctness.

Frama-C is contract-based, has functional properties, and allows extension with plugins. You’re going to test both of them: eva and wp.

Installation

Because installing software is hard, you set out framac/frama-c by Docker.

docker run framac/frama-c:25.0 frama-c --help

Hello world

And now write down example from docs:

int i, t[10];void main(void) {
          for (i=0; i<=8+2; i++)
                  t[i] = i;
}

Run it

docker run -v $(pwd):/working -w /working framac/frama-c:25.0 frama-c -eva rte.c

You must see:

Dijkstra’s Weakest Precondition Calculus

And now write down example from docs:

#include <stddef.h>
/*@
  requires \valid(a+(0..n-1));assigns  a[0..n-1];ensures
  \forall integer i;
    0 <= i < n ==> a[i] == 0;
*/
void set_to_0(int* a, size_t n){
  size_t i;/*@
    loop invariant 0 <= i <= n;
    loop invariant
    \forall integer j;
      0 <= j < i ==> a[j] == 0;
    loop assigns i, a[0..n-1];
    loop variant n-i;
  */
  for(i = 0; i < n; ++i)
    a[i] = 0;
}int main() {
        int x[5] = {1, 1, 1, 1, 1};
        set_to_0(x, 5);
        return 0;
}

Run wp:

docker run -v $(pwd):/working -w /working framac/frama-c:25.0 frama-c -wp introduction_acsl.c

https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf

[1] Mary Hall, D. P. (2009, February 01). Compiler Research: The Next 50 Years | February 2009 | Communications of the ACM. Retrieved from https://cacm.acm.org/magazines/2009/2/19325-compiler-research-the-next-50-years/fulltext

[2] Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; Avigad, Jeremy; de Moura, Leonardo (2017). A metaprogramming framework for formal verification. Proceedings of the ACM on Programming Languages, 1(ICFP), 1–29. doi:10.1145/3110278

[3] V. D’Silva, M. Payer and D. Song, “The Correctness-Security Gap in Compiler Optimization,” 2015 IEEE Security and Privacy Workshops, 2015, pp. 73–87, doi: 10.1109/SPW.2015.33.

[4] Moshe Y. Vardi; (2021). Program verification . Communications of the ACM, (), –. doi:10.1145/3469113

[5] M. Y. Vardi, “Program Verification: a 70+- Year History,” 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE), 2021, pp. 1–2, doi: 10.1109/TASE52547.2021.00011.

[6] Filliâtre, JC. (2012). Verifying Two Lines of C with Why3: An Exercise in Program Verification. In: Joshi, R., Müller, P., Podelski, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2012. Lecture Notes in Computer Science, vol 7152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27705-4_8

[7] Schäfer, S., Schneider, S., & Smolka, G. (2016). Axiomatic semantics for compiler verification. CPP 2016: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. Association for Computing Machinery. doi: 10.1145/2854065.2854083

[8] Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (July 2009), 107–115. https://doi.org/10.1145/1538788.1538814

[9] Daniel Patterson and Amal Ahmed. 2019. The next 700 compiler correctness theorems (functional pearl). Proc. ACM Program. Lang. 3, ICFP, Article 85 (August 2019), 29 pages. https://doi.org/10.1145/3341689

[10] Phillip Mates :: An Introduction to Compiler Verification. (2022, August 29). Retrieved from https://www.ccs.neu.edu/home/mates/articles/compiler-verification-intro.html

[11] Okawa Ericson, L. (2021). Simple formally verified compiler in Lean (Dissertation). Retrieved from http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-459205