From 1c1db56b7b34e3ff6293e216872939ce73cd37e6 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 28 Apr 2020 18:40:01 +0100 Subject: Add flooring division in prelude Defined in terms of tdiv so we don't have to add it to backends that don't already have it --- lib/arith.sail | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/arith.sail b/lib/arith.sail index 6b064433..58f25bbc 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -88,13 +88,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", -- cgit v1.2.3 From 199e10df8e776e4b27f9cfd2357db6babf674ed1 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 28 Apr 2020 17:24:04 +0100 Subject: Functorise and refactor C code generator Currently uses the -c2 option Now generates a sail_state struct which is passed as a pointer to all generated functions. This contains all registers, letbindings, and the exception state. (Letbindings must be included as they can contain pointers to registers). This should make it possible to use sail models in a multi-threaded program by creating multiple sail_states, provided a suitable set of thread-safe memory builtins are provided. Currently the sail_state cannot be passed to the memory builtins. For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c. foo_emu.c wraps the generated library into an emulator that behaves the same as the one we previously generated. The sail_assert and sail_match_failure builtins are now in a separate file, as they must exist even when the RTS is not used. Name mangling can be controlled via the exports and exports_mangled fields of the configuration struct (currently not exposed outside of OCaml). exports allows specifying a name in C for any Sail identifier (before name mangling) and exports_mangled allows specifiying a name for a mangled Sail identifier - this is primarily useful for generic functions and data structures which have been specialised. --- lib/rts.c | 25 ++++++------------------- lib/rts.h | 26 +++++++++----------------- lib/sail.h | 17 ++++++++++------- lib/sail_failure.c | 14 ++++++++++++++ lib/sail_failure.h | 18 ++++++++++++++++++ 5 files changed, 57 insertions(+), 43 deletions(-) create mode 100644 lib/sail_failure.c create mode 100644 lib/sail_failure.h (limited to 'lib') 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 -#include -#include +#include +#include +#include -#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 -#include -#include +#include +#include +#include -#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..98ca3adb 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -1,12 +1,13 @@ -#pragma once +#ifndef SAIL_H +#define SAIL_H -#include -#include -#include -#include -#include +#include +#include +#include +#include +#include -#include +#include static inline void *sail_malloc(size_t size) { @@ -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_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 -- cgit v1.2.3 From 0c4c75d13aad176fc664e159d2b0c48c77b41d27 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 May 2020 09:24:09 +0100 Subject: Various bugfixes and improvements for updated codegen --- lib/sail.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/sail.h b/lib/sail.h index 98ca3adb..0c9b18b5 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -74,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); @@ -99,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); @@ -199,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, @@ -361,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); -- cgit v1.2.3 From ffaa84fe0a79a013da2169bcca76a23d4213d526 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 15 May 2020 10:54:59 +0100 Subject: Add coverage tracking tool See sailcov/README.md for a short description Fix many location info bugs discovered by eyeballing output --- lib/coverage/Cargo.toml | 11 ++++ lib/coverage/Makefile | 3 ++ lib/coverage/src/lib.rs | 132 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 146 insertions(+) create mode 100644 lib/coverage/Cargo.toml create mode 100644 lib/coverage/Makefile create mode 100644 lib/coverage/src/lib.rs (limited to 'lib') 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 "] +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> = Mutex::new(HashSet::new()); + static ref FUNCTIONS: Mutex> = 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>) -> 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, + }, + ) +} -- cgit v1.2.3 From f1ffbfcadfeb013c1619af9d98770872c1ec230f Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 15 May 2020 11:19:52 +0100 Subject: Add coverage header --- lib/sail_coverage.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 lib/sail_coverage.h (limited to 'lib') 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 -- cgit v1.2.3