rTLabsPrinter.ml

   1 open Extracted.RTLabs_syntax
   2
   3 open Extracted.FrontEndOps
   4
   5 open Extracted.Integers
   6
   7 (*
   8 let n_spaces n = String.make n ' '
   9
  10
  11 let rec print_size = function
  12   | AST.SQ q -> Memory.string_of_quantity q
  13   | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
  14   | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
  15   | AST.SArray (i, se) ->
  16     (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
  17 and print_size_list l =
  18   MiscPottier.string_of_list ", " print_size l
  19
  20 let print_global_size = print_size
  21
  22 let print_data = function
  23 (*
  24   | Data_reserve n -> Printf.sprintf "[%d]" n
  25 *)
  26   | AST.Data_int8 i -> Printf.sprintf "(int8) %d" i
  27   | AST.Data_int16 i -> Printf.sprintf "(int16) %d" i
  28   | AST.Data_int32 i -> Printf.sprintf "%d" i
  29   | AST.Data_float32 f -> Printf.sprintf "%f" f
  30   | AST.Data_float64 f -> Printf.sprintf "(float64) %f" f
  31
  32 let print_datas init =
  33   let rec aux = function
  34     | [] -> ""
  35     | [data] -> print_data data
  36     | data :: datas -> Printf.sprintf "%s, %s" (print_data data) (aux datas)
  37   in
  38   Printf.sprintf "{%s}" (aux init)
  39
  40 let print_datas_opt = function
  41   | None -> ""
  42   | Some init -> " = " ^ (print_datas init)
  43
  44 let print_global n (id, size, init_opt) =
  45   Printf.sprintf "%s\"%s\" : %s%s;\n"
  46     (n_spaces n) id (print_global_size size) (print_datas_opt init_opt)
  47
  48 let print_globals eformat n =
  49   List.iter (fun v -> Eformat.printf eformat "%s" (print_global n v))
  50
  51
  52 let print_reg = Register.print
  53
  54 let print_oreg = function
  55   | None -> "_"
  56   | Some r -> print_reg r
  57
  58 let print_decl (r, t) =
  59   (Primitive.print_type t) ^ " " ^ (Register.print r)
  60
  61 let rec print_args args =
  62   Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
  63
  64 let print_result = function
  65   | None -> "_"
  66   | Some (r, t) -> (Primitive.print_type t) ^ " " ^ (Register.print r)
  67
  68 let print_params r =
  69   Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_decl r)
  70
  71 let print_locals r =
  72   Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_decl r)
  73
  74
  75 let print_cmp = function
  76   | AST.Cmp_eq -> "eq"
  77   | AST.Cmp_ne -> "ne"
  78   | AST.Cmp_gt -> "gt"
  79   | AST.Cmp_ge -> "ge"
  80   | AST.Cmp_lt -> "lt"
  81   | AST.Cmp_le -> "le"
  82
  83 let rec print_size = function
  84   | AST.SQ q -> Memory.string_of_quantity q
  85   | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
  86   | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
  87   | AST.SArray (i, se) ->
  88     (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
  89 and print_size_list l =
  90   MiscPottier.string_of_list ", " print_size l
  91
  92 let print_stacksize = print_size
  93
  94 let print_offset (size, depth) =
  95   (print_size size) ^ ", " ^ (string_of_int depth)
  96
  97 let print_sizeof = print_size
  98
  99 let string_of_signedness = function
 100   | AST.Signed -> "s"
 101   | AST.Unsigned -> "u"
 102
 103 let string_of_int_type (size, sign) =
 104   Printf.sprintf "%d%s" size (string_of_signedness sign)
 105
 106 let print_op2 = function
 107   | AST.Op_add -> "add"
 108   | AST.Op_sub -> "sub"
 109   | AST.Op_mul -> "mul"
 110   | AST.Op_div -> "div"
 111   | AST.Op_divu -> "/u"
 112   | AST.Op_mod -> "mod"
 113   | AST.Op_modu -> "modu"
 114   | AST.Op_and -> "and"
 115   | AST.Op_or -> "or"
 116   | AST.Op_xor -> "xor"
 117   | AST.Op_shl -> "shl"
 118   | AST.Op_shr -> "shr"
 119   | AST.Op_shru -> "shru"
 120   | AST.Op_cmp cmp -> print_cmp cmp
 121   | AST.Op_addp -> "addp"
 122   | AST.Op_subp -> "subp"
 123   | AST.Op_subpp -> "subpp"
 124   | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
 125   | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
 126
 127
 128 (*
 129 let print_addressing = function
 130   | RTLabs.Aindexed off -> Printf.sprintf "{ %s }" (print_offset off)
 131   | RTLabs.Aindexed2 -> "add"
 132   | RTLabs.Aglobal (id, off) ->
 133     Printf.sprintf "{ %s }(\"%s\")" (print_offset off) id
 134   | RTLabs.Abased (id, off) ->
 135     Printf.sprintf "add, { %s }(\"%s\")" (print_offset off) id
 136   | RTLabs.Ainstack off -> Printf.sprintf "{ %s }(STACK)" (print_offset off)
 137 *)
 138
 139
 140 let rec print_table = function
 141   | [] -> ""
 142   | [lbl] -> lbl
 143   | lbl :: tbl -> lbl ^ ", " ^ (print_table tbl)
 144 *)
 145 (* Duplicated, also in cerco.ml! *)
 146 let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
 147
 148 let print_identifier pref n = pref ^ "_" ^ string_of_pos n
 149
 150 let print_fun_ident = print_identifier "fun"
 151 let print_ident = print_identifier "id"
 152 let print_label = print_identifier "l"
 153 let print_reg = print_identifier "r"
 154 let print_cost = print_identifier "k"
 155
 156 let print_nat n = string_of_int (Extracted.Glue.int_of_matitanat n)
 157
 158 let print_ubv bv = string_of_int (Extracted.Glue.int_of_bitvector bv)
 159 let print_sbv bv =
 160   let z = Extracted.BitVectorZ.z_of_signed_bitvector Extracted.Nat.O bv in
 161   string_of_int (Extracted.Glue.int_of_matitaZ z)
 162
 163
 164 let print_cst = function
 165 | Ointconst (_, Extracted.AST.Signed, bv) -> print_sbv bv
 166 | Ointconst (_, Extracted.AST.Unsigned, bv) -> print_ubv bv
 167 | Oaddrsymbol (id, off) -> "&" ^ print_ident id ^ " + " ^ print_nat off
 168 | Oaddrstack off -> "SP + " ^ print_nat off
 169
 170 let print_signedness = function
 171   | Extracted.AST.Signed -> ""
 172   | Extracted.AST.Unsigned -> "u"
 173
 174 let print_int_size = function
 175   | Extracted.AST.I8 -> "8"
 176   | Extracted.AST.I16 -> "16"
 177   | Extracted.AST.I32 -> "32"
 178
 179 let print_op1 = function
 180 | Ocastint (src_sy, src_sign, dst_sy, dst_sign) ->
 181   Format.sprintf "(%sint%s->%sint%s)"
 182     (print_signedness src_sign) (print_int_size src_sy)
 183     (print_signedness dst_sign) (print_int_size dst_sy)
 184 | Onegint _ -> "-"
 185 | Onotbool _ -> "!"
 186 | Onotint _ -> "~"
 187 | Oid _ -> ""
 188 | Optrofint (sy, sign) ->
 189   Format.sprintf "(%sint%s->ptr)"
 190     (print_signedness sign) (print_int_size sy)
 191 | Ointofptr (sy, sign) ->
 192   Format.sprintf "(ptr->%sint%s)"
 193     (print_signedness sign) (print_int_size sy)
 194
 195 let print_comparison = function
 196 | Ceq -> "=="
 197 | Cne -> "!="
 198 | Clt -> "<"
 199 | Cle -> "<="
 200 | Cgt -> ">"
 201 | Cge -> ">="
 202
 203 let print_op2 = function
 204 | Oadd _ -> "+"
 205 | Osub _ -> "-"
 206 | Omul _ -> "*"
 207 | Odiv _ -> "/"
 208 | Odivu _ -> "/u"
 209 | Omod _ -> "%"
 210 | Omodu _ -> "%u"
 211 | Oand _ -> "&&"
 212 | Oor _ -> "||"
 213 | Oxor _ -> "^^"
 214 | Oshl _ -> "<<"
 215 | Oshr _ -> ">>"
 216 | Oshru _ -> ">>u"
 217 | Ocmp (_, _, _, cmp) -> print_comparison cmp
 218 | Ocmpu (_, _, cmp) ->  print_comparison cmp ^ "u"
 219 | Oaddpi _ -> "p+"
 220 | Oaddip _ -> "+p"
 221 | Osubpi _ -> "p-"
 222 | Osubpp _ -> "p-p"
 223 | Ocmpp (_, cmp) -> print_comparison cmp ^ "p"
 224
 225 let rec get_list = function
 226   | Extracted.List.Nil -> [ ]
 227   | Extracted.List.Cons (hd, tl) -> hd :: get_list tl
 228
 229 let print_regs regs =
 230   String.concat ", " (List.map print_reg (get_list regs))
 231
 232 let print_statement = function
 233   | St_skip lbl -> "--> " ^ print_label lbl
 234   | St_cost (cost_lbl, lbl) ->
 235       Printf.sprintf "emit %s --> %s"
 236         (print_cost cost_lbl)
 237         (print_label lbl)
 238   | St_const (_, destr, cst, lbl) ->
 239       Printf.sprintf "%s = %s --> %s"
 240         (print_reg destr)
 241         (print_cst cst)
 242         (print_label lbl)
 243   | St_op1 (_, _, op, dst, src, lbl) ->
 244     Format.sprintf "%s = %s%s --> %s"
 245       (print_reg dst) (print_op1 op) (print_reg src)
 246       (print_label lbl)
 247   | St_op2 (_, _, _, op, dst, src1, src2, lbl) ->
 248     Format.sprintf "%s = %s %s %s --> %s"
 249       (print_reg dst) (print_reg src1) (print_op2 op)
 250       (print_reg src2) (print_label lbl)
 251   | St_load (_, addr, dst, lbl) ->
 252     Format.sprintf "%s = *%s --> %s"
 253       (print_reg dst) (print_reg addr) (print_label lbl)
 254   | St_store (_, addr, src, lbl) ->
 255     Format.sprintf "*%s = %s --> %s"
 256       (print_reg addr) (print_reg src) (print_label lbl)
 257   | St_call_id (id, args, Extracted.Types.Some dst, lbl) ->
 258     Format.sprintf "%s = %s(%s) --> %s"
 259       (print_reg dst) (print_fun_ident id) (print_regs args)
 260       (print_label lbl)
 261   | St_call_id (id, args, Extracted.Types.None, lbl) ->
 262     Format.sprintf "%s(%s) --> %s"
 263       (print_fun_ident id) (print_regs args)
 264       (print_label lbl)
 265   | St_call_ptr (addr, args, Extracted.Types.Some dst, lbl) ->
 266     Format.sprintf "%s = *%s(%s) --> %s"
 267       (print_reg dst) (print_reg addr) (print_regs args)
 268       (print_label lbl)
 269   | St_call_ptr (addr, args, Extracted.Types.None, lbl) ->
 270     Format.sprintf "*%s(%s) --> %s"
 271       (print_reg addr) (print_regs args)
 272       (print_label lbl)
 273   | St_cond (src, l_true, l_false) ->
 274     Format.sprintf "if %s then --> %s else --> %s"
 275       (print_reg src) (print_label l_true) (print_label l_false)
 276   | St_return -> "return"
 277
 278 let next = function
 279   | St_skip lbl
 280   | St_cost (_, lbl)
 281   | St_const (_, _, _, lbl)
 282   | St_op1 (_, _, _, _, _, lbl)
 283   | St_op2 (_, _, _, _, _, _, _, lbl)
 284   | St_load (_, _, _, lbl)
 285   | St_store (_, _, _, lbl)
 286   | St_call_id (_, _, _, lbl)
 287   | St_call_ptr (_, _, _, lbl) -> [lbl]
 288   | St_cond (_, l_true, l_false) -> [l_true ; l_false]
 289   | St_return -> [ ]
 290
 291 let get_bool = function
 292   | Extracted.Bool.True -> true
 293   | Extracted.Bool.False -> false
 294
 295 let rec graph_dfs_aux f acc visiting visited graph =
 296   match visiting with
 297   | [ ] -> acc
 298   | hd :: tl ->
 299     let tag = Extracted.PreIdentifiers.LabelTag in
 300     if get_bool (Extracted.Identifiers.member tag visited hd) then
 301       graph_dfs_aux f acc tl visited graph
 302     else
 303       let visited = Extracted.Identifiers.add_set tag visited hd in
 304       match Extracted.Identifiers.lookup tag graph hd with
 305       | Extracted.Types.Some s ->
 306         let acc = f hd s acc in
 307         let visiting = next s @ tl in
 308         graph_dfs_aux f acc visiting visited graph
 309       | Extracted.Types.None ->
 310         graph_dfs_aux f acc tl visited graph
 311
 312 let graph_dfs f init entry =
 313   graph_dfs_aux f init [entry]
 314     (Extracted.Identifiers.empty_set Extracted.PreIdentifiers.LabelTag)
 315
 316 let print_internal_function id def =
 317   let regs = Extracted.List.map Extracted.Types.fst def.f_params in
 318   let pre = Format.sprintf "def %s(%s):"
 319     (print_fun_ident id) (print_regs regs) in
 320   graph_dfs
 321     (fun lbl s acc ->
 322       Format.sprintf "%s\n  %s: %s" acc (print_label lbl) (print_statement s))
 323     pre def.f_entry def.f_graph
 324
 325 let print_external_function id _ =
 326   Format.sprintf "ext %s" (print_fun_ident id)
 327
 328 let print_function = function
 329   | { Extracted.Types.fst = id ;
 330       Extracted.Types.snd = Extracted.AST.Internal def } ->
 331     print_internal_function id def
 332   | { Extracted.Types.fst = id ;
 333       Extracted.Types.snd = Extracted.AST.External def } ->
 334     print_external_function id def
 335
 336 let print_program prog =
 337   let functs = get_list (prog.Extracted.AST.prog_funct) in
 338   String.concat "\n\n" (List.map print_function functs)