2 (* TODO: transform precondition into assertions, transform added code into ghost
5 (** This module defines the main analysis of the plug-in. Its actions are:
6 - build the CFG of the program;
7 - initialize the static environment of analysis (parameters of the
8 functions, number of loops, etc);
9 - compute the cost of each function depending on the costs of the others;
10 - try to solve the inequations formed from the previous step so as to obtain
11 an independent cost for each function;
13 - add the annotations on the program. *)
18 exception ASM_unsupported
19 exception Try_unsupported
21 let string_of_exception = function
22 | ASM_unsupported -> "ASM instructions not supported"
23 | Try_unsupported -> "Try instructions not supported"
24 | Cost_value.Unknown_cost fun_name ->
25 "Cost for function " ^ fun_name ^ " not found."
26 | Cost_value.Unknown_prototype fun_name ->
27 "Prototype for function " ^ fun_name ^ " not found."
40 let string_of_list sep f l =
41 let rec aux = function
44 | e :: l -> (f e) ^ sep ^ (aux l) in
47 let integer_term term = Logic_const.term term Cil_types.Linteger
50 let cint64 = Cil_types.CInt64 (My_bigint.of_int i, Cil_types.IInt, None) in
51 let iterm = Cil_types.TConst cint64 in
54 let cil_logic_int_var x =
55 Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger)
57 let current_kf obj = match obj#current_kf with
58 | None -> raise (Failure "Compute.current_kf")
61 let add_loop_annot obj stmt annot =
62 let annot = Cil_types.User annot in
64 Cil.get_original_kernel_function (Cil.copy_visit ()) (current_kf obj) in
65 Queue.add (fun () -> Annotations.add kf stmt [Ast.self] annot)
66 obj#get_filling_actions
68 let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots
70 let mk_invariant pred =
71 Logic_const.new_code_annotation (Cil_types.AInvariant ([], true, pred))
74 Logic_const.new_code_annotation (Cil_types.AVariant (term, None))
76 let mk_fun_cost_pred rel cost_id cost =
77 let cost_var = Cil_const.make_logic_var cost_id Cil_types.Linteger in
78 let cost_var = Logic_const.tvar cost_var in
79 let old_cost = Logic_const.told cost_var in
80 let new_cost = Cil_types.TBinOp (Cil_types.PlusA, old_cost, cost) in
81 let new_cost = integer_term new_cost in
82 Logic_const.prel (rel, cost_var, new_cost)
84 (** Casts may get in the way when looking for a loop counter, just remove
87 let rec remove_casts e = match e.Cil_types.enode with
88 | Cil_types.Lval lval ->
89 { e with Cil_types.enode = Cil_types.Lval (remove_casts_lval lval) }
90 | Cil_types.SizeOfE e ->
91 { e with Cil_types.enode = Cil_types.SizeOfE (remove_casts e) }
92 | Cil_types.AlignOfE e ->
93 { e with Cil_types.enode = Cil_types.AlignOfE (remove_casts e) }
94 | Cil_types.UnOp (unop, e, typ) ->
95 { e with Cil_types.enode = Cil_types.UnOp (unop, remove_casts e, typ) }
96 | Cil_types.BinOp (binop, e1, e2, typ) ->
98 Cil_types.BinOp (binop, remove_casts e1, remove_casts e2, typ) in
99 { e with Cil_types.enode }
100 | Cil_types.CastE (_, e) -> remove_casts e
101 | Cil_types.AddrOf lval ->
102 { e with Cil_types.enode = Cil_types.AddrOf (remove_casts_lval lval) }
103 | Cil_types.StartOf lval ->
104 { e with Cil_types.enode = Cil_types.StartOf (remove_casts_lval lval) }
105 | Cil_types.Info (e, info) ->
106 { e with Cil_types.enode = Cil_types.Info (remove_casts e, info) }
109 and remove_casts_lval (lhost, offset) =
110 (remove_casts_lhost lhost, remove_casts_offset offset)
112 and remove_casts_lhost = function
113 | Cil_types.Mem e -> Cil_types.Mem (remove_casts e)
116 and remove_casts_offset = function
117 | Cil_types.Field (fieldinfo, offset) ->
118 Cil_types.Field (fieldinfo, remove_casts_offset offset)
119 | Cil_types.Index (e, offset) ->
120 Cil_types.Index (remove_casts e, remove_casts_offset offset)
123 let rec exp_is_var name e = match (remove_casts e).Cil_types.enode with
124 | Cil_types.Lval (Cil_types.Var v, _) -> v.Cil_types.vname = name
125 | Cil_types.Info (e, _) -> exp_is_var name e
128 let has_fun_type varinfo = match varinfo.Cil_types.vtype with
129 | Cil_types.TFun _ -> true
132 let formals_of_varinfo varinfo = match varinfo.Cil_types.vtype with
133 | Cil_types.TFun (_, args, _, _) ->
134 List.map (fun (x, t, _) -> Cil.makeVarinfo false true x t)
135 (Cil.argsToList args)
136 | _ -> assert false (* do not use on these arguments *)
138 let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
140 let dummy_varinfo = Cil.makeVarinfo false false "" (Cil_types.TVoid [])
143 let rec aux acc i = if i >= n then acc else aux (a :: acc) (i+1) in
146 let rec stmt_subs stmt =
147 let added = match stmt.Cil_types.skind with
148 | Cil_types.If (_, block1, block2, _)
149 | Cil_types.TryFinally (block1, block2, _)
150 | Cil_types.TryExcept (block1, _, block2, _) ->
151 (block_subs block1) @ (block_subs block2)
152 | Cil_types.Switch (_, block, _, _)
153 | Cil_types.Loop (_, block, _, _, _)
154 | Cil_types.Block block -> block_subs block
155 | Cil_types.UnspecifiedSequence l ->
156 List.map (fun (stmt, _, _, _, _) -> stmt) l
160 and block_subs block = List.flatten (List.map stmt_subs block.Cil_types.bstmts)
162 let rec first_stmt block = match block.Cil_types.bstmts with
164 | stmt :: _ -> match stmt.Cil_types.skind with
165 | Cil_types.Block block -> first_stmt block
168 let stmt_is_break stmt = match stmt.Cil_types.skind with
169 | Cil_types.Break _ -> true
172 let starts_with_break block = match first_stmt block with
174 (match stmt.Cil_types.skind with
175 | Cil_types.Goto (stmt_ref, _) -> stmt_is_break !stmt_ref
176 | _ -> stmt_is_break stmt)
179 let rec last = function
184 let rec last_stmt block = match last block.Cil_types.bstmts with
186 | Some stmt -> match stmt.Cil_types.skind with
187 | Cil_types. Block block -> last_stmt block
190 module IntSet = Misc.Int.Set
191 module IntMap = Misc.Int.Map
192 module IntCMap = Misc.Int.CMap
195 (*** Temporary variable name generator ***)
197 module GenName = struct
202 let set_prefix prf = prefix := prf
203 let reset () = index := 0
205 let concat suffix = !prefix ^ "_" ^ suffix
208 let s = !prefix ^ (string_of_int !index) in
209 index := !index + 1 ;
212 let rec freshes n = if n = 0 then [] else (freshes (n-1)) @ [fresh ()]
214 let fresh_varinfo fundec =
215 Cil.makeTempVar fundec ~name:(fresh ()) Cil.intType
217 let freshes_varinfo fundec n =
218 let vars = freshes n in
219 List.map (fun name -> Cil.makeTempVar fundec ~name Cil.intType) vars
224 (*** Debug helpers ***)
226 let string_of_intset set =
227 IntSet.fold (fun i s -> s ^ (string_of_int i) ^ " ") set ""
228 let string_of_intset_intmap map =
229 let f i set s = Printf.sprintf "%s%d: %s\n" s i (string_of_intset set) in
232 class print_CFG prj = object inherit Visitor.frama_c_copy prj as super
235 Format.printf "*** %s ***\n\n%!" func.Cil_types.svar.Cil_types.vname ;
238 Format.printf "%d: %a\n--> %!" stmt.Cil_types.sid Cil.d_stmt stmt ;
239 List.iter (fun stmt -> Format.printf "%d %!" stmt.Cil_types.sid)
240 stmt.Cil_types.succs ;
241 Format.printf "\n\n%!")
242 func.Cil_types.sallstmts ;
243 Format.printf "\n\n%!" ;
250 File.create_project_from_visitor "print_CFG" (new print_CFG) in
252 Project.on print_CFG_prj f ()
254 class loop_exit prj = object inherit Visitor.frama_c_copy prj as super
256 method vstmt_aux stmt =
257 let _ = match stmt.Cil_types.skind with
258 | Cil_types.Loop (_, block, _, _, _) ->
259 (match first_stmt block with
261 (match stmt.Cil_types.skind with
262 | Cil_types.If (_, _, block, _) ->
263 (match first_stmt block with
265 (match stmt.Cil_types.skind with
266 | Cil_types.Break _ ->
267 Format.printf "Loop exit: %!" ;
269 (fun stmt -> Format.printf "%d %!" stmt.Cil_types.sid)
270 stmt.Cil_types.succs ;
272 | _ -> Format.printf "If but no break\n%!")
273 | _ -> Format.printf "If but no child\n%!")
274 | _ -> Format.printf "Loop but no if\n%!")
275 | _ -> Format.printf "Loop but no child\n%!")
283 File.create_project_from_visitor "loop_exit" (new loop_exit) in
285 Format.printf "\n%!" ;
286 Project.on loop_exit_prj f ()
291 class make_CFG prj = object inherit Visitor.frama_c_copy prj as super
294 Cfg.clearFileCFG file ;
295 Cfg.computeFileCFG file ;
302 File.create_project_from_visitor "make_CFG" (new make_CFG) in
304 Project.on make_CFG_prj f ()
307 (*** Control points that are gotoed to, control points of a loop. Those will
308 help checking that a loop has a supported form. ***)
310 module PointsInfo = struct
312 type t = { gotoed : IntSet.t IntMap.t ; loop_points : IntSet.t IntMap.t }
314 let empty = { gotoed = IntMap.empty ; loop_points = IntMap.empty }
316 let gotoed points_info = points_info.gotoed
318 let loop_points points_info = points_info.loop_points
320 let mem_gotoed to_id points_info = IntMap.mem to_id (gotoed points_info)
322 let find_gotoed to_id points_info = IntMap.find to_id (gotoed points_info)
324 let add_gotoed to_id to_from_ids points_info =
325 let gotoed = IntMap.add to_id to_from_ids (gotoed points_info) in
326 { points_info with gotoed }
328 let mem_loop_points loop_id points_info =
329 IntMap.mem loop_id (loop_points points_info)
331 let find_loop_points loop_id points_info =
332 IntMap.find loop_id (loop_points points_info)
334 let add_loop_points loop_id ids points_info =
335 let loop_points = IntMap.add loop_id ids (loop_points points_info) in
336 { points_info with loop_points }
340 (*** PointsInfo for each function ***)
342 module PointsInfos = struct
344 type t = PointsInfo.t Misc.String.Map.t
346 let empty = Misc.String.Map.empty
348 let mem = Misc.String.Map.mem
350 let add = Misc.String.Map.add
352 let find = Misc.String.Map.find
354 let add_gotoed fun_name to_id to_from_ids points_infos =
356 if mem fun_name points_infos then find fun_name points_infos
357 else PointsInfo.empty in
358 let points_info = PointsInfo.add_gotoed to_id to_from_ids points_info in
359 add fun_name points_info points_infos
361 let add_loop_points fun_name loop_id ids points_infos =
363 if mem fun_name points_infos then find fun_name points_infos
364 else PointsInfo.empty in
365 let points_info = PointsInfo.add_loop_points loop_id ids points_info in
366 add fun_name points_info points_infos
370 class points_infos points_infos prj =
371 object inherit Visitor.frama_c_copy prj as super
373 val mutable current_fun_name = ""
375 method vstmt_aux stmt =
376 (* because it is initialized in vfunc *)
377 assert (PointsInfos.mem current_fun_name !points_infos) ;
378 let points_info = PointsInfos.find current_fun_name !points_infos in
379 let _ = match stmt.Cil_types.skind with
380 | Cil_types.Goto (stmt_ref, _) ->
381 let from_id = stmt.Cil_types.sid in
382 let to_id = !stmt_ref.Cil_types.sid in
384 if PointsInfo.mem_gotoed to_id points_info then
385 PointsInfo.find_gotoed to_id points_info
387 let to_from_ids = IntSet.add from_id to_from_ids in
389 PointsInfos.add_gotoed current_fun_name to_id to_from_ids
391 | Cil_types.Loop (_, block, _, _, _) ->
392 let loop_id = stmt.Cil_types.sid in
394 if PointsInfo.mem_loop_points loop_id points_info then
395 PointsInfo.find_loop_points loop_id points_info
397 let ids = IntSet.add loop_id ids in
398 let f_stmts stmt = stmt :: (stmt_subs stmt) in
399 let stmts = List.flatten (List.map f_stmts block.Cil_types.bstmts) in
400 let f ids stmt = IntSet.add stmt.Cil_types.sid ids in
401 let ids = List.fold_left f ids stmts in
403 PointsInfos.add_loop_points current_fun_name loop_id ids !points_infos
407 method vfunc fundec =
408 current_fun_name <- fundec.Cil_types.svar.Cil_types.vname ;
410 PointsInfos.add current_fun_name PointsInfo.empty !points_infos ;
415 (** [points_infos ()] returns a mapping that associates to each function of the
416 current program in the currently opened project the control points that are
417 gotoed to and the control points of loops. *)
419 let points_infos () : PointsInfos.t =
420 let map = ref PointsInfos.empty in
421 let points_infos_prj =
422 File.create_project_from_visitor "points_infos" (new points_infos map) in
424 Project.on points_infos_prj f ()
427 (*** Value (flat) domain extremes ***)
429 module BotAndTop = struct
433 let compare = Pervasives.compare
435 let to_string = function
439 let to_cil_term _ = assert false (* should not be used *)
441 let top = ArithSig.A Top
442 let bot = ArithSig.A Bot
448 let addl a v = match a, v with
449 | Bot, _ | _, ArithSig.A Bot -> bot
452 let addr v a = addl a v
454 let minusl a v = match a, v with
455 | Bot, _ | _, ArithSig.A Bot -> bot
458 let minusr v a = match v, a with
459 | _, Bot | ArithSig.A Bot, _ -> bot
462 let mull a v = match a, v with
463 | Bot, _ | _, ArithSig.A Bot -> bot
464 | _, ArithSig.Int 0 -> ArithSig.Int 0
467 let mulr v a = mull a v
469 let divl a v = match a, v with
470 | Bot, _ | _, ArithSig.A Bot | _, ArithSig.Int 0 -> bot
473 let divr v a = match v, a with
474 | _, Bot | ArithSig.A Bot, _ -> bot
477 let modl a v = match a, v with
478 | Bot, _ | _, ArithSig.A Bot | _, ArithSig.Int 0 -> bot
481 let modr v a = match v, a with
482 | _, Bot | ArithSig.A Bot, _ -> bot
485 let maxl a v = match a, v with
486 | Bot, _ | _, ArithSig.A Bot -> bot
489 let maxr v a = maxl a v
491 let lel a v = match a, v with
493 | Top, ArithSig.A Top -> true
496 let ler v a = match v, a with
498 | ArithSig.A Bot, Bot -> true
501 let ltl a v = match a, v with
502 | Bot, ArithSig.A Bot -> false
506 let ltr v a = match v, a with
507 | ArithSig.A Top, Top -> false
511 let gel a v = ler v a
513 let ger v a = lel a v
515 let gtl a v = ltr v a
517 let gtr v a = ltl a v
524 (*** Arithmetic expressions flat domain ***)
526 module ArithValDom = struct
528 include Arith.Make (BotAndTop)
530 let top = A BotAndTop.Top
532 let bot = A BotAndTop.Bot
534 let join v1 v2 = match v1, v2 with
535 | A BotAndTop.Bot, v | v, A BotAndTop.Bot -> v
536 | _ when v1 = v2 -> v1
537 | _ -> A BotAndTop.Top
541 let narrow v1 v2 = match v1, v2 with
542 | A BotAndTop.Top, A _ -> v1
543 | A BotAndTop.Top, _ -> v2
546 let f_is_concrete v subs_res =
550 List.fold_left (&&) true (b :: subs_res)
552 let is_concrete v = fold f_is_concrete v
554 let add_list l = List.fold_left add (Int 0) l
556 let last_value rel _ exit_value increment =
557 let rel_added = of_int (if is_large rel then 0 else 1) in
558 let rel_op = if has_lower_type rel then minus else add in
559 add (rel_op exit_value rel_added) increment
561 let iteration_nb init_value counter increment =
562 div (minus (of_var counter) init_value) increment
566 module Domain = ArithValDom
569 (*** Abstract cost ***)
571 module AbsCost = struct
573 include (Cost_value.Make (ArithValDom))
578 (*** Requirements for loop termination ***)
580 module Require = struct
583 { relation : Domain.relation ;
584 init_value : Domain.t ;
585 exit_value : Domain.t ;
586 increment : Domain.t }
588 let compare = Pervasives.compare
590 let relation require = require.relation
591 let init_value require = require.init_value
592 let exit_value require = require.exit_value
593 let increment require = require.increment
595 let merge f require1 require2 =
596 (* each loop has a single condition relation *)
597 assert (relation require1 = relation require2) ;
598 { relation = relation require1 ;
599 init_value = f (init_value require1) (init_value require2) ;
600 exit_value = f (exit_value require1) (exit_value require2) ;
601 increment = f (increment require1) (increment require2) }
603 let join = merge Domain.join
604 let widen = merge Domain.widen
605 let narrow = merge Domain.narrow
607 let le require1 require2 =
608 (* each loop has a single condition relation *)
609 (relation require1 = relation require2) &&
610 (Domain.le (init_value require1) (init_value require2)) &&
611 (Domain.le (exit_value require1) (exit_value require2)) &&
612 (Domain.le (increment require1) (increment require2))
614 let make relation init_value exit_value increment =
615 { relation ; init_value ; exit_value ; increment }
617 let replace_vars replacements require =
618 let init_value = Domain.replace_vars replacements (init_value require) in
619 let exit_value = Domain.replace_vars replacements (exit_value require) in
620 let increment = Domain.replace_vars replacements (increment require) in
621 { require with init_value ; exit_value ; increment }
623 let to_string require =
624 Printf.sprintf "%s %s %s %s"
625 (Domain.string_of_relation (relation require))
626 (Domain.to_string (init_value require))
627 (Domain.to_string (exit_value require))
628 (Domain.to_string (increment require))
632 (*** Associates Require to control points ***)
634 module Requires = struct
636 module M = Misc.Int.Map
638 type t = Require.t M.t
647 let f_merge _ require1 require2 = match require1, require2 with
649 | Some require, None | None, Some require -> Some require
650 | Some require1, Some require2 -> Some (f require1 require2) in
653 let join = merge Require.join
654 let widen = merge Require.widen
655 let narrow = merge Require.narrow
657 let le requires1 requires2 =
658 let f id require1 res =
659 res && (mem id requires2) && (Require.le require1 (find id requires2)) in
660 M.fold f requires1 true
662 let cardinal = M.cardinal
664 let fold f requires a =
665 let f' _ require a = f require a in
670 let replace_vars replacements = M.map (Require.replace_vars replacements)
672 let to_string requires =
673 let f id require res =
674 Printf.sprintf "%s%d: %s\n%!" res id (Require.to_string require) in
682 module LoopInfo = struct
685 { tmp_loop : Cil_types.varinfo ;
687 relation : Domain.relation ;
688 exit_exp : Cil_types.exp ;
689 increment : Cil_types.exp ;
690 prev_stmts : (Cil_types.stmt * int (* position *)) list ;
691 last_stmts : Cil_types.stmt list }
693 let tmp_loop loop_info = loop_info.tmp_loop
695 let counter loop_info = loop_info.counter
697 let relation loop_info = loop_info.relation
699 let exit_exp loop_info = loop_info.exit_exp
701 let increment loop_info = loop_info.increment
703 let prev_stmts loop_info = loop_info.prev_stmts
705 let last_stmts loop_info = loop_info.last_stmts
707 let make tmp_loop counter relation exit_exp increment prev_stmts last_stmts =
708 { tmp_loop ; counter ; relation ; exit_exp ; increment ;
709 prev_stmts ; last_stmts }
714 module PointKind = struct
717 | LoopStart of LoopInfo.t
718 | LoopExit of LoopInfo.t
719 | ULoopStart (* start of an unrecognized loop *)
720 | ULoopExit (* exit of an unrecognized loop *)
723 let is_recognized_loop_start = function
724 | LoopStart _ -> true
727 let tmp_loop = function
728 | LoopStart loop_info -> LoopInfo.tmp_loop loop_info
729 | _ -> raise (Invalid_argument "PointKind.tmp_loop")
733 module PointKinds = struct
735 type t = PointKind.t IntMap.t
737 let empty = IntMap.empty
740 let find = IntMap.find
741 let fold = IntMap.fold
742 let dom point_kinds = List.map fst (IntMap.bindings point_kinds)
744 let mem_loop_start point point_kinds =
745 mem point point_kinds &&
746 (PointKind.is_recognized_loop_start (find point point_kinds))
748 let find_tmp_loop point point_kinds =
749 let error = Invalid_argument "PointKinds.find_tmp_loop" in
750 PointKind.tmp_loop (IntMap.error_find point point_kinds error)
757 module FunInfo = struct
759 type local_vars = (Cil_types.varinfo * string) list * Cil_types.varinfo list
762 { prototype : local_vars ;
763 (* exactly one start and one end points in Frama-C's CFG *)
764 start_and_end_points : (int * int) option ;
766 point_kinds : PointKinds.t }
769 { prototype = ([], []) ; start_and_end_points = None ; nb_loops = 0 ;
770 point_kinds = PointKinds.empty }
772 let make formals locals nb_loops start_and_end_points point_kinds =
773 { prototype = (formals, locals) ;
774 nb_loops ; start_and_end_points ; point_kinds }
776 let prototype fun_info =
777 List.map (fun (x, _) -> x.Cil_types.vname) (fst fun_info.prototype)
779 let start_and_end_points fun_info = fun_info.start_and_end_points
781 let formals_and_locals fun_info = fun_info.prototype
783 let point_kinds fun_info = fun_info.point_kinds
785 let mem_point point fun_info = PointKinds.mem point fun_info.point_kinds
787 let find_point point fun_info = PointKinds.find point fun_info.point_kinds
789 let points fun_info = PointKinds.dom fun_info.point_kinds
791 let nb_loops fun_info = fun_info.nb_loops
793 let add_nb_loops fun_info =
794 let nb_loops = fun_info.nb_loops + 1 in
795 { fun_info with nb_loops }
797 let mem_loop_start point fun_info =
798 PointKinds.mem_loop_start point fun_info.point_kinds
800 let find_tmp_loop point fun_info =
801 PointKinds.find_tmp_loop point fun_info.point_kinds
805 module FunInfos = struct
807 type t = FunInfo.t Misc.String.Map.t
809 let empty = Misc.String.Map.empty
811 let prototypes = Misc.String.Map.map FunInfo.prototype
813 let mem = Misc.String.Map.mem
816 fun_name formals locals nb_loops start_and_end_points point_kinds
819 FunInfo.make formals locals nb_loops start_and_end_points point_kinds in
820 Misc.String.Map.add fun_name fun_info fun_infos
822 let start_and_end_points fun_name fun_infos =
823 let error = Invalid_argument "FunInfos.start_and_end_points" in
824 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
825 FunInfo.start_and_end_points fun_info
827 let formals_and_locals fun_name fun_infos =
828 let error = Invalid_argument "FunInfos.formals_and_locals" in
829 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
830 FunInfo.formals_and_locals fun_info
832 let mem_point fun_name point fun_infos =
833 Misc.String.Map.mem fun_name fun_infos &&
834 FunInfo.mem_point point (Misc.String.Map.find fun_name fun_infos)
836 let find_point fun_name point fun_infos =
837 FunInfo.find_point point (Misc.String.Map.find fun_name fun_infos)
839 let points fun_name fun_infos =
840 let error = Invalid_argument "FunInfos.points" in
841 FunInfo.points (Misc.String.Map.error_find fun_name fun_infos error)
843 let nb_loops fun_name fun_infos =
844 let error = Invalid_argument "FunInfos.nb_loops" in
845 FunInfo.nb_loops (Misc.String.Map.error_find fun_name fun_infos error)
847 let add_nb_loops fun_name fun_infos =
848 let error = Invalid_argument "FunInfos.add_nb_loops" in
849 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
850 let fun_info = FunInfo.add_nb_loops fun_info in
851 Misc.String.Map.add fun_name fun_info fun_infos
853 let mem_loop_start fun_name point fun_infos =
854 Misc.String.Map.mem fun_name fun_infos &&
855 FunInfo.mem_loop_start point (Misc.String.Map.find fun_name fun_infos)
857 let find_tmp_loop fun_name point fun_infos =
858 let error = Invalid_argument "FunInfos.find_tmp_loop" in
859 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
860 FunInfo.find_tmp_loop point fun_info
862 let point_kinds fun_name fun_infos =
863 let error = Invalid_argument "FunInfos.point_kinds" in
864 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
865 FunInfo.point_kinds fun_info
870 (*** Static environment ***)
872 module StaticEnv = struct
876 f_old_name : string ;
879 cost_varinfo : Cil_types.varinfo ;
880 fun_infos : FunInfos.t ;
881 globals : Misc.String.Set.t ;
882 extern_costs : string Misc.String.Map.t }
884 let init fname f_old_name cost_id cost_incr extern_costs =
885 { fname ; f_old_name ; cost_id ; cost_incr ; cost_varinfo = dummy_varinfo ;
886 fun_infos = FunInfos.empty ;
887 globals = Misc.String.Set.empty ; extern_costs }
889 let fname static_env = static_env.fname
891 let f_old_name static_env = static_env.f_old_name
893 let prototypes static_env = FunInfos.prototypes static_env.fun_infos
896 fun_name formals locals nb_loops start_and_end_points point_kinds
899 FunInfos.add fun_name formals locals nb_loops start_and_end_points
900 point_kinds static_env.fun_infos in
901 { static_env with fun_infos }
903 let globals static_env = static_env.globals
905 let add_globals x static_env =
906 let globals = Misc.String.Set.add x (globals static_env) in
907 { static_env with globals }
909 let formals_and_locals fun_name static_env =
910 FunInfos.formals_and_locals fun_name static_env.fun_infos
912 let locals fun_name static_env = snd (formals_and_locals fun_name static_env)
913 let formals fun_name static_env = fst (formals_and_locals fun_name static_env)
915 let is_local fun_name x static_env =
916 let f varinfo = varinfo.Cil_types.vname = x in
917 List.exists f (locals fun_name static_env)
919 let is_formal fun_name x static_env =
920 let (formals, locals) = formals_and_locals fun_name static_env in
921 let f_local varinfo = varinfo.Cil_types.vname <> x in
922 let f_formal (varinfo, _) = varinfo.Cil_types.vname = x in
923 (List.for_all f_local locals) && (List.exists f_formal formals)
925 let is_global fun_name x static_env =
926 let (formals, locals) = formals_and_locals fun_name static_env in
927 let f_local varinfo = varinfo.Cil_types.vname <> x in
928 let f_formal (varinfo, _) = varinfo.Cil_types.vname <> x in
929 (List.for_all f_local locals) && (List.for_all f_formal formals) &&
930 (Misc.String.Set.mem x (globals static_env))
932 let cost_id static_env = static_env.cost_id
934 let cost_varinfo static_env = static_env.cost_varinfo
936 let cost_incr static_env = static_env.cost_incr
938 let set_cost_varinfo cost_varinfo static_env =
939 { static_env with cost_varinfo }
941 let mem_point fun_name point static_env =
942 FunInfos.mem_point fun_name point static_env.fun_infos
944 let find_point fun_name point static_env =
945 FunInfos.find_point fun_name point static_env.fun_infos
947 let extern_costs static_env = static_env.extern_costs
949 let start_and_end_points fun_name static_env =
950 FunInfos.start_and_end_points fun_name static_env.fun_infos
952 let mem_fun_name fun_name static_env =
953 FunInfos.mem fun_name static_env.fun_infos
955 let points fun_name static_env =
956 FunInfos.points fun_name static_env.fun_infos
958 let nb_loops fun_name static_env =
959 FunInfos.nb_loops fun_name static_env.fun_infos
961 let add_nb_loops fun_name static_env =
962 let fun_infos = FunInfos.add_nb_loops fun_name static_env.fun_infos in
963 { static_env with fun_infos }
965 let mem_loop_start fun_name point static_env =
966 FunInfos.mem_loop_start fun_name point static_env.fun_infos
968 let find_tmp_loop fun_name point static_env =
969 FunInfos.find_tmp_loop fun_name point static_env.fun_infos
971 let point_kinds fun_name static_env =
972 FunInfos.point_kinds fun_name static_env.fun_infos
977 (*** Initializations ***)
979 let special_point f body = match f body with
981 | Some stmt -> Some stmt.Cil_types.sid
983 let start_point = special_point first_stmt
985 let end_point = special_point last_stmt
987 let make_start_and_end_points start_point end_point =
988 match start_point, end_point with
989 | None, _ | _, None -> None
990 | Some start_point, Some end_point -> Some (start_point, end_point)
992 let make_tmp_names formals =
993 let f varinfo = (varinfo, GenName.concat varinfo.Cil_types.vname) in
996 let rec extract_added_value counter e = match e.Cil_types.enode with
997 | Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 ->
999 | Cil_types.BinOp (Cil_types.MinusA, e1, e2, typ)
1000 when exp_is_var counter e1 ->
1001 let enode = Cil_types.UnOp (Cil_types.Neg, e2, typ) in
1002 let e2 = { e2 with Cil_types.enode = enode } in
1004 | Cil_types.CastE (_, e) -> extract_added_value counter e
1008 "Could not find added increment value for counter %s in %a.\n%!"
1009 counter Cil.d_exp e ;
1012 let extract_increment block =
1013 let open Misc.Option in
1015 (fun stmt -> match stmt.Cil_types.skind with
1016 | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
1017 extract_added_value v.Cil_types.vname e
1021 "Could not find increment instruction; found %a instead.\n%!"
1025 let extract_guard block (counter, increment) =
1026 let open Misc.Option in
1027 first_stmt block >>=
1028 (fun stmt -> match stmt.Cil_types.skind with
1029 | Cil_types.If (e, _, block, _) when starts_with_break block ->
1030 (match e.Cil_types.enode with
1031 | Cil_types.BinOp (rel, e1, e2, _)
1032 when exp_is_var counter e1 && Domain.is_supported_rel rel ->
1033 Some (counter, Domain.rel_of_cil_binop rel, e2, increment)
1034 | Cil_types.BinOp (rel, e1, e2, _)
1035 when exp_is_var counter e2 && Domain.is_supported_rel rel ->
1036 let rel = Domain.rel_of_cil_binop rel in
1037 let rel = Domain.opposite rel in
1038 Some (counter, rel, e1, increment)
1041 Format.printf "Unsupported guard condition %a on counter %s.\n%!"
1042 Cil.d_exp e counter ;
1044 | Cil_types.If (_, _, block, _) ->
1046 Format.printf "Loop not guarded by a break:\n%a\n%!" Cil.d_block block ;
1049 if !debug then Format.printf "Loop not guarded:\n%a\n%!" Cil.d_stmt stmt ;
1053 start_id loop_start_info last_stmts loop_exit_info point_kinds =
1054 let point_kinds = PointKinds.add start_id loop_start_info point_kinds in
1055 let f_last_stmts point_kinds stmt =
1056 PointKinds.add stmt.Cil_types.sid loop_exit_info point_kinds in
1057 List.fold_left f_last_stmts point_kinds last_stmts
1059 let add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds =
1062 let loop_start_info = PointKind.ULoopStart in
1063 let loop_exit_info = PointKind.ULoopExit in
1064 add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds
1065 | Some (counter, relation, exit_exp, increment) ->
1068 tmp_loop counter relation exit_exp increment prev_stmts last_stmts in
1069 let loop_start_info = PointKind.LoopStart loop_info in
1070 let loop_exit_info = PointKind.LoopExit loop_info in
1071 add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds
1073 let loop_exits loop_points body =
1074 let f_exists stmt = not (IntSet.mem stmt.Cil_types.sid loop_points) in
1075 let f stmt = List.exists f_exists stmt.Cil_types.succs in
1076 List.filter f (block_subs body)
1078 let stmt_point_kinds fundec points_info point_kinds stmt =
1079 let id = stmt.Cil_types.sid in
1080 match stmt.Cil_types.skind with
1081 | Cil_types.Loop (_, body, _, _, _) ->
1082 let open Misc.Option in
1083 assert (PointsInfo.mem_loop_points id points_info) ;
1084 let loop_points = PointsInfo.find_loop_points id points_info in
1085 let tmp_loop = GenName.fresh_varinfo fundec in
1086 let exps = extract_increment body >>= extract_guard body in
1087 let f_preds res pred =
1088 let pred_id = pred.Cil_types.sid in
1089 if IntSet.mem pred_id loop_points then res
1092 List.map (fun stmt -> stmt.Cil_types.sid) pred.Cil_types.succs in
1093 let opt_pos = Misc.List.pos id succs_id in
1094 (* otherwise pred would not be a predecessor of the loop *)
1095 assert (opt_pos <> None) ;
1096 (pred, Misc.Option.extract opt_pos) :: res in
1098 List.fold_left f_preds [] stmt.Cil_types.preds in
1099 let last_stmts = loop_exits loop_points body in
1100 let last_stmts = match last_stmt body with
1101 | None -> last_stmts
1102 | Some last_stmt -> last_stmt :: last_stmts in
1103 add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds
1104 | _ when PointKinds.mem id point_kinds -> point_kinds
1105 | _ -> PointKinds.add id PointKind.RegularPoint point_kinds
1107 class initialize points_infos static_env prj =
1108 object inherit Visitor.frama_c_copy prj as super
1110 method vglob_aux glob =
1111 let _ = match glob with
1112 | Cil_types.GVarDecl (_, varinfo, _) when has_fun_type varinfo ->
1114 GenName.set_prefix "__tmp" ;
1115 let fun_name = varinfo.Cil_types.vname in
1116 let formals = formals_of_varinfo varinfo in
1117 let formals = make_tmp_names formals in
1120 let start_and_end_points = None in
1121 let point_kinds = PointKinds.empty in
1123 StaticEnv.add_fun_infos
1124 fun_name formals locals nb_loops start_and_end_points point_kinds
1126 | Cil_types.GFun (fundec, _) ->
1128 GenName.set_prefix "__tmp" ;
1129 let fun_name = fundec.Cil_types.svar.Cil_types.vname in
1130 (* supposes a good initialization of [points_infos] *)
1131 assert (PointsInfos.mem fun_name points_infos) ;
1132 let points_info = PointsInfos.find fun_name points_infos in
1133 let formals = fundec.Cil_types.sformals in
1134 let formals = make_tmp_names formals in
1135 let locals = fundec.Cil_types.slocals in
1137 let start_point = start_point fundec.Cil_types.sbody in
1138 let end_point = end_point fundec.Cil_types.sbody in
1139 let start_and_end_points =
1140 make_start_and_end_points start_point end_point in
1141 GenName.set_prefix "__tmp_loop" ;
1143 List.fold_left (stmt_point_kinds fundec points_info) PointKinds.empty
1144 fundec.Cil_types.sallstmts in
1146 StaticEnv.add_fun_infos
1147 fun_name formals locals nb_loops start_and_end_points point_kinds
1149 | Cil_types.GVar (varinfo, _, _)
1150 when varinfo.Cil_types.vname = StaticEnv.cost_id !static_env ->
1151 static_env := StaticEnv.set_cost_varinfo varinfo !static_env ;
1152 static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env
1153 | Cil_types.GVar (varinfo, _, _) | Cil_types.GVarDecl (_, varinfo, _) ->
1154 static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env
1160 let initialize tmp_prefix fname f_old_name cost_id cost_incr extern_costs =
1161 let points_infos = points_infos () in
1162 GenName.set_prefix tmp_prefix ;
1163 let static_env_ref =
1164 ref (StaticEnv.init fname f_old_name cost_id cost_incr extern_costs) in
1165 let initialize_prj =
1166 File.create_project_from_visitor "initialize"
1167 (new initialize points_infos static_env_ref) in
1168 let f () = !static_env_ref in
1169 Project.on initialize_prj f ()
1172 (*** Abstract domains and environments ***)
1174 module type DOMAIN = sig
1176 val of_int : int -> t
1177 val of_var : string -> t
1180 val join : t -> t -> t
1181 val widen : t -> t -> t
1182 val narrow : t -> t -> t
1183 val le : t -> t -> bool
1184 val to_string : t -> string
1186 val add : t -> t -> t
1187 val minus : t -> t -> t
1188 val mul : t -> t -> t
1189 val div : t -> t -> t
1190 val modulo : t -> t -> t
1193 module type VARABSENV = sig
1194 module Domain : DOMAIN
1198 val upd : string -> Domain.t -> t -> t
1199 val find : string -> t -> Domain.t
1200 val init : Misc.String.Set.t -> (string * string) list -> t
1201 val join : t -> t -> t
1202 val widen : t -> t -> t
1203 val narrow : t -> t -> t
1204 val le : t -> t -> bool
1205 val to_string : t -> string
1208 module type ABSENV = sig
1209 module VarAbsEnv : VARABSENV
1210 module Domain : DOMAIN
1212 type addressed = Misc.String.Set.t
1213 val cost : t -> AbsCost.t
1214 val requires : t -> Requires.t
1215 val set_cost : t -> AbsCost.t -> t
1216 val add_cost : t -> AbsCost.t -> t
1217 val add_addressed : t -> addressed -> t
1218 val set_lval : t -> Cil_types.lval -> Domain.t -> t
1219 val top_vars : t -> Misc.String.Set.t -> t
1220 val find : string -> t -> Domain.t
1222 val init : Misc.String.Set.t -> (string * string) list -> t
1223 val join : t -> t -> t
1224 val widen : t -> t -> t
1225 val narrow : t -> t -> t
1226 val le : t -> t -> bool
1227 val add_require : t -> int -> Require.t -> t
1228 val to_string : t -> string
1231 module MakeVarAbsEnv (D : DOMAIN) : VARABSENV with module Domain = D = struct
1235 type t = Domain.t Misc.String.CMap.t
1237 let bot = Misc.String.CMap.empty D.bot
1238 let upd = Misc.String.CMap.upd
1239 let find = Misc.String.CMap.find
1241 let init globals formals =
1242 let f x env = Misc.String.CMap.upd x D.top env in
1243 let env = Misc.String.Set.fold f globals bot in
1244 let f env (x, tmp) =
1245 let env = Misc.String.CMap.upd x (D.of_var tmp) env in
1246 Misc.String.CMap.upd tmp (D.of_var tmp) env in
1247 List.fold_left f env formals
1249 let join = Misc.String.CMap.merge D.join
1250 let widen = Misc.String.CMap.merge D.widen
1251 let narrow = Misc.String.CMap.merge D.narrow
1253 let top = Misc.String.CMap.empty D.top
1256 let f v1 v2 res = res && (Domain.le v1 v2) in
1257 Misc.String.CMap.cmp f env1 env2 true
1260 Misc.String.CMap.to_string (fun x -> x) (fun v -> (D.to_string v) ^ "\n")
1264 module MakeAbsEnv (VAE : VARABSENV)
1265 : ABSENV with module VarAbsEnv = VAE
1266 and module Domain = VAE.Domain = struct
1268 module VarAbsEnv = VAE
1269 module Domain = VarAbsEnv.Domain
1271 type addressed = Misc.String.Set.t
1274 { cost : AbsCost.t ; var_abs_env : VarAbsEnv.t ; addressed : addressed ;
1275 requires : Requires.t }
1277 let init globals formals =
1278 let cost = AbsCost.bot in
1279 let var_abs_env = VarAbsEnv.init globals formals in
1280 let addressed = Misc.String.Set.empty in
1281 let requires = Requires.empty in
1282 { cost ; var_abs_env ; addressed ; requires }
1284 let cost env = env.cost
1286 let requires env = env.requires
1288 let var_abs_env env = env.var_abs_env
1290 let find x env = VarAbsEnv.find x (var_abs_env env)
1292 let set_cost env cost = { env with cost }
1294 let add_cost env cost = { env with cost = AbsCost.add env.cost cost }
1296 let addressed env = env.addressed
1298 let add_addressed env addressed =
1299 { env with addressed = Misc.String.Set.union env.addressed addressed }
1301 let set_lval env lval v = match fst lval with
1302 | Cil_types.Var x ->
1303 let var_abs_env = VarAbsEnv.upd x.Cil_types.vname v env.var_abs_env in
1304 { env with var_abs_env }
1307 let top_vars env vars =
1308 let f x var_abs_env = VarAbsEnv.upd x Domain.top var_abs_env in
1309 let var_abs_env = Misc.String.Set.fold f vars env.var_abs_env in
1310 { env with var_abs_env }
1313 { cost = AbsCost.bot ; var_abs_env = VarAbsEnv.bot ;
1314 addressed = Misc.String.Set.empty ; requires = Requires.empty }
1316 let join env1 env2 =
1317 { cost = AbsCost.join (cost env1) (cost env2) ;
1318 var_abs_env = VarAbsEnv.join (var_abs_env env1) (var_abs_env env2) ;
1319 addressed = Misc.String.Set.union (addressed env1) (addressed env2) ;
1320 requires = Requires.join (requires env1) (requires env2) }
1322 let widen env1 env2 =
1323 { cost = AbsCost.widen (cost env1) (cost env2) ;
1324 var_abs_env = VarAbsEnv.widen (var_abs_env env1) (var_abs_env env2) ;
1325 addressed = Misc.String.Set.union (addressed env1) (addressed env2) ;
1326 requires = Requires.widen (requires env1) (requires env2) }
1328 let narrow env1 env2 =
1329 { cost = AbsCost.narrow (cost env1) (cost env2) ;
1330 var_abs_env = VarAbsEnv.narrow (var_abs_env env1) (var_abs_env env2) ;
1331 addressed = addressed env1 ;
1332 requires = Requires.narrow (requires env1) (requires env2) }
1335 (AbsCost.le (cost env1) (cost env2)) &&
1336 (VarAbsEnv.le (var_abs_env env1) (var_abs_env env2)) &&
1337 (Misc.String.Set.is_subset (addressed env1) (addressed env2)) &&
1338 (Requires.le (requires env1) (requires env2))
1340 let add_require env id require =
1341 { env with requires = Requires.add id require (requires env) }
1344 let f_addressed x res = res ^ x ^ " " in
1345 "Cost: " ^ (AbsCost.to_string (cost env)) ^ "\n" ^
1346 "Var env:\n" ^ (VarAbsEnv.to_string (var_abs_env env)) ^
1347 "Addressed: " ^ (Misc.String.Set.fold f_addressed (addressed env) "") ^
1349 "Requires:\n" ^ (Requires.to_string (requires env)) ^ "\n"
1353 module MakePointsAbsEnv (AE : ABSENV) = struct
1356 module Domain = AbsEnv.Domain
1359 { abs_env : AbsEnv.t IntCMap.t }
1361 let empty = { abs_env = IntCMap.empty AbsEnv.bot }
1364 let abs_env env = env.abs_env
1366 let find point env = IntCMap.find point env.abs_env
1368 let add point abs_env env =
1369 let abs_env = IntCMap.upd point abs_env env.abs_env in
1373 let cmp abs_env1 abs_env2 res = res && (AbsEnv.le abs_env1 abs_env2) in
1374 IntCMap.cmp cmp (abs_env env1) (abs_env env2) true
1376 let cost point env = AbsEnv.cost (find point env)
1378 let requires point env = AbsEnv.requires (find point env)
1380 let init start_point globals formals =
1381 add start_point (AbsEnv.init globals formals) empty
1384 IntCMap.to_string string_of_int AbsEnv.to_string (abs_env env)
1386 let widen env1 env2 =
1387 let abs_env = IntCMap.merge AbsEnv.widen (abs_env env1) (abs_env env2) in
1390 let narrow env1 env2 =
1391 let abs_env = IntCMap.merge AbsEnv.narrow (abs_env env1) (abs_env env2) in
1394 let set_cost id cost env = add id (AbsEnv.set_cost (find id env) cost) env
1399 module PointsAbsEnv = struct
1403 module VAE = MakeVarAbsEnv (D)
1405 module AE = MakeAbsEnv (VAE)
1407 include MakePointsAbsEnv (AE)
1411 module AbsEnv = PointsAbsEnv.AbsEnv
1414 (*** Dependent cost results ***)
1416 module LoopAnnotInfo = struct
1419 { counter : string ;
1420 relation : Domain.relation ;
1421 init_value : Domain.t ;
1422 exit_value : Domain.t ;
1423 increment : Domain.t ;
1424 last_value : Domain.t ;
1427 iteration_nb : Domain.t ;
1428 body_cost : AbsCost.t }
1430 let counter loop_annot_info = loop_annot_info.counter
1432 let relation loop_annot_info = loop_annot_info.relation
1434 let init_value loop_annot_info = loop_annot_info.init_value
1436 let exit_value loop_annot_info = loop_annot_info.exit_value
1438 let increment loop_annot_info = loop_annot_info.increment
1440 let last_value loop_annot_info = loop_annot_info.last_value
1442 let cost_id loop_annot_info = loop_annot_info.cost_id
1444 let tmp_loop loop_annot_info = loop_annot_info.tmp_loop
1446 let iteration_nb loop_annot_info = loop_annot_info.iteration_nb
1448 let body_cost loop_annot_info = loop_annot_info.body_cost
1451 counter relation init_value exit_value increment last_value cost_id
1452 tmp_loop iteration_nb body_cost =
1453 { counter ; relation ; init_value ; exit_value ; increment ; last_value ;
1454 cost_id ; tmp_loop ; iteration_nb ; body_cost }
1458 module LoopAnnot = struct
1461 | Variant of Domain.t
1462 | CounterMod of Domain.t * Domain.t
1463 | CounterLastValue of
1464 string * Domain.relation * Domain.t * Domain.t * Domain.t
1465 | NoIteration of string * Domain.relation * Domain.t * Domain.t
1466 | Cost of string * string * Domain.t * AbsCost.t
1468 let reduce prototypes costs = function
1469 | Cost (cost_id, tmp_loop, iteration_nb, body_cost) ->
1470 let body_cost = AbsCost.reduce prototypes costs body_cost in
1471 Cost (cost_id, tmp_loop, iteration_nb, body_cost)
1474 let compare = Pervasives.compare
1476 let variant_to_cil v =
1477 if Domain.is_concrete v then Some (mk_variant (Domain.to_cil_term v))
1480 let counter_mod_to_cil v1 v2 =
1481 if Domain.is_concrete v1 && Domain.is_concrete v2 then
1482 if v1 = v2 then None
1484 let v1 = Domain.to_cil_term v1 in
1485 let v2 = Domain.to_cil_term v2 in
1486 let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
1487 Some (mk_invariant invariant)
1490 let counter_last_value_to_cil counter rel init_value exit_value last_value =
1491 if Domain.is_concrete init_value &&
1492 Domain.is_concrete exit_value &&
1493 Domain.is_concrete last_value then
1494 let init_value = Domain.to_cil_term init_value in
1495 let exit_value = Domain.to_cil_term exit_value in
1496 let last_value = Domain.to_cil_term last_value in
1497 let rel' = Domain.cil_rel_of_rel rel in
1498 let require = Logic_const.prel (rel', init_value, exit_value) in
1499 let rel' = Domain.cil_rel_of_rel (Domain.mk_large rel) in
1500 let counter = cil_logic_int_var counter in
1501 let prop = Logic_const.prel (rel', counter, last_value) in
1502 let invariant = Logic_const.pimplies (require, prop) in
1503 Some (mk_invariant invariant)
1506 let no_iteration_to_cil counter rel init_value exit_value =
1507 if Domain.is_concrete init_value && Domain.is_concrete exit_value then
1508 let rel = Domain.opposite rel in
1509 let rel' = Domain.cil_rel_of_rel rel in
1510 let init_value = Domain.to_cil_term init_value in
1511 let exit_value = Domain.to_cil_term exit_value in
1512 let require = Logic_const.prel (rel', init_value, exit_value) in
1513 let counter = cil_logic_int_var counter in
1514 let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in
1515 let invariant = Logic_const.pimplies (require, prop) in
1516 Some (mk_invariant invariant)
1519 let cost_to_cil cost_id tmp_loop iteration_nb body_cost =
1520 if Domain.is_concrete iteration_nb && AbsCost.is_concrete body_cost then
1521 let cost_var = cil_logic_int_var cost_id in
1522 let body_cost = AbsCost.to_ext body_cost in
1523 let loop_cost = Domain.mul iteration_nb body_cost in
1524 let cost = Domain.add (Domain.of_var tmp_loop) loop_cost in
1525 if Domain.is_concrete cost then
1526 let cost = Domain.to_cil_term cost in
1527 let invariant = Logic_const.prel (Cil_types.Rle, cost_var, cost) in
1528 Some (mk_invariant invariant)
1532 let to_cil = function
1533 | Variant v -> variant_to_cil v
1534 | CounterMod (v1, v2) -> counter_mod_to_cil v1 v2
1535 | CounterLastValue(counter, rel, init_value, exit_value, last_value) ->
1536 counter_last_value_to_cil counter rel init_value exit_value last_value
1537 | NoIteration (counter, rel, init_value, exit_value) ->
1538 no_iteration_to_cil counter rel init_value exit_value
1539 | Cost (cost_id, tmp_loop, iteration_nb, body_cost) ->
1540 cost_to_cil cost_id tmp_loop iteration_nb body_cost
1542 let make_variant loop_annot_info =
1543 let rel = LoopAnnotInfo.relation loop_annot_info in
1544 let counter = LoopAnnotInfo.counter loop_annot_info in
1545 let last_value = LoopAnnotInfo.last_value loop_annot_info in
1546 let counter_var = Domain.of_var counter in
1547 let (v1, v2) = match rel with
1548 | Domain.Lt | Domain.Le -> (last_value, counter_var)
1549 | Domain.Gt | Domain.Ge -> (counter_var, last_value) in
1550 Variant (Domain.minus v1 v2)
1552 let make_counter_mod loop_annot_info =
1553 let counter = LoopAnnotInfo.counter loop_annot_info in
1554 let init_value = LoopAnnotInfo.init_value loop_annot_info in
1555 let increment = LoopAnnotInfo.increment loop_annot_info in
1556 let mk_value value = Domain.modulo value (Domain.abs increment) in
1557 let v1 = mk_value (Domain.of_var counter) in
1558 let v2 = mk_value init_value in
1561 let make_counter_last_value loop_annot_info =
1562 let counter = LoopAnnotInfo.counter loop_annot_info in
1563 let rel = LoopAnnotInfo.relation loop_annot_info in
1564 let init_value = LoopAnnotInfo.init_value loop_annot_info in
1565 let exit_value = LoopAnnotInfo.exit_value loop_annot_info in
1566 let last_value = LoopAnnotInfo.last_value loop_annot_info in
1567 CounterLastValue (counter, rel, init_value, exit_value, last_value)
1569 let make_no_iteration loop_annot_info =
1570 let counter = LoopAnnotInfo.counter loop_annot_info in
1571 let rel = LoopAnnotInfo.relation loop_annot_info in
1572 let init_value = LoopAnnotInfo.init_value loop_annot_info in
1573 let exit_value = LoopAnnotInfo.exit_value loop_annot_info in
1574 NoIteration (counter, rel, init_value, exit_value)
1576 let make_cost loop_annot_info =
1577 let cost_id = LoopAnnotInfo.cost_id loop_annot_info in
1578 let tmp_loop = LoopAnnotInfo.tmp_loop loop_annot_info in
1579 let iteration_nb = LoopAnnotInfo.iteration_nb loop_annot_info in
1580 let body_cost = LoopAnnotInfo.body_cost loop_annot_info in
1581 Cost (cost_id, tmp_loop, iteration_nb, body_cost)
1585 module LoopAnnots = struct
1587 include Eset.Make (LoopAnnot)
1589 let make loop_annot_info =
1590 let variant = LoopAnnot.make_variant loop_annot_info in
1591 (* let counter_mod = LoopAnnot.make_counter_mod loop_annot_info in *)
1592 let counter_last_value =
1593 LoopAnnot.make_counter_last_value loop_annot_info in
1594 let no_iteration = LoopAnnot.make_no_iteration loop_annot_info in
1595 let cost = LoopAnnot.make_cost loop_annot_info in
1596 of_list [variant ; (* counter_mod ; *)
1597 counter_last_value ; no_iteration ; cost]
1599 let to_cil loop_annots =
1600 let f loop_annot res = match LoopAnnot.to_cil loop_annot with
1601 | Some loop_annot -> loop_annot :: res
1603 fold f loop_annots []
1605 let reduce prototypes costs loop_annots =
1606 let f loop_annot res =
1607 add (LoopAnnot.reduce prototypes costs loop_annot) res in
1608 fold f loop_annots empty
1612 module LoopsAnnots = struct
1614 type t = LoopAnnots.t IntMap.t
1616 let empty = IntMap.empty
1618 let mem = IntMap.mem
1620 let find = IntMap.find
1622 let add = IntMap.add
1624 let to_cil loops_annots =
1625 IntMap.map LoopAnnots.to_cil loops_annots
1627 let reduce prototypes costs loops_annots =
1628 IntMap.map (LoopAnnots.reduce prototypes costs) loops_annots
1632 module CostInfo = struct
1634 type t = { cost : AbsCost.t ; requires : Requires.t ;
1635 loops_annots : LoopsAnnots.t }
1637 let cost cost_info = cost_info.cost
1639 let requires cost_info = cost_info.requires
1641 let make cost requires loops_annots = { cost ; requires ; loops_annots }
1643 let set_cost cost_info cost = { cost_info with cost }
1646 { cost ; requires = Requires.empty ; loops_annots = LoopsAnnots.empty }
1648 let loops_annots cost = cost.loops_annots
1650 let mem_loop_annots id cost = LoopsAnnots.mem id (loops_annots cost)
1652 let find_loop_annots id cost = LoopsAnnots.find id (loops_annots cost)
1654 let to_string cost_info = AbsCost.to_string (cost cost_info)
1656 let reduce_loops_annots prototypes costs cost_info =
1658 LoopsAnnots.reduce prototypes costs cost_info.loops_annots in
1659 { cost_info with loops_annots }
1661 let replace_vars replacements cost_info =
1662 let cost = AbsCost.replace_vars replacements (cost cost_info) in
1663 let requires = Requires.replace_vars replacements (requires cost_info) in
1664 { cost_info with cost ; requires }
1668 module Costs = struct
1670 type t = CostInfo.t Misc.String.Map.t
1672 let empty = Misc.String.Map.empty
1674 let init extern_costs =
1675 let f fun_name cost costs =
1676 let cost_info = CostInfo.init (AbsCost.of_extern cost) in
1677 Misc.String.Map.add fun_name cost_info costs in
1678 Misc.String.Map.fold f extern_costs empty
1680 let mem = Misc.String.Map.mem
1682 let add fun_name cost requires loops_annots costs =
1683 Misc.String.Map.add fun_name
1684 (CostInfo.make cost requires loops_annots) costs
1686 let find_cost fun_name costs =
1687 CostInfo.cost (Misc.String.Map.find fun_name costs)
1689 let find_requires fun_name costs =
1690 CostInfo.requires (Misc.String.Map.find fun_name costs)
1692 let fun_costs = Misc.String.Map.map CostInfo.cost
1694 let set_fun_costs costs fun_costs =
1695 let f fun_name cost_info =
1697 if Misc.String.Map.mem fun_name fun_costs then
1698 Misc.String.Map.find fun_name fun_costs
1699 else CostInfo.cost cost_info in
1700 CostInfo.set_cost cost_info cost in
1701 Misc.String.Map.mapi f costs
1703 let fold = Misc.String.Map.fold
1705 let to_string costs =
1706 let f fun_name cost_info res =
1707 res ^ "\n" ^ fun_name ^ ": " ^ (CostInfo.to_string cost_info) in
1710 let mem_loop_point fun_name id costs =
1711 (Misc.String.Map.mem fun_name costs) &&
1712 (CostInfo.mem_loop_annots id (Misc.String.Map.find fun_name costs))
1714 let find_loop_annots fun_name id costs =
1715 let error = Invalid_argument "Costs.find_loop_annotations" in
1716 let fun_info = Misc.String.Map.error_find fun_name costs error in
1717 CostInfo.find_loop_annots id fun_info
1719 let reduce_loops_annots prototypes costs =
1720 let fun_costs = fun_costs costs in
1722 (CostInfo.reduce_loops_annots prototypes fun_costs) costs
1724 let restore_formals static_env costs =
1725 let f fun_name cost_info =
1726 if StaticEnv.mem_fun_name fun_name static_env then
1727 let formals = StaticEnv.formals fun_name static_env in
1728 let f (formal, tmp) = (tmp, Domain.of_var formal.Cil_types.vname) in
1729 let replacements = Misc.String.Map.of_list (List.map f formals) in
1730 CostInfo.replace_vars replacements cost_info
1732 Misc.String.Map.mapi f costs
1737 (*** Abstract interpretation ***)
1739 module MakeAI (M : sig val static_env : StaticEnv.t end) = struct
1741 let rec addressed e = match e.Cil_types.enode with
1742 | Cil_types.Const _ | Cil_types.SizeOf _ | Cil_types.SizeOfStr _
1743 | Cil_types.AlignOf _ ->
1744 Misc.String.Set.empty
1745 | Cil_types.Lval lval | Cil_types.AddrOf lval | Cil_types.StartOf lval ->
1747 | Cil_types.SizeOfE e | Cil_types.AlignOfE e | Cil_types.UnOp (_, e, _)
1748 | Cil_types.CastE (_, e) | Cil_types.Info (e, _) -> addressed e
1749 | Cil_types.BinOp (_, e1, e2, _) ->
1750 Misc.String.Set.union (addressed e1) (addressed e2)
1752 and lhost_addressed = function
1753 | Cil_types.Var _ -> Misc.String.Set.empty
1754 | Cil_types.Mem e -> addressed e
1756 and offset_addressed = function
1757 | Cil_types.Index (e, offset) ->
1758 Misc.String.Set.union (addressed e) (offset_addressed offset)
1759 | _ -> Misc.String.Set.empty
1761 and lval_addressed (lhost, offset) =
1762 Misc.String.Set.union (lhost_addressed lhost) (offset_addressed offset)
1764 let branch abs_env _ = [abs_env ; abs_env]
1766 let abs_fun_of_unop = function
1767 | Cil_types.Neg -> Domain.neg
1768 | _ -> (fun _ -> Domain.top)
1770 let abs_fun_of_binop = function
1771 | Cil_types.PlusA -> Domain.add
1772 | Cil_types.MinusA -> Domain.minus
1773 | Cil_types.Mult -> Domain.mul
1774 | Cil_types.Div -> Domain.div
1775 | Cil_types.Mod -> Domain.modulo
1776 | _ -> (fun _ _ -> Domain.top)
1778 let rec exp abs_env e = match e.Cil_types.enode with
1779 | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
1780 Domain.of_int (My_bigint.to_int i)
1781 | Cil_types.Lval (Cil_types.Var varinfo, _) ->
1782 AbsEnv.find varinfo.Cil_types.vname abs_env
1783 | Cil_types.Info (e, _) -> exp abs_env e
1784 | Cil_types.UnOp (unop, e, _) ->
1785 abs_fun_of_unop unop (exp abs_env e)
1786 | Cil_types.BinOp (binop, e1, e2, _) ->
1787 abs_fun_of_binop binop (exp abs_env e1) (exp abs_env e2)
1788 | Cil_types.CastE (_, e) -> exp abs_env e (* TODO: may be incorrect *)
1791 let cost_incr_cost = function
1793 (match e.Cil_types.enode with
1794 | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
1795 AbsCost.of_int (My_bigint.to_int i)
1799 let call_proc_cost fun_name abs_env sid f args =
1800 let f_add_addrd addrd e = Misc.String.Set.union addrd (addressed e) in
1801 let addrd = List.fold_left f_add_addrd Misc.String.Set.empty (f :: args) in
1802 let abs_env = AbsEnv.add_addressed abs_env addrd in
1803 let cost = match f.Cil_types.enode with
1804 | Cil_types.Lval (Cil_types.Var var, _)
1805 when var.Cil_types.vname = StaticEnv.cost_incr M.static_env ->
1807 | Cil_types.Lval (Cil_types.Var var, _) ->
1809 fun_name sid var.Cil_types.vname (List.map (exp abs_env) args)
1810 | _ -> AbsCost.top in
1812 Misc.String.Set.union (StaticEnv.globals M.static_env) addrd in
1813 AbsEnv.add_cost (AbsEnv.top_vars abs_env vars_to_top) cost
1815 (* Executing a goto may create a loop. We over-approximate its cost with a
1816 Top. There is one exception though: Frama-C transforms programs so that
1817 there is exactly one return statement that previous return statements in
1818 the code point to with a goto. So if a goto leads to a return, the cost
1819 remains the same; in other cases, it is Top. *)
1821 let stmt_goto abs_env stmt = match stmt.Cil_types.skind with
1822 | Cil_types.Return _ -> [abs_env]
1823 | _ -> [AbsEnv.set_cost abs_env AbsCost.top]
1825 let stmt fun_name abs_env stmt = match stmt.Cil_types.skind with
1826 | Cil_types.Return _ -> []
1827 | Cil_types.Break _ | Cil_types.Continue _
1828 | Cil_types.Loop _ | Cil_types.Block _ | Cil_types.Switch _
1829 | Cil_types.Instr (Cil_types.Skip _ | Cil_types.Code_annot _) -> [abs_env]
1830 | Cil_types.Goto (stmt_ref, _) -> stmt_goto abs_env !stmt_ref
1831 | Cil_types.UnspecifiedSequence l -> make_list (List.length l) abs_env
1832 | Cil_types.If (e, _, _, _) -> branch abs_env e
1833 | Cil_types.Instr (Cil_types.Set (lval, e, _)) ->
1835 Misc.String.Set.union (lval_addressed lval) (addressed e) in
1836 let v = exp abs_env e in
1837 let abs_env = AbsEnv.add_addressed abs_env addressed in
1838 [AbsEnv.set_lval abs_env lval v]
1839 | Cil_types.Instr (Cil_types.Call (None, f, args, _)) ->
1840 [call_proc_cost fun_name abs_env stmt.Cil_types.sid f args]
1841 | Cil_types.Instr (Cil_types.Call (Some lval, f, args, _)) ->
1842 let addressed = lval_addressed lval in
1843 let abs_env = AbsEnv.add_addressed abs_env addressed in
1844 let abs_env = call_proc_cost fun_name abs_env stmt.Cil_types.sid f args in
1845 [AbsEnv.set_lval abs_env lval Domain.top]
1846 | Cil_types.Instr (Cil_types.Asm _) -> raise ASM_unsupported
1847 | Cil_types.TryFinally _ | Cil_types.TryExcept _ -> raise Try_unsupported
1849 let merge_succ_regular points_abs_env abs_env stmt =
1850 let id = stmt.Cil_types.sid in
1851 let abs_env' = PointsAbsEnv.find id points_abs_env in
1852 let abs_env' = AbsEnv.join abs_env abs_env' in
1853 PointsAbsEnv.add id abs_env' points_abs_env
1855 let merge_succ_uloop_start src_id points_abs_env abs_env =
1856 let points_abs_env =
1857 PointsAbsEnv.set_cost src_id AbsCost.top points_abs_env in
1858 let abs_env = AbsEnv.set_cost abs_env (AbsCost.of_int 0) in
1859 merge_succ_regular points_abs_env abs_env
1861 let prev_init_and_cost fun_name counter points_abs_env prev_stmts =
1862 let f (init_value, before_cost) (stmt_, pos) =
1863 let abs_env = PointsAbsEnv.find (stmt_.Cil_types.sid) points_abs_env in
1864 let abs_env = List.nth (stmt fun_name abs_env stmt_) pos in
1865 let init_value = Domain.join init_value (AbsEnv.find counter abs_env) in
1866 let before_cost = AbsCost.join before_cost (AbsEnv.cost abs_env) in
1867 (init_value, before_cost) in
1868 List.fold_left f (Domain.bot, AbsCost.bot) prev_stmts
1870 let body_cost points_abs_env last_stmts =
1871 (* Exiting a loop can only be done through a break or a goto or whatever,
1872 but certainly not with a cost increment instruction. Thus, executing the
1873 last statements of a loop should not change the cost information, so its
1874 unnecessary when this is all we care about. *)
1876 let id = stmt.Cil_types.sid in
1877 AbsCost.join res (AbsEnv.cost (PointsAbsEnv.find id points_abs_env)) in
1878 List.fold_left f AbsCost.bot last_stmts
1880 let loop_cost fun_name id loop_info points_abs_env abs_env =
1881 let cost_id = StaticEnv.cost_id M.static_env in
1882 let tmp_loop = LoopInfo.tmp_loop loop_info in
1883 let counter = LoopInfo.counter loop_info in
1884 let relation = LoopInfo.relation loop_info in
1885 let prev_stmts = LoopInfo.prev_stmts loop_info in
1886 let last_stmts = LoopInfo.last_stmts loop_info in
1887 let (init_value, before_cost) =
1888 prev_init_and_cost fun_name counter points_abs_env prev_stmts in
1889 let exit_value = exp abs_env (LoopInfo.exit_exp loop_info) in
1890 let increment = exp abs_env (LoopInfo.increment loop_info) in
1892 Domain.last_value relation init_value exit_value increment in
1893 let iteration_nb = Domain.iteration_nb init_value counter increment in
1894 let body_cost = body_cost points_abs_env last_stmts in
1896 if AbsCost.is_top body_cost then AbsCost.top
1898 AbsCost.of_loop_cost
1899 fun_name id relation init_value exit_value increment
1900 (AbsCost.extract body_cost) in
1901 let succ_loop_cost = AbsCost.add before_cost loop_cost in
1902 (counter, relation, init_value, exit_value, increment, last_value, cost_id,
1903 tmp_loop, iteration_nb, body_cost, succ_loop_cost)
1905 let merge_succ_loop_start
1906 fun_name src_id loop_info points_abs_env points_abs_env' abs_env =
1907 let src_abs_env = PointsAbsEnv.find src_id points_abs_env in
1908 let (_, rel, init_value, exit_value, increment, _, _, _, _, _, _) =
1909 loop_cost fun_name src_id loop_info points_abs_env src_abs_env in
1910 let require = Require.make rel init_value exit_value increment in
1911 let abs_env = AbsEnv.add_require abs_env src_id require in
1912 merge_succ_uloop_start src_id points_abs_env' abs_env
1914 let merge_succ_loop_exit
1915 fun_name loop_start_id loop_info points_abs_env points_abs_env'
1917 let start_abs_env = PointsAbsEnv.find loop_start_id points_abs_env in
1918 let (_, _, _, _, _, _, _, _, _, _, succ_loop_cost) =
1919 loop_cost fun_name loop_start_id loop_info points_abs_env start_abs_env
1921 let abs_env = AbsEnv.set_cost abs_env succ_loop_cost in
1922 merge_succ_regular points_abs_env' abs_env stmt
1924 let merge_succ_uloop_exit points_abs_env abs_env =
1925 let abs_env = AbsEnv.set_cost abs_env AbsCost.top in
1926 merge_succ_regular points_abs_env abs_env
1928 let merge_succ fun_name src_id points_abs_env =
1929 if StaticEnv.mem_point fun_name src_id M.static_env then
1930 match StaticEnv.find_point fun_name src_id M.static_env with
1931 | PointKind.RegularPoint -> merge_succ_regular
1932 | PointKind.LoopStart loop_info ->
1933 merge_succ_loop_start fun_name src_id loop_info points_abs_env
1934 | PointKind.LoopExit loop_info ->
1935 merge_succ_loop_exit fun_name src_id loop_info points_abs_env
1936 | PointKind.ULoopStart -> merge_succ_uloop_start src_id
1937 | PointKind.ULoopExit -> merge_succ_uloop_exit
1938 else raise (Invalid_argument "AI.merge_succ")
1940 let fundec_stmt fun_name points_abs_env points_abs_env' stmt_ =
1941 let id = stmt_.Cil_types.sid in
1942 let abs_env = PointsAbsEnv.find id points_abs_env in
1943 let abs_envs = stmt fun_name abs_env stmt_ in
1944 (* Otherwise the [stmt] function is not correct. *)
1945 assert (List.length abs_envs = List.length stmt_.Cil_types.succs) ;
1946 let f = merge_succ fun_name id points_abs_env in
1947 List.fold_left2 f points_abs_env' abs_envs stmt_.Cil_types.succs
1949 let rec fundec_stmts fun_name points_abs_env cmp merge stmts =
1951 Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env) ;
1952 let f = fundec_stmt fun_name points_abs_env in
1953 let points_abs_env' = List.fold_left f PointsAbsEnv.bot stmts in
1954 let points_abs_env' = merge points_abs_env points_abs_env' in
1955 if cmp points_abs_env' points_abs_env then
1957 Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env') ;
1959 else fundec_stmts fun_name points_abs_env' cmp merge stmts
1961 let fundec_stmts_widen fun_name points_abs_env =
1962 fundec_stmts fun_name points_abs_env PointsAbsEnv.le PointsAbsEnv.widen
1964 let fundec_stmts_narrow fun_name points_abs_env =
1965 let cmp env1 env2 = PointsAbsEnv.le env2 env1 in
1966 fundec_stmts fun_name points_abs_env cmp PointsAbsEnv.narrow
1968 let loop_annot_info fun_name id points_abs_env loop_info =
1969 let abs_env = PointsAbsEnv.find id points_abs_env in
1970 let (counter, relation, init_value, exit_value, last_value, increment,
1971 cost_id, tmp_loop, iteration_nb, body_cost, _) =
1972 loop_cost fun_name id loop_info points_abs_env abs_env in
1974 counter relation init_value exit_value last_value increment cost_id
1975 tmp_loop.Cil_types.vname iteration_nb body_cost
1977 let loop_annots fun_name points_abs_env id point_kind loops_annots =
1978 match point_kind with
1979 | PointKind.LoopStart loop_info ->
1980 let loop_annot_info =
1981 loop_annot_info fun_name id points_abs_env loop_info in
1982 let loop_annots = LoopAnnots.make loop_annot_info in
1983 LoopsAnnots.add id loop_annots loops_annots
1984 | PointKind.ULoopStart ->
1985 let loop_annots = LoopAnnots.empty in
1986 LoopsAnnots.add id loop_annots loops_annots
1989 let loops_annots fun_name points_abs_env =
1990 PointKinds.fold (loop_annots fun_name points_abs_env)
1991 (StaticEnv.point_kinds fun_name M.static_env) LoopsAnnots.empty
1996 (*** Dependent costs computation ***)
1998 class compute_costs widen narrow loops_annots static_env costs prj =
1999 object inherit Visitor.frama_c_copy prj as super
2001 method vfunc fundec =
2002 let fun_name = fundec.Cil_types.svar.Cil_types.vname in
2003 if fun_name = StaticEnv.cost_incr static_env then begin
2004 costs := Costs.add fun_name AbsCost.top Requires.empty
2005 LoopsAnnots.empty !costs ;
2006 Cil.SkipChildren end
2008 (* The function should be in the static environment because of the
2010 assert (StaticEnv.mem_fun_name fun_name static_env) ;
2011 let _ = match StaticEnv.start_and_end_points fun_name static_env with
2013 costs := Costs.add fun_name AbsCost.top Requires.empty
2014 LoopsAnnots.empty !costs
2015 | Some (start_point, end_point) ->
2016 if !debug then Printf.printf "Interpreting %s\n%!" fun_name ;
2017 let formals = StaticEnv.formals fun_name static_env in
2018 let f_formals (varinfo, tmp) = (varinfo.Cil_types.vname, tmp) in
2019 let globals = StaticEnv.globals static_env in
2020 let formals = List.map f_formals formals in
2021 let env = PointsAbsEnv.init start_point globals formals in
2022 if !debug then Printf.printf "WIDEN\n%!" ;
2023 let env = widen fun_name env fundec.Cil_types.sallstmts in
2024 if !debug then Printf.printf "NARROW\n%!" ;
2025 let env = narrow fun_name env fundec.Cil_types.sallstmts in
2026 let cost = PointsAbsEnv.cost end_point env in
2027 let requires = PointsAbsEnv.requires end_point env in
2028 let loops_annots = loops_annots fun_name env in
2029 (* The last instruction should be a return. Executing it shouldn't
2030 change the environment. *)
2031 costs := Costs.add fun_name cost requires loops_annots !costs in
2032 Cil.SkipChildren end
2036 let compute_costs static_env =
2037 let module AI = MakeAI (struct let static_env = static_env end) in
2038 let costs = ref (Costs.init (StaticEnv.extern_costs static_env)) in
2039 let compute_costs_prj =
2040 File.create_project_from_visitor
2042 (new compute_costs AI.fundec_stmts_widen AI.fundec_stmts_narrow
2043 AI.loops_annots static_env costs) in
2044 let f () = !costs in
2045 Project.on compute_costs_prj f ()
2048 (*** Costs solver ***)
2050 let solve_end costs1 costs2 =
2051 let f fun_name cost res =
2052 res && (Misc.String.Map.mem fun_name costs1) &&
2053 (cost = Misc.String.Map.find fun_name costs1) in
2054 Misc.String.Map.fold f costs2 true
2056 let string_of_fun_costs fun_costs =
2057 let f fun_name cost res =
2058 Printf.sprintf "%s%s: %s\n%!" res fun_name (AbsCost.to_string cost) in
2059 Misc.String.Map.fold f fun_costs ""
2061 let solve_costs static_env costs =
2062 let costs = Costs.restore_formals static_env costs in
2063 let fun_costs = Costs.fun_costs costs in
2064 let prototypes = StaticEnv.prototypes static_env in
2065 let rec aux fun_costs =
2066 if !debug then Printf.printf "%s\n%!" (string_of_fun_costs fun_costs) ;
2067 let fun_costs' = AbsCost.reduces prototypes fun_costs in
2068 if solve_end fun_costs fun_costs' then fun_costs
2069 else aux fun_costs' in
2070 let fun_costs = aux fun_costs in
2071 let costs = Costs.set_fun_costs costs fun_costs in
2072 Costs.reduce_loops_annots prototypes costs
2075 (*** Add annotations ***)
2077 let add_tmp_loop_init cost_varinfo tmp_loop stmt =
2078 let lval = Cil.var tmp_loop in
2080 Cil.new_exp dummy_location (Cil_types.Lval (Cil.var cost_varinfo)) in
2082 Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
2083 let new_stmt = Cil.mkStmt new_stmt in
2084 Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))
2086 let make_tmp_formal_init fundec varinfo tmp_var =
2087 let tmp_var = Cil.makeTempVar fundec ~name:tmp_var varinfo.Cil_types.vtype in
2088 let lval = Cil.var tmp_var in
2089 let e = Cil.new_exp dummy_location (Cil_types.Lval (Cil.var varinfo)) in
2090 let new_stmt = Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
2093 let make_tmp_formals_init fundec l =
2094 let f (varinfo, tmp_var) = make_tmp_formal_init fundec varinfo tmp_var in
2097 let add_tmp_formals_init formals fundec =
2098 let tmp_formals_init = make_tmp_formals_init fundec formals in
2099 let block = tmp_formals_init @ fundec.Cil_types.sbody.Cil_types.bstmts in
2100 let body = { fundec.Cil_types.sbody with Cil_types.bstmts = block } in
2101 { fundec with Cil_types.sbody = body }
2103 let make_require require =
2104 let rel = Require.relation require in
2105 let init_value = Require.init_value require in
2106 let exit_value = Require.exit_value require in
2107 let increment = Require.increment require in
2108 if Domain.is_concrete init_value &&
2109 Domain.is_concrete exit_value &&
2110 Domain.is_concrete increment then
2111 let zero = Domain.of_int 0 in
2112 let rel' = Domain.mk_strict rel in
2113 let cil_init_value = Domain.to_cil_term init_value in
2114 let cil_exit_value = Domain.to_cil_term exit_value in
2115 let cil_zero = Domain.to_cil_term zero in
2116 let cil_increment = Domain.to_cil_term increment in
2117 let cil_rel = Domain.cil_rel_of_rel rel in
2118 let cil_rel' = Domain.cil_rel_of_rel rel' in
2119 let t1 = Logic_const.prel (cil_rel, cil_init_value, cil_exit_value) in
2120 let t2 = Logic_const.prel (cil_rel', cil_zero, cil_increment) in
2121 let t3 = Logic_const.pimplies (t1, t2) in
2124 if Domain.bool_of_cond rel' zero increment then None
2126 if Domain.bool_of_cond (Domain.opposite rel) init_value exit_value then
2129 if Domain.bool_of_cond rel init_value exit_value then Some t2
2134 let make_requires requires =
2136 let added_require = match make_require require with
2138 | Some require -> [require] in
2139 added_require @ res in
2140 Requires.fold f requires []
2142 let add_spec pres post spec =
2143 let requires = List.map Logic_const.new_predicate pres in
2144 let post_cond = [(Cil_types.Normal, Logic_const.new_predicate post)] in
2145 let new_behavior = Cil.mk_behavior ~requires ~post_cond () in
2146 spec.Cil_types.spec_behavior <- new_behavior :: spec.Cil_types.spec_behavior
2148 let add_cost_annotation requires rel cost_id cost spec =
2149 let post = mk_fun_cost_pred rel cost_id cost in
2150 add_spec (make_requires requires) post spec ;
2151 Cil.ChangeDoChildrenPost (spec, identity)
2153 let add_cost_incr_annotation cost_id fundec =
2154 let rel = Cil_types.Req in
2156 Logic_const.tvar (Cil_const.make_logic_var "incr" Cil_types.Linteger) in
2157 add_cost_annotation Requires.empty rel cost_id cost fundec
2159 let add_regular_fun_annotation cost_id requires cost spec =
2160 if AbsCost.is_concrete cost then
2161 let cost = AbsCost.to_ext cost in
2162 let rel = Cil_types.Rle in
2163 if Domain.is_concrete cost then
2164 add_cost_annotation requires rel cost_id (Domain.to_cil_term cost) spec
2168 let add_fundec_annotation static_env costs fun_name spec =
2169 assert (Costs.mem fun_name costs) ;
2170 let cost = Costs.find_cost fun_name costs in
2171 let requires = Costs.find_requires fun_name costs in
2172 let cost_id = StaticEnv.cost_id static_env in
2173 let cost_incr = StaticEnv.cost_incr static_env in
2174 if fun_name = cost_incr then add_cost_incr_annotation cost_id spec
2175 else add_regular_fun_annotation cost_id requires cost spec
2177 class add_annotations static_env costs prj =
2178 object (self) inherit Visitor.frama_c_copy prj as super
2180 val mutable current_fun_name : string = ""
2182 method vstmt_aux stmt = match stmt.Cil_types.skind with
2184 when StaticEnv.mem_loop_start current_fun_name stmt.Cil_types.sid
2186 let cost_varinfo = StaticEnv.cost_varinfo static_env in
2187 (* only use with costs correctly set and initialized *)
2188 assert (Costs.mem_loop_point current_fun_name stmt.Cil_types.sid costs) ;
2190 StaticEnv.find_tmp_loop current_fun_name stmt.Cil_types.sid
2193 Costs.find_loop_annots current_fun_name stmt.Cil_types.sid costs in
2194 add_loop_annots self stmt (LoopAnnots.to_cil annots) ;
2195 let change = add_tmp_loop_init cost_varinfo tmp_loop in
2196 Cil.ChangeDoChildrenPost (stmt, change)
2197 | _ -> Cil.DoChildren
2199 method vfunc fundec =
2200 let fun_name = fundec.Cil_types.svar.Cil_types.vname in
2201 current_fun_name <- fun_name ;
2202 if fun_name = StaticEnv.cost_incr static_env then Cil.DoChildren
2204 let formals = StaticEnv.formals fun_name static_env in
2205 Cil.ChangeDoChildrenPost (fundec, add_tmp_formals_init formals)
2207 method vspec spec = match self#current_kf with
2208 | None -> Cil.JustCopy
2210 match kf.Cil_types.fundec with
2211 | Cil_types.Definition (fundec, _) ->
2212 let fun_name = fundec.Cil_types.svar.Cil_types.vname in
2213 add_fundec_annotation static_env costs fun_name spec
2214 | Cil_types.Declaration (_, f, _, _) ->
2215 let fun_name = f.Cil_types.vname in
2216 add_fundec_annotation static_env costs fun_name spec
2220 let add_annotations static_env costs =
2221 let add_annotations_prj =
2222 File.create_project_from_visitor
2223 "add_annotations" (new add_annotations static_env costs) in
2225 Kernel.CodeOutput.set (StaticEnv.fname static_env) ;
2226 File.pretty_ast () in
2227 Project.on add_annotations_prj f ()
2230 (*** Save results ***)
2232 let save_results static_env costs =
2233 let fname = StaticEnv.f_old_name static_env in
2234 let f fun_name cost_info res =
2235 let cost = CostInfo.cost cost_info in
2237 (if AbsCost.is_concrete cost then
2238 fun_name ^ " " ^ (Domain.to_string (AbsCost.to_ext cost)) ^ "\n"
2240 let s = Costs.fold f costs "" in
2242 try Filename.chop_extension fname
2243 with Invalid_argument "Filename.chop_extension" -> fname in
2244 let save_file = save_file ^ ".cost_results" in
2246 let oc = open_out save_file in
2247 output_string oc s ;
2250 Printf.eprintf "Could not save plug-in results in file %s.\n%!" save_file
2255 let cost ((fname, _), f_old_name, {Cerco.cost_id = cost_id;
2256 cost_incr = cost_incr;
2257 extern_costs = extern_costs} , _) =
2259 Kernel.Files.set [fname] ;
2260 File.init_from_cmdline () ;
2261 if !debug then Printf.printf "Make CFG\n%!" ;
2263 if !debug then print_CFG () ;
2264 if !debug then Printf.printf "Initialize\n%!" ;
2266 initialize "__tmp" fname f_old_name cost_id cost_incr extern_costs in
2267 if !debug then Printf.printf "Compute costs\n%!" ;
2268 let costs = compute_costs static_env in
2269 if !debug then Printf.printf "%s\n%!" (Costs.to_string costs) ;
2270 if !debug then Printf.printf "Solve costs\n%!" ;
2271 let costs = solve_costs static_env costs in
2272 if !debug then Printf.printf "Costs:\n%s\n%!" (Costs.to_string costs) ;
2273 if !debug then Printf.printf "Save results\n%!" ;
2274 save_results static_env costs ;
2275 if !debug then Printf.printf "Add annotations\n%!" ;
2276 add_annotations static_env costs
2277 with e -> Printf.eprintf "** ERROR: %s.\n%!" (string_of_exception e)