source: src/RTLabs/RTLabsToRTL.ma @ 2226

Last change on this file since 2226 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

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