Ignore:
Timestamp:
Oct 10, 2011, 2:17:02 PM (8 years ago)
Author:
tranquil
Message:

work on Cminor completed

File:
1 edited

Legend:

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

    r1291 r1334  
    2323(* State of execution *)
    2424
     25type indexing = CostLabel.const_indexing
     26
    2527type continuation =
    2628    Ct_stop
    2729  | Ct_cont of statement*continuation
     30        | Ct_ind_inc of CostLabel.index*continuation
    2831  | Ct_endblock of continuation
    2932  | Ct_returnto of
    30       ident option*internal_function*Val.address*local_env*continuation
     33      ident option*internal_function*Val.address*local_env*indexing*continuation
    3134
    3235type state =
    3336    State_regular of
    34       internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
     37      internal_function*statement*continuation*Val.address*local_env*
     38                         (function_def Mem.memory)*indexing
    3539  | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
    3640  | State_return of Val.t*continuation*(function_def Mem.memory)
     
    6872                let lbl = CostLabel.string_of_cost_label lbl in
    6973                "cost " ^ lbl
     74        | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0"
     75        | St_ind_inc (_, i) -> "post-increment " ^ string_of_int i
    7076
    7177let print_state = function
    72   | State_regular (_, stmt, _, sp, lenv, mem) ->
    73     Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!"
     78  | State_regular (_, stmt, _, sp, lenv, mem, i) ->
     79    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:"
    7480      (string_of_local_env lenv)
    7581      (Mem.to_string mem)
    76       (Val.to_string (value_of_address sp))
     82      (Val.to_string (value_of_address sp));
     83                        Array.iter (fun a -> Printf.printf "%d, " a) i;
     84                        Printf.printf "\nRegular state: %s\n\n%!"
    7785      (string_of_statement stmt)
    7886  | State_call (_, args, _, mem) ->
     
    223231
    224232let rec callcont = function
    225     Ct_stop                     -> Ct_stop
    226   | Ct_cont(_,k)                -> callcont k
    227   | Ct_endblock(k)              -> callcont k
    228   | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
     233  | Ct_cont(_,k) | Ct_endblock k | Ct_ind_inc(_,k) -> callcont k
     234        | (Ct_stop | Ct_returnto _) as k -> k
    229235
    230236let findlabel lbl st k =
     
    252258  | St_label(l,s)               -> if l=lbl then Some((s,k)) else None
    253259  | St_goto(_)                  -> None
    254   | St_cost (_,s)               -> fdlbl k s
     260  | St_cost (_,s) | St_ind_0(_,s) | St_ind_inc(s,_) -> fdlbl k s
    255261  in match fdlbl k st with
    256262      None -> assert false (*Wrong label*)
     
    264270  (State_call(fun_def,args,cont,m),l1@l2)
    265271
    266 let eval_stmt f k sigma e m s = match s, k with
    267   | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
    268   | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
     272let eval_stmt f k sigma e m i s = match s, k with
     273  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[])
     274  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[])
    269275  | St_skip, (Ct_returnto _ as k) ->
    270276    (State_return (Val.undef,k,Mem.free m sigma),[])
     277  | St_skip,Ct_ind_inc(ind,k) ->
     278                CostLabel.continue_loop (Some ind) i;
     279                (State_regular(f, s, k, sigma, e, m, i),[])
    271280  | St_skip,Ct_stop ->
    272281    (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
     
    274283    let (v,l) = eval_expression sigma e m exp in
    275284    let e = LocalEnv.add x v e in
    276     (State_regular(f, St_skip, k, sigma, e, m),l)
     285    (State_regular(f, St_skip, k, sigma, e, m, i),l)
    277286  | St_store(q,a1,a2),_ ->
    278287    let (v1,l1) = eval_expression sigma e m a1 in
    279288    let (v2,l2) = eval_expression sigma e m a2 in
    280289    let m = Mem.storeq m q (address_of_value v1) v2 in
    281     (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
     290    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
    282291  | St_call(xopt,f',params,_),_ ->
    283     call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
     292    call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,i,k))
    284293  | St_tailcall(f',params,_),_ ->
    285294    call_state sigma e m f' params (callcont k)
    286   | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
     295  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
    287296  | St_ifthenelse(exp,s1,s2),_ ->
    288297    let (v,l) = eval_expression sigma e m exp in
     
    292301        if Val.is_false v then s2
    293302        else error "undefined conditional value." in
    294       (State_regular(f,next_stmt,k,sigma,e,m),l)
    295   | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
    296   | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
    297   | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
    298   | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
     303      (State_regular(f,next_stmt,k,sigma,e,m,i),l)
     304  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[])
     305  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[])
     306  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[])
     307  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[])
    299308  | St_exit(n),Ct_endblock(k) ->
    300     (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
    301   | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
     309    (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[])
     310  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[])
    302311  | St_goto(lbl),_ ->
    303312    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
    304     (State_regular(f,s2,k2,sigma,e,m),[])
     313    (State_regular(f,s2,k2,sigma,e,m,i),[])
    305314  | St_switch(exp,lst,def),_ ->
    306315    let (v,l) = eval_expression sigma e m exp in
    307316    if Val.is_int v then
    308317      try
    309         let i = Val.to_int v in
     318        let v = Val.to_int v in
    310319        let nb_exit =
    311           if List.mem_assoc i lst then List.assoc i lst
     320          if List.mem_assoc v lst then List.assoc v lst
    312321          else def in
    313         (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
     322        (State_regular(f, St_exit nb_exit,k, sigma, e, m, i),l)
    314323      with _ -> error "int value too big."
    315324    else error "undefined switch value."
     
    319328      let (v,l) = eval_expression sigma e m a in
    320329      (State_return (v,callcont k,Mem.free m sigma),l)
    321   | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
     330  | St_cost(lbl,s),_ ->
     331    (* applying current indexing on label *)
     332    let lbl = CostLabel.apply_const_indexing i lbl in
     333                (State_regular(f,s,k,sigma,e,m,i),[lbl])
     334        | St_ind_0(ind,s),_ ->
     335                CostLabel.enter_loop (Some ind) i;
     336                (State_regular(f,s,k,sigma,e,m,i), [])
     337        | St_ind_inc(s,ind),_ ->
     338    (State_regular(f,s,Ct_ind_inc(ind,k),sigma,e,m,i), [])
    322339  | _ -> error "state malformation."
    323340
     
    333350  State_return (v, k, mem')
    334351
     352let max_loop_index =
     353  let f_expr _ _ = () in
     354  let f_stmt stmt _ sub_stmts_res =
     355        let curr_max = List.fold_left max 0 sub_stmts_res in
     356        match stmt with
     357          | Cminor.St_ind_0 (x, _) | Cminor.St_ind_inc (_, x) ->
     358                                                 max (x+1) curr_max
     359          | _ -> curr_max in
     360  CminorFold.statement f_expr f_stmt
     361
    335362let step_call vargs k m = function
    336363  | F_int f ->
    337364    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    338365    let lenv = init_local_env vargs f.f_params f.f_vars in
    339     State_regular(f,f.f_body,k,sp,lenv,m)
     366                let i = Array.make (max_loop_index f.f_body) 0 in
     367    State_regular(f,f.f_body,k,sp,lenv,m,i)
    340368  | F_ext f -> interpret_external k m f.ef_tag vargs
    341369
    342370let step = function
    343   | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
     371  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
    344372  | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    345   | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
    346     (State_regular(f,St_skip,k,sigma,e,m),[])
    347   | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
     373  | State_return(v,Ct_returnto(None,f,sigma,e,i,k),m) ->
     374    (State_regular(f,St_skip,k,sigma,e,m,i),[])
     375  | State_return(v,Ct_returnto(Some x,f,sigma,e,i,k),m) ->
    348376    let e = LocalEnv.add x v e in
    349     (State_regular(f,St_skip,k,sigma,e,m),[])
     377    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    350378  | _ -> error "state malformation."
    351379
     
    371399    | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
    372400      print_and_return_result (compute_result v)
    373     | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
     401    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
    374402      print_and_return_result IntValue.Int32.zero
    375403    | state -> exec debug cost_labels (step state)
Note: See TracChangeset for help on using the changeset viewer.