source: src/RTLabs/RTLabsToRTL_paolo.ma @ 2176

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