Ignore:
Timestamp:
Oct 6, 2011, 6:31:27 PM (9 years ago)
Author:
tranquil
Message:
  • finished changes on annotator
  • implementing indexes in interpreter
File:
1 edited

Legend:

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

    r1291 r1310  
    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  | State of cfunction*statement*continuation*localEnv*memory*indexing
    3738  | Callstate of fundef*Value.t list*continuation*memory
    3839  | Returnstate of Value.t*continuation*memory
     
    113114  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
    114115
     116let string_of_loop_depth = function
     117        | None -> ""
     118        | Some d -> " at " ^ string_of_int d
     119
    115120let rec string_of_statement = function
    116121  | Sskip -> "skip"
     
    121126  | Ssequence _ -> "sequence"
    122127  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
    123   | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
    124   | Sdowhile _ -> "dowhile"
    125   | 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) ^ "; ...)"
    126137  | Sbreak -> "break"
    127138  | Scontinue -> "continue"
     
    159170
    160171let rec call_cont = function
    161   | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
    162   | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
     172  | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k)
     173  | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k
    163174  | k -> k
    164175
     
    178189      | None -> find_label1 lbl s2 k
    179190      )
    180   | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
    181   | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
    182   | Sfor (a1,a2,a3,s1) ->
    183       (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
     191  | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k))
     192  | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k))
     193  | Sfor (i,a1,a2,a3,s1) ->
     194                (* doubt: should we search for labels in a1? *)
     195      (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with
    184196      | Some sk -> Some sk
    185197      | None ->
    186           (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
     198          (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with
    187199          | Some sk -> Some sk
    188           | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
     200          | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k))
    189201          ))
    190202  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
     
    468480  else error "undefined condition guard value."
    469481
    470 let eval_stmt f k e m s = match s, k with
     482(** FIXME: modifying here! *)
     483let eval_stmt f k e m s c = match s, k with
    471484  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
    472   | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    473   | Sskip, Kdowhile(a,s,k) ->
     485  | Sskip, Kwhile(i,a,s,k) as w ->
     486                (* possibly continuing a loop *)
     487                let c = continue_loop i c in
     488    let ((v1,_),l1) = eval_expr e m a in
     489    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     490    let a_true = (State(f,s,w,e,m,c),l1) in
     491    condition v1 a_true a_false
     492  | Sskip, Kdowhile(i,a,s,k) as w ->
     493    let c = continue_loop i c in
    474494    let ((v1, _),l1) = eval_expr e m a in
    475     let a_false = (State(f,Sskip,k,e,m),l1) in
    476     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     495    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     496    let a_true = (State(f,s,w,e,m,c),l1) in
    477497    condition v1 a_true a_false
    478   | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
    479   | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
     498  | Sskip, Kfor3(i,a2,a3,s,k) -> (State(f,Sfor(i,Sskip,a2,a3,s),k,e,m),[])
     499  | Sskip, Kfor2(i,a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    480500  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
    481501  | Sskip, Kcall _ ->
     
    509529    condition v1 a_true a_false
    510530  | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
    511   | Sfor(Sskip,a2,a3,s), _ ->
     531  | Sfor(i,Sskip,a2,a3,s), _ ->
     532                let c = enter_loop i c in
    512533    let ((v1,_),l1) = eval_expr e m a2 in
    513     let a_false = (State(f,Sskip,k,e,m),l1) in
    514     let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
     534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     535    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    515536    condition v1 a_true a_false
    516537  | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
Note: See TracChangeset for help on using the changeset viewer.