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 | module CTL = Ast_ctl |
28 | ||
29 | let prelude = | |
30 | "\\documentclass{article}\n"^ | |
31 | "\\usepackage{fullpage}\n\n"^ | |
32 | "\\newcommand{\\U}{\\,\\mbox{\\sf{U}}\\,}\n"^ | |
33 | "\\newcommand{\\A}{\\mbox{\\sf{A}}}\n"^ | |
34 | "\\newcommand{\\E}{\\mbox{\\sf{E}}}\n"^ | |
35 | "\\newcommand{\\AX}{\\mbox{\\sf{AX}}}\n"^ | |
36 | "\\newcommand{\\EX}{\\mbox{\\sf{EX}}}\n"^ | |
37 | "\\newcommand{\\AF}{\\mbox{\\sf{AF}}}\n"^ | |
38 | "\\newcommand{\\EF}{\\mbox{\\sf{EF}}}\n"^ | |
39 | "\\newcommand{\\AG}{\\mbox{\\sf{AG}}}\n"^ | |
40 | "\\newcommand{\\EG}{\\mbox{\\sf{EG}}}\n\n"^ | |
41 | "\\newcommand{\\mita}[1]{\\mbox{\\it{{#1}}}}\n"^ | |
42 | "\\newcommand{\\mtt}[1]{\\mbox{\\tt{{#1}}}}\n"^ | |
43 | "\\newcommand{\\msf}[1]{\\mbox{\\sf{{#1}}}}\n"^ | |
44 | "\\newcommand{\\mrm}[1]{\\mbox{\\rm{{#1}}}}\n"^ | |
45 | "\\newcommand{\\mth}[1]{\\({#1}\\)}\n\n"^ | |
46 | "\\newcommand{\\ttlb}{\\mbox{\\tt \\char'173}}\n"^ | |
47 | "\\newcommand{\\ttrb}{\\mbox{\\tt \\char'175}}\n\n"^ | |
48 | "\\begin{document}\n" | |
49 | ||
50 | let postlude = "\\end{document}" | |
51 | ||
52 | let check_ct ct res = if ct > 60 then (res^"\\\\\\mbox{}",0) else (res,ct) | |
53 | let texify s = | |
54 | let len = String.length s in | |
55 | let rec loop n = | |
56 | if n = len | |
57 | then "" | |
58 | else | |
59 | match String.get s n with | |
60 | '_' -> Printf.sprintf "\\_%s" (loop (n+1)) | |
61 | | '{' -> Printf.sprintf "{\\ttlb}%s" (loop (n+1)) | |
62 | | '}' -> Printf.sprintf "{\\ttrb}%s" (loop (n+1)) | |
63 | | '>' -> Printf.sprintf "\\mth{>}%s" (loop (n+1)) | |
64 | | c -> Printf.sprintf "%c%s" c (loop (n+1)) in | |
65 | (Printf.sprintf "\\mita{%s}" (loop 0),len) | |
66 | ||
67 | let modif2c pv = function | |
68 | CTL.Modif(v) -> let (s,n) = texify(pv v) in (Printf.sprintf "_{%s}" s,n) | |
69 | | CTL.UnModif(v) -> let (s,n) = texify(pv v) in (Printf.sprintf "_{%s}" s,n) | |
70 | | CTL.Control -> ("",0) | |
71 | ||
72 | let print_diamond ct = function | |
73 | CTL.FORWARD -> ("",ct) | |
74 | | CTL.BACKWARD -> ("\\Delta",ct+1) | |
75 | ||
76 | let rec ctl2c ct pp pv = function | |
77 | CTL.False -> ("\\msf{false}",5) | |
78 | | CTL.True -> ("\\msf{true}",4) | |
79 | | CTL.Pred(p,v) -> | |
80 | let (res,n) = pp p in | |
81 | let (resv,n1) = modif2c pv v in | |
82 | (res^resv,ct+n+n1) | |
83 | | CTL.Not(f) -> | |
84 | let (res,ct) = wrap (ct+1) pp pv f in | |
85 | ("\\neg "^res,ct) | |
86 | | CTL.Exists(_,v,f) -> | |
87 | let (res1,len) = texify(pv v) in | |
88 | let ct = ct + len in | |
89 | let (res1,ct) = check_ct ct res1 in | |
90 | let (res2,ct) = existswrap (ct+1) pp pv f in | |
91 | ("\\exists "^res1^" . "^res2,ct) | |
92 | | CTL.And(_,f1,f2) -> | |
93 | let (res1,ct) = andwrap ct pp pv f1 in | |
94 | let (res1,ct) = check_ct ct res1 in | |
95 | let (res2,ct) = andwrap (ct+1) pp pv f2 in | |
96 | (res1^" \\wedge "^res2,ct) | |
97 | | CTL.AndAny(dir,_,f1,f2) -> | |
98 | let (diamond,ct) = print_diamond (ct+2) dir in | |
99 | let (res1,ct) = andwrap ct pp pv f1 in | |
100 | let (res1,ct) = check_ct ct res1 in | |
101 | let (res2,ct) = andwrap (ct+1) pp pv f2 in | |
102 | (res1^" \\wedge? "^diamond^res2,ct) | |
103 | | CTL.HackForStmt(dir,_,f1,f2) -> | |
104 | let (diamond,ct) = print_diamond (ct+2) dir in | |
105 | let (res1,ct) = andwrap ct pp pv f1 in | |
106 | let (res1,ct) = check_ct ct res1 in | |
107 | let (res2,ct) = andwrap (ct+1) pp pv f2 in | |
108 | (res1^" \\wedge{h} "^diamond^res2,ct) | |
109 | | CTL.Or(f1,f2) -> | |
110 | let (res1,ct) = orwrap ct pp pv f1 in | |
111 | let (res1,ct) = check_ct ct res1 in | |
112 | let (res2,ct) = orwrap (ct+1) pp pv f2 in | |
113 | (res1^" \\vee "^res2,ct) | |
114 | | CTL.SeqOr(f1,f2) -> | |
115 | let (res1,ct) = orwrap ct pp pv f1 in | |
116 | let (res1,ct) = check_ct ct res1 in | |
117 | let (res2,ct) = orwrap (ct+1) pp pv f2 in | |
118 | (res1^" \\mid "^res2,ct) | |
119 | | CTL.Implies(f1,f2) -> | |
120 | let (res1,ct) = wrap ct pp pv f1 in | |
121 | let (res1,ct) = check_ct ct res1 in | |
122 | let (res2,ct) = wrap (ct+1) pp pv f2 in | |
123 | (res1^" \\rightarrow "^res2,ct) | |
124 | | CTL.AF(dir,_,f) -> | |
125 | let (diamond,ct) = print_diamond (ct+2) dir in | |
126 | let (res,ct) = pathwrap ct pp pv f | |
127 | in ("\\AF"^diamond^res,ct) | |
128 | | CTL.AX(dir,_,f) -> | |
129 | let (diamond,ct) = print_diamond (ct+2) dir in | |
130 | let (res,ct) = pathwrap ct pp pv f | |
131 | in ("\\AX"^diamond^res,ct) | |
132 | | CTL.AG(dir,_,f) -> | |
133 | let (diamond,ct) = print_diamond (ct+2) dir in | |
134 | let (res,ct) = pathwrap ct pp pv f | |
135 | in ("\\AG"^diamond^res,ct) | |
136 | | CTL.AW(dir,_,f1,f2) -> | |
137 | let (diamond,ct) = print_diamond (ct+1) dir in | |
138 | let (res1,ct) = existswrap (ct+1) pp pv f1 in | |
139 | let (res1,ct) = check_ct ct res1 in | |
140 | let (res2,ct) = existswrap (ct+3) pp pv f2 in | |
141 | ("\\"^diamond^"A["^res1^" W "^res2^"]\n",ct) | |
142 | | CTL.AU(dir,_,f1,f2) -> | |
143 | let (diamond,ct) = print_diamond (ct+1) dir in | |
144 | let (res1,ct) = existswrap (ct+1) pp pv f1 in | |
145 | let (res1,ct) = check_ct ct res1 in | |
146 | let (res2,ct) = existswrap (ct+3) pp pv f2 in | |
147 | ("\\"^diamond^"A["^res1^" \\U "^res2^"]\n",ct) | |
148 | | CTL.EF(dir,f) -> | |
149 | let (diamond,ct) = print_diamond (ct+2) dir in | |
150 | let (res,ct) = pathwrap ct pp pv f | |
151 | in ("\\EF"^diamond^res,ct) | |
152 | | CTL.EX(dir,f) -> | |
153 | let (diamond,ct) = print_diamond (ct+2) dir in | |
154 | let (res,ct) = pathwrap ct pp pv f | |
155 | in ("\\EX"^diamond^res,ct) | |
156 | | CTL.EG(dir,f) -> | |
157 | let (diamond,ct) = print_diamond (ct+2) dir in | |
158 | let (res,ct) = pathwrap ct pp pv f | |
159 | in ("\\EG"^diamond^res,ct) | |
160 | | CTL.EU(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 | ("\\E"^diamond^"["^res1^" \\U "^res2^"]\n",ct) | |
166 | | CTL.Ref(v) -> | |
167 | let (v,len) = texify(pv (make_var v)) in (v,len+ct) | |
168 | | CTL.Let(v,f1,f2) -> | |
169 | let (v,len) = texify (pv (make_var v)) in | |
170 | let (res1,ct) = letwrap (ct+len+5) pp pv f1 in | |
171 | let (res1,ct) = check_ct ct res1 in | |
172 | let (res2,ct) = letwrap (ct+3) pp pv f2 in | |
173 | let (res2,ct) = check_ct ct res2 in | |
174 | (Printf.sprintf | |
175 | "\\mita{\\sf{let}} \\, %s = %s \\, \\mita{\\sf{in}} \\, %s\n" | |
176 | v res1 res2, ct) | |
177 | | CTL.LetR(d,v,f1,f2) -> | |
178 | let (diamond,ct) = print_diamond (ct+2) d in | |
179 | let (v,len) = texify (pv (make_var v)) in | |
180 | let (res1,ct) = letwrap (ct+len+5) pp pv f1 in | |
181 | let (res1,ct) = check_ct ct res1 in | |
182 | let (res2,ct) = letwrap (ct+3) pp pv f2 in | |
183 | let (res2,ct) = check_ct ct res2 in | |
184 | (Printf.sprintf | |
185 | "\\mita{\\sf{let}}%s \\, %s = %s \\, \\mita{\\sf{in}} \\, %s\n" | |
186 | diamond v res1 res2, ct) | |
187 | | CTL.Uncheck(f) -> | |
188 | let (res,ct) = pathwrap ct pp pv f | |
189 | in (res^"^u",ct+1) | |
190 | | CTL.InnerAnd(f) -> | |
191 | let (res,ct) = pathwrap ct pp pv f | |
192 | in ("("^res^")^{innerAnd}",ct+10) | |
193 | | CTL.XX(_) -> failwith "should not be printed" | |
194 | ||
195 | and make_var x = ("",x) | |
196 | ||
197 | and wrap ct pp pv x = | |
198 | match x with | |
199 | CTL.Ref _ | CTL.False | CTL.True | CTL.Pred(_) -> ctl2c ct pp pv x | |
200 | | _ -> | |
201 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
202 | (Printf.sprintf "(%s)" res,ct+1) | |
203 | ||
204 | and andwrap ct pp pv x = | |
205 | match x with | |
206 | CTL.Ref _ | CTL.And(_,_,_) | CTL.False | CTL.True | CTL.Pred(_) -> | |
207 | ctl2c ct pp pv x | |
208 | | _ -> | |
209 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
210 | (Printf.sprintf "(%s)" res,ct+1) | |
211 | ||
212 | and orwrap ct pp pv x = | |
213 | match x with | |
214 | CTL.Ref _ | CTL.Or(_,_) | CTL.False | CTL.True | CTL.Pred(_) -> | |
215 | ctl2c ct pp pv x | |
216 | | _ -> | |
217 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
218 | (Printf.sprintf "(%s)" res,ct+1) | |
219 | ||
220 | and pathwrap ct pp pv x = | |
221 | match x with | |
222 | CTL.Ref _ | CTL.AX(_,_,_) | CTL.AF(_,_,_) | CTL.AG(_,_,_) | CTL.AU(_,_,_,_) | |
223 | | CTL.EX(_,_) | CTL.EF(_,_) | CTL.EG(_,_) | CTL.EU(_,_,_) -> | |
224 | ctl2c ct pp pv x | |
225 | | _ -> | |
226 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
227 | (Printf.sprintf "(%s)" res,ct+1) | |
228 | ||
229 | and existswrap ct pp pv x = | |
230 | match x with | |
231 | CTL.Ref _ | CTL.AX(_,_,_) | CTL.AF(_,_,_) | CTL.AG(_,_,_) | CTL.AU(_,_,_,_) | |
232 | | CTL.Pred(_) | |
233 | | CTL.EX(_,_) | CTL.EF(_,_) | CTL.EG(_,_) | CTL.EU(_,_,_) | CTL.Exists(_,_,_) | |
234 | | CTL.True | CTL.False | CTL.Not(_) -> | |
235 | ctl2c ct pp pv x | |
236 | | _ -> | |
237 | let (res,ct) = ctl2c (ct+1) pp pv x in | |
238 | (Printf.sprintf "(%s)" res,ct+1) | |
239 | ||
240 | and letwrap ct pp pv x = | |
241 | match x with | |
242 | CTL.Let(_,_,_) -> | |
243 | let (res,ct) = ctl2c (ct+1) pp pv x in (Printf.sprintf "(%s)" res,ct+1) | |
244 | | _ -> ctl2c ct pp pv x | |
245 | ||
246 | let ctltotex rule pp pv ctls o = | |
247 | Printf.fprintf o "\\begin{quote}\\begin{verbatim}\n"; | |
248 | Printf.fprintf o "%s\n" (Pretty_print_cocci.unparse_to_string rule); | |
249 | Printf.fprintf o "\\end{verbatim}\\end{quote}\n\n"; | |
250 | List.iter | |
251 | (function ctl -> | |
252 | Printf.fprintf o "\\[\\begin{array}{l}\n"; | |
253 | let (res,_) = ctl2c 0 pp pv ctl in | |
254 | Printf.fprintf o "%s\n" res) | |
255 | ctls; | |
256 | Printf.fprintf o "\\end{array}\\]\n\n" | |
ae4735db | 257 | |
34e49164 C |
258 | let make_prelude o = Printf.fprintf o "%s\n" prelude |
259 | let make_postlude o = Printf.fprintf o "%s\n" postlude | |
260 | ||
261 | (* ----------------------------------------------------------------------- *) | |
262 | ||
263 | let meta2c (_,s) = s | |
264 | ||
265 | let pred2c = function | |
266 | Lib_engine.InLoop -> ("\\msf{InLoop}",6) | |
267 | | Lib_engine.TrueBranch -> ("\\msf{TrueBranch}",10) | |
268 | | Lib_engine.FalseBranch -> ("\\msf{FalseBranch}",11) | |
269 | | Lib_engine.After -> ("\\msf{After}",5) | |
270 | | Lib_engine.FallThrough -> ("\\msf{FallThrough}",11) | |
951c7801 | 271 | | Lib_engine.LoopFallThrough -> ("\\msf{LoopFallThrough}",15) |
34e49164 C |
272 | | Lib_engine.Return -> ("\\msf{Return}",6) |
273 | | Lib_engine.FunHeader -> ("\\msf{FunHeader}",9) | |
5427db06 | 274 | | Lib_engine.UnsafeBrace -> ("\\msf{UnsafeBrace}",11) |
34e49164 C |
275 | | Lib_engine.Top -> ("\\msf{Top}",3) |
276 | | Lib_engine.Exit -> ("\\msf{Exit}",4) | |
277 | | Lib_engine.ErrorExit -> ("\\msf{ErrorExit}",9) | |
278 | | Lib_engine.Paren(s) -> | |
279 | let s = meta2c s in | |
280 | ("\\msf{Paren}("^s^")",7+(String.length s)) | |
281 | | Lib_engine.Label(s) -> | |
282 | let s = meta2c s in | |
283 | ("\\msf{Label}("^s^")",7+(String.length s)) | |
284 | | Lib_engine.BCLabel(s) -> | |
285 | let s = meta2c s in | |
286 | ("\\msf{BreakContinueLabel}("^s^")",20+(String.length s)) | |
287 | | Lib_engine.PrefixLabel(s) -> | |
288 | let s = meta2c s in | |
289 | ("\\msf{PrefixLabel}("^s^")",13+(String.length s)) | |
290 | | Lib_engine.Match(re) -> | |
291 | let s = Pretty_print_cocci.rule_elem_to_string re in | |
292 | let (s,len) = texify s in | |
293 | (Printf.sprintf "%s" s,len) | |
294 | | Lib_engine.BindGood(nm) -> | |
295 | let s = meta2c nm in | |
296 | ("\\msf{Good}("^s^")",6+(String.length s)) | |
297 | | Lib_engine.BindBad(nm) -> | |
298 | let s = meta2c nm in | |
299 | ("\\msf{Bad}("^s^")",5+(String.length s)) | |
300 | | Lib_engine.Goto -> ("goto",4) | |
301 | | Lib_engine.FakeBrace -> ("fake\\_brace",10) | |
302 | ||
303 | let totex out_file rules ctls = | |
304 | let o = open_out out_file in | |
305 | make_prelude o; | |
306 | List.iter2 | |
307 | (function ast_list -> | |
308 | function ctls -> | |
309 | let (ctls,_) = List.split ctls in | |
310 | ctltotex ast_list pred2c (function (_,x) -> x) ctls o) | |
311 | rules ctls; | |
312 | make_postlude o; | |
313 | close_out o | |
314 |