source: src/RTLabs/RTLabsToRTL_paolo.ma @ 2032

Last change on this file since 2032 was 2032, checked in by sacerdot, 7 years ago

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

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