open Datatypes
open Global
open InterCfg
open InterNode
open IntraCfg
open IntraNode
open List0
open Syn
open TStr
open UserInputType
open VocabA

(** val fail_cmd_mem : pid_t -> t -> bool **)

let fail_cmd_mem = fun f node ->
prerr_string "fail on ";
PPVocab.pp_string PPIL.print_inter_node (f, node);
prerr_endline " by unsound abstract memory";
false

(** val fail_access : pid_t -> t -> bool **)

let fail_access = fun f node ->
prerr_string "fail on ";
PPVocab.pp_string PPIL.print_inter_node (f, node);
prerr_endline " by unsound accessibility";
false

(** val fail_intra_edge : pid_t -> t -> t -> bool **)

let fail_intra_edge = fun f from_node to_node ->
prerr_string "fail on edge ";
PPVocab.pp_string PPIL.print_inter_node (f, from_node);
prerr_string "->";
PPVocab.pp_endline PPIL.print_inter_node (f, to_node);
false

(** val fail_inter_edge : InterNode.t -> InterNode.t -> bool **)

let fail_inter_edge = fun from_node to_node ->
prerr_string "fail on edge ";
PPVocab.pp_string PPIL.print_inter_node from_node;
prerr_string "->";
PPVocab.pp_endline PPIL.print_inter_node to_node;
false

(** val fail_inter_acc : InterNode.t -> InterNode.t -> bool **)

let fail_inter_acc = fun from_node to_node ->
prerr_string "fail on inter acc ";
PPVocab.pp_string PPIL.print_inter_node from_node;
prerr_string "->";
PPVocab.pp_endline PPIL.print_inter_node to_node;
false

(** val fail_inter_edge_invalid : InterNode.t -> InterNode.t -> bool **)

let fail_inter_edge_invalid = fun from_node to_node ->
prerr_string "fail on edge ";
PPVocab.pp_string PPIL.print_inter_node from_node;
prerr_string "->";
PPVocab.pp_string PPIL.print_inter_node to_node;
prerr_endline " by cmd invalidity";
false

(** val fail_inter_edge_no_callof : InterNode.t -> InterNode.t -> bool **)

let fail_inter_edge_no_callof = fun from_node to_node ->
prerr_string "fail on edge ";
PPVocab.pp_string PPIL.print_inter_node from_node;
prerr_string "->";
PPVocab.pp_string PPIL.print_inter_node to_node;
prerr_endline " by call node not found";
false

(** val fail_dens_inputof : InterNode.t -> bool **)

let fail_dens_inputof = fun node ->
prerr_string "fail on node ";
PPVocab.pp_string PPIL.print_inter_node node;
prerr_endline " by invalid densification of inputof.";
false

