From aedaa5cb1435008d1d872b7d6687bec5843798a0 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 1 Apr 2020 09:15:28 +0200
Subject: adapting new stuff for ARM and AArch64

---
 aarch64/Op.v            | 11 ++++++++---
 arm/Op.v                | 11 ++++++++---
 backend/FirstNopproof.v | 17 ++++++++---------
 backend/Injectproof.v   | 15 ++++++---------
 4 files changed, 30 insertions(+), 24 deletions(-)

diff --git a/aarch64/Op.v b/aarch64/Op.v
index c0b9d435..afc25aa6 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -938,14 +938,19 @@ Definition is_trapping_op (op : operation) :=
   end.
                 
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/arm/Op.v b/arm/Op.v
index 671bdbe4..25e48ce1 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -531,14 +531,19 @@ Definition is_trapping_op (op : operation) :=
   end.
                 
 
+Definition args_of_operation op :=
+  if eq_operation op Omove
+  then 1%nat
+  else List.length (fst (type_of_operation op)).
+
 Lemma is_trapping_op_sound:
   forall op vl sp m,
-    op <> Omove ->
     is_trapping_op op = false ->
-    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    (List.length vl) = args_of_operation op ->
     eval_operation genv sp op vl m <> None.
 Proof.
-  destruct op; intros; simpl in *; try congruence.
+  unfold args_of_operation.
+  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v
index 5d9a7d6a..a5d63c25 100644
--- a/backend/FirstNopproof.v
+++ b/backend/FirstNopproof.v
@@ -168,26 +168,25 @@ Proof.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
-      apply symbols_preserved.
+      all: rewrite <- H0.
+      all: auto using eval_addressing_preserved, symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
+      all: rewrite <- H0;
+      apply eval_addressing_preserved;
       apply symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
+      all: rewrite <- H0;
+      apply eval_addressing_preserved;
       apply symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Istore; eauto with firstnop.
-      rewrite <- H0.
-      apply eval_addressing_preserved.
+      all: rewrite <- H0;
+      apply eval_addressing_preserved;
       apply symbols_preserved.
     + constructor; auto with firstnop.
   - left. econstructor. split.
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index 1dd26a24..77cae8a1 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -778,23 +778,20 @@ Section INJECTOR.
           * exists (trs # res <- v).
             split.
             ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial.
-               rewrite eval_addressing_preserved with (ge1 := ge).
-               assumption.
-               exact symbols_preserved.
+               all: try rewrite eval_addressing_preserved with (ge1 := ge).
+               all: auto using symbols_preserved.
             ** apply assign_above; auto.
           * exists (trs # res <- Vundef).
             split.
             ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial.
-               rewrite eval_addressing_preserved with (ge1 := ge).
-               assumption.
-               exact symbols_preserved.
+               all: rewrite eval_addressing_preserved with (ge1 := ge).
+               all: auto using symbols_preserved.
             ** apply assign_above; auto.
         + exists (trs # res <- Vundef).
           split.
           * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial.
-            rewrite eval_addressing_preserved with (ge1 := ge).
-            assumption.
-            exact symbols_preserved.
+            all: rewrite eval_addressing_preserved with (ge1 := ge).
+            all: auto using symbols_preserved.
           * apply assign_above; auto.
     Qed.
 
-- 
cgit