source: src/RTLabs/RTLabsToRTL_paolo.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 33.3 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL_paolo.ma".
3include "common/AssocList.ma".
4include "common/FrontEndOps.ma".
5include "common/Graphs.ma".
6include "joint/TranslateUtils_paolo.ma".
7include "utilities/lists.ma".
8include alias "ASM/BitVector.ma".
9include alias "arithmetics/nat.ma".
10
11definition size_of_sig_type ≝
12  λsig.
13  match sig with
14  [ ASTint isize sign ⇒
15    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
16      isize' ÷ (nat_of_bitvector ? int_size)
17  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
18  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
19  ].
20  cases not_implemented;
21qed.
22
23inductive register_type: Type[0] ≝
24  | register_int: register → register_type
25  | register_ptr: register → register → register_type.
26
27definition local_env ≝ identifier_map RegisterTag (list register).
28
29definition mem_local_env : register → local_env → bool ≝
30  λr,e. member … e r.
31
32definition add_local_env : register → list register → local_env → local_env ≝
33  λr,v,e. add … e r v.
34
35definition find_local_env : register → local_env → list register ≝
36  λr: register.λenv. lookup_def … env r [].
37
38definition find_local_env_arg ≝
39  λr,lenv. map … Reg (find_local_env r lenv).
40
41let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
42  match n with
43  [ O ⇒ 〈[],runiverse〉
44  | S n' ⇒
45     let 〈r,runiverse〉 ≝ fresh … runiverse in
46     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
47      〈r::res,runiverse〉 ].
48
49definition initialize_local_env_internal ≝
50  λlenv_runiverse.
51  λr_sig.
52  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
53  let 〈r, sig〉 ≝ r_sig in
54  let size ≝ size_of_sig_type sig in
55  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
56    〈add_local_env r rs lenv,runiverse〉.
57
58definition initialize_local_env ≝
59  λruniverse.
60  λregisters.
61  λresult.
62  let registers ≝
63    match result with
64    [ None ⇒ registers
65    | Some rt ⇒ rt :: registers
66    ]
67  in
68    foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.
69
70definition map_list_local_env_internal ≝
71  λlenv,res,r. res @ (find_local_env r lenv).
72   
73definition map_list_local_env ≝
74  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
75
76definition make_addr ≝
77  λA.
78  λlst: list A.
79  λprf: 2 = length A lst.
80  match lst return λx. 2 = |x| → A × A with
81  [ nil ⇒ λlst_nil_prf. ?
82  | cons hd tl ⇒ λprf.
83    match tl return λx. 1 = |x| → A × A with
84    [ nil ⇒ λtl_nil_prf. ?
85    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
86    ] ?
87  ] prf.
88  [1: normalize in lst_nil_prf;
89      destruct(lst_nil_prf)
90  |2: normalize in prf;
91      @injective_S
92      assumption
93  |3: normalize in tl_nil_prf;
94      destruct(tl_nil_prf)
95  ]
96qed.
97
98definition find_and_addr ≝
99  λr,lenv. make_addr ? (find_local_env r lenv).
100
101definition rtl_args ≝
102  λregs_list,lenv. flatten … (map … (λr.find_local_env_arg r lenv) regs_list).
103
104definition split_into_bytes:
105  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝
106λsize.
107 match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with
108  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
109[ %[@[int]] //
110| %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) normalize //
111| %[@(let 〈h1,l〉 ≝ split ? 8 … int in
112      let 〈h2,l〉 ≝ split ? 8 … l in
113      let 〈h3,l〉 ≝ split ? 8 … l in
114       [l;h3;h2;h1])]
115  cases (split ????) #h1 #l normalize
116  cases (split ????) #h2 #l normalize
117  cases (split ????) // ]
118qed.
119
120
121lemma eqb_implies_eq:
122  ∀m, n: nat.
123    eqb m n = true → m = n.
124    #m#n@eqb_elim // #_ #F destruct(F) qed.
125   
126definition translate_op:
127  ∀globals. Op2 →
128  ∀dests : list register.
129  ∀srcrs1 : list rtl_argument.
130  ∀srcrs2 : list rtl_argument.
131  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
132  list (rtl_instruction globals)
133   ≝
134  λglobals: list ident.
135  λop.
136  λdestrs.
137  λsrcrs1.
138  λsrcrs2.
139  λprf1,prf2.
140  let f_add ≝ λop,destr,srcr1,srcr2.
141    OP2 rtl_params globals op destr srcr1 srcr2 in
142  let res : list (rtl_instruction globals) ≝
143    map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
144  (* first, clear carry if op relies on it *)
145  match op with
146  [ Addc ⇒ [clear_carry ?]
147  | Sub ⇒ [clear_carry ?]
148  | _ ⇒ [ ]
149  ] @
150  match op with
151  (* if adding, we use a first Add op, that clear the carry, and then Addc's *)
152  [ Add ⇒
153    match destrs return λx.|destrs| = |x| → list (rtl_instruction globals) with
154    [ nil ⇒ λeq_destrs.[ ]
155    | cons destr destrs' ⇒ λeq_destrs.
156      match srcrs1 return λy.|srcrs1| = |y| → list (rtl_instruction globals) with
157      [ nil ⇒ λeq_srcrs1.⊥
158      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
159        match srcrs2 return λz.|srcrs2| = |z| → list (rtl_instruction globals) with
160        [ nil ⇒ λeq_srcrs2.⊥
161        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
162          f_add Add destr srcr1 srcr2 ::
163          map3 ???? (f_add Addc) destrs' srcrs1' srcrs2' ??
164        ] (refl …)
165      ] (refl …)
166    ] (refl …)
167  | _ ⇒ res
168  ].
169  [5,6: assumption
170  |1: >prf1 in eq_destrs; >eq_srcrs1 normalize //
171  |2: >prf2 in eq_srcrs1; >eq_srcrs2 normalize //
172  |3: >prf2 in eq_srcrs1; >eq_srcrs2 normalize #H destruct(H)
173  |4: >prf1 in eq_destrs; >eq_srcrs1 normalize #H destruct(H)
174qed.
175
176let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.|l| = size ≝
177match size with
178[ O ⇒ [ ]
179| S size' ⇒
180  match nat_to_args size' (k ÷ 8) with
181  [ mk_Sig res prf ⇒
182    imm_nat k :: res
183  ]
184]. normalize // qed.
185
186definition size_of_cst ≝ λcst.match cst with
187  [ Ointconst size _ ⇒ size_intsize size
188  | Ofloatconst float ⇒ ? (* not implemented *)
189  | _ ⇒ 2
190  ].
191  cases not_implemented qed.
192
193definition cst_well_defd : list ident → constant → Prop ≝ λglobals,cst.
194  match cst with
195  [ Oaddrsymbol id offset ⇒ member id (eq_identifier ?) globals
196  | _ ⇒ True
197  ].
198
199definition translate_cst :
200  ∀globals: list ident.
201  ∀cst_sig: Σcst : constant.cst_well_defd globals cst.
202  ∀destrs: list register.
203  |destrs| = size_of_cst cst_sig → list (rtl_instruction globals)
204 ≝
205  λglobals,cst_sig,destrs,prf.
206  match cst_sig return λy.cst_sig = y → list (rtl_instruction globals) with
207  [ mk_Sig cst cst_good ⇒ λeqcst_sig.
208    match cst return λx.cst = x → list (rtl_instruction globals)
209    with
210    [ Ointconst size const ⇒ λeqcst.
211      match split_into_bytes size const with
212      [ mk_Sig bytes bytes_length_proof ⇒
213        map2 … (reg_from_byte globals)  destrs bytes ?
214      ]
215    | Ofloatconst float ⇒ λ_.⊥
216    | Oaddrsymbol id offset ⇒ λeqcst.
217      let 〈r1, r2〉 ≝ make_addr … destrs ? in
218      [ADDRESS rtl_params globals id ? r1 r2]
219    | Oaddrstack offset ⇒ λeqcst.
220      let 〈r1, r2〉 ≝ make_addr … destrs ? in
221      [extension rtl_params globals (rtl_st_ext_stack_address r1 r2)]
222    ] (refl …)
223  ] (refl …).
224  [2: cases not_implemented
225  |3: >eqcst in cst_good; //]
226  >eqcst_sig in prf;
227  >eqcst whd in ⊢ (???% → ?); #prf
228  [1: >bytes_length_proof
229      >prf //]
230  //
231  qed.
232
233 
234definition translate_move :
235  ∀globals.
236  ∀destrs: list register.
237  ∀srcrs: list rtl_argument.
238  |destrs| = |srcrs| → list (rtl_instruction globals) ≝
239  λglobals,destrs,srcrs,length_eq.
240  map2 … (λdst,src.MOVE rtl_params … (REG dst src)) destrs srcrs length_eq.
241
242let rec make
243  (A: Type[0]) (elt: A) (n: nat) on n ≝
244  match n with
245  [ O ⇒ [ ]
246  | S n' ⇒ elt :: make A elt n'
247  ].
248 
249lemma make_length:
250  ∀A: Type[0].
251  ∀elt: A.
252  ∀n: nat.
253    n = length ? (make A elt n).
254  #A #ELT #N
255  elim N
256  [ normalize %
257  | #N #IH
258    normalize <IH %
259  ]
260qed.
261
262definition sign_mask : ∀globals.register → register → list (rtl_instruction globals) ≝
263    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
264       byte in destr if srcr is: neg   |  pos
265       destr ← srcr | 127       11...1 | 01...1
266       destr ← destr <rot< 1    1...11 | 1...10
267       destr ← INC destr        0....0 | 1....1
268       destr ← CPL destr        1....1 | 0....0
269     *)
270  λglobals,destr,srcr.
271  [OP2 … Or destr (Reg srcr) (imm_nat 127) ;
272   OP1 … Rl destr destr ;
273   OP1 … Inc destr destr ;
274   OP1 … Cmpl destr destr ].
275   
276definition translate_cast_signed :
277  ∀globals : list ident.
278  list register → register → bind_list register unit (rtl_instruction globals) ≝
279  λglobals,destrs,srcr.
280  ν tmp in
281  (sign_mask ? tmp srcr @
282  translate_move ? destrs (make ? (Reg tmp) (|destrs|)) (make_length …)).
283 
284definition translate_cast_unsigned :
285  ∀globals : list ident.
286  list register → list (rtl_instruction globals) ≝
287  λglobals,destrs.
288  match nat_to_args (|destrs|) 0 with
289  [ mk_Sig res prf ⇒ translate_move ? destrs res ?].
290  // qed.
291
292theorem length_map : ∀A,B.∀f:A→B.∀l : list A.|map … f l| = |l|.
293#A#B#f #l elim l normalize // qed.
294
295(* using size of lists as size of ints *)
296definition translate_cast :
297  ∀globals: list ident.
298  signedness → list register → list register →
299    bind_list register unit (rtl_instruction globals) ≝
300  λglobals,src_sign,destrs,srcrs.
301  match srcrs
302  return λy. y = srcrs → bind_list register unit (rtl_instruction globals)
303  with
304  [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *)
305  | _ ⇒ λeq_srcrs.
306    match reduce_strong ? ? destrs srcrs with
307    [ mk_Sig crl len_proof ⇒
308      (* move prefix of srcrs in destrs *)
309      translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @
310      match \snd (\snd crl) with
311      [ nil ⇒
312        match src_sign return λ_.bind_list register unit (rtl_instruction globals) with
313        [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl))
314        | Signed ⇒
315          translate_cast_signed ? (\snd (\fst crl)) (last_safe ? srcrs ?)
316        ]
317      | _ ⇒ [ ] (* nothing to do if |srcrs| > |destrs| *)
318      ]
319    ]
320  ] (refl …).
321  [ >len_proof >length_map @refl
322  | <eq_srcrs normalize //
323  ] qed.
324 
325definition translate_notint :
326  ∀globals : list ident.
327  ∀destrs : list register.
328  ∀srcrs_arg : list register.
329  |destrs| = |srcrs_arg| → list (rtl_instruction globals) ≝
330  λglobals, destrs, srcrs, prf.
331  map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
332
333
334definition translate_negint : ∀globals.? → ? → ? → bind_list register unit (rtl_instruction globals) ≝
335  λglobals: list ident.
336  λdestrs: list register.
337  λsrcrs: list register.
338  λprf: |destrs| = |srcrs|. (* assert in caml code *)
339  translate_notint … destrs srcrs prf @
340  match nat_to_args (|destrs|) 1 with
341  [ mk_Sig res prf' ⇒
342    translate_op ? Add destrs (map … Reg destrs) res ??
343  ].
344// qed.
345
346definition translate_notbool:
347  ∀globals : list ident.
348  list register → list register →
349    bind_list register unit (rtl_instruction globals) ≝
350  λglobals,destrs,srcrs.
351  match destrs with
352  [ nil ⇒ [ ]
353  | cons destr destrs' ⇒
354    translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *)
355    match srcrs with
356    [ nil ⇒ [reg_from_nat … destr 0]
357    | cons srcr srcrs' ⇒
358      let f : register → rtl_instruction globals ≝
359        λr. OP2 ?? Or destr (Reg destr) (Reg r) in
360      reg_from_reg … srcr destr ::
361      map … f srcrs' @
362      (* now destr is non-null iff srcrs was non-null *)
363      clear_carry … ::
364      (* many uses of 0, better not use immediates *)
365      ν tmp in
366      [reg_from_nat … tmp 0 ;
367       OP2 … Sub destr (Reg tmp) (Reg tmp) ;
368       (* now carry bit is set iff destr was non-null *)
369       OP2 … Addc destr (Reg tmp) (Reg tmp)]
370     ]
371   ].
372
373definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
374  bind_list register unit (rtl_instruction globals) ≝
375  λglobals.
376  λty, ty'.
377  λop1: unary_operation ty ty'.
378  λdestrs: list register.
379  λsrcrs: list register.
380  λprf1: |destrs| = size_of_sig_type ty'.
381  λprf2: |srcrs| = size_of_sig_type ty.
382  match op1
383  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
384    bind_list register unit (rtl_instruction globals) with
385  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
386    translate_cast globals src_sign destrs srcrs
387  | Onegint sz sg ⇒ λeq1,eq2.
388    translate_negint globals destrs srcrs ?
389  | Onotbool _ _ _ _ ⇒ λeq1,eq2.
390    translate_notbool globals destrs srcrs
391  | Onotint sz sg ⇒ λeq1,eq2.
392    translate_notint globals destrs srcrs ?
393  | Optrofint sz sg r ⇒ λeq1,eq2.
394    translate_cast globals Unsigned destrs srcrs
395  | Ointofptr sz sg r ⇒ λeq1,eq2.
396    translate_cast globals Unsigned destrs srcrs
397  | Oid t ⇒ λeq1,eq2.
398      translate_move globals destrs (map … Reg srcrs) ?
399  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
400  ] (refl …) (refl …).
401  [3,4,5,6,7,8,9:  cases not_implemented
402  |*: destruct >prf1 >prf2 //
403  ]
404qed.
405
406let rec range_strong_internal (start : ℕ) (count : ℕ)
407  (* Paolo: no notation to avoid ambiguity *)
408  on count : list (Σn : ℕ.lt n (plus start count)) ≝
409match count return λx.count = x → list (Σn : ℕ. n < start + count)
410  with
411[ O ⇒ λ_.[ ]
412| S count' ⇒ λEQ.
413  let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝
414    λsig.match sig with [mk_Sig n prf ⇒ n] in
415  start :: map … f (range_strong_internal (S start) count')
416] (refl …).
417destruct(EQ) // qed.
418
419definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
420  λend.range_strong_internal 0 end.
421
422definition translate_mul_i :
423  ∀globals.
424  register → register →
425  (* size of destination and sources *)
426  ∀n : ℕ.
427  (* the temporary destination, with a dummy register at the end *)
428  ∀tmp_destrs_dummy : list register.
429  ∀srcrs1,srcrs2 : list rtl_argument.
430  |tmp_destrs_dummy| = S n →
431  n = |srcrs1| →
432  |srcrs1| = |srcrs2| →
433  (* the position of the least significant byte of the result we compute at
434     this stage (goes from 0 to n in the main function) *)
435  ∀k : ℕ.
436  lt k n →
437  (* the position of the byte in the first source we will use in this stage.
438     the position in the other source will be k - i *)
439  (Σi.i<S k) →
440  (* the accumulator *)
441  list (rtl_instruction globals) →
442    list (rtl_instruction globals) ≝
443  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
444    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
445  (* the following will expand to
446     a, b ← srcrs1[i] * srcrs2[k-i]
447     tmp_destrs_dummy[k]   ← tmp_destrs_dummy[k] + a
448     tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C
449     tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C
450     ...
451     tmp_destrs_dummy[n]   ← tmp_destrs_dummy[n] + 0 + C
452     ( all calculations on tmp_destrs_dummy[n] will be eliminated with
453     liveness analysis) *)
454  match i_sig with
455    [ mk_Sig i i_prf ⇒
456      (* we pad the result of a byte multiplication with zeros in order
457         for the bit to be carried. Redundant calculations will be eliminated
458         by constant propagation. *)
459      let args : list rtl_argument ≝
460        [Reg a;Reg b] @ make ? (Imm (zero …)) (n - 1 - k) in
461      let tmp_destrs_view : list register ≝
462        ltl ? tmp_destrs_dummy k in
463      OPACCS rtl_params globals Mul a b
464        (nth_safe ? i srcrs1 ?)
465        (nth_safe ? (k - i) srcrs2 ?) ::
466      translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @
467      acc
468    ].
469[ @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
470  whd >(plus_n_O (S k)) @le_plus // ]
471| <srcrs1_prf
472  @(transitive_le … i_prf k_prf)
473| >length_map //
474| >length_map
475  >length_ltl
476  >tmp_destrs_dummy_prf >length_append
477  <make_length
478  normalize in ⊢ (???(?%?));
479  >plus_minus_commutative
480    [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption]
481  cut (S n = 2 + (n - 1))
482    [2: #EQ >EQ //]
483  >plus_minus_commutative
484    [2: @(transitive_le … k_prf) //]
485  @sym_eq
486  @plus_to_minus
487  <plus_n_Sm
488  //
489] qed.
490
491definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
492λglobals : list ident.
493λdestrs : list register.
494λsrcrs1 : list rtl_argument.
495λsrcrs2 : list rtl_argument.
496λsrcrs1_prf : |destrs| = |srcrs1|.
497λsrcrs2_prf : |srcrs1| = |srcrs2|.
498(* needed fresh registers *)
499νa in
500νb in
501(* temporary registers for the result are created, so to avoid overwriting
502   sources *)
503ννtmp_destrs: |destrs| with tmp_destrs_prf in
504νdummy in
505(* the step calculating all products with least significant byte going in the
506   k-th position of the result *)
507let translate_mul_k : (Σk.k<|destrs|) → list (rtl_instruction globals) →
508  list (rtl_instruction globals) ≝
509  λk_sig,acc.match k_sig with
510  [ mk_Sig k k_prf ⇒
511    foldr … (translate_mul_i ? a b (|destrs|)
512      (tmp_destrs @ [dummy]) srcrs1 srcrs2
513      ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k))
514  ] in
515(* initializing tmp_destrs to zero
516   dummy is intentionally uninitialized *)
517translate_cast_unsigned … tmp_destrs @
518(* the main body, roughly:
519   for k in 0 ... n-1 do
520     for i in 0 ... k do
521       translate_mul_i … k … i *)
522foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
523(* epilogue: saving the result *)
524translate_move … destrs (map … Reg tmp_destrs) ?.
525[ >length_map >tmp_destrs_prf //
526| >length_append <plus_n_Sm <plus_n_O //
527]
528qed.
529
530definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
531    bind_list register unit (rtl_instruction globals) ≝
532  λglobals: list ident.
533  λdiv_not_mod: bool.
534  λdestrs: list register.
535  λsrcrs1: list rtl_argument.
536  λsrcrs2: list rtl_argument.
537  λsrcrs1_prf : |destrs| = |srcrs1|.
538  λsrcrs2_prf : |srcrs1| = |srcrs2|.
539  let return_type ≝ bind_list register unit (rtl_instruction globals) in
540  match destrs return λx.x = destrs → return_type with
541  [ nil ⇒ λ_.[ ]
542  | cons destr destrs' ⇒ λeq_destrs.
543    match destrs' with
544    [ nil ⇒
545      match srcrs1 return λx.x = srcrs1 → return_type  with
546      [ nil ⇒ λeq_srcrs1.⊥
547      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
548        match srcrs2 return λx.x = srcrs2 → return_type  with
549        [ nil ⇒ λeq_srcrs2.⊥
550        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
551          νdummy in
552          let 〈destr1, destr2〉 ≝
553            if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
554          [OPACCS rtl_params globals DivuModu destr1 destr2 srcr1 srcr2]
555        ] (refl …)
556      ] (refl …)
557    | _ ⇒ ? (* not implemented *)
558    ]
559  ] (refl …).
560[3: elim not_implemented]
561destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed.
562
563let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
564  (prf : |l1| = |l2|) on l1 : C ≝
565  match l1 return λx.x = l1 → C with 
566  [ nil ⇒ λ_.init
567  | cons a l1' ⇒ λeq_l1.
568    match l2 return λy.y = l2 → C with
569    [ nil ⇒ λeq_l2.⊥
570    | cons b l2' ⇒ λeq_l2.
571      f a b (foldr2 A B C f init l1' l2' ?)
572    ] (refl …)
573  ] (refl …).
574[destruct normalize in prf; destruct
575|destruct normalize in prf; //
576] qed.
577
578let rec foldr3 (A : Type[0]) (B : Type[0]) (C : Type[0]) (D : Type[0])
579  (f : A→B→C→D→D) (init : D) (l1 : list A) (l2 : list B) (l3 : list C)
580  (prf1 : |l1| = |l2|) (prf2 : |l2| = |l3|) on l1 : D ≝
581  match l1 return λx.x = l1 → D with 
582  [ nil ⇒ λ_.init
583  | cons a l1' ⇒ λeq_l1.
584    match l2 return λy.y = l2 → D with
585    [ nil ⇒ λeq_l2.⊥
586    | cons b l2' ⇒ λeq_l2.
587      match l3 return λz.z = l3 → D with
588      [ nil ⇒ λeq_l3.⊥
589      | cons c l3' ⇒ λeq_l3.
590        f a b c (foldr3 A B C D f init l1' l2' l3' ? ?)
591      ] (refl …)
592    ] (refl …)
593  ] (refl …).
594destruct normalize in prf1; normalize in prf2; destruct // qed.
595
596definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
597  λglobals: list ident.
598  λdestrs: list register.
599  λsrcrs1: list rtl_argument.
600  λsrcrs2: list rtl_argument.
601  λsrcrs1_prf : |destrs| = |srcrs1|.
602  λsrcrs2_prf : |srcrs1| = |srcrs2|.
603  let return_type ≝ bind_list register unit (rtl_instruction globals) in
604  match destrs return λx.x = destrs → return_type with
605  [ nil ⇒ λ_.[ ]
606  | cons destr destrs' ⇒ λeq_destrs.
607    match srcrs1 return λy.y = srcrs1 → return_type with
608    [ nil ⇒ λeq_srcrs1.⊥
609    | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
610      match srcrs2 return λz.z = srcrs2 → return_type with
611      [ nil ⇒ λeq_srcrs2.⊥
612      | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
613        νtmpr in
614        let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝
615          λs1,s2,acc.
616          OP2 … Xor tmpr s1 s2 ::
617          OP2 … Or destr (Reg destr) (Reg tmpr) ::
618          acc in
619        let epilogue : list (rtl_instruction globals) ≝
620          [ clear_carry … ;
621            OP2 … Sub tmpr (Imm (zero …)) (Reg destr) ;
622            (* now carry bit is 1 iff destrs != 0 *)
623            OP2 … Addc destr (Imm (zero …)) (Imm (zero …)) ] in
624         translate_cast_unsigned … destrs' @
625         OP2 rtl_params globals Xor destr srcr1 srcr2 ::
626         foldr2 ??? f epilogue srcrs1' srcrs2' ?
627       ] (refl …)
628     ] (refl …)
629   ] (refl …).
630   destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct // qed.
631
632(* if destrs is 0 or 1, it inverses it. To be used after operations that
633   ensure this. *)
634definition translate_toggle_bool : ∀globals.?→list (rtl_instruction globals) ≝
635  λglobals: list ident.
636  λdestrs: list register.
637  match destrs with
638  [ nil ⇒ [ ]
639  | cons destr _ ⇒ [OP1 rtl_params globals Cmpl destr destr]
640  ].
641 
642definition translate_lt_unsigned :
643  ∀globals.
644  ∀destrs: list register.
645  ∀srcrs1: list rtl_argument.
646  ∀srcrs2: list rtl_argument.
647  |destrs| = |srcrs1| →
648  |srcrs1| = |srcrs2| →
649  list (rtl_instruction globals) ≝
650  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
651  match destrs with
652  [ nil ⇒ [ ]
653  | cons destr destrs' ⇒
654    translate_cast_unsigned … destrs' @
655    (* I perform a subtraction, but the only interest is in the carry bit *)
656    translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @
657    [ OP2 … Addc destr (imm_nat 0) (imm_nat 0) ]
658  ].
659[ <make_length ] assumption qed.
660
661(* shifts signed integers by adding 128 to the most significant byte
662   it replaces it with a fresh register which must be provided *)
663let rec shift_signed globals
664  (tmp : register)
665  (srcrs : list rtl_argument) on srcrs :
666  (list rtl_argument) × (list (rtl_instruction globals)) ≝
667  match srcrs with
668  [ nil ⇒ 〈[ ],[ ]〉
669  | cons srcr srcrs' ⇒
670    match srcrs' with
671    [ nil ⇒ 〈[ Reg tmp ], [ OP2 … Add tmp srcr (imm_nat 128) ]〉
672    | _ ⇒
673      let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in
674      〈srcr :: new_srcrs', op〉
675    ]
676  ].
677
678lemma shift_signed_length : ∀globals,tmp,srcrs.
679  |\fst (shift_signed globals tmp srcrs)| = |srcrs|.
680#globals #tmp #srcrs elim srcrs [//]
681#srcr * [//]
682#srcr' #srcrs'' #Hi
683whd in ⊢ (??(??(???%))?);
684@pair_elim #new_srcrs' #op #EQ >EQ in Hi;
685normalize #Hi >Hi //
686qed.
687
688definition translate_lt_signed :
689  ∀globals.
690  ∀destrs: list register.
691  ∀srcrs1: list rtl_argument.
692  ∀srcrs2: list rtl_argument.
693  |destrs| = |srcrs1| →
694  |srcrs1| = |srcrs2| →
695  bind_list register unit (rtl_instruction globals) ≝
696  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
697  νtmp_last_s1 in
698  νtmp_last_s2 in
699  let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in
700  let new_srcrs1 ≝ \fst p1 in
701  let shift_srcrs1 ≝ \snd p1 in
702  let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in
703  let new_srcrs2 ≝ \fst p2 in
704  let shift_srcrs2 ≝ \snd p2 in
705  shift_srcrs1 @ shift_srcrs2 @
706  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ??.
707>shift_signed_length [2: >shift_signed_length] assumption qed.
708
709definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
710  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
711  if is_unsigned then
712    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
713  else
714    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf.
715
716definition translate_cmp ≝
717  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
718  match cmp with
719  [ Ceq ⇒
720    translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
721    translate_toggle_bool globals destrs
722  | Cne ⇒
723    translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
724  | Clt ⇒
725    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
726  | Cgt ⇒
727    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ?
728  | Cle ⇒
729    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ? @
730    translate_toggle_bool globals destrs
731  | Cge ⇒
732    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
733    translate_toggle_bool globals destrs
734  ].
735// qed.
736 
737definition translate_op2 :
738  ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
739  λglobals: list ident.
740  λop2.
741  λdestrs: list register.
742  λsrcrs1: list rtl_argument.
743  λsrcrs2: list rtl_argument.
744  λsrcrs1_prf: |destrs| = |srcrs1|.
745  λsrcrs2_prf: |srcrs1| = |srcrs2|.
746  match op2 with
747  [ Oadd ⇒
748    translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
749  | Oaddp ⇒
750    translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
751  | Osub ⇒
752    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
753  | Osubpi ⇒
754    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
755  | Osubpp _ ⇒
756    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
757  | Omul ⇒
758    translate_mul globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
759  | Odivu ⇒
760    translate_divumodu8 globals true destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
761  | Omodu ⇒
762    translate_divumodu8 globals false destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
763  | Oand ⇒
764    translate_op globals And destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
765  | Oor ⇒
766    translate_op globals Or destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
767  | Oxor ⇒
768    translate_op globals Xor destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
769  | Ocmp c ⇒
770    translate_cmp false globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
771  | Ocmpu c ⇒
772    translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
773  | Ocmpp c ⇒
774    translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
775  | _ ⇒ ? (* assert false, implemented in run time or float op *)
776  ].
777  cases not_implemented (* XXX: yes, really *) qed.
778
779definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_instruction globals) ≝
780  λglobals: list ident.
781  λsrcrs: list register.
782  λlbl_true: label.
783  match srcrs with
784  [ nil ⇒ [ ]
785  | cons srcr srcrs' ⇒
786    ν tmpr in
787    let f ≝ λr. OP2 rtl_params globals Or tmpr (Reg tmpr) (Reg r) in
788    reg_from_reg globals tmpr srcr ::
789    map … f srcrs' @
790    [ COND … tmpr lbl_true ]
791  ].
792
793(* Paolo: to be controlled (original seemed overly complex) *)
794definition translate_load ≝
795  λglobals: list ident.
796  λaddr : list rtl_argument.
797  λaddr_prf: 2 = |addr|.
798  λdestrs: list register.
799  ν tmp_addr_l in
800  ν tmp_addr_h in
801  let f ≝ λdestr : register.λacc : list (rtl_instruction globals).
802    LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
803    translate_op … Add
804      [tmp_addr_l ; tmp_addr_h]
805      [Reg tmp_addr_l ; Reg tmp_addr_h]
806      [imm_nat 0 ; Imm int_size] ? ? @ acc in
807  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
808  foldr … f [ ] destrs.
809[1: <addr_prf] // qed.
810 
811definition translate_store ≝
812  λglobals: list ident.
813  λaddr : list rtl_argument.
814  λaddr_prf: 2 = |addr|.
815  λsrcrs: list rtl_argument.
816  ν tmp_addr_l in
817  ν tmp_addr_h in
818  let f ≝ λsrcr : rtl_argument.λacc : list (rtl_instruction globals).
819    STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
820    translate_op … Add
821      [tmp_addr_l ; tmp_addr_h]
822      [Reg tmp_addr_l ; Reg tmp_addr_h]
823      [imm_nat 0 ; Imm int_size] ? ? @ acc in
824  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
825  foldr … f [ ] srcrs.
826[1: <addr_prf] // qed.
827
828(* alias for b_adds_graph *)
829definition rtl_adds_graph ≝
830  λglobals.b_adds_graph rtl_params globals register unit
831    (rtl_ertl_fresh_reg rtl_params rtl_params globals).
832
833axiom fake_label: label.
834
835definition stmt_not_return ≝ λstmt.match stmt with
836  [ St_return ⇒ False
837  | _ ⇒ True ].
838
839(* XXX: following conversation with CSC about the mix up in extension statements
840        and extension instructions in RTL, use fake_label in calls to
841        tailcall_* instructions. *)
842definition translate_inst : ∀globals.?→?→?→
843  Prod (bind_list register unit (rtl_instruction globals)) label ≝
844  λglobals: list ident.
845  λlenv: local_env.
846  λstmt.
847  λstmt_prf : stmt_not_return stmt.
848  match stmt return λx.stmt = x →
849    (bind_list register unit (rtl_instruction globals)) × label with
850  [ St_skip lbl' ⇒ λ_.
851    〈[ ], lbl'〉
852  | St_cost cost_lbl lbl' ⇒ λ_.
853    〈[COST_LABEL … cost_lbl], lbl'〉
854  | St_const destr cst lbl' ⇒ λ_.
855    〈translate_cst globals cst (find_local_env destr lenv) ?, lbl'〉
856  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λ_.
857    〈translate_op1 globals ty' ty op1
858      (find_local_env destr lenv)
859      (find_local_env srcr lenv) ??, lbl'〉
860  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ λ_.
861    〈translate_op2 globals op2
862      (find_local_env destr lenv)
863      (find_local_env_arg srcr1 lenv)
864      (find_local_env_arg srcr2 lenv) ??, lbl'〉
865    (* XXX: should we be ignoring this? *)
866  | St_load ignore addr destr lbl' ⇒ λ_.
867    〈translate_load globals
868      (find_local_env_arg addr lenv) ? (find_local_env destr lenv), lbl'〉
869    (* XXX: should we be ignoring this? *)
870  | St_store ignore addr srcr lbl' ⇒ λ_.
871    〈translate_store globals (find_local_env_arg addr lenv) ?
872      (find_local_env_arg srcr lenv), lbl'〉
873  | St_call_id f args retr lbl' ⇒ λ_.
874    (* Paolo: no notation to avoid ambiguity *)
875    〈bcons … (
876      match retr with
877      [ Some retr ⇒
878        CALL_ID rtl_params globals f (rtl_args args lenv) (find_local_env retr lenv)
879      | None ⇒
880        CALL_ID … f (rtl_args args lenv) [ ]
881      ]) [ ], lbl'〉
882  | St_call_ptr f args retr lbl' ⇒ λ_.
883    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
884    (* Paolo: no notation to avoid ambiguity *)
885    〈bcons … (
886      match retr with
887      [ Some retr ⇒
888        extension rtl_params globals (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))
889      | None ⇒
890        extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
891      ]) [ ], lbl'〉
892  | St_tailcall_id f args ⇒ λ_.
893    〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉
894  | St_tailcall_ptr f args ⇒ λ_.
895    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
896    〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉
897  | St_cond r lbl_true lbl_false ⇒ λ_.
898    〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
899  | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
900  | St_return ⇒ λeq_stmt.⊥
901  ] (refl …).
902  [11: cases not_implemented (* jtable case *)
903  |12: >eq_stmt in stmt_prf; normalize //
904  |*: cases daemon
905  (* TODO: proofs regarding lengths of lists, examine! *)
906  (* Paolo: probably hypotheses need to be added *)
907  ]
908qed.
909
910definition translate_stmt ≝
911  λglobals,lenv,lbl,stmt,def.
912  match stmt return λx.stmt = x → rtl_internal_function globals with
913  [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def
914  | _ ⇒ λstmt_eq.
915    let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
916    rtl_adds_graph globals translation lbl lbl' def
917  ] (refl …).
918>stmt_eq normalize % qed.
919 
920 
921(* XXX: we use a "hack" here to circumvent the proof obligations required to
922   create res, an empty internal_function record.  we insert into our graph
923   the start and end nodes to ensure that they are in, and place dummy
924   skip instructions at these nodes. *)
925definition translate_internal ≝
926  λglobals: list ident.
927  λdef.
928  let runiverse ≝ f_reggen def in
929  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
930    (f_params def @ f_locals def) (f_result def) in
931  let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
932  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
933  let result ≝
934    match (f_result def) with
935    [ None ⇒ [ ]
936    | Some r_typ ⇒
937      let 〈r, typ〉 ≝ r_typ in
938        find_local_env r lenv
939    ]
940  in
941  let luniverse' ≝ f_labgen def in
942  let runiverse' ≝ runiverse in
943  let result' ≝ result in
944  let params' ≝ params in
945  let locals' ≝ locals in
946  let stack_size' ≝ f_stacksize def in
947  let entry' ≝ f_entry def in
948  let exit' ≝ f_exit def in
949  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params globals entry') in
950  let graph' ≝ add LabelTag ? graph' exit' (RETURN rtl_params globals) in
951  let res ≝
952    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
953     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
954    foldi … (translate_stmt globals … lenv) (f_graph def) res.
955[ @graph_add_lookup @graph_add
956| @graph_add ]
957qed.
958
959(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
960  because of CompCert heritage *)
961definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
962 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracBrowser for help on using the repository browser.