engine/ctltotex.ml

   1 (*
   2  * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
   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
  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
  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"
 275
 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)
 289   | Lib_engine.LoopFallThrough -> ("\\msf{LoopFallThrough}",15)
 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