[698] | 1 | include "ASM/Util.ma". |
---|
| 2 | include "utilities/BitVectorTrieSet.ma". |
---|
[699] | 3 | include "utilities/IdentifierTools.ma". |
---|
[698] | 4 | include "LIN/LIN.ma". |
---|
[686] | 5 | |
---|
| 6 | let 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 | ] |
---|
| 26 | qed. |
---|
[491] | 27 | |
---|
| 28 | definition 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] | 48 | definition 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] | 55 | definition 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] | 66 | definition 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 | |
---|
| 73 | definition 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 | |
---|
| 78 | definition data_of_int ≝ λbv. DATA bv. |
---|
[686] | 79 | definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). |
---|
| 80 | definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). |
---|
[491] | 81 | |
---|
| 82 | axiom ImplementedInRuntime: False. |
---|
| 83 | |
---|
| 84 | definition 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 |
---|
| 244 | qed. |
---|
| 245 | |
---|
[723] | 246 | definition 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] | 253 | definition 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] | 260 | lemma 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 | ] |
---|
| 272 | qed. |
---|
| 273 | |
---|
[696] | 274 | definition 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 |
---|
| 289 | qed. |
---|
[696] | 290 | |
---|
| 291 | definition 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 | |
---|
| 305 | definition 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 | |
---|
| 312 | definition 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 *) |
---|
| 317 | axiom identifier_prefix: Identifier. |
---|
| 318 | |
---|
[723] | 319 | (* dpm: fresh prefix stuff needs unifying with brian *) |
---|
| 320 | |
---|
[699] | 321 | (* |
---|
[696] | 322 | definition 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 | *) |
---|