source: src/LIN/LINToASM.ma @ 3433

Last change on this file since 3433 was 3066, checked in by tranquil, 7 years ago
  • implemented get_arg_16 for ACC_DPTR
  • LINToASM is now agnostic as to where single global variables end up, as long as all global variables end up at the bottom of XData
  • consequently, ASM preamble is back indicating sizes rather than addresses
  • Assembly now correctly maps identifiers with offsets in case of code points
File size: 19.7 KB
RevLine 
[698]1include "utilities/BitVectorTrieSet.ma".
[2708]2include "utilities/state.ma".
[1264]3
[2767]4include "ASM/Util.ma".
5include "ASM/ASM.ma".
6
7include "LIN/LIN.ma".
8
[2708]9(* utilities to provide Identifier's and addresses  *)
[3039]10record 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]18definition 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]28definition Identifier_of_label :
[3039]29  label → state_monad ASM_universe Identifier ≝
30λl,u.
[2708]31let current ≝ current_funct … u in
32let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
33let 〈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
43definition Identifier_of_ident :
[3039]44  ident → state_monad ASM_universe Identifier ≝
45λi,u.
[2708]46let imap ≝ ident_map … u in
[3039]47let 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]53let id ≝ \fst (\fst res) in
54let univ ≝ \snd (\fst res) in
55let 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]59definition new_ASM_universe :
60∀p : joint_program LIN.ASM_universe ≝
61λp.
62mk_ASM_universe (mk_universe … one)
63  (an_identifier … one (* dummy *))
64  (empty_map …) (empty_map …) one.
65(*@hide_prf normalize nodelta
66cases p -p * #vars #functs #main #cost_init
67#i #H
68normalize nodelta
69letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉)
70cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
71[ %2{H} ] -H
72lapply i -i lapply init_val -init_val
73whd in match prog_var_names; normalize nodelta
74elim 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]
86qed.
87*)
88
[2708]89definition 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
96definition 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]102definition 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]120definition vector_cast :
121∀A,n,m.A → Vector A n → Vector A m ≝
122λA,n,m,dflt,v.
123If leb n m then with prf do
124  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
125else with prf do
126  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
127lapply 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
132qed.
133
[2490]134definition 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]143qed.
[491]144
[2286]145definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
[2443]146
[491]147definition data_of_int ≝ λbv. DATA bv.
[686]148definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
149definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
[491]150
[2286]151(* TODO: check and change to free bit *)
152definition asm_other_bit ≝ BIT_ADDR (zero_byte).
[3039]153definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].
[2286]154
[2708]155definition 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]320qed.
321
[1268]322
[723]323definition 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]335definition translate_code ≝
[2708]336  λglobals.
337  λcode: list (lin_statement globals).
338    m_list_map … (build_translated_statement globals) code.
[723]339
[696]340definition 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]361record 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]368definition store_byte_or_Identifier :
369  (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
[2984]370λby,mut.
371match 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]396definition 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 ;
401let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
402let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
[2946]403match 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]426definition 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]437let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
438match l with
439[ nil ⇒ acc
440| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
441].
442
443definition 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]479definition 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]486definition 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]506cases daemon
[3023]507qed.
Note: See TracBrowser for help on using the repository browser.