Additional tests for ocaml backend

14 files changed, 360 insertions, 22 deletions

diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index 26301d0f..e7c3614b 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -6,7 +6,7 @@
 (defconst sail2-keywords
   '("val" "function" "type" "struct" "union" "enum" "let" "var" "if" "then"
     "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect"
-    "overload" "cast" "sizeof" "constraint" "default" "assert"
+    "overload" "cast" "sizeof" "constraint" "default" "assert" "newtype"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach"))
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d7b69c4f..0cea64a1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1022,6 +1022,8 @@ let generate_undefineds vs_ids (Defs defs) =
   in
   let undefined_tu = function
     | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
+    | Tu_aux (Tu_ty_id (Typ_aux (Typ_tup typs, _), id), _) ->
+       mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
     | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
   in
   let undefined_td = function
diff --git a/src/lexer2.mll b/src/lexer2.mll
index 312183fa..e24de0d0 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -147,6 +147,7 @@ let kw_table =
      ("type",		         (fun x -> Typedef));
      ("undefined",               (fun x -> Undefined));
      ("union",			 (fun x -> Union));
+     ("newtype",                 (fun x -> Newtype));
      ("with",                    (fun x -> With));
      ("val",                     (fun x -> Val));
      ("repeat",                  (fun _ -> Repeat));
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index f753b907..89220356 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -146,6 +146,7 @@ let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "real") = 0 -> string "Num.num"
   | id when Id.compare id (mk_id "exception") = 0 -> string "exn"
   | id when Id.compare id (mk_id "register") = 0 -> string "ref"
+  | id when Id.compare id (mk_id "ref") = 0 -> string "ref"
   | id -> zencode ctx id
 
 let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
@@ -278,7 +279,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
      (string "let rec loop () =" ^//^ loop_body)
      ^/^ string "in"
      ^/^ string "loop ()"
-  | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
+  | E_lit _ | E_list _ | E_id _ | E_tuple _ | E_ref _ -> ocaml_atomic_exp ctx exp
   | E_for (id, exp_from, exp_to, exp_step, ord, exp_body) ->
      let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in
      let loop_mod =
@@ -326,6 +327,7 @@ and ocaml_fexp ctx (FE_aux (FE_Fexp (id, exp), _)) =
 and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
   match exp_aux with
   | E_lit lit -> ocaml_lit lit
+  | E_ref id -> zencode ctx id
   | E_id id ->
      begin
        match Env.lookup_id id (env_of exp) with
@@ -362,10 +364,13 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp =
           separate space [zencode ctx id; string ":="; traced_exp]
        | _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp]
      end
+  | LEXP_deref ref_exp ->
+     separate space [ocaml_atomic_exp ctx ref_exp; string ":="; ocaml_exp ctx exp]
   | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
 and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
   match lexp_aux with
   | LEXP_cast _ | LEXP_id _ -> ocaml_atomic_lexp ctx lexp
+  | LEXP_deref exp -> ocaml_exp ctx exp
   | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
 and ocaml_atomic_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
   match lexp_aux with
@@ -550,6 +555,9 @@ let ocaml_string_of_abbrev ctx id typq typ =
   separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ zencode ctx id); equals]
   ^//^ ocaml_string_typ typ arg
 
+let ocaml_string_of_variant ctx id typq cases =
+  separate space [string "let"; ocaml_string_of id; string "_"; equals; string "\"VARIANT\""]
+
 let ocaml_typedef ctx (TD_aux (td_aux, _)) =
   match td_aux with
   | TD_record (id, _, typq, fields, _) ->
@@ -561,8 +569,10 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
   | TD_variant (id, _, _, cases, _) when string_of_id id = "exception" ->
      ocaml_exceptions ctx cases
   | TD_variant (id, _, typq, cases, _) ->
