From a5491d52d32aa1a15b7f904035fe2e45760bf2f3 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 4 Jun 2018 20:49:49 +0100 Subject: 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. --- src/initial_check.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'src/initial_check.ml') 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 -- cgit v1.2.3