Ocaml semantics can now run aarch64 hello world example using octapod

New testcase for bitfield syntax

Updated to work with latest lem and linksem

13 files changed, 451 insertions, 97 deletions

diff --git a/src/_tags b/src/_tags
index efe34d17..f1d54db1 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,15 +1,16 @@
 true: -traverse, debug, use_menhir
 <**/*.ml>: bin_annot, annot
 # <lem_interp> or <test>: include
-<sail.{byte,native}>: package(zarith), use_pprint, use_nums, use_unix, use_str, use_lem
-<isail.{byte,native}>: package(zarith), package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem
+<sail.{byte,native}>: package(zarith), use_pprint, use_unix, use_str, package(lem)
+<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), use_pprint
 <isail.ml>: package(linenoise)
+<elf_loader.ml>: package(linksem)
 <pprint> or <pprint/src>: include
-<*.m{l,li}>: use_lem
+<*.m{l,li}>: package(lem)
 
 # see http://caml.inria.fr/mantis/view.php?id=4943
-<lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, use_lem
-<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str
+<lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, package(lem)
+<test/*> and not <test/*.cmxa>: use_nums, package(lem), use_str
 
 # disable partial match and unused variable warnings
 <**/*.ml>: warn_y
diff --git a/src/bitfield.ml b/src/bitfield.ml
index 0a32654d..db3411b1 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -1,3 +1,52 @@
+(**************************************************************************)
+(*     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.                                                          *)
+(**************************************************************************)
 
 module Big_int = Nat_big_num
 
@@ -18,6 +67,7 @@ let newtype name size order =
   let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
   ast_of_def_string order nt
 
+(* These functions define the getter and setter for all the bits in the field. *)
 let full_getter name size order =
   let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
   let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
@@ -41,6 +91,7 @@ let full_overload name order =
 let full_accessor name size order =
   combine [full_getter name size order; full_setter name size order; full_overload name order]
 
+(* For every index range, create a getter and setter *)
 let index_range_getter' name field order start stop =
   let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
   let irg_val = Printf.sprintf "val _get_%s : %s -> %s" field name (bitvec size order) in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4e466596..28579291 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -964,7 +964,8 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false))
+let extern_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> None), false))
 
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
@@ -1003,7 +1004,7 @@ let have_undefined_builtins = ref false
 
 let generate_undefineds vs_ids (Defs defs) =
   let gen_vs id str =
-    if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
+    if (IdSet.mem id vs_ids) then [] else [extern_of_string dec_ord id str]
   in
   let undefined_builtins =
     if !have_undefined_builtins then
@@ -1022,7 +1023,7 @@ let generate_undefineds vs_ids (Defs defs) =
            gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
            gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
            (* FIXME: How to handle inc/dec order correctly? *)
-           gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}";
+           gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
            (* Only used with lem_mwords *)
            gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
            gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 7a4b6b33..59b20a17 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -54,7 +54,7 @@ open Value
 
 type gstate =
   { registers : value Bindings.t;
-    letbinds : (Type_check.tannot letbind) list
+    letbinds : (Type_check.tannot letbind) list;
   }
 
 type lstate =
@@ -70,7 +70,7 @@ let rec ast_letbinds (Defs defs) =
 
 let initial_gstate ast =
   { registers = Bindings.empty;
-    letbinds = ast_letbinds ast
+    letbinds = ast_letbinds ast;
   }
 
 let initial_lstate =
@@ -179,6 +179,22 @@ let assertion_failed msg = Yield (Assertion_failed msg)
 
 let liftM2 f m1 m2 = m1 >>= fun x -> m2 >>= fun y -> return (f x y)
 
+let rec pat_ids (P_aux (pat_aux, _)) =
+  match pat_aux with
+  | P_lit _ | P_wild -> IdSet.empty
+  | P_id id -> IdSet.singleton id
+  | P_as (pat, id) -> IdSet.add id (pat_ids pat)
+  | P_var (pat, _) | P_typ (_, pat) -> pat_ids pat
+  | P_app (_, pats) | P_tup pats | P_vector pats | P_vector_concat pats | P_list pats ->
+     List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
+  | P_cons (pat1, pat2) ->
+     IdSet.union (pat_ids pat1) (pat_ids pat2)
+  | P_record (fpats, _) ->
+     List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty
+and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat
+
+let letbind_pat_ids (LB_aux (LB_val (pat, _), _)) = pat_ids pat
+
 let rec subst id value (E_aux (e_aux, annot) as exp) =
   let wrap e_aux = E_aux (e_aux, annot) in
   let e_aux = match e_aux with
@@ -187,34 +203,96 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_id id' -> if Id.compare id id' = 0 then unaux_exp (exp_of_value value) else E_id id'
     | E_lit lit -> E_lit lit
     | E_cast (typ, exp) -> E_cast (typ, subst id value exp)
