Commit 341d1123 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

intermediatet commit before builtins

parent 21f6353c
......@@ -389,9 +389,9 @@ Definition arith_extended
Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
if Int.eq n Int.zero then
Pmov rd r1 ::bi k
else if Int.eq n Int.one then
(* else if Int.eq n Int.one then
Padd W (SOlsr (Int.repr 31)) X16 r1 r1 ::bi
Porr W (SOasr n) rd XZR X16 ::bi k
Porr W (SOasr n) rd XZR X16 ::bi k *)
else
Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi
Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi
......@@ -400,9 +400,9 @@ Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
if Int.eq n Int.zero then
Pmov rd r1 ::bi k
else if Int.eq n Int.one then
(* else if Int.eq n Int.one then
Padd X (SOlsr (Int.repr 63)) X16 r1 r1 ::bi
Porr X (SOasr n) rd XZR X16 ::bi k
Porr X (SOasr n) rd XZR X16 ::bi k *)
else
Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi
Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi
......@@ -1141,8 +1141,11 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c)
| MBop op args res =>
transl_op op args res k
| MBload _ chunk addr args dst =>
transl_load chunk addr args dst k
| MBload t chunk addr args dst =>
match t with
| TRAP => transl_load chunk addr args dst k
| NOTRAP => Error(msg "Asmgenblock.transl_instr_basic: NOTRAP load not supported in aarch64.")
end
| MBstore chunk addr args src =>
transl_store chunk addr args src k
end.
......
This diff is collapsed.
......@@ -6,6 +6,7 @@
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
......@@ -44,6 +45,52 @@ Module AB:=Asmblock.
(** * Agreement between Mach registers and processor registers *)
Hint Extern 2 (_ <> _) => congruence: asmgen.
Lemma ireg_of_eq:
forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
Proof.
unfold ireg_of; intros. destruct (preg_of r) as [[[rr1|]|]|xsp|]; inv H; auto.
Qed.
Lemma freg_of_eq:
forall r r', freg_of r = OK r' -> preg_of r = FR r'.
Proof.
unfold freg_of; intros. destruct (preg_of r) as [[fr|]|xsp|]; inv H; auto.
Qed.
Lemma ireg_of_eq':
forall r r', ireg_of r = OK r' -> dreg_of r = IR r'.
Proof.
unfold ireg_of; intros. destruct r; simpl in *; inv H; auto.
Qed.
Lemma freg_of_eq':
forall r r', freg_of r = OK r' -> dreg_of r = FR r'.
Proof.
unfold freg_of; intros. destruct r; simpl in *; inv H; auto.
Qed.
Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop :=
match rl with
| nil => True
| r1 :: nil => r <> preg_of r1
| r1 :: rl => r <> preg_of r1 /\ preg_notin r rl
end.
Remark preg_notin_charact:
forall r rl,
preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr).
Proof.
induction rl; simpl; intros.
tauto.
destruct rl.
simpl. split. intros. intuition congruence. auto.
rewrite IHrl. split.
intros [A B]. intros. destruct H. congruence. auto.
auto.
Qed.
Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree {
agree_sp: rs#SP = sp;
agree_sp_def: sp <> Vundef;
......@@ -67,6 +114,184 @@ Proof.
intros. destruct H. auto.
Qed.
Lemma preg_vals:
forall ms sp rs, agree ms sp rs ->
forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)).
Proof.
induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.
Qed.
Lemma preg_of_injective:
forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
Proof.
destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
Qed.
Lemma sp_val:
forall ms sp rs, agree ms sp rs -> sp = rs#SP.
Proof.
intros. destruct H; auto.
Qed.
Lemma ireg_val:
forall ms sp rs r r',
agree ms sp rs ->
ireg_of r = OK r' ->
Val.lessdef (ms r) rs#r'.
Proof.
intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto.
Qed.
Lemma preg_of_not_X29: forall dst,
negb (mreg_eq dst R29) = true ->
DR (IR X29) <> preg_of dst.
Proof.
intros. destruct dst; try discriminate.
Qed.
Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
(** Preservation of register agreement under various assignments. *)
Lemma agree_set_mreg:
forall ms sp rs r v rs',
agree ms sp rs ->
Val.lessdef v (rs'#(preg_of r)) ->
(forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
agree (Mach.Regmap.set r v ms) sp rs'.
Proof.
intros. destruct H. split; auto.
rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP.
intros. unfold Mach.Regmap.set. destruct (Mach.RegEq.eq r0 r). congruence.
rewrite H1. auto. apply preg_of_data.
red; intros; elim n. eapply preg_of_injective; eauto.
Qed.
Lemma agree_set_other:
forall ms sp rs r v,
agree ms sp rs ->
data_preg r = false ->
agree ms sp (rs#r <- v).
Proof.
intros. apply agree_exten with rs. auto.
intros. apply Pregmap.gso. congruence.
Qed.
Lemma agree_nextblock:
forall ms sp rs b,
agree ms sp rs -> agree ms sp (incrPC (Ptrofs.repr (size b)) rs).
Proof.
intros. unfold incrPC. apply agree_set_other. auto. auto.
Qed.
Lemma agree_set_res:
forall res ms sp rs v v',
agree ms sp rs ->
Val.lessdef v v' ->
agree (Mach.set_res res v ms) sp (set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v' rs).
Proof.
induction res; simpl; intros.
- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
intros. apply Pregmap.gso; auto.
- auto.
- apply IHres2. apply IHres1. auto.
apply Val.hiword_lessdef; auto.
apply Val.loword_lessdef; auto.
Qed.
Lemma agree_undef_regs:
forall ms sp rl rs rs',
agree ms sp rs ->
(forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
agree (Mach.undef_regs rl ms) sp rs'.
Proof.
intros. destruct H. split; auto.
rewrite <- agree_sp0. apply H0; auto.
rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
intros. destruct (In_dec mreg_eq r rl).
rewrite Mach.undef_regs_same; auto.
rewrite Mach.undef_regs_other; auto. rewrite H0; auto.
apply preg_of_data.
rewrite preg_notin_charact. intros; red; intros. elim n.
exploit preg_of_injective; eauto. congruence.
Qed.
Lemma agree_set_undef_mreg:
forall ms sp rs r v rl rs',
agree ms sp rs ->
Val.lessdef v (rs'#(preg_of r)) ->
(forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') ->
agree (Mach.Regmap.set r v (Mach.undef_regs rl ms)) sp rs'.
Proof.
intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
apply agree_undef_regs with rs; auto.
intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)).
congruence. auto.
intros. rewrite Pregmap.gso; auto.
Qed.
Lemma agree_change_sp:
forall ms sp rs sp',
agree ms sp rs -> sp' <> Vundef ->
agree ms sp' (rs#SP <- sp').
Proof.
intros. inv H. split; auto.
intros. rewrite Pregmap.gso; auto with asmgen.
Qed.
Remark builtin_arg_match:
forall ge (rs: regset) sp m a v,
eval_builtin_arg ge (fun r => rs (dreg_of r)) sp m a v ->
eval_builtin_arg ge (fun r => rs (DR r)) sp m (map_builtin_arg dreg_of a) v.
Proof.
induction 1; simpl; eauto with barg. econstructor.
Qed.
Lemma builtin_args_match:
forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
forall al vl, eval_builtin_args ge ms sp m al vl ->
exists vl', eval_builtin_args ge (fun r => rs (DR r)) sp m' (map (map_builtin_arg dreg_of) al) vl'
/\ Val.lessdef_list vl vl'.
Proof.
induction 3; intros; simpl.
exists (@nil val); split; constructor.
exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto.
intros; eapply preg_val; eauto.
intros (v1' & A & B).
destruct IHlist_forall2 as [vl' [C D]].
exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto.
Qed.
Lemma set_res_other:
forall r res v rs,
data_preg r = false ->
set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v rs r = rs r.
Proof.
induction res; simpl; intros.
- apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate.
- auto.
- rewrite IHres2, IHres1; auto.
Qed.
Lemma undef_regs_other:
forall r rl rs,
(forall r', In r' rl -> r <> r') ->
undef_regs rl rs r = rs r.
Proof.
induction rl; simpl; intros. auto.
rewrite IHrl by auto. rewrite Pregmap.gso; auto.
Qed.
Lemma undef_regs_other_2:
forall r rl rs,
preg_notin r rl ->
undef_regs (map preg_of rl) rs r = rs r.
Proof.
intros. apply undef_regs_other. intros.
exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
rewrite preg_notin_charact in H. auto.
Qed.
Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
| code_tail_0: forall c,
code_tail 0 c c
......@@ -156,6 +381,45 @@ Proof.
- rewrite Ptrofs.unsigned_repr; omega.
Qed.
(** The [find_label] function returns the code tail starting at the
given label. A connection with [code_tail] is then established. *)
Fixpoint find_label (lbl: label) (c: bblocks) {struct c} : option bblocks :=
match c with
| nil => None
| bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl
end.
(* inspired from Mach *)
Lemma find_label_tail:
forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c.
Proof.
induction c; simpl; intros. discriminate.
destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
Qed.
Lemma label_pos_code_tail:
forall lbl c pos c',
find_label lbl c = Some c' ->
exists pos',
label_pos lbl pos c = Some pos'
/\ code_tail (pos' - pos) c c'
/\ pos <= pos' <= pos + size_blocks c.
Proof.
induction c.
simpl; intros. discriminate.
simpl; intros until c'.
case (is_label lbl a).
- intros. inv H. exists pos. split; auto. split.
replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
generalize (size_blocks_pos c). generalize (size_positive a). omega.
- intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
exists pos'. split. auto. split.
replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
constructor. auto. generalize (size_positive a). omega.
Qed.
(** Predictor for return addresses in generated Asm code.
The [return_address_offset] predicate defined here is used in the
......@@ -282,6 +546,129 @@ Proof.
congruence.
Qed.
Section STRAIGHTLINE.
Variable ge: genv.
Variable lk: aarch64_linker.
Variable fn: function.
(** Straight-line code is composed of processor instructions that execute
in sequence (no branches, no function calls and returns).
The following inductive predicate relates the machine states
before and after executing a straight-line sequence of instructions.
Instructions are taken from the first list instead of being fetched
from memory. *)
Inductive exec_straight: list basic -> regset -> mem ->
list basic -> regset -> mem -> Prop :=
| exec_straight_one:
forall i1 c rs1 m1 rs2 m2,
exec_basic lk ge i1 rs1 m1 = Next rs2 m2 ->
exec_straight (i1 :: c) rs1 m1 c rs2 m2
| exec_straight_step:
forall i c rs1 m1 rs2 m2 c' rs3 m3,
exec_basic lk ge i rs1 m1 = Next rs2 m2 ->
exec_straight c rs2 m2 c' rs3 m3 ->
exec_straight (i :: c) rs1 m1 c' rs3 m3.
Lemma exec_straight_trans:
forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
exec_straight c1 rs1 m1 c2 rs2 m2 ->
exec_straight c2 rs2 m2 c3 rs3 m3 ->
exec_straight c1 rs1 m1 c3 rs3 m3.
Proof.
induction 1; intros.
apply exec_straight_step with rs2 m2; auto.
apply exec_straight_step with rs2 m2; auto.
Qed.
Lemma exec_straight_two:
forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
exec_basic lk ge i1 rs1 m1 = Next rs2 m2 ->
exec_basic lk ge i2 rs2 m2 = Next rs3 m3 ->
exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
Proof.
intros. apply exec_straight_step with rs2 m2; auto.
apply exec_straight_one; auto.
Qed.
Lemma exec_straight_three:
forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
exec_basic lk ge i1 rs1 m1 = Next rs2 m2 ->
exec_basic lk ge i2 rs2 m2 = Next rs3 m3 ->
exec_basic lk ge i3 rs3 m3 = Next rs4 m4 ->
exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
Proof.
intros. apply exec_straight_step with rs2 m2; auto.
eapply exec_straight_two; eauto.
Qed.
Inductive exec_straight_opt: list basic -> regset -> mem -> list basic -> regset -> mem -> Prop :=
| exec_straight_opt_refl: forall c rs m,
exec_straight_opt c rs m c rs m
| exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2,
exec_straight c1 rs1 m1 c2 rs2 m2 ->
exec_straight_opt c1 rs1 m1 c2 rs2 m2.
Remark exec_straight_opt_right:
forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2,
exec_straight_opt c1 rs1 m1 c2 rs2 m2 ->
exec_straight c2 rs2 m2 c3 rs3 m3 ->
exec_straight c1 rs1 m1 c3 rs3 m3.
Proof.
destruct 1; intros. auto. eapply exec_straight_trans; eauto.
Qed.
Lemma exec_straight_opt_step:
forall i c rs1 m1 rs2 m2 c' rs3 m3,
exec_basic lk ge i rs1 m1 = Next rs2 m2 ->
exec_straight_opt c rs2 m2 c' rs3 m3 ->
exec_straight (i :: c) rs1 m1 c' rs3 m3.
Proof.
intros. inv H0.
- apply exec_straight_one; auto.
- eapply exec_straight_step; eauto.
Qed.
Lemma exec_straight_opt_step_opt:
forall i c rs1 m1 rs2 m2 c' rs3 m3,
exec_basic lk ge i rs1 m1 = Next rs2 m2 ->
exec_straight_opt c rs2 m2 c' rs3 m3 ->
exec_straight_opt (i :: c) rs1 m1 c' rs3 m3.
Proof.
intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto.
Qed.
(** Linking exec_straight with exec_straight_blocks *)
(* Lemma exec_straight_pc:
forall c c' rs1 m1 rs2 m2,
exec_straight c rs1 m1 c' rs2 m2 ->
rs2 PC = rs1 PC.
Proof.
induction c; intros; try (inv H; fail).
inv H.
- eapply exec_basic_instr_pc; eauto.
- rewrite (IHc c' rs3 m3 rs2 m2); auto.
erewrite exec_basic_instr_pc; eauto.
Qed. *)
Lemma exec_body_pc:
forall ge l rs1 m1 rs2 m2,
exec_body lk ge l rs1 m1 = Next rs2 m2 ->
rs2 PC = rs1 PC.
Proof.
induction l.
- intros. inv H. auto.
- intros until m2. intro EXEB.
inv EXEB. destruct (exec_basic _ _ _ _ _) eqn:EBI; try discriminate.
eapply IHl in H0. rewrite H0.
destruct s.
erewrite exec_basic_instr_pc; eauto.
Qed.
End STRAIGHTLINE.
(** * Properties of the Machblock call stack *)
Section MATCH_STACK.
......
This diff is collapsed.
......@@ -39,7 +39,13 @@ Lemma preg_of_data:
Proof.
intros. destruct r; reflexivity.
Qed.
Hint Resolve preg_of_data: asmgen.
Lemma dreg_of_data:
forall r, data_preg (dreg_of r) = true.
Proof.
intros. destruct r; reflexivity.
Qed.
Hint Resolve preg_of_data dreg_of_data: asmgen.
Lemma data_diff:
forall r r',
......@@ -55,6 +61,12 @@ Proof.
intros. apply data_diff; auto with asmgen.
Qed.
Lemma preg_of_not_SP:
forall r, preg_of r <> SP.
Proof.
intros. unfold preg_of; destruct r; simpl; try discriminate.
Qed.
(*
Lemma preg_of_not_SP:
forall r, preg_of r <> SP.
......@@ -81,73 +93,61 @@ Lemma nextblock_inv1:
forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
Proof.
intros. apply nextblock_inv. red; intro; subst; discriminate.
Qed.
Qed.*)
Ltac desif :=
repeat match goal with
| [ |- context[ if ?f then _ else _ ] ] => destruct f
end.
Ltac decomp :=
repeat match goal with
| [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r)
end.
Ltac Simplif :=
((rewrite nextblock_inv by eauto with asmgen)
|| (rewrite nextblock_inv1 by eauto with asmgen)
((desif)
|| (try unfold compare_long)
|| (try unfold compare_int)
|| (try unfold compare_float)
|| (try unfold compare_single)
|| decomp
|| (rewrite Pregmap.gss)
|| (rewrite nextblock_pc)
|| (rewrite Pregmap.gso by eauto with asmgen)
); auto with asmgen.
Ltac Simpl := repeat Simplif.
Section EPC.
Variable lk: aarch64_linker.
(* For Asmblockgenproof0 *)
Theorem exec_basic_instr_pc:
forall ge b rs1 m1 rs2 m2,
exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
exec_basic lk ge b rs1 m1 = Next rs2 m2 ->
rs2 PC = rs1 PC.
Proof.
intros. destruct b; try destruct i; try destruct i.
all: try (inv H; Simpl).
1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
{ (* PLoadQRRO *)
unfold parexec_load_q_offset in H1.
destruct (gpreg_q_expand _) as [r0 r1] in H1.
destruct (Mem.loadv _ _ _) in H1; try discriminate.
destruct (Mem.loadv _ _ _) in H1; try discriminate.
inv H1. Simpl. }
{ (* PLoadORRO *)
unfold parexec_load_o_offset in H1.
destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
destruct (Mem.loadv _ _ _) in H1; try discriminate.
destruct (Mem.loadv _ _ _) in H1; try discriminate.
destruct (Mem.loadv _ _ _) in H1; try discriminate.
destruct (Mem.loadv _ _ _) in H1; try discriminate.
inv H1. Simpl. }
1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
{ (* PStoreQRRO *)
unfold parexec_store_q_offset in H1.
destruct (gpreg_q_expand _) as [r0 r1] in H1.
unfold eval_offset in H1; try discriminate.
destruct (Mem.storev _ _ _) in H1; try discriminate.
destruct (Mem.storev _ _ _) in H1; try discriminate.
inv H1. Simpl. reflexivity. }
{ (* PStoreORRO *)
unfold parexec_store_o_offset in H1.
destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
unfold eval_offset in H1; try discriminate.
destruct (Mem.storev _ _ _) in H1; try discriminate.
destruct (Mem.storev _ _ _) in H1; try discriminate.
destruct (Mem.storev _ _ _) in H1; try discriminate.
destruct (Mem.storev _ _ _) in H1; try discriminate.
inv H1. Simpl. reflexivity. }
- destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
- destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
- destruct rs; try discriminate. inv H1. Simpl.
- destruct rd; try discriminate. inv H1; Simpl.
- reflexivity.
intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld;
try destruct st; try destruct st; try destruct a.
all: try (inv H; simpl in *; auto; Simpl).
all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl).
all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *;
try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl).