src/clight/runtime.ml

   1
   2 (** This module adds runtime functions in a [Clight] program. These functions
   3     implement unsupported functions by the target architecture that introduce a
   4     branch. We need to define them at the [Clight] level in order to have a
   5     correct labelling. *)
   6
   7
   8 let error_prefix = "Adding runtime functions"
   9 let error = Error.global_error error_prefix
  10
  11 let add_program p s =
  12   let output = s ^ (ClightPrinter.print_program p) in
  13   ClightParser.process (`Source ("add_program",  output))
  14
  15 type operation =
  16   | Unary of Clight.unary_operation * Clight.ctype
  17   | Binary of Clight.binary_operation * Clight.ctype * Clight.ctype
  18   | Cast of Clight.ctype (* destination type *) * Clight.ctype (* source type *)
  19   | Fun of string (* name of the function *)
  20
  21 type op_replacement =
  22     (* operation to be replaced *)
  23     operation *
  24     (* base name of the replacement function *)
  25     string *
  26     (* C definition of the replacement function, provided a name for the
  27        function *)
  28     (string -> string) *
  29     (* dependencies *)
  30     operation list
  31
  32 let string_of_operation = function
  33   | Unary (unop, ctype) ->
  34     (ClightPrinter.string_of_unop unop) ^ "(" ^
  35       (ClightPrinter.string_of_ctype ctype) ^ ")"
  36   | Binary (binop, ctype1, ctype2) ->
  37     (ClightPrinter.string_of_binop binop) ^ "(" ^
  38       (ClightPrinter.string_of_ctype ctype1) ^ ", " ^
  39       (ClightPrinter.string_of_ctype ctype1) ^ ")"
  40   | Cast (ctype1, ctype2) ->
  41     "Cast " ^ (ClightPrinter.string_of_ctype ctype1) ^ " " ^
  42       (ClightPrinter.string_of_ctype ctype2)
  43   | Fun fun_name -> "Fun " ^ fun_name
  44
  45 let string_of_op_replacement (replaced, base_name, c_def, _) =
  46   Printf.sprintf "Replaced: %s\n%s\n"
  47     (string_of_operation replaced) (c_def base_name)
  48
  49 module CtypeSet =
  50   Set.Make (struct type t = Clight.ctype let compare = Pervasives.compare end)
  51
  52
  53 let deps op replacements =
  54   let f res (op', _, _, deps) = if op' = op then deps else res in
  55   List.fold_left f [] replacements
  56
  57
  58 (* Filter used operations only *)
  59
  60 module OperationSet =
  61   Set.Make (struct type t = operation let compare = Pervasives.compare end)
  62
  63 let union_list l = List.fold_left OperationSet.union OperationSet.empty l
  64
  65 let f_ctype ctype _ = ctype
  66
  67 let f_expr e _ sub_expr_descrs_res =
  68   let res_e = match e with
  69     | Clight.Expr (Clight.Evar x, Clight.Tfunction _) ->
  70       OperationSet.singleton (Fun x)
  71     | _ -> OperationSet.empty in
  72   union_list (res_e :: sub_expr_descrs_res)
  73
  74 let f_expr_descr ed _ sub_exprs_res =
  75   let res_ed = match ed with
  76     | Clight.Eunop (unop, Clight.Expr (_, t)) ->
  77       OperationSet.singleton (Unary (unop, t))
  78     | Clight.Ebinop (binop, Clight.Expr (_, t1), Clight.Expr (_, t2)) ->
  79       OperationSet.singleton (Binary (binop, t1, t2))
  80     | Clight.Ecast (t, Clight.Expr (_, t')) ->
  81       OperationSet.singleton (Cast (t, t'))
  82     | _ -> OperationSet.empty in
  83   union_list (res_ed :: sub_exprs_res)
  84
  85 let f_stmt _ sub_exprs_res sub_stmts_res =
  86   OperationSet.union (union_list sub_exprs_res) (union_list sub_stmts_res)
  87
  88 let used_ops_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
  89
  90 let used_ops_fundef = function
  91   | Clight.Internal cfun -> used_ops_stmt cfun.Clight.fn_body
  92   | Clight.External _ -> OperationSet.empty
  93
  94 let used_ops p =
  95   let f ops (_, fundef) = OperationSet.union ops (used_ops_fundef fundef) in
  96   List.fold_left f OperationSet.empty p.Clight.prog_funct
  97
  98
  99 let mem_replacements op =
 100   let f res (op', _, _, _) = res || (op' = op) in
 101   List.fold_left f false
 102
 103 let rec fix equal next x =
 104   let y = next x in
 105   if equal x y then x
 106   else fix equal next y
 107
 108 let needed_replacements used_ops replacements =
 109   let f op = mem_replacements op replacements in
 110   let reduced_used_ops = OperationSet.filter f used_ops in
 111   let next_ops ops =
 112     let add ops op = OperationSet.add op ops in
 113     let f op next_ops = List.fold_left add next_ops (deps op replacements) in
 114     OperationSet.fold f ops ops in
 115   let needed_ops = fix OperationSet.equal next_ops reduced_used_ops in
 116   let f (op, _, _, _) = OperationSet.mem op needed_ops in
 117   List.filter f replacements
 118
 119
 120 let map_fresh_name unique map base_name =
 121   if StringTools.Map.mem base_name map then
 122     (map, StringTools.Map.find base_name map)
 123   else
 124     let fresh_name = unique base_name in
 125     (StringTools.Map.add base_name fresh_name map, fresh_name)
 126
 127 let fresh_replacements unique replacements =
 128   let f (map, l) (op, base_name, new_fun, deps) =
 129     let (map, fresh_name) = map_fresh_name unique map base_name in
 130     (map, l @ [(op, fresh_name, new_fun fresh_name, deps)]) in
 131   snd (List.fold_left f (StringTools.Map.empty, []) replacements)
 132
 133
 134 let add_replacements replacements p =
 135   let f_replacements s (_, _, new_fun, _) = s ^ "\n" ^ new_fun in
 136   let added_string = List.fold_left f_replacements "" replacements in
 137   add_program p added_string
 138
 139
 140 let make_replacement_assoc = List.map (fun (op, name, _, _) -> (op, name))
 141
 142
 143 let add p replacements =
 144   let used_ops = used_ops p in
 145   let needed_replacements = needed_replacements used_ops replacements in
 146   let unique = StringTools.make_unique (ClightAnnotator.all_idents p) in
 147   let replacements = fresh_replacements unique needed_replacements in
 148   let p = add_replacements replacements p in
 149   (p, make_replacement_assoc replacements)
 150
 151
 152 (* Replacement *)
 153
 154 let seq =
 155   List.fold_left
 156     (fun stmt1 stmt2 ->
 157       if stmt1 = Clight.Sskip then stmt2
 158       else
 159         if stmt2 = Clight.Sskip then stmt1
 160         else Clight.Ssequence (stmt1, stmt2))
 161     Clight.Sskip
 162
 163 let f_ctype ctype _ = ctype
 164
 165 let call fresh replaced replacement_assoc args ret_type =
 166   let tmp = fresh () in
 167   let replacement_fun_name = List.assoc replaced replacement_assoc in
 168   let tmpe = Clight.Expr (Clight.Evar tmp, ret_type) in
 169   let (args, args_types) = List.split args in
 170   let f_type = Clight.Tfunction (args_types, ret_type) in
 171   let f = Clight.Expr (Clight.Evar replacement_fun_name, f_type) in
 172   let call = Clight.Scall (Some tmpe, f, args) in
 173   (tmpe, call, [(tmp, ret_type)])
 174
 175 let replace_ident replacement_assoc x t =
 176   let new_name = match t with
 177     | Clight.Tfunction _
 178         when List.mem_assoc (Fun x) replacement_assoc ->
 179       let replacement_fun_name = List.assoc (Fun x) replacement_assoc in
 180       replacement_fun_name
 181     | _ -> x in
 182   (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, [])
 183
 184 let f_expr fresh replacement_assoc e _ _ =
 185
 186   let f (Clight.Expr (ed, t) as e) sub_exprs_res =
 187     let f_sub_exprs (es, stmt, tmps) (e, stmt', tmps') =
 188       (es @ [e], seq [stmt ; stmt'], tmps @ tmps') in
 189     let (sub_exprs, stmt1, tmps1) =
 190       List.fold_left f_sub_exprs ([], Clight.Sskip, []) sub_exprs_res in
 191     let (e, stmt2, tmps2) = match ed, sub_exprs with
 192       | Clight.Evar x, _ -> replace_ident replacement_assoc x t
 193       | Clight.Eunop (unop, Clight.Expr (_, t')), e' :: _
 194           when List.mem_assoc (Unary (unop, t')) replacement_assoc ->
 195         call fresh (Unary (unop, t')) replacement_assoc [(e', t')] t
 196       | Clight.Ebinop (binop, Clight.Expr (_, t1), Clight.Expr (_, t2)),
 197         e1 :: e2 :: _
 198           when List.mem_assoc (Binary (binop, t1, t2)) replacement_assoc ->
 199         call fresh (Binary (binop, t1, t2)) replacement_assoc
 200           [(e1, t1) ; (e2, t2)] t
 201       | Clight.Ecast (t, Clight.Expr (_, t')), e' :: _
 202           when List.mem_assoc (Cast (t, t')) replacement_assoc ->
 203         call fresh (Cast (t, t')) replacement_assoc [(e', t')] t
 204       | _ -> (e, Clight.Sskip, []) in
 205     (ClightFold.expr_fill_exprs e sub_exprs,
 206      seq [stmt1 ; stmt2],
 207      tmps1 @ tmps2) in
 208
 209   ClightFold.expr2 f e
 210
 211 let f_expr_descr ed _ _ _ = ed
 212
 213 let f_stmt stmt sub_exprs_res sub_stmts_res =
 214   let f_sub_exprs (es, stmt, tmps) (e, stmt', tmps') =
 215     (es @ [e], seq [stmt ; stmt'], tmps @ tmps') in
 216   let (sub_exprs, added_stmt, tmps1) =
 217     List.fold_left f_sub_exprs ([], Clight.Sskip, []) sub_exprs_res in
 218   let f_sub_stmts (stmts, tmps) (stmt, tmps') =
 219     (stmts @ [stmt], tmps @ tmps') in
 220   let (sub_stmts, tmps2) = List.fold_left f_sub_stmts ([], []) sub_stmts_res in
 221   let stmt' = ClightFold.statement_fill_subs stmt sub_exprs sub_stmts in
 222   (seq [added_stmt ; stmt'], tmps1 @ tmps2)
 223
 224 let replace_statement fresh replacement_assoc =
 225   ClightFold.statement f_ctype (f_expr fresh replacement_assoc)
 226     f_expr_descr f_stmt
 227
 228 let replace_internal fresh replacement_assoc def =
 229   let (new_body, tmps) =
 230     replace_statement fresh replacement_assoc def.Clight.fn_body in
 231   { def with
 232     Clight.fn_vars = def.Clight.fn_vars @ tmps ; Clight.fn_body = new_body }
 233
 234 let replace_funct fresh replacement_assoc (id, fundef) =
 235   let fundef' = match fundef with
 236     | Clight.Internal def ->
 237       Clight.Internal (replace_internal fresh replacement_assoc def)
 238     | _ -> fundef in
 239   (id, fundef')
 240
 241 let replace fresh replacement_assoc p =
 242   let prog_funct =
 243     List.map (replace_funct fresh replacement_assoc) p.Clight.prog_funct in
 244   { p with Clight.prog_funct = prog_funct }
 245
 246
 247 let save_and_parse p =
 248   try
 249     ClightParser.process (`Source ("replaced", ClightPrinter.print_program p))
 250   with Sys_error _ -> failwith "Error reparsing Clight8 transformation."
 251
 252 let add_replacements p replacements =
 253   let p = ClightCasts.simplify p in
 254   let (p, replacement_assoc) = add p replacements in
 255   let p = ClightCasts.simplify p in
 256   let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in
 257   let fresh () = StringTools.Gen.fresh tmp_universe in
 258   let p = replace fresh replacement_assoc p in
 259   let p = save_and_parse p in
 260   ClightCasts.simplify p
 261
 262
 263 (* Unsupported operations by the 8051. *)
 264
 265 let cint size sign = Clight.Tint (size, sign)
 266
 267 let cints size = cint size AST.Signed
 268 let cintu size = cint size AST.Unsigned
 269
 270 let cint8s = cints Clight.I8
 271 let cint8u = cintu Clight.I8
 272 let cint16s = cints Clight.I16
 273 let cint16u = cintu Clight.I16
 274 let cint32s = cints Clight.I32
 275 let cint32u = cintu Clight.I32
 276
 277 let byte_size_of_intsize = function
 278   | Clight.I8 -> 1
 279   | Clight.I16 -> 2
 280   | Clight.I32 -> 4
 281
 282 let bit_size_of_intsize size = (byte_size_of_intsize size) * 8
 283
 284 let string_of_intsize size = string_of_int (bit_size_of_intsize size)
 285
 286 let ctype_of_intsize = function
 287   | Clight.I8 -> "char"
 288   | Clight.I16 -> "short"
 289   | Clight.I32 -> "int"
 290
 291
 292 (* Unsigned divisions and modulos *)
 293
 294 let divumodu_fun res t s =
 295   "unsigned " ^ t ^ " " ^ s ^ " (unsigned " ^ t ^ " x, unsigned " ^ t ^ " y)" ^
 296     "{\n" ^
 297   "  unsigned " ^ t ^ " quo = 0;\n" ^
 298   "  unsigned " ^ t ^ " rem = x;\n" ^
 299   "  while (rem >= y) {\n" ^
 300   "    quo = quo + 1;\n" ^
 301   "    rem = rem - y;\n" ^
 302   "  }\n" ^
 303   "  return (" ^ res ^ ");\n" ^
 304   "}\n\n"
 305
 306 let divumodu op sizes sizec t =
 307   let (prefix, res) = match op with
 308     | Clight.Odiv -> ("div", "quo")
 309     | Clight.Omod -> ("mod", "rem")
 310     | _ -> assert false (* do not use on these arguments *) in
 311   let cu = cintu sizec in
 312   (Binary (op, cu, cu), "_" ^ prefix ^ sizes ^ "u", divumodu_fun res t, [])
 313
 314 let divu = divumodu Clight.Odiv
 315 let modu = divumodu Clight.Omod
 316
 317
 318 (* Unsigned divisions *)
 319
 320 (* 16 bits unsigned division *)
 321
 322 let div16u = divu "16" Clight.I16 "short"
 323
 324 (* 32 bits unsigned division *)
 325
 326 let div32u = divu "32" Clight.I32 "int"
 327
 328 (* Signed divisions *)
 329
 330 let divs_fun t s =
 331   "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
 332   "  unsigned " ^ t ^ " x1 = (unsigned " ^ t ^ ") x;\n" ^
 333   "  unsigned " ^ t ^ " y1 = (unsigned " ^ t ^ ") y;\n" ^
 334   "  signed " ^ t ^ " sign = 1;\n" ^
 335   "  if (x < 0) { x1 = (unsigned " ^ t ^ ") (-x); sign = -sign; }\n" ^
 336   "  if (y < 0) { y1 = (unsigned " ^ t ^ ") (-y); sign = -sign; }\n" ^
 337   "  unsigned " ^ t ^ " res = (x1/y1);\n" ^
 338   "  return (sign * ((signed " ^ t ^ ") res));\n" ^
 339   "}\n\n"
 340
 341 let divs sizes sizec t =
 342   let cs = cints sizec in
 343   let cu = cintu sizec in
 344   (Binary (Clight.Odiv, cs, cs), "_div" ^ sizes ^ "s", divs_fun t,
 345    [Binary (Clight.Odiv, cu, cu)])
 346
 347 (* 8 bits signed division *)
 348
 349 let div8s = divs "8" Clight.I8 "char"
 350
 351 (* 16 bits signed division *)
 352
 353 let div16s = divs "16" Clight.I16 "short"
 354
 355 (* 32 bits signed division *)
 356
 357 let div32s = divs "32" Clight.I32 "int"
 358
 359
 360 (* Unsigned modulos *)
 361
 362 (* 16 bits unsigned modulo *)
 363
 364 let mod16u = modu "16" Clight.I16 "short"
 365
 366 (* 32 bits unsigned modulo *)
 367
 368 let mod32u = modu "32" Clight.I32 "int"
 369
 370 (* Signed modulos *)
 371
 372 let mods_fun t s =
 373   "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
 374   "  return (x - (x/y) * y);\n" ^
 375   "}\n\n"
 376
 377 let mods size ct t =
 378   (Binary (Clight.Omod, ct, ct), "_mod" ^ size ^ "s", mods_fun t,
 379    [Binary (Clight.Odiv, ct, ct)])
 380
 381 (* 8 bits signed modulo *)
 382
 383 let mod8s = mods "8" cint8s "char"
 384
 385 (* 16 bits signed modulo *)
 386
 387 let mod16s = mods "16" cint16s "short"
 388
 389 (* 32 bits signed modulo *)
 390
 391 let mod32s = mods "32" cint32s "int"
 392
 393
 394 (* Shifts *)
 395
 396 let sh_fun op t s =
 397   t ^ " " ^ s ^ " (" ^ t ^ " x, " ^ t ^ " y) {\n" ^
 398   "  " ^ t ^ " res = x, i;\n" ^
 399   "  for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^
 400   "  return res;\n" ^
 401   "}\n\n"
 402
 403 let sh cop sop direction deps size sign =
 404   let sizes = string_of_intsize size in
 405   let ct = Clight.Tint (size, sign) in
 406   let (short_sign, long_sign) = match sign with
 407     | AST.Signed -> ("s", "signed ")
 408     | AST.Unsigned -> ("u", "unsigned ") in
 409   let t = long_sign ^ (ctype_of_intsize size) in
 410   (Binary (cop, ct, ct), "_sh" ^ direction ^ sizes ^ short_sign,
 411    sh_fun sop t, deps)
 412
 413
 414 (* Shift lefts *)
 415
 416 let shl = sh Clight.Oshl "*" "l" []
 417
 418 (* Signed shift lefts *)
 419
 420 (* 8 bits signed shift left *)
 421
 422 let shl8s = shl Clight.I8 AST.Signed
 423
 424 (* 16 bits signed shift left *)
 425
 426 let shl16s = shl Clight.I16 AST.Signed
 427
 428 (* 32 bits signed shift left *)
 429
 430 let shl32s = shl Clight.I32 AST.Signed
 431
 432 (* Unsigned shift lefts *)
 433
 434 (* 8 bits unsigned shift left *)
 435
 436 let shl8u = shl Clight.I8 AST.Unsigned
 437
 438 (* 16 bits unsigned shift left *)
 439
 440 let shl16u = shl Clight.I16 AST.Unsigned
 441
 442 (* 32 bits unsigned shift left *)
 443
 444 let shl32u = shl Clight.I32 AST.Unsigned
 445
 446
 447 (* Shift rights *)
 448
 449 (* Signed shift rights *)
 450
 451 let shrs_fun size t s =
 452   "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
 453   "  unsigned " ^ t ^ " x1, y1, to_add, res, i;\n" ^
 454   "  if (y < 0) return 0;\n" ^
 455   "  x1 = x; y1 = y; to_add = 1; res = x1;" ^
 456   "  for (i = 0 ; i < " ^ size ^ " ; i++) to_add = to_add * 2;\n" ^
 457   "  to_add = to_add & x1;\n" ^
 458   "  for (i = 0 ; i < y1 ; i++) res = (res / 2) + to_add;\n" ^
 459   "  return ((signed " ^ t ^ ") res);\n" ^
 460   "}\n\n"
 461
 462 let shrs size =
 463   let sizes = string_of_int (bit_size_of_intsize size) in
 464   let op_sizes = string_of_int ((bit_size_of_intsize size) - 1) in
 465   let t = ctype_of_intsize size in
 466   let ct = Clight.Tint (size, AST.Signed) in
 467   let ctdep = Clight.Tint (size, AST.Unsigned) in
 468   (Binary (Clight.Oshr, ct, ct), "_shr" ^ sizes ^ "s", shrs_fun op_sizes t,
 469    [Binary (Clight.Odiv, ctdep, ctdep)])
 470
 471 (* 8 bits signed shift right *)
 472
 473 let shr8s = shrs Clight.I8
 474
 475 (* 16 bits signed shift right *)
 476
 477 let shr16s = shrs Clight.I16
 478
 479 (* 32 bits signed shift right *)
 480
 481 let shr32s = shrs Clight.I32
 482
 483 (* Unsigned shift rights *)
 484
 485 let shru size =
 486   let t_dep = Clight.Tint (size, AST.Unsigned) in
 487   sh Clight.Oshr "/" "r" [Binary (Clight.Odiv, t_dep, t_dep)] size AST.Unsigned
 488
 489 (* 8 bits unsigned shift right *)
 490
 491 let shr8u = shru Clight.I8
 492
 493 (* 16 bits unsigned shift right *)
 494
 495 let shr16u = shru Clight.I16
 496
 497 (* 32 bits unsigned shift right *)
 498
 499 let shr32u = shru Clight.I32
 500
 501
 502 let unsupported =
 503   [div16u ; div32u ; div8s ; div16s ; div32s ;
 504    mod16u ; mod32u ; mod8s ; mod16s ; mod32s ;
 505    shl8s ; shl16s ; shl32s ; shl8u ; shl16u ; shl32u ;
 506    shr8s ; shr16s ; shr32s ; shr8u ; shr16u ; shr32u]
 507
 508
 509 let replace_unsupported p = add_replacements p unsupported