Merge branch 'sail2' into mappings

(involved some manual tinkering with gitignore, type_check, riscv)

18 files changed, 960 insertions, 186 deletions

diff --git a/riscv/.gitignore b/riscv/.gitignore
new file mode 100644
index 00000000..52f3767a
--- /dev/null
+++ b/riscv/.gitignore
@@ -0,0 +1,5 @@
+riscv.lem
+riscv_types.lem
+riscvScript.sml
+riscv_extrasScript.sml
+riscv_typesScript.sml
diff --git a/riscv/Holmakefile b/riscv/Holmakefile
new file mode 100644
index 00000000..8269bc36
--- /dev/null
+++ b/riscv/Holmakefile
@@ -0,0 +1,11 @@
+LEMDIR=../../lem/hol-lib
+
+INCLUDES = $(LEMDIR) ../lib/hol
+
+all: riscvTheory.uo
+.PHONY: all
+
+ifdef POLY
+BASE_HEAP = ../lib/hol/sail-heap
+
+endif
diff --git a/riscv/Makefile b/riscv/Makefile
index d9c3f901..9e07ffa6 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,16 +1,24 @@
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_mem.sail riscv_sys.sail riscv_vmem.sail riscv.sail riscv_step.sail
+SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail
+PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
 
 export SAIL_DIR
 
-all: riscv Riscv.thy
+all: platform Riscv.thy
 
 check: $(SAIL_SRCS) main.sail Makefile
 	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) main.sail
 
-riscv: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL) $(SAIL_FLAGS) -ocaml -o riscv $(SAIL_SRCS) main.sail
+_sbuild/riscv.ml: $(SAIL_SRCS) Makefile main.sail
+	$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS)
+
+_sbuild/platform_main.native: _sbuild/riscv.ml _tags $(PLATFORM_OCAML_SRCS) Makefile
+	cp _tags $(PLATFORM_OCAML_SRCS) _sbuild
+	cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native
+
+platform: _sbuild/platform_main.native
+	rm -f $@ && ln -s $^ $@
 
 riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
 	$(SAIL) $(SAIL_FLAGS) -ocaml -o $@ $^
@@ -35,6 +43,18 @@ Riscv.thy: riscv.lem riscv_extras.lem
 riscv.lem: $(SAIL_SRCS) Makefile
 	$(SAIL) $(SAIL_FLAGS) -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
 
+riscv_sequential.lem: $(SAIL_SRCS) Makefile
+	$(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS)
+
+riscvScript.sml : riscv.lem riscv_extras.lem
+	lem -hol -outdir . -lib ../lib/hol -lib ../src/lem_interp -lib ../src/gen_lib \
+		riscv_extras.lem \
+		riscv_types.lem \
+		riscv.lem
+
+riscvTheory.uo riscvTheory.ui: riscvScript.sml
+	Holmake riscvTheory.uo
+
 # we exclude prelude.sail here, most code there should move to sail lib
 LOC_FILES:=$(SAIL_SRCS) main.sail
 include ../etc/loc.mk
@@ -45,3 +65,7 @@ clean:
 	-rm -f Riscv.thy Riscv_types.thy \
 		Riscv_extras.thy
 	-rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem
