Commit 5e389894 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

PowerPC modeling of registers destroyed by pseudo-instructions

Inlined built-in functions destroy GPR0
parent a4cfb9c2
......@@ -1195,7 +1195,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 GPR0 :: 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',
......@@ -781,16 +781,18 @@ Opaque loadind.
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. simpl. rewrite undef_regs_other_2.
rewrite Pregmap.gso by auto with asmgen.
rewrite <- H1. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
rewrite preg_notin_charact. intros. auto with asmgen.
auto with asmgen.
apply agree_nextinstr. eapply agree_set_res; auto.
eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
eapply agree_undef_regs; eauto.
intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen.
intros. Simpl. rewrite set_res_other by auto.
rewrite undef_regs_other_2; auto with asmgen.
simpl. rewrite undef_regs_other_2; auto with asmgen.
- (* Mgoto *)
assert (f0 = f) by congruence. subst f0.
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