Commit 0df99dc4 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

AArch64 modeling of registers destroyed by pseudo-instructions

Pfmovimms, Pfmovimmd destroy X16
Pbtbl preserves X17
Inlined built-in functions destroy X16 and X30
parent ef5477a4
......@@ -970,9 +970,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfmov rd r1 =>
Next (nextinstr (rs#rd <- (rs#r1))) m
| Pfmovimms rd f =>
Next (nextinstr (rs#rd <- (Vsingle f))) m
Next (nextinstr (rs#X16 <- Vundef #rd <- (Vsingle f))) m
| Pfmovimmd rd f =>
Next (nextinstr (rs#rd <- (Vfloat f))) m
Next (nextinstr (rs#X16 <- Vundef #rd <- (Vfloat f))) m
| Pfmovi S rd r1 =>
Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
| Pfmovi D rd r1 =>
......@@ -1097,7 +1097,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Vint n =>
match list_nth_z tbl (Int.unsigned n) with
| None => Stuck
| Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
| Some lbl => goto_label f lbl (rs#X16 <- Vundef) m
end
| _ => Stuck
end
......@@ -1212,7 +1212,7 @@ Inductive step: state -> trace -> state -> Prop :=
external_call ef ge vargs m t vres m' ->
rs' = nextinstr
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
(undef_regs (IR X16 :: IR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
......
......@@ -831,13 +831,16 @@ Local Transparent destroyed_by_op.
econstructor; eauto.
instantiate (2 := tf); instantiate (1 := x).
unfold nextinstr. rewrite Pregmap.gss.
rewrite set_res_other. rewrite undef_regs_other_2.
rewrite set_res_other. rewrite undef_regs_other.
rewrite <- H1. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
rewrite preg_notin_charact. intros. auto with asmgen.
simpl; intros. destruct H4. congruence. destruct H4. congruence.
exploit list_in_map_inv; eauto. intros (mr & U & V). subst.
auto with asmgen.
auto with asmgen.
apply agree_nextinstr. eapply agree_set_res; auto.
eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
eapply agree_undef_regs; eauto. intros.
simpl. rewrite undef_regs_other_2; auto. Simpl.
congruence.
- (* Mgoto *)
......@@ -879,7 +882,7 @@ Local Transparent destroyed_by_op.
exploit functions_transl; eauto. intro FN.
generalize (transf_function_no_overflow _ _ H5); intro NOOV.
exploit find_label_goto_label. eauto. eauto.
instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef).
instantiate (2 := rs0#X16 <- Vundef).
Simpl. eauto.
eauto.
intros [tc' [rs' [A [B C]]]].
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment