Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Duplicate RTL Op OptionMonad.
Require Export BTL.

Matching BTL and RTL code We define a single verifier able to prove a bisimulation between BTL and RTL code. Hence, in a sense, our verifier imitates the approach of Duplicate, where dupmap maps the BTL nodes to the RTL nodes. The match_function definition gives a "relational" specification of the verifier...

Require Import Errors.

Inductive match_synthetic_node (dupmap: PTree.t node) (cfg: BTL.code): bool -> node -> node -> node -> Prop :=
  | mn_direct pcB pcR indirect:
      dupmap ! pcB = Some pcR ->
      match_synthetic_node dupmap cfg indirect pcB pcB pcR
  | mn_indirect pcX pcB pcR ibf iinfo:
      dupmap ! pcX = None ->
      cfg ! pcX = Some ibf ->
      ibf.(entry) = BF (Bgoto pcB) iinfo ->
      dupmap ! pcB = Some pcR ->
      match_synthetic_node dupmap cfg true pcX pcB pcR
  .
Global Hint Constructors match_synthetic_node: core.

Definition match_nodes dupmap cfg indirect pcX pcR :=
  exists pcB, match_synthetic_node dupmap cfg indirect pcX pcB pcR.

Inductive match_final_inst (dupmap: PTree.t node) (cfg: BTL.code) (indirect: bool):
  final -> instruction -> Prop :=
  | mfi_return or: match_final_inst dupmap cfg indirect (Breturn or) (Ireturn or)
  | mfi_call pcX pcR s ri lr r:
      match_nodes dupmap cfg indirect pcX pcR ->
      match_final_inst dupmap cfg indirect (Bcall s ri lr r pcX) (Icall s ri lr r pcR)
  | mfi_tailcall s ri lr:
      match_final_inst dupmap cfg indirect (Btailcall s ri lr) (Itailcall s ri lr)
  | mfi_builtin pcX pcR ef la br:
      match_nodes dupmap cfg indirect pcX pcR ->
      match_final_inst dupmap cfg indirect (Bbuiltin ef la br pcX) (Ibuiltin ef la br pcR)
  | mfi_jumptable ln ln' r:
      list_forall2 (fun pcX pcR => match_nodes dupmap cfg indirect pcX pcR) ln ln' ->
      match_final_inst dupmap cfg indirect (Bjumptable r ln) (Ijumptable r ln')
.

Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop :=
  | ijo_None_left o: is_join_opt None o o
  | ijo_None_right o: is_join_opt o None o
  | ijo_Some x: is_join_opt (Some x) (Some x) (Some x)
  .

Inductive match_iblock (dupmap: PTree.t node) (cfg: BTL.code) (cfg': RTL.code) (indirect: bool):
  bool -> node -> iblock -> (option node) -> Prop :=
  | mib_BF isfst fi pc i iinfo:
      cfg'!pc = Some i ->
      match_final_inst dupmap cfg indirect fi i ->
      match_iblock dupmap cfg cfg' indirect isfst pc (BF fi iinfo) None
  | mib_nop_on_rtl isfst pc pc' iinfo:
      cfg'!pc = Some (Inop pc') ->
      match_iblock dupmap cfg cfg' indirect isfst pc (Bnop (Some iinfo)) (Some pc')
  | mib_nop_skip pc:
      match_iblock dupmap cfg cfg' indirect false pc (Bnop None) (Some pc)
  | mib_op isfst pc pc' op lr r iinfo:
      cfg'!pc = Some (Iop op lr r pc') ->
      match_iblock dupmap cfg cfg' indirect isfst pc (Bop op lr r iinfo) (Some pc')
  | mib_load isfst pc pc' trap m a lr aa r iinfo:
      cfg'!pc = Some (Iload trap m a lr r pc') ->
      match_iblock dupmap cfg cfg' indirect isfst pc (Bload trap m a lr aa r iinfo) (Some pc')
  | mib_store isfst pc pc' m a lr aa r iinfo:
      cfg'!pc = Some (Istore m a lr r pc') ->
      match_iblock dupmap cfg cfg' indirect isfst pc (Bstore m a lr aa r iinfo) (Some pc')
  | mib_exit pc pc' iinfo:
      match_nodes dupmap cfg indirect pc pc' ->
      match_iblock dupmap cfg cfg' indirect false pc' (BF (Bgoto pc) iinfo) None
  | mib_seq_Some isfst b1 b2 pc1 pc2 opc:
      match_iblock dupmap cfg cfg' indirect isfst pc1 b1 (Some pc2) ->
      match_iblock dupmap cfg cfg' indirect false pc2 b2 opc ->
      match_iblock dupmap cfg cfg' indirect isfst pc1 (Bseq b1 b2) opc
  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo:
      cfg'!pc = Some (Icond c lr pcso pcnot i) ->
      match_iblock dupmap cfg cfg' indirect false pcso bso opc1 ->
      match_iblock dupmap cfg cfg' indirect false pcnot bnot opc2 ->
      is_join_opt opc1 opc2 opc ->
      match_iblock dupmap cfg cfg' indirect isfst pc (Bcond c lr bso bnot iinfo) opc
  .

