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