From 263a44294225fe9b2ab4974c56b5fca0a28574df Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Wed, 14 Oct 2020 13:14:09 +0100
Subject: [PATCH 1/1] Slides for 2xxx.

---
 2020-frama-c/2000-range-intro.term      | 14 ++++++++++++++
 2020-frama-c/2100-range-struct.html     | 31 +++++++++++++++++++++++++++++++
 2020-frama-c/2200-range-predicates.html | 23 +++++++++++++++++++++++
 2020-frama-c/2300-range-is-empty.term   | 12 ++++++++++++
 2020-frama-c/notes.txt                  |  4 ++--
 2020-frama-c/run                        | 10 ++++++++--
 2020-frama-c/style.css                  |  3 +++
 7 files changed, 93 insertions(+), 4 deletions(-)
 create mode 100755 2020-frama-c/2000-range-intro.term
 create mode 100644 2020-frama-c/2100-range-struct.html
 create mode 100644 2020-frama-c/2200-range-predicates.html
 create mode 100755 2020-frama-c/2300-range-is-empty.term

diff --git a/2020-frama-c/2000-range-intro.term b/2020-frama-c/2000-range-intro.term
new file mode 100755
index 0000000..eda773a
--- /dev/null
+++ b/2020-frama-c/2000-range-intro.term
@@ -0,0 +1,14 @@
+#!/bin/bash -
+
+source functions
+
+# Title.
+export title="qemu"
+
+# History.
+remember 'wc -l util/*.c | sort -nr | tail -20'
+remember 'ls -l util/range.c include/qemu/range.h'
+
+pushd ~/d/qemu >/dev/null
+terminal
+popd >/dev/null
diff --git a/2020-frama-c/2100-range-struct.html b/2020-frama-c/2100-range-struct.html
new file mode 100644
index 0000000..ced14e4
--- /dev/null
+++ b/2020-frama-c/2100-range-struct.html
@@ -0,0 +1,31 @@
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<h1>Range type</h1>
+
+<pre class="code">
+<span class="comment">/*
+ * Operations on 64 bit address ranges.
+ * Notes:
+ * - Ranges must not wrap around 0, but can include UINT64_MAX.
+ */</span>
+struct Range {
+    <span class="comment">/*
+     * Do not access members directly, use the functions!
+     * A non-empty range has @lob <= @upb.
+     * An empty range has @lob == @upb + 1.
+     */</span>
+    uint64_t lob;        <span class="comment">/* inclusive lower bound */</span>
+    uint64_t upb;        <span class="comment">/* inclusive upper bound */</span>
+};
+typedef struct Range Range;
+</pre>
+
+<pre>
+┌─────┬─────────┬──────── ── ── ──
+│     │         │
+└─────┴─────────┴──────── ── ── ──
+       ↑       ↑
+       lob   upb
+</pre>
diff --git a/2020-frama-c/2200-range-predicates.html b/2020-frama-c/2200-range-predicates.html
new file mode 100644
index 0000000..f9cd68a
--- /dev/null
+++ b/2020-frama-c/2200-range-predicates.html
@@ -0,0 +1,23 @@
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<h1>Range predicates</h1>
+
+<pre class="code">
+    <span class="comment">/*
+     * Do not access members directly, use the functions!
+     * A non-empty range has @lob <= @upb.
+     * An empty range has @lob == @upb + 1.
+     */</span>
+</pre>
+
+<pre class="code">
+  /*@
+    predicate valid_range(struct Range range) =
+      range.lob <= range.upb + 1;
+
+    predicate empty_range(struct Range range) =
+      range.lob == range.upb + 1;
+  */
+</pre>
diff --git a/2020-frama-c/2300-range-is-empty.term b/2020-frama-c/2300-range-is-empty.term
new file mode 100755
index 0000000..09c6e27
--- /dev/null
+++ b/2020-frama-c/2300-range-is-empty.term
@@ -0,0 +1,12 @@
+#!/bin/bash -
+
+source functions
+
+# Title.
+export title="qemu"
+
+# History.
+remember 'cat snippets/range_is_empty.c'
+remember 'frama-c -wp -wp-rte snippets/range_is_empty.c'
+
+terminal
diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 4b15f26..733cba8 100644
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -70,7 +70,7 @@ Notice a few things here:
 
  - 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:
 
@@ -82,7 +82,7 @@ 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:
 
diff --git a/2020-frama-c/run b/2020-frama-c/run
index d6333b0..48148e4 100755
--- a/2020-frama-c/run
+++ b/2020-frama-c/run
@@ -15,9 +15,15 @@ export GNOME_KEYRING_PID=
 # Clean up after previous run.
 talkdir=$PWD ./restore
 
+# Check environment.
+if ! test -d ~/d/qemu ; then
+    echo "\$HOME/d/qemu must exist"
+    exit 1
+fi
+
 # Precreate any files necessary.
 #(nothing)
 
 # Run techtalk.
-techtalk-pse
-#~/d/techtalk-pse/techtalk-pse
+techtalk-pse "$@"
+#~/d/techtalk-pse/techtalk-pse "$@"
diff --git a/2020-frama-c/style.css b/2020-frama-c/style.css
index 093a8b7..414f374 100644
--- a/2020-frama-c/style.css
+++ b/2020-frama-c/style.css
@@ -71,6 +71,9 @@ pre.code {
 code {
     color: rgb(238,0,0);
 }
+span.comment {
+    color: rgb(238,0,0);
+}
 
 /* Bullet points */
 li {
-- 
1.8.3.1