Merge branch 'sail2' into cheri-mono

In order to use up-to-date sequential CHERI model for test suite

13 files changed, 273 insertions, 149 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 5cf282f9..23a8c92e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1927,7 +1927,7 @@ and compile_block ctx = function
      let setup, _, call, cleanup = compile_aexp ctx exp in
      let rest = compile_block ctx exps in
      let gs = gensym () in
-     setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup @ rest
+     iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest
 
 (** Compile a sail type definition into a IR one. Most of the
    actual work of translating the typedefs into C is done by the code
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index 89987647..02ff072b 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -65,9 +65,9 @@ let rec break n = function
   | (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs)
 
 let print_segment seg =
-  let (Byte_sequence.Sequence bs) = seg.Elf_interpreted_segment.elf64_segment_body in
+  let bs = seg.Elf_interpreted_segment.elf64_segment_body in
   prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
-  List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 bs)
+  List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs))
 
 let read name =
   let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
@@ -112,7 +112,7 @@ let write_file chan paddr i byte =
 
 let load_segment ?writer:(writer=write_sail_lib) seg =
   let open Elf_interpreted_segment in
-  let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
+  let bs = seg.elf64_segment_body in
   let paddr = seg.elf64_segment_paddr in
   let base = seg.elf64_segment_base in
   let offset = seg.elf64_segment_offset in
@@ -121,7 +121,7 @@ let load_segment ?writer:(writer=write_sail_lib) seg =
   prerr_endline ("Segment base address: " ^ Big_int.to_string base);
   prerr_endline ("Segment physical address: " ^ Big_int.to_string paddr);
   print_segment seg;
-  List.iteri (writer paddr) (List.map int_of_char bs)
+  List.iteri (writer paddr) (List.map int_of_char (Byte_sequence.char_list_of_byte_sequence bs))
 
 let load_elf ?writer:(writer=write_sail_lib) name =
   let segments, e_entry, symbol_map = read name in
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index de683047..830f2350 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -38,6 +38,12 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let and_boolM l r = l >>= (fun l -> if l then r else return false)
+
+val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let or_boolM l r = l >>= (fun l -> if l then return true else r)
+
 val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_fail = function
   | B0 -> return false
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..0c5da675 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -194,32 +194,14 @@ let neq_bv l r = not (eq_bv l r)
 
 let inline neq_mword l r = (l <> r)
 
-val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r))
-let ulteq_bv l r = (eq_bv l r) || (ult_bv l r)
-let ugt_bv l r = not (ulteq_bv l r)
-let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r)
-
-val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let slt_bv l r =
-  match (most_significant l, most_significant r) with
-    | (B0, B0) -> ult_bv l r
-    | (B0, B1) -> false
-    | (B1, B0) -> true
-    | (B1, B1) ->
-       let l' = add_one_bit_ignore_overflow (bits_of l) in
-       let r' = add_one_bit_ignore_overflow (bits_of r) in
-       ugt_bv l' r'
-    | (BU, BU) -> ult_bv l r
-    | (BU, _) -> true
-    | (_, BU) -> false
-  end
-let slteq_bv l r = (eq_bv l r) || (slt_bv l r)
-let sgt_bv l r = not (slteq_bv l r)
-let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r)
-
-val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r)
-
-val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
+val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int_bv len n lo =
+  let hi = lo + len - 1 in
+  let bs = bools_of_int (hi + 1) n in
+  of_bools (subrange_list false bs hi lo)
+
+val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+let set_slice_int_bv len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bits_of_int (hi + 1) n in
+  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index b0a29b5e..19e9b519 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -35,6 +35,9 @@ let zero_extend bits len = extz_bits len bits
 val sign_extend : list bitU -> integer -> list bitU
 let sign_extend bits len = exts_bits len bits
 
+val zeros : integer -> list bitU
+let zeros len = repeat [B0] len
+
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
@@ -289,23 +292,21 @@ let duplicate_oracle b n =
 val reverse_endianness : list bitU -> list bitU
 let reverse_endianness v = reverse_endianness_list v
 