+	-rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml
+	-rm -f platform_main.native platform
+	-Holmake cleanAll
+	ocamlbuild -clean
diff --git a/riscv/_tags b/riscv/_tags
new file mode 100644
index 00000000..eab7e89a
--- /dev/null
+++ b/riscv/_tags
@@ -0,0 +1,3 @@
+<**/*.ml>: bin_annot, annot
+<*.m{l,li}>: package(lem), package(linksem), package(zarith)
+<platform_main.native>: package(lem), package(linksem), package(zarith)
diff --git a/riscv/main.sail b/riscv/main.sail
index 06665cec..b2a53b11 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -1,34 +1,8 @@
-val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-
 val elf_tohost = {
   ocaml: "Elf_loader.elf_tohost",
   c: "elf_tohost"
 } :  unit -> int
 
-val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-function loop () = {
-  let tohost = __GetSlice_int(64, elf_tohost(), 0);
-  i : int = 0;
-  while true do {
-    tick_clock();
-    print_int("\nstep: ", i);
-    let retired : bool = step();
-    PC = nextPC;
-    if retired then i = i + 1;
-
-    /* check htif exit */
-    let tohost_val = __ReadRAM(64, 4, 0x0000_0000_0000_0000, tohost);
-    if unsigned(tohost_val) != 0 then {
-      let exit_val = unsigned(tohost_val >> 0b1) in
-      if exit_val == 0 then
-        print("SUCCESS")
-      else
-        print_int("FAILURE: ", exit_val);
-      exit(());
-    }
-  }
-}
-
 val elf_entry = {
   ocaml: "Elf_loader.elf_entry",
   c: "elf_entry"
@@ -41,7 +15,7 @@ function main () = {
   PC = __GetSlice_int(64, elf_entry(), 0);
   try {
     init_sys ();
-    loop ()
+    loop (elf_tohost())
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
     Error_internal_error() => print("Error: internal error")
diff --git a/riscv/platform.ml b/riscv/platform.ml
new file mode 100644
index 00000000..8d93ad4a
--- /dev/null
+++ b/riscv/platform.ml
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(*     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 Sail_lib;;
+module P = Platform_impl;;
+module Elf = Elf_loader;;
+
+(* Mapping to Sail externs *)
+
+let bits_of_int i =
+  get_slice_int (Big_int.of_int 64, Big_int.of_int i, Big_int.zero)
+
+let bits_of_int64 i =
+  get_slice_int (Big_int.of_int 64, Big_int.of_int64 i, Big_int.zero)
+
+let rom_size_ref = ref 0
+let make_rom start_pc =
+  let reset_vec = List.concat (List.map P.uint32_to_bytes (P.reset_vec_int start_pc)) in
+  let dtb = P.make_dtb P.dts in
+  let rom = reset_vec @ dtb in
+  ( rom_size_ref := List.length rom;
+    rom )
+
+let rom_base () = bits_of_int64 P.rom_base
+let rom_size () = bits_of_int   !rom_size_ref
+
+let dram_base () = bits_of_int64 P.dram_base
+let dram_size () = bits_of_int64 P.dram_size
+
+let htif_tohost () =
+  bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
+
+let clint_base () = bits_of_int64 P.clint_base
+let clint_size () = bits_of_int64 P.clint_size
+
+(* terminal I/O *)
+let term_write char_bits =
+  let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
+  P.term_write (char_of_int (Big_int.to_int big_char))
+
+let term_read () =
+  let c = P.term_read () in
+  bits_of_int (int_of_char c)
+
+(* returns starting value for PC, i.e. start of reset vector *)
+let init elf_file =
+  Elf.load_elf elf_file;
+
+  Printf.printf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ()));
+  Printf.printf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size;
+
+  let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in
+  let rom = make_rom start_pc in
+  let rom_base = Big_int.of_int64 P.rom_base in
+  let rec write_rom ofs = function
+    | [] -> ()
+    | h :: tl -> let addr = Big_int.add rom_base (Big_int.of_int ofs) in
+                 (wram addr h);
+                 write_rom (ofs + 1) tl
+  in ( write_rom 0 rom;
+       get_slice_int (Big_int.of_int 64, rom_base, Big_int.zero)
+     )
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
new file mode 100644
index 00000000..9b063404
--- /dev/null
+++ b/riscv/platform_impl.ml
@@ -0,0 +1,166 @@
+(* FIXME: copyright header *)
+
+(* int->byte converters in little-endian order *)
+
+let uint32_to_bytes u = let open Int32 in
+ List.map to_int
+  [ logand u 0xffl;
+    logand (shift_right u 8) 0xffl;
+    logand (shift_right u 16) 0xffl;
+    logand (shift_right u 24) 0xffl;
+  ]
+
+let uint64_to_bytes u = let open Int64 in
+ List.map to_int
+  [ logand u 0xffL;
+    logand (shift_right u 8) 0xffL;
+    logand (shift_right u 16) 0xffL;
+    logand (shift_right u 24) 0xffL;
+    logand (shift_right u 32) 0xffL;
+    logand (shift_right u 40) 0xffL;
+    logand (shift_right u 48) 0xffL;
+    logand (shift_right u 56) 0xffL;
+  ]
+
+(* reset vector for the rom *)
+
+let reset_vec_size = 8l;;
+
+let reset_vec_int start_pc = [
+  0x297l;                                                 (* auipc  t0, 0x0      *)
+  (let open Int32 in
+   add 0x28593l (shift_left (mul reset_vec_size 4l) 20)); (* addi   a1, t0, ofs(dtb) *)
+  0xf1402573l;                                            (* csrr   a0, mhartid  *)
+  0x0182b283l;                                            (* ld     t0, 24(t0)   *)
+  0x28067l;                                               (* jr     t0           *)
+  0x0l;
+  (let open Int64 in to_int32 (logand start_pc 0xffffffffL));
+  (let open Int64 in to_int32 (shift_right_logical start_pc 32));
+]
+
+(* address map *)
+
+let dram_base  = 0x80000000L;;  (* Spike::DRAM_BASE *)
+let dram_size  = Int64.(shift_left 2048L 20)
+let clint_base = 0x02000000L;;  (* Spike::CLINT_BASE *)
+let clint_size = 0x000c0000L;;  (* Spike::CLINT_SIZE *)
+let rom_base   = 0x00001000L;;  (* Spike::DEFAULT_RSTVEC *)
+
+type mem_region = {
+    addr : Int64.t;
+    size : Int64.t
+}
+
+(* dts from spike *)
+let spike_dts isa_spec cpu_hz insns_per_rtc_tick mems =
+    "/dts-v1/;\n"
+  ^ "\n"
+  ^ "/ {\n"
+  ^ "  #address-cells = <2>;\n"
+  ^ "  #size-cells = <2>;\n"
+  ^ "  compatible = \"ucbbar,spike-bare-dev\";\n"
+  ^ "  model = \"ucbbar,spike-bare\";\n"
+  ^ "  cpus {\n"
+  ^ "    #address-cells = <1>;\n"
+  ^ "    #size-cells = <0>;\n"
+  ^ "    timebase-frequency = <" ^ string_of_int (cpu_hz/insns_per_rtc_tick) ^ ">;\n"
+  ^ "    CPU0: cpu@0 {\n"
+  ^ "      device_type = \"cpu\";\n"
+  ^ "      reg = <0>;\n"
+  ^ "      status = \"okay\";\n"
+  ^ "      compatible = \"riscv\";\n"
+  ^ "      riscv,isa = \"" ^ isa_spec ^ "\";\n"
+  ^ "      mmu-type = \"riscv,sv39\";\n"
+  ^ "      clock-frequency = <" ^ string_of_int cpu_hz ^ ">;\n"
+  ^ "      CPU0_intc: interrupt-controller {\n"
+  ^ "        #interrupt-cells = <1>;\n"
+  ^ "        interrupt-controller;\n"
+  ^ "        compatible = \"riscv,cpu-intc\";\n"
+  ^ "      };\n"
+  ^ "    };\n"
+  ^ "  };\n"
+  ^ (List.fold_left (^) ""
+       (List.map (fun m ->
+         "  memory@" ^ Printf.sprintf "%Lx" m.addr ^ " {\n"
+         ^ "    device_type = \"memory\";\n"
+         ^ "    reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.addr 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.addr 0xffffffffL)
+         ^           " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.size 0xffffffffL) ^ ">;\n"
+         ^ "  };\n") mems))
+  ^ "  soc {\n"
+  ^ "    #address-cells = <2>;\n"
+  ^ "    #size-cells = <2>;\n"
+  ^ "    compatible = \"ucbbar,spike-bare-soc\", \"simple-bus\";\n"
+  ^ "    ranges;\n"
+  ^ "    clint@" ^ Printf.sprintf "%Lx" clint_base ^ " {\n"
+  ^ "      compatible = \"riscv,clint0\";\n"
+  ^ "      interrupts-extended = <&CPU0_intc 3 &CPU0_intc 7 >;\n"
+  ^ "      reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_base 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_base 0xffffffffL)
+  ^             " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_size 0xffffffffL) ^ ">;\n"
+  ^ "    };\n"
+  ^ "  };\n"
+  ^ "  htif {\n"
+  ^ "    compatible = \"ucb,htif0\";\n"
+  ^ "  };\n"
+  ^ "};\n"
+
+let cpu_hz = 1000000000;;
+let insns_per_tick = 100;;
+
+let mems = [ { addr = dram_base;
+	       size = dram_size } ];;
+let dts = spike_dts "rv64imac" cpu_hz insns_per_tick mems;;
+
+let bytes_to_string bytes =
+  String.init (List.length bytes) (fun i -> Char.chr (List.nth bytes i))
+
+let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *)
+  try
+    let (cfrom, cto, cerr) =
+      Unix.open_process_full "/usr/bin/dtc -I dts" [||]
+    in (
+      output_string cto dts;
+      (* print_endline " sent dts to dtc ..."; *)
+      close_out cto;
+      (* simple and stupid for now *)
+      let rec accum_bytes cin acc =
+        match (
+          try  Some (input_byte cin)
+          with End_of_file -> None
+        ) with
+          | Some b -> accum_bytes cin (b :: acc)
+          | None   -> List.rev acc
+      in
+      (* let _ = print_endline " accumulating dtb ..." in *)
+      let dtb  = accum_bytes cfrom [] in
+      (* let _ = print_endline " accumulating emsg ..." in *)
+      let emsg = bytes_to_string (accum_bytes cerr []) in
+      match Unix.close_process_full (cfrom, cto, cerr) with
+        | Unix.WEXITED 0 -> dtb
+        | _ -> (Printf.printf "%s\n" ("Error executing dtc: " ^ emsg);
+                exit 1)
+    )
+  with Unix.Unix_error (e, fn, _) ->
+    (Printf.printf "%s\n" ("Error executing dtc: " ^ fn ^ ": " ^ Unix.error_message e);
+     exit 1)
+
+(* Terminal I/O *)
+
+let term_write char =
+  ignore (Unix.write_substring Unix.stdout (String.make 1 char) 0 1)
+
+let rec term_read () =
+  let buf = Bytes.make 1 '\000' in
+  let nbytes = Unix.read Unix.stdin buf 0 1 in
+  (* todo: handle nbytes == 0 *)
+  buf.[0]
+
+(*
+let save_string_to_file s fname =
+  let out = open_out fname in
+  output_string out s;
+  close_out out;;
+
+let _ =
+  save_string_to_file dts "/tmp/platform.dts";
+  save_string_to_file (bytes_to_string (get_dtb dts)) "/tmp/platform.dtb";
+ *)
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
new file mode 100644
index 00000000..cb379cdd
--- /dev/null
+++ b/riscv/platform_main.ml
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*     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 Elf_loader
+open Sail_lib
+open Riscv
+
+(* OCaml driver for generated RISC-V model. *)
+
+let opt_file_arguments = ref ([] : string list)
+
+let options = Arg.align []
+
+let usage_msg = "RISC-V platform options:"
+
+let elf_arg =
+  Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s])
+            usage_msg;
+  ( match !opt_file_arguments with
+      | f :: _ -> print_endline ("Loading ELF file " ^ f); f
+      | _ -> (prerr_endline "Please provide an ELF file."; exit 0)
+  )
+
+let () =
+  Random.self_init ();
+
+  let pc = Platform.init elf_arg in
+
+  sail_call
+    (fun r ->
+      try ( zinit_platform (); (* devices *)
+            zinit_sys ();      (* processor *)
+            zPC := pc;
+            zloop (Elf_loader.elf_tohost ())
+          )
+      with
+        | ZError_not_implemented (zs) ->
+              print_string ("Error: Not implemented: ", zs)
+        | ZError_internal_error (_) ->
+              prerr_endline "Error: internal error"
+    )
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index cf4b2f30..d10dddc9 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -402,9 +402,9 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
 
 val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
 
