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