aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Asmgenproof0.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Asmgenproof0.v')
-rw-r--r--backend/Asmgenproof0.v46
1 files changed, 36 insertions, 10 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index ba7fa3a6..0533d561 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -356,29 +356,55 @@ Proof.
eapply extcall_args_match; eauto.
Qed.
-(** Translation of arguments to annotations. *)
+(** Translation of arguments and results to builtins. *)
-Remark annot_arg_match:
+Remark builtin_arg_match:
forall ge (rs: regset) sp m a v,
- eval_annot_arg ge (fun r => rs (preg_of r)) sp m a v ->
- eval_annot_arg ge rs sp m (map_annot_arg preg_of a) v.
+ eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v ->
+ eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v.
Proof.
- induction 1; simpl; eauto with aarg.
+ induction 1; simpl; eauto with barg.
Qed.
-Lemma annot_args_match:
+Lemma builtin_args_match:
forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
- forall al vl, eval_annot_args ge ms sp m al vl ->
- exists vl', eval_annot_args ge rs sp m' (map (map_annot_arg preg_of) al) vl'
+ forall al vl, eval_builtin_args ge ms sp m al vl ->
+ exists vl', eval_builtin_args ge rs sp m' (map (map_builtin_arg preg_of) al) vl'
/\ Val.lessdef_list vl vl'.
Proof.
induction 3; intros; simpl.
exists (@nil val); split; constructor.
- exploit (@eval_annot_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto.
+ 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 annot_arg_match; auto.
+ exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; 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 (Asm.set_res (map_builtin_res preg_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 set_res_other:
+ forall r res v rs,
+ data_preg r = false ->
+ set_res (map_builtin_res preg_of res) v rs r = rs r.
+Proof.
+ induction res; simpl; intros.
+- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate.
+- auto.
+- rewrite IHres2, IHres1; auto.
Qed.
(** * Correspondence between Mach code and Asm code *)