+val get_slice_int : integer -> integer -> integer -> list bitU
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
-val ult_vec   : list bitU -> list bitU -> bool
-val slt_vec   : list bitU -> list bitU -> bool
-val ugt_vec   : list bitU -> list bitU -> bool
-val sgt_vec   : list bitU -> list bitU -> bool
-val ulteq_vec : list bitU -> list bitU -> bool
-val slteq_vec : list bitU -> list bitU -> bool
-val ugteq_vec : list bitU -> list bitU -> bool
-val sgteq_vec : list bitU -> list bitU -> bool
 let eq_vec    = eq_bv
 let neq_vec   = neq_bv
-let ult_vec   = ult_bv
-let slt_vec   = slt_bv
-let ugt_vec   = ugt_bv
-let sgt_vec   = sgt_bv
-let ulteq_vec = ulteq_bv
-let slteq_vec = slteq_bv
-let ugteq_vec = ugteq_bv
-let sgteq_vec = sgteq_bv
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8bcc0319..22d5b246 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -76,6 +76,9 @@ let zero_extend w _ = Machine_word.zeroExtend w
 val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let sign_extend w _ = Machine_word.signExtend w
 
+val zeros : forall 'a. Size 'a => integer -> mword 'a
+let zeros _ = Machine_word.wordFromNatural 0
+
 val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let vector_truncate w _ = Machine_word.zeroExtend w
 
@@ -310,23 +313,21 @@ let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
 let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
 
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 let inline eq_vec    = eq_mword
 let inline neq_vec   = neq_mword
-let inline ult_vec   = ucmp_mword (<)
-let inline slt_vec   = scmp_mword (<)
-let inline ugt_vec   = ucmp_mword (>)
-let inline sgt_vec   = scmp_mword (>)
-let inline ulteq_vec = ucmp_mword (<=)
-let inline slteq_vec = scmp_mword (<=)
-let inline ugteq_vec = ucmp_mword (>=)
-let inline sgteq_vec = scmp_mword (>=)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2d9eda9c..5c6dc593 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -414,6 +414,7 @@ let rec hexstring_of_bits bs = match bs with
      | (Just n, Just s) -> Just (n :: s)
      | _ -> Nothing
      end
+  | [] -> Just []
   | _ -> Nothing
   end
 declare {isabelle} termination_argument hexstring_of_bits = automatic
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 781bc129..89021890 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -265,3 +265,16 @@ let update_reg_field_bit regfield i reg_val bit =
   let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
+
+(* TODO Add Show typeclass for value and exception type *)
+val show_result : forall 'a 'e. result 'a 'e -> string
+let show_result = function
+  | Value _ -> "Value ()"
+  | Ex (Failure msg) -> "Failure " ^ msg
+  | Ex (Throw _) -> "Throw"
+end
+
+val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit
+let prerr_results rs =
+  let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
+  ()
diff --git a/src/latex.ml b/src/latex.ml
index 01cf55b2..0520d074 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -123,18 +123,19 @@ let commands = ref StringSet.empty
 let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l, _) as annot) =
   let labelling = match label with
     | None -> ""
-    | Some l -> Printf.sprintf "\\label{%s%s}" prefix l
+    | Some l -> Printf.sprintf "\\label{%s}" l
   in
   let cmd = !opt_prefix_latex ^ prefix ^ cmd in
-  if StringSet.mem cmd !commands then
+  let lcmd = String.lowercase cmd in  (* lowercase to avoid file names differing only by case *)
+  if StringSet.mem lcmd !commands then
     latex_command ~label:label dir (cmd ^ "v") no_loc annot
   else
     begin
-      commands := StringSet.add cmd !commands;
-      let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in
+      commands := StringSet.add lcmd !commands;
+      let oc = open_out (Filename.concat dir (cmd ^ ".tex")) in
       output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
       close_out oc;
-      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting{%s/%s_sail.tex}}" dir cmd)
+      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s.tex}}" dir cmd)
     end
 
 let latex_command_id ?prefix:(prefix="") dir id no_loc annot =
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a7da28bc..c3e96d57 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -113,10 +113,7 @@ let rec fix_id remove_tick name = match name with
 let doc_id_lem (Id_aux(i,_)) =
   match i with
   | Id i -> string (fix_id false i)
