Coccinelle release-1.0.0-rc11

[bpt/coccinelle.git] / engine / asttoctl2.ml

(*
 * Copyright 2012, INRIA
 * Julia Lawall, Gilles Muller
 * Copyright 2010-2011, INRIA, University of Copenhagen
 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
 * This file is part of Coccinelle.
 *
 * Coccinelle is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, according to version 2 of the License.
 *
 * Coccinelle is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
 *
 * The authors reserve the right to distribute this or future versions of
 * Coccinelle under other licenses.
 *)


(* for MINUS and CONTEXT, pos is always None in this file *)
(*search for require*)
(* true = don't see all matched nodes, only modified ones *)
let onlyModif = ref true(*false*)

type ex = Exists | Forall
let exists = ref Forall

module Ast = Ast_cocci
module V = Visitor_ast
module CTL = Ast_ctl

let warning s = Printf.fprintf stderr "warning: %s\n" s

type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
type formula = Lib_engine.ctlcocci
type top_formula = NONDECL of Lib_engine.ctlcocci | CODE of Lib_engine.ctlcocci

let union = Common.union_set
let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1
let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1

let foldl1 f xs = List.fold_left f (List.hd xs) (List.tl xs)
let foldr1 f xs =
  let xs = List.rev xs in List.fold_left f (List.hd xs) (List.tl xs)

let used_after = ref ([] : Ast.meta_name list)
let guard_to_strict guard = if guard then CTL.NONSTRICT else CTL.STRICT

let saved = ref ([] : Ast.meta_name list)

let string2var x = ("",x)

(* --------------------------------------------------------------------- *)
(* predicates matching various nodes in the graph *)

let ctl_and s x y    =
  match (x,y) with
    (CTL.False,_) | (_,CTL.False) -> CTL.False
  | (CTL.True,a) | (a,CTL.True) -> a
  | _ -> CTL.And(s,x,y)

let ctl_or x y     =
  match (x,y) with
    (CTL.True,_) | (_,CTL.True) -> CTL.True
  | (CTL.False,a) | (a,CTL.False) -> a
  | _ -> CTL.Or(x,y)

let ctl_or_fl x y     =
  match (x,y) with
    (CTL.True,_) | (_,CTL.True) -> CTL.True
  | (CTL.False,a) | (a,CTL.False) -> a
  | _ -> CTL.Or(y,x)

let ctl_seqor x y     =
  match (x,y) with
    (* drop x or true case because x might have side effects *)
    (CTL.True,_) (* | (_,CTL.True) *) -> CTL.True
  | (CTL.False,a) | (a,CTL.False) -> a
  | _ -> CTL.SeqOr(x,y)

let ctl_not = function
    CTL.True -> CTL.False
  | CTL.False -> CTL.True
  | x -> CTL.Not(x)

let ctl_ax s = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x ->
      match !exists with
	Exists -> CTL.EX(CTL.FORWARD,x)
      |	Forall -> CTL.AX(CTL.FORWARD,s,x)

let ctl_ax_absolute s = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.AX(CTL.FORWARD,s,x)

let ctl_ex = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.EX(CTL.FORWARD,x)

(* This stays being AX even for sgrep_mode, because it is used to identify
the structure of the term, not matching the pattern. *)
let ctl_back_ag = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.AG(CTL.BACKWARD,CTL.NONSTRICT,x)

let ctl_back_ax = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.AX(CTL.BACKWARD,CTL.NONSTRICT,x)

let ctl_back_ex = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.EX(CTL.BACKWARD,x)

let ctl_ef = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.EF(CTL.FORWARD,x)

let ctl_ag s = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.AG(CTL.FORWARD,s,x)

let ctl_au s x y =
  match (x,!exists) with
    (CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y)
  | (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y)
  | (_,Exists) -> CTL.EU(CTL.FORWARD,x,y)
  | (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y)

let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *)
  CTL.XX
    (match (x,!exists) with
      (CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y)
    | (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y)
    | (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y)
    | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y))

let ctl_uncheck = function
    CTL.True -> CTL.True
  | CTL.False -> CTL.False
  | x -> CTL.Uncheck x

let label_pred_maker = function
    None -> CTL.True
  | Some (label_var,used) ->
      used := true;
      CTL.Pred(Lib_engine.PrefixLabel(label_var),CTL.Control)

let bclabel_pred_maker = function
    None -> CTL.True
  | Some (label_var,used) ->
      used := true;
      CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control)

(* label used to be used here, but it is not used; label is only needed after
and within dots *)
let predmaker guard pred label = CTL.Pred pred

let aftpred     = predmaker false (Lib_engine.After,       CTL.Control)
let retpred     = predmaker false (Lib_engine.Return,      CTL.Control)
let funpred     = predmaker false (Lib_engine.FunHeader,   CTL.Control)
let unsbrpred   = predmaker false (Lib_engine.UnsafeBrace, CTL.Control)
let toppred     = predmaker false (Lib_engine.Top,         CTL.Control)
let exitpred    = predmaker false (Lib_engine.ErrorExit,   CTL.Control)
let endpred     = predmaker false (Lib_engine.Exit,        CTL.Control)
let gotopred    = predmaker false (Lib_engine.Goto,        CTL.Control)
let inlooppred  = predmaker false (Lib_engine.InLoop,      CTL.Control)
let truepred    = predmaker false (Lib_engine.TrueBranch,  CTL.Control)
let falsepred   = predmaker false (Lib_engine.FalseBranch, CTL.Control)
let fallpred    = predmaker false (Lib_engine.FallThrough, CTL.Control)
let loopfallpred = predmaker false (Lib_engine.LoopFallThrough, CTL.Control)

(*let aftret label_var =
  ctl_or (aftpred label_var)
    (ctl_or (loopfallpred label_var) (exitpred label_var))*)

let letctr = ref 0
let get_let_ctr _ =
  let cur = !letctr in
  letctr := cur + 1;
  Printf.sprintf "r%d" cur

(* --------------------------------------------------------------------- *)
(* --------------------------------------------------------------------- *)
(* Eliminate OptStm *)