+
     | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps)
     | E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2)
+
     | E_tuple exps -> E_tuple (List.map (subst id value) exps)
-    | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *)
-    | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
-       (* TODO: Fix shadowing *)
-       E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot), subst id value body)
+
     | E_if (cond, then_exp, else_exp) ->
        E_if (subst id value cond, subst id value then_exp, subst id value else_exp)
+
+    | E_loop (loop, cond, body) ->
+       E_loop (loop, subst id value cond, subst id value body)
+    | E_for (id', exp1, exp2, exp3, order, body) when Id.compare id id' = 0 ->
+       E_for (id', exp1, exp2, exp3, order, body)
+    | E_for (id', exp1, exp2, exp3, order, body) ->
+       E_for (id', subst id value exp1, subst id value exp2, subst id value exp3, order, subst id value body)
+
     | E_vector exps -> E_vector (List.map (subst id value) exps)
+    | E_vector_access (exp1, exp2) -> E_vector_access (subst id value exp1, subst id value exp2)
+    | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (subst id value exp1, subst id value exp2, subst id value exp3)
+    | E_vector_update (exp1, exp2, exp3) -> E_vector_update (subst id value exp1, subst id value exp2, subst id value exp3)
+    | E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
+       E_vector_update_subrange (subst id value exp1, subst id value exp2, subst id value exp3, subst id value exp4)
+    | E_vector_append (exp1, exp2) -> E_vector_append (subst id value exp1, subst id value exp2)
+
+    | E_list exps -> E_list (List.map (subst id value) exps)
+    | E_cons (exp1, exp2) -> E_cons (subst id value exp1, subst id value exp2)
+
+    | E_record fexps -> E_record (subst_fexps id value fexps)
+    | E_record_update (exp, fexps) -> E_record_update (subst id value exp, subst_fexps id value fexps)
+    | E_field (exp, id') -> E_field (subst id value exp, id')
+
+    | E_case (exp, pexps) ->
+       E_case (subst id value exp, List.map (subst_pexp id value) pexps)
+
+    | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
+       E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot),
+              if IdSet.mem id (pat_ids pat) then body else subst id value body)
+
+    | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *)
+
+    (* Should be re-written *)
+    | E_sizeof nexp -> E_sizeof nexp
+    | E_constraint nc -> E_constraint nc
+
     | E_return exp -> E_return (subst id value exp)
+    | E_exit exp -> E_exit (subst id value exp)
+    (* Not sure about this, but id should always be immutable while id' must be mutable so should be ok. *)
+    | E_ref id' -> E_ref id'
+    | E_throw exp -> E_throw (subst id value exp)
+
+    | E_try (exp, pexps) ->
+       E_try (subst id value exp, List.map (subst_pexp id value) pexps)
+
     | E_assert (exp1, exp2) -> E_assert (subst id value exp1, subst id value exp2)
+
     | E_internal_value v -> E_internal_value v
     | _ -> failwith ("subst " ^ string_of_exp exp)
   in
   wrap e_aux
 
+and subst_pexp id value (Pat_aux (pexp_aux, annot)) =
+  let pexp_aux = match pexp_aux with
+    | Pat_exp (pat, exp) when IdSet.mem id (pat_ids pat) -> Pat_exp (pat, exp)
+    | Pat_exp (pat, exp) -> Pat_exp (pat, subst id value exp)
+    | Pat_when (pat, guard, exp) when IdSet.mem id (pat_ids pat) -> Pat_when (pat, guard, exp)
+    | Pat_when (pat, guard, exp) -> Pat_when (pat, subst id value guard, subst id value exp)
+  in
+  Pat_aux (pexp_aux, annot)
+
+
+and subst_fexps id value (FES_aux (FES_Fexps (fexps, flag), annot)) =
+  FES_aux (FES_Fexps (List.map (subst_fexp id value) fexps, flag), annot)
+
+and subst_fexp id value (FE_aux (FE_Fexp (id', exp), annot)) =
+  FE_aux (FE_Fexp (id', subst id value exp), annot)
+
 and subst_lexp id value (LEXP_aux (lexp_aux, annot) as lexp) =
   let wrap lexp_aux = LEXP_aux (lexp_aux, annot) in
   let lexp_aux = match lexp_aux with
     | LEXP_deref exp -> LEXP_deref (subst id value exp)
     | LEXP_id id' -> LEXP_id id'
     | LEXP_memory (f, exps) -> LEXP_memory (f, List.map (subst id value) exps)
-    | _ -> failwith ("subst lexp")
+    | LEXP_cast (typ, id') -> LEXP_cast (typ, id')
+    | LEXP_tup lexps -> LEXP_tup (List.map (subst_lexp id value) lexps)
+    | LEXP_vector (lexp, exp) -> LEXP_vector (subst_lexp id value lexp, subst id value exp)
+    | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (subst_lexp id value lexp, subst id value exp1, subst id value exp2)
+    | LEXP_field (lexp, id') -> LEXP_field (subst_lexp id value lexp, id')
   in
   wrap lexp_aux
 
-
 (**************************************************************************)
 (* 2. Expression Evaluation                                               *)
 (**************************************************************************)
@@ -224,13 +302,14 @@ let unit_exp = E_lit (L_aux (L_unit, Parse_ast.Unknown))
 let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp
 let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp)
 
-let rec build_letchain lbs (E_aux (_, annot) as exp) =
-  print_endline ("LETCHAIN " ^ string_of_exp exp);
+let rec build_letchain id lbs (E_aux (_, annot) as exp) =
+  (* print_endline ("LETCHAIN " ^ string_of_exp exp); *)
   match lbs with
   | [] -> exp
-  | lb :: lbs ->
+  | lb :: lbs when IdSet.mem id (letbind_pat_ids lb)->
      let exp = E_aux (E_let (lb, exp), annot) in
-     build_letchain lbs exp
+     build_letchain id lbs exp
+  | _ :: lbs -> build_letchain id lbs exp
 
 let rec step (E_aux (e_aux, annot) as orig_exp) =
   let wrap e_aux' = return (E_aux (e_aux', annot)) in
@@ -248,6 +327,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
   | E_if (exp, then_exp, else_exp) ->
      step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp))
 
+  | E_loop (While, exp, body) when not (is_value exp) ->
+     step exp >>= fun exp' -> wrap (E_loop (While, exp', body))
+  | E_loop (While, exp, body) when is_true exp -> wrap (E_block [body; orig_exp])
+  | E_loop (While, exp, body) when is_false exp -> wrap unit_exp
+  | E_loop _ -> assert false (* Impossible *)
+
   | E_assert (exp, msg) when is_true exp -> wrap unit_exp
   | E_assert (exp, msg) when is_false exp -> assertion_failed "FIXME"
   | E_assert (exp, msg) ->
