Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

9 files changed, 192 insertions, 106 deletions

diff --git a/src/graph.ml b/src/graph.ml
index 62da3292..17638e8b 100644
--- a/src/graph.ml
+++ b/src/graph.ml
@@ -89,6 +89,11 @@ module type S =
        not directed acyclic. *)
     val topsort : graph -> node list
 
+    (** Find strongly connected components using Tarjan's algorithm.
+        This algorithm also returns a topological sorting of the graph
+        components. *)
+    val scc : ?original_order:(node list) -> graph -> node list list
+
     val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit
   end
 
@@ -213,6 +218,63 @@ module Make(Ord: OrderedType) = struct
 
     in topsort' (); !list
 
+  type node_idx = { index : int; root : int }
+
+  let scc ?(original_order : node list option) (cg : graph) =
+    let components = ref [] in
+    let index = ref 0 in
+
+    let stack = ref [] in
+    let push v = (stack := v :: !stack) in
+    let pop () =
+      begin
+        let v = List.hd !stack in
+        stack := List.tl !stack;
+        v
+      end
+    in
+
+    let node_indices = Hashtbl.create (NM.cardinal cg) in
+    let get_index v = (Hashtbl.find node_indices v).index in
+    let get_root v = (Hashtbl.find node_indices v).root in
+    let set_root v r =
+      Hashtbl.replace node_indices v { (Hashtbl.find node_indices v) with root = r } in
+
+    let rec visit_node v =
+      begin
+        Hashtbl.add node_indices v { index = !index; root = !index };
+        index := !index + 1;
+        push v;
+        if NM.mem v cg then NS.iter (visit_edge v) (NM.find v cg);
+        if get_root v = get_index v then (* v is the root of a SCC *)
+          begin
+            let component = ref [] in
+            let finished = ref false in
+            while not !finished do
+              let w = pop () in
+              component := w :: !component;
+              if Ord.compare v w = 0 then finished := true;
+            done;
+            components := !component :: !components;
+          end
+      end
+    and visit_edge v w =
+      if not (Hashtbl.mem node_indices w) then
+        begin
+          visit_node w;
+          if Hashtbl.mem node_indices w then set_root v (min (get_root v) (get_root w));
+        end else begin
+          if List.mem w !stack then set_root v (min (get_root v) (get_index w))
+        end
+    in
+
+    let nodes = match original_order with
+      | Some nodes -> nodes
+      | None -> List.map fst (NM.bindings cg)
+    in
+    List.iter (fun v -> if not (Hashtbl.mem node_indices v) then visit_node v) nodes;
+    List.rev !components
+
   let make_dot node_color edge_color string_of_node out_chan graph =
     Util.opt_colors := false;
     let to_string node = String.escaped (string_of_node node) in
diff --git a/src/graph.mli b/src/graph.mli
index 09b78304..cb29daae 100644
--- a/src/graph.mli
+++ b/src/graph.mli
@@ -91,6 +91,11 @@ module type S =
        not directed acyclic. *)
     val topsort : graph -> node list
 
+    (** Find strongly connected components using Tarjan's algorithm.
+        This algorithm also returns a topological sorting of the graph
+        components. *)
+    val scc : ?original_order:(node list) -> graph -> node list list
+
     val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit
   end
 
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 2b144d35..2b2234b5 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1481,6 +1481,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)"
        | "undefined_bit", _ -> "UNDEFINED(fbits)"
        | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
+       | "undefined_list", _ -> Printf.sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp)
        | fname, _ -> fname
      in
      if fname = "reg_deref" then
@@ -1844,6 +1845,9 @@ let codegen_list_clear id ctyp =
   ^^ string "  sail_free(*rop);"
   ^^ string "}"
 
+let codegen_list_recreate id =
+  string (Printf.sprintf "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id))
+
 let codegen_list_set id ctyp =
   string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
   ^^ string "  if (op == NULL) { *rop = NULL; return; };\n"
@@ -1879,6 +1883,20 @@ let codegen_pick id ctyp =
   else
     string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
 
+let codegen_list_equal id ctyp =
+  let open Printf in
+  ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+  ^^ ksprintf string "  if (op1 == NULL && op2 == NULL) { return true; };\n"
+  ^^ ksprintf string "  if (op1 == NULL || op2 == NULL) { return false; };\n"
+  ^^ ksprintf string "  return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id)
+  ^^ string "}"
+
+let codegen_list_undefined id ctyp =
+  let open Printf in
+  ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)
+  ^^ ksprintf string "  *rop = NULL;\n"
+  ^^ string "}"
+
 let codegen_list ctx ctyp =
   let id = mk_id (string_of_ctyp (CT_list ctyp)) in
   if IdSet.mem id !generated then
