Changeset 2946 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2767 r2946  
    66
    77include "LIN/LIN.ma".
     8
     9
    810
    911(* utilities to provide Identifier's and addresses  *)
     
    2224  let globals_addr_internal ≝
    2325   λres_offset : identifier_map SymbolTag Word × Z.
    24    λx_size: ident × region × nat.
     26   λx_size: ident × region × (list init_data).
    2527    let 〈res, offset〉 ≝ res_offset in
    26     let 〈x, region, size〉 ≝ x_size in
    27       〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in
    28   let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in
     28    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
    2931mk_ASM_universe ? (mk_universe … one)
    3032  (an_identifier … one (* dummy *))
     
    3335@hide_prf
    3436normalize nodelta
    35 cases p -p #vars #functs #main
     37cases p -p * #vars #functs #main #cost_init
    3638#i #H
    37 letin init_val ≝ (〈empty_map ? Word, OZ〉)
     39letin init_val ≝ (〈empty_map ? Word, -(globals_stacksize ??)〉)
    3840cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
    3941[ %2{H} ] -H
     
    354356    ].
    355357
     358definition 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
     365definition do_store_init_data :
     366  ∀globals.ASM_universe globals → Z → init_data → list labelled_instruction ≝
     367λglobals,u,nxt_dptr,data.
     368match 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
     399definition do_store_init_data_list :
     400  ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
     401λglobals,u,start_dptr,data.
     402let 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
     408definition 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
    356437definition get_symboltable :
    357438  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
     
    373454     ! main ← Identifier_of_ident … (prog_main … p) ;
    374455     ! symboltable ← get_symboltable … ;
     456     ! init ← translate_initialization p ;
    375457     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 ? ?))).
    381464cases daemon
    382465qed.
Note: See TracChangeset for help on using the changeset viewer.