Changeset 2708 for src/LIN


Ignore:
Timestamp:
Feb 22, 2013, 7:11:30 PM (7 years ago)
Author:
tranquil
Message:

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2490 r2708  
    33include "LIN/LIN.ma".
    44include "ASM/ASM.ma".
     5include "utilities/state.ma".
     6
     7(* utilities to provide Identifier's and addresses  *)
     8record ASM_universe (globals : list ident) : Type[0] :=
     9{ id_univ : universe ASMTag
     10; current_funct : ident
     11; ident_map : identifier_map SymbolTag Identifier
     12; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
     13; address_map : identifier_map SymbolTag Word
     14; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
     15}.
     16
     17definition new_ASM_universe :
     18∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
     19λp.
     20  let globals_addr_internal ≝
     21   λres_offset : identifier_map SymbolTag Word × Z.
     22   λx_size: ident × region × nat.
     23    let 〈res, offset〉 ≝ res_offset in
     24    let 〈x, region, size〉 ≝ x_size in
     25      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in
     26  let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in
     27mk_ASM_universe ? (mk_universe … one)
     28  (an_identifier … one (* dummy *))
     29  (empty_map …) (empty_map …)
     30  (\fst addresses) ?.
     31@hide_prf
     32normalize nodelta
     33cases p -p #vars #functs #main
     34#i #H
     35letin init_val ≝ (〈empty_map ? Word, OZ〉)
     36cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
     37[ %2{H} ] -H
     38lapply i -i lapply init_val -init_val elim vars -vars
     39[2: ** #id #r #v #tl #IH ] #init_val #i
     40[2: * [2: * ] #H @H ]
     41* [2: #H cases (orb_Prop_true … H) -H ] #H
     42@IH
     43[ %1 cases init_val normalize nodelta #init_map #off
     44  >(proj1 ?? (eqb_true ???) H) @mem_set_add_id
     45| %2{H}
     46| %1 cases init_val in H; normalize nodelta #init_map #off #H
     47  >mem_set_add @orb_Prop_r @H
     48]
     49qed.
     50
     51definition Identifier_of_label :
     52  ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
     53λg,l,u.
     54let current ≝ current_funct … u in
     55let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
     56let 〈id, univ, lmap〉 ≝
     57  match lookup … lmap l with
     58  [ Some id ⇒ 〈id, id_univ … u, lmap〉
     59  | None ⇒
     60    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     61    〈id, univ, add … lmap l id〉
     62  ] in
     63〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
     64  (address_map … u) (globals_are_in … u), id〉.
     65
     66definition Identifier_of_ident :
     67  ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
     68λg,i,u.
     69let imap ≝ ident_map … u in
     70let 〈id, univ, imap〉 ≝
     71  match lookup … imap i with
     72  [ Some id ⇒ 〈id, id_univ … u, imap〉
     73  | None ⇒
     74    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     75    〈id, univ, add … imap i id〉
     76  ] in
     77〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
     78  (address_map … u) (globals_are_in … u), id〉.
     79
     80definition start_funct_translation :
     81  ∀globals.(ident × (joint_function LIN globals)) →
     82    state_monad (ASM_universe globals) unit ≝
     83  λg,id_f,u.
     84    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
     85      (address_map … u) (globals_are_in … u), it〉.
     86
     87definition address_of_ident :
     88  ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
     89λglobals,i,prf,u.
     90〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.
     91
     92definition ASM_fresh :
     93  ∀globals.state_monad (ASM_universe globals) Identifier ≝
     94λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     95〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
     96  (address_map … u) (globals_are_in … u), id〉.
    597
    698definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    22114    ]. @I qed.
    23115
    24 let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
    25                     on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
    26   match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
    27   [ nil ⇒ Ⓧ
    28   | cons hd tl ⇒
    29     λprf.
    30     If eq_A a (\fst hd) then \snd hd else with eq_prf do
    31       association … eq_A a tl ?
    32   ].
    33   elim (orb_Prop_true … prf)
    34     [ > eq_prf *
    35     | # H
    36       assumption
    37     ]
    38 qed.
    39 
    40 definition association_ident ≝ association ident nat (eq_identifier ?).
    41 definition association_block ≝ association block Word eq_block.
    42 
    43116definition vector_cast :
    44117∀A,n,m.A → Vector A n → Vector A m ≝
     
    68141definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
    69142
    70 definition statement_labels ≝
    71   λg: list ident.
    72   λs: lin_statement g.
    73   let 〈label, instr〉 ≝ s in
    74   let generated ≝
    75     match instr with
    76     [ sequential instr' _ ⇒
    77       match instr' with
    78       [ step_seq instr'' ⇒
    79         match instr'' with
    80         [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
    81         | _ ⇒ ∅
    82         ]
    83       | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
    84       ]
    85     | final instr' ⇒
    86       match instr' with
    87       [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
    88       | _ ⇒ ∅
    89       ]
    90     ]
    91   in
    92   match label with
    93   [ None ⇒ generated
    94   | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
    95   ].
    96 
    97 definition function_labels_internal ≝
    98   λglobals: list ident.
    99   λlabels: identifier_set ?.
    100   λstatement: lin_statement globals.
    101     labels ∪ (statement_labels globals statement).
    102 
    103 (* dpm: A = Identifier *)
    104 definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
    105   λA: Type[0].
    106   λglobals: list ident.
    107   λf: A × (joint_function LIN globals).
    108   let 〈ignore, fun_def〉 ≝ f in
    109   match fun_def return λ_. identifier_set ? with
    110   [ Internal stmts ⇒
    111       foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
    112   | External _ ⇒ ∅
    113   ].
    114  
    115 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
    116   λA: Type[0].
    117   λglobals: list ident.
    118   λlabels: identifier_set ?.
    119   λfunct: A × (joint_function LIN globals).
    120     labels ∪ (function_labels ? globals funct).
    121 
    122 (* CSC: here we are silently throwing away the region information *)
    123 definition program_labels ≝
    124  λprogram: lin_program.
    125     foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
    126               ∅ (prog_funct … program).
    127  
    128143definition data_of_int ≝ λbv. DATA bv.
    129144definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
     
    133148definition asm_other_bit ≝ BIT_ADDR (zero_byte).
    134149
    135 definition translate_statements
    136   λglobals: list (ident × nat).
    137   λglobals_old: list ident.
    138   λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
    139   λstatement: joint_statement LIN globals_old.
    140   match statement  with
     150definition translate_statements :
     151  ∀globals.
     152  joint_statement LIN globals →
     153  state_monad (ASM_universe globals) pseudo_instruction ≝
     154  λglobals,statement.
     155  match statement with
    141156  [ final instr ⇒
    142157    match instr with
    143     [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    144     | RETURN ⇒ Instruction (RET ?)
     158    [ GOTO lbl ⇒
     159      ! lbl' ← Identifier_of_label … lbl ;
     160      return Jmp (toASM_ident ? lbl)
     161    | RETURN ⇒ return Instruction (RET ?)
    145162    | TAILCALL abs _ _ ⇒ Ⓧabs
    146163    ]
     
    152169          match ext with
    153170          [ SAVE_CARRY ⇒
    154             Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
     171            return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
    155172          | RESTORE_CARRY ⇒
    156             Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
     173            return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
     174          | LOW_ADDRESS reg lbl ⇒
     175            ! lbl' ← Identifier_of_label … lbl ;
     176            return MovSuccessor (register_address reg) LOW lbl'
     177          | HIGH_ADDRESS reg lbl ⇒
     178            ! lbl' ← Identifier_of_label … lbl ;
     179            return MovSuccessor (register_address reg) HIGH lbl'
    157180          ]
    158         | COMMENT comment ⇒ Comment comment
    159         | COST_LABEL lbl ⇒ Cost lbl
    160         | POP _ ⇒ Instruction (POP ? accumulator_address)
    161         | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    162         | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    163         | CALL f _ _ ⇒
    164           match f with
    165           [ inl f_id ⇒ Call (toASM_ident ? f_id)
    166           | inr _ ⇒ (* TODO call from ptr in DPTR *)
    167             match not_implemented in False with [ ]
    168           ]
     181        | COMMENT comment ⇒ return Comment comment
     182        | POP _ ⇒ return Instruction (POP ? accumulator_address)
     183        | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address)
     184        | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY)
    169185        | OPACCS accs _ _ _ _ ⇒
    170           match accs with
     186          return match accs with
    171187          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    172188          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    173189          ]
    174190        | OP1 op1 _ _ ⇒
    175           match op1 with
     191          return match op1 with
    176192          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    177193          | Inc ⇒ Instruction (INC ? ACC_A)
     
    179195          ]
    180196        | OP2 op2 _ _ reg ⇒
    181           match arg_address … reg
     197          return match arg_address … reg
    182198          return λx.is_in … [[ acc_a;
    183199                                 direct;
     
    221237          | _ ⇒ Ⓧ
    222238          ] (subaddressing_modein …)
    223         | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    224         | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     239        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     240        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    225241        | ADDRESS addr proof _ _ ⇒
    226           let look ≝ association_ident addr globals (prf ? proof) in
    227             Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     242          ! addr' ← address_of_ident … proof ;
     243          return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
    228244        | SET_CARRY ⇒
    229           Instruction (SETB ? CARRY)
     245          return Instruction (SETB ? CARRY)
    230246        | MOVE regs ⇒
    231           match regs with
     247          return match regs with
    232248          [ to_acc _ reg ⇒
    233249            match register_address reg return λx.is_in … [[ acc_a;
     
    276292          ]
    277293        ]
     294      | CALL f _ _ ⇒
     295        match f with
     296        [ inl id ⇒
     297          ! id' ← Identifier_of_ident … id ;
     298          return Call (toASM_ident ? id')
     299        | inr _ ⇒
     300          return Instruction (JMP … INDIRECT_DPTR)
     301        ]
     302      | COST_LABEL lbl ⇒ return Cost lbl
    278303      | COND _ lbl ⇒
    279         (* dpm: this should be handled in translate_code! *)
    280         Instruction (JNZ ? (toASM_ident ? lbl))
     304        ! l ← Identifier_of_label … lbl;
     305        return Instruction (JNZ ? l)
    281306      ]
     307    | FCOND _ _ lbl_true lbl_false ⇒
     308      ! l1 ← Identifier_of_label … lbl_true;
     309      ! l2 ← Identifier_of_label … lbl_false;
     310      return Jnz ACC_A l1 l2
    282311    ].
    283312  try @I
    284313qed.
    285314
    286 (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
    287 definition ident_of_label: label → Identifier ≝
    288  toASM_ident LabelTag.
    289315
    290316definition build_translated_statement ≝
    291317  λglobals.
    292   λglobals_old.
    293   λprf.
    294   λstatement: lin_statement globals_old.
    295     〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
     318  λstatement: lin_statement globals.
     319  ! stmt ← translate_statements globals (\snd statement) ;
     320  match \fst statement with
     321  [ Some lbl ⇒
     322    ! lbl' ← Identifier_of_label globals lbl ;
     323    return 〈Some ? lbl', stmt〉
     324  | None ⇒
     325    return 〈None ?, stmt〉
     326  ].
    296327
    297328definition translate_code ≝
    298   λglobals: list (ident × nat).
    299   λglobals_old: list ident.
    300   λprf.
    301   λcode: list (lin_statement globals_old).
    302     map ? ? (build_translated_statement globals globals_old prf) code.
     329  λglobals.
     330  λcode: list (lin_statement globals).
     331    m_list_map … (build_translated_statement globals) code.
    303332
    304333definition translate_fun_def ≝
    305   λglobals: list (ident × nat).
    306   λglobals_old.
    307   λprf.
    308   λid_def : ident × (joint_function LIN globals_old).
    309     let 〈id, def〉 ≝ id_def in
    310     match def with
     334  λglobals.
     335  λid_def : ident × (joint_function LIN globals).
     336  !_ start_funct_translation … id_def ;
     337  (* ^ modify current function id ^ *)
     338  match \snd id_def with
    311339    [ Internal int ⇒
    312       let code ≝ joint_if_code LIN globals_old int in
    313       match translate_code globals globals_old prf code with
    314       [ nil ⇒ ⊥
     340      let code ≝ joint_if_code … int in
     341      ! id ← Identifier_of_ident … (\fst id_def) ;
     342      ! code' ← translate_code … code ;
     343      match code' with
     344      [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *)
    315345      | cons hd tl ⇒
    316         let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
    317           map ? ? (
    318             λr.
    319             match fst ? ? r with
    320             [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
    321             | None ⇒ 〈None ?, \snd r〉
    322             ]) rest
     346        match \fst hd with
     347        [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl)
     348        | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *)
     349        ]
    323350      ]
    324     | External _ ⇒ [ ]
     351    | External _ ⇒ return [ ]
    325352    ].
    326 cases daemon (*CSC: XXX will be fixed by an invariant later *)
    327 qed.
    328 
    329 include "common/Identifiers.ma".
    330 
    331 let rec flatten_fun_defs
    332   (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    333     (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
    334       on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
    335   match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
    336   [ cons hd tl ⇒
    337     let fun_def ≝ \snd hd in
    338     let fun_id ≝ \fst hd in
    339     let translated ≝ translate_fun_def globals globals_old prf hd in
    340     let size_translated ≝ | translated | in
    341     let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
    342     let new_hd ≝ translated @ tail_trans in
    343     let new_map ≝ add ? ? tail_map fun_id initial_pc in
    344       〈new_hd, new_map〉
    345   | nil ⇒ 〈[ ], empty_map …〉
    346   ].
    347 
    348 definition translate_functs ≝
    349   λglobals.
    350   λglobals_old.
    351   λprf.
    352   λexit_label.
    353   λmain.
    354   λfuncts : list (ident × (joint_function LIN ?)).
    355   let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    356   let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
    357    〈preamble @ flattened, map〉.
    358 
    359 (*CSC: region silently thrown away here *)
    360 definition globals_addr ≝
    361  λl.
    362   let globals_addr_internal ≝
    363    λres_offset.
    364    λx_size: ident × region × nat.
    365     let 〈res, offset〉 ≝ res_offset in
    366     let 〈x, region, size〉 ≝ x_size in
    367       〈〈x, offset〉 :: res, offset + size〉
    368   in
    369     \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    370 
    371 (* dpm: plays the role of the string "_exit" in the O'caml source *)
    372 axiom identifier_prefix: Identifier.
    373 (*CSC: XXXXXXX wrong anyway since labels from different functions can now
    374   clash with each other and with names of functions *)
    375 axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
    376 
    377 (* dpm: fresh prefix stuff needs unifying with brian *)
     353
    378354definition lin_to_asm : lin_program → pseudo_assembly_program ≝
    379355  λp.
    380   let prog_lbls ≝ program_labels … p in
    381   let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    382   let global_addr ≝ globals_addr (prog_vars … p) in
    383   let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
    384   let 〈translated, funct_map〉 ≝
    385     translate_functs global_addr (prog_var_names … p) ? exit_label
    386     (toASM_ident … (prog_main … p)) (prog_funct ?? p) in
    387     〈〈funct_map, global_addr'〉, translated〉.
    388  #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
    389  normalize in match prog_var_names; normalize nodelta
    390  elim (prog_vars … p) //
    391  #hd #tl #IH whd in ⊢ (% → %);
    392  whd in match globals_addr; normalize nodelta
    393  whd in match (foldl ???? (hd::tl)); normalize nodelta
    394  cases hd * #id #reg #size normalize nodelta
    395  cases daemon (*CSC: provable using a pair of lemmas over foldl *)
    396 qed.
     356  state_run ?? (new_ASM_universe p)
     357    (let add_translation ≝
     358      λacc,id_def.
     359      ! code ← translate_fun_def … id_def ;
     360      ! acc ← acc ;
     361      return (code @ acc) in
     362     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
     363     ! exit_label ← ASM_fresh … ;
     364     ! main ← Identifier_of_ident … (prog_main … p) ;
     365     let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     366     (* atm no data identifier is used in the code, so preamble must be empty *)
     367     return 〈[ ], code〉).
Note: See TracChangeset for help on using the changeset viewer.