From 03c5ff3f31d26f05700bc4402dd92d5f00a07093 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 24 Jan 2018 03:18:46 +0000 Subject: More work on experimental C backend --- src/c_backend.ml | 162 +++++++++++++++++++++++++++++++++++++++++++++++++++---- src/isail.ml | 2 +- 2 files changed, 153 insertions(+), 11 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 1527c99b..028f0146 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -58,9 +58,16 @@ let zencode_id = function | Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l) | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l) +let lvar_typ = function + | Local (_, typ) -> typ + | Register typ -> typ + | _ -> assert false + type aexp = | AE_val of aval | AE_app of id * aval list * typ + | AE_cast of aexp * typ + | AE_assign of id * aexp | AE_let of id * aexp * aexp * typ | AE_block of aexp list * aexp * typ | AE_return of aval * typ @@ -73,6 +80,8 @@ and aval = let rec map_aval f = function | AE_val v -> AE_val (f v) + | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) + | AE_assign (id, aexp) -> AE_assign (id, map_aval f aexp) | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ) | AE_let (id, aexp1, aexp2, typ) -> AE_let (id, map_aval f aexp1, map_aval f aexp2, typ) | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) @@ -80,6 +89,8 @@ let rec map_aval f = function let rec map_functions f = function | AE_app (id, vs, typ) -> f id vs typ + | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) + | AE_assign (id, aexp) -> AE_assign (id, map_functions f aexp) | AE_let (id, aexp1, aexp2, typ) -> AE_let (id, map_functions f aexp1, map_functions f aexp2, typ) | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) | AE_val _ | AE_return _ as v -> v @@ -106,6 +117,10 @@ let pp_annot typ doc = let rec pp_aexp = function | AE_val v -> pp_aval v + | AE_cast (aexp, typ) -> + pp_annot typ (string "$" ^^ pp_aexp aexp) + | AE_assign (id, aexp) -> + pp_id id ^^ string " := " ^^ pp_aexp aexp | AE_app (id, args, typ) -> pp_annot typ (pp_id ~color:Util.red id ^^ parens (separate_map (comma ^^ space) pp_aval args)) | AE_let (id, binding, body, typ) -> group @@ -153,7 +168,7 @@ let rec split_block = function let rec anf (E_aux (e_aux, _) as exp) = let to_aval = function | AE_val v -> (v, fun x -> x) - | AE_app (_, _, typ) | AE_let (_, _, _, typ) | AE_return (_, typ) as aexp -> + | AE_app (_, _, typ) | AE_let (_, _, _, typ) | AE_return (_, typ) | AE_cast (_, typ) as aexp -> let id = gensym () in (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, aexp, x, typ_of exp)) in @@ -166,12 +181,26 @@ let rec anf (E_aux (e_aux, _) as exp) = let alast = anf last in AE_block (aexps, alast, typ_of exp) + | E_assign (LEXP_aux (LEXP_id id, _), exp) -> + let aexp = anf exp in + AE_assign (id, aexp) + | E_app (id, exps) -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in wrap (AE_app (id, List.map fst avals, typ_of exp)) + | E_throw exp -> + let aexp = anf exp in + let aval, wrap = to_aval aexp in + wrap (AE_app (mk_id "throw", [aval], unit_typ)) + + | E_return exp -> + let aexp = anf exp in + let aval, wrap = to_aval aexp in + wrap (AE_app (mk_id "return", [aval], unit_typ)) + | E_id id -> let lvar = Env.lookup_id id (env_of exp) in AE_val (AV_id (zencode_id id, lvar)) @@ -189,7 +218,7 @@ let rec anf (E_aux (e_aux, _) as exp) = let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in wrap (AE_val (AV_tuple (List.map fst avals))) - | E_cast (typ, exp) -> anf exp + | E_cast (typ, exp) -> AE_cast (anf exp, typ) | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ -> (* Should be re-written by type checker *) @@ -199,7 +228,10 @@ let rec anf (E_aux (e_aux, _) as exp) = (* Interpreter specific *) failwith "encountered E_internal_value when converting to ANF" - + | E_sizeof _ | E_constraint _ -> + (* Sizeof nodes removed by sizeof rewriting pass *) + failwith "encountered E_sizeof or E_constraint node when converting to ANF" + let max_int64 = Big_int.of_int64 Int64.max_int let min_int64 = Big_int.of_int64 Int64.min_int @@ -227,6 +259,16 @@ let stack_typ (Typ_aux (typ_aux, _) as typ) = end | _ -> None +let heap_typ (Typ_aux (typ_aux, _) as typ) = + match typ_aux with + | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" -> + Some "mpz_t" + | Typ_id id when string_of_id id = "int" -> + Some "mpz_t" + | Typ_app (id, _) when string_of_id id = "vector" -> + Some "sail_bv" + | _ -> None + let is_stack_typ typ = match stack_typ typ with | Some _ -> true | None -> false @@ -237,7 +279,7 @@ let literal_to_cstring (L_aux (l_aux, _) as lit) = Some (Big_int.to_string n ^ "L") | L_hex str when String.length str <= 16 -> let padding = 16 - String.length str in - Some ("0x" ^ String.make padding '0' ^ str ^ "L") + Some ("0x" ^ String.make padding '0' ^ str ^ "ul") | _ -> None let c_literals = @@ -256,8 +298,8 @@ let mask m = if Big_int.less_equal m (Big_int.of_int 64) then let n = Big_int.to_int m in if n mod 4 == 0 - then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "L" - else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "L" + then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "ul" + else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "ul" else failwith "Tried to create a mask literal for a vector greater than 64 bits." @@ -273,7 +315,7 @@ let c_aval = function | AV_id (id, lvar) as v -> begin match lvar with - | Local (Immutable, typ) when is_stack_typ typ -> + | Local (_, typ) when is_stack_typ typ -> AV_C_fragment (string_of_id id, typ) | _ -> v end @@ -287,7 +329,7 @@ let c_fragment_string = function | AV_C_fragment (str, _) -> str | _ -> assert false -let analyze_primop id args typ = +let analyze_primop' id args typ = let no_change = AE_app (id, args, typ) in (* primops add_range and add_atom *) @@ -319,7 +361,6 @@ let analyze_primop id args typ = in match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> - print_endline "small"; let x, y = c_aval x, c_aval y in if is_c_fragment x && is_c_fragment y then AE_val (AV_C_fragment ("(" ^ c_fragment_string x ^ " + " ^ c_fragment_string y ^ ") & " ^ mask n, typ)) @@ -331,10 +372,111 @@ let analyze_primop id args typ = else no_change -let compile_exp exp = +let analyze_primop id args typ = + let no_change = AE_app (id, args, typ) in + try analyze_primop' id args typ with + | Failure _ -> no_change + +type allocation = + | Stack of string + | Heap of string + +let string_of_allocation = function + | Stack str -> "S$" ^ str + | Heap str -> "H$" ^ str + +let choose_allocation typ = + match stack_typ typ with + | Some str -> Stack str + | None -> + match heap_typ typ with + | Some str -> Heap str + | _ -> failwith "don't know where to allocate type" + +type ccall = + | CCallH of (string -> string) + | CCallS of string + +let compile_funcall env id args typ = + let setup = ref [] in + let cleanup = ref [] in + + let _, Typ_aux (fn_typ, _) = Env.get_val_spec id env in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ + | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ + | _ -> assert false + in + let arg_allocs = List.map choose_allocation arg_typs in + print_endline (Util.string_of_list ", " string_of_allocation arg_allocs); + + let setup_arg alloc aval = + match alloc, aval with + | Heap str_h, AV_C_fragment (c, typ) -> + let Some str_s = stack_typ typ in + let g = gensym () in + setup := (str_h ^ " " ^ string_of_id g ^ ";") :: !setup; + setup := Printf.sprintf "init_%s_of_%s(%s, %s);" str_h str_s (string_of_id g) c :: !setup; + cleanup := Printf.sprintf "clear_%s(%s);" str_h (string_of_id g) :: !cleanup; + string_of_id g + | Stack str_h, AV_C_fragment (c, typ) -> c + | Heap str_h, AV_id (id, typ) -> + begin + match choose_allocation (lvar_typ typ) with + | Heap _ -> string_of_id id + | Stack str_s -> + let g = gensym () in + setup := (str_h ^ " " ^ string_of_id g ^ ";") :: !setup; + setup := Printf.sprintf "init_%s_of_%s(%s, %s);" str_h str_s (string_of_id g) (string_of_id id) :: !setup; + cleanup := Printf.sprintf "clear_%s(%s);" str_h (string_of_id g) :: !cleanup; + string_of_id g + end + | Stack str_s, AV_id (id, typ) -> string_of_id id + | _, AV_id _ -> "AV_id" + | _, AV_lit _ -> "AV_lit" + in + + let str_args = List.map2 setup_arg arg_allocs args in + + match choose_allocation ret_typ with + | Heap str_h -> + let call ret = Printf.sprintf "sail_%s(%s, %s);" (string_of_id id) ret (String.concat ", " str_args) in + (List.rev !setup, str_h, CCallH call, !cleanup) + | Stack str_s -> + let call = Printf.sprintf "sail_%s(%s);" (string_of_id id) (String.concat ", " str_args) in + (List.rev !setup, str_s, CCallS call, !cleanup) + +let rec compile_aexp env = function + | AE_let (id, binding, body, typ) -> + let setup, ctyp, call, cleanup = compile_aexp env binding in + let letb1, letb1c = match call with + | CCallH f -> f (string_of_id id), [Printf.sprintf "clear_%s(%s);" ctyp (string_of_id id)] + | CCallS str -> string_of_id id ^ " = " ^ str, [] + in + let letb2 = setup @ [ctyp ^ " " ^ string_of_id id ^ ";"; letb1] @ cleanup in + let setup, ctyp, call, cleanup = compile_aexp env body in + letb2 @ setup, ctyp, call, cleanup @ letb1c + + | AE_app (id, vs, typ) -> + compile_funcall env id vs typ + + | AE_val (AV_C_fragment (c, typ)) -> + let Some ctyp = stack_typ typ in + [], ctyp, CCallS c, [] + +let print_compiled (setup, ctyp, call, cleanup) = + List.iter print_endline setup; + begin match call with + | CCallH f -> print_endline (f ("?" ^ ctyp)) + | CCallS str -> print_endline ("?" ^ ctyp ^ " = " ^ str) + end; + List.iter print_endline cleanup + +let compile_exp env exp = let aexp = anf exp in let aexp = c_literals aexp in let aexp = map_functions analyze_primop aexp in + print_compiled (compile_aexp env aexp); aexp diff --git a/src/isail.ml b/src/isail.ml index 235e46a2..07a72bd2 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -296,7 +296,7 @@ let handle_input' input = vs_ids := Initial_check.val_spec_ids !interactive_ast | ":compile" -> let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord arg) in - let anf = C_backend.compile_exp exp in + let anf = C_backend.compile_exp !interactive_env exp in print_endline (Pretty_print_sail.to_string (C_backend.pp_aexp anf)) | ":u" | ":unload" -> interactive_ast := Ast.Defs []; -- cgit v1.2.3