More list C codegen fixes for issue #59

4 files changed, 43 insertions, 0 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 7491b3e3..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
@@ -1890,6 +1891,12 @@ let codegen_list_equal id ctyp =
   ^^ 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
@@ -1905,6 +1912,7 @@ let codegen_list ctx ctyp =
       ^^ 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/value.ml b/src/value.ml
index b166e99b..3e7782ed 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -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);
diff --git a/test/c/warl_undef.expect b/test/c/warl_undef.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/warl_undef.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/warl_undef.sail b/test/c/warl_undef.sail
new file mode 100644
index 00000000..4828afc8
--- /dev/null
+++ b/test/c/warl_undef.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$option -undefined_gen
+
+$include <prelude.sail>
+
+val "eq_anything" : forall ('a: Type). ('a, 'a) -> bool
+
+overload operator == = {eq_anything}
+
+function neq_anything forall ('a: Type). (x: 'a, y: 'a) -> bool =
+  not_bool(x == y)
+
+overload operator != = {neq_anything}
+
+val "print_endline" : string -> unit
+
+struct WARL_range = {
+  rangelist : list(int),
+}
+
+let x : WARL_range = struct {
+  rangelist = [|0, 1|]
+}
+
+function main () : unit -> unit = {
+  let z: WARL_range = undefined;
+  print_endline("ok")
+}