Ignore:
Timestamp:
Feb 7, 2012, 6:01:43 PM (8 years ago)
Author:
ayache
Message:

Frama-C plug-in (sources+documentation)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.1-5.3/cost-plug-in/plugin/cost_value.ml

    r1462 r1679  
    22(** This module describes the values manipulated by the plug-in. *)
    33
    4 
    5 type relation = Lt | Gt | Le | Ge
    6 
    7 let string_of_relation = function
    8   | Lt -> "<"
    9   | Le -> "<="
    10   | Gt -> ">"
    11   | Ge -> ">="
    12 
    13 let bool_fun_of_relation = function
    14   | Lt -> (<)
    15   | Le -> (<=)
    16   | Gt -> (>)
    17   | Ge -> (>=)
    18 
    19 let mk_strict = function
    20   | Lt | Le -> Lt
    21   | Gt | Ge -> Gt
    22 
    23 let mk_large = function
    24   | Lt | Le -> Le
    25   | Gt | Ge -> Ge
    26 
    27 let opposite = function
    28   | Lt -> Ge
    29   | Le -> Gt
    30   | Gt -> Le
    31   | Ge -> Lt
    32 
    33 type unop = Neg
    34 
    35 let string_of_unop = function
    36   | Neg -> "-"
    37 
    38 let int_fun_of_unop = function
    39   | Neg -> (fun x -> (-x))
    40 
    41 type binop = Add | Sub | Div | Mul | Mod | Max
    42 
    43 let string_of_binop = function
    44   | Add -> "+"
    45   | Sub -> "-"
    46   | Div -> "/"
    47   | Mul -> "*"
    48   | Mod -> "%"
    49   | Max -> "max"
    50 
    51 let int_fun_of_binop = function
    52   | Add -> (+)
    53   | Sub -> (-)
    54   | Div -> (/)
    55   | Mul -> ( * )
    56   | Mod -> (mod)
    57   | Max -> max
    58 
    59 (** Cost values *)
    60 
    61 type t =
    62   | Int of int
    63   | Var of string (* either a parameter or a global, but not a local *)
    64   | UnOp of unop * t
    65   | BinOp of binop * t * t
    66   | 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 sub-values of the cost value [v]. *)
    76 
    77 let subs = function
    78   | 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) -> args
    83 
    84 (** [fill_subs s subs] replaces the sub-values of the cost value [v] with
    85     those in [subs]. *)
    86 
    87 let fill_subs v subs = match v, subs with
    88   | Int _, _ | Var _, _ | Any, _ -> v
    89   | 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 its
    97     children, starting from the leaves and going up in the tree. [f]'s type is
    98     [t -> 'a list -> 'a], where the second argument is the results of the fold
    99     on [v]'s sub-values. *)
    100 
    101 let rec fold (f : t -> 'a list -> 'a) v =
    102   let subs_res = List.map (fold f) (subs v) in
    103   f v subs_res
    104 
    105 
    106 let rec f_to_string v subs_res = match v, subs_res with
    107   | Int i, _ -> string_of_int i
    108   | Var x, _ -> x
    109   | 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 telse
    115   | CostOf (fun_name, _), args ->
    116     let f res v = res ^ v ^ ", " in
    117     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 v
    123 
    124 
    125 (* Variables of a cost value *)
    126 
    127 let union_list l =
    128   List.fold_left StringTools.Set.union StringTools.Set.empty l
    129 
    130 let f_vars v subs_res =
    131   let v_res = match v with
    132     | Var x -> StringTools.Set.singleton x
    133     | _ -> StringTools.Set.empty in
    134   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_vars
    139 
    140 
    141 (* Replace variables by expressions *)
    142 
    143 (*
    144 let f_replace r_list v subs_res =
    145   let v = match v with
    146     | Var x when List.mem_assoc x r_list -> List.assoc x r_list
    147     | _ -> v in
    148   fill_subs v subs_res
    149 *)
    150 
    151 let f_replace r_list v subs_res = match fill_subs v subs_res with
    152   | Var x when List.mem_assoc x r_list -> List.assoc x r_list
    153   | v -> v
    154 
    155 (** [replace r_list v] replaces the variables of [v] that are in the association
    156     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 *)
    1644exception Unknown_cost of string
    165 (* Raised when the prototype of a function is not found *)
    1665exception Unknown_prototype of string
    1676
    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
     8let 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
     15type prototypes = string list Misc.String.Map.t
     16
     17
     18module 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
     48end
     49
     50
     51module 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
    19565      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
     704end
Note: See TracChangeset for help on using the changeset viewer.