engine/ctltotex.ml

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