-val print_int = "print_int" : (string, int) -> unit
-val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
-val print_string = "print_string" : (string, string) -> unit
+val print_int = "prerr_int" : (string, int) -> unit
+val print_bits = "prerr_bits" : forall 'n. (string, bits('n)) -> unit
+val print_string = "prerr_string" : (string, string) -> unit
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
@@ -472,3 +472,7 @@ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
 function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
     let v64 : bits(64) = EXTS(v) in
     (v64 >> shift)[31..0]
+
+/* Copied from arith.sail. */
+val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n * 'm)
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index a4fdc01b..9f4385e7 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -5,7 +5,8 @@ val decode : bits(32) -> option(ast) effect pure
 val decodeCompressed : bits(16) -> option(ast) effect pure
 scattered function decodeCompressed
 
-val execute : ast -> unit effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
+/* returns whether an instruction was retired, used for computing minstret */
+val execute : ast -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
 scattered function execute
 
 val cast print_insn : ast -> string
@@ -32,8 +33,10 @@ function clause execute UTYPE(imm, rd, op) =
     let ret : xlenbits   = match op {
       RISCV_LUI   => off,
       RISCV_AUIPC => PC + off
-    } in
-    X(rd) = ret
+    } in {
+      X(rd) = ret;
+      true
+    }
 
 function clause print_insn UTYPE(imm, rd, op) =
   match (op) {
@@ -71,6 +74,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     X(rd) = nextPC;  /* compatible with JAL and C.JAL */
     let offset : xlenbits = EXTS(imm);
     nextPC = pc + offset;
+    true
 }
 
 function clause print_insn (RISCV_JAL(imm, rd)) =
@@ -90,6 +94,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
     X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
     let newPC : xlenbits = X(rs1) + EXTS(imm);
     nextPC = newPC[63..1] @ 0b0;
+    true
 }
 
 function clause print_insn (RISCV_JALR(imm, rs1, rd)) =
@@ -122,9 +127,10 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) =
     RISCV_BGE  => rs1_val >=_s rs2_val,
     RISCV_BLTU => rs1_val <_u rs2_val,
     RISCV_BGEU => rs1_val >=_u rs2_val
-  } in
-  if taken then
-    nextPC = PC + EXTS(imm)
+  } in {
+    if taken then nextPC = PC + EXTS(imm);
+    true
+  }
 
 function clause print_insn (BTYPE(imm, rs2, rs1, op)) =
   let insn : string =
@@ -174,8 +180,10 @@ function clause execute (ITYPE (imm, rs1, rd, op)) =
     RISCV_XORI  => rs1_val ^ immext,
     RISCV_ORI   => rs1_val | immext,
     RISCV_ANDI  => rs1_val & immext
-  } in
-  X(rd) = result
+  } in {
+    X(rd) = result;
+    true
+  }
 
 function clause print_insn (ITYPE(imm, rs1, rd, op)) =
   let insn : string =
@@ -219,9 +227,10 @@ function clause execute (SHIFTIOP(shamt, rs1, rd, op)) =
       RISCV_SLLI => rs1_val << shamt,
       RISCV_SRLI => rs1_val >> shamt,
       RISCV_SRAI => shift_right_arith64(rs1_val, shamt)
-    } in
-    X(rd) = result
-
+    } in {
+      X(rd) = result;
+      true
+    }
 
 function clause print_insn (SHIFTIOP(shamt, rs1, rd, op)) =
   let insn : string =
@@ -268,8 +277,10 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) =
     RISCV_SRA  => shift_right_arith64(rs1_val, rs2_val[5..0]),
     RISCV_OR   => rs1_val | rs2_val,
     RISCV_AND  => rs1_val & rs2_val
-  } in
-  X(rd) = result
+  } in {
+    X(rd) = result;
+    true
+  }
 
 function clause print_insn (RTYPE(rs2, rs1, rd, op)) =
   let insn : string =
@@ -315,17 +326,17 @@ function extend_value(is_unsigned, value) = match (value) {
   MemException(e) => MemException(e)
 }
 
-val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit effect {escape, rreg, wreg}
+val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
 function process_load(rd, addr, value, is_unsigned) =
   match (extend_value(is_unsigned, value)) {
-    MemValue(result) => X(rd) = result,
-    MemException(e)  => handle_mem_exception(addr, e)
+    MemValue(result) => { X(rd) = result; true },
+    MemException(e)  => { handle_mem_exception(addr, e); false }
   }
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
     let vaddr : xlenbits = X(rs1) + EXTS(imm) in
     match translateAddr(vaddr, Read, Data) {
-      TR_Failure(e) => handle_mem_exception(vaddr, e),
+      TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) =>
         match width {
           BYTE   => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
@@ -383,7 +394,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) <-> imm
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
     let vaddr : xlenbits = X(rs1) + EXTS(imm) in
     match translateAddr(vaddr, Write, Data) {
-      TR_Failure(e) => handle_mem_exception(vaddr, e),
+      TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) =>
         let eares : MemoryOpResult(unit) = match width {
           BYTE   => mem_write_ea(addr, 1, aq, rl, false),
@@ -392,7 +403,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
           DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
         } in
         match (eares) {
-          MemException(e) => handle_mem_exception(addr, e),
+          MemException(e) => { handle_mem_exception(addr, e); false },
           MemValue(_) => {
             let rs2_val = X(rs2) in
             let res : MemoryOpResult(unit) = match width {
@@ -402,8 +413,8 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
               DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
             } in
             match (res) {
-              MemValue(_)     => (),
-              MemException(e) => handle_mem_exception(addr, e)
+              MemValue(_)     => true,
+              MemException(e) => { handle_mem_exception(addr, e); false }
             }
           }
         }
@@ -428,9 +439,11 @@ union clause ast = ADDIW : (bits(12), regbits, regbits)
 
 mapping clause encdec = ADDIW(imm, rs1, rd) <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011
 
-function clause execute (ADDIW(imm, rs1, rd)) =
-  let result : xlenbits = EXTS(imm) + X(rs1) in
-  X(rd) = EXTS(result[31..0])
+function clause execute (ADDIW(imm, rs1, rd)) = {
+  let result : xlenbits = EXTS(imm) + X(rs1);
+  X(rd) = EXTS(result[31..0]);
+  true
+}
 
 function clause print_insn (ADDIW(imm, rs1, rd)) =
   "addiw " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
@@ -450,8 +463,10 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) =
       RISCV_SLLI => rs1_val << shamt,
       RISCV_SRLI => rs1_val >> shamt,
       RISCV_SRAI => shift_right_arith32(rs1_val, shamt)
-    } in
-    X(rd) = EXTS(result)
+    } in {
+      X(rd) = EXTS(result);
+      true
+    }
 
 function clause print_insn (SHIFTW(shamt, rs1, rd, op)) =
   let insn : string =
@@ -488,8 +503,10 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
     RISCV_SLLW => rs1_val << (rs2_val[4..0]),
     RISCV_SRLW => rs1_val >> (rs2_val[4..0]),
     RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0])
-  } in
-  X(rd) = EXTS(result)
+  } in {
+    X(rd) = EXTS(result);
+    true
+  }
 
 function clause print_insn (RTYPEW(rs2, rs1, rd, op)) =
   let insn : string =
