Changeset 2946 for src/LIN/LINToASM.ma
 Timestamp:
 Mar 24, 2013, 11:29:01 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LINToASM.ma
r2767 r2946 6 6 7 7 include "LIN/LIN.ma". 8 9 8 10 9 11 (* utilities to provide Identifier's and addresses *) … … 22 24 let globals_addr_internal ≝ 23 25 λres_offset : identifier_map SymbolTag Word × Z. 24 λx_size: ident × region × nat.26 λx_size: ident × region × (list init_data). 25 27 let 〈res, offset〉 ≝ res_offset in 26 let 〈x, region, size〉 ≝ x_size in27 〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in28 let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars …p) in28 let 〈x, region, data〉 ≝ x_size in 29 〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in 30 let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, (globals_stacksize … p)〉 (prog_vars ?? p) in 29 31 mk_ASM_universe ? (mk_universe … one) 30 32 (an_identifier … one (* dummy *)) … … 33 35 @hide_prf 34 36 normalize nodelta 35 cases p p #vars #functs #main37 cases p p * #vars #functs #main #cost_init 36 38 #i #H 37 letin init_val ≝ (〈empty_map ? Word, OZ〉)39 letin init_val ≝ (〈empty_map ? Word, (globals_stacksize ??)〉) 38 40 cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars)) 39 41 [ %2{H} ] H … … 354 356 ]. 355 357 358 definition store_bytes : list Byte → list labelled_instruction ≝ 359 λbytes. 360 \fold[(append ?), (nil ?)]_{by ∈ bytes} 361 [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA by〉))))))〉 ; 362 〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ; 363 〈None ?, Instruction (INC ? DPTR)〉 ]. @I qed. 364 365 definition do_store_init_data : 366 ∀globals.ASM_universe globals → Z → init_data → list labelled_instruction ≝ 367 λglobals,u,nxt_dptr,data. 368 match data with 369 [ Init_int8 n ⇒ 370 store_bytes [ n ] 371  Init_int16 n ⇒ 372 let 〈by0, by1〉 ≝ vsplit ? 8 8 n in store_bytes [ by0 ; by1 ] 373  Init_int32 n ⇒ 374 let 〈by0, n〉 ≝ vsplit ? 8 24 n in 375 let 〈by1, n〉 ≝ vsplit ? 8 16 n in 376 let 〈by2, by3〉 ≝ vsplit ? 8 8 n in 377 store_bytes [ by0 ; by1 ; by2 ; by3 ] 378  Init_addrof symb ofs ⇒ 379 let addr : Word ≝ 380 match lookup … (address_map … u) symb with 381 [ Some x ⇒ bitvector_of_Z ? (Z_of_unsigned_bitvector … x + ofs) 382  None ⇒ bv_zero ? 383 ] in 384 let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in 385 store_bytes [by0 ; by1] 386  Init_space n ⇒ 387 (* if n = 1 it is better to use INC, ow we can set the DPTR with MOV *) 388 match n with 389 [ O ⇒ [ ] 390  S k ⇒ 391 match k with 392 [ O ⇒ [ 〈None ?, Instruction (INC ? DPTR)〉 ] 393  _ ⇒ [ 〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … nxt_dptr)〉))))〉 ] 394 ] 395 ] 396  Init_null ⇒ store_bytes [ bv_zero ? ; bv_zero ? ] 397 ]. @I qed. 398 399 definition do_store_init_data_list : 400 ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝ 401 λglobals,u,start_dptr,data. 402 let f ≝ λdata,dptr_acc. 403 let 〈dptr, acc〉 ≝ dptr_acc in 404 let nxt_dptr ≝ dptr + size_init_data data in 405 〈nxt_dptr, do_store_init_data … u nxt_dptr data @ acc〉 in 406 \snd (foldr ?? f 〈start_dptr, [ ]〉 data). 407 408 definition translate_initialization : ∀p : lin_program. 409 state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝ 410 λp : lin_program.λu. 411 let start_sp : Z ≝ (globals_stacksize … p) in 412 let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in 413 let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in 414 let init_isp ≝ 415 (* initial stack pointer set to 2Fh in order to use addressable bits *) 416 DATA (zero 2 @@ [[true;false]] @@ maximum 4) in 417 let isp_direct ≝ 418 (* 81h = 10000001b *) 419 DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in 420 let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in 421 let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in 422 〈u, [ 423 〈None ?, Cost (init_cost_label … p)〉 ; 424 (* initialize the internal stack pointer past the addressable bits *) 425 〈None ?, Instruction 426 (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 427 〈isp_direct, init_isp〉)))))〉 ; 428 (* initialize our stack pointer past the globals *) 429 〈None ?, Instruction 430 (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 431 〈reg_spl, DATA spl〉))))))〉 ; 432 〈None ?, Instruction 433 (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 434 〈reg_sph, DATA sph〉))))))〉 ] @ 435 do_store_init_data_list ? u start_sp data〉. @I qed. 436 356 437 definition get_symboltable : 357 438 ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝ … … 373 454 ! main ← Identifier_of_ident … (prog_main … p) ; 374 455 ! symboltable ← get_symboltable … ; 456 ! init ← translate_initialization p ; 375 457 return 376 (let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in 377 ! code_ok ← code_size_opt code ; 378 (* atm no data identifier is used in the code, so preamble must be empty *) 379 return 380 (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))). 458 (let code ≝ 459 init @ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in 460 ! code_ok ← code_size_opt code ; 461 (* atm no data identifier is used in the code, so preamble must be empty *) 462 return 463 (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))). 381 464 cases daemon 382 465 qed.
Note: See TracChangeset
for help on using the changeset viewer.