From 00ca0aa4dce0abdcba574ce907e9a8a62d9d2255 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 15 Feb 2018 19:54:55 +0000 Subject: Can now compile aarch64/duopod to C Goes through the C compiler without any errors, but as we still don't have all the requisite builtins it won't actually produce an executable. There are still a few things that don't work properly, such as vectors of non-bit types - but once those are fixed and the Sail library is implemented fully it should work. --- src/c_backend.ml | 86 +++++++++++++++++++++++++++++++++++++++++++++++-------- src/type_check.ml | 2 +- 2 files changed, 75 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 0324bd3c..d9a964e0 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -283,6 +283,8 @@ and pp_apat = function | AP_global (id, _) -> pp_id id | AP_tup apats -> parens (separate_map (comma ^^ space) pp_apat apats) | AP_app (id, apat) -> pp_id id ^^ parens (pp_apat apat) + | AP_nil -> string "[||]" + | AP_cons (hd_apat, tl_apat) -> pp_apat hd_apat ^^ string " :: " ^^ pp_apat tl_apat and pp_cases cases = surround 2 0 lbrace (separate_map (comma ^^ hardline) pp_case cases) rbrace @@ -304,6 +306,10 @@ and pp_aval = function pp_annot typ (string "[" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "]") | AV_list (avals, typ) -> pp_annot typ (string "[|" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "|]") + | AV_record (fields, typ) -> + pp_annot typ (string "struct {" + ^^ separate_map (comma ^^ space) (fun (id, field) -> pp_id id ^^ string " = " ^^ pp_aval field) (Bindings.bindings fields) + ^^ string "}") let ae_lit lit typ = AE_val (AV_lit (lit, typ)) @@ -339,10 +345,11 @@ let rec anf_pat ?global:(global=false) (P_aux (p_aux, (l, _)) as pat) = | _ -> c_error ~loc:l ("Could not convert pattern to ANF: " ^ string_of_pat pat) let rec apat_globals = function - | AP_wild | AP_id _ -> [] + | AP_nil | AP_wild | AP_id _ -> [] | AP_global (id, typ) -> [(id, typ)] | AP_tup apats -> List.concat (List.map apat_globals apats) | AP_app (_, apat) -> apat_globals apat + | AP_cons (hd_apat, tl_apat) -> apat_globals hd_apat @ apat_globals tl_apat let rec anf (E_aux (e_aux, exp_annot) as exp) = let to_aval = function @@ -442,7 +449,7 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | E_exit exp -> let aexp = anf exp in let aval, wrap = to_aval aexp in - wrap (AE_app (mk_id "exit", [aval], unit_typ)) + wrap (AE_app (mk_id "sail_exit", [aval], unit_typ)) | E_return ret_exp -> let aexp = anf ret_exp in @@ -454,7 +461,7 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (AE_app (mk_id "assert", [aval1; aval2], unit_typ))) + wrap1 (wrap2 (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ))) | E_cons (exp1, exp2) -> let aexp1 = anf exp1 in @@ -1073,6 +1080,7 @@ let rec is_bitvector = function let rec string_of_aval_bit = function | AV_lit (L_aux (L_zero, _), _) -> "0" | AV_lit (L_aux (L_one, _), _) -> "1" + | _ -> assert false let rec chunkify n xs = match Util.take n xs, Util.drop n xs with @@ -1087,7 +1095,7 @@ let rec compile_aval ctx = function [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] | AV_lit (L_aux (L_string str, _), typ) -> - [], (F_lit ("\"" ^ str ^ "\""), ctyp_of_typ ctx typ), [] + [], (F_lit ("\"" ^ String.escaped str ^ "\""), ctyp_of_typ ctx typ), [] | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> let gs = gensym () in @@ -1106,6 +1114,9 @@ let rec compile_aval ctx = function | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit "0", CT_bit), [] | AV_lit (L_aux (L_one, _), _) -> [], (F_lit "1", CT_bit), [] + | AV_lit (L_aux (L_true, _), _) -> [], (F_lit "true", CT_bool), [] + | AV_lit (L_aux (L_false, _), _) -> [], (F_lit "false", CT_bool), [] + | AV_lit (L_aux (_, l) as lit, _) -> c_error ~loc:l ("Encountered unexpected literal " ^ string_of_lit lit) @@ -1144,6 +1155,7 @@ let rec compile_aval ctx = function | AV_vector ([], _) -> c_error "Encountered empty vector literal" + (* Convert a small bitvector to a uint64_t literal. *) | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> begin let bitstring = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals) ^ "ul") in @@ -1159,6 +1171,8 @@ let rec compile_aval ctx = function c_error "Encountered vector literal without vector type" end + (* Convert a bitvector literal that is larger than 64-bits to a + variable size bitvector, converting it in 64-bit chunks. *) | AV_vector (avals, typ) when is_bitvector avals -> let len = List.length avals in let bitstring avals = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals) ^ "ul") in @@ -1174,8 +1188,36 @@ let rec compile_aval ctx = function (F_id gs, CT_bv true), [iclear (CT_bv true) gs] - | AV_vector _ -> - c_error "Have AV_vector" + (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) + | AV_vector (avals, Typ_aux (Typ_app (id, [_; Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) + when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 -> + let len = List.length avals in + let direction = match ord with + | Ord_aux (Ord_inc, _) -> false + | Ord_aux (Ord_dec, _) -> true + in + let gs = gensym () in + let ctyp = CT_uint64 (len, direction) in + let mask i = "0b" ^ String.make (63 - i) '0' ^ "1" ^ String.make i '0' ^ "ul" in + let aval_mask i aval = + let setup, cval, cleanup = compile_aval ctx aval in + match cval with + | (F_lit "0", _) -> [] + | (F_lit "1", _) -> + [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] + | _ -> + setup @ [iif cval [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup + in + [idecl ctyp gs; + icopy (CL_id gs) (F_lit "0ul", ctyp)] + @ List.concat (List.mapi aval_mask (List.rev avals)), + (F_id gs, ctyp), + [] + (* + c_error ("Have AV_vector (small/bits): " ^ Pretty_print_sail.to_string (separate_map (comma ^^ space) pp_aval avals)) *) + + | AV_vector _ as aval -> + c_error ("Have AV_vector: " ^ Pretty_print_sail.to_string (pp_aval aval)) | AV_list (avals, Typ_aux (typ, _)) -> let ctyp = match typ with @@ -1500,7 +1542,7 @@ let rec compile_aexp ctx = function (* Cleanup info will be re-added by fix_early_return *) let return_setup, cval, _ = compile_aval ctx aval in return_setup @ [ireturn cval], - CT_unit, + cval_ctyp cval, (fun clexp -> icomment "unreachable after return"), [] @@ -1520,7 +1562,15 @@ let rec compile_aexp ctx = function (fun clexp -> icopy clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), cleanup + | AE_for _ -> + [], + CT_unit, + (fun clexp -> icomment "for loop"), + [] + +(* | aexp -> failwith ("Cannot compile ANF expression: " ^ Pretty_print_sail.to_string (pp_aexp aexp)) + *) and compile_block ctx = function | [] -> [] @@ -1724,8 +1774,14 @@ let compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> let aexp = map_functions (analyze_primop ctx) (c_literals ctx (anf exp)) in + prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let gs = gensym () in + let pat = match pat with + | P_aux (P_tup [], annot) -> P_aux (P_lit (mk_lit L_unit), annot) + | _ -> pat + in + prerr_endline (string_of_id id ^ " : " ^ string_of_ctyp ctyp); if is_stack_ctyp ctyp then let instrs = [idecl ctyp gs] @ setup @ [call (CL_id gs)] @ cleanup @ [ireturn (F_id gs, ctyp)] in let instrs = fix_exception ctx instrs in @@ -1998,12 +2054,12 @@ let make_dot id graph = let sgen_id id = Util.zencode_string (string_of_id id) let codegen_id id = string (sgen_id id) -let upper_sgen_id id = Util.zencode_upper_string (string_of_id id) +let upper_sgen_id id = Util.zencode_string (string_of_id id) let upper_codegen_id id = string (upper_sgen_id id) let sgen_ctyp = function | CT_unit -> "unit" - | CT_bit -> "bit" + | CT_bit -> "int" | CT_bool -> "bool" | CT_uint64 _ -> "uint64_t" | CT_int64 -> "int64_t" @@ -2014,11 +2070,12 @@ let sgen_ctyp = function | CT_enum (id, _) -> "enum " ^ sgen_id id | CT_variant (id, _) -> "struct " ^ sgen_id id | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) + | CT_vector _ -> "int" (* FIXME *) | CT_string -> "sail_string" let sgen_ctyp_name = function | CT_unit -> "unit" - | CT_bit -> "bit" + | CT_bit -> "int" | CT_bool -> "bool" | CT_uint64 _ -> "uint64_t" | CT_int64 -> "int64_t" @@ -2029,6 +2086,7 @@ let sgen_ctyp_name = function | CT_enum (id, _) -> sgen_id id | CT_variant (id, _) -> sgen_id id | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) + | CT_vector _ -> "int" (* FIXME *) | CT_string -> "sail_string" let sgen_cval_param (frag, ctyp) = @@ -2399,6 +2457,9 @@ let codegen_def' ctx = function | _ -> assert false in let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in + prerr_endline (string_of_id id); + prerr_endline (Util.string_of_list ", " (fun arg -> sgen_id arg) args); + prerr_endline (Util.string_of_list ", " (fun ctyp -> sgen_ctyp ctyp) arg_ctyps); let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in let function_header = match ret_arg with @@ -2451,8 +2512,9 @@ let codegen_def ctx def = let compile_ast ctx (Defs defs) = try - let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "assert") "(bool, string) -> unit effect {escape}" in - let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs])) } in + let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in + let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in + let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in let cdefs = List.concat (List.rev chunks) in let docs = List.map (codegen_def ctx) cdefs in diff --git a/src/type_check.ml b/src/type_check.ml index 3d694a1c..acc79933 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2052,7 +2052,7 @@ let fresh_var = mk_id ("v#" ^ string_of_int n) let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp = - let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in + let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, Env.expand_synonyms env typ, eff))) in let add_effect exp eff = match exp with | (E_aux (exp, (l, Some (env, typ, _)))) -> E_aux (exp, (l, Some (env, typ, eff))) | _ -> failwith "Tried to add effect to unannoted expression" -- cgit v1.2.3