(* for optional thing with nothing after, should check that the optional thing
never occurs.  otherwise the matching stops before it occurs *)
let elim_opt =
  let mcode x = x in
  let donothing r k e = k e in

  let fvlist l =
    List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in

  let mfvlist l =
    List.fold_left Common.union_set [] (List.map Ast.get_mfvs l) in

  let freshlist l =
    List.fold_left Common.union_set [] (List.map Ast.get_fresh l) in

  let inheritedlist l =
    List.fold_left Common.union_set [] (List.map Ast.get_inherited l) in

  let savedlist l =
    List.fold_left Common.union_set [] (List.map Ast.get_saved l) in

  let varlists l =
    (fvlist l, mfvlist l, freshlist l, inheritedlist l, savedlist l) in

  let rec dots_list unwrapped wrapped =
    match (unwrapped,wrapped) with
      ([],_) -> []

    | (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
       d0::s::d1::rest)
    | (Ast.Nest(_,_,_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)
       ::urest,
       d0::s::d1::rest) -> (* why no case for nest as u? *)
	 let l = Ast.get_line stm in
	 let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
	 let new_rest2 = dots_list urest rest in
	 let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) =
	   varlists new_rest1 in
	 let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) =
	   varlists new_rest2 in
	 [d0;
	   {(Ast.make_term
	       (Ast.Disj
		  [{(Ast.make_term(Ast.DOTS(new_rest1))) with
		     Ast.node_line = l;
		     Ast.free_vars = fv_rest1;
		     Ast.minus_free_vars = mfv_rest1;
		     Ast.fresh_vars = fresh_rest1;
		     Ast.inherited = inherited_rest1;
		     Ast.saved_witness = s1};
		    {(Ast.make_term(Ast.DOTS(new_rest2))) with
		      Ast.node_line = l;
		      Ast.free_vars = fv_rest2;
		      Ast.minus_free_vars = mfv_rest2;
		      Ast.fresh_vars = fresh_rest2;
		      Ast.inherited = inherited_rest2;
		      Ast.saved_witness = s2}])) with
	     Ast.node_line = l;
	     Ast.free_vars = fv_rest1;
	     Ast.minus_free_vars = mfv_rest1;
	     Ast.fresh_vars = fresh_rest1;
	     Ast.inherited = inherited_rest1;
	     Ast.saved_witness = s1}]

    | (Ast.OptStm(stm)::urest,_::rest) ->
	 let l = Ast.get_line stm in
	 let new_rest1 = dots_list urest rest in
	 let new_rest2 = stm::new_rest1 in
	 let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) =
	   varlists new_rest1 in
	 let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) =
	   varlists new_rest2 in
	 [{(Ast.make_term
	       (Ast.Disj
		  [{(Ast.make_term(Ast.DOTS(new_rest2))) with
		      Ast.node_line = l;
		      Ast.free_vars = fv_rest2;
		      Ast.minus_free_vars = mfv_rest2;
		      Ast.fresh_vars = fresh_rest2;
		      Ast.inherited = inherited_rest2;
		      Ast.saved_witness = s2};
		    {(Ast.make_term(Ast.DOTS(new_rest1))) with
		     Ast.node_line = l;
		     Ast.free_vars = fv_rest1;
		     Ast.minus_free_vars = mfv_rest1;
		     Ast.fresh_vars = fresh_rest1;
		     Ast.inherited = inherited_rest1;
		     Ast.saved_witness = s1}])) with
	     Ast.node_line = l;
	     Ast.free_vars = fv_rest2;
	     Ast.minus_free_vars = mfv_rest2;
	     Ast.fresh_vars = fresh_rest2;
	     Ast.inherited = inherited_rest2;
	     Ast.saved_witness = s2}]

    | ([Ast.Dots(_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
	let l = Ast.get_line stm in
	let fv_stm = Ast.get_fvs stm in
	let mfv_stm = Ast.get_mfvs stm in
	let fresh_stm = Ast.get_fresh stm in
	let inh_stm = Ast.get_inherited stm in
	let saved_stm = Ast.get_saved stm in
	let fv_d1 = Ast.get_fvs d1 in
	let mfv_d1 = Ast.get_mfvs d1 in
	let fresh_d1 = Ast.get_fresh d1 in
	let inh_d1 = Ast.get_inherited d1 in
	let saved_d1 = Ast.get_saved d1 in
	let fv_both = Common.union_set fv_stm fv_d1 in
	let mfv_both = Common.union_set mfv_stm mfv_d1 in
	let fresh_both = Common.union_set fresh_stm fresh_d1 in
	let inh_both = Common.union_set inh_stm inh_d1 in
	let saved_both = Common.union_set saved_stm saved_d1 in
	[d1;
	  {(Ast.make_term
	      (Ast.Disj
		 [{(Ast.make_term(Ast.DOTS([stm]))) with
		    Ast.node_line = l;
		    Ast.free_vars = fv_stm;
		    Ast.minus_free_vars = mfv_stm;
		    Ast.fresh_vars = fresh_stm;
		    Ast.inherited = inh_stm;
		    Ast.saved_witness = saved_stm};
		   {(Ast.make_term(Ast.DOTS([d1]))) with
		     Ast.node_line = l;
		     Ast.free_vars = fv_d1;
		     Ast.minus_free_vars = mfv_d1;
		     Ast.fresh_vars = fresh_d1;
		     Ast.inherited = inh_d1;
		     Ast.saved_witness = saved_d1}])) with
	     Ast.node_line = l;
	     Ast.free_vars = fv_both;
	     Ast.minus_free_vars = mfv_both;
	     Ast.fresh_vars = fresh_both;
	     Ast.inherited = inh_both;
	     Ast.saved_witness = saved_both}]

    | ([Ast.Nest(_,_,_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
	let l = Ast.get_line stm in
	let rw = Ast.rewrap stm in
	let rwd = Ast.rewrap stm in
	let dots = Ast.Dots(Ast.make_mcode "...",[],[],[]) in
	[d1;rw(Ast.Disj
		 [rwd(Ast.DOTS([stm]));
		   {(Ast.make_term(Ast.DOTS([rw dots])))
		   with Ast.node_line = l}])]

    | (_::urest,stm::rest) -> stm :: (dots_list urest rest)
    | _ -> failwith "not possible" in

  let stmtdotsfn r k d =
    let d = k d in
    Ast.rewrap d
      (match Ast.unwrap d with
	Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
      | Ast.CIRCLES(l) -> failwith "elimopt: not supported"
      | Ast.STARS(l) -> failwith "elimopt: not supported") in

  V.rebuilder
    mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
    donothing donothing stmtdotsfn donothing donothing
    donothing donothing donothing donothing donothing donothing donothing
    donothing donothing donothing donothing donothing

(* --------------------------------------------------------------------- *)
(* after management *)
(* We need Guard for the following case:
<...
 a
 <...
  b
 ...>
...>
foo();

Here the inner <... b ...> should not go past foo.  But foo is not the
"after" of the body of the outer nest, because we don't want to search for
it in the case where the body of the outer nest ends in something other
than dots or a nest. *)

(* what is the difference between tail and end??? *)

type after = After of formula | Guard of formula | Tail | End | VeryEnd

type top = Top | NotTop

let a2n = function After x -> Guard x | a -> a

let print_ctl x =
  let pp_pred (x,_) = Pretty_print_engine.pp_predicate x in
  let pp_meta (_,x) = Common.pp x in
  Pretty_print_ctl.pp_ctl (pp_pred,pp_meta) false x;
  Format.print_newline()

let print_after = function
    After ctl -> Printf.printf "After:\n"; print_ctl ctl
  | Guard ctl -> Printf.printf "Guard:\n"; print_ctl ctl
  | Tail -> Printf.printf "Tail\n"
  | VeryEnd -> Printf.printf "Very End\n"
  | End -> Printf.printf "End\n"

(* --------------------------------------------------------------------- *)
(* Top-level code *)

let fresh_var _ = string2var "_v"
let fresh_pos _ = string2var "_pos" (* must be a constant *)

let fresh_metavar _ = "_S"

(* fvinfo is going to end up being from the whole associated statement.
   it would be better if it were just the free variables in d, but free_vars.ml
   doesn't keep track of free variables on + code *)
let make_meta_rule_elem d fvinfo =
  let nm = fresh_metavar() in
  Ast.make_meta_rule_elem nm d fvinfo

let get_unquantified quantified vars =
  List.filter (function x -> not (List.mem x quantified)) vars

let make_seq guard l =
  let s = guard_to_strict guard in
  foldr1 (function rest -> function cur -> ctl_and s cur (ctl_ax s rest)) l

let make_seq_after2 guard first rest =
  let s = guard_to_strict guard in
  match rest with
    After rest -> ctl_and s first (ctl_ax s (ctl_ax s rest))
  | _ -> first

let make_seq_after guard first rest =
  match rest with
    After rest -> make_seq guard [first;rest]
  | _ -> first

let opt_and guard first rest =
  let s = guard_to_strict guard in
  match first with
    None -> rest
  | Some first -> ctl_and s first rest

let and_after guard first rest =
  let s = guard_to_strict guard in
  match rest with After rest -> ctl_and s first rest | _ -> first

let contains_modif =
  let bind x y = x or y in
  let option_default = false in
  let mcode r (_,_,kind,metapos) =
    match kind with
      Ast.MINUS(_,_,_,_) -> true
    | Ast.PLUS _ -> failwith "not possible"
    | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
  let do_nothing r k e = k e in
  let rule_elem r k re =
    let res = k re in
    match Ast.unwrap re with
      Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
	bind (mcode r ((),(),bef,[])) res
    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res
    | _ -> res in
  let init r k i =
    let res = k i in
    match Ast.unwrap i with
      Ast.StrInitList(allminus,_,_,_,_) -> allminus or res
    | _ -> res in
  let recursor =
    V.combiner bind option_default
      mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
      do_nothing do_nothing do_nothing do_nothing do_nothing
      do_nothing do_nothing do_nothing do_nothing init do_nothing
      do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
  recursor.V.combiner_rule_elem

let contains_pos =
  let bind x y = x or y in
  let option_default = false in
  let mcode r (_,_,kind,metapos) = not (metapos = []) in
  let do_nothing r k e = k e in
  let rule_elem r k re =
    let res = k re in
    match Ast.unwrap re with
      Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
	bind (mcode r ((),(),bef,[])) res
    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res
    | _ -> res in
  let recursor =
    V.combiner bind option_default
      mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
      do_nothing do_nothing do_nothing do_nothing do_nothing
      do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
      do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
  recursor.V.combiner_rule_elem

(* code is not a DisjRuleElem *)
let make_match label guard code =
  let v = fresh_var() in
  let matcher = Lib_engine.Match(code) in
  if contains_modif code && not guard
  then CTL.Exists(true,v,predmaker guard (matcher,CTL.Modif v) label)
  else
    let iso_info = !Flag.track_iso_usage && not (Ast.get_isos code = []) in
    (match (iso_info,!onlyModif,guard,
	    intersect !used_after (Ast.get_fvs code)) with
      (false,true,_,[]) | (_,_,true,_) ->
	predmaker guard (matcher,CTL.Control) label
    | _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))

let make_raw_match label guard code =
  match intersect !used_after (Ast.get_fvs code) with
    [] -> predmaker guard (Lib_engine.Match(code),CTL.Control) label
  | _ ->
      let v = fresh_var() in
    CTL.Exists(true,v,predmaker guard (Lib_engine.Match(code),CTL.UnModif v)
		 label)

let rec seq_fvs quantified = function
    [] -> []
  | fv1::fvs ->
      let t1fvs = get_unquantified quantified fv1 in
      let termfvs =
	List.fold_left Common.union_set []
	  (List.map (get_unquantified quantified) fvs) in
      let bothfvs = Common.inter_set t1fvs termfvs in
      let t1onlyfvs = Common.minus_set t1fvs bothfvs in
      let new_quantified = Common.union_set bothfvs quantified in
      (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs)

let quantify guard =
  List.fold_right
    (function cur ->
      function code -> CTL.Exists (not guard && List.mem cur !saved,cur,code))

let non_saved_quantify =
  List.fold_right
    (function cur -> function code -> CTL.Exists (false,cur,code))

let intersectll lst nested_list =
  List.filter (function x -> List.exists (List.mem x) nested_list) lst

(* --------------------------------------------------------------------- *)
(* Count depth of braces.  The translation of a closed brace appears deeply
nested within the translation of the sequence term, so the name of the
paren var has to take into account the names of the nested braces.  On the
other hand the close brace does not escape, so we don't have to take into
account other paren variable names. *)

(* called repetitively, which is inefficient, but less trouble than adding a
new field to Seq and FunDecl *)
let count_nested_braces s =
  let bind x y = max x y in
  let option_default = 0 in
  let stmt_count r k s =
    match Ast.unwrap s with
      Ast.Seq(_,_,_) | Ast.FunDecl(_,_,_,_) -> (k s) + 1
    | _ -> k s in
  let donothing r k e = k e in
  let mcode r x = 0 in
  let recursor = V.combiner bind option_default
      mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
      donothing donothing donothing donothing donothing
      donothing donothing donothing donothing donothing donothing
      donothing donothing stmt_count donothing donothing donothing in
  let res = string_of_int (recursor.V.combiner_statement s) in
  string2var ("p"^res)

let labelctr = ref 0
let get_label_ctr _ =
  let cur = !labelctr in
  labelctr := cur + 1;
  string2var (Printf.sprintf "l%d" cur)

(* --------------------------------------------------------------------- *)
(* annotate dots with before and after neighbors *)

let print_bef_aft = function
    Ast.WParen (re,n) ->
      Printf.printf "bef/aft\n";
      Pretty_print_cocci.rule_elem "" re;
      Format.print_newline()
  | Ast.Other s ->
      Printf.printf "bef/aft\n";
      Pretty_print_cocci.statement "" s;
      Format.print_newline()
  | Ast.Other_dots d ->
      Printf.printf "bef/aft\n";
      Pretty_print_cocci.statement_dots d;
      Format.print_newline()

(* [] can only occur if we are in a disj, where it comes from a ?  In that
case, we want to use a, which accumulates all of the previous patterns in
their entirety. *)
let rec get_before_elem sl a =
  match Ast.unwrap sl with
    Ast.DOTS(x) ->
      let rec loop sl a =
	match sl with
	  [] -> ([],Common.Right a)
	| [e] ->
	    let (e,ea) = get_before_e e a in
	    ([e],Common.Left ea)
	| e::sl ->
	    let (e,ea) = get_before_e e a in
	    let (sl,sla) = loop sl ea in
	    (e::sl,sla) in
      let (l,a) = loop x a in
      (Ast.rewrap sl (Ast.DOTS(l)),a)
  | Ast.CIRCLES(x) -> failwith "not supported"
  | Ast.STARS(x) -> failwith "not supported"

and get_before sl a =
  match get_before_elem sl a with
    (term,Common.Left x) -> (term,x)
  | (term,Common.Right x) -> (term,x)

and get_before_whencode wc =
  List.map
    (function
	Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w
      | Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w
      |	Ast.WhenModifier(x) -> Ast.WhenModifier(x)
      | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
      | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
    wc

and get_before_e s a =
  match Ast.unwrap s with
    Ast.Dots(d,w,_,aft) ->
      (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)
  | Ast.Nest(starter,stmt_dots,ender,w,multi,_,aft) ->
      let w = get_before_whencode w in
      let (sd,_) = get_before stmt_dots a in
      (*let a =
	got rid of this, don't want to let nests overshoot
	List.filter
	  (function
	      Ast.Other a ->
		let unifies =
		  Unify_ast.unify_statement_dots
		    (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
		(match unifies with
		  Unify_ast.MAYBE -> false
		| _ -> true)
	    | Ast.Other_dots a ->
		let unifies = Unify_ast.unify_statement_dots a stmt_dots in
		(match unifies with
		  Unify_ast.MAYBE -> false
		| _ -> true)
	    | _ -> true)
	  a in*)
      (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,a,aft)),
       [Ast.Other_dots stmt_dots])
  | Ast.Disj(stmt_dots_list) ->
      let (dsl,dsla) =
	List.split (List.map (function e -> get_before e a) stmt_dots_list) in
      (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
  | Ast.Atomic(ast) ->
      (match Ast.unwrap ast with
	Ast.MetaStmt(_,_,_,_) -> (s,[])
      |	_ -> (s,[Ast.Other s]))
  | Ast.Seq(lbrace,body,rbrace) ->
      let index = count_nested_braces s in
      let (bd,_) = get_before body [Ast.WParen(lbrace,index)] in
      (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),[Ast.WParen(rbrace,index)])
  | Ast.Define(header,body) ->
      let (body,_) = get_before body [] in
      (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
  | Ast.AsStmt(stmt,asstmt) ->
      let (stmt,_) = get_before_e stmt [] in
      let (asstmt,_) = get_before_e asstmt [] in
      (Ast.rewrap s (Ast.AsStmt(stmt,asstmt)),[Ast.Other s])
  | Ast.IfThen(ifheader,branch,aft) ->
      let (br,_) = get_before_e branch [] in
      (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s])
  | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
      let (br1,_) = get_before_e branch1 [] in
      let (br2,_) = get_before_e branch2 [] in
      (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
  | Ast.While(header,body,aft) ->
      let (bd,_) = get_before_e body [] in
      (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
  | Ast.For(header,body,aft) ->
      let (bd,_) = get_before_e body [] in
      (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
  | Ast.Do(header,body,tail) ->
      let (bd,_) = get_before_e body [] in
      (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
  | Ast.Iterator(header,body,aft) ->
      let (bd,_) = get_before_e body [] in
      (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
  | Ast.Switch(header,lb,decls,cases,rb) ->
      let index = count_nested_braces s in
      let (de,dea) = get_before decls [Ast.WParen(lb,index)] in
      let cases =
	List.map
	  (function case_line ->
	    match Ast.unwrap case_line with
	      Ast.CaseLine(header,body) ->
		let (body,_) = get_before body [] in
		Ast.rewrap case_line (Ast.CaseLine(header,body))
	    | Ast.OptCase(case_line) -> failwith "not supported")
	  cases in
      (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),
       [Ast.WParen(rb,index)])
  | Ast.FunDecl(header,lbrace,body,rbrace) ->
      let (bd,_) = get_before body [] in
      (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[])
  | _ ->
      Pretty_print_cocci.statement "" s; Format.print_newline();
      failwith "get_before_e: not supported"

let rec get_after sl a =
  match Ast.unwrap sl with
    Ast.DOTS(x) ->
      let rec loop sl =
	match sl with
	  [] -> ([],a)
	| e::sl ->
	    let (sl,sla) = loop sl in
	    let (e,ea) = get_after_e e sla in
	    (e::sl,ea) in
      let (l,a) = loop x in
      (Ast.rewrap sl (Ast.DOTS(l)),a)
  | Ast.CIRCLES(x) -> failwith "not supported"
  | Ast.STARS(x) -> failwith "not supported"

and get_after_whencode a wc =
  List.map
    (function
	Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w
      | Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w
      |	Ast.WhenModifier(x) -> Ast.WhenModifier(x)
      | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
      | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
    wc

and get_after_e s a =
  match Ast.unwrap s with
    Ast.Dots(d,w,bef,_) ->
      (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)
  | Ast.Nest(starter,stmt_dots,ender,w,multi,bef,_) ->
      let w = get_after_whencode a w in
      let (sd,_) = get_after stmt_dots a in
      (*let a =
	 got rid of this. don't want to let nests overshoot
	List.filter
	  (function
	      Ast.Other a ->
		let unifies =
		  Unify_ast.unify_statement_dots
		    (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
		(match unifies with
		  Unify_ast.MAYBE -> false
		| _ -> true)
	    | Ast.Other_dots a ->
		let unifies = Unify_ast.unify_statement_dots a stmt_dots in
		(match unifies with
		  Unify_ast.MAYBE -> false
		| _ -> true)
	    | _ -> true)
	  a in*)
      (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,bef,a)),
       [Ast.Other_dots stmt_dots])
  | Ast.Disj(stmt_dots_list) ->
      let (dsl,dsla) =
	List.split (List.map (function e -> get_after e a) stmt_dots_list) in
      (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
  | Ast.Atomic(ast) ->
      (match Ast.unwrap ast with
	Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots _,i) ->
	  (* check "after" information for metavar optimization *)
	  (* if the error is not desired, could just return [], then
	     the optimization (check for EF) won't take place *)
	  List.iter
	    (function
		Ast.Other x ->
		  (match Ast.unwrap x with
		    Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) ->
		      failwith
			"dots/nest not allowed before and after stmt metavar"
		  | _ -> ())
	      |	Ast.Other_dots x ->
		  (match Ast.undots x with
		    x::_ ->
		      (match Ast.unwrap x with
			Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) ->
			  failwith
			    ("dots/nest not allowed before and after stmt "^
			     "metavar")
		      | _ -> ())
		  | _ -> ())
	      |	_ -> ())
	    a;
	  (Ast.rewrap s
	     (Ast.Atomic
		(Ast.rewrap s
		   (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
      |	Ast.MetaStmt(_,_,_,_) -> (s,[])
      |	_ -> (s,[Ast.Other s]))
  | Ast.Seq(lbrace,body,rbrace) ->
      let index = count_nested_braces s in
      let (bd,_) = get_after body [Ast.WParen(rbrace,index)] in
      (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),
       [Ast.WParen(lbrace,index)])
  | Ast.Define(header,body) ->
      let (body,_) = get_after body a in
      (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
  | Ast.AsStmt(stmt,asstmt) ->
      let (stmt,_) = get_after_e stmt [] in
      let (asstmt,_) = get_after_e asstmt [] in
      (Ast.rewrap s (Ast.AsStmt(stmt,asstmt)),[Ast.Other s])
  | Ast.IfThen(ifheader,branch,aft) ->
      let (br,_) = get_after_e branch a in
      (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s])
  | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
      let (br1,_) = get_after_e branch1 a in
      let (br2,_) = get_after_e branch2 a in
      (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
  | Ast.While(header,body,aft) ->
      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in
      (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
  | Ast.For(header,body,aft) ->
      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in
      (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
  | Ast.Do(header,body,tail) ->
      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in
      (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
  | Ast.Iterator(header,body,aft) ->
      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in
      (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
  | Ast.Switch(header,lb,decls,cases,rb) ->
      let index = count_nested_braces s in
      let cases =
	List.map
	  (function case_line ->
	    match Ast.unwrap case_line with
	      Ast.CaseLine(header,body) ->
		let (body,_) = get_after body [Ast.WParen(rb,index)] in
		Ast.rewrap case_line (Ast.CaseLine(header,body))
	    | Ast.OptCase(case_line) -> failwith "not supported")
	  cases in
      let (de,_) = get_after decls [] in
      (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),[Ast.WParen(lb,index)])
  | Ast.FunDecl(header,lbrace,body,rbrace) ->
      let (bd,_) = get_after body [] in
      (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[])
  | _ -> failwith "get_after_e: not supported"

let preprocess_dots sl =
  let (sl,_) = get_before sl [] in
  let (sl,_) = get_after sl [] in
  sl

let preprocess_dots_e sl =
  let (sl,_) = get_before_e sl [] in
  let (sl,_) = get_after_e sl [] in
  sl

(* --------------------------------------------------------------------- *)
(* various return_related things *)

let rec ends_in_return stmt_list =
  match Ast.unwrap stmt_list with
    Ast.DOTS(x) ->
      (match List.rev x with
	x::_ ->
	  (match Ast.unwrap x with
	    Ast.Atomic(x) ->
	      let rec loop x =
		match Ast.unwrap x with
		  Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true
		| Ast.DisjRuleElem((_::_) as l) -> List.for_all loop l
		| _ -> false in
	      loop x
	  | Ast.Disj(disjs) -> List.for_all ends_in_return disjs
	  | _ -> false)
      |	_ -> false)
  | Ast.CIRCLES(x) -> failwith "not supported"
  | Ast.STARS(x) -> failwith "not supported"

(* --------------------------------------------------------------------- *)
(* expressions *)

let exptymatch l make_match make_guard_match =
  let pos = fresh_pos() in
  let matches_guard_matches =
    List.map
      (function x ->
	let pos = Ast.make_mcode pos in
	(make_match (Ast.set_pos x (Some pos)),
	 make_guard_match (Ast.set_pos x (Some pos))))
      l in
  let (matches,guard_matches) = List.split matches_guard_matches in
  let rec suffixes = function
      [] -> []
    | x::xs -> xs::(suffixes xs) in
  let prefixes =
    (* normally, we check that an expression does not match something
       earlier in the disjunction (calculated as prefixes).  But for large
       disjunctions, this can result in a very big CTL formula.  So we
       give the user the option to say he doesn't want this feature, if that is
       the case. *)
    if !Flag_matcher.no_safe_expressions
    then List.map (function _ -> []) matches
    else List.rev (suffixes (List.rev guard_matches)) in
  let info = (* not null *)
    List.map2
      (function matcher ->
	function negates ->
	  CTL.Exists
	    (false,pos,
	     ctl_and CTL.NONSTRICT matcher
	       (ctl_not
		  (ctl_uncheck (List.fold_left ctl_or_fl CTL.False negates)))))
      matches prefixes in
  CTL.InnerAnd(List.fold_left ctl_or_fl CTL.False (List.rev info))

(* code might be a DisjRuleElem, in which case we break it apart
   code might contain an Exp or Ty
   this one pushes the quantifier inwards *)
let do_re_matches label guard res quantified minus_quantified =
  let make_guard_match x =
    let stmt_fvs = Ast.get_mfvs x in
    let fvs = get_unquantified minus_quantified stmt_fvs in
    non_saved_quantify fvs (make_match None true x) in
  let make_match x =
    let stmt_fvs = Ast.get_fvs x in
    let fvs = get_unquantified quantified stmt_fvs in
    quantify guard fvs (make_match None guard x) in
(* label used to be used here, but it is not use; label is only needed after
and within dots
    ctl_and CTL.NONSTRICT (label_pred_maker label) *)
    (match List.map Ast.unwrap res with
      [] -> failwith "unexpected empty disj"
    | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match
    | Ast.Ty(t)::rest  -> exptymatch res make_match make_guard_match
    | all ->
	if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
	    all
	then failwith "unexpected exp or ty";
	List.fold_left ctl_seqor CTL.False (List.map make_match res))

(* code might be a DisjRuleElem, in which case we break it apart
   code doesn't contain an Exp or Ty
   this one is for use when it is not practical to push the quantifier inwards
 *)
let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl =
  match Ast.unwrap code with
    Ast.DisjRuleElem(res) ->
      let make_match = make_match None guard in
      let orop = if guard then ctl_or else ctl_seqor in
(* label used to be used here, but it is not use; label is only needed after
and within dots
      ctl_and CTL.NONSTRICT (label_pred_maker label) *)
      (List.fold_left orop CTL.False (List.map make_match res))
  | _ -> make_match label guard code

(* --------------------------------------------------------------------- *)
(* control structures *)

let end_control_structure fvs header body after_pred
    after_checks no_after_checks (afvs,afresh,ainh,aft) after label guard =
  (* aft indicates what is added after the whole if, which has to be added
     to the endif node *)
  let (aft_needed,after_branch) =
    match aft with
      Ast.CONTEXT(_,Ast.NOTHING) ->
	(false,make_seq_after2 guard after_pred after)
    | _ ->
	let match_endif =
	  make_match label guard
	    (make_meta_rule_elem aft (afvs,afresh,ainh)) in
	(true,
	 make_seq_after guard after_pred
	   (After(make_seq_after guard match_endif after))) in
  let body = body after_branch in
  let s = guard_to_strict guard in
  (* the code *)
  quantify guard fvs
    (ctl_and s header
       (opt_and guard
	  (match (after,aft_needed) with
	    (After _,_) (* pattern doesn't end here *)
	  | (_,true) (* + code added after *) -> after_checks
	  | _ -> no_after_checks)
	  (ctl_ax_absolute s body)))

let ifthen ifheader branch ((afvs,_,_,_) as aft) after
    quantified minus_quantified label llabel slabel recurse make_match guard =
(* "if (test) thn" becomes:
    if(test) & AX((TrueBranch & AX thn) v FallThrough v After)

    "if (test) thn; after" becomes:
    if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
             & EX After
*)
  (* free variables *)
  let (efvs,bfvs) =
    match seq_fvs quantified
	[Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with
      [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
    | _ -> failwith "not possible" in
  let new_quantified = Common.union_set bfvs quantified in
  let (mefvs,mbfvs) =
    match seq_fvs minus_quantified
	[Ast.get_mfvs ifheader;Ast.get_mfvs branch;[]] with
      [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
    | _ -> failwith "not possible" in
  let new_mquantified = Common.union_set mbfvs minus_quantified in
  (* if header *)
  let if_header = quantify guard efvs (make_match ifheader) in
  (* then branch and after *)
  let lv = get_label_ctr() in
  let used = ref false in
  let true_branch =
    (* no point to put a label on truepred etc; it is local to this construct
       so it must have the same label *)
    make_seq guard
      [truepred None; recurse branch NotTop Tail new_quantified new_mquantified
	  (Some (lv,used)) llabel slabel guard] in
  let after_pred = aftpred None in
  let or_cases after_branch =
    ctl_or true_branch (ctl_or (fallpred None) after_branch) in
  let (if_header,wrapper) =
    if !used
    then
      let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
      (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
       (function body -> quantify true [lv] body))
    else (if_header,function x -> x) in
  wrapper
    (end_control_structure bfvs if_header or_cases after_pred
	(Some(ctl_ex after_pred)) None aft after label guard)

let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
    quantified minus_quantified label llabel slabel recurse make_match guard =
(*  "if (test) thn else els" becomes:
    if(test) & AX((TrueBranch & AX thn) v
                  (FalseBranch & AX (else & AX els)) v After)
             & EX FalseBranch

    "if (test) thn else els; after" becomes:
    if(test) & AX((TrueBranch & AX thn) v
                  (FalseBranch & AX (else & AX els)) v
                  (After & AXAX after))
             & EX FalseBranch
             & EX After
*)
  (* free variables *)
  let (e1fvs,b1fvs,s1fvs) =
    match seq_fvs quantified
	[Ast.get_fvs ifheader;Ast.get_fvs branch1;afvs] with
      [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
	(e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
    | _ -> failwith "not possible" in
  let (e2fvs,b2fvs,s2fvs) =
    (* fvs on else? *)
    (* just combine with the else branch.  no point to have separate
       quantifier, since there is only one possible control-flow path *)
    let else_fvs = Common.union_set (Ast.get_fvs els) (Ast.get_fvs branch2) in
    match seq_fvs quantified [Ast.get_fvs ifheader;else_fvs;afvs] with
      [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
        (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
    | _ -> failwith "not possible" in
  let bothfvs        = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
  let exponlyfvs     = intersect e1fvs e2fvs in
  let new_quantified = union bothfvs quantified in
  (* minus free variables *)
  let (me1fvs,mb1fvs,ms1fvs) =
    match seq_fvs minus_quantified
	[Ast.get_mfvs ifheader;Ast.get_mfvs branch1;[]] with
      [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
	(e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
    | _ -> failwith "not possible" in
  let (me2fvs,mb2fvs,ms2fvs) =
    (* fvs on else? *)
    (* just combine with the else branch.  no point to have separate
       quantifier, since there is only one possible control-flow path *)
    let else_mfvs =
      Common.union_set (Ast.get_mfvs els) (Ast.get_mfvs branch2) in
    match seq_fvs minus_quantified [Ast.get_mfvs ifheader;else_mfvs;[]] with
      [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
	(e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
    | _ -> failwith "not possible" in
  let mbothfvs       = union (union mb1fvs mb2fvs) (intersect ms1fvs ms2fvs) in
  let new_mquantified = union mbothfvs minus_quantified in
  (* if header *)
  let if_header = quantify guard exponlyfvs (make_match ifheader) in
  (* then and else branches *)
  let lv = get_label_ctr() in
  let used = ref false in
  let true_branch =
    make_seq guard
      [truepred None; recurse branch1 NotTop Tail new_quantified new_mquantified
	  (Some (lv,used)) llabel slabel guard] in
  let false_branch =
    make_seq guard
      [falsepred None;
	quantify guard
	  (Common.minus_set (Ast.get_fvs els) new_quantified)
	  (header_match None guard els);
	recurse branch2 NotTop Tail new_quantified new_mquantified
	  (Some (lv,used)) llabel slabel guard] in
  let after_pred = aftpred None in
  let or_cases after_branch =
    ctl_or true_branch (ctl_or false_branch after_branch) in
  let s = guard_to_strict guard in
  let (if_header,wrapper) =
    if !used
    then
      let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
      (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
       (function body -> quantify true [lv] body))
    else (if_header,function x -> x) in
  wrapper
    (end_control_structure bothfvs if_header or_cases after_pred
      (Some(ctl_and s (ctl_ex (falsepred None)) (ctl_ex after_pred)))
      (Some(ctl_ex (falsepred None)))
      aft after label guard)

let forwhile header body ((afvs,_,_,_) as aft) after
    quantified minus_quantified label recurse make_match guard =
  let process _ =
    (* the translation in this case is similar to that of an if with no else *)
    (* free variables *)
    let (efvs,bfvs) =
      match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
	[(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
      | _ -> failwith "not possible" in
    let new_quantified = Common.union_set bfvs quantified in
    (* minus free variables *)
    let (mefvs,mbfvs) =
      match seq_fvs minus_quantified
	  [Ast.get_mfvs header;Ast.get_mfvs body;[]] with
	[(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
      | _ -> failwith "not possible" in
    let new_mquantified = Common.union_set mbfvs minus_quantified in
    (* loop header *)
    let header = quantify guard efvs (make_match header) in
    let lv = get_label_ctr() in
    let used = ref false in
    let body =
      make_seq guard
	[inlooppred None;
	  recurse body NotTop Tail new_quantified new_mquantified
	    (Some (lv,used)) (Some (lv,used)) None guard] in
    let after_pred = loopfallpred None in
    let or_cases after_branch = ctl_or body after_branch in
    let (header,wrapper) =
      if !used
      then
	let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
	(ctl_and CTL.NONSTRICT(*???*) header label_pred,
	 (function body -> quantify true [lv] body))
      else (header,function x -> x) in
    wrapper
      (end_control_structure bfvs header or_cases after_pred
	 (Some(ctl_ex after_pred)) None aft after label guard) in
  match (Ast.unwrap body,aft) with
    (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
      (match Ast.unwrap re with
	Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),
		     Type_cocci.Unitary,_,false)
	when after = Tail or after = End or after = VeryEnd ->
	  let (efvs) =
	    match seq_fvs quantified [Ast.get_fvs header] with
	      [(efvs,_)] -> efvs
	    | _ -> failwith "not possible" in
	  quantify guard efvs (make_match header)
      | _ -> process())
  | _ -> process()

(* --------------------------------------------------------------------- *)
(* statement metavariables *)

(* issue: an S metavariable that is not an if branch/loop body
   should not match an if branch/loop body, so check that the labels
   of the nodes before the first node matched by the S are different
   from the label of the first node matched by the S *)
let sequencibility body label_pred process_bef_aft = function
    Ast.Sequencible | Ast.SequencibleAfterDots [] ->
      body
	(function x ->
	  (ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
  | Ast.SequencibleAfterDots l ->
      (* S appears after some dots.  l is the code that comes after the S.
	 want to search for that first, because S can match anything, while
	 the stuff after is probably more restricted *)
      let afts = List.map process_bef_aft l in
      let ors = foldl1 ctl_or afts in
      ctl_and CTL.NONSTRICT
	(ctl_ef (ctl_and CTL.NONSTRICT ors (ctl_back_ax label_pred)))
	(body
	   (function x ->
	     ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
  | Ast.NotSequencible -> body (function x -> x)

let svar_context_with_add_after stmt s label quantified d ast
    seqible after process_bef_aft guard fvinfo =
  let label_var = (*fresh_label_var*) string2var "_lab" in
  let label_pred =
    CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
  (*let prelabel_pred =
    CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
  let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
  let full_metamatch = matcher d in
  let first_metamatch =
    matcher
      (match d with
	Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_,c)) ->
	  Ast.CONTEXT(pos,Ast.BEFORE(bef,c))
      |	Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
      | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
(*
  let middle_metamatch =
    matcher
      (match d with
	Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
      | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
*)
  let last_metamatch =
    matcher
      (match d with
	Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft,c)) ->
	  Ast.CONTEXT(pos,Ast.AFTER(aft,c))
      |	Ast.CONTEXT(_,_) -> d
      | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in

(*
  let rest_nodes =
    ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
*)

  let to_end = ctl_or (aftpred None) (loopfallpred None) in
  let left_or = (* the whole statement is one node *)
    make_seq_after guard
      (ctl_and CTL.NONSTRICT (ctl_not (ctl_ex to_end)) full_metamatch) after in
  let right_or = (* the statement covers multiple nodes *)
    ctl_and CTL.NONSTRICT
      (ctl_ex
	 (make_seq guard
	    [to_end; make_seq_after guard last_metamatch after]))
      first_metamatch in

(*
  let left_or =
    make_seq guard
      [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
  let right_or =
    make_seq guard
      [first_metamatch;
        ctl_au CTL.NONSTRICT
	  rest_nodes
	  (make_seq guard
	     [ctl_and CTL.NONSTRICT last_metamatch label_pred;
	       and_after guard
		 (ctl_not prelabel_pred) after])] in
*)

  let body f =
    ctl_and CTL.NONSTRICT label_pred
       (f (ctl_and CTL.NONSTRICT
	    (make_raw_match label false ast) (ctl_or left_or right_or))) in
  let stmt_fvs = Ast.get_fvs stmt in
  let fvs = get_unquantified quantified stmt_fvs in
  quantify guard (label_var::fvs)
    (sequencibility body label_pred process_bef_aft seqible)

let svar_minus_or_no_add_after stmt s label quantified d ast
    seqible after process_bef_aft guard fvinfo =
  let label_var = (*fresh_label_var*) string2var "_lab" in
  let label_pred =
    CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
  let prelabel_pred =
    CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
  let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
  let ender =
    match (d,after) with
      (Ast.PLUS _, _) -> failwith "not possible"
    | (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) ->
	(* just match the root. don't care about label; always ok *)
	make_raw_match None false ast
    | (Ast.CONTEXT(pos,Ast.BEFORE(_,_)),(Tail|End|VeryEnd)) ->
	ctl_and CTL.NONSTRICT
	  (make_raw_match None false ast) (* statement *)
	  (matcher d)                     (* transformation *)
    | (Ast.CONTEXT(pos,(Ast.NOTHING|Ast.BEFORE(_,_))),(After a | Guard a)) ->
	(* This case and the MINUS one couldprobably be merged, if
	   HackForStmt were to notice when its arguments are trivial *)
	let first_metamatch = matcher d in
	(* try to follow after link *)
	let to_end = ctl_or (aftpred None) (loopfallpred None) in
	let is_compound =
	  ctl_ex(make_seq guard [to_end; CTL.True; a]) in
	let not_compound =
	  make_seq_after guard (ctl_not (ctl_ex to_end)) after in
	ctl_and CTL.NONSTRICT (make_raw_match label false ast)
	  (ctl_and CTL.NONSTRICT
	     first_metamatch (ctl_or is_compound not_compound))
    | (Ast.CONTEXT(pos,(Ast.AFTER _|Ast.BEFOREAFTER _)),_) ->
	failwith "not possible"
    | (Ast.MINUS(pos,inst,adj,l),after) ->
	let (first_metamatch,last_metamatch,rest_metamatch) =
	  match l with
	    Ast.NOREPLACEMENT ->
	      (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d)
	  | _ -> (matcher d,
		  matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)),
		  ctl_and CTL.NONSTRICT
		    (ctl_not (make_raw_match label false ast))
		    (matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)))) in
	(* try to follow after link *)
	let to_end = ctl_or (aftpred None) (loopfallpred None) in
	let is_compound =
	  ctl_ex
	    (make_seq guard
	       [to_end; make_seq_after guard last_metamatch after]) in
	let not_compound =
	  make_seq_after guard (ctl_not (ctl_ex to_end)) after in
	ctl_and CTL.NONSTRICT
	  (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
	     (ctl_and CTL.NONSTRICT
		first_metamatch (ctl_or is_compound not_compound)))
          (* don't have to put anything before the beginning, so don't have to
          distinguish the first node.  so don't have to bother about paths,
          just use the label. label ensures that found nodes match up with
          what they should because it is in the lhs of the andany. *)
	  (CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
			   ctl_and CTL.NONSTRICT label_pred
			     (make_raw_match label false ast),
			   ctl_and CTL.NONSTRICT prelabel_pred rest_metamatch))
  in
  let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
  let stmt_fvs = Ast.get_fvs stmt in
  let fvs = get_unquantified quantified stmt_fvs in
  quantify guard (label_var::fvs)
    (sequencibility body label_pred process_bef_aft seqible)

(* --------------------------------------------------------------------- *)
(* dots and nests *)

let dots_au is_strict toend label s wrapcode n x seq_after y quantifier =
  let matchgoto = gotopred None in
  let matchbreak =
    make_match None false
      (wrapcode
	 (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in
  let matchcontinue =
     make_match None false
      (wrapcode
	 (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in
  let stop_early =
    if quantifier = Exists
    then Common.Left(CTL.False)
    else if toend
    then Common.Left(CTL.Or(aftpred label,exitpred label))
    else if is_strict
    then Common.Left(aftpred label)
    else
      Common.Right
	(function vx -> function v ->
	  (* vx is the contents of the nest, if any.  we can only stop early
	     if we find neither the ending code nor the nest contents in
	     the if branch.  not sure if this is a good idea. *)
	  let lv = get_label_ctr() in
	  let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
	  let preflabelpred = label_pred_maker (Some (lv,ref true)) in
	  (*let is_paren =
	    (* Rather a special case.  But if the code afterwards is just
	       a } then there is no point checking after a goto that it does
	       not appear. *)
	    (* this optimization doesn't work.  probably depends on whether
	       the destination of the break/goto is local or more global than
	       the dots *)
	    match seq_after with
	      CTL.And(_,e1,e2) ->
		let is_paren = function
		    CTL.Pred(Lib_engine.Paren _,_) -> true
		  | _ -> false in
		is_paren e1 or is_paren e2
	    | _ -> false in *)
	  ctl_or (aftpred label)
	    (quantify false [lv]
	       (ctl_and CTL.NONSTRICT
		  (ctl_and CTL.NONSTRICT (truepred label) labelpred)
		  (ctl_au CTL.NONSTRICT
		     (ctl_and CTL.NONSTRICT (ctl_not v)
			(ctl_and CTL.NONSTRICT vx preflabelpred))
		     (ctl_and CTL.NONSTRICT preflabelpred
			(if !Flag_matcher.only_return_is_error_exit
			then
			  (ctl_and CTL.NONSTRICT
			     (retpred None) (ctl_not seq_after))
			else
			  (ctl_or
			     (ctl_and CTL.NONSTRICT
				(ctl_or (retpred None) matchcontinue)
				(ctl_not seq_after))
			     (ctl_and CTL.NONSTRICT
				(ctl_or matchgoto matchbreak)
				((*if is_paren
                                (* an optim that failed see defn is_paren
                                   and tests/makes_a_loop *)
				then CTL.True
				else*)
				  (ctl_ag s
				     (ctl_not seq_after))))))))))) in
  let op = if quantifier = !exists then ctl_au else ctl_anti_au in
  let v = get_let_ctr() in
  op s x
    (match stop_early with
      Common.Left x1 -> ctl_or y x1
    | Common.Right stop_early ->
	CTL.Let(v,y,
		ctl_or (CTL.Ref v)
		  (ctl_and CTL.NONSTRICT (label_pred_maker label)
		     (stop_early n (CTL.Ref v)))))

let rec dots_and_nests plus nest whencodes bef aft dotcode after label
    process_bef_aft statement_list statement guard quantified wrapcode =
  let ctl_and_ns = ctl_and CTL.NONSTRICT in
  (* proces bef_aft *)
  let shortest l =
    List.fold_left ctl_or_fl CTL.False (List.map process_bef_aft l) in
  let bef_aft = (* to be negated *)
    try
      let _ =
	List.find
	  (function Ast.WhenModifier(Ast.WhenAny) -> true | _ -> false)
	  whencodes in
      CTL.False
    with Not_found -> shortest (Common.union_set bef aft) in
  let is_strict =
    List.exists
      (function Ast.WhenModifier(Ast.WhenStrict) -> true | _ -> false)
      whencodes in
  let check_quantifier quant other =
    if List.exists
	(function Ast.WhenModifier(x) -> x = quant | _ -> false)
	whencodes
    then
      if List.exists
	  (function Ast.WhenModifier(x) -> x = other | _ -> false)
	  whencodes
      then failwith "inconsistent annotation on dots"
      else true
    else false in
  let quantifier =
    if check_quantifier Ast.WhenExists Ast.WhenForall
    then Exists
    else
      if check_quantifier Ast.WhenForall Ast.WhenExists
      then Forall
      else !exists in
  (* the following is used when we find a goto, etc and consider accepting
     without finding the rest of the pattern *)
  let aft = shortest aft in
  (* process whencode *)
  let labelled = label_pred_maker label in
  let whencodes arg =
    let (poswhen,negwhen) =
      List.fold_left
	(function (poswhen,negwhen) ->
	  function
	      Ast.WhenNot whencodes ->
		(poswhen,ctl_or (statement_list whencodes) negwhen)
	    | Ast.WhenAlways stm ->
		(ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen)
	    | Ast.WhenModifier(_) -> (poswhen,negwhen)
	    | Ast.WhenNotTrue(e) ->
		(poswhen,
		  ctl_or (whencond_true e label guard quantified) negwhen)
	    | Ast.WhenNotFalse(e) ->
		(poswhen,
		  ctl_or (whencond_false e label guard quantified) negwhen))
	(CTL.True,CTL.False(*bef_aft*)) (List.rev whencodes) in
    (*bef_aft modifies arg so that inside of a nest can't cause the next
       to overshoot its boundaries, eg a() <...f()...> b() where f is
       a metavariable and the whole thing matches code in a loop;
       don't want f to match eg b(), allowing to go around the loop again*)
    let poswhen = ctl_and_ns arg poswhen in
    let negwhen =
(*    if !exists
      then*)
        (* add in After, because it's not part of the program *)
	ctl_or (aftpred label) negwhen
      (*else negwhen*) in
    ctl_and_ns poswhen (ctl_not negwhen) in
  (* process dot code, if any *)
  let dotcode =
    match (dotcode,guard) with
      (None,_) | (_,true) -> CTL.True
    | (Some dotcode,_) -> dotcode in
  (* process nest code, if any *)
  (* whencode goes in the negated part of the nest; if no nest, just goes
      on the "true" in between code *)
  let plus_var = if plus then get_label_ctr() else string2var "" in
  let plus_var2 = if plus then get_label_ctr() else string2var "" in
  let (ornest,just_nest) =
    (* just_nest is used when considering whether to stop early, to continue
       to collect nest information in the if branch *)
    match (nest,guard && not plus) with
      (None,_) | (_,true) -> (whencodes CTL.True,CTL.True)
    | (Some nest,false) ->
	let v = get_let_ctr() in
	let is_plus x =
	  if plus
	  then
	    (* the idea is that BindGood is sort of a witness; a witness to
	       having found the subterm in at least one place.  If there is
	       not a witness, then there is a risk that it will get thrown
	       away, if it is merged with a node that has an empty
	       environment.  See tests/nestplus.  But this all seems
	       rather suspicious *)
	    CTL.And(CTL.NONSTRICT,x,
		    CTL.Exists(true,plus_var2,
			       CTL.Pred(Lib_engine.BindGood(plus_var),
					CTL.Modif plus_var2)))
	  else x in
	let body =
	  CTL.Let(v,nest,
		  CTL.Or(is_plus (CTL.Ref v),
			 whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
        (body,body) in
  let plus_modifier x =
    if plus
    then
      CTL.Exists
	(false,plus_var,
	 (CTL.And
	    (CTL.NONSTRICT,x,
	     CTL.Not(CTL.Pred(Lib_engine.BindBad(plus_var),CTL.Control)))))
    else x in

  let ender =
    match after with
      (* label within dots is taken care of elsewhere.  the next two lines
         put the label on the code following dots *)
      After f -> ctl_and (guard_to_strict guard) f labelled
    | Guard f ->
	(* actually, label should be None based on the only use of Guard... *)
	assert (label = None);
	ctl_and CTL.NONSTRICT (ctl_uncheck f) labelled
    | VeryEnd ->
	let exit = endpred label in
	let errorexit = exitpred label in
	ctl_or exit errorexit
    (* not at all sure what the next two mean... *)
    | End -> CTL.True
    | Tail ->
	(match label with
	  Some (lv,used) -> used := true;
	    ctl_or (CTL.Pred(Lib_engine.Label lv,CTL.Control))
	      (ctl_back_ex (ctl_or (retpred label) (gotopred label)))
	| None -> endpred label)
	  (* was the following, but not clear why sgrep should allow
	     incomplete patterns
	let exit = endpred label in
	let errorexit = exitpred label in
	if !exists
	then ctl_or exit errorexit (* end anywhere *)
	else exit (* end at the real end of the function *) *) in
  plus_modifier
    (dots_au is_strict ((after = Tail) or (after = VeryEnd))
       label (guard_to_strict guard) wrapcode just_nest
       (ctl_and_ns dotcode
	   (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest) labelled))
       aft ender quantifier)

and get_whencond_exps e =
  match Ast.unwrap e with
    Ast.Exp e -> [e]
  | Ast.DisjRuleElem(res) ->
      List.fold_left Common.union_set [] (List.map get_whencond_exps res)
  | _ -> failwith "not possible"

and make_whencond_headers e e1 label guard quantified =
  let fvs = Ast.get_fvs e in
  let header_pred h =
    quantify guard (get_unquantified quantified fvs)
      (make_match label guard h) in
  let if_header e1 =
    header_pred
      (Ast.rewrap e
	 (Ast.IfHeader
	    (Ast.make_mcode "if",
	     Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
  let while_header e1 =
    header_pred
      (Ast.rewrap e
	 (Ast.WhileHeader
	    (Ast.make_mcode "while",
	     Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
  let for_header e1 =
    header_pred
      (Ast.rewrap e
	 (Ast.ForHeader
	    (Ast.make_mcode "for",Ast.make_mcode "(",None,Ast.make_mcode ";",
	     Some e1,Ast.make_mcode ";",None,Ast.make_mcode ")"))) in
  let if_headers =
    List.fold_left ctl_or CTL.False (List.map if_header e1) in
  let while_headers =
    List.fold_left ctl_or CTL.False (List.map while_header e1) in
  let for_headers =
    List.fold_left ctl_or CTL.False (List.map for_header e1) in
  (if_headers, while_headers, for_headers)

and whencond_true e label guard quantified =
  let e1 = get_whencond_exps e in
  let (if_headers, while_headers, for_headers) =
    make_whencond_headers e e1 label guard quantified in
  ctl_or
    (ctl_and CTL.NONSTRICT (truepred label) (ctl_back_ex if_headers))
    (ctl_and CTL.NONSTRICT
       (inlooppred label) (ctl_back_ex (ctl_or while_headers for_headers)))

and whencond_false e label guard quantified =
  let e1 = get_whencond_exps e in
  let (if_headers, while_headers, for_headers) =
    make_whencond_headers e e1 label guard quantified in
  (* if with else *)
  ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
    (* if without else *)
    (ctl_or (ctl_and CTL.NONSTRICT (fallpred label) (ctl_back_ex if_headers))
       (* failure of loop test *)
       (ctl_and CTL.NONSTRICT (loopfallpred label)
	  (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))

(* --------------------------------------------------------------------- *)
(* the main translation loop *)

let rec statement_list stmt_list top after quantified minus_quantified
    label llabel slabel dots_before guard =
  let isdots x =
    (* include Disj to be on the safe side *)
    match Ast.unwrap x with
      Ast.Dots _ | Ast.Nest _ | Ast.Disj _ -> true | _ -> false in
  let compute_label l e db = if db or isdots e then l else None in
  match Ast.unwrap stmt_list with
    Ast.DOTS(x) ->
      let rec loop top quantified minus_quantified dots_before
	  label llabel slabel
	  = function
	  ([],_,_) -> (match after with After f -> f | _ -> CTL.True)
	| ([e],_,_) ->
	    statement e top after quantified minus_quantified
	      (compute_label label e dots_before)
	      llabel slabel guard
	| (e::sl,fv::fvs,mfv::mfvs) ->
	    let shared = intersectll fv fvs in
	    let unqshared = get_unquantified quantified shared in
	    let new_quantified = Common.union_set unqshared quantified in
	    let minus_shared = intersectll mfv mfvs in
	    let munqshared =
	      get_unquantified minus_quantified minus_shared in
	    let new_mquantified =
	      Common.union_set munqshared minus_quantified in
	    quantify guard unqshared
	      (statement e top
		 (After
		    (let (label1,llabel1,slabel1) =
		      match Ast.unwrap e with
			Ast.Atomic(re) ->
			  (match Ast.unwrap re with
			    Ast.Goto _ -> (None,None,None)
			  | _ -> (label,llabel,slabel))
		      |	_ -> (label,llabel,slabel) in
		    loop NotTop new_quantified new_mquantified (isdots e)
		      label1 llabel1 slabel1
		      (sl,fvs,mfvs)))
		 new_quantified new_mquantified
		 (compute_label label e dots_before) llabel slabel guard)
	| _ -> failwith "not possible" in
      loop top quantified minus_quantified dots_before
	label llabel slabel
	(x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x)
  | Ast.CIRCLES(x) -> failwith "not supported"
  | Ast.STARS(x) -> failwith "not supported"

(* llabel is the label of the enclosing loop and slabel is the label of the
   enclosing switch *)
and statement stmt top after quantified minus_quantified
    label llabel slabel guard =
  let ctl_au     = ctl_au CTL.NONSTRICT in
  let ctl_ax     = ctl_ax CTL.NONSTRICT in
  let ctl_and    = ctl_and CTL.NONSTRICT in
  let make_seq   = make_seq guard in
  let make_seq_after = make_seq_after guard in
  let real_make_match = make_match in
  let make_match = header_match label guard in

  let dots_done = ref false in (* hack for dots cases we can easily handle *)

  let term =
  match Ast.unwrap stmt with
    Ast.Atomic(ast) ->
      (match Ast.unwrap ast with
	(* the following optimisation is not a good idea, because when S
	   is alone, we would like it not to match a declaration.
	   this makes more matching for things like when (...) S, but perhaps
	   that matching is not so costly anyway *)
	(*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
      |	Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_,_)) as d),_),
		     keep,seqible,_)
      | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_,_)) as d),_),
		     keep,seqible,_)->
	  svar_context_with_add_after stmt s label quantified d ast seqible
	    after
	    (process_bef_aft quantified minus_quantified
	       label llabel slabel true)
	    guard
	    (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)

      |	Ast.MetaStmt((s,_,d,_),keep,seqible,_) ->
	  svar_minus_or_no_add_after stmt s label quantified d ast seqible
	    after
	    (process_bef_aft quantified minus_quantified
	       label llabel slabel true)
	    guard
	    (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)

      |	_ ->
	  let term =
	    match Ast.unwrap ast with
	      Ast.DisjRuleElem(res) ->
		do_re_matches label guard res quantified minus_quantified
	    | Ast.Exp(_) | Ast.Ty(_) ->
		let stmt_fvs = Ast.get_fvs stmt in
		let fvs = get_unquantified quantified stmt_fvs in
		CTL.InnerAnd(quantify guard fvs (make_match ast))
	    | _ ->
		let stmt_fvs = Ast.get_fvs stmt in
		let fvs = get_unquantified quantified stmt_fvs in
		quantify guard fvs (make_match ast) in
	  match Ast.unwrap ast with
	    Ast.Break(brk,semi) ->
	      (match (llabel,slabel) with
		(_,Some(lv,used)) -> (* use switch label if there is one *)
		  ctl_and term (bclabel_pred_maker slabel)
	      | _ -> ctl_and term (bclabel_pred_maker llabel))
	  | Ast.Continue(brk,semi) -> ctl_and term (bclabel_pred_maker llabel)
          | Ast.Return((_,info,retmc,pos),(_,_,semmc,_)) ->
	      (* discard pattern that comes after return *)
	      let normal_res = make_seq_after term after in
	      (* the following code tries to propagate the modifications on
		 return; to a close brace, in the case where the final return
		 is absent *)
	      let new_mc =
		match (retmc,semmc) with
		  (Ast.MINUS(_,inst1,adj1,l1),Ast.MINUS(_,_,_,l2))
		  when !Flag.sgrep_mode2 ->
		    (* in sgrep mode, we can propagate the - *)
		    let new_info =
		      match (l1,l2) with
			(Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) ->
			  Ast.NOREPLACEMENT
		      |	_ ->
			  failwith "no replacements allowed in sgrep mode" in
		    Some (Ast.MINUS(Ast.NoPos,inst1,adj1,new_info))
		| (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) ->
		    let change =
		      match (l1,l2) with
			(Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) ->
			  Ast.NOTHING
		      |	(Ast.NOREPLACEMENT,Ast.REPLACEMENT(l,ct))
		      |	(Ast.REPLACEMENT(l,ct),Ast.NOREPLACEMENT) ->
			  Ast.BEFORE(l,ct)
		      |	(Ast.REPLACEMENT(l1,ct1),Ast.REPLACEMENT(l2,ct2)) ->
			  Ast.BEFORE(l1@l2,Ast.lub_count ct1 ct2) in
		    Some (Ast.CONTEXT(Ast.NoPos,change))
		| (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)),
		   Ast.CONTEXT(_,Ast.AFTER(l2,c2))) ->
		     Some
		       (Ast.CONTEXT(Ast.NoPos,
				    Ast.BEFORE(l1@l2,Ast.lub_count c1 c2)))
		| (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
		| (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
		    Some retmc
		| (Ast.CONTEXT(_,Ast.NOTHING),
		   Ast.CONTEXT(_,Ast.AFTER(l,c))) ->
		    Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l,c)))
		| _ -> None in
	      let ret = Ast.make_mcode "return" in
	      let edots =
		Ast.rewrap ast (Ast.Edots(Ast.make_mcode "...",None)) in
	      let semi = Ast.make_mcode ";" in
	      let simple_return =
		make_match(Ast.rewrap ast (Ast.Return(ret,semi))) in
	      let return_expr =
		make_match(Ast.rewrap ast (Ast.ReturnExpr(ret,edots,semi))) in
	      (match new_mc with
		Some new_mc ->
		  let exit = endpred None in
		  let mod_rbrace =
		    Ast.rewrap ast (Ast.SeqEnd (("}",info,new_mc,pos))) in
		  let stripped_rbrace =
		    Ast.rewrap ast (Ast.SeqEnd(Ast.make_mcode "}")) in
		  ctl_or normal_res
		    (ctl_and (make_match mod_rbrace)
		       (ctl_and
			  (ctl_au
			     (make_match stripped_rbrace)
			     (* error exit not possible; it is in the middle
				of code, so a return is needed *)
			     exit)
			  (* worry about perf, but seems correct, not ax *)
			  (ctl_back_ag
			     (ctl_not
				(ctl_uncheck
				   (ctl_or simple_return return_expr))))))
	      |	_ ->
		  (* some change in the middle of the return, so have to
		     find an actual return *)
		  normal_res)
          | _ ->
	      (* should try to deal with the dots_bef_aft problem elsewhere,
		 but don't have the courage... *)
	      let term =
		if guard
		then term
		else
		  do_between_dots stmt term End
		    quantified minus_quantified label llabel slabel guard in
	      dots_done := true;
	      make_seq_after term after)
  | Ast.Seq(lbrace,body,rbrace) ->
      let (lbfvs,b1fvs,b2fvs,rbfvs) =
	match
	  seq_fvs quantified
	    [Ast.get_fvs lbrace;Ast.get_fvs body;Ast.get_fvs rbrace]
	with
	  [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> (lbfvs,b1fvs,b2fvs,rbfvs)
	| _ -> failwith "not possible" in
      let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) =
	match
	  seq_fvs minus_quantified
	    [Ast.get_mfvs lbrace;Ast.get_mfvs body;Ast.get_mfvs rbrace]
	with
	  [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
	    (lbfvs,b1fvs,b2fvs,rbfvs)
	| _ -> failwith "not possible" in
      let pv = count_nested_braces stmt in
      let lv = get_label_ctr() in
      let paren_pred = CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
      let label_pred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
      let start_brace =
	ctl_and
	  (quantify guard lbfvs (make_match lbrace))
	  (ctl_and paren_pred label_pred) in
      let empty_rbrace =
	match Ast.unwrap rbrace with
	  Ast.SeqEnd((data,info,_,pos)) ->
	    Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data))
	| _ -> failwith "unexpected close brace" in
      let end_brace =
	(* label is not needed; paren_pred is enough *)
	quantify guard rbfvs
	  (ctl_au (make_match empty_rbrace)
	     (ctl_and (real_make_match None guard rbrace) paren_pred)) in
      let new_quantified2 =
	Common.union_set b1fvs (Common.union_set b2fvs quantified) in
      let new_mquantified2 =
	Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in
      let pattern_as_given =
	let new_quantified2 = Common.union_set [pv] new_quantified2 in
	quantify true [pv;lv]
	  (quantify guard b1fvs
	     (make_seq
		[start_brace;
		  (ctl_or
		     (if !exists = Exists then CTL.False else (aftpred label))
		     (quantify guard b2fvs
			(statement_list body NotTop
			   (After (make_seq_after end_brace after))
			   new_quantified2 new_mquantified2
			   (Some (lv,ref true))
			   llabel slabel false guard)))])) in
      let empty_body =
	match Ast.undots body with
	  [body] ->
	    (match Ast.unwrap body with
	      Ast.Dots
		((_,i,Ast.CONTEXT(_,Ast.NOTHING),_),[],_,_) ->
		  (match Ast.unwrap rbrace with
		    Ast.SeqEnd((_,_,Ast.CONTEXT(_,Ast.NOTHING),_))
		    when not (contains_pos rbrace) -> true
		  | _ -> false)
	    | _ -> false)
	| _ -> false in
      if empty_body && List.mem after [Tail;End;VeryEnd]
	  (* for just a match of an if branch of the form { ... }, just
	     match the first brace *)
      then quantify guard lbfvs (make_match lbrace)
      else if ends_in_return body
      then
	(* matching error handling code *)
	(* Cases:
	   1. The pattern as given
	   2. A goto, and then some close braces, and then the pattern as
	   given, but without the braces (only possible if there are no
	   decls, and open and close braces are unmodified)
	   3. Part of the pattern as given, then a goto, and then the rest
	   of the pattern.  For this case, we just check that all paths have
	   a goto within the current braces.  checking for a goto at every
	   point in the pattern seems expensive and not worthwhile. *)
	let pattern2 =
	  let body = preprocess_dots body in (* redo, to drop braces *)
	  make_seq
	    [gotopred label;
	      ctl_au
		(make_match empty_rbrace)
		(ctl_ax (* skip the destination label *)
		   (quantify guard b2fvs
		      (statement_list body NotTop End
			 new_quantified2 new_mquantified2 None llabel slabel
			 true guard)))] in
	let pattern3 =
	  let new_quantified2 = Common.union_set [pv] new_quantified2 in
	  quantify true [pv;lv]
	    (quantify guard b1fvs
	       (make_seq
		  [start_brace;
		    ctl_and
		      (CTL.AU (* want AF even for sgrep *)
			 (CTL.FORWARD,CTL.STRICT,
			  CTL.Pred(Lib_engine.PrefixLabel(lv),CTL.Control),
			  ctl_and (* brace must be eventually after goto *)
			    (gotopred (Some (lv,ref true)))
			    (* want AF even for sgrep *)
			    (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
		      (quantify guard b2fvs
			 (statement_list body NotTop Tail
			    new_quantified2 new_mquantified2
			    None(*no label because past the goto*)
			    llabel slabel false guard))])) in
	ctl_or pattern_as_given (ctl_or pattern2 pattern3)
      else pattern_as_given
  | Ast.IfThen(ifheader,branch,aft) ->
      ifthen ifheader branch aft after quantified minus_quantified
	  label llabel slabel statement make_match guard

  | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
      ifthenelse ifheader branch1 els branch2 aft after quantified
	  minus_quantified label llabel slabel statement make_match guard

  | Ast.While(header,body,aft) | Ast.For(header,body,aft)
  | Ast.Iterator(header,body,aft) ->
      forwhile header body aft after quantified minus_quantified
	label statement make_match guard

  | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
      (*ctl_and        seems pointless, disjuncts see label too
	(label_pred_maker label)*)
      let subformulas =
	List.map
	  (function sl ->
	    statement_list sl top after quantified minus_quantified label
	      llabel slabel true guard)
	  stmt_dots_list in
      let safe_subformulas =
	match top with
	  Top -> List.map2 protect_top_level stmt_dots_list subformulas
	| NotTop -> subformulas in
      List.fold_left ctl_seqor CTL.False safe_subformulas

  | Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) ->
      (* label in recursive call is None because label check is already
	 wrapped around the corresponding code. not good enough, want to stay
	 in a specific region, dots and nests will keep going *)

      let bfvs =
	match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
	with
	  [(wcfvs,bothfvs);(bdfvs,_)] -> bothfvs
	| _ -> failwith "not possible" in

      (* no minus version because when code doesn't contain any minus code *)
      let new_quantified = Common.union_set bfvs quantified in

      let dot_code =
	match Ast.get_mcodekind starter with (*ender must have the same mcode*)
	  Ast.MINUS(_,_,_,_) as d ->
            (* no need for the fresh metavar, but ... is a bit weird as a
	       variable name *)
	    Some(make_match (make_meta_rule_elem d ([],[],[])))
	| _ -> None in

      quantify guard bfvs
	(let dots_pattern =
	  statement_list stmt_dots top (a2n after)
	    new_quantified minus_quantified
	    label(*None*) llabel slabel true guard in
	dots_and_nests multi
	  (Some dots_pattern) whencode bef aft dot_code after label
	  (process_bef_aft new_quantified minus_quantified
	     label(*None*) llabel slabel true)
	  (function x -> (* for when code *)
	    statement_list x NotTop Tail
	      new_quantified minus_quantified label(*None*)
	      llabel slabel true true)
	  (function x -> (* for when code *)
	    statement x NotTop Tail
	      new_quantified minus_quantified label(*None*)
	      llabel slabel true)
	  guard quantified
	  (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))

  | Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
      let dot_code =
	match d with
	  Ast.MINUS(_,_,_,_) ->
            (* no need for the fresh metavar, but ... is a bit weird as a
	       variable name *)
	    Some(make_match (make_meta_rule_elem d ([],[],[])))
	| _ -> None in
      dots_and_nests false None whencodes bef aft dot_code after label
	(process_bef_aft quantified minus_quantified None llabel slabel true)
	(function x ->
	  statement_list x NotTop Tail quantified minus_quantified
	    None llabel slabel true true)
	(function x ->
	  statement x NotTop Tail quantified minus_quantified
	    None llabel slabel true)
	guard quantified
	(function x -> Ast.set_fvs [] (Ast.rewrap stmt x))

  | Ast.Switch(header,lb,decls,cases,rb) ->
      let rec intersect_all = function
	  [] -> []
	| [x] -> x
	| x::xs -> intersect x (intersect_all xs) in
      let rec intersect_all2 = function (* pairwise *)
	  [] -> []
	| x::xs ->
	    let front =
	      List.filter
		(function elem -> List.exists (List.mem elem) xs)
		x in
	    Common.union_set front (intersect_all2 xs) in
      let rec union_all l = List.fold_left union [] l in
      (* start normal variables *)
      let header_fvs = Ast.get_fvs header in
      let lb_fvs = Ast.get_fvs lb in
      let decl_fvs = union_all (List.map Ast.get_fvs (Ast.undots decls)) in
      let case_fvs = List.map Ast.get_fvs cases in
      let rb_fvs = Ast.get_fvs rb in
      let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
	   all_casefvs,all_b3fvs,all_rbfvs) =
	List.fold_left
	  (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
		     all_casefvs,all_b3fvs,all_rbfvs) ->
	    function case_fvs ->
	      match seq_fvs quantified [header_fvs;lb_fvs;case_fvs;rb_fvs] with
		[(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
		  (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
		   b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
		   rbfvs::all_rbfvs)
	      |	_ -> failwith "not possible")
	  ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
      let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
	   all_casefvs,all_b3fvs,all_rbfvs) =
	(List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,
	 List.rev all_b2fvs,List.rev all_casefvs,List.rev all_b3fvs,
	 List.rev all_rbfvs) in
      let exponlyfvs = intersect_all all_efvs in
      let lbonlyfvs = intersect_all all_lbfvs in
(* don't do anything with right brace.  Hope there is no + code on it *)
(*      let rbonlyfvs = intersect_all all_rbfvs in*)
      let b1fvs = union_all all_b1fvs in
      let new1_quantified = union b1fvs quantified in
      let b2fvs =
	union (union_all all_b2fvs) (intersect_all2 all_casefvs) in
      let new2_quantified = union b2fvs new1_quantified in
(*      let b3fvs = union_all all_b3fvs in*)
      (* ------------------- start minus free variables *)
      let header_mfvs = Ast.get_mfvs header in
      let lb_mfvs = Ast.get_mfvs lb in
      let decl_mfvs = union_all (List.map Ast.get_mfvs (Ast.undots decls)) in
      let case_mfvs = List.map Ast.get_mfvs cases in
      let rb_mfvs = Ast.get_mfvs rb in
      let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
	   all_mcasefvs,all_mb3fvs,all_mrbfvs) =
	List.fold_left
	  (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
		     all_casefvs,all_b3fvs,all_rbfvs) ->
	    function case_mfvs ->
	      match
		seq_fvs quantified
		  [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
		[(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
		  (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
		   b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
		   rbfvs::all_rbfvs)
	      |	_ -> failwith "not possible")
	  ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
      let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
	   all_mcasefvs,all_mb3fvs,all_mrbfvs) =
	(List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,
	 List.rev all_mb2fvs,List.rev all_mcasefvs,List.rev all_mb3fvs,
	 List.rev all_mrbfvs) in
(* don't do anything with right brace.  Hope there is no + code on it *)
(*      let rbonlyfvs = intersect_all all_rbfvs in*)
      let mb1fvs = union_all all_mb1fvs in
      let new1_mquantified = union mb1fvs quantified in
      let mb2fvs =
	union (union_all all_mb2fvs) (intersect_all2 all_mcasefvs) in
      let new2_mquantified = union mb2fvs new1_mquantified in
(*      let b3fvs = union_all all_b3fvs in*)
      (* ------------------- end collection of free variables *)
      let switch_header = quantify guard exponlyfvs (make_match header) in
      let lb = quantify guard lbonlyfvs (make_match lb) in
(*      let rb = quantify guard rbonlyfvs (make_match rb) in*)
      let case_headers =
	List.map
	  (function case_line ->
	    match Ast.unwrap case_line with
	      Ast.CaseLine(header,body) ->
		let e1fvs =
		  match seq_fvs new2_quantified [Ast.get_fvs header] with
		    [(e1fvs,_)] -> e1fvs
		  | _ -> failwith "not possible" in
		quantify guard e1fvs (real_make_match label true header)
	    | Ast.OptCase(case_line) -> failwith "not supported")
	  cases in
      let lv = get_label_ctr() in
      let used = ref false in
      let (decls_exists_code,decls_all_code) =
	(*don't really understand this*)
	if (Ast.undots decls) = []
	then (CTL.True,CTL.False)
	else
	let res =
	  statement_list decls NotTop Tail
	    new2_quantified new2_mquantified (Some (lv,used)) llabel None
	    false(*?*) guard in
	(res,res) in
      let no_header =
	ctl_not
	  (List.fold_left ctl_or_fl CTL.False
	     (List.map ctl_uncheck
		(decls_all_code::case_headers))) in
      let case_code =
	List.map
	  (function case_line ->
	    match Ast.unwrap case_line with
	      Ast.CaseLine(header,body) ->
		  let (e1fvs,b1fvs,s1fvs) =
		    let fvs = [Ast.get_fvs header;Ast.get_fvs body] in
		    match seq_fvs new2_quantified fvs with
		      [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
		    | _ -> failwith "not possible" in
		  let (me1fvs,mb1fvs,ms1fvs) =
		    let fvs = [Ast.get_mfvs header;Ast.get_mfvs body] in
		    match seq_fvs new2_mquantified fvs with
		      [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
		    | _ -> failwith "not possible" in
		  let case_header =
		    quantify guard e1fvs (make_match header) in
		  let new3_quantified = union b1fvs new2_quantified in
		  let new3_mquantified = union mb1fvs new2_mquantified in
		  let body =
		    statement_list body NotTop Tail
		      new3_quantified new3_mquantified (Some (lv,used)) llabel
		      (Some (lv,used)) false(*?*) guard in
		  quantify guard b1fvs (make_seq [case_header; body])
	    | Ast.OptCase(case_line) -> failwith "not supported")
	  cases in
      let default_required =
	if List.exists
	    (function case ->
	      match Ast.unwrap case with
		Ast.CaseLine(header,_) ->
		  (match Ast.unwrap header with
		    Ast.Default(_,_) -> true
		  | _ -> false)
	      |	_ -> false)
	    cases
	then function x -> x
	else function x -> ctl_or (fallpred label) x in
      let after_pred = aftpred label in
      let body after_branch =
	ctl_or
	  (default_required
	     (quantify guard b2fvs
		(make_seq
		   [ctl_and lb
		       (List.fold_left ctl_and CTL.True
			  (List.map ctl_ex
			     (decls_exists_code :: case_headers)));
		     List.fold_left ctl_or_fl no_header
		       (decls_all_code :: case_code)])))
	  after_branch in
      let aft =
	(rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,
	match Ast.unwrap rb with
	  Ast.SeqEnd(rb) -> Ast.get_mcodekind rb
	| _ -> failwith "not possible") in
      let (switch_header,wrapper) =
	if !used
	then
	  let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
	  (ctl_and switch_header label_pred,
	   (function body -> quantify true [lv] body))
	else (switch_header,function x -> x) in
      wrapper
	(end_control_structure b1fvs switch_header body
	   after_pred (Some(ctl_ex after_pred)) None aft after label guard)
  | Ast.FunDecl(header,lbrace,body,rbrace) ->
      let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) =
	match
	  seq_fvs quantified
	    [Ast.get_fvs header;Ast.get_fvs lbrace;
	      Ast.get_fvs body;Ast.get_fvs rbrace]
	with
	  [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] ->
	    (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs)
	| _ -> failwith "not possible" in
      let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mrbfvs) =
	match
	  seq_fvs quantified
	    [Ast.get_mfvs header;Ast.get_mfvs lbrace;
	      Ast.get_mfvs body;Ast.get_mfvs rbrace]
	with
	  [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] ->
	    (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs)
	| _ -> failwith "not possible" in
      let function_header = quantify guard hfvs (make_match header) in
      let start_brace = quantify guard lbfvs (make_match lbrace) in
      let stripped_rbrace =
	match Ast.unwrap rbrace with
	  Ast.SeqEnd((data,info,_,_)) ->
	    Ast.rewrap rbrace(Ast.SeqEnd (Ast.make_mcode data))
	| _ -> failwith "unexpected close brace" in
      let end_brace =
	let exit = CTL.Pred (Lib_engine.Exit,CTL.Control) in
	let errorexit = CTL.Pred (Lib_engine.ErrorExit,CTL.Control) in
	let fake_brace = CTL.Pred (Lib_engine.FakeBrace,CTL.Control) in
	ctl_and
	  (quantify guard rbfvs (make_match rbrace))
	  (ctl_and
	     (* the following finds the beginning of the fake braces,
		if there are any, not completely sure how this works.
	     sse the examples sw and return *)
	     (ctl_back_ex (ctl_not fake_brace))
	     (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
      let new_quantified3 =
	Common.union_set b1fvs
	  (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
      let new_mquantified3 =
	Common.union_set mb1fvs
	  (Common.union_set mb2fvs
	     (Common.union_set mb3fvs minus_quantified)) in
      let not_minus = function Ast.MINUS(_,_,_,_) -> false | _ -> true in
      let optim1 =
	match (Ast.undots body,
	       contains_modif rbrace or contains_pos rbrace) with
	  ([body],false) ->
	    (match Ast.unwrap body with
	      Ast.Nest(starter,stmt_dots,ender,[],false,_,_)
		(* perhaps could optimize for minus case too... TODO *)
		when not_minus (Ast.get_mcodekind starter)
	      ->
            (* special case for function header + body - header is unambiguous
	       and unique, so we can just look for the nested body anywhere
	       else in the CFG *)
		Some
		  (CTL.AndAny
		     (CTL.FORWARD,guard_to_strict guard,start_brace,
		      statement_list stmt_dots NotTop
		 (* discards match on right brace, but don't need it *)
			(Guard (make_seq_after end_brace after))
			new_quantified3 new_mquantified3
			None llabel slabel true guard))
	    | Ast.Dots((_,i,d,_),whencode,_,_) when
		(List.for_all
		   (* flow sensitive, so not optimizable *)
		   (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
		      false
		 | _ -> true) whencode) ->
     	    (* try to be more efficient for the case where the body is just
	       ...  Perhaps this is too much of a special case, but useful
	       for dropping a parameter and checking that it is never used. *)
		     (match d with
		       Ast.MINUS(_,_,_,_) -> None
		     | _ ->
			 let pv =
			   (* no nested braces, because only dots *)
			   string2var ("p1") in
			 let paren_pred =
			   CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
			 Some (
			 make_seq
			   [ctl_and start_brace paren_pred;
			     match whencode with
			       [] -> CTL.True
			     | _ ->
				 let leftarg =
				   ctl_and
				     (ctl_not
					(List.fold_left
					   (function prev ->
					     function
						 Ast.WhenAlways(s) -> prev
					       | Ast.WhenNot(sl) ->
						   let x =
						     statement_list sl
						       NotTop Tail
						       new_quantified3
						       new_mquantified3
						       label llabel slabel
						       true true in
						   ctl_or prev x
					       | Ast.WhenNotTrue(_)
					       | Ast.WhenNotFalse(_) ->
						   failwith "unexpected"
					       | Ast.WhenModifier
						   (Ast.WhenAny) -> CTL.False
					       | Ast.WhenModifier(_) -> prev)
					   CTL.False whencode))
				     (List.fold_left
					(function prev ->
					  function
					      Ast.WhenAlways(s) ->
						let x =
						  statement s NotTop Tail
						    new_quantified3
						    new_mquantified3
						    label llabel slabel true in
						ctl_and prev x
					    | Ast.WhenNot(sl) -> prev
					    | Ast.WhenNotTrue(_)
					    | Ast.WhenNotFalse(_) ->
						failwith "unexpected"
					    | Ast.WhenModifier(Ast.WhenAny) ->
						CTL.True
					    | Ast.WhenModifier(_) -> prev)
					CTL.True whencode) in
				 ctl_au leftarg
				   (ctl_and
				      (make_match stripped_rbrace)
				      paren_pred)]))
	    | _ -> None)
	| _ -> None in
      let optim2 =
	(* function body is all minus, no whencode *)
	match Ast.undots body with
	  [body] ->
	    (match Ast.unwrap body with
	      Ast.Dots
		((_,i,(Ast.MINUS(_,_,_,Ast.NOREPLACEMENT) as d),_),[],_,_) ->
		  (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with
		    (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)),
		     Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)))
		    when not (contains_pos rbrace) ->
		      Some
			(* andany drops everything to the end, including close
			   braces - not just function body, could check
			   label to keep braces *)
			(ctl_and start_brace
			   (ctl_ax
			      (CTL.AndAny
				 (CTL.FORWARD,guard_to_strict guard,CTL.True,
				  make_match
				    (make_meta_rule_elem d ([],[],[]))))))
		  | _ -> None)
	    | _ -> None)
	| _ -> None in
      let body_code =
	match (optim1,optim2) with
	  (Some o1,_) -> o1
	| (_,Some o2) -> o2
	| _ ->
	    make_seq
	      [start_brace;
		quantify guard b3fvs
		  (statement_list body NotTop
		     (After (make_seq_after end_brace after))
		     new_quantified3 new_mquantified3 None llabel slabel
		     false guard)] in
      quantify guard b1fvs
	(make_seq [function_header; quantify guard b2fvs body_code])
  | Ast.Define(header,body) ->
      let (hfvs,bfvs,bodyfvs) =
	match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body]
	with
	  [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
	| _ -> failwith "not possible" in
      let (mhfvs,mbfvs,mbodyfvs) =
	match seq_fvs minus_quantified [Ast.get_mfvs header;Ast.get_mfvs body]
	with
	  [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
	| _ -> failwith "not possible" in
      let define_header = quantify guard hfvs (make_match header) in
      let body_code =
	statement_list body NotTop after
	  (Common.union_set bfvs quantified)
	  (Common.union_set mbfvs minus_quantified)
	  None llabel slabel true guard in
      quantify guard bfvs (make_seq [define_header; body_code])
  | Ast.AsStmt(stmt,asstmt) ->
      ctl_and
	(statement stmt top after quantified minus_quantified
	   label llabel slabel guard)
	(statement asstmt top after quantified minus_quantified
	   label llabel slabel guard)
  | Ast.OptStm(stm) ->
      failwith "OptStm should have been compiled away\n"
  | Ast.UniqueStm(stm) -> failwith "arities not yet supported"
  | _ -> failwith "not supported" in
  if guard or !dots_done
  then term
  else
    do_between_dots stmt term after quantified minus_quantified
      label llabel slabel guard

(* term is the translation of stmt *)
and do_between_dots stmt term after quantified minus_quantified
    label llabel slabel guard =
    match Ast.get_dots_bef_aft stmt with
      Ast.AddingBetweenDots (brace_term,n)
    | Ast.DroppingBetweenDots (brace_term,n) ->
	let match_brace =
	  statement brace_term NotTop after quantified minus_quantified
	    label llabel slabel guard in
	let v = Printf.sprintf "_r_%d" n in
	let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in
	let case2 = ctl_and CTL.NONSTRICT (ctl_not (CTL.Ref v)) term in
	CTL.Let
	  (v,ctl_or
	     (ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
	     (ctl_back_ex (ctl_back_ex (falsepred label))),
	   ctl_or case1 case2)	
    | Ast.NoDots -> term

(* un_process_bef_aft is because we don't want to do transformation in this
  code, and thus don't case about braces before or after it *)
and process_bef_aft quantified minus_quantified label llabel slabel guard =
  function
    Ast.WParen (re,n) ->
      let paren_pred = CTL.Pred (Lib_engine.Paren n,CTL.Control) in
      let s = guard_to_strict guard in
      quantify true (get_unquantified quantified [n])
	(ctl_and s (make_raw_match None guard re) paren_pred)
  | Ast.Other s ->
      statement s NotTop Tail quantified minus_quantified
	label llabel slabel guard
  | Ast.Other_dots d ->
      statement_list d NotTop Tail quantified minus_quantified
	label llabel slabel true guard

and protect_top_level stmt_dots formula =
  let starts_with_dots =
    match Ast.undots stmt_dots with
      d::ds ->
	(match Ast.unwrap d with
	  Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_)
	| Ast.Stars(_,_,_,_) -> true
	| _ -> false)
    | _ -> false in
  let starts_with_non_context_brace =
    (* None = No danger
       Some false = OK except on function braces
       Some true = Never OK *)
    match Ast.undots stmt_dots with
      d::ds ->
	(match Ast.unwrap d with
	  Ast.Seq(before,body,after) ->
	    let beforemc =
	      match Ast.unwrap before with
		Ast.SeqStart(obr) -> Ast.get_mcodekind obr
	      | _ -> failwith "bad seq" in
	    let aftermc =
	      match Ast.unwrap after with
		Ast.SeqEnd(cbr) -> Ast.get_mcodekind cbr
	      | _ -> failwith "bad seq"in
	    (match (beforemc,aftermc) with
              (* safe cases *)
	      (Ast.CONTEXT(_,(Ast.NOTHING|Ast.AFTER _)),
	       Ast.CONTEXT(_,(Ast.NOTHING|Ast.BEFORE _))) -> None
	    | (Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),
	       Ast.MINUS(_,_,_,Ast.NOREPLACEMENT))
	      when List.length (Ast.undots body) = 1 -> Some false (*ok on if*)
	      (* unsafe, can't be allowed to match fn top *)
	    | _ -> Some true)
	| _ -> None)
    | _ -> None in
  if starts_with_dots
  then (* EX because there is a loop on enter/top *)
    ctl_and CTL.NONSTRICT (toppred None) (ctl_ex formula)
  else
    match starts_with_non_context_brace with
      None -> formula
    | Some false ->
	ctl_and CTL.NONSTRICT
	  (ctl_not(CTL.EX(CTL.BACKWARD,funpred None)))
	  formula
    | Some true ->
	ctl_and CTL.NONSTRICT
	  (ctl_not(CTL.EX(CTL.BACKWARD,unsbrpred None)))
	  formula


(* --------------------------------------------------------------------- *)
(* cleanup: convert AX to EX for pdots.
Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
This is what we wanted in the first place, but it wasn't possible to make
because the AX and its argument are not created in the same place.
Rather clunky... *)
(* also cleanup XX, which is a marker for the case where the programmer
specifies to change the quantifier on .... Assumed to only occur after one AX
or EX, or at top level. *)

let rec cleanup c =
  let c = match c with CTL.XX(c) -> c | _ -> c in
  match c with
    CTL.False    -> CTL.False
  | CTL.True     -> CTL.True
  | CTL.Pred(p)  -> CTL.Pred(p)
  | CTL.Not(phi) -> CTL.Not(cleanup phi)
  | CTL.Exists(keep,v,phi) -> CTL.Exists(keep,v,cleanup phi)
  | CTL.AndAny(dir,s,phi1,phi2) ->
      CTL.AndAny(dir,s,cleanup phi1,cleanup phi2)
  | CTL.HackForStmt(dir,s,phi1,phi2) ->
      CTL.HackForStmt(dir,s,cleanup phi1,cleanup phi2)
  | CTL.And(s,phi1,phi2)   -> CTL.And(s,cleanup phi1,cleanup phi2)
  | CTL.Or(phi1,phi2)      -> CTL.Or(cleanup phi1,cleanup phi2)
  | CTL.SeqOr(phi1,phi2)   -> CTL.SeqOr(cleanup phi1,cleanup phi2)
  | CTL.Implies(phi1,phi2) -> CTL.Implies(cleanup phi1,cleanup phi2)
  | CTL.AF(dir,s,phi1) -> CTL.AF(dir,s,cleanup phi1)
  | CTL.AX(CTL.FORWARD,s,
	   CTL.Let(v1,e1,
		   CTL.And(CTL.NONSTRICT,CTL.AU(CTL.FORWARD,s2,e2,e3),
			   CTL.EU(CTL.FORWARD,e4,e5)))) ->
    CTL.Let(v1,e1,
	    CTL.And(CTL.NONSTRICT,
		    CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)),
		    CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5))))
  | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,cleanup phi)
  | CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) ->
      CTL.AX(dir,s,cleanup phi)
  | CTL.XX(phi)               -> failwith "bad XX"
  | CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1)
  | CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1)
  | CTL.EF(dir,phi1)   -> CTL.EF(dir,cleanup phi1)
  | CTL.EX(dir,phi1)   -> CTL.EX(dir,cleanup phi1)
  | CTL.EG(dir,phi1)   -> CTL.EG(dir,cleanup phi1)
  | CTL.AW(dir,s,phi1,phi2) -> CTL.AW(dir,s,cleanup phi1,cleanup phi2)
  | CTL.AU(dir,s,phi1,phi2) -> CTL.AU(dir,s,cleanup phi1,cleanup phi2)
  | CTL.EU(dir,phi1,phi2)   -> CTL.EU(dir,cleanup phi1,cleanup phi2)
  | CTL.Let (x,phi1,phi2)   -> CTL.Let (x,cleanup phi1,cleanup phi2)
  | CTL.LetR (dir,x,phi1,phi2) -> CTL.LetR (dir,x,cleanup phi1,cleanup phi2)
  | CTL.Ref(s) -> CTL.Ref(s)
  | CTL.Uncheck(phi1)  -> CTL.Uncheck(cleanup phi1)
  | CTL.InnerAnd(phi1) -> CTL.InnerAnd(cleanup phi1)

(* --------------------------------------------------------------------- *)
(* Function declaration *)

(* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)

let top_level name ((ua,pos),fua) (fuas,t) =
  let ua = List.filter (function (nm,_) -> nm = name) ua in
  used_after := ua;
  saved := Ast.get_saved t;
  let quantified = Common.minus_set (Common.union_set ua fuas) pos in
  let (wrap,formula) =
    match Ast.unwrap t with
      Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
    | Ast.NONDECL(stmt) ->
	let unopt = elim_opt.V.rebuilder_statement stmt in
	let unopt = preprocess_dots_e unopt in
	let formula =
	  cleanup
	    (statement unopt Top VeryEnd quantified [] None None None false) in
	((function x -> NONDECL x), formula)
    | Ast.CODE(stmt_dots) ->
	let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
	let unopt = preprocess_dots unopt in
	let formula =
	  statement_list unopt Top VeryEnd quantified [] None None None
	    false false in
	let clean_formula = cleanup (protect_top_level stmt_dots formula) in
	((function x -> CODE x), clean_formula)
    | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" in
  wrap (quantify false quantified formula)

(* --------------------------------------------------------------------- *)
(* Entry points *)

let asttoctlz (name,(_,_,exists_flag),l)
    (used_after,fresh_used_after,fresh_used_after_seeds) positions =
  letctr := 0;
  labelctr := 0;
  (match exists_flag with
    Ast.Exists -> exists := Exists
  | Ast.Forall -> exists := Forall
  | Ast.Undetermined ->
      exists := if !Flag.sgrep_mode2 then Exists else Forall);

  let (l,used_after) =
    List.split
      (List.filter
	 (function (t,_) ->
	   match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
	 (List.combine l (List.combine used_after positions))) in
  let res =
    List.map2 (top_level name)
      (List.combine used_after fresh_used_after)
      (List.combine fresh_used_after_seeds l) in
  exists := Forall;
  res

let asttoctl r used_after positions =
  match r with
    Ast.ScriptRule _ | Ast.InitialScriptRule _ | Ast.FinalScriptRule _ -> []
  | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) ->
      asttoctlz (a,b,c) used_after positions
  | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CODE CTL.True]

let pp_cocci_predicate (pred,modif) =
  Pretty_print_engine.pp_predicate pred

let cocci_predicate_to_string (pred,modif) =
  Pretty_print_engine.predicate_to_string pred