source: src/LIN/LINToASM.ma @ 2984

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

better LINToASM initialization of globals (to be tested!)

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