engine/ctltotex.ml

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