-  | DeIid x ->
-     (* add an extra space through empty to avoid a closing-comment
-      * token in case of x ending with star. *)
-     parens (separate space [colon; string x; empty])
+  | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_lem_type (Id_aux(i,_)) =
   match i with
@@ -124,10 +121,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
   | Id i -> string (fix_id false i)
-  | DeIid x ->
-     (* add an extra space through empty to avoid a closing-comment
-      * token in case of x ending with star. *)
-     parens (separate space [colon; string x; empty])
+  | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_lem_ctor (Id_aux(i,_)) =
   match i with
@@ -137,10 +131,11 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
   | Id i -> string (fix_id false (String.capitalize i))
-  | DeIid x ->
-     (* add an extra space through empty to avoid a closing-comment
-      * token in case of x ending with star. *)
-     separate space [colon; string (String.capitalize x); empty]
+  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+
+let deinfix = function
+  | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
+  | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l)
 
 let doc_var_lem kid = string (fix_id true (string_of_kid kid))
 
@@ -622,31 +617,34 @@ let doc_exp_lem, doc_let_lem =
       raise (Reporting_basic.err_unreachable l
         "E_vector_append should have been rewritten before pretty-printing")
     | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
-    | E_if(c,t,e) ->
-       let epp = if_exp ctxt false c t e in
-       if aexp_needed then parens (align epp) else epp
+    | E_if(c,t,e) -> wrap_parens (align (if_exp ctxt false c t e))
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
        raise (report l "E_for should have been rewritten before pretty-printing")
     | E_loop _ ->
        raise (report l "E_loop should have been rewritten before pretty-printing")
     | E_let(leb,e) ->
-       let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
-       if aexp_needed then parens epp else epp
+       wrap_parens (let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e)
     | E_app(f,args) ->
        begin match f with
-       (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
+       | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
+         when effectful (effect_of full_exp) ->
+          let call = doc_id_lem (append_id f "M") in
+          wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
+       (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "foreach", _) ->
           begin
             match args with
             | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
                let loopvar, body = match body with
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_id id, _), _), _), body), _) -> id, body
+                 | E_aux (E_let (LB_aux (LB_val (_, _), _),
+                   E_aux (E_let (LB_aux (LB_val (_, _), _),
+                   E_aux (E_if (_,
+                   E_aux (E_let (LB_aux (LB_val (
+                     ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _))
+                     | (P_aux (P_var (P_aux (P_id id, _), _), _))
+                     | (P_aux (P_id id, _))), _), _),
+                     body), _), _), _)), _)), _) -> id, body
                  | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
                let step = match ord_exp with
                  | E_aux (E_lit (L_aux (L_false, _)), _) ->
@@ -751,7 +749,7 @@ let doc_exp_lem, doc_let_lem =
                | _ ->
                   doc_id_lem_ctor f ^^ space ^^ 
                     parens (separate_map comma (expV false) args) in
-             if aexp_needed then parens (align epp) else epp
+             wrap_parens (align epp)
           | _ ->
              let call, is_extern = match annot with
                | Some (env, _, _) when Env.is_extern f env "lem" ->
@@ -804,8 +802,7 @@ let doc_exp_lem, doc_let_lem =
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
     | E_lit lit -> doc_lit_lem lit
-    | E_cast(typ,e) ->
-       expV aexp_needed e
+    | E_cast(typ,e) -> expV aexp_needed e
     | E_tuple exps ->
        parens (align (group (separate_map (comma ^^ break 1) expN exps)))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -815,10 +812,9 @@ let doc_exp_lem, doc_let_lem =
            (* when Env.is_record tid env -> *)
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
-       let epp = anglebars (space ^^ (align (separate_map
-                                          (semi_sp ^^ break 1)
-                                          (doc_fexp ctxt recordtyp) fexps)) ^^ space) in
-       if aexp_needed then parens epp else epp
+       wrap_parens (anglebars (space ^^ (align (separate_map
+                                        (semi_sp ^^ break 1)
+                                        (doc_fexp ctxt recordtyp) fexps)) ^^ space))
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
        let recordtyp = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
