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

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/clight/clightInterpret.ml
r1345 r1357 32 32  Kfor3 of int option*expr*statement*statement*continuation 33 33  Kswitch of continuation 34  Kcall of (Value.address*ctype) option*cfunction*localEnv* 35 indexing*continuation 34  Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation 36 35 37 36 type state = 38  State of cfunction*statement*continuation*localEnv*memory*indexing 39  Callstate of fundef*Value.t list*continuation*memory 40  Returnstate of Value.t*continuation*memory 37  State of cfunction*statement*continuation*localEnv*memory*indexing list 38  Callstate of fundef*Value.t list*continuation*memory*indexing list 39  Returnstate of Value.t*continuation*memory*indexing list 41 40 42 41 let string_of_unop = function … … 157 156 (string_of_local_env lenv) 158 157 (Mem.to_string mem); 159 Array.iteri (fun a > Printf.printf "%d,") c; 158 let i = CostLabel.curr_const_ind c in 159 CostLabel.const_ind_iter (fun a > Printf.printf "%d, " a) i; 160 160 Printf.printf "\nRegular state: %s\n\n%!" 161 161 (string_of_statement stmt) 162  Callstate (_, args, _, mem ) >162  Callstate (_, args, _, mem, _) > 163 163 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 164 164 (Mem.to_string mem) 165 165 (MiscPottier.string_of_list " " Value.to_string args) 166  Returnstate (v, _, mem ) >166  Returnstate (v, _, mem, _) > 167 167 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 168 168 (Mem.to_string mem) … … 427 427  Ecost (lbl,e1) > 428 428 (* applying current indexing on label *) 429 let lbl = CostLabel. apply_const_indexing clbl in429 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in 430 430 let (v1,l1) = eval_expr localenv m c e1 in 431 431 (v1,lbl::l1) … … 492 492  Sskip, Kdowhile(i,a,s,k')  Scontinue, Kdowhile (i,a,s,k') > 493 493 (* possibly continuing a loop *) 494 CostLabel.continue_loop i c; (* if loop is not continued, this change494 CostLabel.continue_loop_opt c i; (* if loop is not continued, this change 495 495 will have no effect in the following. *) 496 496 let ((v1,_),l1) = eval_expr e m c a in … … 499 499 condition v1 a_true a_false 500 500  Sskip, Kfor3(i,a2,a3,s,k)  Scontinue, Kfor3(i,a2,a3,s,k) > 501 CostLabel.continue_loop i c;501 CostLabel.continue_loop_opt c i; 502 502 let ((v1,_),l1) = eval_expr e m c a2 in 503 503 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 508 508  Sskip, Kcall _ > 509 509 let m' = free_local_env m e in 510 (Returnstate(Value.undef,k,m' ),[])510 (Returnstate(Value.undef,k,m',c),[]) 511 511  Sassign(a1, a2), _ > 512 512 let ((v1,t1),l1) = (eval_lvalue e m c a1) in … … 517 517 let fd = Mem.find_fun_def m (address_of_value v1) in 518 518 let (vargs,l2) = eval_exprlist e m c al in 519 (Callstate(fd,vargs,Kcall(None,f,e, c,k),m),l1@l2)519 (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2) 520 520  Scall(Some lhs,a,al), _ > 521 521 let ((v1,_),l1) = eval_expr e m c a in … … 523 523 let (vargs,l2) = eval_exprlist e m c al in 524 524 let (vt3,l3) = eval_lvalue e m c lhs in 525 (Callstate(fd,vargs,Kcall(Some vt3,f,e, c,k),m),l1@l2@l3)525 (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3) 526 526  Ssequence(s1,s2), _ > (State(f,s1,Kseq(s2,k),e,m,c),[]) 527 527  Sifthenelse(a,s1,s2), _ > … … 531 531 condition v1 a_true a_false 532 532  Swhile(i,a,s), _ > 533 CostLabel.enter_loop i c;533 CostLabel.enter_loop_opt c i; 534 534 let ((v1,_),l1) = eval_expr e m c a in 535 535 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 537 537 condition v1 a_true a_false 538 538  Sdowhile(i,a,s), _ > 539 CostLabel.enter_loop i c;539 CostLabel.enter_loop_opt c i; 540 540 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[]) 541 541  Sfor(i,Sskip,a2,a3,s), _ > 542 CostLabel.enter_loop i c;542 CostLabel.enter_loop_opt c i; 543 543 let ((v1,_),l1) = eval_expr e m c a2 in 544 544 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 553 553  Sreturn None, _ > 554 554 let m' = free_local_env m e in 555 (Returnstate(Value.undef,(call_cont k),m' ),[])555 (Returnstate(Value.undef,(call_cont k),m',c),[]) 556 556  Sreturn (Some a), _ > 557 557 let ((v1,_),l1) = eval_expr e m c a in 558 558 let m' = free_local_env m e in 559 (Returnstate(v1,call_cont k,m' ),l1)559 (Returnstate(v1,call_cont k,m',c),l1) 560 560  Sswitch(a,sl), _ > 561 561 let ((v,_),l) = eval_expr e m c a in … … 565 565  Scost(lbl,s), _ > 566 566 (* applying current indexing on label *) 567 let lbl = CostLabel. apply_const_indexing clbl in567 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in 568 568 (State(f,s,k,e,m,c),[lbl]) 569 569  Sgoto lbl, _ > … … 578 578 module InterpretExternal = Primitive.Interpret (Mem) 579 579 580 let interpret_external k mem f args =580 let interpret_external k mem c f args = 581 581 let (mem', v) = match InterpretExternal.t mem f args with 582 582  (mem', InterpretExternal.V vs) > … … 584 584 (mem', v) 585 585  (mem', InterpretExternal.A addr) > (mem', value_of_address addr) in 586 Returnstate (v, k, mem' )587 588 let step_call args cont mem = function586 Returnstate (v, k, mem',c) 587 588 let step_call args cont mem c = function 589 589  Internal f > 590 590 let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in 591 591 (* initializing loop indices *) 592 let max_depth = ClightUtils.max_loop_index_lbld f.fn_body in 593 let c = Array.make max_depth 0 in 592 let c = CostLabel.new_const_ind c in 594 593 State (f, f.fn_body, cont, e, mem', c) 595 594  External(id,targs,tres) when List.length targs = List.length args > 596 interpret_external cont mem id args595 interpret_external cont mem c id args 597 596  External(id,_,_) > 598 597 error ("wrong size of arguments when calling external " ^ id ^ ".") … … 600 599 let step = function 601 600  State(f,stmt,k,e,m,c) > eval_stmt f k e m stmt c 602  Callstate(fun_def,vargs,k,m) > (step_call vargs k m fun_def,[]) 603  Returnstate(v,Kcall(None,f,e,c,k),m) > (State(f,Sskip,k,e,m,c),[]) 604  Returnstate(v,Kcall((Some(vv, ty)),f,e,c,k),m) > 601  Callstate(fun_def,vargs,k,m,c) > (step_call vargs k m c fun_def,[]) 602  Returnstate(v,Kcall(None,f,e,k),m,c) > 603 let c = CostLabel.forget_const_ind c in 604 (State(f,Sskip,k,e,m,c),[]) 605  Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) > 606 let c = CostLabel.forget_const_ind c in 605 607 let m' = assign m v ty vv in 606 608 (State(f,Sskip,k,e,m',c),[]) … … 641 643 if debug then print_state state ; 642 644 match state with 643  Returnstate(v,Kstop,_ ) > (* Explicit return in main *)645  Returnstate(v,Kstop,_,_) > (* Explicit return in main *) 644 646 print_and_return_result (compute_result v) 645 647  State(_,Sskip,Kstop,_,_,_) > (* Implicit return in main *) … … 653 655  Some main > 654 656 let mem = init_mem prog in 655 let first_state = (Callstate (find_fundef main mem,[],Kstop,mem ),[]) in657 let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in 656 658 exec debug [] first_state
Note: See TracChangeset
for help on using the changeset viewer.