@@ -262,6 +347,15 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
        | [] -> return (exp_of_value (V_vector (List.map value_of_exp evaluated)))
      end
 
+  | E_list exps ->
+     let evaluated, unevaluated = Util.take_drop is_value exps in
+     begin
+       match unevaluated with
+       | exp :: exps ->
+          step exp >>= fun exp' -> wrap (E_list (evaluated @ exp' :: exps))
+       | [] -> return (exp_of_value (V_list (List.map value_of_exp evaluated)))
+     end
+
   (* Special rules for short circuting boolean operators *)
   | E_app (id, [x; y]) when (string_of_id id = "and_bool" || string_of_id id = "or_bool") && not (is_value x) ->
      step x >>= fun x' -> wrap (E_app (id, [x'; y]))
@@ -273,7 +367,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
   | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) when not (is_value bind) ->
      step bind >>= fun bind' -> wrap (E_let (LB_aux (LB_val (pat, bind'), lb_annot), body))
   | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
-     let matched, bindings = pattern_match pat (value_of_exp bind) in
+     let matched, bindings = pattern_match (Type_check.env_of orig_exp) pat (value_of_exp bind) in
      if matched then
        return  (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
      else
@@ -323,16 +417,29 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      step exp >>= fun exp' -> wrap (E_case (exp', pexps))
   | E_case (_, []) -> failwith "Pattern matching failed"
   | E_case (exp, Pat_aux (Pat_exp (pat, body), _) :: pexps) ->
-     let matched, bindings = pattern_match pat (value_of_exp exp) in
+     let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
      if matched then
        return  (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
      else
        wrap (E_case (exp, pexps))
+  | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when not (is_value guard) ->
+     let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
+     if matched then
+       let guard = List.fold_left (fun guard (id, v) -> subst id v guard) guard (Bindings.bindings bindings) in
+       let body = List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings) in
+       step guard >>= fun guard' ->
+       wrap (E_case (exp, Pat_aux (Pat_when (pat, guard', body), pat_annot) :: pexps))
+     else
+       wrap (E_case (exp, pexps))
+  | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_true guard -> return body
+  | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_false guard -> wrap (E_case (exp, pexps))
 
   | E_cast (typ, exp) -> return exp
 
   | E_throw exp when is_value exp -> throw (value_of_exp exp)
   | E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp')
+  | E_exit exp when is_value exp -> throw (V_ctor ("Exit", [value_of_exp exp]))
+  | E_exit exp -> step exp >>= fun exp' -> wrap (E_exit exp')
 
   | E_ref id -> return (exp_of_value (V_ref (string_of_id id)))
   | E_id id ->
@@ -350,9 +457,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
           return exp
        | Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals))
        | Local (Immutable, _) ->
-          let chain = build_letchain gstate.letbinds orig_exp in
-          print_endline "CHAINED";
+          let chain = build_letchain id gstate.letbinds orig_exp in
           return chain
+       | Enum _ ->
+          return (exp_of_value (V_ctor (string_of_id id, [])))
        | _ -> failwith "id"
      end
 
@@ -388,19 +496,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
           |> return
      end
 
+  | E_field (exp, id) when not (is_value exp) ->
+     step exp >>= fun exp' -> wrap (E_field (exp', id))
+  | E_field (exp, id) ->
+     let record = coerce_record (value_of_exp exp) in
+     return (exp_of_value (StringMap.find (string_of_id id) record))
+
   | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp'))
   | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp]))
