Commit | Line | Data |
---|---|---|
9f8e26f4 | 1 | (* |
ae4735db | 2 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen |
9f8e26f4 C |
3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix |
4 | * This file is part of Coccinelle. | |
5 | * | |
6 | * Coccinelle is free software: you can redistribute it and/or modify | |
7 | * it under the terms of the GNU General Public License as published by | |
8 | * the Free Software Foundation, according to version 2 of the License. | |
9 | * | |
10 | * Coccinelle is distributed in the hope that it will be useful, | |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
13 | * GNU General Public License for more details. | |
14 | * | |
15 | * You should have received a copy of the GNU General Public License | |
16 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
17 | * | |
18 | * The authors reserve the right to distribute this or future versions of | |
19 | * Coccinelle under other licenses. | |
20 | *) | |
21 | ||
22 | ||
5636bb2c C |
23 | (* |
24 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen | |
25 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
26 | * This file is part of Coccinelle. | |
27 | * | |
28 | * Coccinelle is free software: you can redistribute it and/or modify | |
29 | * it under the terms of the GNU General Public License as published by | |
30 | * the Free Software Foundation, according to version 2 of the License. | |
31 | * | |
32 | * Coccinelle is distributed in the hope that it will be useful, | |
33 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
34 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
35 | * GNU General Public License for more details. | |
36 | * | |
37 | * You should have received a copy of the GNU General Public License | |
38 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
39 | * | |
40 | * The authors reserve the right to distribute this or future versions of | |
41 | * Coccinelle under other licenses. | |
42 | *) | |
43 | ||
44 | ||
34e49164 C |
45 | open Common |
46 | ||
47 | open Ograph_extended | |
48 | ||
49 | module F = Control_flow_c | |
50 | ||
51 | (*****************************************************************************) | |
52 | (* Debugging functions *) | |
53 | (*****************************************************************************) | |
ae4735db C |
54 | let show_or_not_predicate pred = |
55 | if !Flag_matcher.debug_engine then begin | |
56 | indent_do (fun () -> | |
57 | adjust_pp_with_indent_and_header "labeling: pred = " (fun () -> | |
34e49164 C |
58 | Pretty_print_engine.pp_predicate pred; |
59 | ); | |
60 | ) | |
61 | end | |
62 | ||
63 | let show_or_not_nodes nodes = | |
ae4735db C |
64 | if !Flag_matcher.debug_engine then begin |
65 | indent_do (fun () -> | |
66 | adjust_pp_with_indent_and_header "labeling: result = " (fun () -> | |
67 | Common.pp_do_in_box (fun () -> | |
34e49164 | 68 | pp "{"; |
ae4735db | 69 | Common.print_between |
34e49164 | 70 | (fun () -> pp ";"; Format.print_cut()) |
ae4735db | 71 | (fun (nodei, (_predTODO, subst)) -> |
34e49164 | 72 | Format.print_int nodei; |
ae4735db | 73 | Common.pp_do_in_box (fun () -> |
34e49164 C |
74 | Pretty_print_engine.pp_binding2_ctlsubst subst |
75 | ) | |
76 | ) nodes; | |
77 | pp "}"; | |
78 | ); | |
79 | ) | |
80 | ) | |
81 | end | |
82 | ||
83 | let show_isos rule_elem = | |
84 | match Ast_cocci.get_isos rule_elem with | |
85 | [] -> () | |
86 | | isos -> | |
87 | let line = Ast_cocci.get_line rule_elem in | |
88 | Printf.printf "rule elem: "; | |
89 | Pretty_print_cocci.rule_elem "" rule_elem; | |
90 | Format.print_newline(); | |
91 | List.iter | |
92 | (function (nm,x) -> | |
93 | Printf.printf " iso: %s(%d): " nm line; | |
94 | Pretty_print_cocci.pp_print_anything x; | |
95 | Format.print_newline()) | |
96 | isos | |
97 | ||
98 | (*****************************************************************************) | |
99 | (* Labeling function *) | |
100 | (*****************************************************************************) | |
101 | let (-->) x v = Ast_ctl.Subst (x,v);; | |
102 | ||
103 | (* Take list of predicate and for each predicate returns where in the | |
ae4735db | 104 | * control flow it matches, and the set of subsitutions for this match. |
34e49164 C |
105 | *) |
106 | let (labels_for_ctl: string list (* dropped isos *) -> | |
ae4735db | 107 | (nodei * F.node) list -> Lib_engine.metavars_binding -> |
34e49164 C |
108 | Lib_engine.label_ctlcocci) = |
109 | fun dropped_isos nodes binding -> | |
110 | ||
ae4735db | 111 | (fun p -> |
34e49164 C |
112 | show_or_not_predicate p; |
113 | ||
ae4735db | 114 | let nodes' = nodes +> List.map (fun (nodei, node) -> |
34e49164 C |
115 | (* todo? put part of this code in pattern ? *) |
116 | (match p, F.unwrap node with | |
ae4735db | 117 | | Lib_engine.Paren s, (F.SeqStart (_, bracelevel, _)) -> |
34e49164 C |
118 | let make_var x = ("",i_to_s x) in |
119 | [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))] | |
ae4735db | 120 | | Lib_engine.Paren s, (F.SeqEnd (bracelevel, _)) -> |
34e49164 C |
121 | let make_var x = ("",i_to_s x) in |
122 | [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))] | |
123 | | Lib_engine.Paren _, _ -> [] | |
ae4735db | 124 | | Lib_engine.Label s, _ -> |
34e49164 | 125 | let labels = F.extract_labels node in |
7f004419 C |
126 | [(nodei, |
127 | (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))] | |
ae4735db | 128 | | Lib_engine.BCLabel s, _ -> |
34e49164 C |
129 | (match F.extract_bclabels node with |
130 | [] -> [] (* null for all nodes that are not break or continue *) | |
131 | | labels -> | |
7f004419 C |
132 | [(nodei, |
133 | (p,[(s --> | |
134 | (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))]) | |
ae4735db | 135 | | Lib_engine.PrefixLabel s, _ -> |
34e49164 | 136 | let labels = F.extract_labels node in |
7f004419 C |
137 | [(nodei, |
138 | (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Prefix labels)))]))] | |
34e49164 | 139 | |
ae4735db C |
140 | | Lib_engine.Match (re), _unwrapnode -> |
141 | let substs = | |
485bce71 | 142 | Pattern_c.match_re_node dropped_isos re node binding |
ae4735db | 143 | +> List.map (fun (re', subst) -> |
34e49164 C |
144 | Lib_engine.Match (re'), subst |
145 | ) | |
146 | in | |
ae4735db C |
147 | substs +> List.map (fun (p', subst) -> |
148 | (nodei, | |
149 | (p', | |
150 | subst +> List.map (fun (s, meta) -> | |
34e49164 C |
151 | s --> Lib_engine.NormalMetaVal meta |
152 | )))) | |
153 | ||
154 | | Lib_engine.InLoop, F.InLoopNode -> [nodei, (p,[])] | |
155 | | Lib_engine.TrueBranch , F.TrueNode -> [nodei, (p,[])] | |
156 | | Lib_engine.FalseBranch, F.FalseNode -> [nodei, (p,[])] | |
157 | | Lib_engine.After, F.AfterNode -> [nodei, (p,[])] | |
158 | | Lib_engine.FallThrough, F.FallThroughNode -> [nodei,(p,[])] | |
951c7801 | 159 | | Lib_engine.LoopFallThrough, F.LoopFallThroughNode -> [nodei,(p,[])] |
34e49164 C |
160 | | Lib_engine.FunHeader, F.FunHeader _ -> [nodei, (p,[])] |
161 | | Lib_engine.Top, F.TopNode -> [nodei, (p,[])] | |
162 | | Lib_engine.Exit, F.Exit -> [nodei, (p,[])] | |
163 | | Lib_engine.ErrorExit, F.ErrorExit -> [nodei, (p,[])] | |
b1b2de81 | 164 | | Lib_engine.Goto, F.Goto(_,_,_) -> [nodei, (p,[])] |
34e49164 C |
165 | |
166 | | Lib_engine.InLoop , _ -> [] | |
167 | | Lib_engine.TrueBranch , _ -> [] | |
168 | | Lib_engine.FalseBranch, _ -> [] | |
169 | | Lib_engine.After, _ -> [] | |
170 | | Lib_engine.FallThrough, _ -> [] | |
951c7801 | 171 | | Lib_engine.LoopFallThrough, _ -> [] |
34e49164 C |
172 | | Lib_engine.FunHeader, _ -> [] |
173 | | Lib_engine.Top, _ -> [] | |
174 | | Lib_engine.Exit, _ -> [] | |
175 | | Lib_engine.ErrorExit, _ -> [] | |
176 | | Lib_engine.Goto, _ -> [] | |
177 | ||
178 | | Lib_engine.BindGood s, _ -> [(nodei, (p,[(s --> Lib_engine.GoodVal)]))] | |
179 | | Lib_engine.BindBad s, _ -> [(nodei, (p,[(s --> Lib_engine.BadVal)]))] | |
180 | | Lib_engine.FakeBrace, _ -> | |
181 | if F.extract_is_fake node then [nodei, (p,[])] else [] | |
182 | ||
ae4735db | 183 | | Lib_engine.Return, node -> |
34e49164 | 184 | (match node with |
ae4735db | 185 | (* todo? should match the Exit code ? |
34e49164 | 186 | * todo: one day try also to match the special function |
ae4735db | 187 | * such as panic(); |
34e49164 C |
188 | *) |
189 | | F.Return _ -> [nodei, (p,[])] | |
190 | | F.ReturnExpr _ -> [nodei, (p,[])] | |
191 | | _ -> [] | |
192 | ) | |
193 | ) | |
194 | ) +> List.concat | |
195 | in | |
196 | ||
197 | show_or_not_nodes nodes'; | |
198 | nodes' | |
ae4735db | 199 | ) |
34e49164 C |
200 | |
201 | (*****************************************************************************) | |
202 | (* Some fix flow, for CTL, for unparse *) | |
203 | (*****************************************************************************) | |
204 | (* could erase info on nodes, and edge, because they are not used by rene *) | |
ae4735db | 205 | let (control_flow_for_ctl: F.cflow -> ('a, 'b) ograph_mutable) = |
34e49164 C |
206 | fun cflow -> cflow |
207 | ||
208 | ||
209 | ||
ae4735db | 210 | (* Just make the final node of the control flow loop over itself. |
34e49164 C |
211 | * It seems that one hypothesis of the SAT algorithm is that each node as at |
212 | * least a successor. | |
ae4735db | 213 | * |
34e49164 | 214 | * update: do same for errorexit node. |
ae4735db C |
215 | * |
216 | * update: also erase the fake nodes (and adjust the edges accordingly), | |
34e49164 C |
217 | * so that AX in CTL can now work. |
218 |