@@ -837,7 +833,7 @@ let doc_exp_lem, doc_let_lem =
        let start = match nexp_simp start with
          | Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i
          | _ -> if dir then "0" else string_of_int (List.length exps) in
-       let expspp =
+       (* let expspp =
          match exps with
          | [] -> empty
          | e :: es ->
@@ -848,7 +844,8 @@ let doc_exp_lem, doc_let_lem =
                      expN e),
                   if count = 20 then 0 else count + 1)
                 (expN e,0) es in
-            align (group expspp) in
+            align (group expspp) in *)
+       let expspp = align (group (flow_map (semi ^^ break 0) expN exps)) in
        let epp = brackets expspp in
        let (epp,aexp_needed) =
          if is_bit_typ etyp && !opt_mwords then
@@ -866,19 +863,17 @@ let doc_exp_lem, doc_let_lem =
        brackets (separate_map semi (expN) exps)
     | E_case(e,pexps) ->
        let only_integers e = expY e in
-       let epp =
-         group ((separate space [string "match"; only_integers e; string "with"]) ^/^
-                  (separate_map (break 1) (doc_case ctxt) pexps) ^/^
-                    (string "end")) in
-       if aexp_needed then parens (align epp) else align epp
+       wrap_parens
+         (group ((separate space [string "match"; only_integers e; string "with"]) ^/^
+                 (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+                 (string "end")))
     | E_try (e, pexps) ->
        if effectful (effect_of e) then
          let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in
-         let epp =
-           group ((separate space [string try_catch; expY e; string "(function "]) ^/^
-                    (separate_map (break 1) (doc_case ctxt) pexps) ^/^
-                      (string "end)")) in
-         if aexp_needed then parens (align epp) else align epp
+         wrap_parens
+           (group ((separate space [string try_catch; expY e; string "(function "]) ^/^
+                   (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+                   (string "end)")))
        else
          raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
     | E_throw e ->
@@ -887,8 +882,7 @@ let doc_exp_lem, doc_let_lem =
     | E_assert (e1,e2) ->
        align (liftR (separate space [string (appendS "assert_exp"); expY e1; expY e2]))
     | E_app_infix (e1,id,e2) ->
-       raise (Reporting_basic.err_unreachable l
-         "E_app_infix should have been rewritten before pretty-printing")
+       expV aexp_needed (E_aux (E_app (deinfix id, [e1; e2]), (l, annot)))
     | E_var(lexp, eq_exp, in_exp) ->
        raise (report l "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
@@ -913,7 +907,7 @@ let doc_exp_lem, doc_let_lem =
          in
          infix 0 1 middle (expV b e1) (expN e2)
        in
-       if aexp_needed then parens (align epp) else epp
+       wrap_parens (align epp)
     | E_internal_return (e1) ->
        wrap_parens (align (separate space [string (appendS "return"); expY e1]))
     | E_sizeof nexp ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 582901dc..b59a248e 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2581,6 +2581,14 @@ let rewrite_defs_letbind_effects =
     | E_cast (typ,exp') ->
        n_exp_name exp' (fun exp' ->
        k (rewrap (E_cast (typ,exp'))))
+    | E_app (op_bool, [l; r])
+      when string_of_id op_bool = "and_bool" || string_of_id op_bool = "or_bool" ->
+       (* Leave effectful operands of Boolean "and"/"or" in place to allow
+          short-circuiting. *)
+       let newreturn = effectful l || effectful r in
+       let l = n_exp_term newreturn l in
+       let r = n_exp_term newreturn r in
+       k (rewrap (E_app (op_bool, [l; r])))
     | E_app (id,exps) ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_app (id,exps))))
@@ -2916,20 +2924,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          |> mk_var_exps_pats pl env
        in
        let exp4 = rewrite_var_updates (add_vars overwrite exp4 vars) in
-       let ord_exp, kids, constr, lower, upper =
-         match destruct_range env (typ_of exp1), destruct_range env (typ_of exp2) with
+       let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp =
+         match destruct_numeric env (typ_of exp1), destruct_numeric env (typ_of exp2) with
            | None, _ | _, None ->
               raise (Reporting_basic.err_unreachable el "Could not determine loop bounds")
-           | Some (kids1, constr1, l1, u1), Some (kids2, constr2, l2, u2) ->
+           | Some (kids1, constr1, n1), Some (kids2, constr2, n2) ->
               let kids = kids1 @ kids2 in
               let constr = nc_and constr1 constr2 in
-              let ord_exp, lower, upper =
+              let ord_exp, lower, upper, lower_exp, upper_exp =
                 if is_order_inc order
-                then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, l1, u2)
-                else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, l2, u1)
+                then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, n1, n2, exp1, exp2)
+                else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, n2, n1, exp2, exp1)
               in
