Changeset 1421 for Deliverables/D2.2
- Timestamp:
- Oct 19, 2011, 5:59:50 PM (9 years ago)
- Location:
- Deliverables/D2.2
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml
r1349 r1421 293 293 let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in 294 294 {p with prog_funct = List.map (process_f cost_universe) p.prog_funct} 295 -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml
r1392 r1421 604 604 (tmps, Cminor.St_cost (lbl, stmt)) 605 605 606 | _ -> assert false (* type error*)606 (* | _ -> assert false (* type error *) *) 607 607 608 608 … … 646 646 647 647 let translate p = 648 (* apply loop peeling *) 649 let p = LoopPeeling.apply p in 648 650 let fresh = ClightAnnotator.make_fresh "_tmp" p in 649 651 { Cminor.vars = List.map translate_global p.Clight.prog_vars ; -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorToRTLabs.ml
r1392 r1421 269 269 (rtlabs_fun : RTLabs.internal_function) 270 270 (lenv : local_env) 271 (exits : Label.t list)271 (* (exits : Label.t list) *) 272 272 (stmt : Cminor.statement) 273 273 : RTLabs.internal_function = … … 321 321 322 322 | Cminor.St_seq (s1, s2) -> 323 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss2 in324 translate_stmt rtlabs_fun lenv exitss1323 let rtlabs_fun = translate_stmt rtlabs_fun lenv s2 in 324 translate_stmt rtlabs_fun lenv (* exits *) s1 325 325 326 326 | Cminor.St_ifthenelse (e, s1, s2) -> 327 327 let old_entry = rtlabs_fun.RTLabs.f_entry in 328 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss2 in328 let rtlabs_fun = translate_stmt rtlabs_fun lenv s2 in 329 329 let lbl_false = rtlabs_fun.RTLabs.f_entry in 330 330 let rtlabs_fun = change_entry rtlabs_fun old_entry in 331 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss1 in331 let rtlabs_fun = translate_stmt rtlabs_fun lenv s1 in 332 332 let lbl_true = rtlabs_fun.RTLabs.f_entry in 333 333 translate_branch rtlabs_fun lenv e lbl_true lbl_false … … 362 362 363 363 | Cminor.St_label (lbl, s) -> 364 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss in364 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in 365 365 let old_entry = rtlabs_fun.RTLabs.f_entry in 366 366 add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry) 367 367 368 368 | Cminor.St_cost (lbl, s) -> 369 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss in369 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in 370 370 let old_entry = rtlabs_fun.RTLabs.f_entry in 371 371 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) 372 372 373 373 | Cminor.St_ind_0 (i, s) -> 374 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss in374 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in 375 375 let old_entry = rtlabs_fun.RTLabs.f_entry in 376 376 generate rtlabs_fun (RTLabs.St_ind_0 (i, old_entry)) 377 377 378 378 | Cminor.St_ind_inc (i, s) -> 379 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss in379 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in 380 380 let old_entry = rtlabs_fun.RTLabs.f_entry in 381 381 generate rtlabs_fun (RTLabs.St_ind_inc (i, old_entry)) … … 456 456 457 457 (* Complete the graph *) 458 translate_stmt rtlabs_fun lenv []f_def.Cminor.f_body458 translate_stmt rtlabs_fun lenv f_def.Cminor.f_body 459 459 460 460 -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml
r1357 r1421 9 9 type sexpr = 10 10 | Sexpr of int*int 11 12 let is_const_sexpr (Sexpr(a, _)) = (a = 0) 11 13 12 14 let sexpr_id = Sexpr(1, 0) … … 75 77 76 78 (* i|-->e ° I *) 77 let rec compose_index i s l = match i, l with79 let rec compose_index_indexing i s l = match i, l with 78 80 | 0, s' :: l' -> compose_sexpr s s' :: l' 79 | x, s' :: l' -> compose_index(i-1) s l'81 | x, s' :: l' -> s' :: compose_index_indexing (i-1) s l' 80 82 | _ -> l 81 83 … … 89 91 | [] -> [] 90 92 | s :: l -> 91 try 92 const_sexpr (ev_sexpr (ExtArray.get c i) s) :: 93 compose_const_indexing_i (i+1) c l 94 with 95 | Invalid_argument _ -> 96 invalid_arg "constant indexing not enough to be applied" 93 let head = 94 (* if s is constant leave it be. In particular, avoid raising the error *) 95 if is_const_sexpr s then s else 96 try 97 const_sexpr (ev_sexpr (ExtArray.get c i) s) 98 with 99 | Invalid_argument _ -> 100 invalid_arg "constant indexing not enough to be applied" in 101 head :: compose_const_indexing_i (i+1) c l 97 102 98 103 module IndexingSet = Set.Make(struct … … 105 110 i : indexing 106 111 } 112 113 let comp_index i s lbl = 114 {lbl with i = compose_index_indexing i s lbl.i} 107 115 108 116 let ev_indexing c lbl = -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli
r1357 r1421 9 9 10 10 (** Simple expressions corresponding to loop tranformations. 11 TODO: leave itabstract or not? *)12 type sexpr 11 TODO: abstract or not? *) 12 type sexpr = Sexpr of int*int 13 13 14 14 val sexpr_id : sexpr … … 76 76 } 77 77 78 (** [apply_const_indexing ind lbl] returns [lbl] where its indexing has been 78 (** [comp_index i s lbl] gives back the label [lbl] where index [i] is remapped 79 to the simple expression [s]. *) 80 val comp_index : index -> sexpr -> t -> t 81 82 83 (** [ev_indexing ind lbl] returns [lbl] where its indexing has been 79 84 evaluated in the constant indexing [ind]. 80 85 @raise Invalid_argument "constant indexing not enough to be applied" if -
Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml
r818 r1421 248 248 | St_switch(_,_,_) -> None 249 249 | St_return(_) -> None 250 | St_label(l,s) -> if l=lbl then Some((s,k)) else None250 | St_label(l,s) when l = lbl -> Some((s,k)) 251 251 | St_goto(_) -> None 252 | St_cost (_,s)-> fdlbl k s252 | St_cost(_,s) | St_label(_,s)-> fdlbl k s 253 253 in match fdlbl k st with 254 254 None -> assert false (*Wrong label*)
Note: See TracChangeset
for help on using the changeset viewer.