← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to src/kernel/loop.ml

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/kernel/loop.ml
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  This file is part of Frama-C.                                         *)
 
4
(*                                                                        *)
 
5
(*  Copyright (C) 2007-2008                                               *)
 
6
(*    CEA (Commissariat � l'�nergie Atomique)                             *)
 
7
(*                                                                        *)
 
8
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
 
9
(*  Lesser General Public License as published by the Free Software       *)
 
10
(*  Foundation, version 2.1.                                              *)
 
11
(*                                                                        *)
 
12
(*  It is distributed in the hope that it will be useful,                 *)
 
13
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
 
14
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
 
15
(*  GNU Lesser General Public License for more details.                   *)
 
16
(*                                                                        *)
 
17
(*  See the GNU Lesser General Public License version 2.1                 *)
 
18
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
 
19
(*                                                                        *)
 
20
(**************************************************************************)
 
21
 
 
22
(* $Id: loop.ml,v 1.12 2008/10/03 13:09:16 uid568 Exp $ *)
 
23
 
 
24
open Cil_types
 
25
open Db_types
 
26
open Cilutil
 
27
open Cil
 
28
 
 
29
let name = "natural_loops"
 
30
 
 
31
module Natural_Loops =
 
32
  Kernel_function.Make_Table
 
33
    (Datatype.List
 
34
       (Datatype.Couple(Cil_datatype.Stmt)(Datatype.List(Cil_datatype.Stmt))))
 
35
    (struct
 
36
       let name = name
 
37
       let size = 97
 
38
       let dependencies = [ Cil_state.self ]
 
39
     end)
 
40
 
 
41
let pretty_natural_loops fmt kf loops =
 
42
  Format.fprintf fmt "Natural_loops for %s:@." (Kernel_function.get_name kf);
 
43
  List.iter
 
44
    (fun (start,members) ->
 
45
       Format.fprintf fmt "Loop start: %d ( " start.sid;
 
46
       List.iter (fun d -> Format.fprintf fmt "%d " d.sid) members;
 
47
       Format.fprintf fmt ")@\n";)
 
48
    loops
 
49
 
 
50
let get_naturals kf =
 
51
  let loops =
 
52
    Natural_Loops.memo
 
53
      (fun kf ->
 
54
         match kf.fundec with
 
55
         | Declaration _ ->
 
56
             []
 
57
         | Definition (cilfundec,_) ->
 
58
             let dbg = 
 
59
               Cmdline.Debug.get () > 0 || Cmdline.Pdg.Verbosity.get() > 0 
 
60
             in
 
61
             if dbg then
 
62
               Format.printf "COMPUTE NATURAL LOOPS FOR %S@." (Kernel_function.get_name kf);
 
63
             let dominators = Dominators.computeIDom cilfundec in
 
64
             (*if dbg then 
 
65
               Format.printf "DONE COMPUTE NATURAL LOOPS IDOM FOR %S@." 
 
66
                 (Kernel_function.get_name kf);*)
 
67
             let naturals = Dominators.findNaturalLoops cilfundec dominators in
 
68
             if dbg then begin
 
69
               Format.printf "DONE COMPUTE NATURAL LOOPS FOR %S@."
 
70
                 (Kernel_function.get_name kf);
 
71
               pretty_natural_loops Format.std_formatter kf naturals;
 
72
             end;
 
73
             naturals)
 
74
      kf
 
75
  in
 
76
  loops
 
77
 
 
78
let is_natural kf =
 
79
  let natural_loops =
 
80
    List.fold_left
 
81
      (fun acc (n,_) -> StmtSet.add n acc)
 
82
      StmtSet.empty
 
83
      (get_naturals kf)
 
84
  in
 
85
(* non natural loop over-approximation try:
 
86
  let can_reach = !stmt_can_reach kf in *)
 
87
  fun stmt -> let nat_loop = StmtSet.mem stmt natural_loops in
 
88
  nat_loop
 
89
(*  if nat_loop then nat_loop
 
90
  else
 
91
    if can_reach stmt stmt
 
92
    then true (* this is non natural loop or an imbricated loop... *)
 
93
    else false
 
94
*)
 
95
let back_edges kf stmt =
 
96
  if is_natural kf stmt then
 
97
    let rec lookup = function
 
98
      | [] -> assert false
 
99
      | (s, pred_s) :: sl -> if s.sid = stmt.sid then pred_s else lookup sl
 
100
    in
 
101
    lookup (get_naturals kf)
 
102
  else
 
103
    []
 
104
 
 
105
let while_for_natural_loop kf stmt =
 
106
  match stmt.skind with
 
107
  | Loop _ -> stmt
 
108
  | _ -> (* the while stmt is probably the non looping predecessor *)
 
109
      let be = back_edges kf stmt in
 
110
      Format.printf "Stmt:%d " stmt.sid;
 
111
      List.iter (fun x -> Format.printf "B_edge:%d " x.sid) be;
 
112
      List.iter (fun x -> Format.printf "Preds:%d " x.sid) stmt.preds;
 
113
      let non_looping_pred =
 
114
        List.filter (fun pred -> not (List.mem pred be)) stmt.preds 
 
115
      in
 
116
      match non_looping_pred with
 
117
      | [x] -> x
 
118
      | _ ->
 
119
          Format.eprintf "@.Lexical non natural loop detected !@.";
 
120
          assert false
 
121
 
 
122
let compute_allstmt_block block =
 
123
  let visitor = object
 
124
    val mutable allstmts = StmtSet.empty
 
125
    method allstmts = allstmts
 
126
    inherit nopCilVisitor as super
 
127
    method vstmt s = 
 
128
      allstmts <- StmtSet.add s allstmts;
 
129
      DoChildren
 
130
  end
 
131
  in
 
132
  ignore (visitCilBlock (visitor:>cilVisitor) block);
 
133
  visitor#allstmts
 
134
 
 
135
let compute_loops_stmts kf =
 
136
  let tbl = InstrHashtbl.create 17 in
 
137
  let visitor = object
 
138
    inherit nopCilVisitor as super
 
139
    method vstmt s =
 
140
      (match s.skind with
 
141
       | Loop (_,block,_,_,_) ->
 
142
           InstrHashtbl.add tbl (Kstmt s) (compute_allstmt_block block)
 
143
       |  _ -> ());
 
144
      DoChildren
 
145
  end
 
146
  in
 
147
  (try
 
148
     ignore 
 
149
       (visitCilFunction 
 
150
          (visitor :> cilVisitor) (Kernel_function.get_definition kf));
 
151
   with Kernel_function.No_Definition -> 
 
152
     ());
 
153
  tbl
 
154
 
 
155
exception No_such_while
 
156
 
 
157
(** @raise No_such_while if [stmt.skind] is not a [While]. *)
 
158
let get_loop_stmts =
 
159
  let module S =
 
160
    Kernel_function.Make_Table
 
161
      (Cil_datatype.InstrHashtbl(Cil_datatype.StmtSet))
 
162
      (struct
 
163
         let name = "LoopStmts"
 
164
         let size = 97
 
165
         let dependencies = [ Cil_state.self ]
 
166
       end)
 
167
  in
 
168
  fun kf loop_stmt ->
 
169
    (match loop_stmt.skind with
 
170
     | Loop _ -> ()
 
171
     | _ -> raise No_such_while);
 
172
    let tbl = S.memo compute_loops_stmts kf in
 
173
    try InstrHashtbl.find tbl (Kstmt loop_stmt) with Not_found -> assert false
 
174
 
 
175
(*
 
176
Local Variables:
 
177
compile-command: "LC_ALL=C make -C ../.."
 
178
End:
 
179
*)