From 0101f0c6da179d503b7495c1b2d5f106b74d6425 Mon Sep 17 00:00:00 2001 From: Morgan Jones Date: Sun, 17 Oct 2021 22:32:05 -0700 Subject: [PATCH] A beginning is a very delicate time --- .gitignore | 5 ++ Makefile | 18 +++++ README.md | 4 + drawSquare.c | 217 +++++++++++++++++++++++++++++++++++++++++++++++++++ klee.nix | 39 +++++++++ shell.nix | 14 ++++ 6 files changed, 297 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 README.md create mode 100644 drawSquare.c create mode 100644 klee.nix create mode 100644 shell.nix diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..24b7a48 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +klee-* +drawSquare +drawSquare.bc +*.swo +*.swp diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..7a7d763 --- /dev/null +++ b/Makefile @@ -0,0 +1,18 @@ +all: klee + +clean: + rm -f drawSquare.bc drawSquare + +klee: drawSquare.bc drawSquare + klee drawSquare.bc + for ktest in klee-last/*.ktest; do \ + KTEST_FILE="$$ktest" ./drawSquare || true; \ + done + +drawSquare.bc: drawSquare.c + clang -emit-llvm -c -g -o $@ $(CFLAGS) $^ + +drawSquare: drawSquare.c + clang -Os -lkleeRuntest -o $@ $(CFLAGS) $^ + +.PHONY: all clean klee diff --git a/README.md b/README.md new file mode 100644 index 0000000..f36d55e --- /dev/null +++ b/README.md @@ -0,0 +1,4 @@ +# Getting started + +1. Run `nix-shell` +2. Run `make clean klee CFLAGS=-DdrawSquare=drawSquareWeird` to run `drawSquareWeird` diff --git a/drawSquare.c b/drawSquare.c new file mode 100644 index 0000000..a78f0a9 --- /dev/null +++ b/drawSquare.c @@ -0,0 +1,217 @@ +// Edit drawSquare. + +#include +#include +#include +#include + +#include + +#ifndef drawSquare +#define drawSquare drawSquareReordered +#endif + +typedef struct line { + int x0, y0, x1, y1; +} line_t; + +static line_t referenceLines[4]; +static int referenceIdx = 0; + +static line_t actualLines[4]; +static int actualIdx = 0; + +/* drawReferenceLine implementation. */ +void drawReferenceLine(int x0, int y0, int x1, int y1) { + if (referenceIdx < sizeof(referenceLines) / sizeof(line_t)) { + referenceLines[referenceIdx++] = (line_t) {x0, y0, x1, y1}; + } else { + exit(1); + } +} + +/* drawLine implementation. */ +void drawLine(int x0, int y0, int x1, int y1) { + if (actualIdx < sizeof(actualLines) / sizeof(line_t)) { + actualLines[actualIdx++] = (line_t) {x0, y0, x1, y1}; + } else { + exit(1); + } +} + +/* drawSquare implementations follow. */ + +void drawSquareWeird(int x, int y, int len) + +{ + + if(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) && len>0) + + { + + drawLine(x, y, x+len, y); + + drawLine(x+len, y, x+len, y-len); + + drawLine(x+len, y-len, x, y-len); + + drawLine(x, y-len, x, y); + + } + + else + + { + + while(len<=0) + + { + + len++; + + } + + while(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) == false) + { + + len--; + + } + + drawLine(x, y, x+len, y); + + drawLine(x+len, y, x+len, y-len); + + drawLine(x+len, y-len, x, y-len); + + drawLine(x, y-len, x, y); + } +} + +static void drawSquareAlmostCorrect(int x, int y, int len) { + if (x+len > 10){ + len = 10-x; + } + + if (y+len > 10){ + len = 10-y; + } + + drawLine(x, y, x+len, y); + + drawLine(x, y, x, y+len); + + drawLine(x+len, y, x+len, y+len); + + drawLine(x, y+len, x+len, y+len); +} + +/* Example drawSquare that's just drawReferenceSquare reordered. */ +static void drawSquareReordered(int x, int y, int len) { + if (x+len > 10){ + len = 10-x; + } + + if (y-len < 0){ + len = y; + } + + drawLine(x, y-len, x, y); + drawLine(x+len, y-len, x, y-len); + drawLine(x, y, x+len, y); + drawLine(x+len, y-len, x+len, y); +} + +/** Draws the "reference" square. */ +static void drawReferenceSquare(int x, int y, int len) { + if (x+len > 10){ + len = 10-x; + } + + if (y-len < 0){ + len = y; + } + + drawReferenceLine(x, y, x+len, y); + drawReferenceLine(x+len, y, x+len, y-len); + drawReferenceLine(x+len, y-len, x, y-len); + drawReferenceLine(x, y-len, x, y); +} + +/** Compares that the drawn square is equal to the reference square. */ +static int compareSquares(void) { + int ret = 0; + + const int numLines = sizeof(actualLines) / sizeof(line_t); + int confirmed[numLines] = {0}; + int numConfirmed = 0; + for (int actualIdx = 0; actualIdx < numLines; actualIdx++) { + line_t *actualLine = &actualLines[actualIdx]; + bool found = false; + for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) { + line_t *referenceLine = &referenceLines[referenceIdx]; + bool skipThis = false; + for (int idx = 0; idx < numConfirmed; idx++) { + if (confirmed[idx] == referenceIdx) { + skipThis = true; + break; + } + } + + if (!skipThis && ( + (actualLine->x0 == referenceLine->x0 + && actualLine->y0 == referenceLine->y0 + && actualLine->x1 == referenceLine->x1 + && actualLine->y1 == referenceLine->y1) || + (actualLine->x1 == referenceLine->x0 + && actualLine->y1 == referenceLine->y0 + && actualLine->x0 == referenceLine->x1 + && actualLine->y0 == referenceLine->y1))) { + found = true; + confirmed[numConfirmed++] = referenceIdx; + break; + } + } + if (!found) { + ret = 1; + break; + } + } + + return ret; +} + +int main() { + int x, y, len; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&y, sizeof(y), "y"); + klee_make_symbolic(&len, sizeof(len), "len"); + klee_assume(x >= 0 && x < 10 && y >= 0 && y < 10 && len > 0 && len <= 10); + + drawReferenceSquare(x, y, len); + drawSquare(x, y, len); + + int ret = compareSquares(); + + if (klee_is_replay()) { + printf("Inputs: x=%d, y=%d, len=%d\n", x, y, len); + + const int numLines = sizeof(referenceLines) / sizeof(line_t); + for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) { + line_t *referenceLine = &referenceLines[referenceIdx]; + printf("Reference: (%d, %d) -> (%d, %d)\n", referenceLine->x0, referenceLine->y0, referenceLine->x1, referenceLine->y1); + } + for (int actualIdx = 0; actualIdx < numLines; actualIdx++) { + line_t *actualLine = &actualLines[actualIdx]; + printf("Actual: (%d, %d) -> (%d, %d)\n", actualLine->x0, actualLine->y0, actualLine->x1, actualLine->y1); + } + + if (ret == 0) { + printf("All outputs matched\n"); + } else { + printf("Outputs mismatched\n"); + } + } + + return 0; +} diff --git a/klee.nix b/klee.nix new file mode 100644 index 0000000..6f6afde --- /dev/null +++ b/klee.nix @@ -0,0 +1,39 @@ +{ stdenv +, lib +, fetchFromGitHub +, cmake +, llvmPackages_9 +, clang_9 +, z3 +, stp +, cryptominisat +, gperftools +, sqlite +, gtest +, lit +, debug ? false +}: + +stdenv.mkDerivation rec { + pname = "klee"; + version = "2.2"; + src = fetchFromGitHub { + owner = "klee"; + repo = "klee"; + rev = "v${version}"; + sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M="; + }; + buildInputs = [ llvmPackages_9.llvm clang_9 z3 stp cryptominisat gperftools sqlite ]; + nativeBuildInputs = [ cmake gtest lit ]; + cmakeFlags = [ + "-DCMAKE_BUILD_TYPE=${if debug then "Debug" else "Release"}" + "-DKLEE_RUNTIME_BUILD_TYPE=${if debug then "Debug" else "Release"}" + "-DENABLE_UNIT_TESTS=ON" + "-DGTEST_SRC_DIR=${gtest.src}" + "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include" + "-DENABLE_POSIX_RUNTIME=ON" + ]; + /*testPhase = '' + make systemtests unittests + '';*/ +} diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..8552db8 --- /dev/null +++ b/shell.nix @@ -0,0 +1,14 @@ +{ pkgs ? import (builtins.fetchTarball { + name = "nixpkgs-unstable"; + url = https://github.com/NixOS/nixpkgs/archive/8f80568885d1b37cccbede85143c00711b19390c.tar.gz; + sha256 = "080cbcj4b08aa02qybf10pbf54cdvaxvgddx1w5gzrga1nacyilh"; +}) {} +}: + +let + klee = pkgs.callPackage ./klee.nix {}; +in +pkgs.stdenv.mkDerivation { + name = "ap-cs-klee"; + buildInputs = with pkgs; [ klee clang_9 gnumake ]; +}