« back to all changes in this revision
Viewing changes to popl09/popltoctl.ml
- browse files at revision 1927
- compare with another revision
- compare with revision 4777
- download diff
- download tarball
- view history from revision 1927
- Committer: Julia Lawall
- Date: 2008-06-10 19:49:56 UTC
- Revision ID: git-v1:bfce445bc28d65de46ab3c6c86424a6d98a24ce5
*** empty log message ***
svn path=/coccinelle/; revision=4494
svn path=/coccinelle/; revision=4494
- files added:
- popl09
- files modified:
- Makefile
added
removed
popl09/popltoctl.ml
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
if guard && contains_modif term
44
then
45
let v = ("","_v") in
46
ctl_exists true v
47
(CTL.Pred (Lib_engine.Match(term),CTL.Modif v))
48
else CTL.Pred (Lib_engine.Match(term),CTL.Control)
49
50
(* --------------------------------------------------------------------- *)
51
52
let is_true = function CTL.True -> true | _ -> false
53
54
let is_false = function CTL.False -> true | _ -> false
55
56
let ctl_true = CTL.True
57
58
let ctl_false = CTL.False
59
60
let ctl_and x y =
61
if is_true x then y
62
else if is_true y then x else CTL.And(CTL.STRICT,x,y)
63
64
let ctl_or x y =
65
if is_false x then y
66
else if is_false y then x else CTL.Or(x,y)
67
68
let ctl_seqor x y = CTL.SeqOr(x,y)
69
70
let ctl_not x = CTL.Not(x)
71
72
let ctl_ax x =
73
if is_true x then CTL.True
74
else CTL.AX(CTL.FORWARD,CTL.STRICT,x)
75
76
let ctl_ex x =
77
if is_true x then CTL.True
78
else CTL.EX(CTL.FORWARD,x)
79
80
let ctl_back_ex x =
81
if is_true x then CTL.True
82
else CTL.EX(CTL.BACKWARD,x)
83
84
let after = CTL.Pred(Lib_engine.After, CTL.Control)
85
let fall = CTL.Pred(Lib_engine.FallThrough, CTL.Control)
86
let exit = CTL.Pred(Lib_engine.Exit, CTL.Control)
87
let truepred = CTL.Pred(Lib_engine.TrueBranch, CTL.Control)
88
let falsepred = CTL.Pred(Lib_engine.FalseBranch, CTL.Control)
89
let retpred = CTL.Pred(Lib_engine.Return, CTL.Control)
90
91
let string2var x = ("",x)
92
93
let labelctr = ref 0
94
let get_label_ctr _ =
95
let cur = !labelctr in
96
labelctr := cur + 1;
97
string2var (Printf.sprintf "l%d" cur)
98
99
let ctl_au x y = CTL.AU(CTL.FORWARD,CTL.STRICT,x,y)
100
101
let ctl_uncheck x = CTL.Uncheck(x)
102
103
let make_meta_rule_elem d =
104
let nm = "_S" in
105
Ast.make_meta_rule_elem nm d ([],[],[])
106
107
(* --------------------------------------------------------------------- *)
108
109
let rec ctl_seq keep_wit a = function
110
Past.Seq(elem,seq) ->
111
ctl_element keep_wit (ctl_seq keep_wit a seq) elem
112
| Past.Empty -> a
113
| Past.SExists(var,seq) -> ctl_exists keep_wit var (ctl_seq keep_wit a seq)
114
115
and ctl_term keep_wit a = function
116
Past.Term(term) ->
117
(match Ast.unwrap term with
118
Ast.MetaStmt(_,_,_,_) -> ctl_true
119
| _ -> ctl_and (predmaker keep_wit term) (ctl_ax a))
120
| Past.TExists(var,term) ->
121
ctl_exists keep_wit var (ctl_term keep_wit a term)
122
123
and ctl_element keep_wit a = function
124
Past.Atomic(term,ba) ->
125
do_between_dots keep_wit ba (ctl_term keep_wit a term) a
126
| Past.IfThen(test,thn,(_,_,_,aft),ba) ->
127
do_between_dots keep_wit ba (ifthen keep_wit (Some a) test thn aft) a
128
| Past.Or(seq1,seq2) ->
129
ctl_seqor (ctl_seq keep_wit a seq1) (ctl_seq keep_wit a seq2)
130
| Past.DInfo(dots) -> ctl_au (guard_ctl_dots keep_wit a dots) a
131
| Past.EExists(var,elem) ->
132
ctl_exists keep_wit var (ctl_element keep_wit a elem)
133
134
(* --------------------------------------------------------------------- *)
135
136
and guard_ctl_seq keep_wit a = function
137
Past.Seq(elem,Past.Empty) -> guard_ctl_element keep_wit a elem
138
| Past.Seq(elem,seq) ->
139
ctl_element keep_wit (guard_ctl_seq keep_wit a seq) elem
140
| Past.Empty -> ctl_true
141
| Past.SExists(var,seq) ->
142
ctl_exists keep_wit var (guard_ctl_seq keep_wit a seq)
143
144
and guard_ctl_term keep_wit a = function
145
Past.Term(term) ->
146
(match Ast.unwrap term with
147
Ast.MetaStmt(_,_,_,_) -> ctl_true
148
| _ -> predmaker keep_wit term)
149
| Past.TExists(var,term) ->
150
ctl_exists keep_wit var (guard_ctl_term keep_wit a term)
151
152
and guard_ctl_element keep_wit a = function
153
Past.Atomic(term,_) -> guard_ctl_term keep_wit a term
154
| Past.IfThen(test,thn,(_,_,_,aft),_) -> ifthen keep_wit None test thn aft
155
| Past.Or(seq1,seq2) ->
156
ctl_seqor
157
(guard_ctl_seq keep_wit a seq1) (guard_ctl_seq keep_wit a seq2)
158
| Past.DInfo(dots) -> ctl_au (guard_ctl_dots keep_wit a dots) a
159
| Past.EExists(var,elem) ->
160
ctl_exists keep_wit var (guard_ctl_element keep_wit a elem)
161
162
and guard_ctl_dots keep_wit a = function
163
Past.Dots -> ctl_true
164
| Past.Nest(_) when not keep_wit -> ctl_true
165
| Past.Nest(seq) ->
166
ctl_or
167
(guard_ctl_seq true a seq)
168
(ctl_not (guard_ctl_seq false a seq))
169
| Past.When(dots,seq) ->
170
ctl_and
171
(guard_ctl_dots keep_wit a dots)
172
(ctl_not (guard_ctl_seq false a seq))
173
174
(* --------------------------------------------------------------------- *)
175
176
and ifthen keep_wit a test thn aft =
177
(* "if (test) thn; after" becomes:
178
if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
179
& EX After
180
(* doesn't work for C code if (x) return 1; else return 2; *)
181
*)
182
let end_code =
183
match (aft,a) with
184
(Ast.CONTEXT(_,Ast.NOTHING),None) -> ctl_true
185
| (Ast.CONTEXT(_,Ast.NOTHING),Some a) -> ctl_ax (ctl_ax a)
186
| (_,None) -> failwith "not possible"
187
| (_,Some a) ->
188
ctl_ax
189
(ctl_and
190
(predmaker keep_wit (make_meta_rule_elem aft))
191
(ctl_ax a)) in
192
let body =
193
ctl_or
194
(ctl_and truepred
195
(ctl_ax
196
(guard_ctl_element keep_wit ctl_true (* not used *) thn)))
197
(ctl_or fall
198
(ctl_and after end_code)) in
199
ctl_and (ctl_term keep_wit body test) (ctl_ex after)
200
201
and do_between_dots keep_wit ba term after =
202
match ba with
203
Past.AddingBetweenDots (brace_term,n)
204
| Past.DroppingBetweenDots (brace_term,n) ->
205
(* not sure at all what to do here for after... *)
206
let match_brace = ctl_element keep_wit after brace_term in
207
let v = Printf.sprintf "_r_%d" n in
208
let case1 = ctl_and (CTL.Ref v) match_brace in
209
let case2 = ctl_and (ctl_not (CTL.Ref v)) term in
210
CTL.Let
211
(v,ctl_or
212
(ctl_back_ex truepred)
213
(ctl_back_ex (ctl_back_ex falsepred)),
214
ctl_or case1 case2)
215
| Past.NoDots -> term
216
217
(* --------------------------------------------------------------------- *)
218
219
let toctl sl = ctl_seq true ctl_true sl
Loggerhead is a web-based interface for Breezy
Version: 2.0.1