open DItv
open DomAbs
open DomArrayBlk
open DomBasic
open DomMem
open Fold
open Global
open InterNode
open SemEval
open SemMem
open SemPrune
open Syn
open TStr
open UserInputType

(** val str_realloc : string_t **)

let str_realloc = "realloc"

(** val str_strlen : string_t **)

let str_strlen = "strlen"

module SMProcLoc = SetMap(Proc)(PowProc)(Loc)(PowLoc)

module type RUN =
 functor (M:Monad.Monad) ->
 functor (MB:sig
  val mem_find : Loc.t -> Mem.t -> Val.t M.m

  val mem_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_pre_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m
 end) ->
 sig
  val run : update_mode -> G.t -> t -> cmd -> Mem.t -> Mem.t M.m
 end

module Run =
 functor (M:Monad.Monad) ->
 functor (MB:sig
  val mem_find : Loc.t -> Mem.t -> Val.t M.m

  val mem_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_pre_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m
 end) ->
 struct
  module SemMem = SemMem.Make(M)(MB)

  module SemEval = SemEval.Make(M)(MB)

  module SemPrune = Make(M)(MB)

  module BJProcMem = BigJoinM(M)(Proc)(PowProc)(Mem)

  (** val eval : update_mode -> t -> exp -> Mem.t -> Val.t M.m **)

  let eval mode =
    SemPrune.SemEval.eval mode

  (** val mem_lookup : PowLoc.t -> Mem.t -> Val.t M.m **)

  let mem_lookup k m0 =
    SemMem.mem_lookup k m0

  (** val mem_update :
      update_mode -> G.t -> Loc.t -> Val.t -> Mem.t -> Mem.t M.m **)

  let mem_update mode g k v m0 =
    SemMem.mem_update mode g k v m0

  (** val mem_wupdate :
      update_mode -> PowLoc.t -> Val.t -> Mem.t -> Mem.t M.m **)

  let mem_wupdate mode k v m0 =
    SemMem.mem_wupdate mode k v m0

  (** val update_rets :
      update_mode -> t -> PowProc.t -> lval option -> Mem.t -> Mem.t M.m **)

  let update_rets mode node callees ret_opt m0 =
    M.bind
      (match ret_opt with
       | Some ret_lv -> SemPrune.SemEval.eval_lv mode node ret_lv m0
       | None -> M.ret PowLoc.bot) (fun ret_locs ->
      let callees_locs = SMProcLoc.map loc_of_proc callees in
      mem_wupdate mode callees_locs (val_of_pow_loc ret_locs) m0)

  (** val external_value : Allocsite.t -> Val.t **)

  let external_value a =
    (((Itv.top, (PowLoc.singleton (loc_of_allocsite a))),
      (ArrayBlk.extern a)), PowProc.bot)

  (** val run_realloc :
      update_mode -> t -> lval -> Val.t list -> Mem.t -> Mem.t M.m **)

  let run_realloc mode node ret_lv vs m0 =
    match vs with
    | [] -> M.ret m0
    | _ :: l ->
      (match l with
       | [] -> M.ret m0
       | size_v :: _ ->
         M.bind (SemPrune.SemEval.eval_lv mode node ret_lv m0) (fun lv ->
           mem_wupdate mode lv (SemPrune.SemEval.eval_alloc' node size_v) m0))

  (** val run_strlen : update_mode -> t -> lval -> Mem.t -> Mem.t M.m **)

  let run_strlen mode node ret_lv m0 =
    M.bind (SemPrune.SemEval.eval_lv mode node ret_lv m0) (fun lv ->
      mem_wupdate mode lv (val_of_itv Itv.zero_pos) m0)

  (** val set_ext_allocsite :
      update_mode -> t -> lval -> Allocsite.t -> Mem.t -> Mem.t M.m **)

  let set_ext_allocsite mode node ret_lv allocsite m0 =
    let ext_v = external_value allocsite in
    M.bind (SemPrune.SemEval.eval_lv mode node ret_lv m0) (fun lv ->
      M.bind (mem_wupdate mode lv ext_v m0) (fun m1 ->
        mem_wupdate mode (PowLoc.singleton (loc_of_allocsite allocsite))
          ext_v m1))

  (** val run_undef_funcs :
      update_mode -> t -> lval option -> pid_t -> Val.t list -> Mem.t ->
      Mem.t M.m **)

  let run_undef_funcs mode node ret_opt ext vs m0 =
    match ret_opt with
    | Some ret_lv ->
      if DStr.DStr.eq_dec ext str_realloc
      then run_realloc mode node ret_lv vs m0
      else if DStr.DStr.eq_dec ext str_strlen
           then run_strlen mode node ret_lv m0
           else set_ext_allocsite mode node ret_lv
                  (allocsite_of_ext (Some ext)) m0
    | None -> M.ret m0

  (** val run : update_mode -> G.t -> t -> cmd -> Mem.t -> Mem.t M.m **)

  let run mode g node =
    let pid = get_pid node in
    (fun cmd0 m0 ->
    match cmd0 with
    | Cset (l, e, _) ->
      let Coq_lval_intro (lh, o, _) = l in
      (match lh with
       | VarLhost (x, is_global) ->
         (match o with
          | NoOffset ->
            let lv = SemPrune.SemEval.eval_var node x is_global in
            M.bind (eval mode node e m0) (fun v -> mem_update mode g lv v m0)
          | _ ->
            M.bind (SemPrune.SemEval.eval_lv mode node l m0) (fun lv ->
              M.bind (eval mode node e m0) (fun v ->
                mem_wupdate mode lv v m0)))
       | MemLhost _ ->
         M.bind (SemPrune.SemEval.eval_lv mode node l m0) (fun lv ->
           M.bind (eval mode node e m0) (fun v -> mem_wupdate mode lv v m0)))
    | Cexternal (l, _) ->
      set_ext_allocsite mode node l (allocsite_of_ext None) m0
    | Calloc (l, a, _) ->
      M.bind (SemPrune.SemEval.eval_lv mode node l m0) (fun lv ->
        M.bind (SemPrune.SemEval.eval_alloc mode node a m0) (fun v ->
          mem_wupdate mode lv v m0))
    | Csalloc (l, s, _) ->
      let allocsite = allocsite_of_node node in
      let pow_loc = PowLoc.singleton (loc_of_allocsite allocsite) in
      M.bind (SemPrune.SemEval.eval_lv mode node l m0) (fun lv ->
        M.bind (mem_wupdate mode pow_loc (eval_string s) m0) (fun m1 ->
          mem_wupdate mode lv (eval_string_loc s allocsite pow_loc) m1))
    | Cfalloc (l, name, _) ->
      M.bind (SemPrune.SemEval.eval_lv mode node l m0) (fun lv ->
        mem_wupdate mode lv (val_of_pow_proc (PowProc.singleton name)) m0)
    | Cassume (e, _) -> SemPrune.prune g mode node e m0
    | Ccall (ret_opt, f, args, _) ->
      M.bind (SemPrune.SemEval.eval_list mode node args m0) (fun vs ->
        match G.is_undef_e f g with
        | Some fname -> run_undef_funcs mode node ret_opt fname vs m0
        | None ->
          M.bind (eval mode node f m0) (fun f_v ->
            let fs = powProc_of_val f_v in
            M.bind (update_rets mode node fs ret_opt m0) (fun m1 ->
              BJProcMem.weak_big_join (SemMem.bind_args mode g vs) fs
                (M.ret m1))))
    | Creturn (ret_opt, _) ->
      (match ret_opt with
       | Some e ->
         M.bind (eval mode node e m0) (fun v ->
           M.bind (mem_lookup (PowLoc.singleton (loc_of_proc pid)) m0)
             (fun ret_loc -> mem_wupdate mode (deref_of_val ret_loc) v m0))
       | None -> M.ret m0)
    | _ -> M.ret m0)
 end

module RunAccess = Run(Acc.MAcc)(AccMem)

(** val run_access :
    update_mode -> G.t -> t -> cmd -> Mem.t -> Mem.t Acc.MAcc.m **)

let run_access =
  RunAccess.run

module RunOnly = Run(Monad.MId)(IdMem)

(** val run_only :
    update_mode -> G.t -> t -> cmd -> Mem.t -> Mem.t Monad.MId.m **)

let run_only =
  RunOnly.run