(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
Set Implicit Arguments.

Require Import Setoid.
Require Import Morphisms.
Require Import Monad hpattern vgtac VocabA Syn Global DLat
        DPow DMap DPos UserInputType.
Require DMem Access.

Definition fail_cmd_mem (f : pid_t) (node : IntraNode.t) := false.
Extract Constant 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".

Definition fail_access (f : pid_t) (node : IntraNode.t) := false.
Extract Constant fail_access =>
"fun f node ->
prerr_string ""fail on "";
PPVocab.pp_string PPIL.print_inter_node (f, node);
prerr_endline "" by unsound accessibility"";
false".

Definition fail_intra_edge (f : pid_t) (from_node to_node : IntraNode.t) :=
  false.
Extract Constant 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".

Definition fail_inter_edge (from_node to_node : InterNode.t) := false.
Extract Constant 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".

Definition fail_inter_acc (from_node to_node : InterNode.t) := false.
Extract Constant 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".

Definition fail_inter_edge_invalid (from_node to_node : InterNode.t) := false.
Extract Constant 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".

Definition fail_inter_edge_no_callof (from_node to_node : InterNode.t) := false.
Extract Constant 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".

Definition fail_dens_inputof (node : InterNode.t) := false.
Extract Constant 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 (Import I : INPUT).

(* Disjoin relation between memories and accessibilities. *)

Definition disjoint (m : Mem.t) (acc : Acc.t) : Prop :=
  forall l (Hl : PowLoc.mem l (Acc.accessof acc) = true),
    Val.eq (Mem.find l m) Val.bot.

Lemma disjoint_bot : forall acc, disjoint Mem.bot acc.
Proof. unfold disjoint; i. by apply Mem.empty_prop with (k:=l). Qed.

Lemma disjoint_join :
  forall m1 m2 acc (Hdis1: disjoint m1 acc) (Hdis2: disjoint m2 acc),
    disjoint (Mem.join m1 m2) acc.
Proof.
unfold disjoint; i. eapply Val.eq_trans; [by apply Mem.join_find|].
apply Val.le_antisym.
- apply Val.join_lub; apply Val.le_refl; [by apply Hdis1|by apply Hdis2].
- by apply Val.bot_prop.
Qed.

Lemma disjoint_le :
  forall m acc1 acc2 (Hle: Acc.le acc2 acc1) (Hdis: disjoint m acc1),
    disjoint m acc2.
Proof.
unfold disjoint. i.
apply Hdis.
eapply PowLoc.le_mem_true; [|by apply Hl].
by apply Acc.accessof_mor'.
Qed.

Lemma disjoint_mor :
  Proper (Mem.eq ==> Acc.eq ==> Basics.impl) disjoint.
Proof.
unfold disjoint. intros m1 m2 Hm a1 a2 Ha Hdis1. i.
eapply Val.eq_trans; [|apply Hdis1].
- apply Val.eq_sym, Mem.find_mor; [by apply Loc.eq_refl|by auto].
- rewrite <- Hl. apply PowLoc.mem_mor; [by apply Loc.eq_refl|].
  by apply Acc.accessof_mor.
Qed.

Lemma disjoint_left :
  forall m a1 a2 (Hdis : disjoint m (Acc.join a1 a2)), disjoint m a1.
Proof.
unfold disjoint; i.
apply Hdis. eapply Acc.le_mem_true; [|by apply Hl].
by apply Acc.join_left.
Qed.

Lemma disjoint_right :
  forall m a1 a2 (Hdis : disjoint m (Acc.join a1 a2)), disjoint m a2.
Proof.
unfold disjoint; i.
apply Hdis. eapply Acc.le_mem_true; [|by apply Hl].
by apply Acc.join_right.
Qed.

Lemma disjoint_mono :
  forall a1 a2 (Hle : Acc.le a1 a2) m (Hdis : disjoint m a2), disjoint m a1.
Proof.
i. intros l Hl1.
apply Hdis. eapply Acc.le_mem_true; [by apply Hle|]. by auto.
Qed.

(* Access map *)

Definition access_map := InterCfg.PidMap.t Acc.t.

Definition get_access (pid : pid_t) (m : access_map) : Acc.t :=
  default Acc.empty (InterCfg.PidMap.find pid m).

Definition get_def_access (pid : pid_t) (m : access_map) : PowLoc.t :=
  Acc.defof (get_access pid m).

Definition get_use_access (pid : pid_t) (m : access_map) : PowLoc.t :=
  Acc.useof (get_access pid m).

Definition get_all_access (pid : pid_t) (m : access_map) : PowLoc.t :=
  Acc.accessof (get_access pid m).

(* Validator *)

Section Validate.

Local Open Scope bool.

Variable g : G.t.

Variable access_map : access_map.

Variables orig_inputof orig_outputof : Table.t Mem.t.

Variables inputof outputof : Table.t Mem.t.

Definition icfg := G.icfg g.

(* [valid_cmd] validates the three conditions at the same time,
  because their processes are similar with regard to abstract memory
  calculation.

  - validity of output memories dangling on nodes
  - validity of access *)

Section IntraCfg.

Variable f : pid_t.

Variable cfg : IntraCfg.t.

Definition table_find n s := default Mem.bot (Table.find n s).

Definition valid_cmd (node : IntraNode.t) (cmd : cmd) : bool :=
  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_map in
  let '(o_m', access_f') := run_access Strong g (f, node) cmd i_m in
  if Acc.le_dec access_f' access_f then
    if Mem.opt_le o_m' o_m then true else fail_cmd_mem f node
  else fail_access f node.

Definition valid_cmds :=
  IntraCfg.NodeMap.for_all print2 valid_cmd (IntraCfg.cmds cfg).

Definition valid_intra_edge (from_node to_node : IntraNode.t) : bool :=
  let from_m := table_find (f, from_node) outputof in
  let to_m := table_find (f, to_node) inputof in
  (* Edges from call nodes to return nodes are validated in
  valid_inter_edge. *)
  if IntraCfg.is_call_node cfg from_node then true else
  if Mem.opt_le from_m to_m then true else
    fail_intra_edge f from_node to_node.

Definition valid_intra_edges : bool :=
  let valid_intra_edges' from_node to_nodes :=
    IntraCfg.NodeSet.for_all (valid_intra_edge from_node) to_nodes in
  IntraCfg.NodeMap.for_all print2 valid_intra_edges' (IntraCfg.succ cfg).

Definition valid_cfg := valid_cmds && valid_intra_edges.

End IntraCfg.

Definition valid_cfgs :=
  InterCfg.PidMap.for_all print2 valid_cfg (InterCfg.cfgs icfg).

Definition valid_inter_edge (from_node to_node : InterNode.t) : bool :=
  let from_m := table_find from_node outputof in
  let to_m := table_find to_node inputof in

  if InterCfg.is_call_node icfg from_node then
    let callee := InterNode.get_pid to_node in
    let access := get_all_access callee access_map in
    let from_m := Mem.restrict access from_m in
    if Mem.opt_le from_m to_m then true else
      fail_inter_edge from_node to_node

  else if G.is_exit_node from_node then
    let callee := InterNode.get_pid from_node in
    let access := get_all_access callee access_map in
    match InterCfg.callof icfg to_node with
    | None => fail_inter_edge_no_callof from_node to_node
    | Some call_node =>
      let caller_m := table_find call_node outputof in
      let caller_m := Mem.subtract access caller_m in
      if Mem.opt_le from_m to_m then
        if Mem.opt_le caller_m to_m then true else
          fail_inter_edge call_node to_node
      else fail_inter_edge from_node to_node
    end

  else fail_inter_edge_invalid from_node to_node.

Definition valid_inter_edges :=
  let valid_inter_edges' from_node to_nodes :=
    InterCfg.NodeSet.for_all (valid_inter_edge from_node) to_nodes in
  InterCfg.NodeMap.for_all print2 valid_inter_edges' (InterCfg.succ icfg).

(* Access info validation: if there is a call from f to g, acc(g) <= acc(f). *)

Definition valid_inter_acc (from_node to_node : InterNode.t) : bool :=
  if InterNode.is_entry_node to_node then
    let caller := InterNode.get_pid from_node in
    let callee := InterNode.get_pid to_node in
    let caller_access := get_access caller access_map in
    let callee_access := get_access callee access_map in
    if Acc.le_dec callee_access caller_access then true else
      fail_inter_acc from_node to_node
  else true.

Definition valid_inter_accs :=
  let valid_inter_accs' from_node to_nodes :=
    InterCfg.NodeSet.for_all (valid_inter_acc from_node) to_nodes in
  InterCfg.NodeMap.for_all print2 valid_inter_accs' (InterCfg.succ icfg).

(* Correct densification validation:
all values of accessed locations should be the same. *)

Definition valid_dens_node f (intra_n : IntraNode.t) (cmd : cmd) : bool :=
  let n := (f, intra_n) in
  let orig_m := table_find n orig_inputof in
  let m := table_find n inputof in
  let '(m', acc_n) := run_access Strong g n cmd orig_m in
  let uses_n := Acc.useof acc_n in
  if Mem.eq_wrt uses_n orig_m m then true else fail_dens_inputof n.

