Changeset 1679 for Deliverables/D5.15.3/costplugin/plugin/cost_value.ml
 Timestamp:
 Feb 7, 2012, 6:01:43 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D5.15.3/costplugin/plugin/cost_value.ml
r1462 r1679 2 2 (** This module describes the values manipulated by the plugin. *) 3 3 4 5 type relation = Lt  Gt  Le  Ge6 7 let string_of_relation = function8  Lt > "<"9  Le > "<="10  Gt > ">"11  Ge > ">="12 13 let bool_fun_of_relation = function14  Lt > (<)15  Le > (<=)16  Gt > (>)17  Ge > (>=)18 19 let mk_strict = function20  Lt  Le > Lt21  Gt  Ge > Gt22 23 let mk_large = function24  Lt  Le > Le25  Gt  Ge > Ge26 27 let opposite = function28  Lt > Ge29  Le > Gt30  Gt > Le31  Ge > Lt32 33 type unop = Neg34 35 let string_of_unop = function36  Neg > ""37 38 let int_fun_of_unop = function39  Neg > (fun x > (x))40 41 type binop = Add  Sub  Div  Mul  Mod  Max42 43 let string_of_binop = function44  Add > "+"45  Sub > ""46  Div > "/"47  Mul > "*"48  Mod > "%"49  Max > "max"50 51 let int_fun_of_binop = function52  Add > (+)53  Sub > ()54  Div > (/)55  Mul > ( * )56  Mod > (mod)57  Max > max58 59 (** Cost values *)60 61 type t =62  Int of int63  Var of string (* either a parameter or a global, but not a local *)64  UnOp of unop * t65  BinOp of binop * t * t66  Cond of t * relation * t * t * t (* ternary expressions *)67  CostOf of string * t list (* cost of a function: function name * args *)68  Any (* any other C expression *)69 70 (** [abs v] return a cost value that represents the absolute value of [v]. *)71 72 let abs v = Cond (Int 0, Le, v, v, UnOp (Neg, v))73 74 75 (** [subs v] returns the subvalues of the cost value [v]. *)76 77 let subs = function78  Int _  Var _  Any > []79  UnOp (_, v) > [v]80  BinOp (_, v1, v2) > [v1 ; v2]81  Cond (t1, _, t2, tif, telse) > [t1 ; t2 ; tif ; telse]82  CostOf (_, args) > args83 84 (** [fill_subs s subs] replaces the subvalues of the cost value [v] with85 those in [subs]. *)86 87 let fill_subs v subs = match v, subs with88  Int _, _  Var _, _  Any, _ > v89  UnOp (unop, _), v :: _ > UnOp (unop, v)90  BinOp (binop, _, _), v1 :: v2 :: _ > BinOp (binop, v1, v2)91  Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ >92 Cond (t1, rel, t2, tif, telse)93  CostOf (fun_name, _), _ > CostOf (fun_name, subs)94  _ > raise (Failure "Cost_value.fill_subs") (* wrong number of arguments *)95 96 (** [fold f v] recursively apply the function [f] on the cost value [v] and its97 children, starting from the leaves and going up in the tree. [f]'s type is98 [t > 'a list > 'a], where the second argument is the results of the fold99 on [v]'s subvalues. *)100 101 let rec fold (f : t > 'a list > 'a) v =102 let subs_res = List.map (fold f) (subs v) in103 f v subs_res104 105 106 let rec f_to_string v subs_res = match v, subs_res with107  Int i, _ > string_of_int i108  Var x, _ > x109  UnOp (unop, _), v :: _ > (string_of_unop unop) ^ "(" ^ v ^ ")"110  BinOp (binop, _, _), v1 :: v2 :: _ >111 "(" ^ v1 ^ ")" ^ (string_of_binop binop) ^ "(" ^ v2 ^ ")"112  Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ >113 Printf.sprintf "(%s %s %s)? (%s) : (%s)"114 t1 (string_of_relation rel) t2 tif telse115  CostOf (fun_name, _), args >116 let f res v = res ^ v ^ ", " in117 fun_name ^ "(" ^ (List.fold_left f "" args) ^ ")"118  Any, _ > "any"119  UnOp _, _  BinOp _, _  Cond _, _ >120 assert false (* wrong number of arguments *)121 122 and to_string v = fold f_to_string v123 124 125 (* Variables of a cost value *)126 127 let union_list l =128 List.fold_left StringTools.Set.union StringTools.Set.empty l129 130 let f_vars v subs_res =131 let v_res = match v with132  Var x > StringTools.Set.singleton x133  _ > StringTools.Set.empty in134 union_list (v_res :: subs_res)135 136 (** [vars v] returns the set of variables of the cost value [v]. *)137 138 let vars = fold f_vars139 140 141 (* Replace variables by expressions *)142 143 (*144 let f_replace r_list v subs_res =145 let v = match v with146  Var x when List.mem_assoc x r_list > List.assoc x r_list147  _ > v in148 fill_subs v subs_res149 *)150 151 let f_replace r_list v subs_res = match fill_subs v subs_res with152  Var x when List.mem_assoc x r_list > List.assoc x r_list153  v > v154 155 (** [replace r_list v] replaces the variables of [v] that are in the association156 list [r_list] with their associated cost value. *)157 158 let replace (r_list : (string * t) list) = fold (f_replace r_list)159 160 161 (* Value reduction (or partial computation) *)162 163 (* Raised when a function is not found in the cost environment *)164 4 exception Unknown_cost of string 165 (* Raised when the prototype of a function is not found *)166 5 exception Unknown_prototype of string 167 6 168 let f_is_independent v subs_res = 169 let v_res = match v with 170  CostOf _ > false 171  _ > true in 172 List.fold_left (&&) true (v_res :: subs_res) 173 174 (** [is_independent v] returns true if and only if the cost value [v] is 175 independent of the cost of other functions (i.e. does not have a CostOf). *) 176 177 let is_independent = fold f_is_independent 178 179 (* Reduction of a cost in the case of a CostOf construct. Replace the formal 180 parameters of the function by the actual arguments. *) 181 182 let f_reduce_CostOf extern_costs costs prots fun_name args = 183 if StringTools.Map.mem fun_name extern_costs then 184 Var (StringTools.Map.find fun_name extern_costs) 185 else 186 if StringTools.Map.mem fun_name prots then 187 let formals = StringTools.Map.find fun_name prots in 188 if List.length formals = List.length args then 189 let r_list = List.combine formals args in 190 if StringTools.Map.mem fun_name costs then 191 let cost = StringTools.Map.find fun_name costs in 192 if is_independent cost then replace r_list cost 193 else CostOf (fun_name, args) 194 else raise (Unknown_cost fun_name) 7 8 let string_of_mset to_list sep f mset = 9 let filter (_, occ) = occ <> 0 in 10 let f' (elt, occ) = 11 if occ = 1 then (f elt) 12 else Printf.sprintf "%d*%s" occ (f elt) in 13 Misc.List.to_string sep f' (List.filter filter (to_list mset)) 14 15 type prototypes = string list Misc.String.Map.t 16 17 18 module type S = sig 19 20 type relation 21 val is_large : relation > bool 22 val has_lower_type : relation > bool 23 24 type t 25 26 val top : t 27 val of_int : int > t 28 val of_var : string > t 29 val add : t > t > t 30 val minus : t > t > t 31 val mul : t > t > t 32 val div : t > t > t 33 val max : t > t > t 34 val cond : t > relation > t > t > t > t 35 val join : t > t > t 36 val widen : t > t > t 37 val narrow : t > t > t 38 39 val le : t > t > bool 40 41 val replace_vars : t Misc.String.Map.t > t > t 42 43 val to_string : t > string 44 val string_of_relation : relation > string 45 46 val compare : t > t > int 47 48 end 49 50 51 module Make (S : S) = struct 52 53 let s_add_list = function 54  [] > S.of_int 0 55  e :: l > List.fold_left S.add e l 56 57 module Args = struct 58 59 type t = S.t list 60 61 let compare = Misc.List.compare S.compare 62 63 let le args1 args2 = 64 if List.length args1 <> List.length args2 then false 195 65 else 196 raise 197 (Failure ("Cost_value.f_reduce_CostOf: formals and actuals for " ^ 198 "function " ^ fun_name ^ " have different sizes.")) 199 else raise (Unknown_prototype fun_name) 200 201 (* Reduction in the general case. When some specific patterns are found that 202 allow to perform a computation (for instance when applying an operation to 203 some integer values), return the result. *) 204 205 let f_reduce extern_costs costs prots v subs_res = match v, subs_res with 206  UnOp (unop, _), (Int i) :: _ > Int (int_fun_of_unop unop i) 207  UnOp (Neg, _), (UnOp (Neg, v)) :: _ > v 208  BinOp (binop, _, _), (Int i1) :: (Int i2) :: _ > 209 Int (int_fun_of_binop binop i1 i2) 210  BinOp (Add, _, _), (BinOp (Add, v, Int i1)) :: (Int i2) :: _ 211  BinOp (Add, _, _), (BinOp (Add, Int i1, v)) :: (Int i2) :: _ > 212 BinOp (Add, Int (i1 + i2), v) 213  BinOp (Add, _, _), v :: (Int 0) :: _ 214  BinOp (Sub, _, _), v :: (Int 0) :: _ 215  BinOp (Add, _, _), (Int 0) :: v :: _ 216  BinOp (Div, _, _), v :: (Int 1) :: _ 217  BinOp (Mul, _, _), v :: (Int 1) :: _ 218  BinOp (Mul, _, _), (Int 1) :: v :: _ > v 219  BinOp (Sub, _, _), (Int 0) :: v :: _ 220  BinOp (Div, _, _), v :: (Int (1)) :: _ 221  BinOp (Mul, _, _), v :: (Int (1)) :: _ 222  BinOp (Mul, _, _), (Int (1)) :: v :: _ > UnOp (Neg, v) 223  BinOp (Div, _, _), (Int 0) :: _ :: _ 224  BinOp (Mul, _, _), _ :: (Int 0) :: _ 225  BinOp (Mul, _, _), (Int 0) :: _ :: _ 226  BinOp (Mod, _, _), (Int 0) :: _ :: _ 227  BinOp (Mod, _, _), _ :: (Int 1) :: _ > Int 0 228  Cond (_, rel, _, _, _), (Int i1) :: (Int i2) :: tif :: _ 229 when bool_fun_of_relation rel i1 i2 > tif 230  Cond (_, rel, _, _, _), (Int i1) :: (Int i2) :: _ :: telse :: _ 231 when not (bool_fun_of_relation rel i1 i2) > telse 232  CostOf (fun_name, _), args > 233 f_reduce_CostOf extern_costs costs prots fun_name args 234  _ > fill_subs v subs_res 235 236 (** [reduce extern_costs costs prots v] apply a partial computation on the value 237 [v] when considering the cost associated to each function in [costs] and 238 their prototype [prots]. *) 239 240 let reduce 241 (extern_costs : string StringTools.Map.t) 242 (costs : t StringTools.Map.t) 243 (prots : string list StringTools.Map.t) 244 : t > t = 245 fold (f_reduce extern_costs costs prots) 246 247 (** [reduces extern_costs costs prots costs_to_reduce] applies a cost reduction 248 on every cost in the mapping [costs_to_reduce]. *) 249 250 let reduces 251 (extern_costs : string StringTools.Map.t) 252 (costs : t StringTools.Map.t) 253 (prots : string list StringTools.Map.t) 254 (costs_to_reduce : t StringTools.Map.t) 255 : t StringTools.Map.t = 256 StringTools.Map.map (reduce extern_costs costs prots) costs_to_reduce 257 258 259 (* Raised when an unsupported expression is found. *) 260 exception Unsupported_exp 261 (* Raised when an unsupported comparison relation. *) 262 exception Unsupported_rel 263 264 265 let rel_of_cil_rel = function 266  Cil_types.Lt > Lt 267  Cil_types.Gt > Gt 268  Cil_types.Le > Le 269  Cil_types.Ge > Ge 270  _ > raise Unsupported_rel 271 272 let cil_rel_of_rel = function 273  Lt > Cil_types.Rlt 274  Gt > Cil_types.Rgt 275  Le > Cil_types.Rle 276  Ge > Cil_types.Rge 277 278 let cil_binop_of_rel = function 279  Lt > Cil_types.Lt 280  Gt > Cil_types.Gt 281  Le > Cil_types.Le 282  Ge > Cil_types.Ge 283 284 285 let unop_of_cil_unop = function 286  Cil_types.Neg > Neg 287  _ > raise (Failure "unop_of_cil_unop") 288 289 let binop_of_cil_binop = function 290  Cil_types.PlusA > Add 291  Cil_types.MinusA > Sub 292  Cil_types.Mult > Mul 293  Cil_types.Div > Div 294  Cil_types.Mod > Mod 295  _ > raise (Failure "binop_of_cil_binop") 296 297 (** [of_cil_exp e] returns a cost value equivalent to the CIL expression [e]. *) 298 299 let rec of_cil_exp e = 300 try match e.Cil_types.enode with 301  Cil_types.Const (Cil_types.CInt64 (i, _, _)) > Int (Int64.to_int i) 302  Cil_types.Lval (Cil_types.Var var, _) > Var (var.Cil_types.vname) 303  Cil_types.UnOp (unop, e, _) > UnOp (unop_of_cil_unop unop, of_cil_exp e) 304  Cil_types.BinOp (binop, e1, e2, _) > 305 BinOp (binop_of_cil_binop binop, of_cil_exp e1, of_cil_exp e2) 306  Cil_types.Info (e, _) > of_cil_exp e 307  _ > Any 308 with Failure ("unop_of_cil_unop"  "binop_of_cil_binop") > Any 309 310 311 let cil_unop_of_unop = function 312  Neg > Cil_types.Neg 313 314 let cil_binop_of_binop = function 315  Add > Cil_types.PlusA 316  Sub > Cil_types.MinusA 317  Mul > Cil_types.Mult 318  Div > Cil_types.Div 319  Mod > Cil_types.Mod 320 (* No direct translation. Handle this case in the calling function. *) 321  Max > assert false 322 323 324 let integer_term term = Logic_const.term term Cil_types.Linteger 325 326 let tinteger i = 327 let cint64 = Cil_types.CInt64 (Int64.of_int i, Cil_types.IInt, None) in 328 let iterm = Cil_types.TConst cint64 in 329 integer_term iterm 330 331 let f_to_cil_term v subs_res = match v, subs_res with 332  Int i, _ > tinteger i 333  Var x, _ > Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger) 334  UnOp (unop, _), t :: _ > 335 integer_term (Cil_types.TUnOp (cil_unop_of_unop unop, t)) 336  UnOp _, _ > assert false (* wrong number of arguments *) 337  BinOp (Max, _, _), t1 :: t2 :: _ > 338 let test = integer_term (Cil_types.TBinOp (Cil_types.Ge, t1, t2)) in 339 integer_term (Cil_types.Tif (test, t1, t2)) 340  BinOp (binop, _, _), t1 :: t2 :: _ > 341 integer_term (Cil_types.TBinOp (cil_binop_of_binop binop, t1, t2)) 342  BinOp _, _ > assert false (* wrong number of arguments *) 343  Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ > 344 let test = integer_term (Cil_types.TBinOp (cil_binop_of_rel rel, t1, t2)) in 345 integer_term (Cil_types.Tif (test, tif, telse)) 346  Cond _, _ > assert false (* wrong number of arguments *) 347  CostOf _, _ > assert false (* should never be used on these arguments *) 348  Any, _ > raise Unsupported_exp 349 350 (** [to_cil_term v] returns a CIL logic term equivalent to the cost value 351 [v]. *) 352 353 let to_cil_term = fold f_to_cil_term 354 355 356 let f_has_locals locals e subs_res = 357 let e_res = match e with 358  Var x > StringTools.Set.mem x locals 359  _ > false in 360 List.fold_left () false (e_res :: subs_res) 361 362 (** [has_locals locals v] returns true if and only if the cost value [v] has a 363 variable in the set [locals]. *) 364 365 let has_locals locals = fold (f_has_locals locals) 366 367 368 let f_has_any e subs_res = List.fold_left () false ((e = Any) :: subs_res) 369 370 (** [has_any v] returns true if and only if the cost value [v] has an Any 371 construct. *) 372 373 let has_any = fold f_has_any 66 let f res arg1 arg2 = res && (S.le arg1 arg2) in 67 List.fold_left2 f true args1 args2 68 69 let replace_vars replacements = List.map (S.replace_vars replacements) 70 71 let to_string = Misc.List.to_string ", " S.to_string 72 73 end 74 75 76 module Externs = struct 77 78 module M = Misc.String.MSet 79 include M 80 81 let add = union 82 83 let le = subset 84 85 let replace_vars _ externs = externs 86 87 let to_string = string_of_mset to_list " + " (fun x > x) 88 89 let to_ext externs = 90 let f x occ ext = S.add (S.mul (S.of_int occ) (S.of_var x)) ext in 91 fold f externs (S.of_int 0) 92 93 end 94 95 96 module FunCall = struct 97 98 type t = 99 { caller : string ; 100 id : int ; 101 callee : string ; 102 args : Args.t } 103 let compare = Pervasives.compare 104 105 let caller fun_call = fun_call.caller 106 let id fun_call = fun_call.id 107 let callee fun_call = fun_call.callee 108 let args fun_call = fun_call.args 109 110 let make caller id callee args = { caller ; id ; callee ; args } 111 112 let apply f f_caller f_id f_callee f_args fun_call = 113 let caller_res = f_caller (caller fun_call) in 114 let id_res = f_id (id fun_call) in 115 let callee_res = f_callee (callee fun_call) in 116 let args_res = f_args (args fun_call) in 117 f caller_res id_res callee_res args_res 118 119 let apply2 f f_caller f_id f_callee f_args fun_call1 fun_call2 = 120 let caller_res = f_caller (caller fun_call1) (caller fun_call2) in 121 let id_res = f_id (id fun_call1) (id fun_call2) in 122 let callee_res = f_callee (callee fun_call1) (callee fun_call2) in 123 let args_res = f_args (args fun_call1) (args fun_call2) in 124 f caller_res id_res callee_res args_res 125 126 let le = 127 let f b1 b2 b3 b4 = b1 && b2 && b3 && b4 in 128 apply2 f (=) (=) (=) Args.le 129 130 let replace_vars replacement = 131 apply make Misc.id Misc.id Misc.id (Args.replace_vars replacement) 132 133 let reduce 134 to_list is_solved replace_vars of_fun_call 135 prototypes costs fun_call = 136 let callee = callee fun_call in 137 let args = args fun_call in 138 if Misc.String.Map.mem callee prototypes then 139 let formals = Misc.String.Map.find callee prototypes in 140 if List.length formals = List.length args then 141 let replacements = 142 Misc.String.Map.of_list (List.combine formals args) in 143 if Misc.String.Map.mem callee costs then 144 let cost' = Misc.String.Map.find callee costs in 145 if is_solved cost' then to_list (replace_vars replacements cost') 146 else [of_fun_call fun_call] 147 else raise (Unknown_cost callee) 148 else 149 raise 150 (Failure ("FunCall.reduce: formals and actuals for " ^ 151 "function " ^ callee ^ " have different sizes.")) 152 else raise (Unknown_prototype callee) 153 154 let to_string fun_call = 155 Printf.sprintf "%s@[%s,%d](%s)" 156 (callee fun_call) (caller fun_call) (id fun_call) 157 (Args.to_string (args fun_call)) 158 159 end 160 161 module FunCalls = struct 162 163 module M = Multiset.Make (FunCall) 164 include M 165 166 let singleton_ fun_call = M.add fun_call empty 167 168 let singleton caller id callee args = 169 singleton (FunCall.make caller id callee args) 170 171 let add = union 172 173 let le1 fun_call occ fun_calls = 174 let f fun_call' occ' = (FunCall.le fun_call fun_call') && (occ <= occ') in 175 exists f fun_calls 176 177 let le fun_calls1 fun_calls2 = 178 let f fun_call occ = le1 fun_call occ fun_calls2 in 179 for_all f fun_calls1 180 181 let called_funs fun_calls = 182 let f fun_call _ called_funs = 183 Misc.String.Set.add (FunCall.callee fun_call) called_funs in 184 fold f fun_calls Misc.String.Set.empty 185 186 let replace_vars replacements fun_calls = 187 let f fun_call _ fun_calls = 188 let fun_call = FunCall.replace_vars replacements fun_call in 189 add (singleton_ fun_call) fun_calls in 190 fold f fun_calls empty 191 192 let to_string = string_of_mset to_list " + " FunCall.to_string 193 194 end 195 196 197 module rec LoopCost : sig 198 type t 199 val compare : t > t > int 200 val make : string > int > S.relation > S.t > S.t > S.t > Cost.t > t 201 val le : t > t > bool 202 val called_funs : t > Misc.String.Set.t 203 val replace_vars : S.t Misc.String.Map.t > t > t 204 val reduce : prototypes > Cost.t Misc.String.Map.t > t > t 205 val to_string : t > string 206 val to_ext : t > S.t 207 end = struct 208 209 type t = 210 { fun_name : string ; 211 id : int ; 212 relation : S.relation ; 213 init_value : S.t ; 214 exit_value : S.t ; 215 increment : S.t ; 216 body_cost : Cost.t } 217 218 let make fun_name id relation init_value exit_value increment body_cost = 219 { fun_name ; id ; relation ; init_value ; exit_value ; increment ; 220 body_cost } 221 222 let fun_name loop_cost = loop_cost.fun_name 223 let id loop_cost = loop_cost.id 224 let relation loop_cost = loop_cost.relation 225 let init_value loop_cost = loop_cost.init_value 226 let exit_value loop_cost = loop_cost.exit_value 227 let increment loop_cost = loop_cost.increment 228 let body_cost loop_cost = loop_cost.body_cost 229 230 let compare = Pervasives.compare 231 232 let apply f 233 f_fun_name f_id f_relation f_init_value f_exit_value f_increment 234 f_body_cost loop_cost = 235 let fun_name_res = f_fun_name (fun_name loop_cost) in 236 let id_res = f_id (id loop_cost) in 237 let relation_res = f_relation (relation loop_cost) in 238 let init_value_res = f_init_value (init_value loop_cost) in 239 let exit_value_res = f_exit_value (exit_value loop_cost) in 240 let increment_res = f_increment (increment loop_cost) in 241 let body_cost_res = f_body_cost (body_cost loop_cost) in 242 f 243 fun_name_res id_res relation_res init_value_res exit_value_res 244 increment_res body_cost_res 245 246 let apply2 f 247 f_fun_name f_id f_relation f_init_value f_exit_value f_increment 248 f_body_cost loop_cost1 loop_cost2 = 249 let fun_name_res = 250 f_fun_name (fun_name loop_cost1) (fun_name loop_cost2) in 251 let id_res = f_id (id loop_cost1) (id loop_cost2) in 252 let relation_res = 253 f_relation (relation loop_cost1) (relation loop_cost2) in 254 let init_value_res = 255 f_init_value (init_value loop_cost1) (init_value loop_cost2) in 256 let exit_value_res = 257 f_exit_value (exit_value loop_cost1) (exit_value loop_cost2) in 258 let increment_res = 259 f_increment (increment loop_cost1) (increment loop_cost2) in 260 let body_cost_res = 261 f_body_cost (body_cost loop_cost1) (body_cost loop_cost2) in 262 f 263 fun_name_res id_res relation_res init_value_res exit_value_res 264 increment_res body_cost_res 265 266 let le = 267 let f b1 b2 b3 b4 b5 b6 b7 = b1 && b2 && b3 && b4 && b5 && b6 && b7 in 268 apply2 f (=) (=) (=) S.le S.le S.le Cost.le 269 270 let called_funs loop_cost = Cost.called_funs (body_cost loop_cost) 271 272 let replace_vars replacements = 273 let arg_replace_vars = S.replace_vars replacements in 274 apply make Misc.id Misc.id Misc.id arg_replace_vars arg_replace_vars 275 arg_replace_vars (Cost.replace_vars replacements) 276 277 let reduce prototypes costs = 278 apply make Misc.id Misc.id Misc.id Misc.id Misc.id Misc.id 279 (Cost.reduce prototypes costs) 280 281 let to_string loop_cost = 282 Printf.sprintf "%s@%d(%s %s %s %s (%s))" 283 (fun_name loop_cost) 284 (id loop_cost) 285 (S.string_of_relation (relation loop_cost)) 286 (S.to_string (init_value loop_cost)) 287 (S.to_string (exit_value loop_cost)) 288 (S.to_string (increment loop_cost)) 289 (Cost.to_string (body_cost loop_cost)) 290 291 let to_ext loop_cost = 292 let rel = relation loop_cost in 293 let init_value = init_value loop_cost in 294 let exit_value = exit_value loop_cost in 295 let increment = increment loop_cost in 296 let body_cost = body_cost loop_cost in 297 let rel_op = if S.has_lower_type rel then S.minus else S.add in 298 let rel_added = S.of_int (if S.is_large rel then 0 else 1) in 299 let iteration_nb = rel_op increment rel_added in 300 let iteration_nb = S.minus iteration_nb init_value in 301 let iteration_nb = S.add exit_value iteration_nb in 302 let iteration_nb = S.div iteration_nb increment in 303 let body_cost = Cost.to_ext body_cost in 304 let cond_body_cost = 305 S.cond init_value rel exit_value body_cost (S.of_int 0) in 306 S.mul iteration_nb cond_body_cost 307 308 end 309 310 311 and LoopCosts : sig 312 type t 313 val empty : t 314 val singleton : 315 string > int > S.relation > S.t > S.t > S.t > Cost.t > t 316 val add : t > t > t 317 val replace_vars : S.t Misc.String.Map.t > t > t 318 val called_funs : t > Misc.String.Set.t 319 val reduce : prototypes > Cost.t Misc.String.Map.t > t > t 320 val to_string : t > string 321 val le : t > t > bool 322 val to_ext : t > S.t 323 end = struct 324 325 module M = Multiset.Make (LoopCost) 326 include M 327 328 let singleton_ loop_cost = M.add loop_cost empty 329 330 let singleton 331 fun_name id relation init_value exit_value increment body_cost = 332 let loop_cost = 333 LoopCost.make 334 fun_name id relation init_value exit_value increment body_cost in 335 singleton_ loop_cost 336 337 let add = union 338 339 let le1 loop_cost occ loop_costs = 340 let f loop_cost' occ' res = 341 res  ((LoopCost.le loop_cost loop_cost') && (occ <= occ')) in 342 fold f loop_costs false 343 344 let le loop_costs1 loop_costs2 = 345 let f loop_cost occ res = res && le1 loop_cost occ loop_costs2 in 346 fold f loop_costs1 true 347 348 let called_funs loop_costs = 349 let f loop_cost _ called_funs = 350 Misc.String.Set.union (LoopCost.called_funs loop_cost) called_funs in 351 fold f loop_costs Misc.String.Set.empty 352 353 let replace_vars replacements loop_costs = 354 let f loop_cost _ loop_costs = 355 let loop_cost = LoopCost.replace_vars replacements loop_cost in 356 add (singleton_ loop_cost) loop_costs in 357 fold f loop_costs empty 358 359 let reduce prototypes replacements loop_costs = 360 let f loop_cost occ loop_costs = 361 add_occ (LoopCost.reduce prototypes replacements loop_cost) occ 362 loop_costs in 363 fold f loop_costs empty 364 365 let to_string = string_of_mset to_list " + " LoopCost.to_string 366 367 let to_ext loop_costs = 368 let f loop_cost occ ext = 369 S.add (S.mul (S.of_int occ) (LoopCost.to_ext loop_cost)) ext in 370 fold f loop_costs (S.of_int 0) 371 372 end 373 374 375 and Base : sig 376 type t 377 val compare : t > t > int 378 val of_int : int > t 379 val of_extern : string > t 380 val of_fun_call_ : FunCall.t > t 381 val of_fun_call : string > int > string > Args.t > t 382 val of_loop_cost : 383 string > int > S.relation > S.t > S.t > S.t > Cost.t > t 384 val add : t > t > t 385 val called_funs : t > Misc.String.Set.t 386 val replace_vars : S.t Misc.String.Map.t > t > t 387 val reduce : prototypes > Cost.t Misc.String.Map.t > t > Base.t list 388 val le : t > t > bool 389 val to_string : t > string 390 val to_ext : t > S.t 391 end = struct 392 393 type t = 394 { constant : int ; 395 externs : Externs.t ; 396 fun_calls : FunCalls.t ; 397 loop_costs : LoopCosts.t } 398 399 let make constant externs fun_calls loop_costs = 400 { constant ; externs ; fun_calls ; loop_costs } 401 402 let compare = Pervasives.compare 403 404 let constant base = base.constant 405 let externs base = base.externs 406 let fun_calls base = base.fun_calls 407 let loop_costs base = base.loop_costs 408 409 let set_fun_calls fun_calls base = { base with fun_calls } 410 let set_loop_costs loop_costs base = { base with loop_costs } 411 412 let to_string base = 413 Printf.sprintf "%d + (%s) + (%s) + (%s)" 414 (constant base) 415 (Externs.to_string (externs base)) 416 (FunCalls.to_string (fun_calls base)) 417 (LoopCosts.to_string (loop_costs base)) 418 419 let of_int i = make i Externs.empty FunCalls.empty LoopCosts.empty 420 421 let of_extern x = 422 make 0 (Externs.singleton x) FunCalls.empty LoopCosts.empty 423 424 let of_fun_call_ fun_call = 425 make 0 Externs.empty (FunCalls.singleton_ fun_call) LoopCosts.empty 426 427 let of_fun_call caller id callee args = 428 let fun_call = FunCall.make caller id callee args in 429 of_fun_call_ fun_call 430 431 let of_loop_cost 432 fun_name id relation init_value exit_value increment body_cost = 433 let loop_costs = 434 LoopCosts.singleton 435 fun_name id relation init_value exit_value increment body_cost in 436 make 0 Externs.empty FunCalls.empty loop_costs 437 438 let apply f f_constant f_externs f_fun_calls f_loop_costs base = 439 let constant_res = f_constant (constant base) in 440 let externs_res = f_externs (externs base) in 441 let fun_calls_res = f_fun_calls (fun_calls base) in 442 let loop_costs_res = f_loop_costs (loop_costs base) in 443 f constant_res externs_res fun_calls_res loop_costs_res 444 445 let apply2 f f_constant f_externs f_fun_calls f_loop_costs base1 base2 = 446 let constant_res = f_constant (constant base1) (constant base2) in 447 let externs_res = f_externs (externs base1) (externs base2) in 448 let fun_calls_res = f_fun_calls (fun_calls base1) (fun_calls base2) in 449 let loop_costs_res = f_loop_costs (loop_costs base1) (loop_costs base2) in 450 f constant_res externs_res fun_calls_res loop_costs_res 451 452 let add = apply2 make (+) Externs.add FunCalls.add LoopCosts.add 453 454 let le = 455 let f b1 b2 b3 b4 = b1 && b2 && b3 && b4 in 456 apply2 f (<=) Externs.le FunCalls.le LoopCosts.le 457 458 let replace_vars replacements = 459 apply make Misc.id 460 (Externs.replace_vars replacements) 461 (FunCalls.replace_vars replacements) 462 (LoopCosts.replace_vars replacements) 463 464 let called_funs base = 465 Misc.String.Set.union 466 (FunCalls.called_funs (fun_calls base)) 467 (LoopCosts.called_funs (loop_costs base)) 468 469 let reduce prototypes costs base = 470 let f fun_call occ base_list = 471 let added_bases = 472 FunCall.reduce 473 Cost.to_list Cost.is_solved Cost.replace_vars of_fun_call_ 474 prototypes costs fun_call in 475 let added_bases = 476 if added_bases = [] then [of_int 0] else added_bases in 477 let added_bases = 478 let f base = Misc.repeat occ (add base) (of_int 0) in 479 List.map f added_bases in 480 let f_base_list res added_base = 481 res @ (List.map (add added_base) base_list) in 482 List.fold_left f_base_list [] added_bases in 483 let loop_costs = LoopCosts.reduce prototypes costs (loop_costs base) in 484 let base = set_loop_costs loop_costs base in 485 let base' = set_fun_calls FunCalls.empty base in 486 FunCalls.fold f (fun_calls base) [base'] 487 488 let to_ext base = 489 let f_fun_calls fun_calls = 490 if not (FunCalls.is_empty fun_calls) then 491 raise (Failure "Base.to_ext: function calls") 492 else S.of_int 0 in 493 let f ext1 ext2 ext3 ext4 = s_add_list [ext1 ; ext2 ; ext3 ; ext4] in 494 apply f S.of_int Externs.to_ext f_fun_calls LoopCosts.to_ext base 495 496 end 497 498 499 and Cost : sig 500 type t 501 val of_int : int > t 502 val of_extern : string > t 503 val of_fun_call : string > int > string > Args.t > t 504 val of_loop_cost : 505 string > int > S.relation > S.t > S.t > S.t > Cost.t > t 506 val of_base : Base.t > t 507 val empty : t 508 val add : t > t > t 509 val join : t > t > t 510 val widen : t > t > t 511 val narrow : t > t > t 512 val called_funs : t > Misc.String.Set.t 513 val has_fun_calls : t > bool 514 val replace_vars : S.t Misc.String.Map.t > t > t 515 val reduce : prototypes > Cost.t Misc.String.Map.t > t > t 516 val is_solved : t > bool 517 val to_list : t > Base.t list 518 val to_string : t > string 519 val le : t > t > bool 520 val to_ext : t > S.t 521 end = struct 522 523 module M = Eset.Make (Base) 524 include M 525 526 let to_string cost = 527 if is_empty cost then "0" 528 else Misc.List.to_string " max " Base.to_string (to_list cost) 529 530 let of_base base = singleton base 531 532 let of_int i = of_base (Base.of_int i) 533 534 let of_extern x = of_base (Base.of_extern x) 535 536 let of_fun_call caller id callee args = 537 of_base (Base.of_fun_call caller id callee args) 538 539 let of_loop_cost 540 fun_name loop_id relation init_value exit_value increment body_cost = 541 of_base 542 (Base.of_loop_cost 543 fun_name loop_id relation init_value exit_value increment body_cost) 544 545 let join1 base cost = 546 let f_exists base' = Base.le base base' in 547 if exists f_exists cost then cost 548 else 549 let f_absorb base' = Base.le base' base in 550 M.add base (M.diff cost (M.filter f_absorb cost)) 551 552 let add cost1 cost2 = 553 if is_empty cost1 then cost2 554 else 555 if is_empty cost2 then cost1 556 else 557 let f2 base1 base2 = join1 (Base.add base1 base2) in 558 let f1 base1 = fold (f2 base1) cost2 in 559 fold f1 cost1 empty 560 561 let join cost1 cost2 = 562 if is_empty cost1 then cost2 563 else 564 if is_empty cost2 then cost1 565 else fold join1 cost1 cost2 566 567 let widen = join 568 569 let narrow = join (* TODO: improve *) 570 571 let mem base cost = 572 let f base' res = res  (Base.le base base') in 573 fold f cost false 574 575 let le cost1 cost2 = 576 let f base res = res && (mem base cost2) in 577 fold f cost1 true 578 579 580 let called_funs cost = 581 let f base called_funs = 582 Misc.String.Set.union (Base.called_funs base) called_funs in 583 fold f cost Misc.String.Set.empty 584 585 let has_fun_calls cost = not (Misc.String.Set.is_empty (called_funs cost)) 586 587 let replace_vars replacements cost = 588 let f base cost = join1 (Base.replace_vars replacements base) cost in 589 fold f cost empty 590 591 let reduce prototypes costs cost = 592 let f base cost = 593 let base_list = Base.reduce prototypes costs base in 594 let f_join cost base = join1 base cost in 595 List.fold_left f_join cost base_list in 596 fold f cost empty 597 598 let is_solved cost = not (has_fun_calls cost) 599 600 let to_ext cost = 601 if is_empty cost then S.of_int 0 602 else 603 let f base ext = S.max (Base.to_ext base) ext in 604 let base = choose cost in 605 let cost = remove base cost in 606 fold f cost (Base.to_ext base) 607 608 end 609 610 611 type t = Top  C of Cost.t 612 613 614 let to_string = function 615  Top > "top" 616  C cost > Cost.to_string cost 617 618 619 let of_int i = C (Cost.of_int i) 620 621 let of_extern fun_name = C (Cost.of_extern fun_name) 622 623 let of_fun_call caller id callee args = 624 C (Cost.of_fun_call caller id callee args) 625 626 let of_loop_cost 627 fun_name loop_id relation init_value exit_value increment body_cost = 628 C (Cost.of_loop_cost 629 fun_name loop_id relation init_value exit_value increment body_cost) 630 631 632 let is_top = function Top > true  _ > false 633 634 let extract = function 635  Top > raise (Failure "Cost_value.extract") 636  C cost > cost 637 638 let top = Top 639 640 let bot = of_int 0 641 642 643 let top_absorbs f = function 644  Top > Top 645  C cost > C (f cost) 646 647 let top_absorbs2 f cost1 cost2 = match cost1, cost2 with 648  Top, _  _, Top > Top 649  C cost1, C cost2 > C (f cost1 cost2) 650 651 652 let add = top_absorbs2 Cost.add 653 654 let join = top_absorbs2 Cost.join 655 656 let widen = top_absorbs2 Cost.widen 657 658 let narrow cost1 cost2 = match cost1, cost2 with 659  cost, Top  Top, cost > cost 660  C cost1, C cost2 > C (Cost.narrow cost1 cost2) 661 662 let le cost1 cost2 = match cost1, cost2 with 663  _, Top > true 664  Top, _ > false 665  C cost1, C cost2 > Cost.le cost1 cost2 666 667 668 let reduce_ prototypes costs cost = 669 let called_funs = Cost.called_funs cost in 670 let costs = 671 let f fun_name _ = Misc.String.Set.mem fun_name called_funs in 672 Misc.String.Map.filter f costs in 673 let f fun_name cost costs = match cost, costs with 674  _, None > None 675  Top, _ > None 676  C cost, Some costs > Some (Misc.String.Map.add fun_name cost costs) in 677 match Misc.String.Map.fold f costs (Some Misc.String.Map.empty) with 678  None > Top 679  Some costs > C (Cost.reduce prototypes costs cost) 680 681 let reduce prototypes costs = function 682  Top > Top 683  C cost > reduce_ prototypes costs cost 684 685 let reduces prototypes costs = 686 Misc.String.Map.map (reduce prototypes costs) costs 687 688 689 let replace_vars replacements = top_absorbs (Cost.replace_vars replacements) 690 691 692 let has_fun_calls = function 693  Top > false 694  C cost > Cost.has_fun_calls cost 695 696 697 let is_concrete cost = (not (is_top cost)) && (not (has_fun_calls cost)) 698 699 let to_ext = function 700  Top > S.top 701  C cost > Cost.to_ext cost 702 703 704 end
Note: See TracChangeset
for help on using the changeset viewer.