-              ord_exp, kids, constr, lower, upper
+              ord_exp, kids, constr, lower, upper, lower_exp, upper_exp
        in
+       (* Bind the loop variable in the body, annotated with constraints *)
        let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in
        let lvar_nc = nc_and constr (nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper)) in
        let lvar_typ = mk_typ (Typ_exist (lvar_kid :: kids, lvar_nc, atom_typ (nvar lvar_kid))) in
@@ -2938,7 +2947,33 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in
        let lb = fix_eff_lb (annot_letbind (lvar_pat, exp1) el env lvar_typ) in
        let body = fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) in
-       let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; body])) el env (typ_of body)) in
+       (* If lower > upper, the loop body never gets executed, and the type
+          checker might not be able to prove that the initial value exp1
+          satisfies the constraints on the loop variable.
+
+          Make this explicit by guarding the loop body with lower <= upper.
+          (for type-checking; the guard is later removed again by the Lem
+          pretty-printer).  This could be implemented with an assertion, but
+          that would force the loop to be effectful, so we use an if-expression
+          instead.  This code assumes that the loop bounds have (possibly
+          existential) atom types, and the loop body has type unit. *)
+       let lower_kid = mk_kid ("loop_" ^ string_of_id id ^ "_lower") in
+       let lower_pat = P_var (annot_pat P_wild el env (typ_of lower_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var lower_kid)]))) in
+       let lb_lower = annot_letbind (lower_pat, lower_exp) el env (typ_of lower_exp) in
+       let upper_kid = mk_kid ("loop_" ^ string_of_id id ^ "_upper") in
+       let upper_pat = P_var (annot_pat P_wild el env (typ_of upper_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var upper_kid)]))) in
+       let lb_upper = annot_letbind (upper_pat, upper_exp) el env (typ_of upper_exp) in
+       let guard = annot_exp (E_constraint (nc_lteq (nvar lower_kid) (nvar upper_kid))) el env bool_typ in
+       let unit_exp = annot_exp (E_lit (mk_lit L_unit)) el env unit_typ in
+       let skip_val = tuple_exp (if overwrite then vars else unit_exp :: vars) in
+       let guarded_body =
+         fix_eff_exp (annot_exp (E_let (lb_lower,
+           fix_eff_exp (annot_exp (E_let (lb_upper,
+             fix_eff_exp (annot_exp (E_if (guard, body, skip_val))
+               el env (typ_of exp4))))
+             el env (typ_of exp4))))
+           el env (typ_of exp4)) in
+       let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of body)) in
        Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
      | E_loop(loop,cond,body) ->
         let vars, varpats =
@@ -2967,7 +3002,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          (* after rewrite_defs_letbind_effects c has no variable updates *)
          let env = env_of_annot annot in
          let typ = typ_of e1 in
-         let eff = union_eff_exps [e1;e2] in
+         let eff = union_eff_exps [c;e1;e2] in
          let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
          Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
     | E_case (e1,ps) ->
diff --git a/src/state.ml b/src/state.ml
index 49fa5a99..5a360456 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -60,6 +60,11 @@ open Pretty_print_sail
 
 let defs_of_string = ast_of_def_string Ast_util.inc_ord
 
