From 7cdd676d002e33015b496f609538a9e86d77c543 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 8 Aug 2019 11:18:38 +0200
Subject: AArch64 port

This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
---
 backend/NeedDomain.v | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

(limited to 'backend/NeedDomain.v')

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.
-- 
cgit