[698] | 1 | include "utilities/BitVectorTrieSet.ma". |
---|
[2708] | 2 | include "utilities/state.ma". |
---|
[1264] | 3 | |
---|
[2767] | 4 | include "ASM/Util.ma". |
---|
| 5 | include "ASM/ASM.ma". |
---|
| 6 | |
---|
| 7 | include "LIN/LIN.ma". |
---|
| 8 | |
---|
[2708] | 9 | (* utilities to provide Identifier's and addresses *) |
---|
[3039] | 10 | record ASM_universe : Type[0] := |
---|
[2708] | 11 | { id_univ : universe ASMTag |
---|
| 12 | ; current_funct : ident |
---|
| 13 | ; ident_map : identifier_map SymbolTag Identifier |
---|
| 14 | ; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier) |
---|
[2978] | 15 | ; fresh_cost_label: Pos |
---|
[2708] | 16 | }. |
---|
| 17 | |
---|
[2978] | 18 | definition report_cost: |
---|
[3039] | 19 | costlabel → state_monad ASM_universe unit ≝ |
---|
| 20 | λcl,u. |
---|
[2978] | 21 | let clw ≝ word_of_identifier … cl in |
---|
| 22 | if leb (fresh_cost_label … u) clw then |
---|
| 23 | 〈mk_ASM_universe … (id_univ … u) (current_funct … u) (ident_map … u) |
---|
[3039] | 24 | (label_map … u) (succ clw), it〉 |
---|
[2978] | 25 | else |
---|
| 26 | 〈u,it〉. |
---|
| 27 | |
---|
[2708] | 28 | definition Identifier_of_label : |
---|
[3039] | 29 | label → state_monad ASM_universe Identifier ≝ |
---|
| 30 | λl,u. |
---|
[2708] | 31 | let current ≝ current_funct … u in |
---|
| 32 | let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in |
---|
| 33 | let 〈id, univ, lmap〉 ≝ |
---|
| 34 | match lookup … lmap l with |
---|
| 35 | [ Some id ⇒ 〈id, id_univ … u, lmap〉 |
---|
| 36 | | None ⇒ |
---|
| 37 | let 〈id, univ〉 ≝ fresh … (id_univ … u) in |
---|
| 38 | 〈id, univ, add … lmap l id〉 |
---|
| 39 | ] in |
---|
| 40 | 〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap) |
---|
[3039] | 41 | (fresh_cost_label … u), id〉. |
---|
[2708] | 42 | |
---|
| 43 | definition Identifier_of_ident : |
---|
[3039] | 44 | ident → state_monad ASM_universe Identifier ≝ |
---|
| 45 | λi,u. |
---|
[2708] | 46 | let imap ≝ ident_map … u in |
---|
[3039] | 47 | let res ≝ match lookup … imap i with |
---|
[2708] | 48 | [ Some id ⇒ 〈id, id_univ … u, imap〉 |
---|
| 49 | | None ⇒ |
---|
| 50 | let 〈id, univ〉 ≝ fresh … (id_univ … u) in |
---|
| 51 | 〈id, univ, add … imap i id〉 |
---|
| 52 | ] in |
---|
[3039] | 53 | let id ≝ \fst (\fst res) in |
---|
| 54 | let univ ≝ \snd (\fst res) in |
---|
| 55 | let imap ≝ \snd res in |
---|
[2708] | 56 | 〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u) |
---|
[3039] | 57 | (fresh_cost_label … u), id〉. |
---|
[2708] | 58 | |
---|
[3039] | 59 | definition new_ASM_universe : |
---|
| 60 | ∀p : joint_program LIN.ASM_universe ≝ |
---|
| 61 | λp. |
---|
| 62 | mk_ASM_universe (mk_universe … one) |
---|
| 63 | (an_identifier … one (* dummy *)) |
---|
| 64 | (empty_map …) (empty_map …) one. |
---|
| 65 | (*@hide_prf normalize nodelta |
---|
| 66 | cases p -p * #vars #functs #main #cost_init |
---|
| 67 | #i #H |
---|
| 68 | normalize nodelta |
---|
| 69 | letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉) |
---|
| 70 | cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars)) |
---|
| 71 | [ %2{H} ] -H |
---|
| 72 | lapply i -i lapply init_val -init_val |
---|
| 73 | whd in match prog_var_names; normalize nodelta |
---|
| 74 | elim vars -vars |
---|
| 75 | [2: ** #id #r #v #tl #IH ] #init_val #i |
---|
| 76 | [2: * [2: * ] #H @H ] |
---|
| 77 | * [2: #H cases (orb_Prop_true … H) -H ] #H |
---|
| 78 | @IH |
---|
| 79 | [ %1 cases init_val normalize nodelta #init_map #off |
---|
| 80 | >(proj1 ?? (eqb_true ???) H) @pair_elim #lft #rgt #_ @mem_set_add_id |
---|
| 81 | | %2{H} |
---|
| 82 | | %1 cases init_val in H; normalize nodelta #init_map #off #H |
---|
| 83 | @pair_elim #lft #rgt #_ |
---|
| 84 | >mem_set_add @orb_Prop_r @H |
---|
| 85 | ] |
---|
| 86 | qed. |
---|
| 87 | *) |
---|
| 88 | |
---|
[2708] | 89 | definition start_funct_translation : |
---|
[3040] | 90 | ∀globals,functions.(ident × (joint_function LIN globals functions)) → |
---|
[3039] | 91 | state_monad ASM_universe unit ≝ |
---|
[3040] | 92 | λg,functs,id_f,u. |
---|
[2708] | 93 | 〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u) |
---|
[3039] | 94 | (fresh_cost_label … u), it〉. |
---|
[2708] | 95 | |
---|
| 96 | definition ASM_fresh : |
---|
[3039] | 97 | state_monad ASM_universe Identifier ≝ |
---|
| 98 | λu.let 〈id, univ〉 ≝ fresh … (id_univ … u) in |
---|
[2708] | 99 | 〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u) |
---|
[3039] | 100 | (fresh_cost_label … u), id〉. |
---|
[2708] | 101 | |
---|
[2286] | 102 | definition register_address: Register → [[ acc_a; direct; registr ]] ≝ |
---|
| 103 | λr: Register. |
---|
| 104 | match r with |
---|
| 105 | [ Register00 ⇒ REGISTER [[ false; false; false ]] |
---|
| 106 | | Register01 ⇒ REGISTER [[ false; false; true ]] |
---|
| 107 | | Register02 ⇒ REGISTER [[ false; true; false ]] |
---|
| 108 | | Register03 ⇒ REGISTER [[ false; true; true ]] |
---|
| 109 | | Register04 ⇒ REGISTER [[ true; false; false ]] |
---|
| 110 | | Register05 ⇒ REGISTER [[ true; false; true ]] |
---|
| 111 | | Register06 ⇒ REGISTER [[ true; true; false ]] |
---|
| 112 | | Register07 ⇒ REGISTER [[ true; true; true ]] |
---|
| 113 | | RegisterA ⇒ ACC_A |
---|
| 114 | | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240) |
---|
[3028] | 115 | | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 130) |
---|
| 116 | | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 131) |
---|
[2286] | 117 | | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) |
---|
| 118 | ]. @I qed. |
---|
| 119 | |
---|
[2443] | 120 | definition vector_cast : |
---|
| 121 | ∀A,n,m.A → Vector A n → Vector A m ≝ |
---|
| 122 | λA,n,m,dflt,v. |
---|
| 123 | If leb n m then with prf do |
---|
| 124 | replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉ |
---|
| 125 | else with prf do |
---|
| 126 | \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)). |
---|
| 127 | lapply prf @(leb_elim n) |
---|
| 128 | [2,3: #_ * #abs elim (abs I) ] |
---|
| 129 | #H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …)) |
---|
| 130 | [ assumption ] |
---|
| 131 | @(transitive_le … (not_le_to_lt … H)) %2 %1 |
---|
| 132 | qed. |
---|
| 133 | |
---|
[2490] | 134 | definition arg_address : hdw_argument → |
---|
[2443] | 135 | [[ acc_a ; direct ; registr ; data ]] ≝ |
---|
[2490] | 136 | λa. |
---|
[2443] | 137 | match a |
---|
| 138 | with |
---|
[2490] | 139 | [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]]) |
---|
| 140 | | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]]) |
---|
[2443] | 141 | ]. |
---|
[2490] | 142 | [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I |
---|
[686] | 143 | qed. |
---|
[491] | 144 | |
---|
[2286] | 145 | definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). |
---|
[2443] | 146 | |
---|
[491] | 147 | definition data_of_int ≝ λbv. DATA bv. |
---|
[686] | 148 | definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). |
---|
| 149 | definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). |
---|
[491] | 150 | |
---|
[2286] | 151 | (* TODO: check and change to free bit *) |
---|
| 152 | definition asm_other_bit ≝ BIT_ADDR (zero_byte). |
---|
[3039] | 153 | definition one_word : Word ≝ bv_zero 15 @@ [[ true ]]. |
---|
[2286] | 154 | |
---|
[2708] | 155 | definition translate_statements : |
---|
| 156 | ∀globals. |
---|
| 157 | joint_statement LIN globals → |
---|
[3039] | 158 | state_monad ASM_universe pseudo_instruction ≝ |
---|
[2708] | 159 | λglobals,statement. |
---|
| 160 | match statement with |
---|
[2490] | 161 | [ final instr ⇒ |
---|
[2286] | 162 | match instr with |
---|
[2708] | 163 | [ GOTO lbl ⇒ |
---|
| 164 | ! lbl' ← Identifier_of_label … lbl ; |
---|
[3023] | 165 | return Jmp (toASM_ident ? lbl') |
---|
[2708] | 166 | | RETURN ⇒ return Instruction (RET ?) |
---|
[2490] | 167 | | TAILCALL abs _ _ ⇒ Ⓧabs |
---|
[2286] | 168 | ] |
---|
[1282] | 169 | | sequential instr _ ⇒ |
---|
[2490] | 170 | match instr with |
---|
[2286] | 171 | [ step_seq instr' ⇒ |
---|
[2490] | 172 | match instr' with |
---|
| 173 | [ extension_seq ext ⇒ |
---|
[2286] | 174 | match ext with |
---|
| 175 | [ SAVE_CARRY ⇒ |
---|
[2708] | 176 | return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉)) |
---|
[2286] | 177 | | RESTORE_CARRY ⇒ |
---|
[2708] | 178 | return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) |
---|
[3016] | 179 | | LOW_ADDRESS lbl ⇒ |
---|
[2708] | 180 | ! lbl' ← Identifier_of_label … lbl ; |
---|
[3039] | 181 | return Mov (inr ?? 〈register_address RegisterA, LOW〉) lbl' one_word |
---|
[3016] | 182 | | HIGH_ADDRESS lbl ⇒ |
---|
[2708] | 183 | ! lbl' ← Identifier_of_label … lbl ; |
---|
[3039] | 184 | return Mov (inr ?? 〈register_address RegisterA, HIGH〉) lbl' one_word |
---|
[2286] | 185 | ] |
---|
[2708] | 186 | | COMMENT comment ⇒ return Comment comment |
---|
| 187 | | POP _ ⇒ return Instruction (POP ? accumulator_address) |
---|
| 188 | | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address) |
---|
| 189 | | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY) |
---|
[2490] | 190 | | OPACCS accs _ _ _ _ ⇒ |
---|
[2708] | 191 | return match accs with |
---|
[2286] | 192 | [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) |
---|
| 193 | | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) |
---|
| 194 | ] |
---|
[2490] | 195 | | OP1 op1 _ _ ⇒ |
---|
[2708] | 196 | return match op1 with |
---|
[2286] | 197 | [ Cmpl ⇒ Instruction (CPL ? ACC_A) |
---|
| 198 | | Inc ⇒ Instruction (INC ? ACC_A) |
---|
| 199 | | Rl ⇒ Instruction (RL ? ACC_A) |
---|
| 200 | ] |
---|
[2490] | 201 | | OP2 op2 _ _ reg ⇒ |
---|
[2708] | 202 | return match arg_address … reg |
---|
[2490] | 203 | return λx.is_in … [[ acc_a; |
---|
| 204 | direct; |
---|
| 205 | registr; |
---|
| 206 | data ]] x → ? with |
---|
| 207 | [ ACC_A ⇒ λacc_a: True. |
---|
| 208 | match op2 with |
---|
| 209 | [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address) |
---|
| 210 | | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address) |
---|
| 211 | | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address) |
---|
| 212 | | Xor ⇒ Instruction (CLR ? ACC_A) |
---|
| 213 | | _ ⇒ Instruction (NOP ?) |
---|
| 214 | ] |
---|
| 215 | | DIRECT d ⇒ λdirect1: True. |
---|
| 216 | match op2 with |
---|
| 217 | [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d)) |
---|
| 218 | | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d)) |
---|
| 219 | | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d)) |
---|
| 220 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) |
---|
| 221 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) |
---|
| 222 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) |
---|
| 223 | ] |
---|
| 224 | | REGISTER r ⇒ λregister1: True. |
---|
| 225 | match op2 with |
---|
| 226 | [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r)) |
---|
| 227 | | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r)) |
---|
| 228 | | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r)) |
---|
| 229 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) |
---|
| 230 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) |
---|
| 231 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) |
---|
| 232 | ] |
---|
| 233 | | DATA b ⇒ λdata : True. |
---|
| 234 | match op2 with |
---|
| 235 | [ Add ⇒ Instruction (ADD ? ACC_A (DATA b)) |
---|
| 236 | | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b)) |
---|
| 237 | | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b)) |
---|
| 238 | | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) |
---|
| 239 | | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) |
---|
| 240 | | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉)) |
---|
| 241 | ] |
---|
| 242 | | _ ⇒ Ⓧ |
---|
| 243 | ] (subaddressing_modein …) |
---|
[2708] | 244 | | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) |
---|
| 245 | | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) |
---|
[3040] | 246 | | ADDRESS id proof off _ _ ⇒ |
---|
[3039] | 247 | ! Id ← Identifier_of_ident … id ; |
---|
[3040] | 248 | return (Mov (inl ?? DPTR) Id off) |
---|
[2490] | 249 | | SET_CARRY ⇒ |
---|
[2708] | 250 | return Instruction (SETB ? CARRY) |
---|
[2286] | 251 | | MOVE regs ⇒ |
---|
[2708] | 252 | return match regs with |
---|
[2490] | 253 | [ to_acc _ reg ⇒ |
---|
| 254 | match register_address reg return λx.is_in … [[ acc_a; |
---|
[1245] | 255 | direct; |
---|
[2490] | 256 | registr]] x → ? with |
---|
| 257 | [ REGISTER r ⇒ λregister9: True. |
---|
| 258 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) |
---|
| 259 | | DIRECT d ⇒ λdirect9: True. |
---|
| 260 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) |
---|
| 261 | | ACC_A ⇒ λacc_a: True. |
---|
| 262 | Instruction (NOP ?) |
---|
| 263 | | _ ⇒ Ⓧ |
---|
| 264 | ] (subaddressing_modein …) |
---|
| 265 | | from_acc reg _ ⇒ |
---|
| 266 | match register_address reg return λx.is_in … [[ acc_a; |
---|
[1245] | 267 | direct; |
---|
[2490] | 268 | registr ]] x → ? with |
---|
| 269 | [ REGISTER r ⇒ λregister8: True. |
---|
| 270 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) |
---|
| 271 | | ACC_A ⇒ λacc: True. |
---|
| 272 | Instruction (NOP ?) |
---|
| 273 | | DIRECT d ⇒ λdirect8: True. |
---|
| 274 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) |
---|
| 275 | | _ ⇒ Ⓧ |
---|
| 276 | ] (subaddressing_modein …) |
---|
| 277 | | int_to_reg reg b ⇒ |
---|
| 278 | match register_address reg return λx.is_in … [[ acc_a; |
---|
| 279 | direct; |
---|
| 280 | registr ]] x → ? with |
---|
| 281 | [ REGISTER r ⇒ λregister7: True. |
---|
| 282 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉)))))) |
---|
| 283 | | ACC_A ⇒ λacc: True. |
---|
| 284 | if eq_bv … (bv_zero …) b then |
---|
| 285 | Instruction (CLR ? ACC_A) |
---|
| 286 | else |
---|
| 287 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) |
---|
| 288 | | DIRECT d ⇒ λdirect7: True. |
---|
| 289 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉))))) |
---|
| 290 | | _ ⇒ Ⓧ |
---|
| 291 | ] (subaddressing_modein …) |
---|
| 292 | | int_to_acc _ b ⇒ |
---|
| 293 | if eq_bv … (bv_zero …) b then |
---|
| 294 | Instruction (CLR ? ACC_A) |
---|
| 295 | else |
---|
| 296 | Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) |
---|
[2286] | 297 | ] |
---|
| 298 | ] |
---|
[2708] | 299 | | CALL f _ _ ⇒ |
---|
| 300 | match f with |
---|
| 301 | [ inl id ⇒ |
---|
| 302 | ! id' ← Identifier_of_ident … id ; |
---|
| 303 | return Call (toASM_ident ? id') |
---|
| 304 | | inr _ ⇒ |
---|
[3039] | 305 | return Instruction (JMP … ACC_DPTR) |
---|
[2708] | 306 | ] |
---|
[2978] | 307 | | COST_LABEL lbl ⇒ |
---|
| 308 | !_ report_cost … lbl ; |
---|
| 309 | return Cost lbl |
---|
[2490] | 310 | | COND _ lbl ⇒ |
---|
[2708] | 311 | ! l ← Identifier_of_label … lbl; |
---|
| 312 | return Instruction (JNZ ? l) |
---|
[722] | 313 | ] |
---|
[2708] | 314 | | FCOND _ _ lbl_true lbl_false ⇒ |
---|
| 315 | ! l1 ← Identifier_of_label … lbl_true; |
---|
| 316 | ! l2 ← Identifier_of_label … lbl_false; |
---|
| 317 | return Jnz ACC_A l1 l2 |
---|
[1149] | 318 | ]. |
---|
[2443] | 319 | try @I |
---|
[686] | 320 | qed. |
---|
| 321 | |
---|
[1268] | 322 | |
---|
[723] | 323 | definition build_translated_statement ≝ |
---|
| 324 | λglobals. |
---|
[2708] | 325 | λstatement: lin_statement globals. |
---|
| 326 | ! stmt ← translate_statements globals (\snd statement) ; |
---|
| 327 | match \fst statement with |
---|
| 328 | [ Some lbl ⇒ |
---|
[3039] | 329 | ! lbl' ← Identifier_of_label … lbl ; |
---|
[2708] | 330 | return 〈Some ? lbl', stmt〉 |
---|
| 331 | | None ⇒ |
---|
| 332 | return 〈None ?, stmt〉 |
---|
| 333 | ]. |
---|
[723] | 334 | |
---|
[686] | 335 | definition translate_code ≝ |
---|
[2708] | 336 | λglobals. |
---|
| 337 | λcode: list (lin_statement globals). |
---|
| 338 | m_list_map … (build_translated_statement globals) code. |
---|
[723] | 339 | |
---|
[696] | 340 | definition translate_fun_def ≝ |
---|
[3040] | 341 | λglobals,functions. |
---|
| 342 | λid_def : ident × (joint_function LIN globals functions). |
---|
[2708] | 343 | !_ start_funct_translation … id_def ; |
---|
| 344 | (* ^ modify current function id ^ *) |
---|
| 345 | match \snd id_def with |
---|
[1268] | 346 | [ Internal int ⇒ |
---|
[2708] | 347 | let code ≝ joint_if_code … int in |
---|
| 348 | ! id ← Identifier_of_ident … (\fst id_def) ; |
---|
| 349 | ! code' ← translate_code … code ; |
---|
| 350 | match code' with |
---|
| 351 | [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *) |
---|
[1379] | 352 | | cons hd tl ⇒ |
---|
[2708] | 353 | match \fst hd with |
---|
| 354 | [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl) |
---|
| 355 | | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *) |
---|
| 356 | ] |
---|
[1379] | 357 | ] |
---|
[2708] | 358 | | External _ ⇒ return [ ] |
---|
[696] | 359 | ]. |
---|
[1515] | 360 | |
---|
[2984] | 361 | record init_mutable : Type[0] ≝ |
---|
[3066] | 362 | { virtual_dptr : Identifier × Z |
---|
| 363 | ; actual_dptr : Identifier × Z |
---|
[3039] | 364 | ; built_code : list (list labelled_instruction) |
---|
| 365 | ; built_preamble : list (Identifier × Word) |
---|
[2984] | 366 | }. |
---|
[2946] | 367 | |
---|
[3039] | 368 | definition store_byte_or_Identifier : |
---|
| 369 | (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝ |
---|
[2984] | 370 | λby,mut. |
---|
| 371 | match mut with |
---|
[3039] | 372 | [ mk_init_mutable virt act acc1 acc2 ⇒ |
---|
[2984] | 373 | let pre ≝ |
---|
[3066] | 374 | if eq_identifier … (\fst virt) (\fst act) then |
---|
| 375 | let off ≝ \snd virt - \snd act in |
---|
| 376 | if eqZb off OZ then [ ] |
---|
| 377 | else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ] |
---|
| 378 | else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] |
---|
| 379 | else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] in |
---|
[3039] | 380 | let post ≝ match by with |
---|
| 381 | [ inl by ⇒ |
---|
| 382 | 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? |
---|
| 383 | 〈ACC_A, DATA by〉))))))〉 |
---|
| 384 | | inr si_id ⇒ |
---|
| 385 | 〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉 |
---|
| 386 | ] in |
---|
[3066] | 387 | mk_init_mutable 〈\fst virt, Zsucc (\snd virt)〉 virt |
---|
[3039] | 388 | ((pre @ |
---|
| 389 | [ post ; |
---|
| 390 | 〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ]) :: |
---|
| 391 | acc1) |
---|
| 392 | acc2 |
---|
[2984] | 393 | ]. @I qed. |
---|
| 394 | |
---|
[3039] | 395 | |
---|
[2946] | 396 | definition do_store_init_data : |
---|
[3051] | 397 | state_monad ASM_universe init_mutable → init_data → |
---|
[3039] | 398 | state_monad ASM_universe init_mutable ≝ |
---|
[3051] | 399 | λm_mut,data. |
---|
[3039] | 400 | ! mut ← m_mut ; |
---|
| 401 | let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in |
---|
| 402 | let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in |
---|
[2946] | 403 | match data with |
---|
| 404 | [ Init_int8 n ⇒ |
---|
[3039] | 405 | return store_byte n mut |
---|
[2946] | 406 | | Init_int16 n ⇒ |
---|
[2984] | 407 | let 〈by0, by1〉 ≝ vsplit ? 8 8 n in |
---|
[3039] | 408 | return store_byte by1 (store_byte by0 mut) |
---|
[2946] | 409 | | Init_int32 n ⇒ |
---|
| 410 | let 〈by0, n〉 ≝ vsplit ? 8 24 n in |
---|
| 411 | let 〈by1, n〉 ≝ vsplit ? 8 16 n in |
---|
| 412 | let 〈by2, by3〉 ≝ vsplit ? 8 8 n in |
---|
[3039] | 413 | return store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut))) |
---|
[2946] | 414 | | Init_addrof symb ofs ⇒ |
---|
[3039] | 415 | ! id ← Identifier_of_ident … symb ; |
---|
| 416 | return store_Identifier HIGH id (store_Identifier LOW id mut) |
---|
[2946] | 417 | | Init_space n ⇒ |
---|
[3066] | 418 | let 〈virt_id, virt_off〉 ≝ virtual_dptr mut in |
---|
| 419 | return mk_init_mutable 〈virt_id, n + virt_off〉 (actual_dptr mut) |
---|
[3039] | 420 | (built_code mut) (built_preamble mut) |
---|
[2984] | 421 | | Init_null ⇒ |
---|
| 422 | let z ≝ bv_zero ? in |
---|
[3039] | 423 | return store_byte z (store_byte z mut) |
---|
[2984] | 424 | ]. |
---|
[2946] | 425 | |
---|
[3039] | 426 | definition do_store_global : |
---|
[3051] | 427 | state_monad ASM_universe init_mutable → |
---|
[3039] | 428 | (ident × region × (list init_data)) → |
---|
| 429 | state_monad ASM_universe init_mutable ≝ |
---|
[3051] | 430 | λm_mut,id_reg_data.! mut ← m_mut ; |
---|
[3039] | 431 | let 〈id, reg, data〉 ≝ id_reg_data in |
---|
| 432 | ! Id ← Identifier_of_ident … id ; |
---|
[3066] | 433 | let mut ≝ mk_init_mutable 〈Id, OZ〉 (actual_dptr … mut) (built_code mut) |
---|
| 434 | (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in |
---|
[3051] | 435 | foldl … do_store_init_data (return mut) data. |
---|
[2946] | 436 | |
---|
[3039] | 437 | let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝ |
---|
| 438 | match l with |
---|
| 439 | [ nil ⇒ acc |
---|
| 440 | | cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl |
---|
| 441 | ]. |
---|
| 442 | |
---|
| 443 | definition translate_premain : ∀p : lin_program.Identifier → |
---|
| 444 | state_monad ASM_universe (list labelled_instruction × (list (Identifier × Word))) ≝ |
---|
[2984] | 445 | λp : lin_program.λexit_label. |
---|
| 446 | ! main ← Identifier_of_ident … (prog_main … p) ; |
---|
| 447 | ! u ← state_get … ; |
---|
[3066] | 448 | (* setting this as actual_dptr will force loading of the correct dptr *) |
---|
| 449 | let dummy_dptr : Identifier × Z ≝ 〈an_identifier … one, -1〉 in |
---|
| 450 | let mut ≝ mk_init_mutable dummy_dptr dummy_dptr [ ] [ ] in |
---|
[3051] | 451 | ! globals_init ← foldl … do_store_global (return mut) (prog_vars … p) ; |
---|
[3066] | 452 | let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … (-(S (globals_stacksize … p)))) in |
---|
[2946] | 453 | let init_isp ≝ |
---|
| 454 | (* initial stack pointer set to 2Fh in order to use addressable bits *) |
---|
| 455 | DATA (zero 2 @@ [[true;false]] @@ maximum 4) in |
---|
| 456 | let isp_direct ≝ |
---|
| 457 | (* 81h = 10000001b *) |
---|
| 458 | DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in |
---|
| 459 | let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in |
---|
| 460 | let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in |
---|
[3039] | 461 | return 〈[ |
---|
[2946] | 462 | 〈None ?, Cost (init_cost_label … p)〉 ; |
---|
| 463 | (* initialize the internal stack pointer past the addressable bits *) |
---|
| 464 | 〈None ?, Instruction |
---|
| 465 | (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? |
---|
| 466 | 〈isp_direct, init_isp〉)))))〉 ; |
---|
| 467 | (* initialize our stack pointer past the globals *) |
---|
| 468 | 〈None ?, Instruction |
---|
| 469 | (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? |
---|
| 470 | 〈reg_spl, DATA spl〉))))))〉 ; |
---|
| 471 | 〈None ?, Instruction |
---|
| 472 | (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? |
---|
| 473 | 〈reg_sph, DATA sph〉))))))〉 ] @ |
---|
[3039] | 474 | reversed_flatten_aux … [ ] (built_code globals_init) @ |
---|
[2984] | 475 | [ 〈None ?, Call main〉 ; |
---|
| 476 | 〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ; |
---|
[3039] | 477 | 〈None ?, Jmp exit_label〉], built_preamble globals_init〉. @I qed. |
---|
[2946] | 478 | |
---|
[2754] | 479 | definition get_symboltable : |
---|
[3039] | 480 | state_monad ASM_universe (list (Identifier × ident)) ≝ |
---|
| 481 | λu. |
---|
[2754] | 482 | let imap ≝ ident_map … u in |
---|
| 483 | let f ≝ λiold,inew.cons ? 〈inew, iold〉 in |
---|
| 484 | 〈u, foldi ??? f imap [ ]〉. |
---|
| 485 | |
---|
[2767] | 486 | definition lin_to_asm : lin_program → option pseudo_assembly_program ≝ |
---|
[696] | 487 | λp. |
---|
[2708] | 488 | state_run ?? (new_ASM_universe p) |
---|
| 489 | (let add_translation ≝ |
---|
| 490 | λacc,id_def. |
---|
| 491 | ! code ← translate_fun_def … id_def ; |
---|
| 492 | ! acc ← acc ; |
---|
| 493 | return (code @ acc) in |
---|
[2984] | 494 | ! exit_label ← ASM_fresh … ; |
---|
[2708] | 495 | ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ; |
---|
[2754] | 496 | ! symboltable ← get_symboltable … ; |
---|
[3039] | 497 | ! 〈init, preamble〉 ← translate_premain p exit_label; |
---|
[2760] | 498 | return |
---|
[2978] | 499 | ( |
---|
| 500 | let code ≝ |
---|
[2984] | 501 | init @ code in |
---|
[2946] | 502 | ! code_ok ← code_size_opt code ; |
---|
| 503 | (* atm no data identifier is used in the code, so preamble must be empty *) |
---|
| 504 | return |
---|
[3039] | 505 | (mk_pseudo_assembly_program preamble code code_ok symboltable exit_label ? ?))). |
---|
[2760] | 506 | cases daemon |
---|
[3023] | 507 | qed. |
---|