Require Import OrderedType.
Require Import CoqlibC.
Require Import Maps.
Require Import Ordered.
Require Import AST.
Require Import Values.
Require Export Machregs.
newly added *
Require Export Locations.
Require Import Conventions Integers Memory.
Require Import List.
Set Implicit Arguments.
Lemma Loc_not_in_notin_R
r locs
(
NOTIN: ~
In (
R r)
locs):
<<
NOTIN:
Loc.notin (
R r)
locs>>.
Proof.
red. ginduction locs; ii; ss. esplits; eauto. destruct a; ss. ii; clarify. eauto. Qed.
Lemma typealign_divide_8:
forall ty,
<<
DIV: (4 *
typealign ty | 8)>>.
Proof.
Definition locset :=
Locmap.t.
Local Opaque Z.mul Z.add.
Local Opaque list_nth_z.
Definition is_one A (
ap:
rpair A):
bool :=
match ap with
|
One _ =>
true
|
Twolong _ _ =>
false
end.
Lemma loc_arguments_one:
forall sg lp (
IN:
In lp (
loc_arguments sg)), <<
ONE:
is_one lp>>.
Proof.
destruct sg;
ss.
unfold loc_arguments in *.
ss.
des_ifs.
clear_tac.
generalize 0
at 1
as ir.
generalize 0
at 1
as fr.
generalize 0
at 1
as ofs.
ginduction sig_args;
ii;
ss.
-
des_ifs;
repeat (
des;
ss;
clarify);
eapply IHsig_args;
eauto.
Qed.
Lemma loc_result_one:
forall sg,
exists mr_res, <<
ONE:
loc_result sg =
One mr_res>>.
Proof.
i. compute. des_ifs; eauto. Qed.
Lemma Loc_cons_right_disjoint
xs0 xs1 x
(
DISJ:
Loc.disjoint xs0 xs1)
(
NOTIN:
Loc.notin x xs0):
<<
DISJ:
Loc.disjoint xs0 (
x ::
xs1)>>.
Proof.
Lemma disjoint_concat l1 l2 x:
Loc.disjoint (
l1++[
x])
l2 ->
Loc.disjoint l1 l2.
Proof.
Lemma norepet_nth_notin l n m
(
NOREPET:
Loc.norepet l)
(
NTH:
list_nth_z l (
Z.of_nat n) =
Some m):
Loc.notin m (
firstn n l).
Proof.
Lemma disjoint_app_inv:
forall l1 l2 l3,
Loc.disjoint l1 (
l2 ++
l3) ->
Loc.disjoint l1 l2 /\
Loc.disjoint l1 l3.
Proof.
i.
ginduction l2;
ii;
ss.
{
esplits;
et.
ss. }
split.
-
ii.
ss.
eapply H;
et.
ss.
des;
clarify;
et.
right.
rewrite in_app_iff.
et.
-
apply Loc.disjoint_cons_right in H.
eapply IHl2;
et.
Qed.
Lemma notin_regs_of_rpairs
ofs tys ir fr ofs2 T
(
LT:
ofs + 2 <=
ofs2):
Loc.notin (
S Outgoing ofs T) (
regs_of_rpairs (
loc_arguments_64 tys ir fr ofs2)).
Proof.
ginduction tys; ss; i.
des_ifs; destruct T; econs; ss; et; try nia; eapply IHtys; try nia.
Qed.
Lemma loc_arguments_norepet_aux
tys (
ir fr ofs:
Z)
locs
(
LOCS: (
regs_of_rpairs (
loc_arguments_64 tys ir fr ofs)) =
locs):
(<<
NOREP:
Loc.norepet locs>>)
/\ (<<
NOTINIR:
Loc.disjoint (
map R (
List.firstn ir.(
Z.to_nat)
int_param_regs))
locs>>)
/\ (<<
NOTINFR:
Loc.disjoint (
map R (
List.firstn fr.(
Z.to_nat)
float_param_regs))
locs>>).
Proof.
Lemma loc_arguments_norepet:
forall sg,
Loc.norepet (
regs_of_rpairs (
loc_arguments sg)).
Proof.
Lemma loc_norepet_app l0 l1
(
NOREPEAT:
Loc.norepet (
l0 ++
l1)):
Loc.norepet l1.
Proof.
induction l0; ss. inv NOREPEAT. eauto. Qed.
Lemma loc_notin_not_in mr locs:
Loc.notin (
R mr)
locs <-> ~
In (
R mr)
locs.
Proof.
induction locs;
ss.
split;
ii;
des;
des_ifs.
-
eapply IHlocs;
eauto.
-
eapply IHlocs;
eauto.
-
apply not_or_and in H.
des.
split;
auto.
ii.
clarify.
-
apply not_or_and in H.
des.
split;
auto.
Qed.
Lemma in_one_in_rpair l (
r:
loc)
(
IN:
In (
One r)
l):
In r (
regs_of_rpairs l).
Proof.
induction l;
ss;
des;
clarify.
-
destruct r;
ss;
eauto.
-
eapply in_or_app;
eauto.
Qed.
Lemma loc_arguments_ofs_bounded
sg lo
(
SZ: 0 <=
lo /\
lo + 4 *
size_arguments sg <=
Ptrofs.max_unsigned)
ofs ty
(
IN:
In (
One (
S Outgoing ofs ty)) (
loc_arguments sg)):
0 <=
lo + 4 *
ofs <=
Ptrofs.max_unsigned.
Proof.
hexploit loc_arguments_bounded.
-
instantiate (1:=
sg).
instantiate (1:=
ty).
instantiate (1:=
ofs).
revert ofs ty IN.
induction (
loc_arguments sg);
ss;
i.
des;
clarify;
ss;
eauto.
eapply in_app_iff.
right.
eapply IHl;
eauto.
-
i.
split.
+
hexploit (
loc_arguments_acceptable sg);
eauto.
intros ACCP.
inv ACCP.
lia.
+
destruct ty;
ss;
lia.
Qed.
Lemma sig_args_length sg
:
Datatypes.length (
sig_args sg) =
Datatypes.length (
loc_arguments sg).
Proof.
unfold loc_arguments in *.
des_ifs.
generalize 0
at 1.
generalize 0
at 1.
generalize 0
at 1.
induction (
sig_args sg);
ss;
i.
des_ifs;
ss;
f_equal;
eauto.
Qed.
Lemma Val_has_type_list_length sg vs
(
TYP:
Val.has_type_list vs (
sig_args sg)):
Datatypes.length vs =
Datatypes.length (
loc_arguments sg).
Proof.
rewrite <-
sig_args_length.
revert vs TYP.
induction (
sig_args sg);
ss;
i;
destruct vs;
ss.
des.
f_equal;
eauto.
Qed.
Ltac _locmap_tac :=
try (
first[
rewrite Locmap.gss;
ss;
check_safe|
rewrite Locmap.gso;
ss]);
try match goal with
| [
H:
Loc.notin _ (
_ ::
_) |-
_] =>
inv H
| [
H:
Loc.norepet (
_ ::
_) |-
_] =>
inv H
| [ |-
Loc.diff _ _] =>
by (
eapply Loc.in_notin_diff;
eauto)
| [
H:
Loc.diff ?
A ?
B |-
Loc.diff ?
B ?
A] =>
apply Loc.diff_sym;
assumption
| [
H:
R ?
x <>
R ?
y |-
_] =>
tryif exists_prop (
x <>
y)
then idtac
else assert(
x <>
y)
by (
ii;
clarify;
ss)
end;
des_safe;
idtac.
Local Opaque Loc.diff.
Ltac locmap_tac :=
repeat _locmap_tac.
Definition locmap_put (
l:
loc) (
v:
val) (
ls:
locset):
locset :=
fun loc =>
if Loc.eq loc l then v else ls loc.
Hint Unfold locmap_put.
Fixpoint fill_arguments (
ls0:
locset) (
args:
list val) (
locs:
list (
rpair loc)):
option locset :=
match args,
locs with
| [], [] =>
Some ls0
|
arg ::
args,
loc ::
locs =>
match fill_arguments ls0 args locs with
|
Some ls1 =>
match loc with
|
One loc =>
Some (
locmap_put loc arg ls1)
|
Twolong hi lo =>
Some (
Locmap.set lo arg.(
Val.loword) (
Locmap.set hi arg.(
Val.hiword)
ls1))
end
|
None =>
None
end
|
_,
_ =>
None
end.
Lemma fill_arguments_progress
ls0 args locs
(
LEN:
length args =
length locs):
exists ls1, <<
LS:
fill_arguments ls0 args locs =
Some ls1>>.
Proof.
ginduction args; ii; destruct locs; ss.
- esplits; eauto.
- exploit IHargs; eauto. i; des. rewrite LS. des_ifs; esplits; eauto.
Qed.
Lemma fill_arguments_spec
vs sg locs ls0 ls1
(
LOCS:
locs =
loc_arguments sg)
(
FILL:
fill_arguments ls0 vs locs =
Some ls1):
<<
FILL:
vs =
map (
fun p =>
Locmap.getpair p ls1)
locs>> /\
<<
OUT:
forall loc
(
NOTIN: ~
In loc (
regs_of_rpairs locs)),
ls1 loc =
ls0 loc>>.
Proof.
Definition extcall_args_reg (
mr:
mreg) (
sg:
signature):
{
In (
R mr) (
regs_of_rpairs (
loc_arguments sg))} +
{~
In (
R mr) (
regs_of_rpairs (
loc_arguments sg))}.
Proof.
generalize (
regs_of_rpairs (
loc_arguments sg)).
induction l.
-
ss.
tauto.
-
ss.
inv IHl; [
tauto|].
destruct a.
+
destruct (
mreg_eq r mr); [
clarify;
eauto|].
right.
intros [];
clarify.
+
right.
intros [];
clarify.
Qed.
Lemma arguments_loc sg sl delta ty
(
IN:
In (
S sl delta ty) (
regs_of_rpairs (
loc_arguments sg))):
sl =
Outgoing /\
0 <=
delta /\
4 *
delta +
size_chunk (
chunk_of_type ty) <= 4 *
size_arguments sg.
Proof.
Lemma regs_of_rpair_In A (
l:
list (
rpair A)):
(
forall r (
IN:
In (
One r)
l),
In r (
regs_of_rpairs l))
/\ (
forall r0 r1 (
IN:
In (
Twolong r0 r1)
l),
In r0 (
regs_of_rpairs l) /\
In r1 (
regs_of_rpairs l)).
Proof.
induction l;
i;
ss;
split;
i;
des;
clarify;
ss;
eauto.
-
eapply in_or_app.
eauto.
-
split;
eapply in_or_app;
right;
eapply (
IHl0 _ _ IN).
Qed.