source: Deliverables/D5.1/cost-plug-in/plugin/cost_value.ml @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 11.6 KB
Line 
1
2(** This module describes the values manipulated by the plug-in. *)
3
4
5type relation = Lt | Gt | Le | Ge
6
7let string_of_relation = function
8  | Lt -> "<"
9  | Le -> "<="
10  | Gt -> ">"
11  | Ge -> ">="
12
13let bool_fun_of_relation = function
14  | Lt -> (<)
15  | Le -> (<=)
16  | Gt -> (>)
17  | Ge -> (>=)
18
19let mk_strict = function
20  | Lt | Le -> Lt
21  | Gt | Ge -> Gt
22
23let mk_large = function
24  | Lt | Le -> Le
25  | Gt | Ge -> Ge
26
27let opposite = function
28  | Lt -> Ge
29  | Le -> Gt
30  | Gt -> Le
31  | Ge -> Lt
32
33type unop = Neg
34
35let string_of_unop = function
36  | Neg -> "-"
37
38let int_fun_of_unop = function
39  | Neg -> (fun x -> (-x))
40
41type binop = Add | Sub | Div | Mul | Mod | Max
42
43let string_of_binop = function
44  | Add -> "+"
45  | Sub -> "-"
46  | Div -> "/"
47  | Mul -> "*"
48  | Mod -> "%"
49  | Max -> "max"
50
51let int_fun_of_binop = function
52  | Add -> (+)
53  | Sub -> (-)
54  | Div -> (/)
55  | Mul -> ( * )
56  | Mod -> (mod)
57  | Max -> max
58
59(** Cost values *)
60
61type 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
72let 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
77let 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
87let 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
101let 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
106let 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
122and to_string v = fold f_to_string v
123
124
125(* Variables of a cost value *)
126
127let union_list l =
128  List.fold_left StringTools.Set.union StringTools.Set.empty l
129
130let 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
138let vars = fold f_vars
139
140
141(* Replace variables by expressions *)
142
143(*
144let 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
151let 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
158let 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 *)
164exception Unknown_cost of string
165(* Raised when the prototype of a function is not found *)
166exception Unknown_prototype of string
167
168let 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
177let 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
182let 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)
195      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
205let 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
240let 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
250let 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. *)
260exception Unsupported_exp
261(* Raised when an unsupported comparison relation. *)
262exception Unsupported_rel
263
264
265let 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
272let 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
278let 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
285let unop_of_cil_unop = function
286  | Cil_types.Neg -> Neg
287  | _ -> raise (Failure "unop_of_cil_unop")
288
289let 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
299let 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
311let cil_unop_of_unop = function
312  | Neg -> Cil_types.Neg
313
314let 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
324let integer_term term = Logic_const.term term Cil_types.Linteger
325
326let 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
331let 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
353let to_cil_term = fold f_to_cil_term
354
355
356let 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
365let has_locals locals = fold (f_has_locals locals)
366
367
368let 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
373let has_any = fold f_has_any
Note: See TracBrowser for help on using the repository browser.