include "ASM/Util.ma". include "utilities/BitVectorTrieSet.ma". include "LIN/LIN.ma". let rec association (i: ident) (l: list (ident × nat)) on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝ match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with [ nil ⇒ λabsd. ? | cons hd tl ⇒ λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)). (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with [ true ⇒ λeq_prf. \snd hd | false ⇒ λeq_prf. association i tl ? ]) (refl ? (eq_identifier ? (\fst hd) i)) ]. [ cases absd | cases prf [ > eq_prf # H cases H | # H assumption ] ] qed. definition statement_labels ≝ λg: list ident. λs: lin_statement g. let 〈label, instr〉 ≝ s in let generated ≝ match instr with [ sequential instr' _ ⇒ match instr' with [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) } | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) } | _ ⇒ ∅ ] | RETURN ⇒ ∅ | GOTO lbl ⇒ {(toASM_ident ? lbl)} ] in match label with [ None ⇒ generated | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl) ]. definition function_labels_internal ≝ λglobals: list ident. λlabels: identifier_set ?. λstatement: lin_statement globals. labels ∪ (statement_labels globals statement). (* dpm: A = Identifier *) definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝ λA: Type[0]. λglobals: list ident. λf: A × (lin_function globals). let 〈ignore, fun_def〉 ≝ f in match fun_def return λ_. identifier_set ? with [ Internal stmts ⇒ foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts) | External _ ⇒ ∅ ]. definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝ λA: Type[0]. λglobals: list ident. λlabels: identifier_set ?. λfunct: A × (lin_function globals). labels ∪ (function_labels ? globals funct). (* CSC: here we are silently throwing away the region information *) definition program_labels ≝ λprogram: lin_program. foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program))) ∅ (prog_funct … program). definition data_of_int ≝ λbv. DATA bv. definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). definition translate_statements ≝ λglobals: list (ident × nat). λglobals_old: list ident. λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals). λstatement: pre_lin_statement globals_old. match statement with [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) | RETURN ⇒ Instruction (RET ?) | sequential instr _ ⇒ match instr with [ extension ext ⇒ ⊥ | COMMENT comment ⇒ Comment comment | COST_LABEL lbl ⇒ Cost (toASM_ident ? lbl) | POP _ ⇒ Instruction (POP ? accumulator_address) | PUSH _ ⇒ Instruction (PUSH ? accumulator_address) | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY) | CALL_ID f _ _ ⇒ Call (toASM_ident ? f) | OPACCS accs _ _ _ _ ⇒ match accs with [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) ] | OP1 op1 _ _ ⇒ match op1 with [ Cmpl ⇒ Instruction (CPL ? ACC_A) | Inc ⇒ Instruction (INC ? ACC_A) ] | OP2 op2 _ _ reg ⇒ match op2 with [ Add ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ ACC_A ⇒ λacc_a: True. Instruction (ADD ? ACC_A accumulator_address) | DIRECT d ⇒ λdirect1: True. Instruction (ADD ? ACC_A (DIRECT d)) | REGISTER r ⇒ λregister1: True. Instruction (ADD ? ACC_A (REGISTER r)) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | Addc ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ ACC_A ⇒ λacc_a: True. Instruction (ADDC ? ACC_A accumulator_address) | DIRECT d ⇒ λdirect2: True. Instruction (ADDC ? ACC_A (DIRECT d)) | REGISTER r ⇒ λregister2: True. Instruction (ADDC ? ACC_A (REGISTER r)) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | Sub ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ ACC_A ⇒ λacc_a: True. Instruction (SUBB ? ACC_A accumulator_address) | DIRECT d ⇒ λdirect3: True. Instruction (SUBB ? ACC_A (DIRECT d)) | REGISTER r ⇒ λregister3: True. Instruction (SUBB ? ACC_A (REGISTER r)) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | And ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ ACC_A ⇒ λacc_a: True. Instruction (NOP ?) | DIRECT d ⇒ λdirect4: True. Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) | REGISTER r ⇒ λregister4: True. Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | Or ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ ACC_A ⇒ λacc_a: True. Instruction (NOP ?) | DIRECT d ⇒ λdirect5: True. Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) | REGISTER r ⇒ λregister5: True. Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | Xor ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ ACC_A ⇒ λacc_a: True. Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) | DIRECT d ⇒ λdirect6: True. Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) | REGISTER r ⇒ λregister6: True. Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') ] | INT reg byte ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ REGISTER r ⇒ λregister7: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) | ACC_A ⇒ λacc: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) | DIRECT d ⇒ λdirect7: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | MOVE regs ⇒ match regs with [ from_acc reg ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ REGISTER r ⇒ λregister8: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) | ACC_A ⇒ λacc: True. Instruction (NOP ?) | DIRECT d ⇒ λdirect8: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg') | to_acc reg ⇒ let reg' ≝ register_address reg in match reg' return λx. bool_to_Prop (is_in … [[ acc_a; direct; registr ]] x) → ? with [ REGISTER r ⇒ λregister9: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) | DIRECT d ⇒ λdirect9: True. Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) | ACC_A ⇒ λacc_a: True. Instruction (NOP ?) | _ ⇒ λother: False. ⊥ ] (subaddressing_modein … reg')] | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) | ADDRESS addr proof _ _ ⇒ let look ≝ association addr globals (prf ? proof) in Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) | COND _ lbl ⇒ (* dpm: this should be handled in translate_code! *) Instruction (JNZ ? (toASM_ident ? lbl)) | SET_CARRY ⇒ Instruction (SETB ? CARRY) ] ]. try assumption try @ I qed. (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *) definition ident_of_label: label → Identifier ≝ toASM_ident LabelTag. definition build_translated_statement ≝ λglobals. λglobals_old. λprf. λstatement: lin_statement globals_old. 〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉. definition translate_code ≝ λglobals: list (ident × nat). λglobals_old: list ident. λprf. λcode: list (lin_statement globals_old). map ? ? (build_translated_statement globals globals_old prf) code. definition translate_fun_def ≝ λglobals: list (ident × nat). λglobals_old. λprf. λid_def. let 〈id, def〉 ≝ id_def in match def with [ Internal int ⇒ let code ≝ joint_if_code … (lin_params globals_old) int in match translate_code globals globals_old prf code with [ nil ⇒ ⊥ | cons hd tl ⇒ let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in map ? ? ( λr. match fst ? ? r with [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉 | None ⇒ 〈None ?, \snd r〉 ]) rest ] | External _ ⇒ [ ] ]. cases daemon (*CSC: XXX will be fixed by an invariant later *) qed. definition translate_functs ≝ λglobals. λglobals_old. λprf. λexit_label. λmain. λfuncts. let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)). (*CSC: region silently thrown away here *) definition globals_addr ≝ λl. let globals_addr_internal ≝ λres_offset. λx_size: ident × region × nat. let 〈res, offset〉 ≝ res_offset in let 〈x, region, size〉 ≝ x_size in 〈〈x, offset〉 :: res, offset + size〉 in \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l). (* dpm: plays the role of the string "_exit" in the O'caml source *) axiom identifier_prefix: Identifier. (*CSC: XXXXXXX wrong anyway since labels from different functions can now clash with each other and with names of functions *) axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier. (* dpm: fresh prefix stuff needs unifying with brian *) definition translate : lin_program → pseudo_assembly_program ≝ λp. let prog_lbls ≝ program_labels … p in let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in let global_addr ≝ globals_addr (prog_vars … p) in let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x,off〉) global_addr in 〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p)〉. #i normalize nodelta -global_addr' global_addr exit_label prog_lbls; normalize in match prog_var_names normalize nodelta elim (prog_vars … p) // #hd #tl #IH whd in ⊢ (% → %) whd in match globals_addr normalize nodelta whd in match (foldl ???? (hd::tl)) normalize nodelta cases hd * #id #reg #size normalize nodelta cases daemon (*CSC: provable using a pair of lemmas over foldl *) qed.