diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 478 | ||||
| -rw-r--r-- | src/isail.ml | 2 | ||||
| -rw-r--r-- | src/sail.ml | 2 | ||||
| -rw-r--r-- | src/util.ml | 8 | ||||
| -rw-r--r-- | src/util.mli | 1 |
5 files changed, 362 insertions, 129 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index b06cd950..2ebd28c8 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -63,26 +63,6 @@ let lvar_typ = function | Register typ -> typ | _ -> assert false -(* - -1) Conversion to ANF - - tannot defs -> (typ, aexp) cdefs - -2) Primitive operation optimizations - -3) Lowering to low-level imperative language - - (typ, aexp) cdefs -> (ctyp, instr list) cdefs - -4) Low level optimizations (e.g. reducing allocations) - -5) Generation of C code - - (ctyp, instr list) -> string - -*) - (**************************************************************************) (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) @@ -121,8 +101,9 @@ type aexp = | AE_let of id * typ * aexp * aexp * typ | AE_block of aexp list * aexp * typ | AE_return of aval * typ - | AE_throw of aval | AE_if of aval * aexp * aexp * typ + | AE_field of aval * id * typ + | AE_record_update of aval * aval Bindings.t * typ | AE_for of id * aexp * aexp * aexp * order * aexp | AE_loop of loop * aexp * aexp @@ -131,6 +112,8 @@ and aval = | AV_id of id * lvar | AV_ref of id * lvar | AV_tuple of aval list + | AV_list of aval list * typ + | AV_vector of aval list * typ | AV_C_fragment of string * typ (* Map over all the avals in an aexp. *) @@ -145,6 +128,11 @@ let rec map_aval f = function | AE_return (aval, typ) -> AE_return (f aval, typ) | AE_if (aval, aexp1, aexp2, typ2) -> AE_if (f aval, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) + | AE_record_update (aval, updates, typ) -> + AE_record_update (f aval, Bindings.map f updates, typ) (* Map over all the functions in an aexp. *) let rec map_functions f = function @@ -155,10 +143,13 @@ let rec map_functions f = function | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) | AE_if (aval, aexp1, aexp2, typ) -> AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) - | AE_val _ | AE_return _ as v -> v + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_functions f aexp1, map_functions f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_functions f aexp1, map_functions f aexp2, map_functions f aexp3, order, map_functions f aexp4) + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ as v -> v (* For debugging we provide a pretty printer for ANF expressions. *) - + let pp_id ?color:(color=Util.green) id = string (string_of_id id |> color |> Util.clear) @@ -179,6 +170,11 @@ let pp_lvar lvar doc = let pp_annot typ doc = string "[" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc +let pp_order = function + | Ord_aux (Ord_inc, _) -> string "inc" + | Ord_aux (Ord_dec, _) -> string "dec" + | _ -> assert false (* Order types have been specialised, so no polymorphism in C backend. *) + let rec pp_aexp = function | AE_val v -> pp_aval v | AE_cast (aexp, typ) -> @@ -205,6 +201,23 @@ let rec pp_aexp = function | AE_block (aexps, aexp, typ) -> pp_annot typ (surround 2 0 lbrace (pp_block (aexps @ [aexp])) rbrace) | AE_return (v, typ) -> pp_annot typ (string "return" ^^ parens (pp_aval v)) + | AE_loop (While, aexp1, aexp2) -> + separate space [string "while"; pp_aexp aexp1; string "do"; pp_aexp aexp2] + | AE_loop (Until, aexp1, aexp2) -> + separate space [string "repeat"; pp_aexp aexp2; string "until"; pp_aexp aexp1] + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let header = + string "foreach" ^^ space ^^ + group (parens (separate (break 1) + [ pp_id id; + string "from " ^^ pp_aexp aexp1; + string "to " ^^ pp_aexp aexp2; + string "by " ^^ pp_aexp aexp3; + string "in " ^^ pp_order order ])) + in + header ^//^ pp_aexp aexp4 + | AE_field _ -> string "FIELD" + | AE_record_update (_, _, typ) -> pp_annot typ (string "RECORD UPDATE") and pp_block = function | [] -> string "()" @@ -215,14 +228,19 @@ and pp_aval = function | AV_lit (lit, typ) -> pp_annot typ (string (string_of_lit lit)) | AV_id (id, lvar) -> pp_lvar lvar (pp_id id) | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals) + | AV_ref (id, lvar) -> string "ref" ^^ space ^^ pp_lvar lvar (pp_id id) | AV_C_fragment (str, typ) -> pp_annot typ (string (str |> Util.cyan |> Util.clear)) + | AV_vector (avals, typ) -> + 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 "|]") let ae_lit lit typ = AE_val (AV_lit (lit, typ)) let gensym_counter = ref 0 let gensym () = - let id = mk_id ("v" ^ string_of_int !gensym_counter) in + let id = mk_id ("gs#" ^ string_of_int !gensym_counter) in incr gensym_counter; id @@ -236,9 +254,18 @@ let rec split_block = function let rec anf (E_aux (e_aux, exp_annot) as exp) = let to_aval = function | AE_val v -> (v, fun x -> x) - | AE_app (_, _, typ) | AE_let (_, _, _, _, typ) | AE_return (_, typ) | AE_cast (_, typ) as aexp -> + | AE_app (_, _, typ) + | AE_let (_, _, _, _, typ) + | AE_return (_, typ) + | AE_cast (_, typ) + | AE_if (_, _, _, typ) + | AE_field (_, _, typ) + as aexp -> let id = gensym () in (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, typ, aexp, x, typ_of exp)) + | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ as aexp -> + let id = gensym () in + (AV_id (id, Local (Immutable, unit_typ)), fun x -> AE_let (id, unit_typ, aexp, x, typ_of exp)) in match e_aux with | E_lit lit -> ae_lit lit (typ_of exp) @@ -253,6 +280,15 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let aexp = anf exp in AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp) + | E_loop (loop_typ, cond, exp) -> + let acond = anf cond in + let aexp = anf exp in + AE_loop (loop_typ, acond, aexp) + + | E_for (id, exp1, exp2, exp3, order, body) -> + let aexp1, aexp2, aexp3, abody = anf exp1, anf exp2, anf exp3, anf body in + AE_for (id, aexp1, aexp2, aexp3, order, abody) + | E_if (cond, then_exp, else_exp) -> let cond_val, wrap = to_aval (anf cond) in let then_aexp = anf then_exp in @@ -263,7 +299,35 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot)) | E_app_infix (x, Id_aux (DeIid op, l), y) -> anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot)) - + + | E_vector 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_val (AV_vector (List.map fst avals, typ_of exp))) + + | E_list 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_val (AV_list (List.map fst avals, typ_of exp))) + + | E_field (exp, id) -> + let aval, wrap = to_aval (anf exp) in + wrap (AE_field (aval, id, typ_of exp)) + + | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = + let aval, wrap = to_aval (anf exp) in + (id, aval), wrap + in + let aval, exp_wrap = to_aval (anf exp) in + let fexps = List.map anf_fexp fexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in + let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in + exp_wrap (wrap (AE_record_update (aval, record, typ_of exp))) + + | E_app (id, exps) -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in @@ -301,7 +365,11 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | E_id id -> let lvar = Env.lookup_id id (env_of exp) in - AE_val (AV_id (zencode_id id, lvar)) + AE_val (AV_id (id, lvar)) + + | E_ref id -> + let lvar = Env.lookup_id id (env_of exp) in + AE_val (AV_ref (id, lvar)) | E_return exp -> let aval, wrap = to_aval (anf exp) in @@ -311,7 +379,7 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in - AE_let (zencode_id id, lvar_typ lvar, anf binding, anf body, typ_of exp) + AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp) | E_tuple exps -> let aexps = List.map anf exps in @@ -339,10 +407,8 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | E_nondet _ -> (* We don't compile E_nondet nodes *) failwith "encountered E_nondet node when converting to ANF" - - (* + | _ -> failwith ("Cannot convert to ANF: " ^ string_of_exp exp) - *) (**************************************************************************) (* 2. Converting sail types to C types *) @@ -375,7 +441,21 @@ type ctyp = | CT_struct of id * ctyp Bindings.t | CT_enum of id * IdSet.t | CT_variant of id * ctyp Bindings.t - + +type ctx = + { records : (ctyp Bindings.t) Bindings.t; + enums : IdSet.t Bindings.t; + variants : (ctyp Bindings.t) Bindings.t; + tc_env : Env.t + } + +let initial_ctx env = + { records = Bindings.empty; + enums = Bindings.empty; + variants = Bindings.empty; + tc_env = env + } + let ctyp_equal ctyp1 ctyp2 = match ctyp1, ctyp2 with | CT_mpz, CT_mpz -> true @@ -385,6 +465,7 @@ let ctyp_equal ctyp1 ctyp2 = | CT_int64, CT_int64 -> true | CT_unit, CT_unit -> true | CT_bool, CT_bool -> true + | CT_struct (id1, _), CT_struct (id2, _) -> Id.compare id1 id2 = 0 | _, _ -> false let string_of_ctyp = function @@ -397,9 +478,10 @@ let string_of_ctyp = function | CT_int -> "int" | CT_unit -> "unit" | CT_bool -> "bool" + | CT_struct (id, _) -> string_of_id id (* Convert a sail type into a C-type *) -let ctyp_of_typ (Typ_aux (typ_aux, _) as typ) = +let ctyp_of_typ ctx (Typ_aux (typ_aux, _) as typ) = match typ_aux with | Typ_id id when string_of_id id = "bit" -> CT_int | Typ_id id when string_of_id id = "bool" -> CT_bool @@ -426,13 +508,16 @@ let ctyp_of_typ (Typ_aux (typ_aux, _) as typ) = | _ -> CT_bv direction end | Typ_id id when string_of_id id = "unit" -> CT_unit + | Typ_id id when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records) + | _ -> failwith ("No C-type for type " ^ string_of_typ typ) -let is_stack_ctyp ctyp = match ctyp with +let rec is_stack_ctyp ctyp = match ctyp with | CT_uint64 _ | CT_int64 | CT_int | CT_unit | CT_bool -> true | CT_bv _ | CT_mpz -> false + | CT_struct (_, fields) -> Bindings.for_all (fun _ ctyp -> is_stack_ctyp ctyp) fields -let is_stack_typ typ = is_stack_ctyp (ctyp_of_typ typ) +let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ) (**************************************************************************) (* 3. Optimization of primitives and literals *) @@ -445,14 +530,14 @@ let literal_to_cstring (L_aux (l_aux, _) as lit) = | L_hex str when String.length str <= 16 -> let padding = 16 - String.length str in Some ("0x" ^ String.make padding '0' ^ str ^ "ul") - | L_unit -> Some "0" + | L_unit -> Some "UNIT" | L_true -> Some "true" | L_false -> Some "false" | _ -> None -let c_literals = +let c_literals ctx = let c_literal = function - | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ typ) -> + | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ ctx typ) -> begin match literal_to_cstring lit with | Some str -> AV_C_fragment (str, typ) @@ -471,7 +556,7 @@ let mask m = else failwith "Tried to create a mask literal for a vector greater than 64 bits." -let c_aval = function +let c_aval ctx = function | AV_lit (lit, typ) as v -> begin match literal_to_cstring lit with @@ -483,7 +568,7 @@ let c_aval = function | AV_id (id, lvar) as v -> begin match lvar with - | Local (_, typ) when is_stack_typ typ -> + | Local (_, typ) when is_stack_typ ctx typ -> AV_C_fragment (string_of_id id, typ) | _ -> v end @@ -497,7 +582,7 @@ let c_fragment_string = function | AV_C_fragment (str, _) -> str | _ -> assert false -let analyze_primop' id args typ = +let analyze_primop' ctx id args typ = let no_change = AE_app (id, args, typ) in (* primops add_range and add_atom *) @@ -510,7 +595,7 @@ let analyze_primop' id args typ = match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) -> if Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 then - let x, y = c_aval x, c_aval y in + let x, y = c_aval ctx x, c_aval ctx 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, typ)) else @@ -529,7 +614,7 @@ 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) -> - let x, y = c_aval x, c_aval y in + let x, y = c_aval ctx x, c_aval ctx 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, typ)) else @@ -546,7 +631,7 @@ 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) -> - let x, y = c_aval x, c_aval y in + let x, y = c_aval ctx x, c_aval ctx 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)) else @@ -557,15 +642,20 @@ let analyze_primop' id args typ = else no_change -let analyze_primop id args typ = +let analyze_primop ctx id args typ = let no_change = AE_app (id, args, typ) in - try analyze_primop' id args typ with + try analyze_primop' ctx id args typ with | Failure _ -> no_change (**************************************************************************) (* 4. Conversion to low-level AST *) (**************************************************************************) +type ctype_def = + | CTD_enum of id * IdSet.t + | CTD_record of id * ctyp Bindings.t + | CTD_variant of id * ctyp Bindings.t + type cval = | CV_id of id * ctyp | CV_C_fragment of string * ctyp @@ -582,6 +672,7 @@ type instr = | I_funcall of id * id * cval list * ctyp | I_convert of id * ctyp * id * ctyp | I_assign of id * cval + | I_copy of id * cval | I_clear of ctyp * id | I_return of id | I_comment of string @@ -589,6 +680,7 @@ type instr = type cdef = | CDEF_reg_dec of ctyp * id | CDEF_fundef of id * id list * instr list + | CDEF_type of ctype_def let pp_ctyp ctyp = string (string_of_ctyp ctyp |> Util.yellow |> Util.clear) @@ -623,39 +715,41 @@ let rec pp_instr = function string "->"; pp_ctyp ctyp1 ] | I_assign (id, cval) -> separate space [pp_id id; string ":="; pp_cval cval] + | I_copy (id, cval) -> + separate space [string "let"; pp_id id; string "="; pp_cval cval] | I_clear (ctyp, id) -> pp_keyword "CLEAR" ^^ pp_ctyp ctyp ^^ parens (pp_id id) | I_return id -> pp_keyword "RETURN" ^^ pp_id id | I_comment str -> string ("// " ^ str) - -let compile_funcall env id args typ = + +let compile_funcall ctx id args typ = let setup = ref [] in let cleanup = ref [] in - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id env in + let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_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_ctyps, ret_ctyp = List.map ctyp_of_typ arg_typs, ctyp_of_typ ret_typ in - let final_ctyp = ctyp_of_typ typ in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in + let final_ctyp = ctyp_of_typ ctx typ in let setup_arg ctyp aval = match aval with | AV_C_fragment (c, typ) -> if is_stack_ctyp ctyp then - CV_C_fragment (c, ctyp_of_typ typ) + CV_C_fragment (c, ctyp_of_typ ctx typ) else let gs = gensym () in setup := I_decl (ctyp, gs) :: !setup; - setup := I_init (ctyp, gs, CV_C_fragment (c, ctyp_of_typ typ)) :: !setup; + setup := I_init (ctyp, gs, CV_C_fragment (c, ctyp_of_typ ctx typ)) :: !setup; cleanup := I_clear (ctyp, gs) :: !cleanup; CV_id (gs, ctyp) | AV_id (id, lvar) -> - let have_ctyp = ctyp_of_typ (lvar_typ lvar) in + let have_ctyp = ctyp_of_typ ctx (lvar_typ lvar) in if ctyp_equal ctyp have_ctyp then CV_id (id, ctyp) else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then @@ -665,7 +759,7 @@ let compile_funcall env id args typ = cleanup := I_clear (ctyp, gs) :: !cleanup; CV_id (gs, ctyp) else - CV_id (mk_id ("????" ^ string_of_ctyp (ctyp_of_typ (lvar_typ lvar))), ctyp) + CV_id (mk_id ("????" ^ string_of_ctyp (ctyp_of_typ ctx (lvar_typ lvar))), ctyp) | _ -> CV_id (mk_id "???", ctyp) in @@ -686,9 +780,9 @@ let compile_funcall env id args typ = (List.rev !setup, final_ctyp, call, !cleanup) -let rec compile_aexp env = function +let rec compile_aexp ctx = function | AE_let (id, _, binding, body, typ) -> - let setup, ctyp, call, cleanup = compile_aexp env binding in + let setup, ctyp, call, cleanup = compile_aexp ctx binding in let letb1, letb1c = if is_stack_ctyp ctyp then [I_decl (ctyp, id); call id], [] @@ -696,38 +790,38 @@ let rec compile_aexp env = function [I_alloc (ctyp, id); call id], [I_clear (ctyp, id)] in let letb2 = setup @ letb1 @ cleanup in - let setup, ctyp, call, cleanup = compile_aexp env body in + let setup, ctyp, call, cleanup = compile_aexp ctx body in letb2 @ setup, ctyp, call, cleanup @ letb1c | AE_app (id, vs, typ) -> - compile_funcall env id vs typ + compile_funcall ctx id vs typ | AE_val (AV_C_fragment (c, typ)) -> - let ctyp = ctyp_of_typ typ in - [], ctyp, (fun id -> I_assign (id, CV_C_fragment (c, ctyp))), [] - + let ctyp = ctyp_of_typ ctx typ in + [], ctyp, (fun id -> I_copy (id, CV_C_fragment (c, ctyp))), [] + | AE_val (AV_id (id, lvar)) -> - let ctyp = ctyp_of_typ (lvar_typ lvar) in - [], ctyp, (fun id' -> I_assign (id', CV_id (id, ctyp))), [] + let ctyp = ctyp_of_typ ctx (lvar_typ lvar) in + [], ctyp, (fun id' -> I_copy (id', CV_id (id, ctyp))), [] | AE_val (AV_lit (lit, typ)) -> - let ctyp = ctyp_of_typ typ in + let ctyp = ctyp_of_typ ctx typ in if is_stack_ctyp ctyp then assert false else let gs = gensym () in [I_alloc (ctyp, gs); I_comment "fix literal init"], ctyp, - (fun id -> I_assign (id, CV_id (gs, ctyp))), + (fun id -> I_copy (id, CV_id (gs, ctyp))), [I_clear (ctyp, gs)] | AE_if (aval, then_aexp, else_aexp, if_typ) -> - let if_ctyp = ctyp_of_typ if_typ in + let if_ctyp = ctyp_of_typ ctx if_typ in let compile_branch aexp = - let setup, ctyp, call, cleanup = compile_aexp env aexp in + let setup, ctyp, call, cleanup = compile_aexp ctx aexp in fun id -> setup @ [call id] @ cleanup in - let setup, ctyp, call, cleanup = compile_aexp env (AE_val aval) in + let setup, ctyp, call, cleanup = compile_aexp ctx (AE_val aval) in let gs = gensym () in setup @ [I_decl (ctyp, gs); call gs], if_ctyp, @@ -736,17 +830,30 @@ let rec compile_aexp env = function compile_branch else_aexp id, if_ctyp)), cleanup - + + | AE_record_update (aval, fields, typ) -> + let update_field (prev_setup, prev_calls, prev_cleanup) (field, aval) = + let setup, _, call, cleanup = compile_aexp ctx (AE_val aval) in + prev_setup @ setup, call :: prev_calls, cleanup @ prev_cleanup + in + let setup, calls, cleanup = List.fold_left update_field ([], [], []) (Bindings.bindings fields) in + let ctyp = ctyp_of_typ ctx typ in + let gs = gensym () in + [I_alloc (ctyp, gs)] @ setup @ List.map (fun call -> call gs) calls, + ctyp, + (fun id -> I_copy (id, CV_id (gs, ctyp))), + cleanup @ [I_clear (ctyp, gs)] + | AE_assign (id, assign_typ, aexp) -> (* assign_ctyp is the type of the C variable we are assigning to, ctyp is the type of the C expression being assigned. These may be different. *) - let assign_ctyp = ctyp_of_typ assign_typ in - let setup, ctyp, call, cleanup = compile_aexp env aexp in - let unit_fragment = CV_C_fragment ("0", CT_unit) in + let assign_ctyp = ctyp_of_typ ctx assign_typ in + let setup, ctyp, call, cleanup = compile_aexp ctx aexp in + let unit_fragment = CV_C_fragment ("UNIT", CT_unit) in let comment = "assign " ^ string_of_ctyp assign_ctyp ^ " := " ^ string_of_ctyp ctyp in if ctyp_equal assign_ctyp ctyp then - setup @ [call id], CT_unit, (fun id -> I_assign (id, unit_fragment)), cleanup + setup @ [call id], CT_unit, (fun id -> I_copy (id, unit_fragment)), cleanup else if not (is_stack_ctyp assign_ctyp) && is_stack_ctyp ctyp then let gs = gensym () in setup @ [ I_comment comment; @@ -755,23 +862,23 @@ let rec compile_aexp env = function I_convert (id, assign_ctyp, gs, ctyp) ], CT_unit, - (fun id -> I_assign (id, unit_fragment)), + (fun id -> I_copy (id, unit_fragment)), cleanup else - failwith ("Failure: " ^ comment) - + failwith comment + | AE_block (aexps, aexp, _) -> - let block = compile_block env aexps in - let setup, ctyp, call, cleanup = compile_aexp env aexp in + let block = compile_block ctx aexps in + let setup, ctyp, call, cleanup = compile_aexp ctx aexp in block @ setup, ctyp, call, cleanup - | AE_cast (aexp, typ) -> compile_aexp env aexp + | AE_cast (aexp, typ) -> compile_aexp ctx aexp -and compile_block env = function +and compile_block ctx = function | [] -> [] | exp :: exps -> - let setup, _, call, cleanup = compile_aexp env exp in - let rest = compile_block env exps in + let setup, _, call, cleanup = compile_aexp ctx exp in + let rest = compile_block ctx exps in let gs = gensym () in setup @ [I_decl (CT_unit, gs); call gs] @ cleanup @ rest @@ -781,20 +888,46 @@ let rec pat_ids (P_aux (p_aux, _)) = | P_tup pats -> List.concat (List.map pat_ids pats) | _ -> failwith "Bad pattern" -let compile_def env = function +let compile_type_def ctx (TD_aux (type_def, _)) = + match type_def with + | TD_enum (id, _, ids, _) -> + CTD_enum (id, IdSet.of_list ids), + { ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums } + + | TD_record (id, _, _, ctors, _) -> + let ctors = List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ ctx typ) ctors) Bindings.empty ctors in + CTD_record (id, ctors), + { ctx with records = Bindings.add id ctors ctx.records } + + | TD_variant (id, _, _, tus, _) -> + let compile_tu (Tu_aux (tu_aux, _)) = + match tu_aux with + | Tu_id id -> CT_unit, id + | Tu_ty_id (typ, id) -> ctyp_of_typ ctx typ, id + in + let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in + CTD_variant (id, ctus), + { ctx with variants = Bindings.add id ctus ctx.variants } + + (* Will be re-written before here, see bitfield.ml *) + | TD_bitfield _ -> failwith "Cannot compile TD_bitfield" + (* All type abbreviations will be removed before now. TODO: point to where this is done. *) + | TD_abbrev _ -> failwith "Cannot compile TD_abbrev" + +let compile_def ctx = function | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) -> - [CDEF_reg_dec (ctyp_of_typ typ, id)] + [CDEF_reg_dec (ctyp_of_typ ctx typ, id)], ctx | DEF_reg_dec _ -> failwith "Unsupported register declaration" (* FIXME *) - | DEF_spec _ -> [] + | DEF_spec _ -> [], ctx | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, pexp), _)]), _)) -> begin match pexp with | Pat_aux (Pat_exp (pat, exp), _) -> - let aexp = map_functions analyze_primop (c_literals (anf exp)) in + let aexp = map_functions (analyze_primop ctx) (c_literals ctx (anf exp)) in print_endline (Pretty_print_sail.to_string (pp_aexp aexp)); - let setup, ctyp, call, cleanup = compile_aexp env aexp in + let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let gs = gensym () in let instrs = if is_stack_ctyp ctyp then @@ -802,12 +935,16 @@ let compile_def env = function else assert false in - [CDEF_fundef (id, pat_ids pat, instrs)] + [CDEF_fundef (id, pat_ids pat, instrs)], ctx | _ -> assert false end - | DEF_default _ -> [] - + | DEF_type type_def -> + let tdef, ctx = compile_type_def ctx type_def in + [CDEF_type tdef], ctx + + | DEF_default _ -> [], ctx + | _ -> assert false (**************************************************************************) @@ -817,29 +954,47 @@ let compile_def env = function 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_codegen_id id = string (upper_sgen_id id) + let sgen_ctyp = function - | CT_unit -> "int" + | CT_unit -> "unit" + | CT_int -> "int" + | CT_bool -> "bool" + | CT_uint64 _ -> "uint64_t" + | CT_int64 -> "int64_t" + | CT_mpz -> "mpz_t" + | CT_bv _ -> "bv_t" + | CT_struct (id, _) -> "struct " ^ sgen_id id + | CT_enum (id, _) -> "enum " ^ sgen_id id + | CT_variant (id, _) -> "struct " ^ sgen_id id + +let sgen_ctyp_name = function + | CT_unit -> "unit" | CT_int -> "int" | CT_bool -> "bool" | CT_uint64 _ -> "uint64_t" | CT_int64 -> "int64_t" | CT_mpz -> "mpz_t" | CT_bv _ -> "bv_t" + | CT_struct (id, _) -> sgen_id id + | CT_enum (id, _) -> sgen_id id + | CT_variant (id, _) -> sgen_id id let sgen_cval = function | CV_C_fragment (c, _) -> c - | CV_id (id, _) -> string_of_id id + | CV_id (id, _) -> sgen_id id | _ -> "CVAL??" let rec codegen_instr = function | I_decl (ctyp, id) -> - string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (string_of_id id)) - | I_assign (id, cval) -> + string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + | I_copy (id, cval) -> let ctyp = cval_ctyp cval in if is_stack_ctyp ctyp then - string (Printf.sprintf "%s = %s;" (string_of_id id) (sgen_cval cval)) + string (Printf.sprintf "%s = %s;" (sgen_id id) (sgen_cval cval)) else - string (Printf.sprintf "set_%s(%s, %s);" (sgen_ctyp ctyp) (string_of_id id) (sgen_cval cval)) + string (Printf.sprintf "set_%s(%s, %s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_cval cval)) | I_if (cval, then_instrs, else_instrs, ctyp) -> string "if" ^^ space ^^ parens (string (sgen_cval cval)) ^^ space ^^ surround 2 0 lbrace (separate_map hardline codegen_instr then_instrs) rbrace @@ -848,51 +1003,120 @@ let rec codegen_instr = function | I_funcall (x, f, args, ctyp) -> let args = Util.string_of_list ", " sgen_cval args in if is_stack_ctyp ctyp then - string (Printf.sprintf "%s = %s(%s);" (string_of_id x) (sgen_id f) args) + string (Printf.sprintf "%s = %s(%s);" (sgen_id x) (sgen_id f) args) else - string (Printf.sprintf "%s(%s, %s);" (sgen_id f) (string_of_id x) args) + string (Printf.sprintf "%s(%s, %s);" (sgen_id f) (sgen_id x) args) | I_clear (ctyp, id) -> - string (Printf.sprintf "clear_%s(%s);" (sgen_ctyp ctyp) (string_of_id id)) + string (Printf.sprintf "clear_%s(%s);" (sgen_ctyp_name ctyp) (sgen_id id)) | I_init (ctyp, id, cval) -> string (Printf.sprintf "init_%s_of_%s(%s, %s);" - (sgen_ctyp ctyp) - (sgen_ctyp (cval_ctyp cval)) - (string_of_id id) + (sgen_ctyp_name ctyp) + (sgen_ctyp_name (cval_ctyp cval)) + (sgen_id id) (sgen_cval cval)) | I_alloc (ctyp, id) -> - string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (string_of_id id)) + string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) ^^ hardline - ^^ string (Printf.sprintf "init_%s(%s);" (sgen_ctyp ctyp) (string_of_id id)) + ^^ string (Printf.sprintf "init_%s(%s);" (sgen_ctyp_name ctyp) (sgen_id id)) | I_convert (x, ctyp1, y, ctyp2) -> if is_stack_ctyp ctyp1 then string (Printf.sprintf "%s = convert_%s_of_%s(%s);" - (string_of_id x) - (sgen_ctyp ctyp1) - (sgen_ctyp ctyp2) - (string_of_id y)) + (sgen_id x) + (sgen_ctyp_name ctyp1) + (sgen_ctyp_name ctyp2) + (sgen_id y)) else string (Printf.sprintf "convert_%s_of_%s(%s, %s);" - (sgen_ctyp ctyp1) - (sgen_ctyp ctyp2) - (string_of_id x) - (string_of_id y)) + (sgen_ctyp_name ctyp1) + (sgen_ctyp_name ctyp2) + (sgen_id x) + (sgen_id y)) | I_return id -> - string (Printf.sprintf "return %s;" (string_of_id id)) + string (Printf.sprintf "return %s;" (sgen_id id)) | I_comment str -> string ("/* " ^ str ^ " */") -let codegen_def env = function +let codegen_type_def ctx = function + | CTD_enum (id, ids) -> + string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline + ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id (IdSet.elements ids); rbrace ^^ semi] + + | CTD_record (id, ctors) -> + (* Generate a set_T function for every struct T *) + let codegen_set (id, ctyp) = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop.%s = op.%s;" (sgen_id id) (sgen_id id)) + else + string (Printf.sprintf "set_%s(rop.%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) + in + let codegen_setter id ctors = + string (let n = sgen_id id in Printf.sprintf "void set_%s(struct %s rop, const struct %s op)" n n n) ^^ space + ^^ surround 2 0 lbrace + (separate_map hardline codegen_set (Bindings.bindings ctors)) + rbrace + in + (* Generate an init/clear_T function for every struct T *) + let codegen_field_init f (id, ctyp) = + if not (is_stack_ctyp ctyp) then + [string (Printf.sprintf "%s_%s(op.%s);" f (sgen_ctyp_name ctyp) (sgen_id id))] + else [] + in + let codegen_init f id ctors = + string (let n = sgen_id id in Printf.sprintf "void %s_%s(struct %s op)" f n n) ^^ space + ^^ surround 2 0 lbrace + (separate hardline (Bindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat)) + rbrace + in + (* Generate the struct and add the generated functions *) + let codegen_ctor (id, ctyp) = + string (sgen_ctyp ctyp) ^^ space ^^ codegen_id id + in + string (Printf.sprintf "// struct %s" (string_of_id id)) ^^ hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_ctor (Bindings.bindings ctors) ^^ semi) + rbrace + ^^ semi ^^ twice hardline + ^^ codegen_setter id ctors + ^^ twice hardline + ^^ codegen_init "init" id ctors + ^^ twice hardline + ^^ codegen_init "clear" id ctors + + | CTD_variant (id, tus) -> + let codegen_tu (id, ctyp) = + separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_id id ^^ semi; rbrace] + in + string (Printf.sprintf "// union %s" (string_of_id id)) ^^ hardline + ^^ string "enum" ^^ space + ^^ string ("kind_" ^ sgen_id id) ^^ space + ^^ separate space [lbrace; separate_map (comma ^^ space) (fun id -> string ("Kind_" ^ sgen_id id)) (List.map fst (Bindings.bindings tus)); rbrace ^^ semi] + ^^ hardline ^^ hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate space [string "enum"; string ("kind_" ^ sgen_id id); string "kind" ^^ semi] + ^^ hardline + ^^ string "union" ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_tu (Bindings.bindings tus) ^^ semi) + rbrace + ^^ semi) + rbrace + ^^ semi + +let codegen_def ctx = function | CDEF_reg_dec (ctyp, id) -> - string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline + ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) | CDEF_fundef (id, args, instrs) -> List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) instrs; - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id env in + let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_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_ctyps, ret_ctyp = List.map ctyp_of_typ arg_typs, ctyp_of_typ ret_typ in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in @@ -901,9 +1125,13 @@ let codegen_def env = function ^^ jump 2 2 (separate_map hardline codegen_instr instrs) ^^ hardline ^^ string "}" -let compile_ast env (Defs defs) = - let cdefs = List.concat (List.map (compile_def env) defs) in - let docs = List.map (codegen_def env) cdefs in + | CDEF_type ctype_def -> + codegen_type_def ctx ctype_def + +let compile_ast ctx (Defs defs) = + 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 let preamble = separate hardline [ string "#include \"sail.h\"" ] @@ -919,12 +1147,12 @@ let print_compiled (setup, ctyp, call, cleanup) = print_endline (Pretty_print_sail.to_string (pp_instr (call (mk_id ("?" ^ string_of_ctyp ctyp))))); List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) cleanup -let compile_exp env exp = +let compile_exp ctx exp = let aexp = anf exp in - let aexp = c_literals aexp in - let aexp = map_functions analyze_primop aexp in + let aexp = c_literals ctx aexp in + let aexp = map_functions (analyze_primop ctx) aexp in print_endline "\n###################### COMPILED ######################\n"; - print_compiled (compile_aexp env aexp); + print_compiled (compile_aexp ctx aexp); print_endline "\n###################### ANF ######################\n"; aexp diff --git a/src/isail.ml b/src/isail.ml index 07a72bd2..ffeb1442 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 !interactive_env exp in + let anf = C_backend.compile_exp (C_backend.initial_ctx !interactive_env) exp in print_endline (Pretty_print_sail.to_string (C_backend.pp_aexp anf)) | ":u" | ":unload" -> interactive_ast := Ast.Defs []; diff --git a/src/sail.ml b/src/sail.ml index bbe26a0d..34933def 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -256,7 +256,7 @@ let main() = (if !(opt_print_c) then let ast_c = rewrite_ast_c ast in - C_backend.compile_ast type_envs ast_c + C_backend.compile_ast (C_backend.initial_ctx type_envs) ast_c else ()); (if !(opt_print_lem) then let ast_lem = rewrite_ast_lem ast in diff --git a/src/util.ml b/src/util.ml index e2dc9b9f..b8670b84 100644 --- a/src/util.ml +++ b/src/util.ml @@ -389,12 +389,16 @@ let rec take n xs = match n, xs with | n, (x :: xs) -> x :: take (n - 1) xs let termcode n = "\x1B[" ^ string_of_int n ^ "m" + let bold str = termcode 1 ^ str + +let red str = termcode 91 ^ str let green str = termcode 92 ^ str let yellow str = termcode 93 ^ str -let red str = termcode 91 ^ str -let cyan str = termcode 96 ^ str let blue str = termcode 94 ^ str +let magenta str = termcode 95 ^ str +let cyan str = termcode 96 ^ str + let clear str = str ^ termcode 0 let zchar c = diff --git a/src/util.mli b/src/util.mli index 2b4d2e93..46d99002 100644 --- a/src/util.mli +++ b/src/util.mli @@ -240,6 +240,7 @@ val red : string -> string val yellow : string -> string val cyan : string -> string val blue : string -> string +val magenta : string -> string val clear : string -> string val warn : string -> unit |