source: src/LIN/LINToASM.ma @ 723

Last change on this file since 723 was 723, checked in by mulligan, 9 years ago

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

File size: 12.6 KB
RevLine 
[698]1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
[699]3include "utilities/IdentifierTools.ma".
[698]4include "LIN/LIN.ma".
[686]5 
6let rec association (i: Identifier) (l: list (Identifier × nat))
[699]7                    on l: member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat ≝
8  match l return λl. member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat with
[686]9  [ nil ⇒ λabsd. ?
10  | cons hd tl ⇒
[699]11    λprf: member i (eq_bv ?) (map ? ? (fst ? ?) (cons ? hd tl)).
[686]12      (match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with
13      [ true ⇒ λeq_prf. \snd hd
14      | false ⇒ λeq_prf. association i tl ?
15      ]) (refl ? (eq_bv ? (\fst hd) i))
16  ].
17  [ cases absd
18  | cases prf
19    [ > eq_prf
20      # H
21      cases H
22    | # H
23      assumption
24    ]
25  ]
26qed.
[491]27
28definition statement_labels ≝
[699]29  λg: list Identifier.
[683]30  λs: LINStatement g.
[722]31  let 〈label, instr〉 ≝ s in
32  let generated ≝
33    match instr with
[723]34    [ Joint_St_Sequential instr' _ ⇒
[722]35        match instr' with
36        [ Joint_Instr_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
37        | Joint_Instr_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
38        | Joint_Instr_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
39        | _ ⇒ set_empty ?
40        ]
[723]41    | Joint_St_Return ⇒ set_empty ?
[722]42    ] in
43  match label with
44  [ None ⇒ generated
45  | Some lbl ⇒ set_insert ? lbl generated
[491]46  ].
47
[683]48definition function_labels_internal ≝
[699]49  λglobals: list Identifier.
[722]50  λlabels: BitVectorTrieSet ?.
[683]51  λstatement: LINStatement globals.
52    set_union ? labels (statement_labels globals statement).
[491]53
54(* dpm: A = Identifier *)
[722]55definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
[491]56  λA: Type[0].
[699]57  λglobals: list Identifier.
[683]58  λf: A × (LINFunctionDefinition globals).
[491]59  let 〈ignore, fun_def〉 ≝ f in
[722]60  match fun_def return λ_. BitVectorTrieSet ? with
[723]61  [ LIN_Fu_Internal stmts proof ⇒
[722]62      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
[491]63  | LIN_Fu_External _ ⇒ set_empty ?
64  ].
65 
[722]66definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
[491]67  λA: Type[0].
[699]68  λglobals: list Identifier.
[722]69  λlabels: BitVectorTrieSet ?.
[683]70  λfunct: A × (LINFunctionDefinition globals).
71    set_union ? labels (function_labels ? globals funct).
[491]72   
73definition program_labels ≝
74  λprogram.
[699]75    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (LIN_Pr_vars program)))
[722]76              (set_empty ?) (LIN_Pr_funs program).
[491]77   
78definition data_of_int ≝ λbv. DATA bv.
[686]79definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
80definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
[491]81
82axiom ImplementedInRuntime: False.
83
84definition translate_statements ≝
[683]85  λglobals: list (Identifier × nat).
[699]86  λglobals_old: list Identifier.
87  λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals).
[723]88  λstatement: PreLINStatement globals_old.
89  match statement with
90  [ Joint_St_Return ⇒ Instruction (RET ?)
91  | Joint_St_Sequential instr _⇒
[722]92    match instr with
[723]93    [ Joint_Instr_Goto lbl ⇒ Jmp lbl
94    | Joint_Instr_Comment comment ⇒ Comment comment
95    | Joint_Instr_CostLabel lbl ⇒ Cost lbl
96    | Joint_Instr_Pop ⇒ Instruction (POP ? accumulator_address)
97    | Joint_Instr_Push ⇒ Instruction (PUSH ? accumulator_address)
98    | Joint_Instr_ClearCarry ⇒ Instruction (CLR ? CARRY)
99    | Joint_Instr_CallId f ⇒ Call f
[722]100    | Joint_Instr_OpAccs accs ⇒
101      match accs with
[723]102      [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
103      | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
[722]104      | Modu ⇒ ?
105      ]
106    | Joint_Instr_Op1 op1 ⇒
107      match op1 with
[723]108      [ Cmpl ⇒ Instruction (CPL ? ACC_A)
109      | Inc ⇒ Instruction (INC ? ACC_A)
[722]110      ]
111    | Joint_Instr_Op2 op2 reg ⇒
112      match op2 with
113      [ Add ⇒
114        let reg' ≝ register_address reg in
115        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
116                                                       direct;
117                                                       register ]] x) → ? with
118        [ ACC_A ⇒ λacc_a: True.
[723]119          Instruction (ADD ? ACC_A accumulator_address)
[722]120        | DIRECT d ⇒ λdirect1: True.
[723]121          Instruction (ADD ? ACC_A (DIRECT d))
[722]122        | REGISTER r ⇒ λregister1: True.
[723]123          Instruction (ADD ? ACC_A (REGISTER r))
[722]124        | _ ⇒ λother: False. ⊥
125        ] (subaddressing_modein … reg')
126      | Addc ⇒
127        let reg' ≝ register_address reg in
128        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
129                                                       direct;
130                                                       register ]] x) → ? with
131        [ ACC_A ⇒ λacc_a: True.
[723]132          Instruction (ADDC ? ACC_A accumulator_address)
[722]133        | DIRECT d ⇒ λdirect2: True.
[723]134          Instruction (ADDC ? ACC_A (DIRECT d))
[722]135        | REGISTER r ⇒ λregister2: True.
[723]136          Instruction (ADDC ? ACC_A (REGISTER r))
[722]137        | _ ⇒ λother: False. ⊥
138        ] (subaddressing_modein … reg')
139      | Sub ⇒
140        let reg' ≝ register_address reg in
141        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
142                                                       direct;
143                                                       register ]] x) → ? with
144        [ ACC_A ⇒ λacc_a: True.
[723]145          Instruction (SUBB ? ACC_A accumulator_address)
[722]146        | DIRECT d ⇒ λdirect3: True.
[723]147          Instruction (SUBB ? ACC_A (DIRECT d))
[722]148        | REGISTER r ⇒ λregister3: True.
[723]149          Instruction (SUBB ? ACC_A (REGISTER r))
[722]150        | _ ⇒ λother: False. ⊥
151        ] (subaddressing_modein … reg')
152      | And ⇒
153        let reg' ≝ register_address reg in
154        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
155                                                       direct;
156                                                       register ]] x) → ? with
157        [ ACC_A ⇒ λacc_a: True.
[723]158          Instruction (NOP ?)
[722]159        | DIRECT d ⇒ λdirect4: True.
[723]160          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
[722]161        | REGISTER r ⇒ λregister4: True.
[723]162          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
[722]163        | _ ⇒ λother: False. ⊥
164        ] (subaddressing_modein … reg')
165      | Or ⇒
166        let reg' ≝ register_address reg in
167        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
168                                                       direct;
169                                                       register ]] x) → ? with
170        [ ACC_A ⇒ λacc_a: True.
[723]171          Instruction (NOP ?)
[722]172        | DIRECT d ⇒ λdirect5: True.
[723]173          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
[722]174        | REGISTER r ⇒ λregister5: True.
[723]175          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
[722]176        | _ ⇒ λother: False. ⊥
177        ] (subaddressing_modein … reg')
178      | Xor ⇒
179        let reg' ≝ register_address reg in
180        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
181                                                       direct;
182                                                       register ]] x) → ? with
183        [ ACC_A ⇒ λacc_a: True.
[723]184          Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
[722]185        | DIRECT d ⇒ λdirect6: True.
[723]186          Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
[722]187        | REGISTER r ⇒ λregister6: True.
[723]188          Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
[722]189        | _ ⇒ λother: False. ⊥
190        ] (subaddressing_modein … reg')
191      ]
192    | Joint_Instr_Int reg byte ⇒
[686]193      let reg' ≝ register_address reg in
[722]194        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
195                                                       direct;
196                                                       register ]] x) → ? with
197        [ REGISTER r ⇒ λregister7: True.
[723]198          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
[722]199        | ACC_A ⇒ λacc: True.
[723]200          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
[722]201        | DIRECT d ⇒ λdirect7: True.
[723]202          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
[722]203        | _ ⇒ λother: False. ⊥
204        ] (subaddressing_modein … reg')
205    | Joint_Instr_FromAcc reg ⇒
[686]206      let reg' ≝ register_address reg in
[722]207        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
208                                                       direct;
209                                                       register ]] x) → ? with
210        [ REGISTER r ⇒ λregister8: True.
[723]211          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
[722]212        | ACC_A ⇒ λacc: True.
[723]213          Instruction (NOP ?)
[722]214        | DIRECT d ⇒ λdirect8: True.
[723]215          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
[722]216        | _ ⇒ λother: False. ⊥
217        ] (subaddressing_modein … reg')
218    | Joint_Instr_ToAcc reg ⇒
[686]219      let reg' ≝ register_address reg in
[722]220        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
221                                                       direct;
222                                                       register ]] x) → ? with
223        [ REGISTER r ⇒ λregister9: True.
[723]224          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
[722]225        | DIRECT d ⇒ λdirect9: True.
[723]226          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
[722]227        | ACC_A ⇒ λacc_a: True.
[723]228          Instruction (NOP ?)
[722]229        | _ ⇒ λother: False. ⊥
230        ] (subaddressing_modein … reg')
[723]231    | Joint_Instr_Load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
232    | Joint_Instr_Store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
[722]233    | Joint_Instr_Address addr proof ⇒
234      let look ≝ association addr globals (prf ? proof) in
[723]235        Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
[722]236    | Joint_Instr_CondAcc lbl ⇒
237      (* dpm: this should be handled in translate_code! *)
[723]238      WithLabel (JNZ ? lbl)
[491]239    ]
[723]240  ].
[686]241  try assumption
242  try @ I
243  cases ImplementedInRuntime
244qed.
245
[723]246definition build_translated_statement ≝
247  λglobals.
248  λglobals_old.
249  λprf.
250  λstatement: LINStatement globals_old.
251    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
252
[686]253definition translate_code ≝
254  λglobals: list (Identifier × nat).
[699]255  λglobals_old: list Identifier.
256  λprf.
257  λcode: list (LINStatement globals_old).
[723]258    map ? ? (build_translated_statement globals globals_old prf) code.
[696]259   
[723]260lemma translate_code_preserves_WellFormedP:
261  ∀globals, globals_old, prf, code.
262    WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code).
263  #G #GO #P #C
264  elim C
265  [ normalize
266    //
267  | #G2 #G02 #IH (* CSC: understand here *)
268    whd in ⊢ (% → %)
269    normalize in ⊢ (% → %)
270    //
271  ]
272qed.
273
[696]274definition translate_fun_def ≝
[723]275  λglobals.
276  λglobals_old.
277  λprf.
[696]278  λid_def.
279    let 〈id, def〉 ≝ id_def in
280    match def with
[723]281    [ LIN_Fu_Internal code proof ⇒
282      match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with
283      [ nil ⇒ λprf2. ⊥
284      | cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl
285      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
[696]286    | _ ⇒ [ ]
287    ].
[723]288    @ prf2
289qed.
[696]290   
291definition translate_functs ≝
292  λglobals.
[699]293  λglobals_old.
294  λprf.
[696]295  λexit_label.
296  λmain.
297  λfuncts.
298  let preamble ≝
299    match main with
300    [ None ⇒ [ ]
[723]301    | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
[696]302    ] in
[699]303      preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
[696]304
305definition globals_addr_internal ≝
306  λres_offset.
307  λx_size: Identifier × nat.
308    let 〈res, offset〉 ≝ res_offset in
309    let 〈x, size〉 ≝ x_size in
310      〈〈x, offset〉 :: res, offset + size〉.
311
312definition globals_addr ≝
313  λl.
[699]314    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
[698]315     
[699]316(* dpm: plays the role of the string "_exit" in the O'caml source *)
317axiom identifier_prefix: Identifier.
318
[723]319(* dpm: fresh prefix stuff needs unifying with brian *)
320
[699]321(*
[696]322definition translate ≝
323  λp.
324  let prog_lbls ≝ program_labels p in
[699]325  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
326  let global_addr ≝ globals_addr (LIN_Pr_vars p) in
327    〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
[723]328*)
Note: See TracBrowser for help on using the repository browser.