source: src/RTLabs/RTLabsToRTL_paolo.ma @ 1988

Last change on this file since 1988 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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