-     separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
-     ^//^ ocaml_cases ctx cases
+     (separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
+      ^//^ ocaml_cases ctx cases)
+     ^^ ocaml_def_end
+     ^^ ocaml_string_of_variant ctx id typq cases
   | TD_enum (id, _, ids, _) ->
      (separate space [string "type"; zencode ctx id; equals]
       ^//^ (bar ^^ space ^^ ocaml_enum ctx ids))
diff --git a/src/parser2.mly b/src/parser2.mly
index 34ab8732..521da6f8 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -154,7 +154,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch Exit
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Record Mutual Var Ref
 
@@ -962,8 +962,12 @@ atomic_exp:
     { mk_exp (E_cast ($3, $1)) $startpos $endpos }
   | lit
     { mk_exp (E_lit $1) $startpos $endpos }
+  | id MinusGt id Unit
+    { mk_exp (E_app (prepend_id "_mod_" $3, [mk_exp (E_ref $1) $startpos($1) $endpos($1)])) $startpos $endpos }
   | id MinusGt id Lparen exp_list Rparen
     { mk_exp (E_app (prepend_id "_mod_" $3, mk_exp (E_ref $1) $startpos($1) $endpos($1) :: $5)) $startpos $endpos }
+  | atomic_exp Dot id Unit
+    { mk_exp (E_app (prepend_id "_mod_" $3, [$1])) $startpos $endpos }
   | atomic_exp Dot id Lparen exp_list Rparen
     { mk_exp (E_app (prepend_id "_mod_" $3, $1 :: $5)) $startpos $endpos }
   | atomic_exp Dot id
@@ -1054,6 +1058,10 @@ type_def:
     { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
   | Enum id Eq Lcurly enum Rcurly
     { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+  | Newtype id Eq type_union
+    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
+  | Newtype id typquant Eq type_union
+    { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos }
   | Union id Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typquant Eq Lcurly type_unions Rcurly
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 87baa746..9b97b88b 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1354,7 +1354,7 @@ let id_is_unbound id env = match Env.lookup_id id env with
   | _ -> false
 
 let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
-  | LEXP_memory _ -> false
+  | LEXP_memory _ | LEXP_deref _ -> false
   | LEXP_id id
   | LEXP_cast (_, id) -> id_is_local_var id env
   | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
@@ -1363,7 +1363,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_field (lexp,_) -> lexp_is_local lexp env
 
 let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
-  | LEXP_memory _ -> false
+  | LEXP_memory _ | LEXP_deref _ -> false
   | LEXP_id id
   | LEXP_cast (_, id) -> id_is_unbound id env
   | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
@@ -1378,7 +1378,7 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
 let rec rewrite_lexp_to_rhs (do_rewrite : tannot lexp -> bool) ((LEXP_aux(lexp,((l,_) as annot))) as le) =
   if do_rewrite le then
     match lexp with
-    | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp))
+    | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ | LEXP_deref _ -> (le, (fun exp -> exp))
     | LEXP_vector (lexp, e) ->
        let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in
        (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot))))
diff --git a/src/type_check.ml b/src/type_check.ml
index d3967e7d..0c1d55ce 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -450,7 +450,8 @@ end = struct
 
   let add_overloads id ids env =
     typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]");
-    { env with overloads = Bindings.add id ids env.overloads }
+    let existing = try Bindings.find id env.overloads with Not_found -> [] in
+    { env with overloads = Bindings.add id (existing @ ids) env.overloads }
 
   let add_smt_op id str env =
     typ_print ("Adding smt binding " ^ string_of_id id ^ " to " ^ str);
@@ -2496,6 +2497,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
         subtyp l env typ vtyp; annot_lexp (LEXP_deref inferred_exp) typ, env
      | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" ->
         subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
+     | _ ->
+        typ_error l (string_of_typ typ  ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")")
      end
   | LEXP_id v ->
      begin match Env.lookup_id v env with
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index b56ce7e2..9bdfdc33 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-type bits ('n : Int) = vector('n - 1, 'n, dec, bit)
+type bits ('n : Int) = vector('n, dec, bit)
 
 infix 4 ==
 
@@ -20,7 +20,7 @@ val eq_real = "eq_real" : (real, real) -> bool
 
 val eq_anything = "(fun (x, y) -> x = y)" : forall ('a : Type). ('a, 'a) -> bool
 
-val length = "length" : forall 'n ('a : Type). vector('n - 1, 'n, dec, 'a) -> atom('n)
+val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
 
 overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything}
 
@@ -33,24 +33,24 @@ val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int).
 overload vector_subrange = {vector_subrange_A, vector_subrange_B}
 
 val vector_access_A = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