@@ -532,8 +549,10 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) =
   let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val) in
   let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val) in
   let result128 = to_bits(128, rs1_int * rs2_int) in
-  let result = if high then result128[127..64] else result128[63..0] in
-  X(rd) = result
+  let result = if high then result128[127..64] else result128[63..0] in {
+    X(rd) = result;
+    true
+  }
 
 function clause print_insn (MUL(rs2, rs1, rd, high, signed1, signed2)) =
   let insn : string =
@@ -565,7 +584,10 @@ function clause execute (DIV(rs2, rs1, rd, s)) =
   let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
   let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
   let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in
-  let q': int = if s & q > xlen_max_signed then xlen_min_signed else q in /* check for signed overflow */  X(rd) = to_bits(xlen, q')
+  let q': int = if s & q > xlen_max_signed then xlen_min_signed else q in /* check for signed overflow */ {
+    X(rd) = to_bits(xlen, q');
+    true
+  }
 
 function clause print_insn (DIV(rs2, rs1, rd, s)) =
   let insn : string = if s then "div   " else "divu  " in
@@ -588,9 +610,11 @@ function clause execute (REM(rs2, rs1, rd, s)) =
   let rs2_val = X(rs2) in
   let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
   let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
-  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in
+  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in {
   /* signed overflow case returns zero naturally as required due to -1 divisor */
-  X(rd) = to_bits(xlen, r)
+    X(rd) = to_bits(xlen, r);
+    true
+  }
 
 function clause print_insn (REM(rs2, rs1, rd, s)) =
   let insn : string = if s then "rem   " else "remu  " in
@@ -609,8 +633,10 @@ function clause execute (MULW(rs2, rs1, rd)) =
   let rs1_int : int = signed(rs1_val) in
   let rs2_int : int = signed(rs2_val) in
   let result32 = to_bits(64, rs1_int * rs2_int)[31..0] in /* XXX surprising behaviour of to_bits requires exapnsion to 64 bits followed by truncation... */
-  let result : xlenbits = EXTS(result32) in
-  X(rd) = result
+  let result : xlenbits = EXTS(result32) in {
+    X(rd) = result;
+    true
+  }
 
 function clause print_insn (MULW(rs2, rs1, rd)) =
   "mulw  " ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2
@@ -628,8 +654,10 @@ function clause execute (DIVW(rs2, rs1, rd, s)) =
   let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
   let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
   let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in
-  let q': int = if s & q > (2 ^ 31 - 1) then  (0 - 2^31) else q in /* check for signed overflow */
-  X(rd) = EXTS(to_bits(32, q'))
+  let q': int = if s & q > (2 ^ 31 - 1) then  (0 - 2^31) else q in /* check for signed overflow */ {
+    X(rd) = EXTS(to_bits(32, q'));
+    true
+  }
 
 function clause print_insn (DIVW(rs2, rs1, rd, s)) =
   let insn : string = if s then "divw  " else "divuw " in
@@ -647,9 +675,11 @@ function clause execute (REMW(rs2, rs1, rd, s)) =
   let rs2_val = X(rs2)[31..0] in
   let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
   let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
-  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in
-  /* signed overflow case returns zero naturally as required due to -1 divisor */
-  X(rd) = EXTS(to_bits(32, r))
+  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in {
+    /* signed overflow case returns zero naturally as required due to -1 divisor */
+    X(rd) = EXTS(to_bits(32, r));
+    true
+  }
 
 function clause print_insn (REMW(rs2, rs1, rd, s)) =
   let insn : string = if s then "remw  " else "remuw " in
@@ -671,7 +701,8 @@ function clause execute (FENCE(pred, succ)) = {
     (0b0001, 0b0001) => MEM_fence_w_w(),
     _ => { print("FIXME: unsupported fence");
            () }
-  }
+  };
+  true
 }
 
 /* FIXME */
@@ -709,7 +740,7 @@ union clause ast = FENCEI : unit
 
 mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111
 
-function clause execute FENCEI() = MEM_fence_i()
+function clause execute FENCEI() = { MEM_fence_i(); true }
 
 function clause print_insn (FENCEI()) =
   "fence.i"
@@ -727,9 +758,11 @@ function clause execute ECALL() =
                       User => E_U_EnvCall,
                       Supervisor => E_S_EnvCall,
                       Machine => E_M_EnvCall
-		    },
-	     excinfo = (None() : option(xlenbits)) } in
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
+                    },
+             excinfo = (None() : option(xlenbits)) } in {
+    nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC);
+    false
+  }
 
 function clause print_insn (ECALL()) =
   "ecall"
@@ -745,7 +778,8 @@ function clause execute MRET() = {
   if cur_privilege == Machine then
     nextPC = handle_exception(cur_privilege, CTL_MRET(), PC)
   else
-    handle_illegal()
+    handle_illegal();
+  false
 }
 
 function clause print_insn (MRET()) =
@@ -758,14 +792,16 @@ union clause ast = SRET : unit
 
 mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
-function clause execute SRET() =
+function clause execute SRET() = {
   match cur_privilege {
     User       => handle_illegal(),
     Supervisor => if mstatus.TSR() == true
                   then handle_illegal()
                   else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC),
     Machine    => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
-  }
+  };
+  false
+}
 
 function clause print_insn (SRET()) =
   "sret"
@@ -777,8 +813,10 @@ union clause ast = EBREAK : unit
 
 mapping clause encdec = EBREAK() <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
-function clause execute EBREAK() =
-  handle_mem_exception(PC, E_Breakpoint)
+function clause execute EBREAK() = {
+  handle_mem_exception(PC, E_Breakpoint);
+  false
+}
 
 function clause print_insn (EBREAK()) =
   "ebreak"
@@ -797,7 +835,9 @@ function clause execute WFI() = {
                   then handle_illegal()
                   else (),
     User       => handle_illegal()
-  }
+  };
+  /* NOTE: since WFI is always interrupted, it should never retire.  TODO: Confirm this. */
+  false
 }
 
 function clause print_insn (WFI()) =
@@ -814,13 +854,14 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
   /* FIXME: spec leaves unspecified what happens if this is executed in M-mode.
      We assume it is the same as S-mode, which is definitely wrong.
    */
-  if cur_privilege == User then handle_illegal()
+  if cur_privilege == User then { handle_illegal(); false }
   else match (architecture(mstatus.SXL()), mstatus.TVM()) {
-    (Some(RV64), true)  => handle_illegal(),
+    (Some(RV64), true)  => { handle_illegal(); false },
     (Some(RV64), false) => {
       let addr : option(vaddr39) = if rs1 == 0 then None() else Some(X(rs1)[38 .. 0]);
       let asid : option(asid64)  = if rs2 == 0 then None() else Some(X(rs2)[15 .. 0]);
-      flushTLB(asid, addr)
+      flushTLB(asid, addr);
+      true
     },
     (_, _) => internal_error("unimplemented sfence architecture")
   }
