source: src/LIN/LINToASM.ma @ 2975

Last change on this file since 2975 was 2975, checked in by tranquil, 6 years ago
  • RTL premain fixed
  • fixed bug in back end ops (subtracting to a porinter was reversed)
  • fixed globals initialization in LINToASM
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
369definition store_bytes : list Byte → list labelled_instruction ≝
370λbytes.
371\fold[(append ?), (nil ?)]_{by ∈ bytes}
372    [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA by〉))))))〉 ;
373      〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ;
374      〈None ?, Instruction (INC ? DPTR)〉 ]. @I qed.
375
376definition do_store_init_data :
377  ∀globals.ASM_universe globals → Z → init_data → list labelled_instruction ≝
378λglobals,u,nxt_dptr,data.
379match data with
380[ Init_int8 n ⇒
381  store_bytes [ n ]
382| Init_int16 n ⇒
383  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in store_bytes [ by0 ; by1 ]
384| Init_int32 n ⇒
385  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
386  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
387  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
388  store_bytes [ by0 ; by1 ; by2 ; by3 ]
389| Init_addrof symb ofs ⇒
390  let addr : Word ≝
391    match lookup … (address_map … u) symb with
392    [ Some x ⇒ bitvector_of_Z ? (Z_of_unsigned_bitvector … x + ofs)
393    | None ⇒ bv_zero ?
394    ] in
395  let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in
396  store_bytes [by0 ; by1] 
397| Init_space n ⇒
398  (* if n = 1 it is better to use INC, ow we can set the DPTR with MOV *)
399  match n with
400  [ O ⇒ [ ]
401  | S k ⇒
402    match k with
403    [ O ⇒ [ 〈None ?, Instruction (INC ? DPTR)〉 ]
404    | _ ⇒ [ 〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … nxt_dptr)〉))))〉 ]
405    ]
406  ]
407| Init_null ⇒ store_bytes [ bv_zero ? ; bv_zero ? ]
408]. @I qed.
409
410definition do_store_init_data_list :
411  ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
412λglobals,u,start_dptr,data.
413let f ≝ λdata,dptr_acc.
414  let 〈dptr, acc〉 ≝ dptr_acc in
415  let nxt_dptr ≝ dptr + size_init_data data in
416  〈nxt_dptr, do_store_init_data … u nxt_dptr data @ acc〉 in
417〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … start_dptr)〉))))〉 ::
418\snd (foldr ?? f 〈start_dptr, [ ]〉 data).
419
420definition translate_initialization : ∀p : lin_program.
421  state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
422  λp : lin_program.λu.
423  let start_sp : Z ≝ -(globals_stacksize … p) in
424  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
425  let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
426  let init_isp ≝
427    (* initial stack pointer set to 2Fh in order to use addressable bits *)
428    DATA (zero 2 @@ [[true;false]] @@ maximum 4) in
429  let isp_direct ≝
430    (* 81h = 10000001b *)
431    DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in
432  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
433  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
434  〈u, [
435    〈None ?, Cost (init_cost_label … p)〉 ;
436    (* initialize the internal stack pointer past the addressable bits *)
437    〈None ?, Instruction
438    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
439      〈isp_direct, init_isp〉)))))〉 ;
440    (* initialize our stack pointer past the globals *)
441    〈None ?, Instruction
442    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
443      〈reg_spl, DATA spl〉))))))〉 ;
444    〈None ?, Instruction
445    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
446      〈reg_sph, DATA sph〉))))))〉 ] @
447  do_store_init_data_list ? u start_sp data〉. @I qed.
448
449definition get_symboltable :
450  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
451  λglobals,u.
452  let imap ≝ ident_map … u in
453  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
454  〈u, foldi ??? f imap [ ]〉.
455
456definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
457  λp.
458  state_run ?? (new_ASM_universe p)
459    (let add_translation ≝
460      λacc,id_def.
461      ! code ← translate_fun_def … id_def ;
462      ! acc ← acc ;
463      return (code @ acc) in
464     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
465     ! exit_label ← ASM_fresh … ;
466     ! main ← Identifier_of_ident … (prog_main … p) ;
467     ! symboltable ← get_symboltable … ;
468     ! init ← translate_initialization p ;
469     ! u ← state_get … ;
470     return
471       (
472        let code ≝
473        init @
474         〈None ?, Call main〉 ::
475         〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ::
476         〈None ?, Jmp exit_label〉 :: code in
477        ! code_ok ← code_size_opt code ; 
478        (* atm no data identifier is used in the code, so preamble must be empty *)
479        return
480          (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
481cases daemon
482qed.
Note: See TracBrowser for help on using the repository browser.