-  (vector('n - 1, 'n, dec, 'a), atom('m)) -> 'a
+  (vector('n, dec, 'a), atom('m)) -> 'a
 
 val vector_access_B = "access" : forall ('n : Int) ('a : Type).
-  (vector('n - 1, 'n, dec, 'a), int) -> 'a
+  (vector('n, dec, 'a), int) -> 'a
 
 overload vector_access = {vector_access_A, vector_access_B}
 
 val vector_update = "update" : forall 'n ('a : Type).
-  (vector('n - 1, 'n, dec, 'a), int, 'a) -> vector('n - 1, 'n, dec, 'a)
+  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
 
 val vector_update_subrange = "update_subrange" : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 val vcons : forall ('n : Int) ('a : Type).
-  ('a, vector('n - 1, 'n, dec, 'a)) -> vector('n, 'n + 1, dec, 'a)
+  ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
 
 val append = "append" : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n - 1, 'n, dec, 'a), vector('m - 1, 'm, dec, 'a)) -> vector('n + 'm - 1, 'n + 'm, dec, 'a)
+  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
 
 val not_bool = "not" : bool -> bool
 
diff --git a/test/ocaml/reg_alias/expect b/test/ocaml/reg_alias/expect
new file mode 100644
index 00000000..21493790
--- /dev/null
+++ b/test/ocaml/reg_alias/expect
@@ -0,0 +1,7 @@
+CR = 0x00
+CR = 0xCA
+CR.CR0 = 0xC
+CR.CR1 = 0b10
+CR.CR2 = 0b10
+CR = 0xFA
+CR = 0xF8
diff --git a/test/ocaml/reg_alias/ra.sail b/test/ocaml/reg_alias/ra.sail
new file mode 100644
index 00000000..f4e6d529
--- /dev/null
+++ b/test/ocaml/reg_alias/ra.sail
@@ -0,0 +1,79 @@
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+struct cr = {
+  CR0 : bits(4),
+  CR1 : bits(2),
+  CR2 : bits(2)
+}
+
+val _set_CR0 : (register(cr), bits(4)) -> unit effect {wreg}
+val _get_CR0 : register(cr) -> bits(4) effect {rreg}
+
+val _set_CR1 : (register(cr), bits(2)) -> unit effect {wreg}
+val _get_CR1 : register(cr) -> bits(2) effect {rreg}
+
+val _set_CR2 : (register(cr), bits(2)) -> unit effect {wreg}
+val _get_CR2 : register(cr) -> bits(2) effect {rreg}
+
+function _set_CR0 (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR0 = v;
+  (*cr_ref) = cr;
+}
+function _get_CR0 cr = reg_deref(cr).CR0
+
+function _set_CR1 (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR1 = v;
+  (*cr_ref) = cr;
+}
+function _get_CR1 cr = reg_deref(cr).CR1
+
+function _set_CR2 (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR2 = v;
+  (*cr_ref) = cr;
+}
+function _get_CR2 cr = reg_deref(cr).CR2
+
+overload _mod_CR0 = {_set_CR0, _get_CR0}
+overload _mod_CR1 = {_set_CR1, _get_CR1}
+overload _mod_CR2 = {_set_CR2, _get_CR2}
+
+val _get_cr : register(cr) -> bits(8) effect {rreg}
+
+function _get_cr cr_ref =
+  let cr = reg_deref(cr_ref) in cr.CR0 @ cr.CR1 @ cr.CR2
+
+val _set_cr : (register(cr), bits(8)) -> unit effect {wreg}
+
+function _set_cr (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR0 = v[7 .. 4];
+  cr.CR1 = v[3 .. 2];
+  cr.CR2 = v[1 .. 0];
+  (*cr_ref) = cr
+}
+
+overload _mod_cr = {_set_cr, _get_cr}
+
+register CR : cr
+
+val main : unit -> unit effect {wreg, rreg}
+
+function main () = {
+  CR->cr() = 0x00;
+  print_bits("CR = ", CR->cr());
+  CR->cr() = 0xCA;
+  print_bits("CR = ", CR->cr());
+  print_bits("CR.CR0 = ", CR->CR0());
+  print_bits("CR.CR1 = ", CR->CR1());
+  print_bits("CR.CR2 = ", CR->CR2());
+  CR->CR0() = 0xF;
+  print_bits("CR = ", CR->cr());
+  CR->CR2() = 0b00;
+  print_bits("CR = ", CR->cr());
+  ()
+}
\ No newline at end of file
diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail
index 94acdf7e..d84f98e0 100644
--- a/test/ocaml/reg_passing/reg_passing.sail
+++ b/test/ocaml/reg_passing/reg_passing.sail
@@ -17,8 +17,8 @@ function f R = {
 val g : unit -> unit effect {rreg, wreg}
 
 function g () = {
-  f(R1);
-  f(R2);
+  f(ref R1);
+  f(ref R2);
 }
 
 val main : unit -> unit effect {rreg, wreg}
@@ -28,7 +28,7 @@ function main () = {
   R2 = 5;
   g ();
   R3 = 10;
-  f(R3);
+  f(ref R3);
   R2 = 20;
   output("R1 = ", R1);
   output("R2 = ", R2);
diff --git a/test/ocaml/reg_ref/expect b/test/ocaml/reg_ref/expect
new file mode 100644
index 00000000..904fc765
--- /dev/null
+++ b/test/ocaml/reg_ref/expect
@@ -0,0 +1,51 @@
+Testing register references
+Register 1
+Assigning 0x00000000
+Register 2
+Assigning 0x00000000
+Register 3
+Assigning 0x00000000
+1 = 0x00000000
+2 = 0x00000000
+3 = 0x00000000
+Register 1
+Assigning 0xCAFEBEEF
+1 = 0xCAFEBEEF
+2 = 0x00000000
+3 = 0x00000000
+Reading 1 to variable
+v = 0xCAFEBEEF
+Register 3
+Assigning 0x00BEEF00
+1 = 0xCAFEBEEF
+2 = 0x00000000
+3 = 0x00BEEF00
+Reading zero register
+0 = 0x00000000
+Register 2
+Assigning 0xDEADCAFE
+2 = 0xDEADCAFE
+Assigning register 2 to register 1
+Register 2
+Assigning 0xCAFEBEEF
+1 = 0xCAFEBEEF
+2 = 0xCAFEBEEF
+3 = 0x00BEEF00
+
+Testing slicing
+s = 0b111
+s = 0b01110
+s = 0xE
+b = 0b01110
+b = 0b01010
+b = 0b01111
+
+Testing bit aliasing
+CR0 = 0x0
+LT = 0b0
+Setting LT to bitone
+CR0 = 0x8
+LT = 0b1
+Setting CR0 to 0b0111
+CR0 = 0x7
+LT = 0b0
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
new file mode 100644
index 00000000..3c11dcb8
--- /dev/null
+++ b/test/ocaml/reg_ref/rr.sail
@@ -0,0 +1,177 @@
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val deref = "reg_deref" : forall ('a : Type). ref('a) -> 'a
+
+/* *** Register reference list example *** */
+
+type regno ('n : Int), 0 <= 'n < 4 = atom('n)
+
+/* regiser x0 : bits(32) is always 0 */
+register x1 : bits(32)
+register x2 : bits(32)
+register x3 : bits(32)
+
+let GPRs : vector(3, dec, register(bits(32))) =
+  [ ref x3, ref x2, ref x1 ]
+
+val rGPR : forall 'n, 0 <= 'n < 4. regno('n) -> bits(32) effect {rreg}
+
+function rGPR 0 = 0x00000000
+and rGPR (r if r > 0) = reg_deref(GPRs[r - 1])
+
+val wGPR : forall 'n, 1 <= 'n < 4. (regno('n), bits(32)) -> unit effect {wreg}
+
+function wGPR (r, v) = {
+  print_int("Register ", r);
+  print_bits("Assigning ", v);
+  (*GPRs[r - 1]) = v
+}
+
+overload _mod_GPR = { rGPR, wGPR }
+
+/* *** Power style vector slicing *** */
+
+/* Create a new type which is a pair of a bitvector and a start index
+
+   slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
+newtype slice ('n : Int) ('m : Int) = MkSlice : (atom('n), bits('m))
+
+/* Extract the bitvector from a slice */
+val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
+
+function slice_bits MkSlice(_, xs) = xs
+
+/* Take a slice from a bitvector */
+val vector_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+  (bits('n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
+
+function vector_slice (v, to, from) = MkSlice(from, v[to .. from])
+
+val slice_slice : forall 'n 'm 'o 'p.
+  (slice('p, 'n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
+
+function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
+
+/* We can update a bitvector from another bitvector or a slice */
+val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+  (ref(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit
+
+function _set_slice (v, stop, start, update) = {
+  v2 = deref(v);
+  v2[stop .. start] = update;
+  (*v) = v2;
+}
+
+val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o <= 'n.
+  (ref(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit
+
+function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update)
+
+val slice_bit : forall 'n. slice('n, 1) -> bit
+
+function slice_bit MkSlice(_, [b]) = b
+
+/* Overload slice modifier */
+overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice}
+
+/* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */
+infix 1 ...
+
+type operator ... ('n : Int) ('m : Int) = slice('m, 'n - ('m - 1))
+
+struct cr = {
+  CR0 : 7 ... 4,
+  /* 7 : LT; 6 : GT; 5 : EQ; 4 : SO; */
+  CR1 : 3 ... 2,
+  CR3 : 1 ... 0,
+}
+
+register CR : cr
+
+val _get_LT : cr -> bit
+val _set_LT : (register(cr), bit) -> unit effect {rreg, wreg}
+
+function _get_LT cr = slice_bit(cr.CR0.slice(7, 7))
+function _set_LT (cr_ref, b) = {
+  cr = reg_deref(cr_ref);
+  cr.CR0 = MkSlice(4, [slice_bits(cr.CR0) with (7 - 4) = b]);
+  (*cr_ref) = cr;
+}
+
+overload _mod_LT = {_get_LT, _set_LT}
+
+/* *** Test Program *** */
+
+val main : unit -> unit effect {wreg, rreg}
+
+val print_regs : unit -> unit effect {rreg}
+
+function print_regs () = {
+  print_bits("1 = ", rGPR(1));
+  print_bits("2 = ", rGPR(2));
+  print_bits("3 = ", rGPR(3));
+}
+
+function main () = {
+  print("Testing register references");
+  wGPR(1) = 0x00000000;
+  wGPR(2) = 0x00000000;
+  wGPR(3) = 0x00000000;
+
+  print_regs ();
+
+  /* Assign to lowest assignable register */
+  wGPR(1) = 0xCAFEBEEF;
+  print_regs ();
+
+  /* Reading to variable */
+  print("Reading 1 to variable");
+  v = rGPR(1);
+  print_bits("v = ", v);
+
+  /* Assign to highest register */
+  wGPR(3) = 0x00BEEF00;
+  print_regs ();
+
+  print("Reading zero register");
+  print_bits("0 = ", rGPR(0));
+
+  /* Test overloaded version */
+  _mod_GPR(2) = 0xDEADCAFE;
+  print_bits("2 = ", _mod_GPR(2));
+
+  /* Method syntax */
+  print("Assigning register 2 to register 1");
+  2.GPR() = 1.GPR();
+  print_regs();
+
+  /* Slice testing */
+  print("\nTesting slicing");
+  let s = 0b01110.slice(3, 1);
+  print_bits("s = ", slice_bits(s));
+  let s = 0b01110.slice(4, 0);
+  print_bits("s = ", slice_bits(s));
+  let s = 0b01110.slice(3, 0);
+  print_bits("s = ", slice_bits(s));
+
+  /* Updating slices */
+  b = 0b01110;
+  print_bits("b = ", b);
+  b->slice(3, 1) = 0b101;
+  print_bits("b = ", b);
+  b->slice(2, 0) = 0xFF.slice(5, 3);
+  print_bits("b = ", b);
+
+  /* Bit aliasing */
+  print("\nTesting bit aliasing");
+  print_bits("CR0 = ", slice_bits(CR.CR0));
+  print_bits("LT = ", [CR.LT()]);
+  print("Setting LT to bitone");
+  CR->LT() = bitone;
+  print_bits("CR0 = ", slice_bits(CR.CR0));
+  print_bits("LT = ", [CR.LT()]);
+  print("Setting CR0 to 0b0111");
+  CR.CR0 = MkSlice(4, 0b0111);
+  print_bits("CR0 = ", slice_bits(CR.CR0));
+  print_bits("LT = ", [CR.LT()]);
+}
diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail
index eb518515..60fa0e46 100644
--- a/test/ocaml/vec_32_64/vec_32_64.sail
+++ b/test/ocaml/vec_32_64/vec_32_64.sail
@@ -1,6 +1,6 @@
-(* This example is more testing the typechecker flow typing rather
+/* This example is more testing the typechecker flow typing rather
 than the ocaml backend, but it does test that recursive functions work
-correctly *)
+correctly */
 
 val get_size : unit -> {|32, 64|}
 
@@ -8,7 +8,7 @@ function get_size () = 32
 
 val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit
 
-val zeros : forall 'n. atom('n) -> vector('n - 1, 'n, dec, bit)
+val zeros : forall 'n. atom('n) -> vector('n, dec, bit)
 
 function zeros n =
   if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1)