Changeset 818 for Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml
 Timestamp:
 May 19, 2011, 4:03:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml
r740 r818 12 12 13 13 14 let rec seq = function 15  [] > Clight.Sskip 16  [stmt] > stmt 17  stmt :: l > Clight.Ssequence (stmt, seq l) 18 19 20 let call tmp f_id args_and_type res_type = 14 let error_prefix = "Clight32 to Clight8" 15 let error s = Error.global_error error_prefix s 16 17 18 let cint32s = Clight.Tint (Clight.I32, AST.Signed) 19 let cint32u = Clight.Tint (Clight.I32, AST.Unsigned) 20 let cint8s = Clight.Tint (Clight.I8, AST.Signed) 21 let cint8u = Clight.Tint (Clight.I8, AST.Unsigned) 22 23 24 (* Change the main so that it returns a 8 bits integer. Indeed, 32 bits integers 25 will be replaced by structures, and returning a structure from the main is 26 not Clight compliant. *) 27 28 let main_ret_type = function 29  Clight.Tint (_, AST.Signed) > cint8s 30  Clight.Tint (_, AST.Unsigned) > cint8u 31  _ > error "The main should return an integer which is not the case." 32 33 let f_ctype ctype _ = ctype 34 let f_expr e _ _ = e 35 let f_expr_descr ed _ _ = ed 36 37 let f_stmt ret_type stmt sub_exprs_res sub_stmts_res = 38 match stmt, sub_exprs_res with 39  Clight.Sreturn (Some _), e :: _ > 40 let e' = Clight.Expr (Clight.Ecast (ret_type, e), ret_type) in 41 Clight.Sreturn (Some e') 42  _ > ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res 43 44 let body_returns ret_type = 45 ClightFold.statement f_ctype f_expr f_expr_descr (f_stmt ret_type) 46 47 let fundef_returns_char = function 48  Clight.Internal cfun > 49 let ret_type = main_ret_type cfun.Clight.fn_return in 50 let body = body_returns ret_type cfun.Clight.fn_body in 51 Clight.Internal {cfun with Clight.fn_return = ret_type ; 52 Clight.fn_body = body } 53  Clight.External _ as fundef > fundef 54 55 let main_returns_char p = match p.Clight.prog_main with 56  None > p 57  Some main > 58 let main_def = List.assoc main p.Clight.prog_funct in 59 let main_def = fundef_returns_char main_def in 60 let prog_funct = 61 MiscPottier.update_list_assoc main main_def p.Clight.prog_funct in 62 { p with Clight.prog_funct = prog_funct } 63 64 65 (* Replacement *) 66 67 let seq = 68 List.fold_left 69 (fun stmt1 stmt2 > Clight.Ssequence (stmt1, stmt2)) 70 Clight.Sskip 71 72 let is_complex = function 73  Clight.Tstruct _  Clight.Tunion _ > true 74  _ > false 75 76 let is_subst_complex type_substitutions res_type = 77 if List.mem_assoc res_type type_substitutions then 78 is_complex (List.assoc res_type type_substitutions) 79 else false 80 81 let addrof_with_type e ctype = 82 let ctype = Clight.Tpointer ctype in 83 (Clight.Expr (Clight.Eaddrof e, ctype), ctype) 84 85 let address_if_subst_complex type_substitutions = 86 let f l (e, ctype) = 87 let arg_and_type = 88 if is_subst_complex type_substitutions ctype then addrof_with_type e ctype 89 else (e, ctype) in 90 l @ [arg_and_type] in 91 List.fold_left f [] 92 93 let make_call_struct tmpe res_type f_var args args_types = 94 let (res_e, res_type) = addrof_with_type tmpe res_type in 95 let f_type = Clight.Tfunction (res_type :: args_types, Clight.Tvoid) in 96 let f = Clight.Expr (f_var, f_type) in 97 Clight.Scall (None, f, res_e :: args) 98 99 let make_call_wo_struct tmpe res_type f_var args args_types = 100 let f_type = Clight.Tfunction (args_types, res_type) in 101 let f = Clight.Expr (f_var, f_type) in 102 Clight.Scall (Some tmpe, f, args) 103 104 let make_call type_substitutions tmp f_id args_with_types res_type = 21 105 let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in 22 let (args, args_type) = List.split args_and_type in 106 let args_with_types = 107 address_if_subst_complex type_substitutions args_with_types in 108 let (args, args_types) = List.split args_with_types in 23 109 let f_var = Clight.Evar f_id in 24 let f_type = Clight.Tfunction (args_type, res_type) in 25 let f = Clight.Expr (f_var, f_type) in 26 (tmpe, Clight.Scall (Some tmpe, f, args)) 27 28 let replace_primitives_expression fresh unop_assoc binop_assoc = 29 30 let rec aux e = 31 let Clight.Expr (ed, t) = e in 110 let call = 111 if is_subst_complex type_substitutions res_type then make_call_struct 112 else make_call_wo_struct in 113 (tmpe, call tmpe res_type f_var args args_types) 114 115 let call fresh replaced type_substitutions replacement_assoc 116 args added_stmt added_tmps ret_type = 117 let tmp = fresh () in 118 let replacement_fun_name = List.assoc replaced replacement_assoc in 119 let (tmpe, call) = 120 make_call type_substitutions tmp replacement_fun_name args ret_type in 121 let stmt = seq (added_stmt @ [call]) in 122 (tmpe, stmt, added_tmps @ [(tmp, ret_type)]) 123 124 let replace_ident replacement_assoc x t = 125 let new_name = match t with 126  Clight.Tfunction _ 127 when List.mem_assoc (Runtime.Fun x) replacement_assoc > 128 let replacement_fun_name = List.assoc (Runtime.Fun x) replacement_assoc in 129 replacement_fun_name 130  _ > x in 131 (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, []) 132 133 let replace_expression fresh type_substitutions replacement_assoc e = 134 135 let rec aux (Clight.Expr (ed, t) as e) = 32 136 let expr ed = Clight.Expr (ed, t) in 33 137 match ed with 34 138 35  Clight.Econst_int _  Clight.Econst_float _  Clight.Evar _ 36  Clight.Esizeof _ > 139  Clight.Econst_int _  Clight.Econst_float _  Clight.Esizeof _ > 37 140 (e, Clight.Sskip, []) 38 141 39  Clight.Ederef e > 40 let (e', stmt, tmps) = aux e in 142  Clight.Evar x > replace_ident replacement_assoc x t 143 144  Clight.Ederef e' > 145 let (e', stmt, tmps) = aux e' in 41 146 (expr (Clight.Ederef e'), stmt, tmps) 42 147 43  Clight.Eaddrof e >44 let (e', stmt, tmps) = aux e in148  Clight.Eaddrof e' > 149 let (e', stmt, tmps) = aux e' in 45 150 (expr (Clight.Eaddrof e'), stmt, tmps) 46 151 47  Clight.Eunop (unop, Clight.Expr (ed', t')) 48 when List.mem_assoc (unop, t') unop_assoc > 49 let (e', stmt, tmps) = aux (Clight.Expr (ed', t')) in 50 let tmp = fresh () in 51 let (tmpe, call) = 52 call tmp (List.assoc (unop, t') unop_assoc) [(e', t')] t in 53 let stmt = seq [stmt ; call] in 54 (tmpe, stmt, tmps @ [(tmp, t)]) 55 56  Clight.Ebinop (binop, Clight.Expr (ed1, t1), Clight.Expr (ed2, t2)) 57 when List.mem_assoc (binop, t1, t2) binop_assoc > 58 let (e1, stmt1, tmps1) = aux (Clight.Expr (ed1, t1)) in 59 let (e2, stmt2, tmps2) = aux (Clight.Expr (ed2, t2)) in 60 let tmp = fresh () in 61 let (tmpe, call) = 62 call tmp (List.assoc (binop, t1, t2) binop_assoc) 63 [(e1, t1) ; (e2, t2)] t in 64 let stmt = seq [stmt1 ; stmt2 ; call] in 65 (tmpe, stmt, tmps1 @ tmps2 @ [(tmp, t)]) 66 67  _ > (e, Clight.Sskip, []) (* TODO *) 152  Clight.Eunop (unop, (Clight.Expr (ed', t') as e')) 153 when List.mem_assoc (Runtime.Unary (unop, t')) replacement_assoc > 154 let (e', stmt, tmps) = aux e' in 155 call fresh (Runtime.Unary (unop, t')) 156 type_substitutions replacement_assoc [(e', t')] 157 [stmt] tmps t 158 159  Clight.Eunop (unop, e') > 160 let (e', stmt, tmps) = aux e' in 161 (expr (Clight.Eunop (unop, e')), stmt, tmps) 162 163  Clight.Ebinop (binop, 164 (Clight.Expr (ed1, t1) as e1), 165 (Clight.Expr (ed2, t2) as e2)) 166 when 167 List.mem_assoc (Runtime.Binary (binop, t1, t2)) replacement_assoc > 168 let (e1, stmt1, tmps1) = aux e1 in 169 let (e2, stmt2, tmps2) = aux e2 in 170 call fresh (Runtime.Binary (binop, t1, t2)) 171 type_substitutions replacement_assoc 172 [(e1, t1) ; (e2, t2)] [stmt1 ; stmt2] (tmps1 @ tmps2) t 173 174  Clight.Ebinop (binop, e1, e2) > 175 let (e1, stmt1, tmps1) = aux e1 in 176 let (e2, stmt2, tmps2) = aux e2 in 177 let stmt = seq [stmt1 ; stmt2] in 178 (expr (Clight.Ebinop (binop, e1, e2)), stmt, tmps1 @ tmps2) 179 180  Clight.Ecast (t, (Clight.Expr (_, t') as e')) 181 when List.mem_assoc (Runtime.Cast (t, t')) replacement_assoc > 182 let (e', stmt, tmps) = aux e' in 183 call fresh (Runtime.Cast (t, t')) 184 type_substitutions replacement_assoc [(e', t')] [stmt] 185 tmps t 186 187  Clight.Ecast (t', e') > 188 let (e', stmt, tmps) = aux e' in 189 (expr (Clight.Ecast (t', e')), stmt, tmps) 190 191  Clight.Econdition (e1, e2, e3) > 192 let (e1, stmt1, tmps1) = aux e1 in 193 let (e2, stmt2, tmps2) = aux e2 in 194 let (e3, stmt3, tmps3) = aux e3 in 195 let stmt = seq [stmt1 ; stmt2 ; stmt3] in 196 (expr (Clight.Econdition (e1, e2, e3)), stmt, tmps1 @ tmps2 @ tmps3) 197 198  Clight.Eandbool (e1, e2) > 199 let (e1, stmt1, tmps1) = aux e1 in 200 let (e2, stmt2, tmps2) = aux e2 in 201 let stmt = seq [stmt1 ; stmt2] in 202 (expr (Clight.Eandbool (e1, e2)), stmt, tmps1 @ tmps2) 203 204  Clight.Eorbool (e1, e2) > 205 let (e1, stmt1, tmps1) = aux e1 in 206 let (e2, stmt2, tmps2) = aux e2 in 207 let stmt = seq [stmt1 ; stmt2] in 208 (expr (Clight.Eorbool (e1, e2)), stmt, tmps1 @ tmps2) 209 210  Clight.Efield (e', field) > 211 let (e', stmt, tmps) = aux e' in 212 (expr (Clight.Efield (e', field)), stmt, tmps) 213 214  Clight.Ecost (lbl, e') > 215 let (e', stmt, tmps) = aux e' in 216 (expr (Clight.Ecost (lbl, e')), stmt, tmps) 217 218  Clight.Ecall (id, e1, e2) > 219 let (e1, stmt1, tmps1) = aux e1 in 220 let (e2, stmt2, tmps2) = aux e2 in 221 let stmt = seq [stmt1 ; stmt2] in 222 (expr (Clight.Ecall (id, e1, e2)), stmt, tmps1 @ tmps2) 68 223 69 224 in 70 aux 71 72 73 let replace_ primitives_expression_list fresh unop_assoc binop_assoc =225 aux e 226 227 228 let replace_expression_list fresh type_substitutions replacement_assoc = 74 229 let f (l, stmt, tmps) e = 75 230 let (e', stmt', tmps') = 76 replace_ primitives_expression fresh unop_assoc binop_assoc e in77 (l @ [e ], seq [stmt ; stmt'], tmps @ tmps') in231 replace_expression fresh type_substitutions replacement_assoc e in 232 (l @ [e'], seq [stmt ; stmt'], tmps @ tmps') in 78 233 List.fold_left f ([], Clight.Sskip, []) 79 234 80 235 81 let replace_ primitives_statement fresh unop_assoc binop_assoc =236 let replace_statement fresh type_substitutions replacement_assoc = 82 237 let aux_exp = 83 replace_ primitives_expression fresh unop_assoc binop_assoc in238 replace_expression fresh type_substitutions replacement_assoc in 84 239 let aux_exp_list = 85 replace_ primitives_expression_list fresh unop_assoc binop_assoc in240 replace_expression_list fresh type_substitutions replacement_assoc in 86 241 87 242 let rec aux = function … … 89 244  Clight.Sskip  Clight.Sbreak  Clight.Scontinue  Clight.Sgoto _ 90 245  Clight.Sreturn None 91 246 as stmt > (stmt, []) 92 247 93 248  Clight.Slabel (lbl, stmt) > … … 116 271 let (args', stmt3, tmps3) = aux_exp_list args in 117 272 let stmt = seq [stmt1 ; stmt2 ; stmt3 ; 118 273 Clight.Scall (Some e', f', args')] in 119 274 (stmt, tmps1 @ tmps2 @ tmps3) 120 275 … … 144 299 let (stmt3', tmps3) = aux stmt3 in 145 300 let stmt = seq [stmt1' ; stmte ; 146 Clight.Swhile (e', seq [stmt 2' ; stmt3' ; stmte])] in301 Clight.Swhile (e', seq [stmt3' ; stmt2' ; stmte])] in 147 302 (stmt, tmpse @ tmps1 @ tmps2 @ tmps3) 148 303 … … 180 335 181 336 182 let replace_primitives_internal fresh unop_assoc binop_assoc def = 337 let f_ctype type_substitutions ctype sub_ctypes_res = match ctype with 338  _ when List.mem_assoc ctype type_substitutions > 339 List.assoc ctype type_substitutions 340  _ > ClightFold.ctype_fill_subs ctype sub_ctypes_res 341 342 let replace_ctype type_substitutions = 343 ClightFold.ctype (f_ctype type_substitutions) 344 345 let f_expr = ClightFold.expr_fill_subs 346 347 let f_expr_descr = ClightFold.expr_descr_fill_subs 348 349 let f_stmt = ClightFold.statement_fill_subs 350 351 let statement_replace_ctype type_substitutions = 352 ClightFold.statement (f_ctype type_substitutions) f_expr f_expr_descr f_stmt 353 354 355 let replace_internal fresh type_substitutions replacement_assoc def = 183 356 let (new_body, tmps) = 184 replace_ primitives_statement fresh unop_assoc binop_assoc357 replace_statement fresh type_substitutions replacement_assoc 185 358 def.Clight.fn_body in 186 { def with Clight.fn_vars = def.Clight.fn_vars @ tmps ; 187 Clight.fn_body = new_body } 188 189 let replace_primitives_funct fresh unop_assoc binop_assoc (id, fundef) = 359 let new_body = statement_replace_ctype type_substitutions new_body in 360 let f (x, t) = (x, replace_ctype type_substitutions t) in 361 let params = List.map f def.Clight.fn_params in 362 let vars = List.map f (def.Clight.fn_vars @ tmps) in 363 { Clight.fn_return = replace_ctype type_substitutions def.Clight.fn_return ; 364 Clight.fn_params = params ; 365 Clight.fn_vars = vars ; 366 Clight.fn_body = new_body } 367 368 let replace_funct fresh type_substitutions replacement_assoc (id, fundef) = 190 369 let fundef' = match fundef with 191 370  Clight.Internal def > 192 371 Clight.Internal 193 (replace_ primitives_internal fresh unop_assoc binop_assoc def)372 (replace_internal fresh type_substitutions replacement_assoc def) 194 373  _ > fundef in 195 374 (id, fundef') 196 375 197 let replace _primitives fresh unop_assoc binop_assoc p =376 let replace fresh type_substitutions replacement_assoc p = 198 377 let prog_funct = 199 List.map (replace_ primitives_funct fresh unop_assoc binop_assoc)378 List.map (replace_funct fresh type_substitutions replacement_assoc) 200 379 p.Clight.prog_funct in 201 380 { p with Clight.prog_funct = prog_funct } 202 381 203 382 383 (* The constant replacement replaces each 32 bits and 16 bits integer constant 384 by a global variable of the same value. They will be replaced by the 385 appropriate structural value by the global replacement that comes 386 afterwards. *) 387 388 module CstMap = 389 Map.Make 390 (struct 391 type t = (int * Clight.intsize * Clight.ctype) 392 let compare = Pervasives.compare 393 end) 394 395 let f_subs fresh replace subs map = 396 let f (l, map) x = 397 let (x, map) = replace fresh map x in 398 (l @ [x], map) in 399 List.fold_left f ([], map) subs 400 401 let rec replace_constant_expr fresh map (Clight.Expr (ed, t) as e) = 402 match ed, t with 403  Clight.Econst_int i, Clight.Tint (Clight.I8, _) > 404 (e, map) 405  Clight.Econst_int i, Clight.Tint (size, _) 406 when CstMap.mem (i, size, t) map > 407 let id = CstMap.find (i, size, t) map in 408 (Clight.Expr (Clight.Evar id, t), map) 409  Clight.Econst_int i, Clight.Tint (size, _) > 410 let id = fresh () in 411 let map = CstMap.add (i, size, t) id map in 412 let id = CstMap.find (i, size, t) map in 413 (Clight.Expr (Clight.Evar id, t), map) 414  _ > 415 let (sub_ctypes, sub_exprs) = ClightFold.expr_descr_subs ed in 416 let (sub_exprs, map) = f_subs fresh replace_constant_expr sub_exprs map in 417 let ed = ClightFold.expr_descr_fill_subs ed sub_ctypes sub_exprs in 418 (Clight.Expr (ed, t), map) 419 420 let rec replace_constant_stmt fresh map stmt = 421 let (sub_exprs, sub_stmts) = ClightFold.statement_subs stmt in 422 let (sub_exprs, map) = 423 f_subs fresh replace_constant_expr sub_exprs map in 424 let (sub_stmts, map) = 425 f_subs fresh replace_constant_stmt sub_stmts map in 426 (ClightFold.statement_fill_subs stmt sub_exprs sub_stmts, map) 427 428 let replace_constant_fundef fresh (functs, map) (id, fundef) = 429 match fundef with 430  Clight.Internal cfun > 431 let (body, map) = replace_constant_stmt fresh map cfun.Clight.fn_body in 432 let fundef = Clight.Internal { cfun with Clight.fn_body = body } in 433 (functs @ [(id, fundef)], map) 434  Clight.External _ > (functs @ [(id, fundef)], map) 435 436 let init_datas i size = 437 [match size with 438  Clight.I8 > Clight.Init_int8 i 439  Clight.I16 > Clight.Init_int16 i 440  Clight.I32 > Clight.Init_int32 i] 441 442 let globals_of_map map = 443 let f (i, size, t) id l = l @ [((id, init_datas i size), t)] in 444 CstMap.fold f map [] 445 446 let replace_constant p = 447 let tmp_universe = ClightAnnotator.fresh_universe "_cst" p in 448 let fresh () = StringTools.Gen.fresh tmp_universe in 449 let (functs, map) = 450 List.fold_left (replace_constant_fundef fresh) 451 ([], CstMap.empty) p.Clight.prog_funct in 452 let csts = globals_of_map map in 453 { p with 454 Clight.prog_funct = functs ; Clight.prog_vars = p.Clight.prog_vars @ csts } 455 456 457 (* Globals replacement *) 458 459 let expand_int size i = 460 let i = Big_int.big_int_of_int i in 461 let i = 462 if Big_int.ge_big_int i Big_int.zero_big_int then i 463 else Big_int.add_big_int i (Big_int.power_int_positive_int 2 size) in 464 let bound = Big_int.power_int_positive_int 2 8 in 465 let rec aux n i = 466 if n >= size then [] 467 else 468 let (next, chunk) = Big_int.quomod_big_int i bound in 469 chunk :: (aux (n+1) next) in 470 List.map (fun i > Clight.Init_int8 (Big_int.int_of_big_int i)) (aux 0 i) 471 472 let expand_init_data = function 473  Clight.Init_int16 i > expand_int 2 i 474  Clight.Init_int32 i > expand_int 4 i 475  init_data > [init_data] 476 477 let expand_init_datas init_datas = 478 List.flatten (List.map expand_init_data init_datas) 479 480 let replace_global type_substitutions ((id, init_datas), t) = 481 let init_datas = expand_init_datas init_datas in 482 ((id, init_datas), replace_ctype type_substitutions t) 483 484 let replace_globals type_substitutions p = 485 let vars = List.map (replace_global type_substitutions) p.Clight.prog_vars in 486 { p with Clight.prog_vars = vars } 487 488 489 (* Unsupported operations by the 8051. *) 490 491 (* 8 bits signed division *) 492 493 let divs_fun s _ = 494 "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^ 495 " unsigned char x1 = (unsigned char) x;\n" ^ 496 " unsigned char y1 = (unsigned char) y;\n" ^ 497 " signed char sign = 1;\n" ^ 498 " if (x < 0) { x1 = (unsigned char) (x); sign = sign; }\n" ^ 499 " if (y < 0) { y1 = (unsigned char) (y); sign = sign; }\n" ^ 500 " return (sign * ((signed char) (x1/y1)));\n" ^ 501 "}\n\n" 502 503 let divs = 504 (Runtime.Binary (Clight.Odiv, cint8s, cint8s), "_divs", [], divs_fun, []) 505 506 507 (* 8 bits signed modulo *) 508 509 let mods_fun s _ = 510 "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^ 511 " return (x  (x/y) * y);\n" ^ 512 "}\n\n" 513 514 let mods = 515 (Runtime.Binary (Clight.Omod, cint8s, cint8s), "_mods", [], mods_fun, 516 [Runtime.Binary (Clight.Odiv, cint8s, cint8s)]) 517 518 519 (* Shifts *) 520 521 let sh_fun signedness op s _ = 522 signedness ^ " char " ^ s ^ " (" ^ signedness ^ " char x, " ^ 523 signedness ^ " char y) {\n" ^ 524 " " ^ signedness ^ " char res = x, i;\n" ^ 525 " for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^ 526 " return res;\n" ^ 527 "}\n\n" 528 529 (* 8 bits shifts left *) 530 531 let shls_fun = sh_fun "signed" "*" 532 533 let shls = 534 (Runtime.Binary (Clight.Oshl, cint8s, cint8s), "_shls", [], shls_fun, []) 535 536 let shlu_fun s _ = 537 "unsigned char " ^ s ^ " (unsigned char x, unsigned char y) {\n" ^ 538 " return ((unsigned char) ((signed char) x << (signed char) y));\n" ^ 539 "}\n\n" 540 541 let shlu = 542 (Runtime.Binary (Clight.Oshl, cint8u, cint8u), "_shlu", [], shlu_fun, 543 [Runtime.Binary (Clight.Oshl, cint8s, cint8s)]) 544 545 (* 8 bits shifts right *) 546 547 let shrs_fun s _ = 548 "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^ 549 " signed char res = x, i;\n" ^ 550 " for (i = 0 ; i < y ; i++) {\n" ^ 551 " res = ((unsigned char) res) / 2;\n" ^ 552 " res = res + ((signed char) 128);\n" ^ 553 " }\n" ^ 554 " return res;\n" ^ 555 "}\n\n" 556 557 let shrs = 558 (Runtime.Binary (Clight.Oshr, cint8s, cint8s), "_shrs", [], shrs_fun, []) 559 560 let shru_fun = sh_fun "unsigned" "/" 561 562 let shru = 563 (Runtime.Binary (Clight.Oshr, cint8u, cint8u), "_shru", [], shru_fun, []) 564 565 566 (* int32 *) 567 568 let struct_int32 name fields = match fields with 569  lolo :: lohi :: hilo :: hihi :: _ > 570 Clight.Tstruct 571 (name, 572 [(lolo, cint8u) ; (lohi, cint8u) ; (hilo, cint8u) ; (hihi, cint8u)]) 573  _ > error ("bad field names when defining type " ^ name ^ ".") 574 575 let struct_int32_name = "struct _int32_" 576 577 let new_int32 int32 = 578 let lolo = "lolo" in 579 let lohi = "lohi" in 580 let hilo = "hilo" in 581 let hihi = "hihi" in 582 (int32, struct_int32_name, [lolo ; lohi ; hilo ; hihi], struct_int32) 583 584 let int32s = new_int32 (Clight.Tint (Clight.I32, AST.Signed)) 585 let int32u = new_int32 (Clight.Tint (Clight.I32, AST.Unsigned)) 586 587 (* 32 bits operations *) 588 589 (* 32 bits equality *) 590 591 let eq_int32s_fun s l = 592 let (int32, lolo, lohi, hilo, hihi) = match l with 593  (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ > 594 (int32, lolo, lohi, hilo, hihi) 595  _ > error ("new type definition not coherent in function " ^ s ^ ".") in 596 int32 ^ " " ^ s ^ " (" ^ int32 ^ " x, " ^ int32 ^ " y) {\n" ^ 597 " " ^ int32 ^ " res;\n" ^ 598 " res." ^ lolo ^ " = 1;\n" ^ 599 " if (x." ^ lolo ^ " != y." ^ lolo ^ ") res." ^ lolo ^ " = 0;\n" ^ 600 " if (x." ^ lohi ^ " != y." ^ lohi ^ ") res." ^ lolo ^ " = 0;\n" ^ 601 " if (x." ^ hilo ^ " != y." ^ hilo ^ ") res." ^ lolo ^ " = 0;\n" ^ 602 " if (x." ^ hihi ^ " != y." ^ hihi ^ ") res." ^ lolo ^ " = 0;\n" ^ 603 " res." ^ lohi ^ " = 0;\n" ^ 604 " res." ^ hilo ^ " = 0;\n" ^ 605 " res." ^ hihi ^ " = 0;\n" ^ 606 " return (res);\n" ^ 607 "}\n\n" 608 609 let eq32s = 610 (Runtime.Binary (Clight.Oeq, cint32s, cint32s), "eq_int32s", 611 [struct_int32_name], eq_int32s_fun, []) 612 613 (* 32 bits casts *) 614 615 let int32s_to_int8s_fun s l = 616 let (int32, lolo, lohi, hilo, hihi) = match l with 617  (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ > 618 (int32, lolo, lohi, hilo, hihi) 619  _ > error ("new type definition not coherent in function " ^ s ^ ".") in 620 "signed char " ^ s ^ " (" ^ int32 ^ " x) {\n" ^ 621 " return ((signed char) x." ^ lolo ^ ");\n" ^ 622 "}\n\n" 623 624 let int32s_to_int8s = 625 (Runtime.Cast (cint8s, cint32s), "int32s_to_int8s", [struct_int32_name], 626 int32s_to_int8s_fun, []) 627 628 629 (* int16 *) 630 631 let struct_int16 name fields = match fields with 632  lo :: hi :: _ > 633 Clight.Tstruct (name, [(lo, cint8u) ; (hi, cint8u)]) 634  _ > error ("bad field names when defining type " ^ name ^ ".") 635 636 let struct_int16_name = "struct _int16_" 637 638 let new_int16 int16 = 639 let lo = "lo" in 640 let hi = "hi" in 641 (int16, struct_int16_name, [lo ; hi], struct_int16) 642 643 let int16s = new_int16 (Clight.Tint (Clight.I16, AST.Signed)) 644 let int16u = new_int16 (Clight.Tint (Clight.I16, AST.Unsigned)) 645 646 647 (* int32 and int16 *) 648 649 let int32_and_int16_types = [int32s ; int32u ; int16s ; int16u] 650 let int32_and_int16_replacements = [eq32s ; int32s_to_int8s] 651 652 653 let unsupported = [divs ; mods ; shls ; shlu ; shrs ; shru] 654 655 656 let save_and_parse p = 657 let tmp_file = Filename.temp_file "clight32toclight8" ".c" in 658 try 659 let oc = open_out tmp_file in 660 output_string oc (ClightPrinter.print_program p) ; 661 close_out oc ; 662 let res = ClightParser.process tmp_file in 663 Misc.SysExt.safe_remove tmp_file ; 664 res 665 with Sys_error _ > failwith "Error reparsing Clight8 transformation." 666 667 let add_replacements p new_types replacements = 668 let p = ClightCasts.simplify p in 669 let (p, type_substitutions, replacement_assoc) = 670 Runtime.add p new_types replacements in 671 let p = ClightCasts.simplify p in 672 let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in 673 let fresh () = StringTools.Gen.fresh tmp_universe in 674 let p = replace fresh type_substitutions replacement_assoc p in 675 let p = replace_globals type_substitutions p in 676 (* Printf.printf "%s\n%!" (ClightPrinter.print_program p) ; *) 677 let p = save_and_parse p in 678 ClightCasts.simplify p 679 204 680 let translate p = 205 (* TODO: restore below *) 206 (* 207 let (p, unop_assoc, binop_assoc) = Runtime.add p in 208 let p = ClightCasts.simplify p in 209 let labs = ClightAnnotator.all_labels p in 210 let tmp_prefix = StringTools.Gen.fresh_prefix labs "_tmp" in 211 let tmp_universe = StringTools.Gen.new_universe tmp_prefix in 212 let fresh () = StringTools.Gen.fresh tmp_universe in 213 let p = replace_primitives fresh unop_assoc binop_assoc p in 214 (* TODO: do the translation *) 215 p 216 *) 217 ClightCasts.simplify p 681 let p = main_returns_char p in 682 let p = replace_constant p in 683 let p = 684 add_replacements p int32_and_int16_types int32_and_int16_replacements in 685 add_replacements p [] unsupported
Note: See TracChangeset
for help on using the changeset viewer.