diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-08-08 11:18:38 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-08 11:18:38 +0200 |
| commit | 7cdd676d002e33015b496f609538a9e86d77c543 (patch) | |
| tree | f4d105bce152445334613e857d4a672976a56f3e /backend/NeedDomain.v | |
| parent | eb85803875c5a4e90be60d870f01fac380ca18b0 (diff) | |
| download | compcert-kvx-7cdd676d002e33015b496f609538a9e86d77c543.tar.gz compcert-kvx-7cdd676d002e33015b496f609538a9e86d77c543.zip | |
AArch64 port
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
Diffstat (limited to 'backend/NeedDomain.v')
| -rw-r--r-- | backend/NeedDomain.v | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index b35c90b2..3c2d8e20 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -594,7 +594,8 @@ Proof. Qed. (** Modular arithmetic operations: add, mul, opposite. - (But not subtraction because of the pointer - pointer case. *) + Also subtraction, but only on 64-bit targets, otherwise + the pointer - pointer case does not fit. *) Definition modarith (x: nval) := match x with @@ -615,6 +616,19 @@ Proof. - inv H; auto. inv H0; auto. destruct w1; auto. Qed. +Lemma sub_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) -> + Archi.ptr64 = true -> + vagree (Val.sub v1 v2) (Val.sub w1 w2) x. +Proof. + unfold modarith; intros. destruct x; simpl in *. +- auto. +- unfold Val.sub; rewrite H1; InvAgree. + apply eqmod_iagree. apply eqmod_sub; apply iagree_eqmod; auto. +- inv H; auto. inv H0; auto. destruct w1; auto. +Qed. + Remark modarith_idem: forall nv, modarith (modarith nv) = modarith nv. Proof. destruct nv; simpl; auto. f_equal; apply complete_mask_idem. @@ -680,7 +694,7 @@ Definition sign_ext (n: Z) (x: nval) := Lemma sign_ext_sound: forall v w x n, vagree v w (sign_ext n x) -> - 0 < n < Int.zwordsize -> + 0 < n -> vagree (Val.sign_ext n v) (Val.sign_ext n w) x. Proof. unfold sign_ext; intros. destruct x; simpl in *. @@ -889,7 +903,8 @@ Lemma default_needs_of_operation_sound: eval_operation ge (Vptr sp Ptrofs.zero) op args1 m1 = Some v1 -> vagree_list args1 args2 nil \/ vagree_list args1 args2 (default nv :: nil) - \/ vagree_list args1 args2 (default nv :: default nv :: nil) -> + \/ vagree_list args1 args2 (default nv :: default nv :: nil) + \/ vagree_list args1 args2 (default nv :: default nv :: default nv :: nil) -> nv <> Nothing -> exists v2, eval_operation ge (Vptr sp Ptrofs.zero) op args2 m2 = Some v2 @@ -901,7 +916,8 @@ Proof. { destruct H0. auto with na. destruct H0. inv H0; constructor; auto with na. - inv H0; constructor; auto with na. inv H8; constructor; auto with na. + destruct H0. inv H0. constructor. inv H8; constructor; auto with na. + inv H0; constructor; auto with na. inv H8; constructor; auto with na. inv H9; constructor; auto with na. } exploit (@eval_operation_inj _ _ _ _ ge ge inject_id). eassumption. auto. auto. auto. |