source: Deliverables/D5.1/cost-plug-in/plugin/compute.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: 38.8 KB
Line 
1
2(** This module adds ACSL annotations to a C file transformed by CerCo's
3    compiler. The annotations are a synthesis of the ones added by CerCo and
4    specify an upper bound of the WCET of each function of the input program. *)
5
6(** Only a subset of the C constructions are supported:
7    - everything that is not supported by CerCo is not supported by the plug-in
8      (switches in particular);
9    - gotos are not supported;
10    - (potentially mutually) recursive functions are not supported;
11    - pointer functions are not supported;
12    - inside a function, parameters must not be assigned nor their address
13      accessed;
14    - loops must start with an initialization (of the so-called loop counter),
15      have a guard condition comparing the loop counter with <, <=, > or >=, and
16      end with an incrementation (or a decrementation) of the loop counter. The
17      expressions in the initialization, the guard and the increment must only
18      refer to parameters, and the parameters cannot be assigned nor their
19      address accessed in the whole function, and the loop counter cannot be
20      assigned nor its address taken inside the loop's body (except in the
21      incrementation). *)
22
23(** The synthesis proceeds as follows:
24    1- The synthesis environment is initialized.
25    2- The cost of each function is computed. At this stage, the costs may
26       depend on the cost of the other functions, but they are left abstract.
27    3- Using the results of 2-, a system of equations is created and tried to
28       be solved. It is solved if the algorithm succeeds in computing the cost
29       of each function independently of the cost of the other functions.
30    4- Using the results of 3-, annotations are added in the source code. *)
31
32
33(*** Exceptions ***)
34
35(* Raised when the algorithm fails to solve the system of inequations made by
36   the cost of each function. *)
37exception Unresolvable
38(* Raised when the cost update function inside the source code is called with a
39   non-constant argument. This should not occur if the code originates from
40   CerCo. *)
41exception Cost_incr_arg_not_constant
42(* Raised when a function pointer is found. *)
43exception Unresolvable_function
44exception Unsupported_exp
45exception Unsupported_loop of string
46exception Unknown_function of string
47exception Nested_loops
48(* Other unsupported cases. *)
49exception Unsupported of string
50
51let string_of_exception cost_incr = function
52  | Unresolvable -> "Costs are unresovable (recursion?)."
53  | Cost_incr_arg_not_constant ->
54    "Call to the update cost function " ^ cost_incr ^
55      " with a non-constant integer argument."
56  | Unresolvable_function -> "Cannot resolve call (function pointer?)."
57  | Unsupported s -> "Unsupported instruction: " ^ s ^ "."
58  | Unsupported_loop s -> "Unsupported loop: " ^ s ^ "."
59  | Unknown_function f -> "Unknown function definition " ^ f ^ "."
60  | Nested_loops -> "Nested loops."
61  | Unsupported_exp | Cost_value.Unsupported_exp -> "Unsupported expression."
62  | Cost_value.Unsupported_rel -> "Unsupported guard condition."
63  | e -> raise e
64
65
66(*** Helpers ***)
67
68let identity x = x
69
70let integer_term term = Logic_const.term term Cil_types.Linteger
71
72let add_loop_annot obj stmt annot = 
73  Queue.add (fun () -> Annotations.add stmt [Ast.self] annot)
74    obj#get_filling_actions
75
76let loop_annotation annot = Db_types.Before (Db_types.User annot)
77
78let mk_invariant pred =
79  let annot =
80    Logic_const.new_code_annotation (Cil_types.AInvariant ([], true, pred)) in
81  loop_annotation annot
82
83let mk_variant term =
84  let annot =
85    Logic_const.new_code_annotation (Cil_types.AVariant (term, None)) in
86  loop_annotation annot
87
88let current_kf obj = match obj#current_kf with
89  | None -> raise (Failure "Compute.current_kf")
90  | Some kf -> kf
91
92let current_fundec obj = match (current_kf obj).Db_types.fundec with
93  | Db_types.Definition (fundec, _) -> fundec
94  | _ -> raise (Failure "Compute.current_fundec")
95
96let current_fun_name obj = (current_fundec obj).Cil_types.svar.Cil_types.vname
97
98let current_spec obj = (current_fundec obj).Cil_types.sspec
99
100let mk_fun_cost_pred rel cost_id cost = 
101  let cost_var = Cil_const.make_logic_var cost_id Cil_types.Linteger in
102  let cost_var = Logic_const.tvar cost_var in
103  let cost = Cost_value.to_cil_term cost in 
104  let old_cost =
105    Logic_const.term (Cil_types.Told cost_var) cost_var.Cil_types.term_type in
106  let new_cost = Cil_types.TBinOp (Cil_types.PlusA, old_cost, cost) in
107  let new_cost = integer_term new_cost in
108  Logic_const.prel (rel, cost_var, new_cost)
109
110let rec make_freshes fundec n prefix =
111  let name = prefix ^ "_tmp" ^ (string_of_int (n-1)) in
112  if n <= 0 then []
113  else (make_freshes fundec (n-1) prefix) @
114       [Cil.makeTempVar fundec ~name Cil.intType]
115
116
117(*** Annotation environment ***)
118
119type fun_info =
120    { (* Variables whose address may be accessed. *)
121      addressed  : StringTools.Set.t ;
122      parameters : string list ;
123      locals     : StringTools.Set.t ;
124      (* Variables that may be assigned. *)
125      modified   : StringTools.Set.t ;
126      nb_loops   : int }
127
128let mk_fun_info addressed parameters locals modified nb_loops =
129  { addressed = addressed ;
130    parameters = parameters ;
131    locals = locals ;
132    modified = modified ;
133    nb_loops = nb_loops }
134
135let init_fun_info =
136  mk_fun_info
137    StringTools.Set.empty [] StringTools.Set.empty StringTools.Set.empty 0
138
139(** An environment associates to each function: the variables whose address may
140    be accessed, the list of its parameters, its locals, and the variables that
141    may be assigned. *)
142
143type env =
144    { fun_infos    : fun_info StringTools.Map.t ;
145      cost_varinfo : Cil_types.varinfo }
146
147let mk_env fun_infos cost_varinfo =
148  { fun_infos = fun_infos ; cost_varinfo = cost_varinfo }
149
150let init_env =
151  mk_env StringTools.Map.empty (Cil.makeVarinfo true false "dummy" Cil.intType)
152
153let get_fun_infos env = env.fun_infos
154
155let get_cost_varinfo env = env.cost_varinfo
156
157let upd_fun_infos env fun_infos = { env with fun_infos = fun_infos }
158
159let upd_cost_varinfo env cost_varinfo =
160  { env with cost_varinfo = cost_varinfo }
161
162let get_fun_info env fun_name =
163  if StringTools.Map.mem fun_name (get_fun_infos env) then
164    StringTools.Map.find fun_name (get_fun_infos env)
165  else raise (Unknown_function fun_name)
166
167let upd_fun_info env fun_name fun_info =
168  let fun_infos = StringTools.Map.add fun_name fun_info (get_fun_infos env) in
169  upd_fun_infos env fun_infos
170
171let get_addressed env fun_name =
172  (get_fun_info env fun_name).addressed
173
174(** [is_addressed_variable env fun_name x] returns true iff the address of the
175    variable [x] may be accessed in function [fun_name] considering the
176    environment [env]. *)
177
178let is_addressed_variable env fun_name x =
179  StringTools.Set.mem x (get_addressed env fun_name)
180
181(** [has_addressed env fun_name set] returns true iff the address of a variable
182    of the set [set] may be accessed in function [fun_name] considering the
183    environment [env]. *)
184
185let has_addressed env fun_name set =
186  let f x res = res || (is_addressed_variable env fun_name x) in
187  StringTools.Set.fold f set false
188
189let upd_addressed env fun_name addressed =
190  let fun_info = get_fun_info env fun_name in
191  let fun_info = { fun_info with addressed = addressed } in
192  upd_fun_info env fun_name fun_info
193
194let get_parameters env fun_name = (get_fun_info env fun_name).parameters
195
196(** [is_parameter env fun_name x] returns true iff [x] is a parameter of the
197    function [fun_name] considering the environment [env]. *)
198
199let is_parameter env fun_name x = List.mem x (get_parameters env fun_name)
200
201(** [are_parameters env fun_name set] returns true iff all variables in the set
202    [set] are parameters of the function [fun_name] considering the environment
203    [env]. *)
204
205let are_parameters env fun_name set =
206  let f x res = res && (is_parameter env fun_name x) in
207  StringTools.Set.fold f set true
208
209let prototypes env =
210  let f fun_info = fun_info.parameters in
211  StringTools.Map.map f (get_fun_infos env)
212
213let get_locals env fun_name = (get_fun_info env fun_name).locals
214
215let get_modified env fun_name = (get_fun_info env fun_name).modified
216
217let upd_modified env fun_name modified =
218  let fun_info = get_fun_info env fun_name in
219  let fun_info = { fun_info with modified = modified } in
220  upd_fun_info env fun_name fun_info
221
222let get_nb_loops env fun_name =
223  (get_fun_info env fun_name).nb_loops
224
225let upd_nb_loops env fun_name nb_loops =
226  let fun_info = get_fun_info env fun_name in
227  let fun_info = { fun_info with nb_loops = nb_loops } in
228  upd_fun_info env fun_name fun_info
229
230let add_nb_loops env fun_name =
231  upd_nb_loops env fun_name ((get_nb_loops env fun_name) + 1)
232
233let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
234
235
236(*** Initializations ***)
237
238(* Initializing the environment simply consists in visiting every function and
239   set their information in the environment. *)
240
241class initializations cost_id env prj = object (self)
242  inherit Visitor.frama_c_copy prj as super
243
244  (* Update the variables whose address may be accessed. This is done by
245     visiting every expression of the program. *)
246  method vexpr e =
247    let _ = match e.Cil_types.enode with
248      | Cil_types.AddrOf (Cil_types.Var var, _) ->
249        let fun_name = current_fun_name self in
250        let addressed = get_addressed !env fun_name in
251        let addressed =
252          StringTools.Set.add var.Cil_types.vname addressed in
253        env := upd_addressed !env fun_name addressed
254      | _ -> () in
255    Cil.DoChildren
256
257  (* Update the variables whose address may be accessed. This is done by
258     visiting every statement of the program. *)
259  method vstmt_aux stmt =
260    let fun_name = current_fun_name self in
261    let _ = match stmt.Cil_types.skind with
262      | Cil_types.Instr (Cil_types.Set ((Cil_types.Var var, _), _, _)) ->
263        let modified = get_modified !env fun_name in
264        let modified = StringTools.Set.add var.Cil_types.vname modified in
265        env := upd_modified !env fun_name modified
266      | Cil_types.Loop _ -> env := add_nb_loops !env fun_name
267      | _ -> () in
268    Cil.DoChildren
269
270  (* When a function is found, create its entry in the environment, set its
271     parameters and its locals (the information is already accessible), and
272     leave empty the set of assigned and addressed variables. The two latters
273     will be updated when visiting the statements and the expressions. *)
274  method vfunc fundec =
275    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
276    let addressed = StringTools.Set.empty in
277    let varinfo_to_string x = x.Cil_types.vname in
278    let parameters = List.map varinfo_to_string fundec.Cil_types.sformals in
279    let f_locals res x = StringTools.Set.add (varinfo_to_string x) res in
280    let locals =
281      List.fold_left f_locals StringTools.Set.empty fundec.Cil_types.slocals in
282    let modified = StringTools.Set.empty in
283    let nb_loops = 0 in
284    let fun_info =
285      mk_fun_info addressed parameters locals modified nb_loops in
286    let fun_infos =
287      StringTools.Map.add fun_name fun_info (get_fun_infos !env) in
288    env := upd_fun_infos !env fun_infos ;
289    Cil.DoChildren
290
291  (* Update the varinfo of the cost variable. *)
292  method vglob_aux glob =
293    let _ = match glob with
294      | Cil_types.GVarDecl (_, varinfo, _)
295      | Cil_types.GVar (varinfo, _, _) when varinfo.Cil_types.vname = cost_id ->
296        env := upd_cost_varinfo !env varinfo
297      | _ -> () in
298    Cil.DoChildren
299
300end
301
302(** [initializations cost_id] consider the current file in the current project
303    and returns a corresponding initialized environment .*)
304
305let initializations cost_id : env =
306  let env : env ref = ref init_env in
307  let initializations_prj =     
308    File.create_project_from_visitor
309      "cerco_initializations" (new initializations cost_id env) in
310  let f () = !env in
311  Project.on initializations_prj f ()
312
313
314(* Test if a block has a loop. Used to test the presence of nested
315   loops. Indeed, they not supported for now, until a bug in Jessie is fixed. *)
316
317let rec has_loop_stmt stmt = match stmt.Cil_types.skind with
318  | Cil_types.Instr _ | Cil_types.Return _ | Cil_types.Goto _
319  | Cil_types.Break _ | Cil_types.Continue _ -> false
320  | Cil_types.If (_, block1, block2, _)
321  | Cil_types.TryFinally (block1, block2, _)
322  | Cil_types.TryExcept (block1, _, block2, _) ->
323    (has_loop block1) || (has_loop block2)
324  | Cil_types.Switch (_, block, _, _)
325  | Cil_types.Block block -> has_loop block
326  | Cil_types.Loop _ -> true
327  | Cil_types.UnspecifiedSequence l ->
328    has_loop_stmt_list (List.map (fun (stmt, _, _, _, _) -> stmt) l)
329
330and has_loop_stmt_list stmt_list =
331  let f res stmt = res || (has_loop_stmt stmt) in
332  List.fold_left f false stmt_list
333
334(** [has_loop block] returns true iff the block of instructions [block] contains
335    a loop. *)
336
337and has_loop block = has_loop_stmt_list block.Cil_types.bstmts
338
339
340(*** Statement and block cost ***)
341
342(* Requirement for loop termination. They have the form:
343   (guard relation, initialization value, exit value, increment) *)
344
345type require = Cost_value.relation * Cost_value.t * Cost_value.t * Cost_value.t
346
347(** [const_incr_cost e] extracts the integer constant that the expression [e]
348    represents. *)
349
350let cost_incr_cost = function
351  | e :: _ ->
352    (match e.Cil_types.enode with
353      | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
354        Cost_value.Int (Int64.to_int i)
355      | _ -> raise Cost_incr_arg_not_constant)
356  | _ -> raise Cost_incr_arg_not_constant
357
358(** [call cost cost_incr f args] returns the cost of calling the function [f] on
359    arguments [args]. If the function is the cost update function [cost_incr],
360    then its cost is the value of its argument, which needs to be a constant
361    integer. Otherwise, it is simply the cost of executing [f] on its
362    arguments. *)
363
364let call_cost cost_incr f args = match f.Cil_types.enode with
365  | Cil_types.Lval (Cil_types.Var var, _)
366      when var.Cil_types.vname = cost_incr ->
367    cost_incr_cost args
368  | Cil_types.Lval (Cil_types.Var var, _) ->
369    (try
370       let args = List.map Cost_value.of_cil_exp args in
371       Cost_value.CostOf (var.Cil_types.vname, args)
372     with Cost_value.Unsupported_exp -> raise Unsupported_exp)
373  | _ -> raise Unresolvable_function
374
375(** [instr_cost cost_incr instr] returns the cost of executing the simple
376    instruction [instr]. Only function calls do have a cost. *)
377
378let instr_cost cost_incr = function
379  | Cil_types.Call (_, f, args, _) ->
380    call_cost cost_incr f args
381  | _ -> Cost_value.Int 0
382
383(* Frama-C sometimes transforms the control flow graph of a function by
384   factorizing a return instructions through added gotos. We handle this special
385   case of gotos with the function below, but other forms are not supported. *)
386
387let goto_cost stmt = match stmt.Cil_types.skind with
388  | Cil_types.Return _ -> ([], Cost_value.Int 0)
389  | _ -> raise (Unsupported "goto")
390
391(* In Frama-C, every C loop construct is transformed into an infinite loop with
392   a break inside a conditional to exit. Initialization of a for loop are
393   located in the very previous instruction. The guard can either be at the
394   beginning of the loop in the cases of for and while loops, or at the end in
395   the case of a do-while loop. Finally, the increment instruction is located at
396   the end in the case of a for loop. *)
397
398(** [extract_counter_and_init stmt_opt] supposes that the optional statement
399    [stmt_opt] is in fact an assignment instruction. In this case, it returns
400    the assigned variable and the expression to assign, otherwise it raises an
401    error. It will be used to extract the loop counter and its first value in
402    the case of a loop initialization instruction. *)
403
404let extract_counter_and_init stmt_opt =
405  let error () = raise (Unsupported_loop "no initialization found") in
406  match stmt_opt with
407    | None -> error ()
408    | Some stmt -> match stmt.Cil_types.skind with
409        | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
410          (v.Cil_types.vname, Cost_value.of_cil_exp e)
411        | _ -> error ()
412
413(** [first_stmt block] returns the first statement of the block [block], if
414    any. *)
415
416let first_stmt block = match block.Cil_types.bstmts with
417  | [] -> raise (Unsupported_loop "no guard")
418  | instr :: _ -> instr
419
420(** [exp_is_var name e] returns true iff the expression [e] is in fact the
421    variable of name [name]. *)
422
423let exp_is_var name e = match e.Cil_types.enode with
424  | Cil_types.Lval (Cil_types.Var v, _) -> v.Cil_types.vname = name
425  | _ -> false
426
427(** [starts_with_break block] returns true iff the block [block] starts with a
428    break instruction. *)
429
430let starts_with_break block = match (first_stmt block).Cil_types.skind with
431  | Cil_types.Break _ -> true
432  | _ -> false
433
434(** [extract_guard counter block] supposes that the first statement of the block
435    [block] is a conditional with an exit instruction. It then supposes that the
436    conditional is a test on the variable [counter]. It returns the comparison
437    relation along with the expression that the counter is compared to. It will
438    be used to extract the guard condition of a loop. *)
439
440let extract_guard counter block = match (first_stmt block).Cil_types.skind with
441  | Cil_types.If (e, _, block, _) when starts_with_break block ->
442    (match e.Cil_types.enode with
443      | Cil_types.BinOp (rel, e1, e2, _) when exp_is_var counter e1 ->
444        (Cost_value.rel_of_cil_rel rel, Cost_value.of_cil_exp e2)
445      | _ -> raise (Unsupported_loop "unsupported guard expression"))
446  | _ -> raise (Unsupported_loop "no guard found")
447
448(** [last l] returns the last element of the list [l], if any. *)
449
450let rec last = function
451  | [] -> raise (Failure "Compute.last")
452  | [e] -> e
453  | _ :: l -> last l
454
455(** [last_stmt block] returns the last statement of the block [block], if
456    any. *)
457
458let last_stmt block = match block.Cil_types.bstmts with
459  | [] -> raise (Unsupported_loop "no increment instruction")
460  | stmts -> last stmts
461
462(** [extract_added_value counter e] supposes that the expression [e] is either
463    an addition or a substraction of the variable [counter]. It returns the
464    added value: exactly the value in case of an addition, and its opposite in
465    case of a substraction. It will be used to extract the increment of the
466    counter in a loop. *)
467
468let extract_added_value counter e = match e.Cil_types.enode with
469  | Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 ->
470    Cost_value.of_cil_exp e2
471  | Cil_types.BinOp (Cil_types.MinusA, e1, e2, _) when exp_is_var counter e1 ->
472    Cost_value.UnOp (Cost_value.Neg, Cost_value.of_cil_exp e2)
473  | _ -> raise (Unsupported_loop "unsupported increment expression")
474
475(** [extract_increment counter block] supposes that the block [block] ends with
476    an increment of the variable [counter]. It returns the increment. It will be
477    used to extract the increment in a loop body. *)
478
479let extract_increment counter block =
480  match (last_stmt block).Cil_types.skind with
481    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _))
482        when v.Cil_types.vname = counter ->
483      extract_added_value counter e
484    | _ -> raise (Unsupported_loop "no increment instruction found")
485
486let check b error = if not b then raise (Unsupported_loop error)
487
488(** [counter_preserved_until_last counter block] returns true iff the variable
489    [counter] is not assigned in the block [block], except potentially at the
490    very last instruction. This is a support condition for loops. *)
491
492let counter_preserved_until_last counter block =
493  let stmt_preserves stmt = match stmt.Cil_types.skind with
494    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), _, _)) ->
495      v.Cil_types.vname <> counter
496    | _ -> true in
497  let rec aux = function
498    | [] | [_] -> true
499    | stmt :: block -> (stmt_preserves stmt) && (aux block) in
500  aux block.Cil_types.bstmts
501
502(** [check supported_loop fun_name env counter init_value exit_value increment
503    block] raises an exception if the loop body [block] of the function
504    [fun_name] is not supported in the environment [env] and with regards to the
505    loop counter [counter], its initialization expression [init_value] and its
506    exit expression [exit_value]. We check that: the address of the loop counter
507    is not accessed in the whole function, the loop counter is not assigned in
508    the body (except at the end), the variables in the initialization and exit
509    expressions are parameters and their address is not accessed nor are they
510    assigned in the whole function. *)
511
512let check_supported_loop
513    fun_name env counter init_value exit_value increment block =
514  let fun_info = get_fun_info env fun_name in
515  let addressed = fun_info.addressed in
516  let parameters = StringTools.Set.of_list fun_info.parameters in
517  let modified = fun_info.modified in
518  let init_value_vars = Cost_value.vars init_value in
519  let exit_value_vars = Cost_value.vars exit_value in
520  let increment_vars = Cost_value.vars increment in
521  let vars = StringTools.Set.union init_value_vars exit_value_vars in
522  let vars = StringTools.Set.union vars increment_vars in
523  let addressed_or_modified = StringTools.Set.union addressed modified in
524  check (not (StringTools.Set.mem counter addressed))
525    "loop counter's address is accessed" ;
526  check (counter_preserved_until_last counter block)
527    "loop counter is modified inside loop body" ;
528  check (StringTools.Set.subset vars parameters)
529    "local or global inside a loop expression" ;
530  check (StringTools.Set.disjoint vars addressed_or_modified)
531    "the value of a parameter in a loop expression may be modified"
532
533(** [mk_loop_cost init_value increment body_cost] returns a function that, when
534    providing a current value of the loop counter, returns the current cost of a
535    loop of first value [init_value], of increment [increment] and whose body
536    cost is [body_cost]. This function will be used with the loop counter for an
537    invariant of the loop, and with the final value of the counter for a total
538    cost of the loop. *)
539
540let mk_loop_cost init_value increment body_cost =
541  fun i ->
542    let v = Cost_value.BinOp (Cost_value.Sub, i, init_value) in
543    let v = Cost_value.BinOp (Cost_value.Div, v, increment) in
544    Cost_value.BinOp (Cost_value.Mul, v, body_cost)
545
546(** [last_value rel init_value exit_value increment] returns the last value
547    taken by the counter of a loop when the first value is [init_value], the
548    comparison relation in the guard is [rel], the compared value is
549    [exit_value] and the increment is [increment]. *)
550
551let last_value rel init_value exit_value increment =
552  let (op1, v1, v2, v3) = match rel with
553    | Cost_value.Le -> (Cost_value.Sub, exit_value, init_value, increment)
554    | Cost_value.Lt ->
555      (Cost_value.Add, init_value, exit_value, Cost_value.Int 0)
556    | Cost_value.Ge -> (Cost_value.Add, init_value, exit_value, increment)
557    | Cost_value.Gt ->
558      (Cost_value.Sub, exit_value, init_value, Cost_value.Int 0) in
559  let res = Cost_value.BinOp (Cost_value.Sub, v1, v2) in
560  let incr_mod = Cost_value.abs increment in
561  let res = Cost_value.BinOp (Cost_value.Mod, res, incr_mod) in
562  let res = Cost_value.BinOp (op1, exit_value, res) in
563  Cost_value.BinOp (Cost_value.Add, res, v3)
564
565(** [stmt_cost fun_name cost_incr env previous_stmt stmt] returns the
566    requirements and the cost of the statement [stmt] of the function [fun_name]
567    in the environment [env] when [cost_incr] is the name of the cost update
568    function and [previous_stmt] is the (optional) previous statement. *)
569
570let rec stmt_cost fun_name cost_incr env previous_stmt stmt
571    : require list * Cost_value.t =
572  let block_cost block = block_cost fun_name cost_incr env block in
573
574  let rec aux stmt = match stmt.Cil_types.skind with
575
576    | Cil_types.Instr instr -> ([], instr_cost cost_incr instr)
577
578    | Cil_types.Goto (stmt_ref, _) -> goto_cost !stmt_ref
579
580    | Cil_types.If (_, block1, block2, _) ->
581      let (requires1, cost1) = block_cost block1 in
582      let (requires2, cost2) = block_cost block2 in
583      (requires1 @ requires2, Cost_value.BinOp (Cost_value.Max, cost1, cost2))
584
585    | Cil_types.Loop (_, block, _, _, _) ->
586      (* if has_loop block then raise Nested_loops
587      else *) loop_cost fun_name cost_incr env previous_stmt block
588
589    | Cil_types.Block block -> block_cost block
590
591    | Cil_types.Return _ | Cil_types.Break _ | Cil_types.Continue _ ->
592      ([], Cost_value.Int 0)
593
594    | Cil_types.Switch _ -> raise (Unsupported "switch")
595
596    | Cil_types.UnspecifiedSequence _ ->
597      raise (Unsupported "unspecified sequence")
598
599    | Cil_types.TryFinally _ -> raise (Unsupported "try finally")
600
601    | Cil_types.TryExcept _ -> raise (Unsupported "try except") in
602
603  aux stmt
604
605(** [block_cost fun_name cost_incr env block] returns the requirements and the
606    cost of the block [block] of the function [fun_name] in the environment
607    [env] when [cost_incr] is the name of the cost update function. *)
608
609and block_cost fun_name cost_incr env block : require list * Cost_value.t =
610  let f (previous_stmt, requires, cost) stmt =
611    let (added_requires, added_cost) =
612      stmt_cost fun_name cost_incr env previous_stmt stmt in
613    (Some stmt,
614     requires @ added_requires,
615     Cost_value.BinOp (Cost_value.Add, cost, added_cost)) in
616  let (_, requires, cost) =
617    List.fold_left f (None, [], Cost_value.Int 0) block.Cil_types.bstmts in
618  (requires, cost)
619
620(** [loop_infos fun_name cost_incr env previous_stmt block] returns all the
621    extracted cost information of a loop in function [fun_name], in environment
622    [env], with [cost_incr] for the name of the cost update function, with
623    (optional) previous statement [previous_stmt] and of body [block]. The
624    returned information are: the requirements for the loop termination, the
625    loop counter, its first value, the comparison relation of the guard, the
626    compared value in the guard, the increment and a function that, provided a
627    current value for the loop counter, returns the current cost of the loop. *)
628
629and loop_infos fun_name cost_incr env previous_stmt block
630    : require list * string * Cost_value.t * Cost_value.relation *
631      Cost_value.t * Cost_value.t * (Cost_value.t -> Cost_value.t) =
632  let (counter, init_value) = extract_counter_and_init previous_stmt in
633  let (rel, exit_value) = extract_guard counter block in
634  let increment = extract_increment counter block in
635  check_supported_loop
636    fun_name env counter init_value exit_value increment block ;
637  let (requires, body_cost) = block_cost fun_name cost_incr env block in
638  let requires = [(rel, init_value, exit_value, increment)] @ requires in
639  let cost = mk_loop_cost init_value increment body_cost in
640  (requires, counter, init_value, rel, exit_value, increment, cost)
641
642(** [loop_cost fun_name cost_incr env previous_stmt block] returns the
643    requirements and the cost of the loop of body [block] in the function
644    [fun_name] in the environment [env] when [cost_incr] is the name of the cost
645    update function and [previous_stmt] is the (optional) previous statement. *)
646
647and loop_cost fun_name cost_incr env previous_stmt block
648    : require list * Cost_value.t =
649  let (requires, _, init_value, rel, exit_value, increment, cost) =
650    loop_infos fun_name cost_incr env previous_stmt block in
651  let cost = cost (last_value rel init_value exit_value increment) in
652  let cost =
653    Cost_value.Cond (init_value, rel, exit_value, cost, Cost_value.Int 0) in
654  (requires, cost)
655
656
657(*** Costs computation ***)
658
659(* Once a cost (that may depend on the cost of the other functions) has been
660   associated to each function of a program, we want to simplify them in order
661   to have independent costs. To this end, we simply apply a fixpoint where at
662   each step, the independent cost of a function is replaced in the cost of
663   whatever function mentions it. For exampe, in the following configuration:
664     cost of f(x) <= x*x + 3
665     cost of g() <= cost of h()
666     cost of h(y) <= -1 + cost of f(y)
667   then a step of the fixpoint will lead to:
668     cost of f(x) <= x*x + 3
669     cost of g() <= cost of h()
670     cost of h(y) <= -1 + y*y + 3 *)
671
672(** [is_solved costs] returns true iff the system of inequations formed by the
673    costs [costs] is solved, i.e. if every cost is independent of the others and
674    does not mention to special cost value [Any]. *)
675
676let is_solved costs =
677  let f _ cost res =
678    res && (Cost_value.is_independent cost) &&
679      (not (Cost_value.has_any cost)) in
680  StringTools.Map.fold f costs true
681
682(** [solve_end costs1 costs2] returns true iff a fixpoint has been reached,
683    i.e. if the costs [costs2] of the current iteration are the same as the
684    costs [costs1] of the previous iteration. *)
685
686let solve_end costs1 costs2 =
687  let f fun_name cost res =
688    res && (StringTools.Map.mem fun_name costs1) &&
689      (cost = StringTools.Map.find fun_name costs1) in
690  StringTools.Map.fold f costs2 true
691
692(** [solve_costs extern_costs prototypes costs] solves the system of inequations
693    formed by the costs [costs]. It applies a reduction operation until a
694    fixpoint is reached. *)
695
696let rec solve_costs extern_costs prototypes costs =
697  let costs' = Cost_value.reduces extern_costs costs prototypes costs in
698  if solve_end costs costs' then
699    if is_solved costs' then costs'
700    else raise Unresolvable
701  else solve_costs extern_costs prototypes costs'
702
703class compute_costs cost_incr env costs prj = object
704  inherit Visitor.frama_c_copy prj as super
705
706  method vfunc fundec =
707    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
708    let block = fundec.Cil_types.sbody in
709    let cost = block_cost fun_name cost_incr env block in
710    costs := StringTools.Map.add fun_name cost !costs ;
711    Cil.SkipChildren
712
713end
714
715(** [compute_costs extern_costs cost_incr env] computes the cost associated to
716    each function of the current program in the current project. First, it
717    computes the costs potentially depending on that of the other functions, and
718    then it tries to solve the system of inequations that this produces. *)
719
720let compute_costs extern_costs cost_incr env
721    : (require list * Cost_value.t) StringTools.Map.t =
722  let costs : (require list * Cost_value.t) StringTools.Map.t ref =
723    ref StringTools.Map.empty  in
724  let compute_costs_prj =       
725    File.create_project_from_visitor
726      "cerco_compute_costs"
727      (new compute_costs cost_incr env costs) in
728  let f () =
729    let (requires, costs) = StringTools.Map.split_couple !costs in
730    let costs = solve_costs extern_costs (prototypes env) costs in
731    StringTools.Map.combine requires costs in
732  Project.on compute_costs_prj f ()
733
734
735(*** Add annotations ***)
736
737let add_tmp_cost_init env tmp_cost stmt =
738  let lval = Cil.var tmp_cost in
739  let e =
740    Cil.new_exp dummy_location
741      (Cil_types.Lval (Cil.var (get_cost_varinfo env))) in
742  let new_stmt =
743    Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
744  let new_stmt = Cil.mkStmt new_stmt in
745  Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))
746
747let make_requires requires =
748  let f (rel, init_value, exit_value, increment) =
749    let init_value = Cost_value.to_cil_term init_value in
750    let exit_value = Cost_value.to_cil_term exit_value in
751    let increment = Cost_value.to_cil_term increment in
752    let rel' = Cost_value.mk_strict rel in
753    let rel = Cost_value.cil_rel_of_rel rel in
754    let rel' = Cost_value.cil_rel_of_rel rel' in
755    let t1 = Logic_const.prel (rel, init_value, exit_value) in
756    let t2 = Logic_const.prel (rel', Cost_value.tinteger 0, increment) in
757    Logic_const.pimplies (t1, t2) in
758  List.map f requires
759
760let add_spec pres post spec =
761  let requires = List.map Logic_const.new_predicate pres in
762  let post_cond = [(Cil_types.Normal, Logic_const.new_predicate post)] in
763  let new_behavior = Cil.mk_behavior ~requires ~post_cond () in
764  spec.Cil_types.spec_behavior <- new_behavior :: spec.Cil_types.spec_behavior
765
766let add_cost_annotation requires rel cost_id cost spec =
767  let post = mk_fun_cost_pred rel cost_id cost in 
768  add_spec (make_requires requires) post spec ;
769  Cil.ChangeDoChildrenPost (spec, identity)
770
771let add_cost_incr_annotation cost_id spec =
772  let rel = Cil_types.Req in
773  let cost = Cost_value.Var "incr" in
774  add_cost_annotation [] rel cost_id cost spec
775
776let add_regular_fun_annotation fun_name cost_id costs spec =
777  let rel = Cil_types.Rle in
778  let (requires, cost) = StringTools.Map.find fun_name costs in
779  add_cost_annotation requires rel cost_id cost spec
780
781let add_fundec_annotation cost_id cost_incr costs fun_name spec =
782  if fun_name = cost_incr then add_cost_incr_annotation cost_id spec
783  else add_regular_fun_annotation fun_name cost_id costs spec
784
785let mk_loop_invariant_counter_init_value
786    extern_costs costs prots counter init_value increment =
787  let mk_value value =
788    let incr_mod = Cost_value.abs increment in
789    let v = Cost_value.BinOp (Cost_value.Mod, value, incr_mod) in
790    Cost_value.to_cil_term (Cost_value.reduce extern_costs costs prots v) in
791  let v1 = mk_value (Cost_value.Var counter) in
792  let v2 = mk_value init_value in
793  let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
794  mk_invariant invariant
795
796let mk_loop_invariant_counter_last_value
797    extern_costs costs prots counter rel init_value exit_value increment =
798  let last_value = last_value rel init_value exit_value increment in
799  let last_value = Cost_value.reduce extern_costs costs prots last_value in
800  let last_value = Cost_value.to_cil_term last_value in
801  let rel' = Cost_value.cil_rel_of_rel rel in
802  let init_value = Cost_value.to_cil_term init_value in
803  let exit_value = Cost_value.to_cil_term exit_value in
804  let require = Logic_const.prel (rel', init_value, exit_value) in
805  let rel' = Cost_value.cil_rel_of_rel (Cost_value.mk_large rel) in
806  let counter = Cost_value.to_cil_term (Cost_value.Var counter) in
807  let prop = Logic_const.prel (rel', counter, last_value) in
808  let invariant = Logic_const.pimplies (require, prop) in
809  mk_invariant invariant
810
811let mk_loop_invariant_counter_no_change counter rel init_value exit_value =
812  let rel = Cost_value.opposite rel in
813  let rel' = Cost_value.cil_rel_of_rel rel in
814  let init_value = Cost_value.to_cil_term init_value in
815  let exit_value = Cost_value.to_cil_term exit_value in
816  let require = Logic_const.prel (rel', init_value, exit_value) in
817  let counter = Cost_value.to_cil_term (Cost_value.Var counter) in
818  let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in
819  let invariant = Logic_const.pimplies (require, prop) in
820  mk_invariant invariant
821
822let mk_loop_invariant_cost
823    extern_costs tmp_cost costs prots cost_id counter cost =
824  let loop_cost = cost (Cost_value.Var counter) in
825  let loop_cost = Cost_value.reduce extern_costs costs prots loop_cost in
826  let loop_cost = Cost_value.to_cil_term loop_cost in
827  let cost_var =
828    Logic_const.tvar (Cil_const.make_logic_var cost_id Cil_types.Linteger) in
829  let tmp_cost = Cost_value.to_cil_term (Cost_value.Var tmp_cost) in
830  let new_cost = Cil_types.TBinOp (Cil_types.PlusA, tmp_cost, loop_cost) in
831  let new_cost = integer_term new_cost in
832  let invariant = Logic_const.prel (Cil_types.Rle, cost_var, new_cost) in
833  mk_invariant invariant
834
835let mk_loop_variant
836    extern_costs costs prots counter init_value rel exit_value increment =
837  let last_value = last_value rel init_value exit_value increment in
838  let counter_var = Cost_value.Var counter in
839  let (v1, v2) = match rel with
840    | Cost_value.Lt | Cost_value.Le -> (last_value, counter_var)
841    | Cost_value.Gt | Cost_value.Ge -> (counter_var, last_value) in
842  let variant = Cost_value.BinOp (Cost_value.Sub, v1, v2) in
843  let variant = Cost_value.reduce extern_costs costs prots variant in
844  mk_variant (Cost_value.to_cil_term variant)
845
846let annot_loop
847    extern_costs tmp_cost cost_id cost_incr env costs obj stmt
848    previous_stmt block =
849  let (_, costs) = StringTools.Map.split_couple costs in
850  let prots = prototypes env in
851  let fun_name = current_fun_name obj in
852  let (_, counter, init_value, rel, exit_value, increment, cost) =
853    loop_infos fun_name cost_incr env previous_stmt block in
854  let invariant_counter_init_value =
855    mk_loop_invariant_counter_init_value
856      extern_costs costs prots counter init_value increment in
857  let invariant_counter_last_value =
858    mk_loop_invariant_counter_last_value
859      extern_costs costs prots counter rel init_value exit_value increment in
860  let invariant_counter_no_change =
861    mk_loop_invariant_counter_no_change counter rel init_value exit_value in
862  let invariant_cost =
863    mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id
864      counter cost in
865  let variant =
866    mk_loop_variant extern_costs costs prots counter init_value rel exit_value
867      increment in
868  add_loop_annot obj stmt invariant_counter_init_value ;
869  add_loop_annot obj stmt invariant_counter_last_value ;
870  add_loop_annot obj stmt invariant_counter_no_change ;
871  add_loop_annot obj stmt invariant_cost ;
872  add_loop_annot obj stmt variant
873
874class add_annotations extern_costs cost_id cost_incr env costs prj =
875object (self) inherit Visitor.frama_c_copy prj as super
876
877  val mutable tmp_costs : Cil_types.varinfo list = []
878  val mutable previous_stmt = None
879
880  method vstmt_aux stmt =
881    let old_stmt = previous_stmt in
882    previous_stmt <- Some stmt ;
883    match stmt.Cil_types.skind with
884      | Cil_types.Loop (_, block, _, _, _) ->
885        assert (List.length tmp_costs > 0) ;
886        let tmp_cost = List.hd tmp_costs in
887        tmp_costs <- List.tl tmp_costs ;
888        let tmp_cost_id = tmp_cost.Cil_types.vname in
889        annot_loop
890          extern_costs tmp_cost_id cost_id cost_incr env costs self stmt
891          old_stmt block ;
892        Cil.ChangeDoChildrenPost (stmt, add_tmp_cost_init env tmp_cost)
893      | _ -> Cil.DoChildren
894
895  method vspec spec = match self#current_kf with
896    | None -> Cil.JustCopy 
897    | Some kf ->
898      match kf.Db_types.fundec with
899        | Db_types.Definition (fundec, _) ->
900          let fun_name = fundec.Cil_types.svar.Cil_types.vname in
901          add_fundec_annotation cost_id cost_incr costs fun_name spec
902        | Db_types.Declaration (_, f, _, _) when
903            StringTools.Map.mem f.Cil_types.vname extern_costs ->
904          let cost = StringTools.Map.find f.Cil_types.vname extern_costs in
905          let cost = Cost_value.Var cost in
906          add_cost_annotation [] Cil_types.Rle cost_id cost spec
907        | _ -> Cil.JustCopy
908
909  method vfunc fundec =
910    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
911    tmp_costs <- make_freshes fundec (get_nb_loops env fun_name) cost_id ;
912    previous_stmt <- None ;
913    Cil.DoChildren
914
915end
916
917let add_annotations extern_costs fname cost_id cost_incr env costs =
918  let add_annotations_prj =     
919    File.create_project_from_visitor
920      "cerco_add_annotations"
921      (new add_annotations extern_costs cost_id cost_incr env costs) in
922  let f () =
923    Parameters.CodeOutput.set fname ;
924    File.pretty_ast () in
925  Project.on add_annotations_prj f ()
926
927
928(*** Saving cost results ***)
929
930let save_results fname costs =
931  let f fun_name (_, cost) res =
932    res ^ fun_name ^ " " ^ (Cost_value.to_string cost) ^ "\n" in
933  let s = StringTools.Map.fold f costs "" in
934  let save_file =
935    try Filename.chop_extension fname
936    with Invalid_argument "Filename.chop_extension" -> fname in
937  let save_file = save_file ^ ".cost_results" in
938  try
939    let oc = open_out save_file in
940    output_string oc s ;
941    close_out oc
942  with Sys_error _ ->
943    Printf.eprintf "Could not save plug-in results in file %s\n%!" save_file
944
945
946(*** Main ***)
947
948let cost ((fname, _), f_old_name, cost_id, cost_incr, extern_costs) =
949  try
950    Parameters.Files.set [fname] ;
951    File.init_from_cmdline () ;
952    let env = initializations cost_id in
953    let costs = compute_costs extern_costs cost_incr env in
954    save_results f_old_name costs ;
955    add_annotations extern_costs fname cost_id cost_incr env costs
956  with e -> Printf.eprintf "** ERROR: %s\n%!" (string_of_exception cost_incr e)
Note: See TracBrowser for help on using the repository browser.