the more relevant and small examples from asplos 2022 tutorial

system-f/stainless.conf

@@ -1,4 +1,3 @@
-compact = true
 timeout = 5
 vc-cache = false
 fail-early = true

tutorials/asplos2022/01-zip/zip.scala

@@ -0,0 +1,60 @@
+import stainless.*
+import stainless.lang.*
+
+// Immutable linked lists.
+enum List[T] {
+  case Nil()
+  case Cons(head: T, tail: List[T])
+
+  def map[U](f: T => U): List[U] =
+    this match {
+      case Nil()            => Nil()
+      case Cons(head, tail) => Cons(f(head), tail.map(f))
+    }
+
+  def size: BigInt = {
+    this match {
+      case Nil()         => BigInt(0)
+      case Cons(_, tail) => BigInt(1) + tail.size
+    }
+  } ensuring (res => res >= 0 && res != -1)
+
+  def sizeFact: Unit = {
+    ()
+  } ensuring(_ => size != -1)
+
+  // NOTE: Adding the postcondition to size is crucial since it allows
+  //   us to conclude that *both* xs and ys are Nil when we know that
+  //   xs.size == ys.size and *either* xs *or* ys is Nil. (This is
+  //   what we need to complete the proof of zip below.)
+}
+
+import List._
+
+
+// A particular list consisting of elements 1, 2 and 3.
+val xs: List[Int] = Cons(1, Cons(2, Cons(3, Nil())))
+
+
+// The usual zip function with specifications.
+def zip(xs: List[Int], ys: List[Boolean]): List[(Int, Boolean)] = {
+  require(xs.size == ys.size)
+  (xs, ys) match {
+    case (Cons(x, xs0), Cons(y, ys0)) =>
+      Cons((x, y), zip(xs0, ys0))
+    case _ =>
+      Nil[(Int, Boolean)]()
+  }
+} ensuring ( res =>   res.map(_._1) == xs &&
+              res.map(_._2) == ys)
+
+// same zip but with weaker require and ensuring
+def zipL(xs: List[Int], ys: List[Boolean]): List[(Int, Boolean)] = {
+  require(xs.size <= ys.size)
+  (xs, ys) match {
+    case (Cons(x, xs0), Cons(y, ys0)) =>
+      Cons((x, y), zipL(xs0, ys0))
+    case _ =>
+      Nil[(Int, Boolean)]()
+  }
+} ensuring ( res =>   res.map(_._1) == xs)

tutorials/asplos2022/02-stack/Stack.scala

@@ -0,0 +1,44 @@
+import stainless.*
+import stainless.collection.List
+import stainless.lang.*
+
+case class Stack[T](private var data: List[T])
+{
+  def list: List[T] = { data }
+
+  def push(a: T): Unit = {
+    data = a :: data
+  } ensuring(_ => list == a :: old(this).list)
+
+  def pop: T = {
+    require(!list.isEmpty)
+    val a = data.head
+    data = data.tail
+    a
+  } ensuring (res =>
+    res == old(this).list.head &&
+    list == old(this).list.tail)
+}
+object Stack {
+  def empty[T]() = Stack[T](List[T]())
+}
+object TestStack {
+  def pushTwo(s: Stack[Int], a: Int, b: Int) = {
+    s.push(b)
+    s.push(a)
+    s.pop
+  } ensuring(res => res == a)
+
+  def pushTwoPopTwo(s1: Stack[Int], s2: Stack[Int]): Unit = {
+    s1.push(1)
+    s2.push(2)
+    s1.pop
+    s2.pop
+    ()
+  }
+
+  // Not allowed in default imperative as we use aliased parameters
+  def callTwoStacks(s: Stack[Int]): Unit = {
+    pushTwoPopTwo(s, s)
+  }
+}

tutorials/asplos2022/02-stack/StackAliased.scala