Definition match_cfg dupmap (cfg: BTL.code) (cfg':RTL.code) (indirect: bool): Prop :=
    forall pc pc', dupmap!pc = Some pc' ->
    exists ib,
      cfg!pc = Some ib /\ match_iblock dupmap cfg cfg' indirect true pc' ib.(entry) None.

Record match_function dupmap f f' indirect: Prop := {
  dupmap_correct: match_cfg dupmap (BTL.fn_code f) (RTL.fn_code f') indirect;
  dupmap_entrypoint: match_nodes dupmap (BTL.fn_code f) indirect (fn_entrypoint f) (RTL.fn_entrypoint f');
  preserv_fnsig: fn_sig f = RTL.fn_sig f';
  preserv_fnparams: fn_params f = RTL.fn_params f';
  preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
}.

Shared verifier between RTL -> BTL and BTL -> RTL

Local Open Scope error_monad_scope.

Definition verify_node_eq n n' :=
  match (Pos.compare n n') with Eq => OK tt | _ => Error(msg "BTL.verify_node_eq: comparison failed") end.

Definition verify_indirection dupmap cfg n n' :=
  match cfg!n with
  | None => Error(msg "BTL.verify_indirection: missing synthetic node")
  | Some ibf =>
      match ibf.(entry) with
      | BF (Bgoto pc1) _ =>
          match dupmap!pc1 with
          | None => Error(msg "BTL.verify_indirection: invalid map")
          | Some revn => verify_node_eq n' revn
          end
      | _ => Error(msg "BTL.verify_indirection: invalid synthetic node")
      end
  end.

Definition verify_is_copy dupmap cfg (indirect: bool) n n' :=
  match dupmap!n with
  | None =>
      if indirect then verify_indirection dupmap cfg n n'
      else Error(msg "BTL.verify_is_copy: invalid map")
  | Some revn => verify_node_eq n' revn
  end.

Fixpoint verify_is_copy_list dupmap cfg indirect ln ln' :=
  match ln with
  | n::ln => match ln' with
             | n'::ln' => do _ <- verify_is_copy dupmap cfg indirect n n';
                          verify_is_copy_list dupmap cfg indirect ln ln'
             | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end
  | nil => match ln' with
          | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'")
          | nil => OK tt end
  end.

Lemma verify_is_copy_correct dupmap cfg indirect pc pc' tt:
  verify_is_copy dupmap cfg indirect pc pc' = OK tt ->
  match_nodes dupmap cfg indirect pc pc'.
Local Hint Resolve verify_is_copy_correct: core.

Lemma verify_is_copy_list_correct dupmap cfg indirect ln: forall ln' tt,
  verify_is_copy_list dupmap cfg indirect ln ln' = OK tt ->
  list_forall2 (fun pc pc' => match_nodes dupmap cfg indirect pc pc') ln ln'.

Fixpoint verify_block (dupmap: PTree.t node) (cfg: code) (cfg': RTL.code)
  indirect isfst pc ib : res (option node) :=
  match ib with
  | BF fi _ =>
      match fi with
      | Bgoto pc1 =>
          do u <- verify_is_copy dupmap cfg indirect pc1 pc;
          if negb isfst then
            OK None
          else Error (msg "BTL.verify_block: isfst is true Bgoto")
      | Breturn or =>
          match cfg'!pc with
          | Some (Ireturn or') =>
              if option_eq Pos.eq_dec or or' then OK None
              else Error (msg "BTL.verify_block: different opt reg in Breturn")
          | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn")
          end
      | Bcall s ri lr r pc1 =>
          match cfg'!pc with
          | Some (Icall s' ri' lr' r' pc2) =>
              do u <- verify_is_copy dupmap cfg indirect pc1 pc2;
              if (signature_eq s s') then
                if (product_eq Pos.eq_dec ident_eq ri ri') then
                  if (list_eq_dec Pos.eq_dec lr lr') then
                    if (Pos.eq_dec r r') then OK None
                    else Error (msg "BTL.verify_block: different r r' in Bcall")
                  else Error (msg "BTL.verify_block: different lr in Bcall")
                else Error (msg "BTL.verify_block: different ri in Bcall")
              else Error (msg "BTL.verify_block: different signatures in Bcall")
          | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall")
          end
      | Btailcall s ri lr =>
          match cfg'!pc with
          | Some (Itailcall s' ri' lr') =>
              if (signature_eq s s') then
                if (product_eq Pos.eq_dec ident_eq ri ri') then
                  if (list_eq_dec Pos.eq_dec lr lr') then OK None
                  else Error (msg "BTL.verify_block: different lr in Btailcall")
                else Error (msg "BTL.verify_block: different ri in Btailcall")
              else Error (msg "BTL.verify_block: different signatures in Btailcall")
          | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall")
          end
      | Bbuiltin ef la br pc1 =>
          match cfg'!pc with
          | Some (Ibuiltin ef' la' br' pc2) =>
              do u <- verify_is_copy dupmap cfg indirect pc1 pc2;
              if (external_function_eq ef ef') then
                if (list_eq_dec builtin_arg_eq_pos la la') then
                  if (builtin_res_eq_pos br br') then OK None
                  else Error (msg "BTL.verify_block: different brr in Bbuiltin")
                else Error (msg "BTL.verify_block: different lbar in Bbuiltin")
              else Error (msg "BTL.verify_block: different ef in Bbuiltin")
          | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin")
          end
      | Bjumptable r ln =>
          match cfg'!pc with
          | Some (Ijumptable r' ln') =>
              do u <- verify_is_copy_list dupmap cfg indirect ln ln';
              if (Pos.eq_dec r r') then OK None
              else Error (msg "BTL.verify_block: different r in Bjumptable")
          | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable")
          end
      end
  | Bnop oiinfo =>
      match oiinfo with
      | Some _ =>
          match cfg'!pc with
          | Some (Inop pc') => OK (Some pc')
          | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop")
          end
      | None =>
          if negb isfst then OK (Some pc)
          else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)")
      end
  | Bop op lr r _ =>
      match cfg'!pc with
      | Some (Iop op' lr' r' pc') =>
          if (eq_operation op op') then
            if (list_eq_dec Pos.eq_dec lr lr') then
              if (Pos.eq_dec r r') then
                OK (Some pc')
              else Error (msg "BTL.verify_block: different r in Bop")
            else Error (msg "BTL.verify_block: different lr in Bop")
          else Error (msg "BTL.verify_block: different operations in Bop")
      | _ => Error (msg "BTL.verify_block: incorrect cfg Bop")
      end
  | Bload tm m a lr _ r _ =>
      match cfg'!pc with
      | Some (Iload tm' m' a' lr' r' pc') =>
          if (trapping_mode_eq tm tm') then
            if (chunk_eq m m') then
              if (eq_addressing a a') then
                if (list_eq_dec Pos.eq_dec lr lr') then
                  if (Pos.eq_dec r r') then
                    OK (Some pc')
                  else Error (msg "BTL.verify_block: different r in Bload")
                else Error (msg "BTL.verify_block: different lr in Bload")
              else Error (msg "BTL.verify_block: different addressing in Bload")
            else Error (msg "BTL.verify_block: different chunk in Bload")
          else Error (msg "BTL.verify_block: different trapping_mode in Bload")
      | _ => Error (msg "BTL.verify_block: incorrect cfg Bload")
      end
  | Bstore m a lr _ r _ =>
      match cfg'!pc with
      | Some (Istore m' a' lr' r' pc') =>
          if (chunk_eq m m') then
            if (eq_addressing a a') then
              if (list_eq_dec Pos.eq_dec lr lr') then
                if (Pos.eq_dec r r') then OK (Some pc')
                else Error (msg "BTL.verify_block: different r in Bstore")
              else Error (msg "BTL.verify_block: different lr in Bstore")
            else Error (msg "BTL.verify_block: different addressing in Bstore")
          else Error (msg "BTL.verify_block: different chunk in Bstore")
      | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore")
      end
  | Bseq b1 b2 =>
      do opc <- verify_block dupmap cfg cfg' indirect isfst pc b1;
      match opc with
      | Some pc' =>
          verify_block dupmap cfg cfg' indirect false pc' b2
      | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)")
      end
  | Bcond c lr bso bnot _ =>
      match cfg'!pc with
      | Some (Icond c' lr' pcso pcnot i') =>
          if (list_eq_dec Pos.eq_dec lr lr') then
            if (eq_condition c c') then
              do opc1 <- verify_block dupmap cfg cfg' indirect false pcso bso;
              do opc2 <- verify_block dupmap cfg cfg' indirect false pcnot bnot;
              match opc1, opc2 with
              | None, o => OK o
              | o, None => OK o
              | Some x, Some x' =>
                  if Pos.eq_dec x x' then OK (Some x)
                  else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond")
              end
            else Error (msg "BTL.verify_block: incompatible conditions in Bcond")
          else Error (msg "BTL.verify_block: different lr in Bcond")
      | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond")
      end
  end.

Lemma verify_block_correct dupmap cfg cfg' indirect ib: forall pc isfst fin,
   verify_block dupmap cfg cfg' indirect isfst pc ib = (OK fin) ->
   match_iblock dupmap cfg cfg' indirect isfst pc ib fin.
Local Hint Resolve verify_block_correct: core.

Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) indirect l: res unit :=
  match l with
  | nil => OK tt
  | (pc, pc')::l =>
    match cfg!pc with
    | Some ib => do o <- verify_block dupmap cfg cfg' indirect true pc' ib.(entry);
                 match o with
                 | None => verify_blocks dupmap cfg cfg' indirect l
                 | _ => Error(msg "BTL.verify_blocks.end")
                 end
    | _ => Error(msg "BTL.verify_blocks.entry")
    end
  end.

Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code) indirect: res unit :=
  verify_blocks dupmap cfg cfg' indirect (PTree.elements dupmap).

Lemma verify_cfg_correct dupmap cfg cfg' indirect tt:
  verify_cfg dupmap cfg cfg' indirect = OK tt ->
  match_cfg dupmap cfg cfg' indirect.

Definition verify_function dupmap f f' indirect: res unit :=
  do _ <- verify_is_copy dupmap (fn_code f) indirect (fn_entrypoint f) (RTL.fn_entrypoint f');
  verify_cfg dupmap (fn_code f) (RTL.fn_code f') indirect.

Lemma verify_function_correct dupmap f f' indirect tt:
  verify_function dupmap f f' indirect = OK tt ->
  fn_sig f = RTL.fn_sig f' ->
  fn_params f = RTL.fn_params f' ->
  fn_stacksize f = RTL.fn_stacksize f' ->
  match_function dupmap f f' indirect.