Changeset 1334 for Deliverables/D2.2
- Timestamp:
- Oct 10, 2011, 2:17:02 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051-indexed-labels-branch/src
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml
r1328 r1334 487 487 488 488 let eval_stmt f k e m s c = 489 let enter_loop = CostLabel.enter_loop in490 let continue_loop = CostLabel.continue_loop in491 489 match s, k with 492 490 | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[]) … … 494 492 | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') -> 495 493 (* possibly continuing a loop *) 496 continue_loop i c; (* if loop is not continued, this change will have no497 effect in the following. Can be made stricter*)494 CostLabel.continue_loop i c; (* if loop is not continued, this change 495 will have no effect in the following. *) 498 496 let ((v1,_),l1) = eval_expr e m c a in 499 497 let a_false = (State(f,Sskip,k',e,m,c),l1) in … … 501 499 condition v1 a_true a_false 502 500 | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) -> 503 continue_loop i c;501 CostLabel.continue_loop i c; 504 502 let ((v1,_),l1) = eval_expr e m c a2 in 505 503 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 533 531 condition v1 a_true a_false 534 532 | Swhile(i,a,s), _ -> 535 enter_loop i c;533 CostLabel.enter_loop i c; 536 534 let ((v1,_),l1) = eval_expr e m c a in 537 535 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 539 537 condition v1 a_true a_false 540 538 | Sdowhile(i,a,s), _ -> 541 enter_loop i c;539 CostLabel.enter_loop i c; 542 540 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[]) 543 541 | Sfor(i,Sskip,a2,a3,s), _ -> 544 enter_loop i c;542 CostLabel.enter_loop i c; 545 543 let ((v1,_),l1) = eval_expr e m c a2 in 546 544 let a_false = (State(f,Sskip,k,e,m,c),l1) in -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml
r818 r1334 486 486 AST.res = ret_type } 487 487 488 let ind_0 i stmt = match i with 489 | None -> stmt 490 | Some x -> Cminor.St_ind_0(x, stmt) 491 492 let ind_inc i stmt = match i with 493 | None -> stmt 494 | Some x -> Cminor.St_ind_inc(stmt, x) 495 488 496 let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res = 489 497 let (tmps, sub_stmts_res) = List.split sub_stmts_res in … … 509 517 ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign)) 510 518 511 | Clight.Swhile _, e :: _, stmt :: _ ->512 let econd = 513 519 | Clight.Swhile (i,_,_), e :: _, stmt :: _ -> 520 let econd = 521 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 514 522 let scond = 515 516 ([], 517 Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond, 518 Cminor.St_block stmt))))519 520 | Clight.Sdowhile _, e :: _, stmt :: _ ->521 let econd = 522 523 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 524 let loop_body = Cminor.St_seq (scond, ind_inc i (Cminor.St_block stmt)) in 525 let loop = ind_0 i (Cminor.St_loop loop_body) in 526 ([], Cminor.St_block loop) 527 528 | Clight.Sdowhile (i,_,_), e :: _, stmt :: _ -> 529 let econd = 530 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 523 531 let scond = 524 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in525 ([], 526 Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt, 527 scond))))528 529 | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->530 let econd = 531 532 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 533 let loop_body = ind_inc i (Cminor.St_seq (Cminor.St_block stmt, scond)) in 534 let loop = ind_0 i (Cminor.St_loop loop_body) in 535 ([], Cminor.St_block loop) 536 537 | Clight.Sfor (i,_,_,_,_), e :: _, stmt1 :: stmt2 :: stmt3 :: _ -> 538 let econd = 539 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 532 540 let scond = 533 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 534 let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in 535 ([], 536 Cminor.St_seq (stmt1, 537 Cminor.St_block 538 (Cminor.St_loop (Cminor.St_seq (scond, body))))) 541 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 542 let body = Cminor.St_seq (ind_inc i (Cminor.St_block stmt3), stmt2) in 543 let body = Cminor.St_seq (scond, body) in 544 let block = Cminor.St_block (ind_0 i (Cminor.St_loop body)) in 545 ([], Cminor.St_seq (stmt1, block)) 539 546 540 547 | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminor.mli
r818 r1334 47 47 | St_goto of string 48 48 | St_cost of CostLabel.t * statement 49 | St_ind_0 of CostLabel.index * statement 50 | St_ind_inc of statement * CostLabel.index 49 51 50 52 -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorFold.ml
r818 r1334 44 44 ([e], [stmt1 ; stmt2]) 45 45 | Cminor.St_loop stmt | Cminor.St_block stmt 46 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) -> 47 ([], [stmt]) 46 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) 47 | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (stmt, _) -> 48 ([], [stmt]) 48 49 49 50 let statement_fill_subs stmt sub_es sub_stmts = -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml
r1291 r1334 23 23 (* State of execution *) 24 24 25 type indexing = CostLabel.const_indexing 26 25 27 type continuation = 26 28 Ct_stop 27 29 | Ct_cont of statement*continuation 30 | Ct_ind_inc of CostLabel.index*continuation 28 31 | Ct_endblock of continuation 29 32 | Ct_returnto of 30 ident option*internal_function*Val.address*local_env* continuation33 ident option*internal_function*Val.address*local_env*indexing*continuation 31 34 32 35 type state = 33 36 State_regular of 34 internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory) 37 internal_function*statement*continuation*Val.address*local_env* 38 (function_def Mem.memory)*indexing 35 39 | State_call of function_def*Val.t list*continuation*(function_def Mem.memory) 36 40 | State_return of Val.t*continuation*(function_def Mem.memory) … … 68 72 let lbl = CostLabel.string_of_cost_label lbl in 69 73 "cost " ^ lbl 74 | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0" 75 | St_ind_inc (_, i) -> "post-increment " ^ string_of_int i 70 76 71 77 let print_state = function 72 | State_regular (_, stmt, _, sp, lenv, mem ) ->73 Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n \nRegular state: %s\n\n%!"78 | State_regular (_, stmt, _, sp, lenv, mem, i) -> 79 Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:" 74 80 (string_of_local_env lenv) 75 81 (Mem.to_string mem) 76 (Val.to_string (value_of_address sp)) 82 (Val.to_string (value_of_address sp)); 83 Array.iter (fun a -> Printf.printf "%d, " a) i; 84 Printf.printf "\nRegular state: %s\n\n%!" 77 85 (string_of_statement stmt) 78 86 | State_call (_, args, _, mem) -> … … 223 231 224 232 let rec callcont = function 225 Ct_stop -> Ct_stop 226 | Ct_cont(_,k) -> callcont k 227 | Ct_endblock(k) -> callcont k 228 | Ct_returnto(a,b,c,d,e) -> Ct_returnto(a,b,c,d,e) 233 | Ct_cont(_,k) | Ct_endblock k | Ct_ind_inc(_,k) -> callcont k 234 | (Ct_stop | Ct_returnto _) as k -> k 229 235 230 236 let findlabel lbl st k = … … 252 258 | St_label(l,s) -> if l=lbl then Some((s,k)) else None 253 259 | St_goto(_) -> None 254 | St_cost (_,s) 260 | St_cost (_,s) | St_ind_0(_,s) | St_ind_inc(s,_) -> fdlbl k s 255 261 in match fdlbl k st with 256 262 None -> assert false (*Wrong label*) … … 264 270 (State_call(fun_def,args,cont,m),l1@l2) 265 271 266 let eval_stmt f k sigma e m s = match s, k with267 | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m ),[])268 | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m ),[])272 let eval_stmt f k sigma e m i s = match s, k with 273 | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[]) 274 | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[]) 269 275 | St_skip, (Ct_returnto _ as k) -> 270 276 (State_return (Val.undef,k,Mem.free m sigma),[]) 277 | St_skip,Ct_ind_inc(ind,k) -> 278 CostLabel.continue_loop (Some ind) i; 279 (State_regular(f, s, k, sigma, e, m, i),[]) 271 280 | St_skip,Ct_stop -> 272 281 (State_return (Val.undef,Ct_stop,Mem.free m sigma),[]) … … 274 283 let (v,l) = eval_expression sigma e m exp in 275 284 let e = LocalEnv.add x v e in 276 (State_regular(f, St_skip, k, sigma, e, m ),l)285 (State_regular(f, St_skip, k, sigma, e, m, i),l) 277 286 | St_store(q,a1,a2),_ -> 278 287 let (v1,l1) = eval_expression sigma e m a1 in 279 288 let (v2,l2) = eval_expression sigma e m a2 in 280 289 let m = Mem.storeq m q (address_of_value v1) v2 in 281 (State_regular(f, St_skip, k, sigma, e, m ),l1@l2)290 (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2) 282 291 | St_call(xopt,f',params,_),_ -> 283 call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e, k))292 call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,i,k)) 284 293 | St_tailcall(f',params,_),_ -> 285 294 call_state sigma e m f' params (callcont k) 286 | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m ),[])295 | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[]) 287 296 | St_ifthenelse(exp,s1,s2),_ -> 288 297 let (v,l) = eval_expression sigma e m exp in … … 292 301 if Val.is_false v then s2 293 302 else error "undefined conditional value." in 294 (State_regular(f,next_stmt,k,sigma,e,m ),l)295 | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m ),[])296 | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m ),[])297 | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m ),[])298 | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m ),[])303 (State_regular(f,next_stmt,k,sigma,e,m,i),l) 304 | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[]) 305 | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[]) 306 | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[]) 307 | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[]) 299 308 | St_exit(n),Ct_endblock(k) -> 300 (State_regular(f,(St_exit (n-1)),k,sigma,e,m ),[])301 | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m ),[])309 (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[]) 310 | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[]) 302 311 | St_goto(lbl),_ -> 303 312 let (s2,k2) = findlabel lbl f.f_body (callcont k) in 304 (State_regular(f,s2,k2,sigma,e,m ),[])313 (State_regular(f,s2,k2,sigma,e,m,i),[]) 305 314 | St_switch(exp,lst,def),_ -> 306 315 let (v,l) = eval_expression sigma e m exp in 307 316 if Val.is_int v then 308 317 try 309 let i= Val.to_int v in318 let v = Val.to_int v in 310 319 let nb_exit = 311 if List.mem_assoc i lst then List.assoc ilst320 if List.mem_assoc v lst then List.assoc v lst 312 321 else def in 313 (State_regular(f, St_exit nb_exit,k, sigma, e, m ),l)322 (State_regular(f, St_exit nb_exit,k, sigma, e, m, i),l) 314 323 with _ -> error "int value too big." 315 324 else error "undefined switch value." … … 319 328 let (v,l) = eval_expression sigma e m a in 320 329 (State_return (v,callcont k,Mem.free m sigma),l) 321 | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl]) 330 | St_cost(lbl,s),_ -> 331 (* applying current indexing on label *) 332 let lbl = CostLabel.apply_const_indexing i lbl in 333 (State_regular(f,s,k,sigma,e,m,i),[lbl]) 334 | St_ind_0(ind,s),_ -> 335 CostLabel.enter_loop (Some ind) i; 336 (State_regular(f,s,k,sigma,e,m,i), []) 337 | St_ind_inc(s,ind),_ -> 338 (State_regular(f,s,Ct_ind_inc(ind,k),sigma,e,m,i), []) 322 339 | _ -> error "state malformation." 323 340 … … 333 350 State_return (v, k, mem') 334 351 352 let max_loop_index = 353 let f_expr _ _ = () in 354 let f_stmt stmt _ sub_stmts_res = 355 let curr_max = List.fold_left max 0 sub_stmts_res in 356 match stmt with 357 | Cminor.St_ind_0 (x, _) | Cminor.St_ind_inc (_, x) -> 358 max (x+1) curr_max 359 | _ -> curr_max in 360 CminorFold.statement f_expr f_stmt 361 335 362 let step_call vargs k m = function 336 363 | F_int f -> 337 364 let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in 338 365 let lenv = init_local_env vargs f.f_params f.f_vars in 339 State_regular(f,f.f_body,k,sp,lenv,m) 366 let i = Array.make (max_loop_index f.f_body) 0 in 367 State_regular(f,f.f_body,k,sp,lenv,m,i) 340 368 | F_ext f -> interpret_external k m f.ef_tag vargs 341 369 342 370 let step = function 343 | State_regular(f,stmt,k,sp,e,m ) -> eval_stmt f k sp e mstmt371 | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt 344 372 | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[]) 345 | State_return(v,Ct_returnto(None,f,sigma,e, k),m) ->346 (State_regular(f,St_skip,k,sigma,e,m ),[])347 | State_return(v,Ct_returnto(Some x,f,sigma,e, k),m) ->373 | State_return(v,Ct_returnto(None,f,sigma,e,i,k),m) -> 374 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 375 | State_return(v,Ct_returnto(Some x,f,sigma,e,i,k),m) -> 348 376 let e = LocalEnv.add x v e in 349 (State_regular(f,St_skip,k,sigma,e,m ),[])377 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 350 378 | _ -> error "state malformation." 351 379 … … 371 399 | State_return(v,Ct_stop,_) -> (* Explicit return in main *) 372 400 print_and_return_result (compute_result v) 373 | State_regular(_,St_skip,Ct_stop,_,_,_ ) -> (* Implicit return in main *)401 | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *) 374 402 print_and_return_result IntValue.Int32.zero 375 403 | state -> exec debug cost_labels (step state) -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorPrinter.ml
r1291 r1334 172 172 (Primitive.print_sig sg) 173 173 | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2) 174 | Cminor.St_ifthenelse (e, s1, Cminor.St_skip) -> 175 Printf.sprintf "%sif (%s) {\n%s%s}\n" 176 (n_spaces n) 177 (print_expression e) 178 (print_body (n+2) s1) 179 (n_spaces n) 174 180 | Cminor.St_ifthenelse (e, s1, s2) -> 175 181 Printf.sprintf "%sif (%s) {\n%s%s}\n%selse {\n%s%s}\n" … … 211 217 let lbl = CostLabel.string_of_cost_label lbl in 212 218 Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s) 219 | Cminor.St_ind_0 (i, s) -> 220 Printf.sprintf "%sindex %d:\n%s" (n_spaces n) i (print_body n s) 221 | Cminor.St_ind_inc (s, i) -> 222 Printf.sprintf "%s%sincrement %d;\n" (print_body n s) (n_spaces n) i 213 223 214 224 let print_internal f_name f_def = … … 255 265 | Cminor.St_goto(_) -> "goto" 256 266 | Cminor.St_cost(_,_) -> "cost" 267 | Cminor.St_ind_0 _ -> "index" 268 | Cminor.St_ind_inc _ -> "increment"
Note: See TracChangeset
for help on using the changeset viewer.