-  | E_assign (LEXP_aux (LEXP_field (lexp, id), _), exp) ->
+  | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
      let open Type_check in
      let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in
-     let ul = (Parse_ast.Unknown, None) in
      let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in
      wrap (E_assign (lexp, exp'))
-  | E_assign (LEXP_aux (LEXP_vector (vec, n), _), exp) ->
+  | E_assign (LEXP_aux (LEXP_vector (vec, n), lexp_annot), exp) ->
      let open Type_check in
      let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
-     let ul = (Parse_ast.Unknown, None) in
-     let exp' = E_aux (E_vector_update (vec_exp, n, exp), ul) in
+     let exp' = E_aux (E_vector_update (vec_exp, n, exp), lexp_annot) in
      wrap (E_assign (vec, exp'))
   | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) ->
      begin
@@ -419,7 +531,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      let id = Id_aux (Id (coerce_ref (value_of_exp reference)), Parse_ast.Unknown) in
      gets >>= fun (lstate, gstate) ->
      puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp
-  | E_assign _ -> assert false
+  | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment"
+     (*
+     let values = coerce_tuple (value_of_exp exp) in
+     wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values))
+      *)
+  | E_assign _ -> failwith (string_of_exp orig_exp);
 
   | E_try (exp, pexps) when is_value exp -> return exp
   | E_try (exp, pexps) ->
@@ -452,40 +569,51 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
   | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id))
 
 and lexp_assign (LEXP_aux (lexp_aux, _) as lexp) value =
-  print_endline ("Assigning: " ^ string_of_lexp lexp ^ " to " ^ string_of_value value |> Util.yellow |> Util.clear);
+  (* print_endline ("Assigning: " ^ string_of_lexp lexp ^ " to " ^ string_of_value value |> Util.yellow |> Util.clear); *)
   match lexp_aux with
   | LEXP_id id -> Bindings.singleton id value
   | _ -> failwith "Unhandled lexp_assign"
 
-and pattern_match (P_aux (p_aux, _) as pat) value =
-  print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear);
+and pattern_match env (P_aux (p_aux, _) as pat) value =
+  (* print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); *)
   match p_aux with
   | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty
   | P_wild -> true, Bindings.empty
   | P_as (pat, id) ->
-     let matched, bindings = pattern_match pat value in
+     let matched, bindings = pattern_match env pat value in
      matched, Bindings.add id value bindings
-  | P_typ (_, pat) -> pattern_match pat value
-  | P_id id -> true, Bindings.singleton id value
-  | P_var (pat, _) -> pattern_match pat value
+  | P_typ (_, pat) -> pattern_match env pat value
+  | P_id id ->
+     let open Type_check in
+     begin
+       match Env.lookup_id id env with
+       | Enum _ | Union _ ->
+          if is_ctor value && string_of_id id = fst (coerce_ctor value)
+          then true, Bindings.empty
+          else false, Bindings.empty
+       | _ -> true, Bindings.singleton id value
+     end
+  | P_var (pat, _) -> pattern_match env pat value
   | P_app (id, pats) ->
      let (ctor, vals) = coerce_ctor value in
      if Id.compare id (mk_id ctor) = 0 then
-       let matches = List.map2 pattern_match pats vals in
+       let matches = List.map2 (pattern_match env) pats vals in
        List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
      else
        false, Bindings.empty
   | P_record _ -> assert false (* TODO *)
-  | P_vector _ -> assert false (* TODO *)
+  | P_vector pats ->
+     let matches = List.map2 (pattern_match env) pats (coerce_gv value) in
+     List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
   | P_vector_concat _ -> assert false (* TODO *)
   | P_tup pats | P_list pats ->
-     let matches = List.map2 pattern_match pats (coerce_listlike value) in
+     let matches = List.map2 (pattern_match env) pats (coerce_listlike value) in
      List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
   | P_cons _ -> assert false (* TODO *)
 
-let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), _)) value =
+let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) value =
   let pexp_of_funcl (FCL_aux (FCL_Funcl (_, pexp), _)) = pexp in
-  E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), (Parse_ast.Unknown, None))
+  E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), annot)
 
 let rec get_fundef id (Defs defs) =
   match defs with
