source: src/RTLabs/RTLabsToRTL_paolo.ma @ 1638

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