Changeset 1310


Ignore:
Timestamp:
Oct 6, 2011, 6:31:27 PM (8 years ago)
Author:
tranquil
Message:
  • finished changes on annotator
  • implementing indexes in interpreter
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
4 edited

Legend:

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

    r1305 r1310  
    1010let cost_id_prefix = "_cost"
    1111let cost_incr_prefix = "_cost_incr"
     12let loop_id_prefix = "_i"
    1213
    1314
     
    313314    | Clight.Internal def ->
    314315        let max_depth = max_loop_index def.Clight.fn_body in
    315         let indexes_defs = loop_indexes_defs l_ind max_depth in
     316        let vars = loop_indexes_defs l_ind max_depth in
     317        let vars = List.rev_append vars def.Clight.fn_vars in
    316318        let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in
    317         Clight.Internal { def with Clight.fn_body = body }
     319        Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
    318320    | Clight.External _ -> def
    319321  in
     
    361363  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
    362364  let cost_decl = cost_decl cost_id in
     365       
     366        (* Create a fresh loop index prefix *)
     367        let names = StringTools.Set.add cost_id names in
     368  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
    363369
    364370  (* Define an increment function for the cost variable. *)
     
    369375
    370376  (* Instrument each function *)
    371   let prog_funct =
    372     List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
     377  let prog_funct = p.Clight.prog_funct in
     378        let prog_funct =
     379    List.map (instrument_funct l_ind cost_mapping cost_incr) prog_funct in
    373380
    374381  (* Glue all this together. *)
  • 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),[])
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1305 r1310  
    1616let make_id prefix depth = prefix ^ string_of_int depth
    1717
    18 type indexing = sexpr array
     18type indexing = sexpr list
     19
     20type const_indexing = int ref list
     21
     22(** [enter_loop n indexing] is used to update indexing when one is entering a
     23    loop indexed by [n].
     24                The function recycles the same constant indexing *)
     25let rec enter_loop n indexing = match n, indexing with
     26        | None, _ -> indexing (* entering a multi-entry loop *)
     27        | Some 0, [] -> [ref 0] (* entering a single entry loop, current depth *)
     28        | Some 0, hd :: tl -> hd := 0; indexing (* as above, reusing slot *)
     29        | Some x, hd :: tl -> hd :: enter_loop (Some (x-1)) tl (* lower depth *)
     30        | Some x, [] -> assert false(* means I'm entering a single entry loop *)
     31                                    (* without having entered the one containing it *)       
     32
     33(** [enter_loop n indexing] is used to update indexing when one is continuing a
     34    loop indexed by [n]. *)
     35let rec continue_loop n indexing = match n, indexing with
     36        | None, _ -> indexing (* continuing a multi-entry loop *)
     37        | Some 0, hd :: tl -> hd := !hd + 1; indexing (* incrementing index *)
     38        | Some x, hd :: tl -> hd :: continue_loop (Some (x-1)) tl (* lower depth *)
     39        | Some _, [] -> assert false (* means I'm continuing a single entry loop *)
     40                                     (* without having entered it *)       
    1941
    2042let sexpr_of i l =
    2143    try
    22         l.(i)
     44        List.nth l i
    2345    with
    24         | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of")
     46                        | Failure _
     47      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
    2548
    26 let id_indexing n = Array.make n sexpr_id
     49let rec id_indexing = function
     50        | 0 -> []
     51        | n -> sexpr_id :: id_indexing (n-1)
    2752
    2853(* a*_+b is composed with c*_+d by substitution: *)
     
    3055let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
    3156    Sexpr (a * c, b * c + d)
     57               
     58let ev_sexpr i (Sexpr(a, b)) = a*i+b
    3259
    3360(* i|-->e ° I *)
    34 let compose_index i s l =
    35   try
    36                 l.(i) <- compose_sexpr s l.(i)
    37         with
    38                 | Not_found -> ()
     61let rec compose_index i s l = match i, l with
     62        | 0, s' :: l' -> compose_sexpr s s' :: l'
     63        | x, s' :: l' -> compose_index (i-1) s l'
     64        | _ -> l
    3965
    4066
    4167(* I°J applies every mapping in I to every mapping in J *)
    42 let compose_indexing m n =
    43         let f i a = compose_index i a n in
    44         Array.iteri f m
     68let rec compose_indexing m n = match m, n with
     69        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
     70        | _ -> n 
    4571
     72let rec compose_const_indexing c m = match c, m with
     73        | i1 :: l1, s2 :: l2 -> ev_sexpr !i1 s2 :: compose_const_indexing l1 l2
     74        | _, [] -> [] (* that's ok as current indexings will not be shrinked *)
     75        | [], _ -> assert false (* means an indexed label is not in the right ctx *)
    4676
    4777module IndexingSet = Set.Make(struct
     
    5989(* if [pretty] is false then a name suitable for labels is given*)
    6090(* ('P' replaces '+') *)
    61 let string_of_sexpr pretty id (Sexpr(a, b)) =
     91let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
    6292        let plus = if pretty then "+" else "P" in
     93        let id = prefix ^ string_of_int i in
    6394  let a_id_s = if a = 1 then id else string_of_int a ^ id in
    6495        let b_s = string_of_int b in
     
    69100(* [pretty] true:  (0,i1+1,2i2+2)*)
    70101(* [pretty] false: _0_i1P1_2i2P2 *)
    71 let string_of_indexing pretty prefix m =
    72         if Array.length m = 0 then "" else
    73         let buff = Buffer.create 16 in
    74   Buffer.add_char buff (if pretty then '(' else '_');
    75         let sep = if pretty then ',' else '_' in
    76         let f i a =
    77                 if i > 0 then Buffer.add_char buff sep;
    78                 let str = string_of_sexpr pretty (prefix ^ string_of_int i) a in
    79                 Buffer.add_string buff str in
    80         Array.iteri f m;
    81         Buffer.contents buff
     102let rec string_of_indexing_tl pretty prefix i = function
     103        | [] -> if pretty then ")" else ""
     104        | hd :: tl ->
     105                let sep = if pretty then "," else "_" in
     106                let str = string_of_sexpr pretty prefix i hd in
     107                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
     108
     109let string_of_indexing pretty prefix = function
     110        | [] -> ""
     111        | hd :: tl ->
     112                let start = if pretty then "(" else "_" in
     113    let str = string_of_sexpr pretty prefix 0 hd in
     114                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
    82115               
    83116let string_of_cost_label ?(pretty = false) lab =
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

    r1305 r1310  
    1919val make_id : string -> index -> string
    2020
    21 type indexing = sexpr array
     21type indexing = sexpr list
     22
     23type const_indexing = int ref list
     24
     25(** [enter_loop n indexing] is used to update indexing when one is entering a
     26    loop indexed by [n].
     27        The function recycles the same constant indexing *)
     28val enter_loop : index option -> const_indexing -> const_indexing
     29
     30(** [continue_loop n indexing] is used to update indexing when one is continuing a
     31    loop indexed by [n]. *)
     32val continue_loop : index option -> const_indexing -> const_indexing
    2233
    2334(** [id_indexing n] generates an identity indexing nested in [n] loops *)
     
    2536
    2637(** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *)
    27 val compose_index : index -> sexpr -> indexing -> unit
     38val compose_index : index -> sexpr -> indexing -> indexing
    2839
    2940(** [compose_index l m] applies all the transformations in  [l] to [m] *)
    30 val compose_indexing : indexing -> indexing -> unit
     41val compose_indexing : indexing -> indexing -> indexing
     42
     43val compose_const_indexing : const_indexing -> indexing -> int list
    3144
    3245module IndexingSet : Set.S with type elt = indexing
Note: See TracChangeset for help on using the changeset viewer.