Require Import AST RTL Maps Globalenvs.
Require Import Coqlib Errors Op.

Lemma product_eq {A B: Type} :
  (forall (a b: A), {a=b} + {a<>b}) ->
  (forall (c d: B), {c=d} + {c<>d}) ->
  forall (x y: A+B), {x=y} + {x<>y}.

Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}.
Global Opaque builtin_arg_eq_pos.

Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
Global Opaque builtin_res_eq_pos.

Module Type DuplicateOracle.

  Parameter duplicate_aux: function -> code * node * (PTree.t node).

End DuplicateOracle.

Module Duplicate (D: DuplicateOracle).

Export D.

Definition duplicate_aux := duplicate_aux.


Local Open Scope error_monad_scope.
Local Open Scope positive_scope.

Verification of node duplications

Definition verify_is_copy dupmap n n' :=
  match dupmap!n' with
  | None => Error(msg "verify_is_copy None")
  | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
  end.

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

Definition verify_mapping_entrypoint dupmap (f f': function): res unit :=
  verify_is_copy dupmap (fn_entrypoint f) (fn_entrypoint f').

Definition verify_match_inst dupmap inst tinst :=
  match inst with
  | Inop n => match tinst with Inop n' => verify_is_copy dupmap n n' | _ => Error(msg "verify_match_inst Inop") end

  | Iop op lr r n => match tinst with
      Iop op' lr' r' n' =>
          do u <- verify_is_copy dupmap n n';
          if (eq_operation op op') then
            if (list_eq_dec Pos.eq_dec lr lr') then
              if (Pos.eq_dec r r') then
                OK tt
              else Error (msg "Different r in Iop")
            else Error (msg "Different lr in Iop")
          else Error(msg "Different operations in Iop")
      | _ => Error(msg "verify_match_inst Inop") end

  | Iload tm m a lr r n => match tinst with
      | Iload tm' m' a' lr' r' n' =>
          do u <- verify_is_copy dupmap n n';
          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 tt
                  else Error (msg "Different r in Iload")
                else Error (msg "Different lr in Iload")
              else Error (msg "Different addressing in Iload")
            else Error (msg "Different mchunk in Iload")
          else Error (msg "Different trapping_mode in Iload")
      | _ => Error (msg "verify_match_inst Iload") end

  | Istore m a lr r n => match tinst with
      | Istore m' a' lr' r' n' =>
          do u <- verify_is_copy dupmap n n';
          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 tt
                else Error (msg "Different r in Istore")
              else Error (msg "Different lr in Istore")
            else Error (msg "Different addressing in Istore")
          else Error (msg "Different mchunk in Istore")
      | _ => Error (msg "verify_match_inst Istore") end

  | Icall s ri lr r n => match tinst with
      | Icall s' ri' lr' r' n' =>
          do u <- verify_is_copy dupmap n n';
          if (signature_eq s s') then
            if (product_eq Pos.eq_dec QualIdent.eq ri ri') then
              if (list_eq_dec Pos.eq_dec lr lr') then
                if (Pos.eq_dec r r') then OK tt
                else Error (msg "Different r r' in Icall")
              else Error (msg "Different lr in Icall")
            else Error (msg "Different ri in Icall")
          else Error (msg "Different signatures in Icall")
      | _ => Error (msg "verify_match_inst Icall") end

  | Itailcall s ri lr => match tinst with
      | Itailcall s' ri' lr' =>
          if (signature_eq s s') then
            if (product_eq Pos.eq_dec QualIdent.eq ri ri') then
              if (list_eq_dec Pos.eq_dec lr lr') then OK tt
              else Error (msg "Different lr in Itailcall")
            else Error (msg "Different ri in Itailcall")
          else Error (msg "Different signatures in Itailcall")
      | _ => Error (msg "verify_match_inst Itailcall") end

  | Ibuiltin ef lbar brr n => match tinst with
      | Ibuiltin ef' lbar' brr' n' =>
          do u <- verify_is_copy dupmap n n';
          if (external_function_eq ef ef') then
            if (list_eq_dec builtin_arg_eq_pos lbar lbar') then
              if (builtin_res_eq_pos brr brr') then OK tt
              else Error (msg "Different brr in Ibuiltin")
            else Error (msg "Different lbar in Ibuiltin")
          else Error (msg "Different ef in Ibuiltin")
      | _ => Error (msg "verify_match_inst Ibuiltin") end

  | Icond cond lr n1 n2 i => match tinst with
      | Icond cond' lr' n1' n2' i' =>
          if (list_eq_dec Pos.eq_dec lr lr') then
            if (eq_condition cond cond') then
              do u1 <- verify_is_copy dupmap n1 n1';
              verify_is_copy dupmap n2 n2'
            else if (eq_condition (negate_condition cond) cond') then
              do u1 <- verify_is_copy dupmap n1 n2';
              verify_is_copy dupmap n2 n1'
            else Error (msg "Incompatible conditions in Icond")
          else Error (msg "Different lr in Icond")
      | _ => Error (msg "verify_match_inst Icond") end

  | Ijumptable r ln => match tinst with
      | Ijumptable r' ln' =>
          do u <- verify_is_copy_list dupmap ln ln';
          if (Pos.eq_dec r r') then OK tt
          else Error (msg "Different r in Ijumptable")
      | _ => Error (msg "verify_match_inst Ijumptable") end

  | Ireturn or => match tinst with
      | Ireturn or' =>
          if (option_eq Pos.eq_dec or or') then OK tt
          else Error (msg "Different or in Ireturn")
      | _ => Error (msg "verify_match_inst Ireturn") end

  | Iassert cond lr n1 => match tinst with
      | Iassert cond' lr' n1' =>
          if (list_eq_dec eq_assert_arg lr lr') then
            if (eq_condition cond cond') then
              verify_is_copy dupmap n1 n1'
            else Error (msg "Incompatible conditions in Icond")
          else Error (msg "Different lr in Icond")
      | _ => Error (msg "verify_match_inst Icond") end
  end.

Definition verify_mapping_mn dupmap f f' (m: positive*positive) :=
  let (tn, n) := m in
  match (fn_code f)!n with
  | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n")
  | Some inst => match (fn_code f')!tn with
                 | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn")
                 | Some tinst => verify_match_inst dupmap inst tinst
                 end
  end.

Fixpoint verify_mapping_mn_rec dupmap f f' lm :=
  match lm with
  | nil => OK tt
  | m :: lm => do u <- verify_mapping_mn dupmap f f' m;
               verify_mapping_mn_rec dupmap f f' lm
  end.

Definition verify_mapping_match_nodes dupmap (f f': function): res unit :=
  verify_mapping_mn_rec dupmap f f' (PTree.elements dupmap).

Definition verify_mapping dupmap (f f': function) : res unit :=
  do u <- verify_mapping_entrypoint dupmap f f';
  verify_mapping_match_nodes dupmap f f'.

Entry points

Definition transf_function (f: function) : res function :=
  let (tcte, dupmap) := duplicate_aux f in
  let (tc, te) := tcte in
  let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te (fn_attr f) in
  do u <- verify_mapping dupmap f f';
  OK f'.

Definition transf_fundef (f: fundef) : res fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: program) : res program :=
  transform_partial_program transf_fundef p.

End Duplicate.