+let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs))
+
+let has_default_order defs =
+  List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs
+
 let find_registers defs =
   List.fold_left
     (fun acc def ->
@@ -77,18 +82,100 @@ let generate_regstate = function
   | [] -> ["type regstate = unit"]
   | registers ->
      let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in
-     let initreg (_, id) = Printf.sprintf "%s = undefined" (string_of_id id) in
-     let regstate =
-       "struct regstate = { " ^
-       (String.concat ", " (List.map reg registers)) ^
-       " }"
-     in
-     let initstate =
-       "let initial_regstate : regstate = struct { " ^
-       (String.concat ", " (List.map initreg registers)) ^
-       " }"
-     in
-     regstate :: (if !Initial_check.opt_undefined_gen then [initstate] else [])
+     ["struct regstate = { " ^ (String.concat ", " (List.map reg registers)) ^ " }"]
+
+let generate_initial_regstate defs =
+  let registers = find_registers defs in
+  if registers = [] then [] else
+  try
+    (* Recursively choose a default value for every type in the spec.
+       vals, constructed below, maps user-defined types to default values. *)
+    let rec lookup_init_val vals (Typ_aux (typ_aux, _) as typ) =
+      match typ_aux with
+      | Typ_id id ->
+         if string_of_id id = "bool" then "false" else
+         if string_of_id id = "bit" then "bitzero" else
+         if string_of_id id = "int" then "0" else
+         if string_of_id id = "nat" then "0" else
+         if string_of_id id = "real" then "0" else
+         if string_of_id id = "string" then "\"\"" else
+         if string_of_id id = "unit" then "()" else
+         Bindings.find id vals []
+      | Typ_app (id, _) when string_of_id id = "list" -> "[||]"
+      | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" ->
+         string_of_nexp nexp
+      | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" ->
+         string_of_nexp nexp
+      | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ;
+                      Typ_arg_aux (Typ_arg_typ etyp, _)])
+        when string_of_id id = "vector" ->
+         (* Output a list of initial values of the vector elements, or a
+            literal binary zero value if this is a bitvector and the
+            environment has a default indexing order (required by the
+            typechecker for binary and hex literals) *)
+         let literal_bitvec = is_bit_typ etyp && has_default_order defs in
+         let init_elem = if literal_bitvec then "0" else lookup_init_val vals etyp in
+         let rec elems len =
+           if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else
+           init_elem :: elems (Nat_big_num.pred len)
+         in
+         if literal_bitvec then "0b" ^ (String.concat "" (elems len)) else
+         "[" ^ (String.concat ", " (elems len)) ^ "]"
+      | Typ_app (id, args) -> Bindings.find id vals args
+      | Typ_tup typs ->
+         "(" ^ (String.concat ", " (List.map (lookup_init_val vals) typs)) ^ ")"
+      | Typ_exist (_, _, typ) -> lookup_init_val vals typ
+      | _ -> raise Not_found
+    in
+    (* Helper functions to instantiate type arguments *)
+    let typ_subst_targ kid (Typ_arg_aux (arg, _)) typ = match arg with
+      | Typ_arg_nexp (Nexp_aux (nexp, _)) -> typ_subst_nexp kid nexp typ
+      | Typ_arg_typ (Typ_aux (typ', _)) -> typ_subst_typ kid typ' typ
+      | Typ_arg_order (Ord_aux (ord, _)) -> typ_subst_order kid ord typ
+    in
+    let typ_subst_quant_item typ (QI_aux (qi, _)) arg = match qi with
+      | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
+         typ_subst_targ kid arg typ
+      | _ -> typ
+    in
+    let typ_subst_typquant tq args typ =
+      List.fold_left2 typ_subst_quant_item typ (quant_items tq) args
+    in
+    let add_typ_init_val vals = function
+      | TD_enum (id, _, id1 :: _, _) ->
+         (* Choose the first value of an enumeration type as default *)
+         Bindings.add id (fun _ -> string_of_id id1) vals
+      | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) ->
+         (* Choose the first variant of a union type as default *)
+         let init_val args =
+           let typ1 = typ_subst_typquant tq args typ1 in
+           string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")"
+         in
+         Bindings.add id init_val vals
+      | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (tq, typ), _)) ->
+         let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in
+         Bindings.add id init_val vals
+      | TD_record (id, _, tq, fields, _) ->
+         let init_val args =
+           let init_field (typ, id) =
+             let typ = typ_subst_typquant tq args typ in
+             string_of_id id ^ " = " ^ lookup_init_val vals typ
+           in
+           "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }"
+         in
+         Bindings.add id init_val vals
+      | TD_bitfield (id, typ, _) ->
+         Bindings.add id (fun _ -> lookup_init_val vals typ) vals
+      | _ -> vals
+    in
+    let init_vals = List.fold_left (fun vals def -> match def with
+      | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td
+      | _ -> vals) Bindings.empty defs
+    in
+    let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in
+    ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"]
+  with
+  | _ -> [] (* Do not generate an initial register state if anything goes wrong *)
 
 let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with
   | Typ_id id -> id
