Merge branch 'sail2' into mono-tweaks

10 files changed, 246 insertions, 49 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 53775166..d57fd559 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -90,13 +90,38 @@ val tdiv_int = {
 } : (int, int) -> int
 
 /*! Remainder for truncating division (has sign of dividend) */
-val tmod_int = {
+val _tmod_int = {
   ocaml: "tmod_int",
   interpreter: "tmod_int",
   lem: "tmod_int",
   c: "tmod_int",
   coq: "Z.rem"
-} : (int, int) -> nat
+} : (int, int) -> int
+
+/*! If we know the second argument is positive, we know the result is positive */
+val _tmod_int_positive = {
+  ocaml: "tmod_int",
+  interpreter: "tmod_int",
+  lem: "tmod_int",
+  c: "tmod_int",
+  coq: "Z.rem"
+} : forall 'n, 'n >= 1. (int, int('n)) -> nat
+
+overload tmod_int = {_tmod_int_positive, _tmod_int}
+
+function fdiv_int(n: int, m: int) -> int = {
+  if n < 0 & m > 0 then {
+    tdiv_int(n + 1, m) - 1
+  } else if n > 0 & m < 0 then {
+    tdiv_int(n - 1, m) - 1
+  } else {
+    tdiv_int(n, m)
+  }
+}
+
+function fmod_int(n: int, m: int) -> int = {
+  n - (m * fdiv_int(n, m))
+}
 
 val abs_int_plain = {
   smt : "abs",
diff --git a/lib/coverage/Cargo.toml b/lib/coverage/Cargo.toml
new file mode 100644
index 00000000..f4fdf1d7
--- /dev/null
+++ b/lib/coverage/Cargo.toml
@@ -0,0 +1,11 @@
+[package]
+name = "sail-coverage"
+version = "0.1.0"
+authors = ["Alasdair <alasdair.armstrong@cl.cam.ac.uk>"]
+edition = "2018"
+
+[dependencies]
+lazy_static = "1.4.0"
+
+[lib]
+crate-type = ["staticlib"]
diff --git a/lib/coverage/Makefile b/lib/coverage/Makefile
new file mode 100644
index 00000000..55ed9fdc
--- /dev/null
+++ b/lib/coverage/Makefile
@@ -0,0 +1,3 @@
+libsail_coverage.a: src/*.rs Cargo.toml Makefile
+	cargo build --release
+	cp target/release/libsail_coverage.a .
diff --git a/lib/coverage/src/lib.rs b/lib/coverage/src/lib.rs
new file mode 100644
index 00000000..003f8b88
--- /dev/null
+++ b/lib/coverage/src/lib.rs
@@ -0,0 +1,132 @@
+extern crate lazy_static;
+use lazy_static::lazy_static;
+
+use std::collections::HashSet;
+use std::ffi::{CStr, CString};
+use std::fs::{OpenOptions, File};
+use std::io::Write;
+use std::os::raw::{c_char, c_int};
+use std::sync::Mutex;
+
+#[derive(Eq, PartialEq, Hash)]
+struct Span {
+    sail_file: CString,
+    line1: i32,
+    char1: i32,
+    line2: i32,
+    char2: i32,
+}
+
+lazy_static! {
+    static ref BRANCHES: Mutex<HashSet<Span>> = Mutex::new(HashSet::new());
+    static ref FUNCTIONS: Mutex<HashSet<Span>> = Mutex::new(HashSet::new());
+}
+
+fn function_entry(_function_name: &CStr, span: Span) {
+    FUNCTIONS.lock().unwrap().insert(span);
+}
+
+fn branch_taken(_branch_id: i32, span: Span) {
+    BRANCHES.lock().unwrap().insert(span);
+}
+
+fn branch_reached(_branch_id: i32, _span: Span) {
+    ()
+}
+
+fn write_locations(file: &mut File, kind: char, spans: &Mutex<HashSet<Span>>) -> bool {
+    for span in spans.lock().unwrap().iter() {
+        let res = write!(
+            file,
+            "{} \"{}\", {}, {}, {}, {}\n",
+            kind,
+            span.sail_file.to_string_lossy(),
+            span.line1,
+            span.char1,
+            span.line2,
+            span.char2,
+        );
+        if res.is_err() {
+            return false;
+        }
+    };
+    true
+}
+
+#[no_mangle]
+pub extern "C" fn sail_coverage_exit() -> c_int {
+    if let Ok(mut file) = OpenOptions::new().create(true).append(true).open("sail_coverage") {
+        if !write_locations(&mut file, 'B', &BRANCHES) {
+            return 1
+        }
+        if !write_locations(&mut file, 'F', &FUNCTIONS) {
+            return 1
+        }
+        0
+    } else {
+        1
+    }
+}
+
+#[no_mangle]
+pub unsafe extern "C" fn sail_function_entry(
+    function_name: *const c_char,
+    sail_file: *const c_char,
+    l1: c_int,
+    c1: c_int,
+    l2: c_int,
+    c2: c_int,
+) {
+    function_entry(
+        CStr::from_ptr(function_name),
+        Span {
+            sail_file: CStr::from_ptr(sail_file).into(),
+            line1: l1 as i32,
+            char1: c1 as i32,
+            line2: l2 as i32,
+            char2: c2 as i32,
+        },
+    )
+}
+
+#[no_mangle]
+pub unsafe extern "C" fn sail_branch_taken(
+    branch_id: c_int,
+    sail_file: *const c_char,
+    l1: c_int,
+    c1: c_int,
+    l2: c_int,
+    c2: c_int,
+) {
+    branch_taken(
+        branch_id as i32,
+        Span {
+            sail_file: CStr::from_ptr(sail_file).into(),
+            line1: l1 as i32,
+            char1: c1 as i32,
+            line2: l2 as i32,
+            char2: c2 as i32,
+        },
+    )
+}
+
+#[no_mangle]
+pub unsafe extern "C" fn sail_branch_reached(
+    branch_id: c_int,
+    sail_file: *const c_char,
+    l1: c_int,
+    c1: c_int,
+    l2: c_int,
+    c2: c_int,
+) {
+    branch_reached(
+        branch_id as i32,
+        Span {
+            sail_file: CStr::from_ptr(sail_file).into(),
+            line1: l1 as i32,
+            char1: c1 as i32,
+            line2: l2 as i32,
+            char2: c2 as i32,
+        },
+    )
+}
diff --git a/lib/rts.c b/lib/rts.c
index edae3965..f0ae149c 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -1,28 +1,15 @@
-#include<string.h>
-#include<getopt.h>
-#include<inttypes.h>
+#include <string.h>
+#include <getopt.h>
+#include <inttypes.h>
 
-#include"sail.h"
-#include"rts.h"
-#include"elf.h"
+#include "sail.h"
+#include "rts.h"
+#include "elf.h"
 
 static uint64_t g_elf_entry;
 uint64_t g_cycle_count = 0;
 static uint64_t g_cycle_limit;
 
-void sail_match_failure(sail_string msg)
-{
-  fprintf(stderr, "Pattern match failure in %s\n", msg);
-  exit(EXIT_FAILURE);
-}
-
-unit sail_assert(bool b, sail_string msg)
-{
-  if (b) return UNIT;
-  fprintf(stderr, "Assertion failed: %s\n", msg);
-  exit(EXIT_FAILURE);
-}
-
 unit sail_exit(unit u)
 {
   fprintf(stderr, "[Sail] Exiting after %" PRIu64 " cycles\n", g_cycle_count);
diff --git a/lib/rts.h b/lib/rts.h
index 68d01cb5..1ba48d59 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -1,22 +1,12 @@
-#pragma once
+#ifndef SAIL_RTS_H
+#define SAIL_RTS_H
 
-#include<inttypes.h>
-#include<stdlib.h>
-#include<stdio.h>
+#include <inttypes.h>
+#include <stdlib.h>
+#include <stdio.h>
 
-#include"sail.h"
-
-/*
- * This function should be called whenever a pattern match failure
- * occurs. Pattern match failures are always fatal.
- */
-void sail_match_failure(sail_string msg);
-
-/*
- * sail_assert implements the assert construct in Sail. If any
- * assertion fails we immediately exit the model.
- */
-unit sail_assert(bool b, sail_string msg);
+#include "sail.h"
+#include "sail_failure.h"
 
 unit sail_exit(unit);
 
@@ -169,3 +159,5 @@ void cleanup_rts(void);
 
 unit z__SetConfig(sail_string, sail_int);
 unit z__ListConfig(const unit u);
+
+#endif
diff --git a/lib/sail.h b/lib/sail.h
index fbbce541..0c9b18b5 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -1,12 +1,13 @@
-#pragma once
+#ifndef SAIL_H
+#define SAIL_H
 
-#include<inttypes.h>
-#include<stdlib.h>
-#include<stdio.h>
-#include<stdbool.h>
-#include<gmp.h>
+#include <inttypes.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdbool.h>
+#include <gmp.h>
 
-#include<time.h>
+#include <time.h>
 
 static inline void *sail_malloc(size_t size)
 {
@@ -73,7 +74,7 @@ bool UNDEFINED(bool)(const unit);
  */
 typedef char *sail_string;
 
-SAIL_BUILTIN_TYPE(sail_string);
+SAIL_BUILTIN_TYPE(sail_string)
 
 void dec_str(sail_string *str, const mpz_t n);
 void hex_str(sail_string *str, const mpz_t n);
@@ -98,7 +99,7 @@ uint64_t sail_int_get_ui(const sail_int);
 
 #define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__)
 
-SAIL_BUILTIN_TYPE(sail_int);
+SAIL_BUILTIN_TYPE(sail_int)
 
 void CREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
 void RECREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
@@ -198,7 +199,7 @@ typedef struct {
 typedef uint64_t mach_bits;
 typedef lbits sail_bits;
 
-SAIL_BUILTIN_TYPE(lbits);
+SAIL_BUILTIN_TYPE(lbits)
 
 void CREATE_OF(lbits, fbits)(lbits *,
 			     const fbits op,
@@ -360,7 +361,7 @@ sbits sub_sbits(const sbits op1, const sbits op2);
 
 typedef mpq_t real;
 
-SAIL_BUILTIN_TYPE(real);
+SAIL_BUILTIN_TYPE(real)
 
 void CREATE_OF(real, sail_string)(real *rop, const sail_string op);
 void CONVERT_OF(real, sail_string)(real *rop, const sail_string op);
@@ -440,3 +441,5 @@ void get_time_ns(sail_int*, const unit);
 /* ***** ARM optimisations ***** */
 
 void arm_align(lbits *, const lbits, const sail_int);
+
+#endif
diff --git a/lib/sail_coverage.h b/lib/sail_coverage.h
new file mode 100644
index 00000000..92f78f9c
--- /dev/null
+++ b/lib/sail_coverage.h
@@ -0,0 +1,12 @@
+#ifndef SAIL_COVERAGE_H
+#define SAIL_COVERAGE_H
+
+int sail_coverage_exit(void);
+
+void sail_function_entry(char *function_name, char *sail_file, int l1, int c1, int l2, int c2);
+
+void sail_branch_taken(int branch_id, char *sail_file, int l1, int c1, int l2, int c2);
+
+void sail_branch_reached(int branch_id, char *sail_file, int l1, int c1, int l2, int c2);
+
+#endif
diff --git a/lib/sail_failure.c b/lib/sail_failure.c
new file mode 100644
index 00000000..b725d42c
--- /dev/null
+++ b/lib/sail_failure.c
@@ -0,0 +1,14 @@
+#include "sail_failure.h"
+
+void sail_match_failure(sail_string msg)
+{
+  fprintf(stderr, "Pattern match failure in %s\n", msg);
+  exit(EXIT_FAILURE);
+}
+
+unit sail_assert(bool b, sail_string msg)
+{
+  if (b) return UNIT;
+  fprintf(stderr, "Assertion failed: %s\n", msg);
+  exit(EXIT_FAILURE);
+}
diff --git a/lib/sail_failure.h b/lib/sail_failure.h
new file mode 100644
index 00000000..d43baf4d
--- /dev/null
+++ b/lib/sail_failure.h
@@ -0,0 +1,18 @@
+#ifndef SAIL_FAILURE_H
+#define SAIL_FAILURE_H
+
+#include "sail.h"
+
+/*
+ * This function should be called whenever a pattern match failure
+ * occurs. Pattern match failures are always fatal.
+ */
+void sail_match_failure(sail_string msg);
+
+/*
+ * sail_assert implements the assert construct in Sail. If any
+ * assertion fails we immediately exit the model.
+ */
+unit sail_assert(bool b, sail_string msg);
+
+#endif