Ignore:
Timestamp:
Dec 6, 2011, 5:04:13 PM (10 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
Files:
23 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/src/ASM/I8051.ml

    r1568 r1589  
    162162  | 130 -> "DPL"
    163163  | 131 -> "DPH"
     164  | -1 -> "carry bit"
    164165  | _ -> assert false (* impossible *)
    165166

  • 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 

  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r1585 r1589  
    4747let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
    4848let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
    49 let forget_ind st =   Printf.printf "forgetting\n";
    50 { st with inds = CostLabel.forget_const_ind st.inds }
     49let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
    5150let enter_loop st = CostLabel.enter_loop st.inds
    5251let continue_loop st = CostLabel.continue_loop st.inds
    … …  
    102101  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
    103102
    104 let init_fun_call name lbls_offs st ptr def =
     103let init_fun_call lbls_offs st ptr def =
    105104  let pc = entry_pc lbls_offs ptr def in
    106105  let st = new_ind st in
    107   Printf.printf "calling %s\n" name;
    108106  change_pc st pc
    109107
    … …  
    149147
    150148let label_of_pointer lbls_offs ptr =
    151 (*
    152   Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
    153 *)
    154149  let off = Val.offset_of_address ptr in
    155150  Labels_Offsets.find2 off lbls_offs
    … …  
    211206  change_pc st next_pc
    212207
    213 let interpret_call name lbls_offs st ptr ra =
     208let interpret_call lbls_offs st ptr ra =
    214209  match Mem.find_fun_def st.mem ptr with
    215210    | LTL.F_int def ->
    216211      let st = save_ra lbls_offs st ra in
    217       init_fun_call name lbls_offs st ptr def
     212      init_fun_call lbls_offs st ptr def
    218213    | LTL.F_ext def ->
    219214      let next_pc =
    … …  
    222217
    223218let interpret_return lbls_offs st =
    224   Printf.printf "returning\n";
    225219  let st = forget_ind st in
    226220  let (st, pc) = return_pc st in
    … …  
    328322
    329323    | LTL.St_call_id (f, lbl) ->
    330       interpret_call f lbls_offs st (Mem.find_global st.mem f) lbl
     324      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
    331325
    332326    | LTL.St_call_ptr lbl ->
    333       interpret_call (Val.string_of_address (dptr st)) lbls_offs st (dptr st) lbl
     327      interpret_call lbls_offs st (dptr st) lbl
    334328
    335329    | LTL.St_condacc (lbl_true, lbl_false) ->
    … …  
    362356    (res, cost_labels) in
    363357  if debug then print_state lbls_offs st ;
    364   Printf.printf "%s\n" (Val.string_of_address st.pc);
    365358  match fetch_stmt lbls_offs st with
    366359    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
    … …  
    411404  match Mem.find_fun_def st.mem ptr with
    412405    | LTL.F_int def ->
    413       init_fun_call main lbls_offs st ptr def
     406      init_fun_call lbls_offs st ptr def
    414407    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    415408

  • Deliverables/D2.2/8051/src/RTL/RTL.mli

    r1572 r1589  
    102102  | St_cond of Register.t * Label.t * Label.t
    103103
    104   (* Return the value of some registers (low bytes first). *)
    105   | St_return of argument list
     104  (* Return control. *)
     105  | St_return
    106106
    107107

  • Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml

    r1585 r1589  
    415415    | St_opaccs (op, i, j, a, b, l) ->
    416416      (simpl_imm_opaccs op i j a b (valu p) l, None)
     417    | St_set_carry l when L.find_cst_carry_in (valu p) = Some 1 -> ([], None)
     418    | St_clear_carry l when L.find_cst_carry_in (valu p) = Some 0 -> ([], None)
    417419    | St_load (i, a, b, l) ->
    418420      ([St_load(i, arg_from_arg (valu p) a, arg_from_arg (valu p) b, l)], None)
    … …  
    426428        | Some _ -> ([], Some [if_true])
    427429        | None -> ([s], Some [if_true ; if_false]))
    428     | St_return rets ->
    429       let rets' = List.map (arg_from_arg (valu p)) rets in
    430       ([St_return rets'], None)
    431430    | St_call_id (f, args, rets, l) ->
    432431      let args' = List.map (arg_from_arg (valu p)) args in

  • Deliverables/D2.2/8051/src/RTL/RTLGraph.ml

    r1580 r1589  
    6262  | St_tailcall_id (f, args), [] -> St_tailcall_id (f, args)
    6363  | St_tailcall_ptr (f1, f2, args), [] -> St_tailcall_ptr (f1, f2, args)
    64   | St_return regs, [] -> St_return regs
     64  | St_return, [] -> St_return
    6565  | _ -> invalid_arg "fill_succs: statement and successors do not match"

  • Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

    r1572 r1589  
    1919   being executed. *)
    2020
    21 type local_env = Val.t Register.Map.t
     21type local_env = {
     22  le_vals : Val.t Register.Map.t ;
     23  le_rets : Register.t list
     24}
    2225
    2326(* Call frames. The execution state has a call stack, each element of the stack
    … …  
    2730
    2831type stack_frame =
    29     { ret_regs : Register.t list ;
     32    { result  : Register.t list ;
    3033      graph    : RTL.graph ;
    3134      pc       : Label.t ;
    … …  
    5558      (if Val.eq v Val.undef then ""
    5659       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
    57   Register.Map.fold f lenv ""
     60  Register.Map.fold f lenv.le_vals ""
    5861
    5962let string_of_args args =
    … …  
    8790
    8891let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
    89   if Register.Map.mem r lenv then Register.Map.find r lenv
    90   else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
     92  try
     93    Register.Map.find r lenv.le_vals
     94  with
     95    | Not_found ->
     96      error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
     97
    9198
    9299let get_local_arg_value (lenv : local_env) : RTL.argument -> Val.t = function
    … …  
    108115
    109116let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs =
    110   let lenv = adds destrs vs lenv in
     117  let lenv = { lenv with le_vals = adds destrs vs lenv.le_vals } in
    111118  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    112119
    … …  
    210217        let args = get_arg_values lenv args in
    211218        let sf =
    212           { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
     219          { result = ret_regs ; graph = graph ; pc = lbl ;
    213220            sp = sp ; lenv = lenv ; carry = carry }
    214221        in
    … …  
    219226        let f_def = Mem.find_fun_def mem addr in
    220227        let args = get_arg_values lenv args in
    221         let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
     228        let sf = { result = ret_regs ; graph = graph ; pc = lbl ;
    222229                   sp = sp ; lenv = lenv ; carry = carry } in
    223230        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    … …  
    240247        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
    241248
    242       | RTL.St_return rl ->
    243         let vl = List.map (get_local_arg_value lenv) rl in
     249      | RTL.St_return ->
     250        let vl = List.map (get_local_value lenv) lenv.le_rets in
    244251        let mem = Mem.free mem sp in
    245252        ReturnState (sfrs, vl, mem, inds, trace)
    … …  
    255262    (locals : Register.Set.t)
    256263    (params : Register.t list)
     264    (rets   : Register.t list)
    257265    (args   : Val.t list) :
    258266    local_env =
    259   let f r lenv = Register.Map.add r Val.undef lenv in
    260   let lenv = Register.Set.fold f locals Register.Map.empty in
    261   let f lenv r v = Register.Map.add r v lenv in
    262   List.fold_left2 f lenv params args
     267  let f r lenv_vals = Register.Map.add r Val.undef lenv_vals in
     268  let lenv_vals = Register.Set.fold f locals Register.Map.empty in
     269  let f lenv_vals r v = Register.Map.add r v lenv_vals in
     270  { le_vals = List.fold_left2 f lenv_vals params args ; le_rets = rets }
    263271
    264272let state_after_call
    … …  
    274282      let inds = new_ind inds in
    275283      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
     284      let lenv =
     285        init_locals def.RTL.f_locals def.RTL.f_params def.RTL.f_result args in
    276286      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    277              init_locals def.RTL.f_locals def.RTL.f_params args,
     287             lenv,
    278288             Val.undef, mem', inds, trace)
    279289    | RTL.F_ext def ->
    … …  
    289299    (trace    : CostLabel.t list) :
    290300    state =
    291   let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    292   let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
     301  let f i lenv_vals r = Register.Map.add r (List.nth ret_vals i) lenv_vals in
     302  let lenv =
     303    {sf.lenv with
     304      le_vals = MiscPottier.foldi f sf.lenv.le_vals sf.result } in
    293305  let inds = forget_ind inds in
    294306  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)

  • Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

    r1580 r1589  
    125125    Printf.sprintf "branch %s <> 0 --> %s, %s"
    126126      (print_reg srcr) lbl_true lbl_false
    127   | RTL.St_return regs ->
    128     Printf.sprintf "return %s" (print_return regs)
     127  | RTL.St_return ->
     128    Printf.sprintf "return"
    129129
    130130
    … …  
    143143
    144144  Printf.sprintf
    145     "%s\"%s\"%s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
     145    "%s\"%s\"%s\n%slocals: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
    146146    (n_spaces n)
    147147    f
    … …  
    149149    (n_spaces (n+2))
    150150    (print_locals def.RTL.f_locals)
    151     (n_spaces (n+2))
    152     (print_result def.RTL.f_result)
     151    (* (n_spaces (n+2)) *)
     152    (* (print_result def.RTL.f_result) *)
    153153    (n_spaces (n+2))
    154154    def.RTL.f_stacksize

  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r1584 r1589  
    350350    add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def
    351351
    352   | RTL.St_return ret_regs ->
    353     add_graph lbl (ERTL.St_return ret_regs) def
     352  | RTL.St_return ->
     353    add_graph lbl (ERTL.St_return) def
    354354
    355355  | RTL.St_tailcall_id _ | RTL.St_tailcall_ptr _ ->

  • Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

    r1572 r1589  
    9696
    9797  (* Return statement. *)
    98   | St_return of argument option
     98  | St_return
    9999
    100100

  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r1572 r1589  
    1919   function being executed. *)
    2020
    21 type local_env = (Val.t * AST.sig_type) Register.Map.t
     21type local_env = {
     22  le_vals : (Val.t * AST.sig_type) Register.Map.t ;
     23  le_ret : Register.t option
     24}
    2225
    2326(* Call frames. The execution state has a call stack, each element of the stack
    … …  
    2730
    2831type stack_frame =
    29     { ret_reg  : Register.t option ;
     32    { result   : Register.t option ;
    3033      graph    : RTLabs.graph ;
    3134      sp       : Val.address ;
    … …  
    5356      (if Val.eq v Val.undef then ""
    5457       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
    55   Register.Map.fold f lenv ""
     58  Register.Map.fold f lenv.le_vals ""
    5659
    5760let string_of_args args =
    … …  
    8487
    8588let get_local_env f lenv r =
    86   if Register.Map.mem r lenv then f (Register.Map.find r lenv)
    87   else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
     89  let a = try Register.Map.find r lenv.le_vals with
     90    | Not_found ->
     91      error ("Unknown local register \"" ^ (Register.print r) ^ "\".") in
     92  f a
    8893
    8994let get_value = get_local_env fst
    … …  
    9297
    9398let update_local r v lenv =
    94   let f (_, t) = Register.Map.add r (v, t) lenv in
    95   get_local_env f lenv r
     99  let f (_, t) = Register.Map.add r (v, t) lenv.le_vals in
     100  { lenv with le_vals = get_local_env f lenv r }
    96101
    97102let update_locals rs vs lenv =
    … …  
    209214        (* Save the stack frame. *)
    210215        let sf =
    211           { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
     216          { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    212217        in
    213218        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    … …  
    219224        (* Save the stack frame. *)
    220225        let sf =
    221           { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
     226          { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    222227        in
    223228        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    … …  
    275280      *)
    276281
    277       | RTLabs.St_return None ->
     282      | RTLabs.St_return ->
    278283        let mem = Mem.free mem sp in
    279         ReturnState (sfrs, Val.undef, mem, inds, trace)
    280 
    281       | RTLabs.St_return (Some r) ->
    282         let v = eval_arg lenv mem sp r in
    283         let mem = Mem.free mem sp in
    284         ReturnState (sfrs, v, mem, inds, trace)
    285 
     284        let res =  match lenv.le_ret with
     285          | None -> Val.undef
     286          | Some r -> get_value lenv r in
     287        ReturnState (sfrs, res, mem, inds, trace)
    286288
    287289module InterpretExternal = Primitive.Interpret (Mem)
    … …  
    297299    (locals           : (Register.t * AST.sig_type) list)
    298300    (params           : (Register.t * AST.sig_type) list)
     301    (ret              : (Register.t * AST.sig_type) option)
    299302    (args             : Val.t list) :
    300303    local_env =
    301304  let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in
    302305  let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in
    303   let lenv = List.fold_left2 f_param Register.Map.empty params args in
    304   List.fold_left f_local lenv locals
     306  let lenv_vals = List.fold_left2 f_param Register.Map.empty params args in
     307  let ret = Option.map fst ret in
     308  { le_vals = List.fold_left f_local lenv_vals locals; le_ret = ret }
    305309
    306310let state_after_call
    … …  
    316320      let (mem', sp) =
    317321        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
    318       let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
     322      let lenv = init_locals
     323        def.RTLabs.f_locals
     324        def.RTLabs.f_params
     325        def.RTLabs.f_result
     326        args in
     327      let graph = def.RTLabs.f_graph in
    319328      (* allocate new constant indexing *)
    320       let graph = def.RTLabs.f_graph in
    321329      let inds = new_ind inds in
    322330      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
    … …  
    334342    (trace   : CostLabel.t list) :
    335343    state =
    336   let lenv = match sf.ret_reg with
     344  let lenv = match sf.result with
    337345    | None -> sf.lenv
    338346    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
    339       (* erase current indexing and revert to previous one *)
    340       let inds = forget_ind inds in
    341       State (sfrs, sf.graph, sf.sp, sf.pc, lenv,
    342              mem, inds, trace)
     347  (* erase current indexing and revert to previous one *)
     348  let inds = forget_ind inds in
     349  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, trace)
    343350
    344351

  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r1580 r1589  
    245245        (print_reg r)
    246246        (print_table tbl)
    247   | RTLabs.St_return None -> Printf.sprintf "return"
    248   | RTLabs.St_return (Some r) -> Printf.sprintf "return %s" (print_arg r)
     247  | RTLabs.St_return -> Printf.sprintf "return"
    249248
    250249

  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1585 r1589  
    1111let error_shift () = error "Shift operations not supported."
    1212
     13let dummy = Label.dummy
    1314
    1415let add_graph lbl stmt def =
    … …  
    174175  translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def
    175176
    176 let translate_cast_signed destrs srcr start_lbl dest_lbl def =
    177   let (def, tmpr) = fresh_reg def in
    178   let insts =
     177let sign_mask destr srcr =
    179178    (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that:
    180179       byte in tmpr if srcr is: neg   |  pos
    … …  
    185184
    186185     *)
    187     [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ;
    188      RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ;
    189      RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ;
    190      RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in
     186  [RTL.St_op2 (I8051.Or, destr, srcr, RTL.Imm 127, dummy) ;
     187   RTL.St_op1 (I8051.Rl, destr, destr, dummy) ;
     188   RTL.St_op1 (I8051.Inc, destr, destr, dummy) ;
     189   RTL.St_op1 (I8051.Cmpl, destr, destr, dummy) ]
     190
     191
     192let translate_cast_signed destrs srcr start_lbl dest_lbl def =
     193  let (def, tmpr) = fresh_reg def in
    191194  let srcrs = MiscPottier.make (RTL.Reg tmpr) (List.length destrs) in
    192   add_translates [adds_graph insts ; translate_move destrs srcrs]
     195  add_translates [adds_graph (sign_mask tmpr srcr); translate_move destrs srcrs]
    193196    start_lbl dest_lbl def
    194197
    … …  
    477480
    478481    | AST.Op_add | AST.Op_addp ->
    479       translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     482      translate_op I8051.Add destrs srcrs1 srcrs2 start_lbl dest_lbl def
    480483
    481484    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
    … …  
    666669    error "Jump tables not supported yet."
    667670
    668   | RTLabs.St_return None ->
    669     add_graph lbl (RTL.St_return []) def
    670 
    671   | RTLabs.St_return (Some r) ->
    672     add_graph lbl (RTL.St_return (find_local_env r lenv)) def
     671  | RTLabs.St_return ->
     672    add_graph lbl RTL.St_return def
     673
     674open BList.Notation
    673675
    674676open BList.Notation
    … …  
    708710      load_args args (fun args ->
    709711        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
    710     | RTLabs.St_return (Some a) ->
    711       load_arg a (fun a ->
    712         RTLabs.St_return (Some a) ^:: bnil)
    713712    | stmt -> stmt ^:: bnil in
    714713  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in

  • Deliverables/D2.2/8051/src/RTLabs/constPropagation.ml

    r1580 r1589  
    332332        | L.V _ | L.A _ -> ([], Some [if_true])
    333333        | _ -> ([s], Some [if_true ; if_false]))
    334     | St_return (Some a) ->
    335       ([St_return (Some (arg_from_arg (valu p) types a))], None)
    336334    | St_call_id (f, args, ret, sg, l) ->
    337335      ([St_call_id (f, args_from_args (valu p) types args, ret, sg, l)], None)

  • Deliverables/D2.2/8051/src/RTLabs/copyPropagation.ml

    r1580 r1589  
    107107    | St_call_ptr (f, args, ret, sign, l) ->
    108108      St_call_ptr (f, List.map copy_of_arg args, ret, sign, l)
    109     | St_return (Some a) -> St_return (Some (copy_of_arg a))
    110109    | stmt -> stmt
    111110

  • Deliverables/D2.2/8051/src/RTLabs/redundancyElimination.ml

    r1580 r1589  
    118118
    119119(* used in possibly non side-effect-free statements *)
    120 let used_at_stmt stmt =
     120let used_at_stmt ret stmt =
    121121  let add_arg s = function
    122122    | Reg r -> Register.Set.add r s
    … …  
    130130    | St_store (_, a, b, _) ->
    131131      add_arg (add_arg Register.Set.empty a) b
    132     | St_return (Some (Reg r))
    133132    | St_cond (r, _, _) -> Register.Set.singleton r
     133    | St_return ->
     134      begin match ret with
     135        | Some (r, _) -> Register.Set.singleton r
     136        | None ->  Register.Set.empty
     137      end
    134138    | _ -> Register.Set.empty
    135139
    136 let used_at g n = used_at_stmt (Label.Map.find n g)
     140let used_at ret g n = used_at_stmt ret (Label.Map.find n g)
    137141
    138142module ExprOrdered = struct
    … …  
    378382    (g : graph)
    379383    (type_of : Register.t -> AST.sig_type)
     384    (ret : (Register.t * AST.sig_type) option)
    380385    (late : Fsing.valuation)
    381386    (lbl : Label.t)
    … …  
    394399        Register.Set.union (Register.Set.remove r used_out) (vars_of g l)
    395400      | _ -> used_out in
    396     Register.Set.union used_out (used_at g l) in
     401    Register.Set.union used_out (used_at ret g l) in
    397402  let used = big_union f succs in
    398403
    … …  
    406411
    407412  let graph = f_def.f_graph in
     413  let ret = f_def.f_result in
    408414
    409415  Fexprid.lfp
    410     (semantics_isolated_used graph type_of (late graph type_of delayed))
     416    (semantics_isolated_used graph type_of ret (late graph type_of delayed))
    411417
    412418(* expressions that are optimally placed at point p, without being isolated *)

  • Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml

    r1572 r1589  
    445445  let exit = Label.Gen.fresh luniverse in
    446446
    447   (* The control flow graph: for now, it is only a return instruction at the
    448      end. *)
    449   let return = match result with
    450     | None -> None
    451     | Some (retr, _) -> Some (RTLabs.Reg retr) in
    452   let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in
     447  let graph = Label.Map.add exit RTLabs.St_return Label.Map.empty in
    453448
    454449  let rtlabs_fun =
Note: See TracChangeset for help on using the changeset viewer.