Commit | Line | Data |
---|---|---|
9f8e26f4 | 1 | (* |
ae4735db | 2 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen |
9f8e26f4 C |
3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix |
4 | * This file is part of Coccinelle. | |
5 | * | |
6 | * Coccinelle is free software: you can redistribute it and/or modify | |
7 | * it under the terms of the GNU General Public License as published by | |
8 | * the Free Software Foundation, according to version 2 of the License. | |
9 | * | |
10 | * Coccinelle is distributed in the hope that it will be useful, | |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
13 | * GNU General Public License for more details. | |
14 | * | |
15 | * You should have received a copy of the GNU General Public License | |
16 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
17 | * | |
18 | * The authors reserve the right to distribute this or future versions of | |
19 | * Coccinelle under other licenses. | |
20 | *) | |
21 | ||
22 | ||
5636bb2c C |
23 | (* |
24 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen | |
25 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
26 | * This file is part of Coccinelle. | |
27 | * | |
28 | * Coccinelle is free software: you can redistribute it and/or modify | |
29 | * it under the terms of the GNU General Public License as published by | |
30 | * the Free Software Foundation, according to version 2 of the License. | |
31 | * | |
32 | * Coccinelle is distributed in the hope that it will be useful, | |
33 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
34 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
35 | * GNU General Public License for more details. | |
36 | * | |
37 | * You should have received a copy of the GNU General Public License | |
38 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
39 | * | |
40 | * The authors reserve the right to distribute this or future versions of | |
41 | * Coccinelle under other licenses. | |
42 | *) | |
43 | ||
44 | ||
34e49164 C |
45 | module CTL = Ast_ctl |
46 | ||
47 | let prelude = | |
48 | "\\documentclass{article}\n"^ | |
49 | "\\usepackage{fullpage}\n\n"^ | |
50 | "\\newcommand{\\U}{\\,\\mbox{\\sf{U}}\\,}\n"^ | |
51 | "\\newcommand{\\A}{\\mbox{\\sf{A}}}\n"^ | |
52 | "\\newcommand{\\E}{\\mbox{\\sf{E}}}\n"^ | |
53 | "\\newcommand{\\AX}{\\mbox{\\sf{AX}}}\n"^ | |
54 | "\\newcommand{\\EX}{\\mbox{\\sf{EX}}}\n"^ | |
55 | "\\newcommand{\\AF}{\\mbox{\\sf{AF}}}\n"^ | |
56 | "\\newcommand{\\EF}{\\mbox{\\sf{EF}}}\n"^ | |
57 | "\\newcommand{\\AG}{\\mbox{\\sf{AG}}}\n"^ | |
58 | "\\newcommand{\\EG}{\\mbox{\\sf{EG}}}\n\n"^ | |
59 | "\\newcommand{\\mita}[1]{\\mbox{\\it{{#1}}}}\n"^ | |
60 | "\\newcommand{\\mtt}[1]{\\mbox{\\tt{{#1}}}}\n"^ | |
61 | "\\newcommand{\\msf}[1]{\\mbox{\\sf{{#1}}}}\n"^ | |
62 | "\\newcommand{\\mrm}[1]{\\mbox{\\rm{{#1}}}}\n"^ | |
63 | "\\newcommand{\\mth}[1]{\\({#1}\\)}\n\n"^ | |
64 | "\\newcommand{\\ttlb}{\\mbox{\\tt \\char'173}}\n"^ | |
65 | "\\newcommand{\\ttrb}{\\mbox{\\tt \\char'175}}\n\n"^ | |
66 | "\\begin{document}\n" | |
67 | ||
68 | let postlude = "\\end{document}" | |
69 | ||
70 | let check_ct ct res = if ct > 60 then (res^"\\\\\\mbox{}",0) else (res,ct) | |
71 | let texify s = | |
72 | let len = String.length s in | |
73 | let rec loop n = | |
74 | if n = len | |
75 | then "" | |
76 | else | |
77 | match String.get s n with | |
78 | '_' -> Printf.sprintf "\\_%s" (loop (n+1)) | |
79 | | '{' -> Printf.sprintf "{\\ttlb}%s" (loop (n+1)) | |
80 | | '}' -> Printf.sprintf "{\\ttrb}%s" (loop (n+1)) | |
81 | | '>' -> Printf.sprintf "\\mth{>}%s" (loop (n+1)) | |
82 | | c -> Printf.sprintf "%c%s" c (loop (n+1)) in | |
83 | (Printf.sprintf "\\mita{%s}" (loop 0),len) | |
84 | ||
85 | let modif2c pv = function | |
86 | CTL.Modif(v) -> let (s,n) = texify(pv v) in (Printf.sprintf "_{%s}" s,n) | |
87 | | CTL.UnModif(v) -> let (s,n) = texify(pv v) in (Printf.sprintf "_{%s}" s,n) | |
88 | | CTL.Control -> ("",0) | |
89 | ||
90 | let print_diamond ct = function | |
91 | CTL.FORWARD -> ("",ct) | |
92 | | CTL.BACKWARD -> ("\\Delta",ct+1) | |
93 | ||
94 | let rec ctl2c ct pp pv = function | |
95 | CTL.False -> ("\\msf{false}",5) | |
96 | | CTL.True -> ("\\msf{true}",4) | |
97 | | CTL.Pred(p,v) -> | |
98 | let (res,n) = pp p in | |
99 | let (resv,n1) = modif2c pv v in | |
100 | (res^resv,ct+n+n1) | |
101 | | CTL.Not(f) -> | |
102 | let (res,ct) = wrap (ct+1) pp pv f in | |
103 | ("\\neg "^res,ct) | |
104 | | CTL.Exists(_,v,f) -> | |
105 | let (res1,len) = texify(pv v) in | |
106 | let ct = ct + len in | |
107 | let (res1,ct) = check_ct ct res1 in | |
108 | let (res2,ct) = existswrap (ct+1) pp pv f in | |
109 | ("\\exists "^res1^" . "^res2,ct) | |
110 | | CTL.And(_,f1,f2) -> | |
111 | let (res1,ct) = andwrap ct pp pv f1 in | |
112 | let (res1,ct) = check_ct ct res1 in | |
113 | let (res2,ct) = andwrap (ct+1) pp pv f2 in | |
114 | (res1^" \\wedge "^res2,ct) | |
115 | | CTL.AndAny(dir,_,f1,f2) -> | |
116 | let (diamond,ct) = print_diamond (ct+2) dir in | |
117 | let (res1,ct) = andwrap ct pp pv f1 in | |
118 | let (res1,ct) = check_ct ct res1 in | |
119 | let (res2,ct) = andwrap (ct+1) pp pv f2 in | |
120 | (res1^" \\wedge? "^diamond^res2,ct) | |
121 | | CTL.HackForStmt(dir,_,f1,f2) -> | |
122 | let (diamond,ct) = print_diamond (ct+2) dir in | |
123 | let (res1,ct) = andwrap ct pp pv f1 in | |
124 | let (res1,ct) = check_ct ct res1 in | |
125 | let (res2,ct) = andwrap (ct+1) pp pv f2 in | |
126 | (res1^" \\wedge{h} "^diamond^res2,ct) | |
127 | | CTL.Or(f1,f2) -> | |
128 | let (res1,ct) = orwrap ct pp pv f1 in | |
129 | let (res1,ct) = check_ct ct res1 in | |
130 | let (res2,ct) = orwrap (ct+1) pp pv f2 in | |
131 | (res1^" \\vee "^res2,ct) | |
132 | | CTL.SeqOr(f1,f2) -> | |
133 | let (res1,ct) = orwrap ct pp pv f1 in | |
134 | let (res1,ct) = check_ct ct res1 in | |
135 | let (res2,ct) = orwrap (ct+1) pp pv f2 in | |
136 | (res1^" \\mid "^res2,ct) | |
137 | | CTL.Implies(f1,f2) -> | |
138 | let (res1,ct) = wrap ct pp pv f1 in | |
139 | let (res1,ct) = check_ct ct res1 in | |
140 | let (res2,ct) = wrap (ct+1) pp pv f2 in | |
141 | (res1^" \\rightarrow "^res2,ct) | |
142 | | CTL.AF(dir,_,f) -> | |
143 | let (diamond,ct) = print_diamond (ct+2) dir in | |
144 | let (res,ct) = pathwrap ct pp pv f | |
145 | in ("\\AF"^diamond^res,ct) | |
146 | | CTL.AX(dir,_,f) -> | |
147 | let (diamond,ct) = print_diamond (ct+2) dir in | |
148 | let (res,ct) = pathwrap ct pp pv f | |
149 | in ("\\AX"^diamond^res,ct) | |
150 | | CTL.AG(dir,_,f) -> | |
151 | let (diamond,ct) = print_diamond (ct+2) dir in | |
152 | let (res,ct) = pathwrap ct pp pv f | |
153 | in ("\\AG"^diamond^res,ct) | |
154 | | CTL.AW(dir,_,f1,f2) -> | |
155 | let (diamond,ct) = print_diamond (ct+1) dir in | |
156 | let (res1,ct) = existswrap (ct+1) pp pv f1 in | |
157 | let (res1,ct) = check_ct ct res1 in | |
158 | let (res2,ct) = existswrap (ct+3) pp pv f2 in | |
159 | ("\\"^diamond^"A["^res1^" W "^res2^"]\n",ct) | |
160 | | CTL.AU(dir,_,f1,f2) -> | |
161 | let (diamond,ct) = print_diamond (ct+1) dir in | |
162 | let (res1,ct) = existswrap (ct+1) pp pv f1 in | |
163 | let (res1,ct) = check_ct ct res1 in | |
164 | let (res2,ct) = existswrap (ct+3) pp pv f2 in | |
165 | ("\\"^diamond^"A["^res1^" \\U "^res2^"]\n",ct) | |
166 | | CTL.EF(dir,f) -> | |
167 | let (diamond,ct) = print_diamond (ct+2) dir in | |
168 | let (res,ct) = pathwrap ct pp pv f | |
169 | in ("\\EF"^diamond^res,ct) | |
170 | | CTL.EX(dir,f) -> | |
171 | let (diamond,ct) = print_diamond (ct+2) dir in | |
172 | let (res,ct) = pathwrap ct pp pv f | |
173 | in ("\\EX"^diamond^res,ct) | |
174 | | CTL.EG(dir,f) -> | |
175 | let (diamond,ct) = print_diamond (ct+2) dir in | |
176 | let (res,ct) = pathwrap ct pp pv f | |
177 | in ("\\EG"^diamond^res,ct) | |
178 | | CTL.EU(dir,f1,f2) -> | |
179 | let (diamond,ct) = print_diamond (ct+1) dir in | |
180 | let (res1,ct) = existswrap (ct+1) pp pv f1 in | |
181 | let (res1,ct) = check_ct ct res1 in | |
182 | let (res2,ct) = existswrap (ct+3) pp pv f2 in | |
183 | ("\\E"^diamond^"["^res1^" \\U "^res2^"]\n",ct) | |
184 | | CTL.Ref(v) -> | |
185 | let (v,len) = texify(pv (make_var v)) in (v,len+ct) | |
186 | | CTL.Let(v,f1,f2) -> | |
187 | let (v,len) = texify (pv (make_var v)) in | |
188 | let (res1,ct) = letwrap (ct+len+5) pp pv f1 in | |
189 | let (res1,ct) = check_ct ct res1 in | |
190 | let (res2,ct) = letwrap (ct+3) pp pv f2 in | |
191 | let (res2,ct) = check_ct ct res2 in | |
192 | (Printf.sprintf | |
193 | "\\mita{\\sf{let}} \\, %s = %s \\, \\mita{\\sf{in}} \\, %s\n" | |
194 | v res1 res2, ct) | |
195 | | CTL.LetR(d,v,f1,f2) -> | |
196 | let (diamond,ct) = print_diamond (ct+2) d in | |
197 | let (v,len) = texify (pv (make_var v)) in | |
198 | let (res1,ct) = letwrap (ct+len+5) pp pv f1 in | |
199 | let (res1,ct) = check_ct ct res1 in | |
200 | let (res2,ct) = letwrap (ct+3) pp pv f2 in | |
201 | let (res2,ct) = check_ct ct res2 in | |
202 | (Printf.sprintf | |
203 | "\\mita{\\sf{let}}%s \\, %s = %s \\, \\mita{\\sf{in}} \\, %s\n" | |
204 | diamond v res1 res2, ct) | |
205 | | CTL.Uncheck(f) -> | |
206 | let (res,ct) = pathwrap ct pp pv f | |
207 | in (res^"^u",ct+1) | |
208 | | CTL.InnerAnd(f) -> | |
209 | let (res,ct) = pathwrap ct pp pv f | |
210 | in ("("^res^")^{innerAnd}",ct+10) | |
211 | | CTL.XX(_) -> failwith "should not be printed" | |
212 | ||
213 | and make_var x = ("",x) | |
214 | ||
215 | and wrap ct pp pv x = | |
216 | match x with | |
217 | CTL.Ref _ | CTL.False | CTL.True | CTL.Pred(_) -> ctl2c ct pp pv x | |
218 | | _ -> | |
219 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
220 | (Printf.sprintf "(%s)" res,ct+1) | |
221 | ||
222 | and andwrap ct pp pv x = | |
223 | match x with | |
224 | CTL.Ref _ | CTL.And(_,_,_) | CTL.False | CTL.True | CTL.Pred(_) -> | |
225 | ctl2c ct pp pv x | |
226 | | _ -> | |
227 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
228 | (Printf.sprintf "(%s)" res,ct+1) | |
229 | ||
230 | and orwrap ct pp pv x = | |
231 | match x with | |
232 | CTL.Ref _ | CTL.Or(_,_) | CTL.False | CTL.True | CTL.Pred(_) -> | |
233 | ctl2c ct pp pv x | |
234 | | _ -> | |
235 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
236 | (Printf.sprintf "(%s)" res,ct+1) | |
237 | ||
238 | and pathwrap ct pp pv x = | |
239 | match x with | |
240 | CTL.Ref _ | CTL.AX(_,_,_) | CTL.AF(_,_,_) | CTL.AG(_,_,_) | CTL.AU(_,_,_,_) | |
241 | | CTL.EX(_,_) | CTL.EF(_,_) | CTL.EG(_,_) | CTL.EU(_,_,_) -> | |
242 | ctl2c ct pp pv x | |
243 | | _ -> | |
244 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
245 | (Printf.sprintf "(%s)" res,ct+1) | |
246 | ||
247 | and existswrap ct pp pv x = | |
248 | match x with | |
249 | CTL.Ref _ | CTL.AX(_,_,_) | CTL.AF(_,_,_) | CTL.AG(_,_,_) | CTL.AU(_,_,_,_) | |
250 | | CTL.Pred(_) | |
251 | | CTL.EX(_,_) | CTL.EF(_,_) | CTL.EG(_,_) | CTL.EU(_,_,_) | CTL.Exists(_,_,_) | |
252 | | CTL.True | CTL.False | CTL.Not(_) -> | |
253 | ctl2c ct pp pv x | |
254 | | _ -> | |
255 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
256 | (Printf.sprintf "(%s)" res,ct+1) | |
257 | ||
258 | and letwrap ct pp pv x = | |
259 | match x with | |
260 | CTL.Let(_,_,_) -> | |
261 | let (res,ct) = ctl2c (ct+1) pp pv x in (Printf.sprintf "(%s)" res,ct+1) | |
262 | | _ -> ctl2c ct pp pv x | |
263 | ||
264 | let ctltotex rule pp pv ctls o = | |
265 | Printf.fprintf o "\\begin{quote}\\begin{verbatim}\n"; | |
266 | Printf.fprintf o "%s\n" (Pretty_print_cocci.unparse_to_string rule); | |
267 | Printf.fprintf o "\\end{verbatim}\\end{quote}\n\n"; | |
268 | List.iter | |
269 | (function ctl -> | |
270 | Printf.fprintf o "\\[\\begin{array}{l}\n"; | |
271 | let (res,_) = ctl2c 0 pp pv ctl in | |
272 | Printf.fprintf o "%s\n" res) | |
273 | ctls; | |
274 | Printf.fprintf o "\\end{array}\\]\n\n" | |
ae4735db | 275 | |
34e49164 C |
276 | let make_prelude o = Printf.fprintf o "%s\n" prelude |
277 | let make_postlude o = Printf.fprintf o "%s\n" postlude | |
278 | ||
279 | (* ----------------------------------------------------------------------- *) | |
280 | ||
281 | let meta2c (_,s) = s | |
282 | ||
283 | let pred2c = function | |
284 | Lib_engine.InLoop -> ("\\msf{InLoop}",6) | |
285 | | Lib_engine.TrueBranch -> ("\\msf{TrueBranch}",10) | |
286 | | Lib_engine.FalseBranch -> ("\\msf{FalseBranch}",11) | |
287 | | Lib_engine.After -> ("\\msf{After}",5) | |
288 | | Lib_engine.FallThrough -> ("\\msf{FallThrough}",11) | |
951c7801 | 289 | | Lib_engine.LoopFallThrough -> ("\\msf{LoopFallThrough}",15) |
34e49164 C |
290 | | Lib_engine.Return -> ("\\msf{Return}",6) |
291 | | Lib_engine.FunHeader -> ("\\msf{FunHeader}",9) | |
292 | | Lib_engine.Top -> ("\\msf{Top}",3) | |
293 | | Lib_engine.Exit -> ("\\msf{Exit}",4) | |
294 | | Lib_engine.ErrorExit -> ("\\msf{ErrorExit}",9) | |
295 | | Lib_engine.Paren(s) -> | |
296 | let s = meta2c s in | |
297 | ("\\msf{Paren}("^s^")",7+(String.length s)) | |
298 | | Lib_engine.Label(s) -> | |
299 | let s = meta2c s in | |
300 | ("\\msf{Label}("^s^")",7+(String.length s)) | |
301 | | Lib_engine.BCLabel(s) -> | |
302 | let s = meta2c s in | |
303 | ("\\msf{BreakContinueLabel}("^s^")",20+(String.length s)) | |
304 | | Lib_engine.PrefixLabel(s) -> | |
305 | let s = meta2c s in | |
306 | ("\\msf{PrefixLabel}("^s^")",13+(String.length s)) | |
307 | | Lib_engine.Match(re) -> | |
308 | let s = Pretty_print_cocci.rule_elem_to_string re in | |
309 | let (s,len) = texify s in | |
310 | (Printf.sprintf "%s" s,len) | |
311 | | Lib_engine.BindGood(nm) -> | |
312 | let s = meta2c nm in | |
313 | ("\\msf{Good}("^s^")",6+(String.length s)) | |
314 | | Lib_engine.BindBad(nm) -> | |
315 | let s = meta2c nm in | |
316 | ("\\msf{Bad}("^s^")",5+(String.length s)) | |
317 | | Lib_engine.Goto -> ("goto",4) | |
318 | | Lib_engine.FakeBrace -> ("fake\\_brace",10) | |
319 | ||
320 | let totex out_file rules ctls = | |
321 | let o = open_out out_file in | |
322 | make_prelude o; | |
323 | List.iter2 | |
324 | (function ast_list -> | |
325 | function ctls -> | |
326 | let (ctls,_) = List.split ctls in | |
327 | ctltotex ast_list pred2c (function (_,x) -> x) ctls o) | |
328 | rules ctls; | |
329 | make_postlude o; | |
330 | close_out o | |
331 |