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

Require Import Errors Linking BTL_SEtheory BTL_SEimpl.

(** External oracle *)
Axiom scheduler: BTL.function -> BTL.code.

Extract Constant scheduler => "BTLScheduleraux.btl_scheduler".

Definition equiv_input_regs (f1 f2: BTL.function): Prop :=
    (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) 
 /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)).

Lemma equiv_input_regs_union f1 f2:
 equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl.
Proof.
 intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto.
 generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS.
 do 2 autodestruct; intuition; try_simplify_someHyps. 
 intros; exploit EQS; eauto; clear EQS. congruence.
Qed.

Lemma equiv_input_regs_pre f1 f2 tbl or:
 equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or.
Proof.
   intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto.
Qed.

Lemma equiv_input_regs_tr_inputs f1 f2 l oreg rs:
  equiv_input_regs f1 f2 ->
  tr_inputs f1 l oreg rs = tr_inputs f2 l oreg rs.
Proof.
  intros; unfold tr_inputs; erewrite equiv_input_regs_pre; eauto.
Qed.

(* a specification of the verification to do on each function *)
Record match_function (f1 f2: BTL.function): Prop := {
  preserv_fnsig: fn_sig f1 = fn_sig f2;
  preserv_fnparams: fn_params f1 = fn_params f2;
  preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
  preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2;
  preserv_inputs: equiv_input_regs f1 f2;
  symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 ->
                    exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2);
}.

Inductive match_fundef: fundef -> fundef -> Prop :=
  | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
  | match_External ef: match_fundef (External ef) (External ef).

Inductive match_stackframes: stackframe -> stackframe -> Prop :=
  | match_stackframe_intro 
      res f sp pc rs rs' f'
      (EQREGS: forall r, rs # r = rs' # r)
      (TRANSF: match_function f f')
      : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs').

Inductive match_states: state -> state -> Prop :=
  | match_states_intro 
      st f sp pc rs rs' m st' f'
      (EQREGS: forall r, rs # r = rs' # r)
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_function f f')
      : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m)
  | match_states_call
      st st' f f' args m
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_fundef f f')
      : match_states (Callstate st f args m) (Callstate st' f' args m)
  | match_states_return
      st st' v m
      (STACKS: list_forall2 match_stackframes st st')
      : match_states (Returnstate st v m) (Returnstate st' v m)
   .

Lemma match_stack_equiv stk1 stk2:
  list_forall2 match_stackframes stk1 stk2 -> 
  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
  list_forall2 match_stackframes stk1 stk3.
Proof.
  induction 1; intros stk3 EQ; inv EQ; constructor; eauto.
  inv H3; inv H; econstructor; eauto.
  intros; rewrite <- EQUIV; auto.
Qed.

Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
Proof.
  Local Hint Resolve match_stack_equiv: core.
  destruct 1; intros EQ; inv EQ; econstructor; eauto.
  intros; rewrite <- EQUIV; auto.
Qed.

Local Open Scope error_monad_scope.

Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit :=
  match lpc with
  | nil => OK tt
  | pc :: lpc' =>
      match (fn_code f1)!pc, (fn_code f2)!pc with
      | Some ibf1, Some ibf2 =>
          do _ <- simu_check f1 f2 ibf1 ibf2;
          check_symbolic_simu_rec f1 f2 lpc'
      | _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch")
      end
  end.

Definition erase_input_regs f1 f2 :=
  let code := PTree.map (fun pc ibf =>
    let oibf := match (fn_code f2)!pc with
                | None => ibf
                | Some oibf => oibf
                end in
    {| entry:= oibf.(entry); input_regs := ibf.(input_regs); binfo := oibf.(binfo) |}) (fn_code f1) in
  BTL.mkfunction (fn_sig f2) (fn_params f2) (fn_stacksize f2) code (fn_entrypoint f2).

Lemma erase_input_regs_correct f1 f2 f3:
  erase_input_regs f1 f2 = f3 ->
  equiv_input_regs f1 f3.
Proof.
  unfold erase_input_regs; simpl; intros.
  unfold equiv_input_regs; intuition auto.
  - subst; simpl. rewrite PTree.gmap, H0; simpl; auto.
  - subst; simpl in H0. rewrite PTree.gmap in H0.
    destruct ((fn_code f1)!pc) eqn:EQF; simpl in H0; inv H0; auto.
  - subst; simpl in H1. rewrite PTree.gmap in H1.
    rewrite H0 in H1; simpl in H1; inv H1; simpl; auto.
Qed.
Global Opaque erase_input_regs.

Definition check_symbolic_simu (f1 f2: BTL.function): res unit :=
  check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))).

Definition transf_function (f: BTL.function) :=
  let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in
  let tf' := erase_input_regs f tf in
  do _ <- check_symbolic_simu f tf';
  OK tf'.

Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x,
  check_symbolic_simu_rec f1 f2 lpc = OK x ->
  forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc ->
       exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
Proof.
  induction lpc; simpl; intros f1 f2 x X pc ib1 (PC & HIN); try contradiction.
  destruct HIN; subst.
  - rewrite PC in X; destruct ((fn_code f2)!pc); monadInv X.
    exists i; split; auto. destruct x0. eapply simu_check_correct; eauto.
  - destruct ((fn_code f1)!a), ((fn_code f2)!a); monadInv X.
    eapply IHlpc; eauto.
Qed.

Lemma check_symbolic_simu_correct x f1 f2:
  check_symbolic_simu f1 f2 = OK x ->
  forall pc ib1, (fn_code f1)!pc = Some ib1 ->
       exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
Proof.
  unfold check_symbolic_simu; intros X pc ib1 PC.
  eapply check_symbolic_simu_rec_correct; intuition eauto.
  apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto.
Qed.

Lemma check_symbolic_simu_input_equiv x f1 f2:
  transf_function f1 = OK f2 ->
  check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2.
Proof.
  unfold transf_function; intros TRANSF X; monadInv TRANSF.
  exploit erase_input_regs_correct; eauto.
Qed.

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

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