@@ -841,7 +882,7 @@ val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
   let vaddr : xlenbits = X(rs1) in
   match translateAddr(vaddr, Read, Data) {
-    TR_Failure(e) => handle_mem_exception(vaddr, e),
+    TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
     TR_Address(addr) =>
       match width {
         WORD   => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false),
@@ -873,10 +914,10 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1;
   X(rd) = EXTZ(status);
 
-  if status == 0b1 then () else {
+  if status == 0b1 then true else {
     vaddr : xlenbits = X(rs1);
     match translateAddr(vaddr, Write, Data) {
-      TR_Failure(e) => handle_mem_exception(vaddr, e),
+      TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) => {
         let eares : MemoryOpResult(unit) = match width {
           WORD   => mem_write_ea(addr, 4, aq, rl, true),
@@ -884,7 +925,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
           _      => internal_error("STORECON expected word or double")
         };
         match (eares) {
-          MemException(e)  => handle_mem_exception(addr, e),
+          MemException(e)  => { handle_mem_exception(addr, e); false },
           MemValue(_) => {
             rs2_val = X(rs2);
             let res : MemoryOpResult(unit) = match width {
@@ -893,8 +934,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
               _      => internal_error("STORECON expected word or double")
             } in
             match (res) {
-              MemValue(_)     => (),
-              MemException(e) => handle_mem_exception(addr, e)
+              MemValue(_)     => true,
+              MemException(e) => { handle_mem_exception(addr, e); false }
             }
           }
         }
@@ -937,7 +978,7 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) <-> encdec_amoop(op)
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   vaddr : xlenbits = X(rs1);
   match translateAddr(vaddr, ReadWrite, Data) {
-    TR_Failure(e) => handle_mem_exception(vaddr, e),
+    TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
     TR_Address(addr) => {
       let eares : MemoryOpResult(unit) = match width {
         WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
@@ -945,7 +986,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
         _      => internal_error ("AMO expected WORD or DOUBLE")
       };
       match (eares) {
-        MemException(e) => handle_mem_exception(addr, e),
+        MemException(e) => { handle_mem_exception(addr, e); false },
         MemValue(_) => {
           let rval : MemoryOpResult(xlenbits) = match width {
             WORD   => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
@@ -953,7 +994,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
           _        => internal_error ("AMO expected WORD or DOUBLE")
           };
           match (rval) {
-            MemException(e) => handle_mem_exception(addr, e),
+            MemException(e) => { handle_mem_exception(addr, e); false },
             MemValue(loaded) => {
               rs2_val : xlenbits = X(rs2);
               result : xlenbits =
@@ -977,8 +1018,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                 _      => internal_error("AMO expected WORD or DOUBLE")
               };
               match (wval) {
-                MemValue(_) => X(rd) = loaded,
-                MemException(e) => handle_mem_exception(addr, e)
+                MemValue(_) => { X(rd) = loaded; true },
+                MemException(e) => { handle_mem_exception(addr, e); false }
               }
             }
           }
@@ -1051,6 +1092,7 @@ function readCSR csr : csreg -> xlenbits =
     0x303 => mideleg.bits(),
     0x304 => mie.bits(),
     0x305 => mtvec.bits(),
+    0x306 => EXTZ(mcounteren.bits()),
     0x340 => mscratch,
     0x341 => mepc,
     0x342 => mcause.bits(),
@@ -1063,6 +1105,7 @@ function readCSR csr : csreg -> xlenbits =
     0x103 => sideleg.bits(),
     0x104 => lower_mie(mie, mideleg).bits(),
     0x105 => stvec.bits(),
+    0x106 => EXTZ(scounteren.bits()),
     0x140 => sscratch,
     0x141 => sepc,
     0x142 => scause.bits(),
@@ -1091,6 +1134,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit =
     0x303 => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) },
     0x304 => { mie = legalize_mie(mie, value); Some(mie.bits()) },
     0x305 => { mtvec = legalize_tvec(mtvec, value); Some(mtvec.bits()) },
+    0x306 => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) },
     0x340 => { mscratch = value; Some(mscratch) },
     0x341 => { mepc = legalize_xepc(value); Some(mepc) },
     0x342 => { mcause->bits() = value; Some(mcause.bits()) },
@@ -1103,6 +1147,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit =
     0x103 => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */
     0x104 => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) },
     0x105 => { stvec = legalize_tvec(stvec, value); Some(stvec.bits()) },
+    0x106 => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) },
     0x140 => { sscratch = value; Some(sscratch) },
     0x141 => { sepc = legalize_xepc(value); Some(sepc) },
     0x142 => { scause->bits() = value; Some(scause.bits()) },
@@ -1113,6 +1158,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit =
     /* trigger/debug */
     0x7a0 => { tselect = value; Some(tselect) },
 
+    /* counters */
+    0xC00 => { mcycle = value; Some(mcycle) },
+    /* FIXME: it is not clear whether writable mtime is platform-dependent. */
+    0xC02 => { minstret = value; minstret_written = true; Some(minstret) },
+
     _     => None()
   } in
   match res {
@@ -1127,7 +1177,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
     _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
   } in
   if ~ (check_CSR(csr, cur_privilege, isWrite))
-  then handle_illegal()
+  then { handle_illegal(); false }
   else {
     let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
     if isWrite then {
@@ -1138,7 +1188,8 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
       } in
       writeCSR(csr, new_val)
     };
-    X(rd) = csr_val
+    X(rd) = csr_val;
+    true
   }
 
 function clause print_insn (CSR(csr, rs1, rd, is_imm, op)) =
@@ -1176,7 +1227,7 @@ function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bit
   else None()
 }
 
-function clause execute NOP() = ()
+function clause execute NOP() = true
 
 function clause print_insn (NOP()) =
   "nop"
@@ -1304,10 +1355,11 @@ function clause execute (C_JAL(imm)) = {
 }
 
 function clause execute (C_ADDIW(imm, rsd)) = {
-  let imm : bits(32) = EXTS(imm) in
-  let rs_val = X(rsd) in
-  let res : bits(32) = rs_val[31..0] + imm in
-  X(rsd) = EXTS(res)
+  let imm : bits(32) = EXTS(imm);
+  let rs_val = X(rsd);
+  let res : bits(32) = rs_val[31..0] + imm;
+  X(rsd) = EXTS(res);
+  true
 }
 
 function clause print_insn (C_JAL(imm)) =
@@ -1686,7 +1738,7 @@ union clause ast = ILLEGAL : word
 
 mapping clause encdec = ILLEGAL(s) <-> s
 
-function clause execute (ILLEGAL(s)) = handle_illegal ()
+function clause execute (ILLEGAL(s)) = { handle_illegal(); false }
 
 function clause print_insn (ILLEGAL(s)) = "illegal " ^ hex_bits_32(s)
 
@@ -1700,7 +1752,7 @@ union clause ast = C_ILLEGAL : unit
 
 function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(C_ILLEGAL())
 
-function clause execute C_ILLEGAL() = handle_illegal ()
+function clause execute C_ILLEGAL() = { handle_illegal(); false }
 
 function clause print_insn (C_ILLEGAL()) =
   "c.illegal"
diff --git a/riscv/riscv_all.sail b/riscv/riscv_all.sail
deleted file mode 100644
index f331b348..00000000
--- a/riscv/riscv_all.sail
+++ /dev/null
@@ -1,5 +0,0 @@
-$include "prelude.sail"
-$include "riscv_types.sail"
-$include "riscv_sys.sail"
-$include "riscv.sail"
-$include "main.sail"
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 491dd56d..fc72ca2b 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -44,12 +44,41 @@ let read_ram addrsize size hexRAM address =
 
 let speculate_conditional_success () = excl_result ()
 
-val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a
-let get_slice_int len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  of_bits_failwith (subrange_list false bits hi lo)
+val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_ram_base () = wordFromInteger 0
+declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
+
+val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_ram_size () = wordFromInteger 0
+declare ocaml target_rep function plat_ram_size = `Platform.dram_size`
+
+val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_rom_base () = wordFromInteger 0
+declare ocaml target_rep function plat_rom_base = `Platform.rom_base`
+
+val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_rom_size () = wordFromInteger 0
+declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
+
+val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_clint_base () = wordFromInteger 0
+declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
+
+val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_clint_size () = wordFromInteger 0
+declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
+
+val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_htif_tohost () = wordFromInteger 0
+declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
+
+val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit
+let plat_term_write _ = ()
+declare ocaml target_rep function plat_term_write = `Platform.term_write`
+
+val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_term_read () = wordFromInteger 0
+declare ocaml target_rep function plat_term_read = `Platform.term_read`
 
 val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_right v m = shiftr v (uint m)
