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