@@ -1889,9 +1907,12 @@ let codegen_list ctx ctyp =
       codegen_node id ctyp ^^ twice hardline
       ^^ codegen_list_init id ^^ twice hardline
       ^^ codegen_list_clear id ctyp ^^ twice hardline
+      ^^ codegen_list_recreate id ^^ twice hardline
       ^^ codegen_list_set id ctyp ^^ twice hardline
       ^^ codegen_cons id ctyp ^^ twice hardline
       ^^ codegen_pick id ctyp ^^ twice hardline
+      ^^ codegen_list_equal id ctyp ^^ twice hardline
+      ^^ codegen_list_undefined id ctyp ^^ twice hardline
     end
 
 (* Generate functions for working with non-bit vectors of some specific type. *)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 81b876a4..c4e8576c 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -283,8 +283,14 @@ let smt_conversion ctx from_ctyp to_ctyp x =
      force_size ctx ctx.lint_size sz x
   | CT_lint, CT_fint sz ->
      force_size ctx sz ctx.lint_size x
+  | CT_lint, CT_fbits (n, _) ->
+     force_size ctx n ctx.lint_size x
+  | CT_lint, CT_lbits _ ->
+     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int ctx.lint_size); force_size ctx (lbits_size ctx) ctx.lint_size x])
   | CT_lbits _, CT_fbits (n, _) ->
      unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
+  | CT_fbits (n, _), CT_fbits (m, _) ->
+     unsigned_size ctx m n x
   | CT_fbits (n, _), CT_lbits _ ->
      Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); unsigned_size ctx (lbits_size ctx) n x])
 
@@ -580,6 +586,8 @@ let bvmask ctx len =
   let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
   bvnot (bvshl all_ones shift)
 
+let fbits_mask ctx n len = bvnot (bvshl (bvones n) len)
+
 let builtin_eq_bits ctx v1 v2 =
   match cval_ctyp v1, cval_ctyp v2 with
   | CT_fbits (n, _), CT_fbits (m, _) ->
@@ -796,9 +804,17 @@ let builtin_vector_subrange ctx vec i j ret_ctyp =
      Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec]))
 
   | CT_fbits (n, _), i_ctyp, CT_constant j, CT_lbits _ when Big_int.equal j Big_int.zero ->
-     let len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
+     let i' = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
+     let len = bvadd i' (bvint ctx.lbits_index (Big_int.of_int 1)) in
      Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx vec)])])
 
+  | CT_fbits (n, b), i_ctyp, j_ctyp, ret_ctyp ->
+     let i' = force_size ctx n (int_size ctx i_ctyp) (smt_cval ctx i) in
+     let j' = force_size ctx n (int_size ctx j_ctyp) (smt_cval ctx j) in
+     let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in
+     let vec' = bvand (bvlshr (smt_cval ctx vec) j') (fbits_mask ctx n len) in
+     smt_conversion ctx (CT_fbits (n, b)) ret_ctyp vec'
+
   | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp)
 
 let builtin_vector_access ctx vec i ret_ctyp =
@@ -844,17 +860,31 @@ let builtin_vector_update ctx vec i x ret_ctyp =
 
 let builtin_vector_update_subrange ctx vec i j x ret_ctyp =
   match cval_ctyp vec, cval_ctyp i, cval_ctyp j, cval_ctyp x, ret_ctyp with
-  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j >= 0 ->
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j > 0 ->
      assert (n = m);
      let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
      let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
      Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])])
 
