Changeset 2773 for extracted/rTLabsToRTL.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/rTLabsToRTL.ml
r2743 r2773 1 1 open Preamble 2 2 3 open BitVectorTrie 4 3 5 open Graphs 4 6 … … 31 33 open FrontEndOps 32 34 33 open BitVectorTrie34 35 35 open CostLabel 36 36 … … 49 49 open Extralib 50 50 51 open Lists 52 53 open Positive 54 55 open Identifiers 56 57 open Exp 58 59 open Arithmetic 60 61 open Vector 62 63 open Div_and_mod 64 65 open Util 66 67 open FoldStuff 68 69 open BitVector 70 71 open Jmeq 72 73 open Russell 74 75 open List 76 51 77 open Setoids 52 78 … … 54 80 55 81 open Option 56 57 open Lists58 59 open Positive60 61 open Identifiers62 63 open Exp64 65 open Arithmetic66 67 open Vector68 69 open Div_and_mod70 71 open Jmeq72 73 open Russell74 75 open List76 77 open Util78 79 open FoldStuff80 81 open BitVector82 82 83 83 open Extranat … … 152 152 > 'a1) > register_type > 'a1 **) 153 153 let rec register_type_rect_Type4 h_register_int h_register_ptr = function 154  Register_int x_ 20782 > h_register_int x_20782155  Register_ptr (x_ 20784, x_20783) > h_register_ptr x_20784 x_20783154  Register_int x_16092 > h_register_int x_16092 155  Register_ptr (x_16094, x_16093) > h_register_ptr x_16094 x_16093 156 156 157 157 (** val register_type_rect_Type5 : … … 159 159 > 'a1) > register_type > 'a1 **) 160 160 let rec register_type_rect_Type5 h_register_int h_register_ptr = function 161  Register_int x_ 20788 > h_register_int x_20788162  Register_ptr (x_ 20790, x_20789) > h_register_ptr x_20790 x_20789161  Register_int x_16098 > h_register_int x_16098 162  Register_ptr (x_16100, x_16099) > h_register_ptr x_16100 x_16099 163 163 164 164 (** val register_type_rect_Type3 : … … 166 166 > 'a1) > register_type > 'a1 **) 167 167 let rec register_type_rect_Type3 h_register_int h_register_ptr = function 168  Register_int x_ 20794 > h_register_int x_20794169  Register_ptr (x_ 20796, x_20795) > h_register_ptr x_20796 x_20795168  Register_int x_16104 > h_register_int x_16104 169  Register_ptr (x_16106, x_16105) > h_register_ptr x_16106 x_16105 170 170 171 171 (** val register_type_rect_Type2 : … … 173 173 > 'a1) > register_type > 'a1 **) 174 174 let rec register_type_rect_Type2 h_register_int h_register_ptr = function 175  Register_int x_ 20800 > h_register_int x_20800176  Register_ptr (x_ 20802, x_20801) > h_register_ptr x_20802 x_20801175  Register_int x_16110 > h_register_int x_16110 176  Register_ptr (x_16112, x_16111) > h_register_ptr x_16112 x_16111 177 177 178 178 (** val register_type_rect_Type1 : … … 180 180 > 'a1) > register_type > 'a1 **) 181 181 let rec register_type_rect_Type1 h_register_int h_register_ptr = function 182  Register_int x_ 20806 > h_register_int x_20806183  Register_ptr (x_ 20808, x_20807) > h_register_ptr x_20808 x_20807182  Register_int x_16116 > h_register_int x_16116 183  Register_ptr (x_16118, x_16117) > h_register_ptr x_16118 x_16117 184 184 185 185 (** val register_type_rect_Type0 : … … 187 187 > 'a1) > register_type > 'a1 **) 188 188 let rec register_type_rect_Type0 h_register_int h_register_ptr = function 189  Register_int x_ 20812 > h_register_int x_20812190  Register_ptr (x_ 20814, x_20813) > h_register_ptr x_20814 x_20813189  Register_int x_16122 > h_register_int x_16122 190  Register_ptr (x_16124, x_16123) > h_register_ptr x_16124 x_16123 191 191 192 192 (** val register_type_inv_rect_Type4 : … … 239 239 PreIdentifiers.identifier > local_env > Registers.register List.list **) 240 240 let find_local_env r lenv = 241 Option.opt_safe (Identifiers.lookup 0PreIdentifiers.RegisterTag lenv r)241 Option.opt_safe (Identifiers.lookup PreIdentifiers.RegisterTag lenv r) 242 242 243 243 (** val find_local_env_arg : … … 255 255 Joint.params > AST.ident List.list > Nat.nat > Registers.register 256 256 List.list Monad.smax_def__o__monad **) 257 let fresh_registers p g 0n =257 let fresh_registers p g n = 258 258 let f = fun acc > 259 259 Monad.m_bind0 (Monad.smax_def State.state_monad) 260 (TranslateUtils.fresh_register p g 0) (fun m >260 (TranslateUtils.fresh_register p g) (fun m > 261 261 Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons (m, acc))) 262 262 in … … 271 271 (match regs with 272 272  List.Nil > (fun _ > List.Nil) 273  List.Cons (hd 0, tl) >273  List.Cons (hd, tl) > 274 274 (fun _ > 275 List.append (find_local_env hd 0.Types.fst lenv)275 List.append (find_local_env hd.Types.fst lenv) 276 276 (map_list_local_env lenv tl))) __ 277 277 … … 279 279 AST.ident List.list > (Registers.register, AST.typ) Types.prod List.list 280 280 > local_env Monad.smax_def__o__monad **) 281 let initialize_local_env globals registers 0=281 let initialize_local_env globals registers = 282 282 let f = fun r_sig lenv > 283 let { Types.fst = r; Types.snd = sig 1} = r_sig in284 let size = size_of_sig_type sig 1in283 let { Types.fst = r; Types.snd = sig0 } = r_sig in 284 let size = size_of_sig_type sig0 in 285 285 Monad.m_bind0 (Monad.smax_def State.state_monad) 286 286 (fresh_registers (Joint.graph_params_to_params RTL.rTL) globals size) … … 289 289 (Identifiers.add PreIdentifiers.RegisterTag lenv r regs)) 290 290 in 291 Monad.m_fold (Monad.smax_def State.state_monad) f registers 0291 Monad.m_fold (Monad.smax_def State.state_monad) f registers 292 292 (Identifiers.empty_map PreIdentifiers.RegisterTag) 293 293 … … 297 297 (Registers.register, AST.typ) Types.prod Types.option > local_env 298 298 Monad.smax_def__o__monad **) 299 let initialize_locals_params_ret globals locals params 0ret =299 let initialize_locals_params_ret globals locals params ret = 300 300 Obj.magic (fun def > 301 301 (let { Types.fst = def'; Types.snd = lenv } = … … 305 305  Types.None > List.Nil 306 306  Types.Some r_sig > List.Cons (r_sig, List.Nil)) 307 (List.append locals params 0)) def307 (List.append locals params)) def 308 308 in 309 309 (fun _ > 310 let params' = map_list_local_env lenv params 0in310 let params' = map_list_local_env lenv params in 311 311 let ret' = 312 312 (match ret with … … 347 347 (match args with 348 348  List.Nil > (fun _ > List.Nil) 349  List.Cons (hd0, tl) > 350 (fun _ > List.append (find_local_env_arg hd0 env) (rtl_args tl env))) 351 __ 349  List.Cons (hd, tl) > 350 (fun _ > List.append (find_local_env_arg hd env) (rtl_args tl env))) __ 352 351 353 352 (** val vrsplit : … … 372 371 (match l with 373 372  List.Nil > (fun _ > List.Nil) 374  List.Cons (hd 0, tl) >375 (fun _ > List.Cons (hd 0, (list_inject_All_aux tl)))) __373  List.Cons (hd, tl) > 374 (fun _ > List.Cons (hd, (list_inject_All_aux tl)))) __ 376 375 377 376 (** val translate_op : … … 379 378 Joint.psd_argument List.list > Joint.psd_argument List.list > 380 379 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 381 let translate_op globals op 4destrs srcrs1 srcrs2 =380 let translate_op globals op destrs srcrs1 srcrs2 = 382 381 let l = 383 382 List.append 384 (match op 4with383 (match op with 385 384  BackEndOps.Add > List.Nil 386 385  BackEndOps.Addc > List.Cons (Joint.CLEAR_CARRY, List.Nil) … … 389 388  BackEndOps.Or > List.Nil 390 389  BackEndOps.Xor > List.Nil) 391 (Util.map3 (fun x x0 x1 > Joint.OP2 (op 4, x, x0, x1))390 (Util.map3 (fun x x0 x1 > Joint.OP2 (op, x, x0, x1)) 392 391 (Obj.magic destrs) (Obj.magic srcrs1) (Obj.magic srcrs2)) 393 392 in … … 406 405 Joint.psd_argument List.list > Joint.psd_argument List.list > 407 406 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 408 let translate_op_asym_unsigned globals op 4destrs srcrs1 srcrs2 =407 let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 = 409 408 let l = List.length destrs in 410 409 let srcrs1' = … … 416 415 srcrs2 417 416 in 418 translate_op globals op 4destrs srcrs1' srcrs2'417 translate_op globals op destrs srcrs1' srcrs2' 419 418 420 419 (** val nat_to_args : … … 432 431 433 432 (** val size_of_cst : AST.typ > FrontEndOps.constant > Nat.nat **) 434 let size_of_cst typ 0= function433 let size_of_cst typ = function 435 434  FrontEndOps.Ointconst (size, x, x0) > AST.size_intsize size 436 435  FrontEndOps.Oaddrsymbol (x, x0) > Nat.S (Nat.S Nat.O) … … 450 449 (Joint.psd_argument_from_byte b) })) destrs 451 450 (Types.pi1 (split_into_bytes size const))) 452  FrontEndOps.Oaddrsymbol (id, offset 0) >451  FrontEndOps.Oaddrsymbol (id, offset) > 453 452 (fun _ _ > 454 let { Types.fst = r 5; Types.snd = r6} = make_addr destrs in455 List.Cons ((Joint.ADDRESS (id, (Obj.magic r 5), (Obj.magic r6))),453 let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in 454 List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))), 456 455 List.Nil)) 457  FrontEndOps.Oaddrstack offset 0>456  FrontEndOps.Oaddrstack offset > 458 457 (fun _ _ > 459 let { Types.fst = r 5; Types.snd = r6} = make_addr destrs in458 let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in 460 459 List.Cons 461 460 ((let x = Joint.Extension_seq 462 (Obj.magic (RTL.Rtl_stack_address (r 5, r6)))461 (Obj.magic (RTL.Rtl_stack_address (r1, r2))) 463 462 in 464 463 x), List.Nil))) __ __ … … 522 521 List.list **) 523 522 let translate_fill_with_zero globals destrs = 524 let res 1= nat_to_args (List.length destrs) Nat.O in525 translate_move globals destrs res 1523 let res = nat_to_args (List.length destrs) Nat.O in 524 translate_move globals destrs res 526 525 527 526 (** val last : 'a1 List.list > 'a1 Types.option **) 528 527 let rec last = function 529 528  List.Nil > Types.None 530  List.Cons (hd 0, tl) >529  List.Cons (hd, tl) > 531 530 (match tl with 532  List.Nil > Types.Some hd 0531  List.Nil > Types.Some hd 533 532  List.Cons (x, x0) > last tl) 534 533 … … 537 536 Joint.psd_argument List.list > Joint.psd_argument List.list > 538 537 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 539 let translate_op_asym_signed globals op 4destrs srcrs1 srcrs2 =538 let translate_op_asym_signed globals op destrs srcrs1 srcrs2 = 540 539 Bind_new.Bnew (fun tmp1 > Bind_new.Bnew (fun tmp2 > 541 540 let l = List.length destrs in … … 562 561 BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0) 563 562 (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0) 564 (translate_op globals op 4destrs srcrs1init.Types.fst563 (translate_op globals op destrs srcrs1init.Types.fst 565 564 srcrs2init.Types.fst)))) 566 565 … … 661 660 > Registers.register List.list > Registers.register List.list > 662 661 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 663 let translate_op1 globals ty ty' op 4destrs srcrs =664 (match op 4with662 let translate_op1 globals ty ty' op1 destrs srcrs = 663 (match op1 with 665 664  FrontEndOps.Ocastint (x, src_sign, x0, x1) > 666 665 (fun _ _ > translate_cast globals src_sign destrs srcrs) … … 904 903 let translate_lt_signed globals destrs srcrs1 srcrs2 = 905 904 Bind_new.Bnew (fun tmp_last_s1 > Bind_new.Bnew (fun tmp_last_s2 > 906 let p 3= shift_signed globals tmp_last_s1 srcrs1 in907 let new_srcrs1 = (Types.pi1 p 3).Types.fst in908 let shift_srcrs1 = (Types.pi1 p 3).Types.snd in909 let p 4= shift_signed globals tmp_last_s2 srcrs2 in910 let new_srcrs2 = (Types.pi1 p 4).Types.fst in911 let shift_srcrs2 = (Types.pi1 p 4).Types.snd in905 let p1 = shift_signed globals tmp_last_s1 srcrs1 in 906 let new_srcrs1 = (Types.pi1 p1).Types.fst in 907 let shift_srcrs1 = (Types.pi1 p1).Types.snd in 908 let p2 = shift_signed globals tmp_last_s2 srcrs2 in 909 let new_srcrs2 = (Types.pi1 p2).Types.fst in 910 let shift_srcrs2 = (Types.pi1 p2).Types.snd in 912 911 BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l) 913 912 (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l) … … 928 927 Joint.psd_argument List.list > (Registers.register, Joint.joint_seq) 929 928 BindLists.bind_list **) 930 let translate_cmp is_unsigned globals cmp 1destrs srcrs1 srcrs2 =931 match cmp 1with929 let translate_cmp is_unsigned globals cmp destrs srcrs1 srcrs2 = 930 match cmp with 932 931  Integers.Ceq > 933 932 BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2) … … 948 947 Joint.psd_argument List.list > Joint.psd_argument List.list > 949 948 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 950 let translate_op2 globals ty1 ty2 ty3 op 4destrs srcrs1 srcrs2 =951 (match op 4with949 let translate_op2 globals ty1 ty2 ty3 op2 destrs srcrs1 srcrs2 = 950 (match op2 with 952 951  FrontEndOps.Oadd (sz, sg) > 953 952 (fun _ _ _ > translate_op globals BackEndOps.Add destrs srcrs1 srcrs2) … … 1081 1080 Joint.params > AST.ident List.list > (Registers.register, 1082 1081 Joint.joint_seq List.list) Bind_new.bind_new > Blocks.bind_step_block **) 1083 let ensure_bind_step_block p g 0b =1082 let ensure_bind_step_block p g b = 1084 1083 Obj.magic 1085 1084 (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l > 1086 Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g 0l))))1085 Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g l)))) 1087 1086 1088 1087 (** val translate_statement : … … 1106 1105 (translate_cst ty globals cst (find_local_env destr lenv)))); 1107 1106 Types.dpi2 = (Obj.magic lbl') }) 1108  RTLabs_syntax.St_op1 (ty, ty', op 4, destr, srcr, lbl') >1107  RTLabs_syntax.St_op1 (ty, ty', op1, destr, srcr, lbl') > 1109 1108 (fun _ > { Types.dpi1 = (Types.Inl 1110 1109 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals 1111 (translate_op1 globals ty' ty op 4(find_local_env destr lenv)1110 (translate_op1 globals ty' ty op1 (find_local_env destr lenv) 1112 1111 (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') }) 1113  RTLabs_syntax.St_op2 (ty1, ty2, ty3, op 4, destr, srcr1, srcr2, lbl') >1112  RTLabs_syntax.St_op2 (ty1, ty2, ty3, op2, destr, srcr1, srcr2, lbl') > 1114 1113 (fun _ > { Types.dpi1 = (Types.Inl 1115 1114 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals 1116 (translate_op2 globals ty2 ty3 ty1 op 4(find_local_env destr lenv)1115 (translate_op2 globals ty2 ty3 ty1 op2 (find_local_env destr lenv) 1117 1116 (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv)))); 1118 1117 Types.dpi2 = (Obj.magic lbl') }) … … 1198 1197 pr.Types.dpi2 1199 1198 in 1200 Identifiers.foldi 0 PreIdentifiers.LabelTag f_trans1201 def.RTLabs_syntax.f_graphinit')) __1199 Identifiers.foldi PreIdentifiers.LabelTag f_trans def.RTLabs_syntax.f_graph 1200 init')) __ 1202 1201 1203 1202 (** val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program > RTL.rtl_program **)
Note: See TracChangeset
for help on using the changeset viewer.