diff options
| -rw-r--r-- | lib/isabelle/Makefile | 16 | ||||
| -rw-r--r-- | lib/isabelle/Prompt_monad_extras.thy | 214 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_extras.thy | 25 | ||||
| -rw-r--r-- | riscv/riscv_extras_embed_sequential.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 168 | ||||
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 168 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 329 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 250 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 8 | ||||
| -rw-r--r-- | src/process_file.ml | 11 |
10 files changed, 720 insertions, 470 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 5ff58069..407e6871 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,10 +1,12 @@ -THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy State.thy Prompt.thy +THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy \ + State_monad.thy State.thy Prompt_monad.thy Prompt.thy +EXTRA_THYS = State_monad_extras.thy Prompt_monad_extras.thy .PHONY: all heap-img clean all: heap-img -heap-img: $(THYS) +heap-img: $(THYS) $(EXTRA_THYS) ROOT @echo '*** To build a heap image with the Sail library, please' @echo '*** add the ROOT file in this directory to your ROOTS file' @echo '*** (e.g. $$HOME/.isabelle/Isabelle<version>/ROOTS)' @@ -23,10 +25,16 @@ Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State.thy: ../../src/gen_lib/state.lem Sail_values.thy +State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt.thy: ../../src/gen_lib/prompt.lem Sail_values.thy +State.thy: ../../src/gen_lib/state.lem State_monad.thy State_monad_extras.thy + lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + +Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy + lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< + +Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_extras.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< clean: diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy new file mode 100644 index 00000000..0c319f97 --- /dev/null +++ b/lib/isabelle/Prompt_monad_extras.thy @@ -0,0 +1,214 @@ +theory Prompt_monad_extras + imports Prompt_monad +begin + +lemma All_bind_dom: "bind_dom (oc, f)" + by (induction oc) (auto intro: bind.domintros; blast intro: bind.domintros)+ + +termination bind using All_bind_dom by auto + +lemma bind_induct[case_names Done Read_mem Read_reg Write_memv Excl_res Write_ea Barrier Footprint Write_reg Escape Fail Error Exception Internal]: + fixes m :: "('a, 'e) outcome" and f :: "'a \<Rightarrow> ('b, 'e) outcome" + assumes "\<And>a f. P (Done a) f" + and "\<And>rk addr sz k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Read_mem (rk, addr, sz) k) f" + and "\<And>reg k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Read_reg reg k) f" + and "\<And>val k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Write_memv val k) f" + and "\<And>k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Excl_res k) f" + and "\<And>wk addr sz m opt f. P m f \<Longrightarrow> P (Write_ea (wk, addr, sz) (m, opt)) f" + and "\<And>bk m opt f. P m f \<Longrightarrow> P (Barrier bk (m, opt)) f" + and "\<And>m opt f. P m f \<Longrightarrow> P (Footprint (m, opt)) f" + and "\<And>reg val m opt f. P m f \<Longrightarrow> P (Write_reg (reg, val) (m, opt)) f" + and "\<And>descr f. P (Escape descr) f" + and "\<And>descr f. P (Fail descr) f" and "\<And>descr f. P (Error descr) f" and "\<And>e f. P (Exception e) f" + and "\<And>i m opt f. P m f \<Longrightarrow> P (Internal i (m, opt)) f" + shows "P m f" + by (rule bind.induct[split_format (complete), OF assms]; blast) + +datatype event = + (* Request to read memory *) + Read_mem read_kind address_lifted nat memory_value + (* Write is imminent, at address lifted, of size nat *) + | Write_ea write_kind address_lifted nat + (* Request the result of store-exclusive *) + | Excl_res bool + (* Request to write memory at last signalled address. Memory value should be 8 + times the size given in ea signal *) + | Write_memv memory_value bool + (* Request a memory barrier *) + | Barrier " barrier_kind " + (* Tell the system to dynamically recalculate dependency footprint *) + | Footprint + (* Request to read register *) + | Read_reg reg_name register_value + (* Request to write register *) + | Write_reg reg_name register_value + | Internal " ( string option * (unit \<Rightarrow> string)option) " + +inductive_set T :: "(('a, 'e)outcome \<times> event \<times> ('a, 'e)outcome) set" where + Read_mem: "\<exists>opt. k v = (m, opt) \<Longrightarrow> ((outcome.Read_mem (rk, addr, sz) k), Read_mem rk addr sz v, m) \<in> T" +| Write_ea: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Write_ea (rk, addr, sz) k), Write_ea rk addr sz, m) \<in> T" +| Excl_res: "\<exists>opt. k r = (m, opt) \<Longrightarrow> ((outcome.Excl_res k), Excl_res r, m) \<in> T" +| Write_memv: "\<exists>opt. k r = (m, opt) \<Longrightarrow> ((outcome.Write_memv v k), Write_memv v r, m) \<in> T" +| Barrier: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Barrier bk k), Barrier bk, m) \<in> T" +| Footprint: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Footprint k), Footprint, m) \<in> T" +| Read_reg: "\<exists>opt. k v = (m, opt) \<Longrightarrow> ((outcome.Read_reg r k), Read_reg r v, m) \<in> T" +| Write_reg: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Write_reg (r, v) k), Write_reg r v, m) \<in> T" +| Internal: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Internal descr k), Internal descr, m) \<in> T" + +inductive_set Traces :: "(('a, 'r)outcome \<times> event list \<times> ('a, 'r)outcome) set" where + Nil: "(s, [], s) \<in> Traces" +| Step: "\<lbrakk>(s, e, s'') \<in> T; (s'', t, s') \<in> Traces\<rbrakk> \<Longrightarrow> (s, e # t, s') \<in> Traces" + +declare Traces.intros[intro] +declare T.intros[intro] + +declare prod.splits[split] +(* lemma fst_case_bind[simp]: "fst (case k of (o1, x) \<Rightarrow> (bind o1 f, x)) = bind (fst k) f" + by (cases k) auto *) + +lemmas Traces_ConsI = T.intros[THEN Step, rotated] + +inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces" +inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces" + +abbreviation Run :: "('a, 'r)outcome \<Rightarrow> event list \<Rightarrow> 'a \<Rightarrow> bool" + where "Run s t a \<equiv> (s, t, Done a) \<in> Traces" + +lemma Run_appendI: + assumes "(s, t1, s') \<in> Traces" + and "Run s' t2 a" + shows "Run s (t1 @ t2) a" +proof (use assms in \<open>induction t1 arbitrary: s\<close>) + case (Cons e t1) + then show ?case by (elim Traces_ConsE) auto +qed auto + +lemma bind_DoneE: + assumes "bind m f = outcome.Done a" + obtains a' where "m = outcome.Done a'" and "f a' = outcome.Done a" + using assms by (auto elim: bind.elims) + +lemma bind_T_cases: + assumes "(bind m f, e, s') \<in> T" + obtains (Done) a where "m = Done a" + | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T" +proof cases + assume D: "\<forall>a. m \<noteq> Done a" + show thesis using assms proof cases + case (Read_mem k v rk addr sz) + then obtain k' where "m = outcome.Read_mem (rk, addr, sz) k'" using D by (cases m) auto + then show ?thesis using Read_mem by (intro Bind[of "fst (k' v)"]) auto + next + case (Write_ea k rk addr sz) + then obtain k' where "m = outcome.Write_ea (rk, addr, sz) k'" using D by (cases m) auto + then show ?thesis using Write_ea by (intro Bind[of "fst k'"]) auto + next + case (Excl_res k r) + then obtain k' where "m = outcome.Excl_res k'" using D by (cases m) auto + then show ?thesis using Excl_res by (intro Bind[of "fst (k' r)"]) auto + next + case (Write_memv k r v) + then obtain k' where "m = outcome.Write_memv v k'" using D by (cases m) auto + then show ?thesis using Write_memv by (intro Bind[of "fst (k' r)"]) auto + next + case (Barrier k bk) + then obtain k' where "m = outcome.Barrier bk k'" using D by (cases m) auto + then show ?thesis using Barrier by (intro Bind[of "fst k'"]) auto + next + case (Footprint k) + then obtain k' where "m = outcome.Footprint k'" using D by (cases m) auto + then show ?thesis using Footprint by (intro Bind[of "fst k'"]) auto + next + case (Read_reg k v r) + then obtain k' where "m = outcome.Read_reg r k'" using D by (cases m) auto + then show ?thesis using Read_reg by (intro Bind[of "fst (k' v)"]) (auto split: prod.splits) + next + case (Write_reg k r v) + then obtain k' where "m = outcome.Write_reg (r, v) k'" using D by (cases m) auto + then show ?thesis using Write_reg by (intro Bind[of "fst k'"]) auto + next + case (Internal k descr) + then obtain k' where "m = outcome.Internal descr k'" using D by (cases m) auto + then show ?thesis using Internal by (intro Bind[of "fst k'"]) auto + qed +qed auto + +lemma Run_bindE: + fixes m :: "('b, 'r) outcome" and a :: 'a + 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" +proof (use assms in \<open>induction "bind m f" t "Done a :: ('a,'r) outcome" arbitrary: m rule: Traces.induct\<close>) + case Nil + obtain am where "m = Done am" and "f am = Done a" using Nil(1) by (elim bind_DoneE) + then show ?case by (intro Nil(2)) auto +next + case (Step e s'' t m) + show thesis using Step(1) + proof (cases rule: bind_T_cases) + case (Done am) + then show ?thesis using Step(1,2) by (intro Step(4)[of "[]" "e # t" am]) auto + next + case (Bind m') + show ?thesis proof (rule Step(3)[OF Bind(1)]) + fix tm tf am + assume "t = tm @ tf" and "Run m' tm am" and "Run (f am) tf a" + then show thesis using Bind by (intro Step(4)[of "e # tm" tf am]) auto + qed + qed +qed + +lemma Run_DoneE: + assumes "Run (Done a) t a'" + obtains "t = []" and "a' = a" + using assms by (auto elim: Traces.cases T.cases) + +lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a" + by (auto elim: Run_DoneE) + +lemma Run_BarrierE[elim!]: + assumes "Run (outcome.Barrier bk k) t a" + obtains t' where "t = Barrier bk # t'" and "Run (fst k) t' a" + using assms by cases (auto elim: T.cases) + +lemma bind_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a" + shows "bind m1 f1 = bind m2 f2" +proof (unfold m, use f in \<open>induction m2 f1 arbitrary: f2 rule: bind_induct\<close>) + case (Read_mem rk addr sz k f) + have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt + using k by (auto intro!: Read_mem.IH[of _ opt v] Read_mem.prems) + then show ?case by auto +next + case (Read_reg reg k f) + have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt + using k by (auto intro!: Read_reg.IH[of _ opt v] Read_reg.prems) + then show ?case by auto +next + case (Write_memv val k f) + have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt + using k by (auto intro!: Write_memv.IH[of _ opt v] Write_memv.prems) + then show ?case by auto +next + case (Excl_res k f) + have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt + using k by (auto intro!: Excl_res.IH[of _ opt v] Excl_res.prems) + then show ?case by auto +next + case (Write_ea wk addr sz m opt f) + show ?case by (auto intro!: Write_ea) +next + case (Barrier bk m opt f) + show ?case by (auto intro!: Barrier) +next + case (Footprint m opt f) + show ?case by (auto intro!: Footprint) +next + case (Write_reg reg val m opt f) + show ?case by (auto intro!: Write_reg) +next + case (Internal i m opt f) + show ?case by (auto intro!: Internal) +qed auto + +end diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy new file mode 100644 index 00000000..c9522f58 --- /dev/null +++ b/lib/isabelle/State_monad_extras.thy @@ -0,0 +1,25 @@ +theory State_monad_extras + imports State_monad +begin + +lemma bind_ext_cong[fundef_cong]: + assumes m: "m1 s = m2 s" + and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" + shows "(bind m1 f1) s = (bind m2 f2) s" +proof - + have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception0 e, s') \<Rightarrow> [(Exception0 e, s')]) (m2 s)) = + List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception0 e, s') \<Rightarrow> [(Exception0 e, s')]) (m2 s))" + using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits) + then show ?thesis using m by (auto simp: bind_def) +qed + +lemma bind_cong[fundef_cong]: + assumes m: "m1 = m2" + and f: "\<And>s a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" + shows "bind m1 f1 = bind m2 f2" + using assms by (blast intro: bind_ext_cong) + +lemma bind_return[simp]: "bind (return x) m = m x" + by (auto simp add: bind_def return_def) + +end diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem index 044b2aa3..2d28f3c2 100644 --- a/riscv/riscv_extras_embed_sequential.lem +++ b/riscv/riscv_extras_embed_sequential.lem @@ -4,6 +4,7 @@ open import Sail_impl_base open import Sail_values open import Sail_operators open import State +open import State_monad let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 5019c2f7..d398ab52 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -1,172 +1,8 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values - -type M 'a 'e = outcome 'a 'e - -val return : forall 'a 'e. 'a -> M 'a 'e -let return a = Done a - -val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e -let rec bind m f = match m with - | Done a -> f a - | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) - | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (bind o f,opt)) - | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt)) - | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (bind o f,opt)) - | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt)) - | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (bind o f,opt)) - | Footprint o_s -> Footprint (let (o,opt) = o_s in (bind o f,opt)) - | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (bind o f,opt)) - | Escape descr -> Escape descr - | Fail descr -> Fail descr - | Error descr -> Error descr - | Exception e -> Exception e - | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt)) -end - -let inline (>>=) = bind -val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e -let inline (>>) m n = m >>= fun (_ : unit) -> n - -val exit : forall 'a 'e. unit -> M 'a 'e -let exit () = Fail Nothing - -val assert_exp : forall 'e. bool -> string -> M unit 'e -let assert_exp exp msg = if exp then Done () else Fail (Just msg) - -val throw : forall 'a 'e. 'e -> M 'a 'e -let throw e = Exception e - -val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) -> M 'a 'e2 -let rec try_catch m h = match m with - | Done a -> Done a - | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) - | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) - | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) - | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (try_catch o h,opt)) - | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (try_catch o h,opt)) - | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (try_catch o h,opt)) - | Footprint o_s -> Footprint (let (o,opt) = o_s in (try_catch o h,opt)) - | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (try_catch o h,opt)) - | Escape descr -> Escape descr - | Fail descr -> Fail descr - | Error descr -> Error descr - | Exception e -> h e - | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (try_catch o h ,opt)) -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 MR 'a 'r 'e = M 'a (either 'r 'e) - -val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e -let early_return r = throw (Left r) - -val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e -let catch_early_return m = - try_catch m - (function - | Left a -> return a - | Right e -> throw e - end) - -(* Lift to monad with early return by wrapping exceptions *) -val liftR : forall 'a 'r 'e. M 'a 'e -> MR '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 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) -> MR 'a 'r 'e2 -let try_catchR m h = - try_catch m - (function - | Left r -> throw (Left r) - | Right e -> h e - end) - - -val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e -let read_mem rk addr sz = - let addr = address_lifted_of_bitv (bits_of addr) in - let sz = natFromInteger sz in - let k memory_value = - let bitv = of_bits (internal_mem_value memory_value) in - (Done bitv,Nothing) in - Read_mem (rk,addr,sz) k - -val excl_result : forall 'e. unit -> M bool 'e -let excl_result () = - let k successful = (return successful,Nothing) in - Excl_res k - -val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e -let write_mem_ea wk addr sz = - let addr = address_lifted_of_bitv (bits_of addr) in - let sz = natFromInteger sz in - Write_ea (wk,addr,sz) (Done (),Nothing) - -val write_mem_val : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e -let write_mem_val v = - let v = external_mem_value (bits_of v) in - let k successful = (return successful,Nothing) in - Write_memv v k - -val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e -let read_reg_aux reg = - let k reg_value = - let v = of_bits (internal_reg_value reg_value) in - (Done v,Nothing) in - Read_reg reg k - -let read_reg reg = - read_reg_aux (external_reg_whole reg) -let read_reg_range reg i j = - read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) -let read_reg_bit reg i = - read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v -> - return (extract_only_element v) -let read_reg_field reg regfield = - read_reg_aux (external_reg_field_whole reg regfield.field_name) -let read_reg_bitfield reg regfield = - read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v -> - return (extract_only_element v) - -let reg_deref = read_reg - -val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e -let write_reg_aux reg_name v = - let regval = external_reg_value reg_name (bits_of v) in - Write_reg (reg_name,regval) (Done (), Nothing) - -let write_reg reg v = - write_reg_aux (external_reg_whole reg) v -let write_reg_range reg i j v = - write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v -let write_reg_pos reg i v = - let iN = natFromInteger i in - write_reg_aux (external_reg_slice reg (iN,iN)) [v] -let write_reg_bit = write_reg_pos -let write_reg_field reg regfield v = - write_reg_aux (external_reg_field_whole reg regfield.field_name) v -(*let write_reg_field_bit reg regfield bit = - write_reg_aux (external_reg_field_whole reg regfield.field_name) - (Vector [bit] 0 (is_inc_of_reg reg))*) -let write_reg_field_range reg regfield i j v = - write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v -let write_reg_field_pos reg regfield i v = - write_reg_field_range reg regfield i i [v] -let write_reg_field_bit = write_reg_field_pos - -let write_reg_ref (reg, v) = write_reg reg v - -val barrier : forall 'e. barrier_kind -> M unit 'e -let barrier bk = Barrier bk (Done (), Nothing) - - -val footprint : forall 'e. M unit 'e -let footprint = Footprint (Done (),Nothing) - +open import Prompt_monad +open import {isabelle} `Prompt_monad_extras` val iter_aux : forall 'a 'e. integer -> (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e let rec iter_aux i f xs = match xs with diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem new file mode 100644 index 00000000..45733caa --- /dev/null +++ b/src/gen_lib/prompt_monad.lem @@ -0,0 +1,168 @@ +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values + +type M 'a 'e = outcome 'a 'e + +val return : forall 'a 'e. 'a -> M 'a 'e +let return a = Done a + +val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e +let rec bind m f = match m with + | Done a -> f a + | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt)) + | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (bind o f,opt)) + | Footprint o_s -> Footprint (let (o,opt) = o_s in (bind o f,opt)) + | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (bind o f,opt)) + | Escape descr -> Escape descr + | Fail descr -> Fail descr + | Error descr -> Error descr + | Exception e -> Exception e + | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt)) +end + +let inline (>>=) = bind +val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e +let inline (>>) m n = m >>= fun (_ : unit) -> n + +val exit : forall 'a 'e. unit -> M 'a 'e +let exit () = Fail Nothing + +val assert_exp : forall 'e. bool -> string -> M unit 'e +let assert_exp exp msg = if exp then Done () else Fail (Just msg) + +val throw : forall 'a 'e. 'e -> M 'a 'e +let throw e = Exception e + +val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) -> M 'a 'e2 +let rec try_catch m h = match m with + | Done a -> Done a + | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (try_catch o h,opt)) + | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (try_catch o h,opt)) + | Footprint o_s -> Footprint (let (o,opt) = o_s in (try_catch o h,opt)) + | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (try_catch o h,opt)) + | Escape descr -> Escape descr + | Fail descr -> Fail descr + | Error descr -> Error descr + | Exception e -> h e + | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (try_catch o h ,opt)) +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 MR 'a 'r 'e = M 'a (either 'r 'e) + +val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e +let early_return r = throw (Left r) + +val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e +let catch_early_return m = + try_catch m + (function + | Left a -> return a + | Right e -> throw e + end) + +(* Lift to monad with early return by wrapping exceptions *) +val liftR : forall 'a 'r 'e. M 'a 'e -> MR '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 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) -> MR 'a 'r 'e2 +let try_catchR m h = + try_catch m + (function + | Left r -> throw (Left r) + | Right e -> h e + end) + + +val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e +let read_mem rk addr sz = + let addr = address_lifted_of_bitv (bits_of addr) in + let sz = natFromInteger sz in + let k memory_value = + let bitv = of_bits (internal_mem_value memory_value) in + (Done bitv,Nothing) in + Read_mem (rk,addr,sz) k + +val excl_result : forall 'e. unit -> M bool 'e +let excl_result () = + let k successful = (return successful,Nothing) in + Excl_res k + +val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e +let write_mem_ea wk addr sz = + let addr = address_lifted_of_bitv (bits_of addr) in + let sz = natFromInteger sz in + Write_ea (wk,addr,sz) (Done (),Nothing) + +val write_mem_val : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e +let write_mem_val v = + let v = external_mem_value (bits_of v) in + let k successful = (return successful,Nothing) in + Write_memv v k + +val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e +let read_reg_aux reg = + let k reg_value = + let v = of_bits (internal_reg_value reg_value) in + (Done v,Nothing) in + Read_reg reg k + +let read_reg reg = + read_reg_aux (external_reg_whole reg) +let read_reg_range reg i j = + read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) +let read_reg_bit reg i = + read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v -> + return (extract_only_element v) +let read_reg_field reg regfield = + read_reg_aux (external_reg_field_whole reg regfield.field_name) +let read_reg_bitfield reg regfield = + read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v -> + return (extract_only_element v) + +let reg_deref = read_reg + +val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e +let write_reg_aux reg_name v = + let regval = external_reg_value reg_name (bits_of v) in + Write_reg (reg_name,regval) (Done (), Nothing) + +let write_reg reg v = + write_reg_aux (external_reg_whole reg) v +let write_reg_range reg i j v = + write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v +let write_reg_pos reg i v = + let iN = natFromInteger i in + write_reg_aux (external_reg_slice reg (iN,iN)) [v] +let write_reg_bit = write_reg_pos +let write_reg_field reg regfield v = + write_reg_aux (external_reg_field_whole reg regfield.field_name) v +(*let write_reg_field_bit reg regfield bit = + write_reg_aux (external_reg_field_whole reg regfield.field_name) + (Vector [bit] 0 (is_inc_of_reg reg))*) +let write_reg_field_range reg regfield i j v = + write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v +let write_reg_field_pos reg regfield i v = + write_reg_field_range reg regfield i i [v] +let write_reg_field_bit = write_reg_field_pos + +let write_reg_ref (reg, v) = write_reg reg v + +val barrier : forall 'e. barrier_kind -> M unit 'e +let barrier bk = Barrier bk (Done (), Nothing) + + +val footprint : forall 'e. M unit 'e +let footprint = Footprint (Done (),Nothing) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index b6852aaf..ac6d55b5 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,253 +1,8 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values - -(* 'a is result type *) - -type memstate = map integer memory_byte -type tagstate = map integer bitU -(* type regstate = map string (vector bitU) *) - -type sequential_state 'regs = - <| regstate : 'regs; - memstate : memstate; - tagstate : tagstate; - write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool|> - -val init_state : forall 'regs. 'regs -> sequential_state 'regs -let init_state regs = - <| regstate = regs; - memstate = Map.empty; - tagstate = Map.empty; - write_ea = Nothing; - last_exclusive_operation_was_load = false |> - -type ex 'e = - | Exit - | Assert of string - | Throw of 'e - -type result 'a 'e = - | Value of 'a - | Exception of (ex 'e) - -(* State, nondeterminism and exception monad with result value type 'a - and exception type 'e. *) -type M 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs) - -val return : forall 'regs 'a 'e. 'a -> M 'regs 'a 'e -let return a s = [(Value a,s)] - -val bind : forall 'regs 'a 'b 'e. M 'regs 'a 'e -> ('a -> M 'regs 'b 'e) -> M 'regs 'b 'e -let bind m f (s : sequential_state 'regs) = - List.concatMap (function - | (Value a, s') -> f a s' - | (Exception e, s') -> [(Exception e, s')] - end) (m s) - -let inline (>>=) = bind -val (>>): forall 'regs 'b 'e. M 'regs unit 'e -> M 'regs 'b 'e -> M 'regs 'b 'e -let inline (>>) m n = m >>= fun (_ : unit) -> n - -val throw : forall 'regs 'a 'e. 'e -> M 'regs 'a 'e -let throw e s = [(Exception (Throw e), s)] - -val try_catch : forall 'regs 'a 'e1 'e2. M 'regs 'a 'e1 -> ('e1 -> M 'regs 'a 'e2) -> M 'regs 'a 'e2 -let try_catch m h s = - List.concatMap (function - | (Value a, s') -> return a s' - | (Exception (Throw e), s') -> h e s' - | (Exception Exit, s') -> [(Exception Exit, s')] - | (Exception (Assert msg), s') -> [(Exception (Assert msg), s')] - end) (m s) - -val exit : forall 'regs 'e 'a. unit -> M 'regs 'a 'e -let exit () s = [(Exception Exit, s)] - -val assert_exp : forall 'regs 'e. bool -> string -> M 'regs unit 'e -let assert_exp exp msg s = if exp then [(Value (), s)] else [(Exception (Assert msg), s)] - -(* 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 MR 'regs 'a 'r 'e = M 'regs 'a (either 'r 'e) - -val early_return : forall 'regs 'a 'r 'e. 'r -> MR 'regs 'a 'r 'e -let early_return r = throw (Left r) - -val catch_early_return : forall 'regs 'a 'e. MR 'regs 'a 'a 'e -> M 'regs 'a 'e -let catch_early_return m = - try_catch m - (function - | Left a -> return a - | Right e -> throw e - end) - -(* Lift to monad with early return by wrapping exceptions *) -val liftR : forall 'a 'r 'regs 'e. M 'regs 'a 'e -> MR 'regs '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 'regs 'a 'r 'e1 'e2. MR 'regs 'a 'r 'e1 -> ('e1 -> MR 'regs 'a 'r 'e2) -> MR 'regs 'a 'r 'e2 -let try_catchR m h = - try_catch m - (function - | Left r -> throw (Left r) - | Right e -> h e - end) - -val range : integer -> integer -> list integer -let rec range i j = - if j < i then [] - else if i = j then [i] - else i :: range (i+1) j - -val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -let get_reg state reg = reg.read_from state.regstate - -val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs -let set_reg state reg v = - <| state with regstate = reg.write_to state.regstate v |> - - -let is_exclusive = function - | Sail_impl_base.Read_plain -> false - | Sail_impl_base.Read_reserve -> true - | Sail_impl_base.Read_acquire -> false - | Sail_impl_base.Read_exclusive -> true - | Sail_impl_base.Read_exclusive_acquire -> true - | Sail_impl_base.Read_stream -> false - | Sail_impl_base.Read_RISCV_acquire -> false - | Sail_impl_base.Read_RISCV_strong_acquire -> false - | Sail_impl_base.Read_RISCV_reserved -> true - | Sail_impl_base.Read_RISCV_reserved_acquire -> true - | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true - | Sail_impl_base.Read_X86_locked -> true -end - - -val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e -let read_mem read_kind addr sz state = - let addr = unsigned addr in - let addrs = range addr (addr+sz-1) in - let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in - let value = of_bits (Sail_values.internal_mem_value memory_value) in - if is_exclusive read_kind - then [(Value value, <| state with last_exclusive_operation_was_load = true |>)] - else [(Value value, state)] - -(* caps are aligned at 32 bytes *) -let cap_alignment = (32 : integer) - -val read_tag : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> M 'regs bitU 'e -let read_tag read_kind addr state = - let addr = (unsigned addr) / cap_alignment in - let tag = match (Map.lookup addr state.tagstate) with - | Just t -> t - | Nothing -> B0 - end in - if is_exclusive read_kind - then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)] - else [(Value tag, state)] - -val excl_result : forall 'regs 'e. unit -> M 'regs bool 'e -let excl_result () state = - let success = - (Value true, <| state with last_exclusive_operation_was_load = false |>) in - (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else [] - -val write_mem_ea : forall 'regs 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit 'e -let write_mem_ea write_kind addr sz state = - [(Value (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)] - -val write_mem_val : forall 'a 'regs 'b 'e. Bitvector 'a => 'a -> M 'regs bool 'e -let write_mem_val v state = - let (write_kind,addr,sz) = match state.write_ea with - | Nothing -> failwith "write ea has not been announced yet" - | Just write_ea -> write_ea end in - let addrs = range addr (addr+sz-1) in - let v = external_mem_value (bits_of v) in - let addresses_with_value = List.zip addrs v in - let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) - state.memstate addresses_with_value in - [(Value true, <| state with memstate = memstate |>)] - -val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e -let write_tag t state = - let (write_kind,addr,sz) = match state.write_ea with - | Nothing -> failwith "write ea has not been announced yet" - | Just write_ea -> write_ea end in - let taddr = addr / cap_alignment in - let tagstate = Map.insert taddr t state.tagstate in - [(Value true, <| state with tagstate = tagstate |>)] - -val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e -let read_reg reg state = - let v = reg.read_from state.regstate in - [(Value v,state)] -(*let read_reg_range reg i j state = - let v = slice (get_reg state (name_of_reg reg)) i j in - [(Value (vec_to_bvec v),state)] -let read_reg_bit reg i state = - let v = access (get_reg state (name_of_reg reg)) i in - [(Value v,state)] -let read_reg_field reg regfield = - let (i,j) = register_field_indices reg regfield in - read_reg_range reg i j -let read_reg_bitfield reg regfield = - let (i,_) = register_field_indices reg regfield in - read_reg_bit reg i *) - -let reg_deref = read_reg - -val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e -let write_reg reg v state = - [(Value (), <| state with regstate = reg.write_to state.regstate v |>)] - -let write_reg_ref (reg, v) = write_reg reg v - -val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e -let update_reg reg f v state = - let current_value = get_reg state reg in - let new_value = f current_value v in - [(Value (), set_reg state reg new_value)] - -let write_reg_field reg regfield = update_reg reg regfield.set_field - -val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a -let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) reg_val i j (bits_of new_val) -let write_reg_range reg i j = update_reg reg (update_reg_range reg i j) - -let update_reg_pos reg i reg_val x = update_list reg.reg_is_inc reg_val i x -let write_reg_pos reg i = update_reg reg (update_reg_pos reg i) - -let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) reg_val i (to_bitU bit) -let write_reg_bit reg i = update_reg reg (update_reg_bit reg i) - -let update_reg_field_range regfield i j reg_val new_val = - let current_field_value = regfield.get_field reg_val in - let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in - regfield.set_field reg_val new_field_value -let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j) - -let update_reg_field_pos regfield i reg_val x = - let current_field_value = regfield.get_field reg_val in - let new_field_value = update_list regfield.field_is_inc current_field_value i x in - regfield.set_field reg_val new_field_value -let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i) - -let update_reg_field_bit regfield i reg_val bit = - let current_field_value = regfield.get_field reg_val in - let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in - regfield.set_field reg_val new_field_value -let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i) - -val barrier : forall 'regs 'e. barrier_kind -> M 'regs unit 'e -let barrier _ = return () - -val footprint : forall 'regs 'e. M 'regs unit 'e -let footprint s = return () s +open import State_monad +open import {isabelle} `State_monad_extras` val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e let rec iter_aux i f xs = match xs with @@ -286,24 +41,30 @@ let rec while_PP vars cond body = val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec while_PM vars cond body = +let rec while_PM vars cond body s = if cond vars then - body vars >>= fun vars -> while_PM vars cond body - else return vars + bind (body vars) (fun vars s' -> while_PM vars cond body s') s + else return vars s val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> ('vars -> 'vars) -> M 'regs 'vars 'e -let rec while_MP vars cond body = - cond vars >>= fun cond_val -> - if cond_val then while_MP (body vars) cond body else return vars +let rec while_MP vars cond body s = + bind + (cond vars) + (fun cond_val s' -> + if cond_val then while_MP (body vars) cond body s' else return vars s') s val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec while_MM vars cond body = - cond vars >>= fun cond_val -> - if cond_val then - body vars >>= fun vars -> while_MM vars cond body - else return vars +let rec while_MM vars cond body s = + bind + (cond vars) + (fun cond_val s' -> + if cond_val then + bind + (body vars) + (fun vars s'' -> while_MM vars cond body s'') s' + else return vars s') s val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars let rec until_PP vars cond body = @@ -312,44 +73,28 @@ let rec until_PP vars cond body = val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec until_PM vars cond body = - body vars >>= fun vars -> - if (cond vars) then return vars else until_PM vars cond body +let rec until_PM vars cond body s = + bind + (body vars) + (fun vars s' -> + if (cond vars) then return vars s' else until_PM vars cond body s') s val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> ('vars -> 'vars) -> M 'regs 'vars 'e -let rec until_MP vars cond body = +let rec until_MP vars cond body s = let vars = body vars in - cond vars >>= fun cond_val -> - if cond_val then return vars else until_MP vars cond body + bind + (cond vars) + (fun cond_val s' -> + if cond_val then return vars s' else until_MP vars cond body s') s val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec until_MM vars cond body = - body vars >>= fun vars -> - cond vars >>= fun cond_val -> - if cond_val then return vars else until_MM vars cond body - -(*let write_two_regs r1 r2 bvec state = - let vec = bvec_to_vec bvec in - 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 - let state1 = set_reg state (name_of_reg r1) r1_v in - let state2 = set_reg state1 (name_of_reg r2) r2_v in - [(Left (), state2)]*) +let rec until_MM vars cond body s = + bind + (body vars) + (fun vars s' -> + bind + (cond vars) + (fun cond_val s''-> + if cond_val then return vars s'' else until_MM vars cond body s'') s') s diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem new file mode 100644 index 00000000..2d8e412e --- /dev/null +++ b/src/gen_lib/state_monad.lem @@ -0,0 +1,250 @@ +open import Pervasives_extra +open import Sail_impl_base +open import Sail_values + +(* 'a is result type *) + +type memstate = map integer memory_byte +type tagstate = map integer bitU +(* type regstate = map string (vector bitU) *) + +type sequential_state 'regs = + <| regstate : 'regs; + memstate : memstate; + tagstate : tagstate; + write_ea : maybe (write_kind * integer * integer); + last_exclusive_operation_was_load : bool|> + +val init_state : forall 'regs. 'regs -> sequential_state 'regs +let init_state regs = + <| regstate = regs; + memstate = Map.empty; + tagstate = Map.empty; + write_ea = Nothing; + last_exclusive_operation_was_load = false |> + +type ex 'e = + | Exit + | Assert of string + | Throw of 'e + +type result 'a 'e = + | Value of 'a + | Exception of (ex 'e) + +(* State, nondeterminism and exception monad with result value type 'a + and exception type 'e. *) +type M 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs) + +val return : forall 'regs 'a 'e. 'a -> M 'regs 'a 'e +let return a s = [(Value a,s)] + +val bind : forall 'regs 'a 'b 'e. M 'regs 'a 'e -> ('a -> M 'regs 'b 'e) -> M 'regs 'b 'e +let bind m f (s : sequential_state 'regs) = + List.concatMap (function + | (Value a, s') -> f a s' + | (Exception e, s') -> [(Exception e, s')] + end) (m s) + +let inline (>>=) = bind +val (>>): forall 'regs 'b 'e. M 'regs unit 'e -> M 'regs 'b 'e -> M 'regs 'b 'e +let inline (>>) m n = m >>= fun (_ : unit) -> n + +val throw : forall 'regs 'a 'e. 'e -> M 'regs 'a 'e +let throw e s = [(Exception (Throw e), s)] + +val try_catch : forall 'regs 'a 'e1 'e2. M 'regs 'a 'e1 -> ('e1 -> M 'regs 'a 'e2) -> M 'regs 'a 'e2 +let try_catch m h s = + List.concatMap (function + | (Value a, s') -> return a s' + | (Exception (Throw e), s') -> h e s' + | (Exception Exit, s') -> [(Exception Exit, s')] + | (Exception (Assert msg), s') -> [(Exception (Assert msg), s')] + end) (m s) + +val exit : forall 'regs 'e 'a. unit -> M 'regs 'a 'e +let exit () s = [(Exception Exit, s)] + +val assert_exp : forall 'regs 'e. bool -> string -> M 'regs unit 'e +let assert_exp exp msg s = if exp then [(Value (), s)] else [(Exception (Assert msg), s)] + +(* 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 MR 'regs 'a 'r 'e = M 'regs 'a (either 'r 'e) + +val early_return : forall 'regs 'a 'r 'e. 'r -> MR 'regs 'a 'r 'e +let early_return r = throw (Left r) + +val catch_early_return : forall 'regs 'a 'e. MR 'regs 'a 'a 'e -> M 'regs 'a 'e +let catch_early_return m = + try_catch m + (function + | Left a -> return a + | Right e -> throw e + end) + +(* Lift to monad with early return by wrapping exceptions *) +val liftR : forall 'a 'r 'regs 'e. M 'regs 'a 'e -> MR 'regs '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 'regs 'a 'r 'e1 'e2. MR 'regs 'a 'r 'e1 -> ('e1 -> MR 'regs 'a 'r 'e2) -> MR 'regs 'a 'r 'e2 +let try_catchR m h = + try_catch m + (function + | Left r -> throw (Left r) + | Right e -> h e + end) + +val range : integer -> integer -> list integer +let rec range i j = + if j < i then [] + else if i = j then [i] + else i :: range (i+1) j + +val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a +let get_reg state reg = reg.read_from state.regstate + +val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs +let set_reg state reg v = + <| state with regstate = reg.write_to state.regstate v |> + + +let is_exclusive = function + | Sail_impl_base.Read_plain -> false + | Sail_impl_base.Read_reserve -> true + | Sail_impl_base.Read_acquire -> false + | Sail_impl_base.Read_exclusive -> true + | Sail_impl_base.Read_exclusive_acquire -> true + | Sail_impl_base.Read_stream -> false + | Sail_impl_base.Read_RISCV_acquire -> false + | Sail_impl_base.Read_RISCV_strong_acquire -> false + | Sail_impl_base.Read_RISCV_reserved -> true + | Sail_impl_base.Read_RISCV_reserved_acquire -> true + | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true + | Sail_impl_base.Read_X86_locked -> true +end + + +val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e +let read_mem read_kind addr sz state = + let addr = unsigned addr in + let addrs = range addr (addr+sz-1) in + let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in + let value = of_bits (Sail_values.internal_mem_value memory_value) in + if is_exclusive read_kind + then [(Value value, <| state with last_exclusive_operation_was_load = true |>)] + else [(Value value, state)] + +(* caps are aligned at 32 bytes *) +let cap_alignment = (32 : integer) + +val read_tag : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> M 'regs bitU 'e +let read_tag read_kind addr state = + let addr = (unsigned addr) / cap_alignment in + let tag = match (Map.lookup addr state.tagstate) with + | Just t -> t + | Nothing -> B0 + end in + if is_exclusive read_kind + then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)] + else [(Value tag, state)] + +val excl_result : forall 'regs 'e. unit -> M 'regs bool 'e +let excl_result () state = + let success = + (Value true, <| state with last_exclusive_operation_was_load = false |>) in + (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else [] + +val write_mem_ea : forall 'regs 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit 'e +let write_mem_ea write_kind addr sz state = + [(Value (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)] + +val write_mem_val : forall 'a 'regs 'b 'e. Bitvector 'a => 'a -> M 'regs bool 'e +let write_mem_val v state = + let (_,addr,sz) = match state.write_ea with + | Nothing -> failwith "write ea has not been announced yet" + | Just write_ea -> write_ea end in + let addrs = range addr (addr+sz-1) in + let v = external_mem_value (bits_of v) in + let addresses_with_value = List.zip addrs v in + let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) + state.memstate addresses_with_value in + [(Value true, <| state with memstate = memstate |>)] + +val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e +let write_tag t state = + let (_,addr,_) = match state.write_ea with + | Nothing -> failwith "write ea has not been announced yet" + | Just write_ea -> write_ea end in + let taddr = addr / cap_alignment in + let tagstate = Map.insert taddr t state.tagstate in + [(Value true, <| state with tagstate = tagstate |>)] + +val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e +let read_reg reg state = + let v = reg.read_from state.regstate in + [(Value v,state)] +(*let read_reg_range reg i j state = + let v = slice (get_reg state (name_of_reg reg)) i j in + [(Value (vec_to_bvec v),state)] +let read_reg_bit reg i state = + let v = access (get_reg state (name_of_reg reg)) i in + [(Value v,state)] +let read_reg_field reg regfield = + let (i,j) = register_field_indices reg regfield in + read_reg_range reg i j +let read_reg_bitfield reg regfield = + let (i,_) = register_field_indices reg regfield in + read_reg_bit reg i *) + +let reg_deref = read_reg + +val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e +let write_reg reg v state = + [(Value (), <| state with regstate = reg.write_to state.regstate v |>)] + +let write_reg_ref (reg, v) = write_reg reg v + +val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e +let update_reg reg f v state = + let current_value = get_reg state reg in + let new_value = f current_value v in + [(Value (), set_reg state reg new_value)] + +let write_reg_field reg regfield = update_reg reg regfield.set_field + +val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a +let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) reg_val i j (bits_of new_val) +let write_reg_range reg i j = update_reg reg (update_reg_range reg i j) + +let update_reg_pos reg i reg_val x = update_list reg.reg_is_inc reg_val i x +let write_reg_pos reg i = update_reg reg (update_reg_pos reg i) + +let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) reg_val i (to_bitU bit) +let write_reg_bit reg i = update_reg reg (update_reg_bit reg i) + +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in + regfield.set_field reg_val new_field_value +let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j) + +let update_reg_field_pos regfield i reg_val x = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update_list regfield.field_is_inc current_field_value i x in + regfield.set_field reg_val new_field_value +let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i) + +let update_reg_field_bit regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in + regfield.set_field reg_val new_field_value +let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i) + +val barrier : forall 'regs 'e. barrier_kind -> M 'regs unit 'e +let barrier _ = return () + +val footprint : forall 'regs 'e. M 'regs unit 'e +let footprint s = return () s diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 48825540..5d127f6d 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1495,15 +1495,15 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = if !opt_sequential then concat [regstate_def; hardline; hardline; - string ("type MR 'a 'r = State.MR regstate 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = State.M regstate 'a " ^ exc_typ); hardline; + string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline; hardline; register_refs ] else concat [ - string ("type MR 'a 'r = Prompt.MR 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = Prompt.M 'a " ^ exc_typ); hardline + string ("type MR 'a 'r = Prompt_monad.MR 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = Prompt_monad.M 'a " ^ exc_typ); hardline ] ]); (print defs_file) diff --git a/src/process_file.ml b/src/process_file.ml index b0034493..9ff208ca 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -228,16 +228,19 @@ let output_lem filename libs defs = let generated_line = generated_line filename in let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in let types_module = (filename ^ "_embed_types" ^ seq_suffix) in - let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in + let monad_modules = + if !Pretty_print_lem.opt_sequential + then ["State_monad"; "State"] + else ["Prompt_monad"; "Prompt"] in let operators_module = "Sail_operators" (* if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" *) in let libs = List.map (fun lib -> lib ^ seq_suffix) libs in let base_imports = [ "Pervasives_extra"; "Sail_impl_base"; "Sail_values"; - operators_module; - monad_module - ] in + operators_module + ] @ monad_modules + in let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in let ((o,_, _) as ext_o) = |