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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.