source: src/LIN/LINToASM.ma @ 3040

Last change on this file since 3040 was 3040, checked in by tranquil, 7 years ago

fixed LINToASM

File size: 19.4 KB
Line 
1include "utilities/BitVectorTrieSet.ma".
2include "utilities/state.ma".
3
4include "ASM/Util.ma".
5include "ASM/ASM.ma".
6
7include "LIN/LIN.ma".
8
9(* utilities to provide Identifier's and addresses  *)
10record ASM_universe : Type[0] :=
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)
15; fresh_cost_label: Pos
16}.
17
18definition report_cost:
19 costlabel → state_monad ASM_universe unit ≝
20 λcl,u.
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)
24    (label_map … u) (succ clw), it〉 
25  else
26   〈u,it〉.
27
28definition Identifier_of_label :
29  label → state_monad ASM_universe Identifier ≝
30λl,u.
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)
41  (fresh_cost_label … u), id〉.
42
43definition Identifier_of_ident :
44  ident → state_monad ASM_universe Identifier ≝
45λi,u.
46let imap ≝ ident_map … u in
47let res ≝ match lookup … imap i with
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
53let id ≝ \fst (\fst res) in
54let univ ≝ \snd (\fst res) in
55let imap ≝ \snd res in
56〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
57  (fresh_cost_label … u), id〉.
58
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
89definition start_funct_translation :
90  ∀globals,functions.(ident × (joint_function LIN globals functions)) →
91    state_monad ASM_universe unit ≝
92  λg,functs,id_f,u.
93    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
94      (fresh_cost_label … u), it〉.
95
96definition ASM_fresh :
97  state_monad ASM_universe Identifier ≝
98λu.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
99〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
100  (fresh_cost_label … u), id〉.
101
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)
115    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 130)
116    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 131)
117    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
118    ]. @I qed.
119
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
134definition arg_address : hdw_argument →
135  [[ acc_a ; direct ; registr ; data ]] ≝
136  λa.
137  match a
138  with
139  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
140  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
141  ].
142  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
143qed.
144
145definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
146
147definition data_of_int ≝ λbv. DATA bv.
148definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
149definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
150
151(* TODO: check and change to free bit *)
152definition asm_other_bit ≝ BIT_ADDR (zero_byte).
153definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].
154
155definition translate_statements :
156  ∀globals.
157  joint_statement LIN globals →
158  state_monad ASM_universe pseudo_instruction ≝
159  λglobals,statement.
160  match statement with
161  [ final instr ⇒
162    match instr with
163    [ GOTO lbl ⇒
164      ! lbl' ← Identifier_of_label … lbl ;
165      return Jmp (toASM_ident ? lbl')
166    | RETURN ⇒ return Instruction (RET ?)
167    | TAILCALL abs _ _ ⇒ Ⓧabs
168    ]
169  | sequential instr _ ⇒
170      match instr with
171      [ step_seq instr' ⇒
172        match instr' with
173        [ extension_seq ext ⇒
174          match ext with
175          [ SAVE_CARRY ⇒
176            return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
177          | RESTORE_CARRY ⇒
178            return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
179          | LOW_ADDRESS lbl ⇒
180            ! lbl' ← Identifier_of_label … lbl ;
181            return Mov (inr ?? 〈register_address RegisterA, LOW〉) lbl' one_word
182          | HIGH_ADDRESS lbl ⇒
183            ! lbl' ← Identifier_of_label … lbl ;
184            return Mov (inr ?? 〈register_address RegisterA, HIGH〉) lbl' one_word
185          ]
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)
190        | OPACCS accs _ _ _ _ ⇒
191          return match accs with
192          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
193          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
194          ]
195        | OP1 op1 _ _ ⇒
196          return match op1 with
197          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
198          | Inc ⇒ Instruction (INC ? ACC_A)
199          | Rl ⇒ Instruction (RL ? ACC_A)
200          ]
201        | OP2 op2 _ _ reg ⇒
202          return match arg_address … reg
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 …)
244        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
245        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
246        | ADDRESS id proof off _ _ ⇒
247          ! Id ← Identifier_of_ident … id ;
248          return (Mov (inl ?? DPTR) Id off)
249        | SET_CARRY ⇒
250          return Instruction (SETB ? CARRY)
251        | MOVE regs ⇒
252          return match regs with
253          [ to_acc _ reg ⇒
254            match register_address reg return λx.is_in … [[ acc_a;
255                                                              direct;
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;
267                                                              direct;
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〉))))))
297          ]
298        ]
299      | CALL f _ _ ⇒
300        match f with
301        [ inl id ⇒
302          ! id' ← Identifier_of_ident … id ;
303          return Call (toASM_ident ? id')
304        | inr _ ⇒
305          return Instruction (JMP … ACC_DPTR)
306        ]
307      | COST_LABEL lbl ⇒
308         !_ report_cost … lbl ;
309         return Cost lbl
310      | COND _ lbl ⇒
311        ! l ← Identifier_of_label … lbl;
312        return Instruction (JNZ ? l)
313      ]
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
318    ].
319  try @I
320qed.
321
322
323definition build_translated_statement ≝
324  λglobals.
325  λstatement: lin_statement globals.
326  ! stmt ← translate_statements globals (\snd statement) ;
327  match \fst statement with
328  [ Some lbl ⇒
329    ! lbl' ← Identifier_of_label … lbl ;
330    return 〈Some ? lbl', stmt〉
331  | None ⇒
332    return 〈None ?, stmt〉
333  ].
334
335definition translate_code ≝
336  λglobals.
337  λcode: list (lin_statement globals).
338    m_list_map … (build_translated_statement globals) code.
339
340definition translate_fun_def ≝
341  λglobals,functions.
342  λid_def : ident × (joint_function LIN globals functions).
343  !_ start_funct_translation … id_def ;
344  (* ^ modify current function id ^ *)
345  match \snd id_def with
346    [ Internal int ⇒
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 *)
352      | cons hd tl ⇒
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        ]
357      ]
358    | External _ ⇒ return [ ]
359    ].
360
361record init_mutable : Type[0] ≝
362{ virtual_dptr : Z
363; actual_dptr : Z
364; built_code : list (list labelled_instruction)
365; built_preamble : list (Identifier × Word)
366}.
367
368definition store_byte_or_Identifier :
369  (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
370λby,mut.
371match mut with
372[ mk_init_mutable virt act acc1 acc2 ⇒
373  let off ≝ virt - act in
374  let pre ≝
375    if eqZb off OZ then [ ]
376    else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ]
377    else [ 〈None ?, Instruction (MOV ? (inl … (inl … (inr …
378        〈DPTR, DATA16 (bitvector_of_Z … virt)〉))))〉 ] in
379  let post ≝ match by with
380    [ inl by ⇒
381      〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
382                               〈ACC_A, DATA by〉))))))〉
383    | inr si_id ⇒
384      〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉
385    ] in
386  mk_init_mutable (Zsucc virt) virt
387    ((pre @
388      [ post ;
389       〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ]) ::
390     acc1)
391    acc2 
392]. @I qed.
393
394
395definition do_store_init_data :
396  init_data → state_monad ASM_universe init_mutable →
397  state_monad ASM_universe init_mutable ≝
398λdata,m_mut.
399! mut ← m_mut ;
400let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
401let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
402match data with
403[ Init_int8 n ⇒
404  return store_byte n mut
405| Init_int16 n ⇒
406  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in
407  return store_byte by1 (store_byte by0 mut)
408| Init_int32 n ⇒
409  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
410  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
411  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
412  return store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut)))
413| Init_addrof symb ofs ⇒
414  ! id ← Identifier_of_ident … symb ;
415  return store_Identifier HIGH id (store_Identifier LOW id mut)
416| Init_space n ⇒
417  return mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut)
418    (built_code mut) (built_preamble mut)
419| Init_null ⇒
420  let z ≝ bv_zero ? in
421  return store_byte z (store_byte z mut)
422].
423
424definition do_store_global :
425  (ident × region × (list init_data)) →
426    state_monad ASM_universe init_mutable →
427    state_monad ASM_universe init_mutable ≝
428  λid_reg_data,m_mut.! mut ← m_mut ;
429  let 〈id, reg, data〉 ≝ id_reg_data in
430  ! Id ← Identifier_of_ident … id ;
431  let mut ≝ mk_init_mutable (virtual_dptr mut) (actual_dptr mut) (built_code mut)
432      (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in
433  foldr … do_store_init_data (return mut) data.
434
435let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
436match l with
437[ nil ⇒ acc
438| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
439].
440
441definition translate_premain : ∀p : lin_program.Identifier →
442  state_monad ASM_universe (list labelled_instruction × (list (Identifier × Word))) ≝
443  λp : lin_program.λexit_label.
444  ! main ← Identifier_of_ident … (prog_main … p) ;
445  ! u ← state_get … ;
446  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
447  let start_sp : Z ≝ -(S (globals_stacksize … p)) in
448  let mut ≝ mk_init_mutable start_sp OZ [ ] [ ] in
449  ! globals_init ← foldr … do_store_global (return mut) (prog_vars … p) ;
450  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
451  let init_isp ≝
452    (* initial stack pointer set to 2Fh in order to use addressable bits *)
453    DATA (zero 2 @@ [[true;false]] @@ maximum 4) in
454  let isp_direct ≝
455    (* 81h = 10000001b *)
456    DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in
457  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
458  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
459  return 〈[
460    〈None ?, Cost (init_cost_label … p)〉 ;
461    (* initialize the internal stack pointer past the addressable bits *)
462    〈None ?, Instruction
463    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
464      〈isp_direct, init_isp〉)))))〉 ;
465    (* initialize our stack pointer past the globals *)
466    〈None ?, Instruction
467    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
468      〈reg_spl, DATA spl〉))))))〉 ;
469    〈None ?, Instruction
470    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
471      〈reg_sph, DATA sph〉))))))〉 ] @
472  reversed_flatten_aux … [ ] (built_code globals_init) @
473  [ 〈None ?, Call main〉 ;
474    〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ;
475    〈None ?, Jmp exit_label〉], built_preamble globals_init〉. @I qed.
476
477definition get_symboltable :
478  state_monad ASM_universe (list (Identifier × ident)) ≝
479  λu.
480  let imap ≝ ident_map … u in
481  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
482  〈u, foldi ??? f imap [ ]〉.
483
484definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
485  λp.
486  state_run ?? (new_ASM_universe p)
487    (let add_translation ≝
488      λacc,id_def.
489      ! code ← translate_fun_def … id_def ;
490      ! acc ← acc ;
491      return (code @ acc) in
492     ! exit_label ← ASM_fresh … ;
493     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
494     ! symboltable ← get_symboltable … ;
495     ! 〈init, preamble〉 ← translate_premain p exit_label;
496     return
497       (
498        let code ≝
499        init @ code in
500        ! code_ok ← code_size_opt code ; 
501        (* atm no data identifier is used in the code, so preamble must be empty *)
502        return
503          (mk_pseudo_assembly_program preamble code code_ok symboltable exit_label ? ?))).
504cases daemon
505qed.
Note: See TracBrowser for help on using the repository browser.