Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (9 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

    r1462 r1542  
    2323(* State of execution *)
    2424
     25type indexing = CostLabel.const_indexing
     26
    2527type continuation =
    2628    Ct_stop
    2729  | Ct_cont of statement*continuation
    28   | Ct_endblock of continuation
     30(*  | Ct_endblock of continuation *)
    2931  | Ct_returnto of
    3032      ident option*internal_function*Val.address*local_env*continuation
     
    3234type state =
    3335    State_regular of
    34       internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
    35   | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
    36   | State_return of Val.t*continuation*(function_def Mem.memory)
     36      internal_function*statement*continuation*Val.address*local_env*
     37                         (function_def Mem.memory)*indexing list
     38  | State_call of function_def*Val.t list*continuation*
     39             (function_def Mem.memory)*indexing list
     40  | State_return of Val.t*continuation*(function_def Mem.memory)*indexing list
    3741
    3842let string_of_local_env lenv =
     
    5761  | St_seq _ -> "sequence"
    5862  | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
    59   | St_loop _ -> "loop"
     63(*  | St_loop _ -> "loop"
    6064  | St_block _ -> "block"
    61   | St_exit n -> "exit " ^ (string_of_int n)
     65  | St_exit n -> "exit " ^ (string_of_int n) *)
    6266  | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
    6367  | St_return None -> "return"
     
    6569  | St_label (lbl, _) -> "label " ^ lbl
    6670  | St_goto lbl -> "goto " ^ lbl
    67   | St_cost (lbl, _) -> "cost " ^ lbl
     71  | St_cost (lbl, _) ->
     72    let lbl = CostLabel.string_of_cost_label lbl in
     73    "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
    6876
    6977let print_state = function
    70   | State_regular (_, stmt, _, sp, lenv, mem) ->
    71     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:"
    7280      (string_of_local_env lenv)
    7381      (Mem.to_string mem)
    74       (Val.to_string (value_of_address sp))
     82      (Val.to_string (value_of_address sp));
     83    let ind = CostLabel.curr_const_ind i in
     84    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) ind;
     85    Printf.printf "\nRegular state: %s\n\n%!"
    7586      (string_of_statement stmt)
    76   | State_call (_, args, _, mem) ->
     87  | State_call (_, args, _, mem,_) ->
    7788    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    7889      (Mem.to_string mem)
    7990      (MiscPottier.string_of_list " " Val.to_string args)
    80   | State_return (v, _, mem) ->
     91  | State_return (v, _, mem,_) ->
    8192    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    8293      (Mem.to_string mem)
     
    221232
    222233let rec callcont = function
    223     Ct_stop                     -> Ct_stop
    224   | Ct_cont(_,k)                -> callcont k
    225   | Ct_endblock(k)              -> callcont k
    226   | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
     234  | Ct_cont(_,k) (*| Ct_endblock k *) -> callcont k
     235  | (Ct_stop | Ct_returnto _) as k -> k
    227236
    228237let findlabel lbl st k =
     
    243252         | Some(v) -> Some(v)
    244253      )
    245   | St_loop(s)                     -> fdlbl (Ct_cont(St_loop(s),k)) s
    246   | St_block(s)                    -> fdlbl (Ct_endblock(k)) s
    247   | St_exit(_)                     -> None
    248   | St_switch(_,_,_)               -> None
    249   | St_return(_)                   -> None
    250   | St_label(l,s) when l = lbl     -> Some((s,k))
    251   | St_goto(_)                     -> None
    252   | St_cost (_,s) | St_label (_,s) -> fdlbl k s
     254(*  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
     255  | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
     256  | St_exit(_)                  -> None *)
     257  | St_switch(_,_,_)            -> None
     258  | St_return(_)                -> None
     259  | St_label(l,s) when l = lbl  -> Some((s,k))
     260  | St_goto(_)                  -> None
     261  | St_cost(_,s)  | St_label(_,s)
     262  | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s
    253263  in match fdlbl k st with
    254264      None -> assert false (*Wrong label*)
     
    256266
    257267
    258 let call_state sigma e m f params cont =
     268let call_state sigma e m i f params cont =
    259269  let (addr,l1) = eval_expression sigma e m f in
    260270  let fun_def = Mem.find_fun_def m (address_of_value addr) in
    261271  let (args,l2) = eval_exprlist sigma e m params in
    262   (State_call(fun_def,args,cont,m),l1@l2)
    263 
    264 let eval_stmt f k sigma e m s = match s, k with
    265   | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
    266   | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
     272  (State_call(fun_def,args,cont,m,i),l1@l2)
     273
     274let eval_stmt f k sigma e m i s = match s, k with
     275  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[])
     276(*  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[]) *)
    267277  | St_skip, (Ct_returnto _ as k) ->
    268     (State_return (Val.undef,k,Mem.free m sigma),[])
     278    (State_return (Val.undef,k,Mem.free m sigma,i),[])
    269279  | St_skip,Ct_stop ->
    270     (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
     280    (State_return (Val.undef,Ct_stop,Mem.free m sigma,i),[])
    271281  | St_assign(x,exp),_ ->
    272282    let (v,l) = eval_expression sigma e m exp in
    273283    let e = LocalEnv.add x v e in
    274     (State_regular(f, St_skip, k, sigma, e, m),l)
     284    (State_regular(f, St_skip, k, sigma, e, m, i),l)
    275285  | St_store(q,a1,a2),_ ->
    276286    let (v1,l1) = eval_expression sigma e m a1 in
    277287    let (v2,l2) = eval_expression sigma e m a2 in
    278288    let m = Mem.storeq m q (address_of_value v1) v2 in
    279     (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
     289    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
    280290  | St_call(xopt,f',params,_),_ ->
    281     call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
     291    call_state sigma e m i f' params (Ct_returnto(xopt,f,sigma,e,k))
    282292  | St_tailcall(f',params,_),_ ->
    283     call_state sigma e m f' params (callcont k)
    284   | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
     293    call_state sigma e m i f' params (callcont k)
     294  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
    285295  | St_ifthenelse(exp,s1,s2),_ ->
    286296    let (v,l) = eval_expression sigma e m exp in
     
    290300        if Val.is_false v then s2
    291301        else error "undefined conditional value." in
    292       (State_regular(f,next_stmt,k,sigma,e,m),l)
    293   | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
    294   | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
    295   | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
    296   | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
     302      (State_regular(f,next_stmt,k,sigma,e,m,i),l)
     303(*  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[])
     304  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[])
     305  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[])
     306  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[])
    297307  | St_exit(n),Ct_endblock(k) ->
    298     (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
    299   | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
    300   | St_goto(lbl),_ -> 
     308    (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[]) *)
     309  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[])
     310  | St_goto(lbl),_ ->
    301311    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
    302     (State_regular(f,s2,k2,sigma,e,m),[])
     312    (State_regular(f,s2,k2,sigma,e,m,i),[])
    303313  | St_switch(exp,lst,def),_ ->
    304314    let (v,l) = eval_expression sigma e m exp in
    305315    if Val.is_int v then
    306316      try
    307         let i = Val.to_int v in
    308         let nb_exit =
    309           if List.mem_assoc i lst then List.assoc i lst
    310           else def in
    311         (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
     317        let v = Val.to_int v in
     318        let lbl =
     319          try
     320            List.assoc v lst
     321          with
     322            | Not_found -> def in
     323        let (s',k') = findlabel lbl f.f_body (callcont k) in
     324        (State_regular(f, s', k', sigma, e, m, i),l)
    312325      with _ -> error "int value too big."
    313326    else error "undefined switch value."
    314327  | St_return(None),_ ->
    315     (State_return (Val.undef,callcont k,Mem.free m sigma),[])
     328    (State_return (Val.undef,callcont k,Mem.free m sigma,i),[])
    316329  | St_return(Some(a)),_ ->
    317330      let (v,l) = eval_expression sigma e m a in
    318       (State_return (v,callcont k,Mem.free m sigma),l)
    319   | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
    320   | _ -> error "state malformation."
     331      (State_return (v,callcont k,Mem.free m sigma,i),l)
     332  | St_cost(lbl,s),_ ->
     333    (* applying current indexing on label *)
     334    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in
     335    (State_regular(f,s,k,sigma,e,m,i),[lbl])
     336  | St_ind_0(ind,s),_ ->
     337    CostLabel.enter_loop i ind;
     338    (State_regular(f,s,k,sigma,e,m,i), [])
     339  | St_ind_inc(ind,s),_ ->
     340    CostLabel.continue_loop i ind;
     341    (State_regular(f,s,k,sigma,e,m,i), [])
     342(*  | _ -> error "state malformation." *)
    321343
    322344
    323345module InterpretExternal = Primitive.Interpret (Mem)
    324346
    325 let interpret_external k mem f args =
     347let interpret_external k mem i f args =
    326348  let (mem', v) = match InterpretExternal.t mem f args with
    327349    | (mem', InterpretExternal.V vs) ->
     
    329351      (mem', v)
    330352    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    331   State_return (v, k, mem')
    332 
    333 let step_call vargs k m = function
     353  State_return (v, k, mem', i)
     354
     355let step_call vargs k m i = function
    334356  | F_int f ->
    335357    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    336358    let lenv = init_local_env vargs f.f_params f.f_vars in
    337     State_regular(f,f.f_body,k,sp,lenv,m)
    338   | F_ext f -> interpret_external k m f.ef_tag vargs
     359    let i = CostLabel.new_const_ind i in
     360    State_regular(f,f.f_body,k,sp,lenv,m,i)
     361  | F_ext f -> interpret_external k m i f.ef_tag vargs
    339362
    340363let step = function
    341   | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
    342   | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    343   | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
    344     (State_regular(f,St_skip,k,sigma,e,m),[])
    345   | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
     364  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
     365  | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[])
     366  | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) ->
     367    let i = CostLabel.forget_const_ind i in
     368    (State_regular(f,St_skip,k,sigma,e,m,i),[])
     369  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) ->
    346370    let e = LocalEnv.add x v e in
    347     (State_regular(f,St_skip,k,sigma,e,m),[])
     371    let i = CostLabel.forget_const_ind i in
     372    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    348373  | _ -> error "state malformation."
    349374
     
    364389    if debug then Printf.printf "Result = %s\n%!"
    365390      (IntValue.Int32.to_string res) ;
    366     (res, cost_labels) in
     391    (res, List.rev cost_labels) in
    367392  if debug then print_state state ;
    368393  match state with
    369     | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
     394    | State_return(v,Ct_stop,_,_) -> (* Explicit return in main *)
    370395      print_and_return_result (compute_result v)
    371     | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
     396    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
    372397      print_and_return_result IntValue.Int32.zero
    373398    | state -> exec debug cost_labels (step state)
     
    379404    | Some main ->
    380405      let mem = init_mem prog in
    381       let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
     406      let main = find_fundef main mem in
     407      let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in
    382408      exec debug [] first_state
Note: See TracChangeset for help on using the changeset viewer.