Allow undefined values in IR for SMT generation

Means we can avoid the use of -undefined_gen for Sail->SMT

6 files changed, 16 insertions, 14 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 1fcfe551..c8cee6ab 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1050,7 +1050,7 @@ let sgen_function_id id =
 let sgen_function_uid uid =
   let str = zencode_uid uid in
   !opt_prefix ^ String.sub str 1 (String.length str - 1)
-  
+
 let codegen_function_id id = string (sgen_function_id id)
 
 let rec sgen_ctyp = function
@@ -1124,11 +1124,11 @@ let rec sgen_value = function
   | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
-  | VL_tuple values -> "(" ^ Util.string_of_list ", " sgen_value values ^ ")"
-  | VL_list [] -> "NULL"
-  | VL_list values -> "[|" ^ Util.string_of_list ", " sgen_value values ^ "|]"
+  | VL_empty_list -> "NULL"
   | VL_enum element -> Util.zencode_string element
   | VL_ref r -> "&" ^ Util.zencode_string r
+  | VL_undefined ->
+     Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal"
 
 let rec sgen_cval = function
   | V_id (id, ctyp) -> sgen_name id
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 202abbd5..051f5c19 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -247,6 +247,10 @@ let rec compile_aval l ctx = function
 
   | AV_lit (L_aux (L_unit, _), _) -> [], V_lit (VL_unit, CT_unit), []
 
+  | AV_lit (L_aux (L_undef, _), typ) ->
+     let ctyp = ctyp_of_typ ctx typ in
+     [], V_lit (VL_undefined, ctyp), []
+
   | AV_lit (L_aux (_, l) as lit, _) ->
      raise (Reporting.err_general l ("Encountered unexpected literal " ^ string_of_lit lit ^ " when converting ANF represention into IR"))
 
@@ -581,12 +585,12 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
      | CT_list ctyp ->
         let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in
         let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in
-        [ijump (V_call (Eq, [cval; V_lit (VL_list [], CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
+        [ijump (V_call (Eq, [cval; V_lit (VL_empty_list, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
      | _ ->
         raise (Reporting.err_general l "Tried to pattern match cons on non list type")
      end
 
-  | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_list [], ctyp)])) case_label], [], ctx
+  | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_empty_list, ctyp)])) case_label], [], ctx
 
 let unit_cval = V_lit (VL_unit, CT_unit)
 
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index 3ab634d2..ca11696e 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -107,7 +107,7 @@ module Ir_formatter = struct
       | I_label label ->
          C.output_label_instr buf label_map label
       | I_jump (cval, label) ->
-         add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " " ^ C.string_of_label (StringMap.find label label_map))
+         add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " " ^ C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map))
       | I_goto label ->
          add_instr n buf indent (C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map))
       | I_match_failure ->
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 8797f78d..725d2a89 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -313,8 +313,6 @@ let rec smt_value ctx vl ctyp =
      else
        Real_lit str
   | VL_enum str, _ -> Enum (Util.zencode_string str)
-  | VL_tuple vls, CT_tup ctyps when List.length vls = List.length ctyps ->
-     Fn ("tup" ^ string_of_int (List.length vls), List.map2 (smt_value ctx) vls ctyps)
   | VL_ref reg_name, _ ->
      let id = mk_id reg_name in
      let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 51140bb7..d24e6b8a 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -362,14 +362,14 @@ let rec string_of_value = function
   | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
-  | VL_tuple values -> "(" ^ Util.string_of_list ", " string_of_value values ^ ")"
-  | VL_list [] -> "NULL"
-  | VL_list values -> "[|" ^ Util.string_of_list ", " string_of_value values ^ "|]"
+  | VL_empty_list -> "NULL"
   | VL_enum element -> Util.zencode_string element
   | VL_ref r -> "&" ^ Util.zencode_string r
+  | VL_undefined -> "undefined"
 
 let rec string_of_cval = function
   | V_id (id, ctyp) -> string_of_name id
+  | V_lit (VL_undefined, ctyp) -> string_of_value VL_undefined ^ " : " ^ string_of_ctyp ctyp
   | V_lit (vl, ctyp) -> string_of_value vl
   | V_call (op, cvals) ->
      Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals)
diff --git a/src/value2.lem b/src/value2.lem
index ec0cd5a8..1c525f80 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -60,7 +60,7 @@ type vl =
   | VL_int of integer
   | VL_string of string
   | VL_real of string
-  | VL_tuple of list vl
-  | VL_list of list vl
+  | VL_empty_list
   | VL_enum of string
   | VL_ref of string
+  | VL_undefined