open BinNums
open Coqlib
open Datatypes
open Iteration
open Kildall
open List0
open ListSet
open Maps
open SSA

(* We follow AC implemention as proposed by Zhao and Zdancewic in [CPP12]. *)

(** val incl_dec : ('a1 -> 'a1 -> bool) -> 'a1 list -> 'a1 list -> bool **)

let rec incl_dec hdec l1 l2 =
  match l1 with
  | [] -> true
  | a :: l3 -> if in_dec hdec a l2 then incl_dec hdec l3 l2 else false

module AtomSet = 
 struct 
  (** val set_eq_dec : ('a1 -> 'a1 -> bool) -> 'a1 set -> 'a1 set -> bool **)
  
  let set_eq_dec hdec l1 l2 =
    let s = incl_dec hdec l1 l2 in if s then incl_dec hdec l2 l1 else false
 end

module Dominators = 
 struct 
  type t = node set option
  
  (** val eq_dec : t -> t -> bool **)
  
  let eq_dec x y =
    match x with
    | Some s ->
      (match y with
       | Some s0 -> AtomSet.set_eq_dec peq s s0
       | None -> false)
    | None ->
      (match y with
       | Some s -> false
       | None -> true)
  
  (** val beq : t -> t -> bool **)
  
  let beq x y =
    if eq_dec x y then true else false
  
  (** val top : t **)
  
  let top =
    Some empty_set
  
  (** val bot : t **)
  
  let bot =
    None
  
  (** val lub : t -> t -> t **)
  
  let lub x y =
    match x with
    | Some cx ->
      (match y with
       | Some cy -> Some (set_inter peq cx cy)
       | None -> x)
    | None -> y
  
  (** val add : t -> node -> t **)
  
  let add x a =
    match x with
    | Some cx -> Some (a :: cx)
    | None -> None
  
  (** val lubs : t list -> t **)
  
  let lubs pds =
    fold_left (fun acc p -> lub acc p) pds bot
 end

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

module Dataflow_Solver_Var_Top = 
 functor (NS:NODE_SET) ->
 struct 
  module L = Dominators
  
  type state = { st_in : L.t PMap.t; st_wrk : NS.t }
  
  (** val state_rect : (L.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.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.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 : (node * L.t) list -> L.t PMap.t **)
  
  let rec start_state_in = function
  | [] -> PMap.init L.bot
  | p :: rem ->
    let (n, v) = p in
    let m = start_state_in rem in PMap.set n (L.lub (PMap.get n m) v) m
  
  (** val start_state : node list PTree.t -> (node * L.t) list -> state **)
  
  let start_state successors entrypoints =
    { st_in = (start_state_in entrypoints); st_wrk =
      (NS.initial successors) }
  
  (** val propagate_succ : state -> L.t -> node -> state **)
  
  let propagate_succ s out n =
    let oldl = PMap.get n (st_in s) in
    let newl = L.lub oldl out in
    if L.beq oldl newl
    then s
    else { st_in = (PMap.set n newl (st_in s)); st_wrk =
           (NS.add n (st_wrk s)) }
  
  (** val propagate_succ_list : state -> L.t -> node set -> state **)
  
  let rec propagate_succ_list s out = function
  | [] -> s
  | n :: rem -> propagate_succ_list (propagate_succ s out n) out rem
  
  (** val step :
      node list PTree.t -> (node -> L.t -> L.t) -> state -> (L.t PMap.t,
      state) sum **)
  
  let step successors 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 successors n))
    | None -> Coq_inl (st_in s)
  
  (** val fixpoint :
      node list PTree.t -> (node -> L.t -> L.t) -> (node * L.t) list -> L.t
      PMap.t option **)
  
  let fixpoint successors transf entrypoints =
    PrimIter.iterate (step successors transf)
      (start_state successors entrypoints)
 end

module AtomNodeSet = 
 struct 
  type t = node set
  
  (** val add : node -> t -> t **)
  
  let add n s =
    set_add peq n s
  
  (** val pick : t -> (node * positive set) option **)
  
  let pick = function
  | [] -> None
  | n :: s' -> Some (n, (set_remove peq n s'))
  
  (** val initial : node list PTree.t -> t **)
  
  let initial successors =
    PTree.fold (fun s pc scs -> add pc s) successors empty_set
 end

module DomDS = Dataflow_Solver_Var_Top(AtomNodeSet)

(** val transfer : node -> Dominators.t -> Dominators.t **)

let transfer lbl before =
  Dominators.add before lbl

(** val dom_compute : coq_function -> Dominators.t PMap.t **)

let dom_compute f =
  match DomDS.fixpoint (successors_map f) transfer ((f.fn_entrypoint,
          Dominators.top) :: []) with
  | Some res -> res
  | None -> PMap.init Dominators.top

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

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