@@ -0,0 +1,58 @@
+import stainless.lang._
+import stainless.collection._
+import stainless.annotation._
+import stainless.proof._
+import stainless.lang.StaticChecks._
+
+// A version of the Stack example that uses the "full" imperative mode.
+// In this mode instances of `Stack` may be aliased.
+object StackAliasedExample {
+  case class Stack[T](private var data: List[T]) extends AnyHeapRef {
+    def list = {
+      reads(Set(this))
+      data
+    }
+
+    def push(a: T): Unit = {
+      reads(Set(this))
+      modifies(Set(this))
+
+      data = a :: data
+    } ensuring(_ => list == a :: old(list))
+
+    def pop: T = {
+      reads(Set(this))
+      modifies(Set(this))
+      require(!list.isEmpty)
+
+      val n = data.head
+      data = data.tail
+      n
+    } ensuring (res => res == old(list).head &&
+                       list == old(list).tail)
+  }
+
+  // Unless we require s1 != s2, the function below fails to verify, because s1 and s2 may point to
+  // the same Stack, in which case the second call to pop might fail.
+  def popBoth[T](s1: Stack[T], s2: Stack[T]): (T, T) = {
+    reads(Set(s1, s2))
+    modifies(Set(s1, s2))
+    require(s1 != s2 && !s1.list.isEmpty && !s2.list.isEmpty)
+    (s1.pop, s2.pop)
+  }
+
+  def pushTwoPopTwo(s1: Stack[Int], s2: Stack[Int]): Unit = {
+    reads(Set(s1, s2))
+    modifies(Set(s1, s2))
+    s1.push(1)
+    s2.push(2)
+    s1.pop
+    s2.pop
+    ()
+  }
+  def callTwoStacks(st: Stack[Int]): Unit = {
+    reads(Set(st))
+    modifies(Set(st))
+    pushTwoPopTwo(st, st)
+  }
+}

tutorials/asplos2022/02-stack/stainless.conf

@@ -0,0 +1,7 @@
+vc-cache = true
+timeout = 1
+strict-arithmetic = false
+batched = true
+solvers = "smt-z3"
+infer-measures = false
+check-measures = false

tutorials/asplos2022/02-stack/verify-StackAliased.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# kill subprocesses on exit or kill
+trap '[ -n "$(jobs -pr)" ] && kill -9 $(jobs -pr)' SIGINT SIGTERM EXIT
+
+../stainless/stainless.sh --no-colors --full-imperative --timeout=3 StackAliased.scala "$@"

tutorials/asplos2022/02-stack/verify.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# kill subprocesses on exit or kill
+trap '[ -n "$(jobs -pr)" ] && kill -9 $(jobs -pr)' SIGINT SIGTERM EXIT
+
+../stainless/stainless.sh --no-colors Stack.scala "$@"

tutorials/asplos2022/03-rgba/.gitignore

@@ -0,0 +1,5 @@
+stainless.h
+stainless.c
+stainless.h.gch
+SPixel
+~

tutorials/asplos2022/03-rgba/Pixel.scala

@@ -0,0 +1,24 @@
+object Pixel {   
+    def r(px: Int): Byte = ((px >>> 24) & 0xff).toByte
+
+    def g(px: Int): Byte = ((px >>> 16) & 0xff).toByte
+
+    def b(px: Int): Byte = ((px >>> 8) & 0xff).toByte
+
+    def a(px: Int): Byte = (px & 0xff).toByte
+
+    def fromRgba0(r: Byte, g: Byte, b: Byte, a: Byte): Int = {
+      // Incorrect version, albeit seemingly correct
+      (r << 24) | (g << 16) | (b << 8) | a
+    }.ensuring(res => Pixel.r(res) == r && Pixel.g(res) == g && Pixel.b(res) == b && Pixel.a(res) == a)
+
+    def example01 = g(fromRgba0(0,-128,8,0))
+
+    // correct version
+    def fromRgba(r: Byte, g: Byte, b: Byte, a: Byte): Int = {
+      (r << 24) | ((g << 16) & 0xffffff) | ((b << 8) & 0xffff) | (a & 0xff)
+    }.ensuring(res => Pixel.r(res) == r && Pixel.g(res) == g && Pixel.b(res) == b && Pixel.a(res) == a) 
+
+    def example1 = g(fromRgba(10,20,30,0))
+}
+

