source: src/LIN/LINToASM.ma @ 3014

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

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

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