2 (** This module describes the values manipulated by the plug-in. *)
4 exception Unknown_cost of string
5 exception Unknown_prototype of string
8 let string_of_mset to_list sep f mset =
9 let filter (_, occ) = occ <> 0 in
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))
15 type prototypes = string list Misc.String.Map.t
21 val is_large : relation -> bool
22 val has_lower_type : relation -> bool
28 val of_var : string -> t
30 val minus : 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
39 val le : t -> t -> bool
41 val replace_vars : t Misc.String.Map.t -> t -> t
43 val to_string : t -> string
44 val string_of_relation : relation -> string
46 val compare : t -> t -> int
51 module Make (S : S) = struct
53 let s_add_list = function
55 | e :: l -> List.fold_left S.add e l
61 let compare = Misc.List.compare S.compare
64 if List.length args1 <> List.length args2 then false
66 let f res arg1 arg2 = res && (S.le arg1 arg2) in
67 List.fold_left2 f true args1 args2
69 let replace_vars replacements = List.map (S.replace_vars replacements)
71 let to_string = Misc.List.to_string ", " S.to_string
76 module Externs = struct
78 module M = Misc.String.MSet
85 let replace_vars _ externs = externs
87 let to_string = string_of_mset to_list " + " (fun x -> x)
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)
96 module FunCall = struct
103 let compare = Pervasives.compare
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
110 let make caller id callee args = { caller ; id ; callee ; args }
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
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
127 let f b1 b2 b3 b4 = b1 && b2 && b3 && b4 in
128 apply2 f (=) (=) (=) Args.le
130 let replace_vars replacement =
131 apply make Misc.id Misc.id Misc.id (Args.replace_vars replacement)
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
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)
150 (Failure ("FunCall.reduce: formals and actuals for " ^
151 "function " ^ callee ^ " have different sizes."))
152 else raise (Unknown_prototype callee)
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))
161 module FunCalls = struct
163 module M = Multiset.Make (FunCall)
166 let singleton_ fun_call = M.add fun_call empty
168 let singleton caller id callee args =
169 singleton (FunCall.make caller id callee args)
173 let le1 fun_call occ fun_calls =
174 let f fun_call' occ' = (FunCall.le fun_call fun_call') && (occ <= occ') in
177 let le fun_calls1 fun_calls2 =
178 let f fun_call occ = le1 fun_call occ fun_calls2 in
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
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
192 let to_string = string_of_mset to_list " + " FunCall.to_string
197 module rec LoopCost : sig
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
210 { fun_name : string ;
212 relation : S.relation ;
218 let make fun_name id relation init_value exit_value increment body_cost =
219 { fun_name ; id ; relation ; init_value ; exit_value ; increment ;
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
230 let compare = Pervasives.compare
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
243 fun_name_res id_res relation_res init_value_res exit_value_res
244 increment_res body_cost_res
247 f_fun_name f_id f_relation f_init_value f_exit_value f_increment
248 f_body_cost loop_cost1 loop_cost2 =
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
253 f_relation (relation loop_cost1) (relation loop_cost2) in
255 f_init_value (init_value loop_cost1) (init_value loop_cost2) in
257 f_exit_value (exit_value loop_cost1) (exit_value loop_cost2) in
259 f_increment (increment loop_cost1) (increment loop_cost2) in
261 f_body_cost (body_cost loop_cost1) (body_cost loop_cost2) in
263 fun_name_res id_res relation_res init_value_res exit_value_res
264 increment_res body_cost_res
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
270 let called_funs loop_cost = Cost.called_funs (body_cost loop_cost)
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)
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)
281 let to_string loop_cost =
282 Printf.sprintf "%s@%d(%s %s %s %s (%s))"
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))
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
305 S.cond init_value rel exit_value body_cost (S.of_int 0) in
306 S.mul iteration_nb cond_body_cost
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
325 module M = Multiset.Make (LoopCost)
328 let singleton_ loop_cost = M.add loop_cost empty
331 fun_name id relation init_value exit_value increment body_cost =
334 fun_name id relation init_value exit_value increment body_cost in
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
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
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
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
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
363 fold f loop_costs empty
365 let to_string = string_of_mset to_list " + " LoopCost.to_string
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)
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
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
395 externs : Externs.t ;
396 fun_calls : FunCalls.t ;
397 loop_costs : LoopCosts.t }
399 let make constant externs fun_calls loop_costs =
400 { constant ; externs ; fun_calls ; loop_costs }
402 let compare = Pervasives.compare
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
409 let set_fun_calls fun_calls base = { base with fun_calls }
410 let set_loop_costs loop_costs base = { base with loop_costs }
413 Printf.sprintf "%d + (%s) + (%s) + (%s)"
415 (Externs.to_string (externs base))
416 (FunCalls.to_string (fun_calls base))
417 (LoopCosts.to_string (loop_costs base))
419 let of_int i = make i Externs.empty FunCalls.empty LoopCosts.empty
422 make 0 (Externs.singleton x) FunCalls.empty LoopCosts.empty
424 let of_fun_call_ fun_call =
425 make 0 Externs.empty (FunCalls.singleton_ fun_call) LoopCosts.empty
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
432 fun_name id relation init_value exit_value increment body_cost =
435 fun_name id relation init_value exit_value increment body_cost in
436 make 0 Externs.empty FunCalls.empty loop_costs
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
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
452 let add = apply2 make (+) Externs.add FunCalls.add LoopCosts.add
455 let f b1 b2 b3 b4 = b1 && b2 && b3 && b4 in
456 apply2 f (<=) Externs.le FunCalls.le LoopCosts.le
458 let replace_vars replacements =
460 (Externs.replace_vars replacements)
461 (FunCalls.replace_vars replacements)
462 (LoopCosts.replace_vars replacements)
464 let called_funs base =
465 Misc.String.Set.union
466 (FunCalls.called_funs (fun_calls base))
467 (LoopCosts.called_funs (loop_costs base))
469 let reduce prototypes costs base =
470 let f fun_call occ base_list =
473 Cost.to_list Cost.is_solved Cost.replace_vars of_fun_call_
474 prototypes costs fun_call in
476 if added_bases = [] then [of_int 0] else added_bases in
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']
489 let f_fun_calls fun_calls =
490 if not (FunCalls.is_empty fun_calls) then
491 raise (Failure "Base.to_ext: function calls")
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
501 val of_int : int -> t
502 val of_extern : string -> t
503 val of_fun_call : string -> int -> string -> Args.t -> t
505 string -> int -> S.relation -> S.t -> S.t -> S.t -> Cost.t -> t
506 val of_base : Base.t -> 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
523 module M = Eset.Make (Base)
527 if is_empty cost then "0"
528 else Misc.List.to_string " max " Base.to_string (to_list cost)
530 let of_base base = singleton base
532 let of_int i = of_base (Base.of_int i)
534 let of_extern x = of_base (Base.of_extern x)
536 let of_fun_call caller id callee args =
537 of_base (Base.of_fun_call caller id callee args)
540 fun_name loop_id relation init_value exit_value increment body_cost =
543 fun_name loop_id relation init_value exit_value increment body_cost)
545 let join1 base cost =
546 let f_exists base' = Base.le base base' in
547 if exists f_exists cost then cost
549 let f_absorb base' = Base.le base' base in
550 M.add base (M.diff cost (M.filter f_absorb cost))
552 let add cost1 cost2 =
553 if is_empty cost1 then cost2
555 if is_empty cost2 then cost1
557 let f2 base1 base2 = join1 (Base.add base1 base2) in
558 let f1 base1 = fold (f2 base1) cost2 in
561 let join cost1 cost2 =
562 if is_empty cost1 then cost2
564 if is_empty cost2 then cost1
565 else fold join1 cost1 cost2
569 let narrow = join (* TODO: improve *)
572 let f base' res = res || (Base.le base base') in
576 let f base res = res && (mem base cost2) in
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
585 let has_fun_calls cost = not (Misc.String.Set.is_empty (called_funs cost))
587 let replace_vars replacements cost =
588 let f base cost = join1 (Base.replace_vars replacements base) cost in
591 let reduce prototypes costs 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
598 let is_solved cost = not (has_fun_calls cost)
601 if is_empty cost then S.of_int 0
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)
611 type t = Top | C of Cost.t
614 let to_string = function
616 | C cost -> Cost.to_string cost
619 let of_int i = C (Cost.of_int i)
621 let of_extern fun_name = C (Cost.of_extern fun_name)
623 let of_fun_call caller id callee args =
624 C (Cost.of_fun_call caller id callee args)
627 fun_name loop_id relation init_value exit_value increment body_cost =
629 fun_name loop_id relation init_value exit_value increment body_cost)
632 let is_top = function Top -> true | _ -> false
634 let extract = function
635 | Top -> raise (Failure "Cost_value.extract")
643 let top_absorbs f = function
645 | C cost -> C (f cost)
647 let top_absorbs2 f cost1 cost2 = match cost1, cost2 with
648 | Top, _ | _, Top -> Top
649 | C cost1, C cost2 -> C (f cost1 cost2)
652 let add = top_absorbs2 Cost.add
654 let join = top_absorbs2 Cost.join
656 let widen = top_absorbs2 Cost.widen
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)
662 let le cost1 cost2 = match cost1, cost2 with
665 | C cost1, C cost2 -> Cost.le cost1 cost2
668 let reduce_ prototypes costs cost =
669 let called_funs = Cost.called_funs cost in
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
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
679 | Some costs -> C (Cost.reduce prototypes costs cost)
681 let reduce prototypes costs = function
683 | C cost -> reduce_ prototypes costs cost
685 let reduces prototypes costs =
686 Misc.String.Map.map (reduce prototypes costs) costs
689 let replace_vars replacements = top_absorbs (Cost.replace_vars replacements)
692 let has_fun_calls = function
694 | C cost -> Cost.has_fun_calls cost
697 let is_concrete cost = (not (is_top cost)) && (not (has_fun_calls cost))
699 let to_ext = function
701 | C cost -> Cost.to_ext cost