open Extracted.RTLabs_syntax open Extracted.FrontEndOps open Extracted.Integers (* let n_spaces n = String.make n ' ' let rec print_size = function | AST.SQ q -> Memory.string_of_quantity q | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}" | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}" | AST.SArray (i, se) -> (print_size se) ^ "[" ^ (string_of_int i) ^ "]" and print_size_list l = MiscPottier.string_of_list ", " print_size l let print_global_size = print_size let print_data = function (* | Data_reserve n -> Printf.sprintf "[%d]" n *) | AST.Data_int8 i -> Printf.sprintf "(int8) %d" i | AST.Data_int16 i -> Printf.sprintf "(int16) %d" i | AST.Data_int32 i -> Printf.sprintf "%d" i | AST.Data_float32 f -> Printf.sprintf "%f" f | AST.Data_float64 f -> Printf.sprintf "(float64) %f" f let print_datas init = let rec aux = function | [] -> "" | [data] -> print_data data | data :: datas -> Printf.sprintf "%s, %s" (print_data data) (aux datas) in Printf.sprintf "{%s}" (aux init) let print_datas_opt = function | None -> "" | Some init -> " = " ^ (print_datas init) let print_global n (id, size, init_opt) = Printf.sprintf "%s\"%s\" : %s%s;\n" (n_spaces n) id (print_global_size size) (print_datas_opt init_opt) let print_globals eformat n = List.iter (fun v -> Eformat.printf eformat "%s" (print_global n v)) let print_reg = Register.print let print_oreg = function | None -> "_" | Some r -> print_reg r let print_decl (r, t) = (Primitive.print_type t) ^ " " ^ (Register.print r) let rec print_args args = Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args) let print_result = function | None -> "_" | Some (r, t) -> (Primitive.print_type t) ^ " " ^ (Register.print r) let print_params r = Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_decl r) let print_locals r = Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_decl r) let print_cmp = function | AST.Cmp_eq -> "eq" | AST.Cmp_ne -> "ne" | AST.Cmp_gt -> "gt" | AST.Cmp_ge -> "ge" | AST.Cmp_lt -> "lt" | AST.Cmp_le -> "le" let rec print_size = function | AST.SQ q -> Memory.string_of_quantity q | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}" | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}" | AST.SArray (i, se) -> (print_size se) ^ "[" ^ (string_of_int i) ^ "]" and print_size_list l = MiscPottier.string_of_list ", " print_size l let print_stacksize = print_size let print_offset (size, depth) = (print_size size) ^ ", " ^ (string_of_int depth) let print_sizeof = print_size let string_of_signedness = function | AST.Signed -> "s" | AST.Unsigned -> "u" let string_of_int_type (size, sign) = Printf.sprintf "%d%s" size (string_of_signedness sign) let print_op2 = function | AST.Op_add -> "add" | AST.Op_sub -> "sub" | AST.Op_mul -> "mul" | AST.Op_div -> "div" | AST.Op_divu -> "/u" | AST.Op_mod -> "mod" | AST.Op_modu -> "modu" | AST.Op_and -> "and" | AST.Op_or -> "or" | AST.Op_xor -> "xor" | AST.Op_shl -> "shl" | AST.Op_shr -> "shr" | AST.Op_shru -> "shru" | AST.Op_cmp cmp -> print_cmp cmp | AST.Op_addp -> "addp" | AST.Op_subp -> "subp" | AST.Op_subpp -> "subpp" | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p" | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u" (* let print_addressing = function | RTLabs.Aindexed off -> Printf.sprintf "{ %s }" (print_offset off) | RTLabs.Aindexed2 -> "add" | RTLabs.Aglobal (id, off) -> Printf.sprintf "{ %s }(\"%s\")" (print_offset off) id | RTLabs.Abased (id, off) -> Printf.sprintf "add, { %s }(\"%s\")" (print_offset off) id | RTLabs.Ainstack off -> Printf.sprintf "{ %s }(STACK)" (print_offset off) *) let rec print_table = function | [] -> "" | [lbl] -> lbl | lbl :: tbl -> lbl ^ ", " ^ (print_table tbl) *) (* Duplicated, also in cerco.ml! *) let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n) let print_identifier pref n = pref ^ "_" ^ string_of_pos n let print_fun_ident = print_identifier "fun" let print_ident = print_identifier "id" let print_label = print_identifier "l" let print_reg = print_identifier "r" let print_cost = print_identifier "k" let print_nat n = string_of_int (Extracted.Glue.int_of_matitanat n) let print_ubv bv = string_of_int (Extracted.Glue.int_of_bitvector bv) let print_sbv bv = let z = Extracted.BitVectorZ.z_of_signed_bitvector Extracted.Nat.O bv in string_of_int (Extracted.Glue.int_of_matitaZ z) let print_cst = function | Ointconst (_, Extracted.AST.Signed, bv) -> print_sbv bv | Ointconst (_, Extracted.AST.Unsigned, bv) -> print_ubv bv | Oaddrsymbol (id, off) -> "&" ^ print_ident id ^ " + " ^ print_nat off | Oaddrstack off -> "SP + " ^ print_nat off let print_signedness = function | Extracted.AST.Signed -> "" | Extracted.AST.Unsigned -> "u" let print_int_size = function | Extracted.AST.I8 -> "8" | Extracted.AST.I16 -> "16" | Extracted.AST.I32 -> "32" let print_op1 = function | Ocastint (src_sy, src_sign, dst_sy, dst_sign) -> Format.sprintf "(%sint%s->%sint%s)" (print_signedness src_sign) (print_int_size src_sy) (print_signedness dst_sign) (print_int_size dst_sy) | Onegint _ -> "-" | Onotbool _ -> "!" | Onotint _ -> "~" | Oid _ -> "" | Optrofint (sy, sign) -> Format.sprintf "(%sint%s->ptr)" (print_signedness sign) (print_int_size sy) | Ointofptr (sy, sign) -> Format.sprintf "(ptr->%sint%s)" (print_signedness sign) (print_int_size sy) let print_comparison = function | Ceq -> "==" | Cne -> "!=" | Clt -> "<" | Cle -> "<=" | Cgt -> ">" | Cge -> ">=" let print_op2 = function | Oadd _ -> "+" | Osub _ -> "-" | Omul _ -> "*" | Odiv _ -> "/" | Odivu _ -> "/u" | Omod _ -> "%" | Omodu _ -> "%u" | Oand _ -> "&&" | Oor _ -> "||" | Oxor _ -> "^^" | Oshl _ -> "<<" | Oshr _ -> ">>" | Oshru _ -> ">>u" | Ocmp (_, _, _, cmp) -> print_comparison cmp | Ocmpu (_, _, cmp) -> print_comparison cmp ^ "u" | Oaddpi _ -> "p+" | Oaddip _ -> "+p" | Osubpi _ -> "p-" | Osubpp _ -> "p-p" | Ocmpp (_, cmp) -> print_comparison cmp ^ "p" let rec get_list = function | Extracted.List.Nil -> [ ] | Extracted.List.Cons (hd, tl) -> hd :: get_list tl let print_regs regs = String.concat ", " (List.map print_reg (get_list regs)) let print_statement = function | St_skip lbl -> "--> " ^ print_label lbl | St_cost (cost_lbl, lbl) -> Printf.sprintf "emit %s --> %s" (print_cost cost_lbl) (print_label lbl) | St_const (_, destr, cst, lbl) -> Printf.sprintf "%s = %s --> %s" (print_reg destr) (print_cst cst) (print_label lbl) | St_op1 (_, _, op, dst, src, lbl) -> Format.sprintf "%s = %s%s --> %s" (print_reg dst) (print_op1 op) (print_reg src) (print_label lbl) | St_op2 (_, _, _, op, dst, src1, src2, lbl) -> Format.sprintf "%s = %s %s %s --> %s" (print_reg dst) (print_reg src1) (print_op2 op) (print_reg src2) (print_label lbl) | St_load (_, addr, dst, lbl) -> Format.sprintf "%s = *%s --> %s" (print_reg dst) (print_reg addr) (print_label lbl) | St_store (_, addr, src, lbl) -> Format.sprintf "*%s = %s --> %s" (print_reg addr) (print_reg src) (print_label lbl) | St_call_id (id, args, Extracted.Types.Some dst, lbl) -> Format.sprintf "%s = %s(%s) --> %s" (print_reg dst) (print_fun_ident id) (print_regs args) (print_label lbl) | St_call_id (id, args, Extracted.Types.None, lbl) -> Format.sprintf "%s(%s) --> %s" (print_fun_ident id) (print_regs args) (print_label lbl) | St_call_ptr (addr, args, Extracted.Types.Some dst, lbl) -> Format.sprintf "%s = *%s(%s) --> %s" (print_reg dst) (print_reg addr) (print_regs args) (print_label lbl) | St_call_ptr (addr, args, Extracted.Types.None, lbl) -> Format.sprintf "*%s(%s) --> %s" (print_reg addr) (print_regs args) (print_label lbl) | St_cond (src, l_true, l_false) -> Format.sprintf "if %s then --> %s else --> %s" (print_reg src) (print_label l_true) (print_label l_false) | St_return -> "return" let next = function | St_skip lbl | St_cost (_, lbl) | St_const (_, _, _, lbl) | St_op1 (_, _, _, _, _, lbl) | St_op2 (_, _, _, _, _, _, _, lbl) | St_load (_, _, _, lbl) | St_store (_, _, _, lbl) | St_call_id (_, _, _, lbl) | St_call_ptr (_, _, _, lbl) -> [lbl] | St_cond (_, l_true, l_false) -> [l_true ; l_false] | St_return -> [ ] let get_bool = function | Extracted.Bool.True -> true | Extracted.Bool.False -> false let rec graph_dfs_aux f acc visiting visited graph = match visiting with | [ ] -> acc | hd :: tl -> let tag = Extracted.PreIdentifiers.LabelTag in if get_bool (Extracted.Identifiers.member tag visited hd) then graph_dfs_aux f acc tl visited graph else let visited = Extracted.Identifiers.add_set tag visited hd in match Extracted.Identifiers.lookup tag graph hd with | Extracted.Types.Some s -> let acc = f hd s acc in let visiting = next s @ tl in graph_dfs_aux f acc visiting visited graph | Extracted.Types.None -> graph_dfs_aux f acc tl visited graph let graph_dfs f init entry = graph_dfs_aux f init [entry] (Extracted.Identifiers.empty_set Extracted.PreIdentifiers.LabelTag) let print_internal_function id def = let regs = Extracted.List.map Extracted.Types.fst def.f_params in let pre = Format.sprintf "def %s(%s):" (print_fun_ident id) (print_regs regs) in graph_dfs (fun lbl s acc -> Format.sprintf "%s\n %s: %s" acc (print_label lbl) (print_statement s)) pre def.f_entry def.f_graph let print_external_function id _ = Format.sprintf "ext %s" (print_fun_ident id) let print_function = function | { Extracted.Types.fst = id ; Extracted.Types.snd = Extracted.AST.Internal def } -> print_internal_function id def | { Extracted.Types.fst = id ; Extracted.Types.snd = Extracted.AST.External def } -> print_external_function id def let print_program prog = let functs = get_list (prog.Extracted.AST.prog_funct) in String.concat "\n\n" (List.map print_function functs)