5 module Varinfo = Cil_datatype.Varinfo
6 module Logic_var = Cil_datatype.Logic_var
7 module Stmt = Cil_datatype.Stmt
8 module Term = Cil_datatype.Term
9 module Logic_label = Cil_datatype.Logic_label
11 (** This module defines the main analysis of the plug-in. Its actions are:
12 - build the CFG of the program;
13 - compute the cost of each function depending on the costs of the others
14 at the same time add the needed invariant and at the cost of each function
22 let string_of_list sep f l =
23 let rec aux = function
26 | e :: l -> (f e) ^ sep ^ (aux l) in
29 let integer_term term = Logic_const.term term Linteger
32 let cint64 = CInt64 (My_bigint.of_int i, IInt, None) in
33 let iterm = TConst cint64 in
36 let cil_logic_int_var x =
37 Logic_const.tvar (Cil_const.make_logic_var x Linteger)
39 let current_kf obj = match obj#current_kf with
40 | None -> raise (Failure "Compute.current_kf")
43 let add_loop_annot obj stmt annot =
44 let annot = User annot in
46 Cil.get_original_kernel_function (Cil.copy_visit ()) (current_kf obj) in
47 Queue.add (fun () -> Annotations.add kf stmt [Ast.self] annot)
48 obj#get_filling_actions
50 let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots
52 let mk_invariant pred =
53 Logic_const.new_code_annotation (AInvariant ([], true, pred))
56 Logic_const.new_code_annotation (AVariant (term, None))
58 let mk_fun_cost_pred rel cost_id cost =
59 let cost_var = Cil_const.make_logic_var cost_id Linteger in
60 let cost_var = Logic_const.tvar cost_var in
61 let old_cost = Logic_const.told cost_var in
62 let new_cost = TBinOp (PlusA, old_cost, cost) in
63 let new_cost = integer_term new_cost in
64 Logic_const.prel (rel, cost_var, new_cost)
66 let rec exp_is_var name e = match (remove_casts e).enode with
67 | Lval (Var v, _) -> v.vname = name
68 | Info (e, _) -> exp_is_var name e
71 let has_fun_type varinfo = match varinfo.vtype with
75 let formals_of_varinfo varinfo = match varinfo.vtype with
76 | TFun (_, args, _, _) ->
77 List.map (fun (x, t, _) -> Cil.makeVarinfo false true x t)
79 | _ -> assert false (* do not use on these arguments *)
81 let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
83 let dummy_varinfo = Cil.makeVarinfo false false "" (TVoid [])
86 let rec aux acc i = if i >= n then acc else aux (a :: acc) (i+1) in
89 let rec stmt_subs stmt =
90 let added = match stmt.skind with
91 | If (_, block1, block2, _)
92 | TryFinally (block1, block2, _)
93 | TryExcept (block1, _, block2, _) ->
94 (block_subs block1) @ (block_subs block2)
95 | Switch (_, block, _, _)
96 | Loop (_, block, _, _, _)
97 | Block block -> block_subs block
98 | UnspecifiedSequence l ->
99 List.map (fun (stmt, _, _, _, _) -> stmt) l
103 and block_subs block = List.flatten (List.map stmt_subs block.bstmts)
105 let rec first_stmt block = match block.bstmts with
107 | stmt :: _ -> match stmt.skind with
108 | Block block -> first_stmt block
111 let stmt_is_break stmt = match stmt.skind with
115 let starts_with_break block = match first_stmt block with
117 (match stmt.skind with
118 | Goto (stmt_ref, _) -> stmt_is_break !stmt_ref
119 | _ -> stmt_is_break stmt)
122 let rec last = function
127 let rec last_stmt block = match last block.bstmts with
129 | Some stmt -> match stmt.skind with
130 | Block block -> last_stmt block
133 class print_CFG = object inherit Visitor.frama_c_inplace as super
136 Format.printf "*** %s ***\n\n%!" func.svar.vname ;
139 Format.printf "%d: %a\n--> %!" stmt.sid Cil.d_stmt stmt ;
140 List.iter (fun stmt -> Format.printf "%d %!" stmt.sid)
142 Format.printf "\n\n%!")
144 Format.printf "\n\n%!" ;
150 Visitor.visitFramacFile (new print_CFG) (Ast.get ())
154 class make_CFG = object inherit Visitor.frama_c_inplace as super
157 Cfg.clearFileCFG ~clear_id:false file ;
158 Cfg.computeFileCFG file ;
164 Visitor.visitFramacFile (new make_CFG) (Ast.get ())
166 (** Extract variant *)
168 let rec extract_added_value counter e = match e.enode with
169 | BinOp (PlusA, e1, e2, _) when exp_is_var counter e1 ->
171 | BinOp (MinusA, e1, e2, typ)
172 when exp_is_var counter e1 ->
173 let enode = UnOp (Neg, e2, typ) in
174 let e2 = { e2 with enode = enode } in
176 | CastE (_, e) -> extract_added_value counter e
180 "Could not find added increment value for counter %s in %a.\n%!"
181 counter Cil.d_exp e ;
184 let extract_increment block =
185 let open Misc.Option in
187 (fun stmt -> match stmt.skind with
188 | Instr (Set ((Var v, _), e, _)) ->
189 extract_added_value v.vname e
193 "Could not find increment instruction; found %a instead.\n%!"
197 let gen_variant counter rel guard increment =
198 let counter = term_of_exp counter in
199 let guard = term_of_exp guard in
200 let increment = term_of_exp increment in
201 let guard = match rel with
202 | Lt | Gt | Ne -> guard
203 | Le | Ge | Eq -> make_binop PlusA (Cil.lconstant My_bigint.one) guard
204 | _ -> assert false (* not implemented TODO be gentle *) in
205 let variant = make_binop MinusA guard counter in
207 if no_division_in_generated_variant
208 then make_binop Mult variant (make_sign increment)
209 else make_binop Div variant increment in
210 simplify_term variant
212 let opposite = function
219 | _ -> assert false (* not implemented TODO be gentle *)
222 let extract_guard block (counter, increment) =
223 let open Misc.Option in
225 (fun stmt -> match stmt.skind with
226 | If (e, _, block, _) when starts_with_break block ->
228 | BinOp (rel, e1, e2, _)
229 when exp_is_var counter e1 (* && Domain.is_supported_rel rel *) ->
230 (*Some (counter, rel, e2, increment)*)
231 Some (gen_variant e1 rel e2 increment)
232 | BinOp (rel, e1, e2, _)
233 when exp_is_var counter e2 (* && Domain.is_supported_rel rel *) ->
234 (* let rel = rel in *)
235 (* let rel = Domain.opposite rel in *)
236 (* Some (counter, rel, e1, increment) *)
237 let rel = opposite rel in
238 Some (gen_variant e2 rel e1 increment)
241 Format.printf "Unsupported guard condition %a on counter %s.\n%!"
242 Cil.d_exp e counter ;
244 | If (_, _, block, _) ->
246 Format.printf "Loop not guarded by a break:\n%a\n%!" Cil.d_block block ;
249 if !debug then Format.printf "Loop not guarded:\n%a\n%!" Cil.d_stmt stmt ;
252 let extract_variant body =
253 let open Misc.Option in
254 extract_increment body >>= extract_guard body
256 let rec find_variant = function
258 | {annot_content = AVariant (t,_)}::_ -> Some t
259 | _::l -> find_variant l
262 (** Function computing cost of special instruction *)
265 { env_fun_cost : term Varinfo.Hashtbl.t;
266 env_cost_incr_name : string; (* TODO put the varinfo *)
267 env_cost_var : logic_var;
268 mutable env_loop_name : unit -> string;
271 let init_loop_name env file =
275 Format.sprintf "__cost_%s_loop_%i" file !i in
276 env.env_loop_name <- f
278 let dumb_env_loop_name () : string = assert false
280 let linteger t = Logic_const.term t Linteger
282 (** Create a function which compute the cost of a loop.
283 It uses the variant as the strictly decreasing positive argument.
284 The cost depend of the other arguments \vec x.
286 \bcost if the cost of the body of the loop (must be always positive!)
287 \phi compute the modification of \vec x by one turn of the loop
291 else (f(v-1,\phi(\vec x)) + \bcost(\vec x))
293 It also create some needed lemmas:
294 - f is always positive
296 or simplifying lemmas:
297 - simpler (eg. algebraic) formulation of f:
298 * \vec x = \empty, \phi = identity, \bcost = c >= 0
301 f(v,\vec x) = \bcost(\vec x) * (v + 1)
302 * \phi(\vec x) = x_1 + 1,x_2,...,x_n
303 \bcost(\vec x) = max(c x_1,0) + \phi(x_2,...,x_n)
304 \phi(x_2,...,x_n) >= 0, c >= 0
305 f(v,\vec x) = \phi(x_2,...,x_n) (v + 1)
306 + c * [y(y+1) - (max(y-v-1,0)(y-v)]/2
308 let create_fun_loop env dep bcost =
309 let v = Cil_const.make_logic_var "v" Linteger in
310 let tv = Logic_const.tvar v in
311 let xargs = List.map fst dep in (** \vec x *)
312 let mod_dep = List.map snd dep in (** \phi *)
313 let args = v::xargs in
314 let targs = List.map Logic_const.tvar args in
316 let signature = Larrow (List.map (fun _ -> Linteger) args, Linteger) in
317 let new_loop_name = env.env_loop_name () in
318 let li = { l_var_info = Cil_const.make_logic_var new_loop_name signature;
321 l_type = Some Linteger;
323 l_body = LBnone (* temporary *) } in
324 let lzero = Cil.lzero () in
326 linteger (TBinOp(MinusA, tv, Cil.lconstant (My_bigint.one))) in
327 (* let body = linteger (Tapp(li,[],tvminusone::mod_dep)) in *)
328 let body = linteger (tapp li (tvminusone::mod_dep)) in
329 let body = linteger (TBinOp(PlusA, body, bcost)) in
331 Tif(linteger (TBinOp(Lt, tv, lzero)), lzero, body) in
332 li.l_body <- LBterm (linteger body);
333 (** Axiom positive *)
334 let lemma = Logic_const.unamed
337 (Prel (Rge, linteger (Tapp(li, [], targs)), lzero)))) in
338 let lemma = Dlemma (new_loop_name ^ "_is_positive", false, [], [], lemma,
339 Cil_datatype.Location.unknown) in
340 (** Register them as global (in reverse order) *)
341 Globals.Annotations.add_generated lemma;
342 Globals.Annotations.add_generated
343 (Dfun_or_pred (li, Cil_datatype.Location.unknown));
346 (** TODO: extend it to some more interesting cases *)
347 let cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body =
348 (** The number of iteration is bounded by the variant + 1, because
349 the variant must be positive at the *start* of an iteration *)
350 let variant = make_binop PlusA variant (Cil.lconstant (My_bigint.one)) in
351 (** Simple version, just do the multiplication *)
352 let nbr_iteration = make_at lab_before_loop variant in
353 (** the nbr_iteration must be positive *)
354 let nbr_iteration = make_max nbr_iteration (Cil.lzero ()) in
355 let sum = make_binop Mult nbr_iteration cost_body in
357 (** make the cost invariant of the loop *)
358 let remaining_nbr_iteration = make_max variant (Cil.lzero ()) in
359 (** ensures cost <= \old(cost) +
360 ([nbr_iteration]-[remaining_nbr_iteration]) * [cost_body] *)
361 let cost_var = Logic_const.tvar env.env_cost_var in
362 let old_cost = make_at lab_before_loop cost_var in
363 let cost_iterations =
365 (make_binop MinusA nbr_iteration remaining_nbr_iteration)
367 let new_cost = make_binop PlusA old_cost cost_iterations in
368 let new_cost = simplify_term new_cost in
369 let invariant = Logic_const.prel (Rle, cost_var, new_cost) in
371 Logic_const.new_code_annotation
372 (AInvariant ([time_cost_behavior],true,invariant)) in
373 Annotations.add kern_fun stmt [Ast.self] (User annot);
376 let cost_loop_term_complexe
377 env kern_fun stmt lab_before_loop variant deps cost_body =
378 (** the nbr_iteration must be positive *)
379 let variant = make_max variant (Cil.lzero ()) in
380 let args = List.map fst deps in (** \phi *)
381 let targs = List.map Logic_const.tvar args in
382 let fl = create_fun_loop env deps cost_body in
383 let app = linteger (tapp fl (variant::targs)) in
384 let sum = make_at lab_before_loop app in
386 (** make the cost invariant of the loop *)
387 (** ensures cost <= \old(cost) +
388 ([nbr_iteration]-[remaining_nbr_iteration]) * [cost_body] *)
389 let cost_var = Logic_const.tvar env.env_cost_var in
390 let old_cost = make_at lab_before_loop cost_var in
391 let cost_iterations = make_binop MinusA sum app in
392 let new_cost = make_binop PlusA old_cost cost_iterations in
393 let new_cost = simplify_term new_cost in
394 let invariant = Logic_const.prel (Rle, cost_var, new_cost) in
396 Logic_const.new_code_annotation
397 (AInvariant ([time_cost_behavior],true,invariant)) in
398 Annotations.add kern_fun stmt [Ast.self] (User annot);
401 let cost_loop_term env kern_fun stmt lab_before_loop variant deps cost_body =
403 let const_during_loop = List.for_all (fun (_,_) -> (** TODO *) false) deps in
405 then cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body
406 else cost_loop_term_complexe
407 env kern_fun stmt lab_before_loop variant deps cost_body
409 let cost_body = simplify_term cost_body in
410 match cost_body.term_node with
412 cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body
414 cost_loop_term_complexe
415 env kern_fun stmt lab_before_loop variant deps cost_body
418 (** computing cost of fundec which contain a call to funvar *)
419 let cost_of_fun_call env funvar args =
420 (** can't fail since we use the callgraph *)
421 let cost = Varinfo.Hashtbl.find env.env_fun_cost funvar in
422 (* match cost.term_node with *)
423 (* | TConst (CInt64 (_,_,_)) -> cost *)
425 (** arguments of the function *)
426 let formals = Cil.getFormalsDecl funvar in
427 (* (** The real arguments are binded using a let and the formal argument are
428 replaced by fresh variable *)
429 let letvars = List.map
430 (fun vi -> Cil.make_temp_logic_var (Ctype vi.vtype))
432 let subst = List.fold_left2 (fun map vi v ->
433 Varinfo.Map.add vi v map) Varinfo.Map.empty formals letvars in
435 Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
437 let cost = List.fold_left2 (fun tlet v arg ->
438 let logic_info = { l_var_info = v; l_type = None; l_tparams = [];
439 l_labels = []; l_profile = [];
440 l_body = LBnone; } in
441 let arg = term_of_exp arg in
443 Logic_const.term (Tlet (logic_info, arg))
446 cost letvars args in*)
447 let subst = List.fold_left2 (fun map vi arg ->
449 Varinfo.Map.add vi (term_of_exp arg) map
450 with Untranslatable_expr _ -> map (** TODO verify that this formal doesn't
451 appear in the cost of the function *)
452 ) Varinfo.Map.empty formals args in
453 let cost = remove_logic_label Logic_const.pre_label cost in
455 Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
459 (** Compute the "wp" of a stmt, in fact just make some substitution *)
460 let stmt_wp stmt term =
461 (** try to propagate \at(i,Label) *)
462 match stmt.skind with
463 | Instr (Set ((Var vi,_),e,_)) ->
466 let t = term_of_exp e in
467 let subst = Varinfo.Map.singleton vi t in
469 Visitor.visitFramacTerm
470 (new subst_with_label stmt subst (Project.current ()))
474 if !debug then Format.eprintf "can't convert exp %a to term: %a.@."
475 Cil.defaultCilPrinter#pExp e print_exception exn;
480 let rec stmts_wp bad_stmts stop_stmts stmt term =
482 Format.printf "stmts_wp sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
484 Stmt.Set.pretty bad_stmts
485 Stmt.Set.pretty stop_stmts;
486 (** statement in last statement *)
487 if Stmt.Set.mem stmt stop_stmts
489 else if Stmt.Set.mem stmt bad_stmts
493 let succs_bad_stmts =
494 match stmt.skind with
495 | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
497 (** Cost of the successors of the instruction *)
499 stmts_wp_succs succs_bad_stmts stop_stmts stmt.succs term in
500 match cost_succs with
501 | [] -> None (** can't go in a good state so count nothing *)
502 | (a::l) -> (** TODO take care of conditions *)
504 let a' = stmt_wp stmt a in
506 Format.printf "[WP]stmt:@,%a@.a:@,%a@.a':@,%a@."
507 Cil.defaultCilPrinter#pStmt stmt
508 Cil.defaultCilPrinter#pTerm a
509 Cil.defaultCilPrinter#pTerm a';
512 and stmts_wp_succs bad_stmts stop_stmts stmts term =
514 match stmts_wp bad_stmts stop_stmts stmt term with
516 | Some t -> t::acc in
517 List.fold_left fold [] stmts
520 (** We go through the cfg we assume that:
521 - all functions called have a cost already computed
522 - no implicit loop (goto), all are explicit Loop
523 - all loops have an invariant (given by the user or previously computed for
526 We iterate on the cfg except when arriving on a loop where we compute the
527 body alone and after that go to the next statements (the break statement)
529 break_statement in which statement to stop the sum (for loop)
533 let rec find_variant = function
535 | {annot_content = AVariant (t,_)}::_ -> Some t
536 | _::l -> find_variant l
538 (** TODO: cache the statement already done after if-then-else
539 (otherwise exponential) *)
540 (** return None if no path arrive to a good_statement or don't go through
542 let rec cfg_sum env kern_fun bad_stmts stop_stmts stmt =
544 Format.printf "sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
546 Stmt.Set.pretty bad_stmts
547 Stmt.Set.pretty stop_stmts;
548 (** statement in last statement *)
549 if Stmt.Set.mem stmt stop_stmts
550 then Some (Cil.lzero ())
551 else if Stmt.Set.mem stmt bad_stmts
555 let succs_bad_stmts =
556 match stmt.skind with
557 | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
559 (** Cost of the successors of the instruction *)
561 cfg_sum_succs env kern_fun succs_bad_stmts stop_stmts
563 match cost_succs with
564 | None -> None (** can't go in a good state so count nothing *)
566 (** Cost of the instruction *)
568 match stmt.skind with
569 (* (\** call to cost_incr *\) *) (** cost_incr is an usual function *)
573 (* Lval (Var var, _)} , *)
575 (* when var.vname = env.env_cost_incr_name -> *)
576 (* term_of_cost_expr cost *)
582 cost_of_fun_call env var args
584 | Loop (_,body,_,_,_) ->
585 cost_loop env kern_fun bad_stmts stop_stmts stmt body
586 | _ -> Cil.lzero () in
587 (** normalize the cost of the instruction regarding the labels *)
588 let labels = NormAtLabels.labels_stmt_pre stmt in
589 let cost_instr = NormAtLabels.preproc_annot_term labels cost_instr in
590 let cost_succs = stmt_wp stmt cost_succs in
591 let sum = make_binop PlusA cost_instr cost_succs in
592 (** remove the at that point to this statement we don't know the value at
593 this point perhaps we will know before ( use Here?? ) *)
595 Visitor.visitFramacTerm
596 (new remove_stmt_label stmt (Project.current ()))
599 Format.printf "Stmt %i sum=%a@."
600 stmt.sid Term.pretty sum;
603 and cfg_sum_succs env kern_fun bad_stmts stop_stmts stmts =
605 let cost_succ = cfg_sum env kern_fun bad_stmts stop_stmts stmt in
606 make_max_opt cost cost_succ in
607 List.fold_left fold None stmts
609 and cost_loop env kern_fun bad_stmts stop_stmts stmt body =
610 (** the first one perhaps not needed *)
611 let bad_stmts = Stmt.Set.union bad_stmts stop_stmts in
612 let stop_stmts = Stmt.Set.singleton stmt in
614 cfg_sum_succs env kern_fun bad_stmts stop_stmts stmt.succs in
615 let cost_body = match cost_body with
616 | None -> (* no cycle in fact *) Cil.lzero ()
617 | Some cost -> simplify_term cost in
618 (** compute free variable and compute their modification by the loop body *)
619 let deps = freevar Logic_var.Set.empty cost_body in
623 stmts_wp_succs bad_stmts stop_stmts stmt.succs (Logic_const.tvar e) in
625 | [] -> assert false (** No cycle? impossible it find one before *)
627 assert (l = []); (* TODO *)
629 Logic_var.Set.fold fold deps [] in
630 (** this stmt is the continue *)
631 let annots = Annotations.get_filter Logic_utils.is_variant stmt in
632 let variant = match annots with
633 | [] -> (** TODO put it somewhere else *)
634 begin match extract_variant body with
637 "Can't@ compute@ cost@ without@ variant@ for@ statement:@,%a@."
638 Stmt.pretty stmt; exit 1
641 Logic_const.new_code_annotation (AVariant (variant,None)) in
642 Annotations.add kern_fun stmt [Ast.self] (User annot);
644 | ( User { annot_content =
646 | AI (_, { annot_content =
647 AVariant (v,_) }) (** usefule case ? *)
650 let v = NormAtLabels.preproc_annot_term
651 (NormAtLabels.labels_loop_inv stmt) v in
652 let v = remove_logic_label Logic_const.here_label v in
654 | _ -> assert false (* result of the filter *)
656 if stmt.labels = [] then
657 stmt.labels <- (** ugly but... *)
658 Label("__stmt_"^(string_of_int stmt.sid),Cil.builtinLoc,false)::
660 let label_before_loop = StmtLabel (ref stmt) in
661 cost_loop_term env kern_fun stmt label_before_loop variant deps cost_body
663 let make_leq_cost env sum =
664 (** ensures cost <= \old(cost) + [sum] *)
665 let cost_var = Logic_const.tvar env.env_cost_var in
666 let old_cost = Logic_const.told cost_var in
667 let new_cost = Logic_const.term
668 (Cil_types.TBinOp (Cil_types.PlusA, old_cost, sum)) Linteger in
669 let post = Logic_const.prel (Rle, cost_var, new_cost) in
670 let post = Logic_const.new_predicate post in
673 let fun_sum env vi kernel_fun =
674 let fst_stmt = Kernel_function.find_first_stmt kernel_fun in
675 let last_stmt = Kernel_function.find_return kernel_fun in
676 let bad_stmts = Stmt.Set.empty in
677 let stop_stmts = Stmt.Set.singleton last_stmt in
678 let sum = cfg_sum env kernel_fun bad_stmts stop_stmts fst_stmt in
679 let sum = match sum with
680 | None -> assert false (* Oups return not achievable?? *)
683 let sum = simplify_term sum in
684 let sum = Logic_const.told sum in (** add old and push it *)
685 let labels = NormAtLabels.labels_fct_post in
686 let sum = NormAtLabels.preproc_annot_term labels sum in
689 Format.printf "@[<hov 3>sum of %a: %a@]@."
690 Cil.defaultCilPrinter#pVar vi
691 Cil.defaultCilPrinter#pTerm sum;
692 (** add postcondition about cost *)
693 let mod_funspec funspec =
694 let post = make_leq_cost env sum in
696 Cil.mk_behavior ~name:time_cost_behavior ~post_cond:[Normal, post] () in
697 {funspec with spec_behavior = behavior::funspec.spec_behavior;}
699 Kernel_function.set_spec kernel_fun mod_funspec;
702 (** Before computing the sum check that the user doesn't specify the cost.
703 In this case use it *)
705 init_loop_name env "fun_sum";
706 let kernel_fun = Globals.Functions.get vi in
707 let funspec = Kernel_function.get_spec kernel_fun in
708 let rec find_cost = function
712 b_assumes = []; (** TODO? allow more general contract? *)
713 (** ensores __cost <= \old(__cost) + t; *)
714 b_post_cond = [_,{ip_content=Prel
716 {term_node = (TLval(TVar cost_var,TNoOffset))},
717 {term_node = TBinOp(PlusA,{term_node = Tat(
718 {term_node = (TLval(TVar cost_var2,TNoOffset))}, old_label)},
720 }::_ when name = time_cost_behavior &&
721 Logic_var.equal cost_var env.env_cost_var &&
722 Logic_var.equal cost_var2 env.env_cost_var &&
723 Logic_label.equal old_label Logic_const.old_label
725 | _::l -> find_cost l in
726 match find_cost funspec.spec_behavior with
727 | None -> fun_sum env vi kernel_fun
730 Format.printf "@[<hov 3>User sum of %a: %a@]@."
731 Cil.defaultCilPrinter#pVar vi
732 Cil.defaultCilPrinter#pTerm sum;
733 let labels = NormAtLabels.labels_fct_post in
734 let sum = NormAtLabels.preproc_annot_term labels sum in
737 let initialize _tmp_prefix _fname cost_var cost_incr _extern_costs =
738 (** TODO? use extern_costs for initializing env_fun_cost ? *)
739 let callgraph = Callgraph.computeGraph (Ast.get ()) in
741 Printf.printf "callgraph size: %a\n%!" Callgraph.printGraph callgraph;
742 let env = { env_fun_cost = Varinfo.Hashtbl.create 10;
743 env_cost_incr_name = cost_incr;
744 env_cost_var = cost_var;
745 env_loop_name = dumb_env_loop_name} in
746 let rec iter : 'a. 'a -> Callgraph.callnode -> unit = fun _ callnode ->
747 match callnode.Callgraph.cnInfo with
748 | Callgraph.NIVar (vi,{contents = true }) ->
749 if not (Varinfo.Hashtbl.mem env.env_fun_cost vi) then begin
750 Inthash.iter iter callnode.Callgraph.cnCallees;
751 let sum = fun_sum env vi in
752 Varinfo.Hashtbl.add env.env_fun_cost vi sum
754 | _ -> () (** put an undefined constant here for top *)
756 (** add the cost of cost_incr *)
757 let cost_incr = Hashtbl.find callgraph cost_incr in
758 let cost_incr = match cost_incr.Callgraph.cnInfo with
759 | Callgraph.NIVar (vi,_) -> vi
760 | _ -> assert false (* cost_incr must be at least declared *) in
761 let arg_cost_incr = List.hd (Cil.getFormalsDecl cost_incr) in
762 let sum_cost_incr = Logic_const.tvar (Cil.cvar_to_lvar arg_cost_incr) in
763 let post_cost_incr = make_leq_cost env sum_cost_incr in
764 Kernel_function.set_spec (Globals.Functions.get cost_incr) (fun funspec ->
766 Writes [Logic_const.(new_identified_term (tvar cost_var)), FromAny] in
768 Cil.mk_behavior ~name:time_cost_behavior
769 ~post_cond:[Normal, post_cost_incr]
771 {funspec with spec_behavior = behavior::funspec.spec_behavior;} );
772 Varinfo.Hashtbl.add env.env_fun_cost cost_incr sum_cost_incr;
773 (** make the other functions *)
774 Hashtbl.iter iter callgraph
779 let cost ((fname, _), _, cost_time, _) =
781 if !debug then Printf.printf "Initialize Cost\n%!" ;
783 Cil.cvar_to_lvar (Globals.Vars.find_from_astinfo
784 cost_time.Cerco.cost_id VGlobal) in
785 initialize "__tmp" fname cost_var
786 cost_time.Cerco.cost_incr cost_time.Cerco.extern_costs;
787 with e -> Format.eprintf "** ERROR: %a.@." print_exception_raise e