@@ -135,9 +222,8 @@ let generate_regval_typ typs =
   (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^
   " }"]
 
-let add_regval_conv id typ defs =
+let add_regval_conv id typ (Defs defs) =
   let id = string_of_id id in
-  let is_defined name = IdSet.mem (mk_id name) (ids_of_defs defs) in
   let typ_str = to_string (doc_typ typ) in
   (* Create a function that converts from regval to the target type. *)
   let from_name = id ^ "_of_regval" in
@@ -146,14 +232,14 @@ let add_regval_conv id typ defs =
     Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id;
     Printf.sprintf "and %s _ = None()" from_name
     ] in
-  let from_defs = if is_defined from_name then [] else [from_val; from_function] in
+  let from_defs = if is_defined defs from_name then [] else [from_val; from_function] in
   (* Create a function that converts from target type to regval. *)
   let to_name = "regval_of_" ^ id in
   let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in
   let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in
-  let to_defs = if is_defined to_name then [] else [to_val; to_function] in
+  let to_defs = if is_defined defs to_name then [] else [to_val; to_function] in
   let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in
-  append_ast defs cdefs
+  append_ast (Defs defs) cdefs
 
 let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
   | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) ->
@@ -393,17 +479,16 @@ let generate_regstate_defs mwords defs =
   let gen_undef = !Initial_check.opt_undefined_gen in
   Initial_check.opt_undefined_gen := false;
   let registers = find_registers defs in
-  let def_ids = ids_of_defs (Defs defs) in
-  let has_def name = IdSet.mem (mk_id name) def_ids in
   let regtyps = register_base_types mwords (List.map fst registers) in
   let option_typ =
-    if has_def "option" then [] else
+    if is_defined defs "option" then [] else
       ["union option ('a : Type) = {None : unit, Some : 'a}"]
   in
-  let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in
-  let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in
+  let regval_typ = if is_defined defs "register_value" then [] else generate_regval_typ regtyps in
+  let regstate_typ = if is_defined defs "regstate" then [] else generate_regstate registers in
+  let initregstate = if is_defined defs "initial_regstate" then [] else generate_initial_regstate defs in
   let defs =
-    option_typ @ regval_typ @ regstate_typ
+    option_typ @ regval_typ @ regstate_typ @ initregstate
     |> List.map defs_of_string
     |> concat_ast
     |> Bindings.fold add_regval_conv regtyps
diff --git a/src/type_check.mli b/src/type_check.mli
index ed240839..1c0e2f09 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -271,6 +271,8 @@ val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option
 
 val destruct_range : Env.t -> typ -> (kid list * n_constraint * nexp * nexp) option
 
+val destruct_numeric : Env.t -> typ -> (kid list * n_constraint * nexp) option
+
 val destruct_vector : Env.t -> typ -> (nexp * order * typ) option
 
 type uvar =
@@ -283,6 +285,9 @@ val string_of_uvar : uvar -> string
 
 val subst_unifiers : uvar KBindings.t -> typ -> typ
 
+val typ_subst_nexp : kid -> nexp_aux -> typ -> typ
+val typ_subst_typ : kid -> typ_aux -> typ -> typ
+val typ_subst_order : kid -> order_aux -> typ -> typ
 val typ_subst_kid : kid -> kid -> typ -> typ
 
 val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option