engine/ctltotex.ml

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