@@ -500,31 +628,45 @@ let stack_state (_, lstate, _) = lstate
 type frame =
   | Done of state * value
   | Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list
+  | Break of frame
 
-let rec eval_frame ast = function
+let rec eval_frame' ast = function
   | Done (state, v) -> Done (state, v)
+  | Break frame -> Break frame
   | Step (out, state, m, stack) ->
      match (m, stack) with
      | Pure v, [] when is_value v -> Done (state, value_of_exp v)
      | Pure v, (head :: stack') when is_value v ->
-        print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear);
+        (* print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); *)
         Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack')
      | Pure exp', _ ->
         let out' = Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp') in
         Step (out', state, step exp', stack)
+     | Yield (Call(id, vals, cont)), _ when string_of_id id = "break" ->
+        let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
+        let body = exp_of_fundef (get_fundef id ast) arg in
+        Break (Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack))
      | Yield (Call(id, vals, cont)), _ ->
-        print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear);
+        (* print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); *)
         let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
         let body = exp_of_fundef (get_fundef id ast) arg in
         Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)
      | Yield (Gets cont), _ ->
-        eval_frame ast (Step (out, state, cont state, stack))
+        eval_frame' ast (Step (out, state, cont state, stack))
      | Yield (Puts (state', cont)), _ ->
-        eval_frame ast (Step (out, state', cont (), stack))
+        eval_frame' ast (Step (out, state', cont (), stack))
      | Yield (Early_return v), [] -> Done (state, v)
      | Yield (Early_return v), (head :: stack') ->
-        print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear);
+        (* print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear); *)
         Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack')
      | Yield (Assertion_failed msg), _ ->
         failwith msg
+     | Yield (Exception v), _ ->
+        print_endline ("Uncaught Exception" |> Util.cyan |> Util.clear);
+        Done (state, v)
      | _ -> assert false
+
+let eval_frame ast frame =
+  try eval_frame' ast frame with
+  | Type_check.Type_error (l, err) ->
+     raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
diff --git a/src/isail.ml b/src/isail.ml
index 5452b7a9..6b60581b 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -76,7 +76,10 @@ let rec user_input callback =
   | None -> ()
   | Some v ->
      mode_clear ();
-     callback v;
+     begin
+       try callback v with
+       | Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
+     end;
      user_input callback
 
 let termcode n = "\x1B[" ^ string_of_int n ^ "m"
@@ -86,25 +89,72 @@ let clear str = str ^ termcode 0
 
 let sail_logo =
   let banner str = str |> bold |> red |> clear in
-  [ "    ___       ___       ___       ___ ";
-    "   /\\  \\     /\\  \\     /\\  \\     /\\__\\";
-    "  /::\\  \\   /::\\  \\   _\\:\\  \\   /:/  /";
-    " /\\:\\:\\__\\ /::\\:\\__\\ /\\/::\\__\\ /:/__/ ";
-    " \\:\\:\\/__/ \\/\\::/  / \\::/\\/__/ \\:\\  \\ ";
-    "  \\::/  /    /:/  /   \\:\\__\\    \\:\\__\\";
-    "   \\/__/     \\/__/     \\/__/     \\/__/";
+  [ {|    ___       ___       ___       ___ |};
+    {|   /\  \     /\  \     /\  \     /\__\|};
+    {|  /::\  \   /::\  \   _\:\  \   /:/  /|};
+    {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
+    {| \:\:\/__/ \/\::/  / \::/\/__/ \:\  \ |};
+    {|  \::/  /    /:/  /   \:\__\    \:\__\|};
+    {|   \/__/     \/__/     \/__/     \/__/|};
     ""
   ]
   |> List.map banner
 
 let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
 
+let print_program () =
+  match !current_mode with
+  | Normal -> ()
+  | Evaluation (Step (out, _, _, stack)) ->
+     let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in
+     List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep);
+     print_endline out
+  | Evaluation _ -> ()
+
+let interactive_state = ref (initial_state !interactive_ast)
+
+let rec run () =
+  match !current_mode with
+  | Normal -> ()
+  | Evaluation frame ->
+     begin
+       match frame with
+       | Done (state, v) ->
+          interactive_state := state;
+          print_endline ("Result = " ^ Value.string_of_value v);
+          current_mode := Normal
+       | Step (out, state, _, stack) ->
+          current_mode := Evaluation (eval_frame !interactive_ast frame);
+          run ()
+       | Break frame ->
+          print_endline "Breakpoint";
+          current_mode := Evaluation frame
+     end
+
+let rec run_steps n =
+  match !current_mode with
+  | _ when n <= 0 -> ()
+  | Normal -> ()
+  | Evaluation frame ->
+     begin
+       match frame with
+       | Done (state, v) ->
+          interactive_state := state;
+          print_endline ("Result = " ^ Value.string_of_value v);
+          current_mode := Normal
+       | Step (out, state, _, stack) ->
+          current_mode := Evaluation (eval_frame !interactive_ast frame);
+          run_steps (n - 1)
+       | Break frame ->
+          print_endline "Breakpoint";
+          current_mode := Evaluation frame
+     end
+
 let handle_input input =
+  LNoise.history_add input |> ignore;
   match !current_mode with
   | Normal ->
      begin
-       LNoise.history_add input |> ignore;
-
        if input <> "" && input.[0] = ':' then
          let n = try String.index input ' ' with Not_found -> String.length input in
          let cmd = Str.string_before input n in
@@ -114,37 +164,50 @@ let handle_input input =
             let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in
             pretty_sail stdout (doc_binding (typq, typ));
             print_newline ();
-         | ":q" | ":quit" ->
-            exit 0
+         | ":elf" ->
+            Elf_loader.load_elf arg
+         | ":q" | ":quit" -> exit 0
          | ":i" | ":infer" ->
             let exp = Initial_check.exp_of_string dec_ord arg in
             let exp = Type_check.infer_exp !interactive_env exp in
             pretty_sail stdout (doc_typ (Type_check.typ_of exp));
             print_newline ()
          | ":v" | ":verbose" ->
-            Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 2
+            Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3;
+            print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug)
 
          | _ -> print_endline ("Unrecognised command " ^ input)
        else if input <> "" then
          let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in
-         current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state !interactive_ast, return exp, [])))
+         current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, [])));
+         print_program ()
        else ()
      end
   | Evaluation frame ->
      begin
