[698] | 1 | include "ASM/Util.ma". |
---|
| 2 | include "utilities/BitVectorTrieSet.ma". |
---|
| 3 | include "LIN/LIN.ma". |
---|
[2286] | 4 | include "ASM/ASM.ma". |
---|
[1264] | 5 | |
---|
[2286] | 6 | definition register_address: Register → [[ acc_a; direct; registr ]] ≝ |
---|
| 7 | λr: Register. |
---|
| 8 | match r with |
---|
| 9 | [ Register00 ⇒ REGISTER [[ false; false; false ]] |
---|
| 10 | | Register01 ⇒ REGISTER [[ false; false; true ]] |
---|
| 11 | | Register02 ⇒ REGISTER [[ false; true; false ]] |
---|
| 12 | | Register03 ⇒ REGISTER [[ false; true; true ]] |
---|
| 13 | | Register04 ⇒ REGISTER [[ true; false; false ]] |
---|
| 14 | | Register05 ⇒ REGISTER [[ true; false; true ]] |
---|
| 15 | | Register06 ⇒ REGISTER [[ true; true; false ]] |
---|
| 16 | | Register07 ⇒ REGISTER [[ true; true; true ]] |
---|
| 17 | | RegisterA ⇒ ACC_A |
---|
| 18 | | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240) |
---|
| 19 | | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82) |
---|
| 20 | | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83) |
---|
| 21 | | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) |
---|
| 22 | ]. @I qed. |
---|
| 23 | |
---|
[2443] | 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 ⇒ Ⓧ |
---|
[686] | 28 | | cons hd tl ⇒ |
---|
[2443] | 29 | λprf. |
---|
| 30 | If eq_A a (\fst hd) then \snd hd else with eq_prf do |
---|
| 31 | association … eq_A a tl ? |
---|
[686] | 32 | ]. |
---|
[2443] | 33 | elim (orb_Prop_true … prf) |
---|
| 34 | [ > eq_prf * |
---|
[686] | 35 | | # H |
---|
| 36 | assumption |
---|
| 37 | ] |
---|
[2443] | 38 | qed. |
---|
| 39 | |
---|
| 40 | definition association_ident ≝ association ident nat (eq_identifier ?). |
---|
| 41 | definition association_block ≝ association block Word eq_block. |
---|
| 42 | |
---|
| 43 | definition vector_cast : |
---|
| 44 | ∀A,n,m.A → Vector A n → Vector A m ≝ |
---|
| 45 | λA,n,m,dflt,v. |
---|
| 46 | If leb n m then with prf do |
---|
| 47 | replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉ |
---|
| 48 | else with prf do |
---|
| 49 | \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)). |
---|
| 50 | lapply prf @(leb_elim n) |
---|
| 51 | [2,3: #_ * #abs elim (abs I) ] |
---|
| 52 | #H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …)) |
---|
| 53 | [ assumption ] |
---|
| 54 | @(transitive_le … (not_le_to_lt … H)) %2 %1 |
---|
| 55 | qed. |
---|
| 56 | |
---|
[2490] | 57 | definition arg_address : hdw_argument → |
---|
[2443] | 58 | [[ acc_a ; direct ; registr ; data ]] ≝ |
---|
[2490] | 59 | λa. |
---|
[2443] | 60 | match a |
---|
| 61 | with |
---|
[2490] | 62 | [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]]) |
---|
| 63 | | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]]) |
---|
[2443] | 64 | ]. |
---|
[2490] | 65 | [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I |
---|
[686] | 66 | qed. |
---|
[491] | 67 | |
---|
[2286] | 68 | definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). |
---|
[2443] | 69 | |
---|
[491] | 70 | definition statement_labels ≝ |
---|
[757] | 71 | λg: list ident. |
---|
[1264] | 72 | λs: lin_statement g. |
---|
[722] | 73 | let 〈label, instr〉 ≝ s in |
---|
| 74 | let generated ≝ |
---|
| 75 | match instr with |
---|
[1282] | 76 | [ sequential instr' _ ⇒ |
---|
[1149] | 77 | match instr' with |
---|
[2286] | 78 | [ step_seq instr'' ⇒ |
---|
| 79 | match instr'' with |
---|
| 80 | [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) } |
---|
| 81 | | _ ⇒ ∅ |
---|
| 82 | ] |
---|
[1515] | 83 | | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) } |
---|
[2286] | 84 | ] |
---|
| 85 | | final instr' ⇒ |
---|
| 86 | match instr' with |
---|
| 87 | [ GOTO lbl ⇒ {(toASM_ident ? lbl)} |
---|
[1515] | 88 | | _ ⇒ ∅ |
---|
[1112] | 89 | ] |
---|
[2286] | 90 | ] |
---|
[1112] | 91 | in |
---|
[722] | 92 | match label with |
---|
| 93 | [ None ⇒ generated |
---|
[1515] | 94 | | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl) |
---|
[491] | 95 | ]. |
---|
| 96 | |
---|
[683] | 97 | definition function_labels_internal ≝ |
---|
[757] | 98 | λglobals: list ident. |
---|
[1515] | 99 | λlabels: identifier_set ?. |
---|
[1264] | 100 | λstatement: lin_statement globals. |
---|
[1515] | 101 | labels ∪ (statement_labels globals statement). |
---|
[491] | 102 | |
---|
| 103 | (* dpm: A = Identifier *) |
---|
[1515] | 104 | definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝ |
---|
[491] | 105 | λA: Type[0]. |
---|
[757] | 106 | λglobals: list ident. |
---|
[2286] | 107 | λf: A × (joint_function LIN globals). |
---|
[491] | 108 | let 〈ignore, fun_def〉 ≝ f in |
---|
[1515] | 109 | match fun_def return λ_. identifier_set ? with |
---|
[1245] | 110 | [ Internal stmts ⇒ |
---|
[1515] | 111 | foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts) |
---|
| 112 | | External _ ⇒ ∅ |
---|
[491] | 113 | ]. |
---|
| 114 | |
---|
[1515] | 115 | definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝ |
---|
[491] | 116 | λA: Type[0]. |
---|
[757] | 117 | λglobals: list ident. |
---|
[1515] | 118 | λlabels: identifier_set ?. |
---|
[2286] | 119 | λfunct: A × (joint_function LIN globals). |
---|
[1515] | 120 | labels ∪ (function_labels ? globals funct). |
---|
[1264] | 121 | |
---|
| 122 | (* CSC: here we are silently throwing away the region information *) |
---|
[491] | 123 | definition program_labels ≝ |
---|
[1264] | 124 | λprogram: lin_program. |
---|
| 125 | foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program))) |
---|
[1515] | 126 | ∅ (prog_funct … program). |
---|
[1264] | 127 | |
---|
[491] | 128 | definition data_of_int ≝ λbv. DATA bv. |
---|
[686] | 129 | definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). |
---|
| 130 | definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). |
---|
[491] | 131 | |
---|
[2286] | 132 | (* TODO: check and change to free bit *) |
---|
| 133 | definition asm_other_bit ≝ BIT_ADDR (zero_byte). |
---|
| 134 | |
---|
[491] | 135 | definition translate_statements ≝ |
---|
[757] | 136 | λglobals: list (ident × nat). |
---|
| 137 | λglobals_old: list ident. |
---|
[2443] | 138 | λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals). |
---|
[2286] | 139 | λstatement: joint_statement LIN globals_old. |
---|
[2490] | 140 | match statement with |
---|
| 141 | [ final instr ⇒ |
---|
[2286] | 142 | match instr with |
---|
| 143 | [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) |
---|
| 144 | | RETURN ⇒ Instruction (RET ?) |
---|
[2490] | 145 | | TAILCALL abs _ _ ⇒ Ⓧabs |
---|
[2286] | 146 | ] |
---|
[1282] | 147 | | sequential instr _ ⇒ |
---|
[2490] | 148 | match instr with |
---|
[2286] | 149 | [ step_seq instr' ⇒ |
---|
[2490] | 150 | match instr' with |
---|
| 151 | [ extension_seq ext ⇒ |
---|
[2286] | 152 | match ext with |
---|
| 153 | [ SAVE_CARRY ⇒ |
---|
| 154 | Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉)) |
---|
| 155 | | RESTORE_CARRY ⇒ |
---|
| 156 | Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) |
---|
| 157 | ] |
---|
[2490] | 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 | ] |
---|
| 169 | | OPACCS accs _ _ _ _ ⇒ |
---|
[2286] | 170 | match accs with |
---|
| 171 | [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) |
---|
| 172 | | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) |
---|
| 173 | ] |
---|
[2490] | 174 | | OP1 op1 _ _ ⇒ |
---|
[2286] | 175 | match op1 with |
---|
| 176 | [ Cmpl ⇒ Instruction (CPL ? ACC_A) |
---|
| 177 | | Inc ⇒ Instruction (INC ? ACC_A) |
---|
| 178 | | Rl ⇒ Instruction (RL ? ACC_A) |
---|
| 179 | ] |
---|
[2490] | 180 | | OP2 op2 _ _ reg ⇒ |
---|
| 181 | match arg_address … reg |
---|
| 182 | return λx.is_in … [[ acc_a; |
---|
| 183 | direct; |
---|
| 184 | registr; |
---|
| 185 | data ]] x → ? with |
---|
| 186 | [ ACC_A ⇒ λacc_a: True. |
---|
| 187 | match op2 with |
---|
| 188 | [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address) |
---|
| 189 | | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address) |
---|
| 190 | | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address) |
---|
| 191 | | Xor ⇒ Instruction (CLR ? ACC_A) |
---|
| 192 | | _ ⇒ Instruction (NOP ?) |
---|
| 193 | ] |
---|
| 194 | | DIRECT d ⇒ λdirect1: True. |
---|
| 195 | match op2 with |
---|
| 196 | [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d)) |
---|
| 197 | | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d)) |
---|
| 198 | | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d)) |
---|
| 199 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) |
---|
| 200 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) |
---|
| 201 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) |
---|
| 202 | ] |
---|
| 203 | | REGISTER r ⇒ λregister1: True. |
---|
| 204 | match op2 with |
---|
| 205 | [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r)) |
---|
| 206 | | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r)) |
---|
| 207 | | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r)) |
---|
| 208 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) |
---|
| 209 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) |
---|
| 210 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) |
---|
| 211 | ] |
---|
| 212 | | DATA b ⇒ λdata : True. |
---|
| 213 | match op2 with |
---|
| 214 | [ Add ⇒ Instruction (ADD ? ACC_A (DATA b)) |
---|
| 215 | | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b)) |
---|
| 216 | | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b)) |
---|
| 217 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) |
---|
| 218 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) |
---|
| 219 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉)) |
---|
| 220 | ] |
---|
| 221 | | _ ⇒ Ⓧ |
---|
| 222 | ] (subaddressing_modein …) |
---|
| 223 | | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) |
---|
| 224 | | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) |
---|
| 225 | | ADDRESS addr proof _ _ ⇒ |
---|
[2443] | 226 | let look ≝ association_ident addr globals (prf ? proof) in |
---|
[2286] | 227 | Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) |
---|
[2490] | 228 | | SET_CARRY ⇒ |
---|
[2286] | 229 | Instruction (SETB ? CARRY) |
---|
| 230 | | MOVE regs ⇒ |
---|
[2490] | 231 | match regs with |
---|
| 232 | [ to_acc _ reg ⇒ |
---|
| 233 | match register_address reg return λx.is_in … [[ acc_a; |
---|
[1245] | 234 | direct; |
---|
[2490] | 235 | registr]] x → ? with |
---|
| 236 | [ REGISTER r ⇒ λregister9: True. |
---|
| 237 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) |
---|
| 238 | | DIRECT d ⇒ λdirect9: True. |
---|
| 239 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) |
---|
| 240 | | ACC_A ⇒ λacc_a: True. |
---|
| 241 | Instruction (NOP ?) |
---|
| 242 | | _ ⇒ Ⓧ |
---|
| 243 | ] (subaddressing_modein …) |
---|
| 244 | | from_acc reg _ ⇒ |
---|
| 245 | match register_address reg return λx.is_in … [[ acc_a; |
---|
[1245] | 246 | direct; |
---|
[2490] | 247 | registr ]] x → ? with |
---|
| 248 | [ REGISTER r ⇒ λregister8: True. |
---|
| 249 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) |
---|
| 250 | | ACC_A ⇒ λacc: True. |
---|
| 251 | Instruction (NOP ?) |
---|
| 252 | | DIRECT d ⇒ λdirect8: True. |
---|
| 253 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) |
---|
| 254 | | _ ⇒ Ⓧ |
---|
| 255 | ] (subaddressing_modein …) |
---|
| 256 | | int_to_reg reg b ⇒ |
---|
| 257 | match register_address reg return λx.is_in … [[ acc_a; |
---|
| 258 | direct; |
---|
| 259 | registr ]] x → ? with |
---|
| 260 | [ REGISTER r ⇒ λregister7: True. |
---|
| 261 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉)))))) |
---|
| 262 | | ACC_A ⇒ λacc: True. |
---|
| 263 | if eq_bv … (bv_zero …) b then |
---|
| 264 | Instruction (CLR ? ACC_A) |
---|
| 265 | else |
---|
| 266 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) |
---|
| 267 | | DIRECT d ⇒ λdirect7: True. |
---|
| 268 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉))))) |
---|
| 269 | | _ ⇒ Ⓧ |
---|
| 270 | ] (subaddressing_modein …) |
---|
| 271 | | int_to_acc _ b ⇒ |
---|
| 272 | if eq_bv … (bv_zero …) b then |
---|
| 273 | Instruction (CLR ? ACC_A) |
---|
| 274 | else |
---|
| 275 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) |
---|
[2286] | 276 | ] |
---|
| 277 | ] |
---|
[2490] | 278 | | COND _ lbl ⇒ |
---|
[1112] | 279 | (* dpm: this should be handled in translate_code! *) |
---|
[1515] | 280 | Instruction (JNZ ? (toASM_ident ? lbl)) |
---|
[722] | 281 | ] |
---|
[1149] | 282 | ]. |
---|
[2443] | 283 | try @I |
---|
[686] | 284 | qed. |
---|
| 285 | |
---|
[1268] | 286 | (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *) |
---|
[1515] | 287 | definition ident_of_label: label → Identifier ≝ |
---|
| 288 | toASM_ident LabelTag. |
---|
[1268] | 289 | |
---|
[723] | 290 | definition build_translated_statement ≝ |
---|
| 291 | λglobals. |
---|
| 292 | λglobals_old. |
---|
| 293 | λprf. |
---|
[1264] | 294 | λstatement: lin_statement globals_old. |
---|
[1268] | 295 | 〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉. |
---|
[723] | 296 | |
---|
[686] | 297 | definition translate_code ≝ |
---|
[757] | 298 | λglobals: list (ident × nat). |
---|
| 299 | λglobals_old: list ident. |
---|
[699] | 300 | λprf. |
---|
[1264] | 301 | λcode: list (lin_statement globals_old). |
---|
[723] | 302 | map ? ? (build_translated_statement globals globals_old prf) code. |
---|
| 303 | |
---|
[696] | 304 | definition translate_fun_def ≝ |
---|
[1268] | 305 | λglobals: list (ident × nat). |
---|
[723] | 306 | λglobals_old. |
---|
| 307 | λprf. |
---|
[2490] | 308 | λid_def : ident × (joint_function LIN globals_old). |
---|
[696] | 309 | let 〈id, def〉 ≝ id_def in |
---|
| 310 | match def with |
---|
[1268] | 311 | [ Internal int ⇒ |
---|
[2286] | 312 | let code ≝ joint_if_code LIN globals_old int in |
---|
[1379] | 313 | match translate_code globals globals_old prf code with |
---|
| 314 | [ nil ⇒ ⊥ |
---|
| 315 | | cons hd tl ⇒ |
---|
[1515] | 316 | let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in |
---|
[757] | 317 | map ? ? ( |
---|
| 318 | λr. |
---|
| 319 | match fst ? ? r with |
---|
[1515] | 320 | [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉 |
---|
[757] | 321 | | None ⇒ 〈None ?, \snd r〉 |
---|
| 322 | ]) rest |
---|
[1379] | 323 | ] |
---|
[1264] | 324 | | External _ ⇒ [ ] |
---|
[696] | 325 | ]. |
---|
[1379] | 326 | cases daemon (*CSC: XXX will be fixed by an invariant later *) |
---|
[723] | 327 | qed. |
---|
[1515] | 328 | |
---|
[1522] | 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) |
---|
[2490] | 333 | (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old))) |
---|
[1522] | 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 | |
---|
[696] | 348 | definition translate_functs ≝ |
---|
| 349 | λglobals. |
---|
[699] | 350 | λglobals_old. |
---|
| 351 | λprf. |
---|
[696] | 352 | λexit_label. |
---|
| 353 | λmain. |
---|
[2490] | 354 | λfuncts : list (ident × (joint_function LIN ?)). |
---|
[1264] | 355 | let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in |
---|
[1522] | 356 | let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in |
---|
| 357 | 〈preamble @ flattened, map〉. |
---|
[696] | 358 | |
---|
[1264] | 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. |
---|
[696] | 365 | let 〈res, offset〉 ≝ res_offset in |
---|
[1264] | 366 | let 〈x, region, size〉 ≝ x_size in |
---|
| 367 | 〈〈x, offset〉 :: res, offset + size〉 |
---|
| 368 | in |
---|
[699] | 369 | \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l). |
---|
[1268] | 370 | |
---|
[699] | 371 | (* dpm: plays the role of the string "_exit" in the O'caml source *) |
---|
[1515] | 372 | axiom identifier_prefix: Identifier. |
---|
[1268] | 373 | (*CSC: XXXXXXX wrong anyway since labels from different functions can now |
---|
| 374 | clash with each other and with names of functions *) |
---|
[1515] | 375 | axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier. |
---|
[699] | 376 | |
---|
[723] | 377 | (* dpm: fresh prefix stuff needs unifying with brian *) |
---|
[1995] | 378 | definition lin_to_asm : lin_program → pseudo_assembly_program ≝ |
---|
[696] | 379 | λp. |
---|
[1264] | 380 | let prog_lbls ≝ program_labels … p in |
---|
[1268] | 381 | let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in |
---|
[1264] | 382 | let global_addr ≝ globals_addr (prog_vars … p) in |
---|
[1522] | 383 | let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in |
---|
[2490] | 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 |
---|
[1522] | 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 |
---|
[1268] | 390 | elim (prog_vars … p) // |
---|
[1522] | 391 | #hd #tl #IH whd in ⊢ (% → %); |
---|
| 392 | whd in match globals_addr; normalize nodelta |
---|
| 393 | whd in match (foldl ???? (hd::tl)); normalize nodelta |
---|
[1268] | 394 | cases hd * #id #reg #size normalize nodelta |
---|
| 395 | cases daemon (*CSC: provable using a pair of lemmas over foldl *) |
---|
[1522] | 396 | qed. |
---|