source: src/RTLabs/RTLabsToRTL_paolo.ma @ 2224

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