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

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml
r1572 r1589 19 19 function being executed. *) 20 20 21 type local_env = (Val.t * AST.sig_type) Register.Map.t 21 type local_env = { 22 le_vals : (Val.t * AST.sig_type) Register.Map.t ; 23 le_ret : Register.t option 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_reg: Register.t option ;32 { result : Register.t option ; 30 33 graph : RTLabs.graph ; 31 34 sp : Val.address ; … … 53 56 (if Val.eq v Val.undef then "" 54 57 else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in 55 Register.Map.fold f lenv ""58 Register.Map.fold f lenv.le_vals "" 56 59 57 60 let string_of_args args = … … 84 87 85 88 let 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 88 93 89 94 let get_value = get_local_env fst … … 92 97 93 98 let update_local r v lenv = 94 let f (_, t) = Register.Map.add r (v, t) lenv in95 get_local_env f lenv r99 let f (_, t) = Register.Map.add r (v, t) lenv.le_vals in 100 { lenv with le_vals = get_local_env f lenv r } 96 101 97 102 let update_locals rs vs lenv = … … 209 214 (* Save the stack frame. *) 210 215 let sf = 211 { re t_reg= destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }216 { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 212 217 in 213 218 CallState (sf :: sfrs, f_def, args, mem, inds, trace) … … 219 224 (* Save the stack frame. *) 220 225 let sf = 221 { re t_reg= destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }226 { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 222 227 in 223 228 CallState (sf :: sfrs, f_def, args, mem, inds, trace) … … 275 280 *) 276 281 277  RTLabs.St_return None>282  RTLabs.St_return > 278 283 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) 286 288 287 289 module InterpretExternal = Primitive.Interpret (Mem) … … 297 299 (locals : (Register.t * AST.sig_type) list) 298 300 (params : (Register.t * AST.sig_type) list) 301 (ret : (Register.t * AST.sig_type) option) 299 302 (args : Val.t list) : 300 303 local_env = 301 304 let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in 302 305 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 } 305 309 306 310 let state_after_call … … 316 320 let (mem', sp) = 317 321 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 319 328 (* allocate new constant indexing *) 320 let graph = def.RTLabs.f_graph in321 329 let inds = new_ind inds in 322 330 State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace) … … 334 342 (trace : CostLabel.t list) : 335 343 state = 336 let lenv = match sf.re t_regwith344 let lenv = match sf.result with 337 345  None > sf.lenv 338 346  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) 343 350 344 351
Note: See TracChangeset
for help on using the changeset viewer.