Changeset 1311 for Deliverables/D3.3/idlookupbranch/LIN
 Timestamp:
 Oct 6, 2011, 6:45:54 PM (8 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 1198,12061233,12361260,12621264,1266,12681271,12741276,12781290,1292
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/LIN/LIN.ma
r1197 r1311 1 1 include "joint/Joint.ma". 2 include "utilities/lists.ma". 2 3 3 definition lin_params: params ≝ 4 mk_params 5 unit unit unit unit registers_move Register 6 unit unit unit unit. 4 definition lin_params__: params__ ≝ 5 mk_params__ unit unit unit unit registers_move Register nat unit False. 6 definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit. 7 definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit. 8 definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit. 7 9 8 definition pre_lin_statement ≝ 9 λglobals: list ident. joint_statement lin_params globals. 10 11 definition lin_statement ≝ 12 λglobals. 13 option ident × (pre_lin_statement globals). 10 definition pre_lin_statement ≝ joint_statement lin_params_. 14 11 15 12 definition well_formed_P ≝ … … 21 18 match \fst hd with 22 19 [ Some lbl ⇒ False 23  None ⇒ True 24 ] 25 ]. 26 27 inductive lin_function_definition (globals: list ident): Type[0] ≝ 28 lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals 29  lin_fu_external: external_function → lin_function_definition globals. 20  None ⇒ True]]. 30 21 31 record lin_program: Type[0] ≝ 32 { 33 lin_pr_vars: list (ident × nat); 34 lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars))); 35 lin_pr_main: option ident 36 }. 22 definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals). 23 24 definition lin_params: ∀globals. params globals ≝ 25 λglobals. 26 mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code) 27 (λcode:Σcode.?. λl. 28 find ?? (λs. let 〈l',x〉 ≝ s in 29 match l' with [ None ⇒ None …  Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code). 30 31 definition lin_function ≝ λglobals. joint_function … (lin_params globals). 32 33 definition lin_program ≝ joint_program lin_params. 
Deliverables/D3.3/idlookupbranch/LIN/LINToASM.ma
r1197 r1311 1 1 include "ASM/Util.ma". 2 2 include "utilities/BitVectorTrieSet.ma". 3 include "utilities/IdentifierTools.ma".4 3 include "LIN/LIN.ma". 5 4 6 5 let rec association (i: ident) (l: list (ident × nat)) 7 6 on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝ … … 32 31 let generated ≝ 33 32 match instr with 34 [ joint_st_sequential instr' _ ⇒33 [ sequential instr' _ ⇒ 35 34 match instr' with 36 [ joint_instr_cost_labellbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)37  joint_instr_condacc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)35 [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 36  COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 38 37  _ ⇒ set_empty ? 39 38 ] 40  joint_st_return ⇒ set_empty ? 41  joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 42  joint_st_extension _ ⇒ set_empty ? 43 ] 39  RETURN ⇒ set_empty ? 40  GOTO lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ] 44 41 in 45 42 match label with … … 54 51 set_union ? labels (statement_labels globals statement). 55 52 53 56 54 (* dpm: A = Identifier *) 57 55 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝ 58 56 λA: Type[0]. 59 57 λglobals: list ident. 60 λf: A × (lin_function _definitionglobals).58 λf: A × (lin_function globals). 61 59 let 〈ignore, fun_def〉 ≝ f in 62 60 match fun_def return λ_. BitVectorTrieSet ? with 63 [ lin_fu_internal stmts proof⇒64 foldl ? ? (function_labels_internal globals) (set_empty ?) stmts65  lin_fu_external _ ⇒ set_empty ?61 [ Internal stmts ⇒ 62 foldl ? ? (function_labels_internal globals) (set_empty ?) (pi1 … (joint_if_code ?? stmts)) 63  External _ ⇒ set_empty ? 66 64 ]. 67 65 … … 70 68 λglobals: list ident. 71 69 λlabels: BitVectorTrieSet ?. 72 λfunct: A × (lin_function _definitionglobals).70 λfunct: A × (lin_function globals). 73 71 set_union ? labels (function_labels ? globals funct). 74 72 73 (* CSC: here we are silently throwing away the region information *) 75 74 definition program_labels ≝ 76 λprogram.77 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_varsprogram)))78 (set_empty ?) (lin_pr_funcsprogram).79 75 λprogram: lin_program. 76 foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program))) 77 (set_empty …) (prog_funct … program). 78 80 79 definition data_of_int ≝ λbv. DATA bv. 81 80 definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). 82 81 definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). 83 84 axiom ImplementedInRuntime: False.85 82 86 83 definition translate_statements ≝ … … 90 87 λstatement: pre_lin_statement globals_old. 91 88 match statement with 92 [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl) 93  joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *) 94  joint_st_return ⇒ Instruction (RET ?) 95  joint_st_sequential instr _ ⇒ 89 [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl) 90  RETURN ⇒ Instruction (RET ?) 91  sequential instr _ ⇒ 96 92 match instr with 97 [ joint_instr_comment comment ⇒ Comment comment 98  joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl) 99  joint_instr_pop ⇒ Instruction (POP ? accumulator_address) 100  joint_instr_push ⇒ Instruction (PUSH ? accumulator_address) 101  joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY) 102  joint_instr_call_id f ⇒ Call (word_of_identifier ? f) 103  joint_instr_opaccs accs ⇒ 93 [ extension ext ⇒ ⊥ 94  COMMENT comment ⇒ Comment comment 95  COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl) 96  POP _ ⇒ Instruction (POP ? accumulator_address) 97  PUSH _ ⇒ Instruction (PUSH ? accumulator_address) 98  CLEAR_CARRY ⇒ Instruction (CLR ? CARRY) 99  CALL_ID f _ _ ⇒ Call (word_of_identifier ? f) 100  OPACCS accs _ _ _ _ ⇒ 104 101 match accs with 105 102 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 106 103  DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 107 104 ] 108  joint_instr_op1 op1⇒105  OP1 op1 _ _ ⇒ 109 106 match op1 with 110 107 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 111 108  Inc ⇒ Instruction (INC ? ACC_A) 112 109 ] 113  joint_instr_op2 op2reg ⇒110  OP2 op2 _ _ reg ⇒ 114 111 match op2 with 115 112 [ Add ⇒ … … 192 189 ] (subaddressing_modein … reg') 193 190 ] 194  joint_instr_intreg byte ⇒191  INT reg byte ⇒ 195 192 let reg' ≝ register_address reg in 196 193 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; … … 205 202  _ ⇒ λother: False. ⊥ 206 203 ] (subaddressing_modein … reg') 207  joint_instr_from_acc reg ⇒ 208 let reg' ≝ register_address reg in 209 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 210 direct; 211 registr ]] x) → ? with 212 [ REGISTER r ⇒ λregister8: True. 213 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) 214  ACC_A ⇒ λacc: True. 215 Instruction (NOP ?) 216  DIRECT d ⇒ λdirect8: True. 217 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) 218  _ ⇒ λother: False. ⊥ 219 ] (subaddressing_modein … reg') 220  joint_instr_to_acc reg ⇒ 221 let reg' ≝ register_address reg in 222 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 223 direct; 224 registr ]] x) → ? with 225 [ REGISTER r ⇒ λregister9: True. 226 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 227  DIRECT d ⇒ λdirect9: True. 228 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 229  ACC_A ⇒ λacc_a: True. 230 Instruction (NOP ?) 231  _ ⇒ λother: False. ⊥ 232 ] (subaddressing_modein … reg') 233  joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 234  joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 235  joint_instr_address addr proof ⇒ 204  MOVE regs ⇒ 205 match regs with 206 [ from_acc reg ⇒ 207 let reg' ≝ register_address reg in 208 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 209 direct; 210 registr ]] x) → ? with 211 [ REGISTER r ⇒ λregister8: True. 212 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) 213  ACC_A ⇒ λacc: True. 214 Instruction (NOP ?) 215  DIRECT d ⇒ λdirect8: True. 216 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) 217  _ ⇒ λother: False. ⊥ 218 ] (subaddressing_modein … reg') 219  to_acc reg ⇒ 220 let reg' ≝ register_address reg in 221 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 222 direct; 223 registr ]] x) → ? with 224 [ REGISTER r ⇒ λregister9: True. 225 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 226  DIRECT d ⇒ λdirect9: True. 227 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 228  ACC_A ⇒ λacc_a: True. 229 Instruction (NOP ?) 230  _ ⇒ λother: False. ⊥ 231 ] (subaddressing_modein … reg')] 232  LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 233  STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 234  ADDRESS addr proof _ _ ⇒ 236 235 let look ≝ association addr globals (prf ? proof) in 237 236 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 238  joint_instr_cond_acclbl ⇒237  COND _ lbl ⇒ 239 238 (* dpm: this should be handled in translate_code! *) 240 239 Instruction (JNZ ? (word_of_identifier ? lbl)) 241  joint_instr_set_carry⇒240  SET_CARRY ⇒ 242 241 Instruction (SETB ? CARRY) 243 242 ] … … 245 244 try assumption 246 245 try @ I 247 cases ImplementedInRuntime 248 qed. 246 qed. 247 248 (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *) 249 definition ident_of_label: label → ident ≝ 250 λl. an_identifier … (word_of_identifier … l). 249 251 250 252 definition build_translated_statement ≝ … … 253 255 λprf. 254 256 λstatement: lin_statement globals_old. 255 〈 \fst statement, translate_statements globals globals_old prf (\snd statement)〉.257 〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉. 256 258 257 259 definition translate_code ≝ … … 270 272 // 271 273  #G2 #G02 #IH (* CSC: understand here *) 272 whd in ⊢ (% → %) 273 normalize in ⊢ (% → %) 274 // 275 ] 274 whd in ⊢ (% → %) whd in match build_translated_statement normalize nodelta 275 cases (\fst G2) normalize // ] 276 276 qed. 277 277 278 278 definition translate_fun_def ≝ 279 λglobals .279 λglobals: list (ident × nat). 280 280 λglobals_old. 281 281 λprf. … … 283 283 let 〈id, def〉 ≝ id_def in 284 284 match def with 285 [ lin_fu_internal code proof ⇒ 286 match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with 285 [ Internal int ⇒ 286 let code_proof ≝ joint_if_code … (lin_params globals_old) int in 287 match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with 287 288 [ nil ⇒ λprf2. ⊥ 288 289  cons hd tl ⇒ λ_. … … 294 295  None ⇒ 〈None ?, \snd r〉 295 296 ]) rest 296 ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)297  _ ⇒ [ ]297 ] (translate_code_preserves_WellFormedP globals globals_old prf (pi1 ?? code_proof) (pi2 ?? code_proof)) 298  External _ ⇒ [ ] 298 299 ]. 299 @prf2300 @prf2 300 301 qed. 301 302 … … 307 308 λmain. 308 309 λfuncts. 309 let preamble ≝ 310 match main with311 [ None ⇒ [ ]312  Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] 313 ] in 314 preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)). 315 316 definitionglobals_addr_internal ≝317 λres_offset.318 λx_size: ident× nat.310 let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in 311 preamble @ 312 (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)). 313 314 (*CSC: region silently thrown away here *) 315 definition globals_addr ≝ 316 λl. 317 let globals_addr_internal ≝ 318 λres_offset. 319 λx_size: ident × region × nat. 319 320 let 〈res, offset〉 ≝ res_offset in 320 let 〈x, size〉 ≝ x_size in 321 〈〈x, offset〉 :: res, offset + size〉. 322 323 definition globals_addr ≝ 324 λl. 321 let 〈x, region, size〉 ≝ x_size in 322 〈〈x, offset〉 :: res, offset + size〉 323 in 325 324 \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l). 326 325 327 326 (* dpm: plays the role of the string "_exit" in the O'caml source *) 328 axiom identifier_prefix: Identifier. 327 axiom identifier_prefix: Word. 328 (*CSC: XXXXXXX wrong anyway since labels from different functions can now 329 clash with each other and with names of functions *) 330 axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word. 329 331 330 332 (* dpm: fresh prefix stuff needs unifying with brian *) 331 332 (* 333 definition translate ≝ 333 definition translate : lin_program → pseudo_assembly_program ≝ 334 334 λp. 335 let prog_lbls ≝ program_labels p in335 let prog_lbls ≝ program_labels … p in 336 336 let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in 337 let global_addr ≝ globals_addr (LIN_Pr_vars p) in 338 〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉. 339 *) 337 let global_addr ≝ globals_addr (prog_vars … p) in 338 let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in 339 〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉. 340 #i normalize nodelta global_addr' global_addr exit_label prog_lbls; 341 normalize in match prog_var_names normalize nodelta 342 elim (prog_vars … p) // 343 #hd #tl #IH whd in ⊢ (% → %) 344 whd in match globals_addr normalize nodelta 345 whd in match (foldl ???? (hd::tl)) normalize nodelta 346 cases hd * #id #reg #size normalize nodelta 347 cases daemon (*CSC: provable using a pair of lemmas over foldl *) 348 qed.
Note: See TracChangeset
for help on using the changeset viewer.