Ignore:
Timestamp:
Nov 23, 2011, 1:55:12 PM (9 years ago)
Author:
tranquil
Message:

branch up to date

File:
1 edited

Legend:

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

    r1357 r1539  
    106106  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
    107107  | Ecost (cost_lbl, e) ->
    108                 let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
    109                 "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     108    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
     109    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
    110110  | Ecall (f, arg, e) ->
    111111    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
     
    151151  LocalEnv.fold f lenv ""
    152152
    153 let print_state state = (match state with
     153let print_state state = match state with
    154154  | State (_, stmt, _, lenv, mem, c) ->
    155155    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
    156156      (string_of_local_env lenv)
    157157      (Mem.to_string mem);
    158                 let i = CostLabel.curr_const_ind c in
    159                 CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     158    let i = CostLabel.curr_const_ind c in
     159    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
    160160    Printf.printf "\nRegular state: %s\n\n%!"
    161161      (string_of_statement stmt)
     
    168168      (Mem.to_string mem)
    169169      (Value.to_string v)
    170         ); Printf.printf "---------------------------------------------------------\n"
    171170
    172171
     
    426425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
    427426    | Ecost (lbl,e1) ->
    428                         (* applying current indexing on label *)
    429                         let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     427      (* applying current indexing on label *)
     428      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    430429      let (v1,l1) = eval_expr localenv m c e1 in
    431430      (v1,lbl::l1)
     
    486485  else error "undefined condition guard value."
    487486
    488 let eval_stmt f k e m s c =
    489         match s, k with
     487let eval_stmt f k e m s c = match s, k with
    490488  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
    491489  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
    492490  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
    493                 (* possibly continuing a loop *)
    494                 CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
    495                                                 will have no effect in the following. *)
     491    (* possibly continuing a loop *)
     492    CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
     493                                        will have no effect in the following. *)
    496494    let ((v1,_),l1) = eval_expr e m c a in
    497495    let a_false = (State(f,Sskip,k',e,m,c),l1) in
     
    504502    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    505503    condition v1 a_true a_false
    506   | Sskip, Kfor2(i,a2,a3,s,k) -> (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
     504  | Sskip, Kfor2(i,a2,a3,s,k) ->
     505    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
    507506  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    508507  | Sskip, Kcall _ ->
     
    531530    condition v1 a_true a_false
    532531  | Swhile(i,a,s), _ ->
    533                 CostLabel.enter_loop_opt c i;
     532    CostLabel.enter_loop_opt c i;
    534533    let ((v1,_),l1) = eval_expr e m c a in
    535534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    537536    condition v1 a_true a_false
    538537  | Sdowhile(i,a,s), _ ->
    539                 CostLabel.enter_loop_opt c i;
    540                 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
     538    CostLabel.enter_loop_opt c i;
     539    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
    541540  | Sfor(i,Sskip,a2,a3,s), _ ->
    542                 CostLabel.enter_loop_opt c i;
     541    CostLabel.enter_loop_opt c i;
    543542    let ((v1,_),l1) = eval_expr e m c a2 in
    544543    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    548547  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
    549548  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
    550         | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
     549  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    551550  | Scontinue, Kseq(_,k)
    552         | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
     551  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
    553552  | Sreturn None, _ ->
    554553    let m' = free_local_env m e in
     
    561560    let ((v,_),l) = eval_expr e m c a in
    562561    let n = Value.to_int v in
    563     (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
     562  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
    564563  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
    565564  | Scost(lbl,s), _ ->
    566                 (* applying current indexing on label *)
    567                 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    568                 (State(f,s,k,e,m,c),[lbl])
     565    (* applying current indexing on label *)
     566    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     567    (State(f,s,k,e,m,c),[lbl])
    569568  | Sgoto lbl, _ ->
    570                 (* if we exit an indexed loop, we don't care. It should not be possible to*)
    571                 (* enter an indexed loop that is not the current one, so we do nothing*)
    572                 (* to loop indexes *)
     569    (* if we exit an indexed loop, we don't care. It should not be possible to *)
     570    (* enter an indexed loop that is not the current one, so we do nothing *)
     571    (* to loop indexes *)
    573572    let (s', k') = find_label lbl f.fn_body (call_cont k) in
    574573    (State(f,s',k',e,m,c),[])
     
    589588  | Internal f ->
    590589    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    591                 (* initializing loop indices *)
    592                 let c = CostLabel.new_const_ind c in
     590    (* initializing loop indices *)
     591    let c = CostLabel.new_const_ind c in
    593592    State (f, f.fn_body, cont, e, mem', c)
    594593  | External(id,targs,tres) when List.length targs = List.length args ->
     
    601600  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
    602601  | 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),[])
     602    let c = CostLabel.forget_const_ind c in
     603    (State(f,Sskip,k,e,m,c),[])
    605604  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
    606605    let c = CostLabel.forget_const_ind c in
Note: See TracChangeset for help on using the changeset viewer.