-       match frame with
-       | Done (_, v) ->
-          print_endline ("Result = " ^ Value.string_of_value v);
-          current_mode := Normal
-       | Step (out, _, _, stack) ->
-          let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in
-          List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep);
-          print_endline out;
-          current_mode := Evaluation (eval_frame !interactive_ast frame)
+       if input <> "" && input.[0] = ':' then
+         let n = try String.index input ' ' with Not_found -> String.length input in
+         let cmd = Str.string_before input n in
+         let arg = String.trim (Str.string_after input n) in
+         match cmd with
+         | ":r" | ":run" ->
+            run ()
+         | ":s" | ":step" ->
+            run_steps (int_of_string arg)
+         | ":q" | ":quit" -> exit 0
+         | _ -> print_endline ("Unrecognised command " ^ input)
+       else
+         match frame with
+         | Done (state, v) ->
+            interactive_state := state;
+            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 ()
      end
 
-
-
 let () =
   (* Auto complete function names based on val specs *)
   LNoise.set_completion_callback
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index 1babc1c9..ae58f7b2 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -69,8 +69,6 @@ let split ch s =
 let lem_dir =
   try Sys.getenv "LEM_DIR" (* LEM_DIR must contain an absolute path *)
   with Not_found -> "../../../lem" ;;
-let lem_libdir = lem_dir / "ocaml-lib" / "_build_zarith";;
-let lem_lib = lem_libdir / "extract" ;;
 let lem = lem_dir / "lem" ;;
 
 (* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *)