tutorials/asplos2022/03-rgba/SPixel.scala

@@ -0,0 +1,36 @@
+import stainless.*
+import stainless.lang.*
+import stainless.annotation.*
+
+object Pixel {   
+    @cCode.`export`
+    def r(px: Int): Byte = ((px >>> 24) & 0xff).toByte
+
+    @cCode.`export`
+    def g(px: Int): Byte = ((px >>> 16) & 0xff).toByte
+
+    @cCode.`export`
+    def b(px: Int): Byte = ((px >>> 8) & 0xff).toByte
+
+    @cCode.`export`
+    def a(px: Int): Byte = (px & 0xff).toByte
+
+    @cCode.`export`
+    def fromRgba0(r: Byte, g: Byte, b: Byte, a: Byte): Int = {
+      // Incorrect version, albeit seemingly correct
+      (r << 24) | (g << 16) | (b << 8) | a
+    }.ensuring(res => Pixel.r(res) == r && Pixel.g(res) == g && Pixel.b(res) == b && Pixel.a(res) == a)
+
+    // Above is wrong because the sub-expressions (g << 16), etc. get promoted to Int and are sign-extended.
+
+    @cCode.`export`
+    def example0 = g(fromRgba0(10,20,-128,0))
+
+    @cCode.`export`
+    def fromRgba(r: Byte, g: Byte, b: Byte, a: Byte): Int = {
+      (r << 24) | ((g << 16) & 0xffffff) | ((b << 8) & 0xffff) | (a & 0xff)
+    }.ensuring(res => Pixel.r(res) == r && Pixel.g(res) == g && Pixel.b(res) == b && Pixel.a(res) == a)
+
+    @cCode.`export`
+    def example = g(fromRgba(10,20,-128,0))
+}

tutorials/asplos2022/03-rgba/common.scala

