engine/ctltotex.ml

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