source: src/RTLabs/RTLabsToRTL.ma @ 1315

Last change on this file since 1315 was 1315, checked in by mulligan, 9 years ago

another move for the same reason. got rtlabs > rtl compiling again by using a daemon

File size: 44.3 KB
RevLine 
[789]1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
[1071]4include "common/FrontEndOps.ma".
[789]5include "common/Graphs.ma".
[1280]6include "joint/TranslateUtils.ma".
[789]7
[1047]8let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
9  match n with
[1281]10  [ O ⇒ 〈[],runiverse〉
11  | S n' ⇒
12     let 〈r,runiverse〉 ≝ fresh … runiverse in
13     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
14      〈r::res,runiverse〉 ].
[1047]15
16definition complete_regs ≝
[1280]17  λglobals.
[1047]18  λdef.
19  λsrcrs1.
20  λsrcrs2.
[1280]21  if leb (length … srcrs2) (length … srcrs1) then
22   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
23    〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
24  else
25   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
26    〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
[1047]27
[1280]28lemma complete_regs_length:
29  ∀globals,def,left,right.
30   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
31 #globals #def #left #right
32 whd in match complete_regs normalize nodelta
33 @leb_elim normalize nodelta #H
34 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
35 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
36 cases (fresh_regs ????) #def' #fresh normalize >append_length
37 generalize in match H -H;
38 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
39 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
40         <plus_minus_m_m /2/ ]
41qed.
[1064]42
[1053]43definition size_of_sig_type ≝
[1052]44  λsig.
45  match sig with
[1047]46  [ ASTint isize sign ⇒
[1053]47    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
48      isize' ÷ (nat_of_bitvector ? int_size)
49  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
50  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
[1047]51  ].
[1053]52  cases not_implemented;
[1052]53qed.
[1047]54
[789]55inductive register_type: Type[0] ≝
56  | register_int: register → register_type
57  | register_ptr: register → register → register_type.
58
[1280]59definition local_env ≝ BitVectorTrie (list register) 16.
[789]60
[1280]61definition mem_local_env : register → local_env → bool ≝
62  λr. member … (word_of_identifier … r).
[1052]63
[1280]64definition add_local_env : register → list register → local_env → local_env ≝
65  λr. insert … (word_of_identifier … r).
[1052]66
[1280]67definition find_local_env : register → local_env → list register ≝
68  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
[1052]69
[789]70definition initialize_local_env_internal ≝
[1281]71  λlenv_runiverse.
[1053]72  λr_sig.
[1281]73  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
[1053]74  let 〈r, sig〉 ≝ r_sig in
75  let size ≝ size_of_sig_type sig in
[1281]76  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
77    〈add_local_env r rs lenv,runiverse〉.
[789]78
79definition initialize_local_env ≝
80  λruniverse.
81  λregisters.
[1053]82  λresult.
[1050]83  let registers ≝ registers @
84    match result with
85    [ None ⇒ [ ]
86    | Some rt ⇒ [ rt ]
87    ]
88  in
[1281]89    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
[1280]90
[1050]91definition map_list_local_env_internal ≝
[1280]92  λlenv,res,r. res @ (find_local_env r lenv).
[1050]93   
94definition map_list_local_env ≝
[1280]95  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
[1050]96
[1053]97definition make_addr ≝
98  λA.
99  λlst: list A.
[1066]100  λprf: 2 ≤ length A lst.
101  match lst return λx. 2 ≤ |x| → A × A with
[1053]102  [ nil ⇒ λlst_nil_prf. ?
103  | cons hd tl ⇒ λprf.
[1066]104    match tl return λx. 1 ≤ |x| → A × A with
[1053]105    [ nil ⇒ λtl_nil_prf. ?
106    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
107    ] ?
108  ] prf.
109  [1: normalize in lst_nil_prf;
[1066]110      cases(not_le_Sn_O 1);
111      #HYP cases(HYP lst_nil_prf)
[1053]112  |2: normalize in prf;
[1066]113      @le_S_S_to_le
114      assumption
[1053]115  |3: normalize in tl_nil_prf;
[1066]116      cases(not_le_Sn_O 0)
[1280]117      #HYP cases(HYP tl_nil_prf)]
[1053]118qed.
[1050]119
[789]120definition find_and_addr ≝
[1280]121  λr,lenv. make_addr ? (find_local_env r lenv).
[789]122
123definition rtl_args ≝
[1280]124  λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).
[789]125
[1057]126definition translate_cst_int_internal ≝
[1282]127  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
[1057]128
[1308]129axiom split_into_bytes:
130  ∀size.
131  ∀int: bvint size.
132    Σbytes: list Byte. |bytes| = size_intsize size.
133
134lemma eqb_implies_eq:
135  ∀m, n: nat.
136    eqb m n = true → m = n.
137  #M
138  elim M
139  [1: #N normalize
140      cases N
141      [1: normalize //
142      |2: #M' normalize #HYP destruct(HYP)
143      ]
144  |2: #M' #IND_HYP #N
145      normalize
146      cases N
147      [1: normalize #HYP destruct(HYP)
148      |2: #M'' normalize #HYP
149          @eq_f @(IND_HYP M'')
150          assumption
151      ]
152   ]
153qed.
154
[1307]155let rec translate_cst
156  (globals: list ident) (cst: constant) (destrs: list register)
157    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
158      on cst: rtl_internal_function globals ≝
159  match cst with
160  [ Ointconst size const ⇒
161    match destrs with
[1308]162    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
163    | _   ⇒
164      let size' ≝ size_intsize size in
165        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
166        [ true  ⇒ λgood_case.
167          match split_into_bytes size const with
168          [ dp bytes bytes_length_proof ⇒
169            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
170              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
171          ]
172        | false ⇒ λbad_case. ?
173        ] (refl … (eqb size' (|destrs|)))
[1307]174    ]
175  | Ofloatconst float ⇒ ⊥
[1308]176  | Oaddrsymbol id offset ⇒
177    let 〈r1, r2〉 ≝ make_addr … destrs ? in
178      add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def
179  | Oaddrstack offset ⇒
180    let 〈r1, r2〉 ≝ make_addr … destrs ? in
[1315]181      ?
182      (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *)
[1307]183  ].
[1308]184  [1: >bytes_length_proof
185      cut(size' = |destrs|)
186      [1: @eqb_implies_eq
187          assumption
188      |2: #EQ_HYP
189          <EQ_HYP %
190      ]
191  |5: cases not_implemented (* XXX: float, error_float in o'caml *)
[1315]192  |*: cases daemon
[1307]193  ].
[1315]194qed.
[1307]195 
[1059]196definition translate_move_internal ≝
[1280]197  λglobals.
[1059]198  λdestr: register.
199  λsrcr: register.
[1283]200    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
[1057]201
[1059]202definition translate_move ≝
[1280]203  λglobals.
[1059]204  λdestrs: list register.
205  λsrcrs: list register.
206  λstart_lbl: label.
[1071]207    match reduce_strong register register destrs srcrs with
[1060]208    [ dp crl_crr len_proof ⇒
209      let commonl ≝ \fst (\fst crl_crr) in
210      let commonr ≝ \fst (\snd crl_crr) in
211      let restl ≝ \snd (\fst crl_crr) in
212      let restr ≝ \snd (\snd crl_crr) in
[1283]213      let f_common ≝ translate_move_internal globals in
[1280]214      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
215      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
216        add_translates … [ translate1 ; translate2 ] start_lbl
[1060]217    ].
218    @len_proof
219qed.
220
221let rec make
222  (A: Type[0]) (elt: A) (n: nat) on n ≝
223  match n with
224  [ O ⇒ [ ]
225  | S n' ⇒ elt :: make A elt n'
226  ].
227 
228lemma make_length:
229  ∀A: Type[0].
230  ∀elt: A.
231  ∀n: nat.
232    n = length ? (make A elt n).
233  #A #ELT #N
234  elim N
235  [ normalize %
236  | #N #IH
237    normalize <IH %
238  ]
239qed.
240
241definition translate_cast_unsigned ≝
[1280]242  λglobals.
[1060]243  λdestrs.
244  λstart_lbl.
245  λdest_lbl.
[1280]246  λdef: joint_internal_function … (rtl_params globals).
247  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
248  let zeros ≝ make … tmp_zero (length … destrs) in
249    add_translates … [
250      adds_graph rtl_params1 … [
[1283]251        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
[1060]252        ];
[1280]253      translate_move globals destrs zeros
[1060]254    ] start_lbl dest_lbl def.
255
[1285]256definition translate_cast_signed:
257    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
258  λglobals: list ident.
[1060]259  λdestrs.
260  λsrcr.
261  λstart_lbl.
262  λdest_lbl.
263  λdef.
[1280]264  let 〈def, tmp_128〉 ≝ fresh_reg … def in
265  let 〈def, tmp_255〉 ≝ fresh_reg … def in
266  let 〈def, tmpr〉 ≝ fresh_reg … def in
267  let 〈def, dummy〉 ≝ fresh_reg … def in
[1060]268  let insts ≝ [
[1285]269    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
270    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
271    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
272    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
273    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
274  ]
275  in
[1280]276  let srcrs ≝ make … tmpr (length … destrs) in
[1285]277    add_translates rtl_params1 globals [
278      adds_graph rtl_params1 globals insts;
279      translate_move globals destrs srcrs
[1060]280    ] start_lbl dest_lbl def.
281
282definition translate_cast ≝
[1285]283  λglobals: list ident.
284  λsrc_size: nat.
285  λsrc_sign: signedness.
286  λdest_size: nat.
287  λdestrs: list register.
288  λsrcrs: list register.
[1066]289  match |srcrs| return λx. |srcrs| = x → ? with
[1285]290  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
[1060]291  | S n' ⇒ λsucc_prf.
292    if ltb dest_size src_size then
[1285]293      translate_move globals destrs srcrs
[1060]294    else
[1071]295      match reduce_strong register register destrs srcrs with
[1060]296      [ dp crl len_proof ⇒
297        let commonl ≝ \fst (\fst crl) in
298        let commonr ≝ \fst (\snd crl) in
299        let restl ≝ \snd (\fst crl) in
300        let restr ≝ \snd (\snd crl) in
[1285]301        let insts_common ≝ translate_move globals commonl commonr in
[1060]302        let sign_reg ≝ last_safe ? srcrs ? in
303        let insts_sign ≝
304          match src_sign with
[1285]305          [ Unsigned ⇒ translate_cast_unsigned globals restl
306          | Signed ⇒ translate_cast_signed globals restl sign_reg
[1060]307          ]
308        in
[1285]309          add_translates rtl_params1 globals [ insts_common; insts_sign ]
[1060]310      ]
311  ] (refl ? (|srcrs|)).
312  >succ_prf //
313qed.
314
315definition translate_negint ≝
[1285]316  λglobals: list ident.
317  λdestrs: list register.
318  λsrcrs: list register.
319  λstart_lbl: label.
320  λdest_lbl: label.
321  λdef: rtl_internal_function globals.
322  λprf: |destrs| = |srcrs|. (* assert in caml code *)
323  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
324  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
325  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
[1060]326  let insts_init ≝ [
[1285]327    sequential … (SET_CARRY …);
328    sequential … (INT rtl_params_ globals tmpr (zero ?))
[1060]329  ] in
[1285]330  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
[1060]331  let insts_add ≝ map … f_add destrs in
[1285]332    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
[1060]333
[1285]334definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
335  λglobals: list ident.
336  λdestrs: list register.
337  λsrcrs: list register.
338  λstart_lbl: label.
339  λdest_lbl: label.
340  λdef: rtl_internal_function globals.
[1060]341  match destrs with
[1285]342  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
[1060]343  | cons destr destrs ⇒
[1285]344    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
345    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
346    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
347    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
[1060]348    let f ≝ λtmp_srcr. [
[1285]349      sequential … (CLEAR_CARRY rtl_params_ globals);
350      sequential … (INT rtl_params_ globals tmpr (zero ?));
351      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
352      sequential … (INT rtl_params_ globals tmpr (zero ?));
353      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
354      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
[1060]355    ] in
[1285]356    let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
357    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
358      add_translates rtl_params1 globals [
359        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
[1060]360      ] start_lbl dest_lbl def
361  ].
362
[1066]363(* TODO: examine this properly.  This is a change from the O'caml code due
364   to us dropping the explicit use of a cast destination size field.  We
365   instead infer the size of the cast's destination from the context.  Is
366   this correct?
367*)
[1064]368definition translate_op1 ≝
[1286]369  λglobals: list ident.
[1066]370  λop1: unary_operation.
[1064]371  λdestrs: list register.
372  λsrcrs: list register.
[1062]373  λprf: |destrs| = |srcrs|.
[1064]374  λstart_lbl: label.
375  λdest_lbl: label.
[1286]376  λdef: rtl_internal_function globals.
[1060]377  match op1 with
[1066]378  [ Ocastint src_sign src_size ⇒
379    let dest_size ≝ |destrs| * 8 in
380    let src_size ≝ bitsize_of_intsize src_size in
[1286]381      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
[1066]382  | Onegint ⇒
[1286]383      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
[1066]384  | Onotbool ⇒
[1286]385      translate_notbool globals destrs srcrs start_lbl dest_lbl def
[1066]386  | Onotint ⇒
[1286]387    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
[1060]388    let l ≝ map2 … f destrs srcrs prf in
[1286]389      adds_graph rtl_params1 globals l start_lbl dest_lbl def
[1066]390  | Optrofint r ⇒
[1286]391      translate_move globals destrs srcrs start_lbl dest_lbl def
[1066]392  | Ointofptr r ⇒
[1286]393      translate_move globals destrs srcrs start_lbl dest_lbl def
[1066]394  | Oid ⇒
[1286]395      translate_move globals destrs srcrs start_lbl dest_lbl def
[1066]396  | _ ⇒ ? (* float operations implemented in runtime *)
[1060]397  ].
[1066]398  cases not_implemented
399qed.
[1061]400 
[1286]401definition translate_op: ∀globals. ? → list register → list register → list register →
402  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
403  λglobals: list ident.
[1061]404  λop.
[1286]405  λdestrs: list register.
406  λsrcrs1: list register.
407  λsrcrs2: list register.
408  λstart_lbl: label.
409  λdest_lbl: label.
410  λdef: rtl_internal_function globals.
[1071]411  match reduce_strong register register srcrs1 srcrs2 with
[1061]412  [ dp reduced first_reduced_proof ⇒
413    let srcrsl_common ≝ \fst (\fst reduced) in
414    let srcrsr_common ≝ \fst (\snd reduced) in
415    let srcrsl_rest ≝ \snd (\fst reduced) in
416    let srcrsr_rest ≝ \snd (\snd reduced) in
[1293]417    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
[1071]418    match reduce_strong register register destrs srcrsl_common with
[1061]419    [ dp reduced second_reduced_proof ⇒
420      let destrs_common ≝ \fst (\fst reduced) in
421      let destrs_rest ≝ \snd (\fst reduced) in
[1071]422      match reduce_strong register register destrs_rest srcrs_rest with
[1061]423      [ dp reduced third_reduced_proof ⇒
424        let destrs_cted ≝ \fst (\fst reduced) in
425        let destrs_rest ≝ \snd (\fst reduced) in
426        let srcrs_cted ≝ \fst (\snd reduced) in
[1286]427        let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
[1061]428        let insts_init ≝ [
[1286]429          sequential … (CLEAR_CARRY …);
430          sequential … (INT rtl_params_ globals tmpr (zero …))
[1061]431        ] in
[1286]432        let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
433        let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
434        let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
435        let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in
436        let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
[1061]437        let insts_rest ≝ map … f_rest destrs_rest in
[1286]438          adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
[1061]439      ]
440    ]
441  ].
[1066]442  [1: @third_reduced_proof
443  |3: @first_reduced_proof
[1286]444  |*: cases daemon (* XXX: some of these look like they may be false *)
[1066]445  ]
[1062]446qed.
[1057]447
[1062]448let rec translate_mul1
[1286]449  (globals: list ident) (dummy: register) (tmpr: register)
450    (destrs: list register) (srcrs1: list register) (srcr2: register)
451      (start_lbl: label)
452        on srcrs1 ≝
[1062]453  match destrs with
[1286]454  [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
[1062]455  | cons destr tl ⇒
456    match tl with
457    [ nil ⇒
458      match srcrs1 with
459      [ nil ⇒
[1286]460        adds_graph rtl_params1 globals [
461          sequential … (INT rtl_params_ globals tmpr (zero …));
462          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
[1062]463        ] start_lbl
464      | cons srcr1 tl' ⇒
[1286]465        adds_graph rtl_params1 globals [
466          sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
467          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
[1062]468        ] start_lbl
469      ]
470    | cons destr2 destrs ⇒
471      match srcrs1 with
472      [ nil ⇒
[1286]473        add_translates rtl_params1 globals [
474          adds_graph rtl_params1 globals [
475            sequential … (INT rtl_params_ globals tmpr (zero …));
476            sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
477            sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
[1062]478          ];
[1286]479          translate_cst globals (Ointconst I8 (zero …)) destrs
[1062]480        ] start_lbl
481      | cons srcr1 srcrs1 ⇒
482        match destrs with
483        [ nil ⇒
[1286]484          add_translates rtl_params1 globals [
485            adds_graph rtl_params1 globals [
486              sequential … (INT rtl_params_ globals tmpr (zero …));
487              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
488              sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
[1062]489            ];
[1286]490            translate_cst globals (Ointconst I8 (zero ?)) destrs
[1062]491          ] start_lbl
492        | cons destr2 destrs ⇒
[1286]493          add_translates rtl_params1 globals [
494            adds_graph rtl_params1 globals [
495              sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
496              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
[1062]497            ];
[1286]498            translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
[1062]499          ] start_lbl
500        ]
501      ]
502    ]
503  ].
504
505definition translate_muli ≝
[1286]506  λglobals: list ident.
[1062]507  λdummy: register.
508  λtmpr: register.
509  λdestrs: list register.
510  λtmp_destrs: list register.
511  λsrcrs1: list register.
512  λdummy_lbl: label.
513  λi: nat.
[1063]514  λi_prf.
515  λtranslates: list ?.
516  λsrcr2i: register.
[1286]517  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in
[1063]518  let tmp_destrs2' ≝
519    match tmp_destrs2 with
520    [ nil ⇒ [ ]
521    | cons tmp_destr2 tmp_destrs2 ⇒ [
[1286]522        adds_graph rtl_params1 globals [
523          sequential rtl_params_ globals (CLEAR_CARRY …);
524          sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
[1063]525        ];
[1286]526        translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
527        translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
528        adds_graph rtl_params1 globals [
529          sequential rtl_params_ globals (CLEAR_CARRY …)
[1063]530        ];
[1286]531        translate_op globals Addc destrs destrs tmp_destrs
[1063]532      ]
533    ]
534  in
535    translates @ tmp_destrs2'.
[1062]536
[1064]537axiom translate_mul:
[1286]538  ∀globals: list ident.
[1064]539  ∀destrs: list register.
540  ∀srcrs1: list register.
541  ∀srcrs2: list register.
542  ∀start_lbl: label.
543  ∀dest_lbl: label.
[1286]544  ∀def: rtl_internal_function globals.
545    rtl_internal_function globals.
[1064]546
547(*
[1063]548definition translate_mul ≝
[1287]549  λglobals: list ident.
[1063]550  λdestrs: list register.
551  λsrcrs1: list register.
552  λsrcrs2: list register.
553  λstart_lbl: label.
554  λdest_lbl: label.
[1287]555  λdef: rtl_internal_function globals.
556  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
557  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
558  let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in
559  let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
560  let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
[1063]561  let insts_init ≝ [
[1287]562    translate_move globals fresh_srcrs1 srcrs1;
563    translate_move globals fresh_srcrs2 srcrs2;
564    translate_cst globals (Ointconst I8 (zero …)) destrs
[1063]565  ]
566  in
[1306]567  let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
568  let insts_mul ≝ foldi … f [ ] srcrs2 in ?.
[1063]569    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
[1064]570*)
[1062]571
[1064]572definition translate_divumodu8 ≝
[1287]573  λglobals: list ident.
[1064]574  λorder: bool.
575  λdestrs: list register.
576  λsrcr1: register.
577  λsrcr2: register.
578  λstart_lbl: label.
579  λdest_lbl: label.
[1287]580  λdef: rtl_internal_function globals.
[1064]581  match destrs with
[1287]582  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
[1064]583  | cons destr destrs ⇒
[1287]584    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
[1064]585    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
[1287]586    let inst_div ≝ adds_graph rtl_params1 globals [
587      sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
[1064]588    ]
589    in
[1287]590    let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
591      add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
[1064]592  ].
[1063]593
[1287]594definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
595  λglobals: list ident.
[1064]596  λdestrs: list register.
597  λsrcrs1: list register.
598  λsrcrs2: list register.
599  λstart_lbl: label.
600  λdest_lbl: label.
[1287]601  λdef: rtl_internal_function globals.
[1064]602  match destrs with
[1287]603  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
[1064]604  | cons destr destrs ⇒
[1287]605    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
606    let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
607    let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
608    let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
609    let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
610    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
[1071]611    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
[1064]612    [ dp crl their_proof ⇒
613      let commonl ≝ \fst (\fst crl) in
614      let commonr ≝ \fst (\snd crl) in
615      let restl ≝ \snd (\snd crl) in
616      let restr ≝ \snd (\snd crl) in
[1293]617      let rest ≝ restl @ restr in
[1064]618      let inits ≝ [
[1287]619        sequential … (INT rtl_params_ globals destr (zero …));
620        sequential … (INT rtl_params_ globals tmp_zero (zero …))
[1064]621      ]
622      in
623      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
[1287]624        sequential … (CLEAR_CARRY …);
625        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
626        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
[1064]627      ]
628      in
[1287]629      let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in
[1064]630      let f_rest ≝ λtmp_srcr. [
[1287]631        sequential … (CLEAR_CARRY …);
632        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
633        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
[1064]634      ]
635      in
[1287]636      let insts_rest ≝ flatten … (map … f_rest rest) in
[1064]637      let insts ≝ inits @ insts_common @ insts_rest in
[1287]638      let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
639        add_translates rtl_params1 globals [
640          save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
[1064]641        ] start_lbl dest_lbl def
642    ]
643  ].
[1293]644  @their_proof
[1064]645qed.
646
647definition translate_eq_reg ≝
[1287]648  λglobals: list ident.
[1064]649  λtmp_zero: register.
650  λtmp_one: register.
651  λtmpr1: register.
652  λtmpr2: register.
653  λdestr: register.
654  λdummy_lbl: label.
655  λsrcr12: register × register.
656  let 〈srcr1, srcr2〉 ≝ srcr12 in
[1287]657  [ sequential … (CLEAR_CARRY …);
658    sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
659    sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
660    sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
661    sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
662    sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
663    sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
664    sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].
[1064]665
666definition translate_eq_list ≝
[1287]667  λglobals: list ident.
[1064]668  λtmp_zero: register.
669  λtmp_one: register.
670  λtmpr1: register.
671  λtmpr2: register.
672  λdestr: register.
673  λleq: list (register × register).
674  λdummy_lbl: label.
[1287]675  let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
676    (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
677      flatten … (map … f leq).
[1064]678
679definition translate_atom ≝
[1287]680  λglobals: list ident.
[1064]681  λtmp_zero: register.
682  λtmp_one: register.
683  λtmpr1: register.
684  λtmpr2: register.
685  λtmpr3: register.
686  λdestr: register.
687  λdummy_lbl: label.
688  λleq: list (register × register).
689  λsrcr1: register.
690  λsrcr2: register.
[1287]691    translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
692    [ sequential … (CLEAR_CARRY …);
693      sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
694      sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
695      sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
696      sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].
[1064]697
698definition translate_lt_main ≝
[1287]699  λglobals: list ident.
[1064]700  λtmp_zero: register.
701  λtmp_one: register.
702  λtmpr1: register.
703  λtmpr2: register.
704  λtmpr3: register.
705  λdestr: register.
706  λdummy_lbl: label.
707  λsrcrs1: list register.
708  λsrcrs2: list register.
709  λproof: |srcrs1| = |srcrs2|.
710  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
711    let 〈insts, leq〉 ≝ insts_leq in
[1287]712    let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
[1064]713      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
714  in
[1287]715    \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
[1064]716
717definition fresh_regs_strong:
[1287]718  ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
719  λglobals: list ident.
[1064]720  λdef.
721  λn.
[1287]722    fresh_regs rtl_params0 globals def n.
[1064]723  @fresh_regs_length
724qed.
725
726definition complete_regs_strong:
[1287]727  ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
728  λglobals: list ident.
[1064]729  λdef.
730  λleft.
731  λright.
[1287]732    complete_regs globals def left right.
[1064]733  @complete_regs_length
734qed.
735
736definition translate_lt ≝
[1287]737  λglobals: list ident.
[1064]738  λdestrs: list register.
[1306]739  λprf_destrs: 0 < |destrs|.
[1064]740  λsrcrs1: list register.
741  λsrcrs2: list register.
742  λstart_lbl: label.
743  λdest_lbl: label.
[1287]744  λdef: rtl_internal_function globals.
[1064]745  match destrs with
[1287]746  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
[1064]747  | _ ⇒
[1287]748    match fresh_regs_strong globals def (|destrs|) with
[1064]749    [ dp def_tmp_destrs tmp_destrs_proof ⇒
750      let def ≝ \fst def_tmp_destrs in
751      let tmp_destrs ≝ \snd def_tmp_destrs in
752      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
[1287]753      let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
754      let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
755      let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
756      let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
757      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
758      match complete_regs_strong globals def srcrs1 srcrs2 with
[1064]759      [ dp srcrs12_added srcrs12_proof ⇒
760        let srcrs1 ≝ \fst (\fst srcrs12_added) in
761        let srcrs2 ≝ \snd (\fst srcrs12_added) in
762        let added ≝ \snd srcrs12_added in
[1287]763        let srcrs1' ≝ rev … srcrs1 in
764        let srcrs2' ≝ rev … srcrs2 in
[1064]765        let insts_init ≝ [
[1287]766          translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
767          translate_cst globals (Ointconst I8 (zero ?)) added;
768          adds_graph rtl_params1 globals [
769            sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
770            sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
[1064]771          ]
772        ]
773        in
774        let insts_main ≝
[1287]775          translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
776          let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
777          let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
778            add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
[1064]779      ]
780    ]
781  ].
782  [2: >tmp_destrs_proof @prf_destrs
783  |1: normalize nodelta
784      generalize in match srcrs12_proof
785      #HYP >rev_length >rev_length @HYP
786  ]
787qed.
788
789definition add_128_to_last ≝
[1287]790  λglobals: list ident.
[1064]791  λtmp_128: register.
792  λrs.
793  λprf: 0 < |rs|.
794  λstart_lbl: label.
795  match rs with
[1287]796  [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
[1064]797  | _ ⇒
[1287]798    let r ≝ last_safe … rs prf in
799      adds_graph rtl_params1 globals [
800        sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
[1064]801      ] start_lbl
802  ].
803
804definition translate_lts ≝
[1287]805  λglobals: list ident.
[1064]806  λdestrs: list register.
[1306]807  λdestrs_prf: 0 < |destrs|.
[1064]808  λsrcrs1: list register.
809  λsrcrs2: list register.
810  λsrcrs1_lt_prf: 0 < |srcrs1|.
[1066]811  λsrcrs2_lt_prf: 0 < |srcrs2|.
[1064]812  λstart_lbl: label.
813  λdest_lbl: label.
[1287]814  λdef: rtl_internal_function globals.
815  match fresh_regs_strong globals def (|srcrs1|) with
[1064]816  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
817    let def ≝ \fst def_tmp_srcrs1 in
818    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
[1287]819    match fresh_regs_strong globals def (|srcrs2|) with
[1064]820    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
821      let def ≝ \fst def_tmp_srcrs2 in
822      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
[1287]823      let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
824        add_translates rtl_params1 globals [
825          translate_move globals tmp_srcrs1 srcrs1;
826          translate_move globals tmp_srcrs2 srcrs2;
827          adds_graph rtl_params1 globals [
828            sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
[1064]829          ];
[1287]830          add_128_to_last globals tmp_128 tmp_srcrs1 ?;
831          add_128_to_last globals tmp_128 tmp_srcrs2 ?;
832          translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
[1064]833        ] start_lbl dest_lbl def
834    ]
835  ].
[1066]836  [1: >srcrs1_prf @srcrs1_lt_prf
837  |2: >srcrs2_prf @srcrs2_lt_prf
[1064]838  ]
839qed.
840
841definition translate_op2 ≝
[1288]842  λglobals: list ident.
[1064]843  λop2.
844  λdestrs: list register.
[1306]845  λdestrs_prf: 0 < |destrs|.
[1064]846  λsrcrs1: list register.
847  λsrcrs2: list register.
[1306]848  λsrcrs1_prf: 0 < |srcrs1|. (* XXX: can this be relaxed? i think it can
849                                     but we need more dep. typ. in modu/divu
850                                     cases *)
851  λsrcrs2_prf: 0 < |srcrs2|.
[1064]852  λstart_lbl: label.
853  λdest_lbl: label.
[1288]854  λdef: rtl_internal_function globals.
[1064]855  match op2 with
[1066]856  [ Oadd ⇒
[1288]857    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]858  | Oaddp ⇒
[1288]859    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]860  | Osub ⇒
[1288]861    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]862  | Osubpi ⇒
[1288]863    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]864  | Osubpp sz ⇒
[1288]865    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]866  | Omul ⇒
[1288]867    translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]868  | Odivu ⇒
[1288]869    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
[1066]870    [ cons hd tl ⇒ λcons_prf.
871      match tl with
[1288]872      [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
[1066]873      | _ ⇒ ? (* not implemented *)
874      ]
875    | nil ⇒ λnil_absrd. ?
876    ] srcrs1_prf
877  | Omodu ⇒
[1288]878    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
[1066]879    [ cons hd tl ⇒ λcons_prf.
880      match tl with
[1288]881      [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
[1066]882      | _ ⇒ ? (* not implemented *)
883      ]
884    | nil ⇒ λnil_absrd. ?
885    ] srcrs1_prf
886  | Oand ⇒
[1288]887    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]888  | Oor ⇒
[1288]889    translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]890  | Oxor ⇒
[1288]891    translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
[1066]892  | Ocmp c ⇒
[1064]893    match c with
[1066]894    [ Ceq ⇒
[1288]895      add_translates rtl_params1 globals [
896        translate_ne globals destrs srcrs1 srcrs2;
897        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1064]898      ] start_lbl dest_lbl def
[1288]899    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
900    | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
901    | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
[1066]902    | Cle ⇒
[1288]903      add_translates rtl_params1 globals [
904        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
905        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1064]906      ] start_lbl dest_lbl def
[1066]907    | Cge ⇒
[1288]908      add_translates rtl_params1 globals [
909        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
910        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1064]911      ] start_lbl dest_lbl def
912    ]
[1066]913  | Ocmpu c ⇒
914    match c with
915    [ Ceq ⇒
[1288]916      add_translates rtl_params1 globals [
917        translate_ne globals destrs srcrs1 srcrs2;
918        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1066]919      ] start_lbl dest_lbl def
[1288]920    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
921    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
922    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
[1066]923    | Cle ⇒
[1288]924      add_translates rtl_params1 globals [
925        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
926        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1066]927      ] start_lbl dest_lbl def
928    | Cge ⇒
[1288]929      add_translates rtl_params1 globals [
930        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
931        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1066]932      ] start_lbl dest_lbl def
933    ]
934  | Ocmpp c ⇒
935    match c with
936    [ Ceq ⇒
[1288]937      add_translates rtl_params1 globals [
938        translate_ne globals destrs srcrs1 srcrs2;
939        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1066]940      ] start_lbl dest_lbl def
[1288]941    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
942    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
943    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
[1066]944    | Cle ⇒
[1288]945      add_translates rtl_params1 globals [
946        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
947        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1066]948      ] start_lbl dest_lbl def
949    | Cge ⇒
[1288]950      add_translates rtl_params1 globals [
951        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
952        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
[1066]953      ] start_lbl dest_lbl def
954    ]
955  | _ ⇒ ? (* assert false, implemented in run time or float op *)
956  ].
957  [ 2,6: normalize in nil_absrd;
958         cases(not_le_Sn_O 0)
959         #HYP cases(HYP nil_absrd)
960  | 3,7,12,17,13,15,18,19,20,21,14,16:
961         assumption
962  | *:   cases not_implemented (* yes, really *)
963  ]
964qed.
965
[1288]966definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
967  λglobals: list ident.
[1066]968  λsrcrs: list register.
969  λstart_lbl: label.
970  λlbl_true: label.
971  λlbl_false: label.
[1288]972  λdef: rtl_internal_function globals.
973  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
974  let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
975  let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
976  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
977  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
[1290]978    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
[1066]979
980definition translate_load ≝
[1292]981  λglobals: list ident.
[1066]982  λaddr.
983  λaddr_prf: 2 ≤ |addr|.
984  λdestrs: list register.
985  λstart_lbl: label.
986  λdest_lbl: label.
[1292]987  λdef: rtl_internal_function globals.
988  match fresh_regs_strong rtl_params0 globals def (|addr|) with
[1066]989  [ dp def_save_addr save_addr_prf ⇒
990    let def ≝ \fst def_save_addr in
991    let save_addr ≝ \snd def_save_addr in
[1292]992    match fresh_regs_strong rtl_params0 globals def (|addr|) with
[1066]993    [ dp def_tmp_addr tmp_addr_prf ⇒
994      let def ≝ \fst def_tmp_addr in
995      let tmp_addr ≝ \snd def_tmp_addr in
[1292]996      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
997      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
998      let insts_save_addr ≝ translate_move globals save_addr addr in
[1066]999      let f ≝ λtranslates_off. λr.
1000        let 〈translates, off〉 ≝ translates_off in
1001        let translates ≝ translates @ [
[1292]1002          adds_graph rtl_params1 globals [
1003            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
[1066]1004          ];
[1292]1005          translate_op2 globals Oaddp tmp_addr ? save_addr [tmpr] ? ?;
1006          adds_graph rtl_params1 globals [
1007            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
[1066]1008          ]
1009        ]
1010        in
[1292]1011        let 〈carry, result〉 ≝ half_add … off int_size in
[1066]1012          〈translates, result〉
1013      in
[1292]1014      let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in
1015        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
[1066]1016    ]
1017  ].
1018  [1: normalize //
1019  |2: >save_addr_prf normalize
1020      @(transitive_le 1 2 (|addr|)) //
1021  |3: >tmp_addr_prf normalize
1022      @(transitive_le 1 2 (|addr|)) //
1023  |*: >tmp_addr_prf assumption
1024  ]
1025qed.
1026
1027definition translate_store ≝
[1292]1028  λglobals: list ident.
[1066]1029  λaddr.
1030  λaddr_prf: 2 ≤ |addr|.
1031  λsrcrs: list register.
1032  λstart_lbl: label.
1033  λdest_lbl: label.
[1292]1034  λdef: rtl_internal_function globals.
1035  match fresh_regs_strong rtl_params0 globals def (|addr|) with
[1066]1036  [ dp def_tmp_addr tmp_addr_prf ⇒
1037    let def ≝ \fst def_tmp_addr in
1038    let tmp_addr ≝ \snd def_tmp_addr in
[1292]1039    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
1040    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
[1066]1041    let f ≝ λtranslate_off. λsrcr.
1042      let 〈translates, off〉 ≝ translate_off in
1043      let translates ≝ translates @ [
[1292]1044        adds_graph rtl_params1 globals [
1045          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
[1066]1046        ];
[1306]1047        translate_op2 globals Oaddp tmp_addr … addr [tmpr] ? ?;
[1292]1048        adds_graph rtl_params1 globals [
1049          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
[1066]1050        ]
1051      ]
1052      in
[1292]1053        let 〈carry, result〉 ≝ half_add … off int_size in
[1066]1054          〈translates, result〉
1055    in
[1306]1056    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in
[1292]1057      add_translates rtl_params1 globals translates start_lbl dest_lbl def
[1066]1058  ].
1059  [1: normalize //
1060  |2: >tmp_addr_prf normalize
1061      @(transitive_le 1 2 (|addr|)) //
1062  |3: >tmp_addr_prf normalize
1063      @(transitive_le 1 2 (|addr|)) //
1064  |*: >tmp_addr_prf assumption
1065  ]
1066qed.
1067
[1293]1068axiom fake_label: label.
1069
1070(* XXX: following conversation with CSC about the mix up in extension statements
[1296]1071        and extension instructions in RTL, use fake_label in calls to
1072        tailcall_* instructions. *)
[1066]1073definition translate_stmt ≝
[1292]1074  λglobals: list ident.
[1281]1075  λlenv: local_env.
[1066]1076  λlbl: label.
1077  λstmt.
[1292]1078  λdef: rtl_internal_function globals.
[1066]1079  match stmt with
[1282]1080  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
[1293]1081  | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
[1066]1082  | St_const destr cst lbl' ⇒
[1293]1083    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
[1066]1084  | St_op1 op1 destr srcr lbl' ⇒
[1293]1085    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
[1066]1086  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
[1306]1087    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
[1307]1088    (* XXX: should we be ignoring this? *)
[1066]1089  | St_load ignore addr destr lbl' ⇒
[1306]1090    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
[1307]1091    (* XXX: should we be ignoring this? *)
[1066]1092  | St_store ignore addr srcr lbl' ⇒
[1306]1093    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
[1066]1094  | St_call_id f args retr lbl' ⇒
1095    match retr with
1096    [ Some retr ⇒
[1293]1097      add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def
1098    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def
[1066]1099    ]
1100  | St_call_ptr f args retr lbl' ⇒
1101    match retr with
1102    [ None ⇒
1103      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
[1293]1104        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
[1066]1105    | Some retr ⇒
1106      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
[1293]1107        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def
[1066]1108    ]
1109  | St_tailcall_id f args ⇒
[1293]1110    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def
[1066]1111  | St_tailcall_ptr f args ⇒
1112    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
[1293]1113      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def
[1066]1114  | St_cond r lbl_true lbl_false ⇒
[1292]1115    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
[1066]1116  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
[1292]1117  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
[1064]1118  ].
[1067]1119  [10: cases not_implemented (* jtable case *)
1120  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
1121  ]
1122qed.
[1064]1123
[1073]1124(* XXX: we use a "hack" here to circumvent the proof obligations required to
1125   create res, an empty internal_function record.  we insert into our graph
1126   the start and end nodes to ensure that they are in, and place dummy
1127   skip instructions at these nodes. *)
[1067]1128definition translate_internal ≝
[1293]1129  λglobals: list ident.
1130  λdef.
[1067]1131  let runiverse ≝ f_reggen def in
[1281]1132  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
[1068]1133    (f_params def @ f_locals def) (f_result def) in
[1292]1134  let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
1135  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
[1149]1136  let result ≝
[1068]1137    match (f_result def) with
1138    [ None ⇒ [ ]
1139    | Some r_typ ⇒
1140      let 〈r, typ〉 ≝ r_typ in
1141        find_local_env r lenv
[1053]1142    ]
[1068]1143  in
1144  let luniverse' ≝ f_labgen def in
1145  let runiverse' ≝ runiverse in
1146  let result' ≝ result in
1147  let params' ≝ params in
1148  let locals' ≝ locals in
1149  let stack_size' ≝ f_stacksize def in
1150  let entry' ≝ f_entry def in
1151  let exit' ≝ f_exit def in
[1293]1152  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in
1153  let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in
[1068]1154  let res ≝
[1281]1155    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
1156     locals' stack_size' graph' ? ? in
[1293]1157    foldi … (translate_stmt globals … lenv) (f_graph def) res.
[1281]1158[ % [@entry' | @graph_add_lookup @graph_add]
1159| % [@exit'  | @graph_add]]
[1073]1160qed.
[1053]1161
[1239]1162(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1163  because of CompCert heritage *)
[1293]1164definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
1165 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracBrowser for help on using the repository browser.