(*
 * Copyright 2010, 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.
 *)


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

(* --------------------------------------------------------------------- *)
(* result type *)

type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
type formula =
    (cocci_predicate,Ast_cocci.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl

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

let contains_modif =
  let bind x y = x or y in
  let option_default = false in
  let mcode r (_,_,kind,_) =
    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,Ast.NoMetaPos)) res
    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) 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

let ctl_exists keep_wit v x =
  CTL.Exists(!Flag_popl.keep_all_wits or keep_wit,v,x)

let predmaker keep_wit term =
  if (!Flag_popl.keep_all_wits or keep_wit) &&
     (!Flag_popl.mark_all or contains_modif term)
  then
    let v = ("","_v") in
    ctl_exists true v
      (CTL.Pred (Lib_engine.Match(term),CTL.Modif v))
  else CTL.Pred (Lib_engine.Match(term),CTL.Control)

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

let is_true = function CTL.True -> true | _ -> false

let is_false = function CTL.False -> true | _ -> false

let ctl_true       = CTL.True

let ctl_false      = CTL.False

let ctl_and x y    =
  if is_true x then y
  else if is_true y then x else CTL.And(CTL.STRICT,x,y)

let ctl_or x y     =
  if is_false x then y
  else if is_false y then x else CTL.Or(x,y)

let ctl_seqor x y  = CTL.SeqOr(x,y)

let ctl_not x      = CTL.Not(x)

let ctl_ax x       =
  if is_true x then CTL.True
  else CTL.AX(CTL.FORWARD,CTL.STRICT,x)

let ctl_ex x       =
  if is_true x then CTL.True
  else CTL.EX(CTL.FORWARD,x)

let ctl_back_ex x  =
  if is_true x then CTL.True
  else CTL.EX(CTL.BACKWARD,x)

let after          = CTL.Pred(Lib_engine.After, CTL.Control)
let fall           = CTL.Pred(Lib_engine.FallThrough, CTL.Control)
let exit           = CTL.Pred(Lib_engine.Exit, CTL.Control)
let truepred       = CTL.Pred(Lib_engine.TrueBranch, CTL.Control)
let falsepred      = CTL.Pred(Lib_engine.FalseBranch, CTL.Control)
let retpred        = CTL.Pred(Lib_engine.Return, CTL.Control)

let string2var x = ("",x)

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

let ctl_au x y = CTL.AU(CTL.FORWARD,CTL.STRICT,x,y)

let ctl_uncheck x  = CTL.Uncheck(x)

let make_meta_rule_elem d =
  let nm = "_S" in
  Ast.make_meta_rule_elem nm d ([],[],[])

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

let rec ctl_seq keep_wit a = function
    Past.Seq(elem,seq) ->
      ctl_element keep_wit (ctl_seq keep_wit a seq) elem
  | Past.Empty -> a
  | Past.SExists(var,seq) -> ctl_exists keep_wit var (ctl_seq keep_wit a seq)

and ctl_term keep_wit a = function
    Past.Atomic(term) -> ctl_and (predmaker keep_wit term) (ctl_ax a)
  | Past.IfThen(test,thn,(_,_,_,aft)) -> ifthen keep_wit (Some a) test thn aft
  | Past.TExists(var,term) ->
      ctl_exists keep_wit var (ctl_term keep_wit a term)

and ctl_element keep_wit a = function
    Past.Term(term,ba) ->
      do_between_dots keep_wit ba (ctl_term keep_wit a term) a
  | Past.Or(seq1,seq2) ->
      ctl_seqor (ctl_seq keep_wit a seq1) (ctl_seq keep_wit a seq2)
  | Past.DInfo(dots) -> ctl_au (guard_ctl_dots keep_wit a dots) a
  | Past.EExists(var,elem) ->
      ctl_exists keep_wit var (ctl_element keep_wit a elem)

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

and guard_ctl_seq keep_wit a = function
    Past.Seq(elem,Past.Empty) -> guard_ctl_element keep_wit a elem
  | Past.Seq(elem,seq) ->
      ctl_element keep_wit (guard_ctl_seq keep_wit a seq) elem
  | Past.Empty -> ctl_true
  | Past.SExists(var,seq) ->
      ctl_exists keep_wit var (guard_ctl_seq keep_wit a seq)

and guard_ctl_term keep_wit = function
    Past.Atomic(term) -> predmaker keep_wit term
  | Past.IfThen(test,thn,(_,_,_,aft)) -> ifthen keep_wit None test thn aft
  | Past.TExists(var,term) ->
      ctl_exists keep_wit var (guard_ctl_term keep_wit term)

and guard_ctl_element keep_wit a = function
    Past.Term(term,_) -> guard_ctl_term keep_wit term
  | Past.Or(seq1,seq2) ->
      ctl_seqor
	(guard_ctl_seq keep_wit a seq1) (guard_ctl_seq keep_wit a seq2)
  | Past.DInfo(dots) -> ctl_au (guard_ctl_dots keep_wit a dots) a
  | Past.EExists(var,elem) ->
      ctl_exists keep_wit var (guard_ctl_element keep_wit a elem)

and guard_ctl_dots keep_wit a = function
    Past.Dots -> ctl_true
(* | Past.Nest(_) when not keep_wit -> ctl_true
   a possible optimization, but irrelevant to popl example *)
  | Past.Nest(seq) ->
      ctl_or
	(guard_ctl_seq true a seq)
	(ctl_not (guard_ctl_seq false a seq))
  | Past.When(dots,seq) ->
      ctl_and
	(guard_ctl_dots keep_wit a dots)
	(ctl_not (guard_ctl_seq false a seq))

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

and ifthen keep_wit a test thn aft =
(* "if (test) thn; after" becomes:
    if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
             & EX After
    (* doesn't work for C code if (x) return 1; else return 2; *)
*)
  let end_code =
    match (aft,a) with
      (Ast.CONTEXT(_,Ast.NOTHING),None) -> ctl_true
    | (Ast.CONTEXT(_,Ast.NOTHING),Some a) -> ctl_ax (ctl_ax a)
    | (_,None) -> failwith "not possible"
    | (_,Some a) ->
	ctl_ax
	  (ctl_and
	     (predmaker keep_wit (make_meta_rule_elem aft))
	     (ctl_ax a)) in
  let body =
    ctl_or
      (ctl_and truepred
	 (ctl_ax
	    (guard_ctl_term keep_wit thn)))
      (ctl_or fall
	 (ctl_and after end_code)) in
  ctl_and (ctl_term keep_wit body test)
    (match a with Some CTL.True | None -> ctl_true | Some _ -> ctl_ex after)

and do_between_dots keep_wit ba term after =
    match ba with
      Past.AddingBetweenDots (brace_term,n)
    | Past.DroppingBetweenDots (brace_term,n) ->
	(* not sure at all what to do here for after... *)
	let match_brace = ctl_term keep_wit after brace_term in
	let v = Printf.sprintf "_r_%d" n in
	let case1 = ctl_and (CTL.Ref v) match_brace in
	let case2 = ctl_and (ctl_not (CTL.Ref v)) term in
	CTL.Let
	  (v,ctl_or
	     (ctl_back_ex truepred)
	     (ctl_back_ex (ctl_back_ex falsepred)),
	   ctl_or case1 case2)	
    | Past.NoDots -> term

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

let toctl sl = ctl_seq true ctl_true sl