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/clight/clightInterpret.ml

    r818 r1542  
    44type localEnv = Value.address LocalEnv.t
    55type memory = Clight.fundef Mem.memory
     6type indexing = CostLabel.const_indexing
    67
    78open Clight
     
    2627  | Kstop
    2728  | Kseq of statement*continuation
    28   | Kwhile of expr*statement*continuation
    29   | Kdowhile of expr*statement*continuation
    30   | Kfor2 of expr*statement*statement*continuation
    31   | Kfor3 of expr*statement*statement*continuation
     29  | Kwhile of int option*expr*statement*continuation
     30  | Kdowhile of int option*expr*statement*continuation
     31  | Kfor2 of int option*expr*statement*statement*continuation
     32  | Kfor3 of int option*expr*statement*statement*continuation
    3233  | Kswitch of continuation
    3334  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    3435
    3536type state =
    36   | State of cfunction*statement*continuation*localEnv*memory
    37   | Callstate of fundef*Value.t list*continuation*memory
    38   | 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
    3940
    4041let string_of_unop = function
     
    104105  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
    105106  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
    106   | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     107  | Ecost (cost_lbl, e) ->
     108    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
     109    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
    107110  | Ecall (f, arg, e) ->
    108111    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
     
    110113let string_of_args args =
    111114  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
     115
     116let string_of_loop_depth = function
     117        | None -> ""
     118        | Some d -> " at " ^ string_of_int d
    112119
    113120let rec string_of_statement = function
     
    119126  | Ssequence _ -> "sequence"
    120127  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
    121   | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
    122   | Sdowhile _ -> "dowhile"
    123   | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
     128  | Swhile (i, e, _) ->
     129                let d = string_of_loop_depth i in
     130                "while" ^ d ^ " (" ^ (string_of_expr e) ^ ")"
     131  | Sdowhile (i, _, _) ->
     132    let d = string_of_loop_depth i in
     133    "dowhile" ^ d
     134  | Sfor (i, s, _, _, _) ->
     135                let d = string_of_loop_depth i in
     136                "for" ^ d ^ " (" ^ (string_of_statement s) ^ "; ...)"
    124137  | Sbreak -> "break"
    125138  | Scontinue -> "continue"
     
    129142  | Slabel (lbl, _) -> "label " ^ lbl
    130143  | Sgoto lbl -> "goto " ^ lbl
    131   | Scost (lbl, _) -> "cost " ^ lbl
     144  | Scost (lbl, _) ->
     145    let lbl = CostLabel.string_of_cost_label lbl in
     146                "cost " ^ lbl
    132147
    133148let string_of_local_env lenv =
     
    136151  LocalEnv.fold f lenv ""
    137152
    138 let print_state = function
    139   | State (_, stmt, _, lenv, mem) ->
    140     Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     153let print_state state = match state with
     154  | State (_, stmt, _, lenv, mem, c) ->
     155    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
    141156      (string_of_local_env lenv)
    142       (Mem.to_string mem)
     157      (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;
     160    Printf.printf "\nRegular state: %s\n\n%!"
    143161      (string_of_statement stmt)
    144   | Callstate (_, args, _, mem) ->
     162  | Callstate (_, args, _, mem, _) ->
    145163    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    146164      (Mem.to_string mem)
    147165      (MiscPottier.string_of_list " " Value.to_string args)
    148   | Returnstate (v, _, mem) ->
     166  | Returnstate (v, _, mem, _) ->
    149167    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    150168      (Mem.to_string mem)
     
    155173
    156174let rec call_cont = function
    157   | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
    158   | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
     175  | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k)
     176  | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k
    159177  | k -> k
    160178
     
    174192      | None -> find_label1 lbl s2 k
    175193      )
    176   | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
    177   | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
    178   | Sfor (a1,a2,a3,s1) ->
    179       (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
     194  | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k))
     195  | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k))
     196  | Sfor (i,a1,a2,a3,s1) ->
     197                (* doubt: should we search for labels in a1? *)
     198      (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with
    180199      | Some sk -> Some sk
    181200      | None ->
    182           (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
     201          (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with
    183202          | Some sk -> Some sk
    184           | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
     203          | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k))
    185204          ))
    186205  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
     
    355374let is_false (v, _) = Value.is_false v
    356375
    357 let rec eval_expr localenv m (Expr (ee, tt)) =
     376let rec eval_expr localenv m c (Expr (ee, tt)) =
    358377  match ee with
    359378    | Econst_int i ->
     
    369388      ((v, tt), [])
    370389    | Ederef e when is_function_type tt || is_big_type tt ->
    371       let ((v1,_),l1) = eval_expr localenv m e in
     390      let ((v1,_),l1) = eval_expr localenv m c e in
    372391      ((v1,tt),l1)
    373392    | Ederef e ->
    374       let ((v1,_),l1) = eval_expr localenv m e in
     393      let ((v1,_),l1) = eval_expr localenv m c e in
    375394      let addr = address_of_value v1 in
    376395      let v = Mem.load m (size_of_ctype tt) addr in
    377396      ((v,tt),l1)
    378397    | Eaddrof exp ->
    379       let ((addr,_),l) = eval_lvalue localenv m exp in
     398      let ((addr,_),l) = eval_lvalue localenv m c exp in
    380399      ((value_of_address addr,tt),l)
    381400    | Ebinop (op,exp1,exp2) -> 
    382       let (v1,l1) = eval_expr localenv m exp1 in
    383       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
    384403      ((eval_binop tt v1 v2 op,tt),l1@l2)
    385404    | Eunop (op,exp) ->
    386       let (e1,l1) = eval_expr localenv m exp in
     405      let (e1,l1) = eval_expr localenv m c exp in
    387406      ((eval_unop tt e1 op,tt),l1)
    388407    | Econdition (e1,e2,e3) ->
    389       let (v1,l1) = eval_expr localenv m e1 in
    390       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)
    391410      else
    392         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)
    393412      else (v1,l1)
    394413    | Eandbool (e1,e2) ->
    395       let (v1,l1) = eval_expr localenv m e1 in
    396       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)
    397416      else (v1,l1)
    398417    | Eorbool (e1,e2) ->
    399       let (v1,l1) = eval_expr localenv m e1 in
    400       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)
    401420      else (v1,l1)
    402421    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
    403422    | Efield (e1,id) ->
    404       let ((v1,t1),l1) = eval_expr localenv m e1 in
     423      let ((v1,t1),l1) = eval_expr localenv m c e1 in
    405424      let addr = address_of_value (get_offset v1 id t1) in
    406425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
    407426    | Ecost (lbl,e1) ->
    408       let (v1,l1) = eval_expr localenv m e1 in
     427      (* applying current indexing on label *)
     428      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     429      let (v1,l1) = eval_expr localenv m c e1 in
    409430      (v1,lbl::l1)
    410431    | Ecall _ -> assert false (* only used by the annotation process *)
    411432    | Ecast (cty,exp) ->
    412       let ((v,ty),l1) = eval_expr localenv m exp in
     433      let ((v,ty),l1) = eval_expr localenv m c exp in
    413434      ((eval_cast (v,ty,cty),tt),l1)
    414435
    415 and eval_lvalue localenv m (Expr (e,t)) = match e with
     436and eval_lvalue localenv m c (Expr (e,t)) = match e with
    416437  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
    417438  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
     
    419440  | Evar id -> ((find_symbol localenv m id,t),[])
    420441  | Ederef ee ->
    421     let ((v,_),l1) = eval_expr localenv m ee in
     442    let ((v,_),l1) = eval_expr localenv m c ee in
    422443    ((address_of_value v,t),l1)
    423444  | Efield (ee,id) ->
    424     let ((v,tt),l1) = eval_expr localenv m ee in
     445    let ((v,tt),l1) = eval_expr localenv m c ee in
    425446    let v' = get_offset v id tt in
    426447    ((address_of_value v', t), l1)
    427448  | Ecost (lbl,ee) ->
    428     let (v,l) = eval_lvalue localenv m ee in
     449    let (v,l) = eval_lvalue localenv m c ee in
    429450    (v,lbl::l)
    430451  | Ecall _ -> assert false (* only used in the annotation process *)
    431452
    432 let eval_exprlist lenv mem es =
     453let eval_exprlist lenv mem c es =
    433454  let f (vs, cost_lbls) e =
    434     let ((v, _), cost_lbls') = eval_expr lenv mem e in
     455    let ((v, _), cost_lbls') = eval_expr lenv mem c e in
    435456    (vs @ [v], cost_lbls @ cost_lbls') in
    436457  List.fold_left f ([], []) es
     
    464485  else error "undefined condition guard value."
    465486
    466 let eval_stmt f k e m s = match s, k with
    467   | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
    468   | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    469   | Sskip, Kdowhile(a,s,k) ->
    470     let ((v1, _),l1) = eval_expr e m a in
    471     let a_false = (State(f,Sskip,k,e,m),l1) in
    472     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     487let eval_stmt f k e m s c = match s, k with
     488  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
     489  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
     490  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
     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. *)
     494    let ((v1,_),l1) = eval_expr e m c a in
     495    let a_false = (State(f,Sskip,k',e,m,c),l1) in
     496    let a_true = (State(f,s,k,e,m,c),l1) in
    473497    condition v1 a_true a_false
    474   | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
    475   | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    476   | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
     498  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
     499    CostLabel.continue_loop_opt c i;
     500    let ((v1,_),l1) = eval_expr e m c a2 in
     501    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     502    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
     503    condition v1 a_true a_false
     504  | Sskip, Kfor2(i,a2,a3,s,k) ->
     505    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
     506  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    477507  | Sskip, Kcall _ ->
    478508    let m' = free_local_env m e in
    479     (Returnstate(Value.undef,k,m'),[])
     509    (Returnstate(Value.undef,k,m',c),[])
    480510  | Sassign(a1, a2), _ ->
    481     let ((v1,t1),l1) = (eval_lvalue e m a1) in
    482     let ((v2,t2),l2) = eval_expr e m a2 in
    483     (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
     511    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
     512    let ((v2,t2),l2) = eval_expr e m c a2 in
     513    (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2)
    484514  | Scall(None,a,al), _ ->
    485     let ((v1,_),l1) = eval_expr e m a in
     515    let ((v1,_),l1) = eval_expr e m c a in
    486516    let fd = Mem.find_fun_def m (address_of_value v1) in
    487     let (vargs,l2) = eval_exprlist e m al in
    488     (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
     517    let (vargs,l2) = eval_exprlist e m c al in
     518    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
    489519  | Scall(Some lhs,a,al), _ ->
    490     let ((v1,_),l1) = eval_expr e m a in
     520    let ((v1,_),l1) = eval_expr e m c a in
    491521    let fd = Mem.find_fun_def m (address_of_value v1) in
    492     let (vargs,l2) = eval_exprlist e m al in
    493     let (vt3,l3) = eval_lvalue e m lhs in
    494     (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
    495   | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
     522    let (vargs,l2) = eval_exprlist e m c al in
     523    let (vt3,l3) = eval_lvalue e m c lhs in
     524    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
     525  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
    496526  | Sifthenelse(a,s1,s2), _ ->
    497     let ((v1,_),l1) = eval_expr e m a in
    498     let a_true = (State(f,s1,k,e,m),l1) in
    499     let a_false = (State(f,s2,k,e,m),l1) in
     527    let ((v1,_),l1) = eval_expr e m c a in
     528    let a_true = (State(f,s1,k,e,m,c),l1) in
     529    let a_false = (State(f,s2,k,e,m,c),l1) in
    500530    condition v1 a_true a_false
    501   | Swhile(a,s), _ ->
    502     let ((v1,_),l1) = eval_expr e m a in
    503     let a_false = (State(f,Sskip,k,e,m),l1) in
    504     let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
     531  | Swhile(i,a,s), _ ->
     532    CostLabel.enter_loop_opt c i;
     533    let ((v1,_),l1) = eval_expr e m c a in
     534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     535    let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in
    505536    condition v1 a_true a_false
    506   | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
    507   | Sfor(Sskip,a2,a3,s), _ ->
    508     let ((v1,_),l1) = eval_expr e m a2 in
    509     let a_false = (State(f,Sskip,k,e,m),l1) in
    510     let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
     537  | Sdowhile(i,a,s), _ ->
     538    CostLabel.enter_loop_opt c i;
     539    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
     540  | Sfor(i,Sskip,a2,a3,s), _ ->
     541    CostLabel.enter_loop_opt c i;
     542    let ((v1,_),l1) = eval_expr e m c a2 in
     543    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     544    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    511545    condition v1 a_true a_false
    512   | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
    513   | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
    514   | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
    515   | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
    516   | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
    517   | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
    518   | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
    519   | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    520   | Scontinue, Kdowhile(a,s,k) ->
    521     let ((v1,_),l1) = eval_expr e m a in
    522     let a_false = (State(f,Sskip,k,e,m),l1) in
    523     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
    524     condition v1 a_true a_false
    525   | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    526   | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
     546  | Sfor(i,a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[])
     547  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
     548  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
     549  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
     550  | Scontinue, Kseq(_,k)
     551  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
    527552  | Sreturn None, _ ->
    528553    let m' = free_local_env m e in
    529     (Returnstate(Value.undef,(call_cont k),m'),[])
     554    (Returnstate(Value.undef,(call_cont k),m',c),[])
    530555  | Sreturn (Some a), _ ->
    531     let ((v1,_),l1) = eval_expr e m a  in
     556    let ((v1,_),l1) = eval_expr e m c a  in
    532557    let m' = free_local_env m e in
    533     (Returnstate(v1,call_cont k,m'),l1)
     558    (Returnstate(v1,call_cont k,m',c),l1)
    534559  | Sswitch(a,sl), _ ->
    535     let ((v,_),l) = eval_expr e m a in
     560    let ((v,_),l) = eval_expr e m c a in
    536561    let n = Value.to_int v in
    537     (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
    538   | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
    539   | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
     562  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
     563  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
     564  | Scost(lbl,s), _ ->
     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])
    540568  | Sgoto lbl, _ ->
     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 *)
    541572    let (s', k') = find_label lbl f.fn_body (call_cont k) in
    542     (State(f,s',k',e,m),[])
     573    (State(f,s',k',e,m,c),[])
    543574  | _ -> assert false (* should be impossible *)
    544575
     
    546577module InterpretExternal = Primitive.Interpret (Mem)
    547578
    548 let interpret_external k mem f args =
     579let interpret_external k mem c f args =
    549580  let (mem', v) = match InterpretExternal.t mem f args with
    550581    | (mem', InterpretExternal.V vs) ->
     
    552583      (mem', v)
    553584    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    554   Returnstate (v, k, mem')
    555 
    556 let step_call args cont mem = function
     585  Returnstate (v, k, mem',c)
     586
     587let step_call args cont mem c = function
    557588  | Internal f ->
    558589    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    559     State (f, f.fn_body, cont, e, mem')
     590    (* initializing loop indices *)
     591    let c = CostLabel.new_const_ind c in
     592    State (f, f.fn_body, cont, e, mem', c)
    560593  | External(id,targs,tres) when List.length targs = List.length args ->
    561     interpret_external cont mem id args
     594    interpret_external cont mem c id args
    562595  | External(id,_,_) ->
    563596    error ("wrong size of arguments when calling external " ^ id ^ ".")
    564597
    565598let step = function
    566   | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
    567   | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    568   | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
    569   | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
     599  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
     600  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
     601  | Returnstate(v,Kcall(None,f,e,k),m,c) ->
     602    let c = CostLabel.forget_const_ind c in
     603    (State(f,Sskip,k,e,m,c),[])
     604  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
     605    let c = CostLabel.forget_const_ind c in
    570606    let m' = assign m v ty vv in
    571     (State(f,Sskip,k,e,m'),[])
     607    (State(f,Sskip,k,e,m',c),[])
    572608  | _ -> error "state malformation."
    573609
     
    603639    if debug then Printf.printf "Result = %s\n%!"
    604640      (IntValue.Int32.to_string res) ;
    605     (res, cost_labels) in
     641    (res, List.rev cost_labels) in
    606642  if debug then print_state state ;
    607643  match state with
    608     | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     644    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
    609645      print_and_return_result (compute_result v)
    610     | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
     646    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
    611647      print_and_return_result IntValue.Int32.zero
    612648    | state -> exec debug cost_labels (step state)
     
    618654    | Some main ->
    619655      let mem = init_mem prog in
    620       let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     656      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
    621657      exec debug [] first_state
Note: See TracChangeset for help on using the changeset viewer.