summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/c_backend.ml214
1 files changed, 171 insertions, 43 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 028f0146..226dfef1 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -62,13 +62,13 @@ 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_let of id * typ * aexp * aexp * typ
| AE_block of aexp list * aexp * typ
| AE_return of aval * typ
@@ -83,7 +83,7 @@ let rec map_aval f = function
| 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_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2)
| AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ)
| AE_return (aval, typ) -> AE_return (f aval, typ)
@@ -91,7 +91,7 @@ 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_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2)
| 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
@@ -123,15 +123,15 @@ let rec pp_aexp = function
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
+ | AE_let (id, id_typ, binding, body, typ) -> group
begin
match binding with
| AE_let _ ->
- (pp_annot typ (separate space [string "let"; pp_id id; string "="])
+ (pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="])
^^ hardline ^^ nest 2 (pp_aexp binding))
^^ hardline ^^ string "in" ^^ space ^^ pp_aexp body
| _ ->
- pp_annot typ (separate space [string "let"; pp_id id; string "="; pp_aexp binding; string "in"])
+ pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="; pp_aexp binding; string "in"])
^^ hardline ^^ pp_aexp body
end
| AE_block (aexps, aexp, typ) ->
@@ -168,9 +168,9 @@ 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) | AE_cast (_, 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))
+ (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, typ, aexp, x, typ_of exp))
in
match e_aux with
| E_lit lit -> ae_lit lit (typ_of exp)
@@ -184,7 +184,7 @@ let rec anf (E_aux (e_aux, _) as 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
@@ -195,12 +195,12 @@ let rec anf (E_aux (e_aux, _) as 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))
@@ -210,7 +210,9 @@ let rec anf (E_aux (e_aux, _) as exp) =
wrap (AE_return (aval, typ_of exp))
| E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) ->
- AE_let (zencode_id id, anf binding, anf body, typ_of exp)
+ 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)
| E_tuple exps ->
let aexps = List.map anf exps in
@@ -231,47 +233,69 @@ let rec anf (E_aux (e_aux, _) as exp) =
| 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
-let stack_typ (Typ_aux (typ_aux, _) as typ) =
+type ctyp =
+ | CT_mpz
+ | CT_bv of bool
+ | CT_uint64 of int * bool
+ | CT_int
+ | CT_int64
+
+let ctyp_equal ctyp1 ctyp2 =
+ match ctyp1, ctyp2 with
+ | CT_mpz, CT_mpz -> true
+ | CT_bv d1, CT_bv d2 -> d1 = d2
+ | CT_uint64 (m1, d1), CT_uint64 (m2, d2) -> m1 = m2 && d1 = d2
+ | CT_int, CT_int -> true
+ | CT_int64, CT_int64 -> true
+ | _, _ -> false
+
+let string_of_ctyp = function
+ | CT_mpz -> "mpz_t"
+ | CT_bv true -> "bv_t<dec>"
+ | CT_bv false -> "bv_t<inc>"
+ | CT_uint64 (n, true) -> "uint64_t<" ^ string_of_int n ^ ", dec>"
+ | CT_uint64 (n, false) -> "uint64_t<" ^ string_of_int n ^ ", int>"
+ | CT_int64 -> "int64_t"
+ | CT_int -> "int"
+
+(* Convert a sail type into a C-type *)
+let ctyp_of_typ (Typ_aux (typ_aux, _) as typ) =
match typ_aux with
- | Typ_id id when string_of_id id = "bit" -> Some "uint64_t"
+ | Typ_id id when string_of_id id = "bit" -> CT_int
+ | Typ_id id when string_of_id id = "bool" -> CT_int
+ | Typ_id id when string_of_id id = "int" -> CT_mpz
| Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" ->
begin
match destruct_range typ with
- | None -> None
+ | None -> assert false (* Checked if range in guard *)
| Some (n, m) ->
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
- Some "int64_t"
- else
- None
- | _ -> None
+ | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
+ when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
+ CT_int64
+ | _ -> CT_mpz
end
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _); _; _]) when string_of_id id = "vector" ->
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _);
+ Typ_arg_aux (Typ_arg_order ord, _);
+ Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id vtyp_id, _)), _)])
+ when string_of_id id = "vector" && string_of_id vtyp_id = "bit" ->
begin
+ let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
match nexp_simp n with
- | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> Some "uint64_t"
- | _ -> None
+ | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_uint64 (Big_int.to_int n, direction)
+ | _ -> CT_bv direction
end
- | _ -> None
+ | _ -> assert false
-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_ctyp ctyp = match ctyp with
+ | CT_uint64 _ | CT_int64 | CT_int -> true
+ | CT_bv _ | CT_mpz -> false
-let is_stack_typ typ = match stack_typ typ with
- | Some _ -> true
- | None -> false
+let is_stack_typ typ = is_stack_ctyp (ctyp_of_typ typ)
let literal_to_cstring (L_aux (l_aux, _) as lit) =
match l_aux with
@@ -377,6 +401,108 @@ let analyze_primop id args typ =
try analyze_primop' id args typ with
| Failure _ -> no_change
+type cval =
+ | CV_id of id * ctyp
+ | CV_C_fragment of string * ctyp
+
+type instr =
+ | I_alloc of ctyp * id
+ | I_init of ctyp * id * cval
+ | I_assign of id * ctyp * id * cval list * ctyp
+ | I_convert of id * ctyp * id * ctyp
+ | I_clear of ctyp * id
+
+let pp_ctyp ctyp =
+ string (string_of_ctyp ctyp |> Util.yellow |> Util.clear)
+
+let pp_keyword str =
+ string ((str |> Util.red |> Util.clear) ^ "$")
+
+and pp_cval = function
+ | CV_id (id, ctyp) -> parens (pp_ctyp ctyp) ^^ (pp_id id)
+ | CV_C_fragment (str, ctyp) -> parens (pp_ctyp ctyp) ^^ (string (str |> Util.cyan |> Util.clear))
+
+let pp_instr = function
+ | I_alloc (ctyp, id) ->
+ parens (pp_ctyp ctyp) ^^ space ^^ pp_id id
+ | I_init (ctyp, id, aval) ->
+ pp_keyword "INIT" ^^ pp_ctyp ctyp ^^ parens (pp_id id ^^ string ", " ^^ pp_cval aval)
+ | I_assign (x, ctyp1, f, args, ctyp2) ->
+ separate space [ parens (pp_ctyp ctyp1); pp_id x; string ":=";
+ pp_id ~color:Util.red f ^^ parens (separate_map (string ", ") pp_cval args);
+ string "->"; pp_ctyp ctyp2 ]
+ | I_convert (x, ctyp1, y, ctyp2) ->
+ separate space [ parens (pp_ctyp ctyp1); pp_id x; string ":=";
+ pp_keyword "CONVERT" ^^ pp_ctyp ctyp2 ^^ parens (pp_id y) ]
+ | I_clear (ctyp, id) ->
+ pp_keyword "CLEAR" ^^ pp_ctyp ctyp ^^ parens (pp_id id)
+
+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_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 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)
+ else
+ let gs = gensym () in
+ setup := I_alloc (ctyp, gs) :: !setup;
+ setup := I_init (ctyp, gs, CV_C_fragment (c, ctyp_of_typ 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
+ if ctyp_equal ctyp have_ctyp then
+ CV_id (id, ctyp)
+ else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then
+ let gs = gensym () in
+ setup := I_alloc (ctyp, gs) :: !setup;
+ setup := I_init (ctyp, gs, CV_id (id, have_ctyp)) :: !setup;
+ 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 "???", ctyp)
+ in
+
+ let sargs = List.map2 setup_arg arg_ctyps args in
+
+ let call =
+ if ctyp_equal final_ctyp ret_ctyp then
+ fun ret -> I_assign (ret, ctyp_of_typ typ, id, sargs, ret_ctyp)
+ else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then
+ let gs = gensym () in
+ setup := I_alloc (ret_ctyp, gs) :: !setup;
+ setup := I_assign (gs, ret_ctyp, id, sargs, ret_ctyp) :: !setup;
+ cleanup := I_clear (ret_ctyp, gs) :: !cleanup;
+ fun ret -> I_convert (ret, final_ctyp, gs, ret_ctyp)
+ else
+ assert false
+ in
+
+ List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) (List.rev !setup);
+ print_endline (Pretty_print_sail.to_string (pp_instr (call (mk_id "?"))));
+ List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) !cleanup;
+
+ print_string (Util.string_of_list ", " string_of_ctyp arg_ctyps);
+ print_string " => ";
+ print_endline (string_of_ctyp ret_ctyp);
+ print_endline (string_of_ctyp final_ctyp);
+
+ AE_app (id, args, typ)
+
+(*
type allocation =
| Stack of string
| Heap of string
@@ -396,7 +522,7 @@ let choose_allocation typ =
type ccall =
| CCallH of (string -> string)
| CCallS of string
-
+
let compile_funcall env id args typ =
let setup = ref [] in
let cleanup = ref [] in
@@ -429,7 +555,7 @@ let compile_funcall env id args typ =
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
+ string_of_id g
end
| Stack str_s, AV_id (id, typ) -> string_of_id id
| _, AV_id _ -> "AV_id"
@@ -471,12 +597,14 @@ let print_compiled (setup, ctyp, call, cleanup) =
| 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);
+ let _ = map_functions (compile_funcall env) aexp in
+ (* print_compiled (compile_aexp env aexp); *)
aexp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:04:21 +0000