Changeset 1059 for src/RTLabs


Ignore:
Timestamp:
Jul 6, 2011, 6:09:39 PM (8 years ago)
Author:
mulligan
Message:

work from today, bit of a mess at the moment

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1057 r1059  
    44include "common/Graphs.ma".
    55include "common/Maps.ma".
    6 include "common/IntValue.ma".
     6(* include "common/IntValue.ma". *)
     7include "common/FrontEndOps.ma".
    78
    89definition add_graph ≝
     
    280281    rtl_st_int r i dest_lbl.
    281282
    282 definition translate_cst ≝
    283   λcst.
    284   λdestrs.
    285   λstart_lbl.
    286   λdest_lbl.
    287   λdef.
    288   match cst with
    289   [ cast_int i ⇒
    290     match destrs with
    291     [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
    292     | _ ⇒
    293       (* this case needs changing when Z is added to stdlib as we are using
    294          nats instead of ints here! *)
    295       let size ≝ length ? destrs in
    296       let is ≝ map … (to_int size) (break size (of_int size (nat_of_bitvector ? i)) size) in
    297       let is' ≝ map … (bitvector_of_nat ?) is in
    298       let l ≝ map2 … (translate_cst_int_internal dest_lbl) destrs is' ? in
    299         adds_graph l start_lbl dest_lbl def
    300     ]
    301   | cast_addrsymbol id ⇒
    302     let 〈r1, r2〉 ≝ make_addr ? destrs ? in
    303       add_graph start_lbl (rtl_st_addr r1 r2 id dest_lbl) def
    304   | _ ⇒ ?
    305   ].
    306   | cast_addrsymbol id ⇒
    307     match destrs with
    308     [ nil ⇒ None ?
    309     | cons hd tl ⇒
    310       match tl with
    311       [ nil ⇒ None ?
    312       | cons hd' tl' ⇒
    313         Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
    314       ]
    315     ]
    316   | cast_offset off ⇒
    317     match destrs with
    318     [ nil ⇒ None ?
    319     | cons hd tl ⇒
    320       match tl with
    321       [ nil ⇒ None ?
    322       | cons hd' tl' ⇒
    323         let 〈def, tmpr〉 ≝ fresh_reg def in
    324         adds_graph [
    325           rtl_st_stack_addr hd hd' start_lbl;
    326           rtl_st_int tmpr off start_lbl;
    327           rtl_st_op2 Add hd hd tmpr start_lbl;
    328           rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
    329           rtl_st_op2 Addc hd' hd' tmpr start_lbl
    330         ] start_lbl dest_lbl def
    331       ]
    332     ]
    333   | cast_stack ⇒ ?
    334   | cast_sizeof size ⇒ ?
    335   (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
    336   ].
    337 
    338 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
    339 
    340   | AST.Cst_stack ->
    341     let (r1, r2) = make_addr destrs in
    342     add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
    343 
    344   | AST.Cst_offset off ->
    345     let i = concrete_offset off in
    346     translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
    347 
    348   | AST.Cst_sizeof size ->
    349     let i = concrete_size size in
    350     translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
     283axiom translate_cst:
     284  ∀cst: constant.
     285  ∀destrs: list register.
     286  ∀start_lbl: label.
     287  ∀dest_lbl: label.
     288  ∀def: rtl_internal_function.
     289    rtl_internal_function.
     290
     291definition translate_move_internal ≝
     292  λstart_lbl: label.
     293  λdestr: register.
     294  λsrcr: register.
     295    rtl_st_move destr srcr start_lbl.
     296
     297definition translate_move ≝
     298  λdestrs: list register.
     299  λsrcrs: list register.
     300  λstart_lbl: label.
     301  λprf: | destrs | = | srcrs |.
     302    let 〈crl, crr〉 ≝ reduce register destrs srcrs in
     303    let 〈commonl, restl〉 ≝ crl in
     304    let 〈commonr, restr〉 ≝ crr in
     305    let f_common ≝ translate_move_internal start_lbl in
     306    let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
     307    let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     308      add_translates [ translate1 ; translate2 ] start_lbl.
     309   
     310let rec translate_move destrs srcrs start_lbl =
     311  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
     312  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
     313  let translates1 = adds_graph (List.map2 f_common common1 common2) in
     314  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
     315  add_translates [translates1 ; translates2] start_lbl
    351316
    352317definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.