source: src/RTLabs/RTLabsToRTL_paolo.ma @ 1692

Last change on this file since 1692 was 1644, checked in by tranquil, 8 years ago

minor changes

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