diff options
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/armV8.sail | 2 | ||||
| -rw-r--r-- | aarch64_small/armV8_A64_sys_regs.sail | 3 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras_embed.lem | 7 |
3 files changed, 5 insertions, 7 deletions
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail index 4b7323f6..d8ee0bbe 100644 --- a/aarch64_small/armV8.sail +++ b/aarch64_small/armV8.sail @@ -125,7 +125,7 @@ function clause execute (TMStart(t)) = { } } -/* external */ val TMCommitEffect : unit -> unit effect {barr} +/* external */ val "TMCommitEffect" : unit -> unit effect {barr} /* TCOMMIT - dummy decoding */ val decodeTMCommit : unit -> option(ast) effect pure diff --git a/aarch64_small/armV8_A64_sys_regs.sail b/aarch64_small/armV8_A64_sys_regs.sail index 36f7c3f6..20aa4a5c 100644 --- a/aarch64_small/armV8_A64_sys_regs.sail +++ b/aarch64_small/armV8_A64_sys_regs.sail @@ -176,8 +176,7 @@ register SCTLR_EL3 : SCTLR_type /* System Control Register (EL3) */ /* CP: added coercion from SCTLR_EL1_type to SCTLR_type for the SCTLR function */ -val cast SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type - +val cast "SCTLR_EL1_type_to_SCTLR_type" : SCTLR_EL1_type -> SCTLR_type bitfield TCR_EL1_type : bits(64) = { diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem index 86570fc4..6b871344 100644 --- a/aarch64_small/armV8_extras_embed.lem +++ b/aarch64_small/armV8_extras_embed.lem @@ -51,9 +51,8 @@ let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST let DataSynchronizationBarrier_All () = barrier Barrier_DSB let InstructionSynchronizationBarrier () = barrier Barrier_ISB -val TMCommitEffect : unit -> M unit +val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e let TMCommitEffect () = barrier Barrier_TM_COMMIT -let duplicate_bits (Vector bits start direction,len) = - let bits' = repeat bits len in - Vector bits' start direction +val SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type +let SCTLR_EL1_type_to_SCTLR_type <| SCTLR_EL1_type_SCTLR_EL1_type_chunk_0 = x |> = <| SCTLR_type_SCTLR_type_chunk_0 = x |> |