open BinNums
open BinPos
open Coqlib
open Datatypes
open FSetAVL
open Int0
open Iteration
open Kildall
open List0
open Maps
open Ordered
open Postorder
open SSA
open Specif

(* We follow CHK implemention as proposed by Zhao and Zdancewic in [CPP12]. 
   They have modified the original algorithm in order to turn it into a suitable
   instanciation of Compcert Kildall framework. *)

module type LATTICEELT = 
 sig 
  type t 
  
  val bot : t
  
  val lub : t -> t -> t * bool
  
  val top : t
 end

(** * The Semilattice of ordered node list *)
module L = 
 struct 
  type t = node list option
  
  (** val bot : t **)
  
  let bot =
    None
  
  (** val merge_aux_func :
      (positive list, (positive list, positive list * bool) sigT) sigT ->
      positive list * bool **)
  
  let rec merge_aux_func x =
    let l1 = projT1 x in
    let l2 = projT1 (projT2 x) in
    let acc = projT2 (projT2 x) in
    let merge_aux0 = fun l3 l4 acc0 ->
      let y = Coq_existT (l3, (Coq_existT (l4, acc0))) in merge_aux_func y
    in
    let (rl, changed) = acc in
    (match l1 with
     | [] -> acc
     | wildcard' :: wildcard'0 ->
       (match l2 with
        | [] -> (rl, true)
        | p2 :: l2' ->
          let filtered_var = Pos.compare_cont wildcard' p2 Eq in
          (match filtered_var with
           | Eq -> merge_aux0 wildcard'0 l2' ((wildcard' :: rl), changed)
           | Lt -> merge_aux0 wildcard'0 l2 (rl, true)
           | Gt -> merge_aux0 l1 l2' (rl, changed))))
  
  (** val merge_aux :
      positive list -> positive list -> (positive list * bool) -> positive
      list * bool **)
  
  let merge_aux l1 l2 acc =
    merge_aux_func (Coq_existT (l1, (Coq_existT (l2, acc))))
  
  (** val merge : positive list -> positive list -> positive list * bool **)
  
  let merge l1 l2 =
    let (rl, changed) = merge_aux l1 l2 ([], false) in ((rev rl), changed)
  
  (** val lub : t -> t -> t * bool **)
  
  let lub x y =
    match x with
    | Some x' ->
      (match y with
       | Some y' -> let (r, changed) = merge x' y' in ((Some r), changed)
       | None -> (x, false))
    | None ->
      (match y with
       | Some l -> (y, true)
       | None -> (x, false))
  
  (** val top : t **)
  
  let top =
    Some []
  
  (** val transfer : positive -> t -> t **)
  
  let transfer n = function
  | Some ps -> Some (n :: ps)
  | None -> None
 end

module type PNODE_SET = 
 sig 
  type t 
  
  val add : positive -> t -> t
  
  val pick : t -> (positive * t) option
  
  val initial : positive list PTree.t -> t
 end

module PositiveSet = Make(OrderedPositive)

module PNodeSetMax = 
 struct 
  type t = PositiveSet.t
  
  (** val add : positive -> t -> t **)
  
  let add n s =
    PositiveSet.add n s
  
  (** val pick : t -> (PositiveSet.elt * PositiveSet.t) option **)
  
  let pick s =
    match PositiveSet.max_elt s with
    | Some n -> Some (n, (PositiveSet.remove n s))
    | None -> None
  
  (** val initial : positive list PTree.t -> PositiveSet.t **)
  
  let initial successors0 =
    PTree.fold (fun s pc scs -> PositiveSet.add pc s) successors0
      PositiveSet.empty
 end

module Weak_Succ_Dataflow_Solver = 
 functor (NS:PNODE_SET) ->
 functor (L__2:LATTICEELT) ->
 struct 
  type state = { st_in : L__2.t PMap.t; st_wrk : NS.t }
  
  (** val state_rect : (L__2.t PMap.t -> NS.t -> 'a1) -> state -> 'a1 **)
  
  let state_rect f s =
    let { st_in = x; st_wrk = x0 } = s in f x x0
  
  (** val state_rec : (L__2.t PMap.t -> NS.t -> 'a1) -> state -> 'a1 **)
  
  let state_rec f s =
    let { st_in = x; st_wrk = x0 } = s in f x x0
  
  (** val st_in : state -> L__2.t PMap.t **)
  
  let st_in s =
    s.st_in
  
  (** val st_wrk : state -> NS.t **)
  
  let st_wrk s =
    s.st_wrk
  
  (** val start_state_in : (positive * L__2.t) list -> L__2.t PMap.t **)
  
  let rec start_state_in = function
  | [] -> PMap.init L__2.bot
  | p :: rem ->
    let (n, v) = p in
    let m = start_state_in rem in
    PMap.set n (fst (L__2.lub (PMap.get n m) v)) m
  
  (** val start_state :
      positive list PTree.t -> (positive * L__2.t) list -> state **)
  
  let start_state successors0 entrypoints =
    { st_in = (start_state_in entrypoints); st_wrk =
      (NS.initial successors0) }
  
  (** val propagate_succ : state -> L__2.t -> positive -> state **)
  
  let propagate_succ s out n =
    let oldl = PMap.get n (st_in s) in
    let (newl, changed) = L__2.lub oldl out in
    if changed
    then { st_in = (PMap.set n newl (st_in s)); st_wrk =
           (NS.add n (st_wrk s)) }
    else s
  
  (** val propagate_succ_list : state -> L__2.t -> positive list -> state **)
  
  let rec propagate_succ_list s out = function
  | [] -> s
  | n :: rem -> propagate_succ_list (propagate_succ s out n) out rem
  
  (** val step :
      positive list PTree.t -> (positive -> L__2.t -> L__2.t) -> state ->
      (L__2.t PMap.t, state) sum **)
  
  let step successors0 transf s =
    match NS.pick (st_wrk s) with
    | Some p ->
      let (n, rem) = p in
      Coq_inr
      (propagate_succ_list { st_in = (st_in s); st_wrk = rem }
        (transf n (PMap.get n (st_in s))) (successors_list successors0 n))
    | None -> Coq_inl (st_in s)
  
  (** val fixpoint :
      positive list PTree.t -> (positive -> L__2.t -> L__2.t) ->
      (positive * L__2.t) list -> L__2.t PMap.t option **)
  
  let fixpoint successors0 transf entrypoints =
    PrimIter.iterate (step successors0 transf)
      (start_state successors0 entrypoints)
 end

module DomDS = Weak_Succ_Dataflow_Solver(PNodeSetMax)(L)

(** val renum_pc :
    Postorder.node PTree.t -> Postorder.node -> Postorder.node **)

let renum_pc pnum pc =
  match PTree.get pc pnum with
  | Some pc' -> pc'
  | None -> Coq_xH

(** val renum :
    (Postorder.node -> Postorder.node) -> Postorder.node list PTree.t ->
    Postorder.node list PTree.t **)

let renum r_pc successors0 =
  PTree.fold (fun pt n l -> PTree.set (r_pc n) (List0.map r_pc l) pt)
    successors0 PTree.empty

(** val dom_compute :
    coq_function -> (Postorder.node -> Postorder.node) * L.t PMap.t **)

let dom_compute f =
  let pnum = postorder (successors_map f) f.fn_entrypoint in
  let r_pc = renum_pc pnum in
  let entry = r_pc f.fn_entrypoint in
  let successors0 = renum r_pc (successors f) in
  (match DomDS.fixpoint successors0 L.transfer ((entry, L.top) :: []) with
   | Some res -> (r_pc, res)
   | None -> (r_pc, (PMap.init L.top)))

(** val test_dom :
    ((Postorder.node -> Postorder.node) * L.t PMap.t) -> Postorder.node ->
    Postorder.node -> bool **)

let test_dom r_pc_m d n =
  let (r_pc, m) = r_pc_m in
  (match PMap.get (r_pc n) m with
   | Some l -> proj_sumbool (in_dec peq (r_pc d) l)
   | None -> true)