From 062da27127bc876eaeb4c728ed50bf744a3bcaa7 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 14 Oct 2020 14:25:32 +0100 Subject: [PATCH] Slides for 4xxx. --- 2020-frama-c/4000-range-is-empty-again.html | 30 +++++++++++++++++++++++++++++ 2020-frama-c/4100-range-contains-1.html | 13 +++++++++++++ 2020-frama-c/4200-range-contains-2.html | 24 +++++++++++++++++++++++ 2020-frama-c/4300-range-make-empty.html | 20 +++++++++++++++++++ 2020-frama-c/4400-range-size-1.html | 13 +++++++++++++ 2020-frama-c/4500-range-size-2.term | 12 ++++++++++++ 2020-frama-c/4600-range-size-3.html | 19 ++++++++++++++++++ 2020-frama-c/4700-range-size-4.term | 12 ++++++++++++ 2020-frama-c/4800-range-init.html | 18 +++++++++++++++++ 2020-frama-c/4850-range-init.html | 30 +++++++++++++++++++++++++++++ 2020-frama-c/4870-range-init-spec.html | 25 ++++++++++++++++++++++++ 2020-frama-c/4890-range-init-spec-2.html | 22 +++++++++++++++++++++ 12 files changed, 238 insertions(+) create mode 100644 2020-frama-c/4000-range-is-empty-again.html create mode 100644 2020-frama-c/4100-range-contains-1.html create mode 100644 2020-frama-c/4200-range-contains-2.html create mode 100644 2020-frama-c/4300-range-make-empty.html create mode 100644 2020-frama-c/4400-range-size-1.html create mode 100755 2020-frama-c/4500-range-size-2.term create mode 100644 2020-frama-c/4600-range-size-3.html create mode 100755 2020-frama-c/4700-range-size-4.term create mode 100644 2020-frama-c/4800-range-init.html create mode 100644 2020-frama-c/4850-range-init.html create mode 100644 2020-frama-c/4870-range-init-spec.html create mode 100644 2020-frama-c/4890-range-init-spec-2.html diff --git a/2020-frama-c/4000-range-is-empty-again.html b/2020-frama-c/4000-range-is-empty-again.html new file mode 100644 index 0000000..74e52f8 --- /dev/null +++ b/2020-frama-c/4000-range-is-empty-again.html @@ -0,0 +1,30 @@ + + + + +

Back to range_is_empty()

+ +
+  /*@
+    predicate valid_range(struct Range range) =
+      range.lob <= range.upb + 1;
+    predicate empty_range(struct Range range) =
+      range.lob == range.upb + 1;
+  */
+
+  /* Is range empty? */
+  /*@
+    requires \valid_read(range);
+    requires valid_range(*range);
+    assigns \nothing;
+    ensures \result <==> empty_range(*range);
+   */
+  static inline bool range_is_empty(const Range *range)
+  {
+      return range->lob > range->upb;
+  }
+
+ +
+  $ frama-c -wp -wp-rte snippets/range_is_empty.c
+
diff --git a/2020-frama-c/4100-range-contains-1.html b/2020-frama-c/4100-range-contains-1.html new file mode 100644 index 0000000..91403c9 --- /dev/null +++ b/2020-frama-c/4100-range-contains-1.html @@ -0,0 +1,13 @@ + + + + +

qemu range_contains()

+ +
+  /* Does range contain val? */
+  static inline bool range_contains(const Range *range, uint64_t val)
+  {
+      return val >= range->lob && val <= range->upb;
+  }
+
diff --git a/2020-frama-c/4200-range-contains-2.html b/2020-frama-c/4200-range-contains-2.html new file mode 100644 index 0000000..f64bb7e --- /dev/null +++ b/2020-frama-c/4200-range-contains-2.html @@ -0,0 +1,24 @@ + + + + +

qemu range_contains()

+ +
+  /*@
+    predicate value_in_range(struct Range range, uint64_t value) =
+      range.lob <= value <= range.upb;
+  */
+
+  /* Does range contain val? */
+  /*@
+    requires \valid_read(range);
+    requires valid_range(*range);
+    assigns \nothing;
+    ensures \result <==> value_in_range(*range, val);
+   */
+  static inline bool range_contains(const Range *range, uint64_t val)
+  {
+      return val >= range->lob && val <= range->upb;
+  }
+
diff --git a/2020-frama-c/4300-range-make-empty.html b/2020-frama-c/4300-range-make-empty.html new file mode 100644 index 0000000..ec8fe4c --- /dev/null +++ b/2020-frama-c/4300-range-make-empty.html @@ -0,0 +1,20 @@ + + + + +

qemu range_make_empty()

+ +
+  /* Initialize range to the empty range */
+  /*@
+    requires \valid(range);
+    requires valid_range(*range);
+    assigns *range;
+    ensures empty_range(*range);
+   */
+  static inline void range_make_empty(Range *range)
+  {
+      *range = range_empty;
+      assert(range_is_empty(range));
+  }
+
diff --git a/2020-frama-c/4400-range-size-1.html b/2020-frama-c/4400-range-size-1.html new file mode 100644 index 0000000..8af73b1 --- /dev/null +++ b/2020-frama-c/4400-range-size-1.html @@ -0,0 +1,13 @@ + + + + +

