C: Fix a bug where function argument type becomes more specific due to flow typing

Added a regression test as c/test/downcast_fn.sail

5 files changed, 49 insertions, 15 deletions

diff --git a/lib/sail.c b/lib/sail.c
index 62801cc7..3c0b0dac 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -173,6 +173,12 @@ void CREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op)
 }
 
 inline
+mach_int CREATE_OF(mach_int, sail_int)(const sail_int op)
+{
+  return mpz_get_ui(op);
+}
+
+inline
 void RECREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op)
 {
   mpz_set_si(*rop, op);
diff --git a/lib/sail.h b/lib/sail.h
index a8651f50..37b6b685 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -101,6 +101,8 @@ SAIL_BUILTIN_TYPE(sail_int);
 void CREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
 void RECREATE_OF(sail_int, mach_int)(sail_int *, const mach_int);
 
+mach_int CREATE_OF(mach_int, sail_int)(const sail_int);
+
 void CREATE_OF(sail_int, sail_string)(sail_int *, const sail_string);
 void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
 
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 61e8777e..43487955 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2235,23 +2235,25 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      string (Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
 
   | I_init (ctyp, id, cval) when is_stack_ctyp ctyp ->
-     string (Printf.sprintf "  %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval))
+     if ctyp_equal ctyp (cval_ctyp cval) then
+       ksprintf string "  %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval)
+     else
+       ksprintf string "  %s %s = CREATE_OF(%s, %s)(%s);"
+                (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_cval cval)
   | I_init (ctyp, id, cval) ->
-     string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_id id)) ^^ hardline
-     ^^ string (Printf.sprintf "  CREATE_OF(%s, %s)(&%s, %s);"
-                               (sgen_ctyp_name ctyp)
-                               (sgen_ctyp_name (cval_ctyp cval))
-                               (sgen_id id)
-                               (sgen_cval_param cval))
+     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
+     ^^ ksprintf string "  CREATE_OF(%s, %s)(&%s, %s);"
+                 (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)
 
   | I_reinit (ctyp, id, cval) when is_stack_ctyp ctyp ->
-     string (Printf.sprintf "  %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval))
+     if ctyp_equal ctyp (cval_ctyp cval) then
+       ksprintf string "  %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval)
+     else
+       ksprintf string "  %s %s = CREATE_OF(%s, %s)(%s);"
+                (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_cval cval)
   | I_reinit (ctyp, id, cval) ->
-     string (Printf.sprintf "  RECREATE_OF(%s, %s)(&%s, %s);"
-                            (sgen_ctyp_name ctyp)
-                            (sgen_ctyp_name (cval_ctyp cval))
-                            (sgen_id id)
-                            (sgen_cval_param cval))
+     ksprintf string "  RECREATE_OF(%s, %s)(&%s, %s);"
+              (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)
 
   | I_reset (ctyp, id) when is_stack_ctyp ctyp ->
      string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_id id))
@@ -2262,7 +2264,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      string (Printf.sprintf "  return %s;" (sgen_cval cval))
 
   | I_throw cval ->
-     c_error "I_throw reached code generator"
+     c_error ~loc:l "I_throw reached code generator"
 
   | I_undefined ctyp ->
      let rec codegen_exn_return ctyp =
@@ -3078,7 +3080,7 @@ let compile_ast ctx c_includes (Defs defs) =
        @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
        @ (if regs = [] then [] else [ "  zinitializze_registers(UNIT);" ])
        @ letbind_initializers
-       @ [  "  if (process_arguments(argc, argv)) exit(EXIT_FAILURE);" ]
+       @ [ "  if (process_arguments(argc, argv)) exit(EXIT_FAILURE);" ]
        @ [ "  zmain(UNIT);" ]
        @ letbind_finalizers
        @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
diff --git a/test/c/downcast_fn.expect b/test/c/downcast_fn.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/downcast_fn.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/downcast_fn.sail b/test/c/downcast_fn.sail
new file mode 100644
index 00000000..d4b8ae5d
--- /dev/null
+++ b/test/c/downcast_fn.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+$include <flow.sail>
+
+val f1 : forall 'n, 0 < 'n <= 8. int('n) -> unit
+
+function f1(_) = ()
+
+val f2 : forall 'n, 'n > 0. int('n) -> unit
+
+function f2(width) =
+  if 'n <= 8 then
+    f1(width)
+  else ()
+
+val "print" : string -> unit
+
+val main : unit -> unit
+
+function main() = {
+  f2(3);
+  print("ok\n")
+}