From f81027f53801b8619afe71cb82dbbe4e4651ff13 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 12 Jul 2018 12:30:42 +0100 Subject: Further anonymise manual --- doc/introduction.tex | 8 ++++---- doc/manual.tex | 2 ++ 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/doc/introduction.tex b/doc/introduction.tex index 9e268de5..1bca5e12 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -27,11 +27,11 @@ 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}. +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~\cite{pldi105,pldi2012,micro2015,FGP16,mixed17}. For +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 @@ -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 @@ -118,7 +118,7 @@ specification document~\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 +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 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 -- cgit v1.2.3 From 870f918d3f6e3e9ed8c8367ce19d1991a8bf40b7 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 11 Jul 2018 20:32:22 +0100 Subject: Fix bug for large integers in OCaml compilation --- src/c_backend.ml | 3 ++- src/ocaml_backend.ml | 15 +++++++++++---- src/rewrites.ml | 1 + 3 files changed, 14 insertions(+), 5 deletions(-) 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/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 -- cgit v1.2.3 From 8195ac7e4d851e9901bfaae92997ea51914c09b2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 12 Jul 2018 12:38:32 +0100 Subject: Temporarily remove some paragraphs from the manual for anonymisation --- doc/introduction.tex | 65 ++++++++++++++++++++++++++-------------------------- 1 file changed, 33 insertions(+), 32 deletions(-) diff --git a/doc/introduction.tex b/doc/introduction.tex index 1bca5e12..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\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. +%% 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: @@ -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\anonymiseomit{~\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 -- cgit v1.2.3 From 79ecf8b83b06a6bd1330e1f243826cbe951a9e7d Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 12 Jul 2018 15:54:11 +0100 Subject: update arm and mips models for new type of write_ram builtin. Also fix c and interpreter implementations of same. --- aarch64/no_devices.sail | 4 ++-- lib/rts.c | 4 ++-- lib/rts.h | 2 +- mips/prelude.sail | 4 ++-- src/value.ml | 4 ++-- 5 files changed, 9 insertions(+), 9 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/lib/rts.c b/lib/rts.c index 84ff4916..97aad8a4 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -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, diff --git a/lib/rts.h b/lib/rts.h index cedb555e..98bbd078 100644 --- a/lib/rts.h +++ b/lib/rts.h @@ -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, diff --git a/mips/prelude.sail b/mips/prelude.sail index 037819bc..85060dda 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -125,10 +125,10 @@ 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/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 -- cgit v1.2.3 From d482dcd0152b1f44faf1ad3b1ae06c029a048dab Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 12 Jul 2018 16:14:13 +0100 Subject: Handle failures during interpreting better Changes to the interpreter to better support constant folding during compilation mean it can now throw exceptions to the caller, allow the caller to handle the error, rather than simply printing an error. This broke the ARM interpreter test because exit() is handled by throwing an Exit exception in the interpreter. --- src/isail.ml | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) 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 -- cgit v1.2.3 From e6977ee8e2ba7a53d69f2fb3b715846a62a50454 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 12 Jul 2018 17:04:11 +0100 Subject: make unziping freebsd kernel more robust if run again. --- test/cheri/run_tests.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3 From 3c4a27d7041d71fb229970dacab013cf84669755 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 12 Jul 2018 17:04:40 +0100 Subject: Add missing builtins needed for cheri128 C. Still doesn't build possibly due to code gen issue. --- lib/sail.c | 13 +++++++++++++ lib/sail.h | 3 +++ mips/prelude.sail | 4 ++-- 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/lib/sail.c b/lib/sail.c index 4cb9cdc1..38c8c273 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -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; diff --git a/lib/sail.h b/lib/sail.h index bbdccd09..9ce3ec6b 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -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 85060dda..4c77d522 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -116,9 +116,9 @@ 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} -- cgit v1.2.3