Changeset 1310 for Deliverables/D2.2
- Timestamp:
- Oct 6, 2011, 6:31:27 PM (8 years ago)
- 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 10 10 let cost_id_prefix = "_cost" 11 11 let cost_incr_prefix = "_cost_incr" 12 let loop_id_prefix = "_i" 12 13 13 14 … … 313 314 | Clight.Internal def -> 314 315 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 316 318 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} 318 320 | Clight.External _ -> def 319 321 in … … 361 363 let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in 362 364 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 363 369 364 370 (* Define an increment function for the cost variable. *) … … 369 375 370 376 (* 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 373 380 374 381 (* Glue all this together. *) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml
r1291 r1310 4 4 type localEnv = Value.address LocalEnv.t 5 5 type memory = Clight.fundef Mem.memory 6 type indexing = CostLabel.const_indexing 6 7 7 8 open Clight … … 26 27 | Kstop 27 28 | Kseq of statement*continuation 28 | Kwhile of expr*statement*continuation29 | Kdowhile of expr*statement*continuation30 | Kfor2 of expr*statement*statement*continuation31 | Kfor3 of expr*statement*statement*continuation29 | 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 32 33 | Kswitch of continuation 33 34 | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation 34 35 35 36 type state = 36 | State of cfunction*statement*continuation*localEnv*memory 37 | State of cfunction*statement*continuation*localEnv*memory*indexing 37 38 | Callstate of fundef*Value.t list*continuation*memory 38 39 | Returnstate of Value.t*continuation*memory … … 113 114 "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")" 114 115 116 let string_of_loop_depth = function 117 | None -> "" 118 | Some d -> " at " ^ string_of_int d 119 115 120 let rec string_of_statement = function 116 121 | Sskip -> "skip" … … 121 126 | Ssequence _ -> "sequence" 122 127 | 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) ^ "; ...)" 126 137 | Sbreak -> "break" 127 138 | Scontinue -> "continue" … … 159 170 160 171 let rec call_cont = function 161 | Kseq (_,k) | Kwhile (_, _,k) | Kdowhile (_,_,k)162 | Kfor2 (_, _,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k172 | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k) 173 | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k 163 174 | k -> k 164 175 … … 178 189 | None -> find_label1 lbl s2 k 179 190 ) 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 184 196 | Some sk -> Some sk 185 197 | None -> 186 (match find_label1 lbl s1 (Kfor2( a2,a3,s1,k)) with198 (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with 187 199 | 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)) 189 201 )) 190 202 | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k) … … 468 480 else error "undefined condition guard value." 469 481 470 let eval_stmt f k e m s = match s, k with 482 (** FIXME: modifying here! *) 483 let eval_stmt f k e m s c = match s, k with 471 484 | 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 474 494 let ((v1, _),l1) = eval_expr e m a in 475 let a_false = (State(f,Sskip,k,e,m ),l1) in476 let a_true = (State(f, Sdowhile(a,s),k,e,m),l1) in495 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 477 497 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),[]) 480 500 | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[]) 481 501 | Sskip, Kcall _ -> … … 509 529 condition v1 a_true a_false 510 530 | 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 512 533 let ((v1,_),l1) = eval_expr e m a2 in 513 let a_false = (State(f,Sskip,k,e,m ),l1) in514 let a_true = (State(f,s,Kfor2( a2,a3,s,k),e,m),l1) in534 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 515 536 condition v1 a_true a_false 516 537 | 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 16 16 let make_id prefix depth = prefix ^ string_of_int depth 17 17 18 type indexing = sexpr array 18 type indexing = sexpr list 19 20 type 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 *) 25 let 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]. *) 35 let 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 *) 19 41 20 42 let sexpr_of i l = 21 43 try 22 l.(i)44 List.nth l i 23 45 with 24 | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of") 46 | Failure _ 47 | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of" 25 48 26 let id_indexing n = Array.make n sexpr_id 49 let rec id_indexing = function 50 | 0 -> [] 51 | n -> sexpr_id :: id_indexing (n-1) 27 52 28 53 (* a*_+b is composed with c*_+d by substitution: *) … … 30 55 let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) = 31 56 Sexpr (a * c, b * c + d) 57 58 let ev_sexpr i (Sexpr(a, b)) = a*i+b 32 59 33 60 (* 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 -> () 61 let 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 39 65 40 66 41 67 (* 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 in44 Array.iteri f m68 let rec compose_indexing m n = match m, n with 69 | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2 70 | _ -> n 45 71 72 let 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 *) 46 76 47 77 module IndexingSet = Set.Make(struct … … 59 89 (* if [pretty] is false then a name suitable for labels is given*) 60 90 (* ('P' replaces '+') *) 61 let string_of_sexpr pretty id(Sexpr(a, b)) =91 let string_of_sexpr pretty prefix i (Sexpr(a, b)) = 62 92 let plus = if pretty then "+" else "P" in 93 let id = prefix ^ string_of_int i in 63 94 let a_id_s = if a = 1 then id else string_of_int a ^ id in 64 95 let b_s = string_of_int b in … … 69 100 (* [pretty] true: (0,i1+1,2i2+2)*) 70 101 (* [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 102 let 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 109 let 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 82 115 83 116 let string_of_cost_label ?(pretty = false) lab = -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli
r1305 r1310 19 19 val make_id : string -> index -> string 20 20 21 type indexing = sexpr array 21 type indexing = sexpr list 22 23 type 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 *) 28 val 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]. *) 32 val continue_loop : index option -> const_indexing -> const_indexing 22 33 23 34 (** [id_indexing n] generates an identity indexing nested in [n] loops *) … … 25 36 26 37 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 27 val compose_index : index -> sexpr -> indexing -> unit38 val compose_index : index -> sexpr -> indexing -> indexing 28 39 29 40 (** [compose_index l m] applies all the transformations in [l] to [m] *) 30 val compose_indexing : indexing -> indexing -> unit 41 val compose_indexing : indexing -> indexing -> indexing 42 43 val compose_const_indexing : const_indexing -> indexing -> int list 31 44 32 45 module IndexingSet : Set.S with type elt = indexing
Note: See TracChangeset
for help on using the changeset viewer.