Definition valid_dens_cfg f cfg :=
  IntraCfg.NodeMap.for_all print2 (valid_dens_node f) (IntraCfg.cmds cfg).

Definition valid_dens :=
  InterCfg.PidMap.for_all print2 valid_dens_cfg (InterCfg.cfgs icfg).

Definition valid : bool :=
  valid_cfgs && valid_inter_edges && valid_inter_accs && valid_dens.

Local Close Scope bool.

End Validate.

(* Alarm report *)

Module AlarmAccess := Alarm Acc.MAcc AccMem.

Definition check_query_access := AlarmAccess.check_query.

Module AlarmOnly := Alarm MId IdMem.

Definition check_query_only := AlarmOnly.check_query.

Section AlarmReport.

Variable (mode : update_mode) (g : G.t) (inputof : Table.t Mem.t).

Definition check_queries node m (q_pos : query * DPos.t)
: query * DPos.t * list status :=
  let '(q, pos) := q_pos in
  let statuses := check_query_only mode node m q in
  (q, pos, statuses).

Fixpoint query_flatten' (q : query) (pos : DPos.t)
         (statuses : list status)
: list (query * DPos.t * status) :=
  match statuses with
    | nil => nil
    | s :: tl => (q, pos, s) :: query_flatten' q pos tl
  end.

Fixpoint query_flatten (l : list (query * DPos.t * list status))
: list (query * DPos.t * status) :=
  match l with
    | nil => nil
    | (q, pos, statuses) :: tl =>
      query_flatten' q pos statuses ++ query_flatten tl
  end.

Definition collect_alarm_result_node pid node cmd acc
: list (query * DPos.t * status) :=
  let query_list := collect_query cmd in
  let m := table_find (pid, node) inputof in
  let query_status_list := List.map (check_queries (pid, node) m) query_list in
  query_flatten query_status_list ++ acc.

Definition collect_alarm_result_intra pid cfg acc
: list (query * DPos.t * status) :=
  let cmds := IntraCfg.cmds cfg in
  IntraCfg.NodeMap.fold (collect_alarm_result_node pid) cmds acc.

Definition collect_alarm_result : list (query * DPos.t * status) :=
  let icfg := G.icfg g in
  let cfgs := InterCfg.cfgs icfg in
  InterCfg.PidMap.fold collect_alarm_result_intra cfgs nil.

End AlarmReport.

End Make.