Commit | Line | Data |
---|---|---|
34e49164 C |
1 | open Common |
2 | ||
3 | open Ograph_extended | |
4 | ||
5 | module F = Control_flow_c | |
6 | ||
7 | (*****************************************************************************) | |
8 | (* Debugging functions *) | |
9 | (*****************************************************************************) | |
ae4735db C |
10 | let show_or_not_predicate pred = |
11 | if !Flag_matcher.debug_engine then begin | |
12 | indent_do (fun () -> | |
13 | adjust_pp_with_indent_and_header "labeling: pred = " (fun () -> | |
34e49164 C |
14 | Pretty_print_engine.pp_predicate pred; |
15 | ); | |
16 | ) | |
17 | end | |
18 | ||
19 | let show_or_not_nodes nodes = | |
ae4735db C |
20 | if !Flag_matcher.debug_engine then begin |
21 | indent_do (fun () -> | |
22 | adjust_pp_with_indent_and_header "labeling: result = " (fun () -> | |
23 | Common.pp_do_in_box (fun () -> | |
34e49164 | 24 | pp "{"; |
ae4735db | 25 | Common.print_between |
34e49164 | 26 | (fun () -> pp ";"; Format.print_cut()) |
ae4735db | 27 | (fun (nodei, (_predTODO, subst)) -> |
34e49164 | 28 | Format.print_int nodei; |
ae4735db | 29 | Common.pp_do_in_box (fun () -> |
34e49164 C |
30 | Pretty_print_engine.pp_binding2_ctlsubst subst |
31 | ) | |
32 | ) nodes; | |
33 | pp "}"; | |
34 | ); | |
35 | ) | |
36 | ) | |
37 | end | |
38 | ||
39 | let show_isos rule_elem = | |
40 | match Ast_cocci.get_isos rule_elem with | |
41 | [] -> () | |
42 | | isos -> | |
43 | let line = Ast_cocci.get_line rule_elem in | |
44 | Printf.printf "rule elem: "; | |
45 | Pretty_print_cocci.rule_elem "" rule_elem; | |
46 | Format.print_newline(); | |
47 | List.iter | |
48 | (function (nm,x) -> | |
49 | Printf.printf " iso: %s(%d): " nm line; | |
50 | Pretty_print_cocci.pp_print_anything x; | |
51 | Format.print_newline()) | |
52 | isos | |
53 | ||
54 | (*****************************************************************************) | |
55 | (* Labeling function *) | |
56 | (*****************************************************************************) | |
57 | let (-->) x v = Ast_ctl.Subst (x,v);; | |
58 | ||
59 | (* Take list of predicate and for each predicate returns where in the | |
ae4735db | 60 | * control flow it matches, and the set of subsitutions for this match. |
34e49164 C |
61 | *) |
62 | let (labels_for_ctl: string list (* dropped isos *) -> | |
ae4735db | 63 | (nodei * F.node) list -> Lib_engine.metavars_binding -> |
34e49164 C |
64 | Lib_engine.label_ctlcocci) = |
65 | fun dropped_isos nodes binding -> | |
66 | ||
ae4735db | 67 | (fun p -> |
34e49164 C |
68 | show_or_not_predicate p; |
69 | ||
ae4735db | 70 | let nodes' = nodes +> List.map (fun (nodei, node) -> |
34e49164 C |
71 | (* todo? put part of this code in pattern ? *) |
72 | (match p, F.unwrap node with | |
ae4735db | 73 | | Lib_engine.Paren s, (F.SeqStart (_, bracelevel, _)) -> |
34e49164 C |
74 | let make_var x = ("",i_to_s x) in |
75 | [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))] | |
ae4735db | 76 | | Lib_engine.Paren s, (F.SeqEnd (bracelevel, _)) -> |
34e49164 C |
77 | let make_var x = ("",i_to_s x) in |
78 | [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))] | |
79 | | Lib_engine.Paren _, _ -> [] | |
ae4735db | 80 | | Lib_engine.Label s, _ -> |
34e49164 | 81 | let labels = F.extract_labels node in |
7f004419 C |
82 | [(nodei, |
83 | (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))] | |
ae4735db | 84 | | Lib_engine.BCLabel s, _ -> |
34e49164 C |
85 | (match F.extract_bclabels node with |
86 | [] -> [] (* null for all nodes that are not break or continue *) | |
87 | | labels -> | |
7f004419 C |
88 | [(nodei, |
89 | (p,[(s --> | |
90 | (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))]) | |
ae4735db | 91 | | Lib_engine.PrefixLabel s, _ -> |
34e49164 | 92 | let labels = F.extract_labels node in |
7f004419 C |
93 | [(nodei, |
94 | (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Prefix labels)))]))] | |
34e49164 | 95 | |
ae4735db C |
96 | | Lib_engine.Match (re), _unwrapnode -> |
97 | let substs = | |
485bce71 | 98 | Pattern_c.match_re_node dropped_isos re node binding |
ae4735db | 99 | +> List.map (fun (re', subst) -> |
34e49164 C |
100 | Lib_engine.Match (re'), subst |
101 | ) | |
102 | in | |
ae4735db C |
103 | substs +> List.map (fun (p', subst) -> |
104 | (nodei, | |
105 | (p', | |
106 | subst +> List.map (fun (s, meta) -> | |
34e49164 C |
107 | s --> Lib_engine.NormalMetaVal meta |
108 | )))) | |
109 | ||
110 | | Lib_engine.InLoop, F.InLoopNode -> [nodei, (p,[])] | |
111 | | Lib_engine.TrueBranch , F.TrueNode -> [nodei, (p,[])] | |
112 | | Lib_engine.FalseBranch, F.FalseNode -> [nodei, (p,[])] | |
113 | | Lib_engine.After, F.AfterNode -> [nodei, (p,[])] | |
114 | | Lib_engine.FallThrough, F.FallThroughNode -> [nodei,(p,[])] | |
951c7801 | 115 | | Lib_engine.LoopFallThrough, F.LoopFallThroughNode -> [nodei,(p,[])] |
34e49164 C |
116 | | Lib_engine.FunHeader, F.FunHeader _ -> [nodei, (p,[])] |
117 | | Lib_engine.Top, F.TopNode -> [nodei, (p,[])] | |
118 | | Lib_engine.Exit, F.Exit -> [nodei, (p,[])] | |
119 | | Lib_engine.ErrorExit, F.ErrorExit -> [nodei, (p,[])] | |
b1b2de81 | 120 | | Lib_engine.Goto, F.Goto(_,_,_) -> [nodei, (p,[])] |
34e49164 C |
121 | |
122 | | Lib_engine.InLoop , _ -> [] | |
123 | | Lib_engine.TrueBranch , _ -> [] | |
124 | | Lib_engine.FalseBranch, _ -> [] | |
125 | | Lib_engine.After, _ -> [] | |
126 | | Lib_engine.FallThrough, _ -> [] | |
951c7801 | 127 | | Lib_engine.LoopFallThrough, _ -> [] |
34e49164 C |
128 | | Lib_engine.FunHeader, _ -> [] |
129 | | Lib_engine.Top, _ -> [] | |
130 | | Lib_engine.Exit, _ -> [] | |
131 | | Lib_engine.ErrorExit, _ -> [] | |
132 | | Lib_engine.Goto, _ -> [] | |
133 | ||
134 | | Lib_engine.BindGood s, _ -> [(nodei, (p,[(s --> Lib_engine.GoodVal)]))] | |
135 | | Lib_engine.BindBad s, _ -> [(nodei, (p,[(s --> Lib_engine.BadVal)]))] | |
136 | | Lib_engine.FakeBrace, _ -> | |
137 | if F.extract_is_fake node then [nodei, (p,[])] else [] | |
138 | ||
ae4735db | 139 | | Lib_engine.Return, node -> |
34e49164 | 140 | (match node with |
ae4735db | 141 | (* todo? should match the Exit code ? |
34e49164 | 142 | * todo: one day try also to match the special function |
ae4735db | 143 | * such as panic(); |
34e49164 C |
144 | *) |
145 | | F.Return _ -> [nodei, (p,[])] | |
146 | | F.ReturnExpr _ -> [nodei, (p,[])] | |
147 | | _ -> [] | |
148 | ) | |
149 | ) | |
150 | ) +> List.concat | |
151 | in | |
152 | ||
153 | show_or_not_nodes nodes'; | |
154 | nodes' | |
ae4735db | 155 | ) |
34e49164 C |
156 | |
157 | (*****************************************************************************) | |
158 | (* Some fix flow, for CTL, for unparse *) | |
159 | (*****************************************************************************) | |
160 | (* could erase info on nodes, and edge, because they are not used by rene *) | |
ae4735db | 161 | let (control_flow_for_ctl: F.cflow -> ('a, 'b) ograph_mutable) = |
34e49164 C |
162 | fun cflow -> cflow |
163 | ||
164 | ||
165 | ||
ae4735db | 166 | (* Just make the final node of the control flow loop over itself. |
34e49164 C |
167 | * It seems that one hypothesis of the SAT algorithm is that each node as at |
168 | * least a successor. | |
ae4735db | 169 | * |
34e49164 | 170 | * update: do same for errorexit node. |
ae4735db C |
171 | * |
172 | * update: also erase the fake nodes (and adjust the edges accordingly), | |
34e49164 C |
173 | * so that AX in CTL can now work. |
174 |