Fix an issue with riscv_platform involving flow typing

- Refactor the flow typing implementation in the type-checker. This
  should fix an issue involving riscv_platform. Specifically it should
  now work better when an if statement contains multiple conditions
  combined with and/or, only some of which imply constraints at the
  type level. This change also simplifies the implementation of flow
  typing, and removes some obscure features that were hardly used -
  specifically, flow typing could modify types, but this was fairly
  obscure and doesn't seem to affect any of our specifications. More
  testing is needed to ensure that this change hasn't inadvertantly
  broken anything, but it does pass all our tests and continue to
  typecheck arm, riscv and cheri.

- Also adds a option for generating faster undefined functions for
  enum and variant types. Previously I tried to optimise away such
  functions in the C backend, because they could be slow and cause
  considerable uneccessary allocation, however this was error prone
  and it turns out a much simpler solution is to simply make the
  functions themselves much faster, at the cost of hard-coding certain
  decisions about what undefined means for these types at compile tile
  (which is fine for fast emulation). This almost doubles the
  performance of the generated C code.

- Add a wrapper for right shift to avoid UB when shifting by 64 or
  more places.

1 files changed, 10 insertions, 3 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 1ba1b9e6..d27281fe 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -55,6 +55,7 @@ module Big_int = Nat_big_num
 
 (* See mli file for details on what these flags do *)
 let opt_undefined_gen = ref false
+let opt_fast_undefined = ref false
 let opt_magic_hash = ref false
 let opt_enum_casts = ref false
 
@@ -1059,8 +1060,11 @@ let generate_undefineds vs_ids (Defs defs) =
        [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
-                            (mk_exp (E_app (mk_id "internal_pick",
-                                            [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
+                            (if !opt_fast_undefined && List.length ids > 0 then
+                               mk_exp (E_id (List.hd ids))
+                             else
+                               mk_exp (E_app (mk_id "internal_pick",
+                                              [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
     | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
@@ -1072,7 +1076,10 @@ let generate_undefineds vs_ids (Defs defs) =
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
-                            (mk_exp (E_app (mk_id "internal_pick",
+                            (if !opt_fast_undefined && List.length tus > 0 then
+                               undefined_tu (List.hd tus)
+                             else
+                               mk_exp (E_app (mk_id "internal_pick",
                                             [mk_exp (E_list (List.map undefined_tu tus))])))]]
     | _ -> []
   in