source: src/RTLabs/RTLabsToRTL_paolo.ma @ 2208

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