diff options
| -rw-r--r-- | lib/isabelle/Makefile | 6 | ||||
| -rw-r--r-- | lib/isabelle/Prompt_monad_extras.thy | 171 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_extras.thy | 4 | ||||
| -rw-r--r-- | riscv/riscv_extras_embed_sequential.lem | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 44 | ||||
| -rw-r--r-- | src/ast_util.mli | 5 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 40 | ||||
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 204 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 126 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 56 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 373 | ||||
| -rw-r--r-- | src/lem_interp/sail_instr_kinds.lem | 436 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 184 | ||||
| -rw-r--r-- | src/process_file.ml | 2 | ||||
| -rw-r--r-- | src/sail.ml | 7 | ||||
| -rw-r--r-- | src/state.ml | 279 |
20 files changed, 1102 insertions, 841 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 84af5d75..50e6d471 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,4 +1,4 @@ -THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy \ +THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ Sail_operators_mwords.thy Sail_operators_bitlists.thy \ State_monad.thy State.thy Prompt_monad.thy Prompt.thy EXTRA_THYS = State_monad_extras.thy Prompt_monad_extras.thy @@ -14,10 +14,10 @@ heap-img: $(THYS) $(EXTRA_THYS) ROOT @echo '*** and add the isabelle binary to your PATH.' isabelle build -b Sail -Sail_impl_base.thy: ../../src/lem_interp/sail_impl_base.lem +Sail_instr_kinds.thy: ../../src/lem_interp/sail_instr_kinds.lem lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_impl_base.thy +Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy index 0c319f97..e93c6052 100644 --- a/lib/isabelle/Prompt_monad_extras.thy +++ b/lib/isabelle/Prompt_monad_extras.thy @@ -2,60 +2,50 @@ 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)+ +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 Error Exception] = bind.induct -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 = +lemma bind_return[simp]: "bind (return a) f = f a" + by (auto simp: return_def) + +lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)" + by (induction m f arbitrary: g rule: bind.induct) auto + +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 Error Exception] = try_catch.induct + +datatype 'regval event = (* Request to read memory *) - Read_mem read_kind address_lifted nat memory_value + e_read_mem read_kind int int "memory_byte list" (* Write is imminent, at address lifted, of size nat *) - | Write_ea write_kind address_lifted nat + | e_write_ea write_kind int int (* Request the result of store-exclusive *) - | Excl_res bool + | e_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 + | e_write_memv "memory_byte list" bool (* Request a memory barrier *) - | Barrier " barrier_kind " - (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint + | e_barrier " barrier_kind " (* Request to read register *) - | Read_reg reg_name register_value + | e_read_reg string 'regval (* 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 + | e_write_reg string 'regval + +inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where + Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T" +| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T" +| Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T" +| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T" +| Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T" +| Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T" +| Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T" + +inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) 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" @@ -63,15 +53,13 @@ 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" +abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool" where "Run s t a \<equiv> (s, t, Done a) \<in> Traces" lemma Run_appendI: @@ -84,60 +72,21 @@ proof (use assms in \<open>induction t1 arbitrary: s\<close>) 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" + 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 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 + using assms by (cases; blast elim: bind.elims) lemma Run_bindE: - fixes m :: "('b, 'r) outcome" and a :: 'a + fixes m :: "('rv, 'b, 'e) monad" 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>) +proof (use assms in \<open>induction "bind m f" t "Done a :: ('rv, 'a, 'e) monad" 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 @@ -166,49 +115,15 @@ lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \< 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" + assumes "Run (Barrier bk k) t a" + obtains t' where "t = e_barrier bk # t'" and "Run 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 + unfolding m using f + by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast) end diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy index c9522f58..cf042a02 100644 --- a/lib/isabelle/State_monad_extras.thy +++ b/lib/isabelle/State_monad_extras.thy @@ -7,8 +7,8 @@ lemma bind_ext_cong[fundef_cong]: 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))" + have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s)) = + List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception e, s') \<Rightarrow> [(Exception 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 diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem index cc2a5277..31eea6ab 100644 --- a/riscv/riscv_extras_embed_sequential.lem +++ b/riscv/riscv_extras_embed_sequential.lem @@ -1,6 +1,6 @@ open import Pervasives open import Pervasives_extra -open import Sail_impl_base +open import Sail_instr_kinds open import Sail_values open import Sail_operators_mwords open import State diff --git a/src/ast_util.ml b/src/ast_util.ml index 7f660745..27ae93e8 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -712,6 +712,21 @@ let rec string_of_index_range (BF_aux (ir, _)) = | BF_range (n, m) -> Big_int.to_string n ^ " .. " ^ Big_int.to_string m | BF_concat (ir1, ir2) -> "(" ^ string_of_index_range ir1 ^ ") : (" ^ string_of_index_range ir2 ^ ")" + +let rec pat_ids (P_aux (pat_aux, _)) = + match pat_aux with + | P_lit _ | P_wild -> IdSet.empty + | P_id id -> IdSet.singleton id + | P_as (pat, id) -> IdSet.add id (pat_ids pat) + | P_var (pat, _) | P_typ (_, pat) -> pat_ids pat + | P_app (_, pats) | P_tup pats | P_vector pats | P_vector_concat pats | P_list pats -> + List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty + | P_cons (pat1, pat2) -> + IdSet.union (pat_ids pat1) (pat_ids pat2) + | P_record (fpats, _) -> + List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty +and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat + let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) = match (List.fold_right (fun (FCL_aux (FCL_Funcl (id, _), _)) id' -> @@ -733,6 +748,20 @@ let id_of_type_def_aux = function | TD_bitfield (id, _, _) -> id let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux +let id_of_val_spec (VS_aux (VS_val_spec (_, id, _, _), _)) = id + +let ids_of_def = function + | DEF_kind (KD_aux (KD_nabbrev (_, id, _, _), _)) -> IdSet.singleton id + | DEF_type td -> IdSet.singleton (id_of_type_def td) + | DEF_fundef fd -> IdSet.singleton (id_of_fundef fd) + | DEF_val (LB_aux (LB_val (pat, _), _)) -> pat_ids pat + | DEF_reg_dec (DEC_aux (DEC_reg (_, id), _)) -> IdSet.singleton id + | DEF_spec vs -> IdSet.singleton (id_of_val_spec vs) + | DEF_internal_mutrec fds -> IdSet.of_list (List.map id_of_fundef fds) + | _ -> IdSet.empty +let ids_of_defs (Defs defs) = + List.fold_left IdSet.union IdSet.empty (List.map ids_of_def defs) + module BE = struct type t = base_effect let compare be1 be2 = String.compare (string_of_base_effect be1) (string_of_base_effect be2) @@ -965,26 +994,13 @@ let split_defs f (Defs defs) = Some (Defs (List.rev pre_defs), def, Defs post_defs) let append_ast (Defs ast1) (Defs ast2) = Defs (ast1 @ ast2) +let concat_ast asts = List.fold_right append_ast asts (Defs []) let type_union_id (Tu_aux (aux, _)) = match aux with | Tu_id id -> id | Tu_ty_id (_, id) -> id -let rec pat_ids (P_aux (pat_aux, _)) = - match pat_aux with - | P_lit _ | P_wild -> IdSet.empty - | P_id id -> IdSet.singleton id - | P_as (pat, id) -> IdSet.add id (pat_ids pat) - | P_var (pat, _) | P_typ (_, pat) -> pat_ids pat - | P_app (_, pats) | P_tup pats | P_vector pats | P_vector_concat pats | P_list pats -> - List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty - | P_cons (pat1, pat2) -> - IdSet.union (pat_ids pat1) (pat_ids pat2) - | P_record (fpats, _) -> - List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty -and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat - let rec subst id value (E_aux (e_aux, annot) as exp) = let wrap e_aux = E_aux (e_aux, annot) in let e_aux = match e_aux with diff --git a/src/ast_util.mli b/src/ast_util.mli index bc2181e8..bbbde27f 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -211,6 +211,7 @@ val string_of_index_range : index_range -> string val id_of_fundef : 'a fundef -> id val id_of_type_def : 'a type_def -> id +val id_of_val_spec : 'a val_spec -> id val id_of_kid : kid -> id val kid_of_id : id -> kid @@ -306,8 +307,12 @@ val rename_fundef : id -> 'a fundef -> 'a fundef val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option val append_ast : 'a defs -> 'a defs -> 'a defs +val concat_ast : 'a defs list -> 'a defs val type_union_id : type_union -> id +val ids_of_def : 'a def -> IdSet.t +val ids_of_defs : 'a defs -> IdSet.t + val pat_ids : 'a pat -> IdSet.t val subst : id -> 'a exp -> 'a exp -> 'a exp diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index d398ab52..756bb699 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -1,24 +1,24 @@ open import Pervasives_extra -open import Sail_impl_base +(*open import Sail_impl_base*) open import Sail_values 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 +val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad '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 -val iteri : forall 'a 'e. (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e +val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e let iteri f xs = iter_aux 0 f xs -val iter : forall 'a 'e. ('a -> M unit 'e) -> list 'a -> M unit 'e +val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e let iter f xs = iteri (fun _ x -> f x) xs -val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e +val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec foreachM_inc (i,stop,by) vars body = if (by > 0 && i <= stop) || (by < 0 && stop <= i) then @@ -27,8 +27,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return vars -val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e +val foreachM_dec : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec foreachM_dec (i,stop,by) vars body = if (by > 0 && i >= stop) || (by < 0 && stop >= i) then @@ -40,21 +40,21 @@ val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'va let rec while_PP vars cond body = if cond vars then while_PP (body vars) cond body else vars -val while_PM : forall 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> M 'vars 'e) -> M 'vars 'e +val while_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) -> + ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec while_PM vars cond body = if cond vars then body vars >>= fun vars -> while_PM vars cond body else return vars -val while_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> - ('vars -> 'vars) -> M 'vars 'e +val while_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> + ('vars -> 'vars) -> monad 'rv '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 -val while_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> - ('vars -> M 'vars 'e) -> M 'vars 'e +val while_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> + ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec while_MM vars cond body = cond vars >>= fun cond_val -> if cond_val then @@ -66,21 +66,21 @@ let rec until_PP vars cond body = let vars = body vars in if (cond vars) then vars else until_PP (body vars) cond body -val until_PM : forall 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> M 'vars 'e) -> M 'vars 'e +val until_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) -> + ('vars -> monad 'rv 'vars 'e) -> monad 'rv '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 -val until_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> - ('vars -> 'vars) -> M 'vars 'e +val until_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> + ('vars -> 'vars) -> monad 'rv 'vars 'e let rec until_MP vars cond body = let vars = body vars in cond vars >>= fun cond_val -> if cond_val then return vars else until_MP vars cond body -val until_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> - ('vars -> M 'vars 'e) -> M 'vars 'e +val until_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> + ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec until_MM vars cond body = body vars >>= fun vars -> cond vars >>= fun cond_val -> diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 45733caa..ff5e3726 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -1,70 +1,88 @@ open import Pervasives_extra -open import Sail_impl_base +(*open import Sail_impl_base*) +open import Sail_instr_kinds open import Sail_values -type M 'a 'e = outcome 'a 'e - -val return : forall 'a 'e. 'a -> M 'a 'e +type register_name = string + +type monad 'regval 'a 'e = + | Done of 'a + | Read_mem of read_kind * integer * integer * (list memory_byte -> monad 'regval 'a 'e) + (* Tell the system a write is imminent, at address lifted, of size nat *) + | Write_ea of write_kind * integer * integer * monad 'regval 'a 'e + (* Request the result of store-exclusive *) + | Excl_res of (bool -> monad 'regval 'a 'e) + (* Request to write memory at last signalled address. Memory value should be 8 + times the size given in ea signal *) + | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e) + (* Request a memory barrier *) + | Barrier of barrier_kind * monad 'regval 'a 'e + (* Request to read register, will track dependency when mode.track_values *) + | Read_reg of register_name * ('regval -> monad 'regval 'a 'e) + (* Request to write register *) + | Write_reg of register_name * 'regval * monad 'regval 'a 'e + (*Result of a failed assert with possible error message to report*) + | Fail of string + | Error of string + (* Exception of type 'e *) + | Exception of 'e + (* TODO: Reading/writing tags *) + +val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e let return a = Done a -val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e +val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv '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)) + | Done a -> f a + | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f) + | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f) + | Read_reg descr k -> Read_reg descr (fun v -> bind (k v) f) + | Excl_res k -> Excl_res (fun v -> bind (k v) f) + | Write_ea wk a sz k -> Write_ea wk a sz (bind k f) + | Barrier bk k -> Barrier bk (bind k f) + | Write_reg r v k -> Write_reg r v (bind k f) + | Fail descr -> Fail descr + | Error descr -> Error descr + | Exception e -> Exception e end let inline (>>=) = bind -val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e +val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e let inline (>>) m n = m >>= fun (_ : unit) -> n -val exit : forall 'a 'e. unit -> M 'a 'e -let exit () = Fail Nothing +val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e +let exit () = Fail "exit" -val assert_exp : forall 'e. bool -> string -> M unit 'e -let assert_exp exp msg = if exp then Done () else Fail (Just msg) +val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e +let assert_exp exp msg = if exp then Done () else Fail msg -val throw : forall 'a 'e. 'e -> M 'a 'e +val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e let throw e = Exception e -val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) -> M 'a 'e2 +val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv '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)) + | Done a -> Done a + | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h) + | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h) + | Read_reg descr k -> Read_reg descr (fun v -> try_catch (k v) h) + | Excl_res k -> Excl_res (fun v -> try_catch (k v) h) + | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h) + | Barrier bk k -> Barrier bk (try_catch k h) + | Write_reg r v k -> Write_reg r v (try_catch k h) + | Fail descr -> Fail descr + | Error descr -> Error descr + | Exception e -> h e 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) +type monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e) -val early_return : forall 'a 'r 'e. 'r -> MR 'a '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 'a 'e. MR 'a 'a 'e -> M 'a 'e +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 @@ -73,11 +91,11 @@ let catch_early_return m = end) (* Lift to monad with early return by wrapping exceptions *) -val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e +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 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) -> MR 'a 'r 'e2 +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 @@ -86,59 +104,62 @@ let try_catchR m h = end) -val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e +val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv '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 addr = unsigned addr in + let k bytes = + let bitv = bits_of_bytes (List.reverse bytes) in + (Done bitv) in + Read_mem rk addr sz k + +val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e let excl_result () = - let k successful = (return successful,Nothing) in + let k successful = (return successful) 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 +val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e +let write_mem_ea wk addr sz = Write_ea wk (unsigned addr) sz (Done ()) +val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e +let write_mem_val v = match bytes_of_bits v with + | Just v -> + let k successful = (return successful) in + Write_memv (List.reverse v) k + | Nothing -> fail "write_mem_val" +end + +val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e let read_reg reg = - read_reg_aux (external_reg_whole reg) + let k v = + match reg.of_regval v with + | Just v -> Done v + | Nothing -> Error "read_reg: unrecognised value" + end + in + Read_reg reg.name k + +(* TODO +val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e let read_reg_range reg i j = - read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) + read_reg_aux of_bits (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 -> + read_reg_aux (fun v -> v) (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) + read_reg_aux (external_reg_field_whole reg regfield) + let read_reg_bitfield reg regfield = - read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v -> - return (extract_only_element v) + read_reg_aux (external_reg_field_whole reg regfield) >>= 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) +val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e +let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) +(* TODO let write_reg reg v = write_reg_aux (external_reg_whole reg) v let write_reg_range reg i j v = @@ -149,20 +170,17 @@ let write_reg_pos reg i 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 = +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))*) + (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) +let write_reg_field_bit = write_reg_field_pos*) +val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e +let barrier bk = Barrier bk (Done ()) -val footprint : forall 'e. M unit 'e -let footprint = Footprint (Done (),Nothing) +(*val footprint : forall 'rv 'e. monad 'rv unit 'e +let footprint = Footprint (Done ())*) diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index ada91bd0..7d6b156b 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -1,6 +1,5 @@ open import Pervasives_extra open import Machine_word -open import Sail_impl_base open import Sail_values (*** Bit vector operations *) diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index d2a2aea1..5658dc21 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -1,6 +1,5 @@ open import Pervasives_extra open import Machine_word -open import Sail_impl_base open import Sail_values open import Sail_operators diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index bd7ef2b4..fcc3153b 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -1,6 +1,5 @@ open import Pervasives_extra open import Machine_word -open import Sail_impl_base open import Sail_values open import Sail_operators diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 4cbcc269..34e4bd98 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -2,7 +2,7 @@ open import Pervasives_extra open import Machine_word -open import Sail_impl_base +(*open import Sail_impl_base*) type ii = integer @@ -57,6 +57,7 @@ val repeat : forall 'a. list 'a -> integer -> list 'a let rec repeat xs n = if n <= 0 then [] else xs ++ repeat xs (n-1) +declare {isabelle} termination_argument repeat = automatic let duplicate_to_list bit length = repeat [bit] length @@ -66,6 +67,7 @@ let rec replace bs (n : integer) b' = match bs with if n = 0 then b' :: bs else b :: replace bs (n - 1) b' end +declare {isabelle} termination_argument replace = automatic let upper n = n @@ -135,7 +137,7 @@ end let cast_bit_bool = bool_of_bitU -let bit_lifted_of_bitU = function +(*let bit_lifted_of_bitU = function | B0 -> Bitl_zero | B1 -> Bitl_one | BU -> Bitl_undef @@ -157,7 +159,7 @@ let bitU_of_bit_lifted = function | Bitl_one -> B1 | Bitl_undef -> BU | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" - end + end*) let not_bit = function | B1 -> B0 @@ -200,6 +202,7 @@ val bits_of_nat_aux : natural -> list bitU let rec bits_of_nat_aux x = if x = 0 then [] else (if x mod 2 = 1 then B1 else B0) :: bits_of_nat_aux (x / 2) +declare {isabelle} termination_argument bits_of_nat_aux = automatic let bits_of_nat n = List.reverse (bits_of_nat_aux n) val nat_of_bits : list bitU -> natural @@ -239,6 +242,7 @@ let signed_of_bits bits = val pad_bitlist : bitU -> list bitU -> integer -> list bitU let rec pad_bitlist b bits n = if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1) +declare {isabelle} termination_argument pad_bitlist = automatic let ext_bits pad len bits = let longer = len - (integerFromNat (List.length bits)) in @@ -259,6 +263,7 @@ let rec add_one_bit_ignore_overflow_aux bits = match bits with | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" end +declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) @@ -300,6 +305,7 @@ let rec hexstring_of_bits bs = match bs with end | _ -> Nothing end +declare {isabelle} termination_argument hexstring_of_bits = automatic let show_bitlist bs = match hexstring_of_bits bs with @@ -370,6 +376,21 @@ let extract_only_element = function | _ -> failwith "extract_only_element called for list with more elements" end +(* just_list takes a list of maybes and returns Just xs if all elements have + a value, and Nothing if one of the elements is Nothing. *) +val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a) +let rec just_list [] = Just [] +and just_list (x :: xs) = + match (x, just_list xs) with + | (Just x, Just xs) -> Just (x :: xs) + | (_, _) -> Nothing + end +declare {isabelle} termination_argument just_list = automatic + +lemma just_list_spec: + ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) && + (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es))) + (*** Machine words *) val length_mword : forall 'a. mword 'a -> integer @@ -503,14 +524,24 @@ let string_of_bv v = show_bitlist (bits_of v) (*** Bytes and addresses *) -val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) -let rec byte_chunks n list = match (n,list) with - | (0,_) -> [] - | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest - | _ -> failwith "byte_chunks not given enough bits" +type memory_byte = list bitU + +val byte_chunks : forall 'a. list 'a -> maybe (list (list 'a)) +let rec byte_chunks bs = match bs with + | [] -> Just [] + | a::b::c::d::e::f::g::h::rest -> + Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest)) + | _ -> Nothing end +declare {isabelle} termination_argument byte_chunks = automatic + +val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte) +let bytes_of_bits bs = byte_chunks (bits_of bs) -val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU +val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> 'a +let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs)) + +(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU let bitv_of_byte_lifteds v = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v @@ -545,10 +576,13 @@ let address_lifted_of_bitv v = end in Address_lifted byte_lifteds maybe_address_integer +val bitv_of_address_lifted : address_lifted -> list bitU +let bitv_of_address_lifted (Address_lifted bs _) = bitv_of_byte_lifteds bs + val address_of_bitv : list bitU -> address let address_of_bitv v = let bytes = bytes_of_bitv v in - address_of_byte_list bytes + address_of_byte_list bytes*) let rec reverse_endianness_list bits = if List.length bits <= 8 then bits else @@ -560,7 +594,7 @@ let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v)) (*** Registers *) -type register_field = string +(*type register_field = string type register_field_index = string * (integer * integer) (* name, start and end *) type register = @@ -570,14 +604,19 @@ type register = bool * (* is increasing *) list register_field_index | UndefinedRegister of integer (* length *) - | RegisterPair of register * register + | RegisterPair of register * register*) -type register_ref 'regstate 'a = - <| reg_name : string; - reg_start : integer; - reg_is_inc : bool; +type register_ref 'regstate 'regval 'a = + <| name : string; + is_inc : bool; read_from : 'regstate -> 'a; - write_to : 'regstate -> 'a -> 'regstate |> + write_to : 'regstate -> 'a -> 'regstate; + of_regval : 'regval -> maybe 'a; + regval_of : 'a -> 'regval |> + +type register_accessors 'regstate 'regval = + ((string -> 'regstate -> maybe 'regval) * + (string -> 'regval -> 'regstate -> maybe 'regstate)) type field_ref 'regtype 'a = <| field_name : string; @@ -586,7 +625,7 @@ type field_ref 'regtype 'a = get_field : 'regtype -> 'a; set_field : 'regtype -> 'a -> 'regtype |> -let name_of_reg = function +(*let name_of_reg = function | Register name _ _ _ _ -> name | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" | RegisterPair _ _ -> failwith "name_of_reg RegisterPair" @@ -597,7 +636,7 @@ let size_of_reg = function | UndefinedRegister size -> size | RegisterPair _ _ -> failwith "size_of_reg RegisterPair" end - + let start_of_reg = function | Register _ _ start _ _ -> start | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister" @@ -638,11 +677,11 @@ let register_field_indices register rfield = let register_field_indices_nat reg regfield= let (i,j) = register_field_indices reg regfield in - (natFromInteger i,natFromInteger j) + (natFromInteger i,natFromInteger j)*) -let rec external_reg_value reg_name v = +(*let rec external_reg_value reg_name v = let (internal_start, external_start, direction) = - match reg_name with + match reg_name with | Reg _ start size dir -> (start, (if dir = D_increasing then start else (start - (size +1))), dir) | Reg_slice _ reg_start dir (slice_start, _) -> @@ -653,10 +692,10 @@ let rec external_reg_value reg_name v = slice_start, dir) | Reg_f_slice _ reg_start dir _ _ (slice_start, _) -> ((if dir = D_increasing then slice_start else (reg_start - slice_start)), - slice_start, dir) + slice_start, dir) end in let bits = bit_lifteds_of_bitv v in - <| rv_bits = bits; + <| rv_bits = bits; rv_dir = direction; rv_start = external_start; rv_start_internal = internal_start |> @@ -672,42 +711,45 @@ let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = match d with (*This is the case the thread/concurrecny model expects, so no change needed*) | D_increasing -> (i,j) - | D_decreasing -> let slice_i = start - i in + | D_decreasing -> let slice_i = start - i in let slice_j = (i - j) + slice_i in (slice_i,slice_j) - end + end *) -let external_reg_whole reg = - Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg) - -let external_reg_slice reg (i,j) = - let start = start_of_reg_nat reg in - let dir = dir_of_reg reg in - Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j)) +(* TODO +let external_reg_whole r = + Reg (r.name) (natFromInteger r.start) (natFromInteger r.size) (dir_of_bool r.is_inc) + +let external_reg_slice r (i,j) = + let start = natFromInteger r.start in + let dir = dir_of_bool r.is_inc in + Reg_slice (r.name) start dir (external_slice dir start (i,j)) -let external_reg_field_whole reg rfield = +let external_reg_field_whole reg rfield = let (m,n) = register_field_indices_nat reg rfield in let start = start_of_reg_nat reg in let dir = dir_of_reg reg in Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n)) - -let external_reg_field_slice reg rfield (i,j) = + +let external_reg_field_slice reg rfield (i,j) = let (m,n) = register_field_indices_nat reg rfield in let start = start_of_reg_nat reg in let dir = dir_of_reg reg in Reg_f_slice (name_of_reg reg) start dir rfield (external_slice dir start (m,n)) - (external_slice dir start (i,j)) + (external_slice dir start (i,j))*) +(*val external_mem_value : list bitU -> memory_value let external_mem_value v = byte_lifteds_of_bitv v $> List.reverse +val internal_mem_value : memory_value -> list bitU let internal_mem_value bytes = - List.reverse bytes $> bitv_of_byte_lifteds + List.reverse bytes $> bitv_of_byte_lifteds*) + - val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars @@ -756,7 +798,7 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) = | RSliceBit of (string * integer) | RField of (string * string) -type niafp = +type niafp = | NIAFP_successor | NIAFP_concrete_address of vector bitU | NIAFP_LR @@ -764,13 +806,13 @@ type niafp = | NIAFP_register of regfp (* only for MIPS *) -type diafp = +type diafp = | DIAFP_none | DIAFP_concrete of vector bitU | DIAFP_reg of regfp let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function - | RFull name -> + | RFull name -> let (start,length,direction,_) = reg_info name Nothing in Reg name start length direction | RSlice (name,i,j) -> diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index ac6d55b5..d4e2b128 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,5 +1,4 @@ open import Pervasives_extra -open import Sail_impl_base open import Sail_values open import State_monad open import {isabelle} `State_monad_extras` diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 2d8e412e..a3bf4b5f 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -1,5 +1,5 @@ open import Pervasives_extra -open import Sail_impl_base +open import Sail_instr_kinds open import Sail_values (* 'a is result type *) @@ -103,37 +103,21 @@ let rec range i j = 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 +val get_reg : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv '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 +val set_reg : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv '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 + let value = bits_of_bytes (List.reverse memory_value) in + if read_is_exclusive read_kind then [(Value value, <| state with last_exclusive_operation_was_load = true |>)] else [(Value value, state)] @@ -147,7 +131,7 @@ let read_tag read_kind addr state = | Just t -> t | Nothing -> B0 end in - if is_exclusive read_kind + if read_is_exclusive read_kind then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)] else [(Value tag, state)] @@ -167,11 +151,15 @@ let write_mem_val v state = | 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 |>)] + match bytes_of_bits v with + | Just v -> + let addresses_with_value = List.zip addrs (List.reverse 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 |>)] + | Nothing -> + [(Exception (Assert "write_mem_val"), state)] + end val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e let write_tag t state = @@ -182,7 +170,7 @@ let write_tag t state = 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 +val read_reg : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> M 'regs 'a 'e let read_reg reg state = let v = reg.read_from state.regstate in [(Value v,state)] @@ -201,13 +189,13 @@ let read_reg_bitfield reg regfield = let reg_deref = read_reg -val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e +val write_reg : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv '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 +val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv '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 @@ -215,14 +203,14 @@ let update_reg reg f v state = 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) +val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a +let update_reg_range reg i j reg_val new_val = set_bits (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 update_reg_pos reg i reg_val x = update_list 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 update_reg_bit reg i reg_val bit = set_bit (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 = diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 219677ac..f029b952 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -49,7 +49,7 @@ (*========================================================================*) open import Pervasives_extra - +open import Sail_instr_kinds class ( EnumerationType 'a ) @@ -478,373 +478,10 @@ end (* Data structures for building up instructions *) -(* careful: changes in the read/write/barrier kinds have to be - reflected in deep_shallow_convert *) -type read_kind = - (* common reads *) - | Read_plain - (* Power reads *) - | Read_reserve - (* AArch64 reads *) - | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream - (* RISC-V reads *) - | Read_RISCV_acquire | Read_RISCV_strong_acquire - | Read_RISCV_reserved | Read_RISCV_reserved_acquire - | Read_RISCV_reserved_strong_acquire - (* x86 reads *) - | Read_X86_locked (* the read part of a lock'd instruction (rmw) *) - -instance (Show read_kind) - let show = function - | Read_plain -> "Read_plain" - | Read_reserve -> "Read_reserve" - | Read_acquire -> "Read_acquire" - | Read_exclusive -> "Read_exclusive" - | Read_exclusive_acquire -> "Read_exclusive_acquire" - | Read_stream -> "Read_stream" - | Read_RISCV_acquire -> "Read_RISCV_acquire" - | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire" - | Read_RISCV_reserved -> "Read_RISCV_reserved" - | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" - | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire" - | Read_X86_locked -> "Read_X86_locked" - end -end - -type write_kind = - (* common writes *) - | Write_plain - (* Power writes *) - | Write_conditional - (* AArch64 writes *) - | Write_release | Write_exclusive | Write_exclusive_release - (* RISC-V *) - | Write_RISCV_release | Write_RISCV_strong_release - | Write_RISCV_conditional | Write_RISCV_conditional_release - | Write_RISCV_conditional_strong_release - (* x86 writes *) - | Write_X86_locked (* the write part of a lock'd instruction (rmw) *) - -instance (Show write_kind) - let show = function - | Write_plain -> "Write_plain" - | Write_conditional -> "Write_conditional" - | Write_release -> "Write_release" - | Write_exclusive -> "Write_exclusive" - | Write_exclusive_release -> "Write_exclusive_release" - | Write_RISCV_release -> "Write_RISCV_release" - | Write_RISCV_strong_release -> "Write_RISCV_strong_release" - | Write_RISCV_conditional -> "Write_RISCV_conditional" - | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" - | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release" - | Write_X86_locked -> "Write_X86_locked" - end -end - -type barrier_kind = - (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync - (* AArch64 barriers *) - | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB - | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB - | Barrier_TM_COMMIT - (* MIPS barriers *) - | Barrier_MIPS_SYNC - (* RISC-V barriers *) - | Barrier_RISCV_rw_rw - | Barrier_RISCV_r_rw - | Barrier_RISCV_r_r - | Barrier_RISCV_rw_w - | Barrier_RISCV_w_w - | Barrier_RISCV_i - (* X86 *) - | Barrier_x86_MFENCE - - -instance (Show barrier_kind) - let show = function - | Barrier_Sync -> "Barrier_Sync" - | Barrier_LwSync -> "Barrier_LwSync" - | Barrier_Eieio -> "Barrier_Eieio" - | Barrier_Isync -> "Barrier_Isync" - | Barrier_DMB -> "Barrier_DMB" - | Barrier_DMB_ST -> "Barrier_DMB_ST" - | Barrier_DMB_LD -> "Barrier_DMB_LD" - | Barrier_DSB -> "Barrier_DSB" - | Barrier_DSB_ST -> "Barrier_DSB_ST" - | Barrier_DSB_LD -> "Barrier_DSB_LD" - | Barrier_ISB -> "Barrier_ISB" - | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" - | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" - | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" - | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" - | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" - | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" - | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" - | Barrier_RISCV_i -> "Barrier_RISCV_i" - | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" - end -end - -type trans_kind = - (* AArch64 *) - | Transaction_start | Transaction_commit | Transaction_abort - -instance (Show trans_kind) - let show = function - | Transaction_start -> "Transaction_start" - | Transaction_commit -> "Transaction_commit" - | Transaction_abort -> "Transaction_abort" - end -end - -type instruction_kind = - | IK_barrier of barrier_kind - | IK_mem_read of read_kind - | IK_mem_write of write_kind - | IK_mem_rmw of (read_kind * write_kind) - | IK_cond_branch - (* unconditional branches are not distinguished in the instruction_kind; - they just have particular nias (and will be IK_simple *) - (* | IK_uncond_branch *) - | IK_trans of trans_kind - | IK_simple - - -instance (Show instruction_kind) - let show = function - | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind) - | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) - | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) - | IK_cond_branch -> "IK_cond_branch" - | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) - | IK_simple -> "IK_simple" - end -end - - - -let ~{ocaml} read_kindCompare rk1 rk2 = - match (rk1, rk2) with - | (Read_plain, Read_plain) -> EQ - | (Read_plain, Read_reserve) -> LT - | (Read_plain, Read_acquire) -> LT - | (Read_plain, Read_exclusive) -> LT - | (Read_plain, Read_exclusive_acquire) -> LT - | (Read_plain, Read_stream) -> LT - - | (Read_reserve, Read_plain) -> GT - | (Read_reserve, Read_reserve) -> EQ - | (Read_reserve, Read_acquire) -> LT - | (Read_reserve, Read_exclusive) -> LT - | (Read_reserve, Read_exclusive_acquire) -> LT - | (Read_reserve, Read_stream) -> LT - - | (Read_acquire, Read_plain) -> GT - | (Read_acquire, Read_reserve) -> GT - | (Read_acquire, Read_acquire) -> EQ - | (Read_acquire, Read_exclusive) -> LT - | (Read_acquire, Read_exclusive_acquire) -> LT - | (Read_acquire, Read_stream) -> LT - - | (Read_exclusive, Read_plain) -> GT - | (Read_exclusive, Read_reserve) -> GT - | (Read_exclusive, Read_acquire) -> GT - | (Read_exclusive, Read_exclusive) -> EQ - | (Read_exclusive, Read_exclusive_acquire) -> LT - | (Read_exclusive, Read_stream) -> LT - - | (Read_exclusive_acquire, Read_plain) -> GT - | (Read_exclusive_acquire, Read_reserve) -> GT - | (Read_exclusive_acquire, Read_acquire) -> GT - | (Read_exclusive_acquire, Read_exclusive) -> GT - | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ - | (Read_exclusive_acquire, Read_stream) -> GT - - | (Read_stream, Read_plain) -> GT - | (Read_stream, Read_reserve) -> GT - | (Read_stream, Read_acquire) -> GT - | (Read_stream, Read_exclusive) -> GT - | (Read_stream, Read_exclusive_acquire) -> GT - | (Read_stream, Read_stream) -> EQ -end -let inline {ocaml} read_kindCompare = defaultCompare - -let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT -let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT -let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT -let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT - -let inline {ocaml} read_kindLess = defaultLess -let inline {ocaml} read_kindLessEq = defaultLessEq -let inline {ocaml} read_kindGreater = defaultGreater -let inline {ocaml} read_kindGreaterEq = defaultGreaterEq - -instance (Ord read_kind) - let compare = read_kindCompare - let (<) = read_kindLess - let (<=) = read_kindLessEq - let (>) = read_kindGreater - let (>=) = read_kindGreaterEq -end - -let ~{ocaml} write_kindCompare wk1 wk2 = - match (wk1, wk2) with - | (Write_plain, Write_plain) -> EQ - | (Write_plain, Write_conditional) -> LT - | (Write_plain, Write_release) -> LT - | (Write_plain, Write_exclusive) -> LT - | (Write_plain, Write_exclusive_release) -> LT - - | (Write_conditional, Write_plain) -> GT - | (Write_conditional, Write_conditional) -> EQ - | (Write_conditional, Write_release) -> LT - | (Write_conditional, Write_exclusive) -> LT - | (Write_conditional, Write_exclusive_release) -> LT - - | (Write_release, Write_plain) -> GT - | (Write_release, Write_conditional) -> GT - | (Write_release, Write_release) -> EQ - | (Write_release, Write_exclusive) -> LT - | (Write_release, Write_exclusive_release) -> LT - - | (Write_exclusive, Write_plain) -> GT - | (Write_exclusive, Write_conditional) -> GT - | (Write_exclusive, Write_release) -> GT - | (Write_exclusive, Write_exclusive) -> EQ - | (Write_exclusive, Write_exclusive_release) -> LT - - | (Write_exclusive_release, Write_plain) -> GT - | (Write_exclusive_release, Write_conditional) -> GT - | (Write_exclusive_release, Write_release) -> GT - | (Write_exclusive_release, Write_exclusive) -> GT - | (Write_exclusive_release, Write_exclusive_release) -> EQ -end -let inline {ocaml} write_kindCompare = defaultCompare - -let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT -let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT -let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT -let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT - -let inline {ocaml} write_kindLess = defaultLess -let inline {ocaml} write_kindLessEq = defaultLessEq -let inline {ocaml} write_kindGreater = defaultGreater -let inline {ocaml} write_kindGreaterEq = defaultGreaterEq - -instance (Ord write_kind) - let compare = write_kindCompare - let (<) = write_kindLess - let (<=) = write_kindLessEq - let (>) = write_kindGreater - let (>=) = write_kindGreaterEq -end - -(* Barrier comparison that uses less memory in Isabelle/HOL *) -let ~{ocaml} barrier_number = function - | Barrier_Sync -> (0 : natural) - | Barrier_LwSync -> 1 - | Barrier_Eieio -> 2 - | Barrier_Isync -> 3 - | Barrier_DMB -> 4 - | Barrier_DMB_ST -> 5 - | Barrier_DMB_LD -> 6 - | Barrier_DSB -> 7 - | Barrier_DSB_ST -> 8 - | Barrier_DSB_LD -> 9 - | Barrier_ISB -> 10 - | Barrier_TM_COMMIT -> 11 - | Barrier_MIPS_SYNC -> 12 - | Barrier_RISCV_rw_rw -> 13 - | Barrier_RISCV_r_rw -> 14 - | Barrier_RISCV_r_r -> 15 - | Barrier_RISCV_rw_w -> 16 - | Barrier_RISCV_w_w -> 17 - | Barrier_RISCV_i -> 18 - | Barrier_x86_MFENCE -> 19 - end - -let ~{ocaml} barrier_kindCompare bk1 bk2 = - let n1 = barrier_number bk1 in - let n2 = barrier_number bk2 in - if n1 < n2 then LT - else if n1 = n2 then EQ - else GT -let inline {ocaml} barrier_kindCompare = defaultCompare - -(*let ~{ocaml} barrier_kindCompare bk1 bk2 = - match (bk1, bk2) with - | (Barrier_Sync, Barrier_Sync) -> EQ - | (Barrier_Sync, _) -> LT - | (_, Barrier_Sync) -> GT - - | (Barrier_LwSync, Barrier_LwSync) -> EQ - | (Barrier_LwSync, _) -> LT - | (_, Barrier_LwSync) -> GT - - | (Barrier_Eieio, Barrier_Eieio) -> EQ - | (Barrier_Eieio, _) -> LT - | (_, Barrier_Eieio) -> GT - - | (Barrier_Isync, Barrier_Isync) -> EQ - | (Barrier_Isync, _) -> LT - | (_, Barrier_Isync) -> GT - - | (Barrier_DMB, Barrier_DMB) -> EQ - | (Barrier_DMB, _) -> LT - | (_, Barrier_DMB) -> GT - - | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ - | (Barrier_DMB_ST, _) -> LT - | (_, Barrier_DMB_ST) -> GT - - | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ - | (Barrier_DMB_LD, _) -> LT - | (_, Barrier_DMB_LD) -> GT - - | (Barrier_DSB, Barrier_DSB) -> EQ - | (Barrier_DSB, _) -> LT - | (_, Barrier_DSB) -> GT - - | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ - | (Barrier_DSB_ST, _) -> LT - | (_, Barrier_DSB_ST) -> GT - - | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ - | (Barrier_DSB_LD, _) -> LT - | (_, Barrier_DSB_LD) -> GT - - | (Barrier_ISB, Barrier_ISB) -> EQ - | (Barrier_ISB, _) -> LT - | (_, Barrier_ISB) -> GT - - | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ - | (Barrier_TM_COMMIT, _) -> LT - | (_, Barrier_TM_COMMIT) -> GT - - | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ - (* | (Barrier_MIPS_SYNC, _) -> LT - | (_, Barrier_MIPS_SYNC) -> GT *) - - end*) - -let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT -let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT -let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT -let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT - -let inline {ocaml} barrier_kindLess = defaultLess -let inline {ocaml} barrier_kindLessEq = defaultLessEq -let inline {ocaml} barrier_kindGreater = defaultGreater -let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq - -instance (Ord barrier_kind) - let compare = barrier_kindCompare - let (<) = barrier_kindLess - let (<=) = barrier_kindLessEq - let (>) = barrier_kindGreater - let (>=) = barrier_kindGreaterEq -end +(* read_kind, write_kind, barrier_kind, trans_kind and instruction_kind have + been moved to sail_instr_kinds.lem. This removes the dependency of the + shallow embedding on the rest of sail_impl_base.lem, and helps avoid name + clashes between the different monad types. *) type event = | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail_instr_kinds.lem new file mode 100644 index 00000000..89ff67b2 --- /dev/null +++ b/src/lem_interp/sail_instr_kinds.lem @@ -0,0 +1,436 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +open import Pervasives_extra + +(* Data structures for building up instructions *) + +(* careful: changes in the read/write/barrier kinds have to be + reflected in deep_shallow_convert *) +type read_kind = + (* common reads *) + | Read_plain + (* Power reads *) + | Read_reserve + (* AArch64 reads *) + | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream + (* RISC-V reads *) + | Read_RISCV_acquire | Read_RISCV_strong_acquire + | Read_RISCV_reserved | Read_RISCV_reserved_acquire + | Read_RISCV_reserved_strong_acquire + (* x86 reads *) + | Read_X86_locked (* the read part of a lock'd instruction (rmw) *) + +instance (Show read_kind) + let show = function + | Read_plain -> "Read_plain" + | Read_reserve -> "Read_reserve" + | Read_acquire -> "Read_acquire" + | Read_exclusive -> "Read_exclusive" + | Read_exclusive_acquire -> "Read_exclusive_acquire" + | Read_stream -> "Read_stream" + | Read_RISCV_acquire -> "Read_RISCV_acquire" + | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire" + | Read_RISCV_reserved -> "Read_RISCV_reserved" + | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" + | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire" + | Read_X86_locked -> "Read_X86_locked" + end +end + +type write_kind = + (* common writes *) + | Write_plain + (* Power writes *) + | Write_conditional + (* AArch64 writes *) + | Write_release | Write_exclusive | Write_exclusive_release + (* RISC-V *) + | Write_RISCV_release | Write_RISCV_strong_release + | Write_RISCV_conditional | Write_RISCV_conditional_release + | Write_RISCV_conditional_strong_release + (* x86 writes *) + | Write_X86_locked (* the write part of a lock'd instruction (rmw) *) + +instance (Show write_kind) + let show = function + | Write_plain -> "Write_plain" + | Write_conditional -> "Write_conditional" + | Write_release -> "Write_release" + | Write_exclusive -> "Write_exclusive" + | Write_exclusive_release -> "Write_exclusive_release" + | Write_RISCV_release -> "Write_RISCV_release" + | Write_RISCV_strong_release -> "Write_RISCV_strong_release" + | Write_RISCV_conditional -> "Write_RISCV_conditional" + | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" + | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release" + | Write_X86_locked -> "Write_X86_locked" + end +end + +type barrier_kind = + (* Power barriers *) + Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + (* AArch64 barriers *) + | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB + | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB + | Barrier_TM_COMMIT + (* MIPS barriers *) + | Barrier_MIPS_SYNC + (* RISC-V barriers *) + | Barrier_RISCV_rw_rw + | Barrier_RISCV_r_rw + | Barrier_RISCV_r_r + | Barrier_RISCV_rw_w + | Barrier_RISCV_w_w + | Barrier_RISCV_i + (* X86 *) + | Barrier_x86_MFENCE + + +instance (Show barrier_kind) + let show = function + | Barrier_Sync -> "Barrier_Sync" + | Barrier_LwSync -> "Barrier_LwSync" + | Barrier_Eieio -> "Barrier_Eieio" + | Barrier_Isync -> "Barrier_Isync" + | Barrier_DMB -> "Barrier_DMB" + | Barrier_DMB_ST -> "Barrier_DMB_ST" + | Barrier_DMB_LD -> "Barrier_DMB_LD" + | Barrier_DSB -> "Barrier_DSB" + | Barrier_DSB_ST -> "Barrier_DSB_ST" + | Barrier_DSB_LD -> "Barrier_DSB_LD" + | Barrier_ISB -> "Barrier_ISB" + | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" + | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" + | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" + | Barrier_RISCV_i -> "Barrier_RISCV_i" + | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" + end +end + +type trans_kind = + (* AArch64 *) + | Transaction_start | Transaction_commit | Transaction_abort + +instance (Show trans_kind) + let show = function + | Transaction_start -> "Transaction_start" + | Transaction_commit -> "Transaction_commit" + | Transaction_abort -> "Transaction_abort" + end +end + +type instruction_kind = + | IK_barrier of barrier_kind + | IK_mem_read of read_kind + | IK_mem_write of write_kind + | IK_mem_rmw of (read_kind * write_kind) + | IK_cond_branch + (* unconditional branches are not distinguished in the instruction_kind; + they just have particular nias (and will be IK_simple *) + (* | IK_uncond_branch *) + | IK_trans of trans_kind + | IK_simple + + +instance (Show instruction_kind) + let show = function + | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind) + | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) + | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) + | IK_cond_branch -> "IK_cond_branch" + | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) + | IK_simple -> "IK_simple" + end +end + + + +let ~{ocaml} read_kindCompare rk1 rk2 = + match (rk1, rk2) with + | (Read_plain, Read_plain) -> EQ + | (Read_plain, Read_reserve) -> LT + | (Read_plain, Read_acquire) -> LT + | (Read_plain, Read_exclusive) -> LT + | (Read_plain, Read_exclusive_acquire) -> LT + | (Read_plain, Read_stream) -> LT + + | (Read_reserve, Read_plain) -> GT + | (Read_reserve, Read_reserve) -> EQ + | (Read_reserve, Read_acquire) -> LT + | (Read_reserve, Read_exclusive) -> LT + | (Read_reserve, Read_exclusive_acquire) -> LT + | (Read_reserve, Read_stream) -> LT + + | (Read_acquire, Read_plain) -> GT + | (Read_acquire, Read_reserve) -> GT + | (Read_acquire, Read_acquire) -> EQ + | (Read_acquire, Read_exclusive) -> LT + | (Read_acquire, Read_exclusive_acquire) -> LT + | (Read_acquire, Read_stream) -> LT + + | (Read_exclusive, Read_plain) -> GT + | (Read_exclusive, Read_reserve) -> GT + | (Read_exclusive, Read_acquire) -> GT + | (Read_exclusive, Read_exclusive) -> EQ + | (Read_exclusive, Read_exclusive_acquire) -> LT + | (Read_exclusive, Read_stream) -> LT + + | (Read_exclusive_acquire, Read_plain) -> GT + | (Read_exclusive_acquire, Read_reserve) -> GT + | (Read_exclusive_acquire, Read_acquire) -> GT + | (Read_exclusive_acquire, Read_exclusive) -> GT + | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ + | (Read_exclusive_acquire, Read_stream) -> GT + + | (Read_stream, Read_plain) -> GT + | (Read_stream, Read_reserve) -> GT + | (Read_stream, Read_acquire) -> GT + | (Read_stream, Read_exclusive) -> GT + | (Read_stream, Read_exclusive_acquire) -> GT + | (Read_stream, Read_stream) -> EQ +end +let inline {ocaml} read_kindCompare = defaultCompare + +let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT +let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT +let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT +let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT + +let inline {ocaml} read_kindLess = defaultLess +let inline {ocaml} read_kindLessEq = defaultLessEq +let inline {ocaml} read_kindGreater = defaultGreater +let inline {ocaml} read_kindGreaterEq = defaultGreaterEq + +instance (Ord read_kind) + let compare = read_kindCompare + let (<) = read_kindLess + let (<=) = read_kindLessEq + let (>) = read_kindGreater + let (>=) = read_kindGreaterEq +end + +let read_is_exclusive = function + | Read_plain -> false + | Read_reserve -> true + | Read_acquire -> false + | Read_exclusive -> true + | Read_exclusive_acquire -> true + | Read_stream -> false + | Read_RISCV_acquire -> false + | Read_RISCV_strong_acquire -> false + | Read_RISCV_reserved -> true + | Read_RISCV_reserved_acquire -> true + | Read_RISCV_reserved_strong_acquire -> true + | Read_X86_locked -> true +end + +let ~{ocaml} write_kindCompare wk1 wk2 = + match (wk1, wk2) with + | (Write_plain, Write_plain) -> EQ + | (Write_plain, Write_conditional) -> LT + | (Write_plain, Write_release) -> LT + | (Write_plain, Write_exclusive) -> LT + | (Write_plain, Write_exclusive_release) -> LT + + | (Write_conditional, Write_plain) -> GT + | (Write_conditional, Write_conditional) -> EQ + | (Write_conditional, Write_release) -> LT + | (Write_conditional, Write_exclusive) -> LT + | (Write_conditional, Write_exclusive_release) -> LT + + | (Write_release, Write_plain) -> GT + | (Write_release, Write_conditional) -> GT + | (Write_release, Write_release) -> EQ + | (Write_release, Write_exclusive) -> LT + | (Write_release, Write_exclusive_release) -> LT + + | (Write_exclusive, Write_plain) -> GT + | (Write_exclusive, Write_conditional) -> GT + | (Write_exclusive, Write_release) -> GT + | (Write_exclusive, Write_exclusive) -> EQ + | (Write_exclusive, Write_exclusive_release) -> LT + + | (Write_exclusive_release, Write_plain) -> GT + | (Write_exclusive_release, Write_conditional) -> GT + | (Write_exclusive_release, Write_release) -> GT + | (Write_exclusive_release, Write_exclusive) -> GT + | (Write_exclusive_release, Write_exclusive_release) -> EQ +end +let inline {ocaml} write_kindCompare = defaultCompare + +let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT +let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT +let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT +let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT + +let inline {ocaml} write_kindLess = defaultLess +let inline {ocaml} write_kindLessEq = defaultLessEq +let inline {ocaml} write_kindGreater = defaultGreater +let inline {ocaml} write_kindGreaterEq = defaultGreaterEq + +instance (Ord write_kind) + let compare = write_kindCompare + let (<) = write_kindLess + let (<=) = write_kindLessEq + let (>) = write_kindGreater + let (>=) = write_kindGreaterEq +end + +(* Barrier comparison that uses less memory in Isabelle/HOL *) +let ~{ocaml} barrier_number = function + | Barrier_Sync -> (0 : natural) + | Barrier_LwSync -> 1 + | Barrier_Eieio -> 2 + | Barrier_Isync -> 3 + | Barrier_DMB -> 4 + | Barrier_DMB_ST -> 5 + | Barrier_DMB_LD -> 6 + | Barrier_DSB -> 7 + | Barrier_DSB_ST -> 8 + | Barrier_DSB_LD -> 9 + | Barrier_ISB -> 10 + | Barrier_TM_COMMIT -> 11 + | Barrier_MIPS_SYNC -> 12 + | Barrier_RISCV_rw_rw -> 13 + | Barrier_RISCV_r_rw -> 14 + | Barrier_RISCV_r_r -> 15 + | Barrier_RISCV_rw_w -> 16 + | Barrier_RISCV_w_w -> 17 + | Barrier_RISCV_i -> 18 + | Barrier_x86_MFENCE -> 19 + end + +let ~{ocaml} barrier_kindCompare bk1 bk2 = + let n1 = barrier_number bk1 in + let n2 = barrier_number bk2 in + if n1 < n2 then LT + else if n1 = n2 then EQ + else GT +let inline {ocaml} barrier_kindCompare = defaultCompare + +(*let ~{ocaml} barrier_kindCompare bk1 bk2 = + match (bk1, bk2) with + | (Barrier_Sync, Barrier_Sync) -> EQ + | (Barrier_Sync, _) -> LT + | (_, Barrier_Sync) -> GT + + | (Barrier_LwSync, Barrier_LwSync) -> EQ + | (Barrier_LwSync, _) -> LT + | (_, Barrier_LwSync) -> GT + + | (Barrier_Eieio, Barrier_Eieio) -> EQ + | (Barrier_Eieio, _) -> LT + | (_, Barrier_Eieio) -> GT + + | (Barrier_Isync, Barrier_Isync) -> EQ + | (Barrier_Isync, _) -> LT + | (_, Barrier_Isync) -> GT + + | (Barrier_DMB, Barrier_DMB) -> EQ + | (Barrier_DMB, _) -> LT + | (_, Barrier_DMB) -> GT + + | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ + | (Barrier_DMB_ST, _) -> LT + | (_, Barrier_DMB_ST) -> GT + + | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ + | (Barrier_DMB_LD, _) -> LT + | (_, Barrier_DMB_LD) -> GT + + | (Barrier_DSB, Barrier_DSB) -> EQ + | (Barrier_DSB, _) -> LT + | (_, Barrier_DSB) -> GT + + | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ + | (Barrier_DSB_ST, _) -> LT + | (_, Barrier_DSB_ST) -> GT + + | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ + | (Barrier_DSB_LD, _) -> LT + | (_, Barrier_DSB_LD) -> GT + + | (Barrier_ISB, Barrier_ISB) -> EQ + | (Barrier_ISB, _) -> LT + | (_, Barrier_ISB) -> GT + + | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ + | (Barrier_TM_COMMIT, _) -> LT + | (_, Barrier_TM_COMMIT) -> GT + + | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ + (* | (Barrier_MIPS_SYNC, _) -> LT + | (_, Barrier_MIPS_SYNC) -> GT *) + + end*) + +let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT +let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT +let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT +let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT + +let inline {ocaml} barrier_kindLess = defaultLess +let inline {ocaml} barrier_kindLessEq = defaultLessEq +let inline {ocaml} barrier_kindGreater = defaultGreater +let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq + +instance (Ord barrier_kind) + let compare = barrier_kindCompare + let (<) = barrier_kindLess + let (<=) = barrier_kindLessEq + let (>) = barrier_kindGreater + let (>=) = barrier_kindGreaterEq +end diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 350b5388..88ad8065 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -217,7 +217,7 @@ let rec lem_nexps_of_typ (Typ_aux (t,_)) = NexpSet.singleton (orig_nexp m) else trec elem_typ | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> - if !opt_sequential then trec etyp else NexpSet.empty + trec etyp | Typ_app(Id_aux (Id "range", _),_) | Typ_app(Id_aux (Id "implicit", _),_) | Typ_app(Id_aux (Id "atom", _), _) -> NexpSet.empty @@ -274,12 +274,7 @@ let doc_typ_lem, doc_atomic_typ_lem = | _ -> string "list" ^^ space ^^ typ elem_typ in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> - (* TODO: Better distinguish register names and contents? *) - (* fn_typ regtypes atyp_needed etyp *) - let tpp = - if !opt_sequential - then string "register_ref regstate " ^^ typ etyp - else string "register" in + let tpp = string "register_ref regstate register_value " ^^ typ etyp in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") @@ -912,7 +907,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with mk_typ (Typ_app (id, targs)) | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in let fs_doc = group (separate_map (break 1) f_pp fs) in - let doc_field (ftyp, fid) = + (* let doc_field (ftyp, fid) = let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (Typ_arg_typ rectyp); @@ -942,12 +937,12 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with doc_op equals (string "field_start") (string (Big_int.to_string start)); semi_sp; doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp; doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; - doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in + doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *) doc_op equals (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq]) - ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^ - if !opt_sequential && string_of_id id = "regstate" then empty - else separate_map hardline doc_field fs + ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline + (* if !opt_sequential && string_of_id id = "regstate" then empty + else separate_map hardline doc_field fs *) | TD_variant(id,nm,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty @@ -1284,8 +1279,8 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = match reg with - | DEC_reg(typ,id) -> - if !opt_sequential then empty + | DEC_reg(typ,id) -> empty + (* if !opt_sequential then empty else let env = env_of_annot annot in let rt = Env.base_typ_of env typ in @@ -1303,7 +1298,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = string "[]"])) ^/^ hardline else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) - else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) + else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) *) | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty @@ -1359,121 +1354,53 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = in separate_map hardline doc_field fields -let rec doc_def_lem regtypes def = +let rec doc_def_lem def = (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with - | DEF_spec v_spec -> (empty,doc_spec_lem v_spec) - | DEF_fixity _ -> (empty,empty) - | DEF_overload _ -> (empty,empty) - | DEF_type t_def -> (group (doc_typdef_lem t_def) ^/^ hardline,empty) - | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty) - - | DEF_default df -> (empty,empty) - | DEF_fundef fdef -> - let doc_fdef = group (doc_fundef_lem fdef) ^/^ hardline in - if is_field_accessor regtypes fdef then (doc_fdef, empty) else (empty, doc_fdef) - | DEF_internal_mutrec fundefs -> - (empty, doc_mutrec_lem fundefs ^/^ hardline) - | DEF_val lbind -> (empty,group (doc_let_lem empty_ctxt lbind) ^/^ hardline) + | DEF_spec v_spec -> doc_spec_lem v_spec + | DEF_fixity _ -> empty + | DEF_overload _ -> empty + | DEF_type t_def -> group (doc_typdef_lem t_def) ^/^ hardline + | DEF_reg_dec dec -> group (doc_dec_lem dec) + + | DEF_default df -> empty + | DEF_fundef fdef -> group (doc_fundef_lem fdef) ^/^ hardline + | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline + | DEF_val (LB_aux (LB_val (pat, _), _) as lbind) -> + group (doc_let_lem empty_ctxt lbind) ^/^ hardline | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" - | DEF_kind _ -> (empty,empty) - - | DEF_comm (DC_comm s) -> (empty,comment (string s)) - | DEF_comm (DC_comm_struct d) -> - let (typdefs,vdefs) = doc_def_lem regtypes d in - (empty,comment (typdefs ^^ hardline ^^ vdefs)) - - -let doc_defs_lem (Defs defs) = - let regtypes = [] in - let field_refs = separate_map hardline doc_regtype_fields regtypes in - let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in - (separate empty typdefs ^^ field_refs, separate empty valdefs) - -let find_registers (Defs defs) = - List.fold_left - (fun acc def -> - match def with - | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), annot)) -> - let env = match annot with - | (_, Some (env, _, _)) -> env - | _ -> Env.empty in - (typ, id, env) :: acc - | _ -> acc - ) [] defs - -let find_exc_typ (Defs defs) = + | DEF_kind _ -> empty + + | DEF_comm (DC_comm s) -> comment (string s) + | DEF_comm (DC_comm_struct d) -> comment (doc_def_lem d) + + +let find_exc_typ defs = let is_exc_typ_def = function | DEF_type td -> string_of_id (id_of_type_def td) = "exception" | _ -> false in if List.exists is_exc_typ_def defs then "exception" else "unit" -let doc_regstate_lem registers = - let l = Parse_ast.Unknown in - let annot = (l, None) in - let regstate = match registers with - | [] -> - TD_abbrev ( - Id_aux (Id "regstate", l), - Name_sect_aux (Name_sect_none, l), - TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_tq [], l), unit_typ), l)) - | _ -> - TD_record ( - Id_aux (Id "regstate", l), - Name_sect_aux (Name_sect_none, l), - TypQ_aux (TypQ_tq [], l), - List.map (fun (typ, id, env) -> (typ, id)) registers, - false) +let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line = + (* let regtypes = find_regtypes d in *) + let state_ids = + State.generate_regstate_defs !opt_mwords defs + |> Initial_check.val_spec_ids in - let initregstate = - if !Initial_check.opt_undefined_gen then - let exp = match registers with - | [] -> E_aux (E_lit (mk_lit L_unit), (l, Some (Env.empty, unit_typ, no_effect))) - | _ -> - let initreg (typ, id, env) = - let annot typ = Some (env, typ, no_effect) in - let initval = undefined_of_typ !opt_mwords l annot typ in - FE_aux (FE_Fexp (id, initval), (l, annot typ)) in - E_aux ( - E_record (FES_aux (FES_Fexps (List.map initreg registers, false), annot)), - (l, Some (Env.empty, mk_id_typ (mk_id "regstate"), no_effect))) - in - doc_op equals (string "let initial_regstate") (doc_exp_lem empty_ctxt false exp) - else empty + let is_state_def = function + | DEF_spec vs -> IdSet.mem (id_of_val_spec vs) state_ids + | DEF_fundef fd -> IdSet.mem (id_of_fundef fd) state_ids + | _ -> false in - doc_typdef_lem (TD_aux (regstate, annot)), - initregstate - -let doc_register_refs_lem registers = - let doc_register_ref (typ, id, env) = - let idd = doc_id_lem id in - let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in - let base_typ = Env.base_typ_of env typ in - let (start, is_inc) = - try - let (start, _, ord, _) = vector_typ_args_of base_typ in - match nexp_simp start with - | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord) - | _ -> - raise (Reporting_basic.err_unreachable Parse_ast.Unknown - ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) - with - | _ -> (Big_int.zero, true) in - concat [string "let "; idd; string " = <|"; hardline; - string " reg_name = \""; idd; string "\";"; hardline; - string " reg_start = "; string (Big_int.to_string start); string ";"; hardline; - string " reg_is_inc = "; string (if is_inc then "true" else "false"); string ";"; hardline; - string " read_from = (fun s -> s."; field; string ");"; hardline; - string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in - separate_map hardline doc_register_ref registers - -let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = - (* let regtypes = find_regtypes d in *) - let (typdefs,valdefs) = doc_defs_lem d in - let regstate_def, initregstate_def = doc_regstate_lem (find_registers d) in - let register_refs = doc_register_refs_lem (find_registers d) in - let exc_typ = find_exc_typ d in + let is_typ_def = function + | DEF_type _ -> true + | _ -> false + in + let exc_typ = find_exc_typ defs in + let typdefs, defs = List.partition is_typ_def defs in + let statedefs, defs = List.partition is_state_def defs in + let register_refs = State.register_refs_lem prefix_recordtype !opt_mwords (State.find_registers defs) in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; @@ -1491,20 +1418,20 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = string "module SIA = Interp_ast"; hardline; hardline] else empty; - typdefs; hardline; + separate empty (List.map doc_def_lem typdefs); hardline; hardline; + separate empty (List.map doc_def_lem statedefs); hardline; + hardline; + register_refs; hardline; if !opt_sequential then - concat [regstate_def; hardline; - hardline; + concat [ 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_monad.MR 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = Prompt_monad.M 'a " ^ exc_typ); hardline + string ("type MR 'a 'r = monadR register_value 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = monad register_value 'a " ^ exc_typ); hardline ] ]); (print defs_file) @@ -1513,6 +1440,5 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) defs_modules;hardline; hardline; - valdefs; - hardline; - initregstate_def]); + separate empty (List.map doc_def_lem defs); + hardline]); diff --git a/src/process_file.ml b/src/process_file.ml index 1da893c3..8e309901 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -239,7 +239,7 @@ let output_lem filename libs defs = let libs = List.map (fun lib -> lib ^ seq_suffix) libs in let base_imports = [ "Pervasives_extra"; - "Sail_impl_base"; + "Sail_instr_kinds"; "Sail_values"; operators_module ] @ monad_modules diff --git a/src/sail.ml b/src/sail.ml index 2aae2472..35a7279b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -267,8 +267,11 @@ let main() = C_backend.compile_ast (C_backend.initial_ctx type_envs) ast_c else ()); (if !(opt_print_lem) - then let ast_lem = rewrite_ast_lem ast in - output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] + then + let mwords = !Pretty_print_lem.opt_mwords in + let type_envs, ast_lem = State.add_regstate_defs mwords type_envs ast in + let ast_lem = rewrite_ast_lem ast_lem in + output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] else ()); end diff --git a/src/state.ml b/src/state.ml new file mode 100644 index 00000000..83af7d2f --- /dev/null +++ b/src/state.ml @@ -0,0 +1,279 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +module Big_int = Nat_big_num + +open Initial_check +open Type_check +open Ast +open Ast_util +open PPrint +open Pretty_print_common +open Pretty_print_sail + +let defs_of_string = ast_of_def_string Ast_util.inc_ord + +let find_registers defs = + List.fold_left + (fun acc def -> + match def with + | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), annot)) -> + let env = match annot with + | (_, Some (env, _, _)) -> env + | _ -> Env.empty + in + (Env.expand_synonyms env typ, id) :: acc + | _ -> acc + ) [] defs + +let generate_regstate = function + | [] -> ["type regstate = unit"] + | registers -> + let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in + let initreg (_, id) = Printf.sprintf "%s = undefined" (string_of_id id) in + let regstate = + "struct regstate = { " ^ + (String.concat ", " (List.map reg registers)) ^ + " }" + in + let initstate = + "let initial_regstate : regstate = struct { " ^ + (String.concat ", " (List.map initreg registers)) ^ + " }" + in + regstate :: (if !Initial_check.opt_undefined_gen then [initstate] else []) + +let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with + | Typ_id id -> id + | Typ_app (id, args) -> + let name_arg (Typ_arg_aux (targ, _)) = match targ with + | Typ_arg_typ targ -> string_of_id (regval_constr_id mwords targ) + | Typ_arg_nexp nexp when is_nexp_constant (nexp_simp nexp) -> + string_of_nexp (nexp_simp nexp) + | Typ_arg_order (Ord_aux (Ord_inc, _)) -> "inc" + | Typ_arg_order (Ord_aux (Ord_dec, _)) -> "dec" + | _ -> + raise (Reporting_basic.err_typ l "Unsupported register type") + in + let builtins = IdSet.of_list (List.map mk_id ["vector"; "list"; "option"]) in + if IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) then id else + append_id id (String.concat "_" ("" :: List.map name_arg args)) + | _ -> raise (Reporting_basic.err_typ l "Unsupported register type") + +let register_base_types mwords typs = + let rec add_base_typs typs (Typ_aux (t, _) as typ) = + let builtins = IdSet.of_list (List.map mk_id ["vector"; "list"; "option"]) in + match t with + | Typ_app (id, args) + when IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) -> + let add_typ_arg base_typs (Typ_arg_aux (targ, _)) = + match targ with + | Typ_arg_typ typ -> add_base_typs typs typ + | _ -> typs + in + List.fold_left add_typ_arg typs args + | _ -> Bindings.add (regval_constr_id mwords typ) typ typs + in + List.fold_left add_base_typs Bindings.empty typs + +let generate_regval_typ typs = + let constr (constr_id, typ) = + Printf.sprintf "Regval_%s : %s" (string_of_id constr_id) (to_string (doc_typ typ)) in + let builtins = + "Regval_vector : (int, bool, list(register_value)), " ^ + "Regval_list : list(register_value), " ^ + "Regval_option : option(register_value)" + in + ["union register_value = { " ^ + (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^ + " }"] + +let add_regval_conv id typ defs = + let id = string_of_id id in + let is_defined name = IdSet.mem (mk_id name) (ids_of_defs defs) in + let typ_str = to_string (doc_typ typ) in + (* Create a function that converts from regval to the target type. *) + let from_name = id ^ "_of_regval" in + let from_val = Printf.sprintf "val %s : register_value -> option(%s)" from_name typ_str in + let from_function = String.concat "\n" [ + Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id; + Printf.sprintf "and %s _ = None" from_name + ] in + let from_defs = if is_defined from_name then [] else [from_val; from_function] in + (* Create a function that converts from target type to regval. *) + let to_name = "regval_of_" ^ id in + let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in + let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in + let to_defs = if is_defined to_name then [] else [to_val; to_function] in + let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in + append_ast defs cdefs + +let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with + | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) -> + let _, size, ord, etyp = vector_typ_args_of typ in + let size = string_of_nexp (nexp_simp size) in + let is_inc = if is_order_inc ord then "true" else "false" in + let etyp_of, of_etyp = regval_convs_lem mwords etyp in + "(fun v -> vector_of_regval " ^ etyp_of ^ " v)", + "(fun v -> regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)" + | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + when string_of_id id = "list" -> + let etyp_of, of_etyp = regval_convs_lem mwords etyp in + "(fun v -> list_of_regval " ^ etyp_of ^ " v)", + "(fun v -> regval_of_list " ^ of_etyp ^ " v)" + | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + when string_of_id id = "option" -> + let etyp_of, of_etyp = regval_convs_lem mwords etyp in + "(fun v -> option_of_regval " ^ etyp_of ^ " v)", + "(fun v -> regval_of_option " ^ of_etyp ^ " v)" + | _ -> + let id = string_of_id (regval_constr_id mwords typ) in + "(fun v -> " ^ id ^ "_of_regval v)", "(fun v -> regval_of_" ^ id ^ " v)" + +let register_refs_lem prefix_recordtype mwords registers = + let generic_convs = + separate_map hardline string [ + "val vector_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (list 'a)"; + "let vector_of_regval of_regval = function"; + " | Regval_vector (_, _, v) -> just_list (List.map of_regval v)"; + " | _ -> Nothing"; + "end"; + ""; + "val regval_of_vector : forall 'a. ('a -> register_value) -> integer -> bool -> list 'a -> register_value"; + "let regval_of_vector regval_of size is_inc xs = Regval_vector (size, is_inc, List.map regval_of xs)"; + ""; + "val list_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (list 'a)"; + "let list_of_regval of_regval = function"; + " | Regval_list v -> just_list (List.map of_regval v)"; + " | _ -> Nothing"; + "end"; + ""; + "val regval_of_list : forall 'a. ('a -> register_value) -> list 'a -> register_value"; + "let regval_of_list regval_of xs = Regval_list (List.map regval_of xs)"; + ""; + "val option_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (maybe 'a)"; + "let option_of_regval of_regval = function"; + " | Regval_option v -> Maybe.map of_regval v"; + " | _ -> Nothing"; + "end"; + ""; + "val regval_of_option : forall 'a. ('a -> register_value) -> maybe 'a -> register_value"; + "let regval_of_option regval_of v = Regval_option (Maybe.map regval_of v)"; + ""; + "" + ] + in + let register_ref (typ, id) = + let idd = string (string_of_id id) in + let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in + let is_inc = + if is_bitvector_typ typ then + let _, _, ord, _ = vector_typ_args_of typ in + if is_order_inc ord then "true" else "false" + else "true" + in + let of_regval, regval_of = regval_convs_lem mwords typ in + concat [string "let "; idd; string " = <|"; hardline; + string " name = \""; idd; string "\";"; hardline; + string " is_inc = "; string is_inc; string ";"; hardline; + string " read_from = (fun s -> s."; field; string ");"; hardline; + string " write_to = (fun s v -> (<| s with "; field; string " = v |>));"; hardline; + string " of_regval = "; string of_regval; string ";"; hardline; + string " regval_of = "; string regval_of; string " |>"; hardline] + in + let refs = separate_map hardline register_ref registers in + let get_set_reg (_, id) = + let idd = string_of_id id in + string (" if reg_name = \"" ^ idd ^ "\" then Just (" ^ idd ^ ".regval_of (" ^ idd ^ ".read_from s)) else"), + string (" if reg_name = \"" ^ idd ^ "\" then Maybe.map (" ^ idd ^ ".write_to s) (" ^ idd ^ ".of_regval v) else") + in + let getters_setters = + let getters, setters = List.split (List.map get_set_reg registers) in + string "val get_regval : string -> regstate -> maybe register_value" ^^ hardline ^^ + string "let get_regval reg_name s =" ^^ hardline ^^ + separate hardline getters ^^ hardline ^^ + string " Nothing" ^^ hardline ^^ hardline ^^ + string "val set_regval : string -> register_value -> regstate -> maybe regstate" ^^ hardline ^^ + string "let set_regval reg_name v s =" ^^ hardline ^^ + separate hardline setters ^^ hardline ^^ + string " Nothing" ^^ hardline ^^ hardline ^^ + string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline + in + separate hardline [generic_convs; refs; getters_setters] + +let generate_regstate_defs mwords defs = + let registers = find_registers defs in + let def_ids = ids_of_defs (Defs defs) in + let has_def name = IdSet.mem (mk_id name) def_ids in + let regtyps = register_base_types mwords (List.map fst registers) in + let option_typ = + if has_def "option" then [] else + ["union option ('a : Type) = {None, Some : 'a}"] + in + let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in + let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in + (* FIXME We currently don't want to generate undefined_type functions + for register state and values. For the Lem backend, this would require + taking the dependencies of those functions into account when partitioning + definitions into the different lem files, which we currently don't do. *) + let gen_undef = !Initial_check.opt_undefined_gen in + Initial_check.opt_undefined_gen := false; + let defs = + option_typ @ regval_typ @ regstate_typ + |> List.map defs_of_string + |> concat_ast + |> Bindings.fold add_regval_conv regtyps + in + Initial_check.opt_undefined_gen := gen_undef; + defs + +let add_regstate_defs mwords env (Defs defs) = + let reg_defs, env = check env (generate_regstate_defs mwords defs) in + env, append_ast (Defs defs) reg_defs |