Changeset 1310
 Timestamp:
 Oct 6, 2011, 6:31:27 PM (8 years ago)
 Location:
 Deliverables/D2.2/8051indexedlabelsbranch/src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/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/8051indexedlabelsbranch/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/8051indexedlabelsbranch/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 multientry 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 (x1)) 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 multientry loop *) 37  Some 0, hd :: tl > hd := !hd + 1; indexing (* incrementing index *) 38  Some x, hd :: tl > hd :: continue_loop (Some (x1)) 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 (n1) 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 (i1) 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/8051indexedlabelsbranch/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.