Ignore:
Timestamp:
Dec 2, 2011, 3:13:04 PM (8 years ago)
Author:
tranquil
Message:
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1580 r1584  
    115115
    116116let change_label lbl = function
    117   | RTL.St_skip _ -> RTL.St_skip lbl
    118   | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
    119   | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl)
    120   | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl)
    121   | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
    122   | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
    123   (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *)
    124   | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
    125   | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
    126     RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
    127   | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
    128   | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
    129     RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
    130   | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
    131   | RTL.St_set_carry _ -> RTL.St_set_carry lbl
    132   | RTL.St_load (dstrs, addr1, addr2, _) ->
    133     RTL.St_load (dstrs, addr1, addr2, lbl)
    134   | RTL.St_store (addr1, addr2, srcrs, _) ->
    135     RTL.St_store (addr1, addr2, srcrs, lbl)
    136   | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
    137   | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
    138     RTL.St_call_ptr (f1, f2, args, retrs, lbl)
    139   | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
    140   | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
    141   | RTL.St_cond _ as inst -> inst
    142   | RTL.St_return regs -> RTL.St_return regs
     117  | (RTL.St_cond _ | RTL.St_return _) as inst -> inst
     118  | stmt -> RTLGraph.fill_succs stmt [lbl]
    143119
    144120(* Add a list of instruction in a graph, from one label to another, by creating
     
    308284  let (def, tmpr) = fresh_reg def in
    309285  let carry_init = match op with
    310     | I8051.Addc | I8051.Sub ->
     286    | I8051.Sub | I8051.Addc ->
    311287      (* depend on carry bit *)
    312288      [RTL.St_clear_carry start_lbl]
    313     | I8051.Add -> assert false (* should not call with add, not correct *)
    314289    | _ -> [] in
    315   let f_add destr srcr1 srcr2 =
     290  let f_add op destr srcr1 srcr2 =
    316291    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
    317292  let insts_add =
    318     MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
     293    match op with
     294      | I8051.Add ->
     295        (* we perform a first add followed by Addc's *)
     296        let f destr srcr1 srcr2 (op, insts) =
     297          (I8051.Addc, f_add op destr srcr1 srcr2 :: insts) in
     298        snd (MiscPottier.fold3_right
     299          f destrs_common srcrs1_common srcrs2_common (I8051.Add, []))
     300      | _ ->
     301        (* we just do the same operation on all *)
     302        MiscPottier.map3 (f_add op) destrs_common srcrs1_common srcrs2_common in
    319303  let f_add_cted destr srcr =
    320304    RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in
     
    331315    start_lbl dest_lbl def
    332316
    333 
    334 let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
    335   match destrs, srcrs1 with
    336     | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
    337     | [destr], [] ->
    338       adds_graph
    339         [RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl)]
    340         start_lbl
    341     | destr1 :: destr2 :: destrs, [] ->
    342       add_translates
    343         [adds_graph
    344             [RTL.St_op2 (I8051.Addc, destr1,
    345                          RTL.Reg destr1, RTL.Imm 0, start_lbl) ;
    346              RTL.St_op2 (I8051.Addc, destr2, RTL.Imm 0, RTL.Imm 0, start_lbl)] ;
    347          translate_cst (AST.Cst_int 0) destrs]
    348         start_lbl
    349     | [destr], srcr1 :: _ ->
    350       adds_graph
    351         [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
    352          RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Reg tmpr, start_lbl)]
    353         start_lbl
    354     | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
    355       add_translates
    356         [adds_graph
    357             [RTL.St_opaccs
    358                 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
    359              RTL.St_op2 (I8051.Addc, destr1, RTL.Reg destr1,
    360                          RTL.Reg tmpr, start_lbl)] ;
    361          translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
    362         start_lbl
    363 
    364 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
    365     srcr2i =
    366   let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
    367   translates @
    368     (match tmp_destrs2 with
    369       | [] -> []
    370       | tmp_destr2 :: tmp_destrs2 ->
    371         [adds_graph [RTL.St_clear_carry dummy_lbl ;
    372                      RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
    373          translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
    374          translate_cst (AST.Cst_int 0) tmp_destrs1 ;
    375          let reg_destrs = List.map (fun r -> RTL.Reg r) destrs in
    376          let tmp_destrs = List.map (fun r -> RTL.Reg r) tmp_destrs in
    377          translate_op I8051.Addc destrs reg_destrs tmp_destrs])
    378 
    379317let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    380   let (def, dummy) = fresh_reg def in
    381   let (def, tmpr) = fresh_reg def in
    382   let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
    383   let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
    384   (* let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in *)
    385   let reg r = RTL.Reg r in
    386   let insts_init =
    387     [translate_move fresh_srcrs1 srcrs1 ;
    388      (* translate_move fresh_srcrs2 srcrs2 ; *)
    389      translate_cst (AST.Cst_int 0) destrs] in
    390   let fresh_srcrs1 = List.map reg fresh_srcrs1 in
    391   let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
    392   let insts_mul = MiscPottier.foldi f [] srcrs2 in
    393   add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
    394 
     318  (* we save those parts of srcrs that could be overwritten *)
     319  let save_srcrs a (def, srcrs, init) = match a with
     320    | RTL.Reg r when List.mem r destrs ->
     321      let (def, new_r) = fresh_reg def in
     322      (def, RTL.Reg new_r :: srcrs,
     323       adds_graph [RTL.St_move (new_r, a, start_lbl)] :: init)
     324    | _ -> (def, a :: srcrs, init) in
     325  let (def, fresh_srcrs1, init) =
     326    List.fold_right save_srcrs srcrs1 (def, [], []) in
     327  let (def, fresh_srcrs2, init) =
     328    List.fold_right save_srcrs srcrs2 (def, [], init) in
     329  let srcrs1_n = List.length srcrs1 in
     330  let srcrs2_n = List.length srcrs2 in
     331  let destrs_n = List.length destrs in
     332  (* the next must be an invariant *)
     333  assert (srcrs1_n = destrs_n && destrs_n = srcrs1_n);
     334  (* we pad destrs with a copy of itself that will be added to it at the end
     335     (when the multiplication overflows) and then three more. The routine
     336     should thus handle overflow nicely, but it must be checked *)
     337  let all_destrs = MiscPottier.fill destrs (2 * destrs_n + 3) in
     338  let init = translate_cst (AST.Cst_int 0) destrs :: init in
     339  (* the registries to hold the temporary results of 8-bit mutliplication *)
     340  let (def, a) = fresh_reg def in
     341  let (def, b) = fresh_reg def in
     342  (* when getting the result, this is what is used (padded to 3 bytes *)
     343  let mul_arg = [RTL.Reg a ; RTL.Reg b ; RTL.Imm 0] in
     344  let mul i j =
     345    let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 i in
     346    let k = i + j in
     347    let dloc = MiscPottier.sublist all_destrs k (k+3) in
     348    let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in
     349    [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ;
     350      translate_op I8051.Add dloc dloc_arg mul_arg ] in
     351  let insts = List.flatten (List.flatten
     352    (MiscPottier.makei (fun i ->
     353      MiscPottier.makei (mul i) srcrs2_n) srcrs1_n)) in
     354  add_translates (init @ insts) start_lbl dest_lbl def
    395355
    396356let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
     
    457417    | [] -> adds_graph [] start_lbl dest_lbl def
    458418    | destr :: destrs ->
    459       (* not sure that it is the correct thing to do, what about signed?
    460          can really srcrs1 and srcrs2 be of different length? Are not all
    461          correct types enforced? *)
    462419      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
    463420      let init = RTL.St_clear_carry start_lbl in
     
    705662    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    706663
     664open BList.Notation
     665
    707666let remove_non_int_immediates def =
    708   let load_arg a lbl g rs = match a with
     667  let load_arg a f = match a with
    709668    | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) ->
    710       let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
    711       let new_r = Register.fresh def.RTLabs.f_runiverse in
    712       let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
    713       (new_l, g, (new_r, t) :: rs, RTLabs.Reg new_r)
    714     | _ -> (lbl, g, rs, a) in
    715   let load_args args lbl g rs =
    716     let f a (lbl', g', rs', args') =
    717       let (lbl'', g'', rs'', a') = load_arg a lbl' g' rs' in
    718       (lbl'', g'', rs'', a' :: args') in
    719     List.fold_right f args (lbl, g, rs, []) in
    720   let f lbl stmt (g, rs) =
    721     match stmt with
    722       | RTLabs.St_op2(op, r, a1, a2, l) ->
    723         let (lbl', g, rs, a1) = load_arg a1 lbl g rs in
    724         let (lbl', g, rs, a2) = load_arg a2 lbl' g rs in
    725         let s = RTLabs.St_op2 (op, r, a1, a2, l) in
    726         let g = Label.Map.add lbl' s g in
    727         (g, rs)
    728       | RTLabs.St_store(q, a1, a2, l) ->
    729         let (lbl', g, rs, a1) = load_arg a1 lbl g rs in
    730         let (lbl', g, rs, a2) = load_arg a2 lbl' g rs in
    731         let s = RTLabs.St_store (q, a1, a2, l) in
    732         let g = Label.Map.add lbl' s g in
    733         (g, rs)
    734       | RTLabs.St_load (q, a, r, l) ->
    735         let (lbl', g, rs, a) = load_arg a lbl g rs in
    736         let s = RTLabs.St_load (q, a, r, l) in
    737         let g = Label.Map.add lbl' s g in
    738         (g, rs)
    739       | RTLabs.St_call_id (f, args, ret, s, l) ->
    740         let (lbl', g, rs, args) = load_args args lbl g rs in
    741         let s = RTLabs.St_call_id (f, args, ret, s, l) in
    742         let g = Label.Map.add lbl' s g in
    743         (g, rs)
    744       | RTLabs.St_tailcall_id (f, args, s) ->
    745         let (lbl', g, rs, args) = load_args args lbl g rs in
    746         let s = RTLabs.St_tailcall_id (f, args, s) in
    747         let g = Label.Map.add lbl' s g in
    748         (g, rs)
    749       | RTLabs.St_call_ptr (f, args, ret, s, l) ->
    750         let (lbl', g, rs, args) = load_args args lbl g rs in
    751         let s = RTLabs.St_call_ptr (f, args, ret, s, l) in
    752         let g = Label.Map.add lbl' s g in
    753         (g, rs)
    754       | RTLabs.St_tailcall_ptr (f, args, s) ->
    755         let (lbl', g, rs, args) = load_args args lbl g rs in
    756         let s = RTLabs.St_tailcall_ptr (f, args, s) in
    757         let g = Label.Map.add lbl' s g in
    758         (g, rs)
    759       | RTLabs.St_return (Some a) ->
    760         let (lbl', g, rs, a) = load_arg a lbl g rs in
    761         let s = RTLabs.St_return (Some a) in
    762         let g = Label.Map.add lbl' s g in
    763         (g, rs)
    764       | _ -> (g, rs) in
     669      fresh_t t (fun tmp ->
     670      RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp))
     671    | _ -> f a in
     672  let rec load_args args f = match args with
     673    | [] -> f []
     674    | a :: args ->
     675      load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in
     676  let trans lbl = function
     677    | RTLabs.St_op2(op, r, a1, a2, l) ->
     678      load_arg a1 (fun a1 ->
     679        load_arg a2 (fun a2 ->
     680          RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil))
     681    | RTLabs.St_store(q, a1, a2, l) ->
     682      load_arg a1 (fun a1 ->
     683        load_arg a2 (fun a2 ->
     684          RTLabs.St_store (q, a1, a2, l) ^:: bnil))
     685    | RTLabs.St_load (q, a, r, l) ->
     686      load_arg a (fun a ->
     687        RTLabs.St_load (q, a, r, l) ^:: bnil)
     688    | RTLabs.St_call_id (f, args, ret, s, l) ->
     689      load_args args (fun args ->
     690        RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil)
     691    | RTLabs.St_tailcall_id (f, args, s) ->
     692      load_args args (fun args ->
     693        RTLabs.St_tailcall_id (f, args, s) ^:: bnil)
     694    | RTLabs.St_call_ptr (f, args, ret, s, l) ->
     695      load_args args (fun args ->
     696        RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil)
     697    | RTLabs.St_tailcall_ptr (f, args, s) ->
     698      load_args args (fun args ->
     699        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
     700    | RTLabs.St_return (Some a) ->
     701      load_arg a (fun a ->
     702        RTLabs.St_return (Some a) ^:: bnil)
     703    | stmt -> stmt ^:: bnil in
     704  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
    765705  let g = def.RTLabs.f_graph in
    766   let (g, rs) = Label.Map.fold f g (g, []) in
    767   let locals = List.rev_append rs def.RTLabs.f_locals in
    768   { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
     706  let fresh_reg def t =
     707    let r = Register.fresh def.RTLabs.f_runiverse in
     708    let locals = (r, t) :: def.RTLabs.f_locals in
     709    ({ def with RTLabs.f_locals = locals }, r) in
     710  let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in
     711  let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in
     712  { def with RTLabs.f_graph = g }
    769713 
    770714let translate_internal def =
Note: See TracChangeset for help on using the changeset viewer.