Ignore:
Timestamp:
Dec 6, 2011, 5:04:13 PM (9 years ago)
Author:
tranquil
Message:
  • turned to argument-less return statements for RTLabs and RTL (there was a hidden invariant, for which the arguments of return statements where equal to the f_result field of the function definition: they were useless and an optimization was breaking the compilation)
  • corrected a bug in liveness analysis I had introduced
Location:
Deliverables/D2.2/8051/src/ERTL
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r1572 r1589  
    173173
    174174  (* Transfer control to the address stored in the return address registers. *)
    175   | St_return of argument list
     175  | St_return
    176176
    177177type graph = statement Label.Map.t
  • Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

    r1572 r1589  
    436436
    437437let compute_result st ret_regs =
    438   let vs = List.map (fun r -> get_arg r st) ret_regs in
     438  let vs = List.map (fun r -> get_reg (Hdw r) st) ret_regs in
    439439  let f res v = res && (Val.is_int v) in
    440440  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
     
    452452  if debug then print_state lbls_offs st ;
    453453  match fetch_stmt lbls_offs st with
    454     | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
    455       print_and_return_result (compute_result st ret_regs, List.rev st.trace)
     454    | ERTL.St_return when Val.eq_address (get_ra st) st.exit ->
     455      print_and_return_result (compute_result st I8051.rets, List.rev st.trace)
    456456    | stmt ->
    457457      let st' = interpret_stmt lbls_offs st stmt in
  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r1580 r1589  
    144144    Printf.sprintf "branch %s <> 0 --> %s, %s"
    145145      (Register.print srcr) lbl_true lbl_false
    146   | ERTL.St_return ret_regs ->
    147     Printf.sprintf "return %s" (print_return ret_regs)
     146  | ERTL.St_return ->
     147    Printf.sprintf "return"
    148148
    149149
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml

    r1585 r1589  
    104104        match Liveness.eliminable (G.liveafter label) stmt with
    105105        | Some successor ->
    106           Printf.printf "dead %s!\n%!" (ERTLPrinter.print_statement stmt);
    107106          LTL.St_skip successor
    108107        | None ->
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r1572 r1589  
    5252  let move_sp_to_dptr off l =
    5353    let off = adjust off in
    54     let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    55     let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
    56     let l = generate (LTL.St_int (I8051.a, 0, l)) in
    57     let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    58     let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
    59     LTL.St_int (I8051.a, off, l)
     54    if off = 0 then
     55      let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     56      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
     57      let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     58      LTL.St_to_acc (I8051.spl, l)
     59    else
     60      let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     61      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
     62      let l = generate (LTL.St_int (I8051.a, 0, l)) in
     63      let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     64      let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
     65      LTL.St_int (I8051.a, off, l)
    6066
    6167
     
    7379    move_sp_to_dptr off l
    7480
    75   (* side-effects : dpl, dph, sst *)
     81  (* side-effects : dpl, dph, st0 *)
    7682  let set_stack_a off l =
    77     let l = generate (LTL.St_store l) in
    78     let l = generate (set_stack_not_a off I8051.sst l) in
     83    let l = generate (set_stack_not_a off I8051.st0 l) in
    7984    LTL.St_from_acc (I8051.st0, l)
    8085
     
    99104  (* side-effects : none if dest = src, a if both colored,
    100105                    (dpl, dph, a) if src spilled or src imm and dest spilled,
    101                     (dpl, dph, a, sst) if dest spilled *)
     106                    (dpl, dph, a, st0) if dest spilled *)
    102107  let move (dest : decision) (src : argument) l =
    103108    match dest, src with
  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r1585 r1589  
    55(* In the following, a ``variable'' means a pseudo-register or an
    66   allocatable hardware register. *)
    7 
    8 (* These functions allow turning an [ERTL] control flow graph into an
    9    explicit graph, that is, making successor edges explicit. This is
    10    useful in itself and facilitates the computation of predecessor
    11    edges. *)
    12 
    13 let statement_successors (stmt : statement) =
    14   match stmt with
    15   | St_return _ ->
    16     Label.Set.empty
    17   | St_skip l
    18   | St_comment (_, l)
    19   | St_cost (_, l)
    20   | St_ind_0 (_, l)
    21   | St_ind_inc (_, l)
    22   | St_set_hdw (_, _, l)
    23   | St_get_hdw (_, _, l)
    24   | St_hdw_to_hdw (_, _, l)
    25   | St_newframe l
    26   | St_delframe l
    27   | St_framesize (_, l)
    28   | St_push (_, l)
    29   | St_pop (_, l)
    30   | St_addrH (_, _, l)
    31   | St_addrL (_, _, l)
    32   (* | St_int (_, _, l) *)
    33   | St_move (_, _, l)
    34   | St_opaccsA (_, _, _, _, l)
    35   | St_opaccsB (_, _, _, _, l)
    36   | St_op1 (_, _, _, l)
    37   | St_op2 (_, _, _, _, l)
    38   | St_clear_carry l
    39   | St_set_carry l
    40   | St_load (_, _, _, l)
    41   | St_store (_, _, _, l)
    42   | St_call_id (_, _, l)
    43   | St_call_ptr (_, _, _, l) ->
    44     Label.Set.singleton l
    45   | St_cond (_, l1, l2) ->
    46     Label.Set.add l1 (Label.Set.singleton l2)
    477
    488(* The analysis uses the lattice of sets of variables. The lattice's
     
    9959  | St_store _
    10060  | St_cond _
    101   | St_return _ ->
     61  | St_return ->
    10262    L.bottom
    10363  | St_clear_carry _
     
    191151  | St_delframe _ ->
    192152    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
    193   | St_return _ ->
     153  | St_return ->
    194154    Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
    195155
     
    207167
    208168let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
    209   let res =
    210169  match stmt with
    211170  | St_skip _
     
    224183  | St_call_ptr _
    225184  | St_cond _
    226   | St_return _ ->
     185  | St_return ->
    227186    None
    228187  | St_get_hdw (r, _, l)
     
    241200  | St_set_hdw (r, _, l)
    242201  | St_hdw_to_hdw (r, _, l) ->
    243     if I8051.RegisterSet.mem r hliveafter then None else Some l in
    244   Printf.printf "%s %sfound eliminable\n"
    245     (ERTLPrinter.print_statement stmt)
    246     (match res with
    247       | Some _ -> ""
    248       | _ -> "not "); res
     202    if I8051.RegisterSet.mem r hliveafter then None else Some l
    249203
    250204(* This is the abstract semantics of instructions. It defines the
     
    312266  let liveafter label (liveafter : valuation) : L.t =
    313267    let stmt : statement = Label.Map.find label int_fun.f_graph in
    314     Label.Set.fold (fun successor accu ->
     268    List.fold_right (fun successor accu ->
    315269      L.join (livebefore successor liveafter) accu
    316     ) (statement_successors stmt) L.bottom
     270    ) (ERTLGraph.successors stmt) L.bottom
    317271  in
    318272
     
    320274
    321275  F.lfp liveafter
     276
     277(* let print_prop ((reg_s, hdw_s) : L.property) : string = *)
     278(*   let fp pr s = Printf.sprintf "%s%s, " s *)
     279(*     (Register.print pr) in *)
     280(*   let fh hr s = Printf.sprintf "%s%s, " s *)
     281(*     (I8051.print_register hr) in *)
     282(*   Printf.sprintf "{ %s%s}\n" *)
     283(*     (Register.Set.fold fp reg_s "") *)
     284(*     (I8051.RegisterSet.fold fh hdw_s "") *)
     285
     286(* let print (def : internal_function) (valu : valuation) : string = *)
     287(*   let f lbl stmt s = match stmt with *)
     288(*     | St_skip _ -> s *)
     289(*     | _ ->  Printf.sprintf "%s%s : %s\n" s lbl *)
     290(*       (print_prop (valu lbl)) in *)
     291(*   Label.Map.fold f def.f_graph "" *)
  • Deliverables/D2.2/8051/src/ERTL/liveness.mli

    r486 r1589  
    4949
    5050val eliminable: L.t -> statement -> Label.t option
    51 
Note: See TracChangeset for help on using the changeset viewer.