Add learning exercises

.github/workflows/ci.yml

@@ -571,6 +571,39 @@ jobs:
           chmod +x bin/*
           make ${{ matrix.s2n-target }}
 
+  exercises:
+    name: "Test SAW exercises"
+    needs: build
+    runs-on: ubuntu-22.04
+    strategy:
+      matrix:
+        ghc: ["8.10.7"]
+    steps:
+      - uses: actions/checkout@v2
+      - run: |
+          mkdir -p exercises/bin
+
+      - name: Download previously-built SAW
+        uses: actions/download-artifact@v2
+        with:
+          name: "${{ runner.os }}-bins"
+          path: ./exercises/bin
+
+      - uses: satackey/[email protected]
+        continue-on-error: true
+
+      - shell: bash
+        name: "make exercises container"
+        working-directory: exercises
+        run: docker build -t exercises .
+
+      - shell: bash
+        name: "run exercises"
+        working-directory: exercises
+        run: |
+          chmod +x bin/*
+          docker run -v $PWD/bin:/saw-bin exercises
+
   # Indicates sufficient CI success for the purposes of mergify merging the pull
   # request, see .github/mergify.yml. This is done instead of enumerating each
   # instance of each job in the mergify configuration for a number of reasons:
@@ -585,5 +618,6 @@ jobs:
       - saw-remote-api-tests
       - cabal-test
       - s2n-tests
+      - exercises
     steps:
       - run: "true"

exercises/.dockerignore

@@ -0,0 +1 @@
+bin

exercises/.gitignore

@@ -0,0 +1 @@
+*.bc

exercises/Dockerfile

@@ -0,0 +1,11 @@
+FROM ubuntu:22.04
+
+RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
+RUN apt-get update && apt-get install -y clang-12 make
+
+RUN find /usr/bin/ -name "*-12" -exec basename {} \; | sed "s/\-12//" | xargs -I{} ln -s /usr/bin/'{}'-12 /usr/bin/'{}'
+
+COPY . /workdir
+
+ENTRYPOINT [ "/workdir/ci-entrypoint.sh" ]
+CMD [ "/bin/bash" ]

exercises/README.md

@@ -0,0 +1,44 @@
+# SAW Exercises #
+
+This directory contains exercises to help SAW learners gain confidence in their
+proof writing abilities by working on simple, well-defined proofs.  Each
+exercise folder contains a well-commented `exercise.saw` file containing
+problems to work on, as well as a `solutions.saw` file with a sample solution.
+Some exercises have more than one valid solution, though the `solutions.saw`
+file will only list one.  We designed the exercises to be completed in
+following order:
+
+1. `memory-safety/popcount`
+2. `memory-safety/swap`
+3. `memory-safety/u128`
+4. `memory-safety/point`
+5. `functional-correctness/popcount`
+6. `functional-correctness/u128`
+7. `functional-correctness/point`
+8. `functional-correctness/swap`
+9. `sha512`
+
+You'll also find a `salsa20` exercise in the `memory-safety` and
+`functional-correctness` folders.  Unlike the other exercises, these exercises
+lack an `exercise.saw` file.  It is an opportunity to test what you've learned
+to write a proof from scratch.  The `salsa20` proofs are simpler than the
+`sha512` proof, but the challenge comes from writing a proof without any
+signposting or helper functions.
+
+## Building Bitcode ##
+
+To run the exercises and solutions, you'll first need to build the bitcode for
+all of the C programs.  To do this, simply run the `Makefile` in `common`:
+
+```bash
+cd common
+make
+```
+
+## Continuous Integration (CI) ##
+
+To ensure these exercises stay up to date, we have integrated them with our CI
+system.  Our CI runs the `ci-entrypoint.sh` script in a docker container
+defined by `Dockerfile`, which in term runs SAW over all of the exercises and
+solutions.  This script and docker image are not intended to be used outside of
+a CI system.

exercises/ci-entrypoint.sh

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+set -xe
+
+# This script checks all of the exercise and solution files.  It is only
+# intended to be executed by the saw-script CI system.
+
+cd /workdir
+mkdir bin
+cp /saw-bin/saw bin/saw
+cp /saw-bin/abc bin/abc
+cp /saw-bin/yices bin/yices
+cp /saw-bin/yices-smt2 bin/yices-smt2
+cp /saw-bin/z3 bin/z3
+chmod +x bin/*
+
+export PATH=/workdir/bin:$PATH
+
+abc -h || true
+z3 --version
+yices --version
+yices-smt2 --version
+
+# Build bitcode for all C programs
+(cd common && make)
+
+# Run SAW over all exercises and solutions
+find . -name solution.saw -o -name exercise.saw | xargs -I % sh -c "saw % || exit 255"

exercises/common/Makefile

@@ -0,0 +1,10 @@
+.SUFFIXES: .c .bc
+.PHONY: all
+
+C_FILES = $(shell find .. -name '*.c')
+BC_FILES = $(patsubst %.c, %.bc, $(C_FILES))
+
+all: $(BC_FILES)
+
+%.bc : %.c
+	clang -g -O0 -c -emit-llvm $< -o $@

exercises/common/helpers.saw

@@ -0,0 +1,60 @@
+/*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+ * SAW helpers
+ */
+// Given a value `v` of type `ty`, allocates and returns a pointer to memory
+// storing `v`
+let alloc_init ty v = do {
+  p <- crucible_alloc ty;
+  crucible_points_to p v;
+  return p;
+};
+
+// Given a value `v` of type `ty`, allocates and returns a read only pointer to
+// memory storing `v`
+let alloc_init_readonly ty v = do {
+  p <- crucible_alloc_readonly ty;
+  crucible_points_to p v;
+  return p;
+};
+
+// Given a name `n` and a type `ty`, allocates a fresh variable `x` of type
+// `ty` and returns a tuple of `x` and a pointer to `x`.
+let ptr_to_fresh n ty = do {
+  x <- crucible_fresh_var n ty;
+  p <- alloc_init ty (crucible_term x);
+  return (x, p);
+};
+
+// Given a name `n` and a type `ty`, allocates a fresh variable `x` of type
+// `ty` and returns a tuple of `x` and a read only pointer to `x`.
+let ptr_to_fresh_readonly n ty = do {
+  x <- crucible_fresh_var n ty;
+  p <- alloc_init_readonly ty (crucible_term x);
+  return (x, p);
+};
+
+// Given a name `n` and a value `v`, assert that the `n` has a value of `v`
+let global_points_to n v = do {
+  crucible_points_to (crucible_global n) (crucible_term v);
+};
+
+// Given a name `n` and a value `v`, declare that n is initialized, and assert that has value v
+let global_alloc_init n v = do {
+  crucible_alloc_global n;
+  global_points_to n v;
+};
+
+// llvm integer type aliases
+let i8 = llvm_int 8;
+let i16 = llvm_int 16;
+let i32 = llvm_int 32;
+let i64 = llvm_int 64;
+let i128 = llvm_int 128;
+let i384 = llvm_int 384;
+let i512 = llvm_int 512;
+

