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

 2 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),[])
Note: See TracChangeset
for help on using the changeset viewer.