diff --git a/lib/isabelle/.gitignore b/lib/isabelle/.gitignore index b6162198a..3d1d8c85e 100644 --- a/lib/isabelle/.gitignore +++ b/lib/isabelle/.gitignore @@ -14,3 +14,11 @@ Sail2_state_lifting.thy Sail2_state.thy Sail2_string.thy Sail2_undefined.thy +Sail2_concurrency_interface.thy +Sail2_concurrency_interface_bitlists.thy +Sail2_concurrency_interface_mwords.thy +Sail2_monadic_combinators.thy +Sail2_undefined_concurrency_interface.thy +Sail2_concurrency_interface_v2.thy +Sail2_monadic_combinators_v2.thy +Sail2_undefined_concurrency_interface_v2.thy diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 00aee595a..10abccb9c 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -5,12 +5,16 @@ THYS = Sail2_instr_kinds.thy Sail2_values.thy Sail2_operators.thy \ Sail2_string.thy Sail2_concurrency_interface.thy \ Sail2_concurrency_interface_mwords.thy \ Sail2_concurrency_interface_bitlists.thy \ - Sail2_monadic_combinators.thy Sail2_undefined_concurrency_interface.thy + Sail2_monadic_combinators.thy Sail2_undefined_concurrency_interface.thy \ + Sail2_concurrency_interface_v2.thy \ + Sail2_monadic_combinators_v2.thy Sail2_undefined_concurrency_interface_v2.thy EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_prompt_monad_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy \ Sail2_concurrency_interface_lemmas.thy \ + Sail2_concurrency_interface_v2_lemmas.thy \ Sail2_monadic_combinators_lemmas.thy \ + Sail2_monadic_combinators_v2_lemmas.thy \ Trace_Properties.thy LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib @@ -60,9 +64,6 @@ Sail2_prompt.thy: ../../src/gen_lib/sail2_prompt.lem Sail2_prompt_monad.thy Sail Sail2_undefined.thy: ../../src/gen_lib/sail2_undefined.lem Sail2_prompt.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail2_undefined_concurrency_interface.thy: ../../src/gen_lib/sail2_undefined_concurrency_interface.lem Sail2_concurrency_interface.thy - lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< - Sail2_state_monad.thy: ../../src/gen_lib/sail2_state_monad.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< @@ -78,6 +79,9 @@ Sail2_string.thy: ../../src/gen_lib/sail2_string.lem Sail2_operators_mwords.thy Sail2_concurrency_interface.thy: ../../src/gen_lib/sail2_concurrency_interface.lem Sail2_string.thy Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< +Sail2_concurrency_interface_v2.thy: ../../src/gen_lib/sail2_concurrency_interface_v2.lem Sail2_string.thy Sail2_values.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + Sail2_concurrency_interface_mwords.thy: ../../src/gen_lib/sail2_concurrency_interface_mwords.lem Sail2_concurrency_interface.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< @@ -87,5 +91,14 @@ Sail2_concurrency_interface_bitlists.thy: ../../src/gen_lib/sail2_concurrency_in Sail2_monadic_combinators.thy: ../../src/gen_lib/sail2_monadic_combinators.lem Sail2_concurrency_interface.thy Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< +Sail2_monadic_combinators_v2.thy: ../../src/gen_lib/sail2_monadic_combinators_v2.lem Sail2_concurrency_interface_v2.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + +Sail2_undefined_concurrency_interface.thy: ../../src/gen_lib/sail2_undefined_concurrency_interface.lem Sail2_concurrency_interface.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + +Sail2_undefined_concurrency_interface_v2.thy: ../../src/gen_lib/sail2_undefined_concurrency_interface_v2.lem Sail2_concurrency_interface_v2.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + clean: -rm $(THYS) diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT index f7275b78e..d74112d4e 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -11,9 +11,12 @@ session "Sail" = "LEM" + Sail2_concurrency_interface_mwords Sail2_concurrency_interface_bitlists Sail2_concurrency_interface_lemmas + Sail2_concurrency_interface_v2_lemmas Sail2_monadic_combinators_lemmas + Sail2_monadic_combinators_v2_lemmas Sail2_string Sail2_undefined Sail2_undefined_concurrency_interface + Sail2_undefined_concurrency_interface_v2 Hoare document_files "root.tex" diff --git a/lib/isabelle/Sail2_concurrency_interface_v2_lemmas.thy b/lib/isabelle/Sail2_concurrency_interface_v2_lemmas.thy new file mode 100644 index 000000000..c32d7da51 --- /dev/null +++ b/lib/isabelle/Sail2_concurrency_interface_v2_lemmas.thy @@ -0,0 +1,520 @@ +theory Sail2_concurrency_interface_v2_lemmas + imports + Sail2_concurrency_interface_v2 + Sail2_values_lemmas +begin + +notation bind (infixr "\" 54) +notation either_bind (infixr "\\<^sub>R" 54) + +abbreviation seq (*:: "('rv,unit,'e)monad \ ('rv,'b,'e)monad \('rv,'b,'e)monad"*) (infixr "\" 54) where + "m \ n \ m \ (\_ :: unit. n)" +abbreviation seqR (*:: "('e,unit)sum \ ('e,'b)sum \('e,'b)sum"*) (infixr "\\<^sub>R" 54) where + "m \\<^sub>R n \ m \\<^sub>R (\_ :: unit. n)" + +lemma All_bind_dom: "bind_dom (m, f)" + by (induction m) (auto intro: bind.domintros) + +termination bind using All_bind_dom by auto +lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = bind.induct + +lemma bind_return[simp]: "bind (return a) f = f a" + by (auto simp: return_def) +lemma bind_return_right[simp]: "bind x return = x" by (induction x) (auto simp: return_def) + +lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\x. bind (f x) g)" + by (induction m f arbitrary: g rule: bind.induct) auto + +lemma bind_assert_True[simp]: "bind (assert_exp True msg) f = f ()" + by (auto simp: assert_exp_def) + +lemma All_try_catch_dom: "try_catch_dom (m, h)" + by (induction m) (auto intro: try_catch.domintros) +termination try_catch using All_try_catch_dom by auto +lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = try_catch.induct + +inductive_set T (*:: "(('rv, 'a, 'e) monad \ 'rv event \ ('rv, 'a, 'e) monad) set"*) where + Choose: "((Choose descr k), E_choose descr v, k v) \ T" +| Read_reg: "((Read_reg r k), E_read_reg r v, k v) \ T" +| Write_reg: "((Write_reg r v k), E_write_reg r v, k) \ T" +| Read_mem: "((Mem_read req k), E_mem_read req v, k v) \ T" +| Write_mem: "((Mem_write req data tags k), E_mem_write req data tags r, k r) \ T" +| Write_announce: "((Mem_write_address_announce req k), E_mem_write_address_announce req, 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" +| TLB_op_request: "((TLB_op_request r k), E_tlb_op_request r, k) \ T" +| Fault: "((Take_exception exn k), E_take_exception exn, k) \ T" +| Eret: "((Return_exception k), E_return_exception, 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" + +lemma emitEvent_iff_T: "emitEvent m e = Some m' \ (m, e, m') \ T" + by (cases e) (auto simp: emitEvent_def elim: T.cases intro: T.intros split: monad.splits) + +lemmas emitEvent_intros = T.intros[folded emitEvent_iff_T] +(* lemmas emitEvent_cases = T.cases[folded emitEvent_iff_T, case_names Choose Read_reg Write_reg Read_mem Write_mem Write_announce Branch_announce Barrier Cache_op TLB_op Fault Eret] *) + +lemma emitEvent_cases: + assumes "emitEvent m e = Some m'" + obtains + (Choose) descr k v where "m = Choose descr k" and "e = E_choose descr v" and "m' = k v" + | (Read_reg) r k v where "m = Read_reg r k" and "e = E_read_reg r v" and "m' = k v" + | (Write_reg) r k v where "m = Write_reg r v k" and "e = E_write_reg r v" and "m' = k" + | (Read_mem) req k v where "m = Mem_read req k" and "e = E_mem_read req v" and "m' = k v" + | (Write_mem) req data tags k r where "m = Mem_write req data tags k" and "e = E_mem_write req data tags r" and "m' = k r" + | (Write_announce) req k where "m = Mem_write_address_announce req k" and "e = E_mem_write_address_announce req" 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" + | (TLB_op_request) r k where "m = TLB_op_request r k" and "e = E_tlb_op_request r" and "m' = k" + | (Take_exception) exn k where "m = Take_exception exn k" and "e = E_take_exception exn" and "m' = k" + | (Return_exception) k where "m = Return_exception k" and "e = E_return_exception" 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" + using assms + by (auto simp: emitEvent_def split: event.splits monad.splits if_splits) + +inductive_set Traces (*:: "(('rv, 'a, 'e) monad \ 'rv event list \ ('rv, 'a, 'e) monad) set"*) where + Nil: "(s, [], s) \ Traces" +| Step: "\emitEvent s e = Some s''; (s'', t, s') \ Traces\ \ (s, e # t, s') \ Traces" + +declare Traces.intros[intro] +(* declare T.intros[intro] *) + +declare prod.splits[split] + +lemmas Traces_ConsI = emitEvent_intros[THEN Step] + +inductive_cases Traces_NilE[elim]: "(s, [], s') \ Traces" +inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \ Traces" + +lemma runTrace_iff_Traces: "runTrace t m = Some m' \ (m, t, m') \ Traces" + by (induction t m rule: runTrace.induct; fastforce simp: bind_eq_Some_conv) + +lemma hasTrace_iff_Traces_final: "hasTrace t m \ (\m'. (m, t, m') \ Traces \ final m')" + by (auto simp: hasTrace_def runTrace_iff_Traces[symmetric] split: option.splits) + +lemma runTrace_eq_iff_id: + "(\t. runTrace t m1 = runTrace t m2) \ (m1 = m2)" + by (auto elim: allE[where x = "[]"]) + +lemma Traces_eq_iff_id: + "(\t m'. (m1, t, m') \ Traces \ (m2, t, m') \ Traces) \ (m1 = m2)" + by (auto elim: allE[where x = "[]"]) + +lemma Traces_cases: + (* fixes m :: "('rv, 'a, 'e) monad" *) + assumes Run: "(m, t, m') \ Traces" + obtains (Nil) a where "m = m'" and "t = []" + | (Choose) descr v k t' where "m = Choose descr k" and "t = E_choose descr v # t'" and "(k v, t', m') \ Traces" + | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \ Traces" + | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = E_write_reg reg v # t'" and "(k, t', m') \ Traces" + | (Read_mem) req k t' v where "m = Mem_read req k" and "t = E_mem_read req v # t'" and "(k v, t', m') \ Traces" + | (Write_mem) req data tags k v t' where "m = Mem_write req data tags k" and "t = E_mem_write req data tags v # t'" and "(k v, t', m') \ Traces" + | (Write_announce) req k t' where "m = Mem_write_address_announce req k" and "t = E_mem_write_address_announce req # 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" + | (TLB_op) r k t' where "m = TLB_op_request r k" and "t = E_tlb_op_request r # t'" and "(k, t', m') \ Traces" + | (Take_exception) exn k t' where "m = Take_exception exn k" and "t = E_take_exception exn # t'" and "(k, t', m') \ Traces" + | (Return_exception) k t' where "m = Return_exception k" and "t = E_return_exception # 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" +proof (use Run in \cases m t m' set: Traces\) + case Nil + then show ?thesis by (auto intro: that(1)) +next + case (Step e m'' t') + then show ?thesis + by (cases m; cases e) (auto simp: emitEvent_def split: if_splits elim: that) +qed + +lemma Traces_iffs: + "\a t m'. (Done a, t, m') \ Traces \ (t = [] \ m' = Done a)" + "\msg t m'. (Fail msg, t, m') \ Traces \ (t = [] \ m' = Fail msg)" + "\e t m'. (Exception e, t, m') \ Traces \ (t = [] \ m' = Exception e)" + "\descr k t m'. (Choose descr k, t, m') \ Traces \ (t = [] \ m' = Choose descr k \ (\a t'. t = E_choose descr a # t' \ (k a, t', m') \ Traces))" + "\reg k t m'. (Read_reg reg k, t, m') \ Traces \ (t = [] \ m' = Read_reg reg k \ (\a t'. t = E_read_reg reg a # t' \ (k a, t', m') \ Traces))" + "\reg a k t m'. (Write_reg reg a k, t, m') \ Traces \ (t = [] \ m' = Write_reg reg a k \ (\t'. t = E_write_reg reg a # t' \ (k, t', m') \ Traces))" + "\req k t m'. (Mem_read req k, t, m') \ Traces \ (t = [] \ m' = Mem_read req k \ (\a t'. t = E_mem_read req a # t' \ (k a, t', m') \ Traces))" + "\req data tags k t m'. (Mem_write req data tags k, t, m') \ Traces \ (t = [] \ m' = Mem_write req data tags k \ (\a t'. t = E_mem_write req data tags a # t' \ (k a, t', m') \ Traces))" + "\req k t m'. (Mem_write_address_announce req k, t, m') \ Traces \ (t = [] \ m' = Mem_write_address_announce req k \ (\t'. t = E_mem_write_address_announce req # 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))" + "\req k t m'. (TLB_op_request req k, t, m') \ Traces \ (t = [] \ m' = TLB_op_request req k \ (\t'. t = E_tlb_op_request req # t' \ (k, t', m') \ Traces))" + "\exn k t m'. (Take_exception exn k, t, m') \ Traces \ (t = [] \ m' = Take_exception exn k \ (\t'. t = E_take_exception exn # t' \ (k, t', m') \ Traces))" + "\k t m'. (Return_exception k, t, m') \ Traces \ (t = [] \ m' = Return_exception k \ (\t'. t = E_return_exception # 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))" + by (auto elim: Traces_cases intro: Traces_ConsI) + +lemmas Done_Traces_iff[iff] = Traces_iffs(1) +lemmas Fail_Traces_iff[iff] = Traces_iffs(2) +lemmas Exception_Traces_iff[iff] = Traces_iffs(3) +lemmas Traces_iff_Cons = Traces_iffs(4-) + +abbreviation Run (*:: "('rv, 'a, 'e) monad \ 'rv event list \ 'a \ bool"*) + where "Run s t a \ (s, t, Done a) \ Traces" + +lemma final_cases: + assumes "final m" + obtains (Done) a where "m = Done a" | (Fail) f where "m = Fail f" | (Ex) e where "m = Exception e" + using assms by (cases m) (auto simp: final_def) + +lemma hasTraces_elim: + assumes "hasTrace t m" + obtains m' where "(m, t, m') \ Traces" and "final m'" + using assms + unfolding hasTrace_iff_Traces_final + by blast + +lemma hasTrace_cases: + assumes "hasTrace t m" + obtains (Run) a where "Run m t a" + | (Fail) f where "(m, t, Fail f) \ Traces" + | (Ex) e where "(m, t, Exception e) \ Traces" + using assms by (elim hasTraces_elim final_cases) auto + +lemma Traces_appendI: + assumes "(s, t1, s') \ Traces" + and "(s', t2, s'') \ Traces" + shows "(s, t1 @ t2, s'') \ Traces" +proof (use assms in \induction t1 arbitrary: s\) + case (Cons e t1) + then show ?case by (elim Traces_ConsE) auto +qed auto + +lemma bind_DoneE: + assumes "bind m f = Done a" + obtains a' where "m = Done a'" and "f a' = Done a" + using assms by (auto elim: bind.elims) + +lemma emitEvent_bind: + assumes "emitEvent m e = Some m'" + shows "emitEvent (bind m f) e = Some (bind m' f)" + using assms + by (cases rule: emitEvent_cases) (auto intro: emitEvent_intros) + +lemma emitEvent_bind_cases: + assumes "emitEvent (bind m f) e = Some m'" + obtains (Done) a where "m = Done a" and "emitEvent (f a) e = Some m'" + | (Bind) m'' where "m' = bind m'' f" and "emitEvent m e = Some m''" +proof (cases "emitEvent m e") + case None + then have "emitEvent (bind m f) e = None \ (\a. m = Done a)" + by (auto simp: emitEvent_def split: event.splits monad.splits) + then show ?thesis + using assms + by (auto intro: Done) +next + case (Some m'') + then show ?thesis + using assms + by (auto simp: emitEvent_bind intro: Bind) +qed + +lemma bind_T_cases: + assumes "(bind m f, e, s') \ T" + obtains (Done) a where "m = Done a" and "(f a, e, s') \ T" + | (Bind) m' where "s' = bind m' f" and "(m, e, m') \ T" + using assms + unfolding emitEvent_iff_T[symmetric] + by (elim emitEvent_bind_cases) + +lemma Traces_bindI: + assumes "Run m t1 a1" + and "(f a1, t2, m') \ Traces" + shows "(m \ f, t1 @ t2, m') \ Traces" + using assms + by (induction t1 arbitrary: m; fastforce intro: Traces_ConsI elim: emitEvent_cases) + +lemma Run_Done_iff[iff]: "Run (Done a) t a' \ t = [] \ a' = a" by auto + +lemma Run_return_iff[iff]: "Run (return a) t a' \ t = [] \ a' = a" by (auto simp: return_def) + +lemma Run_throw[iff]: "Run (throw e) t a \ False" by (auto simp: throw_def) + +lemma Run_early_return_False[iff]: "Run (early_return x) t u \ False" + by (auto simp: early_return_def) + +lemma Run_assert_exp_iff[iff]: "Run (assert_exp c msg) t u \ t = [] \ c" + by (auto simp: assert_exp_def) + +lemma Run_DoneE: + assumes "Run (Done a) t a'" + obtains "t = []" and "a' = a" + using assms + by (auto) + +lemma Run_Nil_iff_Done: "Run m [] a \ m = Done a" + by auto + +lemma Traces_Nil_iff: "(m, [], m') \ Traces \ m' = m" + by auto + +lemma bind_Traces_cases: + assumes "(m \ f, t, m') \ Traces" + obtains (Left) m'' where "(m, t, m'') \ Traces" and "m' = m'' \ f" + | (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "(f am, tf, m') \ Traces" +proof (use assms in \induction "bind m f" t m' arbitrary: m rule: Traces.induct\) + case Nil + then show ?case by (auto simp: Traces_Nil_iff) +next + case (Step e s'' t s') + note IH = Step(3) + note Left' = Step(4) + note Bind' = Step(5) + show thesis + proof (use \emitEvent (m \ f) e = Some s''\ in \cases rule: emitEvent_bind_cases\) + case (Done a) + then show ?thesis using \(s'', t, s') \ Traces\ Step(5)[of "[]" "e # t" a] by auto + next + case (Bind m') + show ?thesis + proof (rule IH) + show "s'' = m' \ f" using Bind by blast + next + fix m'' + assume "(m', t, m'') \ Traces" and "s' = m'' \ f" + then show thesis using \emitEvent m e = Some m'\ Left'[of m''] by auto + next + fix tm tf am + assume "t = tm @ tf" and "Run m' tm am" and "(f am, tf, s') \ Traces" + then show thesis using \emitEvent m e = Some m'\ Bind'[of "e # tm" tf am] by auto + qed + qed +qed + +lemma final_bind_cases: + assumes "final (m \ f)" + obtains (Done) a where "m = Done a" and "final (f a)" + | (Fail) msg where "m = Fail msg" + | (Ex) e where "m = Exception e" + using assms by (cases m) (auto simp: final_def) + +lemma hasFailure_iff_Traces_Fail: "hasFailure t m \ (\msg. (m, t, Fail msg) \ Traces)" + by (auto simp: hasFailure_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits) + +lemma hasException_iff_Traces_Exception: "hasException t m \ (\e. (m, t, Exception e) \ Traces)" + by (auto simp: hasException_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits) + +lemma hasTrace_bind_cases: + assumes "hasTrace t (m \ f)" + obtains (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "hasTrace tf (f am)" + | (Fail) "hasFailure t m" + | (Ex) "hasException t m" +proof - + from assms obtain m' where t: "(m \ f, t, m') \ Traces" and m': "final m'" + by (auto simp: hasTrace_iff_Traces_final) + note [simp] = hasTrace_iff_Traces_final hasFailure_iff_Traces_Fail hasException_iff_Traces_Exception + from t show thesis + proof (cases rule: bind_Traces_cases) + case (Left m'') + then show ?thesis + using m' Fail Ex Bind[of t "[]"] + by (fastforce elim!: final_bind_cases) + next + case (Bind tm am tf) + then show ?thesis + using m' that + by fastforce + qed +qed + +lemma emitEvent_try_catch_cases: + assumes "emitEvent (try_catch m h) e = Some m'" + obtains (NoEx) m'' where "emitEvent m e = Some m''" and "m' = try_catch m'' h" + | (Ex) ex where "m = Exception ex" and "emitEvent (h ex) e = Some m'" + using assms + by (cases m) (auto elim: emitEvent_cases simp: emitEvent_intros) + +(*lemma try_catch_T_cases: + assumes "(try_catch m h, e, m') \ T" + obtains (NoEx) m'' where "(m, e, m'') \ T" and "m' = try_catch m'' h" + | (Ex) ex where "m = Exception ex" and "(h ex, e, m') \ T" + using assms + by (cases m) (auto elim!: T.cases)*) + +lemma try_catch_Traces_cases: + assumes "(try_catch m h, t, mtc) \ Traces" + obtains (NoEx) m' where "(m, t, m') \ Traces" and "mtc = try_catch m' h" + | (Ex) tm ex th where "(m, tm, Exception ex) \ Traces" and "(h ex, th, mtc) \ Traces" and "t = tm @ th" +proof (use assms in \induction "try_catch m h" t mtc arbitrary: m rule: Traces.induct\) + case Nil + then show ?case by auto +next + case (Step e mtc' t mtc) + note e = \emitEvent (try_catch m h) e = Some mtc'\ + note t = \(mtc', t, mtc) \ Traces\ + note IH = Step(3) + note NoEx_ConsE = Step(4) + note Ex_ConsE = Step(5) + show ?case + proof (use e in \cases rule: emitEvent_try_catch_cases\) + case (NoEx m1) + show ?thesis + proof (rule IH) + show "mtc' = try_catch m1 h" using NoEx by auto + next + fix m' + assume "(m1, t, m') \ Traces" and "mtc = try_catch m' h" + then show ?thesis + using NoEx NoEx_ConsE[of m'] + by auto + next + fix tm ex th + assume "(m1, tm, Exception ex) \ Traces" and "(h ex, th, mtc) \ Traces" and "t = tm @ th" + then show ?thesis + using NoEx Ex_ConsE[of "e # tm" ex th] + by auto + qed + next + case (Ex ex) + then show ?thesis + using t Ex_ConsE[of "[]" ex "e # t"] + by auto + qed +qed + +lemma Read_reg_TracesE: + assumes "(Read_reg r k, t, m') \ Traces" + obtains (Nil) "t = []" and "m' = Read_reg r k" + | (Cons) v t' where "t = E_read_reg r v # t'" and "(k v, t', m') \ Traces" + using assms + by (auto elim: Traces_cases) + +lemma Write_reg_TracesE: + assumes "(Write_reg r v k, t, m') \ Traces" + obtains (Nil) "t = []" and "m' = Write_reg r v k" + | (Cons) t' where "t = E_write_reg r v # t'" and "(k, t', m') \ Traces" + using assms + by (auto elim: Traces_cases) + +lemma Mem_write_TracesE: + assumes "(Mem_write req data tags k, t, m') \ Traces" + obtains (Nil) "t = []" and "m' = Mem_write req data tags k" + | (Cons) t' r where "t = E_mem_write req data tags r # t'" and "(k r, t', m') \ Traces" + using assms + by (auto elim: Traces_cases) + +(*lemma Write_ea_TracesE: + assumes "(Write_ea wk addr sz k, t, m') \ Traces" + obtains (Nil) "t = []" and "m' = Write_ea wk addr sz k" + | (Cons) t' where "t = E_write_ea wk addr sz # t'" and "(k, t', m') \ Traces" + using assms + by (auto elim: Traces_cases)*) + +lemma Run_bind_ex: + assumes "Run (bind m f) t a" + shows "\tm am tf. t = tm @ tf \ Run m tm am \ Run (f am) tf a" +proof (use assms in \induction t arbitrary: m\) + case (Nil m) + then show ?case + by (cases m) auto +next + case (Cons e t m) + then consider (Step) m' where "emitEvent m e = Some m'" and "Run (bind m' f) t a" + | (Done) a' where "m = Done a'" + by (elim Traces_ConsE emitEvent_bind_cases) auto + then show ?case + proof cases + case Step + then obtain tm' am' tf where "t = tm' @ tf" and "Run m' tm' am'" and "Run (f am') tf a" + using Cons.IH[of m'] + by blast + then have "e # t = (e # tm') @ tf" and "Run m (e # tm') am'" and "Run (f am') tf a" + using Step + by auto + then show ?thesis + by blast + next + case Done + with Cons.prems show ?thesis + by auto + qed +qed + +lemma Run_bindE: + assumes "Run (bind m f) t a" + obtains tm am tf where "t = tm @ tf" and "Run m tm am" and "Run (f am) tf a" + using Run_bind_ex[OF assms] + by blast + +lemma Run_bindE_ignore_trace: + assumes "Run (m \ f) t a" + obtains tm tf am where "Run m tm am" and "Run (f am) tf a" + using assms by (elim Run_bindE) + +lemma Run_letE: + assumes "Run (let x = y in f x) t a" + obtains "Run (f y) t a" + using assms by auto + +lemma Run_ifE: + assumes "Run (if b then f else g) t a" + obtains "b" and "Run f t a" | "\b" and "Run g t a" + using assms by (auto split: if_splits) + +lemma Run_returnE: + assumes "Run (return x) t a" + obtains "t = []" and "a = x" + using assms by (auto simp: return_def) + +lemma Run_early_returnE: + assumes "Run (early_return x) t a" + shows P + using assms by (auto simp: early_return_def throw_def elim: Traces_cases) + +lemma bind_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\t a. Run m2 t a \ f1 a = f2 a" + shows "bind m1 f1 = bind m2 f2" + unfolding m using f + by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast intro: emitEvent_intros) + +lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits) +lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def) +lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def) +lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def) +lemma liftR_assert_exp[simp]: "liftR (assert_exp e msg) = assert_exp e msg" by (auto simp: liftR_def assert_exp_def) +lemma try_catch_maybe_fail[simp]: "try_catch (maybe_fail msg v) h = maybe_fail msg v" by (cases v; auto simp: maybe_fail_def) +lemma liftR_choose_regval[simp]: "liftR (choose_regval descr) = choose_regval descr" by (auto simp: liftR_def choose_regval_def) +lemma liftR_choose_convert[simp]: "liftR (choose_convert of_rv descr) = choose_convert of_rv descr" by (auto simp: liftR_def choose_convert_def) +lemma liftR_choose_convert_default[simp]: "liftR (choose_convert_default of_rv x descr) = choose_convert_default of_rv x descr" + by (auto simp: liftR_def choose_convert_default_def) +lemma liftR_choose_builtins[simp]: + "liftR (choose_bool RV u) = choose_bool RV u" + "liftR (choose_int RV u) = choose_int RV u" + "liftR (choose_real RV u) = choose_real RV u" + "liftR (choose_string RV u) = choose_string RV u" + unfolding choose_bool_def choose_int_def choose_real_def choose_string_def + by auto + +lemma catch_early_return_bind_liftR: + "catch_early_return (liftR m \ f) = (m \ (\a. catch_early_return (f a)))" + by (induction m) (auto simp: catch_early_return_def liftR_def throw_def) + +lemma catch_early_return_bind_early_return: + "catch_early_return (early_return a \ f) = return a" + by (auto simp: catch_early_return_def early_return_def throw_def) + +lemmas catch_early_return_if_distrib = if_distrib[where f = catch_early_return] +lemmas catch_early_return_prod_distrib = prod.case_distrib[where h = catch_early_return] +lemmas catch_early_return_bind_if_distrib = + if_distrib[where f = "\m. m \ f" for f, THEN refl[of catch_early_return, THEN cong]] + +text \Precondition to ensure reading a register doesn't fail.\ + +fun(sequential) + register_reads_ok (*:: "(string \ ('regval \ bool) option) \ 'regval event \ bool"*) + where + "register_reads_ok f (E_read_reg nm v) = register_read_ok f nm v" + | "register_reads_ok f _ = True" + +lemma read_reg_non_failure: + "(read_reg reg_ref, t, x) \ Traces \ + f (name reg_ref) = Some (fst (register_ops_of reg_ref)) \ + \event \ set t. register_reads_ok f event \ + x \ Fail msg" + by (auto simp: read_reg_def register_read_ok_def register_ops_of_def + elim!: Read_reg_TracesE split: option.split_asm) + +end diff --git a/lib/isabelle/Sail2_monadic_combinators_v2_lemmas.thy b/lib/isabelle/Sail2_monadic_combinators_v2_lemmas.thy new file mode 100644 index 000000000..48217fa47 --- /dev/null +++ b/lib/isabelle/Sail2_monadic_combinators_v2_lemmas.thy @@ -0,0 +1,269 @@ +theory Sail2_monadic_combinators_v2_lemmas + imports Sail2_operators_mwords Sail2_monadic_combinators_v2 +begin + +lemma untilM_domI: + fixes V :: "'vars \ nat" + assumes "Inv vars" + and "\vars t vars' t'. \Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\ \ V vars' < V vars \ 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 whileM_domI: + fixes V :: "'vars \ nat" + assumes "Inv vars" + and "\vars t vars' t'. \Inv vars; Run (cond vars) t True; Run (body vars) t' vars'\ \ V vars' < V vars \ Inv vars'" + shows "whileM_dom (vars, cond, body)" + using assms + by (induction vars rule: measure_induct_rule[where f = V]) + (auto intro: whileM.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 \induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\) + (auto intro: whileM.domintros) + +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 \induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\) + (auto intro: untilM.domintros) + +text \Simplification rules for monadic Boolean connectives\ + +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 \ c)" + "and_boolM x (return True) = x" + "and_boolM x (return False) = x \ (\_. return False)" + "and_boolM (return True) x = x" + "and_boolM (return False) x = return False" + "\x y z. and_boolM (x \ y) z = (x \ (\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) + +lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\x. and_boolM x y" for y] + +lemma or_boolM_simps[simp]: + "or_boolM (return b) (return c) = return (b \ c)" + "or_boolM x (return True) = x \ (\_. return True)" + "or_boolM x (return False) = x" + "\x y z. or_boolM (x \ y) z = (x \ (\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) + +lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\x. or_boolM x y" for y] + +text \Machine word lemmas\ + +lemmas uint_simps[simp] = uint_maybe_def (*uint_fail_def uint_nondet_def*) +lemmas sint_simps[simp] = sint_maybe_def (*sint_fail_def sint_nondet_def*) + +lemma bools_of_bits_nondet_just_list[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "bools_of_bits_nondet RV bus = return bs" +proof - + have f: "foreachM bus bools (\b bools. bool_of_bitU_nondet RV b \ (\b. return (bools @ [b]))) = return (bools @ bs)" + if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools + proof (use that in \induction bus arbitrary: bs bools\) + case (Cons bu bus bs) + obtain b bs' where bs: "bs = b # bs'" and bu: "bool_of_bitU bu = Some b" + using Cons.prems by (cases bu) (auto split: option.splits) + then show ?case + using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"] + by (cases bu) (auto simp: bool_of_bitU_nondet_def split: option.splits) + qed auto + then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_nondet_def + by auto +qed + +lemma of_bits_mword_return_of_bl[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "of_bits_nondet BC_mword RV bus = return (of_bl bs)" + and "of_bits_fail BC_mword bus = return (of_bl bs)" + by (auto simp: of_bits_nondet_def of_bits_fail_def maybe_fail_def assms BC_mword_defs) + +lemma vec_of_bits_of_bl[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "vec_of_bits_maybe bus = Some (of_bl bs)" + (*and "vec_of_bits_fail bus = return (of_bl bs)" + and "vec_of_bits_nondet RV bus = return (of_bl bs)"*) + and "vec_of_bits_failwith bus = of_bl bs" + and "vec_of_bits bus = of_bl bs" + unfolding vec_of_bits_maybe_def (*vec_of_bits_fail_def vec_of_bits_nondet_def*) + vec_of_bits_failwith_def vec_of_bits_def + by (auto simp: assms) + +lemmas access_vec_dec_test_bit[simp] = access_bv_dec_mword[folded access_vec_dec_def] + +lemma access_vec_inc_test_bit[simp]: + fixes w :: "('a::len) word" + assumes "n \ 0" and "nat n < LENGTH('a)" + shows "access_vec_inc w n = bitU_of_bool (bit w (LENGTH('a) - 1 - nat n))" + using assms + by (auto simp: access_vec_inc_def access_bv_inc_def access_list_def BC_mword_defs rev_nth test_bit_bl) + +lemma bool_of_bitU_monadic_simps[simp]: + "bool_of_bitU_fail B0 = return False" + "bool_of_bitU_fail B1 = return True" + "bool_of_bitU_fail BU = Fail ''bool_of_bitU''" + "bool_of_bitU_nondet RV B0 = return False" + "bool_of_bitU_nondet RV B1 = return True" + "bool_of_bitU_nondet RV BU = choose_bool RV ''bool_of_bitU''" + unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def + by auto + +lemma update_vec_dec_simps[simp]: + "update_vec_dec_maybe w i B0 = Some (set_bit w (nat i) False)" + "update_vec_dec_maybe w i B1 = Some (set_bit w (nat i) True)" + "update_vec_dec_maybe w i BU = None" + (*"update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)" + "update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)" + "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''" + "update_vec_dec_nondet RV w i B0 = return (set_bit w (nat i) False)" + "update_vec_dec_nondet RV w i B1 = return (set_bit w (nat i) True)" + "update_vec_dec_nondet RV w i BU = choose_bool RV ''bool_of_bitU'' \ (\b. return (set_bit w (nat i) b))"*) + "update_vec_dec w i B0 = set_bit w (nat i) False" + "update_vec_dec w i B1 = set_bit w (nat i) True" + unfolding update_vec_dec_maybe_def (*update_vec_dec_fail_def update_vec_dec_nondet_def*) update_vec_dec_def + by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def) + +lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]: + "n \ 0 \ nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)" + by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq) + +declare subrange_vec_dec_def[simp] + +lemma update_subrange_vec_dec_update_subrange_list_dec: + assumes "0 \ j" and "j \ i" and "i < int LENGTH('a)" + shows "update_subrange_vec_dec (w :: 'a::len word) i j w' = + of_bl (update_subrange_list_dec (to_bl w) i j (to_bl w'))" + using assms + unfolding update_subrange_vec_dec_def update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: word_update_def split_at_def Let_def nat_diff_distrib min_def) + +lemma subrange_vec_dec_subrange_list_dec: + assumes "0 \ j" and "j \ i" and "i < int LENGTH('a)" and "int LENGTH('b) = i - j + 1" + shows "subrange_vec_dec (w :: 'a::len word) i j = (of_bl (subrange_list_dec (to_bl w) i j) :: 'b::len word)" + using assms unfolding subrange_vec_dec_def + by (auto simp: subrange_list_dec_drop_take slice_take of_bl_drop') + +lemma slice_simp[simp]: "slice w lo len = Word.slice (nat lo) w" + by (auto simp: slice_def) + +declare slice_id[simp] + +lemma of_bools_of_bl[simp]: "of_bools_method BC_mword = of_bl" + by (auto simp: BC_mword_defs) + +lemma of_bl_bin_word_of_int: + "len = LENGTH('a) \ of_bl (bin_to_bl_aux len n []) = (word_of_int n :: ('a::len) word)" + by (auto simp: of_bl_def bin_bl_bin') + +lemma get_slice_int_0_bin_to_bl[simp]: + "len > 0 \ get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)" + unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def + by (auto simp: subrange_list_dec_drop_take size_bin_to_bl_aux) + +lemma to_bl_of_bl[simp]: + fixes bl :: "bool list" + defines w: "w \ of_bl bl :: 'a::len word" + assumes len: "length bl = LENGTH('a)" + shows "to_bl w = bl" + using len unfolding w by (intro word_bl.Abs_inverse) auto + +lemma reverse_endianness_byte[simp]: + "LENGTH('a) = 8 \ reverse_endianness (w :: 'a::len word) = w" + unfolding reverse_endianness_def by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness[simp]: + "8 dvd LENGTH('a) \ reverse_endianness (reverse_endianness w) = (w :: 'a::len word)" + unfolding reverse_endianness_def by (simp) + +lemma replicate_bits_zero[simp]: "replicate_bits 0 n = 0" + by (intro word_eqI) (auto simp: replicate_bits_def test_bit_of_bl rev_nth nth_repeat simp del: repeat.simps) + +declare extz_vec_def[simp] +declare exts_vec_def[simp] +declare concat_vec_def[simp] + +lemma msb_Bits_msb[simp]: + "msb w = bitU_of_bool (Most_significant_bit.msb w)" + by (auto simp: msb_def most_significant_def BC_mword_defs word_msb_alt split: list.splits) + +declare and_vec_def[simp] +declare or_vec_def[simp] +declare xor_vec_def[simp] +declare not_vec_def[simp] + +lemma arith_vec_simps[simp]: + "add_vec l r = l + r" + "sub_vec l r = l - r" + "mult_vec l r = (ucast l) * (ucast r)" + unfolding add_vec_def sub_vec_def mult_vec_def + by auto + +declare adds_vec_def[simp] +declare subs_vec_def[simp] +declare mults_vec_def[simp] + +lemma arith_vec_int_simps[simp]: + "add_vec_int l r = l + (word_of_int r)" + "sub_vec_int l r = l - (word_of_int r)" + "mult_vec_int l r = (ucast l) * (word_of_int r)" + unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def + by (auto simp: arith_op_bv_int_def BC_mword_defs) + +lemma shiftl_simp[simp]: "shiftl w l = w << (nat l)" + by (auto simp: shiftl_def shiftl_mword_def) + +lemma shiftr_simp[simp]: "shiftr w l = w >> (nat l)" + by (auto simp: shiftr_def shiftr_mword_def) + +termination shl_int + apply (rule_tac R="measure (nat o snd)" in shl_int.termination) + apply simp + apply simp + done + +declare shl_int.simps[simp del] + +lemma shl_int[simp]: + "shl_int x y = x << (nat y)" + apply (induct n \ "nat y" arbitrary: x y) + apply (simp add: shl_int.simps) + apply (subst shl_int.simps) + apply (clarsimp dest!: sym[where s="Suc _"] simp: shiftl_int_def) + apply (simp add: nat_diff_distrib) + done + +termination shr_int + apply (rule_tac R="measure (nat o snd)" in shr_int.termination) + apply simp_all + done + +declare shr_int.simps[simp del] + +lemma shr_int[simp]: + "shr_int x i = x >> (nat i)" + apply (induct x i rule: shr_int.induct) + apply (subst shr_int.simps) + apply (clarsimp simp: shiftr_int_def zdiv_zmult2_eq[symmetric]) + apply (simp add: power_Suc[symmetric] Suc_nat_eq_nat_zadd1 del: power_Suc) + done + +end diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index 91cb8973d..ba8cbb60c 100644 --- a/lib/isabelle/Sail2_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -309,7 +309,7 @@ lemma update_list_inc_update[simp]: lemma update_list_dec_update[simp]: "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" - by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int list_update_beyond) lemma update_list_dec_update_rev: "0 \ n \ nat n < length xs \ update_list_dec xs n x = rev ((rev xs)[nat n := x])" diff --git a/src/gen_lib/sail2_concurrency_interface_v2.lem b/src/gen_lib/sail2_concurrency_interface_v2.lem new file mode 100644 index 000000000..3ef227734 --- /dev/null +++ b/src/gen_lib/sail2_concurrency_interface_v2.lem @@ -0,0 +1,370 @@ +open import Pervasives_extra +open import Sail2_values +open import Sail2_string + + + + +type Mem_request 'addr_size 'addr_space 'mem_acc = + <| Mem_request_access_kind : 'mem_acc; + Mem_request_address : mword 'addr_size; + Mem_request_address_space : 'addr_space; + Mem_request_size : integer; + Mem_request_num_tag : integer; |> + + +type monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e = + | Done of 'a + | Fail of string + | Exception of 'e + | Choose of string * ('regval -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e) + | Read_reg of string * ('regval -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e) + | Write_reg of string * 'regval * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Mem_read of Mem_request 'addr_size 'addr_space 'mem_acc * (result (list (mword ty8) * list bool) 'abort -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e) + | Mem_write of Mem_request 'addr_size 'addr_space 'mem_acc * list (mword ty8) * list bool * (result unit 'abort -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e) + | Mem_write_address_announce of Mem_request 'addr_size 'addr_space 'mem_acc * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Barrier_request of 'barrier * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Cache_op_request of 'cache_op * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | TLB_op_request of 'tlb_op * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Take_exception of 'exn * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Return_exception of monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Translation_start of 'trans_start * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + | Translation_end of 'trans_end * monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + +type event 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval = + | E_choose of string * 'regval + | E_read_reg of string * 'regval + | E_write_reg of string * 'regval + | E_mem_read of Mem_request 'addr_size 'addr_space 'mem_acc * result (list (mword ty8) * list bool) 'abort + | E_mem_write of Mem_request 'addr_size 'addr_space 'mem_acc * list (mword ty8) * list bool * result unit 'abort + | E_mem_write_address_announce of Mem_request 'addr_size 'addr_space 'mem_acc + | E_barrier_request of 'barrier + | E_cache_op_request of 'cache_op + | E_tlb_op_request of 'tlb_op + | E_take_exception of 'exn + | E_return_exception + | E_translation_start of 'trans_start + | E_translation_end of 'trans_end + +type trace 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval = + list (event 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval) + +val return : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e. + 'a -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e +let return a = Done a + +val bind : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'b 'e. + monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e -> + ('a -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'b 'e) -> + monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'b 'e +let rec bind m f = match m with + | Done a -> f a + | Fail msg -> Fail msg + | Exception e -> Exception e + | Choose msg k -> Choose msg (fun v -> bind (k v) f) + | Read_reg r k -> Read_reg r (fun v -> bind (k v) f) + | Write_reg r v k -> Write_reg r v (bind k f) + | Mem_read req k -> Mem_read req (fun v -> bind (k v) f) + | Mem_write req data tags k -> Mem_write req data tags (fun v -> bind (k v) f) + | Mem_write_address_announce req k -> Mem_write_address_announce req (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) + | TLB_op_request t k -> TLB_op_request t (bind k f) + | Take_exception exn k -> Take_exception exn (bind k f) + | Return_exception k -> Return_exception (bind k f) + | Translation_start ts k -> Translation_start ts (bind k f) + | Translation_end te k -> Translation_end te (bind k f) +end + +val throw : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e. + 'e -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e +let throw e = Exception e + +val try_catch : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e1 'e2. + monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e1 -> + ('e1 -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e2) -> + monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e2 +let rec try_catch m h = match m with + | Done a -> Done a + | Fail msg -> Fail msg + | Exception e -> h e + | Choose msg k -> Choose msg (fun v -> try_catch (k v) h) + | Read_reg r k -> Read_reg r (fun v -> try_catch (k v) h) + | Write_reg r v k -> Write_reg r v (try_catch k h) + | Mem_read req k -> Mem_read req (fun v -> try_catch (k v) h) + | Mem_write req data tags k -> Mem_write req data tags (fun v -> try_catch (k v) h) + | Mem_write_address_announce req k -> Mem_write_address_announce req (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) + | TLB_op_request t k -> TLB_op_request t (try_catch k h) + | Take_exception exn k -> Take_exception exn (try_catch k h) + | Return_exception k -> Return_exception (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) +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 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'r 'e = + monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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) + +(* val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e *) +let catch_early_return m = + try_catch m + (function + | Left a -> return a + | Right e -> throw e + end) + +val pure_early_return : forall 'a. either 'a 'a -> 'a +let pure_early_return = function + | Left a -> a + | Right a -> a +end + +(*val pure_early_return_embed : forall 'rv 'a 'r 'e. either 'r 'a -> monadR 'rv 'a 'r 'e*) +let pure_early_return_embed = function + | Left r -> throw (Left r) + | Right a -> return a +end + +val either_bind : forall 'e 'a 'b. either 'e 'a -> ('a -> either 'e 'b) -> either 'e 'b +let either_bind m f = + match m with + | Left e -> Left e + | Right x -> f x + end + +(* Lift to monad with early return by wrapping exceptions *) +(* val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e *) +let liftR m = try_catch m (fun e -> throw (Right e)) + +(* Catch exceptions in the presence of early returns *) +(* val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) -> monadR 'rv 'a 'r 'e2 *) +let try_catchR m h = + try_catch m + (function + | Left r -> throw (Left r) + | Right e -> h e + end) + +(* val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e *) +let maybe_fail msg = function + | Just a -> return a + | Nothing -> Fail msg +end + +val assert_exp : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + bool -> string -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let assert_exp exp msg = if exp then Done () else Fail msg + +val exit : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e. + unit -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e +let exit _ = Fail "exit" + +val read_reg : forall 's 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e. + register_ref 's 'regval 'a -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e +let read_reg reg = + let k v = + match reg.of_regval v with + | Just v -> Done v + | Nothing -> Fail "read_reg: unrecognised value" + end + in + Read_reg reg.name k + +let inline reg_deref = read_reg + +val write_reg : forall 's 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e. + register_ref 's 'regval 'a -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) + +val sail_mem_read : forall 'abort 'barrier 'cache_op 'exn 'pa 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + Mem_request 'addr_size 'addr_space 'mem_acc -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval (result (list (mword ty8) * list bool) 'abort) 'e +let sail_mem_read req = Mem_read req return + +val sail_mem_write : forall 'abort 'barrier 'cache_op 'exn 'pa 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + Mem_request 'addr_size 'addr_space 'mem_acc -> + list (mword ty8) -> + list bool -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval (result unit 'abort) 'e +let sail_mem_write req data tags = Mem_write req data tags return + +val choose_regval : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. + string -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'rv 'e +let choose_regval descr = Choose descr return + +val choose_convert : forall 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e 'a. + ('rv -> maybe 'a) -> string -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e 'a. + ('rv -> maybe 'a) -> 'a -> string -> monad 'abort 'barrier 'cache_op 'fault 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 + end)) + +let choose_bool descr = choose_convert_default bool_of_regval false descr +let choose_bit descr = bind (choose_bool descr) (fun b -> return (bitU_of_bool b)) +let choose_int descr = choose_convert_default int_of_regval 0 descr +let choose_real descr = choose_convert_default real_of_regval 0 descr +let choose_string descr = choose_convert_default string_of_regval "default" descr + +let headM = function + | x :: _ -> return x + | [] -> Fail "headM" +end + +let tailM = function + | _ :: xs -> return xs + | [] -> Fail "tailM" +end + +val sail_mem_address_announce : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + Mem_request 'addr_size 'addr_space 'mem_acc -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_mem_address_announce req = Mem_write_address_announce req (return ()) + +val sail_translation_start : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'trans_start -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_translation_start ts = Translation_start ts (return ()) + +val sail_translation_end : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'trans_end -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_translation_end te = Translation_end te (return ()) + +val instr_announce : forall 'instr 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'instr -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let instr_announce _ = return () (* TODO *) + +val branch_announce : forall 'addr 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. Bitvector 'addr => + integer -> 'addr -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let branch_announce _ _ = return () + +val sail_barrier : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'barrier -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_barrier barrier = Barrier_request barrier (return ()) + +val sail_cache_op : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'cache_op -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_cache_op cache_op = Cache_op_request cache_op (return ()) + +val sail_tlbi : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'tlb_op -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_tlbi tlb_op = TLB_op_request tlb_op (return ()) + +val sail_take_exception : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + 'exn -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_take_exception exn = Take_exception exn (return ()) + +val sail_return_exception : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + unit -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_return_exception _ = Return_exception (return ()) + +val sail_instr_announce : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e 'addr. + 'addr -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let sail_instr_announce _ = return () + +(* We treat the cycle count operations as dummy operations. We don't currently use cycle_count as an end-of-instruction marker + in the Lem targets, and we're going to move get_cycle_count into the Arm model directly soon. *) +val cycle_count : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + unit -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval unit 'e +let cycle_count () = return () + +val get_cycle_count : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'e. + unit -> + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval integer 'e +let get_cycle_count () = return 0 + +(* Event traces *) + +val emitEvent : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e. + Eq 'regval, Eq 'barrier, Eq 'cache_op, Eq 'tlb_op, Eq 'exn, Eq 'trans_start, Eq 'trans_end => + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e + -> event 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval + -> maybe (monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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) -> + if r' = r then Just (k v) else Nothing + | (E_write_reg r v, Write_reg r' v' k) -> + if r' = r && v' = v then Just k else Nothing + | (E_mem_read req v, Mem_read req' k) -> + if req' = req then Just (k v) else Nothing + | (E_mem_write req data tags r, Mem_write req' data' tags' k) -> + if req' = req && data' = data && tags' = tags then Just (k r) else Nothing + | (E_mem_write_address_announce a, Mem_write_address_announce a' k) -> + if a' = a then Just k else Nothing + | (E_barrier_request r, Barrier_request r' k) -> + if r' = r then Just k else Nothing + | (E_cache_op_request r, Cache_op_request r' k) -> + if r' = r then Just k else Nothing + | (E_tlb_op_request r, TLB_op_request r' k) -> + if r' = r then Just k else Nothing + | (E_take_exception exn, Take_exception exn' k) -> + if exn' = exn then Just k else Nothing + | (E_return_exception, Return_exception k) -> + Just k + | (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 + | _ -> Nothing +end + +(*val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)*) +let rec runTrace t m = match t with + | [] -> Just m + | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t') +end + +declare {isabelle} termination_argument runTrace = automatic + +(*val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool*) +let final = function + | Done _ -> true + | Fail _ -> true + | Exception _ -> true + | _ -> false +end + +(*val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*) +let hasTrace t m = match runTrace t m with + | Just m -> final m + | Nothing -> false +end + +(*val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*) +let hasException t m = match runTrace t m with + | Just (Exception _) -> true + | _ -> false +end + +(*val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*) +let hasFailure t m = match runTrace t m with + | Just (Fail _) -> true + | _ -> false +end + +(* Define a type synonym that also takes the register state as a type parameter, + 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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'regstate 'a 'e = + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'e +type base_monadR 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'regstate 'a 'r 'e = + monadR 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'regval 'a 'r 'e diff --git a/src/gen_lib/sail2_monadic_combinators_v2.lem b/src/gen_lib/sail2_monadic_combinators_v2.lem new file mode 100644 index 000000000..d62ff29f5 --- /dev/null +++ b/src/gen_lib/sail2_monadic_combinators_v2.lem @@ -0,0 +1,276 @@ +open import Pervasives_extra +(*open import Sail_impl_base*) +open import Sail2_values +open import Sail2_concurrency_interface_v2 +open import {isabelle} `Sail2_concurrency_interface_v2_lemmas` + +val (>>=) : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'b 'e. + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e + -> ('a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'b 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'b 'e +declare isabelle target_rep function (>>=) = infix `\` +let inline ~{isabelle} (>>=) = bind + +val (>>$=) : forall 'e 'a 'b. either 'e 'a -> ('a -> either 'e 'b) -> either 'e 'b +declare isabelle target_rep function (>>$=) = infix `\\<^sub>R` +let inline ~{isabelle} (>>$=) = either_bind + +val (>>) : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'b 'e. + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv unit 'e + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'b 'e + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'b 'e +declare isabelle target_rep function (>>) = infix `\` +let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n + +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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. + integer + -> (integer -> 'a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv unit 'e) + -> list 'a + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 () + end + +declare {isabelle} termination_argument iter_aux = automatic + +val iteri : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. + (integer -> 'a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv unit 'e) + -> list 'a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv unit 'e +let iteri f xs = iter_aux 0 f xs + +val iter : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. + ('a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv unit 'e) + -> list 'a + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv unit 'e +let iter f xs = iteri (fun _ x -> f x) xs + +val foreachM : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'a 'rv 'vars 'e. + list 'a -> 'vars + -> ('a -> 'vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e +let rec foreachM l vars body = +match l with +| [] -> return vars +| (x :: xs) -> + body x vars >>= fun vars -> + foreachM xs vars body +end + +val foreachE : forall 'a 'vars 'e. + list 'a -> 'vars -> ('a -> 'vars -> either 'e 'vars) -> either 'e 'vars +let rec foreachE l vars body = +match l with +| [] -> Right vars +| (x :: xs) -> + body x vars >>$= fun vars -> + foreachE xs vars body +end + +declare {isabelle} termination_argument foreachM = automatic + +val genlistM : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'a 'rv 'e. + (nat -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e) + -> nat + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. + monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. + bitU -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. Register_Value 'rv => + bitU -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. Register_Value 'rv => + list bitU -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => + list bitU -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Bitvector 'a => + list bitU -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e +let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits) + +val mword_nondet : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Size 'a, Register_Value 'rv => + unit -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e. + 'vars + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e +let rec whileM vars cond body = + cond vars >>= fun cond_val -> + if cond_val then + body vars >>= fun vars -> whileM vars cond body + else return vars + +val whileE : forall 'vars 'e. 'vars -> ('vars -> either 'e bool) -> ('vars -> either 'e 'vars) -> either 'e 'vars +let rec whileE vars cond body = + cond vars >>$= fun cond_val -> + if cond_val then + body vars >>$= fun vars -> whileE vars cond body + else Right vars + +val whileMT_aux : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e. + nat + -> 'vars + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 + body vars >>= fun vars -> whileMT_aux limit vars cond body +and whileMT_aux 0 _ _ _ = + Fail "whileMT: termination limit reached" + +declare {isabelle} termination_argument whileMT_aux = automatic + +val whileMT : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e. + 'vars + -> ('vars -> integer) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e. + 'vars + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e +let rec untilM vars cond body = + body vars >>= fun vars -> + cond vars >>= fun cond_val -> + if cond_val then return vars else untilM vars cond body + +val untilE : forall 'e 'vars. 'vars -> ('vars -> either 'e bool) -> ('vars -> either 'e 'vars) -> either 'e 'vars +let rec untilE vars cond body = + body vars >>$= fun vars -> + cond vars >>$= fun cond_val -> + if cond_val then Right vars else untilE vars cond body + +val untilMT_aux : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e. + nat + -> 'vars + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e +let rec untilMT_aux (limit+1) vars cond body = + body vars >>= fun vars -> + cond vars >>= fun cond_val -> + if cond_val then return vars else untilMT_aux limit vars cond body +and untilMT_aux 0 _ _ _ = + Fail "untilMT: termination limit reached" + +declare {isabelle} termination_argument untilMT_aux = automatic + +val untilMT : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e. + 'vars + -> ('vars -> integer) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv bool 'e) + -> ('vars -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'vars 'e) + -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. Register_Value 'rv => + string -> nat -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv (list bool) 'e +let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n + +val choose_bitvector : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => + string -> nat -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Register_Value 'rv => + string -> list 'a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 + | Just x -> return x + | Nothing -> Fail ("choose_from_list " ^ descr) + end + +val choose_int_in_range : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. Register_Value 'rv => + string -> integer -> integer -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space '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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'e. Register_Value 'rv => + string -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv integer 'e +let choose_nat descr = choose_int descr >>= fun i -> return (max 0 i) + +val internal_pick : forall 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Register_Value 'rv => + list 'a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e +let internal_pick xs = choose_from_list "internal_pick" xs + +(*let write_two_regs r1 r2 vec = + let is_inc = + let is_inc_r1 = is_inc_of_reg r1 in + let is_inc_r2 = is_inc_of_reg r2 in + let () = ensure (is_inc_r1 = is_inc_r2) + "write_two_regs called with vectors of different direction" in + is_inc_r1 in + + let (size_r1 : integer) = size_of_reg r1 in + let (start_vec : integer) = get_start vec in + let size_vec = length vec in + let r1_v = + if is_inc + then slice vec start_vec (size_r1 - start_vec - 1) + else slice vec start_vec (start_vec - size_r1 - 1) in + let r2_v = + if is_inc + then slice vec (size_r1 - start_vec) (size_vec - start_vec) + else slice vec (start_vec - size_r1) (start_vec - size_vec) in + write_reg r1 r1_v >> write_reg r2 r2_v*) diff --git a/src/gen_lib/sail2_undefined_concurrency_interface_v2.lem b/src/gen_lib/sail2_undefined_concurrency_interface_v2.lem new file mode 100644 index 000000000..ba6e0488e --- /dev/null +++ b/src/gen_lib/sail2_undefined_concurrency_interface_v2.lem @@ -0,0 +1,30 @@ +open import Pervasives_extra +open import Sail2_values +open import Sail2_concurrency_interface_v2 +open import Sail2_monadic_combinators_v2 + +(* Default implementations of "undefined" functions for builtin types via + nondeterministic choice, for use with the -undefined_gen option of Sail. + + 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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => + integer -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e +let undefined_bitvector n = choose_bitvector "undefined_bitvector" (natFromInteger n) + +let undefined_unit () = return () +let undefined_bits = undefined_bitvector +let undefined_bit () = choose_bit "undefined_bit" +let undefined_bool () = choose_bool "undefined_bool" +let undefined_string () = choose_string "undefined_string" +let undefined_int () = choose_int "undefined_int" +let undefined_nat () = choose_nat "undefined_nat" +let undefined_real () = choose_real "undefined_real" +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 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv 'a 'e. + integer -> 'a -> monad 'abort 'barrier 'cache_op 'exn 'tlb_op 'trans_start 'trans_end 'mem_acc 'addr_size 'addr_space 'rv (list 'a) 'e +let undefined_vector len u = return (repeat [u] len) diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 887eeaaa3..7c5ef6d9e 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -1249,13 +1249,13 @@ let split_defs target all_errors (splits : split_req list) env ast = Util.progress "Monomorphising " (string_of_int idx ^ "/" ^ string_of_int num_defs) idx num_defs; match aux with | DEF_type _ | DEF_constraint _ | DEF_val _ | DEF_default _ | DEF_register _ | DEF_overload _ | DEF_fixity _ - | DEF_pragma _ | DEF_internal_mutrec _ -> + | DEF_pragma _ | DEF_internal_mutrec _ | DEF_outcome _ | DEF_impl _ | DEF_instantiation _ -> [def] | DEF_fundef fd -> [DEF_aux (DEF_fundef (map_fundef fd), def_annot)] | DEF_let lb -> [DEF_aux (DEF_let (map_letbind lb), def_annot)] | DEF_scattered sd -> List.map (fun x -> DEF_aux (DEF_scattered x, def_annot)) (map_scattered_def sd) | DEF_measure (id, pat, exp) -> [DEF_aux (DEF_measure (id, pat, map_exp exp), def_annot)] - | DEF_impl _ | DEF_instantiation _ | DEF_outcome _ | DEF_mapdef _ | DEF_loop_measures _ -> + | DEF_mapdef _ | DEF_loop_measures _ -> Reporting.unreachable (def_loc def) __POS__ "Found definition that should have been rewritten previously during monomorphisation" in diff --git a/src/lib/outcome_rewrites.ml b/src/lib/outcome_rewrites.ml index 8deca5021..27e818aee 100644 --- a/src/lib/outcome_rewrites.ml +++ b/src/lib/outcome_rewrites.ml @@ -103,9 +103,9 @@ let rec instantiated_or_abstract l = function if List.for_all Option.is_none xs then Some def else raise (Reporting.err_general l "Multiple instantiations found for target") -let instantiate target ast = - (* Some backends will need the instantiations to hook up to a particular interface *) - let keep_original_defs = String.compare target "coq" == 0 in +(** Generate instantiations of outcomes declared using [instantiation]. Some backends will need the instantiations to + hook up to a particular interface; they can set [?keep_original_defs] to [true]. *) +let instantiate ?(keep_original_defs = false) target ast = let process_def outcomes = function | DEF_aux (DEF_outcome (OV_aux (OV_outcome (id, TypSchm_aux (TypSchm_ts (typq, typ), _), args), l), outcome_defs), _) as def -> diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 87bdde5f8..93d2dba86 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -4871,7 +4871,11 @@ let all_rewriters = ("rewrite_loops_with_escape_effect", basic_rewriter rewrite_loops_with_escape_effect); ("simple_types", basic_rewriter rewrite_simple_types); ( "instantiate_outcomes", - String_rewriter (fun target -> basic_rewriter (fun _ -> Outcome_rewrites.instantiate target)) + String_rewriter + (fun target -> + Bool_rewriter + (fun keep_original_defs -> basic_rewriter (fun _ -> Outcome_rewrites.instantiate ~keep_original_defs target)) + ) ); ("top_sort_defs", basic_rewriter (fun _ -> Callgraph.top_sort_defs)); ( "constant_fold", @@ -4907,7 +4911,7 @@ let all_rewriters = let rewrites_interpreter = [ - ("instantiate_outcomes", [String_arg "interpreter"]); + ("instantiate_outcomes", [String_arg "interpreter"; Bool_arg false]); ("realize_mappings", []); ("toplevel_string_append", []); ("pat_string_append", []); diff --git a/src/lib/state.ml b/src/lib/state.ml index 94cf5a1f3..b4d8d33f6 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -57,6 +57,8 @@ open Pretty_print_sail let opt_type_grouped_regstate = ref false +module StringMap = Map.Make (String) + let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs defs) let get_bitfield_typ_id env typ = @@ -544,12 +546,19 @@ let generate_isa_lemmas env defs = in let regval_class_typ_ids = List.map (fun (t, _) -> mk_id t) regval_class_typs_lem in let register_defs = - let reg_id id = remove_leading_underscores (string_of_id id) in + let add_reg_def (previous_names, regs) (_, id, _) = + let id' = remove_leading_underscores (string_of_id id) ^ "_ref" in + (* Handle name clashes when generating Isabelle definitions from Lem: + If a name after mangling has already been used, Lem appends a 0, 1, ... *) + let id'', i = + match StringMap.find_opt id' previous_names with Some i -> (id' ^ string_of_int i, i + 1) | None -> (id', 0) + in + (StringMap.add id' i previous_names, (id'' ^ "_def") :: regs) + in + let _, regs = List.fold_left add_reg_def (StringMap.empty, []) registers in hang 2 (flow_map (break 1) string - (["lemmas register_defs"; "="; "get_regval_unfold"; "set_regval_unfold"] - @ List.map (fun (typ, id, _) -> reg_id id ^ "_ref_def") registers - ) + (["lemmas register_defs"; "="; "get_regval_unfold"; "set_regval_unfold"] @ List.rev regs) ) in let conv_lemma typ_id = @@ -620,7 +629,6 @@ let generate_isa_lemmas env defs = ] ) in - let module StringMap = Map.Make (String) in let field_id typ = remove_leading_underscores (string_of_id (id_of_regtyp IdSet.empty typ)) in let field_id_stripped typ = remove_trailing_underscores (field_id typ) in (* TODO: Handle bitfield registers *) diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml index 4d118529c..efebc87e4 100644 --- a/src/sail_c_backend/sail_plugin_c.ml +++ b/src/sail_c_backend/sail_plugin_c.ml @@ -165,7 +165,7 @@ let c_cpp_rewrites (mode : c_backend_mode) = let target_name = string_of_mode mode in let open Rewrites in [ - ("instantiate_outcomes", [String_arg target_name]); + ("instantiate_outcomes", [String_arg target_name; Bool_arg false]); ("realize_mappings", []); ("remove_vector_subrange_pats", []); ("toplevel_string_append", []); diff --git a/src/sail_coq_backend/sail_plugin_coq.ml b/src/sail_coq_backend/sail_plugin_coq.ml index 46fecbfae..ef1681a16 100644 --- a/src/sail_coq_backend/sail_plugin_coq.ml +++ b/src/sail_coq_backend/sail_plugin_coq.ml @@ -125,7 +125,7 @@ let coq_rewrites = let open Rewrites in [ ("move_termination_measures", []); - ("instantiate_outcomes", [String_arg "coq"]); + ("instantiate_outcomes", [String_arg "coq"; Bool_arg true]); ("realize_mappings", []); ("remove_extern_defs", [String_arg "coq"]); ("remove_vector_subrange_pats", []); diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 6ea220bb6..d65550a3f 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -156,7 +156,7 @@ let lean_rewrites = let open Rewrites in [ ("move_termination_measures", []); - ("instantiate_outcomes", [String_arg "lean"]); + ("instantiate_outcomes", [String_arg "lean"; Bool_arg false]); ("realize_mappings", []); ("remove_vector_subrange_pats", []); ("remove_duplicate_valspecs", []); diff --git a/src/sail_lem_backend/pretty_print_lem.ml b/src/sail_lem_backend/pretty_print_lem.ml index b9ca7bfad..561e36d28 100644 --- a/src/sail_lem_backend/pretty_print_lem.ml +++ b/src/sail_lem_backend/pretty_print_lem.ml @@ -328,7 +328,7 @@ let lem_tyvars_of_typ params_to_print typ = (lem_nexps_of_typ params_to_print typ) KidSet.empty (* When making changes here, check whether they affect lem_tyvars_of_typ *) -let doc_typ_lem, doc_typ_lem_brackets, doc_atomic_typ_lem = +let doc_typ_lem, doc_typ_lem_brackets, doc_atomic_typ_lem, doc_typ_arg_lem = (* following the structure of parser for precedence *) let rec typ params_to_print atyp_needed ty = tup_typ params_to_print atyp_needed ty and tup_typ params_to_print atyp_needed (Typ_aux (t, l) as ty) = @@ -428,7 +428,7 @@ let doc_typ_lem, doc_typ_lem_brackets, doc_atomic_typ_lem = let ty' = if !Monomorphise.opt_mwords then ty else Env.expand_synonyms env ty in typ params_to_print atyp_needed ty' in - (top false, top true, atomic_typ) + (top false, top true, atomic_typ, doc_typ_arg_lem) let doc_fn_typ_lem ?(monad = empty) params_to_print env (Typ_aux (aux, l) as ty) = match aux with @@ -1724,8 +1724,7 @@ let doc_def_lem effect_info params_to_print type_env (DEF_aux (aux, _) as def) = group (doc_let_lem { empty_ctxt with params_to_print } lbind) ^/^ hardline | DEF_scattered sdef -> unreachable (def_loc def) __POS__ "doc_def_lem: shoulnd't have DEF_scattered at this point" | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "Lem doesn't support mappings" - | DEF_outcome _ | DEF_impl _ | DEF_instantiation _ -> - unreachable (def_loc def) __POS__ "Event definition found when generating lem" + | DEF_outcome _ | DEF_impl _ | DEF_instantiation _ -> empty | DEF_pragma _ -> empty | DEF_measure _ -> empty (* we might use these in future *) | DEF_loop_measures _ -> empty @@ -1815,25 +1814,51 @@ let doc_ast_lem out_filename split_files base_imports extra_imports ctx effect_i in let register_refs = State.register_refs_lem register_ref_tannot type_env (State.find_registers defs) in let extra_monad_params = - match concurrency_monad_params with - | None -> empty - | Some params -> - let open Monad_params in - space - ^^ separate_map space - (doc_typ_lem_brackets params_to_print type_env) - [ - params.abort_type; - params.barrier_type; - params.cache_op_type; - params.fault_type; - params.pa_type; - params.tlbi_type; - params.translation_summary_type; - params.trans_start_type; - params.trans_end_type; - params.arch_ak_type; - ] + if Preprocess.have_symbol "CONCURRENCY_INTERFACE_V2" then begin + let open Monad_params in + let type_substs, id_substs = find_instantiations defs in + let pp_typish name default = + match KBindings.find_opt (mk_kid name) type_substs with + | Some typ_arg -> doc_typ_arg_lem params_to_print typ_arg + | None -> string default + in + let pp_typ_or_unit name = pp_typish name "unit" in + space + ^^ separate_map space pp_typ_or_unit + [ + "abort"; + "barrier"; + "cache_op"; + "exn"; + "tlbi"; + "trans_start"; + "trans_end"; + "mem_acc"; + "addr_size"; + "addr_space"; + ] + end + else begin + match concurrency_monad_params with + | None -> empty + | Some params -> + let open Monad_params in + space + ^^ separate_map space + (doc_typ_lem_brackets params_to_print type_env) + [ + params.abort_type; + params.barrier_type; + params.cache_op_type; + params.fault_type; + params.pa_type; + params.tlbi_type; + params.translation_summary_type; + params.trans_start_type; + params.trans_end_type; + params.arch_ak_type; + ] + end in let types_doc = concat diff --git a/src/sail_lem_backend/sail_plugin_lem.ml b/src/sail_lem_backend/sail_plugin_lem.ml index e09501b8a..cad8bfa08 100644 --- a/src/sail_lem_backend/sail_plugin_lem.ml +++ b/src/sail_lem_backend/sail_plugin_lem.ml @@ -91,7 +91,7 @@ let lem_rewrites = let open Rewrites in [ ("move_termination_measures", []); - ("instantiate_outcomes", [String_arg "lem"]); + ("instantiate_outcomes", [String_arg "lem"; Bool_arg true]); ("realize_mappings", []); ("remove_vector_subrange_pats", []); ("remove_duplicate_valspecs", []); @@ -167,7 +167,9 @@ let lem_target out_file { ctx; ast; effect_info; env = type_env; _ } = let out_filename = match out_file with Some f -> f | None -> "out" in let concurrency_monad_params = Monad_params.find_monad_parameters type_env in let monad_modules = - if Option.is_some concurrency_monad_params then + if Preprocess.have_symbol "CONCURRENCY_INTERFACE_V2" then + ["Sail2_concurrency_interface_v2"; "Sail2_monadic_combinators_v2"; "Sail2_undefined_concurrency_interface_v2"] + else if Option.is_some concurrency_monad_params then [ "Sail2_concurrency_interface"; "Sail2_monadic_combinators"; @@ -176,12 +178,10 @@ let lem_target out_file { ctx; ast; effect_info; env = type_env; _ } = else "Sail2_concurrency_interface_bitlists" ); ] - else ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_undefined"] + else ["Sail2_instr_kinds"; "Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_undefined"] in let operators_module = if !Monomorphise.opt_mwords then "Sail2_operators_mwords" else "Sail2_operators_bitlists" in - let base_imports = - ["Pervasives_extra"; "Sail2_instr_kinds"; "Sail2_values"; "Sail2_string"; operators_module] @ monad_modules - in + let base_imports = ["Pervasives_extra"; "Sail2_values"; "Sail2_string"; operators_module] @ monad_modules in let isa_thy_name = String.capitalize_ascii out_filename ^ "_lemmas" in let isa_lemmas = separate hardline @@ -190,7 +190,9 @@ let lem_target out_file { ctx; ast; effect_info; env = type_env; _ } = string " imports"; string (" " ^ String.capitalize_ascii out_filename); string " Sail.Sail2_values_lemmas"; - ( if Option.is_some concurrency_monad_params then string " Sail.Sail2_concurrency_interface_lemmas" + ( if Preprocess.have_symbol "CONCURRENCY_INTERFACE_V2" then + string " Sail.Sail2_concurrency_interface_v2_lemmas" + else if Option.is_some concurrency_monad_params then string " Sail.Sail2_concurrency_interface_lemmas" else string " Sail.Sail2_state_lemmas" ); string " Sail.Add_Cancel_Distinct"; diff --git a/src/sail_ocaml_backend/sail_plugin_ocaml.ml b/src/sail_ocaml_backend/sail_plugin_ocaml.ml index 8fae11ef3..497c98a72 100644 --- a/src/sail_ocaml_backend/sail_plugin_ocaml.ml +++ b/src/sail_ocaml_backend/sail_plugin_ocaml.ml @@ -82,7 +82,7 @@ let stash_pre_rewrite_info (ast : _ Ast_defs.ast) _ type_envs = let ocaml_rewrites = let open Rewrites in [ - ("instantiate_outcomes", [String_arg "ocaml"]); + ("instantiate_outcomes", [String_arg "ocaml"; Bool_arg false]); ("realize_mappings", []); ("remove_vector_subrange_pats", []); ("toplevel_string_append", []); @@ -133,7 +133,7 @@ let tofrominterp_options = let tofrominterp_rewrites = let open Rewrites in [ - ("instantiate_outcomes", [String_arg "interpreter"]); + ("instantiate_outcomes", [String_arg "interpreter"; Bool_arg false]); ("realize_mappings", []); ("toplevel_string_append", []); ("pat_string_append", []); diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml index 16555e972..7382b14bf 100644 --- a/src/sail_smt_backend/sail_plugin_smt.ml +++ b/src/sail_smt_backend/sail_plugin_smt.ml @@ -105,7 +105,7 @@ let smt_options = let smt_rewrites = let open Rewrites in [ - ("instantiate_outcomes", [String_arg "c"]); + ("instantiate_outcomes", [String_arg "c"; Bool_arg false]); ("realize_mappings", []); ("remove_vector_subrange_pats", []); ("toplevel_string_append", []); diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 296cd3871..7af5526cf 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -245,7 +245,7 @@ let verilog_options = let verilog_rewrites = let open Rewrites in [ - ("instantiate_outcomes", [String_arg "systemverilog"]); + ("instantiate_outcomes", [String_arg "systemverilog"; Bool_arg false]); ("realize_mappings", []); ("remove_vector_subrange_pats", []); ("toplevel_string_append", []);