diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-06-15 15:11:26 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-07-06 15:41:51 +0200 |
| commit | dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a (patch) | |
| tree | 82c09b8cff023557084d6257acdef84b1311dd35 /x86/SelectOpproof.v | |
| parent | 92fc8a425034abc1247203a4c0d471e8b6d0e941 (diff) | |
| download | compcert-dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a.tar.gz compcert-dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a.zip | |
Extend builtin arguments with a pointer addition operator
This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.
Current status: x86 port only, the only new addressing mode handled is reg + offset.
Diffstat (limited to 'x86/SelectOpproof.v')
| -rw-r--r-- | x86/SelectOpproof.v | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index e2e0b830..fdbadaa8 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -947,6 +947,22 @@ Proof. - apply D; auto. Qed. +Theorem eval_builtin_arg_addr: + forall addr al vl v, + eval_exprlist ge sp e m nil al vl -> + Op.eval_addressing ge sp addr vl = Some v -> + CminorSel.eval_builtin_arg ge sp e m (builtin_arg_addr addr al) v. +Proof. + intros until v. unfold builtin_arg_addr; case (builtin_arg_addr_match addr al); intros; InvEval. +- set (v2 := if Archi.ptr64 then Vlong (Int64.repr n) else Vint (Int.repr n)). + assert (EQ: v = if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2). + { unfold Op.eval_addressing in H0; unfold v2; destruct Archi.ptr64; simpl in H0; inv H0; auto. } + rewrite EQ. constructor. constructor; auto. unfold v2; destruct Archi.ptr64; constructor. +- rewrite eval_addressing_Aglobal in H0. inv H0. constructor. +- rewrite eval_addressing_Ainstack in H0. inv H0. constructor. +- constructor. econstructor. eauto. rewrite eval_Olea_ptr. auto. +Qed. + Theorem eval_builtin_arg: forall a v, eval_expr ge sp e m nil a v -> @@ -955,10 +971,12 @@ Proof. intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval. - constructor. - constructor. -- constructor. -- constructor. -- constructor. -- constructor. +- destruct Archi.ptr64 eqn:SF. ++ constructor; auto. ++ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption. +- destruct Archi.ptr64 eqn:SF. ++ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption. ++ constructor; auto. - simpl in H5. inv H5. constructor. - constructor; auto. - inv H. InvEval. rewrite eval_addressing_Aglobal in H6. inv H6. constructor; auto. |