From c56569385e4b4b1433fb07e01930d9c3b429746d Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 22 Apr 2024 15:36:20 +0100 Subject: [PATCH] Add Isabelle support for translation start/end outcomes --- .../Sail2_concurrency_interface_lemmas.thy | 8 + src/gen_lib/sail2_concurrency_interface.lem | 172 ++++++++++-------- src/gen_lib/sail2_monadic_combinators.lem | 158 ++++++++-------- .../sail2_undefined_concurrency_interface.lem | 8 +- 4 files changed, 187 insertions(+), 159 deletions(-) diff --git a/lib/isabelle/Sail2_concurrency_interface_lemmas.thy b/lib/isabelle/Sail2_concurrency_interface_lemmas.thy index 07dc68c5a..ab1b1502c 100644 --- a/lib/isabelle/Sail2_concurrency_interface_lemmas.thy +++ b/lib/isabelle/Sail2_concurrency_interface_lemmas.thy @@ -40,6 +40,8 @@ inductive_set T (*:: "(('rv, 'a, 'e) monad \ 'rv event \ ('rv, 'a, | Read_mem: "((Mem_read_request req k), E_mem_read_request req v, k v) \ T" | Write_mem: "((Mem_write_request req k), E_mem_write_request req r, k r) \ T" | Write_announce: "((Mem_write_announce_address a k), E_mem_write_announce_address a, k) \ T" +| Translation_start: "((Translation_start ts k), E_translation_start ts, k) \ T" +| Translation_end: "((Translation_end te k), E_translation_end te, k) \ T" | Branch_announce: "((Branch_announce_address a k), E_branch_announce_address a, k) \ T" | Barrier_request: "((Barrier_request r k), E_barrier_request r, k) \ T" | Cache_op_request: "((Cache_op_request r k), E_cache_op_request r, k) \ T" @@ -62,6 +64,8 @@ lemma emitEvent_cases: | (Read_mem) req k v where "m = Mem_read_request req k" and "e = E_mem_read_request req v" and "m' = k v" | (Write_mem) req k r where "m = Mem_write_request req k" and "e = E_mem_write_request req r" and "m' = k r" | (Write_announce) a k where "m = Mem_write_announce_address a k" and "e = E_mem_write_announce_address a" and "m' = k" + | (Translation_start) ts k where "m = Translation_start ts k" and "e = E_translation_start ts" and "m' = k" + | (Translation_end) te k where "m = Translation_end te k" and "e = E_translation_end te" and "m' = k" | (Branch_announce) a k where "m = Branch_announce_address a k" and "e = E_branch_announce_address a" and "m' = k" | (Barrier_request) r k where "m = Barrier_request r k" and "e = E_barrier_request r" and "m' = k" | (Cache_op_request) r k where "m = Cache_op_request r k" and "e = E_cache_op_request r" and "m' = k" @@ -109,6 +113,8 @@ lemma Traces_cases: | (Read_mem) req k t' v where "m = Mem_read_request req k" and "t = E_mem_read_request req v # t'" and "(k v, t', m') \ Traces" | (Write_mem) req k v t' where "m = Mem_write_request req k" and "t = E_mem_write_request req v # t'" and "(k v, t', m') \ Traces" | (Write_announce) a k t' where "m = Mem_write_announce_address a k" and "t = E_mem_write_announce_address a # t'" and "(k, t', m') \ Traces" + | (Translation_start) ts k t' where "m = Translation_start ts k" and "t = E_translation_start ts # t'" and "(k, t', m') \ Traces" + | (Translation_end) te k t' where "m = Translation_end te k" and "t = E_translation_end te # t'" and "(k, t', m') \ Traces" | (Branch_announce) a k t' where "m = Branch_announce_address a k" and "t = E_branch_announce_address a # t'" and "(k, t', m') \ Traces" | (Barrier) r k t' where "m = Barrier_request r k" and "t = E_barrier_request r # t'" and "(k, t', m') \ Traces" | (Cache_op) r k t' where "m = Cache_op_request r k" and "t = E_cache_op_request r # t'" and "(k, t', m') \ Traces" @@ -134,6 +140,8 @@ lemma Traces_iffs: "\req k t m'. (Mem_read_request req k, t, m') \ Traces \ (t = [] \ m' = Mem_read_request req k \ (\a t'. t = E_mem_read_request req a # t' \ (k a, t', m') \ Traces))" "\req k t m'. (Mem_write_request req k, t, m') \ Traces \ (t = [] \ m' = Mem_write_request req k \ (\a t'. t = E_mem_write_request req a # t' \ (k a, t', m') \ Traces))" "\a k t m'. (Mem_write_announce_address a k, t, m') \ Traces \ (t = [] \ m' = Mem_write_announce_address a k \ (\t'. t = E_mem_write_announce_address a # t' \ (k, t', m') \ Traces))" + "\ts k t m'. (Translation_start ts k, t, m') \ Traces \ (t = [] \ m' = Translation_start ts k \ (\t'. t = E_translation_start ts # t' \ (k, t', m') \ Traces))" + "\te k t m'. (Translation_end te k, t, m') \ Traces \ (t = [] \ m' = Translation_end te k \ (\t'. t = E_translation_end te # t' \ (k, t', m') \ Traces))" "\a k t m'. (Branch_announce_address a k, t, m') \ Traces \ (t = [] \ m' = Branch_announce_address a k \ (\t'. t = E_branch_announce_address a # t' \ (k, t', m') \ Traces))" "\req k t m'. (Barrier_request req k, t, m') \ Traces \ (t = [] \ m' = Barrier_request req k \ (\t'. t = E_barrier_request req # t' \ (k, t', m') \ Traces))" "\req k t m'. (Cache_op_request req k, t, m') \ Traces \ (t = [] \ m' = Cache_op_request req k \ (\t'. t = E_cache_op_request req # t' \ (k, t', m') \ Traces))" diff --git a/src/gen_lib/sail2_concurrency_interface.lem b/src/gen_lib/sail2_concurrency_interface.lem index cfc2f4d7c..04de44710 100644 --- a/src/gen_lib/sail2_concurrency_interface.lem +++ b/src/gen_lib/sail2_concurrency_interface.lem @@ -89,30 +89,34 @@ type Mem_write_announce_address 'pa = Mem_write_announce_address_size : integer; |> -type monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e = +type monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e = | Done of 'a | Fail of string | Exception of 'e - | Choose of string * ('regval -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e) - | Read_reg of string * ('regval -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e) - | Write_reg of string * 'regval * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | Mem_read_request of Mem_read_request_bl 'pa 'translation_summary 'arch_ak * (result (list bitU * maybe bool) 'abort -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e) - | Mem_write_request of Mem_write_request_bl 'pa 'translation_summary 'arch_ak * (result (maybe bool) 'abort -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e) - | Mem_write_announce_address of Mem_write_announce_address 'pa * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | Branch_announce_address of (list bitU) * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | Barrier_request of 'barrier * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | Cache_op_request of 'cache_op * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | TLB_op_request of 'tlb_op * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | Fault_announce of 'fault * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - | Eret_announce of 'pa * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - -type event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval = + | Choose of string * ('regval -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e) + | Read_reg of string * ('regval -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e) + | Write_reg of string * 'regval * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Mem_read_request of Mem_read_request_bl 'pa 'translation_summary 'arch_ak * (result (list bitU * maybe bool) 'abort -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e) + | Mem_write_request of Mem_write_request_bl 'pa 'translation_summary 'arch_ak * (result (maybe bool) 'abort -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e) + | Mem_write_announce_address of Mem_write_announce_address 'pa * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Translation_start of 'trans_start * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Translation_end of 'trans_end * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Branch_announce_address of (list bitU) * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Barrier_request of 'barrier * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Cache_op_request of 'cache_op * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | TLB_op_request of 'tlb_op * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Fault_announce of 'fault * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + | Eret_announce of 'pa * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + +type event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval = | E_choose of string * 'regval | E_read_reg of string * 'regval | E_write_reg of string * 'regval | E_mem_read_request of Mem_read_request_bl 'pa 'translation_summary 'arch_ak * result (list bitU * maybe bool) 'abort | E_mem_write_request of Mem_write_request_bl 'pa 'translation_summary 'arch_ak * result (maybe bool) 'abort | E_mem_write_announce_address of Mem_write_announce_address 'pa + | E_translation_start of 'trans_start + | E_translation_end of 'trans_end | E_branch_announce_address of (list bitU) | E_barrier_request of 'barrier | E_cache_op_request of 'cache_op @@ -120,17 +124,17 @@ type event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'ar | E_fault_announce of 'fault | E_eret_announce of 'pa -type trace 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval = - list (event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval) +type trace 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval = + list (event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval) -val return : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e. - 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e +val return : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e. + 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e let return a = Done a -val bind : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'b 'e. - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e -> - ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'b 'e) -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'b 'e +val bind : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'b 'e. + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e -> + ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'b 'e) -> + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'b 'e let rec bind m f = match m with | Done a -> f a | Fail msg -> Fail msg @@ -141,6 +145,8 @@ let rec bind m f = match m with | Mem_read_request req k -> Mem_read_request req (fun v -> bind (k v) f) | Mem_write_request req k -> Mem_write_request req (fun v -> bind (k v) f) | Mem_write_announce_address a k -> Mem_write_announce_address a (bind k f) + | Translation_start ts k -> Translation_start ts (bind k f) + | Translation_end te k -> Translation_end te (bind k f) | Branch_announce_address addr k -> Branch_announce_address addr (bind k f) | Barrier_request b k -> Barrier_request b (bind k f) | Cache_op_request c k -> Cache_op_request c (bind k f) @@ -149,14 +155,14 @@ let rec bind m f = match m with | Eret_announce pa k -> Eret_announce pa (bind k f) end -val throw : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e. - 'e -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e +val throw : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e. + 'e -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e let throw e = Exception e -val try_catch : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e1 'e2. - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e1 -> - ('e1 -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e2) -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e2 +val try_catch : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e1 'e2. + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e1 -> + ('e1 -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e2) -> + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e2 let rec try_catch m h = match m with | Done a -> Done a | Fail msg -> Fail msg @@ -167,6 +173,8 @@ let rec try_catch m h = match m with | Mem_read_request req k -> Mem_read_request req (fun v -> try_catch (k v) h) | Mem_write_request req k -> Mem_write_request req (fun v -> try_catch (k v) h) | Mem_write_announce_address a k -> Mem_write_announce_address a (try_catch k h) + | Translation_start ts k -> Translation_start ts (try_catch k h) + | Translation_end te k -> Translation_end te (try_catch k h) | Branch_announce_address addr k -> Branch_announce_address addr (try_catch k h) | Barrier_request b k -> Barrier_request b (try_catch k h) | Cache_op_request c k -> Cache_op_request c (try_catch k h) @@ -178,8 +186,8 @@ end (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "either 'r 'e", where "Right e" represents a proper exception and "Left r" an early return of value "r". *) -type monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'r 'e = - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a (either 'r 'e) +type monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'r 'e = + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a (either 'r 'e) (* val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e *) let early_return r = throw (Left r) @@ -224,16 +232,16 @@ let maybe_fail msg = function | Nothing -> Fail msg end -val assert_exp : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. - bool -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e +val assert_exp : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. + bool -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let assert_exp exp msg = if exp then Done () else Fail msg -val exit : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e. - unit -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e +val exit : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e. + unit -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e let exit _ = Fail "exit" -val read_reg : forall 's 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e. - register_ref 's 'regval 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e +val read_reg : forall 's 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e. + register_ref 's 'regval 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e let read_reg reg = let k v = match reg.of_regval v with @@ -245,20 +253,20 @@ let read_reg reg = let inline reg_deref = read_reg -val write_reg : forall 's 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e. - register_ref 's 'regval 'a -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e +val write_reg : forall 's 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e. + register_ref 's 'regval 'a -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) -val choose_regval : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. - string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'rv 'e +val choose_regval : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. + string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'rv 'e let choose_regval descr = Choose descr return -val choose_convert : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e 'a. - ('rv -> maybe 'a) -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val choose_convert : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e 'a. + ('rv -> maybe 'a) -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let choose_convert of_rv descr = Choose descr (fun rv -> maybe_fail descr (of_rv rv)) -val choose_convert_default : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e 'a. - ('rv -> maybe 'a) -> 'a -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val choose_convert_default : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e 'a. + ('rv -> maybe 'a) -> 'a -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let choose_convert_default of_rv x descr = Choose descr (fun rv -> return (match of_rv rv with | Just a -> a | Nothing -> x @@ -280,9 +288,9 @@ let tailM = function | [] -> Fail "tailM" end -val sail_mem_read : forall 'vasize 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'bv 'e. Size 'vasize, Bitvector 'bv => +val sail_mem_read : forall 'vasize 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'bv 'e. Size 'vasize, Bitvector 'bv => Mem_read_request 'vasize 'pa 'translation_summary 'arch_ak -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval (result ('bv * maybe bool) 'abort) 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval (result ('bv * maybe bool) 'abort) 'e let sail_mem_read req = let k = function | Ok (res, tag) -> @@ -294,63 +302,71 @@ let sail_mem_read req = end in Mem_read_request (mem_read_request_to_bl req) k -val sail_mem_write : forall 'vasize 'valuesize 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. Size 'vasize, Size 'valuesize => +val sail_mem_write : forall 'vasize 'valuesize 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. Size 'vasize, Size 'valuesize => Mem_write_request 'vasize 'pa 'translation_summary 'arch_ak 'valuesize -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval (result (maybe bool) 'abort) 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval (result (maybe bool) 'abort) 'e let sail_mem_write req = Mem_write_request (mem_write_request_to_bl req) return -val sail_mem_write_announce_address : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_mem_write_announce_address : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. Mem_write_announce_address 'pa -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_mem_write_announce_address req = Mem_write_announce_address req (return ()) -val instr_announce : forall 'instr 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_translation_start : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. + 'trans_start -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e +let sail_translation_start ts = Translation_start ts (return ()) + +val sail_translation_end : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. + 'trans_end -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e +let sail_translation_end te = Translation_end te (return ()) + +val instr_announce : forall 'instr 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'instr -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let instr_announce pa = return () (* TODO *) -val branch_announce : forall 'addr 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. Bitvector 'addr => +val branch_announce : forall 'addr 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. Bitvector 'addr => integer -> 'addr -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let branch_announce addr_size addr = Branch_announce_address (bits_of addr) (return ()) -val sail_barrier : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_barrier : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'barrier -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_barrier barrier = Barrier_request barrier (return ()) -val sail_cache_op : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_cache_op : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'cache_op -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_cache_op cache_op = Cache_op_request cache_op (return ()) -val sail_tlbi : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_tlbi : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'tlb_op -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_tlbi tlb_op = TLB_op_request tlb_op (return ()) -val sail_take_exception : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_take_exception : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'fault -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_take_exception fault = Fault_announce fault (return ()) -val sail_return_exception : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_return_exception : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'pa -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_return_exception pa = Eret_announce pa (return ()) -val sail_instr_announce : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. +val sail_instr_announce : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'e. 'pa -> - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval unit 'e let sail_instr_announce pa = return () (* Event traces *) -val emitEvent : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e. - Eq 'regval, Eq 'pa, Eq 'barrier, Eq 'cache_op, Eq 'tlb_op, Eq 'fault => - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e - -> event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval - -> maybe (monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e) +val emitEvent : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e. + Eq 'regval, Eq 'pa, Eq 'barrier, Eq 'cache_op, Eq 'tlb_op, Eq 'fault, Eq 'trans_start, Eq 'trans_end => + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e + -> event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval + -> maybe (monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e) let emitEvent m e = match (e, m) with | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing | (E_read_reg r v, Read_reg r' k) -> @@ -363,6 +379,10 @@ let emitEvent m e = match (e, m) with if req' = req then Just (k r) else Nothing | (E_mem_write_announce_address a, Mem_write_announce_address a' k) -> if a' = a then Just k else Nothing + | (E_translation_start ts, Translation_start ts' k) -> + if ts' = ts then Just k else Nothing + | (E_translation_end te, Translation_end te' k) -> + if te' = te then Just k else Nothing | (E_branch_announce_address addr, Branch_announce_address addr' k) -> if addr' = addr then Just k else Nothing | (E_barrier_request r, Barrier_request r' k) -> @@ -418,7 +438,7 @@ end in order to make switching to the state monad without changing generated definitions easier, see also lib/hol/prompt_monad.lem. *) -type base_monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'regstate 'a 'e = - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e -type base_monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'regstate 'a 'r 'e = - monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'r 'e +type base_monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'regstate 'a 'e = + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'e +type base_monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'regstate 'a 'r 'e = + monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'regval 'a 'r 'e diff --git a/src/gen_lib/sail2_monadic_combinators.lem b/src/gen_lib/sail2_monadic_combinators.lem index e14fab980..11c128d03 100644 --- a/src/gen_lib/sail2_monadic_combinators.lem +++ b/src/gen_lib/sail2_monadic_combinators.lem @@ -4,10 +4,10 @@ open import Sail2_values open import Sail2_concurrency_interface open import {isabelle} `Sail2_concurrency_interface_lemmas` -val (>>=) : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'b 'e. - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e - -> ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'b 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'b 'e +val (>>=) : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'b 'e. + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e + -> ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'b 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'b 'e declare isabelle target_rep function (>>=) = infix `\` let inline ~{isabelle} (>>=) = bind @@ -15,10 +15,10 @@ val (>>$=) : forall 'e 'a 'b. either 'e 'a -> ('a -> either 'e 'b) -> either 'e declare isabelle target_rep function (>>$=) = infix `\\<^sub>R` let inline ~{isabelle} (>>$=) = either_bind -val (>>) : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'b 'e. - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'b 'e - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'b 'e +val (>>) : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'b 'e. + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'b 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'b 'e declare isabelle target_rep function (>>) = infix `\` let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n @@ -26,11 +26,11 @@ val (>>$) : forall 'e 'a. either 'e unit -> either 'e 'a -> either 'e 'a declare isabelle target_rep function (>>$) = infix `\\<^sub>R` let inline ~{isabelle} (>>$) m n = m >>$= fun (_ : unit) -> n -val iter_aux : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. +val iter_aux : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. integer - -> (integer -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e) + -> (integer -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e) -> list 'a - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e let rec iter_aux i f xs = match xs with | x :: xs -> f i x >> iter_aux (i + 1) f xs | [] -> return () @@ -38,21 +38,21 @@ let rec iter_aux i f xs = match xs with declare {isabelle} termination_argument iter_aux = automatic -val iteri : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. - (integer -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e) - -> list 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e +val iteri : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. + (integer -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e) + -> list 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e let iteri f xs = iter_aux 0 f xs -val iter : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. - ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e) +val iter : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. + ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e) -> list 'a - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv unit 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv unit 'e let iter f xs = iteri (fun _ x -> f x) xs -val foreachM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'a 'rv 'vars 'e. +val foreachM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'a 'rv 'vars 'e. list 'a -> 'vars - -> ('a -> 'vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('a -> 'vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let rec foreachM l vars body = match l with | [] -> return vars @@ -73,77 +73,77 @@ end declare {isabelle} termination_argument foreachM = automatic -val genlistM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'a 'rv 'e. - (nat -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e) +val genlistM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'a 'rv 'e. + (nat -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e) -> nat - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv (list 'a) 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv (list 'a) 'e let genlistM f n = let indices = genlist (fun n -> n) n in foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x])))) -val and_boolM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e +val and_boolM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e let and_boolM l r = l >>= (fun l -> if l then r else return false) val and_boolE : forall 'e. either 'e bool -> either 'e bool -> either 'e bool let and_boolE l r = l >>$= (fun l -> if l then r else Right false) -val or_boolM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. - monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e +val or_boolM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. + monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e let or_boolM l r = l >>= (fun l -> if l then return true else r) val or_boolE : forall 'e. either 'e bool -> either 'e bool -> either 'e bool let or_boolE l r = l >>$= (fun l -> if l then Right true else r) -val bool_of_bitU_fail : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. - bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e +val bool_of_bitU_fail : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. + bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e let bool_of_bitU_fail = function | B0 -> return false | B1 -> return true | BU -> Fail "bool_of_bitU" end -val bool_of_bitU_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. Register_Value 'rv => - bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e +val bool_of_bitU_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. Register_Value 'rv => + bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e let bool_of_bitU_nondet = function | B0 -> return false | B1 -> return true | BU -> choose_bool "bool_of_bitU" end -val bools_of_bits_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. Register_Value 'rv => - list bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv (list bool) 'e +val bools_of_bits_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. Register_Value 'rv => + list bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv (list bool) 'e let bools_of_bits_nondet bits = foreachM bits [] (fun b bools -> bool_of_bitU_nondet b >>= (fun b -> return (bools ++ [b]))) -val of_bits_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => - list bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val of_bits_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => + list bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let of_bits_nondet bits = bools_of_bits_nondet bits >>= (fun bs -> return (of_bools bs)) -val of_bits_fail : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Bitvector 'a => - list bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val of_bits_fail : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Bitvector 'a => + list bitU -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits) -val mword_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Size 'a, Register_Value 'rv => - unit -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv (mword 'a) 'e +val mword_nondet : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Size 'a, Register_Value 'rv => + unit -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv (mword 'a) 'e let mword_nondet () = bools_of_bits_nondet (repeat [BU] (integerFromNat size)) >>= (fun bs -> return (wordFromBitlist bs)) -val whileM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e. +val whileM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e. 'vars - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let rec whileM vars cond body = cond vars >>= fun cond_val -> if cond_val then @@ -157,12 +157,12 @@ let rec whileE vars cond body = body vars >>$= fun vars -> whileE vars cond body else Right vars -val whileMT_aux : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e. +val whileMT_aux : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e. nat -> 'vars - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let rec whileMT_aux (limit+1) vars cond body = cond vars >>= fun cond_val -> if not(cond_val) then return vars else @@ -172,21 +172,21 @@ and whileMT_aux 0 _ _ _ = declare {isabelle} termination_argument whileMT_aux = automatic -val whileMT : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e. +val whileMT : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e. 'vars -> ('vars -> integer) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let whileMT vars measure cond body = (* whileMT in coq-sail keeps executing one more iteration when the measure reaches 0, so add 1 for our whileMT_aux above *) whileMT_aux (natFromInteger (measure vars + 1)) vars cond body -val untilM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e. +val untilM : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e. 'vars - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let rec untilM vars cond body = body vars >>= fun vars -> cond vars >>= fun cond_val -> @@ -198,12 +198,12 @@ let rec untilE vars cond body = cond vars >>$= fun cond_val -> if cond_val then Right vars else untilE vars cond body -val untilMT_aux : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e. +val untilMT_aux : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e. nat -> 'vars - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let rec untilMT_aux (limit+1) vars cond body = body vars >>= fun vars -> cond vars >>= fun cond_val -> @@ -213,26 +213,26 @@ and untilMT_aux 0 _ _ _ = declare {isabelle} termination_argument untilMT_aux = automatic -val untilMT : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e. +val untilMT : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e. 'vars -> ('vars -> integer) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv bool 'e) - -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e) - -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'vars 'e + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'vars 'e let untilMT vars measure cond body = (* untilMT in coq-sail keeps executing one more iteration when the measure reaches 0, so add 1 for our untilMT_aux above *) untilMT_aux (natFromInteger (measure vars + 1)) vars cond body -val choose_bools : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. Register_Value 'rv => - string -> nat -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv (list bool) 'e +val choose_bools : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. Register_Value 'rv => + string -> nat -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv (list bool) 'e let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n -val choose_bitvector : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => - string -> nat -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val choose_bitvector : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => + string -> nat -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let choose_bitvector descr n = choose_bools descr n >>= fun v -> return (of_bools v) -val choose_from_list : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Register_Value 'rv => - string -> list 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val choose_from_list : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Register_Value 'rv => + string -> list 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let choose_from_list descr xs = choose_int ("choose_from_list " ^ descr) >>= fun idx -> match index xs (natFromInteger idx mod List.length xs) with @@ -240,18 +240,18 @@ let choose_from_list descr xs = | Nothing -> Fail ("choose_from_list " ^ descr) end -val choose_int_in_range : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. Register_Value 'rv => - string -> integer -> integer -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv integer 'e +val choose_int_in_range : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. Register_Value 'rv => + string -> integer -> integer -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv integer 'e let choose_int_in_range descr i j = choose_int descr >>= fun k -> return (max i (min j k)) -val choose_nat : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e. Register_Value 'rv => - string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv integer 'e +val choose_nat : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'e. Register_Value 'rv => + string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv integer 'e let choose_nat descr = choose_int descr >>= fun i -> return (max 0 i) -val internal_pick : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Register_Value 'rv => - list 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val internal_pick : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Register_Value 'rv => + list 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let internal_pick xs = choose_from_list "internal_pick" xs (*let write_two_regs r1 r2 vec = diff --git a/src/gen_lib/sail2_undefined_concurrency_interface.lem b/src/gen_lib/sail2_undefined_concurrency_interface.lem index edad723cb..07d4e9209 100644 --- a/src/gen_lib/sail2_undefined_concurrency_interface.lem +++ b/src/gen_lib/sail2_undefined_concurrency_interface.lem @@ -9,8 +9,8 @@ open import Sail2_monadic_combinators Changes here need to be reflected in ../../lib/hol/sail2_undefined.lem (identical except for type class constraints). *) -val undefined_bitvector : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => - integer -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e +val undefined_bitvector : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => + integer -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e let undefined_bitvector n = choose_bitvector "undefined_bitvector" (natFromInteger n) let undefined_unit () = return () @@ -25,6 +25,6 @@ let undefined_range i j = choose_int_in_range "undefined_range" i j let undefined_atom i = return i (* TODO: Choose each vector element individually *) -val undefined_vector : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e. - integer -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv (list 'a) 'e +val undefined_vector : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv 'a 'e. + integer -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'trans_start 'trans_end 'arch_ak 'rv (list 'a) 'e let undefined_vector len u = return (repeat [u] len)