@@ -59,5 +88,5 @@ let shift_bits_left v m = shiftl v (uint m)
 val print_string : string -> string -> unit
 let print_string msg s = prerr_endline (msg ^ s)
 
-val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
+val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
+let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 375f48b3..788ef594 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -1,20 +1,27 @@
 /* memory */
 
-union MemoryOpResult ('a : Type) = {
-  MemValue : 'a,
-  MemException: ExceptionType
-}
-
 function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool =
   unsigned(addr) % width == 0
 
-function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+// only used for actual memory regions, to avoid MMIO effects
+function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
   match (t, __RISCV_read(addr, width)) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
-    (_, Some(v))          => MemValue(v)
+    (_, Some(v))          => { print("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+                               MemValue(v) }
   }
 
+function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+  /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
+  if   t == Data & within_mmio_readable(addr, width)
+  then mmio_read(addr, width)
+  else if within_phys_mem(addr, width)
+  then phys_mem_read(t, addr, width)
+  else MemException(E_Load_Access_Fault)
+
+/* FIXME: We assume atomic accesses are only done to memory-backed regions.  MMIO is not modeled. */
+
 val MEMr                         : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 val MEMr_strong_acquire          : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
@@ -22,20 +29,21 @@ val MEMr_reserved                : forall 'n. (xlenbits, atom('n)) -> MemoryOpRe
 val MEMr_reserved_acquire        : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 
