source: Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin/compute.ml @ 1689

Last change on this file since 1689 was 1689, checked in by tranquil, 8 years ago

kept out the wrapper (which I did not touch, so not sure it works)

File size: 45.5 KB
RevLine 
[1462]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
[1508]205let are_parameters env fun_name =
206        StringTools.Set.for_all (is_parameter env fun_name)
[1462]207
208let prototypes env =
209  let f fun_info = fun_info.parameters in
210  StringTools.Map.map f (get_fun_infos env)
211
212let get_locals env fun_name = (get_fun_info env fun_name).locals
213
214let get_modified env fun_name = (get_fun_info env fun_name).modified
215
216let upd_modified env fun_name modified =
217  let fun_info = get_fun_info env fun_name in
218  let fun_info = { fun_info with modified = modified } in
219  upd_fun_info env fun_name fun_info
220
221let get_nb_loops env fun_name =
222  (get_fun_info env fun_name).nb_loops
223
224let upd_nb_loops env fun_name nb_loops =
225  let fun_info = get_fun_info env fun_name in
226  let fun_info = { fun_info with nb_loops = nb_loops } in
227  upd_fun_info env fun_name fun_info
228
229let add_nb_loops env fun_name =
230  upd_nb_loops env fun_name ((get_nb_loops env fun_name) + 1)
231
232let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
233
234
235(*** Initializations ***)
236
237(* Initializing the environment simply consists in visiting every function and
238   set their information in the environment. *)
239
240class initializations cost_id env prj = object (self)
241  inherit Visitor.frama_c_copy prj as super
242
243  (* Update the variables whose address may be accessed. This is done by
244     visiting every expression of the program. *)
245  method vexpr e =
246    let _ = match e.Cil_types.enode with
247      | Cil_types.AddrOf (Cil_types.Var var, _) ->
248        let fun_name = current_fun_name self in
249        let addressed = get_addressed !env fun_name in
250        let addressed =
251          StringTools.Set.add var.Cil_types.vname addressed in
252        env := upd_addressed !env fun_name addressed
253      | _ -> () in
254    Cil.DoChildren
255
256  (* Update the variables whose address may be accessed. This is done by
257     visiting every statement of the program. *)
258  method vstmt_aux stmt =
259    let fun_name = current_fun_name self in
260    let _ = match stmt.Cil_types.skind with
261      | Cil_types.Instr (Cil_types.Set ((Cil_types.Var var, _), _, _)) ->
262        let modified = get_modified !env fun_name in
263        let modified = StringTools.Set.add var.Cil_types.vname modified in
264        env := upd_modified !env fun_name modified
265      | Cil_types.Loop _ -> env := add_nb_loops !env fun_name
266      | _ -> () in
267    Cil.DoChildren
268
269  (* When a function is found, create its entry in the environment, set its
270     parameters and its locals (the information is already accessible), and
271     leave empty the set of assigned and addressed variables. The two latters
272     will be updated when visiting the statements and the expressions. *)
273  method vfunc fundec =
274    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
275    let addressed = StringTools.Set.empty in
276    let varinfo_to_string x = x.Cil_types.vname in
277    let parameters = List.map varinfo_to_string fundec.Cil_types.sformals in
278    let f_locals res x = StringTools.Set.add (varinfo_to_string x) res in
279    let locals =
280      List.fold_left f_locals StringTools.Set.empty fundec.Cil_types.slocals in
281    let modified = StringTools.Set.empty in
282    let nb_loops = 0 in
283    let fun_info =
284      mk_fun_info addressed parameters locals modified nb_loops in
285    let fun_infos =
286      StringTools.Map.add fun_name fun_info (get_fun_infos !env) in
287    env := upd_fun_infos !env fun_infos ;
288    Cil.DoChildren
289
290  (* Update the varinfo of the cost variable. *)
291  method vglob_aux glob =
292    let _ = match glob with
293      | Cil_types.GVarDecl (_, varinfo, _)
294      | Cil_types.GVar (varinfo, _, _) when varinfo.Cil_types.vname = cost_id ->
295        env := upd_cost_varinfo !env varinfo
296      | _ -> () in
297    Cil.DoChildren
298
299end
300
301(** [initializations cost_id] consider the current file in the current project
302    and returns a corresponding initialized environment .*)
303
304let initializations cost_id : env =
305  let env : env ref = ref init_env in
306  let initializations_prj =     
307    File.create_project_from_visitor
308      "cerco_initializations" (new initializations cost_id env) in
309  let f () = !env in
310  Project.on initializations_prj f ()
311
312
313(* Test if a block has a loop. Used to test the presence of nested
314   loops. Indeed, they not supported for now, until a bug in Jessie is fixed. *)
315
316let rec has_loop_stmt stmt = match stmt.Cil_types.skind with
317  | Cil_types.Instr _ | Cil_types.Return _ | Cil_types.Goto _
318  | Cil_types.Break _ | Cil_types.Continue _ -> false
319  | Cil_types.If (_, block1, block2, _)
320  | Cil_types.TryFinally (block1, block2, _)
321  | Cil_types.TryExcept (block1, _, block2, _) ->
322    (has_loop block1) || (has_loop block2)
323  | Cil_types.Switch (_, block, _, _)
324  | Cil_types.Block block -> has_loop block
325  | Cil_types.Loop _ -> true
326  | Cil_types.UnspecifiedSequence l ->
327    has_loop_stmt_list (List.map (fun (stmt, _, _, _, _) -> stmt) l)
328
329and has_loop_stmt_list stmt_list =
330  let f res stmt = res || (has_loop_stmt stmt) in
331  List.fold_left f false stmt_list
332
333(** [has_loop block] returns true iff the block of instructions [block] contains
334    a loop. *)
335
336and has_loop block = has_loop_stmt_list block.Cil_types.bstmts
337
338
339(*** Statement and block cost ***)
340
341(* Requirement for loop termination. They have the form:
342   (guard relation, initialization value, exit value, increment) *)
343
344type require = Cost_value.relation * Cost_value.t * Cost_value.t * Cost_value.t
345
346(** [const_incr_cost e] extracts the integer constant that the expression [e]
347    represents. *)
348
[1508]349let cost_incr_cost e =
350  match e.Cil_types.enode with
351    | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
352      Cost_value.Int (Int64.to_int i)
353    | _ -> raise Cost_incr_arg_not_constant
[1462]354
355(** [call cost cost_incr f args] returns the cost of calling the function [f] on
356    arguments [args]. If the function is the cost update function [cost_incr],
357    then its cost is the value of its argument, which needs to be a constant
358    integer. Otherwise, it is simply the cost of executing [f] on its
359    arguments. *)
360
361let call_cost cost_incr f args = match f.Cil_types.enode with
[1508]362  | Cil_types.Lval (Cil_types.Var var, Cil_types.NoOffset)
[1462]363      when var.Cil_types.vname = cost_incr ->
[1508]364    cost_incr_cost (List.hd args)
365  | Cil_types.Lval (Cil_types.Var var, Cil_types.NoOffset) ->
[1462]366    (try
367       let args = List.map Cost_value.of_cil_exp args in
368       Cost_value.CostOf (var.Cil_types.vname, args)
369     with Cost_value.Unsupported_exp -> raise Unsupported_exp)
370  | _ -> raise Unresolvable_function
371
372(** [instr_cost cost_incr instr] returns the cost of executing the simple
373    instruction [instr]. Only function calls do have a cost. *)
374
375let instr_cost cost_incr = function
376  | Cil_types.Call (_, f, args, _) ->
377    call_cost cost_incr f args
378  | _ -> Cost_value.Int 0
379
380(* Frama-C sometimes transforms the control flow graph of a function by
381   factorizing a return instructions through added gotos. We handle this special
382   case of gotos with the function below, but other forms are not supported. *)
383
384let goto_cost stmt = match stmt.Cil_types.skind with
385  | Cil_types.Return _ -> ([], Cost_value.Int 0)
386  | _ -> raise (Unsupported "goto")
387
388(* In Frama-C, every C loop construct is transformed into an infinite loop with
389   a break inside a conditional to exit. Initialization of a for loop are
390   located in the very previous instruction. The guard can either be at the
391   beginning of the loop in the cases of for and while loops, or at the end in
392   the case of a do-while loop. Finally, the increment instruction is located at
393   the end in the case of a for loop. *)
394
395(** [extract_counter_and_init stmt_opt] supposes that the optional statement
396    [stmt_opt] is in fact an assignment instruction. In this case, it returns
397    the assigned variable and the expression to assign, otherwise it raises an
398    error. It will be used to extract the loop counter and its first value in
399    the case of a loop initialization instruction. *)
400
[1508]401let extract_counter_and_init stmt2_opt stmt1_opt =
[1462]402  let error () = raise (Unsupported_loop "no initialization found") in
[1508]403  match stmt2_opt, stmt1_opt with
404    | None, _ | _, None -> error ()
405    | Some stmt2, Some stmt1 ->
406      match stmt2.Cil_types.skind, stmt1.Cil_types.skind with
407        | Cil_types.Instr (Cil_types.Set ((Cil_types.Var i, _), z, _)),
408          Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
409          (match Cost_value.of_cil_exp z with
410            | Cost_value.Int 0 ->
411              (v.Cil_types.vname, i.Cil_types.vname, Cost_value.of_cil_exp e)
412            | _ -> error())
[1462]413        | _ -> error ()
414
415(** [first_stmt block] returns the first statement of the block [block], if
416    any. *)
417
418let first_stmt block = match block.Cil_types.bstmts with
419  | [] -> raise (Unsupported_loop "no guard")
420  | instr :: _ -> instr
421
422(** [exp_is_var name e] returns true iff the expression [e] is in fact the
423    variable of name [name]. *)
424
425let exp_is_var name e = match e.Cil_types.enode with
[1508]426  | Cil_types.Lval (Cil_types.Var v, Cil_types.NoOffset) ->
427    v.Cil_types.vname = name
[1462]428  | _ -> false
429
[1508]430let var_of_exp e = match e.Cil_types.enode with
431  | Cil_types.Lval (Cil_types.Var v, Cil_types.NoOffset) ->
432    v.Cil_types.vname
433  | _ -> invalid_arg "var_of_exp"
434
435let const_of_exp e =
436  match e.Cil_types.enode with
437    | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
438      Int64.to_int i
439    | _ -> invalid_arg "const_of_exp"
440
[1462]441(** [starts_with_break block] returns true iff the block [block] starts with a
442    break instruction. *)
443
444let starts_with_break block = match (first_stmt block).Cil_types.skind with
445  | Cil_types.Break _ -> true
446  | _ -> false
447
448(** [extract_guard counter block] supposes that the first statement of the block
449    [block] is a conditional with an exit instruction. It then supposes that the
450    conditional is a test on the variable [counter]. It returns the comparison
451    relation along with the expression that the counter is compared to. It will
452    be used to extract the guard condition of a loop. *)
453
454let extract_guard counter block = match (first_stmt block).Cil_types.skind with
455  | Cil_types.If (e, _, block, _) when starts_with_break block ->
456    (match e.Cil_types.enode with
457      | Cil_types.BinOp (rel, e1, e2, _) when exp_is_var counter e1 ->
458        (Cost_value.rel_of_cil_rel rel, Cost_value.of_cil_exp e2)
459      | _ -> raise (Unsupported_loop "unsupported guard expression"))
460  | _ -> raise (Unsupported_loop "no guard found")
461
462(** [last l] returns the last element of the list [l], if any. *)
463
464let rec last = function
465  | [] -> raise (Failure "Compute.last")
466  | [e] -> e
467  | _ :: l -> last l
468
[1508]469let rec last_2 = function
470  | [] | [_] -> raise (Failure "Compute.last_2")
471  | [e1 ; e2] -> (e1, e2)
472  | _ :: l -> last_2 l
473
474let rec last_stmt stmt = match stmt.Cil_types.skind with
475  | Cil_types.Block block ->
476    last_stmt (last block.Cil_types.bstmts)
477  | _ -> stmt
478
479(** [last_2_stmt block] returns the last two statement of the block [block], if
[1462]480    any. *)
481
[1508]482let last_2_stmt block = match block.Cil_types.bstmts with
483  | [] | [_] -> raise (Unsupported_loop "no increment instruction")
484  | stmts ->
485    let (snd_last, last) = last_2 stmts in
486    (last_stmt snd_last, last)
[1462]487
[1508]488
[1462]489(** [extract_added_value counter e] supposes that the expression [e] is either
490    an addition or a substraction of the variable [counter]. It returns the
491    added value: exactly the value in case of an addition, and its opposite in
492    case of a substraction. It will be used to extract the increment of the
493    counter in a loop. *)
494
495let extract_added_value counter e = match e.Cil_types.enode with
496  | Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 ->
497    Cost_value.of_cil_exp e2
498  | Cil_types.BinOp (Cil_types.MinusA, e1, e2, _) when exp_is_var counter e1 ->
499    Cost_value.UnOp (Cost_value.Neg, Cost_value.of_cil_exp e2)
500  | _ -> raise (Unsupported_loop "unsupported increment expression")
501
502(** [extract_increment counter block] supposes that the block [block] ends with
503    an increment of the variable [counter]. It returns the increment. It will be
504    used to extract the increment in a loop body. *)
505
[1508]506let extract_increment counter index block =
507  let (snd_last, last) = last_2_stmt block in
508  match snd_last.Cil_types.skind, last.Cil_types.skind with
509    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var i, _), o, _)),
510      Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _))
511      when v.Cil_types.vname = counter && i.Cil_types.vname = index ->
512      (match extract_added_value index o with
513        | Cost_value.Int 1 -> extract_added_value counter e
514        | _ -> raise (Unsupported_loop "loop index malformation"))
[1462]515    | _ -> raise (Unsupported_loop "no increment instruction found")
516
517let check b error = if not b then raise (Unsupported_loop error)
518
519(** [counter_preserved_until_last counter block] returns true iff the variable
520    [counter] is not assigned in the block [block], except potentially at the
521    very last instruction. This is a support condition for loops. *)
522
523let counter_preserved_until_last counter block =
524  let stmt_preserves stmt = match stmt.Cil_types.skind with
525    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), _, _)) ->
526      v.Cil_types.vname <> counter
527    | _ -> true in
528  let rec aux = function
529    | [] | [_] -> true
530    | stmt :: block -> (stmt_preserves stmt) && (aux block) in
531  aux block.Cil_types.bstmts
532
533(** [check supported_loop fun_name env counter init_value exit_value increment
534    block] raises an exception if the loop body [block] of the function
535    [fun_name] is not supported in the environment [env] and with regards to the
536    loop counter [counter], its initialization expression [init_value] and its
537    exit expression [exit_value]. We check that: the address of the loop counter
538    is not accessed in the whole function, the loop counter is not assigned in
539    the body (except at the end), the variables in the initialization and exit
540    expressions are parameters and their address is not accessed nor are they
541    assigned in the whole function. *)
542
543let check_supported_loop
544    fun_name env counter init_value exit_value increment block =
545  let fun_info = get_fun_info env fun_name in
546  let addressed = fun_info.addressed in
547  let parameters = StringTools.Set.of_list fun_info.parameters in
548  let modified = fun_info.modified in
549  let init_value_vars = Cost_value.vars init_value in
550  let exit_value_vars = Cost_value.vars exit_value in
551  let increment_vars = Cost_value.vars increment in
552  let vars = StringTools.Set.union init_value_vars exit_value_vars in
553  let vars = StringTools.Set.union vars increment_vars in
554  let addressed_or_modified = StringTools.Set.union addressed modified in
555  check (not (StringTools.Set.mem counter addressed))
556    "loop counter's address is accessed" ;
557  check (counter_preserved_until_last counter block)
558    "loop counter is modified inside loop body" ;
559  check (StringTools.Set.subset vars parameters)
560    "local or global inside a loop expression" ;
561  check (StringTools.Set.disjoint vars addressed_or_modified)
562    "the value of a parameter in a loop expression may be modified"
563
[1508]564let rec mk_loop_cost_index index k v inc cost =
565  let round_up h a b =
566    let h_mod_a = h mod a in
567    let b_mod_a = b mod a in
568    h - h_mod_a + b_mod_a + if h_mod_a <= b_mod_a then 0 else a in
569  match cost with
570  | Cost_value.CostCond (i, cond, tif, telse) when i <> index ->
571    let tif = mk_loop_cost_index index k v inc tif in
572    let telse = mk_loop_cost_index index k v inc telse in
573    Cost_value.CostCond (i, cond, tif, telse)
574  | Cost_value.CostCond (_, Cost_value.Ceq h, _, telse) when k > h ->
575    mk_loop_cost_index index k v inc telse
576  | Cost_value.CostCond (_, Cost_value.Ceq h, tif, telse) when k = h ->
577    (* let sum = *)
578      Cost_value.add tif (mk_loop_cost_index index (k+inc) v inc telse) (* in *)
579    (* Cost_value.Cond(v, Cost_value.Le, Cost_value.Int k, Cost_value.Int 0, sum) *)
580  | Cost_value.CostCond (_, Cost_value.Ceq h, tif, telse)
581    when (h - k) mod inc = 0 ->
582    let tif' = mk_loop_cost_index index k v inc telse in
583    let h_val = Cost_value.Int h in
584    let sum =
585      Cost_value.add tif (mk_loop_cost_index index (h + inc) v inc telse) in
586    let telse' =
587      Cost_value.add (mk_loop_cost_index index k h_val inc telse) sum in
588    Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse')
589  | Cost_value.CostCond (_, Cost_value.Ceq _, _, telse) ->
590    mk_loop_cost_index index k v inc telse
591  | Cost_value.CostCond (_, Cost_value.Cgeq h, tif, _) when k >= h ->
592    mk_loop_cost_index index k v inc tif
593  | Cost_value.CostCond (_, Cost_value.Cgeq h, tif, telse) ->
594    let tif' = mk_loop_cost_index index k v inc telse in
595    let h_val = Cost_value.Int h in
596    let telse' =
597      Cost_value.add
598        (mk_loop_cost_index index k h_val inc telse)
599        (mk_loop_cost_index index (round_up h inc k) v inc tif) in
600    Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse')
601  (* I'm supposing unrolling is never repeated *)
602  | Cost_value.CostCond (_, Cost_value.Cmod (a, b), tif, telse) when inc = 1 ->
603    let k' = round_up k a b in
604    let sub = Cost_value.sub
605      (mk_loop_cost_index index k' v a tif)
606      (mk_loop_cost_index index k' v a telse) in
607    Cost_value.add (mk_loop_cost_index index k v 1 telse) sub
608  | Cost_value.CostCond (_, Cost_value.Cmod (a, b), tif, telse)
609    when inc = a ->
610    let next = if k mod inc = b then tif else telse in
611    mk_loop_cost_index index k v inc next
612  | Cost_value.CostCond (_, Cost_value.Cmod _, _, _) ->
613    raise (Unsupported_loop "possible repeated unrolling")
614  | Cost_value.CostCond (_, Cost_value.Cgeqmod (h, a, b), tif, telse)
615    when k >= h ->
616    let next =
617      Cost_value.CostCond (index, Cost_value.Cmod (a, b), tif, telse) in
618    mk_loop_cost_index index k v inc next
619  | Cost_value.CostCond (_, Cost_value.Cgeqmod (h, a, b), tif, telse) ->
620    let tif' = mk_loop_cost_index index k v inc telse in
621    let h_val = Cost_value.Int h in
622    let next =
623      Cost_value.CostCond (index, Cost_value.Cmod (a, b), tif, telse) in
624    let telse' =
625      Cost_value.add
626        (mk_loop_cost_index index k h_val inc telse)
627        (mk_loop_cost_index index (round_up h inc k) v inc next) in
628    Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse')
629  | Cost_value.CostCond _ ->
630    raise (Unsupported_loop "unsupported cost condition")
631  | _ ->
632    let k_val = Cost_value.Int k in
633    let inc_val = Cost_value.Int inc in
634    let inc_val_m_1 = Cost_value.sub inc_val (Cost_value.Int 1) in
635    let n = Cost_value.add (Cost_value.sub v k_val) inc_val_m_1 in
636    let n = Cost_value.div n inc_val in
637    Cost_value.mul n cost
638    (* let zero = Cost_value.Int 0 in *)
639    (* Cost_value.Cond (v, Cost_value.Gt, k_val, Cost_value.mul n cost, zero) *)
640
[1462]641(** [mk_loop_cost init_value increment body_cost] returns a function that, when
642    providing a current value of the loop counter, returns the current cost of a
643    loop of first value [init_value], of increment [increment] and whose body
644    cost is [body_cost]. This function will be used with the loop counter for an
645    invariant of the loop, and with the final value of the counter for a total
646    cost of the loop. *)
647
[1508]648let mk_loop_cost init_value increment index body_cost =
[1462]649  fun i ->
650    let v = Cost_value.BinOp (Cost_value.Sub, i, init_value) in
651    let v = Cost_value.BinOp (Cost_value.Div, v, increment) in
[1508]652    (* this will in general reduce the steps and the size of amalgamation *)
653    let e = StringTools.Map.empty in
654    let body_cost = Cost_value.reduce e e e body_cost in
655    let body_cost = Cost_value.amalgamation body_cost in
[1689]656    Printf.printf "%s\n" (to_string body_cost);
[1508]657    mk_loop_cost_index index 0 v 1 body_cost
[1462]658
[1508]659
660
[1462]661(** [last_value rel init_value exit_value increment] returns the last value
662    taken by the counter of a loop when the first value is [init_value], the
663    comparison relation in the guard is [rel], the compared value is
664    [exit_value] and the increment is [increment]. *)
665
666let last_value rel init_value exit_value increment =
667  let (op1, v1, v2, v3) = match rel with
668    | Cost_value.Le -> (Cost_value.Sub, exit_value, init_value, increment)
669    | Cost_value.Lt ->
670      (Cost_value.Add, init_value, exit_value, Cost_value.Int 0)
671    | Cost_value.Ge -> (Cost_value.Add, init_value, exit_value, increment)
672    | Cost_value.Gt ->
673      (Cost_value.Sub, exit_value, init_value, Cost_value.Int 0) in
674  let res = Cost_value.BinOp (Cost_value.Sub, v1, v2) in
675  let incr_mod = Cost_value.abs increment in
676  let res = Cost_value.BinOp (Cost_value.Mod, res, incr_mod) in
677  let res = Cost_value.BinOp (op1, exit_value, res) in
678  Cost_value.BinOp (Cost_value.Add, res, v3)
679
[1508]680(** [stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt] returns the
[1462]681    requirements and the cost of the statement [stmt] of the function [fun_name]
682    in the environment [env] when [cost_incr] is the name of the cost update
[1508]683    function, [ind_set] is the set of loop indices encountered at this point
684    (which will be at most a singleton until nested loops are not supported)
685    and [prev2] and [prev1] are the (optional) previous statements. *)
[1462]686
[1508]687let rec stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt
[1462]688    : require list * Cost_value.t =
[1508]689  let block_cost block = block_cost fun_name cost_incr ind_set env block in
[1462]690
691  let rec aux stmt = match stmt.Cil_types.skind with
692    | Cil_types.Instr instr -> ([], instr_cost cost_incr instr)
693
694    | Cil_types.Goto (stmt_ref, _) -> goto_cost !stmt_ref
695
[1508]696    | Cil_types.If (e, block1, block2, _) ->
[1462]697      let (requires1, cost1) = block_cost block1 in
698      let (requires2, cost2) = block_cost block2 in
[1508]699      let cost =
700        match Cost_value.mk_cost_cond e with
701          | Some (ind, cost_cond) when List.mem ind ind_set ->
702            Cost_value.CostCond (ind, cost_cond, cost1, cost2)
703          | _ -> Cost_value.max cost1 cost2 in
704      (requires1 @ requires2, cost)
[1462]705
706    | Cil_types.Loop (_, block, _, _, _) ->
707      (* if has_loop block then raise Nested_loops
[1508]708      else *) loop_cost fun_name cost_incr ind_set env prev2 prev1 block
[1462]709
710    | Cil_types.Block block -> block_cost block
711
712    | Cil_types.Return _ | Cil_types.Break _ | Cil_types.Continue _ ->
713      ([], Cost_value.Int 0)
714
715    | Cil_types.Switch _ -> raise (Unsupported "switch")
716
[1508]717    | Cil_types.UnspecifiedSequence l ->
718      (* not interested in execution order, costs should reflect the
719         particular order chosen by the compiler *)
720      block_cost (Cil.block_from_unspecified_sequence l)
[1462]721
722    | Cil_types.TryFinally _ -> raise (Unsupported "try finally")
723
724    | Cil_types.TryExcept _ -> raise (Unsupported "try except") in
725
726  aux stmt
727
[1508]728(** [block_cost fun_name cost_incr ind_set env block] returns the requirements
729    and the cost of the block [block] of the function [fun_name] in the
730    environment [env] when [cost_incr] is the name of the cost update function
731    and [ind_set] is the set of loop indices whose scope we are in. *)
[1462]732
[1508]733and block_cost fun_name cost_incr ind_set env block
734    : require list * Cost_value.t =
735  let f (prev2, prev1, requires, cost) stmt =
[1462]736    let (added_requires, added_cost) =
[1508]737      stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt in
738    (prev1, Some stmt,
[1462]739     requires @ added_requires,
[1508]740     Cost_value.add cost added_cost) in
741  let (_, _, requires, cost) =
742    List.fold_left f (None,None,[],Cost_value.Int 0) block.Cil_types.bstmts in
[1462]743  (requires, cost)
744
[1508]745(** [loop_infos fun_name cost_incr ind_set env prev2 prev1 block] returns all
746    the extracted cost information of a loop in function [fun_name], in
747    environment [env], with [cost_incr] for the name of the cost update
748    function and [ind_set] for the loop indexes whose scope we are in, with
749    (optional) previous statements [prev2], [prev1] and of body [block]. The
[1462]750    returned information are: the requirements for the loop termination, the
[1508]751    loop counter, the loop index, its first value, the comparison relation of
752    the guard, the compared value in the guard, the increment and a function
753    that, provided a current value for the loop counter, returns the current
754    cost of the loop. *)
[1462]755
[1508]756and loop_infos fun_name cost_incr ind_set env prev2 prev1 block
757    : require list * string * string * Cost_value.t * Cost_value.relation *
[1462]758      Cost_value.t * Cost_value.t * (Cost_value.t -> Cost_value.t) =
[1508]759  let (counter, index, init_value) = extract_counter_and_init prev2 prev1 in
760  let ind_set = index :: ind_set in
[1462]761  let (rel, exit_value) = extract_guard counter block in
[1508]762  let increment = extract_increment counter index block in
[1462]763  check_supported_loop
764    fun_name env counter init_value exit_value increment block ;
[1508]765  let (requires, body_cost) = block_cost fun_name cost_incr ind_set env block in
766  let requires = (rel, init_value, exit_value, increment) :: requires in
767  let cost = mk_loop_cost init_value increment index body_cost in
768  (requires, counter, index, init_value, rel, exit_value, increment, cost)
[1462]769
[1508]770(** [loop_cost fun_name cost_incr ind_set env prev2 prev1 block] returns the
[1462]771    requirements and the cost of the loop of body [block] in the function
772    [fun_name] in the environment [env] when [cost_incr] is the name of the cost
[1508]773    update function, [ind_set] is the set of loop indexes whose scope we are in
774    and [prev2] and [prev1] are the (optional) previous statements. *)
[1462]775
[1508]776and loop_cost fun_name cost_incr ind_set env prev2 prev1 block
[1462]777    : require list * Cost_value.t =
[1508]778  let (requires, _, _,  init_value, rel, exit_value, increment, cost) =
779    loop_infos fun_name cost_incr ind_set env prev2 prev1 block in
[1462]780  let cost = cost (last_value rel init_value exit_value increment) in
781  let cost =
782    Cost_value.Cond (init_value, rel, exit_value, cost, Cost_value.Int 0) in
783  (requires, cost)
784
785
786(*** Costs computation ***)
787
788(* Once a cost (that may depend on the cost of the other functions) has been
789   associated to each function of a program, we want to simplify them in order
790   to have independent costs. To this end, we simply apply a fixpoint where at
791   each step, the independent cost of a function is replaced in the cost of
792   whatever function mentions it. For exampe, in the following configuration:
793     cost of f(x) <= x*x + 3
794     cost of g() <= cost of h()
795     cost of h(y) <= -1 + cost of f(y)
796   then a step of the fixpoint will lead to:
797     cost of f(x) <= x*x + 3
798     cost of g() <= cost of h()
799     cost of h(y) <= -1 + y*y + 3 *)
800
801(** [is_solved costs] returns true iff the system of inequations formed by the
802    costs [costs] is solved, i.e. if every cost is independent of the others and
803    does not mention to special cost value [Any]. *)
804
805let is_solved costs =
806  let f _ cost res =
807    res && (Cost_value.is_independent cost) &&
808      (not (Cost_value.has_any cost)) in
809  StringTools.Map.fold f costs true
810
811(** [solve_end costs1 costs2] returns true iff a fixpoint has been reached,
812    i.e. if the costs [costs2] of the current iteration are the same as the
813    costs [costs1] of the previous iteration. *)
814
815let solve_end costs1 costs2 =
816  let f fun_name cost res =
817    res && (StringTools.Map.mem fun_name costs1) &&
818      (cost = StringTools.Map.find fun_name costs1) in
819  StringTools.Map.fold f costs2 true
820
821(** [solve_costs extern_costs prototypes costs] solves the system of inequations
822    formed by the costs [costs]. It applies a reduction operation until a
823    fixpoint is reached. *)
824
825let rec solve_costs extern_costs prototypes costs =
826  let costs' = Cost_value.reduces extern_costs costs prototypes costs in
827  if solve_end costs costs' then
828    if is_solved costs' then costs'
829    else raise Unresolvable
830  else solve_costs extern_costs prototypes costs'
831
832class compute_costs cost_incr env costs prj = object
833  inherit Visitor.frama_c_copy prj as super
834
835  method vfunc fundec =
836    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
837    let block = fundec.Cil_types.sbody in
[1508]838    let cost = block_cost fun_name cost_incr [] env block in
[1462]839    costs := StringTools.Map.add fun_name cost !costs ;
840    Cil.SkipChildren
841
842end
843
844(** [compute_costs extern_costs cost_incr env] computes the cost associated to
845    each function of the current program in the current project. First, it
846    computes the costs potentially depending on that of the other functions, and
847    then it tries to solve the system of inequations that this produces. *)
848
849let compute_costs extern_costs cost_incr env
850    : (require list * Cost_value.t) StringTools.Map.t =
851  let costs : (require list * Cost_value.t) StringTools.Map.t ref =
852    ref StringTools.Map.empty  in
853  let compute_costs_prj =       
854    File.create_project_from_visitor
855      "cerco_compute_costs"
856      (new compute_costs cost_incr env costs) in
857  let f () =
858    let (requires, costs) = StringTools.Map.split_couple !costs in
859    let costs = solve_costs extern_costs (prototypes env) costs in
860    StringTools.Map.combine requires costs in
861  Project.on compute_costs_prj f ()
862
863
864(*** Add annotations ***)
865
[1508]866let add_tmp_cost_init env tmp_cost obj stmt =
[1462]867  let lval = Cil.var tmp_cost in
868  let e =
869    Cil.new_exp dummy_location
870      (Cil_types.Lval (Cil.var (get_cost_varinfo env))) in
871  let new_stmt =
872    Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
873  let new_stmt = Cil.mkStmt new_stmt in
[1508]874  obj#chop_index ;
[1462]875  Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))
876
[1508]877(* will transform requirements (rel, init_value, exit_value, increment) *)
878(* into (init_value rel exit_value) ⇒ (increment rel' 0) where rel' is  *)
879(* the strict version of rel. If this requirement is trivially satisfied *)
880(* it is suppressed *)
[1462]881let make_requires requires =
[1508]882  let f (rel, init_value, exit_value, increment) reqs =
[1462]883    let rel' = Cost_value.mk_strict rel in
[1508]884    match init_value, exit_value, increment with
885      | _, _, Cost_value.Int i
886        when Cost_value.bool_fun_of_relation rel' 0 i ->
887        reqs
888      | Cost_value.Int i, Cost_value.Int e, _
889        when not (Cost_value.bool_fun_of_relation rel i e) ->
890        reqs
891      | _ ->
892        let rel = Cost_value.cil_rel_of_rel rel in
893        let rel' = Cost_value.cil_rel_of_rel rel' in
894        let init_value = Cost_value.to_cil_term init_value in
895        let exit_value = Cost_value.to_cil_term exit_value in
896        let increment = Cost_value.to_cil_term increment in
897        let t1 = Logic_const.prel (rel, init_value, exit_value) in
898        let t2 = Logic_const.prel (rel', Cost_value.tinteger 0, increment) in
899        Logic_const.pimplies (t1, t2) :: reqs in
900  List.fold_right f requires []
[1462]901
902let add_spec pres post spec =
903  let requires = List.map Logic_const.new_predicate pres in
904  let post_cond = [(Cil_types.Normal, Logic_const.new_predicate post)] in
905  let new_behavior = Cil.mk_behavior ~requires ~post_cond () in
906  spec.Cil_types.spec_behavior <- new_behavior :: spec.Cil_types.spec_behavior
907
908let add_cost_annotation requires rel cost_id cost spec =
909  let post = mk_fun_cost_pred rel cost_id cost in 
910  add_spec (make_requires requires) post spec ;
911  Cil.ChangeDoChildrenPost (spec, identity)
912
913let add_cost_incr_annotation cost_id spec =
914  let rel = Cil_types.Req in
915  let cost = Cost_value.Var "incr" in
916  add_cost_annotation [] rel cost_id cost spec
917
918let add_regular_fun_annotation fun_name cost_id costs spec =
919  let rel = Cil_types.Rle in
920  let (requires, cost) = StringTools.Map.find fun_name costs in
921  add_cost_annotation requires rel cost_id cost spec
922
923let add_fundec_annotation cost_id cost_incr costs fun_name spec =
924  if fun_name = cost_incr then add_cost_incr_annotation cost_id spec
925  else add_regular_fun_annotation fun_name cost_id costs spec
926
927let mk_loop_invariant_counter_init_value
928    extern_costs costs prots counter init_value increment =
929  let mk_value value =
930    let incr_mod = Cost_value.abs increment in
931    let v = Cost_value.BinOp (Cost_value.Mod, value, incr_mod) in
932    Cost_value.to_cil_term (Cost_value.reduce extern_costs costs prots v) in
933  let v1 = mk_value (Cost_value.Var counter) in
934  let v2 = mk_value init_value in
935  let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
936  mk_invariant invariant
937
938let mk_loop_invariant_counter_last_value
939    extern_costs costs prots counter rel init_value exit_value increment =
940  let last_value = last_value rel init_value exit_value increment in
941  let last_value = Cost_value.reduce extern_costs costs prots last_value in
942  let last_value = Cost_value.to_cil_term last_value in
943  let rel' = Cost_value.cil_rel_of_rel rel in
944  let init_value = Cost_value.to_cil_term init_value in
945  let exit_value = Cost_value.to_cil_term exit_value in
946  let require = Logic_const.prel (rel', init_value, exit_value) in
947  let rel' = Cost_value.cil_rel_of_rel (Cost_value.mk_large rel) in
948  let counter = Cost_value.to_cil_term (Cost_value.Var counter) in
949  let prop = Logic_const.prel (rel', counter, last_value) in
950  let invariant = Logic_const.pimplies (require, prop) in
951  mk_invariant invariant
952
953let mk_loop_invariant_counter_no_change counter rel init_value exit_value =
954  let rel = Cost_value.opposite rel in
955  let rel' = Cost_value.cil_rel_of_rel rel in
956  let init_value = Cost_value.to_cil_term init_value in
957  let exit_value = Cost_value.to_cil_term exit_value in
958  let require = Logic_const.prel (rel', init_value, exit_value) in
959  let counter = Cost_value.to_cil_term (Cost_value.Var counter) in
960  let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in
961  let invariant = Logic_const.pimplies (require, prop) in
962  mk_invariant invariant
963
964let mk_loop_invariant_cost
965    extern_costs tmp_cost costs prots cost_id counter cost =
966  let loop_cost = cost (Cost_value.Var counter) in
967  let loop_cost = Cost_value.reduce extern_costs costs prots loop_cost in
968  let loop_cost = Cost_value.to_cil_term loop_cost in
969  let cost_var =
970    Logic_const.tvar (Cil_const.make_logic_var cost_id Cil_types.Linteger) in
971  let tmp_cost = Cost_value.to_cil_term (Cost_value.Var tmp_cost) in
972  let new_cost = Cil_types.TBinOp (Cil_types.PlusA, tmp_cost, loop_cost) in
973  let new_cost = integer_term new_cost in
974  let invariant = Logic_const.prel (Cil_types.Rle, cost_var, new_cost) in
975  mk_invariant invariant
976
977let mk_loop_variant
978    extern_costs costs prots counter init_value rel exit_value increment =
979  let last_value = last_value rel init_value exit_value increment in
980  let counter_var = Cost_value.Var counter in
981  let (v1, v2) = match rel with
982    | Cost_value.Lt | Cost_value.Le -> (last_value, counter_var)
983    | Cost_value.Gt | Cost_value.Ge -> (counter_var, last_value) in
984  let variant = Cost_value.BinOp (Cost_value.Sub, v1, v2) in
985  let variant = Cost_value.reduce extern_costs costs prots variant in
986  mk_variant (Cost_value.to_cil_term variant)
987
988let annot_loop
989    extern_costs tmp_cost cost_id cost_incr env costs obj stmt
[1508]990    prev2 prev1 block =
[1462]991  let (_, costs) = StringTools.Map.split_couple costs in
992  let prots = prototypes env in
993  let fun_name = current_fun_name obj in
[1508]994  let (_, counter, index, init_value, rel, exit_value, increment, cost) =
995    loop_infos fun_name cost_incr obj#get_ind_set env prev2 prev1 block in
[1462]996  let invariant_counter_init_value =
997    mk_loop_invariant_counter_init_value
998      extern_costs costs prots counter init_value increment in
999  let invariant_counter_last_value =
1000    mk_loop_invariant_counter_last_value
1001      extern_costs costs prots counter rel init_value exit_value increment in
1002  let invariant_counter_no_change =
1003    mk_loop_invariant_counter_no_change counter rel init_value exit_value in
1004  let invariant_cost =
[1689]1005     mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id
[1462]1006      counter cost in
1007  let variant =
1008    mk_loop_variant extern_costs costs prots counter init_value rel exit_value
1009      increment in
[1508]1010  obj#push_index index;
[1462]1011  add_loop_annot obj stmt invariant_counter_init_value ;
1012  add_loop_annot obj stmt invariant_counter_last_value ;
1013  add_loop_annot obj stmt invariant_counter_no_change ;
1014  add_loop_annot obj stmt invariant_cost ;
1015  add_loop_annot obj stmt variant
1016
1017class add_annotations extern_costs cost_id cost_incr env costs prj =
1018object (self) inherit Visitor.frama_c_copy prj as super
1019
1020  val mutable tmp_costs : Cil_types.varinfo list = []
[1508]1021  val mutable prev2 = None
1022  val mutable prev1 = None
1023  val mutable ind_set : string list = []
[1462]1024
[1508]1025  method get_ind_set = ind_set
1026  method push_index index = ind_set <- index :: ind_set
1027  method chop_index = ind_set <- List.tl ind_set
1028
[1462]1029  method vstmt_aux stmt =
[1508]1030    let snd_last_stmt = prev2 in
1031    let last_stmt = prev1 in
1032    prev2 <- last_stmt ;
1033    prev1 <- Some stmt ;
[1462]1034    match stmt.Cil_types.skind with
1035      | Cil_types.Loop (_, block, _, _, _) ->
1036        assert (List.length tmp_costs > 0) ;
1037        let tmp_cost = List.hd tmp_costs in
1038        tmp_costs <- List.tl tmp_costs ;
1039        let tmp_cost_id = tmp_cost.Cil_types.vname in
1040        annot_loop
1041          extern_costs tmp_cost_id cost_id cost_incr env costs self stmt
[1508]1042          snd_last_stmt last_stmt block ;
1043        Cil.ChangeDoChildrenPost (stmt, add_tmp_cost_init env tmp_cost self)
[1462]1044      | _ -> Cil.DoChildren
1045
1046  method vspec spec = match self#current_kf with
1047    | None -> Cil.JustCopy 
1048    | Some kf ->
1049      match kf.Db_types.fundec with
1050        | Db_types.Definition (fundec, _) ->
1051          let fun_name = fundec.Cil_types.svar.Cil_types.vname in
1052          add_fundec_annotation cost_id cost_incr costs fun_name spec
1053        | Db_types.Declaration (_, f, _, _) when
1054            StringTools.Map.mem f.Cil_types.vname extern_costs ->
1055          let cost = StringTools.Map.find f.Cil_types.vname extern_costs in
1056          let cost = Cost_value.Var cost in
1057          add_cost_annotation [] Cil_types.Rle cost_id cost spec
1058        | _ -> Cil.JustCopy
1059
1060  method vfunc fundec =
1061    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
1062    tmp_costs <- make_freshes fundec (get_nb_loops env fun_name) cost_id ;
[1508]1063    prev2 <- None ;
1064    prev1 <- None ;
[1462]1065    Cil.DoChildren
1066
1067end
1068
1069let add_annotations extern_costs fname cost_id cost_incr env costs =
[1508]1070  let add_annotations_prj =
1071    let visitor =
1072      new add_annotations extern_costs cost_id cost_incr env costs in
1073    File.create_project_from_visitor "cerco_add_annotations"
1074      (visitor :> Project.t -> Visitor.frama_c_visitor) in
[1462]1075  let f () =
1076    Parameters.CodeOutput.set fname ;
1077    File.pretty_ast () in
1078  Project.on add_annotations_prj f ()
1079
1080
1081(*** Saving cost results ***)
1082
1083let save_results fname costs =
1084  let f fun_name (_, cost) res =
1085    res ^ fun_name ^ " " ^ (Cost_value.to_string cost) ^ "\n" in
1086  let s = StringTools.Map.fold f costs "" in
1087  let save_file =
1088    try Filename.chop_extension fname
1089    with Invalid_argument "Filename.chop_extension" -> fname in
1090  let save_file = save_file ^ ".cost_results" in
1091  try
1092    let oc = open_out save_file in
1093    output_string oc s ;
1094    close_out oc
1095  with Sys_error _ ->
1096    Printf.eprintf "Could not save plug-in results in file %s\n%!" save_file
1097
1098
1099(*** Main ***)
1100
1101let cost ((fname, _), f_old_name, cost_id, cost_incr, extern_costs) =
1102  try
1103    Parameters.Files.set [fname] ;
1104    File.init_from_cmdline () ;
1105    let env = initializations cost_id in
1106    let costs = compute_costs extern_costs cost_incr env in
1107    save_results f_old_name costs ;
1108    add_annotations extern_costs fname cost_id cost_incr env costs
1109  with e -> Printf.eprintf "** ERROR: %s\n%!" (string_of_exception cost_incr e)
Note: See TracBrowser for help on using the repository browser.