-  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j >= 0 ->
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j > 0 ->
      assert (n = m);
      let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
      Fn ("concat", [smt_cval ctx x; bot])
 
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j = 0 ->
+     assert (n = m);
+     let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
+     Fn ("concat", [top; smt_cval ctx x])
+
+  | CT_fbits (n, b), ctyp_i, ctyp_j, ctyp_x, CT_fbits (m, _) ->
+     assert (n = m);
+     let i' = force_size ctx n (int_size ctx ctyp_i) (smt_cval ctx i) in
+     let j' = force_size ctx n (int_size ctx ctyp_j) (smt_cval ctx j) in
+     let x' = smt_conversion ctx ctyp_x (CT_fbits (n, b)) (smt_cval ctx x) in
+     let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in
+     let mask = bvshl (fbits_mask ctx n len) j' in
+     bvor (bvand (smt_cval ctx vec) (bvnot mask)) (bvand (bvshl x' j') mask)
+
   | _ -> builtin_type_error ctx "vector_update_subrange" [vec; i; j; x] (Some ret_ctyp)
 
 let builtin_unsigned ctx v ret_ctyp =
@@ -873,6 +903,10 @@ let builtin_unsigned ctx v ret_ctyp =
   | CT_lbits _, CT_lint ->
      Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v]))
 
+  | CT_lbits _, CT_fint m ->
+     let smt = Fn ("contents", [smt_cval ctx v]) in
+     force_size ctx m (lbits_size ctx) smt
+
   | ctyp, _ -> builtin_type_error ctx "unsigned" [v] (Some ret_ctyp)
 
 let builtin_signed ctx v ret_ctyp =
@@ -1021,6 +1055,13 @@ let builtin_get_slice_int ctx v1 v2 v3 ret_ctyp =
      let contents = unsigned_size ~checked:false ctx (lbits_size ctx) ctx.lint_size (smt_cval ctx v2) in
      Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])])
 
+  | CT_lint, ctyp2, ctyp3, ret_ctyp ->
+     let len = Extract (ctx.lbits_index - 1, 0, smt_cval ctx v1) in
+     let smt2 = force_size ctx (lbits_size ctx) (int_size ctx ctyp2) (smt_cval ctx v2) in
+     let smt3 = force_size ctx (lbits_size ctx) (int_size ctx ctyp3) (smt_cval ctx v3) in
+     let result = bvand (bvmask ctx len) (bvlshr smt2 smt3) in
+     smt_conversion ctx CT_lint ret_ctyp result
+
   | _ -> builtin_type_error ctx "get_slice_int" [v1; v2; v3] (Some ret_ctyp)
 
 let builtin_count_leading_zeros ctx v ret_ctyp =
diff --git a/src/nl_flow.ml b/src/nl_flow.ml
index 6196f23b..24ef73fa 100644
--- a/src/nl_flow.ml
+++ b/src/nl_flow.ml
@@ -60,6 +60,13 @@ let rec escapes (E_aux (aux, _)) =
   | E_block exps -> escapes (List.hd (List.rev exps))
   | _ -> false
 
+let rec returns (E_aux (aux, _)) =
+  match aux with
+  | E_return _ -> true
+  | E_block [] -> false
+  | E_block exps -> returns (List.hd (List.rev exps))
+  | _ -> false
+
 let is_bitvector_literal (L_aux (aux, _)) =
   match aux with
   | L_bin _ | L_hex _ -> true
@@ -112,6 +119,12 @@ let analyze' exps =
         List.map (modify_unsigned id value) exps
      | _ -> exps
      end
+  | (E_aux (E_if (cond, then_exp, _), (l, _)) as exp) :: next :: rest
+    when returns then_exp ->
+     let msg = mk_lit_exp (L_string "") in
+     let not_cond = locate (fun _ -> gen_loc l) (mk_exp (E_app (mk_id "not_bool", [cond]))) in
+     let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (not_cond, msg))) in
+     exp :: assertion :: next :: rest
   | _ -> exps
 
 let analyze exps =
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 03994657..90fc8aba 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -114,6 +114,8 @@ let rec undefined_vector (len, item) =
   then []
   else item :: undefined_vector (Big_int.sub len (Big_int.of_int 1), item)
 
+let undefined_list _ = []
+
 let rec undefined_bitvector len =
   if Big_int.equal len Big_int.zero
   then []
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 75f2ff6e..4814554b 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -72,7 +72,7 @@ let conditional_add typ_or_exp bound used id =
     if typ_or_exp (*true for typ*)
     then ["bit";"vector";"unit";"string";"int";"bool"]
     else ["=="; "!="; "|";"~";"&";"add_int"] in
