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