Skip to content

Commit

Permalink
aarch64 asmrefine: copy ArchSetup from RISCV64
Browse files Browse the repository at this point in the history
Signed-off-by: Rafal Kolanski <[email protected]>
  • Loading branch information
Xaphiosis authored and lsf37 committed Oct 8, 2023
1 parent ad24d95 commit 01ec36b
Showing 1 changed file with 33 additions and 0 deletions.
33 changes: 33 additions & 0 deletions tools/asmrefine/AARCH64/ArchSetup.thy
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)

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 comments on commit 01ec36b

Please sign in to comment.