@@ -85,9 +83,8 @@ let lem_opts = [A "-lib"; P "../lem_interp";
 dispatch begin function
 | After_rules ->
     (* ocaml_lib "lem_interp/interp"; *)
-    ocaml_lib ~extern:true ~dir:lem_libdir  ~tag_name:"use_lem" lem_lib;
     ocaml_lib ~extern:false ~dir:"pprint/src" ~tag_name:"use_pprint" "pprint/src/PPrintLib";
-    
+
     rule "lem -> ml"
     ~prod: "%.ml"
     ~dep: "%.lem"
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 89220356..55695114 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -647,7 +647,7 @@ let ocaml_main spec =
           ^//^ (string "Random.self_init ();"
                 ^/^ string "load_elf ();"
                 ^/^ string (if !opt_trace_ocaml then "Sail_lib.opt_trace := true;" else "Sail_lib.opt_trace := false;")
-                ^/^ string "initialize_registers ();"
+                ^/^ string "zinitializze_registers ();"
                 ^/^ string "Printexc.record_backtrace true;"
                 ^/^ string "zmain ()")
          ]
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2ecaf91d..3b74d38a 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2924,6 +2924,9 @@ let rewrite_defs_ocaml = [
   ]
 
 let rewrite_defs_interpreter = [
+    ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+    ("tuple_assignments", rewrite_tuple_assignments);
+    ("remove_vector_concat", rewrite_defs_remove_vector_concat);
     ("constraint", rewrite_constraint);
     ("trivial_sizeof", rewrite_trivial_sizeof);
     ("sizeof", rewrite_sizeof);
diff --git a/src/sail.ml b/src/sail.ml
index 974885c6..eee80045 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -60,7 +60,6 @@ let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
 let opt_print_sil = ref false
 let opt_print_ocaml = ref false
-let opt_convert = ref false
 let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_libs_lem = ref ([]:string list)
@@ -118,9 +117,6 @@ let options = Arg.align ([
   ( "-no_effects",
     Arg.Set Type_check.opt_no_effects,
     " (experimental) turn off effect checking");
-  ( "-convert",
-    Arg.Set opt_convert,
-    " (experimental) convert sail to new syntax for use with -new_parser");
   ( "-just_check",
     Arg.Set opt_just_check,
     " (experimental) terminate immediately after typechecking");
@@ -185,10 +181,6 @@ let main() =
                         -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
     let ast = convert_ast Ast_util.inc_ord ast in
 
-    if !opt_convert
-    then (Pretty_print_sail.pp_defs stdout ast; exit 0)
-    else ();
-
     let (ast, type_envs) = check_ast ast in
 
     let (ast, type_envs) =
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index b4dffba9..72974b9a 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -87,10 +87,10 @@ let undefined_bit () =
 let undefined_bool () =
   if !random then Random.bool () else false
 
-let rec undefined_vector (start_index, len, item) =
+let rec undefined_vector (len, item) =
   if Big_int.equal len Big_int.zero
   then []
-  else item :: undefined_vector (start_index, Big_int.sub len (Big_int.of_int 1), item)
+  else item :: undefined_vector (Big_int.sub len (Big_int.of_int 1), item)
 
 let undefined_string () = ""
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 3269de1d..b77d800e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -76,7 +76,7 @@ type type_error =
   (* First parameter is the error that caused us to start doing type
      coercions, the second is the errors encountered by all possible
      coercions *)
-  | Err_no_casts of type_error * type_error list
+  | Err_no_casts of unit exp * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
   | Err_unresolved_quants of id * quant_item list
   | Err_subtype of typ * typ * n_constraint list
@@ -86,11 +86,13 @@ type type_error =
 let pp_type_error err =
   let open PPrint in
   let rec pp_err = function
-    | Err_no_casts (trigger, []) ->
-       (string "Tried performing type coercion because" ^//^ pp_err trigger)
-       ^/^ string "No possible coercions"
-    | Err_no_casts (trigger, errs) ->
-       (string "Tried performing type coerction because" ^//^ pp_err trigger)
+    | Err_no_casts (exp, trigger, []) ->
+       (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp)
+       ^/^ (string "Failed because" ^//^ pp_err trigger)
+       ^/^ string "There were no possible casts"
+    | Err_no_casts (exp, trigger, errs) ->
+       (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp)
+       ^/^ string "Failed because" ^//^ pp_err trigger
     | Err_no_overloading (id, errs) ->
        string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
          group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^^ space ^^ pp_err err) errs)
@@ -2173,7 +2175,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
     | _ -> failwith "Cannot switch type for unannotated function"
   in
   let rec try_casts trigger errs = function
-    | [] -> typ_raise l (Err_no_casts (trigger, errs))
+    | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, trigger, errs))
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ);
         try
diff --git a/src/type_check.mli b/src/type_check.mli
index 33615e43..b43cab6b 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -56,7 +56,7 @@ val opt_tc_debug : int ref
 val opt_no_effects : bool ref
 
 type type_error =
-  | Err_no_casts of type_error * type_error list
+  | Err_no_casts of unit exp * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
   | Err_unresolved_quants of id * quant_item list
   | Err_subtype of typ * typ * n_constraint list
diff --git a/src/value.ml b/src/value.ml
index d9690899..2ddeecae 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -186,6 +186,10 @@ let value_append = function
   | [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2)
   | _ -> failwith "value append"
 
+let value_slice = function
+  | [v1; v2; v3] -> V_vector (Sail_lib.slice (coerce_gv v1, coerce_int v2, coerce_int v3))
+  | _ -> failwith "value slice"
+
 let value_not = function
   | [v] -> V_bool (not (coerce_bool v))
   | _ -> failwith "value not"
@@ -214,6 +218,21 @@ let value_get_slice_int = function
   | [v1; v2; v3] -> mk_vector (Sail_lib.get_slice_int (coerce_int v1, coerce_int v2, coerce_int v3))
   | _ -> failwith "value get_slice_int"
 
+let value_set_slice_int = function
+  | [v1; v2; v3; v4] ->
+     V_int (Sail_lib.set_slice_int (coerce_int v1, coerce_int v2, coerce_int v3, coerce_bv v4))
+  | _ -> failwith "value set_slice_int"
+
+let value_set_slice = function
+  | [v1; v2; v3; v4; v5] ->
+     mk_vector (Sail_lib.set_slice (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_int v4, coerce_bv v5))
+  | _ -> failwith "value set_slice"
+
+let value_hex_slice = function
+  | [v1; v2; v3] ->
+     mk_vector (Sail_lib.hex_slice (coerce_string v1, coerce_int v2, coerce_int v3))
+  | _ -> failwith "value hex_slice"
+
 let value_add = function
   | [v1; v2] -> V_int (Sail_lib.add (coerce_int v1, coerce_int v2))
   | _ -> failwith "value add"
@@ -222,6 +241,46 @@ let value_sub = function
   | [v1; v2] -> V_int (Sail_lib.sub (coerce_int v1, coerce_int v2))
   | _ -> failwith "value sub"
 
+let value_mult = function
+  | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value mult"
+
+let value_quotient = function
+  | [v1; v2] -> V_int (Sail_lib.quotient (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value quotient"
+
+let value_modulus = function
+  | [v1; v2] -> V_int (Sail_lib.modulus (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value modulus"
+
+let value_add_vec_int = function
+  | [v1; v2] -> mk_vector (Sail_lib.add_vec_int (coerce_bv v1, coerce_int v2))
+  | _ -> failwith "value add_vec_int"
+
+let value_add_vec = function
+  | [v1; v2] -> mk_vector (Sail_lib.add_vec (coerce_bv v1, coerce_bv v2))
+  | _ -> failwith "value add_vec"
+
+let value_sub_vec = function
+  | [v1; v2] -> mk_vector (Sail_lib.sub_vec (coerce_bv v1, coerce_bv v2))
+  | _ -> failwith "value sub_vec"
+
+let value_shl_int = function
+  | [v1; v2] -> V_int (Sail_lib.shl_int (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value shl_int"
+
+let value_shr_int = function
+  | [v1; v2] -> V_int (Sail_lib.shr_int (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value shr_int"
+
+let value_max_int = function
+  | [v1; v2] -> V_int (Sail_lib.max_int (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value max_int"
+
+let value_min_int = function
+  | [v1; v2] -> V_int (Sail_lib.min_int (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value min_int"
+
 let value_replicate_bits = function
   | [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value replicate_bits"
@@ -230,6 +289,11 @@ let is_bit = function
   | V_bit _ -> true
   | _ -> false
 
+
+let is_ctor = function
+  | V_ctor _ -> true
+  | _ -> false
+
 let rec string_of_value = function
   | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
   | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]"
@@ -257,10 +321,28 @@ let value_print = function
   | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
   | _ -> assert false
 
+let value_internal_pick = function
+  | [v1] -> List.hd (coerce_listlike v1);
+  | _ -> failwith "value internal_pick"
+
 let value_undefined_vector = function
-  | [v1; v2; v3] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, coerce_int v2, v3))
+  | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
   | _ -> failwith "value undefined_vector"
 
+let value_read_ram = function
+  | [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4))
+  | _ -> failwith "value read_ram"
+
+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
+  | _ -> failwith "value write_ram"
+
+let value_putchar = function
+  | [v] -> Sail_lib.putchar (coerce_int v); V_unit
+  | _ -> failwith "value putchar"
+
 let primops =
   List.fold_left
     (fun r (x, y) -> StringMap.add x y r)
@@ -269,6 +351,7 @@ let primops =
       ("or_bool", or_bool);
       ("print_endline", value_print);
       ("prerr_endline", value_print);
+      ("putchar", value_putchar);
       ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
       ("print_bits", fun [msg; bits] -> print_endline (coerce_string msg ^ string_of_value bits); V_unit);
       ("eq_int", value_eq_int);
@@ -284,6 +367,7 @@ let primops =
       ("access", value_access);
       ("update", value_update);
       ("update_subrange", value_update_subrange);
+      ("slice", value_slice);
       ("append", value_append);
       ("not", value_not);
       ("not_vec", value_not_vec);
@@ -292,10 +376,28 @@ let primops =
       ("uint", value_uint);
       ("sint", value_sint);
       ("get_slice_int", value_get_slice_int);
+      ("set_slice_int", value_set_slice_int);
+      ("set_slice", value_set_slice);
+      ("hex_slice", value_hex_slice);
       ("add", value_add);
       ("sub", value_sub);
+      ("mult", value_mult);
+      ("quotient", value_quotient);
+      ("modulus", value_modulus);
+      ("shr_int", value_shr_int);
+      ("shl_int", value_shl_int);
+      ("max_int", value_max_int);
+      ("min_int", value_min_int);
+      ("add_vec_int", value_add_vec_int);
+      ("add_vec", value_add_vec);
+      ("sub_vec", value_sub_vec);
+      ("read_ram", value_read_ram);
+      ("write_ram", value_write_ram);
       ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
+      ("undefined_int", fun _ -> V_int Big_int.zero);
+      ("undefined_bool", fun _ -> V_bool false);
       ("undefined_vector", value_undefined_vector);
+      ("internal_pick", value_internal_pick);
       ("replicate_bits", value_replicate_bits);
       ("Elf_loader.elf_entry", fun _ -> V_int (Big_int.of_int 0));
     ]