Changeset 1291 for Deliverables/D2.2
- Timestamp:
- Oct 5, 2011, 10:20:41 AM (9 years ago)
- Location:
- Deliverables/D2.2/8051-indexed-labels-branch
- Files:
-
- 22 edited
- 1 copied
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASM.mli
r619 r1291 102 102 type labelled_instruction = 103 103 [ instruction 104 | `Cost of string104 | `Cost of CostLabel.t 105 105 | `Label of string 106 106 | `Jmp of string … … 122 122 type program = 123 123 { code : BitVectors.byte list ; 124 cost_labels : stringBitVectors.WordMap.t ;124 cost_labels : CostLabel.t BitVectors.WordMap.t ; 125 125 exit_addr : BitVectors.word ; 126 126 has_main : bool } -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.ml
r818 r1291 131 131 132 132 exit_addr : BitVectors.word; 133 cost_labels : stringBitVectors.WordMap.t133 cost_labels : CostLabel.t BitVectors.WordMap.t 134 134 } 135 135 -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.mli
r743 r1291 98 98 99 99 exit_addr : BitVectors.word; 100 cost_labels : stringBitVectors.WordMap.t100 cost_labels : CostLabel.t BitVectors.WordMap.t 101 101 } 102 102 -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/Pretty.ml
r818 r1291 43 43 function 44 44 `Label l -> l ^ ":" 45 | `Cost l -> l ^ ":" 45 (* ugly-printing *) 46 | `Cost l -> CostLabel.string_of_cost_label l ^ ":" 46 47 | `Jmp j -> "ljmp " ^ j 47 48 | `Call j -> "lcall " ^ j … … 106 107 cost 107 108 (if BitVectors.WordMap.mem pc p.ASM.cost_labels then 108 (BitVectors.WordMap.find pc p.ASM.cost_labels) 109 else ""), 109 let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in 110 CostLabel.string_of_cost_label ~pretty:true lbl 111 else ""), 110 112 new_pc) in 111 113 fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code) -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLPrinter.ml
r818 r1291 43 43 Printf.sprintf "*** %s *** --> %s" s lbl 44 44 | ERTL.St_cost (cost_lbl, lbl) -> 45 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 45 46 Printf.sprintf "emit %s --> %s" cost_lbl lbl 46 47 | ERTL.St_get_hdw (r1, r2, lbl) -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINPrinter.ml
r818 r1291 26 26 Printf.sprintf "*** %s ***" s 27 27 | LIN.St_cost cost_lbl -> 28 Printf.sprintf "emit %s" cost_lbl 28 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 29 Printf.sprintf "emit %s" cost_lbl 29 30 | LIN.St_int (dstr, i) -> 30 31 Printf.sprintf "imm %s, %d" (print_reg dstr) i -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINToASM.ml
r818 r1291 12 12 | LIN.St_goto lbl 13 13 | LIN.St_label lbl 14 | LIN.St_cost lbl15 14 | LIN.St_condacc lbl -> Label.Set.singleton lbl 15 (* quite dubious about the following *) 16 | LIN.St_cost lbl -> Label.Set.singleton (CostLabel.string_of_cost_label lbl) 16 17 | _ -> Label.Set.empty 17 18 -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLPrinter.ml
r818 r1291 25 25 Printf.sprintf "*** %s *** --> %s" s lbl 26 26 | LTL.St_cost (cost_lbl, lbl) -> 27 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 27 28 Printf.sprintf "emit %s --> %s" cost_lbl lbl 28 29 | LTL.St_int (dstr, i, lbl) -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLPrinter.ml
r818 r1291 43 43 | RTL.St_skip lbl -> "--> " ^ lbl 44 44 | RTL.St_cost (cost_lbl, lbl) -> 45 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 45 46 Printf.sprintf "emit %s --> %s" cost_lbl lbl 46 47 | RTL.St_addr (dstr1, dstr2, id, lbl) -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.ml
r818 r1291 136 136 | RTLabs.St_skip lbl -> "--> " ^ lbl 137 137 | RTLabs.St_cost (cost_lbl, lbl) -> 138 Printf.sprintf "emit %s --> %s" cost_lbl lbl 138 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 139 Printf.sprintf "emit %s --> %s" cost_lbl lbl 139 140 | RTLabs.St_cst (destr, cst, lbl) -> 140 141 Printf.sprintf "imm %s, %s --> %s" -
Deliverables/D2.2/8051-indexed-labels-branch/src/checker.ml
r619 r1291 14 14 in 15 15 let sentence (k, (v1, v2)) = 16 let k = CostLabel.string_of_cost_label ~pretty:true k in 16 17 Printf.sprintf " Label %s %s in language `%s' \ 17 18 whereas it %s in language `%s'." 18 k (string_of_value v1) lang1 (string_of_value v2) lang219 k (string_of_value v1) lang1 (string_of_value v2) lang2 19 20 in 20 21 String.concat "\n" (List.map sentence ds) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clight.mli
r818 r1291 113 113 | Eorbool of expr*expr (**r sequential or ([||]) *) 114 114 | Esizeof of ctype (**r size of a type *) 115 | Efield of expr*ident 115 | Efield of expr*ident (**r access to a member of a struct or union *) 116 116 117 117 (** The following constructors are used by the annotation process only. *) 118 118 119 | Ecost of CostLabel.t *expr (**r cost label. *)119 | Ecost of CostLabel.t * expr (**r cost label. *) 120 120 | Ecall of ident * expr * expr 121 121 -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml
r818 r1291 25 25 Label.Set.union user_labels1 user_labels2) 26 26 27 let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) 27 let empty_triple = 28 (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) 28 29 29 30 let name_singleton id = 30 31 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) 31 32 32 let cost_label_singleton cost_lbl =33 (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)33 let cost_label_singleton lbl = 34 (StringTools.Set.empty, CostLabel.Set.singleton lbl, Label.Set.empty) 34 35 35 36 let label_singleton lbl = … … 77 78 (StringTools.Set.union vars names, cost_labels, user_labels) 78 79 | Clight.External (id, _, _) -> 79 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in 80 (StringTools.Set.singleton id, CostLabel.Set.empty, 81 Label.Set.empty) in 80 82 let fun_idents (id, f_def) = 81 83 let (names, cost_labels, user_labels) = def_idents f_def in … … 93 95 let all_labels p = 94 96 let (_, cost_labels, user_labels) = prog_idents p in 95 let all = 96 CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) 97 cost_labels StringTools.Set.empty in 98 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all 97 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 98 let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 99 Label.Set.fold StringTools.Set.add user_labels all 99 100 100 101 let all_idents p = 101 102 let (names, cost_labels, user_labels) = prog_idents p in 103 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 104 let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 102 105 let to_string_set fold set = 103 106 fold (fun lbl idents -> StringTools.Set.add lbl idents) set 104 107 StringTools.Set.empty in 105 let cost_labels = to_string_set CostLabel.Set.fold cost_labels in106 108 let user_labels = to_string_set Label.Set.fold user_labels in 107 109 StringTools.Set.union names (StringTools.Set.union cost_labels user_labels) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.mli
r818 r1291 6 6 Then, each cost label in the program is replaced by an increment of the cost 7 7 variable, following the mapping [cost_map]. The function also returns the 8 name of the cost variable and the name of the cost increment function. *) 9 8 name of the cost variable and the name of the cost increment function. 9 10 TODO: int to expressions *) 10 11 val instrument : Clight.program -> int CostLabel.Map.t -> 11 12 Clight.program * string * string -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml
r818 r1291 104 104 | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")" 105 105 | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field 106 | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e) 106 | Ecost (cost_lbl, e) -> 107 let cost_lbl = CostLabel.string_of_cost_label cost_lbl in 108 "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e) 107 109 | Ecall (f, arg, e) -> 108 110 "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")" … … 129 131 | Slabel (lbl, _) -> "label " ^ lbl 130 132 | Sgoto lbl -> "goto " ^ lbl 131 | Scost (lbl, _) -> "cost " ^ lbl 133 | Scost (lbl, _) -> 134 let lbl = CostLabel.string_of_cost_label lbl in 135 "cost " ^ lbl 132 136 133 137 let string_of_local_env lenv = -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml
r818 r1291 6 6 7 7 8 (* Add a cost label in front of a statement . *)8 (* Add a cost label in front of a statement with the current indexing. *) 9 9 10 let add_starting_cost_label cost_universe stmt =11 Clight.Scost (CostLabel. Gen.freshcost_universe, stmt)10 let add_starting_cost_label indexing cost_universe stmt = 11 Clight.Scost (CostLabel.fresh indexing cost_universe, stmt) 12 12 13 13 (* Add a cost label at the end of a statement. *) 14 14 15 let add_ending_cost_label cost_universe stmt = 16 Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip) 15 let add_ending_cost_label indexing cost_universe stmt = 16 let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in 17 Clight.Ssequence (stmt, lbld_skip) 17 18 18 19 … … 24 25 25 26 26 let add_cost_label_e cost_universe e =27 Expr (Ecost (CostLabel. Gen.freshcost_universe, e), typeof e)27 let add_cost_label_e indexing cost_universe e = 28 Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e) 28 29 29 30 30 31 (* Add cost labels to an expression. *) 31 32 32 let rec add_cost_labels_e cost_universe = function33 | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)33 let rec add_cost_labels_e ind cost_universe = function 34 | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty) 34 35 35 and add_cost_labels_expr cost_universe exp = match exp with36 and add_cost_labels_expr ind cost_universe exp = match exp with 36 37 | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp 37 | Ederef e -> Ederef (add_cost_labels_e cost_universe e)38 | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e)39 | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e))38 | Ederef e -> Ederef (add_cost_labels_e ind cost_universe e) 39 | Eaddrof e -> Eaddrof (add_cost_labels_e ind cost_universe e) 40 | Eunop (op,e) -> Eunop (op,(add_cost_labels_e ind cost_universe e)) 40 41 | Ebinop (op,e1,e2) -> 41 42 Ebinop (op, 42 add_cost_labels_e cost_universe e1,43 add_cost_labels_e cost_universe e2)44 | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e)43 add_cost_labels_e ind cost_universe e1, 44 add_cost_labels_e ind cost_universe e2) 45 | Ecast (t,e) -> Ecast (t, add_cost_labels_e ind cost_universe e) 45 46 | Eandbool (e1,e2) -> 46 let e1' = add_cost_labels_e cost_universe e1 in47 let e2' = add_cost_labels_e cost_universe e2 in48 let b1 = add_cost_label_e cost_universe (const_int 1) in49 let b2 = add_cost_label_e cost_universe (const_int 0) in47 let e1' = add_cost_labels_e ind cost_universe e1 in 48 let e2' = add_cost_labels_e ind cost_universe e2 in 49 let b1 = add_cost_label_e ind cost_universe (const_int 1) in 50 let b2 = add_cost_label_e ind cost_universe (const_int 0) in 50 51 let e2' = Expr (Econdition (e2', b1, b2), int_type) in 51 let e2' = add_cost_label_e cost_universe e2' in52 let e3' = add_cost_label_e cost_universe (const_int 0) in52 let e2' = add_cost_label_e ind cost_universe e2' in 53 let e3' = add_cost_label_e ind cost_universe (const_int 0) in 53 54 Econdition (e1', e2', e3') 54 55 | Eorbool (e1,e2) -> 55 let e1' = add_cost_labels_e cost_universe e1 in56 let e2' = add_cost_label_e cost_universe (const_int 1) in57 let e3' = add_cost_labels_e cost_universe e2 in58 let b1 = add_cost_label_e cost_universe (const_int 1) in59 let b2 = add_cost_label_e cost_universe (const_int 0) in56 let e1' = add_cost_labels_e ind cost_universe e1 in 57 let e2' = add_cost_label_e ind cost_universe (const_int 1) in 58 let e3' = add_cost_labels_e ind cost_universe e2 in 59 let b1 = add_cost_label_e ind cost_universe (const_int 1) in 60 let b2 = add_cost_label_e ind cost_universe (const_int 0) in 60 61 let e3' = Expr (Econdition (e3', b1, b2), int_type) in 61 let e3' = add_cost_label_e cost_universe e3' in62 let e3' = add_cost_label_e ind cost_universe e3' in 62 63 Econdition (e1', e2', e3') 63 | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id)64 | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id) 64 65 | Econdition (e1,e2,e3) -> 65 let e1' = add_cost_labels_e cost_universe e1 in66 let e2' = add_cost_labels_e cost_universe e2 in67 let e2' = add_cost_label_e cost_universe e2' in68 let e3' = add_cost_labels_e cost_universe e3 in69 let e3' = add_cost_label_e cost_universe e3' in66 let e1' = add_cost_labels_e ind cost_universe e1 in 67 let e2' = add_cost_labels_e ind cost_universe e2 in 68 let e2' = add_cost_label_e ind cost_universe e2' in 69 let e3' = add_cost_labels_e ind cost_universe e3 in 70 let e3' = add_cost_label_e ind cost_universe e3' in 70 71 Econdition (e1', e2', e3') 71 72 | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *) 72 73 73 let add_cost_labels_opt cost_universe = function 74 | None -> None 75 | Some e -> Some (add_cost_labels_e cost_universe e) 74 let add_cost_labels_opt ind cost_universe = 75 Option.map (add_cost_labels_e ind cost_universe) 76 76 77 let add_cost_labels_lst cost_universe l =78 List.map (add_cost_labels_e cost_universe) l77 let add_cost_labels_lst ind cost_universe l = 78 List.map (add_cost_labels_e ind cost_universe) l 79 79 80 80 81 81 (* Add cost labels to a statement. *) 82 82 83 let rec add_cost_labels_st cost_universe = function83 let rec add_cost_labels_st ind cost_universe = function 84 84 | Sskip -> Sskip 85 85 | Sassign (e1,e2) -> 86 Sassign (add_cost_labels_e cost_universe e1,87 add_cost_labels_e cost_universe e2)86 Sassign (add_cost_labels_e ind cost_universe e1, 87 add_cost_labels_e ind cost_universe e2) 88 88 | Scall (e1,e2,lst) -> 89 Scall (add_cost_labels_opt cost_universe e1,90 add_cost_labels_e cost_universe e2,91 add_cost_labels_lst cost_universe lst)89 Scall (add_cost_labels_opt ind cost_universe e1, 90 add_cost_labels_e ind cost_universe e2, 91 add_cost_labels_lst ind cost_universe lst) 92 92 | Ssequence (s1,s2) -> 93 Ssequence (add_cost_labels_st cost_universe s1,94 add_cost_labels_st cost_universe s2)93 Ssequence (add_cost_labels_st ind cost_universe s1, 94 add_cost_labels_st ind cost_universe s2) 95 95 | Sifthenelse (e,s1,s2) -> 96 let s1' = add_cost_labels_st cost_universe s1 in97 let s1' = add_starting_cost_label cost_universe s1' in98 let s2' = add_cost_labels_st cost_universe s2 in99 let s2' = add_starting_cost_label cost_universe s2' in100 Sifthenelse (add_cost_labels_e cost_universe e, s1', s2')96 let s1' = add_cost_labels_st ind cost_universe s1 in 97 let s1' = add_starting_cost_label ind cost_universe s1' in 98 let s2' = add_cost_labels_st ind cost_universe s2 in 99 let s2' = add_starting_cost_label ind cost_universe s2' in 100 Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2') 101 101 | Swhile (e,s) -> 102 let s' = add_cost_labels_st cost_universe s in103 let s' = add_starting_cost_label cost_universe s' in104 add_ending_cost_label cost_universe105 (Swhile (add_cost_labels_e cost_universe e, s'))102 let s' = add_cost_labels_st ind cost_universe s in 103 let s' = add_starting_cost_label ind cost_universe s' in 104 add_ending_cost_label ind cost_universe 105 (Swhile (add_cost_labels_e ind cost_universe e, s')) 106 106 | Sdowhile (e,s) -> 107 let s1 = add_cost_labels_st cost_universe s in108 let s2 = add_cost_labels_st cost_universe s in109 let s2' = add_starting_cost_label cost_universe s2 in110 add_ending_cost_label cost_universe111 (Ssequence (s1, Swhile (add_cost_labels_e cost_universe e, s2')))107 let s1 = add_cost_labels_st ind cost_universe s in 108 let s2 = add_cost_labels_st ind cost_universe s in 109 let s2' = add_starting_cost_label ind cost_universe s2 in 110 add_ending_cost_label ind cost_universe 111 (Ssequence (s1, Swhile (add_cost_labels_e ind cost_universe e, s2'))) 112 112 | Sfor (s1,e,s2,s3) -> 113 let s1' = add_cost_labels_st cost_universe s1 in114 let s2' = add_cost_labels_st cost_universe s2 in115 let s3' = add_cost_labels_st cost_universe s3 in116 let s3' = add_starting_cost_label cost_universe s3' in117 add_ending_cost_label cost_universe118 (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3'))119 | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e)113 let s1' = add_cost_labels_st ind cost_universe s1 in 114 let s2' = add_cost_labels_st ind cost_universe s2 in 115 let s3' = add_cost_labels_st ind cost_universe s3 in 116 let s3' = add_starting_cost_label ind cost_universe s3' in 117 add_ending_cost_label ind cost_universe 118 (Sfor (s1', add_cost_labels_e ind cost_universe e, s2', s3')) 119 | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e) 120 120 | Sswitch (e,ls) -> 121 Sswitch (add_cost_labels_e cost_universe e,122 add_cost_labels_ls cost_universe ls)121 Sswitch (add_cost_labels_e ind cost_universe e, 122 add_cost_labels_ls ind cost_universe ls) 123 123 | Slabel (lbl,s) -> 124 let s' = add_cost_labels_st cost_universe s in125 let s' = add_starting_cost_label cost_universe s' in124 let s' = add_cost_labels_st ind cost_universe s in 125 let s' = add_starting_cost_label ind cost_universe s' in 126 126 Slabel (lbl,s') 127 127 | Scost (_,_) -> assert false 128 128 | _ as stmt -> stmt 129 129 130 and add_cost_labels_ls cost_universe = function130 and add_cost_labels_ls ind cost_universe = function 131 131 | LSdefault s -> 132 let s' = add_cost_labels_st cost_universe s in133 let s' = add_starting_cost_label cost_universe s' in132 let s' = add_cost_labels_st ind cost_universe s in 133 let s' = add_starting_cost_label ind cost_universe s' in 134 134 LSdefault s' 135 135 | LScase (i,s,ls) -> 136 let s' = add_cost_labels_st cost_universe s in137 let s' = add_starting_cost_label cost_universe s' in138 LScase (i, s', add_cost_labels_ls cost_universe ls)136 let s' = add_cost_labels_st ind cost_universe s in 137 let s' = add_starting_cost_label ind cost_universe s' in 138 LScase (i, s', add_cost_labels_ls ind cost_universe ls) 139 139 140 140 141 141 (* Add cost labels to a function. *) 142 142 143 let add_cost_labels_f cost_universe = function143 let add_cost_labels_f ind cost_universe = function 144 144 | (id,Internal fd) -> (id,Internal { 145 145 fn_return = fd.fn_return ; 146 146 fn_params = fd.fn_params ; 147 147 fn_vars = fd.fn_vars ; 148 fn_body = add_starting_cost_label cost_universe149 (add_cost_labels_st cost_universe fd.fn_body)148 fn_body = add_starting_cost_label ind cost_universe 149 (add_cost_labels_st ind cost_universe fd.fn_body) 150 150 }) 151 151 | (id,External (a,b,c)) -> (id,External (a,b,c)) … … 157 157 let add_cost_labels p = 158 158 let labs = ClightAnnotator.all_labels p in 159 let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in 160 let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in 161 let cost_universe = CostLabel.Gen.new_universe cost_prefix in 159 let add = CostLabel.Atom.Set.add in 160 let empty = CostLabel.Atom.Set.empty in 161 let labs = StringTools.Set.fold add labs empty in 162 let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in 163 let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in 164 let ind = CostLabel.Indexing.empty in 162 165 { 163 prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct;166 prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct; 164 167 prog_main = p.prog_main; 165 168 prog_vars = p.prog_vars -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightPrinter.ml
r818 r1291 196 196 | Efield(e1, id) -> 197 197 fprintf p "%a.%s" print_expr_prec (level, e1) id 198 | Ecost (lbl,e1) -> 199 fprintf p "(/* %s */ %a)" lbl print_expr e1 200 | Ecall (f, arg, e) -> 198 | Ecost(lbl, e1) -> 199 (* printing label uglily even if in comment for consistence *) 200 let lbl = CostLabel.string_of_cost_label lbl in 201 fprintf p "(/* %s */ %a)" lbl print_expr e1 202 | Ecall(f, arg, e) -> 201 203 fprintf p "(%s(%a), %a)" f print_expr arg print_expr e 202 204 … … 272 274 fprintf p "goto %s;" lbl 273 275 | Scost (lbl,s1) -> 276 let lbl = CostLabel.string_of_cost_label lbl in 274 277 fprintf p "%s:@ %a" lbl print_stmt s1 275 278 -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorAnnotator.ml
r818 r1291 204 204 let all_labels p = 205 205 let (cost_labels, user_labels) = prog_labels p in 206 let all = 207 CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) 208 cost_labels StringTools.Set.empty in 206 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 207 let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 209 208 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml
r818 r1291 65 65 | St_label (lbl, _) -> "label " ^ lbl 66 66 | St_goto lbl -> "goto " ^ lbl 67 | St_cost (lbl, _) -> "cost " ^ lbl 67 | St_cost (lbl, _) -> 68 let lbl = CostLabel.string_of_cost_label lbl in 69 "cost " ^ lbl 68 70 69 71 let print_state = function -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorPrinter.ml
r818 r1291 116 116 (add_parenthesis e3) 117 117 | Cminor.Exp_cost (lab, e) -> 118 let lab = CostLabel.string_of_cost_label lab in 118 119 Printf.sprintf "/* %s */ %s" lab (print_expression e) 119 120 and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with … … 208 209 Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl 209 210 | Cminor.St_cost (lbl, s) -> 210 Printf.sprintf "%s%s:\n%s" 211 211 let lbl = CostLabel.string_of_cost_label lbl in 212 Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s) 212 213 213 214 let print_internal f_name f_def = -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml
r486 r1291 1 module Atom = 2 struct 3 include StringTools 4 end 1 5 2 include StringTools 6 module StringMap = Map.Make(String) 7 8 module Index = 9 struct 10 include StringTools 11 end 12 13 (** Simple expressions are for now affine maps of the form a*_+b *) 14 type sexpr = 15 | Sexpr of int*int 16 17 let sexpr_id = Sexpr(1, 0) 18 19 let sexpr_of i l = snd (List.find (function (j, _) -> j = i) l) 20 21 (** not using Map as insertion order matters *) 22 module Indexing = 23 struct 24 type t = (Index.t * sexpr) list 25 let compare = compare (* built-in lexicographic order *) 26 let empty = [] 27 end 28 29 (* a*_+b is composed with c*_+d by substitution: *) 30 (* namely a*_+b ° c*_+d = c*(a*_+b)+d *) 31 let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) = 32 Sexpr (a * c, b * c + d) 33 34 (* i|-->e ° j|-->f = j|-->e°f if i=j, j|-->f otherwise *) 35 (* NB: if simple expressions are changed to more complex ones,*) 36 (* this must change *) 37 let compose_index_singl i1 s1 (i2,s2) = 38 (i2, if i1 = i2 then compose_sexpr s1 s2 else s2) 39 40 (* i|-->e ° I *) 41 let compose_index i s = List.map (compose_index_singl i s) 42 43 (* I°J applies every mapping in I to every mapping in J *) 44 (* TODO: can we use the shape indexings have in actual usage? *) 45 let compose_indexing = List.fold_right (function (i,s) -> compose_index i s) 46 47 48 module IndexingSet = Set.Make(Indexing) 49 50 51 type t = { 52 name : Atom.t; 53 i : Indexing.t 54 } 55 56 (* if [pretty] is false then a name suitable for labels is given*) 57 (* ('P' replaces '+') *) 58 let string_of_sexpr pretty id (Sexpr(a, b)) = 59 let plus = if pretty then "+" else "P" in 60 let a_id_s = if a = 1 then id else string_of_int a^id in 61 let b_s = string_of_int b in 62 if a = 0 then b_s else 63 if b = 0 then a_id_s else a_id_s^plus^b_s 64 65 (* examples:*) 66 (* [pretty] true: (0,i+1,2j+2)*) 67 (* [pretty] false: _0_iP1_2jP2 *) 68 let string_of_indexing pretty = function 69 | [] -> "" 70 | (i, s) :: l -> 71 (* !!! assuming i starts with '_' which can be omitted !!! *) 72 let i = String.sub i 1 (String.length i) in 73 let left = if pretty then "(" else "_" in 74 let right = if pretty then ")" else "" in 75 let sep = if pretty then "," else "_" in 76 let first = string_of_sexpr pretty i s in 77 let f accu (j, t) = accu ^ sep ^ (string_of_sexpr pretty j t) in 78 left ^ List.fold_left f first l ^ right 79 80 let string_of_cost_label ?(pretty = false) lab = 81 lab.name ^ string_of_indexing pretty lab.i 82 83 let fresh l universe = 84 {name = Atom.Gen.fresh universe; i = l} 85 86 (* TODO: urgh. Necessary? *) 87 type aux_t = t 88 89 (** labels are endowed with a lexicographical ordering *) 90 module T : Map.OrderedType with type t = aux_t = 91 struct 92 type t = aux_t 93 let compare = compare (* uses the built-in lexicographical comparison *) 94 end 95 96 module Map = Map.Make(T) 97 module Set = Set.Make(T) 98 (** [constant_map d x] produces a finite map which associates 99 [x] to every element of the set [d]. *) 100 101 let indexings_of atom s = 102 let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in 103 Set.fold f s IndexingSet.empty 3 104 4 105 let constant_map d x = 5 106 Set.fold (fun k accu -> Map.add k x accu) d Map.empty 107 108 (** **) -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli
r486 r1291 1 1 2 (** This module provides functions to manipulate and create freshcost2 (** This module provides functions to manipulate and create indexed cost 3 3 labels. *) 4 5 (** [Atom] provides functions for cost atoms, the root of indexed costs *) 6 module Atom : sig 7 include StringSig.S 8 end 4 9 5 include StringSig.S 10 (** Loop indices, to be identified with Clight identifiers *) 11 module Index : sig 12 include StringSig.S 13 end 14 15 (** Simple expressions corresponding to loop tranformations. *) 16 type sexpr 17 18 val sexpr_id : sexpr 19 20 module Indexing : sig 21 include Set.OrderedType 22 val empty : t 23 end 24 25 (** [sexpr_of i l] extracts the simple expression relative to [i] in [l]. 26 It raises an [Invalid_argument] exception if [i] is not handled by [l] *) 27 val sexpr_of : Index.t -> Indexing.t -> sexpr 28 29 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 30 val compose_index : Index.t -> sexpr -> Indexing.t -> Indexing.t 31 32 (** [compose_index l m] applies all the transformations in [l] to [m] *) 33 val compose_indexing : Indexing.t -> Indexing.t -> Indexing.t 34 35 module IndexingSet : Set.S with type elt = Indexing.t 36 37 type t = { 38 name : Atom.t; 39 i : Indexing.t 40 } 41 42 (** [string_of_cost_label t] converts an indexed label to a 43 string suitable for a label name in source. 44 [string_of_cost_label ~pretty:true t] prints a more readable form *) 45 val string_of_cost_label : ?pretty : bool -> t -> string 46 47 (** [fresh i u] creates a fresh label using [u] as name universe, inside 48 the indexing [i] (which represents the nested loops containing the label) *) 49 val fresh : Indexing.t -> Atom.Gen.universe -> t 50 51 module Set : Set.S with type elt = t 52 module Map : Map.S with type key = t 53 54 (** [indexings_of a s] produces the set of indexings of an atom [a] occurring 55 in the set of indexed labels [s]. *) 56 val indexings_of : Atom.t -> Set.t -> IndexingSet.t 6 57 7 58 (** [constant_map d x] produces a finite map which associates 8 59 [x] to every element of the set [d]. *) 9 60 val constant_map : Set.t -> 'a -> 'a Map.t 61
Note: See TracChangeset
for help on using the changeset viewer.