-  let i = (string_of_id id) in
+  let i = (string_of_id (if typ_or_exp then prepend_id "typ:" id else id)) in
   if Nameset.mem i bound || List.mem i known_list
   then used
   else Nameset.add i used
@@ -106,12 +106,6 @@ and free_type_names_t_args consider_var targs =
   nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs)
 
 
-let rec free_type_names_tannot consider_var tannot =
-  match Type_check.destruct_tannot tannot with
-  | None -> mt
-  | Some (_, t, _) -> free_type_names_t consider_var t
-
-
 let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
   match t with
   | Typ_var (Kid_aux (Var v,l)) ->
@@ -131,6 +125,11 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
        used t'
   | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
 
+and fv_of_tannot consider_var bound used tannot =
+  match Type_check.destruct_tannot tannot with
+  | None -> mt
+  | Some (_, t, _) -> fv_of_typ consider_var bound used t
+
 and fv_of_targ consider_var bound used (Ast.A_aux(targ,_)) : Nameset.t = match targ with
   | A_typ t -> fv_of_typ consider_var bound used t
   | A_nexp n -> fv_of_nexp consider_var bound used n
@@ -167,13 +166,13 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
   | P_as(p,id) -> let b,ns = pat_bindings consider_var bound used p in
     Nameset.add (string_of_id id) b,ns
   | P_typ(t,p) ->
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      let ns = fv_of_typ consider_var bound used t in pat_bindings consider_var bound ns p
   | P_id id ->
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      Nameset.add (string_of_id id) bound,used
   | P_app(id,pats) ->
-    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
     list_fv bound (Nameset.add (string_of_id id) used) pats
   | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
   | _ -> bound,used
@@ -185,7 +184,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
     list_fv bound used set es
   | E_id id | E_ref id ->
      let used = conditional_add_exp bound used id in
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      bound,used,set
   | E_cast (t,e) ->
     let u = fv_of_typ consider_var (if consider_var then bound else mt) used t in
