asmrefine: arch-split for machine word size.
Arch-split memory operations used when translating graph-lang.
This commit is contained in:
parent
89a53c0818
commit
b4242a3ae8
|
@ -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
|
|
@ -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
|
|
@ -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>
|
||||
|
|
|
@ -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
|
|
@ -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
|
Loading…
Reference in New Issue