diff options
| -rw-r--r-- | aarch64/no_devices.sail | 4 | ||||
| -rw-r--r-- | doc/introduction.tex | 67 | ||||
| -rw-r--r-- | doc/manual.tex | 2 | ||||
| -rw-r--r-- | lib/rts.c | 4 | ||||
| -rw-r--r-- | lib/rts.h | 2 | ||||
| -rw-r--r-- | lib/sail.c | 13 | ||||
| -rw-r--r-- | lib/sail.h | 3 | ||||
| -rw-r--r-- | mips/prelude.sail | 8 | ||||
| -rw-r--r-- | src/c_backend.ml | 3 | ||||
| -rw-r--r-- | src/isail.ml | 25 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 15 | ||||
| -rw-r--r-- | src/rewrites.ml | 1 | ||||
| -rw-r--r-- | src/value.ml | 4 | ||||
| -rwxr-xr-x | test/cheri/run_tests.sh | 2 |
14 files changed, 98 insertions, 55 deletions
diff --git a/aarch64/no_devices.sail b/aarch64/no_devices.sail index 882aa6b3..57dad4e2 100644 --- a/aarch64/no_devices.sail +++ b/aarch64/no_devices.sail @@ -1,6 +1,6 @@ val ___WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem} + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmem} val __InitRAM : forall 'm. (atom('m), int, bits('m), bits(8)) -> unit @@ -25,7 +25,7 @@ val __WriteRAM : forall 'n 'm. function __WriteRAM(addr_length, bytes, hex_ram, addr, data) = { - ___WriteRAM(addr_length, bytes, hex_ram, addr, data) + let _ = ___WriteRAM(addr_length, bytes, hex_ram, addr, data) in () } function __TraceMemoryWrite(bytes, addr, data) = () diff --git a/doc/introduction.tex b/doc/introduction.tex index 9e268de5..1f9d9dba 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -21,27 +21,27 @@ pseudocode, which has recently become machine-processed~\cite{Reid16}. For MIPS~\cite{MIPS64-II,MIPS64-III} there is also reasonably detailed pseudocode. -The behaviour of concurrent code is often described less well. In a -line of research from 2007--2018 we have developed mathematically -rigorous models for the allowed architectural envelope of concurrent -code, for x86, IBM Power, \riscv, and ARM, that have been reasonably -well validated by experimental testing and by discussion with the -vendors and -others~\cite{x86popl,tphols09,cacm,CAV2010,Alglave:2011:LRT:1987389.1987395,pldi105,pldi2012,micro2015,FGP16,mixed17}. -In the course of this, we have identified a number of subtle issues -relating to the interface between the intra-instruction semantics and -the inter-instruction concurrency -semantics~\cite{pldi105,pldi2012,micro2015,FGP16,mixed17}. For -example, the concurrency models, rather than treating each instruction -execution as an atomic unit, require exposed register and memory -events, knowledge of the potential register and memory footprints of -instructions, and knowledge of changes to those during execution. Our -early work in this area had hand-coded instruction semantics for quite -small fragments of the instruction sets, just enough for concurrency -litmus tests and expressed in various ad hoc ways. As our models have -matured, we have switched to modelling the intra-instruction semantics -more completely and in a style closer to the vendor-documentation -pseudocode, and Sail was developed for this. +%% The behaviour of concurrent code is often described less well. In a +%% line of research from 2007--2018 we have developed mathematically +%% rigorous models for the allowed architectural envelope of concurrent +%% code, for x86, IBM Power, \riscv, and ARM, that have been reasonably +%% well validated by experimental testing and by discussion with the +%% vendors and +%% others\anonymiseomit{~\cite{x86popl,tphols09,cacm,CAV2010,Alglave:2011:LRT:1987389.1987395,pldi105,pldi2012,micro2015,FGP16,mixed17}}. +%% In the course of this, we have identified a number of subtle issues +%% relating to the interface between the intra-instruction semantics and +%% the inter-instruction concurrency +%% semantics\anonymiseomit{~\cite{pldi105,pldi2012,micro2015,FGP16,mixed17}}. For +%% example, the concurrency models, rather than treating each instruction +%% execution as an atomic unit, require exposed register and memory +%% events, knowledge of the potential register and memory footprints of +%% instructions, and knowledge of changes to those during execution. Our +%% early work in this area had hand-coded instruction semantics for quite +%% small fragments of the instruction sets, just enough for concurrency +%% litmus tests and expressed in various ad hoc ways. As our models have +%% matured, we have switched to modelling the intra-instruction semantics +%% more completely and in a style closer to the vendor-documentation +%% pseudocode, and Sail was developed for this. Sail is intended: @@ -77,7 +77,7 @@ and generate: \item An internal representation of the fully type-annotated definition (a deep embedding of the definition) in a form that can be executed by the Sail interpreter. These are both expressed in - Lem~\cite{Lem-icfp2014,Lemcode}, a language of type, function, and + Lem\anonymiseomit{~\cite{Lem-icfp2014,Lemcode}}, a language of type, function, and relation definitions that can be compiled into OCaml and various theorem provers. The Sail interpreter can also be used to analyse instruction definitions (or partially executed instructions) to @@ -101,25 +101,26 @@ binary descriptions, although this is something we plan to add. Sail has been used to develop models of parts of several architectures: \begin{center} \begin{tabular}{|l|l|} \hline -ARMv8 (hand) & hand-written \\ \hline +% ARMv8 (hand) & hand-written \\ \hline ARMv8 (ASL) & generated from ARM's v8.3 public ASL spec \\ \hline -IBM Power & extracted/patched from IBM Framemaker XML \\ \hline +% IBM Power & extracted/patched from IBM Framemaker XML \\ \hline MIPS & hand-written \\ \hline CHERI & hand-written \\ \hline \riscv & hand-written \\ \hline \end{tabular} \end{center} -The ARMv8 (hand) and IBM Power models cover all user-mode instructions -except vector, float, and load-multiple instructions, without -exceptions; for ARMv8 this is for the A64 fragment. +%% The ARMv8 (hand) and IBM Power models cover all user-mode instructions +%% except vector, float, and load-multiple instructions, without +%% exceptions; for ARMv8 this is for the A64 fragment. -The ARMv8 (hand) model is hand-written based on the ARMv8-A -specification document~\cite{armarmv8,FGP16}, principally by \anonymise{Flur}. +%% The ARMv8 (hand) model is hand-written based on the ARMv8-A +%% specification document\anonymiseomit{~\cite{armarmv8,FGP16}}, +%% principally by \anonymise{Flur}. -The Power model is based on an automatic extraction of pseudocode and -decoding data from an XML export of the Framemaker document source of -the IBM Power manual~\cite{Power2.06,micro2015}, with manual patching -as necessary, principally by \anonymise{Kerneis and Gray}. +%% The Power model is based on an automatic extraction of pseudocode and +%% decoding data from an XML export of the Framemaker document source of +%% the IBM Power manual\anonymiseomit{~\cite{Power2.06,micro2015}}, with manual patching +%% as necessary, principally by \anonymise{Kerneis and Gray}. The ARMv8 (ASL) model is based on an automatic translation of ARM's machine-readable public v8.3 ASL specification\footnote{ARM v8-A diff --git a/doc/manual.tex b/doc/manual.tex index d28719a4..d731ecd3 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -67,11 +67,13 @@ \ifdefined\ANON \author{Anonymous} \newcommand\anonymise[1]{\emph{redacted}} +\newcommand\anonymiseomit[1]{} \else \author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and Peter Sewell} \newcommand\anonymise[1]{#1} +\newcommand\anonymiseomit[1]{#1} \fi \maketitle @@ -208,7 +208,7 @@ void kill_mem() // ***** Memory builtins ***** -unit write_ram(const mpz_t addr_size, // Either 32 or 64 +bool write_ram(const mpz_t addr_size, // Either 32 or 64 const mpz_t data_size_mpz, // Number of bytes const sail_bits hex_ram, // Currently unused const sail_bits addr_bv, @@ -231,7 +231,7 @@ unit write_ram(const mpz_t addr_size, // Either 32 or 64 } mpz_clear(buf); - return UNIT; + return true; } void read_ram(sail_bits *data, @@ -53,7 +53,7 @@ uint64_t read_mem(uint64_t); // These memory builtins are intended to match the semantics for the // __ReadRAM and __WriteRAM functions in ASL. -unit write_ram(const mpz_t addr_size, // Either 32 or 64 +bool write_ram(const mpz_t addr_size, // Either 32 or 64 const mpz_t data_size_mpz, // Number of bytes const sail_bits hex_ram, // Currently unused const sail_bits addr_bv, @@ -781,6 +781,19 @@ void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits } } +void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2) +{ + rop->len = op1.len; + mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2)); + normalize_sail_bits(rop); +} + +void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2) +{ + rop->len = op1.len; + mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2)); +} + void reverse_endianness(sail_bits *rop, const sail_bits op) { rop->len = op.len; @@ -273,6 +273,9 @@ void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2); void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2); void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2); +void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2); + void reverse_endianness(sail_bits*, sail_bits); /* ***** Sail reals ***** */ diff --git a/mips/prelude.sail b/mips/prelude.sail index 037819bc..4c77d522 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -116,19 +116,19 @@ val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int -val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} +val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} -val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} +val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom", c:"max_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} overload min = {min_atom, min_nat, min_int} overload max = {max_atom, max_nat, max_int} val __WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv} + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} val __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -function __MIPS_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) +function __MIPS_write (addr, width, data) = let _ = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) in () val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} diff --git a/src/c_backend.ml b/src/c_backend.ml index e4bbd393..cb732e2d 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -2655,7 +2655,8 @@ let instrument_tracing ctx = let module StringSet = Set.Make(String) in let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in let rec instrument = function - | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs -> + | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs when not (Env.is_extern id ctx.tc_env "c") -> + let trace_start = iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id))) in diff --git a/src/isail.ml b/src/isail.ml index 593167f9..4adc1cd2 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -127,7 +127,12 @@ let rec run () = print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal | Step (out, state, _, stack) -> - current_mode := Evaluation (eval_frame !interactive_ast frame); + begin + try + current_mode := Evaluation (eval_frame !interactive_ast frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; run () | Break frame -> print_endline "Breakpoint"; @@ -147,7 +152,12 @@ let rec run_steps n = print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal | Step (out, state, _, stack) -> - current_mode := Evaluation (eval_frame !interactive_ast frame); + begin + try + current_mode := Evaluation (eval_frame !interactive_ast frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; run_steps (n - 1) | Break frame -> print_endline "Breakpoint"; @@ -352,9 +362,14 @@ let handle_input' input = print_endline ("Result = " ^ Value.string_of_value v); current_mode := Normal | Step (out, state, _, stack) -> - interactive_state := state; - current_mode := Evaluation (eval_frame !interactive_ast frame); - print_program () + begin + try + interactive_state := state; + current_mode := Evaluation (eval_frame !interactive_ast frame); + print_program () + with + | Failure str -> print_endline str; current_mode := Normal + end | Break frame -> print_endline "Breakpoint"; current_mode := Evaluation frame diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 5ffb1647..236c4222 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -167,10 +167,13 @@ let ocaml_lit (L_aux (lit_aux, _)) = | L_one -> string "B1" | L_true -> string "true" | L_false -> string "false" - | L_num n -> if Big_int.equal n Big_int.zero - then string "Big_int.zero" - else parens (string "Big_int.of_int" ^^ space - ^^ string "(" ^^ string (Big_int.to_string n) ^^ string ")") + | L_num n -> + if Big_int.equal n Big_int.zero then + string "Big_int.zero" + else if Big_int.less_equal (Big_int.of_int min_int) n && Big_int.less_equal n (Big_int.of_int max_int) then + parens (string "Big_int.of_int" ^^ space ^^ parens (string (Big_int.to_string n))) + else + parens (string "Big_int.of_string" ^^ space ^^ dquotes (string (Big_int.to_string n))) | L_undef -> failwith "undefined should have been re-written prior to ocaml backend" | L_string str -> string_lit str | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str))) @@ -389,6 +392,10 @@ let ocaml_dec_spec ctx (DEC_aux (reg, _)) = separate space [string "let"; zencode ctx id; colon; parens (ocaml_typ ctx typ); string "ref"; equals; string "ref"; parens (ocaml_exp ctx (initial_value_for id ctx.register_inits))] + | DEC_config (id, typ, exp) -> + separate space [string "let"; zencode ctx id; colon; + parens (ocaml_typ ctx typ); string "ref"; equals; + string "ref"; parens (ocaml_exp ctx exp)] | _ -> failwith "Unsupported register declaration" let first_function = ref true diff --git a/src/rewrites.ml b/src/rewrites.ml index fad1f4d2..8fe30d6b 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2304,6 +2304,7 @@ let rewrite_type_def_typs rw_typ rw_typquant rw_typschm (TD_aux (td, annot)) = let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) = match ds with | DEC_reg (typ, id) -> DEC_aux (DEC_reg (rw_typ typ, id), annot) + | DEC_config (id, typ, exp) -> DEC_aux (DEC_config (id, rw_typ typ, exp), annot) | _ -> assert false (* Remove overload definitions and cast val specs from the diff --git a/src/value.ml b/src/value.ml index 1d2346af..dccb216e 100644 --- a/src/value.ml +++ b/src/value.ml @@ -406,8 +406,8 @@ let value_read_ram = function let value_write_ram = function | [v1; v2; v3; v4; v5] -> - Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5); - V_unit + let b = Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5) in + V_bool(b) | _ -> failwith "value write_ram" let value_load_raw = function diff --git a/test/cheri/run_tests.sh b/test/cheri/run_tests.sh index 848a07e2..337974d7 100755 --- a/test/cheri/run_tests.sh +++ b/test/cheri/run_tests.sh @@ -67,7 +67,7 @@ fi printf "Booting FreeBSD-MIPS...\n" -bunzip2 freebsd-beri-sim-mdroot-smoketest_bootonly-kernel.bz2 +bunzip2 -fk freebsd-beri-sim-mdroot-smoketest_bootonly-kernel.bz2 time $SAILDIR/mips/mips_c --cyclelimit 85000000 --binary 0x100000,freebsd-beri-sim-mdroot-smoketest_bootonly-kernel --binary 0x7f010000,sim.dtb --image simboot_128m.sailbin > freebsd_out.txt if grep -q 'Done booting' freebsd_out.txt; then |