Commit | Line | Data |
---|---|---|
951c7801 C |
1 | module Past = Ast_popl |
2 | module Ast = Ast_cocci | |
3 | module V = Visitor_ast | |
4 | module CTL = Ast_ctl | |
5 | ||
6 | (* --------------------------------------------------------------------- *) | |
7 | (* result type *) | |
8 | ||
9 | type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif | |
10 | type formula = | |
11 | (cocci_predicate,Ast_cocci.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl | |
12 | ||
13 | (* --------------------------------------------------------------------- *) | |
14 | ||
15 | let contains_modif = | |
16 | let bind x y = x or y in | |
17 | let option_default = false in | |
18 | let mcode r (_,_,kind,_) = | |
19 | match kind with | |
20 | Ast.MINUS(_,_) -> true | |
21 | | Ast.PLUS -> failwith "not possible" | |
22 | | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in | |
23 | let do_nothing r k e = k e in | |
24 | let rule_elem r k re = | |
25 | let res = k re in | |
26 | match Ast.unwrap re with | |
27 | Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) -> | |
28 | bind (mcode r ((),(),bef,Ast.NoMetaPos)) res | |
29 | | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res | |
30 | | _ -> res in | |
31 | let recursor = | |
32 | V.combiner bind option_default | |
33 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
34 | mcode | |
35 | do_nothing do_nothing do_nothing do_nothing | |
36 | do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing | |
37 | do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in | |
38 | recursor.V.combiner_rule_elem | |
39 | ||
40 | let ctl_exists v x keep_wit = CTL.Exists(v,x,keep_wit) | |
41 | ||
42 | let predmaker guard term = | |
43 | let pos = ("","_p") in | |
44 | ctl_exists true pos | |
45 | (if guard && contains_modif term | |
46 | then | |
47 | let v = ("","_v") in | |
48 | ctl_exists true v | |
49 | (CTL.Pred (Lib_engine.Match(term),CTL.Modif v)) | |
50 | else CTL.Pred (Lib_engine.Match(term),CTL.Control)) | |
51 | ||
52 | (* --------------------------------------------------------------------- *) | |
53 | ||
54 | let is_true = function CTL.True -> true | _ -> false | |
55 | ||
56 | let is_false = function CTL.False -> true | _ -> false | |
57 | ||
58 | let ctl_true = CTL.True | |
59 | ||
60 | let ctl_false = CTL.False | |
61 | ||
62 | let ctl_and x y = | |
63 | if is_true x then y | |
64 | else if is_true y then x else CTL.And(CTL.STRICT,x,y) | |
65 | ||
66 | let ctl_or x y = | |
67 | if is_false x then y | |
68 | else if is_false y then x else CTL.Or(x,y) | |
69 | ||
70 | let ctl_seqor x y = CTL.SeqOr(x,y) | |
71 | ||
72 | let ctl_not x = CTL.Not(x) | |
73 | ||
74 | let ctl_ax x = | |
75 | if is_true x then CTL.True | |
76 | else CTL.AX(CTL.FORWARD,CTL.STRICT,x) | |
77 | ||
78 | let after = CTL.Pred(Lib_engine.After, CTL.Control) | |
79 | let exit = CTL.Pred(Lib_engine.Exit, CTL.Control) | |
80 | let truepred = CTL.Pred(Lib_engine.TrueBranch, CTL.Control) | |
81 | let retpred = CTL.Pred(Lib_engine.Return, CTL.Control) | |
82 | ||
83 | let string2var x = ("",x) | |
84 | ||
85 | let labelctr = ref 0 | |
86 | let get_label_ctr _ = | |
87 | let cur = !labelctr in | |
88 | labelctr := cur + 1; | |
89 | string2var (Printf.sprintf "l%d" cur) | |
90 | ||
91 | let ctl_au x seq_after y = | |
92 | let lv = get_label_ctr() in | |
93 | let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in | |
94 | let preflabelpred = CTL.Pred(Lib_engine.PrefixLabel lv,CTL.Control) in | |
95 | let matchgoto = CTL.Pred(Lib_engine.Goto,CTL.Control) in | |
96 | let matchbreak = | |
97 | predmaker false | |
98 | (Ast.make_term | |
99 | (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in | |
100 | let matchcontinue = | |
101 | predmaker false | |
102 | (Ast.make_term | |
103 | (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in | |
104 | let stop_early = | |
105 | ctl_or after | |
106 | (ctl_and (ctl_and truepred labelpred) | |
107 | (CTL.AU | |
108 | (CTL.FORWARD,CTL.STRICT,preflabelpred, | |
109 | ctl_and preflabelpred | |
110 | (ctl_or retpred | |
111 | (ctl_and (ctl_or (ctl_or matchgoto matchbreak) matchcontinue) | |
112 | (CTL.AG | |
113 | (CTL.FORWARD,CTL.STRICT, | |
114 | ctl_not seq_after))))))) in | |
115 | CTL.AU(CTL.FORWARD,CTL.STRICT,x,ctl_or y stop_early) | |
116 | ||
117 | let ctl_uncheck x = CTL.Uncheck(x) | |
118 | ||
119 | (* --------------------------------------------------------------------- *) | |
120 | ||
121 | let rec ctl_seq keep_wit a = function | |
122 | Past.Seq(elem,seq) -> | |
123 | ctl_element keep_wit (ctl_seq keep_wit a seq) elem | |
124 | | Past.Empty -> a | |
125 | | Past.SExists(var,seq) -> ctl_exists keep_wit var (ctl_seq keep_wit a seq) | |
126 | ||
127 | and ctl_element keep_wit a = function | |
128 | Past.Term(term) -> ctl_and (predmaker keep_wit term) (ctl_ax a) | |
129 | | Past.Or(seq1,seq2) -> | |
130 | ctl_seqor (ctl_seq keep_wit a seq1) (ctl_seq keep_wit a seq2) | |
131 | | Past.DInfo(dots,seq_bef,seq_aft) -> | |
132 | let shortest l = | |
133 | List.fold_left ctl_or ctl_false | |
134 | (List.map (ctl_element false ctl_true) l) in | |
135 | let s = shortest (Common.union_set seq_bef seq_aft) in | |
136 | ctl_au (ctl_and (guard_ctl_dots keep_wit dots) (ctl_not s)) | |
137 | (shortest seq_aft) a | |
138 | | Past.EExists(var,elem) -> | |
139 | ctl_exists keep_wit var (ctl_element keep_wit a elem) | |
140 | ||
141 | (* --------------------------------------------------------------------- *) | |
142 | ||
143 | and guard_ctl_seq keep_wit = function | |
144 | Past.Seq(elem,Past.Empty) -> guard_ctl_element keep_wit elem | |
145 | | Past.Seq(elem,seq) -> | |
146 | ctl_element keep_wit (guard_ctl_seq keep_wit seq) elem | |
147 | | Past.Empty -> ctl_true | |
148 | | Past.SExists(var,seq) -> | |
149 | ctl_exists keep_wit var (guard_ctl_seq keep_wit seq) | |
150 | ||
151 | and guard_ctl_element keep_wit = function | |
152 | Past.Term(term) -> predmaker keep_wit term | |
153 | | Past.Or(seq1,seq2) -> | |
154 | ctl_seqor (guard_ctl_seq keep_wit seq1) (guard_ctl_seq keep_wit seq2) | |
155 | | Past.DInfo(dots,seq_bef,seq_aft) -> | |
156 | let shortest l = | |
157 | List.fold_left ctl_or ctl_false | |
158 | (List.map (ctl_element false ctl_true) l) in | |
159 | let s = shortest (Common.union_set seq_bef seq_aft) in | |
160 | let aft = ctl_or s exit in | |
161 | ctl_au (ctl_and (guard_ctl_dots keep_wit dots) (ctl_not s)) | |
162 | (shortest seq_aft) aft | |
163 | | Past.EExists(var,elem) -> | |
164 | ctl_exists keep_wit var (guard_ctl_element keep_wit elem) | |
165 | ||
166 | and guard_ctl_dots keep_wit = function | |
167 | Past.Dots -> ctl_true | |
168 | | Past.Nest(_) when not keep_wit -> ctl_true | |
169 | | Past.Nest(seq) -> | |
170 | ctl_or (guard_ctl_seq true seq) (ctl_not (guard_ctl_seq false seq)) | |
171 | | Past.When(dots,seq) -> | |
172 | ctl_and | |
173 | (guard_ctl_dots keep_wit dots) | |
174 | (ctl_not (ctl_seq false ctl_true seq)) | |
175 | | Past.DExists(var,dots) -> | |
176 | ctl_exists keep_wit var (guard_ctl_dots keep_wit dots) | |
177 | ||
178 | (* --------------------------------------------------------------------- *) | |
179 | ||
180 | let toctl sl = ctl_seq true ctl_true sl |