@@ -0,0 +1,72 @@
+import stainless.*
+import stainless.lang.*
+import stainless.annotation._
+
+object common {
+  object Pixel {
+    @cCode.`export`
+    def r(px: Int): Byte = ((px >>> 24) & 0xff).toByte
+
+    @cCode.`export`
+    def g(px: Int): Byte = ((px >>> 16) & 0xff).toByte
+
+    @cCode.`export`
+    def b(px: Int): Byte = ((px >>> 8) & 0xff).toByte
+
+    @cCode.`export`
+    def a(px: Int): Byte = (px & 0xff).toByte
+
+    @cCode.`export`
+    def fromRgba(r: Byte, g: Byte, b: Byte, a: Byte): Int = {
+      (r << 24) | ((g << 16) & 0xffffff) | ((b << 8) & 0xffff) | (a & 0xff)
+      // Incorrect version, albeit seemingly correct:
+      //  (r << 24) | (g << 16) | (b << 8) | a
+      // This is due to the fact that the sub-expressions (g << 16), etc. get promoted to Int and are sign-extent.
+    }.ensuring(res => Pixel.r(res) == r && Pixel.g(res) == g && Pixel.b(res) == b && Pixel.a(res) == a)
+
+    @cCode.`export`
+    def incremented(px: Int)(dr: Byte = 0, dg: Byte = 0, db: Byte = 0, da: Byte = 0): Int = {
+      fromRgba(((Pixel.r(px) + dr) & 0xff).toByte, ((Pixel.g(px) + dg) & 0xff).toByte, ((Pixel.b(px) + db) & 0xff).toByte, ((Pixel.a(px) + da) & 0xff).toByte)
+    }.ensuring(res =>
+      Pixel.r(res) == ((Pixel.r(px) + dr) & 0xff).toByte &&
+      Pixel.g(res) == ((Pixel.g(px) + dg) & 0xff).toByte &&
+      Pixel.b(res) == ((Pixel.b(px) + db) & 0xff).toByte &&
+      Pixel.a(res) == ((Pixel.a(px) + da) & 0xff).toByte)
+
+    // withRgba is a convenience wrapper around fromRgba that returns a copy of a pixel with selected modified channels.
+    // Example:
+    //   val px: Int = ...
+    //   val px2 = Pixel.withRgba(px)(g = 123, b = 3) // Same as px, except with G=123 and B=3
+    @cCode.`export`
+    def withRgba(px: Int)(r: Byte = Pixel.r(px), g: Byte = Pixel.g(px), b: Byte = Pixel.b(px), a: Byte = Pixel.a(px)): Int =
+      fromRgba(r, g, b, a)
+  }
+
+  /////////////////////////////////////////////////////////////////////////////////////////////////////
+
+  @cCode.`export`
+  def write16(data: Array[Byte], i: Int, value: Short): Unit = {
+    require(data.length >= 2 && i >= 0 && i < data.length - 1)
+    data(i) = ((0xff00 & value) >>> 8).toByte
+    data(i + 1) = (0xff & value).toByte
+  }.ensuring(_ => read16(data, i) == value && old(data).length == data.length)
+
+  @cCode.`export`
+  def write32(data: Array[Byte], i: Int, value: Int): Unit = {
+    require(data.length >= 4 && i >= 0 && i < data.length - 3)
+    write16(data, i, (value >>> 16).toShort)
+    write16(data, i + 2, value.toShort)
+  }.ensuring(_ => read32(data, i) == value && old(data).length == data.length)
+
+  @cCode.`export`
+  def read16(data: Array[Byte], i: Int): Short = {
+    require(data.length >= 2 && i >= 0 && i < data.length - 1)
+    (((((data(i) & 0xff) << 8) & 0xffff) | (data(i + 1) & 0xff)) & 0xffff).toShort
+  }
+
+  @cCode.`export`
+  def read32(data: Array[Byte], i: Int): Int = {
+    require(data.length >= 4 && i >= 0 && i < data.length - 3)
+    (read16(data, i) << 16) | (read16(data, i + 2) & 0xffff)
+  }
+}

tutorials/asplos2022/03-rgba/gcc.sh

@@ -0,0 +1 @@
+gcc stainless.h stainless.c main.c -o SPixel

tutorials/asplos2022/03-rgba/genc.sh

@@ -0,0 +1,3 @@
+#!/bin/bash
+../stainless/stainless.sh --genc SPixel.scala
+

tutorials/asplos2022/03-rgba/main.c

@@ -0,0 +1,8 @@
+#include <stdio.h>
+#include "stainless.h"
+
+int main() {
+  printf("example0 = %d\n", example0());
+  printf("example = %d\n", example());
+  return 0;
+}

tutorials/asplos2022/03-rgba/stainless.conf

@@ -0,0 +1,6 @@
+vc-cache = true
+timeout = 15
+strict-arithmetic = false
+batched = true
+solvers = "smt-z3"
+infer-measures = false

tutorials/asplos2022/03-rgba/verify-common.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# kill subprocesses on exit or kill
+trap '[ -n "$(jobs -pr)" ] && kill -9 $(jobs -pr)' SIGINT SIGTERM EXIT
+
+../stainless/stainless.sh common.scala "$@"

tutorials/asplos2022/03-rgba/verify-pixel.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# kill subprocesses on exit or kill
+trap '[ -n "$(jobs -pr)" ] && kill -9 $(jobs -pr)' SIGINT SIGTERM EXIT
+
+../stainless/stainless.sh Pixel.scala "$@"

tutorials/asplos2022/03-rgba/verify-spixel.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# kill subprocesses on exit or kill
+trap '[ -n "$(jobs -pr)" ] && kill -9 $(jobs -pr)' SIGINT SIGTERM EXIT
+
+../stainless/stainless.sh SPixel.scala "$@"