-16th Nov 2020
+Monday 16th Nov 2020
Formally proving tiny bits of qemu using Frama-C
-[in medias res]
+\f
In early October I was talking to one of the developers of Frama-C,
which is a modular framework for verifying C programs. It's been on
I will provide links to tutorials etc at the end.
\f
+= OVERVIEW OF FRAMA-C ECOSYSTEM =
+
+The name stands for "Framework for Static Analysis of the C language".
+
+It's modular, with a core program that reads C source code
+and turns it into Abstract Syntax Trees. And a set of plugins
+to do static analysis by annotating these syntax trees.
+Plugins can cooperate, so analysis can be passed between
+plugins.
+
+The following slides are taken from David Mentré‘s 2016 presentation.
+
+\f
I decided to spend a day or two last month seeing if I could formally
prove some code inside qemu, and I arbitrarily picked one of the
smallest pieces of code in the "util/" subdirectory:
- I'm using structs directly from the C code.
- - The comments in the upstream code translate into predicates.
+ - The upstream comments translate into machine-checkable code.
The first upstream function is:
and using the predicates we can write a specification:
- $ less snippets/range_is_empty.c
+ $ cat snippets/range_is_empty.c
And we can compile and prove that:
checked it, and it's correct - the code is bug-free.
\f
-= OVERVIEW OF FRAMA-C ECOSYSTEM =
-
-
-XXX Modular Framework for analysis of C
-
-XXX Take some slides from David Mentre's presentation.
-
-XXX Explain which companies are using Frama-C.
-
-XXX WP plugin
-
-XXX ACSL language
-
-
-
-\f
-= BACK TO RANGE.C =
-
Going back to what we proved so far:
/*@
One way to find the problem would be to find a COUNTEREXAMPLE. A
counterexample is an instance of an input that satisfies all of the
-preconditions, but makes the postcondition false. Now Frama-C has
+preconditions, but makes the postcondition false. Frama-C has
pluggable provers, and one prover called Z3, originally written by
Microsoft, can be used with Frama-C and can sometimes find
-counterexamples. However for some reason the version of Z3 in Fedora
-does not like to work with the version of Frama-C in Fedora and I
-don't know why.
+counterexamples.
+
+ $ frama-c -wp -wp-rte snippets/range_size.c -wp-prover alt-ergo,why3:z3-ce
+
+Unfortunately Z3 cannot find a counterexample in this case. I even
+upped the timeout to run Z3 longer but it still couldn't find one.
+
+[Z3 model_compact issue: https://git.frama-c.com/pub/frama-c/-/issues/33]
So this is the counterexample which I worked out myself: