diff options
| -rw-r--r-- | aarch64_small/aarch64_regfp.sail | 31 | ||||
| -rw-r--r-- | aarch64_small/armV8_common_lib.sail | 108 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras.lem | 36 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras_embed.lem | 67 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras_embed_sequential.lem | 69 | ||||
| -rw-r--r-- | lib/regfp.sail | 59 | ||||
| -rw-r--r-- | src/gen_lib/sail2_deep_shallow_convert.lem | 68 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 63 | ||||
| -rw-r--r-- | src/lem_interp/sail2_instr_kinds.lem | 175 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 4 | ||||
| -rw-r--r-- | src/toFromInterp_backend.ml | 8 |
11 files changed, 443 insertions, 245 deletions
diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail index ce155f0a..be4a2cba 100644 --- a/aarch64_small/aarch64_regfp.sail +++ b/aarch64_small/aarch64_regfp.sail @@ -223,22 +223,25 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst }, (ClearExclusiveMonitor(imm)) => (), /*ClearExclusiveLocal*/ (Barrier(op,domain,types)) => { + let (dom, typ) = + (match domain { + MBReqDomain_Nonshareable => A64_NonShare + MBReqDomain_InnerShareable => A64_InnerShare + MBReqDomain_OuterShareable => A64_OuterShare + MBReqDomain_FullSystem => A64_FullShare + }, + match types { + MBReqTypes_Reads => A64_barrier_LD + MBReqTypes_Writes => A64_barrier_ST + MBReqTypes_All => A64_barrier_all + }) + in { ik = match op { - MemBarrierOp_DSB => - match types { - MBReqTypes_Reads => IK_barrier(Barrier_DSB_LD), - MBReqTypes_Writes => IK_barrier(Barrier_DSB_ST), - MBReqTypes_All => IK_barrier(Barrier_DSB) - }, - MemBarrierOp_DMB => - match types { - MBReqTypes_Reads => IK_barrier(Barrier_DMB_LD), - MBReqTypes_Writes => IK_barrier(Barrier_DMB_ST), - MBReqTypes_All => IK_barrier(Barrier_DMB) - }, - MemBarrierOp_ISB => - IK_barrier(Barrier_ISB) + MemBarrierOp_DSB => IK_barrier(Barrier_DSB (dom, typ)) + MemBarrierOp_DMB => IK_barrier(Barrier_DMB (dom, typ)) + MemBarrierOp_ISB => IK_barrier(Barrier_ISB) }; + } }, (DataCache(t,dc_op)) => { diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail index b758b28e..d3d82c6d 100644 --- a/aarch64_small/armV8_common_lib.sail +++ b/aarch64_small/armV8_common_lib.sail @@ -563,45 +563,101 @@ function BigEndianReverse (value) = { /** FUNCTION:shared/functions/memory/DataMemoryBarrier */ -/* external */ val DataMemoryBarrier_Reads : unit -> unit effect {barr} -function DataMemoryBarrier_Reads () = __barrier(Barrier_DMB_LD) -/* external */ val DataMemoryBarrier_Writes : unit -> unit effect {barr} -function DataMemoryBarrier_Writes () = __barrier(Barrier_DMB_ST) -/* external */ val DataMemoryBarrier_All : unit -> unit effect {barr} -function DataMemoryBarrier_All () = __barrier(Barrier_DMB) +/* external */ val DataMemoryBarrier_NonShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_NonShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_NonShAll : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_InnerShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_InnerShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_InnerShAll : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_OuterShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_OuterShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_OuterShAll : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_FullShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_FullShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_FullShAll : unit -> unit effect {barr} + +function DataMemoryBarrier_NonShReads = __barrier(Barrier_DMB (A64_NonShare, A64_barrier_LD)) +function DataMemoryBarrier_NonShWrites = __barrier(Barrier_DMB (A64_NonShare, A64_barrier_ST)) +function DataMemoryBarrier_NonShAll = __barrier(Barrier_DMB (A64_NonShare, A64_barrier_all)) +function DataMemoryBarrier_InnerShReads = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +function DataMemoryBarrier_InnerShWrites = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +function DataMemoryBarrier_InnerShAll = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_all)) +function DataMemoryBarrier_OuterShReads = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +function DataMemoryBarrier_OuterShWrites = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +function DataMemoryBarrier_OuterShAll = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_all)) +function DataMemoryBarrier_FullShReads = __barrier(Barrier_DMB (A64_FullShare, A64_barrier_LD)) +function DataMemoryBarrier_FullShWrites = __barrier(Barrier_DMB (A64_FullShare, A64_barrier_ST)) +function DataMemoryBarrier_FullShAll = __barrier(Barrier_DMB (A64_FullShare, A64_barrier_all)) val DataMemoryBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr, escape} function DataMemoryBarrier(domain, types) = { - if domain != MBReqDomain_FullSystem & domain != MBReqDomain_InnerShareable then - not_implemented("DataMemoryBarrier: not MBReqDomain_FullSystem or _InnerShareable"); - - match types { - MBReqTypes_Reads => DataMemoryBarrier_Reads(), - MBReqTypes_Writes => DataMemoryBarrier_Writes(), - MBReqTypes_All => DataMemoryBarrier_All() + match (domain, types) { + (MBReqDomain_Nonshareable, MBReqTypes_Reads) => DataMemoryBarrier_NonShReads() + (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataMemoryBarrier_NonShWrites() + (MBReqDomain_Nonshareable, MBReqTypes_All) => DataMemoryBarrier_NonShAll() + + (MBReqDomain_InnerShareable, MBReqTypes_Reads) => DataMemoryBarrier_InnerShReads() + (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataMemoryBarrier_InnerShWrites() + (MBReqDomain_InnerShareable, MBReqTypes_All) => DataMemoryBarrier_InnerShAll() + + (MBReqDomain_OuterShareable, MBReqTypes_Reads) => DataMemoryBarrier_OuterShReads() + (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataMemoryBarrier_OuterShWrites() + (MBReqDomain_OuterShareable, MBReqTypes_All) => DataMemoryBarrier_OuterShAll() + + (MBReqDomain_FullSystem, MBReqTypes_Reads) => DataMemoryBarrier_FullShReads() + (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataMemoryBarrier_FullShWrites() + (MBReqDomain_FullSystem, MBReqTypes_All) => DataMemoryBarrier_FullShAll() }; } /** FUNCTION:shared/functions/memory/DataSynchronizationBarrier */ -/* external */ val DataSynchronizationBarrier_Reads : unit -> unit effect {barr} -function DataSynchronizationBarrier_Reads () = __barrier(Barrier_DSB_LD) -/* external */ val DataSynchronizationBarrier_Writes : unit -> unit effect {barr} -function DataSynchronizationBarrier_Writes () = __barrier(Barrier_DSB_ST) -/* external */ val DataSynchronizationBarrier_All : unit -> unit effect {barr} -function DataSynchronizationBarrier_All () = __barrier(Barrier_DSB) +/* external */ val DataSynchronizationBarrier_NonShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_NonShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_NonShAll : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_InnerShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_InnerShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_InnerShAll : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_OuterShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_OuterShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_OuterShAll : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_FullShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_FullShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_FullShAll : unit -> unit effect {barr} + +function DataSynchronizationBarrier_NonShReads = __barrier(Barrier_DSB (A64_NonShare, A64_barrier_LD)) +function DataSynchronizationBarrier_NonShWrites = __barrier(Barrier_DSB (A64_NonShare, A64_barrier_ST)) +function DataSynchronizationBarrier_NonShAll = __barrier(Barrier_DSB (A64_NonShare, A64_barrier_all)) +function DataSynchronizationBarrier_InnerShReads = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +function DataSynchronizationBarrier_InnerShWrites = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +function DataSynchronizationBarrier_InnerShAll = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_all)) +function DataSynchronizationBarrier_OuterShReads = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +function DataSynchronizationBarrier_OuterShWrites = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +function DataSynchronizationBarrier_OuterShAll = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_all)) +function DataSynchronizationBarrier_FullShReads = __barrier(Barrier_DSB (A64_FullShare, A64_barrier_LD)) +function DataSynchronizationBarrier_FullShWrites = __barrier(Barrier_DSB (A64_FullShare, A64_barrier_ST)) +function DataSynchronizationBarrier_FullShAll = __barrier(Barrier_DSB (A64_FullShare, A64_barrier_all)) val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr,escape} function DataSynchronizationBarrier(domain, types) = { - if domain != MBReqDomain_FullSystem then - not_implemented("DataSynchronizationBarrier: not MBReqDomain_FullSystem"); - - match types { - MBReqTypes_Reads => DataSynchronizationBarrier_Reads(), - MBReqTypes_Writes => DataSynchronizationBarrier_Writes(), - MBReqTypes_All => DataSynchronizationBarrier_All() + match (domain, types) { + (MBReqDomain_Nonshareable, MBReqTypes_Reads) => DataSynchronizationBarrier_NonShReads() + (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataSynchronizationBarrier_NonShWrites() + (MBReqDomain_Nonshareable, MBReqTypes_All) => DataSynchronizationBarrier_NonShAll() + + (MBReqDomain_InnerShareable, MBReqTypes_Reads) => DataSynchronizationBarrier_InnerShReads() + (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_InnerShWrites() + (MBReqDomain_InnerShareable, MBReqTypes_All) => DataSynchronizationBarrier_InnerShAll() + + (MBReqDomain_OuterShareable, MBReqTypes_Reads) => DataSynchronizationBarrier_OuterShReads() + (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_OuterShWrites() + (MBReqDomain_OuterShareable, MBReqTypes_All) => DataSynchronizationBarrier_OuterShAll() + + (MBReqDomain_FullSystem, MBReqTypes_Reads) => DataSynchronizationBarrier_FullShReads() + (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataSynchronizationBarrier_FullShWrites() + (MBReqDomain_FullSystem, MBReqTypes_All) => DataSynchronizationBarrier_FullShAll() }; } diff --git a/aarch64_small/armV8_extras.lem b/aarch64_small/armV8_extras.lem index 9a187ecb..da48c836 100644 --- a/aarch64_small/armV8_extras.lem +++ b/aarch64_small/armV8_extras.lem @@ -65,13 +65,33 @@ let aArch64_excl_res : excl_res = Just ("speculate_exclusive_success", (ER (Just f))) let aArch64_barrier_functions = - [ ("DataMemoryBarrier_Reads", Barrier_DMB_LD); - ("DataMemoryBarrier_Writes", Barrier_DMB_ST); - ("DataMemoryBarrier_All", Barrier_DMB); - ("DataSynchronizationBarrier_Reads", Barrier_DSB_LD); - ("DataSynchronizationBarrier_Writes", Barrier_DSB_ST); - ("DataSynchronizationBarrier_All", Barrier_DSB); - ("InstructionSynchronizationBarrier", Barrier_ISB); + [ ("DataMemoryBarrier_NonShReads", Barrier_DMB (A64_NonShare, A64_barrier_LD)); + ("DataMemoryBarrier_NonShWrites", Barrier_DMB (A64_NonShare, A64_barrier_ST)); + ("DataMemoryBarrier_NonShAll", Barrier_DMB (A64_NonShare, A64_barrier_all)); + ("DataMemoryBarrier_InnerShReads", Barrier_DMB (A64_InnerShare, A64_barrier_LD)); + ("DataMemoryBarrier_InnerShWrites", Barrier_DMB (A64_InnerShare, A64_barrier_ST)); + ("DataMemoryBarrier_InnerShAll", Barrier_DMB (A64_InnerShare, A64_barrier_all)); + ("DataMemoryBarrier_OuterShReads", Barrier_DMB (A64_OuterShare, A64_barrier_LD)); + ("DataMemoryBarrier_OuterShWrites", Barrier_DMB (A64_OuterShare, A64_barrier_ST)); + ("DataMemoryBarrier_OuterShAll", Barrier_DMB (A64_OuterShare, A64_barrier_all)); + ("DataMemoryBarrier_FullShReads", Barrier_DMB (A64_FullShare, A64_barrier_LD)); + ("DataMemoryBarrier_FullShWrites", Barrier_DMB (A64_FullShare, A64_barrier_ST)); + ("DataMemoryBarrier_FullShAll", Barrier_DMB (A64_FullShare, A64_barrier_all)); - ("TMCommitEffect", Barrier_TM_COMMIT); + ("DataSynchronizationBarrier_NonShReads", Barrier_DSB (A64_NonShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_NonShWrites", Barrier_DSB (A64_NonShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_NonShAll", Barrier_DSB (A64_NonShare, A64_barrier_all)); + ("DataSynchronizationBarrier_InnerShReads", Barrier_DSB (A64_InnerShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_InnerShWrites", Barrier_DSB (A64_InnerShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_InnerShAll", Barrier_DSB (A64_InnerShare, A64_barrier_all)); + ("DataSynchronizationBarrier_OuterShReads", Barrier_DSB (A64_OuterShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_OuterShWrites", Barrier_DSB (A64_OuterShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_OuterShAll", Barrier_DSB (A64_OuterShare, A64_barrier_all)); + ("DataSynchronizationBarrier_FullShReads", Barrier_DSB (A64_FullShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_FullShWrites", Barrier_DSB (A64_FullShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_FullShAll", Barrier_DSB (A64_FullShare, A64_barrier_all)); + + ("InstructionSynchronizationBarrier", Barrier_ISB ()); + + ("TMCommitEffect", Barrier_TM_COMMIT ()); ] diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem index c5a1b8bc..54f9fc8a 100644 --- a/aarch64_small/armV8_extras_embed.lem +++ b/aarch64_small/armV8_extras_embed.lem @@ -43,24 +43,61 @@ let wMem_Val_ATOMIC_ORDERED addr size v = write_mem Write_exclusive_release () a let speculate_exclusive_success () = excl_result () -val DataMemoryBarrier_Reads : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataMemoryBarrier_Writes : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataMemoryBarrier_All : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_Reads : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_Writes : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_All : forall 'rv 'e. unit -> monad 'rv unit 'e -val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataMemoryBarrier_NonShReads () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_LD)) +let DataMemoryBarrier_NonShWrites () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_ST)) +let DataMemoryBarrier_NonShAll () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_all)) +let DataMemoryBarrier_InnerShReads () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +let DataMemoryBarrier_InnerShWrites () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +let DataMemoryBarrier_InnerShAll () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_all)) +let DataMemoryBarrier_OuterShReads () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +let DataMemoryBarrier_OuterShWrites () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +let DataMemoryBarrier_OuterShAll () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_all)) +let DataMemoryBarrier_FullShReads () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_LD)) +let DataMemoryBarrier_FullShWrites () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_ST)) +let DataMemoryBarrier_FullShAll () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_all)) + +val DataSynchronizationBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataSynchronizationBarrier_NonShReads () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_LD)) +let DataSynchronizationBarrier_NonShWrites () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_ST)) +let DataSynchronizationBarrier_NonShAll () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_all)) +let DataSynchronizationBarrier_InnerShReads () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +let DataSynchronizationBarrier_InnerShWrites () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +let DataSynchronizationBarrier_InnerShAll () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_all)) +let DataSynchronizationBarrier_OuterShReads () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +let DataSynchronizationBarrier_OuterShWrites () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +let DataSynchronizationBarrier_OuterShAll () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_all)) +let DataSynchronizationBarrier_FullShReads () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_LD)) +let DataSynchronizationBarrier_FullShWrites () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_ST)) +let DataSynchronizationBarrier_FullShAll () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_all)) -let DataMemoryBarrier_Reads () = barrier Barrier_DMB_LD -let DataMemoryBarrier_Writes () = barrier Barrier_DMB_ST -let DataMemoryBarrier_All () = barrier Barrier_DMB -let DataSynchronizationBarrier_Reads () = barrier Barrier_DSB_LD -let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST -let DataSynchronizationBarrier_All () = barrier Barrier_DSB -let InstructionSynchronizationBarrier () = barrier Barrier_ISB +val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +let InstructionSynchronizationBarrier () = barrier (Barrier_ISB ()) val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e -let TMCommitEffect () = barrier Barrier_TM_COMMIT +let TMCommitEffect () = barrier (Barrier_TM_COMMIT ()) 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 |> diff --git a/aarch64_small/armV8_extras_embed_sequential.lem b/aarch64_small/armV8_extras_embed_sequential.lem index d2bb8330..91494238 100644 --- a/aarch64_small/armV8_extras_embed_sequential.lem +++ b/aarch64_small/armV8_extras_embed_sequential.lem @@ -35,24 +35,61 @@ let wMem_Val_ATOMIC (_,v) = write_mem_val v >>= fun b -> return (if b then B0 el let speculate_exclusive_success () = excl_result () >>= fun b -> return (if b then B1 else B0) -val DataMemoryBarrier_Reads : unit -> M unit -val DataMemoryBarrier_Writes : unit -> M unit -val DataMemoryBarrier_All : unit -> M unit -val DataSynchronizationBarrier_Reads : unit -> M unit -val DataSynchronizationBarrier_Writes : unit -> M unit -val DataSynchronizationBarrier_All : unit -> M unit -val InstructionSynchronizationBarrier : unit -> M unit - -let DataMemoryBarrier_Reads () = barrier Barrier_DMB_LD -let DataMemoryBarrier_Writes () = barrier Barrier_DMB_ST -let DataMemoryBarrier_All () = barrier Barrier_DMB -let DataSynchronizationBarrier_Reads () = barrier Barrier_DSB_LD -let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST -let DataSynchronizationBarrier_All () = barrier Barrier_DSB -let InstructionSynchronizationBarrier () = barrier Barrier_ISB +val DataMemoryBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataMemoryBarrier_NonShReads () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_LD)) +let DataMemoryBarrier_NonShWrites () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_ST)) +let DataMemoryBarrier_NonShAll () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_all)) +let DataMemoryBarrier_InnerShReads () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +let DataMemoryBarrier_InnerShWrites () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +let DataMemoryBarrier_InnerShAll () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_all)) +let DataMemoryBarrier_OuterShReads () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +let DataMemoryBarrier_OuterShWrites () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +let DataMemoryBarrier_OuterShAll () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_all)) +let DataMemoryBarrier_FullShReads () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_LD)) +let DataMemoryBarrier_FullShWrites () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_ST)) +let DataMemoryBarrier_FullShAll () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_all)) + +val DataSynchronizationBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataSynchronizationBarrier_NonShReads () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_LD)) +let DataSynchronizationBarrier_NonShWrites () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_ST)) +let DataSynchronizationBarrier_NonShAll () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_all)) +let DataSynchronizationBarrier_InnerShReads () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +let DataSynchronizationBarrier_InnerShWrites () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +let DataSynchronizationBarrier_InnerShAll () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_all)) +let DataSynchronizationBarrier_OuterShReads () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +let DataSynchronizationBarrier_OuterShWrites () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +let DataSynchronizationBarrier_OuterShAll () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_all)) +let DataSynchronizationBarrier_FullShReads () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_LD)) +let DataSynchronizationBarrier_FullShWrites () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_ST)) +let DataSynchronizationBarrier_FullShAll () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_all)) + +val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +let InstructionSynchronizationBarrier () = barrier (Barrier_ISB ()) val TMCommitEffect : unit -> M unit -let TMCommitEffect () = barrier Barrier_TM_COMMIT +let TMCommitEffect () = barrier (Barrier_TM_COMMIT ()) let duplicate_bits (Vector bits start direction,len) = let bits' = repeat bits len in diff --git a/lib/regfp.sail b/lib/regfp.sail index da9c11d6..070ff524 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -60,31 +60,40 @@ enum write_kind = { Write_X86_locked } -enum barrier_kind = { - Barrier_Sync, - Barrier_LwSync, - Barrier_Eieio, - Barrier_Isync, - Barrier_DMB, - Barrier_DMB_ST, - Barrier_DMB_LD, - Barrier_DSB, - Barrier_DSB_ST, - Barrier_DSB_LD, - Barrier_ISB, - Barrier_MIPS_SYNC, - Barrier_RISCV_rw_rw, - Barrier_RISCV_r_rw, - Barrier_RISCV_r_r, - Barrier_RISCV_rw_w, - Barrier_RISCV_w_w, - Barrier_RISCV_w_rw, - Barrier_RISCV_rw_r, - Barrier_RISCV_r_w, - Barrier_RISCV_w_r, - Barrier_RISCV_tso, - Barrier_RISCV_i, - Barrier_x86_MFENCE +enum a64_barrier_domain = { + A64_FullShare, + A64_InnerShare, + A64_OuterShare, + A64_NonShare +} + +enum a64_barrier_type = { + A64_barrier_all, + A64_barrier_LD, + A64_barrier_ST +} + +union barrier_kind = { + Barrier_Sync : unit, + Barrier_LwSync : unit, + Barrier_Eieio : unit, + Barrier_Isync : unit, + Barrier_DMB : (a64_barrier_domain, a64_barrier_type), + Barrier_DSB : (a64_barrier_domain, a64_barrier_type), + Barrier_ISB : unit, + Barrier_MIPS_SYNC : unit, + Barrier_RISCV_rw_rw : unit, + Barrier_RISCV_r_rw : unit, + Barrier_RISCV_r_r : unit, + Barrier_RISCV_rw_w : unit, + Barrier_RISCV_w_w : unit, + Barrier_RISCV_w_rw : unit, + Barrier_RISCV_rw_r : unit, + Barrier_RISCV_r_w : unit, + Barrier_RISCV_w_r : unit, + Barrier_RISCV_tso : unit, + Barrier_RISCV_i : unit, + Barrier_x86_MFENCE : unit } enum trans_kind = { diff --git a/src/gen_lib/sail2_deep_shallow_convert.lem b/src/gen_lib/sail2_deep_shallow_convert.lem index b963e537..2e3543b4 100644 --- a/src/gen_lib/sail2_deep_shallow_convert.lem +++ b/src/gen_lib/sail2_deep_shallow_convert.lem @@ -455,17 +455,61 @@ instance (ToFromInterpValue write_kind) end +let a64_barrier_domainToInterpValue = function + | A64_FullShare -> + V_ctor (Id_aux (Id "A64_FullShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 0) (toInterpValue ()) + | A64_InnerShare -> + V_ctor (Id_aux (Id "A64_InnerShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 1) (toInterpValue ()) + | A64_OuterShare -> + V_ctor (Id_aux (Id "A64_OuterShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 2) (toInterpValue ()) + | A64_NonShare -> + V_ctor (Id_aux (Id "A64_NonShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 3) (toInterpValue ()) +end +let rec a64_barrier_domainFromInterpValue v = match v with + | V_ctor (Id_aux (Id "A64_FullShare") _) _ _ v -> A64_FullShare + | V_ctor (Id_aux (Id "A64_InnerShare") _) _ _ v -> A64_InnerShare + | V_ctor (Id_aux (Id "A64_OuterShare") _) _ _ v -> A64_OuterShare + | V_ctor (Id_aux (Id "A64_NonShare") _) _ _ v -> A64_NonShare + | V_tuple [v] -> a64_barrier_domainFromInterpValue v + | v -> failwith ("fromInterpValue a64_barrier_domain: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue a64_barrier_domain) + let toInterpValue = a64_barrier_domainToInterpValue + let fromInterpValue = a64_barrier_domainFromInterpValue +end + +let a64_barrier_typeToInterpValue = function + | A64_barrier_all -> + V_ctor (Id_aux (Id "A64_barrier_all") Unknown) (T_id "a64_barrier_type") (C_Enum 0) (toInterpValue ()) + | A64_barrier_LD -> + V_ctor (Id_aux (Id "A64_barrier_LD") Unknown) (T_id "a64_barrier_type") (C_Enum 1) (toInterpValue ()) + | A64_barrier_ST -> + V_ctor (Id_aux (Id "A64_barrier_ST") Unknown) (T_id "a64_barrier_type") (C_Enum 2) (toInterpValue ()) +end +let rec a64_barrier_typeFromInterpValue v = match v with + | V_ctor (Id_aux (Id "A64_barrier_all") _) _ _ v -> A64_barrier_all + | V_ctor (Id_aux (Id "A64_barrier_LD") _) _ _ v -> A64_barrier_LD + | V_ctor (Id_aux (Id "A64_barrier_ST") _) _ _ v -> A64_barrier_ST + | V_tuple [v] -> a64_barrier_typeFromInterpValue v + | v -> failwith ("fromInterpValue a64_barrier_type: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue a64_barrier_type) + let toInterpValue = a64_barrier_typeToInterpValue + let fromInterpValue = a64_barrier_typeFromInterpValue +end + + let barrier_kindToInterpValue = function | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ()) | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ()) | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ()) | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ()) - | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ()) - | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ()) - | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ()) - | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ()) - | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) - | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) + | Barrier_DMB (dom,typ) -> + V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ)) + | Barrier_DSB (dom,typ) -> + V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ)) | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ()) @@ -482,12 +526,12 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync - | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB - | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST - | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD - | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB - | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST - | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD + | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> + let (dom, typ) = fromInterpValue v in + Barrier_DMB (dom,typ) + | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> + let (dom, typ) = fromInterpValue v in + Barrier_DSB (dom,typ) | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 74e43a8f..3413494e 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -579,74 +579,13 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ -> NIA_indirect_address | _ -> failwith "Register footprint analysis did not return nia of expected type" end in - let readk_to_readk = function - | "Read_plain" -> Read_plain - | "Read_reserve" -> Read_reserve - | "Read_acquire" -> Read_acquire - | "Read_exclusive" -> Read_exclusive - | "Read_exclusive_acquire" -> Read_exclusive_acquire - | "Read_stream" -> Read_stream - | "Read_RISCV_acquire" -> Read_RISCV_acquire - | "Read_RISCV_strong_acquire" -> Read_RISCV_strong_acquire - | "Read_RISCV_reserved" -> Read_RISCV_reserved - | "Read_RISCV_reserved_acquire" -> Read_RISCV_reserved_acquire - | "Read_RISCV_reserved_strong_acquire" -> Read_RISCV_reserved_strong_acquire - | "Read_X86_locked" -> Read_X86_locked - | r -> failwith ("unknown read kind: " ^ r) end in - let writek_to_writek = function - | "Write_plain" -> Write_plain - | "Write_conditional" -> Write_conditional - | "Write_release" -> Write_release - | "Write_exclusive" -> Write_exclusive - | "Write_exclusive_release" -> Write_exclusive_release - | "Write_RISCV_release" -> Write_RISCV_release - | "Write_RISCV_strong_release" -> Write_RISCV_strong_release - | "Write_RISCV_conditional" -> Write_RISCV_conditional - | "Write_RISCV_conditional_release" -> Write_RISCV_conditional_release - | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release - | "Write_X86_locked" -> Write_X86_locked - | w -> failwith ("unknown write kind: " ^ w) end in - let ik_to_ik = function - | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> - IK_barrier (match b with - | "Barrier_Sync" -> Barrier_Sync - | "Barrier_LwSync" -> Barrier_LwSync - | "Barrier_Eieio" -> Barrier_Eieio - | "Barrier_Isync" -> Barrier_Isync - | "Barrier_DMB" -> Barrier_DMB - | "Barrier_DMB_ST" -> Barrier_DMB_ST - | "Barrier_DMB_LD" -> Barrier_DMB_LD - | "Barrier_DSB" -> Barrier_DSB - | "Barrier_DSB_ST" -> Barrier_DSB_ST - | "Barrier_DSB_LD" -> Barrier_DSB_LD - | "Barrier_ISB" -> Barrier_ISB - | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC - | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE - end) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> - IK_mem_read(readk_to_readk r) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> - IK_mem_write(writek_to_writek w) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ - (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ; - (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) -> - IK_mem_rmw(readk_to_readk readk, writek_to_writek writek) - | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ -> - IK_branch - | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> - IK_simple - | _ -> failwith "Analysis returned unexpected instruction kind" - end in let (regs1,regs2,regs3,nias,dia,ik) = (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3, List.map nia_to_nia nias, dia_to_dia dia, - ik_to_ik ik) in + fromInterpValue ik) in ((regs1,regs2,regs3,nias,dia,ik), events) | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end) | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed" diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem index bd3a3eb7..f3cdfbc9 100644 --- a/src/lem_interp/sail2_instr_kinds.lem +++ b/src/lem_interp/sail2_instr_kinds.lem @@ -136,58 +136,86 @@ instance (Show write_kind) end end +type a64_barrier_domain = + A64_FullShare + | A64_InnerShare + | A64_OuterShare + | A64_NonShare + +type a64_barrier_type = + A64_barrier_all + | A64_barrier_LD + | A64_barrier_ST + type barrier_kind = (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + Barrier_Sync of unit | Barrier_LwSync of unit | Barrier_Eieio of unit | Barrier_Isync of unit (* AArch64 barriers *) - | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB - | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB - | Barrier_TM_COMMIT + | Barrier_DMB of (a64_barrier_domain * a64_barrier_type) + | Barrier_DSB of (a64_barrier_domain * a64_barrier_type) + | Barrier_ISB of unit + | Barrier_TM_COMMIT of unit (* MIPS barriers *) - | Barrier_MIPS_SYNC + | Barrier_MIPS_SYNC of unit (* RISC-V barriers *) - | Barrier_RISCV_rw_rw - | Barrier_RISCV_r_rw - | Barrier_RISCV_r_r - | Barrier_RISCV_rw_w - | Barrier_RISCV_w_w - | Barrier_RISCV_w_rw - | Barrier_RISCV_rw_r - | Barrier_RISCV_r_w - | Barrier_RISCV_w_r - | Barrier_RISCV_tso - | Barrier_RISCV_i + | Barrier_RISCV_rw_rw of unit + | Barrier_RISCV_r_rw of unit + | Barrier_RISCV_r_r of unit + | Barrier_RISCV_rw_w of unit + | Barrier_RISCV_w_w of unit + | Barrier_RISCV_w_rw of unit + | Barrier_RISCV_rw_r of unit + | Barrier_RISCV_r_w of unit + | Barrier_RISCV_w_r of unit + | Barrier_RISCV_tso of unit + | Barrier_RISCV_i of unit (* X86 *) - | Barrier_x86_MFENCE + | Barrier_x86_MFENCE of unit +let string_a64_barrier_domain = function + | A64_FullShare -> "A64_FullShare" + | A64_InnerShare -> "A64_InnerShare" + | A64_OuterShare -> "A64_OuterShare" + | A64_NonShare -> "A64_NonShare" +end + +instance (Show a64_barrier_domain) + let show = string_a64_barrier_domain +end + +let string_a64_barrier_type = function + | A64_barrier_all -> "A64_barrier_all" + | A64_barrier_LD -> "A64_barrier_LD" + | A64_barrier_ST -> "A64_barrier_ST" +end + +instance (Show a64_barrier_type) + let show = string_a64_barrier_type +end instance (Show barrier_kind) let show = function - | Barrier_Sync -> "Barrier_Sync" - | Barrier_LwSync -> "Barrier_LwSync" - | Barrier_Eieio -> "Barrier_Eieio" - | Barrier_Isync -> "Barrier_Isync" - | Barrier_DMB -> "Barrier_DMB" - | Barrier_DMB_ST -> "Barrier_DMB_ST" - | Barrier_DMB_LD -> "Barrier_DMB_LD" - | Barrier_DSB -> "Barrier_DSB" - | Barrier_DSB_ST -> "Barrier_DSB_ST" - | Barrier_DSB_LD -> "Barrier_DSB_LD" - | Barrier_ISB -> "Barrier_ISB" - | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" - | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" - | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" - | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" - | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" - | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" - | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" - | Barrier_RISCV_w_rw -> "Barrier_RISCV_w_rw" - | Barrier_RISCV_rw_r -> "Barrier_RISCV_rw_r" - | Barrier_RISCV_r_w -> "Barrier_RISCV_r_w" - | Barrier_RISCV_w_r -> "Barrier_RISCV_w_r" - | Barrier_RISCV_tso -> "Barrier_RISCV_tso" - | Barrier_RISCV_i -> "Barrier_RISCV_i" - | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" + | Barrier_Sync () -> "Barrier_Sync" + | Barrier_LwSync () -> "Barrier_LwSync" + | Barrier_Eieio () -> "Barrier_Eieio" + | Barrier_Isync () -> "Barrier_Isync" + | Barrier_DMB (dom,typ) -> "Barrier_DMB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")" + | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")" + | Barrier_ISB () -> "Barrier_ISB" + | Barrier_TM_COMMIT () -> "Barrier_TM_COMMIT" + | Barrier_MIPS_SYNC () -> "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw () -> "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw () -> "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r () -> "Barrier_RISCV_r_r" + | Barrier_RISCV_rw_w () -> "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w () -> "Barrier_RISCV_w_w" + | Barrier_RISCV_w_rw () -> "Barrier_RISCV_w_rw" + | Barrier_RISCV_rw_r () -> "Barrier_RISCV_rw_r" + | Barrier_RISCV_r_w () -> "Barrier_RISCV_r_w" + | Barrier_RISCV_w_r () -> "Barrier_RISCV_w_r" + | Barrier_RISCV_tso () -> "Barrier_RISCV_tso" + | Barrier_RISCV_i () -> "Barrier_RISCV_i" + | Barrier_x86_MFENCE () -> "Barrier_x86_MFENCE" end end @@ -304,32 +332,45 @@ instance (EnumerationType write_kind) end end +instance (EnumerationType a64_barrier_domain) + let toNat = function + | A64_FullShare -> 0 + | A64_InnerShare -> 1 + | A64_OuterShare -> 2 + | A64_NonShare -> 3 + end +end + +instance (EnumerationType a64_barrier_type) + let toNat = function + | A64_barrier_all -> 0 + | A64_barrier_LD -> 1 + | A64_barrier_ST -> 2 + end +end + instance (EnumerationType barrier_kind) let toNat = function - | Barrier_Sync -> 0 - | Barrier_LwSync -> 1 - | Barrier_Eieio ->2 - | Barrier_Isync -> 3 - | Barrier_DMB -> 4 - | Barrier_DMB_ST -> 5 - | Barrier_DMB_LD -> 6 - | Barrier_DSB -> 7 - | Barrier_DSB_ST -> 8 - | Barrier_DSB_LD -> 9 - | Barrier_ISB -> 10 - | Barrier_TM_COMMIT -> 11 - | Barrier_MIPS_SYNC -> 12 - | Barrier_RISCV_rw_rw -> 13 - | Barrier_RISCV_r_rw -> 14 - | Barrier_RISCV_r_r -> 15 - | Barrier_RISCV_rw_w -> 16 - | Barrier_RISCV_w_w -> 17 - | Barrier_RISCV_w_rw -> 18 - | Barrier_RISCV_rw_r -> 19 - | Barrier_RISCV_r_w -> 20 - | Barrier_RISCV_w_r -> 21 - | Barrier_RISCV_tso -> 22 - | Barrier_RISCV_i -> 23 - | Barrier_x86_MFENCE -> 24 + | Barrier_Sync () -> 0 + | Barrier_LwSync () -> 1 + | Barrier_Eieio () -> 2 + | Barrier_Isync () -> 3 + | Barrier_DMB (dom,typ) -> 4 + (toNat dom) + (4 * (toNat typ)) (* 4-15 *) + | Barrier_DSB (dom,typ) -> 16 + (toNat dom) + (4 * (toNat typ)) (* 16-27 *) + | Barrier_ISB () -> 28 + | Barrier_TM_COMMIT () -> 29 + | Barrier_MIPS_SYNC () -> 30 + | Barrier_RISCV_rw_rw () -> 31 + | Barrier_RISCV_r_rw () -> 32 + | Barrier_RISCV_r_r () -> 33 + | Barrier_RISCV_rw_w () -> 34 + | Barrier_RISCV_w_w () -> 35 + | Barrier_RISCV_w_rw () -> 36 + | Barrier_RISCV_rw_r () -> 37 + | Barrier_RISCV_r_w () -> 38 + | Barrier_RISCV_w_r () -> 39 + | Barrier_RISCV_tso () -> 40 + | Barrier_RISCV_i () -> 41 + | Barrier_x86_MFENCE () -> 42 end end diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 4890b8d1..2d8b282e 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1129,6 +1129,8 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -1201,6 +1203,8 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml index 49739c30..b787fad4 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -141,6 +141,8 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = begin match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -199,6 +201,8 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = end | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_domain", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_type", _), _, _) -> empty | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty @@ -296,6 +300,8 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = begin match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -349,6 +355,8 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = end | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_domain", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_type", _), _, _) -> empty | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty |