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