exercises/functional-correctness/complete-examples/add/add.c

@@ -0,0 +1,3 @@
+#include <stdint.h>
+
+uint32_t add(uint32_t x, uint32_t y) { return x + y; }

exercises/functional-correctness/complete-examples/add/solution.saw

@@ -0,0 +1,21 @@
+let add_spec = do {
+     // Create fresh variables for `x` and `y`
+     x <- llvm_fresh_var "x" (llvm_int 32);
+     y <- llvm_fresh_var "y" (llvm_int 32);
+
+     // Invoke the function with the fresh variables
+     llvm_execute_func [llvm_term x, llvm_term y];
+
+     // The function returns a value containing the sum of x and y
+     llvm_return (llvm_term {{ x + y }});
+};
+
+// Load LLVM bitcode to verify
+m <- llvm_load_module "add.bc";
+
+// Verify the `add` function satisfies its specification
+llvm_verify m "add" [] true add_spec (do {
+     //simplify (cryptol_ss());
+     //print_goal;
+     z3;
+});

exercises/functional-correctness/point/Point.cry

@@ -0,0 +1,12 @@
+module Point where
+
+type Point = {x : [32], y : [32]}
+
+POINT_ZERO : Point
+POINT_ZERO = zero
+
+point_add : Point -> Point -> Point
+point_add p1 p2 = { x = p1.x + p2.x, y = p1.y + p2.y }
+
+point_add_commutes : Point -> Point -> Bit
+property point_add_commutes p1 p2 = point_add p1 p2 == point_add p2 p1

