Changeset 1589 for Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
 Timestamp:
 Dec 6, 2011, 5:04:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r1572 r1589 19 19 being executed. *) 20 20 21 type local_env = Val.t Register.Map.t 21 type local_env = { 22 le_vals : Val.t Register.Map.t ; 23 le_rets : Register.t list 24 } 22 25 23 26 (* Call frames. The execution state has a call stack, each element of the stack … … 27 30 28 31 type stack_frame = 29 { re t_regs: Register.t list ;32 { result : Register.t list ; 30 33 graph : RTL.graph ; 31 34 pc : Label.t ; … … 55 58 (if Val.eq v Val.undef then "" 56 59 else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in 57 Register.Map.fold f lenv ""60 Register.Map.fold f lenv.le_vals "" 58 61 59 62 let string_of_args args = … … 87 90 88 91 let 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 91 98 92 99 let get_local_arg_value (lenv : local_env) : RTL.argument > Val.t = function … … 108 115 109 116 let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs = 110 let lenv = adds destrs vs lenvin117 let lenv = { lenv with le_vals = adds destrs vs lenv.le_vals } in 111 118 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 112 119 … … 210 217 let args = get_arg_values lenv args in 211 218 let sf = 212 { re t_regs= ret_regs ; graph = graph ; pc = lbl ;219 { result = ret_regs ; graph = graph ; pc = lbl ; 213 220 sp = sp ; lenv = lenv ; carry = carry } 214 221 in … … 219 226 let f_def = Mem.find_fun_def mem addr in 220 227 let args = get_arg_values lenv args in 221 let sf = { re t_regs= ret_regs ; graph = graph ; pc = lbl ;228 let sf = { result = ret_regs ; graph = graph ; pc = lbl ; 222 229 sp = sp ; lenv = lenv ; carry = carry } in 223 230 CallState (sf :: sfrs, f_def, args, mem, inds, trace) … … 240 247 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v 241 248 242  RTL.St_return rl>243 let vl = List.map (get_local_ arg_value lenv) rlin249  RTL.St_return > 250 let vl = List.map (get_local_value lenv) lenv.le_rets in 244 251 let mem = Mem.free mem sp in 245 252 ReturnState (sfrs, vl, mem, inds, trace) … … 255 262 (locals : Register.Set.t) 256 263 (params : Register.t list) 264 (rets : Register.t list) 257 265 (args : Val.t list) : 258 266 local_env = 259 let f r lenv = Register.Map.add r Val.undef lenvin260 let lenv = Register.Set.fold f locals Register.Map.empty in261 let f lenv r v = Register.Map.add r v lenvin262 List.fold_left2 f lenv params args267 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 } 263 271 264 272 let state_after_call … … 274 282 let inds = new_ind inds in 275 283 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 276 286 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, 278 288 Val.undef, mem', inds, trace) 279 289  RTL.F_ext def > … … 289 299 (trace : CostLabel.t list) : 290 300 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 293 305 let inds = forget_ind inds in 294 306 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
Note: See TracChangeset
for help on using the changeset viewer.