qemu range_size()

+ +
+  /* Get the size of range. */
+  static inline uint64_t range_size(const Range *range)
+  {
+      return range->upb - range->lob + 1;
+  }
+
diff --git a/2020-frama-c/4500-range-size-2.term b/2020-frama-c/4500-range-size-2.term new file mode 100755 index 0000000..7c4b874 --- /dev/null +++ b/2020-frama-c/4500-range-size-2.term @@ -0,0 +1,12 @@ +#!/bin/bash - + +source functions + +# Title. +export title="qemu’s range_size()" + +# History. +remember 'cat snippets/range_size.c' +remember 'frama-c -wp -wp-rte snippets/range_size.c' + +terminal diff --git a/2020-frama-c/4600-range-size-3.html b/2020-frama-c/4600-range-size-3.html new file mode 100644 index 0000000..28e5f5f --- /dev/null +++ b/2020-frama-c/4600-range-size-3.html @@ -0,0 +1,19 @@ + + + + +

qemu range_size() counterexample

+ +
+  /* Get the size of range. */
+  static inline uint64_t range_size(const Range *range)
+  {
+      return range->upb - range->lob + 1;
+  }
+
+
+  ┌─────────────────────────────────────────────────┐ 
+  │░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░│
+  └─────────────────────────────────────────────────┘
+  range->lob == 0           range->upb == UINT64_MAX
+
diff --git a/2020-frama-c/4700-range-size-4.term b/2020-frama-c/4700-range-size-4.term new file mode 100755 index 0000000..ade027b --- /dev/null +++ b/2020-frama-c/4700-range-size-4.term @@ -0,0 +1,12 @@ +#!/bin/bash - + +source functions + +# Title. +export title="qemu’s range_size()" + +# History. +remember 'cat snippets/range_size-good.c' +remember 'frama-c -wp -wp-rte snippets/range_size-good.c' + +terminal diff --git a/2020-frama-c/4800-range-init.html b/2020-frama-c/4800-range-init.html new file mode 100644 index 0000000..8b30bc9 --- /dev/null +++ b/2020-frama-c/4800-range-init.html @@ -0,0 +1,18 @@ + + + + +

qemu range_init_nofail()

+ +
+  /*
+   * Initialize range to span the interval [lob,lob + size - 1].
+   * size may be 0. Range must not overflow.
+   */
+  static inline void range_init_nofail(Range *range, uint64_t lob,
+                                       uint64_t size)
+  {
+      range->lob = lob;
+      range->upb = lob + size - 1;
+  }
+
diff --git a/2020-frama-c/4850-range-init.html b/2020-frama-c/4850-range-init.html new file mode 100644 index 0000000..3e9d01e --- /dev/null +++ b/2020-frama-c/4850-range-init.html @@ -0,0 +1,30 @@ + + + + +

qemu range_init_nofail()

+ +
+  /*
+   * Initialize range to span the interval [lob,lob + size - 1].
+   * size may be 0. Range must not overflow.
+   */
+  static inline void range_init_nofail(Range *range, uint64_t lob,
+                                       uint64_t size)
+  {
+      range->lob = lob;
+      range->upb = lob + size - 1;
+  }
+
+
+  lob == 0  size == 0
+  ┌─────────────────────────────────────────────────┐ 
+  │░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░│
+  └─────────────────────────────────────────────────┘
+
+
+  lob == 1  size == 0
+  ┌─────────────────────────────────────────────────┐ 
+  │ │                                               │
+  └─────────────────────────────────────────────────┘
+
diff --git a/2020-frama-c/4870-range-init-spec.html b/2020-frama-c/4870-range-init-spec.html new file mode 100644 index 0000000..a676f66 --- /dev/null +++ b/2020-frama-c/4870-range-init-spec.html @@ -0,0 +1,25 @@ + + + + +

qemu range_init_nofail() spec

+ +
+  /*@
+    requires \valid(range);
+    requires lob + (integer)size <= UINT64_MAX;
+    assigns *range;
+    behavior empty:
+      assumes lob > 0 && size == 0;
+      ensures empty_range(*range);
+    behavior non_empty:
+      assumes size > 0;
+      ensures range->lob == lob;
+      ensures size_of_bounds(lob, range->upb) == size;
+    behavior total:
+      assumes lob == 0 && size == 0;
+      ensures total_range(*range);
+    complete behaviors;
+    disjoint behaviors;
+   */
+
diff --git a/2020-frama-c/4890-range-init-spec-2.html b/2020-frama-c/4890-range-init-spec-2.html new file mode 100644 index 0000000..0db511f --- /dev/null +++ b/2020-frama-c/4890-range-init-spec-2.html @@ -0,0 +1,22 @@ + + + + +

New empty_range and total_range predicates

+ +
+  /*@ // before:
+    predicate empty_range(struct Range range) =
+      range.lob == range.upb + 1;
+  */
+
+ +
+  /*@ // after:
+    predicate empty_range(struct Range range) =
+      range.lob > 0 && range.lob == range.upb + 1;
+
+    predicate total_range(struct Range range) =
+      range.lob == 0 && range.upb == UINT64_MAX;
+  */
+
-- 1.8.3.1