diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/armv8_extras.lem | 53 | ||||
| -rw-r--r-- | src/gen_lib/power_extras.lem | 47 |
2 files changed, 0 insertions, 100 deletions
diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem deleted file mode 100644 index abab2163..00000000 --- a/src/gen_lib/armv8_extras.lem +++ /dev/null @@ -1,53 +0,0 @@ -open import Pervasives -open import Sail_impl_base -open import Vector -open import Sail_values -open import Prompt - -val rMem_NORMAL : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) -val rMem_STREAM : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) -val rMem_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) -val rMem_ATOMICL : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) -val rMem_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) - -let rMem_NORMAL (addr,size) = read_memory Read_plain addr size -let rMem_STREAM (addr,size) = read_memory Read_stream addr size -let rMem_ORDERED (addr,size) = read_memory Read_acquire addr size -let rMem_ATOMIC (addr,size) = read_memory Read_exclusive addr size -let rMem_ATOMIC_ORDERED (addr,size) = read_memory Read_exclusive_acquire addr size - -val wMem_Addr_NORMAL : forall 'e. (vector bitU * integer) -> M 'e unit -val wMem_Addr_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit -val wMem_Addr_ATOMIC : forall 'e. (vector bitU * integer) -> M 'e unit -val wMem_Addr_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit - -let wMem_Addr_NORMAL (addr,size) = write_memory_ea Write_plain addr size -let wMem_Addr_ORDERED (addr,size) = write_memory_ea Write_release addr size -let wMem_Addr_ATOMIC (addr,size) = write_memory_ea Write_exclusive addr size -let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_memory_ea Write_exclusive_release addr size - - -val wMem_Val_NORMAL : forall 'e. (integer * vector bitU) -> M 'e unit -val wMem_Val_ATOMIC : forall 'e. (integer * vector bitU) -> M 'e bitU - -let wMem_Val_NORMAL (_,v) = write_memory_val v >>= fun _ -> return () -(* in ARM the status returned is inversed *) -let wMem_Val_ATOMIC (_,v) = write_memory_val v >>= fun b -> return (if b then O else I) - - -val DataMemoryBarrier_Reads : forall 'e. unit -> M 'e unit -val DataMemoryBarrier_Writes : forall 'e. unit -> M 'e unit -val DataMemoryBarrier_All : forall 'e. unit -> M 'e unit -val DataSynchronizationBarrier_Reads : forall 'e. unit -> M 'e unit -val DataSynchronizationBarrier_Writes : forall 'e. unit -> M 'e unit -val DataSynchronizationBarrier_All : forall 'e. unit -> M 'e unit -val InstructionSynchronizationBarrier : forall 'e. unit -> M 'e unit - -let DataMemoryBarrier_Reads () = barrier DMB_LD -let DataMemoryBarrier_Writes () = barrier DMB_ST -let DataMemoryBarrier_All () = barrier DMB -let DataSynchronizationBarrier_Reads () = barrier DSB_LD -let DataSynchronizationBarrier_Writes () = barrier DSB_ST -let DataSynchronizationBarrier_All () = barrier DSB -let InstructionSynchronizationBarrier () = barrier Isync - diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem deleted file mode 100644 index c16b197f..00000000 --- a/src/gen_lib/power_extras.lem +++ /dev/null @@ -1,47 +0,0 @@ -open import Pervasives -open import Sail_impl_base -open import Vector -open import Sail_values -open import Prompt - -val MEMr : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) -val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) - -let MEMr (addr,size) = read_memory Read_plain addr size -let MEMr_reserve (addr,size) = read_memory Read_reserve addr size - - -val MEMw_EA : forall 'e. (vector bitU * integer) -> M 'e unit -val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit - -let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size -let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size - - -val MEMw : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit -val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU - -let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return () -let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b) - - -val I_Sync : forall 'e. unit -> M 'e unit -val H_Sync : forall 'e. unit -> M 'e unit -val LW_Sync : forall 'e. unit -> M 'e unit -val EIEIO_Sync : forall 'e. unit -> M 'e unit - -let I_Sync () = barrier Isync -let H_Sync () = barrier Sync -let LW_Sync () = barrier LwSync -let EIEIO_Sync () = barrier Eieio - -let recalculate_dependency () = footprint - -let trap () = exit "error" -(* this needs to change, but for that we'd have to make the type checker know about trap - * as an effect *) - -val countLeadingZeroes : vector bitU * integer -> integer -let countLeadingZeroes (Vector bits _ _ ,n) = - let (_,bits) = List.splitAt (natFromInteger n) bits in - integerFromNat (List.length (takeWhile ((=) O) bits)) |