 Timestamp:
 Oct 7, 2011, 1:48:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/clight/clightInterpret.ml
r1310 r1319 32 32  Kfor3 of int option*expr*statement*statement*continuation 33 33  Kswitch of continuation 34  Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation 34  Kcall of (Value.address*ctype) option*cfunction*localEnv* 35 indexing*continuation 35 36 36 37 type state = … … 152 153 153 154 let print_state = function 154  State (_, stmt, _, lenv, mem ) >155 Printf.printf "Local environment:\n%s\n\nMemory:%s\n Regular state: %s\n\n%!"155  State (_, stmt, _, lenv, mem, c) > 156 Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing:" 156 157 (string_of_local_env lenv) 157 (Mem.to_string mem) 158 (Mem.to_string mem); 159 Array.iteri (fun a > Printf.printf "%d,") c; 160 Printf.printf "\nRegular state: %s\n\n%!" 158 161 (string_of_statement stmt) 159 162  Callstate (_, args, _, mem) > … … 371 374 let is_false (v, _) = Value.is_false v 372 375 373 let rec eval_expr localenv m (Expr (ee, tt)) =376 let rec eval_expr localenv m c (Expr (ee, tt)) = 374 377 match ee with 375 378  Econst_int i > … … 385 388 ((v, tt), []) 386 389  Ederef e when is_function_type tt  is_big_type tt > 387 let ((v1,_),l1) = eval_expr localenv m e in390 let ((v1,_),l1) = eval_expr localenv m c e in 388 391 ((v1,tt),l1) 389 392  Ederef e > 390 let ((v1,_),l1) = eval_expr localenv m e in393 let ((v1,_),l1) = eval_expr localenv m c e in 391 394 let addr = address_of_value v1 in 392 395 let v = Mem.load m (size_of_ctype tt) addr in 393 396 ((v,tt),l1) 394 397  Eaddrof exp > 395 let ((addr,_),l) = eval_lvalue localenv m exp in398 let ((addr,_),l) = eval_lvalue localenv m c exp in 396 399 ((value_of_address addr,tt),l) 397 400  Ebinop (op,exp1,exp2) > 398 let (v1,l1) = eval_expr localenv m exp1 in399 let (v2,l2) = eval_expr localenv m exp2 in401 let (v1,l1) = eval_expr localenv m c exp1 in 402 let (v2,l2) = eval_expr localenv m c exp2 in 400 403 ((eval_binop tt v1 v2 op,tt),l1@l2) 401 404  Eunop (op,exp) > 402 let (e1,l1) = eval_expr localenv m exp in405 let (e1,l1) = eval_expr localenv m c exp in 403 406 ((eval_unop tt e1 op,tt),l1) 404 407  Econdition (e1,e2,e3) > 405 let (v1,l1) = eval_expr localenv m e1 in406 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)408 let (v1,l1) = eval_expr localenv m c e1 in 409 if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2) 407 410 else 408 if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)411 if is_false v1 then let (v3,l3) = eval_expr localenv m c e3 in (v3,l1@l3) 409 412 else (v1,l1) 410 413  Eandbool (e1,e2) > 411 let (v1,l1) = eval_expr localenv m e1 in412 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)414 let (v1,l1) = eval_expr localenv m c e1 in 415 if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2) 413 416 else (v1,l1) 414 417  Eorbool (e1,e2) > 415 let (v1,l1) = eval_expr localenv m e1 in416 if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)418 let (v1,l1) = eval_expr localenv m c e1 in 419 if is_false v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2) 417 420 else (v1,l1) 418 421  Esizeof cty > ((Value.of_int (sizeof cty),tt),[]) 419 422  Efield (e1,id) > 420 let ((v1,t1),l1) = eval_expr localenv m e1 in423 let ((v1,t1),l1) = eval_expr localenv m c e1 in 421 424 let addr = address_of_value (get_offset v1 id t1) in 422 425 ((Mem.load m (size_of_ctype tt) addr, tt), l1) 423 426  Ecost (lbl,e1) > 424 let (v1,l1) = eval_expr localenv m e1 in 427 (* applying current indexing on label *) 428 let lbl = CostLabel.apply_const_indexing c lbl in 429 let (v1,l1) = eval_expr localenv m c e1 in 425 430 (v1,lbl::l1) 426 431  Ecall _ > assert false (* only used by the annotation process *) 427 432  Ecast (cty,exp) > 428 let ((v,ty),l1) = eval_expr localenv m exp in433 let ((v,ty),l1) = eval_expr localenv m c exp in 429 434 ((eval_cast (v,ty,cty),tt),l1) 430 435 431 and eval_lvalue localenv m (Expr (e,t)) = match e with436 and eval_lvalue localenv m c (Expr (e,t)) = match e with 432 437  Econst_int _  Econst_float _  Eaddrof _  Eunop (_,_)  Ebinop (_,_,_) 433 438  Ecast (_,_)  Econdition (_,_,_)  Eandbool (_,_)  Eorbool (_,_) … … 435 440  Evar id > ((find_symbol localenv m id,t),[]) 436 441  Ederef ee > 437 let ((v,_),l1) = eval_expr localenv m ee in442 let ((v,_),l1) = eval_expr localenv m c ee in 438 443 ((address_of_value v,t),l1) 439 444  Efield (ee,id) > 440 let ((v,tt),l1) = eval_expr localenv m ee in445 let ((v,tt),l1) = eval_expr localenv m c ee in 441 446 let v' = get_offset v id tt in 442 447 ((address_of_value v', t), l1) 443 448  Ecost (lbl,ee) > 444 let (v,l) = eval_lvalue localenv m ee in449 let (v,l) = eval_lvalue localenv m c ee in 445 450 (v,lbl::l) 446 451  Ecall _ > assert false (* only used in the annotation process *) 447 452 448 let eval_exprlist lenv mem es =453 let eval_exprlist lenv mem c es = 449 454 let f (vs, cost_lbls) e = 450 let ((v, _), cost_lbls') = eval_expr lenv mem e in455 let ((v, _), cost_lbls') = eval_expr lenv mem c e in 451 456 (vs @ [v], cost_lbls @ cost_lbls') in 452 457 List.fold_left f ([], []) es … … 480 485 else error "undefined condition guard value." 481 486 482 (** FIXME: modifying here! *) 483 let eval_stmt f k e m s c = match s, k with 484  Sskip, Kseq(s,k) > (State(f,s,k,e,m),[]) 485  Sskip, Kwhile(i,a,s,k) as w > 487 let eval_stmt f k e m s c = 488 let enter_loop = CostLabel.enter_loop in 489 let continue_loop = CostLabel.continue_loop in 490 match s, k with 491  Sskip, Kseq(s,k) > (State(f,s,k,e,m,c),[]) 492  Sskip, Kwhile(i,a,s,k')  Scontinue, Kwhile(i,a,s,k') 493  Sskip, Kdowhile(i,a,s,k')  Scontinue, Kdowhile (i,a,s,k') > 486 494 (* possibly continuing a loop *) 487 let c = continue_loop i c in 488 let ((v1,_),l1) = eval_expr e m a in 495 continue_loop i c; (* if loop is not continued, this change will have no 496 effect in the following. Can be made stricter *) 497 let ((v1,_),l1) = eval_expr e m c a in 498 let a_false = (State(f,Sskip,k',e,m,c),l1) in 499 let a_true = (State(f,s,k,e,m,c),l1) in 500 condition v1 a_true a_false 501  Sskip, Kfor3(i,a2,a3,s,k)  Scontinue, Kfor3(i,a2,a3,s,k) > 502 continue_loop i c; 503 let ((v1,_),l1) = eval_expr e m c a2 in 489 504 let a_false = (State(f,Sskip,k,e,m,c),l1) in 490 let a_true = (State(f,s, w,e,m,c),l1) in505 let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in 491 506 condition v1 a_true a_false 492  Sskip, Kdowhile(i,a,s,k) as w > 493 let c = continue_loop i c in 494 let ((v1, _),l1) = eval_expr e m a in 495 let a_false = (State(f,Sskip,k,e,m,c),l1) in 496 let a_true = (State(f,s,w,e,m,c),l1) in 497 condition v1 a_true a_false 498  Sskip, Kfor3(i,a2,a3,s,k) > (State(f,Sfor(i,Sskip,a2,a3,s),k,e,m),[]) 499  Sskip, Kfor2(i,a2,a3,s,k) > (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 500  Sskip, Kswitch k > (State(f,Sskip,k,e,m),[]) 507  Sskip, Kfor2(i,a2,a3,s,k) > (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[]) 508  Sskip, Kswitch k > (State(f,Sskip,k,e,m,c),[]) 501 509  Sskip, Kcall _ > 502 510 let m' = free_local_env m e in 503 511 (Returnstate(Value.undef,k,m'),[]) 504 512  Sassign(a1, a2), _ > 505 let ((v1,t1),l1) = (eval_lvalue e m a1) in506 let ((v2,t2),l2) = eval_expr e m a2 in507 (State(f,Sskip,k,e,assign m v2 t1 v1 ),l1@l2)513 let ((v1,t1),l1) = (eval_lvalue e m c a1) in 514 let ((v2,t2),l2) = eval_expr e m c a2 in 515 (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2) 508 516  Scall(None,a,al), _ > 509 let ((v1,_),l1) = eval_expr e m a in517 let ((v1,_),l1) = eval_expr e m c a in 510 518 let fd = Mem.find_fun_def m (address_of_value v1) in 511 let (vargs,l2) = eval_exprlist e m al in512 (Callstate(fd,vargs,Kcall(None,f,e, k),m),l1@l2)519 let (vargs,l2) = eval_exprlist e m c al in 520 (Callstate(fd,vargs,Kcall(None,f,e,c,k),m),l1@l2) 513 521  Scall(Some lhs,a,al), _ > 514 let ((v1,_),l1) = eval_expr e m a in522 let ((v1,_),l1) = eval_expr e m c a in 515 523 let fd = Mem.find_fun_def m (address_of_value v1) in 516 let (vargs,l2) = eval_exprlist e m al in517 let (vt3,l3) = eval_lvalue e m lhs in518 (Callstate(fd,vargs,Kcall(Some vt3,f,e, k),m),l1@l2@l3)519  Ssequence(s1,s2), _ > (State(f,s1,Kseq(s2,k),e,m ),[])524 let (vargs,l2) = eval_exprlist e m c al in 525 let (vt3,l3) = eval_lvalue e m c lhs in 526 (Callstate(fd,vargs,Kcall(Some vt3,f,e,c,k),m),l1@l2@l3) 527  Ssequence(s1,s2), _ > (State(f,s1,Kseq(s2,k),e,m,c),[]) 520 528  Sifthenelse(a,s1,s2), _ > 521 let ((v1,_),l1) = eval_expr e m a in522 let a_true = (State(f,s1,k,e,m ),l1) in523 let a_false = (State(f,s2,k,e,m ),l1) in529 let ((v1,_),l1) = eval_expr e m c a in 530 let a_true = (State(f,s1,k,e,m,c),l1) in 531 let a_false = (State(f,s2,k,e,m,c),l1) in 524 532 condition v1 a_true a_false 525  Swhile(a,s), _ > 526 let ((v1,_),l1) = eval_expr e m a in 527 let a_false = (State(f,Sskip,k,e,m),l1) in 528 let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in 533  Swhile(i,a,s), _ > 534 enter_loop i c; 535 let ((v1,_),l1) = eval_expr e m c a in 536 let a_false = (State(f,Sskip,k,e,m,c),l1) in 537 let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in 529 538 condition v1 a_true a_false 530  Sdowhile(a,s), _ > (State(f,s,Kdowhile(a,s,k),e,m),[]) 539  Sdowhile(i,a,s), _ > 540 enter_loop i c; 541 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[]) 531 542  Sfor(i,Sskip,a2,a3,s), _ > 532 let c = enter_loop i c in533 let ((v1,_),l1) = eval_expr e m a2 in543 enter_loop i c; 544 let ((v1,_),l1) = eval_expr e m c a2 in 534 545 let a_false = (State(f,Sskip,k,e,m,c),l1) in 535 546 let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in 536 547 condition v1 a_true a_false 537  Sfor(a1,a2,a3,s), _ > (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[]) 538  Sbreak, Kseq(s,k) > (State(f,Sbreak,k,e,m),[]) 539  Sbreak, Kwhile(_,_,k) > (State(f,Sskip,k,e,m),[]) 540  Sbreak, Kdowhile(_,_,k) > (State(f,Sskip,k,e,m),[]) 541  Sbreak, Kfor2(_,_,_,k) > (State(f,Sskip,k,e,m),[]) 542  Sbreak, Kswitch k > (State(f,Sskip,k,e,m),[]) 543  Scontinue, Kseq(_,k) > (State(f,Scontinue,k,e,m),[]) 544  Scontinue, Kwhile(a,s,k) > (State(f,Swhile(a,s),k,e,m),[]) 545  Scontinue, Kdowhile(a,s,k) > 546 let ((v1,_),l1) = eval_expr e m a in 547 let a_false = (State(f,Sskip,k,e,m),l1) in 548 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in 549 condition v1 a_true a_false 550  Scontinue, Kfor2(a2,a3,s,k) > (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 551  Scontinue, Kswitch k > (State(f,Scontinue,k,e,m),[]) 548  Sfor(i,a1,a2,a3,s), _ > (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[]) 549  Sbreak, Kseq(s,k) > (State(f,Sbreak,k,e,m,c),[]) 550  Sbreak, Kwhile(_,_,_,k)  Sbreak, Kdowhile(_,_,_,k) 551  Sbreak, Kfor2(_,_,_,_,k)  Sbreak, Kswitch k > (State(f,Sskip,k,e,m,c),[]) 552  Scontinue, Kseq(_,k) 553  Scontinue, Kswitch k > (State(f,Scontinue,k,e,m,c),[]) 552 554  Sreturn None, _ > 553 555 let m' = free_local_env m e in 554 556 (Returnstate(Value.undef,(call_cont k),m'),[]) 555 557  Sreturn (Some a), _ > 556 let ((v1,_),l1) = eval_expr e m a in558 let ((v1,_),l1) = eval_expr e m c a in 557 559 let m' = free_local_env m e in 558 560 (Returnstate(v1,call_cont k,m'),l1) 559 561  Sswitch(a,sl), _ > 560 let ((v,_),l) = eval_expr e m a in562 let ((v,_),l) = eval_expr e m c a in 561 563 let n = Value.to_int v in 562 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l) 563  Slabel(lbl,s), _ > (State(f,s,k,e,m),[]) 564  Scost(lbl,s), _ > (State(f,s,k,e,m),[lbl]) 564 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l) 565  Slabel(lbl,s), _ > (State(f,s,k,e,m,c),[]) 566  Scost(lbl,s), _ > 567 (* applying current indexing on label *) 568 let lbl = CostLabel.apply_const_indexing c lbl in 569 (State(f,s,k,e,m,c),[lbl]) 565 570  Sgoto lbl, _ > 571 (* if we exit an indexed loop, we don't care. It should not be possible to*) 572 (* enter an indexed loop that is not the current one, so we do nothing*) 573 (* to loop indexes *) 566 574 let (s', k') = find_label lbl f.fn_body (call_cont k) in 567 (State(f,s',k',e,m ),[])575 (State(f,s',k',e,m,c),[]) 568 576  _ > assert false (* should be impossible *) 569 577 … … 582 590  Internal f > 583 591 let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in 584 State (f, f.fn_body, cont, e, mem') 592 (* initializing loop indices *) 593 let max_depth = ClightUtils.max_loop_index_lbld f.fn_body in 594 let c = Array.make max_depth 0 in 595 State (f, f.fn_body, cont, e, mem', c) 585 596  External(id,targs,tres) when List.length targs = List.length args > 586 597 interpret_external cont mem id args … … 589 600 590 601 let step = function 591  State(f,stmt,k,e,m ) > eval_stmt f k e m stmt602  State(f,stmt,k,e,m,c) > eval_stmt f k e m stmt c 592 603  Callstate(fun_def,vargs,k,m) > (step_call vargs k m fun_def,[]) 593  Returnstate(v,Kcall(None,f,e, k),m) > (State(f,Sskip,k,e,m),[])594  Returnstate(v,Kcall((Some(vv, ty)),f,e, k),m) >604  Returnstate(v,Kcall(None,f,e,c,k),m) > (State(f,Sskip,k,e,m,c),[]) 605  Returnstate(v,Kcall((Some(vv, ty)),f,e,c,k),m) > 595 606 let m' = assign m v ty vv in 596 (State(f,Sskip,k,e,m' ),[])607 (State(f,Sskip,k,e,m',c),[]) 597 608  _ > error "state malformation." 598 609 … … 633 644  Returnstate(v,Kstop,_) > (* Explicit return in main *) 634 645 print_and_return_result (compute_result v) 635  State(_,Sskip,Kstop,_,_ ) > (* Implicit return in main *)646  State(_,Sskip,Kstop,_,_,_) > (* Implicit return in main *) 636 647 print_and_return_result IntValue.Int32.zero 637 648  state > exec debug cost_labels (step state)
Note: See TracChangeset
for help on using the changeset viewer.