Setup test suite for C backend

7 files changed, 273 insertions, 4 deletions

diff --git a/test/c/exception.expect b/test/c/exception.expect
new file mode 100644
index 00000000..79d97c6a
--- /dev/null
+++ b/test/c/exception.expect
@@ -0,0 +1,6 @@
+in g()
+g return
+Caught Estring
+test
+2nd try Caught Epair
+x = 33
diff --git a/test/c/exception.sail b/test/c/exception.sail
new file mode 100644
index 00000000..27248021
--- /dev/null
+++ b/test/c/exception.sail
@@ -0,0 +1,52 @@
+$include <flow.sail>
+
+val print = "print_endline" : string -> unit
+val print_int = "print_int" : (string, int) -> unit
+
+union exception = {
+  Epair : (range(0, 255), range(0, 255)),
+  Eunknown,
+  Estring : string
+}
+
+val f : unit -> unit effect {escape}
+
+function f () = throw(Estring("test"))
+
+val g : unit -> string effect {escape}
+
+function g () = {
+  print("in g()");
+  return("g return");
+  throw(Estring("never thrown from g"));
+}
+
+val main : unit -> unit effect {escape}
+
+function main () = {
+  try {
+    print(g());
+    f(); // will throw Estring
+    throw(Epair(42, 24));
+    throw(Eunknown);
+  } catch {
+    Eunknown     => print("Caught Eunknown"),
+    Epair(x, y)  => print("Caught Epair"),
+    Estring(str) => {
+      print("Caught Estring");
+      print(str)
+    }
+  };
+  try () catch {
+    _ => print("Unreachable!")
+  };
+  try throw(Epair(33, 1)) catch {
+    Epair(x, _)  => {
+      print("2nd try Caught Epair");
+      print_int("x = ", x);
+    },
+    _            => ()
+  };
+  f();
+  ()
+}
\ No newline at end of file
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
new file mode 100755
index 00000000..930c5bc8
--- /dev/null
+++ b/test/c/run_tests.sh
@@ -0,0 +1,83 @@
+
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+cd $DIR
+SAILDIR="$DIR/../.."
+
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[0;33m'
+NC='\033[0m'
+
+rm -f $DIR/tests.xml
+
+pass=0
+fail=0
+XML=""
+
+function green {
+    (( pass += 1 ))
+    printf "$1: ${GREEN}$2${NC}\n"
+    XML+="    <testcase name=\"$1\"/>\n"
+}
+
+function yellow {
+    (( fail += 1 ))
+    printf "$1: ${YELLOW}$2${NC}\n"
+    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
+}
+
+function red {
+    (( fail += 1 ))
+    printf "$1: ${RED}$2${NC}\n"
+    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
+}
+
+function finish_suite {
+    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
+    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
+    printf "$XML" >> $DIR/tests.xml
+    XML=""
+    pass=0
+    fail=0
+}
+
+printf "<testsuites>\n" >> $DIR/tests.xml
+
+shopt -s nullglob;
+for file in $DIR/*.sail;
+do
+    if $SAILDIR/sail -no_warn -c $file 1> ${file%.sail}.c 2> /dev/null;
+    then
+	green "compiling $(basename $file)" "ok";
+	if gcc ${file%.sail}.c -lgmp;
+	then
+	    green "compiling $(basename ${file%.sail}.c)" "ok";
+	    $DIR/a.out 1> ${file%.sail}.result 2> /dev/null;
+	    if diff ${file%.sail}.result ${file%.sail}.expect;
+	    then
+		green "executing $(basename ${file%.sail})" "ok"
+	    else
+		red "executing $(basename ${file%.sail})" "fail"
+	    fi;
+	    if valgrind -q --leak-check=full --errors-for-leak-kinds=all --error-exitcode=1 $DIR/a.out 1> /dev/null 2> /dev/null;
+	    then
+		green "executing $(basename ${file%.sail}) with valgrind" "ok"
+	    else
+		red "executing $(basename ${file%.sail}) with valgrind" "fail"
+	    fi
+	else
+	    red "compiling generated C" "fail"
+	fi
+    else
+	red "compiling $file" "fail"
+    fi;
+    rm -f ${file%.sail}.c
+    rm -r ${file%.sail}.result
+done
+
+finish_suite "C testing"
+
+printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/c/sail.h b/test/c/sail.h
new file mode 100644
index 00000000..e86dd542
--- /dev/null
+++ b/test/c/sail.h
@@ -0,0 +1,124 @@
+#ifndef SAIL_LIB
+#define SAIL_LIB
+
+#include<stdio.h>
+#include<inttypes.h>
+#include<stdlib.h>
+#include<stdbool.h>
+#include<string.h>
+#include<gmp.h>
+
+typedef int unit;
+
+#define UNIT 0
+
+typedef struct {
+  mp_bitcnt_t len;
+  mpz_t bits;
+} bv_t;
+
+typedef char *sail_string;
+
+// This function should be called whenever a pattern match failure
+// occurs. Pattern match failures are always fatal.
+void sail_match_failure(void) {
+  fprintf(stderr, "Pattern match failure\n");
+  exit(1);
+}
+
+bool not(const bool b) {
+  return !b;
+}
+
+// ***** Sail strings *****
+void init_sail_string(sail_string *str) {
+  char *istr = (char *) malloc(1 * sizeof(char));
+  istr[0] = '\0';
+  *str = istr;
+}
+
+void set_sail_string(sail_string *str1, const sail_string str2) {
+  size_t len = strlen(str2);
+  *str1 = realloc(*str1, len + 1);
+  *str1 = strcpy(*str1, str2);
+}
+
+void clear_sail_string(sail_string *str) {
+  free(*str);
+}
+
+unit print_endline(sail_string str) {
+  printf("%s\n", str);
+  return UNIT;
+}
+
+unit print_int(const sail_string str, const mpz_t op) {
+  fputs(str, stdout);
+  mpz_out_str(stdout, 10, op);
+  putchar('\n');
+  return UNIT;
+}
+
+unit print_int64(const sail_string str, const int64_t op) {
+  printf("%s%" PRId64 "\n", str, op);
+  return UNIT;
+}
+
+// ***** Multiple precision integers *****
+
+// We wrap around the GMP functions so they follow a consistent naming
+// scheme that is shared with the other builtin sail types.
+
+void set_mpz_t(mpz_t *rop, const mpz_t op) {
+  mpz_set(*rop, op);
+}
+
+void init_mpz_t(mpz_t *op) {
+  mpz_init(*op);
+}
+
+void clear_mpz_t(mpz_t *op) {
+  mpz_clear(*op);
+}
+
+void init_mpz_t_of_int64_t(mpz_t *rop, int64_t op) {
+  mpz_init_set_si(*rop, op);
+}
+
+void init_mpz_t_of_sail_string(mpz_t *rop, sail_string str) {
+  mpz_init_set_str(*rop, str, 10);
+}
+
+// ***** Sail builtins for integers *****
+
+bool eq_int(const mpz_t op1, const mpz_t op2) {
+  return !abs(mpz_cmp(op1, op2));
+}
+
+bool lt(const mpz_t op1, const mpz_t op2) {
+  return mpz_cmp(op1, op2) < 0;
+}
+
+bool gt(const mpz_t op1, const mpz_t op2) {
+  return mpz_cmp(op1, op2) > 0;
+}
+
+void add_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
+{
+  mpz_add(*rop, op1, op2);
+}
+
+void sub_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
+{
+  mpz_sub(*rop, op1, op2);
+}
+
+void neg_int(mpz_t *rop, const mpz_t op) {
+  mpz_neg(*rop, op);
+}
+
+void abs_int(mpz_t *rop, const mpz_t op) {
+  mpz_abs(*rop, op);
+}
+
+#endif
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index 370048a0..d9ae07ba 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -43,8 +43,6 @@ function finish_suite {
     fail=0
 }
 
-SAILLIBDIR="$DIR/../../lib/"
-
 printf "<testsuites>\n" >> $DIR/tests.xml
 
 for i in `ls -d */`;
diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index ab121d61..70ce4998 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -61,9 +61,9 @@ fi
 for test in $DIR/tests/*.elf; do
     if $SAILDIR/riscv/riscv "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}"
     then
-       green `basename $test` "ok"
+       green "$(basename $test)" "ok"
     else
-       red `basename $test` "fail"
+       red "$(basename $test)" "fail"
     fi
 done
 
diff --git a/test/run_tests.sh b/test/run_tests.sh
index b3224aea..45013f0d 100755
--- a/test/run_tests.sh
+++ b/test/run_tests.sh
@@ -18,6 +18,12 @@ printf "******************************************\n\n"
 ./test/ocaml/run_tests.sh
 
 printf "******************************************\n"
+printf "* C tests                                *\n"
+printf "******************************************\n\n"
+
+./test/c/run_tests.sh
+
+printf "******************************************\n"
 printf "* Lem tests                              *\n"
 printf "******************************************\n\n"