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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/rTLToERTL.ml
r2730 r2773 17 17 open Extralib 18 18 19 open Lists 20 21 open Positive 22 23 open Identifiers 24 25 open Registers 26 27 open Exp 28 19 29 open Setoids 20 30 … … 23 33 open Option 24 34 25 open Lists26 27 open Positive28 29 open Identifiers30 31 open Registers32 33 open Exp34 35 35 open Extranat 36 36 … … 81 81 open LabelledObjects 82 82 83 open BitVectorTrie 84 83 85 open Graphs 84 85 open BitVectorTrie86 86 87 87 open CostLabel … … 146 146 AST.ident List.list > Registers.register List.list > Joint.joint_seq 147 147 List.list **) 148 let get_params_hdw globals params 0=149 save_hdws globals (Util.zip_pottier params 0I8051.registerParams)148 let get_params_hdw globals params = 149 save_hdws globals (Util.zip_pottier params I8051.registerParams) 150 150 151 151 (** val get_param_stack : … … 167 167 AST.ident List.list > Registers.register List.list > 168 168 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 169 let get_params_stack globals params 0=169 let get_params_stack globals params = 170 170 Bind_new.Bnew (fun tmpr > Bind_new.Bnew (fun addr1 > Bind_new.Bnew 171 171 (fun addr2 > 172 172 let params_length_byte = 173 173 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 174 (Nat.S (Nat.S Nat.O)))))))) (List.length params 0)174 (Nat.S (Nat.S Nat.O)))))))) (List.length params) 175 175 in 176 176 let l = … … 198 198 List.Nil)))))))))))))) 199 199 (List.flatten 200 (List.map (get_param_stack globals addr1 addr2) params 0))200 (List.map (get_param_stack globals addr1 addr2) params)) 201 201 in 202 202 Bind_new.Bret l))) … … 205 205 AST.ident List.list > Registers.register List.list > 206 206 (Registers.register, Joint.joint_seq) BindLists.bind_list **) 207 let get_params globals params 0=208 let n = Nat.min (List.length params 0) (List.length I8051.registerParams) in207 let get_params globals params = 208 let n = Nat.min (List.length params) (List.length I8051.registerParams) in 209 209 let { Types.fst = hdw_params; Types.snd = stack_params } = 210 Util.list_split n params 0210 Util.list_split n params 211 211 in 212 212 BindLists.bappend … … 263 263 List.list > (Registers.register, Joint.joint_seq List.list) 264 264 Bind_new.bind_new **) 265 let prologue globals params 0sral srah sregs =265 let prologue globals params sral srah sregs = 266 266 BindLists.bappend 267 267 (let l = List.Cons … … 273 273 Bind_new.Bret l) 274 274 (BindLists.bappend (let l = save_hdws globals sregs in Bind_new.Bret l) 275 (get_params globals params 0))275 (get_params globals params)) 276 276 277 277 (** val set_params_hdw : 278 278 AST.ident List.list > Joint.psd_argument List.list > Joint.joint_seq 279 279 List.list **) 280 let set_params_hdw globals params 0=281 restore_hdws globals (Util.zip_pottier params 0I8051.registerParams)280 let set_params_hdw globals params = 281 restore_hdws globals (Util.zip_pottier params I8051.registerParams) 282 282 283 283 (** val set_param_stack : … … 298 298 AST.ident List.list > Joint.psd_argument List.list > 299 299 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 300 let set_params_stack globals params 0=300 let set_params_stack globals params = 301 301 Bind_new.Bnew (fun addr1 > Bind_new.Bnew (fun addr2 > 302 302 let params_length_byte = 303 303 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 304 (Nat.S (Nat.S Nat.O)))))))) (List.length params 0)304 (Nat.S (Nat.S Nat.O)))))))) (List.length params) 305 305 in 306 306 let l = … … 320 320 List.Nil)))))))))) 321 321 (List.flatten 322 (List.map (set_param_stack globals addr1 addr2) params 0))322 (List.map (set_param_stack globals addr1 addr2) params)) 323 323 in 324 324 Bind_new.Bret l)) … … 328 328 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new 329 329 Types.sig0 **) 330 let set_params globals params 0=331 let n = Nat.min (List.length params 0) (List.length I8051.registerParams) in332 let hdw_stack_params = List.split params 0n in330 let set_params globals params = 331 let n = Nat.min (List.length params) (List.length I8051.registerParams) in 332 let hdw_stack_params = List.split params n in 333 333 let hdw_params = hdw_stack_params.Types.fst in 334 334 let stack_params = hdw_stack_params.Types.snd in … … 378 378  Joint.Step_seq s0 > 379 379 (match s0 with 380  Joint.COMMENT msg 0>381 Bind_new.Bret 382 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 383 globals (List.Cons ((Joint.COMMENT msg 0), List.Nil)))380  Joint.COMMENT msg > 381 Bind_new.Bret 382 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 383 globals (List.Cons ((Joint.COMMENT msg), List.Nil))) 384 384  Joint.MOVE rs > 385 385 Bind_new.Bret … … 398 398 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 399 399 globals List.Nil) 400  Joint.ADDRESS (x0, r 5, r6) >401 Bind_new.Bret 402 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 403 globals (List.Cons ((Joint.ADDRESS (x0, r 5, r6)), List.Nil)))404  Joint.OPACCS (op 4, destr1, destr2, srcr1, srcr2) >405 Bind_new.Bret 406 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 407 globals (List.Cons ((Joint.OPACCS (op 4, destr1, destr2, srcr1,400  Joint.ADDRESS (x0, r1, r2) > 401 Bind_new.Bret 402 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 403 globals (List.Cons ((Joint.ADDRESS (x0, r1, r2)), List.Nil))) 404  Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) > 405 Bind_new.Bret 406 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 407 globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1, 408 408 srcr2)), List.Nil))) 409  Joint.OP1 (op 4, destr, srcr) >410 Bind_new.Bret 411 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 412 globals (List.Cons ((Joint.OP1 (op 4, destr, srcr)), List.Nil)))413  Joint.OP2 (op 4, destr, srcr1, srcr2) >414 Bind_new.Bret 415 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 416 globals (List.Cons ((Joint.OP2 (op 4, destr, srcr1, srcr2)),409  Joint.OP1 (op1, destr, srcr) > 410 Bind_new.Bret 411 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 412 globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil))) 413  Joint.OP2 (op2, destr, srcr1, srcr2) > 414 Bind_new.Bret 415 (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL) 416 globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)), 417 417 List.Nil))) 418 418  Joint.CLEAR_CARRY > … … 483 483 Bind_new.bind_new **) 484 484 let translate_data globals def = 485 let params 0= (Types.pi1 def).Joint.joint_if_params in485 let params = (Types.pi1 def).Joint.joint_if_params in 486 486 let new_stacksize = 487 487 Nat.plus (Types.pi1 def).Joint.joint_if_stacksize 488 (Nat.minus (List.length (Obj.magic params 0))488 (Nat.minus (List.length (Obj.magic params)) 489 489 (List.length I8051.registerParams)) 490 490 in … … 492 492 Obj.magic 493 493 (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) 494 (Obj.magic (prologue globals (Obj.magic params 0) ral rah to_save))494 (Obj.magic (prologue globals (Obj.magic params) ral rah to_save)) 495 495 (fun prologue0 > 496 496 Monad.m_return0 (Monad.max_def Bind_new.bindNew) 497 497 { TranslateUtils.init_ret = (Obj.magic Types.It); 498 498 TranslateUtils.init_params = 499 (Obj.magic (List.length (Obj.magic params 0)));499 (Obj.magic (List.length (Obj.magic params))); 500 500 TranslateUtils.init_stack_size = new_stacksize; 501 501 TranslateUtils.added_prologue = prologue0; TranslateUtils.f_step =
Note: See TracChangeset
for help on using the changeset viewer.