diff options
62 files changed, 3041 insertions, 356 deletions
diff --git a/editors/sail-mode.el b/editors/sail-mode.el index 0d70b51e..5c1d1e07 100644 --- a/editors/sail-mode.el +++ b/editors/sail-mode.el @@ -46,7 +46,7 @@ (defconst sail2-special '("_prove" "_not_prove" "create" "kill" "convert" "undefined" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" - "$latex" "$property" "$counterexample" "$suppress_warnings")) + "$latex" "$property" "$counterexample" "$suppress_warnings" "$assert")) (defconst sail2-font-lock-keywords `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) diff --git a/etc/default_config.json b/etc/default_config.json new file mode 100644 index 00000000..79f166af --- /dev/null +++ b/etc/default_config.json @@ -0,0 +1,30 @@ +{ + "codegen": { + // Apply some default name mangling rules if true. If false, + // mangle everything. + "default_exports": true, + // An array containing either ["identifier", "string"] or + // "identifier". For the first case the identifier will be + // rewritten into string in the generated C source. For the + // second the identifier will be preserved without name + // mangling. + "exports": [], + // Generic functions must always have name mangling applied + // due to specialization. They can be renamed using ["symbol", + // "string"] pairs in this array, where "symbol" is any + // mangled symbol that appears in the generated C. + "exports_mangled": [ + ["ztuple_z8z5i64zCz0z5iz9", "tuple_i64_int"] + ], + // Include the following extra headers in the generated + // C. Should be specified as either "<header.h>" or "header.h" + "extra_headers": [], + // An array of extra string lines that are added to the + // sail_state struct. + "extra_state": [], + // The sail_state struct will be passed to the following array + // of primops, which are specified via the "foo" string from + // val id = "foo" : ... in Sail. + "state_primops": [] + } +} diff --git a/language/jib.ott b/language/jib.ott index 63c86126..9c739ec4 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -57,6 +57,7 @@ grammar name :: '' ::= | id nat :: :: name + | global id nat :: :: global | have_exception nat :: :: have_exception | current_exception nat :: :: current_exception | throw_location nat :: :: throw_location 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, + }, + ) +} @@ -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); @@ -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 @@ -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 @@ -36,7 +36,7 @@ depends: [ "conf-gmp" "conf-zlib" "base64" {< "3.0.0"} - "yojson" + "yojson" {<= "1.7.0"} "pprint" ] available: [ocaml-version >= "4.06.1"] diff --git a/sailcov/Makefile b/sailcov/Makefile new file mode 100644 index 00000000..bc9e39d8 --- /dev/null +++ b/sailcov/Makefile @@ -0,0 +1,4 @@ + +sailcov: *.ml dune + dune build main.exe + cp -f _build/default/main.exe sailcov diff --git a/sailcov/README.md b/sailcov/README.md new file mode 100644 index 00000000..17c6b395 --- /dev/null +++ b/sailcov/README.md @@ -0,0 +1,56 @@ +sailcov +======= + +sailcov is a simple branch coverage visualiser for sail specifications. + +### Usage + +First, compile your model to c using the `-c_coverage` flag and +including the [sail_coverage.h](../lib/sail_coverage.h) header via +the `-c_include sail_coverage.h` flag. Currently the `-c_coverage` +option will print information about possible branches and function +calls to stdout, which will be needed later, so redirect this to a +file called `all_branches`, i.e. + +``` +sail -c -c_coverage -c_include sail_coverage.h my_model.sail -o my_model > all_branches +``` + +Next we need to link implementations of the coverage tracking +functions into the generated C. This done by using the static library +in [lib/coverage/](../lib/coverage/). Currently this is written in Rust +for want of an obvious hashset implementation in C and can be built +using `cargo build --release` which will produce a `libsail_coverage.a` +static library. Once this is done, we can link this into our C +emulator by passing `$SAIL_DIR/lib/coverage/libsail_coverage.a +-lpthread -ldl` to gcc, where SAIL_DIR is the location of this +repository. + +Finally, when we run our model it will append coverage information +into a file called `sail_coverage`. The tool in this directory can +compare that with the data contained in the `all_branches` file +described above and produce an html coverage report for each file in +the specification. For example: + +``` +sailcov -a all_branches -t sail_coverage my_model.sail +``` + +which produces a `my_model.html` file. Multiple sail files can be +passed to the tool, and it will produce html for each +individually. See +[riscv_vmem_sv39.html](https://alasdair.github.io/riscv_vmem_sv39.html) +for an example of the output. There is also a `--tab-width` option for +sailcov that can be used to control the tab width in the generated +html. + +### Colour options + +`sailcov -help` will list the available options for the colours used in +the output. The hue and saturation for the colours used for covered +and uncovered code can be individually set. Alternatively the default +red/green colours for uncovered/covered can be swapped for a +yellow/blue theme using `--alt-colors` or `--alt-colours`. See the +alternate +[riscv_vmem_sv39.html](https://alasdair.github.io/alt_riscv_vmem_sv39.html) +for an example. diff --git a/sailcov/dune b/sailcov/dune new file mode 100644 index 00000000..c69fec07 --- /dev/null +++ b/sailcov/dune @@ -0,0 +1,2 @@ +(executable + (name main)) diff --git a/sailcov/dune-project b/sailcov/dune-project new file mode 100644 index 00000000..4c6dd5ae --- /dev/null +++ b/sailcov/dune-project @@ -0,0 +1 @@ +(lang dune 2.4) diff --git a/sailcov/main.ml b/sailcov/main.ml new file mode 100644 index 00000000..4f1e054c --- /dev/null +++ b/sailcov/main.ml @@ -0,0 +1,378 @@ + +let opt_files = ref ([] : string list) + +let opt_taken = ref "sail_coverage" +let opt_all = ref "all_branches" + +let opt_tab_width = ref 4 + +let opt_index = ref None +let opt_index_default = ref None +let opt_prefix = ref "" + +type color = { + hue: int; + saturation: int; + } + +let opt_bad_color = ref { hue = 0; saturation = 85 } +let opt_good_color = ref { hue = 120; saturation = 85 } +let opt_darken = ref 5 + +let clamp_degree n = max 0 (min n 360) +let clamp_percent n = max 0 (min n 100) + +let use_alt_colors () = + opt_good_color := { !opt_good_color with hue = 220 }; + opt_bad_color := { !opt_good_color with hue = 50 } + +let options = + Arg.align [ + ( "-t", + Arg.String (fun str -> opt_taken := str), + "<file> coverage information for branches taken while executing the model (default: sail_coverage)"); + ( "--taken", + Arg.String (fun str -> opt_taken := str), + " long form of -t"); + ( "-a", + Arg.String (fun str -> opt_all := str), + "<file> information about all possible branches (default: all_branches)"); + ( "--all", + Arg.String (fun str -> opt_all := str), + " long form of -a"); + ( "--tab-width", + Arg.Int (fun n -> opt_tab_width := n), + "<integer> set the tab width for html output (default: 4)"); + ( "--index", + Arg.String (fun str -> opt_index := Some str), + "<name> create a <name>.html page as an index"); + ( "--index-default", + Arg.String (fun str -> opt_index_default := Some str), + "<file> The .sail file that will be displayed by the generated index page by default"); + ( "--prefix", + Arg.String (fun str -> opt_prefix := str), + "<string> Prepend a prefix to all generated html coverage files"); + ( "--covered-hue", + Arg.Int (fun n -> opt_good_color := { !opt_good_color with hue = clamp_degree n }), + "<int> set the hue (between 0 and 360) of the color used for code that is covered (default: 120 (green))"); + ( "--uncovered-hue", + Arg.Int (fun n -> opt_bad_color := { !opt_bad_color with hue = clamp_degree n }), + "<int> set the hue (between 0 and 360) of the color used for code that is not covered (default: 0 (red))"); + ( "--covered-saturation", + Arg.Int (fun n -> opt_good_color := { !opt_good_color with saturation = clamp_percent n }), + "<int> set the saturation (between 0 and 100) of the color used for code that is covered (default: 85)"); + ( "--uncovered-saturation", + Arg.Int (fun n -> opt_bad_color := { !opt_bad_color with saturation = clamp_percent n }), + "<int> set the hue (between 0 and 100) of the color used for code that is not covered (default: 85)"); + ( "--nesting-darkness", + Arg.Int (fun n -> opt_darken := n), + "<int> factor which controls how much darker nested spans of the same color become (default: 5)"); + ( "--alt-colors", + Arg.Unit use_alt_colors, + " swap default colors from red/green into alternate yellow/blue theme"); + ( "--alt-colours", + Arg.Unit use_alt_colors, + "") + ] + +type span = { + file : string; + l1 : int; + c1 : int; + l2 : int; + c2 : int; + } + +let string_of_span span = + Printf.sprintf "\"%s\" %d:%d - %d:%d" span.file span.l1 span.c1 span.l2 span.c2 + +module Span = struct + type t = span + let compare s1 s2 = compare s1 s2 +end + +module SpanSet = Set.Make(Span) +module SpanMap = Map.Make(Span) + +let mk_span _ file l1 c1 l2 c2 = { file = Filename.basename file; l1 = l1; c1 = c1; l2 = l2; c2 = c2 } + +let read_coverage filename = + let spans = ref SpanSet.empty in + let chan = open_in filename in + try + let rec loop () = + let line = input_line chan in + spans := SpanSet.add (Scanf.sscanf line "%c %S, %d, %d, %d, %d" mk_span) !spans; + loop () + in + loop () + with End_of_file -> + close_in chan; + !spans + +(** We color the source either red (bad) or green (good) if it's + covered vs uncovered. If we have nested uncovered branches, they + will be increasingly bad, whereas nested covered branches will be + increasingly good. *) +type source_char = { + mutable badness : int; + mutable goodness : int; + mutable bad_zero_width: bool; + char : char; + } + +let zero_width span = span.l1 = span.l2 && span.c1 = span.c2 + +let mark_bad_region source span = + if zero_width span then ( + source.(span.l2 - 1).(span.c2 - 1).bad_zero_width <- true + ) else ( + source.(span.l1 - 1).(span.c1).badness <- source.(span.l1 - 1).(span.c1).badness + 1; + source.(span.l2 - 1).(span.c2 - 1).badness <- source.(span.l2 - 1).(span.c2 - 1).badness - 1 + ) + +let mark_good_region source span = + if not (zero_width span) then ( + source.(span.l1 - 1).(span.c1).goodness <- source.(span.l1 - 1).(span.c1).goodness + 1; + source.(span.l2 - 1).(span.c2 - 1).goodness <- source.(span.l2 - 1).(span.c2 - 1).goodness - 1 + ) + +let process_line l = Array.init (String.length l) (fun n -> { badness = 0; goodness = 0; char = l.[n]; bad_zero_width = false }) + +let read_source filename = + let lines = ref [] in + let chan = open_in filename in + try + let rec loop () = + lines := process_line (input_line chan) :: !lines; + loop () + in + loop () + with End_of_file -> + close_in chan; + Array.of_list (List.rev !lines) + +let output_html_char chan c = + if c == ' ' then + output_string chan " " + else if c == '<' then + output_string chan "<" + else if c == '>' then + output_string chan ">" + else if c == '"' then + output_string chan """ + else if c == '\t' then + output_string chan (String.concat "" (List.init !opt_tab_width (fun _ -> " "))) + else + output_char chan c + +let file_info file all taken = + let all = SpanSet.filter (fun s -> s.file = Filename.basename file) all in + let taken = SpanSet.filter (fun s -> s.file = Filename.basename file) taken in + let not_taken = SpanSet.diff all taken in + + let percent = + if SpanSet.cardinal all != 0 then + let p = 100. *. (Float.of_int (SpanSet.cardinal taken) /. Float.of_int (SpanSet.cardinal all)) in + Printf.sprintf "%.0f%%" p + else + "-" + in + + taken, + not_taken, + Printf.sprintf "%s (%d/%d) %s" (Filename.basename file) (SpanSet.cardinal taken) (SpanSet.cardinal all) percent + +let index_css = " +body, html { + width: 100%; + height: 100%; + margin: 0; + padding: 0; +} + +table { + width: 100%; + height: 100%; + margin: 0; + padding: 0; + border-collapse: collapse; + overflow: hidden; +} + +.left { + width: 20%; +} + +.left .scroll { + height: 100vh; + overflow-x: hidden; + overflow-y: auto; +} + +.right { + width: 80%; +} + +td { + padding: 0; + margin: 0; +} + +tr { + padding: 0; + margin: 0; + height: 100%; + overflow-x: hidden; + overflow-y: auto; +} + +iframe { + height: 100%; + width: 100%; + display: block; + margin: 0; + padding: 0; +} +" + +let html_file_for file = + !opt_prefix ^ Filename.remove_extension (Filename.basename file) ^ ".html" + +let main () = + let all = read_coverage !opt_all in + let taken = read_coverage !opt_taken in + List.iter (fun file -> + let taken, not_taken, desc = file_info file all taken in + print_endline desc; + + let source = read_source file in + SpanSet.iter (mark_good_region source) taken; + SpanSet.iter (mark_bad_region source) not_taken; + + let output_file = html_file_for file in + let chan = open_out output_file in + + let current_goodness = ref 0 in + let current_badness = ref 0 in + + let clamp_lightness l = max 30 (min 80 l) in + + let html_color color darkness = + Printf.sprintf "hsl(%d, %d%%, %d%%)" + color.hue color.saturation (clamp_lightness ((80 + !opt_darken) - darkness * !opt_darken)) + in + let good_color () = html_color !opt_good_color !current_goodness in + let bad_color () = html_color !opt_bad_color !current_badness in + + output_string chan "<!DOCTYPE html>\n"; + output_string chan "<html lang=\"en\">\n<head>\n<meta charset=\"utf-8\">\n"; + output_string chan (Printf.sprintf "<title>%s</title>" (Filename.remove_extension (Filename.basename file))); + output_string chan "</head>\n"; + output_string chan "<body>\n"; + output_string chan (Printf.sprintf "<h1>%s</h1>\n" desc); + output_string chan "<code style=\"display: block\">\n"; + + Array.iter (fun line -> + Array.iter (fun loc -> + if loc.goodness < 0 && loc.badness < 0 then ( + output_html_char chan loc.char; + current_goodness := !current_goodness + loc.goodness; + current_badness := !current_badness + loc.badness; + for _ = 1 to abs loc.goodness + abs loc.badness do + output_string chan (Printf.sprintf "</span>") + done + ) else if loc.goodness < 0 then ( + assert (loc.badness >= 0); + output_html_char chan loc.char; + current_goodness := !current_goodness + loc.goodness; + for _ = 1 to abs loc.goodness do + output_string chan (Printf.sprintf "</span>") + done + ) else if loc.badness < 0 then ( + assert (loc.goodness >= 0); + output_html_char chan loc.char; + current_badness := !current_badness + loc.badness; + for _ = 1 to abs loc.badness do + output_string chan (Printf.sprintf "</span>") + done + ) else if loc.badness > 0 then ( + assert (loc.goodness <= 0); + current_badness := !current_badness + loc.badness; + for _ = 1 to loc.badness do + output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (bad_color ())); + done; + output_html_char chan loc.char + ) else if loc.goodness > 0 then ( + assert (!current_badness == 0); + current_goodness := !current_goodness + loc.goodness; + for _ = 1 to loc.goodness do + output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (good_color ())); + done; + output_html_char chan loc.char + ) else ( + output_html_char chan loc.char + ); + + if loc.bad_zero_width then ( + output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (bad_color ())); + output_string chan "«Invisible branch not taken here»"; + output_string chan "</span>" + ); + + assert (!current_goodness >= 0); + assert (!current_badness >= 0) + + ) line; + output_string chan "<br>\n" + ) source; + + output_string chan "</code>\n"; + output_string chan "</body>\n"; + output_string chan "</html>"; + + close_out chan + ) !opt_files; + + begin match !opt_index with + | Some name -> + let chan = open_out (name ^ ".html") in + + output_string chan "<!DOCTYPE html>\n"; + output_string chan "<html lang=\"en\">\n"; + Printf.ksprintf (output_string chan) + "<head>\n<meta charset=\"utf-8\">\n<title>Coverage Report</title>\n<style>%s</style>\n</head>\n" + index_css; + output_string chan "<body>\n"; + + output_string chan "<table><tr><td class=\"left\"><div class=\"scroll\">"; + List.iter (fun file -> + let _, _, desc = file_info file all taken in + Printf.ksprintf (output_string chan) "<a href=\"%s\" target=\"source\">%s</a><br>\n" + (html_file_for file) desc + ) !opt_files; + output_string chan "</div></td>"; + + output_string chan "<td class=\"right\">"; + begin match !opt_index_default with + | Some default_file -> + Printf.ksprintf (output_string chan) "<iframe src=\"%s\" name=\"source\"></iframe>" + (html_file_for default_file); + | None -> + output_string chan "<iframe name=\"source\"></iframe>" + end; + output_string chan "</td></tr></table>\n"; + output_string chan "</body>\n"; + output_string chan "</html>"; + close_out chan + | None -> () + end + +let usage_msg = "usage: sailcov -t <file> -a <file> <.sail files>\n" + +let _ = + Arg.parse options + (fun s -> opt_files := !opt_files @ [s]) + usage_msg; + try main () with + | Sys_error msg -> prerr_endline msg; exit 1 @@ -2,10 +2,12 @@ true: -traverse, debug, use_menhir <**/parser.ml>: bin_annot, annot <**/*.ml> and not <**/parser.ml>: bin_annot, annot -<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), package(base64), package(pprint) +<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(omd), package(base64), package(pprint), package(yojson) <isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(base64), package(yojson), package(pprint) <isail.ml>: package(linenoise), package(yojson) +<jib/c_codegen.m{l,li}>: package(yojson) +<sail.ml>: package(yojson) <elf_loader.ml>: package(linksem) <latex.ml>: package(omd) <**/*.m{l,li}>: package(lem), package(base64), package(pprint) diff --git a/src/ast_util.ml b/src/ast_util.ml index ac5da907..d0af5da3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -89,7 +89,7 @@ let untyp_pat = function | P_aux (P_typ (typ, pat), _) -> pat, Some typ | pat -> pat, None -let mk_pexp pexp_aux = Pat_aux (pexp_aux, no_annot) +let mk_pexp ?loc:(l=Parse_ast.Unknown) pexp_aux = Pat_aux (pexp_aux, (l, ())) let mk_mpat mpat_aux = MP_aux (mpat_aux, no_annot) let mk_mpexp mpexp_aux = MPat_aux (mpexp_aux, no_annot) diff --git a/src/ast_util.mli b/src/ast_util.mli index 6be8ca34..1449a390 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -84,7 +84,7 @@ val mk_nexp : nexp_aux -> nexp val mk_exp : ?loc:l -> unit exp_aux -> unit exp val mk_pat : unit pat_aux -> unit pat val mk_mpat : unit mpat_aux -> unit mpat -val mk_pexp : unit pexp_aux -> unit pexp +val mk_pexp : ?loc:l -> unit pexp_aux -> unit pexp val mk_mpexp : unit mpexp_aux -> unit mpexp val mk_lexp : unit lexp_aux -> unit lexp val mk_lit : lit_aux -> lit diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 35417ac8..1c273df1 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -374,4 +374,10 @@ let () = ~name:"fix_registers" ~help:"Fix the value of specified registers, specified as a \ list of <register>=<value>. Can also fix a specific \ - register field as <register>.<field>=<value>." + register field as <register>.<field>=<value>. Note that \ + this is not used to set registers normally, but instead \ + fixes their value such that the constant folding rewrite \ + (which is subsequently invoked by this command) will \ + replace register reads with the fixed values. Requires a \ + target (c, lem, etc.), as the set of functions that can \ + be constant folded can differ on a per-target basis." diff --git a/src/interactive.ml b/src/interactive.ml index 2cca944c..93df1dc0 100644 --- a/src/interactive.ml +++ b/src/interactive.ml @@ -55,6 +55,7 @@ open Printf let opt_interactive = ref false let opt_emacs_mode = ref false let opt_suppress_banner = ref false +let opt_auto_interpreter_rewrites = ref false let env = ref Type_check.initial_env @@ -80,7 +81,9 @@ let reflect_typ action = | ArgInt (_, next) -> int_typ :: arg_typs (next 0) | Action _ -> [] in - function_typ (arg_typs action) unit_typ no_effect + match action with + | Action _ -> function_typ [unit_typ] unit_typ no_effect + | _ -> function_typ (arg_typs action) unit_typ no_effect let generate_help name help action = let rec args = function diff --git a/src/interactive.mli b/src/interactive.mli index 933d0a46..b0cce425 100644 --- a/src/interactive.mli +++ b/src/interactive.mli @@ -54,6 +54,7 @@ open Type_check val opt_interactive : bool ref val opt_emacs_mode : bool ref val opt_suppress_banner : bool ref +val opt_auto_interpreter_rewrites : bool ref val ast : tannot defs ref diff --git a/src/interpreter.ml b/src/interpreter.ml index a30e90bc..b3e8fe31 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -961,7 +961,7 @@ let rec initialize_registers allow_registers gstate = begin let env = Type_check.env_of_annot annot in let typ = Type_check.Env.expand_synonyms env typ in - let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit (L_undef))))) in + let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit L_undef)))) in let exp = Type_check.check_exp env exp typ in { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers } end diff --git a/src/isail.ml b/src/isail.ml index 02908321..dc7858c9 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -113,7 +113,8 @@ let sep = "-----------------------------------------------------" |> Util.blue | let vs_ids = ref (val_spec_ids !Interactive.ast) -let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops) +let interactive_state = + ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops) (* We can't set up the elf commands in elf_loader.ml because it's used by Sail OCaml emulators at runtime, so set them up here. *) @@ -192,34 +193,75 @@ let rec run () = match !current_mode with | Normal | Emacs -> () | Evaluation frame -> - begin - match frame with - | Done (state, v) -> - interactive_state := state; - print_endline ("Result = " ^ Value.string_of_value v); - current_mode := Normal - | Fail (_, _, _, _, msg) -> - print_endline ("Error: " ^ msg); - current_mode := Normal - | Step (out, state, _, stack) -> - begin - try - current_mode := Evaluation (eval_frame frame) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run () - | Break frame -> - print_endline "Breakpoint"; - current_mode := Evaluation frame - | Effect_request (out, state, stack, eff) -> - begin - try - current_mode := Evaluation (!Interpreter.effect_interp state eff) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run () + begin match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal + | Step (out, state, _, stack) -> + begin + try + current_mode := Evaluation (eval_frame frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run () + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (!Interpreter.effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run () + end + +let rec run_function depth = + let run_function' stack = + match depth with + | None -> run_function (Some (List.length stack)) + | Some n -> + if List.compare_length_with stack n >= 0 then + run_function depth + else + () + in + match !current_mode with + | Normal | Emacs -> () + | Evaluation frame -> + begin match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal + | Step (out, state, _, stack) -> + begin + try + current_mode := Evaluation (eval_frame frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_function' stack + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (!Interpreter.effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_function' stack end let rec run_steps n = @@ -227,36 +269,35 @@ let rec run_steps n = | _ when n <= 0 -> () | Normal | Emacs -> () | Evaluation frame -> - begin - match frame with - | Done (state, v) -> - interactive_state := state; - print_endline ("Result = " ^ Value.string_of_value v); - current_mode := Normal - | Fail (_, _, _, _, msg) -> - print_endline ("Error: " ^ msg); - current_mode := Normal - | Step (out, state, _, stack) -> - begin - try - current_mode := Evaluation (eval_frame frame) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run_steps (n - 1) - | Break frame -> - print_endline "Breakpoint"; - current_mode := Evaluation frame - | Effect_request (out, state, stack, eff) -> - begin - try - current_mode := Evaluation (!Interpreter.effect_interp state eff) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run_steps (n - 1) + begin match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal + | Step (out, state, _, stack) -> + begin + try + current_mode := Evaluation (eval_frame frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_steps (n - 1) + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (!Interpreter.effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_steps (n - 1) end - + let help = let open Printf in let open Util in @@ -297,6 +338,8 @@ let help = | ":s" | ":step" -> sprintf "(:s | :step) %s - Perform a number of evaluation steps." (color yellow "<number>") + | ":f" | ":step_function" -> + sprintf "(:s | :step) - Perform evaluation steps until the currently evaulating function returns." | ":n" | ":normal" -> "(:n | :normal) - Exit evaluation mode back to normal mode." | ":clear" -> @@ -314,6 +357,8 @@ let help = | ":option" -> sprintf ":option %s - Parse string as if it was an option passed on the command line. e.g. :option -help." (color yellow "<string>") + | ":recheck" -> + sprintf ":recheck - Re type-check the Sail AST, and synchronize the interpreters internal state to that AST." | ":rewrite" -> sprintf ":rewrite %s - Apply a rewrite to the AST. %s shows all possible rewrites. See also %s" (color yellow "<rewrite> <args>") (color green ":list_rewrites") (color green ":rewrites") @@ -419,6 +464,9 @@ let handle_input' input = let cmd = Str.string_before input n in let arg = String.trim (Str.string_after input n) in Command (cmd, arg) + else if String.length input >= 2 && input.[0] = '/' && input.[1] = '/' then + (* Treat anything starting with // as a comment *) + Empty else if input <> "" then Expression input else @@ -468,7 +516,7 @@ let handle_input' input = let more_commands = Util.string_of_list " " fst !Interactive.commands in let commands = [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help :output :option"; - "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :rewrite :rewrites :list_rewrites :compile " ^ more_commands; + "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :recheck :rewrite :rewrites :list_rewrites :compile " ^ more_commands; "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; ""; ":(c)ommand can be called as either :c or :command." ] @@ -510,9 +558,15 @@ let handle_input' input = | ":l" | ":load" -> let files = Util.split_on_char ' ' arg in let (_, ast, env) = Process_file.load_files options !Interactive.env files in + let ast, env = + if !Interactive.opt_auto_interpreter_rewrites then + Process_file.rewrite_ast_target "interpreter" env ast + else + ast, env + in Interactive.ast := append_ast !Interactive.ast ast; - interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; Interactive.env := env; + interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; vs_ids := val_spec_ids !Interactive.ast | ":u" | ":unload" -> Interactive.ast := Ast.Defs []; @@ -684,7 +738,11 @@ let handle_input' input = | ":r" | ":run" -> run () | ":s" | ":step" -> - run_steps (int_of_string arg) + run_steps (int_of_string arg); + print_program () + | ":f" | ":step_function" -> + run_function None; + print_program () | _ -> unrecognised_command cmd end | Expression str -> @@ -819,6 +877,13 @@ let () = | _ -> None ); + if !Interactive.opt_auto_interpreter_rewrites then ( + let new_ast, new_env = Process_file.rewrite_ast_target "interpreter" !Interactive.env !Interactive.ast in + Interactive.ast := new_ast; + Interactive.env := new_env; + interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops + ); + (* Read the script file if it is set with the -is option, and excute them *) begin match !opt_interactive_script with | None -> () diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 6bc447c0..c81f729c 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -106,6 +106,8 @@ and 'a aval = | AV_record of ('a aval) Bindings.t * 'a | AV_cval of cval * 'a +let aexp_loc (AE_aux (_, _, l)) = l + (* Renaming variables in ANF expressions *) let rec apat_bindings (AP_aux (apat_aux, _, _)) = @@ -523,13 +525,13 @@ let rec apat_globals (AP_aux (aux, _, _)) = let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in - let to_aval (AE_aux (aexp_aux, env, l) as aexp) = - let mk_aexp aexp = AE_aux (aexp, env, l) in + let to_aval (AE_aux (aexp_aux, env, _) as aexp) = + let mk_aexp (AE_aux (_, _, l)) aexp = AE_aux (aexp, env, l) in match aexp_aux with | AE_val v -> (v, fun x -> x) | AE_short_circuit (_, _, _) -> let id = gensym () in - (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp x (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp))) | AE_app (_, _, typ) | AE_let (_, _, _, _, _, typ) | AE_return (_, typ) @@ -542,10 +544,10 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | AE_record_update (_, _, typ) | AE_block (_, _, typ) -> let id = gensym () in - (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (Immutable, id, typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp x (AE_let (Immutable, id, typ, aexp, x, typ_of exp))) | AE_assign _ | AE_for _ | AE_loop _ | AE_write_ref _ -> let id = gensym () in - (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp x (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp))) in match e_aux with | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) @@ -701,7 +703,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_var (LEXP_aux (LEXP_id id, _), binding, body) | E_var (LEXP_aux (LEXP_cast (_, id), _), binding, body) - | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> + | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) + | E_let (LB_aux (LB_val (P_aux (P_typ (_, P_aux (P_id id, _)), _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp)) diff --git a/src/jib/anf.mli b/src/jib/anf.mli index d01fe146..b96766da 100644 --- a/src/jib/anf.mli +++ b/src/jib/anf.mli @@ -133,8 +133,10 @@ and 'a aval = counter to ensure uniqueness. This function resets that counter. *) val reset_anf_counter : unit -> unit +val aexp_loc : 'a aexp -> Parse_ast.l + (** {2 Functions for transforming ANF expressions} *) - + val aval_typ : typ aval -> typ val aexp_typ : typ aexp -> typ diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2b2234b5..b1d6cc40 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -62,14 +62,15 @@ open Anf module Big_int = Nat_big_num let opt_static = ref false +let static () = if !opt_static then "static " else "" let opt_no_main = ref false -let opt_memo_cache = ref false let opt_no_lib = ref false let opt_no_rts = ref false let opt_prefix = ref "z" let opt_extra_params = ref None let opt_extra_arguments = ref None - +let opt_branch_coverage = ref false + let extra_params () = match !opt_extra_params with | Some str -> str ^ ", " @@ -130,12 +131,47 @@ let rec is_stack_ctyp ctyp = match ctyp with let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true)) -module C_config : Config = struct - -(** Convert a sail type into a C-type. This function can be quite - slow, because it uses ctx.local_env and SMT to analyse the Sail - types and attempts to fit them into the smallest possible C - types, provided ctx.optimize_smt is true (default) **) +let hex_char = + let open Sail2_values in + function + | '0' -> [B0; B0; B0; B0] + | '1' -> [B0; B0; B0; B1] + | '2' -> [B0; B0; B1; B0] + | '3' -> [B0; B0; B1; B1] + | '4' -> [B0; B1; B0; B0] + | '5' -> [B0; B1; B0; B1] + | '6' -> [B0; B1; B1; B0] + | '7' -> [B0; B1; B1; B1] + | '8' -> [B1; B0; B0; B0] + | '9' -> [B1; B0; B0; B1] + | 'A' | 'a' -> [B1; B0; B1; B0] + | 'B' | 'b' -> [B1; B0; B1; B1] + | 'C' | 'c' -> [B1; B1; B0; B0] + | 'D' | 'd' -> [B1; B1; B0; B1] + | 'E' | 'e' -> [B1; B1; B1; B0] + | 'F' | 'f' -> [B1; B1; B1; B1] + | _ -> failwith "Invalid hex character" + +let literal_to_fragment (L_aux (l_aux, _) as lit) = + match l_aux with + | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> + Some (V_lit (VL_int n, CT_fint 64)) + | L_hex str when String.length str <= 16 -> + let padding = 16 - String.length str in + let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in + let content = Util.string_to_list str |> List.map hex_char |> List.concat in + Some (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true))) + | L_unit -> Some (V_lit (VL_unit, CT_unit)) + | L_true -> Some (V_lit (VL_bool true, CT_bool)) + | L_false -> Some (V_lit (VL_bool false, CT_bool)) + | _ -> None + +module C_config(Opts : sig val branch_coverage : bool end) : Config = struct + + (** Convert a sail type into a C-type. This function can be quite + slow, because it uses ctx.local_env and SMT to analyse the Sail + types and attempts to fit them into the smallest possible C + types, provided ctx.optimize_smt is true (default) **) let rec convert_typ ctx typ = let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in match typ_aux with @@ -232,41 +268,6 @@ module C_config : Config = struct (* 3. Optimization of primitives and literals *) (**************************************************************************) - let hex_char = - let open Sail2_values in - function - | '0' -> [B0; B0; B0; B0] - | '1' -> [B0; B0; B0; B1] - | '2' -> [B0; B0; B1; B0] - | '3' -> [B0; B0; B1; B1] - | '4' -> [B0; B1; B0; B0] - | '5' -> [B0; B1; B0; B1] - | '6' -> [B0; B1; B1; B0] - | '7' -> [B0; B1; B1; B1] - | '8' -> [B1; B0; B0; B0] - | '9' -> [B1; B0; B0; B1] - | 'A' | 'a' -> [B1; B0; B1; B0] - | 'B' | 'b' -> [B1; B0; B1; B1] - | 'C' | 'c' -> [B1; B1; B0; B0] - | 'D' | 'd' -> [B1; B1; B0; B1] - | 'E' | 'e' -> [B1; B1; B1; B0] - | 'F' | 'f' -> [B1; B1; B1; B1] - | _ -> failwith "Invalid hex character" - - let literal_to_fragment (L_aux (l_aux, _) as lit) = - match l_aux with - | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> - Some (V_lit (VL_int n, CT_fint 64)) - | L_hex str when String.length str <= 16 -> - let padding = 16 - String.length str in - let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in - let content = Util.string_to_list str |> List.map hex_char |> List.concat in - Some (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true))) - | L_unit -> Some (V_lit (VL_unit, CT_unit)) - | L_true -> Some (V_lit (VL_bool true, CT_bool)) - | L_false -> Some (V_lit (VL_bool false, CT_bool)) - | _ -> None - let c_literals ctx = let rec c_literal env l = function | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) -> @@ -558,13 +559,15 @@ module C_config : Config = struct analyze_functions ctx analyze_primop (c_literals ctx aexp) - let unroll_loops () = None + let unroll_loops = None let specialize_calls = false let ignore_64 = false let struct_value = false let use_real = false + let branch_coverage = Opts.branch_coverage + let track_throw = true end - + (** Functions that have heap-allocated return types are implemented by passing a pointer a location where the return value should be stored. The ANF -> Sail IR pass for expressions simply outputs an @@ -1117,7 +1120,11 @@ let rec sgen_value = function | VL_bits ([], _) -> "UINT64_C(0)" | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" - | VL_int i -> Big_int.to_string i ^ "l" + | VL_int i -> + if Big_int.equal i (min_int 64) then + "INT64_MIN" + else + "INT64_C(" ^ Big_int.to_string i ^ ")" | VL_bool true -> "true" | VL_bool false -> "false" | VL_unit -> "UNIT" @@ -1329,6 +1336,7 @@ let rec sgen_clexp = function | CL_id (Throw_location _, _) -> "throw_location" | CL_id (Return _, _) -> assert false | CL_id (Name (id, _), _) -> "&" ^ sgen_id id + | CL_id (Global (id, _), _) -> "&" ^ sgen_id id | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ zencode_uid field ^ ")" | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")" | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))" @@ -1341,6 +1349,7 @@ let rec sgen_clexp_pure = function | CL_id (Throw_location _, _) -> "throw_location" | CL_id (Return _, _) -> assert false | CL_id (Name (id, _), _) -> sgen_id id + | CL_id (Global (id, _), _) -> sgen_id id | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ zencode_uid field | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))" @@ -1584,7 +1593,7 @@ let codegen_type_def ctx = function in let codegen_undefined = let name = sgen_id id in - string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) + string (Printf.sprintf "static enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) in string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi] @@ -2042,16 +2051,15 @@ let codegen_alloc = function let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline - ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id)) | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> - let static = if !opt_static then "static " else "" in if Env.is_extern id ctx.tc_env "c" then empty else if is_stack_ctyp ret_ctyp then - string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%s%s %s(%s%s);" (static ()) (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) else - string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" (static ()) (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with @@ -2092,8 +2100,7 @@ let codegen_def' ctx = function codegen_type_def ctx ctype_def | CDEF_startup (id, instrs) -> - let static = if !opt_static then "static " else "" in - let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in + let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl instrs ^^ twice hardline ^^ startup_header ^^ hardline @@ -2102,8 +2109,7 @@ let codegen_def' ctx = function ^^ string "}" | CDEF_finish (id, instrs) -> - let static = if !opt_static then "static " else "" in - let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in + let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl (List.filter is_decl instrs) ^^ twice hardline ^^ finish_header ^^ hardline @@ -2119,7 +2125,7 @@ let codegen_def' ctx = function let cleanup = List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings) in - separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) ^^ string "{" ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline @@ -2219,10 +2225,10 @@ let rec get_recursive_functions (Defs defs) = | [] -> IdSet.empty let jib_of_ast env ast = - let module Jibc = Make(C_config) in + let module Jibc = Make(C_config(struct let branch_coverage = !opt_branch_coverage end)) in let ctx = initial_ctx (add_special_functions env) in Jibc.compile_ast ctx ast - + let compile_ast env output_chan c_includes ast = try let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in @@ -2240,6 +2246,7 @@ let compile_ast env output_chan c_includes ast = @ (if !opt_no_rts then [] else [ string "#include \"rts.h\""; string "#include \"elf.h\"" ]) + @ (if !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else []) @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes)) in @@ -2282,7 +2289,7 @@ let compile_ast env output_chan c_includes ast = in let model_init = separate hardline (List.map string - ( [ "void model_init(void)"; + ( [ Printf.sprintf "%svoid model_init(void)" (static ()); "{"; " setup_rts();" ] @ fst exn_boilerplate @@ -2294,7 +2301,7 @@ let compile_ast env output_chan c_includes ast = in let model_fini = separate hardline (List.map string - ( [ "void model_fini(void)"; + ( [ Printf.sprintf "%svoid model_fini(void)" (static ()); "{" ] @ letbind_finalizers @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) @@ -2304,22 +2311,32 @@ let compile_ast env output_chan c_includes ast = @ [ "}" ] )) in - let model_default_main = separate hardline (List.map string - [ "int model_main(int argc, char *argv[])"; - "{"; - " model_init();"; - " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; - Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); - " model_fini();"; - " return EXIT_SUCCESS;"; - "}" ] ) + let model_default_main = + ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (static ()); + "{"; + " model_init();"; + " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; + Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); + " model_fini();" ] + @ (if !opt_branch_coverage then + [ " if (sail_coverage_exit() != 0) {"; + " fprintf(stderr, \"Could not write coverage information\\n\");"; + " exit(EXIT_FAILURE);"; + " }" ] + else + [] + ) + @ [ " return EXIT_SUCCESS;"; + "}" ]) + |> List.map string + |> separate hardline in let model_main = separate hardline (if (!opt_no_main) then [] else List.map string - [ "int main(int argc, char *argv[])"; - "{"; - " return model_main(argc, argv);"; - "}" ] ) + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ] ) in let hlhl = hardline ^^ hardline in @@ -2336,3 +2353,10 @@ let compile_ast env output_chan c_includes ast = with | Type_error (_, l, err) -> c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) + +let compile_ast_clib env ast codegen = + let cdefs, ctx = jib_of_ast env ast in + let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in + Jib_interactive.ir := cdefs'; + let cdefs = insert_heap_returns Bindings.empty cdefs in + codegen ctx cdefs diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index e627ebd8..b10e53d3 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -88,15 +88,8 @@ val opt_prefix : string ref val opt_extra_params : string option ref val opt_extra_arguments : string option ref -(** (WIP) [opt_memo_cache] will store the compiled function - definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum - of the original function to be compiled. Enabled using the -memo - flag. Uses Marshal so it's quite picky about the exact version of - the Sail version. This cache can obviously become stale if the C - backend changes - it'll load an old version compiled without said - changes. *) -val opt_memo_cache : bool ref - +val opt_branch_coverage : bool ref + (** Optimization flags *) val optimize_primops : bool ref @@ -108,3 +101,5 @@ val optimize_fixed_bits : bool ref val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit + +val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml new file mode 100644 index 00000000..d5015318 --- /dev/null +++ b/src/jib/c_codegen.ml @@ -0,0 +1,1714 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open Jib_compile +open Jib_util +open Type_check +open PPrint +open Printf +open Value2 + +module StringMap = Map.Make(String) +module StringSet = Set.Make(String) +module Big_int = Nat_big_num +module Json = Yojson.Basic + +let (gensym, _) = symbol_generator "c2" +let ngensym () = name (gensym ()) + +let zencode_id id = Util.zencode_string (string_of_id id) + +let zencode_uid (id, ctyps) = + match ctyps with + | [] -> Util.zencode_string (string_of_id id) + | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) + +let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty + +let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) +let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) + +(** This function is used to split types into those we allocate on the + stack, versus those which need to live on the heap, or otherwise + require some additional memory management *) +let rec is_stack_ctyp ctyp = match ctyp with + | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true + | CT_fint n -> n <= 64 + (* | CT_lint when !optimize_fixed_int -> true *) + | CT_lint -> false + (* | CT_lbits _ when !optimize_fixed_bits -> true *) + | CT_lbits _ -> false + | CT_real | CT_string | CT_list _ | CT_vector _ | CT_fvector _ -> false + | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields + | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *) + | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps + | CT_ref ctyp -> true + | CT_poly -> true + | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64) + +let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true)) + +type codegen_options = { + (** Rewrites a Sail identifier into a user-specified name in the generated C *) + exports : string Bindings.t; + (** Rewrites a generated symbol after name-mangling has ocurred *) + exports_mangled : string StringMap.t; + (** Extra headers to include in the generated .h file *) + extra_headers : string list; + (** Extra lines that are included in the sail_state struct. Used + to add user-specified state to the structs, which can then be + passed to primops in state_primops *) + extra_state : string list; + (** Primitives in this set will be passed a pointer to the + sail_state struct *) + state_primops : StringSet.t; + } + +let initial_options = { + exports = Bindings.empty; + exports_mangled = StringMap.empty; + extra_headers = []; + extra_state = []; + state_primops = StringSet.empty; + } + +let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports } + +let add_custom_export opts id into = { opts with exports = Bindings.add id into opts.exports } + +let add_mangled_rename opts (from, into) = + { opts with exports_mangled = StringMap.add from into opts.exports_mangled } + +let add_export_uid opts (id, ctyps) = + match ctyps with + | [] -> { opts with exports = Bindings.add id (string_of_id id) opts.exports } + | _ -> opts + +let ctype_def_initial_options opts = function + | CTD_enum (id, ids) -> + List.fold_left add_export (add_export opts id) ids + | CTD_struct (id, members) | CTD_variant (id, members) -> + List.fold_left add_export_uid (add_export opts id) (List.map fst members) + +let cdef_initial_options opts = function + | CDEF_type ctype_def -> ctype_def_initial_options opts ctype_def + | CDEF_reg_dec (id, _, _) -> add_export opts id + | CDEF_let (_, bindings, _) -> List.fold_left (fun opts (id, _) -> add_export opts id) opts bindings + | _ -> opts + +let default_options cdefs = + let opts = List.fold_left cdef_initial_options initial_options cdefs in + let opts = add_export opts (mk_id "initialize_registers") in + let opts = add_custom_export opts (mk_id "main") "sail_main" in + List.fold_left add_mangled_rename opts (List.init 9 (fun n -> "ztup" ^ string_of_int n, "tuple_" ^ string_of_int n)) + +let options_from_json json cdefs = + let open Json.Util in + let bad_key k json = + raise (Reporting.err_general Parse_ast.Unknown + (sprintf "Invalid %s key in codegen json configuration: %s" k (Json.to_string json))) + in + let opts = match member "default_exports" json with + | `Bool true -> default_options cdefs + | `Bool false -> initial_options + | `Null -> + Reporting.simple_warn "No default_exports key in codegen json configuration"; + initial_options + | json -> bad_key "default_exports" json + in + let process_exports opts = function + | `List [`String from; `String into] -> add_custom_export opts (mk_id from) into + | `String str -> add_export opts (mk_id str) + | json -> bad_key "exports" json + in + let opts = match member "exports" json with + | `List exports -> List.fold_left process_exports opts exports + | `Null -> + Reporting.simple_warn "No exports key in codegen json configuration"; + opts + | json -> bad_key "exports" json + in + let process_exports_mangled opts = function + | `List [`String from; `String into] -> add_mangled_rename opts (from, into) + | json -> bad_key "exports_mangled" json + in + let opts = match member "exports_mangled" json with + | `List exports -> List.fold_left process_exports_mangled opts exports + | `Null -> + Reporting.simple_warn "No exports_mangled key in codegen json configuration"; + opts + | json -> bad_key "exports_mangled" json + in + let process_extra_header opts = function + | `String header -> { opts with extra_headers = header :: opts.extra_headers } + | json -> bad_key "extra_headers" json + in + let opts = match member "extra_headers" json with + | `List headers -> List.fold_left process_extra_header opts headers + | `Null -> + Reporting.simple_warn "No extra_headers key in codegen json configuration"; + opts + | json -> bad_key "extra_headers" json + in + let process_extra_state opts = function + | `String member -> { opts with extra_state = member :: opts.extra_state } + | json -> bad_key "extra_state" json + in + let opts = match member "extra_state" json with + | `List members -> List.fold_left process_extra_state opts members + | `Null -> + Reporting.simple_warn "No extra_state key in codegen json configuration"; + opts + | json -> bad_key "extra_state" json + in + opts + +module type Options = sig + val opts : codegen_options +end + +module Make(O: Options) = struct + +let mangle str = + let mangled = Util.zencode_string str in + match StringMap.find_opt mangled O.opts.exports_mangled with + | Some export -> export + | None -> mangled + +let sgen_id id = + match Bindings.find_opt id O.opts.exports with + | Some export -> export + | None -> mangle (string_of_id id) + +let sgen_name = + function + | Name (id, _) -> + sgen_id id + | Global (id, _) -> + sprintf "(state->%s)" (sgen_id id) + | Have_exception _ -> + "(state->have_exception)" + | Return _ -> + assert false + | Current_exception _ -> + "(*(state->current_exception))" + | Throw_location _ -> + "(state->throw_location)" + +let sgen_uid (id, ctyps) = + match ctyps with + | [] -> sgen_id id + | _ -> + mangle (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) + +let codegen_id id = string (sgen_id id) +let codegen_uid id = string (sgen_uid id) + +let sgen_function_id id = sgen_id id +let sgen_function_uid uid = sgen_uid uid +let codegen_function_id id = string (sgen_function_id id) + +let rec sgen_ctyp = function + | CT_unit -> "unit" + | CT_bit -> "fbits" + | CT_bool -> "bool" + | CT_fbits _ -> "uint64_t" + | CT_sbits _ -> "sbits" + | CT_fint _ -> "int64_t" + | CT_constant _ -> "int64_t" + | CT_lint -> "sail_int" + | CT_lbits _ -> "lbits" + | CT_tup _ as tup -> "struct " ^ mangle ("tuple_" ^ string_of_ctyp tup) + | CT_struct (id, _) -> "struct " ^ sgen_id id + | CT_enum (id, _) -> "enum " ^ sgen_id id + | CT_variant (id, _) -> "struct " ^ sgen_id id + | CT_list _ as l -> mangle (string_of_ctyp l) + | CT_vector _ as v -> mangle (string_of_ctyp v) + | CT_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ)) + | CT_string -> "sail_string" + | CT_real -> "real" + | CT_ref ctyp -> sgen_ctyp ctyp ^ "*" + | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) + +let rec sgen_ctyp_name = function + | CT_unit -> "unit" + | CT_bit -> "fbits" + | CT_bool -> "bool" + | CT_fbits _ -> "fbits" + | CT_sbits _ -> "sbits" + | CT_fint _ -> "mach_int" + | CT_constant _ -> "mach_int" + | CT_lint -> "sail_int" + | CT_lbits _ -> "lbits" + | CT_tup _ as tup -> mangle ("tuple_" ^ string_of_ctyp tup) + | CT_struct (id, _) -> sgen_id id + | CT_enum (id, _) -> sgen_id id + | CT_variant (id, _) -> sgen_id id + | CT_list _ as l -> mangle (string_of_ctyp l) + | CT_vector _ as v -> mangle (string_of_ctyp v) + | CT_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ)) + | CT_string -> "sail_string" + | CT_real -> "real" + | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp + | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) + +let sgen_mask n = + if n = 0 then + "UINT64_C(0)" + else if n <= 64 then + let chars_F = String.make (n / 4) 'F' in + let first = match (n mod 4) with + | 0 -> "" + | 1 -> "1" + | 2 -> "3" + | 3 -> "7" + | _ -> assert false + in + "UINT64_C(0x" ^ first ^ chars_F ^ ")" + else + failwith "Tried to create a mask literal for a vector greater than 64 bits." + +let rec sgen_value = function + | VL_bits ([], _) -> "UINT64_C(0)" + | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" + | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" + | VL_int i -> + if Big_int.equal i (min_int 64) then + "INT64_MIN" + else + "INT64_C(" ^ Big_int.to_string i ^ ")" + | VL_bool true -> "true" + | VL_bool false -> "false" + | VL_unit -> "UNIT" + | VL_bit Sail2_values.B0 -> "UINT64_C(0)" + | VL_bit Sail2_values.B1 -> "UINT64_C(1)" + | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value" + | VL_real str -> str + | VL_string str -> "\"" ^ str ^ "\"" + | VL_empty_list -> "NULL" + | VL_enum element -> mangle element + | VL_ref r -> "&(state->" ^ sgen_id (mk_id r) ^ ")" + | VL_undefined -> + Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal" + +let rec sgen_cval ctx = function + | V_id (id, ctyp) -> + sgen_name id + | V_lit (vl, ctyp) -> sgen_value vl + | V_call (op, cvals) -> sgen_call ctx op cvals + | V_field (f, field) -> + sprintf "%s.%s" (sgen_cval ctx f) (sgen_uid field) + | V_tuple_member (f, _, n) -> + sprintf "%s.%s" (sgen_cval ctx f) (mangle ("tup" ^ string_of_int n)) + | V_ctor_kind (f, ctor, unifiers, _) -> + sgen_cval ctx f ^ ".kind" + ^ " != Kind_" ^ sgen_uid (ctor, unifiers) + | V_struct (fields, _) -> + sprintf "{%s}" + (Util.string_of_list ", " (fun (field, cval) -> sgen_uid field ^ " = " ^ sgen_cval ctx cval) fields) + | V_ctor_unwrap (ctor, f, unifiers, _) -> + sprintf "%s.%s" + (sgen_cval ctx f) + (sgen_uid (ctor, unifiers)) + | V_poly (f, _) -> sgen_cval ctx f + +and sgen_call ctx op cvals = + match op, cvals with + | Bnot, [v] -> "!(" ^ sgen_cval ctx v ^ ")" + | List_hd, [v] -> + sprintf "(%s).hd" ("*" ^ sgen_cval ctx v) + | List_tl, [v] -> + sprintf "(%s).tl" ("*" ^ sgen_cval ctx v) + | Eq, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_sbits _ -> + sprintf "eq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> + sprintf "(%s == %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + end + | Neq, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_sbits _ -> + sprintf "neq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> + sprintf "(%s != %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + end + | Ilt, [v1; v2] -> + sprintf "(%s < %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Igt, [v1; v2] -> + sprintf "(%s > %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Ilteq, [v1; v2] -> + sprintf "(%s <= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Igteq, [v1; v2] -> + sprintf "(%s >= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Iadd, [v1; v2] -> + sprintf "(%s + %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Isub, [v1; v2] -> + sprintf "(%s - %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Unsigned 64, [vec] -> + sprintf "((mach_int) %s)" (sgen_cval ctx vec) + | Signed 64, [vec] -> + begin match cval_ctyp vec with + | CT_fbits (n, _) -> + sprintf "fast_signed(%s, %d)" (sgen_cval ctx vec) n + | _ -> assert false + end + | Bvand, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + sprintf "(%s & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | CT_sbits _ -> + sprintf "and_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvnot, [v] -> + begin match cval_ctyp v with + | CT_fbits (n, _) -> + sprintf "(~(%s) & %s)" (sgen_cval ctx v) (sgen_cval ctx (v_mask_lower n)) + | CT_sbits _ -> + sprintf "not_sbits(%s)" (sgen_cval ctx v) + | _ -> assert false + end + | Bvor, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + sprintf "(%s | %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | CT_sbits _ -> + sprintf "or_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvxor, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + sprintf "(%s ^ %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | CT_sbits _ -> + sprintf "xor_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvadd, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits (n, _) -> + sprintf "((%s + %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n)) + | CT_sbits _ -> + sprintf "add_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvsub, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits (n, _) -> + sprintf "((%s - %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n)) + | CT_sbits _ -> + sprintf "sub_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvaccess, [vec; n] -> + begin match cval_ctyp vec with + | CT_fbits _ -> + sprintf "(UINT64_C(1) & (%s >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n) + | CT_sbits _ -> + sprintf "(UINT64_C(1) & (%s.bits >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n) + | _ -> assert false + end + | Slice len, [vec; start] -> + begin match cval_ctyp vec with + | CT_fbits _ -> + sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start) + | CT_sbits _ -> + sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s.bits >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start) + | _ -> assert false + end + | Sslice 64, [vec; start; len] -> + begin match cval_ctyp vec with + | CT_fbits _ -> + sprintf "sslice(%s, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len) + | CT_sbits _ -> + sprintf "sslice(%s.bits, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len) + | _ -> assert false + end + | Set_slice, [vec; start; slice] -> + begin match cval_ctyp vec, cval_ctyp slice with + | CT_fbits (n, _), CT_fbits (m, _) -> + sprintf "((%s & ~(%s << %s)) | (%s << %s))" (sgen_cval ctx vec) (sgen_mask m) (sgen_cval ctx start) (sgen_cval ctx slice) (sgen_cval ctx start) + | _ -> assert false + end + | Zero_extend n, [v] -> + begin match cval_ctyp v with + | CT_fbits _ -> sgen_cval ctx v + | CT_sbits _ -> + sprintf "fast_zero_extend(%s, %d)" (sgen_cval ctx v) n + | _ -> assert false + end + | Sign_extend n, [v] -> + begin match cval_ctyp v with + | CT_fbits (m, _) -> + sprintf "fast_sign_extend(%s, %d, %d)" (sgen_cval ctx v) m n + | CT_sbits _ -> + sprintf "fast_sign_extend2(%s, %d)" (sgen_cval ctx v) n + | _ -> assert false + end + | Replicate n, [v] -> + begin match cval_ctyp v with + | CT_fbits (m, _) -> + sprintf "fast_replicate_bits(UINT64_C(%d), %s, %d)" m (sgen_cval ctx v) n + | _ -> assert false + end + | Concat, [v1; v2] -> + (* Optimized routines for all combinations of fixed and small bits + appends, where the result is guaranteed to be smaller than 64. *) + begin match cval_ctyp v1, cval_ctyp v2 with + | CT_fbits (0, _), CT_fbits (n2, _) -> + sgen_cval ctx v2 + | CT_fbits (n1, _), CT_fbits (n2, _) -> + sprintf "(%s << %d) | %s" (sgen_cval ctx v1) n2 (sgen_cval ctx v2) + | CT_sbits (64, ord1), CT_fbits (n2, _) -> + sprintf "append_sf(%s, %s, %d)" (sgen_cval ctx v1) (sgen_cval ctx v2) n2 + | CT_fbits (n1, ord1), CT_sbits (64, ord2) -> + sprintf "append_fs(%s, %d, %s)" (sgen_cval ctx v1) n1 (sgen_cval ctx v2) + | CT_sbits (64, ord1), CT_sbits (64, ord2) -> + sprintf "append_ss(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | _, _ -> + failwith "Could not generate cval primop" + +let sgen_cval_param ctx cval = + match cval_ctyp cval with + | CT_lbits direction -> + sgen_cval ctx cval ^ ", " ^ string_of_bool direction + | CT_sbits (_, direction) -> + sgen_cval ctx cval ^ ", " ^ string_of_bool direction + | CT_fbits (len, direction) -> + sgen_cval ctx cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction + | _ -> + sgen_cval ctx cval + +let rec sgen_clexp ctx = function + | CL_id (Have_exception _, _) -> "(state->have_exception)" + | CL_id (Current_exception _, _) -> "(state->current_exception)" + | CL_id (Throw_location _, _) -> "(state->throw_location)" + | CL_id (Return _, _) -> assert false + | CL_id (Global (id, _), _) -> "&(state->" ^ sgen_id id ^ ")" + | CL_id (Name (id, _), _) -> "&" ^ sgen_id id + | CL_field (clexp, field) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ sgen_uid field ^ ")" + | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ mangle ("tup" ^ string_of_int n) ^ ")" + | CL_addr clexp -> "(*(" ^ sgen_clexp ctx clexp ^ "))" + | CL_void -> assert false + | CL_rmw _ -> assert false + +let rec sgen_clexp_pure ctx = function + | CL_id (Have_exception _, _) -> "(state->have_exception)" + | CL_id (Current_exception _, _) -> "(state->current_exception)" + | CL_id (Throw_location _, _) -> "(state->throw_location)" + | CL_id (Return _, _) -> assert false + | CL_id (Global (id, _), _) -> "state->" ^ sgen_id id + | CL_id (Name (id, _), _) -> sgen_id id + | CL_field (clexp, field) -> sgen_clexp_pure ctx clexp ^ "." ^ sgen_uid field + | CL_tuple (clexp, n) -> sgen_clexp_pure ctx clexp ^ "." ^ mangle ("tup" ^ string_of_int n) + | CL_addr clexp -> "(*(" ^ sgen_clexp_pure ctx clexp ^ "))" + | CL_void -> assert false + | CL_rmw _ -> assert false + +(** Generate instructions to copy from a cval to a clexp. This will + insert any needed type conversions from big integers to small + integers (or vice versa), or from arbitrary-length bitvectors to + and from uint64 bitvectors as needed. *) +let rec codegen_conversion l ctx clexp cval = + let ctyp_to = clexp_ctyp clexp in + let ctyp_from = cval_ctyp cval in + match ctyp_to, ctyp_from with + (* When both types are equal, we don't need any conversion. *) + | _, _ when ctyp_equal ctyp_to ctyp_from -> + if is_stack_ctyp ctyp_to then + ksprintf string " %s = %s;" (sgen_clexp_pure ctx clexp) (sgen_cval ctx cval) + else + ksprintf string " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp ctx clexp) (sgen_cval ctx cval) + + | CT_ref ctyp_to, ctyp_from -> + codegen_conversion l ctx (CL_addr clexp) cval + + (* If we have to convert between tuple types, convert the fields individually. *) + | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from -> + let len = List.length ctyps_to in + let conversions = + List.mapi (fun i ctyp -> codegen_conversion l ctx (CL_tuple (clexp, i)) (V_tuple_member (cval, len, i))) ctyps_from + in + string " /* conversions */" + ^^ hardline + ^^ separate hardline conversions + ^^ hardline + ^^ string " /* end conversions */" + + (* For anything not special cased, just try to call a appropriate CONVERT_OF function. *) + | _, _ when is_stack_ctyp (clexp_ctyp clexp) -> + ksprintf string " %s = CONVERT_OF(%s, %s)(%s);" + (sgen_clexp_pure ctx clexp) (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_cval_param ctx cval) + | _, _ -> + ksprintf string " CONVERT_OF(%s, %s)(%s, %s);" + (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_clexp ctx clexp) (sgen_cval_param ctx cval) + +let extra_params () = "sail_state *state, " + +let extra_arguments is_extern = + if is_extern then + "" + else + "state, " + +let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = + match instr with + | I_decl (ctyp, id) when is_stack_ctyp ctyp -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) + | I_decl (ctyp, id) -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline + ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) + + | I_copy (clexp, cval) -> codegen_conversion l ctx clexp cval + + | I_jump (cval, label) -> + ksprintf string " if (%s) goto %s;" (sgen_cval ctx cval) label + + | I_if (cval, [then_instr], [], ctyp) -> + ksprintf string " if (%s)" (sgen_cval ctx cval) ^^ hardline + ^^ twice space ^^ codegen_instr fid ctx then_instr + | I_if (cval, then_instrs, [], ctyp) -> + string " if" ^^ space ^^ parens (string (sgen_cval ctx cval)) ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace) + | I_if (cval, then_instrs, else_instrs, ctyp) -> + string " if" ^^ space ^^ parens (string (sgen_cval ctx cval)) ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace) + ^^ space ^^ string "else" ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) else_instrs) (twice space ^^ rbrace) + + | I_block instrs -> + string " {" + ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline + ^^ string " }" + + | I_try_block instrs -> + string " { /* try */" + ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline + ^^ string " }" + + | I_funcall (x, special_extern, f, args) -> + let c_args = Util.string_of_list ", " (sgen_cval ctx) args in + let ctyp = clexp_ctyp x in + let fname, is_extern = + if special_extern then + (string_of_id (fst f), true) + else if Env.is_extern (fst f) ctx.tc_env "c" then + (Env.get_extern (fst f) ctx.tc_env "c", true) + else + (sgen_function_uid f, false) + in + let sail_state_arg = + if is_extern && StringSet.mem fname O.opts.state_primops then + "sail_state *state, " + else + "" + in + let fname = + match fname, ctyp with + | "internal_pick", _ -> sprintf "pick_%s" (sgen_ctyp_name ctyp) + | "cons", _ -> + begin match snd f with + | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp) + | _ -> Reporting.unreachable l __POS__ "cons without specified type" + end + | "eq_anything", _ -> + begin match args with + | cval :: _ -> sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> Reporting.unreachable l __POS__ "eq_anything function with bad arity." + end + | "length", _ -> + begin match args with + | cval :: _ -> sprintf "length_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> Reporting.unreachable l __POS__ "length function with bad arity." + end + | "vector_access", CT_bit -> "bitvector_access" + | "vector_access", _ -> + begin match args with + | cval :: _ -> sprintf "vector_access_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> Reporting.unreachable l __POS__ "vector access function with bad arity." + end + | "vector_update_subrange", _ -> sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) + | "vector_subrange", _ -> sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) + | "vector_update", CT_fbits _ -> "update_fbits" + | "vector_update", CT_lbits _ -> "update_lbits" + | "vector_update", _ -> sprintf "vector_update_%s" (sgen_ctyp_name ctyp) + | "string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_fbits _ -> "string_of_fbits" + | CT_lbits _ -> "string_of_lbits" + | _ -> assert false + end + | "decimal_string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_fbits _ -> "decimal_string_of_fbits" + | CT_lbits _ -> "decimal_string_of_lbits" + | _ -> assert false + end + | "internal_vector_update", _ -> sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) + | "internal_vector_init", _ -> sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) + | "undefined_bitvector", CT_fbits _ -> "UNDEFINED(fbits)" + | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)" + | "undefined_bit", _ -> "UNDEFINED(fbits)" + | "undefined_vector", _ -> sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) + | "undefined_list", _ -> sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp) + | fname, _ -> fname + in + if fname = "reg_deref" then + if is_stack_ctyp ctyp then + ksprintf string " %s = *(%s);" (sgen_clexp_pure ctx x) c_args + else + ksprintf string " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure ctx x) c_args + else + if is_stack_ctyp ctyp then + ksprintf string " %s = %s(%s%s%s);" (sgen_clexp_pure ctx x) fname sail_state_arg (extra_arguments is_extern) c_args + else + ksprintf string " %s(%s%s%s, %s);" fname sail_state_arg (extra_arguments is_extern) (sgen_clexp ctx x) c_args + + | I_clear (ctyp, id) when is_stack_ctyp ctyp -> + empty + | I_clear (ctyp, id) -> + ksprintf string " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) + + | I_init (ctyp, id, cval) -> + codegen_instr fid ctx (idecl ctyp id) ^^ hardline + ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval + + | I_reinit (ctyp, id, cval) -> + codegen_instr fid ctx (ireset ctyp id) ^^ hardline + ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval + + | I_reset (ctyp, id) when is_stack_ctyp ctyp -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) + | I_reset (ctyp, id) -> + ksprintf string " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) + + | I_return cval -> + ksprintf string " return %s;" (sgen_cval ctx cval) + + | I_throw cval -> + Reporting.unreachable l __POS__ "I_throw reached code generator" + + | I_undefined ctyp -> + let rec codegen_exn_return ctyp = + match ctyp with + | CT_unit -> "UNIT", [] + | CT_bit -> "UINT64_C(0)", [] + | CT_fint _ -> "INT64_C(0xdeadc0de)", [] + (* | CT_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", [] *) + | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] + | CT_sbits _ -> "undefined_sbits()", [] + (* | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits(false)", [] *) + | CT_bool -> "false", [] + | CT_enum (_, ctor :: _) -> sgen_id ctor, [] + | CT_tup ctyps when is_stack_ctyp ctyp -> + let gs = ngensym () in + let fold (inits, prev) (n, ctyp) = + let init, prev' = codegen_exn_return ctyp in + sprintf ".%s = %s" (mangle ("tup" ^ string_of_int n)) init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in + sgen_name gs, + [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | CT_struct (id, ctors) when is_stack_ctyp ctyp -> + let gs = ngensym () in + let fold (inits, prev) (uid, ctyp) = + let init, prev' = codegen_exn_return ctyp in + sprintf ".%s = %s" (sgen_uid uid) init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) ctors in + sgen_name gs, + [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | ctyp -> Reporting.unreachable l __POS__ ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp) + in + let ret, prev = codegen_exn_return ctyp in + separate_map hardline (fun str -> string (" " ^ str)) (List.rev prev) + ^^ hardline + ^^ ksprintf string " return %s;" ret + + | I_comment str -> + string (" /* " ^ str ^ " */") + + | I_label str -> + string (str ^ ": ;") + + | I_goto str -> + ksprintf string " goto %s;" str + + | I_raw _ when ctx.no_raw -> empty + | I_raw str -> + string (" " ^ str) + + | I_end _ -> assert false + + | I_match_failure -> + string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") + +(**************************************************************************) +(* Code generation for type definitions (enums, structs, and variants) *) +(**************************************************************************) + +let codegen_type_def_header = function + | CTD_enum (id, ids) -> + ksprintf string "// enum %s" (string_of_id id) ^^ hardline + ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi] + ^^ twice hardline + + | CTD_struct (id, ctors) -> + let codegen_ctor (id, ctyp) = + string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id + in + ksprintf string "// struct %s" (string_of_id id) ^^ hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_ctor ctors ^^ semi) + rbrace + ^^ semi ^^ twice hardline + + | CTD_variant (id, tus) -> + let codegen_tu (ctor_id, ctyp) = + separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace] + in + ksprintf string "// union %s" (string_of_id id) ^^ hardline + ^^ string "enum" ^^ space + ^^ string ("kind_" ^ sgen_id id) ^^ space + ^^ separate space [ lbrace; + separate_map (comma ^^ space) (fun id -> string ("Kind_" ^ sgen_uid id)) (List.map fst tus); + rbrace ^^ semi ] + ^^ twice hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate space [string "enum"; string ("kind_" ^ sgen_id id); string "kind" ^^ semi] + ^^ hardline + ^^ string "union" ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_tu tus ^^ semi) + rbrace + ^^ semi) + rbrace + ^^ semi + ^^ twice hardline + +let codegen_type_def_body ctx = function + | CTD_enum (id, ((first_id :: _) as ids)) -> + let codegen_eq = + let name = sgen_id id in + string (Printf.sprintf "bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name) + in + let codegen_undefined = + let name = sgen_id id in + string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) + in + codegen_eq + ^^ twice hardline + ^^ codegen_undefined + + | CTD_enum (id, []) -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot compile empty enum " ^ string_of_id id) + + | CTD_struct (id, ctors) -> + let struct_ctyp = CT_struct (id, ctors) in + (* Generate a set_T function for every struct T *) + let codegen_set (id, ctyp) = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op.%s;" (sgen_uid id) (sgen_uid id)) + else + string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid id)) + in + let codegen_setter id ctors = + string (let n = sgen_id id in Printf.sprintf "static void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space + ^^ surround 2 0 lbrace + (separate_map hardline codegen_set (UBindings.bindings ctors)) + rbrace + in + (* Generate an init/clear_T function for every struct T *) + let codegen_field_init f (id, ctyp) = + if not (is_stack_ctyp ctyp) then + [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_uid id))] + else [] + in + let codegen_init f id ctors = + string (let n = sgen_id id in Printf.sprintf "static void %s(%s)(struct %s *op)" f n n) ^^ space + ^^ surround 2 0 lbrace + (separate hardline (UBindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat)) + rbrace + in + let codegen_eq = + let codegen_eq_test (id, ctyp) = + string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid id)) + in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ space + ^^ surround 2 0 lbrace + (string "return" ^^ space + ^^ separate_map (string " && ") codegen_eq_test ctors + ^^ string ";") + rbrace + in + (* Generate the struct and add the generated functions *) + let codegen_ctor (id, ctyp) = + string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id + in + codegen_setter id (ctor_bindings ctors) + ^^ (if not (is_stack_ctyp struct_ctyp) then + twice hardline + ^^ codegen_init "CREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "RECREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "KILL" id (ctor_bindings ctors) + else empty) + ^^ twice hardline + ^^ codegen_eq + + | CTD_variant (id, tus) -> + let codegen_tu (ctor_id, ctyp) = + separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace] + in + (* Create an if, else if, ... block that does something for each constructor *) + let rec each_ctor v f = function + | [] -> string "{}" + | [(ctor_id, ctyp)] -> + string (Printf.sprintf "if (%skind == Kind_%s)" v (sgen_uid ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (f ctor_id ctyp) + ^^ hardline ^^ rbrace + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (%skind == Kind_%s) " v (sgen_uid ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (f ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ each_ctor v f ctors + in + let codegen_init = + let n = sgen_id id in + let ctor_id, ctyp = List.hd tus in + string (Printf.sprintf "static void CREATE(%s)(struct %s *op)" n n) + ^^ hardline + ^^ surround 2 0 lbrace + (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_uid ctor_id)) ^^ hardline + ^^ if not (is_stack_ctyp ctyp) then + string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) + else empty) + rbrace + in + let codegen_reinit = + let n = sgen_id id in + string (Printf.sprintf "static void RECREATE(%s)(struct %s *op) {}" n n) + in + let clear_field v ctor_id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "/* do nothing */") + else + string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_uid ctor_id)) + in + let codegen_clear = + let n = sgen_id id in + string (Printf.sprintf "static void KILL(%s)(struct %s *op)" n n) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "op->" (clear_field "op") tus ^^ semi) + rbrace + in + let codegen_ctor (ctor_id, ctyp) = + let ctor_args = Printf.sprintf "%s op" (sgen_ctyp ctyp) in + string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_uid ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "rop->" (clear_field "rop") tus ^^ hardline + ^^ string ("rop->kind = Kind_" ^ sgen_uid ctor_id) ^^ semi ^^ hardline + ^^ if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op;" (sgen_uid ctor_id)) + else + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) ^^ hardline + ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id))) + rbrace + in + let codegen_setter = + let n = sgen_id id in + let set_field ctor_id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op.%s;" (sgen_uid ctor_id) (sgen_uid ctor_id)) + else + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) + ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid ctor_id)) + in + string (Printf.sprintf "static void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "rop->" (clear_field "rop") tus + ^^ semi ^^ hardline + ^^ string "rop->kind = op.kind" + ^^ semi ^^ hardline + ^^ each_ctor "op." set_field tus) + rbrace + in + let codegen_eq = + let codegen_eq_test ctor_id ctyp = + string (Printf.sprintf "return EQUAL(%s)(op1.%s, op2.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid ctor_id)) + in + let rec codegen_eq_tests = function + | [] -> string "return false;" + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (op1.kind == Kind_%s && op2.kind == Kind_%s) " (sgen_uid ctor_id) (sgen_uid ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (codegen_eq_test ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ codegen_eq_tests ctors + in + let n = sgen_id id in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2) " n n n) + ^^ surround 2 0 lbrace (codegen_eq_tests tus) rbrace + in + codegen_init + ^^ twice hardline + ^^ codegen_reinit + ^^ twice hardline + ^^ codegen_clear + ^^ twice hardline + ^^ codegen_setter + ^^ twice hardline + ^^ codegen_eq + ^^ twice hardline + ^^ separate_map (twice hardline) codegen_ctor tus + +let codegen_type_def ctx ctype_def = + codegen_type_def_header ctype_def, codegen_type_def_body ctx ctype_def + +(**************************************************************************) +(* Code generation for generated types (lists, tuples, etc) *) +(**************************************************************************) + +(** GLOBAL: because C doesn't have real anonymous tuple types + (anonymous structs don't quite work the way we need) every tuple + type in the spec becomes some generated named struct in C. This is + done in such a way that every possible tuple type has a unique name + associated with it. This global variable keeps track of these + generated struct names, so we never generate two copies of the + struct that is used to represent them in C. + + The way this works is that codegen_def scans each definition's type + annotations for tuple types and generates the required structs + using codegen_type_def before the actual definition is generated by + codegen_def'. + + This variable should be reset to empty only when the entire AST has + been translated to C. **) +let generated = ref IdSet.empty + +let codegen_tup ctx ctyps = + let id = mk_id ("tuple_" ^ string_of_ctyp (CT_tup ctyps)) in + if IdSet.mem id !generated then + empty, empty + else + begin + let _, fields = List.fold_left (fun (n, fields) ctyp -> n + 1, UBindings.add (mk_id ("tup" ^ string_of_int n), []) ctyp fields) + (0, UBindings.empty) + ctyps + in + generated := IdSet.add id !generated; + codegen_type_def ctx (CTD_struct (id, UBindings.bindings fields)) + end + +let codegen_list_header id = + ksprintf string "// generated list type %s" (string_of_id id) ^^ hardline + ^^ ksprintf string "struct node_%s;" (sgen_id id) ^^ hardline + ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id) + ^^ twice hardline + +let codegen_node id ctyp = + ksprintf string "struct node_%s {\n %s hd;\n struct node_%s *tl;\n};\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) + ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id) + +let codegen_list_init id = + ksprintf string "static void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id) + +let codegen_list_clear id ctyp = + ksprintf string "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (*rop == NULL) return;" + ^^ (if is_stack_ctyp ctyp then empty + else ksprintf string " KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) + ^^ ksprintf string " KILL(%s)(&(*rop)->tl);\n" (sgen_id id) + ^^ string " sail_free(*rop);" + ^^ string "}" + +let codegen_list_recreate id = + ksprintf string "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id) + +let codegen_list_set id ctyp = + ksprintf string "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ string " if (op == NULL) { *rop = NULL; return; };\n" + ^^ ksprintf string " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id) + ^^ (if is_stack_ctyp ctyp then + string " (*rop)->hd = op->hd;\n" + else + ksprintf string " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp) + ^^ ksprintf string " COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp)) + ^^ ksprintf string " internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id) + ^^ string "}" + ^^ twice hardline + ^^ ksprintf string "static void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " KILL(%s)(rop);\n" (sgen_id id) + ^^ ksprintf string " internal_set_%s(rop, op);\n" (sgen_id id) + ^^ string "}" + +let codegen_cons id ctyp = + let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in + ksprintf string "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) + ^^ ksprintf string " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id) + ^^ (if is_stack_ctyp ctyp then + string " (*rop)->hd = x;\n" + else + ksprintf string " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp) + ^^ ksprintf string " COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp)) + ^^ string " (*rop)->tl = xs;\n" + ^^ string "}" + +let codegen_pick id ctyp = + if is_stack_ctyp ctyp then + ksprintf string "static %s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id) + else + ksprintf string "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) + +let codegen_list_equal id ctyp = + ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (op1 == NULL && op2 == NULL) { return true; };\n" + ^^ ksprintf string " if (op1 == NULL || op2 == NULL) { return false; };\n" + ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id) + ^^ string "}" + +let codegen_list_undefined id ctyp = + ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp) + ^^ ksprintf string " *rop = NULL;\n" + ^^ string "}" + +let codegen_list ctx ctyp = + let id = mk_id (string_of_ctyp (CT_list ctyp)) in + if IdSet.mem id !generated then ( + (empty, empty) + ) else ( + generated := IdSet.add id !generated; + let header = codegen_list_header id in + let body = + codegen_node id ctyp ^^ twice hardline + ^^ codegen_list_init id ^^ twice hardline + ^^ codegen_list_clear id ctyp ^^ twice hardline + ^^ codegen_list_recreate id ^^ twice hardline + ^^ codegen_list_set id ctyp ^^ twice hardline + ^^ codegen_cons id ctyp ^^ twice hardline + ^^ codegen_pick id ctyp ^^ twice hardline + ^^ codegen_list_equal id ctyp ^^ twice hardline + ^^ codegen_list_undefined id ctyp + in + (header, body) + ) + +(* Generate functions for working with non-bit vectors of some specific type. *) +let codegen_vector_header ctx id (direction, ctyp) = + let vector_typedef = + string (Printf.sprintf "struct %s {\n size_t len;\n %s *data;\n};\n" (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id)) + in + vector_typedef ^^ twice hardline + +let codegen_vector_body ctx id (direction, ctyp) = + let vector_init = + string (Printf.sprintf "static void CREATE(%s)(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id)) + in + let vector_set = + string (Printf.sprintf "static void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id)) + ^^ string " rop->len = op.len;\n" + ^^ string (Printf.sprintf " rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string " for (int i = 0; i < op.len; i++) {\n" + ^^ string (if is_stack_ctyp ctyp then + " (rop->data)[i] = op.data[i];\n" + else + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + let vector_clear = + string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)) + ^^ (if is_stack_ctyp ctyp then empty + else + string " for (int i = 0; i < (rop->len); i++) {\n" + ^^ string (Printf.sprintf " KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n") + ^^ string " if (rop->data != NULL) sail_free(rop->data);\n" + ^^ string "}" + in + let vector_update = + string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, sail_int n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string " int m = sail_int_get_ui(n);\n" + ^^ string " if (rop->data == op.data) {\n" + ^^ string (if is_stack_ctyp ctyp then + " rop->data[m] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string " } else {\n" + ^^ string (Printf.sprintf " COPY(%s)(rop, op);\n" (sgen_id id)) + ^^ string (if is_stack_ctyp ctyp then + " rop->data[m] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + let internal_vector_update = + string (Printf.sprintf "static void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (if is_stack_ctyp ctyp then + " rop->data[n] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string "}" + in + let vector_access = + if is_stack_ctyp ctyp then + string (Printf.sprintf "static %s vector_access_%s(%s op, sail_int n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id)) + ^^ string " int m = sail_int_get_ui(n);\n" + ^^ string " return op.data[m];\n" + ^^ string "}" + else + string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, sail_int n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + ^^ string " int m = sail_int_get_ui(n);\n" + ^^ string (Printf.sprintf " COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp)) + ^^ string "}" + in + let internal_vector_init = + string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id)) + ^^ string " rop->len = len;\n" + ^^ string (Printf.sprintf " rop->data = sail_malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ (if not (is_stack_ctyp ctyp) then + string " for (int i = 0; i < len; i++) {\n" + ^^ string (Printf.sprintf " CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n" + else empty) + ^^ string "}" + in + let vector_undefined = + string (Printf.sprintf "static void undefined_vector_%s(%s *rop, sail_int len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf " rop->len = sail_int_get_ui(len);\n") + ^^ string (Printf.sprintf " rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string " for (int i = 0; i < (rop->len); i++) {\n" + ^^ string (if is_stack_ctyp ctyp then + " (rop->data)[i] = elem;\n" + else + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + vector_init ^^ twice hardline + ^^ vector_clear ^^ twice hardline + ^^ vector_undefined ^^ twice hardline + ^^ vector_access ^^ twice hardline + ^^ vector_set ^^ twice hardline + ^^ vector_update ^^ twice hardline + ^^ internal_vector_update ^^ twice hardline + ^^ internal_vector_init ^^ twice hardline + +let codegen_vector ctx (direction, ctyp) = + let id = mk_id (string_of_ctyp (CT_vector (direction, ctyp))) in + if IdSet.mem id !generated then ( + empty, empty + ) else ( + generated := IdSet.add id !generated; + codegen_vector_header ctx id (direction, ctyp), + codegen_vector_body ctx id (direction, ctyp) + ) + +(**************************************************************************) +(* Code generation for definitions *) +(**************************************************************************) + +(** To keep things neat we use GCC's local labels extension to limit + the scope of labels. We do this by iterating over all the blocks + and adding a __label__ declaration with all the labels local to + that block. + + See https://gcc.gnu.org/onlinedocs/gcc/Local-Labels.html **) +let add_local_labels' instrs = + let is_label (I_aux (instr, _)) = + match instr with + | I_label str -> [str] + | _ -> [] + in + let labels = List.concat (List.map is_label instrs) in + let local_label_decl = iraw ("__label__ " ^ String.concat ", " labels ^ ";\n") in + if labels = [] then + instrs + else + local_label_decl :: instrs + +let is_decl = function + | I_aux (I_decl _, _) -> true + | _ -> false + +let codegen_decl = function + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id)) + | _ -> assert false + +let codegen_alloc = function + | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) + | _ -> assert false + +let add_local_labels instrs = + match map_instrs add_local_labels' (iblock instrs) with + | I_aux (I_block instrs, _) -> instrs + | _ -> assert false + +let codegen_def_header ctx = function + | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> + if Env.is_extern id ctx.tc_env "c" then + empty + else if is_stack_ctyp ret_ctyp then + ksprintf string "%s %s(%s%s);" + (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps) + ^^ twice hardline + else + ksprintf string "void %s(%s%s *rop, %s);" + (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps) + ^^ twice hardline + + | CDEF_type ctype_def -> + codegen_type_def_header ctype_def + + | _ -> empty + +let codegen_def_body ctx = function + | CDEF_reg_dec _ -> empty + + | CDEF_spec _ -> empty + + | CDEF_fundef (id, ret_arg, args, instrs) as def -> + let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with + | Some vs -> vs + | None -> + Reporting.unreachable (id_loc id) __POS__ ("No valspec found for " ^ string_of_id id) + in + + (* Check that the function has the correct arity at this point. *) + if List.length arg_ctyps <> List.length args then + Reporting.unreachable (id_loc id) __POS__ + ("function arguments " + ^ Util.string_of_list ", " string_of_id args + ^ " matched against type " + ^ Util.string_of_list ", " string_of_ctyp arg_ctyps) + else (); + + let instrs = add_local_labels instrs in + let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in + let function_header = + match ret_arg with + | None -> + assert (is_stack_ctyp ret_ctyp); + string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline + | Some gs -> + assert (not (is_stack_ctyp ret_ctyp)); + string "void" ^^ space ^^ codegen_function_id id + ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) + ^^ hardline + in + function_header + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline + ^^ string "}" + ^^ twice hardline + + | CDEF_type ctype_def -> + codegen_type_def_body ctx ctype_def + + | CDEF_startup (id, instrs) -> + let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_function_id id)) in + separate_map hardline codegen_decl instrs + ^^ twice hardline + ^^ startup_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline codegen_alloc instrs) ^^ hardline + ^^ string "}" + + | CDEF_finish (id, instrs) -> + let finish_header = string (Printf.sprintf "void finish_%s(void)" (sgen_function_id id)) in + separate_map hardline codegen_decl (List.filter is_decl instrs) + ^^ twice hardline + ^^ finish_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline + ^^ string "}" + + | CDEF_let (number, bindings, instrs) -> + let instrs = add_local_labels instrs in + let setup = + List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (global id)]) bindings) + in + let cleanup = + List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (global id)]) bindings) + in + hardline ^^ string (Printf.sprintf "void sail_create_letbind_%d(sail_state *state) " number) + ^^ string "{" + ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline + ^^ string "}" + ^^ hardline ^^ string (Printf.sprintf "void sail_kill_letbind_%d(sail_state *state) " number) + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline + ^^ string "}" + ^^ twice hardline + +(** As we generate C we need to generate specialized version of tuple, + list, and vector type. These must be generated in the correct + order. The ctyp_dependencies function generates a list of + c_gen_typs in the order they must be generated. Types may be + repeated in ctyp_dependencies so it's up to the code-generator not + to repeat definitions pointlessly (using the !generated variable) + *) +type c_gen_typ = + | CTG_tup of ctyp list + | CTG_list of ctyp + | CTG_vector of bool * ctyp + +let rec ctyp_dependencies = function + | CT_tup ctyps -> List.concat (List.map ctyp_dependencies ctyps) @ [CTG_tup ctyps] + | CT_list ctyp -> ctyp_dependencies ctyp @ [CTG_list ctyp] + | CT_vector (direction, ctyp) | CT_fvector (_, direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)] + | CT_ref ctyp -> ctyp_dependencies ctyp + | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors) + | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors) + | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly | CT_constant _ -> [] + +let codegen_ctg ctx = function + | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp) + | CTG_tup ctyps -> codegen_tup ctx ctyps + | CTG_list ctyp -> codegen_list ctx ctyp + +let codegen_progress n total = function + | CDEF_reg_dec (id, _, _) -> + Util.progress "Codegen " ("R " ^ string_of_id id) n total + | CDEF_fundef (id, _, _, _) -> + Util.progress "Codegen " (string_of_id id) n total + | _ -> + Util.progress "Codegen " "" n total + +(** When we generate code for a definition, we need to first generate + any auxillary type definitions that are required. *) +let codegen_def n total ctx def = + codegen_progress n total def; + let ctyps = cdef_ctyps def |> CTSet.elements in + (* We should have erased any polymorphism introduced by variants at this point! *) + if List.exists is_polymorphic ctyps then + let polymorphic_ctyps = List.filter is_polymorphic ctyps in + Reporting.unreachable Parse_ast.Unknown __POS__ + (sprintf "Found polymorphic types:\n%s\nwhile generating definition." + (Util.string_of_list "\n" string_of_ctyp polymorphic_ctyps)) + else + let deps = List.concat (List.map ctyp_dependencies ctyps) in + let deps_header, deps_body = List.map (codegen_ctg ctx) deps |> List.split in + concat deps_header ^^ codegen_def_header ctx def, + concat deps_body ^^ codegen_def_body ctx def + +let codegen_state_struct_def ctx = function + | CDEF_reg_dec (id, ctyp, _) -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline + + | CDEF_let (_, [], _) -> empty + | CDEF_let (_, bindings, _) -> + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + ^^ hardline + + | _ -> empty + +let codegen_state_struct ctx cdefs = + string "struct sail_state {" ^^ hardline + ^^ concat_map (codegen_state_struct_def ctx) cdefs + ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then ( + empty + ) else ( + string " // exception handling support" ^^ hardline + ^^ ksprintf string " struct %s *current_exception;" (sgen_id (mk_id "exception")) ^^ hardline + ^^ string " bool have_exception;" ^^ hardline + ^^ string " sail_string *throw_location;" ^^ hardline + )) + ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) O.opts.extra_state + ^^ string "};" + +let is_cdef_startup = function + | CDEF_startup _ -> true + | _ -> false + +let sgen_startup = function + | CDEF_startup (id, _) -> + Printf.sprintf " startup_%s();" (sgen_id id) + | _ -> assert false + +let sgen_instr id ctx instr = + Pretty_print_sail.to_string (codegen_instr id ctx instr) + +let is_cdef_finish = function + | CDEF_startup _ -> true + | _ -> false + +let sgen_finish = function + | CDEF_startup (id, _) -> + Printf.sprintf " finish_%s();" (sgen_id id) + | _ -> assert false + +let rec get_recursive_functions (Defs defs) = + match defs with + | DEF_internal_mutrec fundefs :: defs -> + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + + | (DEF_fundef fdef as def) :: defs -> + let open Rewriter in + let ids = ref IdSet.empty in + let collect_funcalls e_aux annot = + match e_aux with + | E_app (id, args) -> (ids := IdSet.add id !ids; E_aux (e_aux, annot)) + | _ -> E_aux (e_aux, annot) + in + let map_exp = { + id_exp_alg with + e_aux = (fun (e_aux, annot) -> collect_funcalls e_aux annot) + } in + let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in + let _ = rewrite_def map_defs def in + if IdSet.mem (id_of_fundef fdef) !ids then + IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + else + get_recursive_functions (Defs defs) + + | _ :: defs -> get_recursive_functions (Defs defs) + | [] -> IdSet.empty + +let codegen_output file_name docs = + let chan = open_out file_name in + output_string chan (Pretty_print_sail.to_string docs); + flush chan; + close_out chan + +let add_extra_header str = + if String.length str > 0 then ( + if str.[0] == '<' && str.[String.length str - 1] == '>' then + string ("#include " ^ str) ^^ hardline + else + string ("#include \"" ^ str ^ "\"") ^^ hardline + ) else ( + empty + ) + +let codegen ctx output_name cdefs = + let total = List.length cdefs in + let docs_header, docs_body = List.mapi (fun n def -> codegen_def (n + 1) total ctx def) cdefs |> List.split in + + let state = codegen_state_struct ctx cdefs in + + let stdlib_headers = + string "#include <stdint.h>" ^^ hardline + ^^ string "#include <stdbool.h>" + in + let sail_headers = + string "#include \"sail.h\"" ^^ hardline + ^^ string "#include \"sail_failure.h\"" + in + + let register_init_clear (id, ctyp, instrs) = + if is_stack_ctyp ctyp then + List.map (sgen_instr (mk_id "reg") ctx) instrs, [] + else + [ Printf.sprintf " CREATE(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ] + @ List.map (sgen_instr (mk_id "reg") ctx) instrs, + [ Printf.sprintf " KILL(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ] + in + + let header = + stdlib_headers ^^ hardline + ^^ sail_headers ^^ hardline + ^^ concat_map add_extra_header O.opts.extra_headers ^^ hardline + ^^ string "struct sail_state;" ^^ hardline + ^^ string "typedef struct sail_state sail_state;" + ^^ twice hardline + ^^ concat docs_header + ^^ state + ^^ twice hardline + ^^ string "void sail_initialize_state(sail_state *state);" + ^^ hardline + ^^ string "void sail_finalize_state(sail_state *state);" + ^^ hardline + in + + let regs = c_ast_registers cdefs in + + let letbind_initializers = + List.map (fun n -> Printf.sprintf " sail_create_letbind_%d(state);" n) (List.rev ctx.letbinds) + in + let letbind_finalizers = + List.map (fun n -> Printf.sprintf " sail_kill_letbind_%d(state);" n) ctx.letbinds + in + + let body = + ksprintf string "#include \"%s.h\"" (Filename.basename output_name) + ^^ twice hardline + ^^ concat docs_body + ^^ string "void sail_initialize_letbindings(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string letbind_initializers ^^ hardline + ^^ string "}" + ^^ twice hardline + ^^ string "void sail_finalize_letbindings(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string letbind_finalizers ^^ hardline + ^^ string "}" + ^^ twice hardline + ^^ string "void sail_initialize_state(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string (List.map (fun r -> fst (register_init_clear r)) regs |> List.concat) + ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then ( + empty + ) else ( + string " state->have_exception = false;" + ^^ ksprintf string " state->current_exception = sail_malloc(sizeof(struct %s));" + (sgen_id (mk_id "exception")) ^^ hardline + ^^ ksprintf string " CREATE(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline + ^^ string " state->throw_location = sail_malloc(sizeof(sail_string));" ^^ hardline + ^^ string " CREATE(sail_string)(state->throw_location);" + )) + ^^ hardline + ^^ string " sail_initialize_letbindings(state);" ^^ hardline + ^^ string "}" + ^^ twice hardline + ^^ string "void sail_finalize_state(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string (List.map (fun r -> snd (register_init_clear r)) regs |> List.concat) + ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then ( + empty + ) else ( + ksprintf string " KILL(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline + ^^ string " sail_free(state->current_exception);" ^^ hardline + ^^ string " KILL(sail_string)(state->throw_location);" ^^ hardline + ^^ string " sail_free(state->throw_location);" + )) + ^^ hardline + ^^ string " sail_finalize_letbindings(state);" ^^ hardline + ^^ string "}" + ^^ hardline + in + + codegen_output (output_name ^ ".h") header; + codegen_output (output_name ^ ".c") body + +let emulator ctx output_name cdefs = + codegen ctx output_name cdefs; + + let headers = separate hardline + ([ string "#include \"sail.h\""; + string "#include \"sail_failure.h\""; + string "#include \"rts.h\""; + string "#include \"elf.h\""; + ksprintf string "#include \"%s.h\"" (Filename.basename output_name) ] + @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*))) + in + + let startup cdefs = + List.map sgen_startup (List.filter is_cdef_startup cdefs) + in + let finish cdefs = + List.map sgen_finish (List.filter is_cdef_finish cdefs) + in + + let regs = c_ast_registers cdefs in + + let model_init = separate hardline (List.map string + ( [ "void model_initialize(sail_state *state)"; + "{"; + " sail_initialize_state(state);"; + " setup_rts();" ] + @ startup cdefs + @ (if regs = [] then [] else [ Printf.sprintf " %s(state, UNIT);" (sgen_function_id (mk_id "initialize_registers")) ]) + @ [ "}" ] )) + in + + let model_fini = separate hardline (List.map string + ( [ "void model_finalize(sail_state *state)"; + "{" ] + @ finish cdefs + @ [ " cleanup_rts();"; + " sail_finalize_state(state);"; + "}" ])) + in + + let model_default_main = separate hardline (List.map string + ([ "int model_main(int argc, char *argv[])"; + "{"; + " sail_state state;"; + " model_initialize(&state);"; + " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; + sprintf " %s(&state, UNIT);" (sgen_function_id (mk_id "main")) ] + @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else + [ " if (state.have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *state.throw_location);}" ]) + @ [ " model_finalize(&state);" ] + @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else + [ " if (state.have_exception) {return(EXIT_FAILURE);}" ]) + @ [ " return EXIT_SUCCESS;"; + "}" ])) + in + + let model_main = separate hardline (List.map string + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ]) + in + + let emu = + headers ^^ twice hardline + ^^ model_init ^^ twice hardline + ^^ model_fini ^^ twice hardline + ^^ model_default_main ^^ twice hardline + ^^ model_main ^^ hardline + in + codegen_output (output_name ^ "_emu.c") emu + +end diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 34477967..84705ae2 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -58,7 +58,6 @@ open Value2 open Anf let opt_memo_cache = ref false -let opt_track_throw = ref true let optimize_aarch64_fast_struct = ref false @@ -174,11 +173,13 @@ let initial_ctx env = module type Config = sig val convert_typ : ctx -> typ -> ctyp val optimize_anf : ctx -> typ aexp -> typ aexp - val unroll_loops : unit -> int option + val unroll_loops : int option val specialize_calls : bool val ignore_64 : bool val struct_value : bool val use_real : bool + val branch_coverage : bool + val track_throw : bool end module Make(C: Config) = struct @@ -190,6 +191,59 @@ let rec chunkify n xs = | xs, [] -> [xs] | xs, ys -> xs :: chunkify n ys +let name_or_global ctx id = + if Env.is_register id ctx.local_env || IdSet.mem id (Env.get_toplevel_lets ctx.local_env) then + global id + else + name id + +let coverage_branch_count = ref 0 + +let coverage_loc_args l = + match Reporting.simp_loc l with + | None -> None + | Some (p1, p2) -> + Some (Printf.sprintf "\"%s\", %d, %d, %d, %d" + (String.escaped p1.pos_fname) p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)) + +let coverage_branch_reached l = + let branch_id = !coverage_branch_count in + incr coverage_branch_count; + branch_id, + if C.branch_coverage then + begin match coverage_loc_args l with + | None -> [] + | Some args -> + [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)] + end + else + [] + +let append_into_block instrs instr = + match instrs with + | [] -> instr + | _ -> iblock (instrs @ [instr]) + +let coverage_branch_taken branch_id (AE_aux (_, _, l)) = + if not C.branch_coverage then + [] + else + match coverage_loc_args l with + | None -> [] + | Some args -> + print_endline ("B " ^ args); + [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)] + +let coverage_function_entry id l = + if not C.branch_coverage then + [] + else + match coverage_loc_args l with + | None -> [] + | Some args -> + print_endline ("F " ^ args); + [iraw (Printf.sprintf "sail_function_entry(\"%s\", %s);" (string_of_id id) args)] + let rec compile_aval l ctx = function | AV_cval (cval, typ) -> let ctyp = cval_ctyp cval in @@ -201,13 +255,11 @@ let rec compile_aval l ctx = function [], cval, [] | AV_id (id, typ) -> - begin - try - let _, ctyp = Bindings.find id ctx.locals in - [], V_id (name id, ctyp), [] - with - | Not_found -> - [], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), [] + begin match Bindings.find_opt id ctx.locals with + | Some (_, ctyp) -> + [], V_id (name id, ctyp), [] + | None -> + [], V_id (name_or_global ctx id, ctyp_of_typ ctx (lvar_typ typ)), [] end | AV_ref (id, typ) -> @@ -520,7 +572,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | AP_global (pid, typ) -> let global_ctyp = ctyp_of_typ ctx typ in - [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx + [icopy l (CL_id (global pid, global_ctyp)) cval], [], ctx | AP_id (pid, _) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with @@ -624,6 +676,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_case (aval, cases, typ) -> let ctyp = ctyp_of_typ ctx typ in let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + (* Get the number of cases, because we don't want to check branch + coverage for matches with only a single case. *) + let num_cases = List.length cases in + let branch_id, on_reached = coverage_branch_reached l in let case_return_id = ngensym () in let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = @@ -643,7 +699,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) - @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ body_setup + @ (if num_cases > 1 then coverage_branch_taken branch_id body else []) + @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in if is_dead_aexp body then @@ -651,7 +709,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = else [iblock case_instrs; ilabel case_label] in - aval_setup @ [idecl ctyp case_return_id] + aval_setup + @ (if num_cases > 1 then on_reached else []) + @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], @@ -664,8 +724,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctyp = ctyp_of_typ ctx typ in let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in let try_return_id = ngensym () in - let handled_exception_label = label "handled_exception_" in - let fallthrough_label = label "fallthrough_exception_" in + let post_exception_handlers_label = label "post_exception_handlers_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) @@ -686,19 +745,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ [icomment "end guard"] else []) @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup - @ [igoto handled_exception_label] + @ [igoto post_exception_handlers_label] in [iblock case_instrs; ilabel try_label] in assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [idecl ctyp try_return_id; itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); - ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label] + ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) post_exception_handlers_label; + icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool))] @ List.concat (List.map compile_case cases) - @ [igoto fallthrough_label; - ilabel handled_exception_label; - icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool)); - ilabel fallthrough_label], + @ [(* fallthrough *) + icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool)); + ilabel post_exception_handlers_label], (fun clexp -> icopy l clexp (V_id (try_return_id, ctyp))), [] @@ -709,16 +768,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = compile_aexp ctx then_aexp else let if_ctyp = ctyp_of_typ ctx if_typ in + let branch_id, on_reached = coverage_branch_reached l in let compile_branch aexp = let setup, call, cleanup = compile_aexp ctx aexp in - fun clexp -> setup @ [call clexp] @ cleanup + fun clexp -> coverage_branch_taken branch_id aexp @ setup @ [call clexp] @ cleanup in let setup, cval, cleanup = compile_aval l ctx aval in setup, - (fun clexp -> iif l cval - (compile_branch then_aexp clexp) - (compile_branch else_aexp clexp) - if_ctyp), + (fun clexp -> + append_into_block on_reached + (iif l cval + (compile_branch then_aexp clexp) + (compile_branch else_aexp clexp) + if_ctyp)), cleanup (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) @@ -778,7 +840,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup - @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), (field_id, []))) cval] + @ [icopy l (CL_field (CL_id (name_or_global ctx id, ctyp_of_typ ctx typ), (field_id, []))) cval] @ field_cleanup in List.concat (List.map compile_fields (Bindings.bindings fields)), @@ -792,7 +854,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | None -> ctyp_of_typ ctx assign_typ in let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup + setup @ [call (CL_id (name_or_global ctx id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup | AE_write_ref (id, assign_typ, aexp) -> let assign_ctyp = @@ -801,7 +863,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | None -> ctyp_of_typ ctx assign_typ in let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_addr (CL_id (name id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup + setup @ [call (CL_addr (CL_id (name_or_global ctx id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in @@ -948,7 +1010,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* We can either generate an actual loop body for C, or unroll the body for SMT *) let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in - let body = match C.unroll_loops () with Some times -> unroll times 0 | None -> actual in + let body = match C.unroll_loops with Some times -> unroll times 0 | None -> actual in variable_init from_gs from_setup from_call from_cleanup @ variable_init to_gs to_setup to_call to_cleanup @@ -1057,7 +1119,7 @@ let fix_exception_block ?return:(return=None) ctx instrs = before @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval; icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool))] - @ (if !opt_track_throw then + @ (if C.track_throw then let loc_string = Reporting.short_loc_to_string l in [icopy l (CL_id (throw_location, CT_string)) (V_lit (VL_string loc_string, CT_string))] else []) @@ -1258,6 +1320,7 @@ let compile_funcl ctx id pat guard exp = let instrs = arg_setup @ destructure @ guard_instrs @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + let instrs = coverage_function_entry id (exp_loc exp) @ instrs in [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx @@ -1302,7 +1365,7 @@ and compile_def' n total ctx = function | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in + let instrs = setup @ [call (CL_id (global id, ctyp_of_typ ctx typ))] @ cleanup in [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx | DEF_reg_dec (DEC_aux (_, (l, _))) -> diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 9014d8f7..47ca6962 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -61,11 +61,15 @@ open Type_check ARM v8.5 spec. It is unsound in general. *) val optimize_aarch64_fast_struct : bool ref -(** If true (default) track the location of the last exception thrown, - useful for debugging C but we want to turn it off for SMT generation - where we can't use strings *) -val opt_track_throw : bool ref - +(** (WIP) [opt_memo_cache] will store the compiled function + definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum + of the original function to be compiled. Enabled using the -memo + flag. Uses Marshal so it's quite picky about the exact version of + the Sail version. This cache can obviously become stale if the Sail + changes - it'll load an old version compiled without said + changes. *) +val opt_memo_cache : bool ref + (** {2 Jib context} *) (** Dynamic context for compiling Sail to Jib. We need to pass a @@ -96,7 +100,7 @@ module type Config = sig val optimize_anf : ctx -> typ aexp -> typ aexp (** Unroll all for loops a bounded number of times. Used for SMT generation. *) - val unroll_loops : unit -> int option + val unroll_loops : int option (** If false, function arguments must match the function type exactly. If true, they can be more specific. *) val specialize_calls : bool @@ -108,6 +112,12 @@ module type Config = sig val struct_value : bool (** Allow real literals *) val use_real : bool + (** Insert branch coverage operations *) + val branch_coverage : bool + (** If true track the location of the last exception thrown, useful + for debugging C but we want to turn it off for SMT generation + where we can't use strings *) + val track_throw : bool end module Make(C: Config) : sig diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml index 4bf726aa..d30fe183 100644 --- a/src/jib/jib_ir.ml +++ b/src/jib/jib_ir.ml @@ -62,7 +62,7 @@ module StringMap = Map.Make(String) let string_of_name = let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in function - | Name (id, n) -> zencode_id id ^ ssa_num n + | Name (id, n) | Global (id, n) -> zencode_id id ^ ssa_num n | Have_exception n -> "have_exception" ^ ssa_num n | Return n -> diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index e0f3bf0d..f156a040 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -76,6 +76,7 @@ let optimize_unit instrs = in let non_pointless_copy (I_aux (aux, annot)) = match aux with + | I_decl (CT_unit, _) -> false | I_copy (CL_void, _) -> false | _ -> true in @@ -245,6 +246,7 @@ let rec find_function fid = function let ssa_name i = function | Name (id, _) -> Name (id, i) + | Global (id, _) -> Global (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i | Throw_location _ -> Throw_location i diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 310a38a5..26509a69 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -345,7 +345,7 @@ let rec smt_cval ctx cval = | _ -> match cval with | V_lit (vl, ctyp) -> smt_value ctx vl ctyp - | V_id (Name (id, _) as ssa_id, _) -> + | V_id ((Name (id, _) | Global (id, _)) as ssa_id, _) -> begin match Type_check.Env.lookup_id id ctx.tc_env with | Enum _ -> Enum (zencode_id id) | _ when Bindings.mem id ctx.shared -> Shared (zencode_id id) @@ -1405,8 +1405,8 @@ let rec generate_ctype_defs ctx = function | [] -> [] let rec generate_reg_decs ctx inits = function - | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits)-> - Declare_const (zencode_name (Name (id, 0)), smt_ctyp ctx ctyp) + | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Global (id, 0)) inits)-> + Declare_const (zencode_name (Global (id, 0)), smt_ctyp ctx ctyp) :: generate_reg_decs ctx inits cdefs | _ :: cdefs -> generate_reg_decs ctx inits cdefs | [] -> [] @@ -1418,7 +1418,7 @@ let rec generate_reg_decs ctx inits = function let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) -module SMT_config : Jib_compile.Config = struct +module SMT_config(Opts : sig val unroll_limit : int end) : Jib_compile.Config = struct open Jib_compile (** Convert a sail type into a C-type. This function can be quite @@ -1581,9 +1581,11 @@ let unroll_static_foreach ctx = function let specialize_calls = true let ignore_64 = true - let unroll_loops () = Some !opt_unroll_limit + let unroll_loops = Some Opts.unroll_limit let struct_value = true let use_real = true + let branch_coverage = false + let track_throw = false end @@ -1897,7 +1899,7 @@ let smt_instr ctx = | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> begin match id, cval with - | Name (id, _), _ when IdSet.mem id ctx.preserved -> + | (Name (id, _) | Global (id, _)), _ when IdSet.mem id ctx.preserved -> [preserve_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] | _, V_lit (VL_undefined, _) -> @@ -1959,7 +1961,7 @@ let rec find_function lets id = function | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 -> lets, Some (heap_return, args, body) | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in find_function (lets @ vars @ setup) id cdefs; | _ :: cdefs -> find_function lets id cdefs @@ -2145,7 +2147,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_write_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - ifuncall (CL_id (name r, reg_ctyp)) function_id args; + ifuncall (CL_id (global r, reg_ctyp)) function_id args; igoto end_label; ilabel next_label] in @@ -2169,7 +2171,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_deref_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label; - icopy l clexp (V_id (name r, reg_ctyp)); + icopy l clexp (V_id (global r, reg_ctyp)); igoto end_label; ilabel next_label] in @@ -2191,7 +2193,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_write_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - icopy l (CL_id (name r, reg_ctyp)) cval; + icopy l (CL_id (global r, reg_ctyp)) cval; igoto end_label; ilabel next_label] in @@ -2325,7 +2327,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function let rec smt_cdefs props lets name_file ctx ast = function | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs; | cdef :: cdefs -> smt_cdef props lets name_file ctx ast cdef; @@ -2351,7 +2353,7 @@ let rec build_register_map rmap = function let compile env ast = let cdefs, jib_ctx = - let module Jibc = Jib_compile.Make(SMT_config) in + let module Jibc = Jib_compile.Make(SMT_config(struct let unroll_limit = !opt_unroll_limit end)) in let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in let t = Profile.start () in let cdefs, ctx = Jibc.compile_ast ctx ast in diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index fe3238a4..f9777f9e 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -502,6 +502,7 @@ let rename_variables graph root children = let ssa_name i = function | Name (id, _) -> Name (id, i) + | Global (id, _) -> Global (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i | Throw_location _ -> Throw_location i diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 9b06c7be..88f09bcf 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -144,11 +144,16 @@ module Name = struct | Name (x, n), Name (y, m) -> let c1 = Id.compare x y in if c1 = 0 then compare n m else c1 + | Global (x, n), Global (y, m) -> + let c1 = Id.compare x y in + if c1 = 0 then compare n m else c1 | Have_exception n, Have_exception m -> compare n m | Current_exception n, Current_exception m -> compare n m | Return n, Return m -> compare n m | Name _, _ -> 1 | _, Name _ -> -1 + | Global _, _ -> 1 + | _, Global _ -> -1 | Have_exception _, _ -> 1 | _, Have_exception _ -> -1 | Current_exception _, _ -> 1 @@ -166,6 +171,7 @@ let throw_location = Throw_location (-1) let return = Return (-1) let name id = Name (id, -1) +let global id = Global (id, -1) let rec cval_rename from_id to_id = function | V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp) @@ -261,7 +267,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) = let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true) = let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in function - | Name (id, n) -> + | Name (id, n) | Global (id, n) -> (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n | Have_exception n -> "have_exception" ^ ssa_num n diff --git a/src/lexer.mll b/src/lexer.mll index 8000879e..40f4b470 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -288,8 +288,10 @@ rule token = parse | "-" digit+ as i { (Num(Big_int.of_string i)) } | "0b" (binarydigit+ as i) { (Bin(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) } | "0x" (hexdigit+ as i) { (Hex(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) } - | '"' { (String( - string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) } + | '"' { let startpos = Lexing.lexeme_start_p lexbuf in + let contents = string startpos (Buffer.create 10) lexbuf in + lexbuf.lex_start_p <- startpos; + String(contents) } | eof { Eof } | _ as c { raise (LexError( Printf.sprintf "Unexpected character: %c" c, @@ -331,10 +333,6 @@ and string pos b = parse | '\\' '\n' ws { Lexing.new_line lexbuf; string pos b lexbuf } | '\\' { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos, "illegal backslash escape in string"*) } - | '"' { let s = unescaped(Buffer.contents b) in - (*try Ulib.UTF8.validate s; s - with Ulib.UTF8.Malformed_code -> - raise (Reporting.Fatal_error (Reporting.Err_syntax (pos, - "String literal is not valid utf8"))) *) s } + | '"' { unescaped (Buffer.contents b) } | eof { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos, "String literal not terminated")))*) } diff --git a/src/process_file.ml b/src/process_file.ml index d2a86595..116788b9 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -108,6 +108,8 @@ let have_symbol symbol = let clear_symbols () = symbols := default_symbols +let add_symbol str = symbols := StringSet.add str !symbols + let cond_pragma l defs = let depth = ref 0 in let in_then = ref true in diff --git a/src/process_file.mli b/src/process_file.mli index d1fa2cb8..c9eb5e9e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -54,6 +54,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val clear_symbols : unit -> unit val have_symbol : string -> bool +val add_symbol : string -> unit val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/reporting.ml b/src/reporting.ml index d5e3003c..603bc84f 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -127,6 +127,11 @@ let short_loc_to_string l = Printf.sprintf "%s %d:%d - %d:%d" p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol) +let loc_to_coverage l = + match simp_loc l with + | None -> None + | Some (p1, p2) -> Some (p1.pos_fname, p1.pos_cnum - p1.pos_bol, p2.pos_lnum, p2.pos_cnum - p2.pos_bol) + let print_err l m1 m2 = print_err_internal (Loc l) m1 m2 @@ -179,7 +184,7 @@ let ignored_files = ref StringSet.empty let suppress_warnings_for_file f = ignored_files := StringSet.add f !ignored_files - + let warn str1 l str2 = if !opt_warnings then match simp_loc l with @@ -191,3 +196,5 @@ let warn str1 l str2 = | Some _ -> () else () + +let simple_warn str = warn str Parse_ast.Unknown "" diff --git a/src/reporting.mli b/src/reporting.mli index e0744c66..54875398 100644 --- a/src/reporting.mli +++ b/src/reporting.mli @@ -116,6 +116,9 @@ val print_error : error -> unit location, the second after. *) val warn : string -> Parse_ast.l -> string -> unit +(** Print a simple one-line warning without a location. *) +val simple_warn: string -> unit + (** Will suppress all warnings for a given file. Used by $suppress_warnings directive in process_file.ml *) val suppress_warnings_for_file : string -> unit diff --git a/src/rewrites.ml b/src/rewrites.ml index f9ce4d84..35659bb4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -489,6 +489,13 @@ let remove_vector_concat_pat pat = let decls = List.fold_left (fun f g x -> f (g x)) (fun b -> b) decls in + (* Finally we patch up the top location for the expressions wrapped + by decls, otherwise this can cause the coverage instrumentation + to get super confused by the generated locations *) + let decls (E_aux (_, (l, _)) as exp) = + let E_aux (aux, (_, annot)) = decls exp in + E_aux (aux, (gen_loc l, annot)) in + (* at this point shouldn't have P_as patterns in P_vector_concat patterns any more, all P_as and P_id vectors should have their declarations in decls. Now flatten all vector_concat patterns *) @@ -691,7 +698,7 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2 | P_wild, _ -> Some [] - | P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) -> + | P_app (Id_aux (id1,_),args1), P_app (Id_aux (id2,_),args2) -> if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None | P_vector pats1, P_vector pats2 | P_vector_concat pats1, P_vector_concat pats2 @@ -1394,9 +1401,6 @@ let updates_vars exp = lit vectors in patterns or expressions *) let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) = - let rewrap e = E_aux (e,annot) in - let rewrap_effects e eff = - E_aux (e, (l,Some (env_of_annot annot, typ_of_annot annot, eff))) in let rewrite_rec = rewriters.rewrite_exp rewriters in let rewrite_base = rewrite_exp rewriters in match exp with @@ -5132,6 +5136,7 @@ let rewrites_target tgt = | "lem" -> rewrites_lem | "ocaml" -> rewrites_ocaml | "c" -> rewrites_c + | "c2" -> rewrites_c | "ir" -> rewrites_c @ [("properties", [])] | "smt" -> rewrites_c @ [("properties", [])] | "sail" -> [] diff --git a/src/sail.ml b/src/sail.ml index b2ca498a..34fffd2e 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -51,9 +51,13 @@ open Process_file module Big_int = Nat_big_num +module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None +(* Note: May cause a deprecated warning for json type, but this cannot be + fixed without breaking Ubuntu 18.04 CI *) +let opt_config : Json.json option ref = ref None let opt_print_version = ref false let opt_target = ref None let opt_tofrominterp_output_dir : string option ref = ref None @@ -72,25 +76,45 @@ let opt_have_feature = ref None let set_target name = Arg.Unit (fun _ -> opt_target := Some name) +let load_json_config file = + try Json.from_file file with + | Yojson.Json_error desc | Sys_error desc -> + prerr_endline "Error when loading configuration file:"; + prerr_endline desc; + exit 1 + let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix"); ( "-i", - Arg.Tuple [Arg.Set Interactive.opt_interactive], + Arg.Tuple [Arg.Set Interactive.opt_interactive; + Arg.Set Interactive.opt_auto_interpreter_rewrites; + Arg.Set Initial_check.opt_undefined_gen], " start interactive interpreter"); ( "-is", - Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.String (fun s -> opt_interactive_script := Some s)], + Arg.Tuple [Arg.Set Interactive.opt_interactive; + Arg.Set Interactive.opt_auto_interpreter_rewrites; + Arg.Set Initial_check.opt_undefined_gen; + Arg.String (fun s -> opt_interactive_script := Some s)], "<filename> start interactive interpreter and execute commands in script"); ( "-iout", Arg.String (fun file -> Value.output_redirect (open_out file)), "<filename> print interpreter output to file"); + ( "-interact_custom", + Arg.Set Interactive.opt_interactive, + " drop to an interactive session after running Sail. Differs from \ + -i in that it does not set up the interpreter in the interactive \ + shell."); ( "-emacs", Arg.Set Interactive.opt_emacs_mode, " run sail interactively as an emacs mode child process"); ( "-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings"); + ( "-config", + Arg.String (fun file -> opt_config := Some (load_json_config file)), + " JSON configuration file"); ( "-tofrominterp", set_target "tofrominterp", " output OCaml functions to translate between shallow embedding and interpreter"); @@ -149,10 +173,10 @@ let options = Arg.align ([ set_target "ir", " print intermediate representation"); ( "-smt", - Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw], + Arg.Tuple [set_target "smt"], " print SMT translated version of input"); ( "-smt_auto", - Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw; Arg.Set Jib_smt.opt_auto], + Arg.Tuple [set_target "smt"; Arg.Set Jib_smt.opt_auto], " generate SMT and automatically call the solver (implies -smt)"); ( "-smt_ignore_overflow", Arg.Set Jib_smt.opt_ignore_overflow, @@ -175,6 +199,9 @@ let options = Arg.align ([ ( "-c", Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); + ( "-c2", + Arg.Tuple [set_target "c2"; Arg.Set Initial_check.opt_undefined_gen], + " output a C translated version of the input (experimental code-generation)"); ( "-c_include", Arg.String (fun i -> opt_includes_c := i::!opt_includes_c), "<filename> provide additional include for C output"); @@ -205,6 +232,9 @@ let options = Arg.align ([ ( "-c_fold_unit", Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str), " remove comma separated list of functions from C output, replacing them with unit"); + ( "-c_coverage", + Arg.Set C_backend.opt_branch_coverage, + " instrument C code to track branch coverage"); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); @@ -294,7 +324,7 @@ let options = Arg.align ([ Arg.Clear opt_memo_z3, " do not memoize calls to z3 (default)"); ( "-memo", - Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], + Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set Jib_compile.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); ( "-have_feature", Arg.String (fun symbol -> opt_have_feature := Some symbol), @@ -464,6 +494,32 @@ let target name out_name ast type_envs = flush output_chan; if close then close_out output_chan else () + | Some "c2" -> + let module StringMap = Map.Make(String) in + let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in + let ast_c, type_envs = + if !opt_specialize_c then + Specialize.(specialize_passes 2 int_specialization type_envs ast_c) + else + ast_c, type_envs + in + let output_name = match !opt_file_out with Some f -> f | None -> "out" in + Reporting.opt_warnings := true; + let codegen ctx cdefs = + let open Json.Util in + let codegen_opts = match !opt_config with + | Some config -> C_codegen.options_from_json (member "codegen" config) cdefs + | None -> C_codegen.default_options cdefs + in + let module Codegen = + C_codegen.Make( + struct let opts = codegen_opts end + ) + in + Codegen.emulator ctx output_name cdefs + in + C_backend.compile_ast_clib type_envs ast_c codegen; + | Some "ir" -> let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *) diff --git a/src/type_check.ml b/src/type_check.ml index 9b70f645..e471f33d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2994,7 +2994,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_exp = crule check_exp env exp exc_typ in annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape]) | E_var (lexp, bind, exp), _ -> - let lexp, bind, env = match bind_assignment env lexp bind with + let lexp, bind, env = match bind_assignment l env lexp bind with | E_aux (E_assign (lexp, bind), _), env -> lexp, bind, env | _, _ -> assert false in @@ -3059,8 +3059,8 @@ and check_block l env exps ret_typ = match Nl_flow.analyze exps with | [] -> (match ret_typ with Some typ -> typ_equality l env typ unit_typ; [] | None -> []) | [exp] -> [final env exp] - | (E_aux (E_assign (lexp, bind), _) :: exps) -> - let texp, env = bind_assignment env lexp bind in + | (E_aux (E_assign (lexp, bind), (assign_l, _)) :: exps) -> + let texp, env = bind_assignment assign_l env lexp bind in texp :: check_block l env exps ret_typ | ((E_aux (E_assert (constr_exp, msg), _) as exp) :: exps) -> let msg = assert_msg msg in @@ -3548,9 +3548,9 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (A_aux (typ_arg_au | _, A_order _ -> typ_error env l "Cannot bind type pattern against order" | _, _ -> typ_error env l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat) -and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) = - let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in - let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, mk_tannot env typ eff)) in +and bind_assignment assign_l env (LEXP_aux (lexp_aux, (lexp_l, ())) as lexp) (E_aux (_, (exp_l, ())) as exp) = + let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (assign_l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in + let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (lexp_l, mk_tannot env typ eff)) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in let has_typ v env = match Env.lookup_id v env with @@ -3559,7 +3559,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as in match lexp_aux with | LEXP_memory (f, xs) -> - check_exp env (E_aux (E_app (f, xs @ [exp]), (l, ()))) unit_typ, env + check_exp env (E_aux (E_app (f, xs @ [exp]), (lexp_l, ()))) unit_typ, env | LEXP_cast (typ_annot, v) -> let checked_exp = crule check_exp env exp typ_annot in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in @@ -3817,7 +3817,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let inferred_exps = List.map (irule infer_exp env) exps in annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps))) | E_assign (lexp, bind) -> - fst (bind_assignment env lexp bind) + fst (bind_assignment l env lexp bind) | E_record_update (exp, fexps) -> let inferred_exp = irule infer_exp env exp in let typ = typ_of inferred_exp in diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail index f9d7e7c5..458d8dfd 100644 --- a/test/builtins/divmod.sail +++ b/test/builtins/divmod.sail @@ -5,39 +5,67 @@ $include <arith.sail> $include <smt.sail> function main (() : unit) -> unit = { - assert(ediv_int( 7 , 5) == 1); - assert(ediv_int( 7 , -5) == -1); - assert(ediv_int(-7 , 5) == -2); - assert(ediv_int(-7 , -5) == 2); - assert(ediv_int( 12 , 3) == 4); - assert(ediv_int( 12 , -3) == -4); - assert(ediv_int(-12 , 3) == -4); - assert(ediv_int(-12 , -3) == 4); + assert(ediv_int(7, 5) == 1); + assert(ediv_int(7, -5) == -1); + assert(ediv_int(-7, 5) == -2); + assert(ediv_int(-7, -5) == 2); + assert(ediv_int(12, 3) == 4); + assert(ediv_int(12, -3) == -4); + assert(ediv_int(-12, 3) == -4); + assert(ediv_int(-12, -3) == 4); - assert(emod_int( 7 , 5) == 2); - assert(emod_int( 7 , -5) == 2); - assert(emod_int(-7 , 5) == 3); - assert(emod_int(-7 , -5) == 3); - assert(emod_int( 12 , 3) == 0); - assert(emod_int( 12 , -3) == 0); - assert(emod_int(-12 , 3) == 0); - assert(emod_int(-12 , -3) == 0); + assert(emod_int(7, 5) == 2); + assert(emod_int(7, -5) == 2); + assert(emod_int(-7, 5) == 3); + assert(emod_int(-7, -5) == 3); + assert(emod_int(12, 3) == 0); + assert(emod_int(12, -3) == 0); + assert(emod_int(-12, 3) == 0); + assert(emod_int(-12, -3) == 0); - assert(tdiv_int( 7 , 5) == 1); - assert(tdiv_int( 7 , -5) == -1); - assert(tdiv_int(-7 , 5) == -1); - assert(tdiv_int(-7 , -5) == 1); - assert(tdiv_int( 12 , 3) == 4); - assert(tdiv_int( 12 , -3) == -4); - assert(tdiv_int(-12 , 3) == -4); - assert(tdiv_int(-12 , -3) == 4); + assert(tdiv_int(7, 5) == 1); + assert(tdiv_int(7, -5) == -1); + assert(tdiv_int(-7, 5) == -1); + assert(tdiv_int(-7, -5) == 1); + assert(tdiv_int(12, 3) == 4); + assert(tdiv_int(12, -3) == -4); + assert(tdiv_int(-12, 3) == -4); + assert(tdiv_int(-12, -3) == 4); - assert(tmod_int( 7 , 5) == 2); - assert(tmod_int( 7 , -5) == 2); - assert(tmod_int(-7 , 5) == -2); - assert(tmod_int(-7 , -5) == -2); - assert(tmod_int( 12 , 3) == 0); - assert(tmod_int( 12 , -3) == 0); - assert(tmod_int(-12 , 3) == 0); - assert(tmod_int(-12 , -3) == 0); + assert(tmod_int(7, 5) == 2); + assert(tmod_int(7, -5) == 2); + assert(tmod_int(-7, 5) == -2); + assert(tmod_int(-7, -5) == -2); + assert(tmod_int(12, 3) == 0); + assert(tmod_int(12, -3) == 0); + assert(tmod_int(-12, 3) == 0); + assert(tmod_int(-12, -3) == 0); + + assert(fdiv_int(7, 5) == 1); + assert(fdiv_int(7, -5) == -2); + assert(fdiv_int(-7, 5) == -2); + assert(fdiv_int(-7, -5) == 1); + assert(fdiv_int(12, 3) == 4); + assert(fdiv_int(12, -3) == -4); + assert(fdiv_int(-12, 3) == -4); + assert(fdiv_int(-12, -3) == 4); + + assert(fmod_int(7, 5) == 2); + assert(fmod_int(7, -5) == -3); + assert(fmod_int(-7, 5) == 3); + assert(fmod_int(-7, -5) == -2); + assert(fmod_int(12, 3) == 0); + assert(fmod_int(12, -3) == 0); + assert(fmod_int(-12, 3) == 0); + assert(fmod_int(-12, -3) == 0); + + assert(fdiv_int(5, 2) == 2); + assert(fdiv_int(-5, -2) == 2); + assert(fdiv_int(5, -2) == -3); + assert(fdiv_int(-5, 2) == -3); + + assert(tdiv_int(5, 2) == 2); + assert(tdiv_int(-5, -2) == 2); + assert(tdiv_int(5, -2) == -2); + assert(tdiv_int(-5, 2) == -2); }
\ No newline at end of file diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail index a9480ab6..51001ec3 100644 --- a/test/c/cheri_capreg.sail +++ b/test/c/cheri_capreg.sail @@ -63,29 +63,6 @@ struct CapStruct = { length : bits(64), } -let null_cap : CapStruct = struct { - tag = false, - padding = zeros(), - otype = zeros(), - uperms = zeros(), - perm_reserved11_14 = zeros(), - access_system_regs = false, - permit_unseal = false, - permit_ccall = false, - permit_seal = false, - permit_store_local_cap = false, - permit_store_cap = false, - permit_load_cap = false, - permit_store = false, - permit_load = false, - permit_execute = false, - global = false, - sealed = false, - address = zeros(), - base = zeros(), - length = 0xffffffffffffffff -} - let default_cap : CapStruct = struct { tag = true, padding = zeros(), diff --git a/test/c/exception.expect b/test/c/exception.expect index 79d97c6a..faab808f 100644 --- a/test/c/exception.expect +++ b/test/c/exception.expect @@ -4,3 +4,5 @@ Caught Estring test 2nd try Caught Epair x = 33 +in g() +Fall through OK diff --git a/test/c/exception.sail b/test/c/exception.sail index 4e74fcae..251852c9 100644 --- a/test/c/exception.sail +++ b/test/c/exception.sail @@ -47,6 +47,19 @@ function main () = { }, _ => () }; + try throw(Eunknown()) catch { + _ => try let _ = g() in () catch { + _ => print("caught old exception") + } + }; + try + try throw Eunknown() catch { + Estring(_) => () + } + catch { + Eunknown() => print("Fall through OK"), + _ => () + }; f(); () -}
\ No newline at end of file +} diff --git a/test/c/execute.isail b/test/c/execute.isail index 018dd92c..f4b5ea0f 100644 --- a/test/c/execute.isail +++ b/test/c/execute.isail @@ -1,4 +1,3 @@ -:rewrites interpreter initialize_registers() :run main() diff --git a/test/c/run_tests.py b/test/c/run_tests.py index c9474614..28a4d28d 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -26,6 +26,28 @@ def test_c(name, c_opts, sail_opts, valgrind): step('diff {}.result {}.expect'.format(basename, basename)) if valgrind: step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}.bin".format(basename), expected_status = 1 if basename == "exception" else 0) + step('rm {}.c {}.bin {}.result'.format(basename, basename, basename)) + print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) + sys.exit() + results.collect(tests) + return results.finish() + +def test_c2(name, c_opts, sail_opts, valgrind): + banner('Testing {} with C (-c2) options: {} Sail options: {} valgrind: {}'.format(name, c_opts, sail_opts, valgrind)) + results = Results(name) + for filenames in chunks(os.listdir('.'), parallel()): + tests = {} + for filename in filenames: + basename = os.path.splitext(os.path.basename(filename))[0] + tests[filename] = os.fork() + if tests[filename] == 0: + step('sail -no_warn -c2 {} {} -o {}'.format(sail_opts, filename, basename)) + step('gcc {} {}.c {}_emu.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, basename, sail_dir, sail_dir, basename)) + step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) + step('diff {}.result {}.expect'.format(basename, basename)) + if valgrind: + step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0) + step('rm {}.c {} {}.result'.format(basename, basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -42,6 +64,7 @@ def test_interpreter(name): if tests[filename] == 0: step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename)) step('diff {}.iresult {}.expect'.format(basename, basename)) + step('rm {}.iresult'.format(basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -59,6 +82,8 @@ def test_ocaml(name): step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {}_ocaml {}'.format(basename, basename, filename)) step('./{}_ocaml 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.oresult {}.expect'.format(basename, basename)) + step('rm -r _sbuild_{}'.format(basename)) + step('rm {}.oresult {}_ocaml'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -90,6 +115,7 @@ def test_lem(name): xml = '<testsuites>\n' +xml += test_c2('unoptimized C', '', '', True) xml += test_c('unoptimized C', '', '', True) xml += test_c('optimized C', '-O2', '-O', True) xml += test_c('constant folding', '', '-Oconstant_fold', True) diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 8045141f..6605aba4 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [[96mReplicate/v2.sail[0m]:13:4-30 13[96m |[0m replicate_bits(x, 'N / 'M) [91m |[0m [91m^------------------------^[0m - [91m |[0m Tried performing type coercion from {('ex194# : Int), true. bitvector(('M * 'ex194#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) + [91m |[0m Tried performing type coercion from {('ex215# : Int), true. bitvector(('M * 'ex215#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) [91m |[0m Coercion failed because: [91m |[0m Mismatched argument types in subtype check [91m |[0m diff --git a/test/typecheck/pass/constant_nexp/v2.expect b/test/typecheck/pass/constant_nexp/v2.expect index 7c0e8093..75a7f380 100644 --- a/test/typecheck/pass/constant_nexp/v2.expect +++ b/test/typecheck/pass/constant_nexp/v2.expect @@ -3,6 +3,6 @@ Type error: 12[96m |[0m let _ = czeros(sizeof('n - 10) + 20); [91m |[0m [91m^--------------------------^[0m [91m |[0m Could not resolve quantifiers for czeros - [91m |[0m [94m*[0m is_constant(('fv50#n : Int)) + [91m |[0m [94m*[0m is_constant(('fv130#n : Int)) [91m |[0m [94m*[0m (('n - 10) + 20) >= 0 [91m |[0m diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 8d061933..80ebe927 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26[96m |[0m Some(Ctor1(a, x, c)) [91m |[0m [91m^------------^[0m [91m |[0m Could not resolve quantifiers for Ctor1 - [91m |[0m [94m*[0m datasize('ex276#) + [91m |[0m [94m*[0m datasize('ex297#) [91m |[0m diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index b8427446..4e65ab38 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error: [91m |[0m [91m^---------------^[0m [91m |[0m Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (33, unsigned(a)) [91m |[0m Coercion failed because: - [91m |[0m (int(33), int('ex232#)) is not a subtype of (int('ex227#), int('ex228#)) + [91m |[0m (int(33), int('ex253#)) is not a subtype of (int('ex248#), int('ex249#)) [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex227# bound here + [91m |[0m [93m |[0m 'ex248# bound here [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex228# bound here + [91m |[0m [93m |[0m 'ex249# bound here [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex232# bound here + [91m |[0m [93m |[0m 'ex253# bound here [91m |[0m diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 4df0b3aa..04d53f11 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error: [91m |[0m [91m^---------------^[0m [91m |[0m Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (31, unsigned(a)) [91m |[0m Coercion failed because: - [91m |[0m (int(31), int('ex232#)) is not a subtype of (int('ex227#), int('ex228#)) + [91m |[0m (int(31), int('ex253#)) is not a subtype of (int('ex248#), int('ex249#)) [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex227# bound here + [91m |[0m [93m |[0m 'ex248# bound here [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex228# bound here + [91m |[0m [93m |[0m 'ex249# bound here [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65 [91m |[0m 17[96m |[0m if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a)); [91m |[0m [93m |[0m [93m^---------------^[0m - [91m |[0m [93m |[0m 'ex232# bound here + [91m |[0m [93m |[0m 'ex253# bound here [91m |[0m diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 61a664c5..cae93129 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25[96m |[0m Some(Ctor(64, unsigned(0b0 @ b @ a))) [91m |[0m [91m^-----------------------------^[0m [91m |[0m Could not resolve quantifiers for Ctor - [91m |[0m [94m*[0m (datasize(64) & (0 <= 'ex271# & 'ex271# < 64)) + [91m |[0m [94m*[0m (datasize(64) & (0 <= 'ex292# & 'ex292# < 64)) [91m |[0m diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index e6ce41c6..9810cfd4 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 'ex188# & 'ex188# < 3) + [91m |[0m [94m*[0m (0 <= 'ex209# & 'ex209# < 3) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 7d796f18..707d2217 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,7 +5,7 @@ Type error: [91m |[0m No overloading for vector_access, tried: [91m |[0m [94m*[0m bitvector_access [91m |[0m Could not resolve quantifiers for bitvector_access - [91m |[0m [94m*[0m (0 <= 'ex188# & 'ex188# < 4) + [91m |[0m [94m*[0m (0 <= 'ex209# & 'ex209# < 4) [91m |[0m [94m*[0m plain_vector_access [91m |[0m No valid casts resulted in unification [91m |[0m diff --git a/test/typecheck/pass/reg_32_64/v1.expect b/test/typecheck/pass/reg_32_64/v1.expect index eb398991..4c80e83d 100644 --- a/test/typecheck/pass/reg_32_64/v1.expect +++ b/test/typecheck/pass/reg_32_64/v1.expect @@ -1,7 +1,7 @@ Type error: -[[96mreg_32_64/v1.sail[0m]:35:9-28 +[[96mreg_32_64/v1.sail[0m]:35:2-6 35[96m |[0m R(0) = 0xCAFE_CAFE_0000_00; - [91m |[0m [91m^-----------------^[0m + [91m |[0m [91m^--^[0m [91m |[0m No overloading for R, tried: [91m |[0m [94m*[0m set_R [91m |[0m Could not resolve quantifiers for set_R |