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