module Make =
 functor (I:INPUT) ->
 struct
  type access_map = I.Acc.t PidMap.t

  (** val get_access : pid_t -> access_map -> I.Acc.t **)

  let get_access pid m0 =
    default I.Acc.empty (PidMap.find pid m0)

  (** val get_def_access : pid_t -> access_map -> I.PowLoc.t **)

  let get_def_access pid m0 =
    I.Acc.defof (get_access pid m0)

  (** val get_use_access : pid_t -> access_map -> I.PowLoc.t **)

  let get_use_access pid m0 =
    I.Acc.useof (get_access pid m0)

  (** val get_all_access : pid_t -> access_map -> I.PowLoc.t **)

  let get_all_access pid m0 =
    I.Acc.accessof (get_access pid m0)

  (** val icfg : G.t -> InterCfg.t **)

  let icfg g =
    g.G.icfg

  (** val table_find : I.Table.key -> I.Mem.t I.Table.t -> I.Mem.t **)

  let table_find n s =
    default I.Mem.bot (I.Table.find n s)

  (** val valid_cmd :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> pid_t ->
      t -> cmd -> bool **)

  let valid_cmd g access_map0 inputof outputof f node cmd0 =
    let i_m = table_find (f, node) inputof in
    let o_m = table_find (f, node) outputof in
    let access_f = get_access f access_map0 in
    let (o_m', access_f') = I.run_access Strong g (f, node) cmd0 i_m in
    if I.Acc.le_dec access_f' access_f
    then if I.Mem.opt_le o_m' o_m then true else fail_cmd_mem f node
    else fail_access f node

  (** val valid_cmds :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> pid_t ->
      IntraCfg.t -> bool **)

  let valid_cmds g access_map0 inputof outputof f cfg =
    NodeMap.for_all print2 (valid_cmd g access_map0 inputof outputof f)
      cfg.cmds

  (** val valid_intra_edge :
      I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> pid_t -> IntraCfg.t -> t -> t
      -> bool **)

  let valid_intra_edge inputof outputof f cfg from_node to_node =
    let from_m = table_find (f, from_node) outputof in
    let to_m = table_find (f, to_node) inputof in
    if is_call_node cfg from_node
    then true
    else if I.Mem.opt_le from_m to_m
         then true
         else fail_intra_edge f from_node to_node

  (** val valid_intra_edges :
      I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> pid_t -> IntraCfg.t -> bool **)

  let valid_intra_edges inputof outputof f cfg =
    let valid_intra_edges' = fun from_node to_nodes ->
      NodeSet.for_all (valid_intra_edge inputof outputof f cfg from_node)
        to_nodes
    in
    NodeMap.for_all print2 valid_intra_edges' cfg.succ

  (** val valid_cfg :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> pid_t ->
      IntraCfg.t -> bool **)

  let valid_cfg g access_map0 inputof outputof f cfg =
    (&&) (valid_cmds g access_map0 inputof outputof f cfg)
      (valid_intra_edges inputof outputof f cfg)

  (** val valid_cfgs :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> bool **)

  let valid_cfgs g access_map0 inputof outputof =
    PidMap.for_all print2 (valid_cfg g access_map0 inputof outputof)
      (icfg g).cfgs

  (** val valid_inter_edge :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t ->
      InterNode.t -> InterNode.t -> bool **)

  let valid_inter_edge g access_map0 inputof outputof from_node to_node =
    let from_m = table_find from_node outputof in
    let to_m = table_find to_node inputof in
    if InterCfg.is_call_node (icfg g) from_node
    then let callee = get_pid to_node in
         let access = get_all_access callee access_map0 in
         let from_m0 = I.Mem.restrict access from_m in
         if I.Mem.opt_le from_m0 to_m
         then true
         else fail_inter_edge from_node to_node
    else if G.is_exit_node from_node
         then let callee = get_pid from_node in
              let access = get_all_access callee access_map0 in
              (match InterCfg.callof (icfg g) to_node with
               | Some call_node ->
                 let caller_m = table_find call_node outputof in
                 let caller_m0 = I.Mem.subtract access caller_m in
                 if I.Mem.opt_le from_m to_m
                 then if I.Mem.opt_le caller_m0 to_m
                      then true
                      else fail_inter_edge call_node to_node
                 else fail_inter_edge from_node to_node
               | None -> fail_inter_edge_no_callof from_node to_node)
         else fail_inter_edge_invalid from_node to_node

  (** val valid_inter_edges :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> bool **)

  let valid_inter_edges g access_map0 inputof outputof =
    let valid_inter_edges' = fun from_node to_nodes ->
      InterCfg.NodeSet.for_all
        (valid_inter_edge g access_map0 inputof outputof from_node) to_nodes
    in
    InterCfg.NodeMap.for_all print2 valid_inter_edges' (icfg g).InterCfg.succ

  (** val valid_inter_acc :
      access_map -> InterNode.t -> InterNode.t -> bool **)

  let valid_inter_acc access_map0 from_node to_node =
    if InterNode.is_entry_node to_node
    then let caller = get_pid from_node in
         let callee = get_pid to_node in
         let caller_access = get_access caller access_map0 in
         let callee_access = get_access callee access_map0 in
         if I.Acc.le_dec callee_access caller_access
         then true
         else fail_inter_acc from_node to_node
    else true

  (** val valid_inter_accs : G.t -> access_map -> bool **)

  let valid_inter_accs g access_map0 =
    let valid_inter_accs' = fun from_node to_nodes ->
      InterCfg.NodeSet.for_all (valid_inter_acc access_map0 from_node)
        to_nodes
    in
    InterCfg.NodeMap.for_all print2 valid_inter_accs' (icfg g).InterCfg.succ

  (** val valid_dens_node :
      G.t -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> string_t -> t -> cmd
      -> bool **)

  let valid_dens_node g orig_inputof inputof f intra_n cmd0 =
    let n = (f, intra_n) in
    let orig_m = table_find n orig_inputof in
    let m0 = table_find n inputof in
    let (_, acc_n) = I.run_access Strong g n cmd0 orig_m in
    let uses_n = I.Acc.useof acc_n in
    if I.Mem.eq_wrt uses_n orig_m m0 then true else fail_dens_inputof n

  (** val valid_dens_cfg :
      G.t -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> string_t -> IntraCfg.t
      -> bool **)

  let valid_dens_cfg g orig_inputof inputof f cfg =
    NodeMap.for_all print2 (valid_dens_node g orig_inputof inputof f)
      cfg.cmds

  (** val valid_dens :
      G.t -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> bool **)

  let valid_dens g orig_inputof inputof =
    PidMap.for_all print2 (valid_dens_cfg g orig_inputof inputof)
      (icfg g).cfgs

  (** val valid :
      G.t -> access_map -> I.Mem.t I.Table.t -> I.Mem.t I.Table.t -> I.Mem.t
      I.Table.t -> bool **)

  let valid g access_map0 orig_inputof inputof outputof =
    (&&)
      ((&&)
        ((&&) (valid_cfgs g access_map0 inputof outputof)
          (valid_inter_edges g access_map0 inputof outputof))
        (valid_inter_accs g access_map0)) (valid_dens g orig_inputof inputof)

  module AlarmAccess = I.Alarm(I.Acc.MAcc)(I.AccMem)

  (** val check_query_access :
      update_mode -> InterNode.t -> I.Mem.t -> I.query -> I.status list
      I.Acc.MAcc.m **)

  let check_query_access =
    AlarmAccess.check_query

  module AlarmOnly = I.Alarm(Monad.MId)(I.IdMem)

  (** val check_query_only :
      update_mode -> InterNode.t -> I.Mem.t -> I.query -> I.status list
      Monad.MId.m **)

  let check_query_only =
    AlarmOnly.check_query

  (** val check_queries :
      update_mode -> InterNode.t -> I.Mem.t -> (I.query * DPos.DPos.t) ->
      (I.query * DPos.DPos.t) * I.status list **)

  let check_queries mode node m0 = function
  | (q, pos) ->
    let statuses = check_query_only mode node m0 q in ((q, pos), statuses)

  (** val query_flatten' :
      I.query -> DPos.DPos.t -> I.status list ->
      ((I.query * DPos.DPos.t) * I.status) list **)

  let rec query_flatten' q pos = function
  | [] -> []
  | s :: tl -> ((q, pos), s) :: (query_flatten' q pos tl)

  (** val query_flatten :
      ((I.query * DPos.DPos.t) * I.status list) list ->
      ((I.query * DPos.DPos.t) * I.status) list **)

  let rec query_flatten = function
  | [] -> []
  | p :: tl ->
    let (p0, statuses) = p in
    let (q, pos) = p0 in
    app (query_flatten' q pos statuses) (query_flatten tl)

  (** val collect_alarm_result_node :
      update_mode -> I.Mem.t I.Table.t -> string_t -> t' -> cmd ->
      ((I.query * DPos.DPos.t) * I.status) list ->
      ((I.query * DPos.DPos.t) * I.status) list **)

  let collect_alarm_result_node mode inputof pid node cmd0 acc =
    let query_list = I.collect_query cmd0 in
    let m0 = table_find (pid, node) inputof in
    let query_status_list =
      map (check_queries mode (pid, node) m0) query_list
    in
    app (query_flatten query_status_list) acc

  (** val collect_alarm_result_intra :
      update_mode -> I.Mem.t I.Table.t -> string_t -> IntraCfg.t ->
      ((I.query * DPos.DPos.t) * I.status) list ->
      ((I.query * DPos.DPos.t) * I.status) list **)

  let collect_alarm_result_intra mode inputof pid cfg acc =
    let cmds0 = cfg.cmds in
    NodeMap.fold (collect_alarm_result_node mode inputof pid) cmds0 acc

  (** val collect_alarm_result :
      update_mode -> G.t -> I.Mem.t I.Table.t ->
      ((I.query * DPos.DPos.t) * I.status) list **)

  let collect_alarm_result mode g inputof =
    let icfg0 = g.G.icfg in
    let cfgs0 = icfg0.cfgs in
    PidMap.fold (collect_alarm_result_intra mode inputof) cfgs0 []
 end