source: src/RTLabs/RTLAbstoRTL.ma @ 1239

Last change on this file since 1239 was 1239, checked in by sacerdot, 8 years ago

RTLAbstoRTL ported to new datatypes.

Note: RTL syntax/semantics is not (yet?) an instance of Joint.

File size: 41.4 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/FrontEndOps.ma".
5include "common/Graphs.ma".
6
7definition add_graph ≝
8  λl: label.
9  λstmt.
10  λp.
11  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
12  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
13  let rtl_if_result' ≝ rtl_if_result p in
14  let rtl_if_params' ≝ rtl_if_params p in
15  let rtl_if_locals' ≝ rtl_if_locals p in
16  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
17  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
18  let rtl_if_entry' ≝ rtl_if_entry p in
19  let rtl_if_exit' ≝ rtl_if_exit p in
20    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
21                             rtl_if_params' rtl_if_params' rtl_if_locals'
22                             rtl_if_stacksize' rtl_if_graph' ? ?.
23  [1: cases(rtl_if_entry')
24      #LABEL #HYP %
25      [1: @LABEL
26      |2: cases(HYP)
27          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
28          normalize nodelta;
29          /2/
30      ]
31  |2: cases(rtl_if_exit')
32      #LABEL #HYP %
33      [1: @LABEL
34      |2: cases(HYP)
35          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
36          normalize nodelta;
37          /2/
38      ]
39  ]
40qed.
41     
42definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
43  λdef.
44    let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in
45    let locals ≝ rtl_if_locals def in
46    let rtl_if_luniverse' ≝ new_univ in
47    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
48    let rtl_if_result' ≝ rtl_if_result def in
49    let rtl_if_params' ≝ rtl_if_params def in
50    let rtl_if_locals' ≝ rtl_if_locals def in
51    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
52    let rtl_if_graph' ≝ rtl_if_graph def in
53    let rtl_if_entry' ≝ rtl_if_entry def in
54    let rtl_if_exit' ≝ rtl_if_exit def in
55      〈mk_rtl_internal_function
56        rtl_if_luniverse' rtl_if_runiverse' rtl_if_result'
57        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
58        rtl_if_entry' rtl_if_exit', lbl〉.
59
60axiom register_fresh: universe RegisterTag → register.
61
62definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
63  λdef.
64    let r ≝ register_fresh (rtl_if_runiverse def) in
65    let locals ≝ r :: rtl_if_locals def in
66    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
67    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
68    let rtl_if_result' ≝ rtl_if_result def in
69    let rtl_if_params' ≝ rtl_if_params def in
70    let rtl_if_locals' ≝ locals in
71    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
72    let rtl_if_graph' ≝ rtl_if_graph def in
73    let rtl_if_entry' ≝ rtl_if_entry def in
74    let rtl_if_exit' ≝ rtl_if_exit def in
75      〈mk_rtl_internal_function
76        rtl_if_luniverse' rtl_if_runiverse' rtl_if_result'
77        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
78        rtl_if_entry' rtl_if_exit', r〉.
79       
80let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
81  match n with
82  [ O   ⇒ 〈def, [ ]〉
83  | S n ⇒
84    let 〈def, res〉 ≝ fresh_regs def n in
85    let 〈def, r〉 ≝ fresh_reg def in
86      〈def, r :: res〉
87  ].
88
89axiom fresh_regs_length:
90  ∀def: rtl_internal_function.
91  ∀n: nat.
92    |(\snd (fresh_regs def n))| = n.
93   
94definition addr_regs ≝
95  λregs.
96  match regs with
97  [ cons hd tl ⇒
98    match tl with
99    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
100    | nil          ⇒ None (register × register)
101    ]
102  | nil ⇒ None (register × register) (* registers are not an address *)
103  ].
104
105let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
106  match n with
107  [ O ⇒ [ ]
108  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
109  ].
110
111definition choose_rest ≝
112  λA: Type[0].
113  λleft, right: list A.
114  λprfl: 0 < |left|.
115  λprfr: 0 < |right|.
116  match left return λx. 0 < |x| → list A with
117  [ nil ⇒ λnil_prf.
118    match right return λx. 0 < |x| → list A with
119    [ nil ⇒ λnil_nil_absrd. ?
120    | _ ⇒ λnil_cons_prf. right
121    ] prfr
122  | _ ⇒ λcons_prf. right
123  ] prfl.
124  normalize in nil_prf;
125  cases(not_le_Sn_O 0)
126  #HYP
127  cases(HYP nil_prf)
128qed.
129
130definition complete_regs ≝
131  λdef.
132  λsrcrs1.
133  λsrcrs2.
134  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
135  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
136    if gtb nb_added 0 then
137      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
138    else
139      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
140
141(* obvious, but proof doesn't look easy! *)
142axiom complete_regs_length:
143  ∀def.
144  ∀left.
145  ∀right.
146    |\fst (\fst (complete_regs def left right))| = |\snd (\fst (complete_regs def left right))|.
147
148definition size_of_sig_type ≝
149  λsig.
150  match sig with
151  [ ASTint isize sign ⇒
152    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
153      isize' ÷ (nat_of_bitvector ? int_size)
154  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
155  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
156  ].
157  cases not_implemented;
158qed.
159
160inductive register_type: Type[0] ≝
161  | register_int: register → register_type
162  | register_ptr: register → register → register_type.
163
164definition local_env ≝ BitVectorTrie (list register).
165
166definition mem_local_env ≝
167  λr: register.
168  match r with
169  [ an_identifier w ⇒ member (list register) 16 w
170  ].
171
172definition add_local_env ≝
173  λr: register.
174  match r with
175  [ an_identifier w ⇒ insert (list register) 16 w
176  ].
177
178definition find_local_env ≝
179  λr: register.
180  λbvt.
181  match r with
182  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
183  ].
184
185definition initialize_local_env_internal ≝
186  λruniverse.
187  λlenv.
188  λr_sig.
189  let 〈r, sig〉 ≝ r_sig in
190  let size ≝ size_of_sig_type sig in
191  let rs ≝ register_freshes runiverse size in
192    add_local_env r rs lenv.
193
194definition initialize_local_env ≝
195  λruniverse.
196  λregisters.
197  λresult.
198  let registers ≝ registers @
199    match result with
200    [ None ⇒ [ ]
201    | Some rt ⇒ [ rt ]
202    ]
203  in
204    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
205 
206definition map_list_local_env_internal ≝
207  λlenv.
208  λres.
209  λr.
210    res @ (find_local_env r lenv).
211   
212definition map_list_local_env ≝
213  λlenv.
214  λregs.
215    foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
216
217definition make_addr ≝
218  λA.
219  λlst: list A.
220  λprf: 2 ≤ length A lst.
221  match lst return λx. 2 ≤ |x| → A × A with
222  [ nil ⇒ λlst_nil_prf. ?
223  | cons hd tl ⇒ λprf.
224    match tl return λx. 1 ≤ |x| → A × A with
225    [ nil ⇒ λtl_nil_prf. ?
226    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
227    ] ?
228  ] prf.
229  [1: normalize in lst_nil_prf;
230      cases(not_le_Sn_O 1);
231      #HYP cases(HYP lst_nil_prf)
232  |2: normalize in prf;
233      @le_S_S_to_le
234      assumption
235  |3: normalize in tl_nil_prf;
236      cases(not_le_Sn_O 0)
237      #HYP cases(HYP tl_nil_prf)
238  ]
239qed.
240
241definition find_and_addr ≝
242  λr.
243  λlenv.
244    make_addr ? (find_local_env r lenv).
245
246definition rtl_args ≝
247  λregs_list.
248  λlenv.
249    flatten ? (map ? ? (
250      λr. find_local_env r lenv) regs_list).
251
252definition change_label ≝
253  λlbl.
254  λstmt: rtl_statement.
255  match stmt with
256  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
257  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
258  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
259  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
260  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
261  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
262  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
263  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
264  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
265  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
266  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
267  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
268  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
269  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
270  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
271  | rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2
272  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
273  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
274  | rtl_st_return ⇒ rtl_st_return
275  ].
276
277(* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
278   of implementing everything as a bitvector, which is bounded.  If we implemented
279   labels as unbounded nats then this function will never fail.
280*)
281(* Fixed with changes to label generation.
282*)
283let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
284  match stmt_list with
285  [ nil ⇒ def
286  | cons hd tl ⇒
287    match tl with
288    [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
289    | cons hd' tl' ⇒
290      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
291      let stmt ≝ change_label tmp_lbl hd in
292      let def ≝ add_graph start_lbl stmt new_def in
293        adds_graph tl tmp_lbl dest_lbl new_def
294    ]
295  ].
296
297let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
298                       (def: ?) on translate_list ≝
299  match translate_list with
300  [ nil ⇒ def
301  | cons hd tl ⇒
302    match tl with
303    [ nil ⇒ hd start_lbl dest_lbl def
304    | cons hd' tl' ⇒
305      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
306      let applied ≝ hd start_lbl tmp_lbl new_def in
307        add_translates tl tmp_lbl dest_lbl applied
308    ]
309  ].
310
311definition translate_cst_int_internal ≝
312  λdest_lbl.
313  λr.
314  λi.
315    rtl_st_int r i dest_lbl.
316
317axiom translate_cst:
318  ∀cst: constant.
319  ∀destrs: list register.
320  ∀start_lbl: label.
321  ∀dest_lbl: label.
322  ∀def: rtl_internal_function.
323    rtl_internal_function.
324
325definition translate_move_internal ≝
326  λstart_lbl: label.
327  λdestr: register.
328  λsrcr: register.
329    rtl_st_move destr srcr start_lbl.
330
331definition translate_move ≝
332  λdestrs: list register.
333  λsrcrs: list register.
334  λstart_lbl: label.
335    match reduce_strong register register destrs srcrs with
336    [ dp crl_crr len_proof ⇒
337      let commonl ≝ \fst (\fst crl_crr) in
338      let commonr ≝ \fst (\snd crl_crr) in
339      let restl ≝ \snd (\fst crl_crr) in
340      let restr ≝ \snd (\snd crl_crr) in
341      let f_common ≝ translate_move_internal start_lbl in
342      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
343      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
344        add_translates [ translate1 ; translate2 ] start_lbl
345    ].
346    @len_proof
347qed.
348
349let rec make
350  (A: Type[0]) (elt: A) (n: nat) on n ≝
351  match n with
352  [ O ⇒ [ ]
353  | S n' ⇒ elt :: make A elt n'
354  ].
355 
356lemma make_length:
357  ∀A: Type[0].
358  ∀elt: A.
359  ∀n: nat.
360    n = length ? (make A elt n).
361  #A #ELT #N
362  elim N
363  [ normalize %
364  | #N #IH
365    normalize <IH %
366  ]
367qed.
368
369definition translate_cast_unsigned ≝
370  λdestrs.
371  λstart_lbl.
372  λdest_lbl.
373  λdef.
374  let 〈def, tmp_zero〉 ≝ fresh_reg def in
375  let zeros ≝ make ? tmp_zero (length ? destrs) in
376    add_translates [
377      adds_graph [
378        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
379        ];
380      translate_move destrs zeros
381    ] start_lbl dest_lbl def.
382
383definition translate_cast_signed ≝
384  λdestrs.
385  λsrcr.
386  λstart_lbl.
387  λdest_lbl.
388  λdef.
389  let 〈def, tmp_128〉 ≝ fresh_reg def in
390  let 〈def, tmp_255〉 ≝ fresh_reg def in
391  let 〈def, tmpr〉 ≝ fresh_reg def in
392  let 〈def, dummy〉 ≝ fresh_reg def in
393  let insts ≝ [
394    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
395    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
396    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
397    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
398    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
399  ] in
400  let srcrs ≝ make ? tmpr (length ? destrs) in
401    add_translates [
402      adds_graph insts;
403      translate_move destrs srcrs
404    ] start_lbl dest_lbl def.
405
406definition translate_cast ≝
407  λsrc_size.
408  λsrc_sign.
409  λdest_size.
410  λdestrs.
411  λsrcrs.
412  match |srcrs| return λx. |srcrs| = x → ? with
413  [ O ⇒ λzero_prf. adds_graph [ ]
414  | S n' ⇒ λsucc_prf.
415    if ltb dest_size src_size then
416      translate_move destrs srcrs
417    else
418      match reduce_strong register register destrs srcrs with
419      [ dp crl len_proof ⇒
420        let commonl ≝ \fst (\fst crl) in
421        let commonr ≝ \fst (\snd crl) in
422        let restl ≝ \snd (\fst crl) in
423        let restr ≝ \snd (\snd crl) in
424        let insts_common ≝ translate_move commonl commonr in
425        let sign_reg ≝ last_safe ? srcrs ? in
426        let insts_sign ≝
427          match src_sign with
428          [ Unsigned ⇒ translate_cast_unsigned restl
429          | Signed ⇒ translate_cast_signed restl sign_reg
430          ]
431        in
432          add_translates [ insts_common; insts_sign ]
433      ]
434  ] (refl ? (|srcrs|)).
435  >succ_prf //
436qed.
437
438definition translate_negint ≝
439  λdestrs.
440  λsrcrs.
441  λstart_lbl.
442  λdest_lbl.
443  λdef.
444  λprf: | destrs | = | srcrs |. (* assert in caml code *)
445  let 〈def, tmpr〉 ≝ fresh_reg def in
446  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
447  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
448  let insts_init ≝ [
449    rtl_st_set_carry start_lbl;
450    rtl_st_int tmpr (zero ?) start_lbl
451  ] in
452  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
453  let insts_add ≝ map … f_add destrs in
454    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
455
456definition translate_notbool ≝
457  λdestrs.
458  λsrcrs.
459  λstart_lbl.
460  λdest_lbl.
461  λdef.
462  match destrs with
463  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
464  | cons destr destrs ⇒
465    let 〈def, tmpr〉 ≝ fresh_reg def in
466    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
467    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
468    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
469    let f ≝ λtmp_srcr. [
470      rtl_st_clear_carry start_lbl;
471      rtl_st_int tmpr (zero ?) start_lbl;
472      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
473      rtl_st_int tmpr (zero ?) start_lbl;
474      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
475      rtl_st_op2 Xor destr destr tmpr start_lbl
476    ] in
477    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
478    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
479      add_translates [
480        save_srcrs; adds_graph insts; epilogue
481      ] start_lbl dest_lbl def
482  ].
483
484(* TODO: examine this properly.  This is a change from the O'caml code due
485   to us dropping the explicit use of a cast destination size field.  We
486   instead infer the size of the cast's destination from the context.  Is
487   this correct?
488*)
489definition translate_op1 ≝
490  λop1: unary_operation.
491  λdestrs: list register.
492  λsrcrs: list register.
493  λprf: |destrs| = |srcrs|.
494  λstart_lbl: label.
495  λdest_lbl: label.
496  λdef: rtl_internal_function.
497  match op1 with
498  [ Ocastint src_sign src_size ⇒
499    let dest_size ≝ |destrs| * 8 in
500    let src_size ≝ bitsize_of_intsize src_size in
501      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
502  | Onegint ⇒
503      translate_negint destrs srcrs start_lbl dest_lbl def prf
504  | Onotbool ⇒
505      translate_notbool destrs srcrs start_lbl dest_lbl def
506  | Onotint ⇒
507    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
508    let l ≝ map2 … f destrs srcrs prf in
509      adds_graph l start_lbl dest_lbl def
510  | Optrofint r ⇒
511      translate_move destrs srcrs start_lbl dest_lbl def
512  | Ointofptr r ⇒
513      translate_move destrs srcrs start_lbl dest_lbl def
514  | Oid ⇒
515      translate_move destrs srcrs start_lbl dest_lbl def
516  | _ ⇒ ? (* float operations implemented in runtime *)
517  ].
518  cases not_implemented
519qed.
520 
521definition translate_op ≝
522  λop.
523  λdestrs.
524  λsrcrs1.
525  λsrcrs2.
526  λstart_lbl.
527  λdest_lbl.
528  λdef.
529  match reduce_strong register register srcrs1 srcrs2 with
530  [ dp reduced first_reduced_proof ⇒
531    let srcrsl_common ≝ \fst (\fst reduced) in
532    let srcrsr_common ≝ \fst (\snd reduced) in
533    let srcrsl_rest ≝ \snd (\fst reduced) in
534    let srcrsr_rest ≝ \snd (\snd reduced) in
535    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
536    match reduce_strong register register destrs srcrsl_common with
537    [ dp reduced second_reduced_proof ⇒
538      let destrs_common ≝ \fst (\fst reduced) in
539      let destrs_rest ≝ \snd (\fst reduced) in
540      match reduce_strong register register destrs_rest srcrs_rest with
541      [ dp reduced third_reduced_proof ⇒
542        let destrs_cted ≝ \fst (\fst reduced) in
543        let destrs_rest ≝ \snd (\fst reduced) in
544        let srcrs_cted ≝ \fst (\snd reduced) in
545        let 〈def, tmpr〉 ≝ fresh_reg def in
546        let insts_init ≝ [
547          rtl_st_clear_carry start_lbl;
548          rtl_st_int tmpr (zero ?) start_lbl
549        ] in
550        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
551        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
552        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
553        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
554        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
555        let insts_rest ≝ map … f_rest destrs_rest in
556          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
557      ]
558    ]
559  ].
560  [1: @third_reduced_proof
561  |3: @first_reduced_proof
562  |*: cases daemon (* TODO *)
563  ]
564qed.
565
566let rec translate_mul1
567  (dummy: register) (tmpr: register) (destrs: list register)
568  (srcrs1: list register) (srcr2: register) (start_lbl: label)
569    on srcrs1 ≝
570  match destrs with
571  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
572  | cons destr tl ⇒
573    match tl with
574    [ nil ⇒
575      match srcrs1 with
576      [ nil ⇒
577        adds_graph [
578          rtl_st_int tmpr (zero ?) start_lbl;
579          rtl_st_op2 Addc destr destr tmpr start_lbl
580        ] start_lbl
581      | cons srcr1 tl' ⇒
582        adds_graph [
583          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
584          rtl_st_op2 Addc destr destr tmpr start_lbl
585        ] start_lbl
586      ]
587    | cons destr2 destrs ⇒
588      match srcrs1 with
589      [ nil ⇒
590        add_translates [
591          adds_graph [
592            rtl_st_int tmpr (zero ?) start_lbl;
593            rtl_st_op2 Addc destr destr tmpr start_lbl;
594            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
595          ];
596          translate_cst (Ointconst I8 (zero ?)) destrs
597        ] start_lbl
598      | cons srcr1 srcrs1 ⇒
599        match destrs with
600        [ nil ⇒
601          add_translates [
602            adds_graph [
603              rtl_st_int tmpr (zero ?) start_lbl;
604              rtl_st_op2 Addc destr destr tmpr start_lbl;
605              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
606            ];
607            translate_cst (Ointconst I8 (zero ?)) destrs
608          ] start_lbl
609        | cons destr2 destrs ⇒
610          add_translates [
611            adds_graph [
612              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
613              rtl_st_op2 Addc destr destr tmpr start_lbl
614            ];
615            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
616          ] start_lbl
617        ]
618      ]
619    ]
620  ].
621
622definition translate_muli ≝
623  λdummy: register.
624  λtmpr: register.
625  λdestrs: list register.
626  λtmp_destrs: list register.
627  λsrcrs1: list register.
628  λdummy_lbl: label.
629  λi: nat.
630  λi_prf.
631  λtranslates: list ?.
632  λsrcr2i: register.
633  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
634  let tmp_destrs2' ≝
635    match tmp_destrs2 with
636    [ nil ⇒ [ ]
637    | cons tmp_destr2 tmp_destrs2 ⇒ [
638        adds_graph [
639          rtl_st_clear_carry dummy_lbl;
640          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
641        ];
642        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
643        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
644        adds_graph [
645          rtl_st_clear_carry dummy_lbl
646        ];
647        translate_op Addc destrs destrs tmp_destrs
648      ]
649    ]
650  in
651    translates @ tmp_destrs2'.
652
653axiom translate_mul:
654  ∀destrs: list register.
655  ∀srcrs1: list register.
656  ∀srcrs2: list register.
657  ∀start_lbl: label.
658  ∀dest_lbl: label.
659  ∀def: rtl_internal_function.
660    rtl_internal_function.
661
662(*
663definition translate_mul ≝
664  λdestrs: list register.
665  λsrcrs1: list register.
666  λsrcrs2: list register.
667  λstart_lbl: label.
668  λdest_lbl: label.
669  λdef: rtl_internal_function.
670  let 〈def, dummy〉 ≝ fresh_reg def in
671  let 〈def, tmpr〉 ≝ fresh_reg def in
672  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
673  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
674  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
675  let insts_init ≝ [
676    translate_move fresh_srcrs1 srcrs1;
677    translate_move fresh_srcrs2 srcrs2;
678    translate_cst (Ointconst I8 (zero ?)) destrs
679  ]
680  in
681  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
682  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
683    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
684*)
685
686definition translate_divumodu8 ≝
687  λorder: bool.
688  λdestrs: list register.
689  λsrcr1: register.
690  λsrcr2: register.
691  λstart_lbl: label.
692  λdest_lbl: label.
693  λdef: rtl_internal_function.
694  match destrs with
695  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
696  | cons destr destrs ⇒
697    let 〈def, dummy〉 ≝ fresh_reg def in
698    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
699    let inst_div ≝ adds_graph [
700      rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
701    ]
702    in
703    let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
704      add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
705  ].
706
707definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
708  λdestrs: list register.
709  λsrcrs1: list register.
710  λsrcrs2: list register.
711  λstart_lbl: label.
712  λdest_lbl: label.
713  λdef: rtl_internal_function.
714  match destrs with
715  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
716  | cons destr destrs ⇒
717    let 〈def, tmpr〉 ≝ fresh_reg def in
718    let 〈def, tmp_zero〉 ≝ fresh_reg def in
719    let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
720    let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
721    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
722    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
723    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
724    [ dp crl their_proof ⇒
725      let commonl ≝ \fst (\fst crl) in
726      let commonr ≝ \fst (\snd crl) in
727      let restl ≝ \snd (\snd crl) in
728      let restr ≝ \snd (\snd crl) in
729      let rest ≝ choose_rest ? restl restr ? ? in
730      let inits ≝ [
731        rtl_st_int destr (zero ?) start_lbl;
732        rtl_st_int tmp_zero (zero ?) start_lbl
733      ]
734      in
735      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
736        rtl_st_clear_carry start_lbl;
737        rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
738        rtl_st_op2 Or destr destr tmpr start_lbl
739      ]
740      in
741      let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
742      let f_rest ≝ λtmp_srcr. [
743        rtl_st_clear_carry start_lbl;
744        rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
745        rtl_st_op2 Or destr destr tmpr start_lbl
746      ]
747      in
748      let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
749      let insts ≝ inits @ insts_common @ insts_rest in
750      let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
751        add_translates [
752          save_srcrs1; save_srcrs2; adds_graph insts; epilogue
753        ] start_lbl dest_lbl def
754    ]
755  ].
756  [1: @their_proof
757  |*: cases not_implemented (* choose rest requires non-emptiness proofs but
758                               these appear impossible to obtain, similar proof
759                               to above *)
760  ]
761qed.
762
763definition translate_eq_reg ≝
764  λtmp_zero: register.
765  λtmp_one: register.
766  λtmpr1: register.
767  λtmpr2: register.
768  λdestr: register.
769  λdummy_lbl: label.
770  λsrcr12: register × register.
771  let 〈srcr1, srcr2〉 ≝ srcr12 in
772  [ rtl_st_clear_carry dummy_lbl;
773    rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
774    rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
775    rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
776    rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
777    rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
778    rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
779    rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
780
781definition translate_eq_list ≝
782  λtmp_zero: register.
783  λtmp_one: register.
784  λtmpr1: register.
785  λtmpr2: register.
786  λdestr: register.
787  λleq: list (register × register).
788  λdummy_lbl: label.
789  let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
790    (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
791      flatten ? (map ? ? f leq).
792
793definition translate_atom ≝
794  λtmp_zero: register.
795  λtmp_one: register.
796  λtmpr1: register.
797  λtmpr2: register.
798  λtmpr3: register.
799  λdestr: register.
800  λdummy_lbl: label.
801  λleq: list (register × register).
802  λsrcr1: register.
803  λsrcr2: register.
804    translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
805    [ rtl_st_clear_carry dummy_lbl;
806      rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
807      rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
808      rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
809      rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
810
811definition translate_lt_main ≝
812  λtmp_zero: register.
813  λtmp_one: register.
814  λtmpr1: register.
815  λtmpr2: register.
816  λtmpr3: register.
817  λdestr: register.
818  λdummy_lbl: label.
819  λsrcrs1: list register.
820  λsrcrs2: list register.
821  λproof: |srcrs1| = |srcrs2|.
822  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
823    let 〈insts, leq〉 ≝ insts_leq in
824    let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
825      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
826  in
827    \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
828
829definition fresh_regs_strong:
830  rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
831  λdef.
832  λn.
833    fresh_regs def n.
834  @fresh_regs_length
835qed.
836
837definition complete_regs_strong:
838  rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
839  λdef.
840  λleft.
841  λright.
842    complete_regs def left right.
843  @complete_regs_length
844qed.
845
846definition translate_lt ≝
847  λdestrs: list register.
848  λprf_destrs: lt 0 (|destrs|).
849  λsrcrs1: list register.
850  λsrcrs2: list register.
851  λstart_lbl: label.
852  λdest_lbl: label.
853  λdef: rtl_internal_function.
854  match destrs with
855  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
856  | _ ⇒
857    match fresh_regs_strong def (|destrs|) with
858    [ dp def_tmp_destrs tmp_destrs_proof ⇒
859      let def ≝ \fst def_tmp_destrs in
860      let tmp_destrs ≝ \snd def_tmp_destrs in
861      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
862      let 〈def, tmp_zero〉 ≝ fresh_reg def in
863      let 〈def, tmp_one〉 ≝ fresh_reg def in
864      let 〈def, tmpr1〉 ≝ fresh_reg def in
865      let 〈def, tmpr2〉 ≝ fresh_reg def in
866      let 〈def, tmpr3〉 ≝ fresh_reg def in
867      match complete_regs_strong def srcrs1 srcrs2 with
868      [ dp srcrs12_added srcrs12_proof ⇒
869        let srcrs1 ≝ \fst (\fst srcrs12_added) in
870        let srcrs2 ≝ \snd (\fst srcrs12_added) in
871        let added ≝ \snd srcrs12_added in
872        let srcrs1' ≝ rev ? srcrs1 in
873        let srcrs2' ≝ rev ? srcrs2 in
874        let insts_init ≝ [
875          translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
876          translate_cst (Ointconst I8 (zero ?)) added;
877          adds_graph [
878            rtl_st_int tmp_zero (zero ?) start_lbl;
879            rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
880          ]
881        ]
882        in
883        let insts_main ≝
884          translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
885          let insts_main ≝ [ adds_graph insts_main ] in
886          let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
887            add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
888      ]
889    ]
890  ].
891  [2: >tmp_destrs_proof @prf_destrs
892  |1: normalize nodelta
893      generalize in match srcrs12_proof
894      #HYP >rev_length >rev_length @HYP
895  ]
896qed.
897
898definition add_128_to_last ≝
899  λtmp_128: register.
900  λrs.
901  λprf: 0 < |rs|.
902  λstart_lbl: label.
903  match rs with
904  [ nil ⇒ adds_graph [ ] start_lbl
905  | _ ⇒
906    let r ≝ last_safe ? rs prf in
907      adds_graph [
908        rtl_st_op2 Add r r tmp_128 start_lbl
909      ] start_lbl
910  ].
911
912definition translate_lts ≝
913  λdestrs: list register.
914  λdestrs_prf: lt 0 (|destrs|).
915  λsrcrs1: list register.
916  λsrcrs2: list register.
917  λsrcrs1_lt_prf: 0 < |srcrs1|.
918  λsrcrs2_lt_prf: 0 < |srcrs2|.
919  λstart_lbl: label.
920  λdest_lbl: label.
921  λdef: rtl_internal_function.
922  match fresh_regs_strong def (|srcrs1|) with
923  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
924    let def ≝ \fst def_tmp_srcrs1 in
925    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
926    match fresh_regs_strong def (|srcrs2|) with
927    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
928      let def ≝ \fst def_tmp_srcrs2 in
929      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
930      let 〈def, tmp_128〉 ≝ fresh_reg def in
931        add_translates [
932          translate_move tmp_srcrs1 srcrs1;
933          translate_move tmp_srcrs2 srcrs2;
934          adds_graph [
935            rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
936          ];
937          add_128_to_last tmp_128 tmp_srcrs1 ?;
938          add_128_to_last tmp_128 tmp_srcrs2 ?;
939          translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2
940        ] start_lbl dest_lbl def
941    ]
942  ].
943  [1: >srcrs1_prf @srcrs1_lt_prf
944  |2: >srcrs2_prf @srcrs2_lt_prf
945  ]
946qed.
947
948definition translate_op2 ≝
949  λop2.
950  λdestrs: list register.
951  λdestrs_prf: lt 0 (|destrs|).
952  λsrcrs1: list register.
953  λsrcrs2: list register.
954  λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can
955                                   but we need more dep. typ. in modu/divu
956                                   cases *)
957  λsrcrs2_prf: lt 0 (|srcrs2|).
958  λstart_lbl: label.
959  λdest_lbl: label.
960  λdef: rtl_internal_function.
961  match op2 with
962  [ Oadd ⇒
963    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
964  | Oaddp ⇒
965    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
966  | Osub ⇒
967    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
968  | Osubpi ⇒
969    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
970  | Osubpp sz ⇒
971    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
972  | Omul ⇒
973    translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
974  | Odivu ⇒
975    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
976    [ cons hd tl ⇒ λcons_prf.
977      match tl with
978      [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
979      | _ ⇒ ? (* not implemented *)
980      ]
981    | nil ⇒ λnil_absrd. ?
982    ] srcrs1_prf
983  | Omodu ⇒
984    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
985    [ cons hd tl ⇒ λcons_prf.
986      match tl with
987      [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
988      | _ ⇒ ? (* not implemented *)
989      ]
990    | nil ⇒ λnil_absrd. ?
991    ] srcrs1_prf
992  | Oand ⇒
993    translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def
994  | Oor ⇒
995    translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
996  | Oxor ⇒
997    translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
998  | Ocmp c ⇒
999    match c with
1000    [ Ceq ⇒
1001      add_translates [
1002        translate_ne destrs srcrs1 srcrs2;
1003        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1004      ] start_lbl dest_lbl def
1005    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
1006    | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
1007    | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
1008    | Cle ⇒
1009      add_translates [
1010        translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;
1011        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1012      ] start_lbl dest_lbl def
1013    | Cge ⇒
1014      add_translates [
1015        translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;
1016        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1017      ] start_lbl dest_lbl def
1018    ]
1019  | Ocmpu c ⇒
1020    match c with
1021    [ Ceq ⇒
1022      add_translates [
1023        translate_ne destrs srcrs1 srcrs2;
1024        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1025      ] start_lbl dest_lbl def
1026    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
1027    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
1028    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
1029    | Cle ⇒
1030      add_translates [
1031        translate_lt destrs destrs_prf srcrs2 srcrs1;
1032        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1033      ] start_lbl dest_lbl def
1034    | Cge ⇒
1035      add_translates [
1036        translate_lt destrs destrs_prf srcrs1 srcrs2;
1037        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1038      ] start_lbl dest_lbl def
1039    ]
1040  | Ocmpp c ⇒
1041    match c with
1042    [ Ceq ⇒
1043      add_translates [
1044        translate_ne destrs srcrs1 srcrs2;
1045        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1046      ] start_lbl dest_lbl def
1047    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
1048    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
1049    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
1050    | Cle ⇒
1051      add_translates [
1052        translate_lt destrs destrs_prf srcrs2 srcrs1;
1053        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1054      ] start_lbl dest_lbl def
1055    | Cge ⇒
1056      add_translates [
1057        translate_lt destrs destrs_prf srcrs1 srcrs2;
1058        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
1059      ] start_lbl dest_lbl def
1060    ]
1061  | _ ⇒ ? (* assert false, implemented in run time or float op *)
1062  ].
1063  [ 2,6: normalize in nil_absrd;
1064         cases(not_le_Sn_O 0)
1065         #HYP cases(HYP nil_absrd)
1066  | 3,7,12,17,13,15,18,19,20,21,14,16:
1067         assumption
1068  | *:   cases not_implemented (* yes, really *)
1069  ]
1070qed.
1071
1072definition translate_cond ≝
1073  λsrcrs: list register.
1074  λstart_lbl: label.
1075  λlbl_true: label.
1076  λlbl_false: label.
1077  λdef: rtl_internal_function.
1078  let 〈def, tmpr〉 ≝ fresh_reg def in
1079  let 〈def, tmp_lbl〉 ≝ fresh_label def in
1080  let init ≝ rtl_st_int tmpr (zero ?) start_lbl in
1081  let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in
1082  let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in
1083    add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 
1084
1085definition translate_load ≝
1086  λaddr.
1087  λaddr_prf: 2 ≤ |addr|.
1088  λdestrs: list register.
1089  λstart_lbl: label.
1090  λdest_lbl: label.
1091  λdef: rtl_internal_function.
1092  match fresh_regs_strong def (|addr|) with
1093  [ dp def_save_addr save_addr_prf ⇒
1094    let def ≝ \fst def_save_addr in
1095    let save_addr ≝ \snd def_save_addr in
1096    match fresh_regs_strong def (|addr|) with
1097    [ dp def_tmp_addr tmp_addr_prf ⇒
1098      let def ≝ \fst def_tmp_addr in
1099      let tmp_addr ≝ \snd def_tmp_addr in
1100      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
1101      let 〈def, tmpr〉 ≝ fresh_reg def in
1102      let insts_save_addr ≝ translate_move save_addr addr in
1103      let f ≝ λtranslates_off. λr.
1104        let 〈translates, off〉 ≝ translates_off in
1105        let translates ≝ translates @ [
1106          adds_graph [
1107            rtl_st_int tmpr off start_lbl
1108          ];
1109          translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
1110          adds_graph [
1111            rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
1112          ]
1113        ]
1114        in
1115        let 〈carry, result〉 ≝ half_add ? off int_size in
1116          〈translates, result〉
1117      in
1118      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
1119        add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
1120    ]
1121  ].
1122  [1: normalize //
1123  |2: >save_addr_prf normalize
1124      @(transitive_le 1 2 (|addr|)) //
1125  |3: >tmp_addr_prf normalize
1126      @(transitive_le 1 2 (|addr|)) //
1127  |*: >tmp_addr_prf assumption
1128  ]
1129qed.
1130
1131definition translate_store ≝
1132  λaddr.
1133  λaddr_prf: 2 ≤ |addr|.
1134  λsrcrs: list register.
1135  λstart_lbl: label.
1136  λdest_lbl: label.
1137  λdef: rtl_internal_function.
1138  match fresh_regs_strong def (|addr|) with
1139  [ dp def_tmp_addr tmp_addr_prf ⇒
1140    let def ≝ \fst def_tmp_addr in
1141    let tmp_addr ≝ \snd def_tmp_addr in
1142    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
1143    let 〈def, tmpr〉 ≝ fresh_reg def in
1144    let f ≝ λtranslate_off. λsrcr.
1145      let 〈translates, off〉 ≝ translate_off in
1146      let translates ≝ translates @ [
1147        adds_graph [
1148          rtl_st_int tmpr off start_lbl
1149        ];
1150        translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
1151        adds_graph [
1152          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
1153        ]
1154      ]
1155      in
1156        let 〈carry, result〉 ≝ half_add ? off int_size in
1157          〈translates, result〉
1158    in
1159    let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
1160      add_translates translates start_lbl dest_lbl def
1161  ].
1162  [1: normalize //
1163  |2: >tmp_addr_prf normalize
1164      @(transitive_le 1 2 (|addr|)) //
1165  |3: >tmp_addr_prf normalize
1166      @(transitive_le 1 2 (|addr|)) //
1167  |*: >tmp_addr_prf assumption
1168  ]
1169qed.
1170
1171definition translate_stmt ≝
1172  λlenv.
1173  λlbl: label.
1174  λstmt.
1175  λdef: rtl_internal_function.
1176  match stmt with
1177  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
1178  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
1179  | St_const destr cst lbl' ⇒
1180    translate_cst cst (find_local_env destr lenv) lbl lbl' def
1181  | St_op1 op1 destr srcr lbl' ⇒
1182    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
1183  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
1184    translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
1185  | St_load ignore addr destr lbl' ⇒
1186    translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
1187  | St_store ignore addr srcr lbl' ⇒
1188    translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
1189  | St_call_id f args retr lbl' ⇒
1190    match retr with
1191    [ Some retr ⇒
1192      add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1193    | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
1194    ]
1195  | St_call_ptr f args retr lbl' ⇒
1196    match retr with
1197    [ None ⇒
1198      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1199        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
1200    | Some retr ⇒
1201      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1202        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
1203    ]
1204  | St_tailcall_id f args ⇒
1205    add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
1206  | St_tailcall_ptr f args ⇒
1207    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
1208      add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
1209  | St_cond r lbl_true lbl_false ⇒
1210    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
1211  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
1212  | St_return ⇒ add_graph lbl rtl_st_return def
1213  ].
1214  [10: cases not_implemented (* jtable case *)
1215  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
1216  ]
1217qed.
1218
1219(* XXX: we use a "hack" here to circumvent the proof obligations required to
1220   create res, an empty internal_function record.  we insert into our graph
1221   the start and end nodes to ensure that they are in, and place dummy
1222   skip instructions at these nodes. *)
1223definition translate_internal ≝
1224  λdef.
1225  let runiverse ≝ f_reggen def in
1226  let lenv ≝ initialize_local_env runiverse
1227    (f_params def @ f_locals def) (f_result def) in
1228  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
1229  let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
1230  let result ≝
1231    match (f_result def) with
1232    [ None ⇒ [ ]
1233    | Some r_typ ⇒
1234      let 〈r, typ〉 ≝ r_typ in
1235        find_local_env r lenv
1236    ]
1237  in
1238  let luniverse' ≝ f_labgen def in
1239  let runiverse' ≝ runiverse in
1240  let result' ≝ result in
1241  let params' ≝ params in
1242  let locals' ≝ locals in
1243  let stack_size' ≝ f_stacksize def in
1244  let entry' ≝ f_entry def in
1245  let exit' ≝ f_exit def in
1246  let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in
1247  let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in
1248  let res ≝
1249    mk_rtl_internal_function luniverse' runiverse' result' params'
1250                         locals' stack_size' graph' ? ? in
1251    foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
1252  [1: %
1253      [1: @entry'
1254      |2: normalize nodelta;
1255          @graph_add_lookup
1256          @graph_add
1257      ]
1258  |2: %
1259      [1: @exit'
1260      |2: normalize nodelta;
1261          @graph_add
1262      ]
1263  ]
1264qed.
1265
1266(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1267  because of CompCert heritage *)
1268definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
1269 λp. transform_program … p (transf_fundef … translate_internal).
Note: See TracBrowser for help on using the repository browser.