source: Deliverables/D5.1-5.3/cost-plug-in/plugin/compute.ml @ 1679

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

Frama-C plug-in (sources+documentation)

File size: 74.5 KB
Line 
1
2(* TODO: goto'ed label: top cost *)
3
4(*** Exceptions ***)
5
6exception ASM_unsupported
7exception Try_unsupported
8
9let string_of_exception = function
10  | ASM_unsupported -> "ASM instructions not supported"
11  | Try_unsupported -> "Try instructions not supported"
12  | Cost_value.Unknown_cost fun_name ->
13    "Cost for function " ^ fun_name ^ " not found."
14  | Cost_value.Unknown_prototype fun_name ->
15    "Prototype for function " ^ fun_name ^ " not found."
16  | e -> raise e
17
18
19(*** Debug flag ***)
20
21let debug = ref false
22
23
24(*** Helpers ***)
25
26let identity x = x
27
28let string_of_list sep f l =
29  let rec aux = function
30    | [] -> ""
31    | [e] -> f e
32    | e :: l -> (f e) ^ sep ^ (aux l) in
33  aux l
34
35let integer_term term = Logic_const.term term Cil_types.Linteger
36
37let tinteger i =
38  let cint64 = Cil_types.CInt64 (Int64.of_int i, Cil_types.IInt, None) in
39  let iterm = Cil_types.TConst cint64 in
40  integer_term iterm
41
42let cil_logic_int_var x =
43  Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger)
44
45type loops_annotation =
46    (string -> string ->
47     (Db_types.rooted_code_annotation Db_types.before_after) list)
48
49type loops_annotations = loops_annotation list
50
51let add_loop_annot obj stmt annot = 
52  Queue.add (fun () -> Annotations.add stmt [Ast.self] annot)
53    obj#get_filling_actions
54
55let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots
56
57let loop_annotation annot = Db_types.Before (Db_types.User annot)
58
59let mk_invariant pred =
60  let annot =
61    Logic_const.new_code_annotation (Cil_types.AInvariant ([], true, pred)) in
62  loop_annotation annot
63
64let mk_variant term =
65  let annot =
66    Logic_const.new_code_annotation (Cil_types.AVariant (term, None)) in
67  loop_annotation annot
68
69let current_kf obj = match obj#current_kf with
70  | None -> raise (Failure "Compute.current_kf")
71  | Some kf -> kf
72
73let current_fundec obj = match (current_kf obj).Db_types.fundec with
74  | Db_types.Definition (fundec, _) -> fundec
75  | _ -> raise (Failure "Compute.current_fundec")
76
77let current_fun_name obj = (current_fundec obj).Cil_types.svar.Cil_types.vname
78
79let current_spec obj = (current_fundec obj).Cil_types.sspec
80
81let mk_fun_cost_pred rel cost_id cost = 
82  let cost_var = Cil_const.make_logic_var cost_id Cil_types.Linteger in
83  let cost_var = Logic_const.tvar cost_var in
84  let old_cost =
85    Logic_const.term (Cil_types.Told cost_var) cost_var.Cil_types.term_type in
86  let new_cost = Cil_types.TBinOp (Cil_types.PlusA, old_cost, cost) in
87  let new_cost = integer_term new_cost in
88  Logic_const.prel (rel, cost_var, new_cost)
89
90let rec remove_casts e = match e.Cil_types.enode with
91  | Cil_types.Lval lval ->
92    { e with Cil_types.enode = Cil_types.Lval (remove_casts_lval lval) }
93  | Cil_types.SizeOfE e ->
94    { e with Cil_types.enode = Cil_types.SizeOfE (remove_casts e) }
95  | Cil_types.AlignOfE e ->
96    { e with Cil_types.enode = Cil_types.AlignOfE (remove_casts e) }
97  | Cil_types.UnOp (unop, e, typ) ->
98    { e with Cil_types.enode = Cil_types.UnOp (unop, remove_casts e, typ) }
99  | Cil_types.BinOp (binop, e1, e2, typ) ->
100    let enode =
101      Cil_types.BinOp (binop, remove_casts e1, remove_casts e2, typ) in
102    { e with Cil_types.enode }
103  | Cil_types.CastE (_, e) -> remove_casts e
104  | Cil_types.AddrOf lval ->
105    { e with Cil_types.enode = Cil_types.AddrOf (remove_casts_lval lval) }
106  | Cil_types.StartOf lval ->
107    { e with Cil_types.enode = Cil_types.StartOf (remove_casts_lval lval) }
108  | Cil_types.Info (e, info) ->
109    { e with Cil_types.enode = Cil_types.Info (remove_casts e, info) }
110  | _ -> e
111
112and remove_casts_lval (lhost, offset) =
113  (remove_casts_lhost lhost, remove_casts_offset offset)
114
115and remove_casts_lhost = function
116  | Cil_types.Mem e -> Cil_types.Mem (remove_casts e)
117  | lhost -> lhost
118
119and remove_casts_offset = function
120  | Cil_types.Field (fieldinfo, offset) ->
121    Cil_types.Field (fieldinfo, remove_casts_offset offset)
122  | Cil_types.Index (e, offset) ->
123    Cil_types.Index (remove_casts e, remove_casts_offset offset)
124  | offset -> offset
125
126let rec exp_is_var name e = match (remove_casts e).Cil_types.enode with
127  | Cil_types.Lval (Cil_types.Var v, _) -> v.Cil_types.vname = name
128  | Cil_types.Info (e, _) -> exp_is_var name e
129  | _ -> false
130
131let has_fun_type varinfo = match varinfo.Cil_types.vtype with
132  | Cil_types.TFun _ -> true
133  | _ -> false
134
135let formals_of_varinfo varinfo = match varinfo.Cil_types.vtype with
136  | Cil_types.TFun (_, None, _, _) -> []
137  | Cil_types.TFun (_, Some l, _, _) ->
138    List.map (fun (x, t, _) -> Cil.makeVarinfo false true x t) l
139  | _ -> assert false (* do not use on these arguments *)
140
141let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
142
143let dummy_varinfo = Cil.makeVarinfo false false "" (Cil_types.TVoid [])
144
145let make_list n a =
146  let rec aux acc i = if i >= n then acc else aux (a :: acc) (i+1) in
147  aux [] 0
148
149let rec stmt_subs stmt =
150  let added = match stmt.Cil_types.skind with
151    | Cil_types.If (_, block1, block2, _)
152    | Cil_types.TryFinally (block1, block2, _)
153    | Cil_types.TryExcept (block1, _, block2, _) ->
154      (block_subs block1) @ (block_subs block2)
155    | Cil_types.Switch (_, block, _, _)
156    | Cil_types.Loop (_, block, _, _, _)
157    | Cil_types.Block block -> block_subs block
158    | Cil_types.UnspecifiedSequence l ->
159      List.map (fun (stmt, _, _, _, _) -> stmt) l
160    | _ -> [] in
161  stmt :: added
162
163and block_subs block = List.flatten (List.map stmt_subs block.Cil_types.bstmts)
164
165let rec first_stmt block = match block.Cil_types.bstmts with
166  | [] -> None
167  | stmt :: _ -> match stmt.Cil_types.skind with
168      | Cil_types.Block block -> first_stmt block
169      | _ -> Some stmt
170
171let stmt_is_break stmt = match stmt.Cil_types.skind with
172  | Cil_types.Break _ -> true
173  | _ -> false
174
175let starts_with_break block = match first_stmt block with
176  | Some stmt ->
177    (match stmt.Cil_types.skind with
178      | Cil_types.Goto (stmt_ref, _) -> stmt_is_break !stmt_ref
179      | _ -> stmt_is_break stmt)
180  | _ -> false
181
182let rec last = function
183  | [] -> None
184  | [e] -> Some e
185  | _ :: l -> last l
186
187let rec last_stmt block = match last block.Cil_types.bstmts with
188  | None -> None
189  | Some stmt -> match stmt.Cil_types.skind with
190      | Cil_types. Block block -> last_stmt block
191      | _ -> Some stmt
192
193module IntSet = Misc.Int.Set
194module IntMap = Misc.Int.Map
195module IntCMap = Misc.Int.CMap
196
197
198(*** Temporary variable name generator ***)
199
200module GenName = struct
201
202  let prefix = ref ""
203  let index = ref 0
204
205  let set_prefix prf = prefix := prf
206  let reset () = index := 0
207
208  let concat suffix = !prefix ^ "_" ^ suffix
209
210  let fresh () =
211    let s = !prefix ^ (string_of_int !index) in
212    index := !index + 1 ;
213    s
214
215  let rec freshes n = if n = 0 then [] else (freshes (n-1)) @ [fresh ()]
216
217  let fresh_varinfo fundec =
218    Cil.makeTempVar fundec ~name:(fresh ()) Cil.intType
219
220  let freshes_varinfo fundec n =
221    let vars = freshes n in
222    List.map (fun name -> Cil.makeTempVar fundec ~name Cil.intType) vars
223
224end
225
226
227(*** Debug helpers ***)
228
229let string_of_intset set =
230  IntSet.fold (fun i s -> s ^ (string_of_int i) ^ " ") set ""
231let string_of_intset_intmap map =
232  let f i set s = Printf.sprintf "%s%d: %s\n" s i (string_of_intset set) in
233  IntMap.fold f map ""
234
235class print_CFG prj = object inherit Visitor.frama_c_copy prj as super
236
237  method vfunc func =
238    Format.printf "*** %s ***\n\n%!" func.Cil_types.svar.Cil_types.vname ;
239    List.iter
240      (fun stmt ->
241        Format.printf "%d: %a\n--> %!" stmt.Cil_types.sid Cil.d_stmt stmt ;
242        List.iter (fun stmt -> Format.printf "%d %!" stmt.Cil_types.sid)
243          stmt.Cil_types.succs ;
244        Format.printf "\n\n%!")
245      func.Cil_types.sallstmts ;
246    Format.printf "\n\n%!" ;
247    Cil.SkipChildren
248
249end
250
251let print_CFG () =
252  let print_CFG_prj =
253    File.create_project_from_visitor "print_CFG" (new print_CFG) in
254  let f () = () in
255  Project.on print_CFG_prj f ()
256
257class loop_exit prj = object inherit Visitor.frama_c_copy prj as super
258
259  method vstmt_aux stmt =
260    let _ = match stmt.Cil_types.skind with
261      | Cil_types.Loop (_, block, _, _, _) ->
262        (match first_stmt block with
263          | Some stmt ->
264            (match stmt.Cil_types.skind with
265              | Cil_types.If (_, _, block, _) ->
266                (match first_stmt block with
267                  | Some stmt ->
268                    (match stmt.Cil_types.skind with
269                      | Cil_types.Break _ ->
270                        Format.printf "Loop exit: %!" ;
271                        List.iter
272                          (fun stmt -> Format.printf "%d %!" stmt.Cil_types.sid)
273                          stmt.Cil_types.succs ;
274                        Format.printf "\n%!"
275                      | _ -> Format.printf "If but no break\n%!")
276                  | _ -> Format.printf "If but no child\n%!")
277              | _ -> Format.printf "Loop but no if\n%!")
278          | _ -> Format.printf "Loop but no child\n%!")
279      | _ -> () in
280    Cil.DoChildren
281
282end
283
284let loop_exit () =
285  let loop_exit_prj =
286    File.create_project_from_visitor "loop_exit" (new loop_exit) in
287  let f () = () in
288  Format.printf "\n%!" ;
289  Project.on loop_exit_prj f ()
290
291
292(*** Make CFG ***)
293
294class make_CFG prj = object inherit Visitor.frama_c_copy prj as super
295
296  method vfile file =
297    Cfg.clearFileCFG file ;
298    Cfg.computeFileCFG file ;
299    Cil.SkipChildren
300
301end
302
303let make_CFG () =
304  let make_CFG_prj =
305    File.create_project_from_visitor "make_CFG" (new make_CFG) in
306  let f () = () in
307  Project.on make_CFG_prj f ()
308
309
310(*** Control points that are goto'ed to, control points of a loop. ***)
311
312module PointsInfo = struct
313
314  type t = { gotoed : IntSet.t IntMap.t ; loop_points : IntSet.t IntMap.t }
315
316  let empty = { gotoed = IntMap.empty ; loop_points = IntMap.empty }
317
318  let gotoed points_info = points_info.gotoed
319
320  let loop_points points_info = points_info.loop_points
321
322  let mem_gotoed to_id points_info = IntMap.mem to_id (gotoed points_info)
323
324  let find_gotoed to_id points_info = IntMap.find to_id (gotoed points_info)
325
326  let add_gotoed to_id to_from_ids points_info =
327    let gotoed = IntMap.add to_id to_from_ids (gotoed points_info) in
328    { points_info with gotoed }
329
330  let mem_loop_points loop_id points_info =
331    IntMap.mem loop_id (loop_points points_info)
332
333  let find_loop_points loop_id points_info =
334    IntMap.find loop_id (loop_points points_info)
335
336  let add_loop_points loop_id ids points_info =
337    let loop_points = IntMap.add loop_id ids (loop_points points_info) in
338    { points_info with loop_points }
339
340end
341
342module PointsInfos = struct
343
344  type t = PointsInfo.t Misc.String.Map.t
345
346  let empty = Misc.String.Map.empty
347
348  let mem = Misc.String.Map.mem
349
350  let add = Misc.String.Map.add
351
352  let find = Misc.String.Map.find
353
354  let add_gotoed fun_name to_id to_from_ids points_infos =
355    let points_info =
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   
360
361  let add_loop_points fun_name loop_id ids points_infos =
362    let points_info =
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   
367
368end
369
370class points_infos points_infos prj =
371object inherit Visitor.frama_c_copy prj as super
372
373  val mutable current_fun_name = ""
374
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
383        let to_from_ids =
384          if PointsInfo.mem_gotoed to_id points_info then
385            PointsInfo.find_gotoed to_id points_info
386          else IntSet.empty in
387        let to_from_ids = IntSet.add from_id to_from_ids in
388        points_infos :=
389          PointsInfos.add_gotoed current_fun_name to_id to_from_ids
390          !points_infos
391      | Cil_types.Loop (_, block, _, _, _) ->
392        let loop_id = stmt.Cil_types.sid in
393        let ids =
394          if PointsInfo.mem_loop_points loop_id points_info then
395            PointsInfo.find_loop_points loop_id points_info
396          else IntSet.empty in
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
402        points_infos :=
403          PointsInfos.add_loop_points current_fun_name loop_id ids !points_infos
404      | _ -> () in
405    Cil.DoChildren
406
407  method vfunc fundec =
408    current_fun_name <- fundec.Cil_types.svar.Cil_types.vname ;
409    points_infos :=
410      PointsInfos.add current_fun_name PointsInfo.empty !points_infos ;
411    Cil.DoChildren
412
413end
414
415let points_infos () =
416  let map = ref PointsInfos.empty in
417  let points_infos_prj =
418    File.create_project_from_visitor "points_infos" (new points_infos map) in
419  let f () = !map in
420  Project.on points_infos_prj f ()
421
422
423(*** Value (flat) domain extremes ***)
424
425module BotAndTop = struct
426
427  type t = Bot | Top
428
429  let compare = Pervasives.compare
430
431  let to_string = function
432    | Bot -> "bot"
433    | Top -> "top"
434
435  let to_cil_term _ = assert false (* should not be used *)
436
437  let top = ArithSig.A Top
438  let bot = ArithSig.A Bot
439
440  let neg = function
441    | Top -> top
442    | Bot -> bot
443
444  let addl a v = match a, v with
445    | Bot, _ | _, ArithSig.A Bot -> bot
446    | Top, _ -> top
447
448  let addr v a = addl a v
449
450  let minusl a v = match a, v with
451    | Bot, _ | _, ArithSig.A Bot -> bot
452    | Top, _ -> top
453
454  let minusr v a = match v, a with
455    | _, Bot | ArithSig.A Bot, _ -> bot
456    | _, Top -> top
457
458  let mull a v = match a, v with
459    | Bot, _ | _, ArithSig.A Bot -> bot
460    | _, ArithSig.Int 0 -> ArithSig.Int 0
461    | Top, _ -> top
462
463  let mulr v a = mull a v
464
465  let divl a v = match a, v with
466    | Bot, _ | _, ArithSig.A Bot | _, ArithSig.Int 0 -> bot
467    | Top, _ -> top
468
469  let divr v a = match v, a with
470    | _, Bot | ArithSig.A Bot, _ -> bot
471    | _, Top -> top
472
473  let modl a v = match a, v with
474    | Bot, _ | _, ArithSig.A Bot | _, ArithSig.Int 0 -> bot
475    | Top, _ -> top
476
477  let modr v a = match v, a with
478    | _, Bot | ArithSig.A Bot, _ -> bot
479    | _, Top -> top
480
481  let maxl a v = match a, v with
482    | Bot, _ | _, ArithSig.A Bot -> bot
483    | Top, _ -> top
484
485  let maxr v a = maxl a v
486
487  let lel a v = match a, v with
488    | Bot, _ -> true
489    | Top, ArithSig.A Top -> true
490    | Top, _ -> false
491
492  let ler v a = match v, a with
493    | _, Top -> true
494    | ArithSig.A Bot, Bot -> true
495    | _, Bot -> false
496
497  let ltl a v = match a, v with
498    | Bot, ArithSig.A Bot -> false
499    | Bot, _ -> true
500    | Top, _ -> false
501
502  let ltr v a = match v, a with
503    | ArithSig.A Top, Top -> false
504    | _, Top -> true
505    | _, Bot -> false
506
507  let gel a v = ler v a
508
509  let ger v a = lel a v
510
511  let gtl a v = ltr v a
512
513  let gtr v a = ltl a v
514
515  let compute v = v
516
517end
518
519
520(*** Arithmetic expressions flat domain ***)
521
522module ArithValDom = struct
523
524  include Arith.Make (BotAndTop)
525
526  let top = A BotAndTop.Top
527
528  let bot = A BotAndTop.Bot
529
530  let join v1 v2 = match v1, v2 with
531    | A BotAndTop.Bot, v | v, A BotAndTop.Bot -> v
532    | _ when v1 = v2 -> v1
533    | _ -> A BotAndTop.Top
534
535  let widen = join
536
537  let narrow v1 v2 = match v1, v2 with
538    | A BotAndTop.Top, A _ -> v1
539    | A BotAndTop.Top, _ -> v2
540    | _ -> v1
541
542  let f_is_concrete v subs_res =
543    let b = match v with
544      | A _ -> false
545      | _ -> true in
546    List.fold_left (&&) true (b :: subs_res)
547
548  let is_concrete v = fold f_is_concrete v
549
550  let add_list l = List.fold_left add (Int 0) l
551
552  let last_value rel _ exit_value increment =
553    let rel_added = of_int (if is_large rel then 0 else 1) in
554    let rel_op = if has_lower_type rel then minus else add in
555    add (rel_op exit_value rel_added) increment
556
557(*
558  let last_value rel init_value exit_value increment =
559    let (op1, v1, v2, v3) = match rel with
560      | Le -> (minus, exit_value, init_value, increment)
561      | Lt -> (add, init_value, exit_value, of_int 0)
562      | Ge -> (add, init_value, exit_value, increment)
563      | Gt -> (minus, exit_value, init_value, of_int 0) in
564    let res = minus v1 v2 in
565    let res = modulo res (abs increment) in
566    let res = op1 exit_value res in
567    add res v3
568*)
569
570  let iteration_nb init_value counter increment =
571    div (minus (of_var counter) init_value) increment
572
573end
574
575module Domain = ArithValDom
576
577
578(*** Abstract cost ***)
579
580module AbsCost = struct
581
582  include (Cost_value.Make (ArithValDom))
583
584end
585
586
587(*** Requirements for loop termination ***)
588
589module Require = struct
590
591  type t =
592      { relation : Domain.relation ;
593        init_value : Domain.t ;
594        exit_value : Domain.t ;
595        increment : Domain.t }
596
597  let compare = Pervasives.compare
598
599  let relation require = require.relation
600  let init_value require = require.init_value
601  let exit_value require = require.exit_value
602  let increment require = require.increment
603
604  let merge f require1 require2 =
605      (* each loop has a single condition relation *)
606    assert (relation require1 = relation require2) ;
607    { relation = relation require1 ;
608      init_value = f (init_value require1) (init_value require2) ;
609      exit_value = f (exit_value require1) (exit_value require2) ;
610      increment = f (increment require1) (increment require2) }
611
612  let join = merge Domain.join
613  let widen = merge Domain.widen
614  let narrow = merge Domain.narrow
615
616  let le require1 require2 =
617      (* each loop has a single condition relation *)
618    (relation require1 = relation require2) &&
619    (Domain.le (init_value require1) (init_value require2)) &&
620    (Domain.le (exit_value require1) (exit_value require2)) &&
621    (Domain.le (increment require1) (increment require2))
622
623  let make relation init_value exit_value increment =
624    { relation ; init_value ; exit_value ; increment }
625
626  let replace_vars replacements require =
627    let init_value = Domain.replace_vars replacements (init_value require) in
628    let exit_value = Domain.replace_vars replacements (exit_value require) in
629    let increment = Domain.replace_vars replacements (increment require) in
630    { require with init_value ; exit_value ; increment }
631
632  let to_string require =
633    Printf.sprintf "%s %s %s %s"
634      (Domain.string_of_relation (relation require))
635      (Domain.to_string (init_value require))
636      (Domain.to_string (exit_value require))
637      (Domain.to_string (increment require))
638
639end
640
641module Requires = struct
642
643  module M = Misc.Int.Map
644
645  type t = Require.t M.t
646
647  let empty = M.empty
648
649  let mem = M.mem
650
651  let find = M.find
652
653  let merge f =
654    let f_merge _ require1 require2 = match require1, require2 with
655      | None, None -> None
656      | Some require, None | None, Some require -> Some require
657      | Some require1, Some require2 -> Some (f require1 require2) in
658    M.merge f_merge
659
660  let join = merge Require.join
661  let widen = merge Require.widen
662  let narrow = merge Require.narrow
663
664  let le requires1 requires2 =
665    let f id require1 res =
666      res && (mem id requires2) && (Require.le require1 (find id requires2)) in
667    M.fold f requires1 true
668
669  let cardinal = M.cardinal
670
671  let fold f requires a =
672    let f' _ require a = f require a in
673    M.fold f' requires a
674
675  let add = M.add
676
677  let replace_vars replacements = M.map (Require.replace_vars replacements)
678
679  let to_string requires =
680    let f id require res =
681      Printf.sprintf "%s%d: %s\n%!" res id (Require.to_string require) in
682    M.fold f requires ""
683
684end
685
686
687(*** Point kind ***)
688
689module LoopInfo = struct
690
691  type t =
692      { tmp_loop : Cil_types.varinfo ;
693        counter : string ;
694        relation : Domain.relation ;
695        exit_exp : Cil_types.exp ;
696        increment : Cil_types.exp ;
697        prev_stmts : (Cil_types.stmt * int (* position *)) list ;
698        last_stmts : Cil_types.stmt list }
699
700  let tmp_loop loop_info = loop_info.tmp_loop
701
702  let counter loop_info = loop_info.counter
703
704  let relation loop_info = loop_info.relation
705
706  let exit_exp loop_info = loop_info.exit_exp
707
708  let increment loop_info = loop_info.increment
709
710  let prev_stmts loop_info = loop_info.prev_stmts
711
712  let last_stmts loop_info = loop_info.last_stmts
713
714  let make tmp_loop counter relation exit_exp increment prev_stmts last_stmts =
715    { tmp_loop ; counter ; relation ; exit_exp ; increment ;
716      prev_stmts ; last_stmts }
717
718
719end
720
721module PointKind = struct
722
723  type t =
724    | LoopStart of LoopInfo.t
725    | LoopExit of LoopInfo.t
726    | ULoopStart (* start of an unrecognized loop *)
727    | ULoopExit (* exit of an unrecognized loop *)
728    | RegularPoint
729
730  let is_recognized_loop_start = function
731    | LoopStart _ -> true
732    | _ -> false
733
734  let tmp_loop = function
735    | LoopStart loop_info -> LoopInfo.tmp_loop loop_info
736    | _ -> raise (Invalid_argument "PointKind.tmp_loop")
737
738end
739
740module PointKinds = struct
741
742  type t = PointKind.t IntMap.t
743
744  let empty = IntMap.empty
745  let add = IntMap.add
746  let mem = IntMap.mem
747  let find = IntMap.find
748  let fold = IntMap.fold
749  let dom point_kinds = List.map fst (IntMap.bindings point_kinds)
750
751  let mem_loop_start point point_kinds =
752    mem point point_kinds &&
753    (PointKind.is_recognized_loop_start (find point point_kinds))
754
755  let find_tmp_loop point point_kinds =
756    let error = Invalid_argument "PointKinds.find_tmp_loop" in
757    PointKind.tmp_loop (IntMap.error_find point point_kinds error)
758
759end
760
761
762(*** Fun infos ***)
763
764module FunInfo = struct
765
766  type local_vars = (Cil_types.varinfo * string) list * Cil_types.varinfo list
767
768  type t =
769      { prototype : local_vars ;
770        (* exactly one start and one end points in Frama-C's CFG *)
771        start_and_end_points : (int * int) option ;
772        nb_loops : int ;
773        point_kinds : PointKinds.t }
774
775  let empty =
776    { prototype = ([], []) ; start_and_end_points = None ; nb_loops = 0 ;
777      point_kinds = PointKinds.empty }
778
779  let make formals locals nb_loops start_and_end_points point_kinds =
780    { prototype = (formals, locals) ;
781      nb_loops ; start_and_end_points ; point_kinds }
782
783  let prototype fun_info =
784    List.map (fun (x, _) -> x.Cil_types.vname) (fst fun_info.prototype)
785
786  let start_and_end_points fun_info = fun_info.start_and_end_points
787
788  let formals_and_locals fun_info = fun_info.prototype
789
790  let point_kinds fun_info = fun_info.point_kinds
791
792  let mem_point point fun_info = PointKinds.mem point fun_info.point_kinds
793
794  let find_point point fun_info = PointKinds.find point fun_info.point_kinds
795
796  let points fun_info = PointKinds.dom fun_info.point_kinds
797
798  let nb_loops fun_info = fun_info.nb_loops
799
800  let add_nb_loops fun_info =
801    let nb_loops = fun_info.nb_loops + 1 in
802    { fun_info with nb_loops }
803
804  let mem_loop_start point fun_info =
805    PointKinds.mem_loop_start point fun_info.point_kinds
806
807  let find_tmp_loop point fun_info =
808    PointKinds.find_tmp_loop point fun_info.point_kinds
809
810end
811
812module FunInfos = struct
813
814  type t = FunInfo.t Misc.String.Map.t
815
816  let empty = Misc.String.Map.empty
817
818  let prototypes = Misc.String.Map.map FunInfo.prototype
819
820  let mem = Misc.String.Map.mem
821
822  let add
823      fun_name formals locals nb_loops start_and_end_points point_kinds
824      fun_infos =
825    let fun_info =
826      FunInfo.make formals locals nb_loops start_and_end_points point_kinds in
827    Misc.String.Map.add fun_name fun_info fun_infos
828
829  let start_and_end_points fun_name fun_infos =
830    let error = Invalid_argument "FunInfos.start_and_end_points" in
831    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
832    FunInfo.start_and_end_points fun_info
833
834  let formals_and_locals fun_name fun_infos =
835    let error = Invalid_argument "FunInfos.formals_and_locals" in
836    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
837    FunInfo.formals_and_locals fun_info
838
839  let mem_point fun_name point fun_infos =
840    Misc.String.Map.mem fun_name fun_infos &&
841    FunInfo.mem_point point (Misc.String.Map.find fun_name fun_infos)
842
843  let find_point fun_name point fun_infos =
844    FunInfo.find_point point (Misc.String.Map.find fun_name fun_infos)
845
846  let points fun_name fun_infos =
847    let error = Invalid_argument "FunInfos.points" in
848    FunInfo.points (Misc.String.Map.error_find fun_name fun_infos error)
849
850  let nb_loops fun_name fun_infos =
851    let error = Invalid_argument "FunInfos.nb_loops" in
852    FunInfo.nb_loops (Misc.String.Map.error_find fun_name fun_infos error)
853
854  let add_nb_loops fun_name fun_infos =
855    let error = Invalid_argument "FunInfos.add_nb_loops" in
856    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
857    let fun_info = FunInfo.add_nb_loops fun_info in
858    Misc.String.Map.add fun_name fun_info fun_infos
859
860  let mem_loop_start fun_name point fun_infos =
861    Misc.String.Map.mem fun_name fun_infos &&
862    FunInfo.mem_loop_start point (Misc.String.Map.find fun_name fun_infos)
863
864  let find_tmp_loop fun_name point fun_infos =
865    let error = Invalid_argument "FunInfos.find_tmp_loop" in
866    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
867    FunInfo.find_tmp_loop point fun_info
868
869  let point_kinds fun_name fun_infos =
870    let error = Invalid_argument "FunInfos.point_kinds" in
871    let fun_info = Misc.String.Map.error_find fun_name fun_infos error in
872    FunInfo.point_kinds fun_info
873
874end
875
876
877(*** Static environment ***)
878
879module StaticEnv = struct
880
881  type t =
882      { fname : string ;
883        f_old_name : string ;
884        cost_id : string ;
885        cost_incr : string ;
886        cost_varinfo : Cil_types.varinfo ;
887        fun_infos : FunInfos.t ;
888        globals : Misc.String.Set.t ;
889        extern_costs : string Misc.String.Map.t }
890
891  let init fname f_old_name cost_id cost_incr extern_costs =
892    { fname ; f_old_name ; cost_id ; cost_incr ; cost_varinfo = dummy_varinfo ;
893      fun_infos = FunInfos.empty ;
894      globals = Misc.String.Set.empty ; extern_costs }
895
896  let fname static_env = static_env.fname
897
898  let f_old_name static_env = static_env.f_old_name
899
900  let prototypes static_env = FunInfos.prototypes static_env.fun_infos
901
902  let add_fun_infos
903      fun_name formals locals nb_loops start_and_end_points point_kinds
904      static_env =
905    let fun_infos =
906      FunInfos.add fun_name formals locals nb_loops start_and_end_points
907        point_kinds static_env.fun_infos in
908    { static_env with fun_infos }
909
910  let globals static_env = static_env.globals
911
912  let add_globals x static_env =
913    let globals = Misc.String.Set.add x (globals static_env) in
914    { static_env with globals }
915
916  let formals_and_locals fun_name static_env =
917    FunInfos.formals_and_locals fun_name static_env.fun_infos
918
919  let locals fun_name static_env = snd (formals_and_locals fun_name static_env)
920  let formals fun_name static_env = fst (formals_and_locals fun_name static_env)
921
922  let is_local fun_name x static_env =
923    let f varinfo = varinfo.Cil_types.vname = x in
924    List.exists f (locals fun_name static_env)
925
926  let is_formal fun_name x static_env =
927    let (formals, locals) = formals_and_locals fun_name static_env in
928    let f_local varinfo = varinfo.Cil_types.vname <> x in
929    let f_formal (varinfo, _) = varinfo.Cil_types.vname = x in
930    (List.for_all f_local locals) && (List.exists f_formal formals)
931
932  let is_global fun_name x static_env =
933    let (formals, locals) = formals_and_locals fun_name static_env in
934    let f_local varinfo = varinfo.Cil_types.vname <> x in
935    let f_formal (varinfo, _) = varinfo.Cil_types.vname <> x in
936    (List.for_all f_local locals) && (List.for_all f_formal formals) &&
937    (Misc.String.Set.mem x (globals static_env))
938
939  let cost_id static_env = static_env.cost_id
940
941  let cost_varinfo static_env = static_env.cost_varinfo
942
943  let cost_incr static_env = static_env.cost_incr
944
945  let set_cost_varinfo cost_varinfo static_env =
946    { static_env with cost_varinfo }
947
948  let mem_point fun_name point static_env =
949    FunInfos.mem_point fun_name point static_env.fun_infos
950
951  let find_point fun_name point static_env =
952    FunInfos.find_point fun_name point static_env.fun_infos
953
954  let extern_costs static_env = static_env.extern_costs
955
956  let start_and_end_points fun_name static_env =
957    FunInfos.start_and_end_points fun_name static_env.fun_infos
958
959  let mem_fun_name fun_name static_env =
960    FunInfos.mem fun_name static_env.fun_infos
961
962  let points fun_name static_env =
963    FunInfos.points fun_name static_env.fun_infos
964
965  let nb_loops fun_name static_env =
966    FunInfos.nb_loops fun_name static_env.fun_infos
967
968  let add_nb_loops fun_name static_env =
969    let fun_infos = FunInfos.add_nb_loops fun_name static_env.fun_infos in
970    { static_env with fun_infos }
971
972  let mem_loop_start fun_name point static_env =
973    FunInfos.mem_loop_start fun_name point static_env.fun_infos
974
975  let find_tmp_loop fun_name point static_env =
976    FunInfos.find_tmp_loop fun_name point static_env.fun_infos
977
978  let point_kinds fun_name static_env =
979    FunInfos.point_kinds fun_name static_env.fun_infos
980
981end
982
983
984(*** Initializations ***)
985
986let special_point f body = match f body with
987  | None -> None
988  | Some stmt -> Some stmt.Cil_types.sid
989
990let start_point = special_point first_stmt
991
992let end_point = special_point last_stmt
993
994let make_start_and_end_points start_point end_point =
995  match start_point, end_point with
996    | None, _ | _, None -> None
997    | Some start_point, Some end_point -> Some (start_point, end_point)
998
999let make_tmp_names formals =
1000  let f varinfo = (varinfo, GenName.concat varinfo.Cil_types.vname) in
1001  List.map f formals
1002
1003let rec extract_added_value counter e = match e.Cil_types.enode with
1004  | Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 ->
1005    Some (counter, e2)
1006  | Cil_types.BinOp (Cil_types.MinusA, e1, e2, typ)
1007      when exp_is_var counter e1 ->
1008    let enode = Cil_types.UnOp (Cil_types.Neg, e2, typ) in
1009    let e2 = { e2 with Cil_types.enode = enode } in
1010    Some (counter, e2)
1011  | Cil_types.CastE (_, e) -> extract_added_value counter e
1012  | _ ->
1013    if !debug then
1014      Format.printf
1015        "Could not find added increment value for counter %s in %a.\n%!"
1016        counter Cil.d_exp e ;
1017    None
1018
1019let extract_increment block =
1020  let open Misc.Option in
1021  last_stmt block >>=
1022  (fun stmt -> match stmt.Cil_types.skind with
1023    | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) ->
1024      extract_added_value v.Cil_types.vname e
1025    | _ ->
1026      if !debug then
1027        Format.printf
1028          "Could not find increment instruction; found %a instead.\n%!"
1029          Cil.d_stmt stmt ;
1030      None)
1031
1032let extract_guard block (counter, increment) =
1033  let open Misc.Option in
1034  first_stmt block >>=
1035  (fun stmt -> match stmt.Cil_types.skind with
1036    | Cil_types.If (e, _, block, _) when starts_with_break block ->
1037      (match e.Cil_types.enode with
1038        | Cil_types.BinOp (rel, e1, e2, _)
1039            when exp_is_var counter e1 && Domain.is_supported_rel rel ->
1040          Some (counter, Domain.rel_of_cil_binop rel, e2, increment)
1041        | Cil_types.BinOp (rel, e1, e2, _)
1042            when exp_is_var counter e2 && Domain.is_supported_rel rel ->
1043          let rel = Domain.rel_of_cil_binop rel in
1044          let rel = Domain.opposite rel in
1045          Some (counter, rel, e1, increment)
1046        | _ ->
1047          if !debug then
1048            Format.printf "Unsupported guard condition %a on counter %s.\n%!"
1049              Cil.d_exp e counter ;
1050          None)
1051    | Cil_types.If (_, _, block, _) ->
1052      if !debug then
1053        Format.printf "Loop not guarded by a break:\n%a\n%!" Cil.d_block block ;
1054      None
1055    | _ ->
1056      if !debug then Format.printf "Loop not guarded:\n%a\n%!" Cil.d_stmt stmt ;
1057      None)
1058
1059let add_point_kinds
1060    start_id loop_start_info last_stmts loop_exit_info point_kinds =
1061  let point_kinds = PointKinds.add start_id loop_start_info point_kinds in
1062  let f_last_stmts point_kinds stmt =
1063    PointKinds.add stmt.Cil_types.sid loop_exit_info point_kinds in
1064  List.fold_left f_last_stmts point_kinds last_stmts
1065
1066let add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds =
1067  match exps with
1068    | None ->
1069      let loop_start_info = PointKind.ULoopStart in
1070      let loop_exit_info = PointKind.ULoopExit in
1071      add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds
1072    | Some (counter, relation, exit_exp, increment) ->
1073      let loop_info =
1074        LoopInfo.make
1075          tmp_loop counter relation exit_exp increment prev_stmts last_stmts in
1076      let loop_start_info = PointKind.LoopStart loop_info in
1077      let loop_exit_info = PointKind.LoopExit loop_info in
1078      add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds
1079
1080let loop_exits loop_points body =
1081  let f_exists stmt = not (IntSet.mem stmt.Cil_types.sid loop_points) in
1082  let f stmt = List.exists f_exists stmt.Cil_types.succs in
1083  List.filter f (block_subs body)
1084
1085let stmt_point_kinds fundec points_info point_kinds stmt =
1086  let id = stmt.Cil_types.sid in
1087  match stmt.Cil_types.skind with
1088    | Cil_types.Loop (_, body, _, _, _) ->
1089      let open Misc.Option in
1090      assert (PointsInfo.mem_loop_points id points_info) ;
1091      let loop_points = PointsInfo.find_loop_points id points_info in
1092      let tmp_loop = GenName.fresh_varinfo fundec in
1093      let exps = extract_increment body >>= extract_guard body in
1094      let f_preds res pred =
1095        let pred_id = pred.Cil_types.sid in
1096        if IntSet.mem pred_id loop_points then res
1097        else
1098          let succs_id =
1099            List.map (fun stmt -> stmt.Cil_types.sid) pred.Cil_types.succs in
1100          let opt_pos = Misc.List.pos id succs_id in
1101          (* otherwise pred would not be a predecessor of the loop *)
1102          assert (opt_pos <> None) ;
1103          (pred, Misc.Option.extract opt_pos) :: res in
1104      let prev_stmts =
1105        List.fold_left f_preds [] stmt.Cil_types.preds in
1106      let last_stmts = loop_exits loop_points body in
1107      let last_stmts = match last_stmt body with
1108        | None -> last_stmts
1109        | Some last_stmt -> last_stmt :: last_stmts in
1110      add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds
1111    | _ when PointKinds.mem id point_kinds -> point_kinds
1112    | _ -> PointKinds.add id PointKind.RegularPoint point_kinds
1113
1114class initialize points_infos static_env prj =
1115object inherit Visitor.frama_c_copy prj as super
1116
1117  method vglob_aux glob =
1118    let _ = match glob with
1119      | Cil_types.GVarDecl (_, varinfo, _) when has_fun_type varinfo ->
1120        GenName.reset () ;
1121        GenName.set_prefix "__tmp" ;
1122        let fun_name = varinfo.Cil_types.vname in
1123        let formals = formals_of_varinfo varinfo in
1124        let formals = make_tmp_names formals in
1125        let locals = [] in
1126        let nb_loops = 0 in
1127        let start_and_end_points = None in
1128        let point_kinds = PointKinds.empty in
1129        static_env :=
1130          StaticEnv.add_fun_infos
1131          fun_name formals locals nb_loops start_and_end_points point_kinds
1132          !static_env
1133      | Cil_types.GFun (fundec, _) ->
1134        GenName.reset () ;
1135        GenName.set_prefix "__tmp" ;
1136        let fun_name = fundec.Cil_types.svar.Cil_types.vname in
1137        (* supposes a good initialization of [points_infos] *)
1138        assert (PointsInfos.mem fun_name points_infos) ;
1139        let points_info = PointsInfos.find fun_name points_infos in
1140        let formals = fundec.Cil_types.sformals in
1141        let formals = make_tmp_names formals in
1142        let locals = fundec.Cil_types.slocals in
1143        let nb_loops = 0 in
1144        let start_point = start_point fundec.Cil_types.sbody in
1145        let end_point = end_point fundec.Cil_types.sbody in
1146        let start_and_end_points =
1147          make_start_and_end_points start_point end_point in
1148        GenName.set_prefix "__tmp_loop" ;
1149        let point_kinds =
1150          List.fold_left (stmt_point_kinds fundec points_info) PointKinds.empty
1151            fundec.Cil_types.sallstmts in
1152        static_env :=
1153          StaticEnv.add_fun_infos
1154          fun_name formals locals nb_loops start_and_end_points point_kinds
1155          !static_env
1156      | Cil_types.GVar (varinfo, _, _)
1157          when varinfo.Cil_types.vname = StaticEnv.cost_id !static_env ->
1158        static_env := StaticEnv.set_cost_varinfo varinfo !static_env ;
1159        static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env
1160      | Cil_types.GVar (varinfo, _, _) | Cil_types.GVarDecl (_, varinfo, _) ->
1161        static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env
1162      | _ -> () in
1163    Cil.DoChildren
1164
1165end
1166
1167let initialize tmp_prefix fname f_old_name cost_id cost_incr extern_costs =
1168  let points_infos = points_infos () in
1169  GenName.set_prefix tmp_prefix ;
1170  let static_env_ref =
1171    ref (StaticEnv.init fname f_old_name cost_id cost_incr extern_costs) in
1172  let initialize_prj =
1173    File.create_project_from_visitor "initialize"
1174      (new initialize points_infos static_env_ref) in
1175  let f () = !static_env_ref in
1176  Project.on initialize_prj f ()
1177
1178
1179(*** Abstract domains and environments ***)
1180
1181module type DOMAIN = sig
1182  type t
1183  val of_int : int -> t
1184  val of_var : string -> t
1185  val top : t
1186  val bot : t
1187  val join : t -> t -> t
1188  val widen : t -> t -> t
1189  val narrow : t -> t -> t
1190  val le : t -> t -> bool
1191  val to_string : t -> string
1192  val neg : t -> t
1193  val add : t -> t -> t
1194  val minus : t -> t -> t
1195  val mul : t -> t -> t
1196  val div : t -> t -> t
1197  val modulo : t -> t -> t
1198end
1199
1200module type VARABSENV = sig
1201  module Domain : DOMAIN
1202  type t
1203  val bot       : t
1204  val top       : t
1205  val upd       : string -> Domain.t -> t -> t
1206  val find      : string -> t -> Domain.t
1207  val init      : Misc.String.Set.t -> (string * string) list -> t
1208  val join      : t -> t -> t
1209  val widen     : t -> t -> t
1210  val narrow    : t -> t -> t
1211  val le        : t -> t -> bool
1212  val to_string : t -> string
1213end
1214
1215module type ABSENV = sig
1216  module VarAbsEnv : VARABSENV
1217  module Domain : DOMAIN
1218  type t
1219  type addressed = Misc.String.Set.t
1220  val cost : t -> AbsCost.t
1221  val requires : t -> Requires.t
1222  val set_cost : t -> AbsCost.t -> t
1223  val add_cost : t -> AbsCost.t -> t
1224  val add_addressed : t -> addressed -> t
1225  val set_lval : t -> Cil_types.lval -> Domain.t -> t
1226  val top_vars : t -> Misc.String.Set.t -> t
1227  val find : string -> t -> Domain.t
1228  val bot : t
1229  val init : Misc.String.Set.t -> (string * string) list -> t
1230  val join : t -> t -> t
1231  val widen : t -> t -> t
1232  val narrow : t -> t -> t
1233  val le : t -> t -> bool
1234  val add_require : t -> int -> Require.t -> t
1235  val to_string : t -> string
1236end
1237
1238module MakeVarAbsEnv (D : DOMAIN) : VARABSENV with module Domain = D = struct
1239
1240  module Domain = D
1241
1242  type t = Domain.t Misc.String.CMap.t
1243
1244  let bot = Misc.String.CMap.empty D.bot
1245  let upd = Misc.String.CMap.upd
1246  let find = Misc.String.CMap.find
1247
1248  let init globals formals =
1249    let f x env = Misc.String.CMap.upd x D.top env in
1250    let env = Misc.String.Set.fold f globals bot in
1251    let f env (x, tmp) =
1252      let env = Misc.String.CMap.upd x (D.of_var tmp) env in
1253      Misc.String.CMap.upd tmp (D.of_var tmp) env in
1254    List.fold_left f env formals
1255
1256  let join = Misc.String.CMap.merge D.join
1257  let widen = Misc.String.CMap.merge D.widen
1258  let narrow = Misc.String.CMap.merge D.narrow
1259
1260  let top = Misc.String.CMap.empty D.top
1261
1262  let le env1 env2 =
1263    let f v1 v2 res = res && (Domain.le v1 v2) in
1264    Misc.String.CMap.cmp f env1 env2 true
1265
1266  let to_string =
1267    Misc.String.CMap.to_string (fun x -> x) (fun v -> (D.to_string v) ^ "\n")
1268
1269end
1270
1271module MakeAbsEnv (VAE : VARABSENV)
1272  : ABSENV with module VarAbsEnv = VAE
1273           and  module Domain = VAE.Domain = struct
1274
1275  module VarAbsEnv = VAE
1276  module Domain = VarAbsEnv.Domain
1277
1278  type addressed = Misc.String.Set.t
1279
1280  type t =
1281      { cost : AbsCost.t ; var_abs_env : VarAbsEnv.t ; addressed : addressed ;
1282        requires : Requires.t }
1283
1284  let init globals formals =
1285    let cost = AbsCost.bot in
1286    let var_abs_env = VarAbsEnv.init globals formals in
1287    let addressed = Misc.String.Set.empty in
1288    let requires = Requires.empty in
1289    { cost ; var_abs_env ; addressed ; requires }
1290
1291  let cost env = env.cost
1292
1293  let requires env = env.requires
1294
1295  let var_abs_env env = env.var_abs_env
1296
1297  let find x env = VarAbsEnv.find x (var_abs_env env)
1298
1299  let set_cost env cost = { env with cost }
1300
1301  let add_cost env cost = { env with cost = AbsCost.add env.cost cost }
1302
1303  let addressed env = env.addressed
1304
1305  let add_addressed env addressed =
1306    { env with addressed = Misc.String.Set.union env.addressed addressed }
1307
1308  let set_lval env lval v = match fst lval with
1309    | Cil_types.Var x ->
1310      let var_abs_env = VarAbsEnv.upd x.Cil_types.vname v env.var_abs_env in
1311      { env with var_abs_env }
1312    | _ -> env
1313
1314  let top_vars env vars =
1315    let f x var_abs_env = VarAbsEnv.upd x Domain.top var_abs_env in
1316    let var_abs_env = Misc.String.Set.fold f vars env.var_abs_env in
1317    { env with var_abs_env }
1318
1319  let bot =
1320    { cost = AbsCost.bot ; var_abs_env = VarAbsEnv.bot ;
1321      addressed = Misc.String.Set.empty ; requires = Requires.empty }
1322
1323  let join env1 env2 =
1324    { cost = AbsCost.join (cost env1) (cost env2) ;
1325      var_abs_env = VarAbsEnv.join (var_abs_env env1) (var_abs_env env2) ;
1326      addressed = Misc.String.Set.union (addressed env1) (addressed env2) ;
1327      requires = Requires.join (requires env1) (requires env2) }
1328
1329  let widen env1 env2 =
1330    { cost = AbsCost.widen (cost env1) (cost env2) ;
1331      var_abs_env = VarAbsEnv.widen (var_abs_env env1) (var_abs_env env2) ;
1332      addressed = Misc.String.Set.union (addressed env1) (addressed env2) ;
1333      requires = Requires.widen (requires env1) (requires env2) }
1334
1335  let narrow env1 env2 =
1336    { cost = AbsCost.narrow (cost env1) (cost env2) ;
1337      var_abs_env = VarAbsEnv.narrow (var_abs_env env1) (var_abs_env env2) ;
1338      addressed = addressed env1 ;
1339      requires = Requires.narrow (requires env1) (requires env2) }
1340
1341  let le env1 env2 =
1342    (AbsCost.le (cost env1) (cost env2)) &&
1343    (VarAbsEnv.le (var_abs_env env1) (var_abs_env env2)) &&
1344    (Misc.String.Set.is_subset (addressed env1) (addressed env2)) &&
1345    (Requires.le (requires env1) (requires env2))
1346
1347  let add_require env id require =
1348    { env with requires = Requires.add id require (requires env) }
1349
1350  let to_string env =
1351    let f_addressed x res = res ^ x ^ " " in
1352    "Cost: " ^ (AbsCost.to_string (cost env)) ^ "\n" ^
1353    "Var env:\n" ^ (VarAbsEnv.to_string (var_abs_env env)) ^
1354    "Addressed: " ^ (Misc.String.Set.fold f_addressed (addressed env) "") ^
1355    "\n" ^
1356    "Requires:\n" ^ (Requires.to_string (requires env)) ^ "\n"
1357
1358end
1359
1360module MakePointsAbsEnv (AE : ABSENV) = struct
1361
1362  module AbsEnv = AE
1363  module Domain = AbsEnv.Domain
1364
1365  type t =
1366      { abs_env : AbsEnv.t IntCMap.t }
1367
1368  let empty = { abs_env = IntCMap.empty AbsEnv.bot }
1369  let bot = empty
1370
1371  let abs_env env = env.abs_env
1372
1373  let find point env = IntCMap.find point env.abs_env
1374
1375  let add point abs_env env =
1376    let abs_env = IntCMap.upd point abs_env env.abs_env in
1377    { abs_env }
1378
1379  let le env1 env2 =
1380    let cmp abs_env1 abs_env2 res = res && (AbsEnv.le abs_env1 abs_env2) in
1381    IntCMap.cmp cmp (abs_env env1) (abs_env env2) true
1382
1383  let cost point env = AbsEnv.cost (find point env)
1384
1385  let requires point env = AbsEnv.requires (find point env)
1386
1387  let init start_point globals formals =
1388    add start_point (AbsEnv.init globals formals) empty
1389
1390  let to_string env =
1391    IntCMap.to_string string_of_int AbsEnv.to_string (abs_env env)
1392
1393  let widen env1 env2 =
1394    let abs_env = IntCMap.merge AbsEnv.widen (abs_env env1) (abs_env env2) in
1395    { abs_env }
1396
1397  let narrow env1 env2 =
1398    let abs_env = IntCMap.merge AbsEnv.narrow (abs_env env1) (abs_env env2) in
1399    { abs_env }
1400
1401  let set_cost id cost env = add id (AbsEnv.set_cost (find id env) cost) env
1402
1403end
1404
1405
1406module PointsAbsEnv = struct
1407
1408  module D = Domain
1409
1410  module VAE = MakeVarAbsEnv (D)
1411
1412  module AE = MakeAbsEnv (VAE)
1413
1414  include MakePointsAbsEnv (AE)
1415
1416end
1417
1418module AbsEnv  = PointsAbsEnv.AbsEnv
1419
1420
1421(*** Dependent cost results ***)
1422
1423module LoopAnnotInfo = struct
1424
1425  type t =
1426      { counter : string ;
1427        relation : Domain.relation ;
1428        init_value : Domain.t ;
1429        exit_value : Domain.t ;
1430        increment : Domain.t ;
1431        last_value : Domain.t ;
1432        cost_id : string ;
1433        tmp_loop : string ;
1434        iteration_nb : Domain.t ;
1435        body_cost : AbsCost.t }
1436
1437  let counter loop_annot_info = loop_annot_info.counter
1438
1439  let relation loop_annot_info = loop_annot_info.relation
1440
1441  let init_value loop_annot_info = loop_annot_info.init_value
1442
1443  let exit_value loop_annot_info = loop_annot_info.exit_value
1444
1445  let increment loop_annot_info = loop_annot_info.increment
1446
1447  let last_value loop_annot_info = loop_annot_info.last_value
1448
1449  let cost_id loop_annot_info = loop_annot_info.cost_id
1450
1451  let tmp_loop loop_annot_info = loop_annot_info.tmp_loop
1452
1453  let iteration_nb loop_annot_info = loop_annot_info.iteration_nb
1454
1455  let body_cost loop_annot_info = loop_annot_info.body_cost
1456
1457  let make
1458      counter relation init_value exit_value increment last_value cost_id
1459      tmp_loop iteration_nb body_cost =
1460    { counter ; relation ; init_value ; exit_value ; increment ; last_value ;
1461      cost_id ; tmp_loop ; iteration_nb ; body_cost }
1462
1463end
1464
1465module LoopAnnot = struct
1466
1467  type t =
1468    | Variant of Domain.t
1469    | CounterMod of Domain.t * Domain.t
1470    | CounterLastValue of
1471        string * Domain.relation * Domain.t * Domain.t * Domain.t
1472    | NoIteration of string * Domain.relation * Domain.t * Domain.t
1473    | Cost of string * string * Domain.t * AbsCost.t
1474
1475  let reduce prototypes costs = function
1476    | Cost (cost_id, tmp_loop, iteration_nb, body_cost) ->
1477      let body_cost = AbsCost.reduce prototypes costs body_cost in
1478      Cost (cost_id, tmp_loop, iteration_nb, body_cost)
1479    | v -> v
1480
1481  let compare = Pervasives.compare
1482
1483  let variant_to_cil v =
1484    if Domain.is_concrete v then Some (mk_variant (Domain.to_cil_term v))
1485    else None
1486
1487  let counter_mod_to_cil v1 v2 =
1488    if Domain.is_concrete v1 && Domain.is_concrete v2 then
1489      if v1 = v2 then None
1490      else
1491        let v1 = Domain.to_cil_term v1 in
1492        let v2 = Domain.to_cil_term v2 in
1493        let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
1494        Some (mk_invariant invariant)
1495    else None
1496
1497  let counter_last_value_to_cil counter rel init_value exit_value last_value =
1498    if Domain.is_concrete init_value &&
1499       Domain.is_concrete exit_value &&
1500       Domain.is_concrete last_value then
1501      let init_value = Domain.to_cil_term init_value in
1502      let exit_value = Domain.to_cil_term exit_value in
1503      let last_value = Domain.to_cil_term last_value in
1504      let rel' = Domain.cil_rel_of_rel rel in
1505      let require = Logic_const.prel (rel', init_value, exit_value) in
1506      let rel' = Domain.cil_rel_of_rel (Domain.mk_large rel) in
1507      let counter = cil_logic_int_var counter in
1508      let prop = Logic_const.prel (rel', counter, last_value) in
1509      let invariant = Logic_const.pimplies (require, prop) in
1510      Some (mk_invariant invariant)
1511    else None
1512
1513  let no_iteration_to_cil counter rel init_value exit_value =
1514    if Domain.is_concrete init_value && Domain.is_concrete exit_value then
1515      let rel = Domain.opposite rel in
1516      let rel' = Domain.cil_rel_of_rel rel in
1517      let init_value = Domain.to_cil_term init_value in
1518      let exit_value = Domain.to_cil_term exit_value in
1519      let require = Logic_const.prel (rel', init_value, exit_value) in
1520      let counter = cil_logic_int_var counter in
1521      let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in
1522      let invariant = Logic_const.pimplies (require, prop) in
1523      Some (mk_invariant invariant)
1524    else None
1525
1526  let cost_to_cil cost_id tmp_loop iteration_nb body_cost =
1527    if Domain.is_concrete iteration_nb && AbsCost.is_concrete body_cost then
1528      let cost_var = cil_logic_int_var cost_id in
1529      let body_cost = AbsCost.to_ext body_cost in
1530      let loop_cost = Domain.mul iteration_nb body_cost in
1531      let cost = Domain.add (Domain.of_var tmp_loop) loop_cost in
1532      if Domain.is_concrete cost then
1533        let cost = Domain.to_cil_term cost in
1534        let invariant = Logic_const.prel (Cil_types.Rle, cost_var, cost) in
1535        Some (mk_invariant invariant)
1536      else None
1537    else None
1538
1539  let to_cil = function
1540    | Variant v -> variant_to_cil v
1541    | CounterMod (v1, v2) -> counter_mod_to_cil v1 v2
1542    | CounterLastValue(counter, rel, init_value, exit_value, last_value) ->
1543      counter_last_value_to_cil counter rel init_value exit_value last_value
1544    | NoIteration (counter, rel, init_value, exit_value) ->
1545      no_iteration_to_cil counter rel init_value exit_value
1546    | Cost (cost_id, tmp_loop, iteration_nb, body_cost) ->
1547      cost_to_cil cost_id tmp_loop iteration_nb body_cost
1548
1549  let make_variant loop_annot_info =
1550    let rel = LoopAnnotInfo.relation loop_annot_info in
1551    let counter = LoopAnnotInfo.counter loop_annot_info in
1552    let last_value = LoopAnnotInfo.last_value loop_annot_info in
1553    let counter_var = Domain.of_var counter in
1554    let (v1, v2) = match rel with
1555      | Domain.Lt | Domain.Le -> (last_value, counter_var)
1556      | Domain.Gt | Domain.Ge -> (counter_var, last_value) in
1557    Variant (Domain.minus v1 v2)
1558
1559  let make_counter_mod loop_annot_info =
1560    let counter = LoopAnnotInfo.counter loop_annot_info in
1561    let init_value = LoopAnnotInfo.init_value loop_annot_info in
1562    let increment = LoopAnnotInfo.increment loop_annot_info in
1563    let mk_value value = Domain.modulo value (Domain.abs increment) in
1564    let v1 = mk_value (Domain.of_var counter) in
1565    let v2 = mk_value init_value in
1566    CounterMod (v1, v2)
1567
1568  let make_counter_last_value loop_annot_info =
1569    let counter = LoopAnnotInfo.counter loop_annot_info in
1570    let rel = LoopAnnotInfo.relation loop_annot_info in
1571    let init_value = LoopAnnotInfo.init_value loop_annot_info in
1572    let exit_value = LoopAnnotInfo.exit_value loop_annot_info in
1573    let last_value = LoopAnnotInfo.last_value loop_annot_info in
1574    CounterLastValue (counter, rel, init_value, exit_value, last_value)
1575
1576  let make_no_iteration loop_annot_info =
1577    let counter = LoopAnnotInfo.counter loop_annot_info in
1578    let rel = LoopAnnotInfo.relation loop_annot_info in
1579    let init_value = LoopAnnotInfo.init_value loop_annot_info in
1580    let exit_value = LoopAnnotInfo.exit_value loop_annot_info in
1581    NoIteration (counter, rel, init_value, exit_value)
1582
1583  let make_cost loop_annot_info =
1584    let cost_id = LoopAnnotInfo.cost_id loop_annot_info in
1585    let tmp_loop = LoopAnnotInfo.tmp_loop loop_annot_info in
1586    let iteration_nb = LoopAnnotInfo.iteration_nb loop_annot_info in
1587    let body_cost = LoopAnnotInfo.body_cost loop_annot_info in
1588    Cost (cost_id, tmp_loop, iteration_nb, body_cost)
1589
1590end
1591
1592module LoopAnnots = struct
1593
1594  include Eset.Make (LoopAnnot)
1595
1596  let make loop_annot_info =
1597    let variant = LoopAnnot.make_variant loop_annot_info in
1598    (* let counter_mod = LoopAnnot.make_counter_mod loop_annot_info in *)
1599    let counter_last_value =
1600      LoopAnnot.make_counter_last_value loop_annot_info in
1601    let no_iteration = LoopAnnot.make_no_iteration loop_annot_info in
1602    let cost = LoopAnnot.make_cost loop_annot_info in
1603    of_list [variant ; (* counter_mod ; *)
1604             counter_last_value ; no_iteration ; cost]
1605
1606  let to_cil loop_annots =
1607    let f loop_annot res = match LoopAnnot.to_cil loop_annot with
1608      | Some loop_annot -> loop_annot :: res
1609      | None -> res in
1610    fold f loop_annots []
1611
1612  let reduce prototypes costs loop_annots =
1613    let f loop_annot res =
1614      add (LoopAnnot.reduce prototypes costs loop_annot) res in
1615    fold f loop_annots empty
1616
1617end
1618
1619module LoopsAnnots = struct
1620
1621  type t = LoopAnnots.t IntMap.t
1622
1623  let empty = IntMap.empty
1624
1625  let mem = IntMap.mem
1626
1627  let find = IntMap.find
1628
1629  let add = IntMap.add
1630
1631  let to_cil loops_annots =
1632    IntMap.map LoopAnnots.to_cil loops_annots
1633
1634  let reduce prototypes costs loops_annots =
1635    IntMap.map (LoopAnnots.reduce prototypes costs) loops_annots
1636
1637end
1638
1639module CostInfo = struct
1640
1641  type t = { cost : AbsCost.t ; requires : Requires.t ;
1642             loops_annots : LoopsAnnots.t }
1643
1644  let cost cost_info = cost_info.cost
1645
1646  let requires cost_info = cost_info.requires
1647
1648  let make cost requires loops_annots = { cost ; requires ; loops_annots }
1649
1650  let set_cost cost_info cost = { cost_info with cost }
1651
1652  let init cost =
1653    { cost ; requires = Requires.empty ; loops_annots = LoopsAnnots.empty }
1654
1655  let loops_annots cost = cost.loops_annots
1656
1657  let mem_loop_annots id cost = LoopsAnnots.mem id (loops_annots cost)
1658
1659  let find_loop_annots id cost = LoopsAnnots.find id (loops_annots cost)
1660
1661  let to_string cost_info = AbsCost.to_string (cost cost_info)
1662
1663  let reduce_loops_annots prototypes costs cost_info =
1664    let loops_annots =
1665      LoopsAnnots.reduce prototypes costs cost_info.loops_annots in
1666    { cost_info with loops_annots }
1667
1668  let replace_vars replacements cost_info =
1669    let cost = AbsCost.replace_vars replacements (cost cost_info) in
1670    let requires = Requires.replace_vars replacements (requires cost_info) in
1671    { cost_info with cost ; requires }
1672
1673end
1674
1675module Costs = struct
1676
1677  type t = CostInfo.t Misc.String.Map.t
1678
1679  let empty = Misc.String.Map.empty
1680
1681  let init extern_costs =
1682    let f fun_name cost costs =
1683      let cost_info = CostInfo.init (AbsCost.of_extern cost) in
1684      Misc.String.Map.add fun_name cost_info costs in
1685    Misc.String.Map.fold f extern_costs empty
1686
1687  let mem = Misc.String.Map.mem
1688
1689  let add fun_name cost requires loops_annots costs =
1690    Misc.String.Map.add fun_name
1691      (CostInfo.make cost requires loops_annots) costs
1692
1693  let find_cost fun_name costs =
1694    CostInfo.cost (Misc.String.Map.find fun_name costs)
1695
1696  let find_requires fun_name costs =
1697    CostInfo.requires (Misc.String.Map.find fun_name costs)
1698
1699  let fun_costs = Misc.String.Map.map CostInfo.cost
1700
1701  let set_fun_costs costs fun_costs =
1702    let f fun_name cost_info =
1703      let cost =
1704        if Misc.String.Map.mem fun_name fun_costs then
1705          Misc.String.Map.find fun_name fun_costs
1706        else CostInfo.cost cost_info in
1707      CostInfo.set_cost cost_info cost in
1708    Misc.String.Map.mapi f costs
1709
1710  let fold = Misc.String.Map.fold
1711
1712  let to_string costs =
1713    let f fun_name cost_info res =
1714      res ^ "\n" ^ fun_name ^ ": " ^ (CostInfo.to_string cost_info) in
1715    fold f costs ""
1716
1717  let mem_loop_point fun_name id costs =
1718    (Misc.String.Map.mem fun_name costs) &&
1719    (CostInfo.mem_loop_annots id (Misc.String.Map.find fun_name costs))
1720
1721  let find_loop_annots fun_name id costs =
1722    let error = Invalid_argument "Costs.find_loop_annotations" in
1723    let fun_info = Misc.String.Map.error_find fun_name costs error in
1724    CostInfo.find_loop_annots id fun_info
1725
1726  let reduce_loops_annots prototypes costs =
1727    let fun_costs = fun_costs costs in
1728    Misc.String.Map.map
1729      (CostInfo.reduce_loops_annots prototypes fun_costs) costs
1730
1731  let restore_formals static_env costs =
1732    let f fun_name cost_info =
1733      if StaticEnv.mem_fun_name fun_name static_env then
1734        let formals = StaticEnv.formals fun_name static_env in
1735        let f (formal, tmp) = (tmp, Domain.of_var formal.Cil_types.vname) in
1736        let replacements = Misc.String.Map.of_list (List.map f formals) in
1737        CostInfo.replace_vars replacements cost_info
1738      else cost_info in
1739    Misc.String.Map.mapi f costs
1740
1741end
1742
1743
1744(*** Abstract interpretation ***)
1745
1746module MakeAI (M : sig val static_env : StaticEnv.t end) = struct
1747
1748  let rec addressed e = match e.Cil_types.enode with
1749    | Cil_types.Const _ | Cil_types.SizeOf _ | Cil_types.SizeOfStr _
1750    | Cil_types.AlignOf _ ->
1751      Misc.String.Set.empty
1752    | Cil_types.Lval lval | Cil_types.AddrOf lval | Cil_types.StartOf lval ->
1753      lval_addressed lval
1754    | Cil_types.SizeOfE e | Cil_types.AlignOfE e | Cil_types.UnOp (_, e, _)
1755    | Cil_types.CastE (_, e) | Cil_types.Info (e, _) -> addressed e
1756    | Cil_types.BinOp (_, e1, e2, _) ->
1757      Misc.String.Set.union (addressed e1) (addressed e2)
1758
1759  and lhost_addressed = function
1760    | Cil_types.Var _ -> Misc.String.Set.empty
1761    | Cil_types.Mem e -> addressed e
1762
1763  and offset_addressed = function
1764    | Cil_types.Index (e, offset) ->
1765      Misc.String.Set.union (addressed e) (offset_addressed offset)
1766    | _ -> Misc.String.Set.empty
1767
1768  and lval_addressed (lhost, offset) =
1769    Misc.String.Set.union (lhost_addressed lhost) (offset_addressed offset)
1770
1771  let branch abs_env _ = [abs_env ; abs_env]
1772
1773  let abs_fun_of_unop = function
1774    | Cil_types.Neg -> Domain.neg
1775    | _ -> (fun _ -> Domain.top)
1776
1777  let abs_fun_of_binop = function
1778    | Cil_types.PlusA -> Domain.add
1779    | Cil_types.MinusA -> Domain.minus
1780    | Cil_types.Mult -> Domain.mul
1781    | Cil_types.Div -> Domain.div
1782    | Cil_types.Mod -> Domain.modulo
1783    | _ -> (fun _ _ -> Domain.top)
1784
1785  let rec exp abs_env e = match e.Cil_types.enode with
1786    | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
1787      Domain.of_int (Int64.to_int i)
1788    | Cil_types.Lval (Cil_types.Var varinfo, _) ->
1789      AbsEnv.find varinfo.Cil_types.vname abs_env
1790    | Cil_types.Info (e, _) -> exp abs_env e
1791    | Cil_types.UnOp (unop, e, _) ->
1792      abs_fun_of_unop unop (exp abs_env e)
1793    | Cil_types.BinOp (binop, e1, e2, _) ->
1794      abs_fun_of_binop binop (exp abs_env e1) (exp abs_env e2)
1795    | Cil_types.CastE (_, e) -> exp abs_env e (* TODO: maybe incorrect *)
1796    | _ -> Domain.top
1797
1798  let cost_incr_cost = function
1799    | e :: _ ->
1800      (match e.Cil_types.enode with
1801        | Cil_types.Const (Cil_types.CInt64 (i, _, _)) ->
1802          AbsCost.of_int (Int64.to_int i)
1803        | _ -> AbsCost.top)
1804    | _ -> AbsCost.top
1805
1806  let call_proc_cost fun_name abs_env sid f args =
1807    let f_add_addrd addrd e = Misc.String.Set.union addrd (addressed e) in
1808    let addrd = List.fold_left f_add_addrd Misc.String.Set.empty (f :: args) in
1809    let abs_env = AbsEnv.add_addressed abs_env addrd in
1810    let cost = match f.Cil_types.enode with
1811      | Cil_types.Lval (Cil_types.Var var, _)
1812          when var.Cil_types.vname = StaticEnv.cost_incr M.static_env ->
1813        cost_incr_cost args
1814      | Cil_types.Lval (Cil_types.Var var, _) ->
1815        AbsCost.of_fun_call
1816          fun_name sid var.Cil_types.vname (List.map (exp abs_env) args)
1817      | _ -> AbsCost.top in
1818    let vars_to_top =
1819      Misc.String.Set.union (StaticEnv.globals M.static_env) addrd in
1820    AbsEnv.add_cost (AbsEnv.top_vars abs_env vars_to_top) cost
1821
1822  let stmt fun_name abs_env stmt = match stmt.Cil_types.skind with
1823    | Cil_types.Return _ -> []
1824    | Cil_types.Goto _ | Cil_types.Break _ | Cil_types.Continue _
1825    | Cil_types.Loop _ | Cil_types.Block _ | Cil_types.Switch _
1826    | Cil_types.Instr (Cil_types.Skip _ | Cil_types.Code_annot _) -> [abs_env]
1827    | Cil_types.UnspecifiedSequence l -> make_list (List.length l) abs_env
1828    | Cil_types.If (e, _, _, _) -> branch abs_env e
1829    | Cil_types.Instr (Cil_types.Set (lval, e, _)) ->
1830      let addressed =
1831        Misc.String.Set.union (lval_addressed lval) (addressed e) in
1832      let v = exp abs_env e in
1833      let abs_env = AbsEnv.add_addressed abs_env addressed in
1834      [AbsEnv.set_lval abs_env lval v]
1835    | Cil_types.Instr (Cil_types.Call (None, f, args, _)) ->
1836      [call_proc_cost fun_name abs_env stmt.Cil_types.sid f args]
1837    | Cil_types.Instr (Cil_types.Call (Some lval, f, args, _)) ->
1838      let addressed = lval_addressed lval in
1839      let abs_env = AbsEnv.add_addressed abs_env addressed in
1840      let abs_env = call_proc_cost fun_name abs_env stmt.Cil_types.sid f args in
1841      [AbsEnv.set_lval abs_env lval Domain.top]
1842    | Cil_types.Instr (Cil_types.Asm _) -> raise ASM_unsupported
1843    | Cil_types.TryFinally _ | Cil_types.TryExcept _ -> raise Try_unsupported
1844
1845  let merge_succ_regular points_abs_env abs_env stmt =
1846    let id = stmt.Cil_types.sid in
1847    let abs_env' = PointsAbsEnv.find id points_abs_env in
1848    let abs_env' = AbsEnv.join abs_env abs_env' in
1849    PointsAbsEnv.add id abs_env' points_abs_env
1850
1851  let merge_succ_uloop_start src_id points_abs_env abs_env =
1852    let points_abs_env =
1853      PointsAbsEnv.set_cost src_id AbsCost.top points_abs_env in
1854    let abs_env = AbsEnv.set_cost abs_env (AbsCost.of_int 0) in
1855    merge_succ_regular points_abs_env abs_env
1856
1857  let prev_init_and_cost fun_name counter points_abs_env prev_stmts =
1858    let f (init_value, before_cost) (stmt_, pos) =
1859      let abs_env = PointsAbsEnv.find (stmt_.Cil_types.sid) points_abs_env in
1860      let abs_env = List.nth (stmt fun_name abs_env stmt_) pos in
1861      let init_value = Domain.join init_value (AbsEnv.find counter abs_env) in
1862      let before_cost = AbsCost.join before_cost (AbsEnv.cost abs_env) in
1863      (init_value, before_cost) in
1864    List.fold_left f (Domain.bot, AbsCost.bot) prev_stmts
1865
1866  let body_cost points_abs_env last_stmts =
1867    (* Exiting of a loop can only be done through a break or a goto or whatever,
1868       but certainly not with a cost increment instruction. Thus executing the
1869       last statements of a loop should not change the cost information, so its
1870       unnecessary when this is all we care about. *)
1871    let f res stmt =
1872      let id = stmt.Cil_types.sid in
1873      AbsCost.join res (AbsEnv.cost (PointsAbsEnv.find id points_abs_env)) in
1874    List.fold_left f AbsCost.bot last_stmts
1875
1876  let loop_cost fun_name id loop_info points_abs_env abs_env =
1877    let cost_id = StaticEnv.cost_id M.static_env in
1878    let tmp_loop = LoopInfo.tmp_loop loop_info in
1879    let counter = LoopInfo.counter loop_info in
1880    let relation = LoopInfo.relation loop_info in
1881    let prev_stmts = LoopInfo.prev_stmts loop_info in
1882    let last_stmts = LoopInfo.last_stmts loop_info in
1883    let (init_value, before_cost) =
1884      prev_init_and_cost fun_name counter points_abs_env prev_stmts in
1885    let exit_value = exp abs_env (LoopInfo.exit_exp loop_info) in
1886    let increment = exp abs_env (LoopInfo.increment loop_info) in
1887    let last_value =
1888      Domain.last_value relation init_value exit_value increment in
1889    let iteration_nb = Domain.iteration_nb init_value counter increment in
1890    let body_cost = body_cost points_abs_env last_stmts in
1891    let loop_cost =
1892      if AbsCost.is_top body_cost then AbsCost.top
1893      else
1894        AbsCost.of_loop_cost
1895          fun_name id relation init_value exit_value increment
1896          (AbsCost.extract body_cost) in
1897    let succ_loop_cost = AbsCost.add before_cost loop_cost in
1898    (counter, relation, init_value, exit_value, increment, last_value, cost_id,
1899     tmp_loop, iteration_nb, body_cost, succ_loop_cost)
1900
1901  let merge_succ_loop_start
1902      fun_name src_id loop_info points_abs_env points_abs_env' abs_env =
1903    let src_abs_env = PointsAbsEnv.find src_id points_abs_env in
1904    let (_, rel, init_value, exit_value, increment, _, _, _, _, _, _) =
1905      loop_cost fun_name src_id loop_info points_abs_env src_abs_env in
1906    let require = Require.make rel init_value exit_value increment in
1907    let abs_env = AbsEnv.add_require abs_env src_id require in
1908    merge_succ_uloop_start src_id points_abs_env' abs_env
1909
1910  let merge_succ_loop_exit
1911      fun_name loop_start_id loop_info points_abs_env points_abs_env'
1912      abs_env stmt =
1913    let start_abs_env = PointsAbsEnv.find loop_start_id points_abs_env in
1914    let (_, _, _, _, _, _, _, _, _, _, succ_loop_cost) =
1915      loop_cost fun_name loop_start_id loop_info points_abs_env start_abs_env
1916    in
1917    let abs_env = AbsEnv.set_cost abs_env succ_loop_cost in
1918    merge_succ_regular points_abs_env' abs_env stmt
1919
1920  let merge_succ_uloop_exit points_abs_env abs_env =
1921    let abs_env = AbsEnv.set_cost abs_env AbsCost.top in
1922    merge_succ_regular points_abs_env abs_env
1923
1924  let merge_succ fun_name src_id points_abs_env =
1925    if StaticEnv.mem_point fun_name src_id M.static_env then
1926      match StaticEnv.find_point fun_name src_id M.static_env with
1927        | PointKind.RegularPoint -> merge_succ_regular
1928        | PointKind.LoopStart loop_info ->
1929          merge_succ_loop_start fun_name src_id loop_info points_abs_env
1930        | PointKind.LoopExit loop_info ->
1931          merge_succ_loop_exit fun_name src_id loop_info points_abs_env
1932        | PointKind.ULoopStart -> merge_succ_uloop_start src_id
1933        | PointKind.ULoopExit -> merge_succ_uloop_exit
1934    else raise (Invalid_argument "AI.merge_succ")
1935
1936  let fundec_stmt fun_name points_abs_env points_abs_env' stmt_ =
1937    let id = stmt_.Cil_types.sid in
1938    let abs_env = PointsAbsEnv.find id points_abs_env in
1939    let abs_envs = stmt fun_name abs_env stmt_ in
1940    (* Otherwise the [stmt] function is not correct. *)
1941    assert (List.length abs_envs = List.length stmt_.Cil_types.succs) ;
1942    let f = merge_succ fun_name id points_abs_env in
1943    List.fold_left2 f points_abs_env' abs_envs stmt_.Cil_types.succs
1944
1945  let rec fundec_stmts fun_name points_abs_env cmp merge stmts =
1946    if !debug then
1947      Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env) ;
1948    let f = fundec_stmt fun_name points_abs_env in
1949    let points_abs_env' = List.fold_left f PointsAbsEnv.bot stmts in
1950    let points_abs_env' = merge points_abs_env points_abs_env' in
1951    if cmp points_abs_env' points_abs_env then
1952      (if !debug then
1953          Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env') ;
1954       points_abs_env')
1955    else fundec_stmts fun_name points_abs_env' cmp merge stmts
1956
1957  let fundec_stmts_widen fun_name points_abs_env =
1958    fundec_stmts fun_name points_abs_env PointsAbsEnv.le PointsAbsEnv.widen
1959
1960  let fundec_stmts_narrow fun_name points_abs_env =
1961    let cmp env1 env2 = PointsAbsEnv.le env2 env1 in
1962    fundec_stmts fun_name points_abs_env cmp PointsAbsEnv.narrow
1963
1964  let loop_annot_info fun_name id points_abs_env loop_info =
1965    let abs_env = PointsAbsEnv.find id points_abs_env in
1966    let (counter, relation, init_value, exit_value, last_value, increment,
1967         cost_id, tmp_loop, iteration_nb, body_cost, _) =
1968      loop_cost fun_name id loop_info points_abs_env abs_env in
1969    LoopAnnotInfo.make
1970      counter relation init_value exit_value last_value increment cost_id
1971      tmp_loop.Cil_types.vname iteration_nb body_cost
1972
1973  let loop_annots fun_name points_abs_env id point_kind loops_annots =
1974    match point_kind with
1975      | PointKind.LoopStart loop_info ->
1976        let loop_annot_info =
1977          loop_annot_info fun_name id points_abs_env loop_info in
1978        let loop_annots = LoopAnnots.make loop_annot_info in
1979        LoopsAnnots.add id loop_annots loops_annots
1980      | PointKind.ULoopStart ->
1981        let loop_annots = LoopAnnots.empty in
1982        LoopsAnnots.add id loop_annots loops_annots
1983      | _ -> loops_annots
1984
1985  let loops_annots fun_name points_abs_env =
1986    PointKinds.fold (loop_annots fun_name points_abs_env)
1987      (StaticEnv.point_kinds fun_name M.static_env) LoopsAnnots.empty
1988
1989end
1990
1991
1992(*** Dependent costs computation ***)
1993
1994class compute_costs widen narrow loops_annots static_env costs prj =
1995object inherit Visitor.frama_c_copy prj as super
1996
1997  method vfunc fundec =
1998    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
1999    if fun_name = StaticEnv.cost_incr static_env then begin
2000      costs := Costs.add fun_name AbsCost.top Requires.empty
2001        LoopsAnnots.empty !costs ;
2002      Cil.SkipChildren end
2003    else begin
2004      (* The function should be in the static environment because of the
2005         initializations. *)
2006      assert (StaticEnv.mem_fun_name fun_name static_env) ;
2007      let _ = match StaticEnv.start_and_end_points fun_name static_env with
2008        | None ->
2009          costs := Costs.add fun_name AbsCost.top Requires.empty
2010            LoopsAnnots.empty !costs
2011        | Some (start_point, end_point) ->
2012          if !debug then Printf.printf "Interpreting %s\n%!" fun_name ;
2013          let formals = StaticEnv.formals fun_name static_env in
2014          let f_formals (varinfo, tmp) = (varinfo.Cil_types.vname, tmp) in
2015          let globals = StaticEnv.globals static_env in
2016          let formals = List.map f_formals formals in
2017          let env = PointsAbsEnv.init start_point globals formals in
2018          if !debug then Printf.printf "WIDEN\n%!" ;
2019          let env = widen fun_name env fundec.Cil_types.sallstmts in
2020          if !debug then Printf.printf "NARROW\n%!" ;
2021          let env = narrow fun_name env fundec.Cil_types.sallstmts in
2022          let cost = PointsAbsEnv.cost end_point env in
2023          let requires = PointsAbsEnv.requires end_point env in
2024          let loops_annots = loops_annots fun_name env in
2025          (* The last instruction should be a return. Executing it shouldn't
2026             change the environment. *)
2027          costs := Costs.add fun_name cost requires loops_annots !costs in
2028      Cil.SkipChildren end
2029
2030end
2031
2032let compute_costs static_env =
2033  let module AI = MakeAI (struct let static_env = static_env end) in
2034  let costs = ref (Costs.init (StaticEnv.extern_costs static_env)) in
2035  let compute_costs_prj =       
2036    File.create_project_from_visitor
2037      "compute_costs"
2038      (new compute_costs AI.fundec_stmts_widen AI.fundec_stmts_narrow
2039         AI.loops_annots static_env costs) in
2040  let f () = !costs in
2041  Project.on compute_costs_prj f ()
2042
2043
2044(*** Costs solver ***)
2045
2046let solve_end costs1 costs2 =
2047  let f fun_name cost res =
2048    res && (Misc.String.Map.mem fun_name costs1) &&
2049      (cost = Misc.String.Map.find fun_name costs1) in
2050  Misc.String.Map.fold f costs2 true
2051
2052let string_of_fun_costs fun_costs =
2053  let f fun_name cost res =
2054    Printf.sprintf "%s%s: %s\n%!" res fun_name (AbsCost.to_string cost) in
2055  Misc.String.Map.fold f fun_costs ""
2056
2057let solve_costs static_env costs =
2058  let costs = Costs.restore_formals static_env costs in
2059  let fun_costs = Costs.fun_costs costs in
2060  let prototypes = StaticEnv.prototypes static_env in
2061  let rec aux fun_costs =
2062    if !debug then Printf.printf "%s\n%!" (string_of_fun_costs fun_costs) ;
2063    let fun_costs' = AbsCost.reduces prototypes fun_costs in
2064    if solve_end fun_costs fun_costs' then fun_costs
2065    else aux fun_costs' in
2066  let fun_costs = aux fun_costs in
2067  let costs = Costs.set_fun_costs costs fun_costs in
2068  Costs.reduce_loops_annots prototypes costs
2069
2070
2071(*** Add annotations ***)
2072
2073let add_tmp_loop_init cost_varinfo tmp_loop stmt =
2074  let lval = Cil.var tmp_loop in
2075  let e =
2076    Cil.new_exp dummy_location (Cil_types.Lval (Cil.var cost_varinfo)) in
2077  let new_stmt =
2078    Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
2079  let new_stmt = Cil.mkStmt new_stmt in
2080  Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))
2081
2082let make_tmp_formal_init fundec varinfo tmp_var =
2083  let tmp_var = Cil.makeTempVar fundec ~name:tmp_var varinfo.Cil_types.vtype in
2084  let lval = Cil.var tmp_var in
2085  let e = Cil.new_exp dummy_location (Cil_types.Lval (Cil.var varinfo)) in
2086  let new_stmt = Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
2087  Cil.mkStmt new_stmt
2088
2089let make_tmp_formals_init fundec l =
2090  let f (varinfo, tmp_var) = make_tmp_formal_init fundec varinfo tmp_var in
2091  List.map f l
2092
2093let add_tmp_formals_init formals fundec =
2094  let tmp_formals_init = make_tmp_formals_init fundec formals in
2095  let block = tmp_formals_init @ fundec.Cil_types.sbody.Cil_types.bstmts in
2096  let body = { fundec.Cil_types.sbody with Cil_types.bstmts = block } in
2097  { fundec with Cil_types.sbody = body }
2098
2099let make_require require =
2100  let rel = Require.relation require in
2101  let init_value = Require.init_value require in
2102  let exit_value = Require.exit_value require in
2103  let increment = Require.increment require in
2104  if Domain.is_concrete init_value &&
2105     Domain.is_concrete exit_value &&
2106     Domain.is_concrete increment then
2107    let zero = Domain.of_int 0 in
2108    let rel' = Domain.mk_strict rel in
2109    let cil_init_value = Domain.to_cil_term init_value in
2110    let cil_exit_value = Domain.to_cil_term exit_value in
2111    let cil_zero = Domain.to_cil_term zero in
2112    let cil_increment = Domain.to_cil_term increment in
2113    let cil_rel = Domain.cil_rel_of_rel rel in
2114    let cil_rel' = Domain.cil_rel_of_rel rel' in
2115    let t1 = Logic_const.prel (cil_rel, cil_init_value, cil_exit_value) in
2116    let t2 = Logic_const.prel (cil_rel', cil_zero, cil_increment) in
2117    let t3 = Logic_const.pimplies (t1, t2) in
2118    if Domain.bool_of_cond rel' zero increment then None
2119    else
2120      if Domain.bool_of_cond (Domain.opposite rel) init_value exit_value then
2121        None
2122      else
2123        if Domain.bool_of_cond rel init_value exit_value then Some t2
2124        else Some t3
2125  else None
2126
2127let make_requires requires =
2128  let f require res =
2129    let added_require = match make_require require with
2130    | None -> []
2131    | Some require -> [require] in
2132    added_require @ res in
2133  Requires.fold f requires []
2134
2135let add_spec pres post spec =
2136  let requires = List.map Logic_const.new_predicate pres in
2137  let post_cond = [(Cil_types.Normal, Logic_const.new_predicate post)] in
2138  let new_behavior = Cil.mk_behavior ~requires ~post_cond () in
2139  spec.Cil_types.spec_behavior <- new_behavior :: spec.Cil_types.spec_behavior
2140
2141let add_cost_annotation requires rel cost_id cost spec =
2142  let post = mk_fun_cost_pred rel cost_id cost in 
2143  add_spec (make_requires requires) post spec ;
2144  Cil.ChangeDoChildrenPost (spec, identity)
2145
2146let add_cost_incr_annotation cost_id fundec =
2147  let rel = Cil_types.Req in
2148  let cost =
2149    Logic_const.tvar (Cil_const.make_logic_var "incr" Cil_types.Linteger)  in
2150  add_cost_annotation Requires.empty rel cost_id cost fundec
2151
2152let add_regular_fun_annotation cost_id requires cost spec =
2153  if AbsCost.is_concrete cost then
2154    let cost = AbsCost.to_ext cost in
2155    let rel = Cil_types.Rle in
2156    if Domain.is_concrete cost then
2157      add_cost_annotation requires rel cost_id (Domain.to_cil_term cost) spec
2158    else Cil.DoChildren
2159  else Cil.DoChildren
2160
2161let add_fundec_annotation static_env costs fun_name spec =
2162  assert (Costs.mem fun_name costs) ;
2163  let cost = Costs.find_cost fun_name costs in
2164  let requires = Costs.find_requires fun_name costs in
2165  let cost_id = StaticEnv.cost_id static_env in
2166  let cost_incr = StaticEnv.cost_incr static_env in
2167  if fun_name = cost_incr then add_cost_incr_annotation cost_id spec
2168  else add_regular_fun_annotation cost_id requires cost spec
2169
2170class add_annotations static_env costs prj =
2171object (self) inherit Visitor.frama_c_copy prj as super
2172
2173  val mutable current_fun_name : string = ""
2174
2175  method vstmt_aux stmt = match stmt.Cil_types.skind with
2176    | Cil_types.Loop _
2177        when StaticEnv.mem_loop_start current_fun_name stmt.Cil_types.sid
2178          static_env ->
2179      let cost_varinfo = StaticEnv.cost_varinfo static_env in
2180      (* only use with costs correctly set and initialized *)
2181      assert (Costs.mem_loop_point current_fun_name stmt.Cil_types.sid costs) ;
2182      let tmp_loop =
2183        StaticEnv.find_tmp_loop current_fun_name stmt.Cil_types.sid
2184          static_env in
2185      let annots =
2186        Costs.find_loop_annots current_fun_name stmt.Cil_types.sid costs in
2187      add_loop_annots self stmt (LoopAnnots.to_cil annots) ;
2188      let change = add_tmp_loop_init cost_varinfo tmp_loop in
2189      Cil.ChangeDoChildrenPost (stmt, change)
2190    | _ -> Cil.DoChildren
2191
2192  method vfunc fundec =
2193    let fun_name = fundec.Cil_types.svar.Cil_types.vname in
2194    current_fun_name <- fun_name ;
2195    if fun_name = StaticEnv.cost_incr static_env then Cil.SkipChildren
2196    else
2197      let formals = StaticEnv.formals fun_name static_env in
2198      Cil.ChangeDoChildrenPost (fundec, add_tmp_formals_init formals)
2199
2200  method vspec spec = match self#current_kf with
2201    | None -> Cil.JustCopy 
2202    | Some kf ->
2203      match kf.Db_types.fundec with
2204        | Db_types.Definition (fundec, _) ->
2205          let fun_name = fundec.Cil_types.svar.Cil_types.vname in
2206          add_fundec_annotation static_env costs fun_name spec
2207        | Db_types.Declaration (_, f, _, _) ->
2208          let fun_name = f.Cil_types.vname in
2209          add_fundec_annotation static_env costs fun_name spec
2210
2211end
2212
2213let add_annotations static_env costs =
2214  let add_annotations_prj =     
2215    File.create_project_from_visitor
2216      "add_annotations" (new add_annotations static_env costs) in
2217  let f () =
2218    Parameters.CodeOutput.set (StaticEnv.fname static_env) ;
2219    File.pretty_ast () in
2220  Project.on add_annotations_prj f ()
2221
2222
2223(*** Save results ***)
2224
2225let save_results static_env costs =
2226  let fname = StaticEnv.f_old_name static_env in
2227  let f fun_name cost_info res =
2228    let cost = CostInfo.cost cost_info in
2229    res ^
2230      (if AbsCost.is_concrete cost then
2231          fun_name ^ " " ^ (Domain.to_string (AbsCost.to_ext cost)) ^ "\n"
2232       else "") in
2233  let s = Costs.fold f costs "" in
2234  let save_file =
2235    try Filename.chop_extension fname
2236    with Invalid_argument "Filename.chop_extension" -> fname in
2237  let save_file = save_file ^ ".cost_results" in
2238  try
2239    let oc = open_out save_file in
2240    output_string oc s ;
2241    close_out oc
2242  with Sys_error _ ->
2243    Printf.eprintf "Could not save plug-in results in file %s.\n%!" save_file
2244
2245
2246(*** Main ***)
2247
2248let cost ((fname, _), f_old_name, cost_id, cost_incr, extern_costs) =
2249  try
2250    Parameters.Files.set [fname] ;
2251    File.init_from_cmdline () ;
2252    if !debug then Printf.printf "Make CFG\n%!" ;
2253    make_CFG () ;
2254    if !debug then print_CFG () ;
2255    if !debug then Printf.printf "Initialize\n%!" ;
2256    let static_env =
2257      initialize "__tmp" fname f_old_name cost_id cost_incr extern_costs in
2258    if !debug then Printf.printf "Compute costs\n%!" ;
2259    let costs = compute_costs static_env in
2260    if !debug then Printf.printf "%s\n%!" (Costs.to_string costs) ;
2261    if !debug then Printf.printf "Solve costs\n%!" ;
2262    let costs = solve_costs static_env costs in
2263    if !debug then Printf.printf "Costs:\n%s\n%!" (Costs.to_string costs) ;
2264    if !debug then Printf.printf "Save results\n%!" ;
2265    save_results static_env costs ;
2266    if !debug then Printf.printf "Add annotations\n%!" ;
2267    add_annotations static_env costs
2268  with e -> Printf.eprintf "** ERROR: %s.\n%!" (string_of_exception e)
Note: See TracBrowser for help on using the repository browser.