source: src/RTLabs/RTLabsToRTL_paolo.ma @ 1640

Last change on this file since 1640 was 1640, checked in by tranquil, 9 years ago
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File size: 32.4 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  ].
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 … (λr.λb : Byte.r ← (b : rtl_argument)) 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.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  [destr ← srcr .Or. 127 ;
272   destr ← .Rl. destr ;
273   destr ← .Inc. destr ;
274   destr ← .Cmpl. 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 ⇒ [destr ← 0]
357    | cons srcr srcrs' ⇒
358      let f : register → rtl_instruction globals ≝
359        λr. destr ← destr .Or. r in
360      MOVE rtl_params globals 〈destr,srcr〉 ::
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      [tmp ← 0 ;
367       destr ← tmp .Sub. tmp ;
368       (* now carry bit is set iff destr was non-null *)
369       destr ← tmp .Addc. 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
406include alias "arithmetics/nat.ma".
407
408let rec range_strong_internal (start : ℕ) (count : ℕ)
409  (* Paolo: no notation to avoid ambiguity *)
410  on count : list (Σn : ℕ.lt n (plus start count)) ≝
411match count return λx.count = x → list (Σn : ℕ. n < start + count)
412  with
413[ O ⇒ λ_.[ ]
414| S count' ⇒ λEQ.
415  let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝
416    λsig.match sig with [mk_Sig n prf ⇒ n] in
417  start :: map … f (range_strong_internal (S start) count')
418] (refl …).
419destruct(EQ) // qed.
420
421definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
422  λend.range_strong_internal 0 end.
423
424definition translate_mul_i :
425  ∀globals.
426  register → register →
427  (* size of destination and sources *)
428  ∀n : ℕ.
429  (* the temporary destination, with a dummy register at the end *)
430  ∀tmp_destrs_dummy : list register.
431  ∀srcrs1,srcrs2 : list rtl_argument.
432  |tmp_destrs_dummy| = S n →
433  n = |srcrs1| →
434  |srcrs1| = |srcrs2| →
435  (* the position of the least significant byte of the result we compute at
436     this stage (goes from 0 to n in the main function) *)
437  ∀k : ℕ.
438  lt k n →
439  (* the position of the byte in the first source we will use in this stage.
440     the position in the other source will be k - i *)
441  (Σi.i<S k) →
442  (* the accumulator *)
443  list (rtl_instruction globals) →
444    list (rtl_instruction globals) ≝
445  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
446    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
447  (* the following will expand to
448     a, b ← srcrs1[i] * srcrs2[k-i]
449     tmp_destrs_dummy[k]   ← tmp_destrs_dummy[k] + a
450     tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C
451     tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C
452     ...
453     tmp_destrs_dummy[n]   ← tmp_destrs_dummy[n] + 0 + C
454     ( all calculations on tmp_destrs_dummy[n] will be eliminated with
455     liveness analysis) *)
456  match i_sig with
457    [ mk_Sig i i_prf ⇒
458      (* we pad the result of a byte multiplication with zeros in order
459         for the bit to be carried. Redundant calculations will be eliminated
460         by constant propagation. *)
461      let args : list rtl_argument ≝
462        [Reg a;Reg b] @ make ? (Imm (zero …)) (n - 1 - k) in
463      let tmp_destrs_view : list register ≝
464        ltl ? tmp_destrs_dummy k in
465      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (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          [❮destr1, destr2❯ ← srcr1 .DivuModu. 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
563(* Paolo: to be moved elsewhere *)
564let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
565  (prf : |l1| = |l2|) on l1 : C ≝
566  match l1 return λx.x = l1 → C with 
567  [ nil ⇒ λ_.init
568  | cons a l1' ⇒ λeq_l1.
569    match l2 return λy.y = l2 → C with
570    [ nil ⇒ λeq_l2.⊥
571    | cons b l2' ⇒ λeq_l2.
572      f a b (foldr2 A B C f init l1' l2' ?)
573    ] (refl …)
574  ] (refl …).
575destruct normalize in prf;  [destruct|//]
576qed.
577
578definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
579  λglobals: list ident.
580  λdestrs: list register.
581  λsrcrs1: list rtl_argument.
582  λsrcrs2: list rtl_argument.
583  λsrcrs1_prf : |destrs| = |srcrs1|.
584  λsrcrs2_prf : |srcrs1| = |srcrs2|.
585  let return_type ≝ bind_list register unit (rtl_instruction globals) in
586  match destrs return λx.x = destrs → return_type with
587  [ nil ⇒ λ_.[ ]
588  | cons destr destrs' ⇒ λeq_destrs.
589    match srcrs1 return λy.y = srcrs1 → return_type with
590    [ nil ⇒ λeq_srcrs1.⊥
591    | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
592      match srcrs2 return λz.z = srcrs2 → return_type with
593      [ nil ⇒ λeq_srcrs2.⊥
594      | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
595        νtmpr in
596        let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝
597          λs1,s2,acc.
598          tmpr  ← s1 .Xor. s2 ::
599          destr ← destr .Or. tmpr ::
600          acc in
601        let epilogue : list (rtl_instruction globals) ≝
602          [ CLEAR_CARRY … ;
603            tmpr ← 0 .Sub. destr ;
604            (* now carry bit is 1 iff destrs != 0 *)
605            destr ← 0 .Addc. 0 ] in
606         translate_cast_unsigned … destrs' @
607         destr ← srcr1 .Xor. srcr2 ::
608         foldr2 ??? f epilogue srcrs1' srcrs2' ?
609       ] (refl …)
610     ] (refl …)
611   ] (refl …).
612   destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct // qed.
613
614(* if destrs is 0 or 1, it inverses it. To be used after operations that
615   ensure this. *)
616definition translate_toggle_bool : ∀globals.?→list (rtl_instruction globals) ≝
617  λglobals: list ident.
618  λdestrs: list register.
619  match destrs with
620  [ nil ⇒ [ ]
621  | cons destr _ ⇒ [destr ← .Cmpl. destr]
622  ].
623 
624definition translate_lt_unsigned :
625  ∀globals.
626  ∀destrs: list register.
627  ∀srcrs1: list rtl_argument.
628  ∀srcrs2: list rtl_argument.
629  |destrs| = |srcrs1| →
630  |srcrs1| = |srcrs2| →
631  list (rtl_instruction globals) ≝
632  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
633  match destrs with
634  [ nil ⇒ [ ]
635  | cons destr destrs' ⇒
636    translate_cast_unsigned … destrs' @
637    (* I perform a subtraction, but the only interest is in the carry bit *)
638    translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @
639    [ destr ← 0 .Addc. 0 ]
640  ].
641[ <make_length ] assumption qed.
642
643(* shifts signed integers by adding 128 to the most significant byte
644   it replaces it with a fresh register which must be provided *)
645let rec shift_signed globals
646  (tmp : register)
647  (srcrs : list rtl_argument) on srcrs :
648  (list rtl_argument) × (list (rtl_instruction globals)) ≝
649  match srcrs with
650  [ nil ⇒ 〈[ ],[ ]〉
651  | cons srcr srcrs' ⇒
652    match srcrs' with
653    [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
654    | _ ⇒
655      let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in
656      〈srcr :: new_srcrs', op〉
657    ]
658  ].
659
660lemma shift_signed_length : ∀globals,tmp,srcrs.
661  |\fst (shift_signed globals tmp srcrs)| = |srcrs|.
662#globals #tmp #srcrs elim srcrs [//]
663#srcr * [//]
664#srcr' #srcrs'' #Hi
665whd in ⊢ (??(??(???%))?);
666@pair_elim #new_srcrs' #op #EQ >EQ in Hi;
667normalize #Hi >Hi //
668qed.
669
670definition translate_lt_signed :
671  ∀globals.
672  ∀destrs: list register.
673  ∀srcrs1: list rtl_argument.
674  ∀srcrs2: list rtl_argument.
675  |destrs| = |srcrs1| →
676  |srcrs1| = |srcrs2| →
677  bind_list register unit (rtl_instruction globals) ≝
678  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
679  νtmp_last_s1 in
680  νtmp_last_s2 in
681  let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in
682  let new_srcrs1 ≝ \fst p1 in
683  let shift_srcrs1 ≝ \snd p1 in
684  let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in
685  let new_srcrs2 ≝ \fst p2 in
686  let shift_srcrs2 ≝ \snd p2 in
687  shift_srcrs1 @ shift_srcrs2 @
688  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ??.
689>shift_signed_length [2: >shift_signed_length] assumption qed.
690
691definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
692  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
693  if is_unsigned then
694    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
695  else
696    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf.
697
698definition translate_cmp ≝
699  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
700  match cmp with
701  [ Ceq ⇒
702    translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
703    translate_toggle_bool globals destrs
704  | Cne ⇒
705    translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
706  | Clt ⇒
707    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
708  | Cgt ⇒
709    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ?
710  | Cle ⇒
711    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ? @
712    translate_toggle_bool globals destrs
713  | Cge ⇒
714    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
715    translate_toggle_bool globals destrs
716  ].
717// qed.
718 
719definition translate_op2 :
720  ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
721  λglobals: list ident.
722  λop2.
723  λdestrs: list register.
724  λsrcrs1: list rtl_argument.
725  λsrcrs2: list rtl_argument.
726  λsrcrs1_prf: |destrs| = |srcrs1|.
727  λsrcrs2_prf: |srcrs1| = |srcrs2|.
728  match op2 with
729  [ Oadd ⇒
730    translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
731  | Oaddp ⇒
732    translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
733  | Osub ⇒
734    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
735  | Osubpi ⇒
736    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
737  | Osubpp _ ⇒
738    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
739  | Omul ⇒
740    translate_mul globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
741  | Odivu ⇒
742    translate_divumodu8 globals true destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
743  | Omodu ⇒
744    translate_divumodu8 globals false destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
745  | Oand ⇒
746    translate_op globals And destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
747  | Oor ⇒
748    translate_op globals Or destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
749  | Oxor ⇒
750    translate_op globals Xor destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
751  | Ocmp c ⇒
752    translate_cmp false globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
753  | Ocmpu c ⇒
754    translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
755  | Ocmpp c ⇒
756    translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
757  | _ ⇒ ? (* assert false, implemented in run time or float op *)
758  ].
759  cases not_implemented (* XXX: yes, really *) qed.
760
761definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_instruction globals) ≝
762  λglobals: list ident.
763  λsrcrs: list register.
764  λlbl_true: label.
765  match srcrs with
766  [ nil ⇒ [ ]
767  | cons srcr srcrs' ⇒
768    ν tmpr in
769    let f : register → rtl_instruction globals ≝
770      λr. tmpr ← tmpr .Or. r in
771    MOVE rtl_params globals 〈tmpr,srcr〉 ::
772    map … f srcrs' @
773    [ COND ?? tmpr lbl_true ]
774  ].
775
776(* Paolo: to be controlled (original seemed overly complex) *)
777definition translate_load ≝
778  λglobals: list ident.
779  λaddr : list rtl_argument.
780  λaddr_prf: 2 = |addr|.
781  λdestrs: list register.
782  ν tmp_addr_l in
783  ν tmp_addr_h in
784  let f ≝ λdestr : register.λacc : list (rtl_instruction globals).
785    LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
786    translate_op … Add
787      [tmp_addr_l ; tmp_addr_h]
788      [Reg tmp_addr_l ; Reg tmp_addr_h]
789      [imm_nat 0 ; Imm int_size] ? ? @ acc in
790  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
791  foldr … f [ ] destrs.
792[1: <addr_prf] // qed.
793 
794definition translate_store ≝
795  λglobals: list ident.
796  λaddr : list rtl_argument.
797  λaddr_prf: 2 = |addr|.
798  λsrcrs: list rtl_argument.
799  ν tmp_addr_l in
800  ν tmp_addr_h in
801  let f ≝ λsrcr : rtl_argument.λacc : list (rtl_instruction globals).
802    STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
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 [ ] srcrs.
809[1: <addr_prf] // qed.
810
811(* alias for b_adds_graph *)
812definition rtl_adds_graph ≝
813  λglobals.b_adds_graph rtl_params globals register unit
814    (rtl_ertl_fresh_reg rtl_params rtl_params globals).
815
816axiom fake_label: label.
817
818definition stmt_not_return ≝ λstmt.match stmt with
819  [ St_return ⇒ False
820  | _ ⇒ True ].
821
822(* XXX: following conversation with CSC about the mix up in extension statements
823        and extension instructions in RTL, use fake_label in calls to
824        tailcall_* instructions. *)
825definition translate_inst : ∀globals.?→?→?→
826  Prod (bind_list register unit (rtl_instruction globals)) label ≝
827  λglobals: list ident.
828  λlenv: local_env.
829  λstmt.
830  λstmt_prf : stmt_not_return stmt.
831  match stmt return λx.stmt = x →
832    (bind_list register unit (rtl_instruction globals)) × label with
833  [ St_skip lbl' ⇒ λ_.
834    〈[ ], lbl'〉
835  | St_cost cost_lbl lbl' ⇒ λ_.
836    〈[COST_LABEL … cost_lbl], lbl'〉
837  | St_const destr cst lbl' ⇒ λ_.
838    〈translate_cst globals cst (find_local_env destr lenv) ?, lbl'〉
839  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λ_.
840    〈translate_op1 globals ty' ty op1
841      (find_local_env destr lenv)
842      (find_local_env srcr lenv) ??, lbl'〉
843  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ λ_.
844    〈translate_op2 globals op2
845      (find_local_env destr lenv)
846      (find_local_env_arg srcr1 lenv)
847      (find_local_env_arg srcr2 lenv) ??, lbl'〉
848    (* XXX: should we be ignoring this? *)
849  | St_load ignore addr destr lbl' ⇒ λ_.
850    〈translate_load globals
851      (find_local_env_arg addr lenv) ? (find_local_env destr lenv), lbl'〉
852    (* XXX: should we be ignoring this? *)
853  | St_store ignore addr srcr lbl' ⇒ λ_.
854    〈translate_store globals (find_local_env_arg addr lenv) ?
855      (find_local_env_arg srcr lenv), lbl'〉
856  | St_call_id f args retr lbl' ⇒ λ_.
857    (* Paolo: no notation to avoid ambiguity *)
858    〈bcons … (
859      match retr with
860      [ Some retr ⇒
861        CALL_ID rtl_params globals f (rtl_args args lenv) (find_local_env retr lenv)
862      | None ⇒
863        CALL_ID … f (rtl_args args lenv) [ ]
864      ]) [ ], lbl'〉
865  | St_call_ptr f args retr lbl' ⇒ λ_.
866    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
867    (* Paolo: no notation to avoid ambiguity *)
868    〈bcons … (
869      match retr with
870      [ Some retr ⇒
871        extension rtl_params globals (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))
872      | None ⇒
873        extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
874      ]) [ ], lbl'〉
875  | St_tailcall_id f args ⇒ λ_.
876    〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉
877  | St_tailcall_ptr f args ⇒ λ_.
878    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
879    〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉
880  | St_cond r lbl_true lbl_false ⇒ λ_.
881    〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
882  | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
883  | St_return ⇒ λeq_stmt.⊥
884  ] (refl …).
885  [11: cases not_implemented (* jtable case *)
886  |12: >eq_stmt in stmt_prf; normalize //
887  |*: cases daemon
888  (* TODO: proofs regarding lengths of lists, examine! *)
889  (* Paolo: probably hypotheses need to be added *)
890  ]
891qed.
892
893definition translate_stmt ≝
894  λglobals,lenv,lbl,stmt,def.
895  match stmt return λx.stmt = x → rtl_internal_function globals with
896  [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) 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>stmt_eq normalize % qed.
902 
903 
904(* XXX: we use a "hack" here to circumvent the proof obligations required to
905   create res, an empty internal_function record.  we insert into our graph
906   the start and end nodes to ensure that they are in, and place dummy
907   skip instructions at these nodes. *)
908definition translate_internal ≝
909  λglobals: list ident.
910  λdef.
911  let runiverse ≝ f_reggen def in
912  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
913    (f_params def @ f_locals def) (f_result def) in
914  let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in
915  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
916  let result ≝
917    match (f_result def) with
918    [ None ⇒ [ ]
919    | Some r_typ ⇒
920      let 〈r, typ〉 ≝ r_typ in
921        find_local_env r lenv
922    ]
923  in
924  let luniverse' ≝ f_labgen def in
925  let runiverse' ≝ runiverse in
926  let result' ≝ result in
927  let params' ≝ parameters in
928  let locals' ≝ locals in
929  let stack_size' ≝ f_stacksize def in
930  let entry' ≝ f_entry def in
931  let exit' ≝ f_exit def in
932  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry'
933    (GOTO (rtl_params : params) globals entry') in
934  let graph' ≝ add LabelTag ? graph' exit'
935    (RETURN (rtl_params : params) globals) in
936  let res ≝
937    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
938     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
939    foldi … (translate_stmt globals … lenv) (f_graph def) res.
940[ @graph_add_lookup @graph_add
941| @graph_add ]
942qed.
943
944(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
945  because of CompCert heritage *)
946definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
947 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracBrowser for help on using the repository browser.