summaryrefslogtreecommitdiff
path: root/backend/Reloadproof.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-04-09 16:59:13 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-04-09 16:59:13 +0000
commitabe2bb5c40260a31ce5ee27b841bcbd647ff8b88 (patch)
treeae109a136508da283a9e2be5f039c5f9cca4f95c /backend/Reloadproof.v
parentffd6080f9e1e742c73ac38354b31c6fc4e3963ba (diff)
Merge of branch "unsigned-offsets":
- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Reloadproof.v')
-rw-r--r--backend/Reloadproof.v15
1 files changed, 8 insertions, 7 deletions
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index a3ed303..09a9101 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -156,10 +156,10 @@ Proof.
Qed.
Lemma not_enough_temporaries_addr:
- forall (ge: genv) sp addr src args ls v,
+ forall (ge: genv) sp addr src args ls v m,
enough_temporaries (src :: args) = false ->
eval_addressing ge sp addr (List.map ls args) = Some v ->
- eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) = Some v.
+ eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v.
Proof.
intros.
apply eval_op_for_binary_addressing; auto.
@@ -692,7 +692,8 @@ Proof.
unfold call_regs, parameter_of_argument.
generalize (loc_arguments_acceptable _ _ H).
unfold loc_argument_acceptable.
- destruct x. auto.
+ destruct x.
+ intros. destruct (in_dec Loc.eq (R m) temporaries). contradiction. auto.
destruct s; intros; try contradiction. auto.
Qed.
@@ -1015,9 +1016,9 @@ Proof.
exploit add_reloads_correct.
eapply enough_temporaries_op_args; eauto. auto.
intros [ls2 [A [B C]]]. instantiate (1 := ls) in B.
- assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) = Some tv
+ assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv
/\ Val.lessdef v tv).
- apply eval_operation_lessdef with (map rs args); auto.
+ apply eval_operation_lessdef with (map rs args) m; auto.
rewrite B. eapply agree_locs; eauto.
rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
destruct H1 as [tv [P Q]].
@@ -1291,7 +1292,7 @@ Proof.
intros [ls2 [A [B C]]].
left; econstructor; split.
eapply plus_right. eauto. eapply exec_Lcond_true; eauto.
- rewrite B. apply eval_condition_lessdef with (map rs args); auto.
+ rewrite B. apply eval_condition_lessdef with (map rs args) m; auto.
eapply agree_locs; eauto.
apply find_label_transf_function; eauto.
traceEq.
@@ -1306,7 +1307,7 @@ Proof.
intros [ls2 [A [B C]]].
left; econstructor; split.
eapply plus_right. eauto. eapply exec_Lcond_false; eauto.
- rewrite B. apply eval_condition_lessdef with (map rs args); auto.
+ rewrite B. apply eval_condition_lessdef with (map rs args) m; auto.
eapply agree_locs; eauto.
traceEq.
econstructor; eauto with coqlib.