diff options
36 files changed, 2887 insertions, 364 deletions
diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail index ce155f0a..884a9e81 100644 --- a/aarch64_small/aarch64_regfp.sail +++ b/aarch64_small/aarch64_regfp.sail @@ -183,7 +183,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (GenerateExceptionEL1(imm)) => not_implemented("GenerateExceptionEL1"), (GenerateExceptionEL2(imm)) => not_implemented("GenerateExceptionEL2"), (GenerateExceptionEL3(imm)) => not_implemented("GenerateExceptionEL3"), - (DebugBreakpoint(comment)) => not_implemented("DebugBreakpoint"), + (DebugBreakpoint(comment)) => not_implemented("DebugBreakpoint"), (ExternalDebugBreakpoint()) => not_implemented("ExternalDebugBreakpoint"), (DebugSwitchToExceptionLevel(target_level)) => not_implemented("DebugSwitchToExceptionLevel"), (MoveSystemImmediate(operand,field)) => @@ -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) : (a64_barrier_domain, a64_barrier_type) = + (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..66f05086 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() }; } @@ -982,7 +1038,7 @@ function Hint_Yield() -> unit = () /** FUNCTION:shared/functions/system/InstructionSynchronizationBarrier */ /* external */ val InstructionSynchronizationBarrier : unit -> unit effect {barr} -function InstructionSynchronizationBarrier () = __barrier(Barrier_ISB) +function InstructionSynchronizationBarrier () = __barrier(Barrier_ISB()) /** FUNCTION:shared/functions/system/InterruptPending */ function InterruptPending () -> boolean = not_implemented_extern("InterruptPending") 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/aarch64_small/prelude.sail b/aarch64_small/prelude.sail index c904aec6..2e5412a5 100644 --- a/aarch64_small/prelude.sail +++ b/aarch64_small/prelude.sail @@ -17,6 +17,7 @@ $include <flow.sail> $include <arith.sail> $include <option.sail> $include <vector_dec.sail> + $include <regfp.sail> infix 7 >> diff --git a/doc/manual.tex b/doc/manual.tex index 1cab3afa..38b14322 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -24,7 +24,7 @@ } \lstdefinelanguage{sail} - { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, + { morekeywords={val,function,mapping,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct, foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint}, keywordstyle={\bf\ttfamily\color{blue}}, diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 9bf47f5b..b9901fc9 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -85,6 +85,78 @@ can drop it and simply write: \mrbfn{my_replicate_bits_three} %included. If we use the wildcard key, then we cannot omit specific %backends to force them to use a definition in Sail. +\subsection{Mappings} +\label{sec:mappings} + +Mappings are a feature of Sail that allow concise expression of +bidirectional relationships between values that are common in ISA +specifications: for example, bit-representations of an enum type or +assembly-language string representations of an instruction AST. + +They are defined similarly to functions, with a \verb|val|-spec and a +definition. Currently, they only work for monomorphic types. + +\begin{center} + \ll{val} \textit{name} \ll{:} \textit{type$_1$} \ll{<->} \textit{type$_2$} +\end{center} + +\begin{center} + \ll{mapping} \textit{name} \ll{=} \verb|{| + \textit{pattern} \ll{<->} \textit{pattern} \ll{,} + \textit{pattern} \ll{<->} \textit{pattern} \ll{,} + $\ldots$ + \verb|}| +\end{center} + +All the functionality of pattern matching, described below, is +available, including guarded patterns: but note that guards apply only +to one side. This sometimes leads to unavoidable duplicated code. + +As a shorthand, you can also specify a mapping and its type +simultaneously. + +\begin{center} + \ll{mapping} \textit{name} \ll{:} \textit{type$_1$} \ll{<->} \textit{type$_2$} \ll{=} \verb|{| + \textit{pattern} \ll{<->} \textit{pattern} \ll{,} + \textit{pattern} \ll{<->} \textit{pattern} \ll{,} + $\ldots$ + \verb|}| +\end{center} + +A simple example from our RISC-V model: + +\begin{lstlisting} +mapping size_bits : word_width <-> bits(2) = { + BYTE <-> 0b00, + HALF <-> 0b01, + WORD <-> 0b10, + DOUBLE <-> 0b11 +} +\end{lstlisting} + +Mappings are used simply by calling them as if they were functions: +type inference will determine in which direction the mapping +runs. (This gives rise to the restriction that the types on either +side of a mapping must be different.) + +\begin{lstlisting} + let width : word_width = size_bits(0b00); + let width : bits(2) = size_bits(BYTE); +\end{lstlisting} + +Mappings are implemented by transforming them at compile time into a +forwards and a backwards function, along with some auxiliary +functions. Once a mapping is declared with a \verb|val|-spec, it can +be implemented by defining these functions manually instead of +defining the mapping as above. These functions and their types are: + +\begin{lstlisting} + val name_forwards : type_1 -> type_2 + val name_backwards : type_2 -> type_1 + val name_forwards_matches : type_1 -> bool + val name_backwards_matches : type_2 -> bool +\end{lstlisting} + \subsection{Numeric Types} \label{sec:numeric} @@ -415,6 +487,44 @@ match ys { } \end{lstlisting} +\paragraph{Matching on strings} + +Unusually, Sail allows strings and concatenations of strings to be +used in pattern-matching. The match operates in a simple left-to-right +fashion. + +\begin{lstlisting} + match s { + "hello" ^ " " ^ "world" => print("matched hello world"), + _ => print("wildcard") + } +\end{lstlisting} + +Note that a string match is always greedy, so + +\begin{lstlisting} + match s { + "hello" ^ s ^ "world" => print("matched hello" ^ s ^ "world"), + "hello" ^ s => print("matched hello" ^ s), + _ => print("wildcard") + } +\end{lstlisting} + +while syntactically valid, will never match the first case. + +String matching is most often used with \emph{mappings}, covered +above, to allow parsing of strings containing, for example, integers: + +\begin{lstlisting} + match s { + "int=" ^ int(x) ^ ";" => x + _ => -1 + } +\end{lstlisting} + +This is intended to be used to parse assembly languages. + + \paragraph{As patterns} Like OCaml, Sail also supports naming parts of patterns using the diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v new file mode 100644 index 00000000..d23ff322 --- /dev/null +++ b/lib/coq/Hoare.v @@ -0,0 +1,810 @@ +Require Import String ZArith. +Require Import Sail2_state_monad Sail2_prompt Sail2_state Sail2_state_monad_lemmas. +Require Import Sail2_state_lemmas. + +(*adhoc_overloading + Monad_Syntax.bind State_monad.bindS*) + +(*section \<open>Hoare logic for the state, exception and nondeterminism monad\<close> + +subsection \<open>Hoare triples\<close> +*) +Definition predS regs := sequential_state regs -> Prop. + +Definition PrePost {Regs A E} (P : predS Regs) (f : monadS Regs A E) (Q : result A E -> predS Regs) : Prop := + (*"\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>"*) + forall s, P s -> (forall r s', List.In (r, s') (f s) -> Q r s'). + +Notation "{{ P }} m {{ Q }}" := (PrePost P m Q). + +(* +lemma PrePostI: + assumes "\<And>s r s'. P s \<Longrightarrow> (r, s') \<in> f s \<Longrightarrow> Q r s'" + shows "PrePost P f Q" + using assms unfolding PrePost_def by auto + +lemma PrePost_elim: + assumes "PrePost P f Q" and "P s" and "(r, s') \<in> f s" + obtains "Q r s'" + using assms by (fastforce simp: PrePost_def) +*) +Lemma PrePost_consequence Regs X E (A P : predS Regs) (f : monadS Regs X E) (B Q : result X E -> predS Regs) : + PrePost A f B -> + (forall s, P s -> A s) -> + (forall v s, B v s -> Q v s) -> + PrePost P f Q. +intros Triple PA BQ. +intros s Pre r s' IN. +specialize (Triple s). +auto. +Qed. + +Lemma PrePost_strengthen_pre Regs X E (A B : predS Regs) (f : monadS Regs X E) (C : result X E -> predS Regs) : + PrePost A f C -> + (forall s, B s -> A s) -> + PrePost B f C. +eauto using PrePost_consequence. +Qed. + +Lemma PrePost_weaken_post Regs X E (A : predS Regs) (f : monadS Regs X E) (B C : result X E -> predS Regs) : + PrePost A f B -> + (forall v s, B v s -> C v s) -> + PrePost A f C. +eauto using PrePost_consequence. +Qed. + +Lemma PrePost_True_post (*[PrePost_atomI, intro, simp]:*) Regs A E (P : predS Regs) (m : monadS Regs A E) : + PrePost P m (fun _ _ => True). +unfold PrePost. auto. +Qed. + +Lemma PrePost_any Regs A E (m : monadS Regs A E) (Q : result A E -> predS Regs) : + PrePost (fun s => forall r s', List.In (r, s') (m s) -> Q r s') m Q. +unfold PrePost. auto. +Qed. + +Lemma PrePost_returnS (*[intro, PrePost_atomI]:*) Regs A E (P : result A E -> predS Regs) (x : A) : + PrePost (P (Value x)) (returnS x) P. +unfold PrePost, returnS. +intros s p r s' IN. +simpl in IN. +destruct IN as [[=] | []]. +subst; auto. +Qed. + +Lemma PrePost_bindS (*[intro, PrePost_compositeI]:*) Regs A B E (m : monadS Regs A E) (f : A -> monadS Regs B E) (P : predS Regs) (Q : result B E -> predS Regs) (R : A -> predS Regs) : + (forall s a s', List.In (Value a, s') (m s) -> PrePost (R a) (f a) Q) -> + (PrePost P m (fun r => match r with Value a => R a | Ex e => Q (Ex e) end)) -> + PrePost P (bindS m f) Q. +intros F M s Pre r s' IN. +destruct (bindS_cases IN) as [(a & a' & s'' & [= ->] & IN' & IN'') | [(e & [= ->] & IN') | (e & a & s'' & [= ->] & IN' & IN'')]]. +* eapply F. apply IN'. specialize (M s Pre (Value a') s'' IN'). apply M. assumption. +* specialize (M _ Pre _ _ IN'). apply M. +* specialize (M _ Pre _ _ IN'). simpl in M. eapply F; eauto. +Qed. + +Lemma PrePost_bindS_ignore Regs A B E (m : monadS Regs A E) (f : monadS Regs B E) (P : predS Regs) (Q : result B E -> predS Regs) (R : predS Regs) : + PrePost R f Q -> + PrePost P m (fun r => match r with Value a => R | Ex e => Q (Ex e) end) -> + PrePost P (bindS m (fun _ => f)) Q. +intros F M. +eapply PrePost_bindS; eauto. +* intros. apply F. +* apply M. +Qed. + +Lemma PrePost_bindS_unit Regs B E (m : monadS Regs unit E) (f : unit -> monadS Regs B E) P Q R : + PrePost R (f tt) Q -> + PrePost P m (fun r => match r with Value a => R | Ex e => Q (Ex e) end) -> + PrePost P (bindS m f) Q. +intros F M. +eapply PrePost_bindS with (R := fun _ => R). +* intros. destruct a. apply F. +* apply M. +Qed. + +Lemma PrePost_readS (*[intro, PrePost_atomI]:*) Regs A E (P : result A E -> predS Regs) f : + PrePost (fun s => P (Value (f s)) s) (readS f) P. +unfold PrePost, readS, returnS. +intros s Pre r s' [H | []]. +inversion H; subst. +assumption. +Qed. + +Lemma PrePost_updateS (*[intro, PrePost_atomI]:*) Regs E (P : result unit E -> predS Regs) f : + PrePost (fun s => P (Value tt) (f s)) (updateS f) P. +unfold PrePost, readS, returnS. +intros s Pre r s' [H | []]. +inversion H; subst. +assumption. +Qed. + +Lemma PrePost_if Regs A E b (f g : monadS Regs A E) P Q : + (b = true -> PrePost P f Q) -> + (b = false -> PrePost P g Q) -> + PrePost P (if b then f else g) Q. +intros T F. +destruct b; auto. +Qed. + +Lemma PrePost_if_branch (*[PrePost_compositeI]:*) Regs A E b (f g : monadS Regs A E) Pf Pg Q : + (b = true -> PrePost Pf f Q) -> + (b = false -> PrePost Pg g Q) -> + PrePost (if b then Pf else Pg) (if b then f else g) Q. +destruct b; auto. +Qed. + +Lemma PrePost_if_then Regs A E b (f g : monadS Regs A E) P Q : + b = true -> + PrePost P f Q -> + PrePost P (if b then f else g) Q. +intros; subst; auto. +Qed. + +Lemma PrePost_if_else Regs A E b (f g : monadS Regs A E) P Q : + b = false -> + PrePost P g Q -> + PrePost P (if b then f else g) Q. +intros; subst; auto. +Qed. + +Lemma PrePost_prod_cases (*[PrePost_compositeI]:*) Regs A B E (f : A -> B -> monadS Regs A E) P Q x : + PrePost P (f (fst x) (snd x)) Q -> + PrePost P (match x with (a, b) => f a b end) Q. +destruct x; auto. +Qed. + +Lemma PrePost_option_cases (*[PrePost_compositeI]:*) Regs A B E x (s : A -> monadS Regs B E) n PS PN Q : + (forall a, PrePost (PS a) (s a) Q) -> + PrePost PN n Q -> + PrePost (match x with Some a => PS a | None => PN end) (match x with Some a => s a | None => n end) Q. +destruct x; auto. +Qed. + +Lemma PrePost_let (*[intro, PrePost_compositeI]:*) Regs A B E y (m : A -> monadS Regs B E) P Q : + PrePost P (m y) Q -> + PrePost P (let x := y in m x) Q. +auto. +Qed. + +Lemma PrePost_and_boolS (*[PrePost_compositeI]:*) Regs E (l r : monadS Regs bool E) P Q R : + PrePost R r Q -> + PrePost P l (fun r => match r with Value true => R | _ => Q r end) -> + PrePost P (and_boolS l r) Q. +intros Hr Hl. +unfold and_boolS. +eapply PrePost_bindS. +2: { instantiate (1 := fun a => if a then R else Q (Value false)). + eapply PrePost_weaken_post. + apply Hl. + intros [[|] | ] s H; auto. } +* intros. destruct a; eauto. + apply PrePost_returnS. +Qed. + +Lemma PrePost_or_boolS (*[PrePost_compositeI]:*) Regs E (l r : monadS Regs bool E) P Q R : + PrePost R r Q -> + PrePost P l (fun r => match r with Value false => R | _ => Q r end) -> + PrePost P (or_boolS l r) Q. +intros Hr Hl. +unfold or_boolS. +eapply PrePost_bindS. +* intros. + instantiate (1 := fun a => if a then Q (Value true) else R). + destruct a; eauto. + apply PrePost_returnS. +* eapply PrePost_weaken_post. + apply Hl. + intros [[|] | ] s H; auto. +Qed. + +Lemma PrePost_failS (*[intro, PrePost_atomI]:*) Regs A E msg (Q : result A E -> predS Regs) : + PrePost (Q (Ex (Failure msg))) (failS msg) Q. +intros s Pre r s' [[= <- <-] | []]. +assumption. +Qed. + +Lemma PrePost_assert_expS (*[intro, PrePost_atomI]:*) Regs E (c : bool) m (P : result unit E -> predS Regs) : + PrePost (if c then P (Value tt) else P (Ex (Failure m))) (assert_expS c m) P. +destruct c; simpl. +* apply PrePost_returnS. +* apply PrePost_failS. +Qed. + +Lemma PrePost_chooseS (*[intro, PrePost_atomI]:*) Regs A E xs (Q : result A E -> predS Regs) : + PrePost (fun s => forall x, List.In x xs -> Q (Value x) s) (chooseS xs) Q. +unfold PrePost, chooseS. +intros s IN r s' IN'. +apply List.in_map_iff in IN'. +destruct IN' as (x & [= <- <-] & IN'). +auto. +Qed. + +Lemma case_result_combine (*[simp]:*) A E X r (Q : result A E -> X) : + (match r with Value a => Q (Value a) | Ex e => Q (Ex e) end) = Q r. +destruct r; auto. +Qed. + +Lemma PrePost_foreachS_Nil (*[intro, simp, PrePost_atomI]:*) Regs A Vars E vars body (Q : result Vars E -> predS Regs) : + PrePost (Q (Value vars)) (foreachS (A := A) nil vars body) Q. +simpl. apply PrePost_returnS. +Qed. + +Lemma PrePost_foreachS_Cons Regs A Vars E (x : A) xs vars body (Q : result Vars E -> predS Regs) : + (forall s vars' s', List.In (Value vars', s') (body x vars s) -> PrePost (Q (Value vars')) (foreachS xs vars' body) Q) -> + PrePost (Q (Value vars)) (body x vars) Q -> + PrePost (Q (Value vars)) (foreachS (x :: xs) vars body) Q. +intros XS X. +simpl. +eapply PrePost_bindS. +* apply XS. +* apply PrePost_weaken_post with (B := Q). + assumption. + intros; rewrite case_result_combine. + assumption. +Qed. + +Lemma PrePost_foreachS_invariant Regs A Vars E (xs : list A) vars body (Q : result Vars E -> predS Regs) : + (forall x vars, List.In x xs -> PrePost (Q (Value vars)) (body x vars) Q) -> + PrePost (Q (Value vars)) (foreachS xs vars body) Q. +revert vars. +induction xs. +* intros. apply PrePost_foreachS_Nil. +* intros. apply PrePost_foreachS_Cons. + + auto with datatypes. + + apply H. auto with datatypes. +Qed. + +(*subsection \<open>Hoare quadruples\<close> + +text \<open>It is often convenient to treat the exception case separately. For this purpose, we use +a Hoare logic similar to the one used in [1]. It features not only Hoare triples, but also quadruples +with two postconditions: one for the case where the computation succeeds, and one for the case where +there is an exception. + +[1] D. Cock, G. Klein, and T. Sewell, ‘Secure Microkernels, State Monads and Scalable Refinement’, +in Theorem Proving in Higher Order Logics, 2008, pp. 167–182.\<close> +*) +Definition PrePostE {Regs A Ety} (P : predS Regs) (f : monadS Regs A Ety) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : Prop := +(* ("\<lbrace>_\<rbrace> _ \<lbrace>_ \<bar> _\<rbrace>")*) + PrePost P f (fun v => match v with Value a => Q a | Ex e => E e end). + +Notation "{{ P }} m {{ Q | X }}" := (PrePostE P m Q X). + +(*lemmas PrePost_defs = PrePost_def PrePostE_def*) + +Lemma PrePostE_I (*[case_names Val Err]:*) Regs A Ety (P : predS Regs) f (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + (forall s a s', P s -> List.In (Value a, s') (f s) -> Q a s') -> + (forall s e s', P s -> List.In (Ex e, s') (f s) -> E e s') -> + PrePostE P f Q E. +intros. unfold PrePostE. +unfold PrePost. +intros s Pre [a | e] s' IN; eauto. +Qed. + +Lemma PrePostE_PrePost Regs A Ety P m (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePost P m (fun v => match v with Value a => Q a | Ex e => E e end) -> + PrePostE P m Q E. +auto. +Qed. + +Lemma PrePostE_elim Regs A Ety P f r s s' (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE P f Q E -> + P s -> + List.In (r, s') (f s) -> + (exists v, r = Value v /\ Q v s') \/ + (exists e, r = Ex e /\ E e s'). +intros PP Pre IN. +specialize (PP _ Pre _ _ IN). +destruct r; eauto. +Qed. + +Lemma PrePostE_consequence Regs Aty Ety (P : predS Regs) f A B C (Q : Aty -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE A f B C -> + (forall s, P s -> A s) -> + (forall v s, B v s -> Q v s) -> + (forall e s, C e s -> E e s) -> + PrePostE P f Q E. +intros PP PA BQ CE. +intros s Pre [a | e] s' IN. +* apply BQ. specialize (PP _ (PA _ Pre) _ _ IN). + apply PP. +* apply CE. specialize (PP _ (PA _ Pre) _ _ IN). + apply PP. +Qed. + +Lemma PrePostE_strengthen_pre Regs Aty Ety (P : predS Regs) f R (Q : Aty -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE R f Q E -> + (forall s, P s -> R s) -> + PrePostE P f Q E. +intros PP PR. +eapply PrePostE_consequence; eauto. +Qed. + +Lemma PrePostE_weaken_post Regs Aty Ety (A : predS Regs) f (B C : Aty -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE A f B E -> + (forall v s, B v s -> C v s) -> + PrePostE A f C E. +intros PP BC. +eauto using PrePostE_consequence. +Qed. + +Lemma PrePostE_weaken_Epost Regs Aty Ety (A : predS Regs) f (B : Aty -> predS Regs) (E F : ex Ety -> predS Regs) : + PrePostE A f B E -> + (forall v s, E v s -> F v s) -> + PrePostE A f B F. +intros PP EF. +eauto using PrePostE_consequence. +Qed. +(*named_theorems PrePostE_compositeI +named_theorems PrePostE_atomI*) + +Lemma PrePostE_conj_conds Regs Aty Ety (P1 P2 : predS Regs) m (Q1 Q2 : Aty -> predS Regs) (E1 E2 : ex Ety -> predS Regs) : + PrePostE P1 m Q1 E1 -> + PrePostE P2 m Q2 E2 -> + PrePostE (fun s => P1 s /\ P2 s) m (fun r s => Q1 r s /\ Q2 r s) (fun e s => E1 e s /\ E2 e s). +intros H1 H2. +apply PrePostE_I. +* intros s a s' [p1 p2] IN. + specialize (H1 _ p1 _ _ IN). + specialize (H2 _ p2 _ _ IN). + simpl in *. + auto. +* intros s a s' [p1 p2] IN. + specialize (H1 _ p1 _ _ IN). + specialize (H2 _ p2 _ _ IN). + simpl in *. + auto. +Qed. + +(*lemmas PrePostE_conj_conds_consequence = PrePostE_conj_conds[THEN PrePostE_consequence]*) + +Lemma PrePostE_post_mp Regs Aty Ety (P : predS Regs) m (Q Q' : Aty -> predS Regs) (E: ex Ety -> predS Regs) : + PrePostE P m Q' E -> + PrePostE P m (fun r s => Q' r s -> Q r s) E -> + PrePostE P m Q E. +intros H1 H2. +eapply PrePostE_conj_conds in H1. 2: apply H2. +eapply PrePostE_consequence. apply H1. all: simpl; intuition. +Qed. + +Lemma PrePostE_cong Regs Aty Ety (P1 P2 : predS Regs) m1 m2 (Q1 Q2 : Aty -> predS Regs) (E1 E2 : ex Ety -> predS Regs) : + (forall s, P1 s <-> P2 s) -> + (forall s, P1 s -> m1 s = m2 s) -> + (forall r s, Q1 r s <-> Q2 r s) -> + (forall e s, E1 e s <-> E2 e s) -> + PrePostE P1 m1 Q1 E1 <-> PrePostE P2 m2 Q2 E2. +intros P12 m12 Q12 E12. +unfold PrePostE, PrePost. +split. +* intros. apply P12 in H0. rewrite <- m12 in H1; auto. specialize (H _ H0 _ _ H1). + destruct r; [ apply Q12 | apply E12]; auto. +* intros. rewrite m12 in H1; auto. apply P12 in H0. specialize (H _ H0 _ _ H1). + destruct r; [ apply Q12 | apply E12]; auto. +Qed. + +Lemma PrePostE_True_post (*[PrePostE_atomI, intro, simp]:*) Regs A E P (m : monadS Regs A E) : + PrePostE P m (fun _ _ => True) (fun _ _ => True). +intros s Pre [a | e]; auto. +Qed. + +Lemma PrePostE_any Regs A Ety m (Q : result A Ety -> predS Regs) E : + PrePostE (Ety := Ety) (fun s => forall r s', List.In (r, s') (m s) -> match r with Value a => Q a s' | Ex e => E e s' end) m Q E. +apply PrePostE_I. +intros. apply (H (Value a)); auto. +intros. apply (H (Ex e)); auto. +Qed. + +Lemma PrePostE_returnS (*[PrePostE_atomI, intro, simp]:*) Regs A E P (x : A) (Q : ex E -> predS Regs) : + PrePostE (P x) (returnS x) P Q. +unfold PrePostE, PrePost. +intros s Pre r s' [[= <- <-] | []]. +assumption. +Qed. + +Lemma PrePostE_bindS (*[intro, PrePostE_compositeI]:*) Regs A B Ety P m (f : A -> monadS Regs B Ety) Q R E : + (forall s a s', List.In (Value a, s') (m s) -> PrePostE (R a) (f a) Q E) -> + PrePostE P m R E -> + PrePostE P (bindS m f) Q E. +intros. +unfold PrePostE in *. +eauto using PrePost_bindS. +Qed. + +Lemma PrePostE_bindS_ignore Regs A B Ety (P : predS Regs) (m : monadS Regs A Ety) (f : monadS Regs B Ety) R Q E : + PrePostE R f Q E -> + PrePostE P m (fun _ => R) E -> + PrePostE P (bindS m (fun _ => f)) Q E. +apply PrePost_bindS_ignore. +Qed. + +Lemma PrePostE_bindS_unit Regs A Ety (P : predS Regs) (m : monadS Regs unit Ety) (f : unit -> monadS Regs A Ety) Q R E : + PrePostE R (f tt) Q E -> + PrePostE P m (fun _ => R) E -> + PrePostE P (bindS m f) Q E. +apply PrePost_bindS_unit. +Qed. + +Lemma PrePostE_readS (*[PrePostE_atomI, intro]:*) Regs A Ety (P : predS Regs) f (Q : result A Ety -> predS Regs) E : + PrePostE (Ety := Ety) (fun s => Q (f s) s) (readS f) Q E. +unfold PrePostE, PrePost, readS. +intros s Pre [a | e] s' [[= <- <-] | []]. +assumption. +Qed. + +Lemma PrePostE_updateS (*[PrePostE_atomI, intro]:*) Regs Ety f (Q : unit -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => Q tt (f s)) (updateS f) Q E. +intros s Pre [a | e] s' [[= <- <-] | []]. +assumption. +Qed. + +Lemma PrePostE_if_branch (*[PrePostE_compositeI]:*) Regs A Ety (b : bool) (f g : monadS Regs A Ety) Pf Pg Q E : + (b = true -> PrePostE Pf f Q E) -> + (b = false -> PrePostE Pg g Q E) -> + PrePostE (if b then Pf else Pg) (if b then f else g) Q E. +destruct b; auto. +Qed. + +Lemma PrePostE_if Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E : + (b = true -> PrePostE P f Q E) -> + (b = false -> PrePostE P g Q E) -> + PrePostE P (if b then f else g) Q E. +destruct b; auto. +Qed. + +Lemma PrePostE_if_then Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E : + b = true -> + PrePostE P f Q E -> + PrePostE P (if b then f else g) Q E. +intros; subst; auto. +Qed. + +Lemma PrePostE_if_else Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E : + b = false -> + PrePostE P g Q E -> + PrePostE P (if b then f else g) Q E. +intros; subst; auto. +Qed. + +Lemma PrePostE_prod_cases (*[PrePostE_compositeI]:*) Regs A B C Ety x (f : A -> B -> monadS Regs C Ety) P Q E : + PrePostE P (f (fst x) (snd x)) Q E -> + PrePostE P (match x with (a, b) => f a b end) Q E. +destruct x; auto. +Qed. + +Lemma PrePostE_option_cases (*[PrePostE_compositeI]:*) Regs A B Ety x (s : option A -> monadS Regs B Ety) n PS PN Q E : + (forall a, PrePostE (PS a) (s a) Q E) -> + PrePostE PN n Q E -> + PrePostE (match x with Some a => PS a | None => PN end) (match x with Some a => s a | None => n end) Q E. +apply PrePost_option_cases. +Qed. + +Lemma PrePostE_sum_cases (*[PrePostE_compositeI]:*) Regs A B C Ety x (l : A -> monadS Regs C Ety) (r : B -> monadS Regs C Ety) Pl Pr Q E : + (forall a, PrePostE (Pl a) (l a) Q E) -> + (forall b, PrePostE (Pr b) (r b) Q E) -> + PrePostE (match x with inl a => Pl a | inr b => Pr b end) (match x with inl a => l a | inr b => r b end) Q E. +intros; destruct x; auto. +Qed. + +Lemma PrePostE_let (*[PrePostE_compositeI]:*) Regs A B Ety y (m : A -> monadS Regs B Ety) P Q E : + PrePostE P (m y) Q E -> + PrePostE P (let x := y in m x) Q E. +auto. +Qed. + +Lemma PrePostE_and_boolS (*[PrePostE_compositeI]:*) Regs Ety (l r : monadS Regs bool Ety) P Q R E : + PrePostE R r Q E -> + PrePostE P l (fun r => if r then R else Q false) E -> + PrePostE P (and_boolS l r) Q E. +intros Hr Hl. +unfold and_boolS. +eapply PrePostE_bindS. +* intros. + instantiate (1 := fun a => if a then R else Q false). + destruct a; eauto. + apply PrePostE_returnS. +* assumption. +Qed. + +Lemma PrePostE_or_boolS (*[PrePostE_compositeI]:*) Regs Ety (l r : monadS Regs bool Ety) P Q R E : + PrePostE R r Q E -> + PrePostE P l (fun r => if r then Q true else R) E -> + PrePostE P (or_boolS l r) Q E. +intros Hr Hl. +unfold or_boolS. +eapply PrePostE_bindS. +* intros. + instantiate (1 := fun a => if a then Q true else R). + destruct a; eauto. + apply PrePostE_returnS. +* assumption. +Qed. + +Lemma PrePostE_failS (*[PrePostE_atomI, intro]:*) Regs A Ety msg (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (E (Failure msg)) (failS msg) Q E. +unfold PrePostE, PrePost, failS. +intros s Pre r s' [[= <- <-] | []]. +assumption. +Qed. + +Lemma PrePostE_assert_expS (*[PrePostE_atomI, intro]:*) Regs Ety (c : bool) m P (Q : ex Ety -> predS Regs) : + PrePostE (if c then P tt else Q (Failure m)) (assert_expS c m) P Q. +unfold assert_expS. +destruct c; auto using PrePostE_returnS, PrePostE_failS. +Qed. + +Lemma PrePostE_maybe_failS (*[PrePostE_atomI]:*) Regs A Ety msg v (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => match v with Some v => Q v s | None => E (Failure msg) s end) (maybe_failS msg v) Q E. +unfold maybe_failS. +destruct v; auto using PrePostE_returnS, PrePostE_failS. +Qed. + +Lemma PrePostE_exitS (*[PrePostE_atomI, intro]:*) Regs A Ety msg (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (E (Failure "exit")) (exitS msg) Q E. +unfold exitS. +apply PrePostE_failS. +Qed. + +Lemma PrePostE_chooseS (*[intro, PrePostE_atomI]:*) Regs A Ety (xs : list A) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => forall x, List.In x xs -> Q x s) (chooseS xs) Q E. +unfold chooseS. +intros s IN r s' IN'. +apply List.in_map_iff in IN'. +destruct IN' as (x & [= <- <-] & IN'). +auto. +Qed. + +Lemma PrePostE_throwS (*[PrePostE_atomI]:*) Regs A Ety e (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (E (Throw e)) (throwS e) Q E. +unfold throwS. +intros s Pre r s' [[= <- <-] | []]. +assumption. +Qed. + +Lemma PrePostE_try_catchS (*[PrePostE_compositeI]:*) Regs A E1 E2 m h P (Ph : E1 -> predS Regs) (Q : A -> predS Regs) (E : ex E2 -> predS Regs) : + (forall s e s', List.In (Ex (Throw e), s') (m s) -> PrePostE (Ph e) (h e) Q E) -> + PrePostE P m Q (fun ex => match ex with Throw e => Ph e | Failure msg => E (Failure msg) end) -> + PrePostE P (try_catchS m h) Q E. +intros. +intros s Pre r s' IN. +destruct (try_catchS_cases IN) as [(a' & [= ->] & IN') | [(msg & [= ->] & IN') | (e & s'' & IN1 & IN2)]]. +* specialize (H0 _ Pre _ _ IN'). apply H0. +* specialize (H0 _ Pre _ _ IN'). apply H0. +* specialize (H _ _ _ IN1). specialize (H0 _ Pre _ _ IN1). simpl in *. + specialize (H _ H0 _ _ IN2). apply H. +Qed. + +Lemma PrePostE_catch_early_returnS (*[PrePostE_compositeI]:*) Regs A Ety m P (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE P m Q (fun ex => match ex with Throw (inl a) => Q a | Throw (inr e) => E (Throw e) | Failure msg => E (Failure msg) end) -> + PrePostE P (catch_early_returnS m) Q E. +unfold catch_early_returnS. +intro H. +apply PrePostE_try_catchS with (Ph := fun e => match e with inl a => Q a | inr e => E (Throw e) end). +* intros. destruct e. + + apply PrePostE_returnS. + + apply PrePostE_throwS. +* apply H. +Qed. + +Lemma PrePostE_early_returnS (*[PrePostE_atomI]:*) Regs A E1 E2 r (Q : A -> predS Regs) (E : ex (E1 + E2) -> predS Regs) : + PrePostE (E (Throw (inl r))) (early_returnS r) Q E. +unfold early_returnS. +apply PrePostE_throwS. +Qed. + +Lemma PrePostE_liftRS (*[PrePostE_compositeI]:*) Regs A E1 E2 m P (Q : A -> predS Regs) (E : ex (E1 + E2) -> predS Regs) : + PrePostE P m Q (fun ex => match ex with Throw e => E (Throw (inr e)) | Failure msg => E (Failure msg) end) -> + PrePostE P (liftRS m) Q E. +unfold liftRS. +apply PrePostE_try_catchS. +auto using PrePostE_throwS. +Qed. + +Lemma PrePostE_foreachS_Cons Regs A Vars Ety (x : A) xs vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) : + (forall s vars' s', List.In (Value vars', s') (body x vars s) -> PrePostE (Q vars') (foreachS xs vars' body) Q E) -> + PrePostE (Q vars) (body x vars) Q E -> + PrePostE (Q vars) (foreachS (x :: xs) vars body) Q E. +intros. +simpl. +apply PrePostE_bindS with (R := Q); auto. +Qed. + +Lemma PrePostE_foreachS_invariant Regs A Vars Ety (xs : list A) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) : + (forall x vars, List.In x xs -> PrePostE (Q vars) (body x vars) Q E) -> + PrePostE (Q vars) (foreachS xs vars body) Q E. +unfold PrePostE. +intros H. +apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a | Ex e => E e end). +auto. +Qed. + + +Lemma PrePostE_use_pre Regs A Ety m (P : predS Regs) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + (forall s, P s -> PrePostE P m Q E) -> + PrePostE P m Q E. +unfold PrePostE, PrePost. +intros H s p r s' IN. +eapply H; eauto. +Qed. + +Local Open Scope Z. +Local Opaque _limit_reduces. +Ltac gen_reduces := + match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. + + +Lemma PrePostE_untilST Regs Vars Ety vars measure cond (body : Vars -> monadS Regs Vars Ety) Inv Inv' (Q : Vars -> predS Regs) E : + (forall vars, PrePostE (Inv' Q vars) (cond vars) (fun c s' => Inv Q vars s' /\ (c = true -> Q vars s')) E) -> + (forall vars, PrePostE (Inv Q vars) (body vars) (fun vars' s' => Inv' Q vars' s' /\ measure vars' < measure vars) E) -> + (forall vars s, Inv Q vars s -> measure vars >= 0) -> + PrePostE (Inv Q vars) (untilST vars measure cond body) Q E. + +intros Hcond Hbody Hmeasure. +unfold untilST. +apply PrePostE_use_pre. intros s0 Pre0. +assert (measure vars >= 0) as Hlimit_0 by eauto. clear s0 Pre0. +remember (measure vars) as limit eqn: Heqlimit in Hlimit_0 |- *. +assert (measure vars <= limit) as Hlimit by omega. clear Heqlimit. +generalize (Sail2_prompt.Zwf_guarded limit). +revert vars Hlimit. +apply Wf_Z.natlike_ind with (x := limit). +* intros vars Hmeasure_limit [acc]. simpl. + eapply PrePostE_bindS; [ | apply Hbody ]. + intros s vars' s' IN. + eapply PrePostE_bindS with (R := (fun c s' => (Inv Q vars' s' /\ (c = true -> Q vars' s')) /\ measure vars' < measure vars)). + 2: { + apply PrePostE_weaken_Epost with (E := (fun e s' => E e s' /\ measure vars' < measure vars)). 2: tauto. + eapply PrePostE_conj_conds. + apply Hcond. + apply PrePostE_I; tauto. + } + intros. + destruct a. + - eapply PrePostE_strengthen_pre; try apply PrePostE_returnS. + intros ? [[? ?] ?]; auto. + - apply PrePostE_I; + intros ? ? ? [[Pre ?] ?] ?; exfalso; + specialize (Hmeasure _ _ Pre); omega. +* intros limit' Hlimit' IH vars Hmeasure_limit [acc]. + simpl. + destruct (Z_ge_dec _ _); try omega. + eapply PrePostE_bindS; [ | apply Hbody]. + intros s vars' s' IN. + eapply PrePostE_bindS with (R := (fun c s' => (Inv Q vars' s' /\ (c = true -> Q vars' s')) /\ measure vars' < measure vars)). + 2: { + apply PrePostE_weaken_Epost with (E := (fun e s' => E e s' /\ measure vars' < measure vars)). 2: tauto. + eapply PrePostE_conj_conds. + apply Hcond. + apply PrePostE_I; tauto. + } + intros. + destruct a. + - eapply PrePostE_strengthen_pre; try apply PrePostE_returnS. + intros ? [[? ?] ?]; auto. + - gen_reduces. + replace (Z.succ limit' - 1) with limit'; [ | omega]. + intro acc'. + apply PrePostE_use_pre. intros sx [[Pre _] Hreduces]. + apply Hmeasure in Pre. + eapply PrePostE_strengthen_pre; [apply IH | ]. + + omega. + + tauto. +* omega. +Qed. + + +Lemma PrePostE_untilST_pure_cond Regs Vars Ety vars measure cond (body : Vars -> monadS Regs Vars Ety) Inv (Q : Vars -> predS Regs) E : + (forall vars, PrePostE (Inv Q vars) (body vars) (fun vars' s' => Inv Q vars' s' /\ measure vars' < measure vars /\ (cond vars' = true -> Q vars' s')) E) -> + (forall vars s, Inv Q vars s -> measure vars >= 0) -> + (PrePostE (Inv Q vars) (untilST vars measure (fun vars => returnS (cond vars)) body) Q E). +intros Hbody Hmeasure. +apply PrePostE_untilST with (Inv' := fun Q vars s => Inv Q vars s /\ (cond vars = true -> Q vars s)). +* intro. + apply PrePostE_returnS with (P := fun c s' => Inv Q vars0 s' /\ (c = true -> Q vars0 s')). +* intro. + eapply PrePost_weaken_post; [ apply Hbody | ]. + simpl. intros [a |e]; eauto. tauto. +* apply Hmeasure. +Qed. + +Local Close Scope Z. + +(* +lemma PrePostE_liftState_untilM: + assumes dom: (forall s, Inv Q vars s -> untilM_dom (vars, cond, body)) + and cond: (forall vars, PrePostE (Inv' Q vars) (liftState r (cond vars)) (fun c s' => Inv Q vars s' /\ (c \<longrightarrow> Q vars s')) E) + and body: (forall vars, PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E) + shows "PrePostE (Inv Q vars) (liftState r (untilM vars cond body)) Q E" +proof - + have domS: "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" if "Inv Q vars s" for s + using dom that by (intro untilM_dom_untilS_dom) + then have "PrePostE (Inv Q vars) (untilS vars (liftState r \<circ> cond) (liftState r \<circ> body)) Q E" + using cond body by (auto intro: PrePostE_untilS simp: comp_def) + moreover have "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" + if "Inv Q vars s" for s + unfolding liftState_untilM[OF domS[OF that] dom[OF that]] .. + ultimately show ?thesis by (auto cong: PrePostE_cong) +qed + +lemma PrePostE_liftState_untilM_pure_cond: + assumes dom: (forall s, Inv Q vars s -> untilM_dom (vars, return \<circ> cond, body)" + and body: (forall vars, PrePostE (Inv Q vars) (liftState r (body vars)) (fun vars' s' => Inv Q vars' s' /\ (cond vars' \<longrightarrow> Q vars' s')) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E" + using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp) +*) +Lemma PrePostE_choose_boolS_any (*[PrePostE_atomI]:*) Regs Ety unit_val (Q : bool -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => forall b, Q b s) (choose_boolS unit_val) Q E. +unfold choose_boolS, seqS. +eapply PrePostE_strengthen_pre. +apply PrePostE_chooseS. +simpl. intros. destruct x; auto. +Qed. + +Lemma PrePostE_bool_of_bitU_nondetS_any Regs Ety b (Q : bool -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => forall b, Q b s) (bool_of_bitU_nondetS b) Q E. +unfold bool_of_bitU_nondetS, undefined_boolS. +destruct b. +* intros s Pre r s' [[= <- <-] | []]. auto. +* intros s Pre r s' [[= <- <-] | []]. auto. +* apply PrePostE_choose_boolS_any. +Qed. +(* +Lemma PrePostE_bools_of_bits_nondetS_any: + PrePostE (fun s => forall bs, Q bs s) (bools_of_bits_nondetS bs) Q E. + unfolding bools_of_bits_nondetS_def + by (rule PrePostE_weaken_post[where B = "fun _ s => forall bs, Q bs s"], rule PrePostE_strengthen_pre, + (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS + PrePostE_bool_of_bitU_nondetS_any)+) + auto +*) +Lemma PrePostE_choose_boolsS_any Regs Ety n (Q : list bool -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => forall bs, Q bs s) (choose_boolsS n) Q E. +unfold choose_boolsS, genlistS. +apply PrePostE_weaken_post with (B := fun _ s => forall bs, Q bs s). +* apply PrePostE_foreachS_invariant with (Q := fun _ s => forall bs, Q bs s). + intros. apply PrePostE_bindS with (R := fun _ s => forall bs, Q bs s). + + intros. apply PrePostE_returnS with (P := fun _ s => forall bs, Q bs s). + + eapply PrePostE_strengthen_pre. + apply PrePostE_choose_boolS_any. + intuition. +* intuition. +Qed. + +Lemma nth_error_exists {A} {l : list A} {n} : + n < Datatypes.length l -> exists x, List.In x l /\ List.nth_error l n = Some x. +revert n. induction l. +* simpl. intros. apply PeanoNat.Nat.nlt_0_r in H. destruct H. +* intros. destruct n. + + exists a. auto with datatypes. + + simpl in H. apply Lt.lt_S_n in H. + destruct (IHl n H) as [x H1]. + intuition eauto with datatypes. +Qed. + +Lemma nth_error_modulo {A} {xs : list A} n : + xs <> nil -> + exists x, List.In x xs /\ List.nth_error xs (PeanoNat.Nat.modulo n (Datatypes.length xs)) = Some x. +intro notnil. +assert (Datatypes.length xs <> 0) by (rewrite List.length_zero_iff_nil; auto). +assert (PeanoNat.Nat.modulo n (Datatypes.length xs) < Datatypes.length xs) by auto using PeanoNat.Nat.mod_upper_bound. +destruct (nth_error_exists H0) as [x [H1 H2]]. +exists x. +auto. +Qed. + +Lemma PrePostE_internal_pick Regs A Ety (xs : list A) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : + xs <> nil -> + PrePostE (fun s => forall x, List.In x xs -> Q x s) (internal_pickS xs) Q E. +unfold internal_pickS. +intro notnil. +eapply PrePostE_bindS with (R := fun _ s => forall x, List.In x xs -> Q x s). +* intros. + destruct (nth_error_modulo (Sail2_values.nat_of_bools a) notnil) as (x & IN & nth). + rewrite nth. + eapply PrePostE_strengthen_pre. + apply PrePostE_returnS. + intuition. +* eapply PrePostE_strengthen_pre. + apply PrePostE_choose_boolsS_any. + intuition. +Qed. diff --git a/lib/coq/Makefile b/lib/coq/Makefile index f763db6f..fa453d90 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,6 +1,8 @@ BBV_DIR?=../../../bbv -SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_state_lifting.v Sail2_string.v Sail2_real.v +CORESRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_state_lifting.v Sail2_string.v Sail2_real.v +PROOFSRC=Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v +SRC=$(CORESRC) $(PROOFSRC) COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index 338bf10b..d03d5e63 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -139,29 +139,45 @@ instance (Show write_kind) end end *) + +Inductive a64_barrier_domain := + A64_FullShare + | A64_InnerShare + | A64_OuterShare + | A64_NonShare. + +Inductive a64_barrier_type := + A64_barrier_all + | A64_barrier_LD + | A64_barrier_ST. + Inductive barrier_kind := (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + | Barrier_Sync : unit -> barrier_kind + | Barrier_LwSync : unit -> barrier_kind + | Barrier_Eieio : unit -> barrier_kind + | Barrier_Isync : unit -> barrier_kind (* AArch64 barriers *) - | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB - | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB + | Barrier_DMB : a64_barrier_domain -> a64_barrier_type -> barrier_kind + | Barrier_DSB : a64_barrier_domain -> a64_barrier_type -> barrier_kind + | Barrier_ISB : unit -> barrier_kind (* | Barrier_TM_COMMIT*) (* MIPS barriers *) - | Barrier_MIPS_SYNC + | Barrier_MIPS_SYNC : unit -> barrier_kind (* 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 : unit -> barrier_kind + | Barrier_RISCV_r_rw : unit -> barrier_kind + | Barrier_RISCV_r_r : unit -> barrier_kind + | Barrier_RISCV_rw_w : unit -> barrier_kind + | Barrier_RISCV_w_w : unit -> barrier_kind + | Barrier_RISCV_w_rw : unit -> barrier_kind + | Barrier_RISCV_rw_r : unit -> barrier_kind + | Barrier_RISCV_r_w : unit -> barrier_kind + | Barrier_RISCV_w_r : unit -> barrier_kind + | Barrier_RISCV_tso : unit -> barrier_kind + | Barrier_RISCV_i : unit -> barrier_kind (* X86 *) - | Barrier_x86_MFENCE. + | Barrier_x86_MFENCE : unit -> barrier_kind. Scheme Equality for barrier_kind. (* diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 68d097fb..79bf87eb 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -53,6 +53,10 @@ Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < s (*declare {isabelle} termination_argument foreachM = automatic*) +Definition genlistM {A RV E} (f : nat -> monad RV A E) (n : nat) : monad RV (list A) E := + let indices := List.seq 0 n in + foreachM indices [] (fun n xs => (f n >>= (fun x => returnm (xs ++ [x])))). + (*val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*) Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then r else returnm false). @@ -145,7 +149,8 @@ Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool else returnm vars else Fail "Termination limit reached". -Definition whileMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := +Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := + let limit := measure vars in whileMT' limit vars cond body (Zwf_guarded limit). (*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> @@ -157,7 +162,8 @@ Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc) else Fail "Termination limit reached". -Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := +Definition untilMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := + let limit := measure vars in untilMT' limit vars cond body (Zwf_guarded limit). (*let write_two_regs r1 r2 vec = @@ -181,23 +187,21 @@ Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool else slice vec (start_vec - size_r1) (start_vec - size_vec) in write_reg r1 r1_v >> write_reg r2 r2_v*) -Fixpoint pick_bit_list {rv e} (n:nat) : monad rv (list bool) e := - match n with - | O => returnm [] - | S m => choose_bool "pick_bit_list" >>= fun b => - pick_bit_list m >>= fun t => - returnm (b::t) - end%list. +Definition choose_bools {RV E} (descr : string) (n : nat) : monad RV (list bool) E := + genlistM (fun _ => choose_bool descr) n. + +Definition choose {RV A E} (descr : string) (xs : list A) : monad RV A E := + (* Use sufficiently many nondeterministically chosen bits and convert into an + index into the list *) + choose_bools descr (List.length xs) >>= fun bs => + let idx := ((nat_of_bools bs) mod List.length xs)%nat in + match List.nth_error xs idx with + | Some x => returnm x + | None => Fail ("choose " ++ descr) + end. Definition internal_pick {rv a e} (xs : list a) : monad rv a e := - let n := length xs in - match xs with - | h::_ => - pick_bit_list (2 + n) >>= fun bs => - let i := (Word.wordToNat (wordFromBitlist bs) mod n)%nat in - returnm (List.nth i xs h) - | [] => Fail "internal_pick called on empty list" - end. + choose "internal_pick" xs. Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e := match n with diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index b73d5013..dc635cb4 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -32,7 +32,7 @@ end. (*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*) Definition genlistS {A RV E} (f : nat -> monadS RV A E) n : monadS RV (list A) E := - let indices := genlist (fun n => n) n in + let indices := List.seq 0 n in foreachS indices [] (fun n xs => (f n >>$= (fun x => returnS (xs ++ [x])))). (*val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e*) @@ -43,6 +43,31 @@ Definition and_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E := Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E := l >>$= (fun l => if l then returnS true else r). +Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFact (P b)} E) (y : monadS rv {b:bool & ArithFact (Q b)} E) + `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))} + : monadS rv {b:bool & ArithFact (R b)} E. +refine ( + x >>$= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then + fun p => y >>$= fun '(existT _ y _) => returnS (existT _ y _) + else fun p => returnS (existT _ false _)) p +). +* constructor. destruct H. destruct a0. change y with (andb true y). auto. +* constructor. destruct H. change false with (andb false false). apply fact. + assumption. + congruence. +Defined. +Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFact (P b)} E) (r : monadS rv {b : bool & ArithFact (Q b)} E) + `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))} + : monadS rv {b : bool & ArithFact (R b)} E. +refine ( + l >>$= fun '(existT _ l (Build_ArithFact _ p)) => + (if l return P l -> _ then fun p => returnS (existT _ true _) + else fun p => r >>$= fun '(existT _ r _) => returnS (existT _ r _)) p +). +* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence. +* constructor. destruct H. destruct a0. change r with (orb false r). auto. +Defined. + (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e*) Definition bool_of_bitU_fail {RV E} (b : bitU) : monadS RV bool E := match b with @@ -96,21 +121,47 @@ let rec untilS vars cond body s = (cond vars >>$= (fun cond_val s'' -> if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s *) + +Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E := + if Z_ge_dec limit 0 then + cond vars >>$= fun cond_val => + if cond_val then + body vars >>$= fun vars => whileST' (limit - 1) vars cond body (_limit_reduces acc) + else returnS vars + else failS "Termination limit reached". + +Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := + let limit := measure vars in + whileST' limit vars cond body (Zwf_guarded limit). + +(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> + ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*) +Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E := + if Z_ge_dec limit 0 then + body vars >>$= fun vars => + cond vars >>$= fun cond_val => + if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc) + else failS "Termination limit reached". + +Definition untilST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := + let limit := measure vars in + untilST' limit vars cond body (Zwf_guarded limit). + + (*val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e*) Definition choose_boolsS {RV E} n : monadS RV (list bool) E := genlistS (fun _ => choose_boolS tt) n. (* TODO: Replace by chooseS and prove equivalence to prompt monad version *) -(*val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e -let internal_pickS xs = +(*val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e*) +Definition internal_pickS {RV A E} (xs : list A) : monadS RV A E := (* Use sufficiently many nondeterministically chosen bits and convert into an index into the list *) - choose_boolsS (List.length xs) >>$= fun bs -> - let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in - match index xs idx with - | Just x -> returnS x - | Nothing -> failS "choose internal_pick" - end + choose_boolsS (List.length xs) >>$= fun bs => + let idx := ((nat_of_bools bs) mod List.length xs)%nat in + match List.nth_error xs idx with + | Some x => returnS x + | None => failS "choose internal_pick" + end. -*) diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v new file mode 100644 index 00000000..54cf45cc --- /dev/null +++ b/lib/coq/Sail2_state_lemmas.v @@ -0,0 +1,798 @@ +Require Import Sail2_values Sail2_prompt_monad Sail2_prompt Sail2_state_monad Sail2_state Sail2_state Sail2_state_lifting. +Require Import Sail2_state_monad_lemmas. + +(* Monad lifting *) + +Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} {s} : + liftState r (bind m f) s = bindS (liftState r m) (fun x => liftState r (f x)) s. +revert s. induction m; simpl. +all: try (intros; unfold seqS; rewrite bindS_assoc; auto using bindS_ext_cong). +all: try auto. +* intro s. + rewrite bindS_returnS_left. + reflexivity. +Qed. +Hint Rewrite liftState_bind : liftState. + +Lemma liftState_return Regval Regs A E {r : Sail2_values.register_accessors Regs Regval} {a :A} : + liftState (E:=E) r (returnm a) = returnS a. +reflexivity. +Qed. +Hint Rewrite liftState_return : liftState. + +(* +Lemma Value_liftState_Run: + List.In (Value a, s') (liftState r m s) + exists t, Run m t a. + by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>; + simp add: failS_def throwS_def returnS_def del: read_regvalS.simps; + blast elim: Value_bindS_elim) + +lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] +*) +Lemma liftState_if_distrib {Regs Regval A E r x y} {c : bool} : + @liftState Regs Regval A E r (if c then x else y) = if c then liftState r x else liftState r y. +destruct c; reflexivity. +Qed. +Lemma liftState_if_distrib_sumbool {Regs Regval A E P Q r x y} {c : sumbool P Q} : + @liftState Regs Regval A E r (if c then x else y) = if c then liftState r x else liftState r y. +destruct c; reflexivity. +Qed. + +Lemma Value_bindS_iff {Regs A B E} {f : A -> monadS Regs B E} {b m s s''} : + List.In (Value b, s'') (bindS m f s) <-> (exists a s', List.In (Value a, s') (m s) /\ List.In (Value b, s'') (f a s')). +split. +* intro H. + apply bindS_cases in H. + destruct H as [(? & ? & ? & [= <-] & ? & ?) | [(? & [= <-] & ?) | (? & ? & ? & [= <-] & ? & ?)]]; + eauto. +* intros (? & ? & ? & ?). + eauto with bindS_intros. +Qed. + +Lemma Ex_bindS_iff {Regs A B E} {f : A -> monadS Regs B E} {m e s s''} : + List.In (Ex e, s'') (bindS m f s) <-> List.In (Ex e, s'') (m s) \/ (exists a s', List.In (Value a, s') (m s) /\ List.In (Ex e, s'') (f a s')). +split. +* intro H. + apply bindS_cases in H. + destruct H as [(? & ? & ? & [= <-] & ? & ?) | [(? & [= <-] & ?) | (? & ? & ? & [= <-] & ? & ?)]]; + eauto. +* intros [H | (? & ? & H1 & H2)]; + eauto with bindS_intros. +Qed. + +Lemma liftState_throw Regs Regval A E {r} {e : E} : + @liftState Regval Regs A E r (throw e) = throwS e. +reflexivity. +Qed. +Lemma liftState_assert Regs Regval E {r c msg} : + @liftState Regval Regs _ E r (assert_exp c msg) = assert_expS c msg. +destruct c; reflexivity. +Qed. +Lemma liftState_exit Regs Regval A E r : + @liftState Regval Regs A E r (exit tt) = exitS tt. +reflexivity. +Qed. +Lemma liftState_exclResult Regs Regval E r : + @liftState Regs Regval _ E r (excl_result tt) = excl_resultS tt. +reflexivity. +Qed. +Lemma liftState_barrier Regs Regval E r bk : + @liftState Regs Regval _ E r (barrier bk) = returnS tt. +reflexivity. +Qed. +Lemma liftState_footprint Regs Regval E r : + @liftState Regs Regval _ E r (footprint tt) = returnS tt. +reflexivity. +Qed. +Lemma liftState_choose_bool Regs Regval E r descr : + @liftState Regs Regval _ E r (choose_bool descr) = choose_boolS tt. +reflexivity. +Qed. +(*declare undefined_boolS_def[simp]*) +Lemma liftState_undefined Regs Regval E r : + @liftState Regs Regval _ E r (undefined_bool tt) = undefined_boolS tt. +reflexivity. +Qed. +Lemma liftState_maybe_fail Regs Regval A E r msg x : + @liftState Regs Regval A E r (maybe_fail msg x) = maybe_failS msg x. +destruct x; reflexivity. +Qed. +Lemma liftState_and_boolM Regs Regval E r x y s : + @liftState Regs Regval _ E r (and_boolM x y) s = and_boolS (liftState r x) (liftState r y) s. +unfold and_boolM, and_boolS. +rewrite liftState_bind. +apply bindS_ext_cong; auto. +intros. rewrite liftState_if_distrib. +reflexivity. +Qed. +Lemma liftState_and_boolMP Regs Regval E P Q R r x y s H : + @liftState Regs Regval _ E r (@and_boolMP _ _ P Q R x y H) s = and_boolSP (liftState r x) (liftState r y) s. +unfold and_boolMP, and_boolSP. +rewrite liftState_bind. +simpl. +apply bindS_ext_cong; auto. +intros [[|] [A]] s' ?. +* rewrite liftState_bind; + simpl; + apply bindS_ext_cong; auto; + intros [a' A'] s'' ?; + rewrite liftState_return; + reflexivity. +* rewrite liftState_return. + reflexivity. +Qed. + +Lemma liftState_or_boolM Regs Regval E r x y s : + @liftState Regs Regval _ E r (or_boolM x y) s = or_boolS (liftState r x) (liftState r y) s. +unfold or_boolM, or_boolS. +rewrite liftState_bind. +apply bindS_ext_cong; auto. +intros. rewrite liftState_if_distrib. +reflexivity. +Qed. +Lemma liftState_or_boolMP Regs Regval E P Q R r x y s H : + @liftState Regs Regval _ E r (@or_boolMP _ _ P Q R x y H) s = or_boolSP (liftState r x) (liftState r y) s. +unfold or_boolMP, or_boolSP. +rewrite liftState_bind. +simpl. +apply bindS_ext_cong; auto. +intros [[|] [A]] s' ?. +* rewrite liftState_return. + reflexivity. +* rewrite liftState_bind; + simpl; + apply bindS_ext_cong; auto; + intros [a' A'] s'' ?; + rewrite liftState_return; + reflexivity. +Qed. +Hint Rewrite liftState_throw liftState_assert liftState_exit liftState_exclResult + liftState_barrier liftState_footprint liftState_choose_bool + liftState_undefined liftState_maybe_fail + liftState_and_boolM liftState_and_boolMP + liftState_or_boolM liftState_or_boolMP + : liftState. + +Lemma liftState_try_catch Regs Regval A E1 E2 r m h s : + @liftState Regs Regval A E2 r (try_catch (E1 := E1) m h) s = try_catchS (liftState r m) (fun e => liftState r (h e)) s. +revert s. +induction m; intros; simpl; +try solve +[ auto +| unfold seqS; + erewrite try_catchS_bindS_no_throw; intros; + only 2,3: (autorewrite with ignore_throw; reflexivity); + apply bindS_ext_cong; auto +]. +rewrite try_catchS_throwS. reflexivity. +Qed. +Hint Rewrite liftState_try_catch : liftState. + +Lemma liftState_early_return Regs Regval A R E r x : + liftState (Regs := Regs) r (@early_return Regval A R E x) = early_returnS x. +reflexivity. +Qed. +Hint Rewrite liftState_early_return : liftState. + +Lemma liftState_catch_early_return (*[liftState_simp]:*) Regs Regval A E r m s : + liftState (Regs := Regs) r (@catch_early_return Regval A E m) s = catch_early_returnS (liftState r m) s. +unfold catch_early_return, catch_early_returnS. +autorewrite with liftState. +apply try_catchS_cong; auto. +intros [a | e] s'; auto. +Qed. +Hint Rewrite liftState_catch_early_return : liftState. + +Lemma liftState_liftR Regs Regval A R E r m s : + liftState (Regs := Regs) r (@liftR Regval A R E m) s = liftRS (liftState r m) s. +unfold liftR, liftRS. autorewrite with liftState. +apply try_catchS_cong; auto. +Qed. +Hint Rewrite liftState_liftR : liftState. + +Lemma liftState_try_catchR Regs Regval A R E1 E2 r m h s : + liftState (Regs := Regs) r (@try_catchR Regval A R E1 E2 m h) s = try_catchRS (liftState r m) (fun x => liftState r (h x)) s. +unfold try_catchR, try_catchRS. autorewrite with liftState. +apply try_catchS_cong; auto. +intros [r' | e] s'; auto. +Qed. +Hint Rewrite liftState_try_catchR : liftState. +(* +Lemma liftState_bool_of_bitU_nondet Regs Regval : + "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b" + by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp) +Hint Rewrite liftState_bool_of_bitU_nondet : liftState. +*) +Lemma liftState_read_memt Regs Regval A B E H rk a sz r s : + liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) s = read_memtS rk a sz s. +unfold read_memt, read_memt_bytes, read_memtS, maybe_failS. simpl. +apply bindS_ext_cong; auto. +intros [byte bit] s' valIn. +destruct (option_map _); auto. +Qed. +Hint Rewrite liftState_read_memt : liftState. + +Lemma liftState_read_mem Regs Regval A B E H rk asz a sz r s : + liftState (Regs := Regs) r (@read_mem Regval A B E H rk asz a sz) s = read_memS rk a sz s. +unfold read_mem, read_memS, read_memtS. simpl. +unfold read_mem_bytesS, read_memt_bytesS. +repeat rewrite bindS_assoc. +apply bindS_ext_cong; auto. +intros [ bytes | ] s' valIn; auto. simpl. +apply bindS_ext_cong; auto. +intros [byte bit] s'' valIn'. +rewrite bindS_returnS_left. autorewrite with liftState. +destruct (option_map _); auto. +Qed. +Hint Rewrite liftState_read_mem : liftState. + +Lemma liftState_write_mem_ea Regs Regval A E rk asz a sz r : + liftState (Regs := Regs) r (@write_mem_ea Regval A E rk asz a sz) = returnS tt. +reflexivity. +Qed. +Hint Rewrite liftState_write_mem_ea : liftState. + +Lemma liftState_write_memt Regs Regval A B E wk addr sz v t r : + liftState (Regs := Regs) r (@write_memt Regval A B E wk addr sz v t) = write_memtS wk addr sz v t. +unfold write_memt, write_memtS. +destruct (Sail2_values.mem_bytes_of_bits v); auto. +Qed. +Hint Rewrite liftState_write_memt : liftState. + +Lemma liftState_write_mem Regs Regval A B E wk addrsize addr sz v r : + liftState (Regs := Regs) r (@write_mem Regval A B E wk addrsize addr sz v) = write_memS wk addr sz v. +unfold write_mem, write_memS, write_memtS. +destruct (Sail2_values.mem_bytes_of_bits v); simpl; auto. +Qed. +Hint Rewrite liftState_write_mem : liftState. + +Lemma bindS_rw_left Regs A B E m1 m2 (f : A -> monadS Regs B E) s : + m1 s = m2 s -> + bindS m1 f s = bindS m2 f s. +intro H. unfold bindS. rewrite H. reflexivity. +Qed. + +Lemma liftState_read_reg_readS Regs Regval A E reg get_regval' set_regval' s : + (forall s, map_bind reg.(of_regval) (get_regval' reg.(name) s) = Some (reg.(read_from) s)) -> + liftState (Regs := Regs) (get_regval', set_regval') (@read_reg _ Regval A E reg) s = readS (fun x => reg.(read_from) (regstate x)) s. +intros. +unfold read_reg. simpl. unfold readS. +erewrite bindS_rw_left. 2: { + apply bindS_returnS_left. +} +specialize (H (regstate s)). +destruct (get_regval' _ _) as [v | ]; only 2: discriminate H. +rewrite bindS_returnS_left. +simpl in *. +rewrite H. +reflexivity. +Qed. + +Lemma liftState_write_reg_updateS Regs Regval A E get_regval' set_regval' reg (v : A) s : + (forall s, set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)) -> + liftState (Regs := Regs) (Regval := Regval) (E := E) (get_regval', set_regval') (write_reg reg v) s = updateS (fun s => {| regstate := (write_to reg v s.(regstate)); memstate := s.(memstate); tagstate := s.(tagstate) |}) s. +intros. +unfold write_reg. simpl. unfold readS, seqS. +erewrite bindS_rw_left. 2: { + apply bindS_returnS_left. +} +specialize (H (regstate s)). +destruct (set_regval' _ _) as [v' | ]; only 2: discriminate H. +injection H as H1. +unfold updateS. +rewrite <- H1. +reflexivity. +Qed. +(* +Lemma liftState_iter_aux Regs Regval A E : + liftState r (iter_aux i f xs) = iterS_aux i (fun i x => liftState r (f i x)) xs. + by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) + (auto simp: liftState_simp cong: bindS_cong) +Hint Rewrite liftState_iter_aux : liftState. + +lemma liftState_iteri[liftState_simp]: + "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs" + by (auto simp: iteri_def iteriS_def liftState_simp) + +lemma liftState_iter[liftState_simp]: + "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs" + by (auto simp: iter_def iterS_def liftState_simp) +*) +Lemma liftState_foreachM Regs Regval A Vars E (xs : list A) (vars : Vars) (body : A -> Vars -> monad Regval Vars E) r s : + liftState (Regs := Regs) r (foreachM xs vars body) s = foreachS xs vars (fun x vars => liftState r (body x vars)) s. +revert vars s. +induction xs as [ | h t]. +* reflexivity. +* intros vars s. simpl. + autorewrite with liftState. + apply bindS_ext_cong; auto. +Qed. +Hint Rewrite liftState_foreachM : liftState. + +Lemma foreachS_cong {A RV Vars E} xs vars f f' s : + (forall a vars s, f a vars s = f' a vars s) -> + @foreachS A RV Vars E xs vars f s = foreachS xs vars f' s. +intro H. +revert s vars. +induction xs. +* reflexivity. +* intros. simpl. + apply bindS_ext_cong; auto. +Qed. + +Lemma liftState_genlistM Regs Regval A E r f n s : + liftState (Regs := Regs) r (@genlistM A Regval E f n) s = genlistS (fun x => liftState r (f x)) n s. +unfold genlistM, genlistS. +autorewrite with liftState. +apply foreachS_cong. +intros; autorewrite with liftState. +apply bindS_ext_cong; auto. +Qed. +Hint Rewrite liftState_genlistM : liftState. + +Lemma liftState_choose_bools Regs Regval E descr n r s : + liftState (Regs := Regs) r (@choose_bools Regval E descr n) s = choose_boolsS n s. +unfold choose_bools, choose_boolsS. +autorewrite with liftState. +reflexivity. +Qed. +Hint Rewrite liftState_choose_bools : liftState. + +(* +Lemma liftState_bools_of_bits_nondet[liftState_simp]: + "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs" + unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def + by (auto simp: liftState_simp comp_def) +Hint Rewrite liftState_choose_bools : liftState. +*) + +Lemma liftState_internal_pick Regs Regval A E r (xs : list A) s : + liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) s = internal_pickS xs s. +unfold internal_pick, internal_pickS. +unfold choose. +autorewrite with liftState. +apply bindS_ext_cong. +* autorewrite with liftState. + reflexivity. +* intros. + destruct (nth_error _ _); auto. +Qed. +Hint Rewrite liftState_internal_pick : liftState. + +Lemma liftRS_returnS (*[simp]:*) A R Regs E x : + @liftRS A R Regs E (returnS x) = returnS x. +reflexivity. +Qed. + +Lemma concat_singleton A (xs : list A) : + concat (xs::nil) = xs. +simpl. +rewrite app_nil_r. +reflexivity. +Qed. + +Lemma liftRS_bindS Regs A B R E (m : monadS Regs A E) (f : A -> monadS Regs B E) s : + @liftRS B R Regs E (bindS m f) s = bindS (liftRS m) (fun x => liftRS (f x)) s. +unfold liftRS, try_catchS, bindS, throwS, returnS. +induction (m s) as [ | [[a | [msg | e]] t]]. +* reflexivity. +* simpl. rewrite flat_map_app. rewrite IHl. reflexivity. +* simpl. rewrite IHl. reflexivity. +* simpl. rewrite IHl. reflexivity. +Qed. + +Lemma liftRS_assert_expS_True (*[simp]:*) Regs R E msg : + @liftRS _ R Regs E (assert_expS true msg) = returnS tt. +reflexivity. +Qed. + +(* +lemma untilM_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "Inv vars" + and "\<And>vars t vars' t'. \<lbrakk>Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\<rbrakk> \<Longrightarrow> V vars' < V vars \<and> Inv vars'" + shows "untilM_dom (vars, cond, body)" + using assms + by (induction vars rule: measure_induct_rule[where f = V]) + (auto intro: untilM.domintros) + +lemma untilM_dom_untilS_dom: + assumes "untilM_dom (vars, cond, body)" + shows "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + using assms + by (induction vars cond body arbitrary: s rule: untilM.pinduct) + (rule untilS.domintros, auto elim!: Value_liftState_Run) + +lemma measure2_induct: + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> nat" + assumes "\<And>x1 y1. (\<And>x2 y2. f x2 y2 < f x1 y1 \<Longrightarrow> P x2 y2) \<Longrightarrow> P x1 y1" + shows "P x y" +proof - + have "P (fst x) (snd x)" for x + by (induction x rule: measure_induct_rule[where f = "\<lambda>x. f (fst x) (snd x)"]) (auto intro: assms) + then show ?thesis by auto +qed + +lemma untilS_domI: + fixes V :: "'vars \<Rightarrow> 'regs sequential_state \<Rightarrow> nat" + assumes "Inv vars s" + and "\<And>vars s vars' s' s''. + \<lbrakk>Inv vars s; (Value vars', s') \<in> body vars s; (Value False, s'') \<in> cond vars' s'\<rbrakk> + \<Longrightarrow> V vars' s'' < V vars s \<and> Inv vars' s''" + shows "untilS_dom (vars, cond, body, s)" + using assms + by (induction vars s rule: measure2_induct[where f = V]) + (auto intro: untilS.domintros) + +lemma whileS_dom_step: + assumes "whileS_dom (vars, cond, body, s)" + and "(Value True, s') \<in> cond vars s" + and "(Value vars', s'') \<in> body vars s'" + shows "whileS_dom (vars', cond, body, s'')" + by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>) + (auto intro: whileS.domintros) + +lemma whileM_dom_step: + assumes "whileM_dom (vars, cond, body)" + and "Run (cond vars) t True" + and "Run (body vars) t' vars'" + shows "whileM_dom (vars', cond, body)" + by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\<close>) + (auto intro: whileM.domintros) + +lemma whileM_dom_ex_step: + assumes "whileM_dom (vars, cond, body)" + and "\<exists>t. Run (cond vars) t True" + and "\<exists>t'. Run (body vars) t' vars'" + shows "whileM_dom (vars', cond, body)" + using assms by (blast intro: whileM_dom_step) + +lemmas whileS_pinduct = whileS.pinduct[case_names Step] + +lemma liftState_whileM: + assumes "whileS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + and "whileM_dom (vars, cond, body)" + shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" +proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: whileS.pinduct\<close>) + case Step: (1 vars s) + note domS = Step(1) and IH = Step(2) and domM = Step(3) + show ?case unfolding whileS.psimps[OF domS] whileM.psimps[OF domM] liftState_bind + proof (intro bindS_ext_cong, goal_cases cond while) + case (while a s') + have "bindS (liftState r (body vars)) (liftState r \<circ> (\<lambda>vars. whileM vars cond body)) s' = + bindS (liftState r (body vars)) (\<lambda>vars. whileS vars (liftState r \<circ> cond) (liftState r \<circ> body)) s'" + if "a" + proof (intro bindS_ext_cong, goal_cases body while') + case (while' vars' s'') + have "whileM_dom (vars', cond, body)" proof (rule whileM_dom_ex_step[OF domM]) + show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) + show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run) + qed + then show ?case using while while' that IH by auto + qed auto + then show ?case by (auto simp: liftState_simp) + qed auto +qed +*) + +Local Opaque _limit_reduces. +Ltac gen_reduces := + match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. + +Lemma liftState_whileM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s : + liftState (Regs := RV) r (whileMT vars measure cond body) s = whileST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s. +unfold whileMT, whileST. +generalize (measure vars) as limit. intro. +revert vars s. +destruct (Z.le_decidable 0 limit). +* generalize (Zwf_guarded limit) as acc. + apply Wf_Z.natlike_ind with (x := limit). + + intros [acc] *; simpl. + autorewrite with liftState. + apply bindS_ext_cong; auto. + intros. rewrite liftState_if_distrib. + destruct a; autorewrite with liftState; auto. + apply bindS_ext_cong; auto. + intros. destruct (_limit_reduces _). simpl. + reflexivity. + + clear limit H. + intros limit H IH [acc] vars s. simpl. + destruct (Z_ge_dec _ _); try omega. + autorewrite with liftState. + apply bindS_ext_cong; auto. + intros. rewrite liftState_if_distrib. + destruct a; autorewrite with liftState; auto. + apply bindS_ext_cong; auto. + intros. + gen_reduces. + replace (Z.succ limit - 1) with limit; try omega. intro acc'. + apply IH. + + assumption. +* intros. simpl. + destruct (Z_ge_dec _ _); try omega. + reflexivity. +Qed. + +(* +lemma untilM_dom_step: + assumes "untilM_dom (vars, cond, body)" + and "Run (body vars) t vars'" + and "Run (cond vars') t' False" + shows "untilM_dom (vars', cond, body)" + by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\<close>) + (auto intro: untilM.domintros) + +lemma untilM_dom_ex_step: + assumes "untilM_dom (vars, cond, body)" + and "\<exists>t. Run (body vars) t vars'" + and "\<exists>t'. Run (cond vars') t' False" + shows "untilM_dom (vars', cond, body)" + using assms by (blast intro: untilM_dom_step) + +lemma liftState_untilM: + assumes "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + and "untilM_dom (vars, cond, body)" + shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" +proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: untilS.pinduct\<close>) + case Step: (1 vars s) + note domS = Step(1) and IH = Step(2) and domM = Step(3) + show ?case unfolding untilS.psimps[OF domS] untilM.psimps[OF domM] liftState_bind + proof (intro bindS_ext_cong, goal_cases body k) + case (k vars' s') + show ?case unfolding comp_def liftState_bind + proof (intro bindS_ext_cong, goal_cases cond until) + case (until a s'') + have "untilM_dom (vars', cond, body)" if "\<not>a" + proof (rule untilM_dom_ex_step[OF domM]) + show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run) + show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run) + qed + then show ?case using k until IH by (auto simp: comp_def liftState_simp) + qed auto + qed auto +qed*) + +Lemma liftState_untilM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s : + liftState (Regs := RV) r (untilMT vars measure cond body) s = untilST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s. +unfold untilMT, untilST. +generalize (measure vars) as limit. intro. +revert vars s. +destruct (Z.le_decidable 0 limit). +* generalize (Zwf_guarded limit) as acc. + apply Wf_Z.natlike_ind with (x := limit). + + intros [acc] *; simpl. + autorewrite with liftState. + apply bindS_ext_cong; auto. + intros. autorewrite with liftState. + apply bindS_ext_cong; auto. + intros. rewrite liftState_if_distrib. + destruct a0; auto. + destruct (_limit_reduces _). simpl. + reflexivity. + + clear limit H. + intros limit H IH [acc] vars s. simpl. + destruct (Z_ge_dec _ _); try omega. + autorewrite with liftState. + apply bindS_ext_cong; auto. + intros. autorewrite with liftState; auto. + apply bindS_ext_cong; auto. + intros. rewrite liftState_if_distrib. + destruct a0; autorewrite with liftState; auto. + gen_reduces. + replace (Z.succ limit - 1) with limit; try omega. intro acc'. + apply IH. + + assumption. +* intros. simpl. + destruct (Z_ge_dec _ _); try omega. + reflexivity. +Qed. + +(* + +text \<open>Simplification rules for monadic Boolean connectives\<close> + +lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto + +lemma and_boolM_simps[simp]: + "and_boolM (return b) (return c) = return (b \<and> c)" + "and_boolM x (return True) = x" + "and_boolM x (return False) = x \<bind> (\<lambda>_. return False)" + "\<And>x y z. and_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. and_boolM (y r) z))" + by (auto simp: and_boolM_def) + +lemma and_boolM_return_if: + "and_boolM (return b) y = (if b then y else return False)" + by (auto simp: and_boolM_def) + +lemma and_boolM_return_return_and[simp]: "and_boolM (return l) (return r) = return (l \<and> r)" + by (auto simp: and_boolM_def) + +lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolM x y" for y] + +lemma or_boolM_simps[simp]: + "or_boolM (return b) (return c) = return (b \<or> c)" + "or_boolM x (return True) = x \<bind> (\<lambda>_. return True)" + "or_boolM x (return False) = x" + "\<And>x y z. or_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. or_boolM (y r) z))" + by (auto simp: or_boolM_def) + +lemma or_boolM_return_if: + "or_boolM (return b) y = (if b then return True else y)" + by (auto simp: or_boolM_def) + +lemma or_boolM_return_return_or[simp]: "or_boolM (return l) (return r) = return (l \<or> r)" + by (auto simp: or_boolM_def) + +lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolM x y" for y] + +lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto + +lemma and_boolS_simps[simp]: + "and_boolS (returnS b) (returnS c) = returnS (b \<and> c)" + "and_boolS x (returnS True) = x" + "and_boolS x (returnS False) = bindS x (\<lambda>_. returnS False)" + "\<And>x y z. and_boolS (bindS x y) z = (bindS x (\<lambda>r. and_boolS (y r) z))" + by (auto simp: and_boolS_def) + +lemma and_boolS_returnS_if: + "and_boolS (returnS b) y = (if b then y else returnS False)" + by (auto simp: and_boolS_def) + +lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y] + +lemma and_boolS_returnS_True[simp]: "and_boolS (returnS True) c = c" + by (auto simp: and_boolS_def) + +lemma or_boolS_simps[simp]: + "or_boolS (returnS b) (returnS c) = returnS (b \<or> c)" + "or_boolS (returnS False) m = m" + "or_boolS x (returnS True) = bindS x (\<lambda>_. returnS True)" + "or_boolS x (returnS False) = x" + "\<And>x y z. or_boolS (bindS x y) z = (bindS x (\<lambda>r. or_boolS (y r) z))" + by (auto simp: or_boolS_def) + +lemma or_boolS_returnS_if: + "or_boolS (returnS b) y = (if b then returnS True else y)" + by (auto simp: or_boolS_def) + +lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y] + +lemma Run_or_boolM_E: + assumes "Run (or_boolM l r) t a" + obtains "Run l t True" and "a" + | tl tr where "Run l tl False" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: or_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma Run_and_boolM_E: + assumes "Run (and_boolM l r) t a" + obtains "Run l t False" and "\<not>a" + | tl tr where "Run l tl True" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: and_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" + by (auto simp: maybe_failS_def) + +text \<open>Event traces\<close> + +lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" + unfolding bind_eq_Some_conv[symmetric] by auto + +lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma emitEventS_update_cases: + assumes "emitEventS ra e s = Some s'" + obtains + (Write_mem) wk addr sz v tag r + where "e = E_write_memt wk addr sz v tag r \<or> (e = E_write_mem wk addr sz v r \<and> tag = B0)" + and "s' = put_mem_bytes addr sz v tag s" + | (Write_reg) r v rs' + where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'" + and "s' = s\<lparr>regstate := rs'\<rparr>" + | (Read) "s' = s" + using assms + by (elim emitEventS.elims) + (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff) + +lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s" + by (cases "emitEventS ra e s"; auto) + +lemma runTraceS_ConsE: + assumes "runTraceS ra (e # t) s = Some s'" + obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'" + using assms by (auto simp: bind_eq_Some_conv) + +lemma runTraceS_ConsI: + assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''" + shows "runTraceS ra (e # t) s = Some s''" + using assms by auto + +lemma runTraceS_Cons_tl: + assumes "emitEventS ra e s = Some s'" + shows "runTraceS ra (e # t) s = runTraceS ra t s'" + using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv) + +lemma runTraceS_appendE: + assumes "runTraceS ra (t @ t') s = Some s'" + obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'" +proof - + have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'" + proof (use assms in \<open>induction t arbitrary: s\<close>) + case (Cons e t) + from Cons.prems + obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'" + by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv) + with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI) + qed auto + then show ?thesis using that by blast +qed + +lemma runTraceS_nth_split: + assumes "runTraceS ra t s = Some s'" and n: "n < length t" + obtains s1 s2 where "runTraceS ra (take n t) s = Some s1" + and "emitEventS ra (t ! n) s1 = Some s2" + and "runTraceS ra (drop (Suc n) t) s2 = Some s'" +proof - + have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'" + using assms + by (auto simp: id_take_nth_drop[OF n, symmetric]) + then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that) +qed + +text \<open>Memory accesses\<close> + +lemma get_mem_bytes_put_mem_bytes_same_addr: + assumes "length v = sz" + shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)" +proof (unfold assms[symmetric], induction v rule: rev_induct) + case Nil + then show ?case by (auto simp: get_mem_bytes_def) +next + case (snoc x xs) + then show ?case + by (cases tag) + (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff + cong: option.case_cong split: if_splits option.splits) +qed + +lemma memstate_put_mem_bytes: + assumes "length v = sz" + shows "memstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma tagstate_put_mem_bytes: + assumes "length v = sz" + shows "tagstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma get_mem_bytes_cong: + assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow> + (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')" + shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s" +proof (use assms in \<open>induction sz\<close>) + case 0 + then show ?case by (auto simp: get_mem_bytes_def) +next + case (Suc sz) + then show ?case + by (auto simp: get_mem_bytes_def Let_def + intro!: map_option_cong map_cong foldl_cong + arg_cong[where f = just_list] arg_cong2[where f = and_bit]) +qed + +lemma get_mem_bytes_tagged_tagstate: + assumes "get_mem_bytes addr sz s = Some (v, B1)" + shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1" + using assms + by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits) + +end +*)
\ No newline at end of file diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v index 235e4b9e..faee9569 100644 --- a/lib/coq/Sail2_state_monad.v +++ b/lib/coq/Sail2_state_monad.v @@ -50,10 +50,10 @@ Definition returnS {Regs A E} (a:A) : monadS Regs A E := fun s => [(Value a,s)]. (*val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e*) Definition bindS {Regs A B E} (m : monadS Regs A E) (f : A -> monadS Regs B E) : monadS Regs B E := fun (s : sequential_state Regs) => - List.concat (List.map (fun v => match v with - | (Value a, s') => f a s' - | (Ex e, s') => [(Ex e, s')] - end) (m s)). + List.flat_map (fun v => match v with + | (Value a, s') => f a s' + | (Ex e, s') => [(Ex e, s')] + end) (m s). (*val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e*) Definition seqS {Regs B E} (m : monadS Regs unit E) (n : monadS Regs B E) : monadS Regs B E := @@ -96,11 +96,11 @@ Definition throwS {Regs A E} (e : E) :monadS Regs A E := (*val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) -> monadS 'regs 'a 'e2*) Definition try_catchS {Regs A E1 E2} (m : monadS Regs A E1) (h : E1 -> monadS Regs A E2) : monadS Regs A E2 := fun s => - List.concat (List.map (fun v => match v with + List.flat_map (fun v => match v with | (Value a, s') => returnS a s' | (Ex (Throw e), s') => h e s' | (Ex (Failure msg), s') => [(Ex (Failure msg), s')] - end) (m s)). + end) (m s). (*val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e*) Definition assert_expS {Regs E} (exp : bool) (msg : string) : monadS Regs unit E := diff --git a/lib/coq/Sail2_state_monad_lemmas.v b/lib/coq/Sail2_state_monad_lemmas.v new file mode 100644 index 00000000..e2b98d79 --- /dev/null +++ b/lib/coq/Sail2_state_monad_lemmas.v @@ -0,0 +1,479 @@ +Require Import Sail2_state_monad. +(*Require Import Sail2_values_lemmas.*) + +Lemma bindS_ext_cong (*[fundef_cong]:*) {Regs A B E} + {m1 m2 : monadS Regs A E} {f1 f2 : A -> monadS Regs B E} s : + m1 s = m2 s -> + (forall a s', List.In (Value a, s') (m2 s) -> f1 a s' = f2 a s') -> + bindS m1 f1 s = bindS m2 f2 s. +intros. +unfold bindS. +rewrite H. +rewrite !List.flat_map_concat_map. +f_equal. +apply List.map_ext_in. +intros [[a|a] s'] H_in; auto. +Qed. + +(* +lemma bindS_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\<And>s a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" + shows "bindS m1 f1 = bindS m2 f2" + using assms by (intro ext bindS_ext_cong; blast) +*) + +Lemma bindS_returnS_left (*[simp]:*) {Regs A B E} {x : A} {f : A -> monadS Regs B E} {s} : + bindS (returnS x) f s = f x s. +unfold returnS, bindS. +simpl. +auto using List.app_nil_r. +Qed. + +Lemma bindS_returnS_right (*[simp]:*) {Regs A E} {m : monadS Regs A E} {s} : + bindS m returnS s = m s. +unfold returnS, bindS. +induction (m s) as [|[[a|a] s'] t]; auto; +simpl; +rewrite IHt; +reflexivity. +Qed. + +Lemma bindS_readS {Regs A E} {f} {m : A -> monadS Regs A E} {s} : + bindS (readS f) m s = m (f s) s. +unfold readS, bindS. +simpl. +rewrite List.app_nil_r. +reflexivity. +Qed. + +Lemma bindS_updateS {Regs A E} {f : sequential_state Regs -> sequential_state Regs} {m : unit -> monadS Regs A E} {s} : + bindS (updateS f) m s = m tt (f s). +unfold updateS, bindS. +simpl. +auto using List.app_nil_r. +Qed. + +Lemma bindS_assertS_True (*[simp]:*) {Regs A E msg} {f : unit -> monadS Regs A E} {s} : + bindS (assert_expS true msg) f s = f tt s. +unfold assert_expS, bindS. +simpl. +auto using List.app_nil_r. +Qed. + +Lemma bindS_chooseS_returnS (*[simp]:*) {Regs A B E} {xs : list A} {f : A -> B} {s} : + bindS (Regs := Regs) (E := E) (chooseS xs) (fun x => returnS (f x)) s = chooseS (List.map f xs) s. +unfold chooseS, bindS, returnS. +induction xs; auto. +simpl. rewrite IHxs. +reflexivity. +Qed. + +Lemma result_cases : forall (A E : Type) (P : result A E -> Prop), + (forall a, P (Value a)) -> + (forall e, P (Ex (Throw e))) -> + (forall msg, P (Ex (Failure msg))) -> + forall r, P r. +intros. +destruct r; auto. +destruct e; auto. +Qed. + +Lemma result_state_cases {A E S} {P : result A E * S -> Prop} : + (forall a s, P (Value a, s)) -> + (forall e s, P (Ex (Throw e), s)) -> + (forall msg s, P (Ex (Failure msg), s)) -> + forall rs, P rs. +intros. +destruct rs as [[a|[e|msg]] s]; auto. +Qed. + +(* TODO: needs sets, not lists +Lemma monadS_ext_eqI {Regs A E} {m m' : monadS Regs A E} s : + (forall a s', List.In (Value a, s') (m s) <-> List.In (Value a, s') (m' s)) -> + (forall e s', List.In (Ex (Throw e), s') (m s) <-> List.In (Ex (Throw e), s') (m' s)) -> + (forall msg s', List.In (Ex (Failure msg), s') (m s) <-> List.In (Ex (Failure msg), s') (m' s)) -> + m s = m' s. +proof (intro set_eqI) + fix x + show "x \<in> m s \<longleftrightarrow> x \<in> m' s" using assms by (cases x rule: result_state_cases) auto +qed + +lemma monadS_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\<And>s a s'. (Value a, s') \<in> m s \<longleftrightarrow> (Value a, s') \<in> m' s" + and "\<And>s e s'. (Ex (Throw e), s') \<in> m s \<longleftrightarrow> (Ex (Throw e), s') \<in> m' s" + and "\<And>s msg s'. (Ex (Failure msg), s') \<in> m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m' s" + shows "m = m'" + using assms by (intro ext monadS_ext_eqI) +*) + +Lemma bindS_cases {Regs A B E} {m} {f : A -> monadS Regs B E} {r s s'} : + List.In (r, s') (bindS m f s) -> + (exists a a' s'', r = Value a /\ List.In (Value a', s'') (m s) /\ List.In (Value a, s') (f a' s'')) \/ + (exists e, r = Ex e /\ List.In (Ex e, s') (m s)) \/ + (exists e a s'', r = Ex e /\ List.In (Value a, s'') (m s) /\ List.In (Ex e, s') (f a s'')). +unfold bindS. +intro IN. +apply List.in_flat_map in IN. +destruct IN as [[r' s''] [INr' INr]]. +destruct r' as [a'|e']. +* destruct r as [a|e]. + + left. eauto 10. + + right; right. eauto 10. +* right; left. simpl in INr. destruct INr as [|[]]. inversion H. subst. eauto 10. +Qed. + +Lemma bindS_intro_Value {Regs A B E} {m} {f : A -> monadS Regs B E} {s a s' a' s''} : + List.In (Value a', s'') (m s) -> List.In (Value a, s') (f a' s'') -> List.In (Value a, s') (bindS m f s). +intros; unfold bindS. +apply List.in_flat_map. +eauto. +Qed. +Lemma bindS_intro_Ex_left {Regs A B E} {m} {f : A -> monadS Regs B E} {s e s'} : + List.In (Ex e, s') (m s) -> List.In (Ex e, s') (bindS m f s). +intros; unfold bindS. +apply List.in_flat_map. +exists (Ex e, s'). +auto with datatypes. +Qed. +Lemma bindS_intro_Ex_right {Regs A B E} {m} {f : A -> monadS Regs B E} {s e s' a s''} : + List.In (Ex e, s') (f a s'') -> List.In (Value a, s'') (m s) -> List.In (Ex e, s') (bindS m f s). +intros; unfold bindS. +apply List.in_flat_map. +eauto. +Qed. +Hint Resolve bindS_intro_Value bindS_intro_Ex_left bindS_intro_Ex_right : bindS_intros. + +Lemma bindS_assoc (*[simp]:*) {Regs A B C E} {m} {f : A -> monadS Regs B E} {g : B -> monadS Regs C E} {s} : + bindS (bindS m f) g s = bindS m (fun x => bindS (f x) g) s. +unfold bindS. +induction (m s) as [ | [[a | e] t]]. +* reflexivity. +* simpl. rewrite <- IHl. + rewrite !List.flat_map_concat_map. + rewrite List.map_app. + rewrite List.concat_app. + reflexivity. +* simpl. rewrite IHl. reflexivity. +Qed. + +Lemma bindS_failS (*[simp]:*) {Regs A B E} {msg} {f : A -> monadS Regs B E} : + bindS (failS msg) f = failS msg. +reflexivity. +Qed. +Lemma bindS_throwS (*[simp]:*) {Regs A B E} {e} {f : A -> monadS Regs B E} : + bindS (throwS e) f = throwS e. +reflexivity. +Qed. +(*declare seqS_def[simp]*) + +Lemma Value_bindS_elim {Regs A B E} {a m} {f : A -> monadS Regs B E} {s s'} : + List.In (Value a, s') (bindS m f s) -> + exists s'' a', List.In (Value a', s'') (m s) /\ List.In (Value a, s') (f a' s''). +intro H. +apply bindS_cases in H. +destruct H as [(a0 & a' & s'' & [= <-] & [*]) | [(e & [= ] & _) | (_ & _ & _ & [= ] & _)]]. +eauto. +Qed. + +Lemma Ex_bindS_elim {Regs A B E} {e m s s'} {f : A -> monadS Regs B E} : + List.In (Ex e, s') (bindS m f s) -> + List.In (Ex e, s') (m s) \/ + exists s'' a', List.In (Value a', s'') (m s) /\ List.In (Ex e, s') (f a' s''). +intro H. +apply bindS_cases in H. +destruct H as [(? & ? & ? & [= ] & _) | [(? & [= <-] & X) | (? & ? & ? & [= <-] & X)]]; +eauto. +Qed. + +Lemma try_catchS_returnS (*[simp]:*) {Regs A E1 E2} {a} {h : E1 -> monadS Regs A E2}: + try_catchS (returnS a) h = returnS a. +reflexivity. +Qed. +Lemma try_catchS_failS (*[simp]:*) {Regs A E1 E2} {msg} {h : E1 -> monadS Regs A E2}: + try_catchS (failS msg) h = failS msg. +reflexivity. +Qed. +Lemma try_catchS_throwS (*[simp]:*) {Regs A E1 E2} {e} {h : E1 -> monadS Regs A E2} {s}: + try_catchS (throwS e) h s = h e s. +unfold try_catchS, throwS. +simpl. +auto using List.app_nil_r. +Qed. + +Lemma try_catchS_cong (*[cong]:*) {Regs A E1 E2 m1 m2} {h1 h2 : E1 -> monadS Regs A E2} {s} : + (forall s, m1 s = m2 s) -> + (forall e s, h1 e s = h2 e s) -> + try_catchS m1 h1 s = try_catchS m2 h2 s. +intros H1 H2. +unfold try_catchS. +rewrite H1. +rewrite !List.flat_map_concat_map. +f_equal. +apply List.map_ext_in. +intros [[a|[e|msg]] s'] H_in; auto. +Qed. + +Lemma try_catchS_cases {Regs A E1 E2 m} {h : E1 -> monadS Regs A E2} {r s s'} : + List.In (r, s') (try_catchS m h s) -> + (exists a, r = Value a /\ List.In (Value a, s') (m s)) \/ + (exists msg, r = Ex (Failure msg) /\ List.In (Ex (Failure msg), s') (m s)) \/ + (exists e s'', List.In (Ex (Throw e), s'') (m s) /\ List.In (r, s') (h e s'')). +unfold try_catchS. +intro IN. +apply List.in_flat_map in IN. +destruct IN as [[r' s''] [INr' INr]]. +destruct r' as [a'|[e'|msg]]. +* left. simpl in INr. destruct INr as [[= <- <-] | []]. eauto 10. +* simpl in INr. destruct INr as [[= <- <-] | []]. eauto 10. +* eauto 10. +Qed. + +Lemma try_catchS_intros {Regs A E1 E2} {m} {h : E1 -> monadS Regs A E2} : + (forall s a s', List.In (Value a, s') (m s) -> List.In (Value a, s') (try_catchS m h s)) /\ + (forall s msg s', List.In (Ex (Failure msg), s') (m s) -> List.In (Ex (Failure msg), s') (try_catchS m h s)) /\ + (forall s e s'' r s', List.In (Ex (Throw e), s'') (m s) -> List.In (r, s') (h e s'') -> List.In (r, s') (try_catchS m h s)). +repeat split; unfold try_catchS; intros; +apply List.in_flat_map. +* eexists; split; [ apply H | ]. simpl. auto. +* eexists; split; [ apply H | ]. simpl. auto. +* eexists; split; [ apply H | ]. simpl. auto. +Qed. + +Lemma no_Ex_basic_builtins (*[simp]:*) {Regs E} {s s' : sequential_state Regs} {e : ex E} : + (forall A (a:A), ~ List.In (Ex e, s') (returnS a s)) /\ + (forall A (f : _ -> A), ~ List.In (Ex e, s') (readS f s)) /\ + (forall f, ~ List.In (Ex e, s') (updateS f s)) /\ + (forall A (xs : list A), ~ List.In (Ex e, s') (chooseS xs s)). +repeat split; intros; +unfold returnS, readS, updateS, chooseS; simpl; +try intuition congruence. +* intro H. + apply List.in_map_iff in H. + destruct H as [x [X _]]. + congruence. +Qed. + +Import List.ListNotations. +Definition ignore_throw_aux {A E1 E2 S} (rs : result A E1 * S) : list (result A E2 * S) := +match rs with +| (Value a, s') => [(Value a, s')] +| (Ex (Throw e), s') => [] +| (Ex (Failure msg), s') => [(Ex (Failure msg), s')] +end. +Definition ignore_throw {A E1 E2 S} (m : S -> list (result A E1 * S)) s : list (result A E2 * S) := + List.flat_map ignore_throw_aux (m s). + +Lemma ignore_throw_cong {A E1 E2 S} {m1 m2 : S -> list (result A E1 * S)} s : + (forall s, m1 s = m2 s) -> + ignore_throw (E2 := E2) m1 s = ignore_throw m2 s. +intro H. +unfold ignore_throw. +rewrite H. +reflexivity. +Qed. + +Lemma ignore_throw_aux_member_simps (*[simp]:*) {A E1 E2 S} {s' : S} {ms} : + (forall a:A, List.In (Value a, s') (ignore_throw_aux (E1 := E1) (E2 := E2) ms) <-> ms = (Value a, s')) /\ + (forall e, ~ List.In (Ex (E := E2) (Throw e), s') (ignore_throw_aux ms)) /\ + (forall msg, List.In (Ex (E := E2) (Failure msg), s') (ignore_throw_aux ms) <-> ms = (Ex (Failure msg), s')). +destruct ms as [[a' | [e' | msg']] s]; simpl; +intuition congruence. +Qed. + +Lemma ignore_throw_member_simps (*[simp]:*) {A E1 E2 S} {s s' : S} {m} : + (forall {a:A}, List.In (Value (E := E2) a, s') (ignore_throw m s) <-> List.In (Value (E := E1) a, s') (m s)) /\ + (forall {a:A}, List.In (Value (E := E2) a, s') (ignore_throw m s) <-> List.In (Value a, s') (m s)) /\ + (forall e, ~ List.In (Ex (E := E2) (Throw e), s') (ignore_throw m s)) /\ + (forall {msg}, List.In (Ex (E := E2) (Failure msg), s') (ignore_throw m s) <-> List.In (Ex (Failure msg), s') (m s)). +unfold ignore_throw. +repeat apply conj; intros; try apply conj; +rewrite ?List.in_flat_map; +solve +[ intros [x [H1 H2]]; apply ignore_throw_aux_member_simps in H2; congruence +| intro H; eexists; split; [ apply H | apply ignore_throw_aux_member_simps; reflexivity] ]. +Qed. + +Lemma ignore_throw_cases {A E S} {m : S -> list (result A E * S)} {r s s'} : + ignore_throw m s = m s -> + List.In (r, s') (m s) -> + (exists a, r = Value a) \/ + (exists msg, r = Ex (Failure msg)). +destruct r as [a | [e | msg]]; eauto. +* intros H1 H2. rewrite <- H1 in H2. + apply ignore_throw_member_simps in H2. + destruct H2. +Qed. + +(* *** *) +Lemma flat_map_app {A B} {f : A -> list B} {l1 l2} : + List.flat_map f (l1 ++ l2) = (List.flat_map f l1 ++ List.flat_map f l2)%list. +rewrite !List.flat_map_concat_map. +rewrite List.map_app, List.concat_app. +reflexivity. +Qed. + +Lemma ignore_throw_bindS (*[simp]:*) Regs A B E E2 {m} {f : A -> monadS Regs B E} {s} : + ignore_throw (E2 := E2) (bindS m f) s = bindS (ignore_throw m) (fun s => ignore_throw (f s)) s. +unfold bindS, ignore_throw. +induction (m s) as [ | [[a | [e | msg]] t]]. +* reflexivity. +* simpl. rewrite <- IHl. rewrite flat_map_app. reflexivity. +* simpl. rewrite <- IHl. reflexivity. +* simpl. apply IHl. +Qed. +Hint Rewrite ignore_throw_bindS : ignore_throw. + +Lemma try_catchS_bindS_no_throw {Regs A B E1 E2} {m1 : monadS Regs A E1} {m2 : monadS Regs A E2} {f : A -> monadS Regs B _} {s h} : + (forall s, ignore_throw m1 s = m1 s) -> + (forall s, ignore_throw m1 s = m2 s) -> + try_catchS (bindS m1 f) h s = bindS m2 (fun a => try_catchS (f a) h) s. +intros Ignore1 Ignore2. +transitivity ((ignore_throw m1 >>$= (fun a => try_catchS (f a) h)) s). +* unfold bindS, try_catchS, ignore_throw. + specialize (Ignore1 s). revert Ignore1. unfold ignore_throw. + induction (m1 s) as [ | [[a | [e | msg]] t]]; auto. + + intro Ig. simpl. rewrite flat_map_app. rewrite IHl. auto. injection Ig. auto. + + intro Ig. simpl. rewrite IHl. reflexivity. injection Ig. auto. + + intro Ig. exfalso. clear -Ig. + assert (List.In (Ex (Throw msg), t) (List.flat_map ignore_throw_aux l)). + simpl in Ig. rewrite Ig. simpl. auto. + apply List.in_flat_map in H. + destruct H as [x [H1 H2]]. + apply ignore_throw_aux_member_simps in H2. + assumption. +* apply bindS_ext_cong; auto. +Qed. + +Lemma concat_map_singleton {A B} {f : A -> B} {a : list A} : + List.concat (List.map (fun x => [f x]%list) a) = List.map f a. +induction a; simpl; try rewrite IHa; auto with datatypes. +Qed. + +(*lemma no_throw_basic_builtins[simp]:*) +Lemma no_throw_basic_builtins_1 Regs A E E2 {a : A} : + ignore_throw (E1 := E2) (returnS a) = @returnS Regs A E a. +reflexivity. Qed. +Lemma no_throw_basic_builtins_2 Regs A E E2 {f : sequential_state Regs -> A} : + ignore_throw (E1 := E) (E2 := E2) (readS f) = readS f. +reflexivity. Qed. +Lemma no_throw_basic_builtins_3 Regs E E2 {f : sequential_state Regs -> sequential_state Regs} : + ignore_throw (E1 := E) (E2 := E2) (updateS f) = updateS f. +reflexivity. Qed. +Lemma no_throw_basic_builtins_4 Regs A E1 E2 {xs : list A} s : + ignore_throw (E1 := E1) (chooseS xs) s = @chooseS Regs A E2 xs s. +unfold ignore_throw, chooseS. +rewrite List.flat_map_concat_map, List.map_map. simpl. +rewrite concat_map_singleton. +reflexivity. +Qed. +Lemma no_throw_basic_builtins_5 Regs E1 E2 : + ignore_throw (E1 := E1) (choose_boolS tt) = @choose_boolS Regs E2 tt. +reflexivity. Qed. +Lemma no_throw_basic_builtins_6 Regs A E1 E2 msg : + ignore_throw (E1 := E1) (failS msg) = @failS Regs A E2 msg. +reflexivity. Qed. +Lemma no_throw_basic_builtins_7 Regs A E1 E2 msg x : + ignore_throw (E1 := E1) (maybe_failS msg x) = @maybe_failS Regs A E2 msg x. +destruct x; reflexivity. Qed. + +Hint Rewrite no_throw_basic_builtins_1 no_throw_basic_builtins_2 + no_throw_basic_builtins_3 no_throw_basic_builtins_4 + no_throw_basic_builtins_5 no_throw_basic_builtins_6 + no_throw_basic_builtins_7 : ignore_throw. + +Lemma ignore_throw_option_case_distrib_1 Regs B C E1 E2 (c : sequential_state Regs -> option B) s (n : monadS Regs C E1) (f : B -> monadS Regs C E1) : + ignore_throw (E2 := E2) (match c s with None => n | Some b => f b end) s = + match c s with None => ignore_throw n s | Some b => ignore_throw (f b) s end. +destruct (c s); auto. +Qed. +Lemma ignore_throw_option_case_distrib_2 Regs B C E1 E2 (c : option B) (n : monadS Regs C E1) (f : B -> monadS Regs C E1) : + ignore_throw (E2 := E2) (match c with None => n | Some b => f b end) = + match c with None => ignore_throw n | Some b => ignore_throw (f b) end. +destruct c; auto. +Qed. + +Lemma ignore_throw_let_distrib Regs A B E1 E2 (y : A) (f : A -> monadS Regs B E1) : + ignore_throw (E2 := E2) (let x := y in f x) = (let x := y in ignore_throw (f x)). +reflexivity. +Qed. + +Lemma no_throw_mem_builtins_1 Regs E1 E2 rk a sz s : + ignore_throw (E2 := E2) (@read_memt_bytesS Regs E1 rk a sz) s = read_memt_bytesS rk a sz s. +unfold read_memt_bytesS. autorewrite with ignore_throw. +apply bindS_ext_cong; auto. intros. autorewrite with ignore_throw. reflexivity. +Qed. +Hint Rewrite no_throw_mem_builtins_1 : ignore_throw. +Lemma no_throw_mem_builtins_2 Regs E1 E2 rk a sz s : + ignore_throw (E2 := E2) (@read_mem_bytesS Regs E1 rk a sz) s = read_mem_bytesS rk a sz s. +unfold read_mem_bytesS. autorewrite with ignore_throw. +apply bindS_ext_cong; intros; autorewrite with ignore_throw; auto. +destruct a0; reflexivity. +Qed. +Hint Rewrite no_throw_mem_builtins_2 : ignore_throw. +Lemma no_throw_mem_builtins_3 Regs A E1 E2 a s : + ignore_throw (E2 := E2) (@read_tagS Regs A E1 a) s = read_tagS a s. +reflexivity. Qed. +Hint Rewrite no_throw_mem_builtins_3 : ignore_throw. +Lemma no_throw_mem_builtins_4 Regs A V E1 E2 rk a sz s H : + ignore_throw (E2 := E2) (@read_memtS Regs E1 A V rk a sz H) s = read_memtS rk a sz s. +unfold read_memtS. autorewrite with ignore_throw. +apply bindS_ext_cong; intros; autorewrite with ignore_throw. +reflexivity. destruct a0; simpl. autorewrite with ignore_throw. +reflexivity. +Qed. +Hint Rewrite no_throw_mem_builtins_4 : ignore_throw. +Lemma no_throw_mem_builtins_5 Regs A V E1 E2 rk a sz s H : + ignore_throw (E2 := E2) (@read_memS Regs E1 A V rk a sz H) s = read_memS rk a sz s. +unfold read_memS. autorewrite with ignore_throw. +apply bindS_ext_cong; intros; autorewrite with ignore_throw; auto. +destruct a0; auto. +Qed. +Hint Rewrite no_throw_mem_builtins_5 : ignore_throw. +Lemma no_throw_mem_builtins_6 Regs E1 E2 wk addr sz v t s : + ignore_throw (E2 := E2) (@write_memt_bytesS Regs E1 wk addr sz v t) s = write_memt_bytesS wk addr sz v t s. +unfold write_memt_bytesS. unfold seqS. autorewrite with ignore_throw. +reflexivity. +Qed. +Hint Rewrite no_throw_mem_builtins_6 : ignore_throw. +Lemma no_throw_mem_builtins_7 Regs E1 E2 wk addr sz v s : + ignore_throw (E2 := E2) (@write_mem_bytesS Regs E1 wk addr sz v) s = write_mem_bytesS wk addr sz v s. +unfold write_mem_bytesS. autorewrite with ignore_throw. reflexivity. +Qed. +Hint Rewrite no_throw_mem_builtins_7 : ignore_throw. +Lemma no_throw_mem_builtins_8 Regs E1 E2 A B wk addr sz v t s : + ignore_throw (E2 := E2) (@write_memtS Regs E1 A B wk addr sz v t) s = write_memtS wk addr sz v t s. +unfold write_memtS. rewrite ignore_throw_option_case_distrib_2. +destruct (Sail2_values.mem_bytes_of_bits v); autorewrite with ignore_throw; auto. +Qed. +Hint Rewrite no_throw_mem_builtins_8 : ignore_throw. +Lemma no_throw_mem_builtins_9 Regs E1 E2 A B wk addr sz v s : + ignore_throw (E2 := E2) (@write_memS Regs E1 A B wk addr sz v) s = write_memS wk addr sz v s. +unfold write_memS. autorewrite with ignore_throw; auto. +Qed. +Hint Rewrite no_throw_mem_builtins_9 : ignore_throw. +Lemma no_throw_mem_builtins_10 Regs E1 E2 s : + ignore_throw (E2 := E2) (@excl_resultS Regs E1 tt) s = excl_resultS tt s. +reflexivity. Qed. +Hint Rewrite no_throw_mem_builtins_10 : ignore_throw. +Lemma no_throw_mem_builtins_11 Regs E1 E2 s : + ignore_throw (E2 := E2) (@undefined_boolS Regs E1 tt) s = undefined_boolS tt s. +reflexivity. Qed. +Hint Rewrite no_throw_mem_builtins_11 : ignore_throw. + +Lemma no_throw_read_regvalS Regs RV E1 E2 r reg_name s : + ignore_throw (E2 := E2) (@read_regvalS Regs RV E1 r reg_name) s = read_regvalS r reg_name s. +destruct r; simpl. autorewrite with ignore_throw. +apply bindS_ext_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2. +autorewrite with ignore_throw. reflexivity. +Qed. +Hint Rewrite no_throw_read_regvalS : ignore_throw. + +Lemma no_throw_write_regvalS Regs RV E1 E2 r reg_name v s : + ignore_throw (E2 := E2) (@write_regvalS Regs RV E1 r reg_name v) s = write_regvalS r reg_name v s. +destruct r; simpl. autorewrite with ignore_throw. +apply bindS_ext_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2. +autorewrite with ignore_throw. reflexivity. +Qed. +Hint Rewrite no_throw_write_regvalS : ignore_throw. 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 = { @@ -283,6 +283,13 @@ void platform_read_mem(lbits *data, const sbits addr, const mpz_t n) { + sbits sdata; + uint64_t len = mpz_get_ui(n); /* Sail type says always >0 */ + if (len <= 8) { + /* fast path for small reads */ + sdata = fast_read_ram(len, addr.bits); + RECREATE_OF(lbits, sbits)(data, sdata, true); + } else { mpz_t mpz_addr_size; mpz_init(mpz_addr_size); mpz_set_ui(mpz_addr_size, addr_size); @@ -292,6 +299,7 @@ void platform_read_mem(lbits *data, read_ram(data, mpz_addr_size, n, (lbits){.len=0, .bits=NULL}, (lbits){.len=addr.len, .bits=&addr_bv}); mpz_clear(mpz_addr_size); mpz_clear(addr_bv); + } } unit platform_write_mem_ea(const int write_kind, @@ -325,7 +333,7 @@ bool platform_excl_res(const unit unit) return true; } -unit platform_barrier(const int barrier_kind) +unit platform_barrier() { return UNIT; } @@ -86,7 +86,7 @@ bool platform_write_mem(const int write_kind, const mpz_t n, const lbits data); bool platform_excl_res(const unit unit); -unit platform_barrier(const int barrier_kind); +unit platform_barrier(); 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/optimize.ml b/src/optimize.ml index 1fc2fbe8..b0d05bef 100644 --- a/src/optimize.ml +++ b/src/optimize.ml @@ -52,43 +52,57 @@ open Ast open Ast_util open Rewriter +let rec split_at_function' id defs acc = + match defs with + | [] -> None + | ([def], env) :: defs when is_fundef id def -> Some (acc, (def, env), defs) + | (def, env) :: defs -> split_at_function' id defs ((def, env) :: acc) + +let split_at_function id defs = + match split_at_function' id defs [] with + | None -> None + | Some (pre_defs, def, post_defs) -> + Some (List.rev pre_defs, def, post_defs) + let recheck (Defs defs) = let defs = Type_check.check_with_envs Type_check.initial_env defs in let rec find_optimizations = function - | ([DEF_pragma ("optimize", pragma, p_l)], env) - :: ([DEF_spec vs as def1], _) - :: ([DEF_fundef fdef as def2], _) - :: defs -> + | ([DEF_pragma ("optimize", pragma, p_l)], env) :: ([DEF_spec vs as def1], _) :: defs -> let id = id_of_val_spec vs in let args = Str.split (Str.regexp " +") (String.trim pragma) in begin match args with | ["unroll"; n]-> let n = int_of_string n in + begin match split_at_function id defs with + | Some (intervening_defs, ((DEF_fundef fdef as def2, _)), defs) -> + let rw_app subst (fn, args) = + if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args) + in + let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in + let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in - let rw_app subst (fn, args) = - if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args) - in - let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in - let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in - - let specs = ref [def1] in - let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in + let specs = ref [def1] in + let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in - for i = 1 to n do - let current_id = append_id id ("_unroll_" ^ string_of_int i) in - let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in - (* Create a valspec for the new unrolled function *) - specs := !specs @ [DEF_spec (rename_valspec current_id vs)]; - (* Then duplicate it's function body and make it call the next unrolled function *) - bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))] - done; + for i = 1 to n do + let current_id = append_id id ("_unroll_" ^ string_of_int i) in + let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in + (* Create a valspec for the new unrolled function *) + specs := !specs @ [DEF_spec (rename_valspec current_id vs)]; + (* Then duplicate it's function body and make it call the next unrolled function *) + bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))] + done; - !specs @ !bodies @ find_optimizations defs + !specs @ List.concat (List.map fst intervening_defs) @ !bodies @ find_optimizations defs + | _ -> + Reporting.warn "Could not find function body for unroll pragma at " p_l ""; + def1 :: find_optimizations defs + end | _ -> Reporting.warn "Unrecognised optimize pragma at" p_l ""; - def1 :: def2 :: find_optimizations defs + def1 :: find_optimizations defs end | (defs, _) :: defs' -> diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 25abfed8..58c71e82 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1625,22 +1625,22 @@ let doc_exp, doc_let = ,_),body'),_) -> body' | _ -> body in - let msuffix, measure_pp = - match measure with - | None -> "", [] - | Some exp -> "T", [expY exp] - in let used_vars_body = find_e_ids body in let varstuple_pp, lambda = make_loop_vars [] varstuple in + let msuffix, measure_pp = + match measure with + | None -> "", [] + | Some exp -> "T", [parens (prefix 2 1 (group lambda) (expN exp))] + in parens ( (prefix 2 1) - ((separate space) (string (combinator ^ csuffix ^ msuffix):: - measure_pp@[varstuple_pp])) - ((prefix 0 1) - (parens (prefix 2 1 (group lambda) (expN cond))) - (parens (prefix 2 1 (group lambda) (expN body)))) + (string (combinator ^ csuffix ^ msuffix)) + (separate (break 1) + (varstuple_pp::measure_pp@ + [parens (prefix 2 1 (group lambda) (expN cond)); + parens (prefix 2 1 (group lambda) (expN body))])) ) end | Id_aux (Id "early_return", _) -> diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index fe241ee7..1367d9eb 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1150,6 +1150,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 @@ -1222,6 +1224,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/process_file.ml b/src/process_file.ml index 60261196..8b542445 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -95,10 +95,14 @@ let default_symbols = [ "FEATURE_IMPLICITS"; "FEATURE_CONSTANT_TYPES"; "FEATURE_BITVECTOR_TYPE"; + "FEATURE_UNION_BARRIER"; ] let symbols = ref default_symbols +let have_symbol symbol = + StringSet.mem symbol !symbols + let clear_symbols () = symbols := default_symbols let cond_pragma l defs = diff --git a/src/process_file.mli b/src/process_file.mli index 91cde014..55c7906b 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -53,6 +53,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val clear_symbols : unit -> unit +val have_symbol : string -> bool val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/rewrites.ml b/src/rewrites.ml index 3012e49b..87891b6d 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1034,7 +1034,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = let mk_num_exp i = mk_lit_exp (L_num i) in let check_eq_exp l r = let exp = mk_exp (E_app_infix (l, Id_aux (Operator "==", Parse_ast.Unknown), r)) in - check_exp env exp bool_typ in + check_exp (Env.no_casts env) exp bool_typ in let access_bit_exp rootid l typ idx = let access_aux = E_vector_access (mk_exp (E_id rootid), mk_num_exp idx) in @@ -3309,7 +3309,7 @@ let rewrite_lit_ocaml (L_aux (lit, _)) = match lit with | L_num _ | L_string _ | L_hex _ | L_bin _ | L_real _ | L_unit -> false | _ -> true -let rewrite_defs_pat_lits rewrite_lit env = +let rewrite_defs_pat_lits rewrite_lit env ast = let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = let guards = ref [] in let counter = ref 0 in @@ -3349,8 +3349,18 @@ let rewrite_defs_pat_lits rewrite_lit env = end in + let rewrite_funcl (FCL_aux (FCL_Funcl (id, pexp), (l, annot))) = + FCL_aux (FCL_Funcl (id, rewrite_pexp pexp), (l, annot)) in + let rewrite_fun (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, annot))) = + FD_aux (FD_function (recopt, tannotopt, effectopt, List.map rewrite_funcl funcls), (l, annot)) in + let rewrite_def = function + | DEF_fundef fdef -> DEF_fundef (rewrite_fun fdef) + | def -> def + in + let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } + let Defs defs = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in + Defs (List.map rewrite_def defs) (* Now all expressions have no blocks anymore, any term is a sequence of let-expressions, @@ -4913,13 +4923,13 @@ let rewrites_lem = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("pattern_literals", [Literal_arg "lem"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); ("remove_numeral_pats", []); + ("pattern_literals", [Literal_arg "lem"]); ("guarded_pats", []); ("bitvector_exps", []); (* ("register_ref_writes", rewrite_register_ref_writes); *) @@ -4955,13 +4965,13 @@ let rewrites_coq = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("pattern_literals", [Literal_arg "lem"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); ("remove_numeral_pats", []); + ("pattern_literals", [Literal_arg "lem"]); ("guarded_pats", []); ("bitvector_exps", []); (* ("register_ref_writes", rewrite_register_ref_writes); *) @@ -5001,13 +5011,13 @@ let rewrites_ocaml = [ ("mapping_builtins", []); ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); - ("pattern_literals", [Literal_arg "ocaml"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); ("remove_not_pats", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); + ("pattern_literals", [Literal_arg "ocaml"]); ("remove_numeral_pats", []); ("exp_lift_assign", []); ("top_sort_defs", []); @@ -5030,12 +5040,12 @@ let rewrites_c = [ ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); + ("remove_vector_concat", []); + ("remove_bitvector_pats", []); ("pattern_literals", [Literal_arg "all"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); - ("remove_vector_concat", []); - ("remove_bitvector_pats", []); ("exp_lift_assign", []); ("merge_function_clauses", []); ("optimize_recheck_defs", []); diff --git a/src/sail.ml b/src/sail.ml index e9b1914d..516b3726 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -70,6 +70,7 @@ let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None let opt_ocaml_generators = ref ([]:string list) let opt_splice = ref ([]:string list) +let opt_have_feature = ref None let set_target name = Arg.Unit (fun _ -> opt_target := Some name) @@ -276,6 +277,9 @@ let options = Arg.align ([ ( "-memo", Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); + ( "-have_feature", + Arg.String (fun symbol -> opt_have_feature := Some symbol), + " check if a feature symbol is set by default"); ( "-splice", Arg.String (fun s -> opt_splice := s :: !opt_splice), "<filename> add functions from file, replacing existing definitions where necessary"); @@ -410,6 +414,9 @@ let load_files ?check:(check=false) type_envs files = else let ast = Scattered.descatter ast in let ast, type_envs = rewrite_ast_initial type_envs ast in + (* Recheck after descattering so that the internal type environments always + have complete variant types *) + let ast, type_envs = Type_error.check Type_check.initial_env ast in let out_name = match !opt_file_out with | None when parsed = [] -> "out.sail" @@ -545,7 +552,17 @@ let target name out_name ast type_envs = | Some t -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Undefined target: " ^ t)) +let feature_check () = + match !opt_have_feature with + | None -> () + | Some symbol -> + if Process_file.have_symbol symbol then + exit 0 + else + exit 2 + let main () = + feature_check (); if !opt_print_version then print_endline version else 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 diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail index df588662..398e814f 100644 --- a/test/c/pattern_concat_nest.sail +++ b/test/c/pattern_concat_nest.sail @@ -1,27 +1,6 @@ default Order dec -type bits ('n : Int) = bitvector('n, dec) - -union option ('a : Type) = {None : unit, Some : 'a} - -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", c: "vector_subrange"} - : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm & 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) - -val bitvector_access = {ocaml: "access", lem: "access_vec_dec", c: "vector_access"} - : forall ('n : Int) ('m : Int), 0 <= 'm & 'm + 1 <= 'n. - (bits('n), atom('m)) -> bit - -overload vector_access = {bitvector_access} - -val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"}: (bit, bit) -> bool - -overload operator == = { - eq_bit -} - -val and_bool = {ocaml: "and_bool", lem: "and_bool", smt: "and_bool", interpreter: "and_bool", c: "and_bool"}: (bool, bool) -> bool - +$include <prelude.sail> //////////////////////////////////////////////////////////// diff --git a/test/c/rv_duopod_bug.expect b/test/c/rv_duopod_bug.expect new file mode 100644 index 00000000..681c7c43 --- /dev/null +++ b/test/c/rv_duopod_bug.expect @@ -0,0 +1,2 @@ +0 0x0000000000000000 +1 0xFFFFFFFFFFFFFFFF diff --git a/test/c/rv_duopod_bug.sail b/test/c/rv_duopod_bug.sail new file mode 100644 index 00000000..9a11996c --- /dev/null +++ b/test/c/rv_duopod_bug.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val rX : int -> bits(64) + +function rX 0 = sail_zeros(64) +and rX (r if r > 0) = sail_ones(64) + +function main() -> unit = { + print_bits("0 ", rX(0)); + print_bits("1 ", rX(1)) +} diff --git a/test/run_tests.sh b/test/run_tests.sh index a228e270..1af340d8 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -36,6 +36,12 @@ printf "==========================================\n" TEST_PAR=8 ./c/run_tests.py printf "\n==========================================\n" +printf "SMT tests\n" +printf "==========================================\n" + +TEST_PAR=8 ./smt/run_tests.py + +printf "\n==========================================\n" printf "Builtins tests\n" printf "==========================================\n" diff --git a/test/smt/mem_builtins.unsat.sail b/test/smt/mem_builtins.unsat.sail index 28e44658..eb003891 100644 --- a/test/smt/mem_builtins.unsat.sail +++ b/test/smt/mem_builtins.unsat.sail @@ -5,7 +5,7 @@ $include <regfp.sail> $property function prop() -> bool = { - __barrier(Barrier_DSB); + __barrier(Barrier_DSB(A64_FullShare, A64_barrier_all)); let _ = __excl_res(); __write_mem_ea(Write_exclusive_release, 32, 0xFFFF_FFFF, 8); true diff --git a/test/smt/store_load_scattered.sat.sail b/test/smt/store_load_scattered.sat.sail index d556295f..c039e87c 100644 --- a/test/smt/store_load_scattered.sat.sail +++ b/test/smt/store_load_scattered.sat.sail @@ -6,7 +6,7 @@ $include "test/arch.sail" scattered union ast -val execute : ast -> bool +val execute : ast -> bool effect {rmem, rreg, wmv, wreg} union clause ast = LOAD : (bits(2), bits(2)) |