Library mcertikos.layerlib.AsmImplTactic

Require Import Coqlib.
Require Import Asm.
Require Import Values.
Require Import Integers.
Require Import CommonTactic.
Require Import AST.
Require Import Smallstep.
Require Import liblayers.compat.CompatLayers.
Require Import LAsm.
Require Import FunctionalExtensionality.
Require Import AsmImplLemma.
Require Import LRegSet.
Require Import Conventions.
Require Import AuxLemma.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.




 Ltac store_split:=
   repeat match goal with
            | H: _ ∧ _ = _ |- _ ⇒ destruct H as [H ?]; subst
          end.

 Ltac one_step_forward´:=
   match goal with
     | |- star _ _ _ _ _ ⇒
       eapply star_left; try reflexivity
     | |- plus _ _ _ _ _ ⇒
       econstructor
   end;
   match goal with
     | |- step _ _ _ _ ⇒
       econstructor; try eassumption;
       try reflexivity
     | _ ⇒ idtac
   end; simpl.

 Ltac one_step_forward n:=
   match goal with
     | |- star _ _ _ _ _ ⇒
       eapply star_left; try reflexivity
     | |- plus _ _ _ _ _ ⇒
       econstructor
   end;
   match goal with
     | |- step _ _ _ _ ⇒
       econstructor; try eassumption;
       match goal with
         | H: _ PC = Vptr ?b _ |- _ = Vptr ?b _ ⇒
           try reflexivity
         | |- find_instr ?num _ = _ ⇒
           replace num with n;
             [pc_add_simpl; simpl| try reflexivity]
         | _ ⇒ simpl
       end
     | _ ⇒ idtac
   end.

 Lemma val_add_vptr:
   ∀ n b ofs,
     Int.repr n = Int.add ofs Int.one →
     Val.add (Vptr b ofs) Vone = Vptr b (Int.repr n).
 Proof.
   simpl. intros.
   congruence.
 Qed.

 Ltac Lregset_simpl_tac:=
   repeat match goal with
            | |- context [undef_regs (map _ destroyed_at_call) (Lregset_fold _)] ⇒
              rewrite Lregset_fold_destroyed
            | |- context[(Lregset_fold _) _] ⇒
              rewrite Lregset_fold_get; simpl
            | |- context [nextinstr (Lregset_fold _)] ⇒
              rewrite Lregset_fold_nextinstr
            | |- context [nextinstr_nf (Lregset_fold _)] ⇒
              rewrite Lregset_fold_nextinstr_nf
            | |- context[(Lregset_fold _) # RA <- _ ] ⇒
              rewrite Lregset_fold_ra
            | |- context[(Lregset_fold _) # PC <- _ ] ⇒
              rewrite Lregset_fold_pc
            | |- context[(Lregset_fold _) # (IR ?i) <- _ ] ⇒
              match i with
                | EAX ⇒ rewrite Lregset_fold_eax
                | EDX ⇒ rewrite Lregset_fold_edx
                | ESP ⇒ rewrite Lregset_fold_esp
                | ECX ⇒ rewrite Lregset_fold_ecx
                | EDI ⇒ rewrite Lregset_fold_edi
                | ESI ⇒ rewrite Lregset_fold_esi
                | EBX ⇒ rewrite Lregset_fold_ebx
                | EBP ⇒ rewrite Lregset_fold_ebp
              end
            | |- context[(Lregset_fold _) # (CR ?i) <- _ ] ⇒
              match i with
                | ZF ⇒ rewrite Lregset_fold_zf
                | CF ⇒ rewrite Lregset_fold_cf
                | PF ⇒ rewrite Lregset_fold_pf
                | SF ⇒ rewrite Lregset_fold_sf
                | OF ⇒ rewrite Lregset_fold_of
              end
          end.

 Ltac Lregset_simpl_tac´ n :=
   Lregset_simpl_tac;
   match goal with
     | |- context [Val.add (Vptr ?b ?ofs) Vone] ⇒
       rewrite (val_add_vptr n b ofs); [| try reflexivity]
   end.

 Lemma reg_false:
   ∀ reg: preg,
     reg ≠ PC →
     reg ≠ EBP →
     reg ≠ EBX →
     reg ≠ ESI →
     reg ≠ EDI →
     reg ≠ ESP →
     reg ≠ RA →
     reg ≠ EAX →
     reg ≠ ECX →
     reg ≠ EDX →
     reg ≠ OF →
     reg ≠ SF →
     reg ≠ PF →
     reg ≠ CF →
     reg ≠ ZF →
     reg ≠ XMM7 →
     reg ≠ XMM6 →
     reg ≠ XMM5 →
     reg ≠ XMM4 →
     reg ≠ XMM3 →
     reg ≠ XMM2 →
     reg ≠ XMM1 →
     reg ≠ XMM0 →
     reg ≠ ST0 →
     False.
 Proof.
   intros.
   destruct reg; try congruence.
   destruct i; try congruence.
   destruct f; try congruence.
   destruct c; try congruence.
 Qed.

 Ltac link_nextblock_asm :=
   repeat match goal with
            | Hstore: Mem.store _ _ _ _ _ = Some ?fm |- context[Mem.nextblock ?fm] ⇒
              rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore)
          end; try reflexivity.

 Ltac link_inject_neutral_asm :=
   repeat match goal with
            | Hstore: Mem.store _ _ _ _ _ = Some ?fm |- Mem.inject_neutral _ ?fm ⇒
              eapply Mem.store_inject_neutral; eauto 1
          end.

 Lemma inv_reg_le:
   ∀ (rs: regset) a b,
     (∀ r,
        val_inject (Mem.flat_inj a)
                   (rs r) (rs r)) →
     (a ≤ b)%positive →
     (∀ r,
        val_inject (Mem.flat_inj b)
                   (rs r) (rs r)).
 Proof.
   intros. eapply val_inject_incr; [|eauto].
   eapply flat_inj_inject_incr; assumption.
 Qed.