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

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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)
Note: See TracChangeset for help on using the changeset viewer.