-function MEMr                         (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_acquire                 (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_strong_acquire          (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_reserved                (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_reserved_acquire        (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr                         (addr, width) = phys_mem_read(Data, addr, width)
+function MEMr_acquire                 (addr, width) = phys_mem_read(Data, addr, width)
+function MEMr_strong_acquire          (addr, width) = phys_mem_read(Data, addr, width)
+function MEMr_reserved                (addr, width) = phys_mem_read(Data, addr, width)
+function MEMr_reserved_acquire        (addr, width) = phys_mem_read(Data, addr, width)
+function MEMr_reserved_strong_acquire (addr, width) = phys_mem_read(Data, addr, width)
 
-val mem_read : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, escape}
+/* NOTE: The rreg effect is due to MMIO. */
+val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
 
 function mem_read (addr, width, aq, rl, res) = {
   if (aq | res) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_Load_Addr_Align)
   else match (aq, rl, res) {
-    (false, false, false) => MEMr(addr, width),
+    (false, false, false) => checked_mem_read(Data, addr, width),
     (true,  false, false) => MEMr_acquire(addr, width),
     (false, false, true)  => MEMr_reserved(addr, width),
     (true,  false, true)  => MEMr_reserved_acquire(addr, width),
@@ -76,10 +84,22 @@ function mem_write_ea (addr, width, aq, rl, con) = {
   }
 }
 
-function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) =
-  if (__RISCV_write(addr, width, data))
+// only used for actual memory regions, to avoid MMIO effects
+function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) = {
+  print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  if   __RISCV_write(addr, width, data)
   then MemValue(())
   else MemException(E_SAMO_Access_Fault)
+}
+
+function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) =
+  if   within_mmio_writable(addr, width)
+  then mmio_write(addr, width, data)
+  else if within_phys_mem(addr, width)
+  then phys_mem_write(addr, width, data)
+  else MemException(E_SAMO_Access_Fault)
+
+/* FIXME: We assume atomic accesses are only done to memory-backed regions.  MMIO is not modeled. */
 
 val MEMval                            : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
 val MEMval_release                    : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
@@ -88,21 +108,21 @@ val MEMval_conditional                : forall 'n. (xlenbits, atom('n), bits(8 *
 val MEMval_conditional_release        : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
 val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
 
-function MEMval                            (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_release                    (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_strong_release             (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_conditional                (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_conditional_release        (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data)
-
+function MEMval                            (addr, width, data) = phys_mem_write(addr, width, data)
+function MEMval_release                    (addr, width, data) = phys_mem_write(addr, width, data)
+function MEMval_strong_release             (addr, width, data) = phys_mem_write(addr, width, data)
+function MEMval_conditional                (addr, width, data) = phys_mem_write(addr, width, data)
+function MEMval_conditional_release        (addr, width, data) = phys_mem_write(addr, width, data)
+function MEMval_conditional_strong_release (addr, width, data) = phys_mem_write(addr, width, data)
 
-val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(unit) effect {wmv, escape}
+/* NOTE: The wreg effect is due to MMIO. */
+val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(unit) effect {wmv, wreg, escape}
 
 function mem_write_value (addr, width, value, aq, rl, con) = {
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_SAMO_Addr_Align)
   else match (aq, rl, con) {
-    (false, false, false) => MEMval(addr, width, value),
+    (false, false, false) => checked_mem_write(addr, width, value),
     (false, true,  false) => MEMval_release(addr, width, value),
     (false, false, true)  => MEMval_conditional(addr, width, value),
     (false, true,  true)  => MEMval_conditional_release(addr, width, value),
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
new file mode 100644
index 00000000..4dc976ea
--- /dev/null
+++ b/riscv/riscv_platform.sail
@@ -0,0 +1,191 @@
+/* Platform and devices */
+
+/* Current constraints on this implementation are:
+   - it cannot access memory directly, but instead provides definitions for the physical memory model
+   - it can access system register state, needed to manipulate interrupt bits
+   - it relies on externs to get platform address information and doesn't hardcode them.
+*/
+
+/* Main memory */
+val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
+val plat_ram_size = {ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
+
+/* ROM holding reset vector and device-tree DTB */
+val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits
+val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits
+
+/* Location of clock-interface, which should match with the spec in the DTB */
+val plat_clint_base = {ocaml: "Platform.clint_base", lem: "plat_clint_base"} : unit -> xlenbits
+val plat_clint_size = {ocaml: "Platform.clint_size", lem: "plat_clint_size"} : unit -> xlenbits
+
+/* Location of HTIF ports */
+val plat_htif_tohost = {ocaml: "Platform.htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits
+// todo: fromhost
+
+val phys_mem_segments : unit -> list((xlenbits, xlenbits))
+function phys_mem_segments() =
+  (plat_rom_base (), plat_rom_size ()) ::
+  (plat_ram_base (), plat_ram_size ()) ::
+  [||]
+
+/* Physical memory map predicates */
+
+function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+  /* todo: iterate over segment list */
+  if (  plat_ram_base() <=_u addr
+      & (addr + sizeof('n)) <=_u (plat_ram_base() + plat_ram_size ()))
+       then true
+  else if (  plat_rom_base() <=_u addr
+           & (addr + sizeof('n)) <=_u (plat_rom_base() + plat_rom_size()))
+       then true
+  else false
+
+function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+    plat_clint_base() <=_u addr
+  & (addr + sizeof('n)) <=_u (plat_clint_base() + plat_clint_size())
+
+function within_htif_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+    plat_htif_tohost() == addr
+
+/* TODO */
+function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+    false
+
+/* CLINT (Core Local Interruptor), based on Spike. */
+
+val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int
+
+// assumes a single hart, since this typically is a vector of per-hart registers.
+register mtimecmp : xlenbits  // memory-mapped internal clint register.
+
+/* CLINT memory-mapped IO */
+
+let MSIP_BASE     : xlenbits = 0x0000000000000000
+let MTIMECMP_BASE : xlenbits = 0x0000000000004000
+let MTIME_BASE    : xlenbits = 0x000000000000bff8
+
+/* 0000 msip hart 0         -- memory-mapped software interrupt
+ * 0004 msip hart 1
+ * 4000 mtimecmp hart 0 lo  -- memory-mapped timer thresholds
+ * 4004 mtimecmp hart 0 hi
+ * 4008 mtimecmp hart 1 lo
+ * 400c mtimecmp hart 1 hi
+ * bff8 mtime lo            -- memory-mapped clocktimer value
+ * bffc mtime hi
+ */
+
+val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+function clint_load(addr, width) = {
+  let addr = addr - plat_clint_base ();
+  /* FIXME: For now, only allow exact aligned access. */
+  if addr == MSIP_BASE & ('n == 8 | 'n == 4)
+  then {
+    print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI()));
+    MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n)))
+  }
+  else if addr == MTIMECMP_BASE & ('n == 8)
+  then {
+    print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
+    MemValue(zero_extend(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */
+  }
+  else if addr == MTIME_BASE & ('n == 8)
+  then {
+    print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
+    MemValue(zero_extend(mtime, 64))
+  }
+  else {
+    print("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
+    MemException(E_Load_Access_Fault)
+  }
+}
+
+val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
+function clint_store(addr, width, data) = {
+  let addr = addr - plat_clint_base ();
+  print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
+    mip->MSI() = data[0] == 0b1;
+    MemValue(())
+  } else if addr == MTIMECMP_BASE & 'n == 8 then {
+    mtimecmp = zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */
+    MemValue(())
+  } else MemException(E_SAMO_Access_Fault)
+}
+
+/* Basic terminal character I/O. */
+
+val plat_term_write = {ocaml: "Platform.term_write", lem: "plat_term_write"} : bits(8) -> unit
+val plat_term_read  = {ocaml: "Platform.term_read",  lem: "plat_term_read"}  : unit -> bits(8)
+
+/* Spike's HTIF device interface, which multiplexes the above MMIO devices. */
+
+bitfield htif_cmd : bits(64) = {
+  device  : 63 .. 56,
+  cmd     : 55 .. 48,
+  payload : 47 .. 0
+}
+
+register htif_done : bool
+register htif_exit_code : xlenbits
+
+val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
+function htif_load(addr, width) = MemValue(EXTZ(0b0))
+
+/* FIXME: The wreg effect is an artifact of using 'register' to implement device state. */
+val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
+function htif_store(addr, width, data) = {
+  // since htif is only available at a single address, we'll assume here that physical memory
+  // model has correctly dispatched the address.
+  let cbits : xlenbits = EXTZ(data);
+  let cmd = Mk_htif_cmd(cbits);
+  match cmd.device() {
+    0x00 => { /* syscall-proxy */
+      print("htif-syscall-proxy[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+      if cmd.payload()[0] == 0b1
+      then {
+           htif_done = true;
+           htif_exit_code = (zero_extend(cmd.payload(), xlen) >> 0b01) : xlenbits
+      }
+      else ()
+    },
+    0x01 => { /* terminal */
+      print("htif-term[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+      match cmd.cmd() {
+        0x00 => /* TODO: terminal input handling */ (),
+        0x01 => plat_term_write(cmd.payload()[7..0]),
+        c    => print("Unknown term cmd: " ^ BitStr(c))
+      }
+    },
+    d => print("htif-????[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data))
+  };
+  MemValue(())
+}
+
+/* Top-level MMIO dispatch */
+
+function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+  within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n)
+
+function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+  within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
+
+function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+  if   within_clint(addr, width)
+  then clint_load(addr, width)
+  else if within_htif_readable(addr, width) & (1 <= 'n)
+  then htif_load(addr, width)
+  else MemException(E_Load_Access_Fault)
+
+function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) =
+  if   within_clint(addr, width)
+  then clint_store(addr, width, data)
+  else if within_htif_writable(addr, width) & 'n <= 8
+  then htif_store(addr, width, data)
+  else MemException(E_SAMO_Access_Fault)
+
+/* Platform initialization */
+
+function init_platform() -> unit = {
+  htif_done = false;
+  htif_exit_code = EXTZ(0b0);
+}
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 7ddd8a44..36f633ef 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -42,8 +42,8 @@ function fetch() -> FetchResult = {
 }
 
 /* returns whether an instruction was executed */
-val step : unit -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-function step() = {
+val step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function step(step_no) = {
   match curInterrupt(mip, mie, mideleg) {
     Some(intr, priv) => {
       print_bits("Handling interrupt: ", intr);
@@ -59,30 +59,28 @@ function step() = {
         F_RVC(h) => {
           match decodeCompressed(h) {
             None() => {
-              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(h) ^ " :  <no-decode>");
+              print("[" ^ string_of_int(step_no) ^ "] " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
               handle_decode_exception(EXTZ(h));
               false
             },
             Some(ast) => {
-              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(h) ^ " :  " ^ ast);
+              print("[" ^ string_of_int(step_no) ^ "] " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
               nextPC = PC + 2;
-              execute(ast);
-              true
+              execute(ast)
             }
           }
         },
         F_Base(w) => {
           match decode(w) {
             None() => {
-              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(w) ^ " :  <no-decode>");
+              print("[" ^ string_of_int(step_no) ^ "] " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
               handle_decode_exception(EXTZ(w));
               false
             },
             Some(ast) => {
-              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(w) ^ " :  " ^ ast);
+              print("[" ^ string_of_int(step_no) ^ "] " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
               nextPC = PC + 4;
-              execute(ast);
-              true
+              execute(ast)
             }
           }
         }
@@ -90,3 +88,27 @@ function step() = {
     }
   }
 }
+
+val loop : int -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
+function loop (tohost_addr) = {
+  let tohost = __GetSlice_int(64, tohost_addr, 0);
+  i : int = 0;
+  while true do {
+    tick_clock();
+    minstret_written = false;     /* see note for minstret */
+    let retired = step(i);
+    PC = nextPC;
+    if retired then {
+      i = i + 1;
+      retire_instruction()
+    };
+
+    /* check htif exit */
+    if htif_done then {
+      let exit_val = unsigned(htif_exit_code);
+      if exit_val == 0 then print("SUCCESS")
+      else print_int("FAILURE: ", exit_val);
+      exit(());
+    }
+  }
+}
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 3e36ebc7..9373701c 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -235,10 +235,54 @@ function legalize_xepc(v : xlenbits) -> xlenbits = {
 register mtval : xlenbits
 register mscratch : xlenbits
 
-/* time/cycles */
+/* counters */
+
+bitfield Counteren : bits(32) = {
+  HPM  : 31 .. 3,
+  IR   : 2,
+  TM   : 1,
+  CY   : 0
+}
+
+register mcounteren : Counteren
+register scounteren : Counteren
+
+function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
+  /* no HPM counters yet */
+  let c = update_IR(c, v[2]);
+  let c = update_TM(c, v[1]);
+  let c = update_CY(c, v[0]);
+  c
+}
+
+function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
+  /* no HPM counters yet */
+  let c = update_IR(c, v[2]);
+  let c = update_TM(c, v[1]);
+  let c = update_CY(c, v[0]);
+  c
+}
+
 register mcycle : xlenbits
 register mtime : xlenbits
+
+/* minstret is an architectural register, and can be written to.  The
+   spec says that minstret increments on instruction retires need to
+   occur before any explicit writes to instret.  However, in our
+   simulation loop, we need to execute an instruction to find out
+   whether it retired, and hence can only increment instret after
+   execution.  To avoid doing this in the case minstret was explicitly
+   written to, we track writes to it in a separate model-internal
+   register.
+*/
 register minstret : xlenbits
+register minstret_written : bool
+
+function retire_instruction() -> unit = {
+  if   minstret_written == true
+  then minstret_written = false
+  else minstret = minstret + 1
+}
 
 /* informational registers */
 register mvendorid : xlenbits
@@ -597,10 +641,27 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) =
 function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
   ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == true)
 
+function check_Counteren(csr : csreg, p : Privilege) -> bool =
+  match(csr, p) {
+    (0xC00, Supervisor) => mcounteren.CY() == true,
+    (0xC01, Supervisor) => mcounteren.TM() == true,
+    (0xC02, Supervisor) => mcounteren.IR() == true,
+
+    (0xC00, User) => scounteren.CY() == true,
+    (0xC01, User) => scounteren.TM() == true,
+    (0xC02, User) => scounteren.IR() == true,
+
+    (_, _) => /* no HPM counters for now */
+              if   0xC03 <=_u csr & csr <=_u 0xC1F
+              then false
+              else true
+  }
+
 function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
     is_CSR_defined(csr, p)
   & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
   & check_TVM_SATP(csr, p)
+  & check_Counteren(csr, p)
 
 /* Exception delegation: given an exception and the privilege at which
  * it occured, returns the privilege at which it should be handled.
@@ -790,17 +851,31 @@ function init_sys() -> unit = {
   cur_privilege = Machine;
 
   misa->MXL() = arch_to_bits(RV64);
-  misa->C() = true;
-  misa->U() = true;
-  misa->S() = true;
+  misa->A() = true; /* atomics */
+  misa->C() = true; /* RVC */
+  misa->I() = true; /* base integer ISA */
+  misa->M() = true; /* integer multiply/divide */
+  misa->U() = true; /* user-mode */
+  misa->S() = true; /* supervisor-mode */
 
   mstatus->SXL() = misa.MXL();
   mstatus->UXL() = misa.MXL();
   mstatus->SD()  = false;
 
   mhartid = EXTZ(0b0);
+
+  mcounteren->bits() = EXTZ(0b0);
+  minstret = EXTZ(0b0);
+  minstret_written = false;
 }
 
 function tick_clock() -> unit = {
   mcycle = mcycle + 1
 }
+
+/* memory access exceptions, defined here for use by the platform model. */
+
+union MemoryOpResult ('a : Type) = {
+  MemValue : 'a,
+  MemException: ExceptionType
+}
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index f0147e36..42042293 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -97,21 +97,20 @@ type amo = bits(1)
 /* base architecture definitions */
 enum Architecture = {RV32, RV64, RV128}
 type arch_xlen = bits(2)
-function architecture(a : arch_xlen) -> option(Architecture) = {
+function architecture(a : arch_xlen) -> option(Architecture) =
   match (a) {
     0b01 => Some(RV32),
     0b10 => Some(RV64),
     0b11 => Some(RV128),
     _    => None()
   }
-}
-function arch_to_bits(a : Architecture) -> arch_xlen = {
+
+function arch_to_bits(a : Architecture) -> arch_xlen =
   match (a) {
     RV32  => 0b01,
     RV64  => 0b10,
     RV128 => 0b11
   }
-}
 
 /* privilege levels */
 
@@ -119,35 +118,48 @@ type priv_level = bits(2)
 enum Privilege = {User, Supervisor, Machine}
 
 val cast privLevel_to_bits : Privilege -> priv_level
-function privLevel_to_bits (p) = {
+function privLevel_to_bits (p) =
   match (p) {
     User => 0b00,
     Supervisor => 0b01,
     Machine => 0b11
   }
-}
 
 val cast privLevel_of_bits : priv_level -> Privilege
-function privLevel_of_bits (p) = {
+function privLevel_of_bits (p) =
   match (p) {
     0b00 => User,
     0b01 => Supervisor,
     0b11 => Machine
   }
-}
 
 val cast privLevel_to_str : Privilege -> string
-function privLevel_to_str (p) = {
+function privLevel_to_str (p) =
   match (p) {
     User => "U",
     Supervisor => "S",
     Machine => "M"
   }
-}
 
 /* access types */
+
 enum AccessType = {Read, Write, ReadWrite, Execute}
+val cast accessType_to_str : AccessType -> string
+function accessType_to_str (a) =
+  match (a) {
+    Read => "R",
+    Write => "W",
+    ReadWrite => "RW",
+    Execute => "X"
+  }
+
 enum ReadType   = {Instruction, Data}
+val cast readType_to_str : ReadType -> string
+function readType_to_str (r) =
+  match (r) {
+    Instruction => "I",
+    Data => "D"
+  }
 
 /* architectural exception and interrupt definitions */
 
@@ -173,7 +185,7 @@ enum ExceptionType = {
 }
 
 val cast exceptionType_to_bits : ExceptionType -> exc_code
-function exceptionType_to_bits(e) = {
+function exceptionType_to_bits(e) =
   match (e) {
     E_Fetch_Addr_Align => 0x0,
     E_Fetch_Access_Fault => 0x1,
@@ -192,10 +204,9 @@ function exceptionType_to_bits(e) = {
     E_Reserved_14 => 0xe,
     E_SAMO_Page_Fault => 0xf
   }
-}
 
 val cast exceptionType_to_str : ExceptionType -> string
-function exceptionType_to_str(e) = {
+function exceptionType_to_str(e) =
   match (e) {
     E_Fetch_Addr_Align => "fisaligned-fetch",
     E_Fetch_Access_Fault => "fetch-access-fault",
@@ -214,7 +225,6 @@ function exceptionType_to_str(e) = {
     E_Reserved_14 => "reserved-1",
     E_SAMO_Page_Fault => "store/amo-page-fault"
   }
-}
 
 enum InterruptType = {
   I_U_Software,
@@ -229,7 +239,7 @@ enum InterruptType = {
 }
 
 val cast interruptType_to_bits : InterruptType -> exc_code
-function interruptType_to_bits (i) = {
+function interruptType_to_bits (i) =
   match (i) {
     I_U_Software => 0x0,
     I_S_Software => 0x1,
@@ -241,19 +251,17 @@ function interruptType_to_bits (i) = {
     I_S_External => 0x9,
     I_M_External => 0xb
   }
-}
 
 type tv_mode = bits(2)
 enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved}
 
 val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode
-function trapVectorMode_of_bits (m) = {
+function trapVectorMode_of_bits (m) =
   match (m) {
     0b00 => TV_Direct,
     0b01 => TV_Vector,
     _    => TV_Reserved
   }
-}
 
 /* other exceptions */
 
@@ -277,38 +285,35 @@ type ext_status = bits(2)
 enum ExtStatus = {Off, Initial, Clean, Dirty}
 
 val cast extStatus_to_bits : ExtStatus -> ext_status
-function extStatus_to_bits(e) = {
+function extStatus_to_bits(e) =
   match (e) {
     Off => 0b00,
     Initial => 0b01,
     Clean => 0b10,
     Dirty => 0b11
   }
-}
 
 val cast extStatus_of_bits : ext_status -> ExtStatus
-function extStatus_of_bits(e) = {
+function extStatus_of_bits(e) =
   match (e) {
     0b00 => Off,
     0b01 => Initial,
     0b10 => Clean,
     0b11 => Dirty
   }
-}
 
 /* supervisor-level address translation modes */
 
 type satp_mode = bits(4)
 enum SATPMode = {Sbare, Sv32, Sv39}
 
-function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = {
+function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) =
   match (a, m) {
     (_, 0x0)    => Some(Sbare),
     (RV32, 0x1) => Some(Sv32),
     (RV64, 0x8) => Some(Sv39),
     (_, _)      => None()
   }
-}
 
 /* CSR access control bits (from CSR addresses) */
 type csrRW = bits(2)  /* read/write */
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index 4fb7b5d5..d5efe252 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -131,7 +131,8 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
   let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
                                 PTE39_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
-  match (checked_mem_read(Data, EXTZ(pte_addr), 8)) {
+  /* FIXME: we assume here that walks only access memory-backed addresses. */
+  match (phys_mem_read(Data, EXTZ(pte_addr), 8)) {
     MemException(_) => PTW_Failure(PTW_Access),
     MemValue(v) => {
       let pte = Mk_SV39_PTE(v);