Changeset 1319 for Deliverables/D2.2
- Timestamp:
- Oct 7, 2011, 1:48:26 PM (8 years ago)
- Location:
- Deliverables/D2.2/8051-indexed-labels-branch/src
- Files:
-
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml
r1310 r1319 289 289 Clight.LScase (i, s', ls') 290 290 291 (* calculating the maximal depth of single-entry loops *)292 (* (as already calculated during the labeling phase) *)293 294 let rec max_loop_index =295 let f_expr _ _ = () in296 let f_stmt stmt _ sub_stmts_res =297 let curr_max = List.fold_left max 0 sub_stmts_res in298 match stmt with299 | Clight.Swhile (Some x, _, _) | Clight.Sdowhile (Some x, _, _)300 | Clight.Sfor (Some x, _, _, _, _) -> max x curr_max (* = curr_max+1 ? *)301 | _ -> curr_max in302 ClightFold.statement2 f_expr f_stmt303 304 291 let rec loop_indexes_defs prefix max_depth = 305 292 if max_depth = 0 then [] else 293 let max_depth = max_depth - 1 in 306 294 let uint = Clight.Tint(Clight.I32, AST.Unsigned) in 307 295 let id = CostLabel.make_id prefix max_depth in 308 (id, uint) :: loop_indexes_defs prefix (max_depth-1)296 (id, uint) :: loop_indexes_defs prefix max_depth 309 297 310 298 (* Instrument a function. *) … … 313 301 let def = match def with 314 302 | Clight.Internal def -> 315 let max_depth = max_loop_indexdef.Clight.fn_body in303 let max_depth = ClightUtils.max_loop_index_lbld def.Clight.fn_body in 316 304 let vars = loop_indexes_defs l_ind max_depth in 317 305 let vars = List.rev_append vars def.Clight.fn_vars in -
Deliverables/D2.2/8051-indexed-labels-branch/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) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml
r1297 r1319 99 99 let s2' = add_starting_cost_label ind cost_universe s2' in 100 100 Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2') 101 | Swhile (e,s) -> 101 | Swhile (i,e,s) -> 102 let ind = match i with 103 | None -> ind 104 | Some _ -> CostLabel.add_id_indexing ind in 102 105 let s' = add_cost_labels_st ind cost_universe s in 103 106 let s' = add_starting_cost_label ind cost_universe s' in 104 107 add_ending_cost_label ind cost_universe 105 (Swhile (add_cost_labels_e ind cost_universe e, s')) 106 | Sdowhile (e,s) -> 107 let s1 = add_cost_labels_st ind cost_universe s in 108 let s2 = add_cost_labels_st ind cost_universe s in 109 let s2' = add_starting_cost_label ind cost_universe s2 in 108 (Swhile (i,add_cost_labels_e ind cost_universe e, s')) 109 | Sdowhile (i,e,s) -> 110 let ind = match i with 111 | None -> ind 112 | Some _ -> CostLabel.add_id_indexing ind in 113 let s' = add_cost_labels_st ind cost_universe s in 114 let s' = add_starting_cost_label ind cost_universe s' in 110 115 add_ending_cost_label ind cost_universe 111 (S sequence (s1, Swhile (add_cost_labels_e ind cost_universe e, s2')))112 | Sfor ( s1,e,s2,s3) ->116 (Sdowhile (i,add_cost_labels_e ind cost_universe e, s')) 117 | Sfor (i,s1,e,s2,s3) -> 113 118 let s1' = add_cost_labels_st ind cost_universe s1 in 119 let ind = match i with 120 | None -> ind 121 | Some _ -> CostLabel.add_id_indexing ind in 114 122 let s2' = add_cost_labels_st ind cost_universe s2 in 115 123 let s3' = add_cost_labels_st ind cost_universe s3 in 116 124 let s3' = add_starting_cost_label ind cost_universe s3' in 117 125 add_ending_cost_label ind cost_universe 118 (Sfor ( s1', add_cost_labels_e ind cost_universe e, s2', s3'))126 (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3')) 119 127 | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e) 120 128 | Sswitch (e,ls) -> … … 162 170 let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in 163 171 let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in 164 let ind = CostLabel. id_indexing 0in172 let ind = CostLabel.empty_indexing in 165 173 { 166 174 prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct; -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightUtils.ml
r486 r1319 2 2 open Clight 3 3 4 4 (* 5 5 (* TODO: Alignment constraints? *) 6 6 let rec size_of_ctype = function … … 72 72 | Tpointer (sp,_) | Tarray (sp,_,_) | Tcomp_ptr (sp,_) -> sp 73 73 | _ -> assert false (* do not use on those arguments *) 74 *) 75 76 let max_loop_index_lbld = 77 let f_expr _ _ = () in 78 let f_stmt stmt _ sub_stmts_res = 79 let curr_max = List.fold_left max 0 sub_stmts_res in 80 match stmt with 81 | Clight.Swhile (Some x, _, _) | Clight.Sdowhile (Some x, _, _) 82 | Clight.Sfor (Some x, _, _, _, _) -> max x curr_max (* = curr_max+1 ? *) 83 | _ -> curr_max in 84 ClightFold.statement2 f_expr f_stmt -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightUtils.mli
r486 r1319 1 1 2 (* 2 3 val size_of_ctype : Clight.ctype -> int 3 4 … … 13 14 14 15 val region_of_pointer_type : Clight.ctype -> AST.region 16 *) 17 18 (** [max_loop_index_labld s] calculates the maximal depth plus one of 19 single-entry loops in [s], if [s] has already been labeled *) 20 val max_loop_index_lbld : Clight.statement -> int -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml
r1310 r1319 12 12 let sexpr_id = Sexpr(1, 0) 13 13 14 let const_sexpr n = Sexpr(0, n) 15 14 16 type index = int 15 17 … … 18 20 type indexing = sexpr list 19 21 20 type const_indexing = int ref list22 type const_indexing = int array 21 23 22 24 (** [enter_loop n indexing] is used to update indexing when one is entering a 23 25 loop indexed by [n]. 24 26 The function recycles the same constant indexing *) 25 let rec enter_loop n indexing = match n, indexing with 26 | None, _ -> indexing (* entering a multi-entry loop *) 27 | Some 0, [] -> [ref 0] (* entering a single entry loop, current depth *) 28 | Some 0, hd :: tl -> hd := 0; indexing (* as above, reusing slot *) 29 | Some x, hd :: tl -> hd :: enter_loop (Some (x-1)) tl (* lower depth *) 30 | Some x, [] -> assert false(* means I'm entering a single entry loop *) 31 (* without having entered the one containing it *) 27 let rec enter_loop n indexing = match n with 28 | None -> () 29 | Some x -> indexing.(x) <- 0 32 30 33 31 (** [enter_loop n indexing] is used to update indexing when one is continuing a 34 32 loop indexed by [n]. *) 35 let rec continue_loop n indexing = match n, indexing with 36 | None, _ -> indexing (* continuing a multi-entry loop *) 37 | Some 0, hd :: tl -> hd := !hd + 1; indexing (* incrementing index *) 38 | Some x, hd :: tl -> hd :: continue_loop (Some (x-1)) tl (* lower depth *) 39 | Some _, [] -> assert false (* means I'm continuing a single entry loop *) 40 (* without having entered it *) 33 let rec continue_loop n indexing = match n with 34 | None -> () 35 | Some x -> indexing.(x) <- indexing.(x) + 1 41 36 42 37 let sexpr_of i l = … … 47 42 | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of" 48 43 49 let rec id_indexing = function50 | 0 -> [] 51 | n -> sexpr_id :: id_indexing (n-1) 44 let empty_indexing = [] 45 46 let add_id_indexing ind = sexpr_id :: ind 52 47 53 48 (* a*_+b is composed with c*_+d by substitution: *) … … 70 65 | _ -> n 71 66 72 let rec compose_const_indexing c m = match c, m with73 | i1 :: l1, s2 :: l2 -> ev_sexpr !i1 s2 :: compose_const_indexing l1 l274 | _, [] -> [] (* that's ok as current indexings will not be shrinked *)75 | [], _ -> assert false (* means an indexed label is not in the right ctx *)67 let rec compose_const_indexing_i i c = function 68 | [] -> [] 69 | s :: l -> 70 const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l 76 71 77 72 module IndexingSet = Set.Make(struct … … 80 75 end) 81 76 82 83 77 type t = { 84 78 name : Atom.t; 85 79 i : indexing 86 80 } 81 82 let apply_const_indexing c lbl = 83 {lbl with i = compose_const_indexing_i 0 c lbl.i} 87 84 88 85 -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli
r1310 r1319 21 21 type indexing = sexpr list 22 22 23 type const_indexing = int ref list23 type const_indexing = int array 24 24 25 25 (** [enter_loop n indexing] is used to update indexing when one is entering a 26 26 loop indexed by [n]. 27 27 The function recycles the same constant indexing *) 28 val enter_loop : index option -> const_indexing -> const_indexing28 val enter_loop : index option -> const_indexing -> unit 29 29 30 30 (** [continue_loop n indexing] is used to update indexing when one is continuing a 31 31 loop indexed by [n]. *) 32 val continue_loop : index option -> const_indexing -> const_indexing32 val continue_loop : index option -> const_indexing -> unit 33 33 34 (** [ id_indexing n] generates an identity indexing nested in [n] loops*)35 val id_indexing : int ->indexing34 (** [empty_indexing] generates an empty indexing *) 35 val empty_indexing : indexing 36 36 37 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 38 val compose_index : index -> sexpr -> indexing -> indexing 39 40 (** [compose_index l m] applies all the transformations in [l] to [m] *) 41 val compose_indexing : indexing -> indexing -> indexing 42 43 val compose_const_indexing : const_indexing -> indexing -> int list 37 (** [add_id_indexing ind] adds an identity mapping in front of ind **) 38 val add_id_indexing : indexing -> indexing 44 39 45 40 module IndexingSet : Set.S with type elt = indexing … … 49 44 i : indexing 50 45 } 46 47 val apply_const_indexing : const_indexing -> t -> t 48 51 49 52 50 (** [string_of_cost_label pref t] converts an indexed label to a
Note: See TracChangeset
for help on using the changeset viewer.