Module Conventions1C

Require Import CoqlibC Decidableplus.
Require Import ASTC Machregs Locations.
newly added *
Require Export Conventions1.

Set Implicit Arguments.



Lemma loc_arguments_length_aux: forall tys ir fr ofs,
    <<LEN: length (loc_arguments_64 tys ir fr ofs) = length tys>>.
Proof.
i. ginduction tys; ii; ss. des_ifs; s; rewrite IHtys; ss. Qed.

Lemma loc_arguments_length: forall sg,
    <<LEN: length (loc_arguments sg) = length (sig_args sg)>>.
Proof.
  destruct sg; ss. unfold loc_arguments. des_ifs. ss. rewrite loc_arguments_length_aux. ss.
Qed.

Local Opaque Z.add Z.mul Z.sub Z.div.
Local Opaque list_nth_z.

Let size_arguments_loc_arguments_aux: forall
    tys ofs x y z
    (IN: z <= ofs < size_arguments_64 tys x y z),
    exists base ty, (<<IN: In (S Outgoing base ty) (regs_of_rpairs (loc_arguments_64 tys x y z))>>)
               /\ (<<RANGE: base <= ofs < base + (Memdata.size_chunk (chunk_of_type ty))>>).
Proof.
  i. ginduction tys; ii; ss; try xomega.
  destruct a; ss; des_ifs; ss; try (exploit IHtys; eauto; []; i; des; []); try (by esplits; eauto);
    des; destruct (classic (z + 2 <= ofs)); try (exploit IHtys; eauto; []; i; des; []); try (by esplits; eauto); esplits; eauto; ss; lia.
Qed.

Lemma size_arguments_loc_arguments
      sg ofs
      (IN: 0 <= ofs < size_arguments sg):
    exists base ty, (<<IN: In (S Outgoing base ty) (regs_of_rpairs (loc_arguments sg))>>)
               /\ (<<RANGE: base <= ofs < base + (Memdata.size_chunk (chunk_of_type ty))>>).
Proof.
  destruct sg; ss. unfold size_arguments, loc_arguments in *. ss. des_ifs. clear_tac.
  eapply size_arguments_loc_arguments_aux; eauto.
Qed.

Lemma loc_args_callee_save_disjoint sg mr
      (EXT: In (R mr) (regs_of_rpairs (loc_arguments sg))):
    ~ Conventions1.is_callee_save mr.
Proof.
  exploit in_regs_of_rpairs_inv; eauto. i. des.
  exploit loc_arguments_acceptable; eauto. i.
  unfold forall_rpair, loc_argument_acceptable in *.
  des_ifs; ss; des; clarify; eauto.
Qed.