exercises/functional-correctness/point/exercise.saw

@@ -0,0 +1,87 @@
+///////////////////////////////////////////////////////////////////////////////
+// Exercise: Point Functional Correctness
+///////////////////////////////////////////////////////////////////////////////
+
+
+include "../../common/helpers.saw";
+import "Point.cry";
+
+m <- llvm_load_module "point.bc";
+
+///////////////////////////////////////////////////////////////////////////////
+// Part 1: Simple Point Equality
+///////////////////////////////////////////////////////////////////////////////
+
+// Convert the memory safety spec below into a functional correctness
+// specification.
+
+// You can specify the values in a struct by using llvm_struct_value:
+//     llvm_struct_value [ <field_0>, <field_1>, ... <field_n> ];
+
+let point_eq_spec = do {
+    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point");
+    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point");
+
+    llvm_execute_func [p1_ptr, p2_ptr];
+
+    ret <- llvm_fresh_var "ret" (llvm_int 1);
+    llvm_return (llvm_term ret);
+};
+
+point_eq_ov <- llvm_verify m "point_eq" [] true point_eq_spec z3;
+
+///////////////////////////////////////////////////////////////////////////////
+// Part 2: Point Allocation
+///////////////////////////////////////////////////////////////////////////////
+
+// Convert the memory safety proofs below into functional correctness proofs.
+
+let point_new_spec = do {
+    p_x <- llvm_fresh_var "p_x" (llvm_int 32);
+    p_y <- llvm_fresh_var "p_y" (llvm_int 32);
+
+    llvm_execute_func [ llvm_term p_x, llvm_term p_y ];
+
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    llvm_return ret_ptr;
+};
+
+point_new_ov <- llvm_verify m "point_new" [] true point_new_spec z3;
+
+let point_copy_spec = do {
+    (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_struct "struct.point");
+
+    llvm_execute_func [p_ptr];
+
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    llvm_return ret_ptr;
+};
+
+point_copy_ov <- llvm_verify m "point_copy" [point_new_ov] true point_copy_spec z3;
+
+///////////////////////////////////////////////////////////////////////////////
+// Part 3: Point Addition
+///////////////////////////////////////////////////////////////////////////////
+
+// Convert the memory safety proof below into a proof that the C `point_add`
+// function is equivalent to the Cryptol `point_add` function  in Point.cry.
+
+let point_add_spec = do {
+    llvm_alloc_global "ZERO";
+    zero_global <- llvm_fresh_var "zero_global" (llvm_struct "struct.point");
+    llvm_points_to (llvm_global "ZERO") (llvm_term zero_global);
+
+    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point");
+    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point");
+
+    llvm_execute_func [p1_ptr, p2_ptr];
+
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    llvm_return ret_ptr;
+};
+
+llvm_verify m "point_add"
+    [point_new_ov, point_copy_ov, point_eq_ov]
+    true
+    point_add_spec
+    z3;

exercises/functional-correctness/point/point.c

@@ -0,0 +1,42 @@
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct point {
+    uint32_t x;
+    uint32_t y;
+} point;
+
+point ZERO = {0, 0};
+
+// Check whether two points are equal
+bool point_eq(const point *p1, const point *p2) {
+    return p1->x == p2->x && p1->y == p2-> y;
+}
+
+// Allocate and return a new point
+point* point_new(uint32_t x, uint32_t y) {
+    point* ret = malloc(sizeof(point));
+    ret->x = x;
+    ret->y = y;
+    return ret;
+}
+
+// Return a new point containing a copy of `p`
+point* point_copy(const point* p) {
+    return point_new(p->x, p->y);
+}
+
+// Add two points
+point* point_add(const point *p1, const point *p2) {
+    // Save an addition by checking for zero
+    if (point_eq(p1, &ZERO)) {
+        return point_copy(p2);
+    }
+
+    if (point_eq(p2, &ZERO)) {
+        return point_copy(p1);
+    }
+
+    return point_new(p1->x + p2->x, p1->y + p2->y);
+}