@@ -211,7 +210,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
   | E_vector_update_subrange(v,i1,i2,e) -> list_fv bound used set [v;i1;i2;e]
   | E_vector_append(e1,e2) | E_cons(e1,e2) -> list_fv bound used set [e1;e2]
   | E_record fexps ->
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      List.fold_right
        (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (bound,used,set)
   | E_record_update(e, fexps) ->
@@ -260,7 +259,7 @@ and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
 and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
   match lexp with
   | LEXP_id id ->
-    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+    let used = fv_of_tannot consider_var bound used tannot in
     let i = string_of_id id in
     if Nameset.mem i bound
     then bound, used, Nameset.add i set
@@ -268,7 +267,7 @@ and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
   | LEXP_deref exp ->
     fv_of_exp consider_var bound used set exp
   | LEXP_cast(typ,id) ->
-    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+    let used = fv_of_tannot consider_var bound used tannot in
     let i = string_of_id id in
     let used_t = fv_of_typ consider_var bound used typ in
     if Nameset.mem i bound
@@ -311,18 +310,18 @@ let fv_of_abbrev consider_var bound used typq typ_arg =
 
 let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
   | TD_abbrev(id,typq,typ_arg) ->
-     init_env (string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
+     init_env ("typ:" ^ string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
   | TD_record(id,typq,tids,_) ->
-    let binds = init_env (string_of_id id) in
+    let binds = init_env ("typ:" ^ string_of_id id) in
     let bounds = if consider_var then typq_bindings typq else mt in
     binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
   | TD_variant(id,typq,tunions,_) ->
-    let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
+    let bindings = Nameset.add ("typ:" ^ string_of_id id) (if consider_var then typq_bindings typq else mt) in
     typ_variants consider_var bindings tunions
   | TD_enum(id,ids,_) ->
-    Nameset.of_list (List.map string_of_id (id::ids)),mt
+    Nameset.of_list (("typ:" ^ string_of_id id) :: List.map string_of_id ids),mt
   | TD_bitfield(id,typ,_) ->
-    init_env (string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
+    init_env ("typ:" ^ string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
 
 let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) =
   match t with
@@ -521,68 +520,9 @@ let group_defs consider_scatter_as_one (Ast.Defs defs) =
  *)
 
 module Namemap = Map.Make(String)
-(* Nodes are labeled with strings.  A graph is represented as a map associating
-   each node with its sucessors *)
-type graph = Nameset.t Namemap.t
+module NameGraph = Graph.Make(String)
 type node_idx = { index : int; root : int }
 
-(* Find strongly connected components using Tarjan's algorithm.
-   This algorithm also returns a topological sorting of the graph components. *)
-let scc ?(original_order : string list option) (g : graph) =
-  let components = ref [] in
-  let index = ref 0 in
-
-  let stack = ref [] in
-  let push v = (stack := v :: !stack) in
-  let pop () =
-    begin
-      let v = List.hd !stack in
-      stack := List.tl !stack;
-      v
-    end
-  in
-
-  let node_indices = Hashtbl.create (Namemap.cardinal g) in
-  let get_index v = (Hashtbl.find node_indices v).index in
-  let get_root v = (Hashtbl.find node_indices v).root in
-  let set_root v r =
-    Hashtbl.replace node_indices v { (Hashtbl.find node_indices v) with root = r } in
-
-  let rec visit_node v =
-    begin
-      Hashtbl.add node_indices v { index = !index; root = !index };
-      index := !index + 1;
-      push v;
-      if Namemap.mem v g then Nameset.iter (visit_edge v) (Namemap.find v g);
-      if get_root v = get_index v then (* v is the root of a SCC *)
-        begin
-          let component = ref [] in
-          let finished = ref false in
-          while not !finished do
-            let w = pop () in
-            component := w :: !component;
-            if String.compare v w = 0 then finished := true;
-          done;
-          components := !component :: !components;
-        end
-    end
-  and visit_edge v w =
-    if not (Hashtbl.mem node_indices w) then
-      begin
-        visit_node w;
-        if Hashtbl.mem node_indices w then set_root v (min (get_root v) (get_root w));
-      end else begin
-        if List.mem w !stack then set_root v (min (get_root v) (get_index w))
-      end
-  in
-
-  let nodes = match original_order with
-    | Some nodes -> nodes
-    | None -> List.map fst (Namemap.bindings g)
-  in
-  List.iter (fun v -> if not (Hashtbl.mem node_indices v) then visit_node v) nodes;
-  List.rev !components
-
 let add_def_to_map id d defset =
   Namemap.add id
     (match Namemap.find id defset with
@@ -593,11 +533,14 @@ let add_def_to_map id d defset =
 let add_def_to_graph (prelude, original_order, defset, graph) d =
   let bound, used = fv_of_def false true [] d in
   let used = match d with
-    | DEF_reg_dec _ ->
+    | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, _), annot))
+    | DEF_reg_dec (DEC_aux (DEC_config (_, typ, _), annot)) ->
        (* For a register, we need to ensure that any undefined_type
           functions for types used by the register are placed before
           the register declaration. *)
-       let undefineds = Nameset.map (fun name -> "undefined_" ^ name) used in
+       let env = Type_check.env_of_annot annot in
+       let typ' = Type_check.Env.expand_synonyms env typ in
+       let undefineds = Nameset.map (fun name -> "undefined_" ^ name) (free_type_names_t false typ') in
        Nameset.union undefineds used
     | _ -> used
   in
@@ -607,13 +550,15 @@ let add_def_to_graph (prelude, original_order, defset, graph) d =
        definition is attached to only one of the identifiers, so it will not
        be duplicated in the final output. *)
     let id = Nameset.choose bound in
-    let other_ids = Nameset.remove id bound in
-    let graph_id = Namemap.add id (Nameset.union used other_ids) graph in
-    let add_other_node id' g = Namemap.add id' (Nameset.singleton id) g in
+    let other_ids = Nameset.elements (Nameset.remove id bound) in
+    let graph' =
+      NameGraph.add_edges id (other_ids @ Nameset.elements used) graph
+      |> List.fold_right (fun id' g -> NameGraph.add_edge id' id g) other_ids
+    in
     prelude,
     original_order @ [id],
     add_def_to_map id d defset,
-    Nameset.fold add_other_node other_ids graph_id
+    graph'
   with
   | Not_found ->
      (* Some definitions do not bind any identifiers at all.  This *should*
@@ -627,19 +572,6 @@ let add_def_to_graph (prelude, original_order, defset, graph) d =
         beginning when using a backend that requires topological sorting. *)
      prelude @ [d], original_order, defset, graph
 
-let print_dot graph component : unit =
-  match component with
-  | root :: _ ->
-     prerr_endline ("// Dependency cycle including " ^ root);
-     prerr_endline ("digraph cycle_" ^ root ^ " {");
-     List.iter (fun caller ->
-       let print_edge callee = prerr_endline ("  \"" ^ caller ^ "\" -> \"" ^ callee ^ "\";") in
-       Namemap.find caller graph
-       |> Nameset.filter (fun id -> List.mem id component)
-       |> Nameset.iter print_edge) component;
-     prerr_endline "}"
-  | [] -> ()
-
 let def_of_component graph defset comp =
   let get_def id = if Namemap.mem id defset then Namemap.find id defset else [] in
   match List.concat (List.map get_def comp) with
@@ -653,7 +585,7 @@ let def_of_component graph defset comp =
           raise (Reporting.err_unreachable (def_loc def) __POS__
             "Trying to merge non-function definition with mutually recursive functions") in
      let fundefs = List.concat (List.map get_fundefs defs) in
-     print_dot graph (List.map (fun fd -> string_of_id (id_of_fundef fd)) fundefs);
+     (* print_dot graph (List.map (fun fd -> string_of_id (id_of_fundef fd)) fundefs); *)
      [DEF_internal_mutrec fundefs]
   (* We could merge other stuff, in particular overloads, but don't need to just now *)
   | defs -> defs
@@ -661,7 +593,7 @@ let def_of_component graph defset comp =
 let top_sort_defs (Defs defs) =
   let prelude, original_order, defset, graph =
     List.fold_left add_def_to_graph ([], [], Namemap.empty, Namemap.empty) defs in
-  let components = scc ~original_order:original_order graph in
+  let components = NameGraph.scc ~original_order:original_order graph in
   Defs (prelude @ List.concat (List.map (def_of_component graph defset) components))
 
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 73ad5362..3b047040 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2838,20 +2838,25 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      in
      annot_exp (E_record_update (checked_exp, List.map check_fexp fexps)) typ
   | E_record fexps, _ ->
-     (* TODO: check record fields are total *)
      let rectyp_id = match Env.expand_synonyms env typ with
        | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
           rectyp_id
        | _ -> typ_error env l ("The type " ^ string_of_typ typ ^ " is not a record")
      in
+     let record_fields = ref (Env.get_record rectyp_id env |> snd |> List.map snd |> IdSet.of_list) in
      let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
+       record_fields := IdSet.remove field !record_fields;
        let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
        let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error env l ("Unification error: " ^ m) in
        let field_typ' = subst_unifiers unifiers field_typ in
        let checked_exp = crule check_exp env exp field_typ' in
        FE_aux (FE_Fexp (field, checked_exp), (l, None))
      in
-     annot_exp (E_record (List.map check_fexp fexps)) typ
+     let fexps = List.map check_fexp fexps in
+     if IdSet.is_empty !record_fields then
+       annot_exp (E_record fexps) typ
+     else
+       typ_error env l ("struct literal missing fields: " ^ string_of_list ", " string_of_id (IdSet.elements !record_fields))
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
      begin
        match letbind with
diff --git a/src/value.ml b/src/value.ml
index 3a9a071f..3e7782ed 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -123,7 +123,7 @@ let rec string_of_value = function
 let rec eq_value v1 v2 =
   match v1, v2 with
   | V_vector v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
-  | V_list v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
+  | V_list v1s, V_list v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
   | V_int n, V_int m -> Big_int.equal n m
   | V_real n, V_real m -> Rational.equal n m
   | V_bool b1, V_bool b2 -> b1 = b2
@@ -491,6 +491,10 @@ let value_undefined_vector = function
   | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
   | _ -> failwith "value undefined_vector"
 
+let value_undefined_list = function
+  | [_] -> V_list []
+  | _ -> failwith "value undefined_list"
+
 let value_undefined_bitvector = function
   | [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0)))
   | _ -> failwith "value undefined_bitvector"
@@ -747,6 +751,7 @@ let primops = ref
        ("undefined_bool", fun _ -> V_bool false);
        ("undefined_bitvector", value_undefined_bitvector);
        ("undefined_vector", value_undefined_vector);
+       ("undefined_list", value_undefined_list);
        ("undefined_string", fun _ -> V_string "");
        ("internal_pick", value_internal_pick);
        ("replicate_bits", value_replicate_bits);