 Timestamp:
 Oct 11, 2011, 5:42:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/cminor/cminorInterpret.ml
r1345 r1357 31 31  Ct_endblock of continuation 32 32  Ct_returnto of 33 ident option*internal_function*Val.address*local_env* indexing*continuation33 ident option*internal_function*Val.address*local_env*continuation 34 34 35 35 type state = 36 36 State_regular of 37 37 internal_function*statement*continuation*Val.address*local_env* 38 (function_def Mem.memory)*indexing 39  State_call of function_def*Val.t list*continuation*(function_def Mem.memory) 40  State_return of Val.t*continuation*(function_def Mem.memory) 38 (function_def Mem.memory)*indexing list 39  State_call of function_def*Val.t list*continuation* 40 (function_def Mem.memory)*indexing list 41  State_return of Val.t*continuation*(function_def Mem.memory)*indexing list 41 42 42 43 let string_of_local_env lenv = … … 81 82 (Mem.to_string mem) 82 83 (Val.to_string (value_of_address sp)); 83 Array.iter (fun a > Printf.printf "%d, " a) i; 84 let ind = CostLabel.curr_const_ind i in 85 CostLabel.const_ind_iter (fun a > Printf.printf "%d, " a) ind; 84 86 Printf.printf "\nRegular state: %s\n\n%!" 85 87 (string_of_statement stmt) 86  State_call (_, args, _, mem ) >88  State_call (_, args, _, mem,_) > 87 89 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 88 90 (Mem.to_string mem) 89 91 (MiscPottier.string_of_list " " Val.to_string args) 90  State_return (v, _, mem ) >92  State_return (v, _, mem,_) > 91 93 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 92 94 (Mem.to_string mem) … … 264 266 265 267 266 let call_state sigma e m f params cont =268 let call_state sigma e m i f params cont = 267 269 let (addr,l1) = eval_expression sigma e m f in 268 270 let fun_def = Mem.find_fun_def m (address_of_value addr) in 269 271 let (args,l2) = eval_exprlist sigma e m params in 270 (State_call(fun_def,args,cont,m ),l1@l2)272 (State_call(fun_def,args,cont,m,i),l1@l2) 271 273 272 274 let eval_stmt f k sigma e m i s = match s, k with … … 274 276  St_skip,Ct_endblock(k) > (State_regular(f, St_skip, k, sigma, e, m, i),[]) 275 277  St_skip, (Ct_returnto _ as k) > 276 (State_return (Val.undef,k,Mem.free m sigma ),[])278 (State_return (Val.undef,k,Mem.free m sigma,i),[]) 277 279  St_skip,Ct_ind_inc(ind,k) > 278 CostLabel.continue_loop (Some ind) i;280 CostLabel.continue_loop i ind; 279 281 (State_regular(f, s, k, sigma, e, m, i),[]) 280 282  St_skip,Ct_stop > 281 (State_return (Val.undef,Ct_stop,Mem.free m sigma ),[])283 (State_return (Val.undef,Ct_stop,Mem.free m sigma,i),[]) 282 284  St_assign(x,exp),_ > 283 285 let (v,l) = eval_expression sigma e m exp in … … 290 292 (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2) 291 293  St_call(xopt,f',params,_),_ > 292 call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,i,k))294 call_state sigma e m i f' params (Ct_returnto(xopt,f,sigma,e,k)) 293 295  St_tailcall(f',params,_),_ > 294 call_state sigma e m f' params (callcont k)296 call_state sigma e m i f' params (callcont k) 295 297  St_seq(s1,s2),_ > (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[]) 296 298  St_ifthenelse(exp,s1,s2),_ > … … 324 326 else error "undefined switch value." 325 327  St_return(None),_ > 326 (State_return (Val.undef,callcont k,Mem.free m sigma ),[])328 (State_return (Val.undef,callcont k,Mem.free m sigma,i),[]) 327 329  St_return(Some(a)),_ > 328 330 let (v,l) = eval_expression sigma e m a in 329 (State_return (v,callcont k,Mem.free m sigma ),l)331 (State_return (v,callcont k,Mem.free m sigma,i),l) 330 332  St_cost(lbl,s),_ > 331 333 (* applying current indexing on label *) 332 let lbl = CostLabel. apply_const_indexing ilbl in334 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in 333 335 (State_regular(f,s,k,sigma,e,m,i),[lbl]) 334 336  St_ind_0(ind,s),_ > 335 CostLabel.enter_loop (Some ind) i;337 CostLabel.enter_loop i ind; 336 338 (State_regular(f,s,k,sigma,e,m,i), []) 337 339  St_ind_inc(s,ind),_ > … … 342 344 module InterpretExternal = Primitive.Interpret (Mem) 343 345 344 let interpret_external k mem f args =346 let interpret_external k mem i f args = 345 347 let (mem', v) = match InterpretExternal.t mem f args with 346 348  (mem', InterpretExternal.V vs) > … … 348 350 (mem', v) 349 351  (mem', InterpretExternal.A addr) > (mem', value_of_address addr) in 350 State_return (v, k, mem') 351 352 let max_loop_index = 353 let f_expr _ _ = () in 354 let f_stmt stmt _ sub_stmts_res = 355 let curr_max = List.fold_left max 0 sub_stmts_res in 356 match stmt with 357  Cminor.St_ind_0 (x, _)  Cminor.St_ind_inc (_, x) > 358 max (x+1) curr_max 359  _ > curr_max in 360 CminorFold.statement f_expr f_stmt 361 362 let step_call vargs k m = function 352 State_return (v, k, mem', i) 353 354 let step_call vargs k m i = function 363 355  F_int f > 364 356 let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in 365 357 let lenv = init_local_env vargs f.f_params f.f_vars in 366 let i = Array.make (max_loop_index f.f_body) 0in358 let i = CostLabel.new_const_ind i in 367 359 State_regular(f,f.f_body,k,sp,lenv,m,i) 368  F_ext f > interpret_external k m f.ef_tag vargs360  F_ext f > interpret_external k m i f.ef_tag vargs 369 361 370 362 let step = function 371 363  State_regular(f,stmt,k,sp,e,m,i) > eval_stmt f k sp e m i stmt 372  State_call(fun_def,vargs,k,m) > (step_call vargs k m fun_def,[]) 373  State_return(v,Ct_returnto(None,f,sigma,e,i,k),m) > 364  State_call(fun_def,vargs,k,m,i) > (step_call vargs k m i fun_def,[]) 365  State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) > 366 let i = CostLabel.forget_const_ind i in 374 367 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 375  State_return(v,Ct_returnto(Some x,f,sigma,e, i,k),m) >368  State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) > 376 369 let e = LocalEnv.add x v e in 370 let i = CostLabel.forget_const_ind i in 377 371 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 378 372  _ > error "state malformation." … … 397 391 if debug then print_state state ; 398 392 match state with 399  State_return(v,Ct_stop,_ ) > (* Explicit return in main *)393  State_return(v,Ct_stop,_,_) > (* Explicit return in main *) 400 394 print_and_return_result (compute_result v) 401 395  State_regular(_,St_skip,Ct_stop,_,_,_,_) > (* Implicit return in main *) … … 409 403  Some main > 410 404 let mem = init_mem prog in 411 let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in 405 let main = find_fundef main mem in 406 let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in 412 407 exec debug [] first_state
Note: See TracChangeset
for help on using the changeset viewer.