From b4242a3ae864a5b50b78e869e35f538cf43b5fdd Mon Sep 17 00:00:00 2001
From: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
Date: Tue, 26 Nov 2019 11:50:02 +1100
Subject: [PATCH] asmrefine: arch-split for machine word size.

Arch-split memory operations used when translating graph-lang.
---
 tools/asmrefine/ARM/ArchSetup.thy     | 27 +++++++++++++++++++++++++++
 tools/asmrefine/ARM_HYP/ArchSetup.thy | 27 +++++++++++++++++++++++++++
 tools/asmrefine/CommonOps.thy         |  2 +-
 tools/asmrefine/RISCV64/ArchSetup.thy | 27 +++++++++++++++++++++++++++
 tools/asmrefine/X64/ArchSetup.thy     | 27 +++++++++++++++++++++++++++
 5 files changed, 109 insertions(+), 1 deletion(-)
 create mode 100644 tools/asmrefine/ARM/ArchSetup.thy
 create mode 100644 tools/asmrefine/ARM_HYP/ArchSetup.thy
 create mode 100644 tools/asmrefine/RISCV64/ArchSetup.thy
 create mode 100644 tools/asmrefine/X64/ArchSetup.thy

diff --git a/tools/asmrefine/ARM/ArchSetup.thy b/tools/asmrefine/ARM/ArchSetup.thy
new file mode 100644
index 000000000..481637241
--- /dev/null
+++ b/tools/asmrefine/ARM/ArchSetup.thy
@@ -0,0 +1,27 @@
+theory ArchSetup
+imports
+  "CLib.CTranslationNICTA"
+begin
+
+abbreviation (input)
+  "(arch_load_machine_word
+      (load_word32 :: word32 mem_read)
+      (load_word64 :: word64 mem_read)
+      :: machine_word mem_read)
+    \<equiv> load_word32"
+
+abbreviation (input)
+  "(arch_store_machine_word
+      (store_word32 :: word32 mem_upd)
+      (store_word64 :: word64 mem_upd)
+      :: machine_word mem_upd)
+    \<equiv> store_word32"
+
+abbreviation (input)
+  "(arch_machine_word_constructor
+      (from_word32 :: word32 \<Rightarrow> 'a)
+      (from_word64 :: word64 \<Rightarrow> 'a)
+      :: machine_word \<Rightarrow> 'a)
+    \<equiv> from_word32"
+
+end
\ No newline at end of file
diff --git a/tools/asmrefine/ARM_HYP/ArchSetup.thy b/tools/asmrefine/ARM_HYP/ArchSetup.thy
new file mode 100644
index 000000000..481637241
--- /dev/null
+++ b/tools/asmrefine/ARM_HYP/ArchSetup.thy
@@ -0,0 +1,27 @@
+theory ArchSetup
+imports
+  "CLib.CTranslationNICTA"
+begin
+
+abbreviation (input)
+  "(arch_load_machine_word
+      (load_word32 :: word32 mem_read)
+      (load_word64 :: word64 mem_read)
+      :: machine_word mem_read)
+    \<equiv> load_word32"
+
+abbreviation (input)
+  "(arch_store_machine_word
+      (store_word32 :: word32 mem_upd)
+      (store_word64 :: word64 mem_upd)
+      :: machine_word mem_upd)
+    \<equiv> store_word32"
+
+abbreviation (input)
+  "(arch_machine_word_constructor
+      (from_word32 :: word32 \<Rightarrow> 'a)
+      (from_word64 :: word64 \<Rightarrow> 'a)
+      :: machine_word \<Rightarrow> 'a)
+    \<equiv> from_word32"
+
+end
\ No newline at end of file
diff --git a/tools/asmrefine/CommonOps.thy b/tools/asmrefine/CommonOps.thy
index e8fc345fd..a75cbfd71 100644
--- a/tools/asmrefine/CommonOps.thy
+++ b/tools/asmrefine/CommonOps.thy
@@ -12,7 +12,7 @@ theory CommonOps
 
 imports "CLib.CTranslationNICTA"
   "GlobalsSwap"
-
+  "$L4V_ARCH/ArchSetup"
 begin
 
 text \<open>Additional constants needed to make conversion to and from the graph lang easy\<close>
diff --git a/tools/asmrefine/RISCV64/ArchSetup.thy b/tools/asmrefine/RISCV64/ArchSetup.thy
new file mode 100644
index 000000000..8df048a76
--- /dev/null
+++ b/tools/asmrefine/RISCV64/ArchSetup.thy
@@ -0,0 +1,27 @@
+theory ArchSetup
+imports
+  "CLib.CTranslationNICTA"
+begin
+
+abbreviation (input)
+  "(arch_load_machine_word
+      (load_word32 :: word32 mem_read)
+      (load_word64 :: word64 mem_read)
+      :: machine_word mem_read)
+    \<equiv> load_word64"
+
+abbreviation (input)
+  "(arch_store_machine_word
+      (store_word32 :: word32 mem_upd)
+      (store_word64 :: word64 mem_upd)
+      :: machine_word mem_upd)
+    \<equiv> store_word64"
+
+abbreviation (input)
+  "(arch_machine_word_constructor
+      (from_word32 :: word32 \<Rightarrow> 'a)
+      (from_word64 :: word64 \<Rightarrow> 'a)
+      :: machine_word \<Rightarrow> 'a)
+    \<equiv> from_word64"
+
+end
\ No newline at end of file
diff --git a/tools/asmrefine/X64/ArchSetup.thy b/tools/asmrefine/X64/ArchSetup.thy
new file mode 100644
index 000000000..8df048a76
--- /dev/null
+++ b/tools/asmrefine/X64/ArchSetup.thy
@@ -0,0 +1,27 @@
+theory ArchSetup
+imports
+  "CLib.CTranslationNICTA"
+begin
+
+abbreviation (input)
+  "(arch_load_machine_word
+      (load_word32 :: word32 mem_read)
+      (load_word64 :: word64 mem_read)
+      :: machine_word mem_read)
+    \<equiv> load_word64"
+
+abbreviation (input)
+  "(arch_store_machine_word
+      (store_word32 :: word32 mem_upd)
+      (store_word64 :: word64 mem_upd)
+      :: machine_word mem_upd)
+    \<equiv> store_word64"
+
+abbreviation (input)
+  "(arch_machine_word_constructor
+      (from_word32 :: word32 \<Rightarrow> 'a)
+      (from_word64 :: word64 \<Rightarrow> 'a)
+      :: machine_word \<Rightarrow> 'a)
+    \<equiv> from_word64"
+
+end
\ No newline at end of file