Changeset 1319 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 7, 2011, 1:48:26 PM (8 years ago)
Author:
tranquil
Message:

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
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  
    289289    Clight.LScase (i, s', ls')
    290290               
    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 _ _ = () in
    296   let f_stmt stmt _ sub_stmts_res =
    297                 let curr_max = List.fold_left max 0 sub_stmts_res in
    298                 match stmt with
    299                   | Clight.Swhile (Some x, _, _) | Clight.Sdowhile (Some x, _, _)
    300                   | Clight.Sfor (Some x, _, _, _, _) -> max x curr_max (* = curr_max+1 ? *)
    301                         | _ -> curr_max in
    302   ClightFold.statement2 f_expr f_stmt
    303        
    304291let rec loop_indexes_defs prefix max_depth =
    305292        if max_depth = 0 then [] else
     293        let max_depth = max_depth - 1 in
    306294  let uint = Clight.Tint(Clight.I32, AST.Unsigned) in
    307295        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
    309297
    310298(* Instrument a function. *)
    … …  
    313301  let def = match def with
    314302    | Clight.Internal def ->
    315         let max_depth = max_loop_index def.Clight.fn_body in
     303        let max_depth = ClightUtils.max_loop_index_lbld def.Clight.fn_body in
    316304        let vars = loop_indexes_defs l_ind max_depth in
    317305        let vars = List.rev_append vars def.Clight.fn_vars in

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml

    r1310 r1319  
    3232  | Kfor3 of int option*expr*statement*statement*continuation
    3333  | 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
    3536
    3637type state =
    … …  
    152153
    153154let print_state = function
    154   | State (_, stmt, _, lenv, mem) ->
    155     Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     155  | State (_, stmt, _, lenv, mem, c) ->
     156    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing:"
    156157      (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%!"
    158161      (string_of_statement stmt)
    159162  | Callstate (_, args, _, mem) ->
    … …  
    371374let is_false (v, _) = Value.is_false v
    372375
    373 let rec eval_expr localenv m (Expr (ee, tt)) =
     376let rec eval_expr localenv m c (Expr (ee, tt)) =
    374377  match ee with
    375378    | Econst_int i ->
    … …  
    385388      ((v, tt), [])
    386389    | Ederef e when is_function_type tt || is_big_type tt ->
    387       let ((v1,_),l1) = eval_expr localenv m e in
     390      let ((v1,_),l1) = eval_expr localenv m c e in
    388391      ((v1,tt),l1)
    389392    | Ederef e ->
    390       let ((v1,_),l1) = eval_expr localenv m e in
     393      let ((v1,_),l1) = eval_expr localenv m c e in
    391394      let addr = address_of_value v1 in
    392395      let v = Mem.load m (size_of_ctype tt) addr in
    393396      ((v,tt),l1)
    394397    | Eaddrof exp ->
    395       let ((addr,_),l) = eval_lvalue localenv m exp in
     398      let ((addr,_),l) = eval_lvalue localenv m c exp in
    396399      ((value_of_address addr,tt),l)
    397400    | Ebinop (op,exp1,exp2) -> 
    398       let (v1,l1) = eval_expr localenv m exp1 in
    399       let (v2,l2) = eval_expr localenv m exp2 in
     401      let (v1,l1) = eval_expr localenv m c exp1 in
     402      let (v2,l2) = eval_expr localenv m c exp2 in
    400403      ((eval_binop tt v1 v2 op,tt),l1@l2)
    401404    | Eunop (op,exp) ->
    402       let (e1,l1) = eval_expr localenv m exp in
     405      let (e1,l1) = eval_expr localenv m c exp in
    403406      ((eval_unop tt e1 op,tt),l1)
    404407    | Econdition (e1,e2,e3) ->
    405       let (v1,l1) = eval_expr localenv m e1 in
    406       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)
    407410      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)
    409412      else (v1,l1)
    410413    | Eandbool (e1,e2) ->
    411       let (v1,l1) = eval_expr localenv m e1 in
    412       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)
    413416      else (v1,l1)
    414417    | Eorbool (e1,e2) ->
    415       let (v1,l1) = eval_expr localenv m e1 in
    416       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)
    417420      else (v1,l1)
    418421    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
    419422    | Efield (e1,id) ->
    420       let ((v1,t1),l1) = eval_expr localenv m e1 in
     423      let ((v1,t1),l1) = eval_expr localenv m c e1 in
    421424      let addr = address_of_value (get_offset v1 id t1) in
    422425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
    423426    | 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
    425430      (v1,lbl::l1)
    426431    | Ecall _ -> assert false (* only used by the annotation process *)
    427432    | Ecast (cty,exp) ->
    428       let ((v,ty),l1) = eval_expr localenv m exp in
     433      let ((v,ty),l1) = eval_expr localenv m c exp in
    429434      ((eval_cast (v,ty,cty),tt),l1)
    430435
    431 and eval_lvalue localenv m (Expr (e,t)) = match e with
     436and eval_lvalue localenv m c (Expr (e,t)) = match e with
    432437  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
    433438  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
    … …  
    435440  | Evar id -> ((find_symbol localenv m id,t),[])
    436441  | Ederef ee ->
    437     let ((v,_),l1) = eval_expr localenv m ee in
     442    let ((v,_),l1) = eval_expr localenv m c ee in
    438443    ((address_of_value v,t),l1)
    439444  | Efield (ee,id) ->
    440     let ((v,tt),l1) = eval_expr localenv m ee in
     445    let ((v,tt),l1) = eval_expr localenv m c ee in
    441446    let v' = get_offset v id tt in
    442447    ((address_of_value v', t), l1)
    443448  | Ecost (lbl,ee) ->
    444     let (v,l) = eval_lvalue localenv m ee in
     449    let (v,l) = eval_lvalue localenv m c ee in
    445450    (v,lbl::l)
    446451  | Ecall _ -> assert false (* only used in the annotation process *)
    447452
    448 let eval_exprlist lenv mem es =
     453let eval_exprlist lenv mem c es =
    449454  let f (vs, cost_lbls) e =
    450     let ((v, _), cost_lbls') = eval_expr lenv mem e in
     455    let ((v, _), cost_lbls') = eval_expr lenv mem c e in
    451456    (vs @ [v], cost_lbls @ cost_lbls') in
    452457  List.fold_left f ([], []) es
    … …  
    480485  else error "undefined condition guard value."
    481486
    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 ->
     487let 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') ->
    486494                (* 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
    489504    let a_false = (State(f,Sskip,k,e,m,c),l1) in
    490     let a_true = (State(f,s,w,e,m,c),l1) in
     505    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    491506    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),[])
    501509  | Sskip, Kcall _ ->
    502510    let m' = free_local_env m e in
    503511    (Returnstate(Value.undef,k,m'),[])
    504512  | Sassign(a1, a2), _ ->
    505     let ((v1,t1),l1) = (eval_lvalue e m a1) in
    506     let ((v2,t2),l2) = eval_expr e m a2 in
    507     (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)
    508516  | Scall(None,a,al), _ ->
    509     let ((v1,_),l1) = eval_expr e m a in
     517    let ((v1,_),l1) = eval_expr e m c a in
    510518    let fd = Mem.find_fun_def m (address_of_value v1) in
    511     let (vargs,l2) = eval_exprlist e m al in
    512     (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)
    513521  | Scall(Some lhs,a,al), _ ->
    514     let ((v1,_),l1) = eval_expr e m a in
     522    let ((v1,_),l1) = eval_expr e m c a in
    515523    let fd = Mem.find_fun_def m (address_of_value v1) in
    516     let (vargs,l2) = eval_exprlist e m al in
    517     let (vt3,l3) = eval_lvalue e m lhs in
    518     (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),[])
    520528  | Sifthenelse(a,s1,s2), _ ->
    521     let ((v1,_),l1) = eval_expr e m a in
    522     let a_true = (State(f,s1,k,e,m),l1) in
    523     let a_false = (State(f,s2,k,e,m),l1) in
     529    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
    524532    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
    529538    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),[])
    531542  | Sfor(i,Sskip,a2,a3,s), _ ->
    532                 let c = enter_loop i c in
    533     let ((v1,_),l1) = eval_expr e m a2 in
     543                enter_loop i c;
     544    let ((v1,_),l1) = eval_expr e m c a2 in
    534545    let a_false = (State(f,Sskip,k,e,m,c),l1) in
    535546    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    536547    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),[])
    552554  | Sreturn None, _ ->
    553555    let m' = free_local_env m e in
    554556    (Returnstate(Value.undef,(call_cont k),m'),[])
    555557  | Sreturn (Some a), _ ->
    556     let ((v1,_),l1) = eval_expr e m a  in
     558    let ((v1,_),l1) = eval_expr e m c a  in
    557559    let m' = free_local_env m e in
    558560    (Returnstate(v1,call_cont k,m'),l1)
    559561  | Sswitch(a,sl), _ ->
    560     let ((v,_),l) = eval_expr e m a in
     562    let ((v,_),l) = eval_expr e m c a in
    561563    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])
    565570  | 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 *)
    566574    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),[])
    568576  | _ -> assert false (* should be impossible *)
    569577
    … …  
    582590  | Internal f ->
    583591    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)
    585596  | External(id,targs,tres) when List.length targs = List.length args ->
    586597    interpret_external cont mem id args
    … …  
    589600
    590601let step = function
    591   | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
     602  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
    592603  | 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) ->
    595606    let m' = assign m v ty vv in
    596     (State(f,Sskip,k,e,m'),[])
     607    (State(f,Sskip,k,e,m',c),[])
    597608  | _ -> error "state malformation."
    598609
    … …  
    633644    | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
    634645      print_and_return_result (compute_result v)
    635     | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
     646    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
    636647      print_and_return_result IntValue.Int32.zero
    637648    | state -> exec debug cost_labels (step state)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

    r1297 r1319  
    9999      let s2' = add_starting_cost_label ind cost_universe s2' in
    100100      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
    102105      let s' = add_cost_labels_st ind cost_universe s in
    103106      let s' = add_starting_cost_label ind cost_universe s' in
    104107      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
    110115      add_ending_cost_label ind cost_universe
    111         (Ssequence (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) ->
    113118      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
    114122      let s2' = add_cost_labels_st ind cost_universe s2 in
    115123      let s3' = add_cost_labels_st ind cost_universe s3 in
    116124      let s3' = add_starting_cost_label ind cost_universe s3' in
    117125      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'))
    119127  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
    120128  | Sswitch (e,ls) ->
    … …  
    162170  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
    163171  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
    164         let ind = CostLabel.id_indexing 0 in
     172        let ind = CostLabel.empty_indexing in
    165173  {
    166174    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  
    22open Clight
    33
    4 
     4(*
    55(* TODO: Alignment constraints? *)
    66let rec size_of_ctype = function
    … …  
    7272  | Tpointer (sp,_) | Tarray (sp,_,_) | Tcomp_ptr (sp,_) -> sp
    7373  | _ -> assert false (* do not use on those arguments *)
     74*)
     75
     76let 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  
    11
     2(*
    23val size_of_ctype : Clight.ctype -> int
    34
    … …  
    1314
    1415val 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 *)
     20val max_loop_index_lbld : Clight.statement -> int

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1310 r1319  
    1212let sexpr_id = Sexpr(1, 0)
    1313
     14let const_sexpr n = Sexpr(0, n)
     15
    1416type index = int
    1517
    … …  
    1820type indexing = sexpr list
    1921
    20 type const_indexing = int ref list
     22type const_indexing = int array
    2123
    2224(** [enter_loop n indexing] is used to update indexing when one is entering a
    2325    loop indexed by [n].
    2426                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 *)       
     27let rec enter_loop n indexing = match n with
     28        | None -> ()
     29        | Some x -> indexing.(x) <- 0
    3230
    3331(** [enter_loop n indexing] is used to update indexing when one is continuing a
    3432    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 *)       
     33let rec continue_loop n indexing = match n with
     34        | None -> ()
     35        | Some x -> indexing.(x) <- indexing.(x) + 1
    4136
    4237let sexpr_of i l =
    … …  
    4742      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
    4843
    49 let rec id_indexing = function
    50         | 0 -> []
    51         | n -> sexpr_id :: id_indexing (n-1)
     44let empty_indexing = []
     45
     46let add_id_indexing ind = sexpr_id :: ind
    5247
    5348(* a*_+b is composed with c*_+d by substitution: *)
    … …  
    7065        | _ -> n 
    7166
    72 let rec compose_const_indexing c m = match c, m with
    73         | i1 :: l1, s2 :: l2 -> ev_sexpr !i1 s2 :: compose_const_indexing l1 l2
    74         | _, [] -> [] (* that's ok as current indexings will not be shrinked *)
    75         | [], _ -> assert false (* means an indexed label is not in the right ctx *)
     67let 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
    7671
    7772module IndexingSet = Set.Make(struct
    … …  
    8075        end)
    8176
    82 
    8377type t = {
    8478    name : Atom.t;
    8579    i : indexing
    8680}
     81
     82let apply_const_indexing c lbl =
     83    {lbl with i = compose_const_indexing_i 0 c lbl.i}
    8784
    8885

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

    r1310 r1319  
    2121type indexing = sexpr list
    2222
    23 type const_indexing = int ref list
     23type const_indexing = int array
    2424
    2525(** [enter_loop n indexing] is used to update indexing when one is entering a
    2626    loop indexed by [n].
    2727        The function recycles the same constant indexing *)
    28 val enter_loop : index option -> const_indexing -> const_indexing
     28val enter_loop : index option -> const_indexing -> unit
    2929
    3030(** [continue_loop n indexing] is used to update indexing when one is continuing a
    3131    loop indexed by [n]. *)
    32 val continue_loop : index option -> const_indexing -> const_indexing
     32val continue_loop : index option -> const_indexing -> unit
    3333
    34 (** [id_indexing n] generates an identity indexing nested in [n] loops *)
    35 val id_indexing : int -> indexing
     34(** [empty_indexing] generates an empty indexing *)
     35val empty_indexing : indexing
    3636
    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 **)
     38val add_id_indexing : indexing -> indexing
    4439
    4540module IndexingSet : Set.S with type elt = indexing
    … …  
    4944        i : indexing
    5045}
     46
     47val apply_const_indexing : const_indexing -> t -> t
     48
    5149
    5250(** [string_of_cost_label pref t] converts an indexed label to a
Note: See TracChangeset for help on using the changeset viewer.