Ignore:
Timestamp:
Oct 11, 2011, 5:42:20 PM (9 years ago)
Author:
tranquil
Message:
  • changed implementation of constant indexings with extensible arrays
  • work on ASM completed
  • next: optimizations!
File:
1 edited

Legend:

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

    r1345 r1357  
    3232  | Kfor3 of int option*expr*statement*statement*continuation
    3333  | Kswitch of continuation
    34   | Kcall of (Value.address*ctype) option*cfunction*localEnv*
    35         indexing*continuation
     34  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    3635
    3736type state =
    38   | State of cfunction*statement*continuation*localEnv*memory*indexing
    39   | Callstate of fundef*Value.t list*continuation*memory
    40   | Returnstate of Value.t*continuation*memory
     37  | State of cfunction*statement*continuation*localEnv*memory*indexing list
     38  | Callstate of fundef*Value.t list*continuation*memory*indexing list
     39  | Returnstate of Value.t*continuation*memory*indexing list
    4140
    4241let string_of_unop = function
     
    157156      (string_of_local_env lenv)
    158157      (Mem.to_string mem);
    159                 Array.iteri (fun a -> Printf.printf "%d,") c;
     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)
    162   | Callstate (_, args, _, mem) ->
     162  | Callstate (_, args, _, mem, _) ->
    163163    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    164164      (Mem.to_string mem)
    165165      (MiscPottier.string_of_list " " Value.to_string args)
    166   | Returnstate (v, _, mem) ->
     166  | Returnstate (v, _, mem, _) ->
    167167    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    168168      (Mem.to_string mem)
     
    427427    | Ecost (lbl,e1) ->
    428428                        (* applying current indexing on label *)
    429                         let lbl = CostLabel.apply_const_indexing c lbl in
     429                        let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    430430      let (v1,l1) = eval_expr localenv m c e1 in
    431431      (v1,lbl::l1)
     
    492492  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
    493493                (* possibly continuing a loop *)
    494                 CostLabel.continue_loop i c; (* if loop is not continued, this change
     494                CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
    495495                                                will have no effect in the following. *)
    496496    let ((v1,_),l1) = eval_expr e m c a in
     
    499499    condition v1 a_true a_false
    500500  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
    501     CostLabel.continue_loop i c;
     501    CostLabel.continue_loop_opt c i;
    502502    let ((v1,_),l1) = eval_expr e m c a2 in
    503503    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    508508  | Sskip, Kcall _ ->
    509509    let m' = free_local_env m e in
    510     (Returnstate(Value.undef,k,m'),[])
     510    (Returnstate(Value.undef,k,m',c),[])
    511511  | Sassign(a1, a2), _ ->
    512512    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
     
    517517    let fd = Mem.find_fun_def m (address_of_value v1) in
    518518    let (vargs,l2) = eval_exprlist e m c al in
    519     (Callstate(fd,vargs,Kcall(None,f,e,c,k),m),l1@l2)
     519    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
    520520  | Scall(Some lhs,a,al), _ ->
    521521    let ((v1,_),l1) = eval_expr e m c a in
     
    523523    let (vargs,l2) = eval_exprlist e m c al in
    524524    let (vt3,l3) = eval_lvalue e m c lhs in
    525     (Callstate(fd,vargs,Kcall(Some vt3,f,e,c,k),m),l1@l2@l3)
     525    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
    526526  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
    527527  | Sifthenelse(a,s1,s2), _ ->
     
    531531    condition v1 a_true a_false
    532532  | Swhile(i,a,s), _ ->
    533                 CostLabel.enter_loop i c;
     533                CostLabel.enter_loop_opt c i;
    534534    let ((v1,_),l1) = eval_expr e m c a in
    535535    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    537537    condition v1 a_true a_false
    538538  | Sdowhile(i,a,s), _ ->
    539                 CostLabel.enter_loop i c;
     539                CostLabel.enter_loop_opt c i;
    540540                (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
    541541  | Sfor(i,Sskip,a2,a3,s), _ ->
    542                 CostLabel.enter_loop i c;
     542                CostLabel.enter_loop_opt c i;
    543543    let ((v1,_),l1) = eval_expr e m c a2 in
    544544    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    553553  | Sreturn None, _ ->
    554554    let m' = free_local_env m e in
    555     (Returnstate(Value.undef,(call_cont k),m'),[])
     555    (Returnstate(Value.undef,(call_cont k),m',c),[])
    556556  | Sreturn (Some a), _ ->
    557557    let ((v1,_),l1) = eval_expr e m c a  in
    558558    let m' = free_local_env m e in
    559     (Returnstate(v1,call_cont k,m'),l1)
     559    (Returnstate(v1,call_cont k,m',c),l1)
    560560  | Sswitch(a,sl), _ ->
    561561    let ((v,_),l) = eval_expr e m c a in
     
    565565  | Scost(lbl,s), _ ->
    566566                (* applying current indexing on label *)
    567                 let lbl = CostLabel.apply_const_indexing c lbl in
     567                let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    568568                (State(f,s,k,e,m,c),[lbl])
    569569  | Sgoto lbl, _ ->
     
    578578module InterpretExternal = Primitive.Interpret (Mem)
    579579
    580 let interpret_external k mem f args =
     580let interpret_external k mem c f args =
    581581  let (mem', v) = match InterpretExternal.t mem f args with
    582582    | (mem', InterpretExternal.V vs) ->
     
    584584      (mem', v)
    585585    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    586   Returnstate (v, k, mem')
    587 
    588 let step_call args cont mem = function
     586  Returnstate (v, k, mem',c)
     587
     588let step_call args cont mem c = function
    589589  | Internal f ->
    590590    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    591591                (* initializing loop indices *)
    592                 let max_depth = ClightUtils.max_loop_index_lbld f.fn_body in
    593                 let c = Array.make max_depth 0 in
     592                let c = CostLabel.new_const_ind c in
    594593    State (f, f.fn_body, cont, e, mem', c)
    595594  | External(id,targs,tres) when List.length targs = List.length args ->
    596     interpret_external cont mem id args
     595    interpret_external cont mem c id args
    597596  | External(id,_,_) ->
    598597    error ("wrong size of arguments when calling external " ^ id ^ ".")
     
    600599let step = function
    601600  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
    602   | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    603   | Returnstate(v,Kcall(None,f,e,c,k),m) -> (State(f,Sskip,k,e,m,c),[])
    604   | Returnstate(v,Kcall((Some(vv, ty)),f,e,c,k),m) ->
     601  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
     602  | 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),[])
     605  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
     606    let c = CostLabel.forget_const_ind c in
    605607    let m' = assign m v ty vv in
    606608    (State(f,Sskip,k,e,m',c),[])
     
    641643  if debug then print_state state ;
    642644  match state with
    643     | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     645    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
    644646      print_and_return_result (compute_result v)
    645647    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
     
    653655    | Some main ->
    654656      let mem = init_mem prog in
    655       let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     657      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
    656658      exec debug [] first_state
Note: See TracChangeset for help on using the changeset viewer.