Add summary slide about range.

[libguestfs-talks.git] / 2020-frama-c / notes.txt

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 3dbe211..43dd078 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -1,7 +1,7 @@
-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
@@ -14,6 +14,19 @@ tool.
 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:
@@ -92,22 +105,6 @@ Frama-C parsed the C code and the formal specification and machine
 checked it, and it's correct - the code is bug-free.
 
 \f
-= OVERVIEW OF FRAMA-C ECOSYSTEM =
-
-Let's interrupt this and talk about Frama-C.  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
-= BACK TO RANGE.C =
-
 Going back to what we proved so far:
 
   /*@
@@ -252,12 +249,17 @@ looks equally trivial and yet it cannot be proven.  Why?
 
 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 the version of Z3 in Fedora does not like to
-work with the version of Frama-C in Fedora
-(https://git.frama-c.com/pub/frama-c/-/issues/33).
+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:
 
@@ -400,8 +402,10 @@ point out a few things about the final proof:
    modifications, so it would be possible to maintain the annotations
    upstream, and run the proof checker as a CI test.
 
- - It probably doesn't make sense for qemu right now though, unless we
-   could prove more substantial pieces of code.
+ - It probably doesn't make sense for qemu right now though:
+   * concerted effort to prove more substantial pieces of code
+   * would need upstream effort to modularise qemu
+   * co-develop modules and proofs
 
 \f
 = POWER OF 2 =