diff options
| -rw-r--r-- | language/l2.ott | 4 | ||||
| -rw-r--r-- | lib/isabelle/Makefile | 4 | ||||
| -rw-r--r-- | lib/isabelle/Sail_values_lemmas.thy | 71 | ||||
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 25 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 161 | ||||
| -rw-r--r-- | riscv/prelude.sail | 4 | ||||
| -rw-r--r-- | riscv/riscv_extras.lem | 6 | ||||
| -rw-r--r-- | src/ast_util.ml | 4 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 25 | ||||
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 25 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 290 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 179 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 274 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 428 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 27 | ||||
| -rw-r--r-- | src/pretty_print_common.ml | 4 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 12 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 4 | ||||
| -rw-r--r-- | src/rewrites.ml | 33 |
19 files changed, 891 insertions, 689 deletions
diff --git a/language/l2.ott b/language/l2.ott index c34dedb5..a437f915 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -230,9 +230,7 @@ base_effect :: 'BE_' ::= | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} - | escape :: :: escape {{ com potential call of $[[exit]]$ }} - | lset :: :: lset {{ com local mutation; not user-writable }} - | lret :: :: lret {{ com local return; not user-writable }} + | escape :: :: escape {{ com potential exception }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 688dfa07..d6bcf9bb 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -23,10 +23,10 @@ Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy +Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy Prompt.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy +Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy Prompt.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy index 2114d991..df2fc808 100644 --- a/lib/isabelle/Sail_values_lemmas.thy +++ b/lib/isabelle/Sail_values_lemmas.thy @@ -2,6 +2,8 @@ theory Sail_values_lemmas imports Sail_values begin +lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) + termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) termination index_list @@ -21,32 +23,67 @@ lemma just_list_cases: | (Some) ys where "xs = map Some ys" and "y = Some ys" using assms by (cases y) auto -abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict instance_Sail_values_BitU_Sail_values_bitU_dict" -lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def -abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict" -lemmas BC_mword_def = instance_Sail_values_Bitvector_Machine_word_mword_dict_def +lemma bitops_bitU_of_bool[simp]: + "and_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<and> y)" + "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<or> y)" + "xor_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool ((x \<or> y) \<and> \<not>(x \<and> y))" + "not_bit (bitU_of_bool x) = bitU_of_bool (\<not>x)" + "not_bit \<circ> bitU_of_bool = bitU_of_bool \<circ> Not" + by (auto simp: bitU_of_bool_def not_bit_def) lemma image_bitU_of_bool_B0_B1: "bitU_of_bool ` bs \<subseteq> {B0, B1}" by (auto simp: bitU_of_bool_def split: if_splits) -lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU \<circ> bitU_of_bool = id" - by (intro ext) (auto simp: bool_of_bitU_def bitU_of_bool_def) +lemma bool_of_bitU_bitU_of_bool[simp]: + "bool_of_bitU \<circ> bitU_of_bool = Some" + "bool_of_bitU \<circ> (bitU_of_bool \<circ> f) = Some \<circ> f" + "bool_of_bitU (bitU_of_bool x) = Some x" + by (intro ext, auto simp: bool_of_bitU_def bitU_of_bool_def)+ + +abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict instance_Sail_values_BitU_Sail_values_bitU_dict" +lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def +abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict" +lemmas BC_mword_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_def + length_mword_def access_mword_def access_mword_inc_def access_mword_dec_def + (*update_mword_def update_mword_inc_def update_mword_dec_def*) + subrange_list_def subrange_list_inc_def subrange_list_dec_def + update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def + +lemma BC_mword_simps[simp]: + "unsigned_method BC_mword a = Some (uint a)" + "signed_method BC_mword a = Some (sint a)" + "length_method BC_mword (a :: ('a :: len) word) = int (LENGTH('a))" + by (auto simp: BC_mword_defs word_size) lemma nat_of_bits_aux_bl_to_bin_aux: - assumes "set bs \<subseteq> {B0, B1}" - shows "nat_of_bits_aux acc bs = nat (bl_to_bin_aux (map bool_of_bitU bs) (int acc))" - by (use assms in \<open>induction acc bs rule: nat_of_bits_aux.induct\<close>) - (auto simp: Bit_def bool_of_bitU_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux]) + "nat_of_bools_aux acc bs = nat (bl_to_bin_aux bs (int acc))" + by (induction acc bs rule: nat_of_bools_aux.induct) + (auto simp: Bit_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux] split: if_splits) -lemma nat_of_bits_bl_to_bin[simp]: "nat_of_bits (map bitU_of_bool bs) = nat (bl_to_bin bs)" - by (auto simp: nat_of_bits_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux image_bitU_of_bool_B0_B1) +lemma nat_of_bits_bl_to_bin[simp]: "nat_of_bools bs = nat (bl_to_bin bs)" + by (auto simp: nat_of_bools_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux) -lemma unsigned_bits_of_mword: - "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = unsigned_method BC_mword a" - by (auto simp: BC_bitU_list_def BC_mword_def unsigned_of_bits_def) +lemma unsigned_bits_of_mword[simp]: + "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" + by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) -lemma unsigned_bits_of_bitU_list: - "unsigned_method BC_bitU_list (bits_of_method BC_bitU_list a) = unsigned_method BC_bitU_list a" +lemma bits_of_bitU_list[simp]: + "bits_of_method BC_bitU_list v = v" + "of_bits_method BC_bitU_list v = Some v" by (auto simp: BC_bitU_list_def) +lemma access_list_dec_rev_nth: + assumes "0 \<le> i" and "nat i < size xs" + shows "access_list_dec xs i = rev xs ! (nat i)" + using assms + by (auto simp: access_list_dec_def access_list_inc_def length_list_def rev_nth + intro!: arg_cong2[where f = List.nth]) + +lemma access_bv_dec_mword[simp]: + fixes w :: "('a::len) word" + assumes "0 \<le> n" and "nat n < LENGTH('a)" + shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))" + using assms + by (auto simp: access_bv_dec_def access_list_def access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl word_size) + end diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index d8ab5db9..36fb987f 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -26,6 +26,8 @@ lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ( lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def) lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def) lemma liftState_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def) +lemma liftState_maybe_fail[simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x" + by (auto simp: maybe_fail_def maybe_failS_def split: option.splits) lemma liftState_try_catch[simp]: "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)" @@ -47,19 +49,26 @@ lemma liftState_try_catchR[simp]: "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)" by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong) -lemma liftState_read_mem_BC[simp]: +lemma liftState_read_mem_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" - using assms by (auto simp: read_mem_def read_memS_def read_mem_bytesS_def) -lemmas liftState_read_mem[simp] = - liftState_read_mem_BC[OF unsigned_bits_of_mword] liftState_read_mem_BC[OF unsigned_bits_of_bitU_list] + using assms + by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def split: option.splits) + +lemma liftState_read_mem[simp]: + "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz" + "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz" + by (auto simp: liftState_read_mem_BC) lemma liftState_write_mem_ea_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" - shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a sz" + shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)" using assms by (auto simp: write_mem_ea_def write_mem_eaS_def) -lemmas liftState_write_mem_ea[simp] = - liftState_write_mem_ea_BC[OF unsigned_bits_of_mword] liftState_write_mem_ea_BC[OF unsigned_bits_of_bitU_list] + +lemma liftState_write_mem_ea[simp]: + "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)" + "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)" + by (auto simp: liftState_write_mem_ea_BC) lemma liftState_write_mem_val: "liftState r (write_mem_val BC v) = write_mem_valS BC v" @@ -80,7 +89,7 @@ qed lemma liftState_write_reg_updateS: assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)" shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))" - using assms by (auto simp: write_reg_def bindS_readS updateS_def returnS_def) + using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS) lemma liftState_iter_aux[simp]: shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs" diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index 291157f5..e7286fcf 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -4,23 +4,15 @@ theory State_monad_lemmas Sail_values_lemmas begin -context +(*context notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp] -begin - -abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> {(Ex e, s')})" -abbreviation "bindS_app ms f \<equiv> \<Union>(bindS_aux f ` ms)" +begin*) lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" and f: "\<And>a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" shows "bindS m1 f1 s = bindS m2 f2 s" using assms unfolding bindS_def by (auto split: result.splits) -(* proof - - have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2" - using f by (auto split: result.splits) - then show ?thesis using m by (auto simp: bindS_def) -qed *) lemma bindS_cong[fundef_cong]: assumes m: "m1 = m2" @@ -29,21 +21,16 @@ lemma bindS_cong[fundef_cong]: using assms by (intro ext bindS_ext_cong; blast) lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x" - by (auto simp add: bindS_def) + by (auto simp add: bindS_def returnS_def) lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" - by (intro ext) (auto simp: bindS_def split: result.splits) -(* proof - - have "List.concat (map (bindS_aux returnS) ms) = ms" for ms :: "(('a, 'e) result \<times> 'regs sequential_state) list" - by (induction ms) (auto split: result.splits) - then show ?thesis unfolding bindS_def by blast -qed *) + by (intro ext) (auto simp: bindS_def returnS_def split: result.splits) lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" - by (auto simp: bindS_def) + by (auto simp: bindS_def readS_def returnS_def) lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" - by (auto simp: bindS_def) + by (auto simp: bindS_def updateS_def returnS_def) lemma result_cases: @@ -84,17 +71,6 @@ lemma monadS_eqI: shows "m = m'" using assms by (intro ext monadS_ext_eqI) -lemma - assumes "(Value a, s') \<in> bindS m f s" - obtains a' s'' where "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" - using assms by (auto simp: bindS_def split: result.splits) - -lemma - assumes "(Ex e, s') \<in> bindS m f s" - obtains (Left) "(Ex e, s') \<in> m s" - | (Right) a s'' where "(Value a, s'') \<in> m s" and "(Ex e, s') \<in> f a s''" - using assms by (auto simp: bindS_def split: result.splits) - lemma bindS_cases: assumes "(r, s') \<in> bindS m f s" obtains (Value) a a' s'' where "r = Value a" and "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" @@ -110,15 +86,9 @@ lemma bindS_intros: lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)" by (auto elim!: bindS_cases intro: bindS_intros monadS_eqI) -(*proof - - have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) = - List.concat (map (bindS_aux (\<lambda>x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs - by (induction xs) (auto split: result.splits) - then show ?thesis unfolding bindS_def by auto -qed*) - -lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def) -lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def) + +lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def failS_def) +lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def throwS_def) declare seqS_def[simp] lemma Value_bindS_elim: @@ -132,18 +102,10 @@ lemma Ex_bindS_elim: | (Right) s'' a' where "(Value a', s'') \<in> m s" and "(Ex e, s') \<in> f a' s''" using assms by (auto elim: bindS_cases) -abbreviation - "try_catchS_aux h r \<equiv> - (case r of - (Value a, s') => returnS a s' - | (Ex (Throw e), s') => h e s' - | (Ex (Failure msg), s') => {(Ex (Failure msg), s')})" -abbreviation "try_catchS_app ms h \<equiv> \<Union>(try_catchS_aux h ` ms)" - lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a" and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg" and try_catchS_throwS[simp]: "try_catchS (throwS e) h = h e" - by (auto simp: try_catchS_def) + by (auto simp: try_catchS_def returnS_def failS_def throwS_def) lemma try_catchS_cong[cong]: assumes "\<And>s. m1 s = m2 s" and "\<And>e s. h1 e s = h2 e s" @@ -155,13 +117,14 @@ lemma try_catchS_cases: obtains (Value) a where "r = Value a" and "(Value a, s') \<in> m s" | (Fail) msg where "r = Ex (Failure msg)" and "(Ex (Failure msg), s') \<in> m s" | (h) e s'' where "(Ex (Throw e), s'') \<in> m s" and "(r, s') \<in> h e s''" - using assms by (cases r rule: result_cases) (auto simp: try_catchS_def split: result.splits ex.splits) + using assms + by (cases r rule: result_cases) (auto simp: try_catchS_def returnS_def split: result.splits ex.splits) lemma try_catchS_intros: "\<And>m h s a s'. (Value a, s') \<in> m s \<Longrightarrow> (Value a, s') \<in> try_catchS m h s" "\<And>m h s msg s'. (Ex (Failure msg), s') \<in> m s \<Longrightarrow> (Ex (Failure msg), s') \<in> try_catchS m h s" "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s" - by (auto simp: try_catchS_def intro: bexI[rotated]) + by (auto simp: try_catchS_def returnS_def intro: bexI[rotated]) fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where "ignore_throw_aux (Value a, s') = {(Value a, s')}" @@ -169,42 +132,23 @@ fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) | "ignore_throw_aux (Ex (Failure msg), s') = {(Ex (Failure msg), s')}" definition "ignore_throw m s \<equiv> \<Union>(ignore_throw_aux ` m s)" -(*fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) list" where - "ignore_throw_aux r \<equiv> - (case r of - (Value a, s') => returnS a s' - | (Ex (Throw e), s') => h e s' - | (Ex (Failure msg), s') => {(Ex (Failure msg), s')})" -fun ignore_throw_app :: "(('a, 'e1) result \<times> 's) list \<Rightarrow> (('a, 'e2) result \<times> 's) list" where - "ignore_throw_app [] = []" -| "ignore_throw_app ((Value a, s) # ms) = (Value a, s) # ignore_throw_app ms" -| "ignore_throw_app ((Ex (Failure msg), s) # ms) = (Ex (Failure msg), s) # ignore_throw_app ms" -| "ignore_throw_app ((Ex (Throw e), s) # ms) = ignore_throw_app ms" -abbreviation ignore_throw :: "('r, 'a, 'e1) monadS \<Rightarrow> ('r, 'a, 'e2) monadS" where - "ignore_throw m \<equiv> \<lambda>s. ignore_throw_app (m s)" - -lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \<longleftrightarrow> False" - by (induction ms rule: ignore_throw_app.induct) auto - -lemma ignore_throw_app_append[simp]: - "ignore_throw_app (ms1 @ ms2) = ignore_throw_app ms1 @ ignore_throw_app ms2" - by (induction ms1 rule: ignore_throw_app.induct) auto - -lemma ignore_throw_app_bindS_app[simp]: - "ignore_throw_app (bindS_app ms f) = bindS_app (ignore_throw_app ms) (ignore_throw \<circ> f)" - by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits)*) - -lemma [simp]: +lemma ignore_throw_cong: + assumes "\<And>s. m1 s = m2 s" + shows "ignore_throw m1 = ignore_throw m2" + using assms by (auto simp: ignore_throw_def) + +lemma ignore_throw_aux_member_simps[simp]: "(Value a, s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Value a, s')" "(Ex (Throw e), s') \<in> ignore_throw_aux ms \<longleftrightarrow> False" "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')" by (cases ms rule: result_state_cases; auto)+ -(*lemma [simp]: "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" +lemma ignore_throw_member_simps[simp]: + "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" "(Ex (Throw e), s') \<in> ignore_throw m s \<longleftrightarrow> False" - "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')" - by (auto simp: ignore_throw_def)*) + "(Ex (Failure msg), s') \<in> ignore_throw m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m s" + by (auto simp: ignore_throw_def) lemma ignore_throw_cases: assumes no_throw: "ignore_throw m s = m s" @@ -232,43 +176,21 @@ proof also have "\<dots> = bindS m2 (\<lambda>a. try_catchS (f a) h) s" using m2 by (intro bindS_ext_cong) auto finally show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" . qed -(*proof - fix s - have 1: "try_catchS_app (bindS_app ms f) h = - bindS_app (ignore_throw_app ms) (\<lambda>a s'. try_catchS_app (f a s') h)" - if "ignore_throw_app ms = ms" for ms - using that by (induction ms rule: ignore_throw_app.induct) auto - then show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" - using m1 unfolding try_catchS_def bindS_def m2[symmetric] by blast -qed*) - -(*lemma no_throwI: - fixes m1 :: "('regs, 'a, 'e1) monadS" and m2 :: "('regs, 'a, 'e2) monadS" - assumes "\<And>a s'. (Value a, s') \<in> m1 s \<longleftrightarrow> (Value a, s') \<in> m2 s" - and "\<And>msg s'. (Ex (Failure msg), s') \<in> m1 s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m2 s" - and "\<And>e s'. (Ex (Throw e), s') \<notin> m1 s" - and "\<And>e s'. (Ex (Throw e), s') \<notin> m2 s" - shows "ignore_throw m1 s = m2 s" - using assms by (intro monadS_ext_eqI) (auto simp: ignore_throw_def)*) - -(*lemma no_throw_bindSI: - assumes "ignore_throw m1 s = m2 s" -and "\<And>a s'. (Value a, s') \<in> m2 s \<Longrightarrow> ignore_throw (f1 a) s' = f2 a s'" -shows "ignore_throw (bindS m1 f1) s = bindS m2 f2 s" - using assms unfolding ignore_throw_bindS apply (intro monadS_ext_eqI) apply auto apply (auto elim!: bindS_cases intro: bindS_intros) - defer thm bindS_intros - apply (intro bindS_intros(3)) apply auto - apply (intro bindS_intros(3)) apply auto - done - -lemma - "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" - unfolding read_mem_bytesS_def Let_def seqS_def - apply (intro no_throw_bindSI) - oops*) + +lemma no_throw_basic_builtins[simp]: + "ignore_throw (returnS a) = returnS a" + "\<And>f. ignore_throw (readS f) = readS f" + "\<And>f. ignore_throw (updateS f) = updateS f" + "ignore_throw (chooseS xs) = chooseS xs" + "ignore_throw (failS msg) = failS msg" + "ignore_throw (maybe_failS msg x) = maybe_failS msg x" + unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def + by (intro ext; auto split: option.splits)+ + +lemmas ignore_throw_option_case_distrib = + option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s] lemma no_throw_mem_builtins: - "\<And>a. ignore_throw (returnS a) = returnS a" "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" @@ -280,20 +202,21 @@ lemma no_throw_mem_builtins: unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def unfolding excl_resultS_def undefined_boolS_def - by (auto simp: ignore_throw_def bindS_def chooseS_def Let_def split: option.splits prod.splits) + by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong + simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def) lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s" by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong) lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s" - by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) + by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = write_regvalS r reg_name v s" - by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) + by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) -lemmas no_throw_builtins[simp, intro] = +lemmas no_throw_builtins[simp] = no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS -end +(* end *) end diff --git a/riscv/prelude.sail b/riscv/prelude.sail index b6c80ffb..f6532215 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -110,9 +110,9 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys) overload operator | = {or_bool, or_vec} -val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) -val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) +val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index 49499445..9d9ccf89 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -49,7 +49,7 @@ let get_slice_int len n lo = (* TODO: Is this the intended behaviour? *) let hi = lo + len - 1 in let bits = bits_of_int (hi + 1) n in - of_bits (get_bits false bits hi lo) + of_bits_failwith (subrange_list false bits hi lo) val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b let sign_extend v len = exts_vec len v @@ -57,9 +57,9 @@ val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> b let zero_extend v len = extz_vec len v val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a -let shift_bits_right v m = shiftr v (unsigned m) +let shift_bits_right v m = shiftr v (uint m) val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a -let shift_bits_left v m = shiftl v (unsigned m) +let shift_bits_left v m = shiftl v (uint m) val prerr_endline : string -> unit let prerr_endline _ = () diff --git a/src/ast_util.ml b/src/ast_util.ml index 82ef660d..5261a6d2 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -512,8 +512,8 @@ let string_of_base_effect_aux = function | BE_unspec -> "unspec" | BE_nondet -> "nondet" | BE_escape -> "escape" - | BE_lset -> "lset" - | BE_lret -> "lret" + (*| BE_lset -> "lset" + | BE_lret -> "lret"*) let string_of_base_kind_aux = function | BK_type -> "Type" diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 1d8623df..8cef266e 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -30,20 +30,35 @@ end declare {isabelle} termination_argument foreachM = automatic -val bool_of_bitU_undef : forall 'rv 'e. bitU -> monad 'rv bool 'e -let bool_of_bitU_undef = function +val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e +let bool_of_bitU_fail = function + | B0 -> return false + | B1 -> return true + | BU -> Fail "bool_of_bitU" +end + +val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e +let bool_of_bitU_oracle = function | B0 -> return false | B1 -> return true | BU -> undefined_bool () end -val bools_of_bitUs : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e -let bools_of_bitUs bits = +val bools_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e +let bools_of_bits_oracle bits = foreachM bits [] (fun b bools -> - bool_of_bitU_undef b >>= (fun b -> + bool_of_bitU_oracle b >>= (fun b -> return (bools ++ [b]))) +val of_bits_oracle : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e +let of_bits_oracle bits = + bools_of_bits_oracle bits >>= (fun bs -> + return (of_bools bs)) + +val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e +let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits) + val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec whileM vars cond body = diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index edbe1f03..92b9ac5e 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -127,11 +127,20 @@ let try_catchR m h = | Right e -> h e end) +val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e +let maybe_fail msg = function + | Just a -> return a + | Nothing -> Fail msg +end + +val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e +let read_mem_bytes rk addr sz = + Read_mem rk (bits_of addr) (nat_of_int sz) return 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 k bytes = Done (bits_of_mem_bytes bytes) in - Read_mem rk (bits_of addr) (natFromInteger sz) k + read_mem_bytes rk addr sz >>= (fun bytes -> + maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))) val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e let read_tag addr = Read_tag (bits_of addr) return @@ -142,7 +151,7 @@ let excl_result () = Excl_res 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 (bits_of addr) (natFromInteger sz) (Done ()) +let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ()) val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e let write_mem_val v = match mem_bytes_of_bits v with @@ -166,10 +175,10 @@ let read_reg reg = (* 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 of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j)) + read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j)) let read_reg_bit reg i = - read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v -> + read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v -> return (extract_only_element v) let read_reg_field reg regfield = @@ -188,9 +197,9 @@ let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) let write_reg reg v = write_reg_aux (external_reg_whole reg) v let write_reg_range reg i j v = - write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v + write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v let write_reg_pos reg i v = - let iN = natFromInteger i in + let iN = nat_of_int i in write_reg_aux (external_reg_slice reg (iN,iN)) [v] let write_reg_bit = write_reg_pos let write_reg_field reg regfield v = @@ -199,7 +208,7 @@ let write_reg_field_bit reg regfield bit = write_reg_aux (external_reg_field_whole reg regfield.field_name) (Vector [bit] 0 (is_inc_of_reg reg)) let write_reg_field_range reg regfield i j v = - write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v + write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int 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*) diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 9354f9d4..9b0857d9 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -4,20 +4,21 @@ open import Sail_values (*** Bit vector operations *) -val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c -let concat_bv l r = of_bits (bits_of l ++ bits_of r) +val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU +let concat_bv l r = (bits_of l ++ bits_of r) -val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b -let cons_bv b v = of_bits (b :: bits_of v) +val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU +let cons_bv b v = b :: bits_of v -let bool_of_bv v = extract_only_element (bits_of v) -let cast_unit_bv b = of_bits [b] -let bv_of_bit len b = of_bits (extz_bits len [b]) -let int_of_bv sign = if sign then signed else unsigned +val cast_unit_bv : bitU -> list bitU +let cast_unit_bv b = [b] + +val bv_of_bit : integer -> bitU -> list bitU +let bv_of_bit len b = extz_bits len [b] let most_significant v = match bits_of v with | b :: _ -> b - | _ -> failwith "most_significant applied to empty vector" + | _ -> B0 (* Treat empty bitvector as all zeros *) end let get_max_representable_in sign (n : integer) : integer = @@ -36,135 +37,106 @@ let get_min_representable_in _ (n : integer) : integer = else if n = 5 then min_5 else 0 - (integerPow 2 (natFromInteger n)) -val bitwise_binop_bv : forall 'a. Bitvector 'a => - (bool -> bool -> bool) -> 'a -> 'a -> 'a -let bitwise_binop_bv op l r = of_bits (binop_bits op (bits_of l) (bits_of r)) - -let and_bv = bitwise_binop_bv (&&) -let or_bv = bitwise_binop_bv (||) -let xor_bv = bitwise_binop_bv xor -let not_bv v = of_bits (not_bits (bits_of v)) - -val arith_op_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b -let arith_op_bv op sign size l r = - let (l',r') = (int_of_bv sign l, int_of_bv sign r) in - let n = op l' r' in - of_int (size * length l) n - - -let add_bv = arith_op_bv integerAdd false 1 -let sadd_bv = arith_op_bv integerAdd true 1 -let sub_bv = arith_op_bv integerMinus false 1 -let mult_bv = arith_op_bv integerMult false 2 -let smult_bv = arith_op_bv integerMult true 2 - -let inline add_mword = Machine_word.plus -let inline sub_mword = Machine_word.minus -val mult_mword : forall 'a 'b. Size 'b => mword 'a -> mword 'a -> mword 'b -let mult_mword l r = times (zeroExtend l) (zeroExtend r) - -val arith_op_bv_int : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> integer -> 'b -let arith_op_bv_int op sign size l r = - let l' = int_of_bv sign l in - let n = op l' r in - of_int (size * length l) n - -let add_bv_int = arith_op_bv_int integerAdd false 1 -let sadd_bv_int = arith_op_bv_int integerAdd true 1 -let sub_bv_int = arith_op_bv_int integerMinus false 1 -let mult_bv_int = arith_op_bv_int integerMult false 2 -let smult_bv_int = arith_op_bv_int integerMult true 2 - -val arith_op_int_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b -let arith_op_int_bv op sign size l r = - let r' = int_of_bv sign r in - let n = op l r' in - of_int (size * length r) n - -let add_int_bv = arith_op_int_bv integerAdd false 1 -let sadd_int_bv = arith_op_int_bv integerAdd true 1 -let sub_int_bv = arith_op_int_bv integerMinus false 1 -let mult_int_bv = arith_op_int_bv integerMult false 2 -let smult_int_bv = arith_op_int_bv integerMult true 2 - -let arith_op_bv_bit op sign (size : integer) l r = - let l' = int_of_bv sign l in - let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - of_int (size * length l) n - -let add_bv_bit = arith_op_bv_bit integerAdd false 1 -let sadd_bv_bit = arith_op_bv_bit integerAdd true 1 -let sub_bv_bit = arith_op_bv_bit integerMinus true 1 - -val arith_op_overflow_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU) +val arith_op_bv_int : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a +let arith_op_bv_int op sign l r = + let r' = of_int (length l) r in + arith_op_bv op sign l r' + +val arith_op_int_bv : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a +let arith_op_int_bv op sign l r = + let l' = of_int (length r) l in + arith_op_bv op sign l' r + +let arith_op_bv_bool op sign l r = arith_op_bv_int op sign l (if r then 1 else 0) +let arith_op_bv_bit op sign l r = Maybe.map (arith_op_bv_bool op sign l) (bool_of_bitU r) + +(* TODO (or just omit and define it per spec if needed) +val arith_op_overflow_bv : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU) let arith_op_overflow_bv op sign size l r = let len = length l in let act_size = len * size in - let (l_sign,r_sign) = (int_of_bv sign l,int_of_bv sign r) in - let (l_unsign,r_unsign) = (int_of_bv false l,int_of_bv false r) in - let n = op l_sign r_sign in - let n_unsign = op l_unsign r_unsign in - let correct_size = of_int act_size n in - let one_more_size_u = bits_of_int (act_size + 1) n_unsign in - let overflow = - if n <= get_max_representable_in sign len && - n >= get_min_representable_in sign len - then B0 else B1 in - let c_out = most_significant one_more_size_u in - (correct_size,overflow,c_out) + match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with + | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) -> + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size = of_int act_size n in + let one_more_size_u = bits_of_int (act_size + 1) n_unsign in + let overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then B0 else B1 in + let c_out = most_significant one_more_size_u in + (correct_size,overflow,c_out) + | (_, _, _, _) -> + (repeat [BU] act_size, BU, BU) + end let add_overflow_bv = arith_op_overflow_bv integerAdd false 1 -let add_overflow_bv_signed = arith_op_overflow_bv integerAdd true 1 +let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1 let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1 -let sub_overflow_bv_signed = arith_op_overflow_bv integerMinus true 1 +let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1 let mult_overflow_bv = arith_op_overflow_bv integerMult false 2 -let mult_overflow_bv_signed = arith_op_overflow_bv integerMult true 2 +let mults_overflow_bv = arith_op_overflow_bv integerMult true 2 -val arith_op_overflow_bv_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU) +val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU) let arith_op_overflow_bv_bit op sign size l r_bit = let act_size = length l * size in - let l' = int_of_bv sign l in - let l_u = int_of_bv false l in - let (n,nu,changed) = match r_bit with - | B1 -> (op l' 1, op l_u 1, true) - | B0 -> (l',l_u,false) - | BU -> failwith "arith_op_overflow_bv_bit applied to undefined bit" - end in - let correct_size = of_int act_size n in - let one_larger = bits_of_int (act_size + 1) nu in - let overflow = - if changed - then - if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then B0 else B1 - else B0 in - (correct_size,overflow,most_significant one_larger) + match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with + | (Just l', Just l_u, false) -> + let (n, nu, changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l', l_u, false) + | BU -> (* unreachable due to check above *) + failwith "arith_op_overflow_bv_bit applied to undefined bit" + end in + let correct_size = of_int act_size n in + let one_larger = bits_of_int (act_size + 1) nu in + let overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then B0 else B1 + else B0 in + (correct_size, overflow, most_significant one_larger) + | (_, _, _) -> + (repeat [BU] act_size, BU, BU) + end let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1 -let add_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerAdd true 1 +let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1 let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1 -let sub_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerMinus true 1 +let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*) type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot -val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a +let invert_shift = function + | LL_shift -> RR_shift + | RR_shift -> LL_shift + | RR_shift_arith -> LL_shift + | LL_rot -> RR_rot + | RR_rot -> LL_rot +end + +val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU let shift_op_bv op v n = + let v = bits_of v in + if n = 0 then v else + let (op, n) = if n > 0 then (op, n) else (invert_shift op, ~n) in match op with | LL_shift -> - of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n) + subrange_list true v n (length v - 1) ++ repeat [B0] n | RR_shift -> - of_bits (repeat [B0] n ++ get_bits true v 0 (length v - n - 1)) + repeat [B0] n ++ subrange_list true v 0 (length v - n - 1) | RR_shift_arith -> - of_bits (repeat [most_significant v] n ++ get_bits true v 0 (length v - n - 1)) + repeat [most_significant v] n ++ subrange_list true v 0 (length v - n - 1) | LL_rot -> - of_bits (get_bits true v n (length v - 1) ++ get_bits true v 0 (n - 1)) + subrange_list true v n (length v - 1) ++ subrange_list true v 0 (n - 1) | RR_rot -> - of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1)) + subrange_list false v 0 (n - 1) ++ subrange_list false v n (length v - 1) end let shiftl_bv = shift_op_bv LL_shift (*"<<"*) @@ -173,10 +145,11 @@ let arith_shiftr_bv = shift_op_bv RR_shift_arith let rotl_bv = shift_op_bv LL_rot (*"<<<"*) let rotr_bv = shift_op_bv LL_rot (*">>>"*) -let shiftl_mword w n = Machine_word.shiftLeft w (natFromInteger n) -let shiftr_mword w n = Machine_word.shiftRight w (natFromInteger n) -let rotl_mword w n = Machine_word.rotateLeft (natFromInteger n) w -let rotr_mword w n = Machine_word.rotateRight (natFromInteger n) w +let shiftl_mword w n = Machine_word.shiftLeft w (nat_of_int n) +let shiftr_mword w n = Machine_word.shiftRight w (nat_of_int n) +let arith_shiftr_mword w n = Machine_word.arithShiftRight w (nat_of_int n) +let rotl_mword w n = Machine_word.rotateLeft (nat_of_int n) w +let rotr_mword w n = Machine_word.rotateRight (nat_of_int n) w let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 @@ -184,27 +157,19 @@ let rec arith_op_no0 (op : integer -> integer -> integer) l r = else Just (op l r) val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b let arith_op_bv_no0 op sign size l r = - let act_size = length l * size in - let (l',r') = (int_of_bv sign l,int_of_bv sign r) in - let n = arith_op_no0 op l' r' in - let (representable,n') = - match n with - | Just n' -> - (n' <= get_max_representable_in sign act_size && - n' >= get_min_representable_in sign act_size, n') - | _ -> (false,0) - end in - if representable then (of_int act_size n') else (of_bits (repeat [BU] act_size)) + Maybe.bind (int_of_bv sign l) (fun l' -> + Maybe.bind (int_of_bv sign r) (fun r' -> + if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r')))) let mod_bv = arith_op_bv_no0 hardware_mod false 1 let quot_bv = arith_op_bv_no0 hardware_quot false 1 -let quot_bv_signed = arith_op_bv_no0 hardware_quot true 1 +let quots_bv = arith_op_bv_no0 hardware_quot true 1 let mod_mword = Machine_word.modulo let quot_mword = Machine_word.unsignedDivide -let quot_mword_signed = Machine_word.signedDivide +let quots_mword = Machine_word.signedDivide let arith_op_bv_int_no0 op sign size l r = arith_op_bv_no0 op sign size l (of_int (length l) r) @@ -212,26 +177,49 @@ let arith_op_bv_int_no0 op sign size l r = let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1 let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1 -let replicate_bits_bv v count = of_bits (repeat (bits_of v) count) +let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r) +let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r) +let quots_mword_int l r = Machine_word.signedDivide l (wordFromInteger r) + +let replicate_bits_bv v count = repeat (bits_of v) count let duplicate_bit_bv bit len = replicate_bits_bv [bit] len val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let eq_bv l r = (unsigned l = unsigned r) +let eq_bv l r = (bits_of l = bits_of r) + +let eq_mword l r = (l = r) val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let neq_bv l r = (unsigned l <> unsigned r) - -val ucmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool -let ucmp_bv cmp l r = cmp (unsigned l) (unsigned r) - -val scmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool -let scmp_bv cmp l r = cmp (signed l) (signed r) - -let ult_bv = ucmp_bv (<) -let slt_bv = scmp_bv (<) -let ugt_bv = ucmp_bv (>) -let sgt_bv = scmp_bv (>) -let ulteq_bv = ucmp_bv (<=) -let slteq_bv = scmp_bv (<=) -let ugteq_bv = ucmp_bv (>=) -let sgteq_bv = scmp_bv (>=) +let neq_bv l r = not (eq_bv l r) + +let neq_mword l r = (l <> r) + +val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r)) +let ulteq_bv l r = (eq_bv l r) || (ult_bv l r) +let ugt_bv l r = not (ulteq_bv l r) +let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r) + +val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let slt_bv l r = + match (most_significant l, most_significant r) with + | (B0, B0) -> ult_bv l r + | (B0, B1) -> false + | (B1, B0) -> true + | (B1, B1) -> + let l' = add_one_bit_ignore_overflow (bits_of l) in + let r' = add_one_bit_ignore_overflow (bits_of r) in + ugt_bv l' r' + | (BU, BU) -> ult_bv l r + | (BU, _) -> true + | (_, BU) -> false + end +let slteq_bv l r = (eq_bv l r) || (slt_bv l r) +let sgt_bv l r = not (slteq_bv l r) +let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r) + +val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool +let ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r) + +val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool +let scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index a627f560..9b81e233 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -2,9 +2,27 @@ open import Pervasives_extra open import Machine_word open import Sail_values open import Sail_operators +open import Prompt_monad +open import Prompt (* Specialisation of operators to bit lists *) +val uint_maybe : list bitU -> maybe integer +let uint_maybe v = unsigned v +let uint_fail v = maybe_fail "uint" (unsigned v) +let uint_oracle v = + bools_of_bits_oracle v >>= (fun bs -> + return (int_of_bools false bs)) +let uint v = maybe_failwith (uint_maybe v) + +val sint_maybe : list bitU -> maybe integer +let sint_maybe v = signed v +let sint_fail v = maybe_fail "sint" (signed v) +let sint_oracle v = + bools_of_bits_oracle v >>= (fun bs -> + return (int_of_bools true bs)) +let sint v = maybe_failwith (sint_maybe v) + val access_vec_inc : list bitU -> integer -> bitU let access_vec_inc = access_bv_inc @@ -13,9 +31,15 @@ let access_vec_dec = access_bv_dec val update_vec_inc : list bitU -> integer -> bitU -> list bitU let update_vec_inc = update_bv_inc +let update_vec_inc_maybe v i b = Just (update_vec_inc v i b) +let update_vec_inc_fail v i b = return (update_vec_inc v i b) +let update_vec_inc_oracle v i b = return (update_vec_inc v i b) val update_vec_dec : list bitU -> integer -> bitU -> list bitU let update_vec_dec = update_bv_dec +let update_vec_dec_maybe v i b = Just (update_vec_dec v i b) +let update_vec_dec_fail v i b = return (update_vec_dec v i b) +let update_vec_dec_oracle v i b = return (update_vec_dec v i b) val subrange_vec_inc : list bitU -> integer -> integer -> list bitU let subrange_vec_inc = subrange_bv_inc @@ -40,21 +64,30 @@ let concat_vec = concat_bv val cons_vec : bitU -> list bitU -> list bitU let cons_vec = cons_bv +let cons_vec_maybe b v = Just (cons_vec b v) +let cons_vec_fail b v = return (cons_vec b v) +let cons_vec_oracle b v = return (cons_vec b v) -val bool_of_vec : mword ty1 -> bitU -let bool_of_vec = bool_of_bv - -val cast_unit_vec : bitU -> mword ty1 +val cast_unit_vec : bitU -> list bitU let cast_unit_vec = cast_unit_bv +let cast_unit_vec_maybe b = Just (cast_unit_vec b) +let cast_unit_vec_fail b = return (cast_unit_vec b) +let cast_unit_vec_oracle b = return (cast_unit_vec b) val vec_of_bit : integer -> bitU -> list bitU let vec_of_bit = bv_of_bit +let vec_of_bit_maybe len b = Just (vec_of_bit len b) +let vec_of_bit_fail len b = return (vec_of_bit len b) +let vec_of_bit_oracle len b = return (vec_of_bit len b) val msb : list bitU -> bitU let msb = most_significant -val int_of_vec : bool -> list bitU -> integer -let int_of_vec = int_of_bv +val int_of_vec_maybe : bool -> list bitU -> maybe integer +let int_of_vec_maybe = int_of_bv +let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v) +let int_of_vec_oracle sign v = bools_of_bits_oracle v >>= (fun v -> return (int_of_bools sign v)) +let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v) val string_of_vec : list bitU -> string let string_of_vec = string_of_bv @@ -63,52 +96,75 @@ val and_vec : list bitU -> list bitU -> list bitU val or_vec : list bitU -> list bitU -> list bitU val xor_vec : list bitU -> list bitU -> list bitU val not_vec : list bitU -> list bitU -let and_vec = and_bv -let or_vec = or_bv -let xor_vec = xor_bv -let not_vec = not_bv +let and_vec = binop_list and_bit +let or_vec = binop_list or_bit +let xor_vec = binop_list xor_bit +let not_vec = List.map not_bit + +val arith_op_double_bl : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> 'a -> 'a -> list bitU +let arith_op_double_bl op sign l r = + let len = 2 * length l in + let l' = if sign then exts_bv len l else extz_bv len l in + let r' = if sign then exts_bv len r else extz_bv len r in + arith_op_bv op sign l' r' val add_vec : list bitU -> list bitU -> list bitU -val sadd_vec : list bitU -> list bitU -> list bitU +val adds_vec : list bitU -> list bitU -> list bitU val sub_vec : list bitU -> list bitU -> list bitU val mult_vec : list bitU -> list bitU -> list bitU -val smult_vec : list bitU -> list bitU -> list bitU -let add_vec = add_bv -let sadd_vec = sadd_bv -let sub_vec = sub_bv -let mult_vec = mult_bv -let smult_vec = smult_bv - -val add_vec_int : list bitU -> integer -> list bitU -val sadd_vec_int : list bitU -> integer -> list bitU -val sub_vec_int : list bitU -> integer -> list bitU -val mult_vec_int : list bitU -> integer -> list bitU -val smult_vec_int : list bitU -> integer -> list bitU -let add_vec_int = add_bv_int -let sadd_vec_int = sadd_bv_int -let sub_vec_int = sub_bv_int -let mult_vec_int = mult_bv_int -let smult_vec_int = smult_bv_int - -val add_int_vec : integer -> list bitU -> list bitU -val sadd_int_vec : integer -> list bitU -> list bitU -val sub_int_vec : integer -> list bitU -> list bitU -val mult_int_vec : integer -> list bitU -> list bitU -val smult_int_vec : integer -> list bitU -> list bitU -let add_int_vec = add_int_bv -let sadd_int_vec = sadd_int_bv -let sub_int_vec = sub_int_bv -let mult_int_vec = mult_int_bv -let smult_int_vec = smult_int_bv - -val add_vec_bit : list bitU -> bitU -> list bitU -val sadd_vec_bit : list bitU -> bitU -> list bitU -val sub_vec_bit : list bitU -> bitU -> list bitU -let add_vec_bit = add_bv_bit -let sadd_vec_bit = sadd_bv_bit -let sub_vec_bit = sub_bv_bit - -val add_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) +val mults_vec : list bitU -> list bitU -> list bitU +let add_vec = arith_op_bv integerAdd false +let adds_vec = arith_op_bv integerAdd true +let sub_vec = arith_op_bv integerMinus false +let mult_vec = arith_op_double_bl integerMult false +let mults_vec = arith_op_double_bl integerMult true + +val add_vec_int : list bitU -> integer -> list bitU +val adds_vec_int : list bitU -> integer -> list bitU +val sub_vec_int : list bitU -> integer -> list bitU +val mult_vec_int : list bitU -> integer -> list bitU +val mults_vec_int : list bitU -> integer -> list bitU +let add_vec_int l r = arith_op_bv_int integerAdd false l r +let adds_vec_int l r = arith_op_bv_int integerAdd true l r +let sub_vec_int l r = arith_op_bv_int integerMinus false l r +let mult_vec_int l r = arith_op_double_bl integerMult false l (of_int (length l) r) +let mults_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r) + +val add_int_vec : integer -> list bitU -> list bitU +val adds_int_vec : integer -> list bitU -> list bitU +val sub_int_vec : integer -> list bitU -> list bitU +val mult_int_vec : integer -> list bitU -> list bitU +val mults_int_vec : integer -> list bitU -> list bitU +let add_int_vec l r = arith_op_int_bv integerAdd false l r +let adds_int_vec l r = arith_op_int_bv integerAdd true l r +let sub_int_vec l r = arith_op_int_bv integerMinus false l r +let mult_int_vec l r = arith_op_double_bl integerMult false (of_int (length r) l) r +let mults_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r + +val add_vec_bit : list bitU -> bitU -> list bitU +val adds_vec_bit : list bitU -> bitU -> list bitU +val sub_vec_bit : list bitU -> bitU -> list bitU + +let add_vec_bool l r = arith_op_bv_bool integerAdd false l r +let add_vec_bit_maybe l r = arith_op_bv_bit integerAdd false l r +let add_vec_bit_fail l r = maybe_fail "add_vec_bit" (add_vec_bit_maybe l r) +let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r)) +let add_vec_bit l r = fromMaybe (repeat [BU] (length l)) (add_vec_bit_maybe l r) + +let adds_vec_bool l r = arith_op_bv_bool integerAdd true l r +let adds_vec_bit_maybe l r = arith_op_bv_bit integerAdd true l r +let adds_vec_bit_fail l r = maybe_fail "adds_vec_bit" (adds_vec_bit_maybe l r) +let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r)) +let adds_vec_bit l r = fromMaybe (repeat [BU] (length l)) (adds_vec_bit_maybe l r) + +let sub_vec_bool l r = arith_op_bv_bool integerMinus false l r +let sub_vec_bit_maybe l r = arith_op_bv_bit integerMinus false l r +let sub_vec_bit_fail l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r) +let sub_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r)) +let sub_vec_bit l r = fromMaybe (repeat [BU] (length l)) (sub_vec_bit_maybe l r) + +(*val add_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) val add_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) val sub_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) val sub_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) @@ -128,7 +184,7 @@ val sub_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU let add_overflow_vec_bit = add_overflow_bv_bit let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed let sub_overflow_vec_bit = sub_overflow_bv_bit -let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed +let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*) val shiftl : list bitU -> integer -> list bitU val shiftr : list bitU -> integer -> list bitU @@ -141,23 +197,28 @@ let arith_shiftr = arith_shiftr_bv let rotl = rotl_bv let rotr = rotr_bv -val mod_vec : list bitU -> list bitU -> list bitU -val quot_vec : list bitU -> list bitU -> list bitU -val quot_vec_signed : list bitU -> list bitU -> list bitU -let mod_vec = mod_bv -let quot_vec = quot_bv -let quot_vec_signed = quot_bv_signed +val mod_vec : list bitU -> list bitU -> list bitU +val quot_vec : list bitU -> list bitU -> list bitU +val quots_vec : list bitU -> list bitU -> list bitU +let mod_vec l r = fromMaybe (repeat [BU] (length l)) (mod_bv l r) +let quot_vec l r = fromMaybe (repeat [BU] (length l)) (quot_bv l r) +let quots_vec l r = fromMaybe (repeat [BU] (length l)) (quots_bv l r) -val mod_vec_int : list bitU -> integer -> list bitU -val quot_vec_int : list bitU -> integer -> list bitU -let mod_vec_int = mod_bv_int -let quot_vec_int = quot_bv_int +val mod_vec_int : list bitU -> integer -> list bitU +val quot_vec_int : list bitU -> integer -> list bitU +let mod_vec_int l r = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r) +let quot_vec_int l r = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r) val replicate_bits : list bitU -> integer -> list bitU let replicate_bits = replicate_bits_bv val duplicate : bitU -> integer -> list bitU let duplicate = duplicate_bit_bv +let duplicate_maybe b n = Just (duplicate b n) +let duplicate_fail b n = return (duplicate b n) +let duplicate_oracle b n = + bool_of_bitU_oracle b >>= (fun b -> + return (duplicate (bitU_of_bool b) n)) val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 7411c0a9..ea7c11cf 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -2,59 +2,109 @@ open import Pervasives_extra open import Machine_word open import Sail_values open import Sail_operators +open import Prompt_monad +open import Prompt + +val mword_zero : forall 'a. Size 'a => mword 'a +let mword_zero = wordFromInteger 0 (* Specialisation of operators to machine words *) +let uint v = unsignedIntegerFromWord v +let uint_maybe v = Just (uint v) +let uint_fail v = return (uint v) +let uint_oracle v = return (uint v) + +let sint v = signedIntegerFromWord v +let sint_maybe v = Just (sint v) +let sint_fail v = return (sint v) +let sint_oracle v = return (sint v) + +val vec_of_bits_failwith : forall 'a. Size 'a => integer -> list bitU -> mword 'a +let vec_of_bits_failwith _ bits = of_bits_failwith bits + +val vec_of_bits_fail : forall 'rv 'a 'e. Size 'a => integer -> list bitU -> monad 'rv (mword 'a) 'e +let vec_of_bits_fail _ bits = of_bits_fail bits + +val vec_of_bits_oracle : forall 'rv 'a 'e. Size 'a => integer -> list bitU -> monad 'rv (mword 'a) 'e +let vec_of_bits_oracle _ bits = of_bits_oracle bits + val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU let access_vec_inc = access_bv_inc val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU let access_vec_dec = access_bv_dec -val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a -let update_vec_inc = update_bv_inc +let update_vec_dec_maybe w i b = update_mword_dec w i b +let update_vec_dec_fail w i b = + bool_of_bitU_fail b >>= (fun b -> + return (update_mword_bool_dec w i b)) +let update_vec_dec_oracle w i b = + bool_of_bitU_oracle b >>= (fun b -> + return (update_mword_bool_dec w i b)) +let update_vec_dec w i b = maybe_failwith (update_vec_dec_maybe w i b) + +let update_vec_inc_maybe w i b = update_mword_inc w i b +let update_vec_inc_fail w i b = + bool_of_bitU_fail b >>= (fun b -> + return (update_mword_bool_inc w i b)) +let update_vec_inc_oracle w i b = + bool_of_bitU_oracle b >>= (fun b -> + return (update_mword_bool_inc w i b)) +let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b) -val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a -let update_vec_dec = update_bv_dec +val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b +let subrange_vec_dec w i j = Machine_word.word_extract (nat_of_int i) (nat_of_int j) w val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -let subrange_vec_inc = subrange_bv_inc +let subrange_vec_inc w i j = subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) -val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -let subrange_vec_dec = subrange_bv_dec +val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a +let update_subrange_vec_dec w i j w' = Machine_word.word_update w (nat_of_int i) (nat_of_int j) w' val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_subrange_vec_inc = update_subrange_bv_inc - -val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_subrange_vec_dec = update_subrange_bv_dec +let update_subrange_vec_inc w i j w' = update_subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) w' val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let extz_vec = extz_bv +let extz_vec _ w = Machine_word.zeroExtend w val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let exts_vec = exts_bv +let exts_vec _ w = Machine_word.signExtend w val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c -let concat_vec = concat_bv - -val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b -let cons_vec = cons_bv - -val bool_of_vec : mword ty1 -> bitU -let bool_of_vec = bool_of_bv - -val cast_unit_vec : bitU -> mword ty1 -let cast_unit_vec = cast_unit_bv - -val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a -let vec_of_bit = bv_of_bit +let concat_vec = Machine_word.word_concat + +val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> mword 'a -> mword 'b +let cons_vec_bool b w = wordFromBitlist (b :: bitlistFromWord w) +let cons_vec_maybe b w = Maybe.map (fun b -> cons_vec_bool b w) (bool_of_bitU b) +let cons_vec_fail b w = bool_of_bitU_fail b >>= (fun b -> return (cons_vec_bool b w)) +let cons_vec_oracle b w = bool_of_bitU_oracle b >>= (fun b -> return (cons_vec_bool b w)) +let cons_vec b w = maybe_failwith (cons_vec_maybe b w) + +val vec_of_bool : forall 'a. Size 'a => integer -> bool -> mword 'a +let vec_of_bool _ b = wordFromBitlist [b] +let vec_of_bit_maybe len b = Maybe.map (vec_of_bool len) (bool_of_bitU b) +let vec_of_bit_fail len b = bool_of_bitU_fail b >>= (fun b -> return (vec_of_bool len b)) +let vec_of_bit_oracle len b = bool_of_bitU_oracle b >>= (fun b -> return (vec_of_bool len b)) +let vec_of_bit len b = maybe_failwith (vec_of_bit_maybe len b) + +val cast_bool_vec : bool -> mword ty1 +let cast_bool_vec b = vec_of_bool 1 b +let cast_unit_vec_maybe b = vec_of_bit_maybe 1 b +let cast_unit_vec_fail b = bool_of_bitU_fail b >>= (fun b -> return (cast_bool_vec b)) +let cast_unit_vec_oracle b = bool_of_bitU_oracle b >>= (fun b -> return (cast_bool_vec b)) +let cast_unit_vec b = maybe_failwith (cast_unit_vec_maybe b) val msb : forall 'a. Size 'a => mword 'a -> bitU let msb = most_significant val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer -let int_of_vec = int_of_bv +let int_of_vec sign w = + if sign + then signedIntegerFromWord w + else unsignedIntegerFromWord w +let int_of_vec_maybe sign w = Just (int_of_vec sign w) +let int_of_vec_fail sign w = return (int_of_vec sign w) val string_of_vec : forall 'a. Size 'a => mword 'a -> string let string_of_vec = string_of_bv @@ -63,63 +113,83 @@ val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val or_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a -let and_vec = and_bv -let or_vec = or_bv -let xor_vec = xor_bv -let not_vec = not_bv +let and_vec = Machine_word.lAnd +let or_vec = Machine_word.lOr +let xor_vec = Machine_word.lXor +let not_vec = Machine_word.lNot val add_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -val sadd_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +val adds_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val sub_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val mult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b -val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b -let add_vec = add_bv -let sadd_vec = sadd_bv -let sub_vec = sub_bv -let mult_vec = mult_bv -let smult_vec = smult_bv +val mults_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b +let add_vec l r = arith_op_bv integerAdd false l r +let adds_vec l r = arith_op_bv integerAdd true l r +let sub_vec l r = arith_op_bv integerMinus true l r +let mult_vec l r = arith_op_bv integerMult false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b) +let mults_vec l r = arith_op_bv integerMult true (signExtend l : mword 'b) (signExtend r : mword 'b) val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val sadd_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val adds_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -val smult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -let add_vec_int = add_bv_int -let sadd_vec_int = sadd_bv_int -let sub_vec_int = sub_bv_int -let mult_vec_int = mult_bv_int -let smult_vec_int = smult_bv_int +val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let add_vec_int l r = arith_op_bv_int integerAdd false l r +let adds_vec_int l r = arith_op_bv_int integerAdd true l r +let sub_vec_int l r = arith_op_bv_int integerMinus true l r +let mult_vec_int l r = arith_op_bv_int integerMult false (zeroExtend l : mword 'b) r +let mults_vec_int l r = arith_op_bv_int integerMult true (signExtend l : mword 'b) r val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a -val sadd_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a +val adds_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -val smult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let add_int_vec = add_int_bv -let sadd_int_vec = sadd_int_bv -let sub_int_vec = sub_int_bv -let mult_int_vec = mult_int_bv -let smult_int_vec = smult_int_bv - -val add_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a -val sadd_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a -val sub_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a -let add_vec_bit = add_bv_bit -let sadd_vec_bit = sadd_bv_bit -let sub_vec_bit = sub_bv_bit - -val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val add_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val sub_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -let add_overflow_vec = add_overflow_bv -let add_overflow_vec_signed = add_overflow_bv_signed -let sub_overflow_vec = sub_overflow_bv -let sub_overflow_vec_signed = sub_overflow_bv_signed -let mult_overflow_vec = mult_overflow_bv -let mult_overflow_vec_signed = mult_overflow_bv_signed +val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b +let add_int_vec l r = arith_op_int_bv integerAdd false l r +let adds_int_vec l r = arith_op_int_bv integerAdd true l r +let sub_int_vec l r = arith_op_int_bv integerMinus true l r +let mult_int_vec l r = arith_op_int_bv integerMult false l (zeroExtend r : mword 'b) +let mults_int_vec l r = arith_op_int_bv integerMult true l (signExtend r : mword 'b) + +val add_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a +val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a +val sub_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a + +let add_vec_bool l r = arith_op_bv_bool integerAdd false l r +let add_vec_bit_maybe l r = Maybe.map (add_vec_bool l) (bool_of_bitU r) +let add_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (add_vec_bool l r)) +let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r)) +let add_vec_bit l r = maybe_failwith (add_vec_bit_maybe l r) + +let adds_vec_bool l r = arith_op_bv_bool integerAdd true l r +let adds_vec_bit_maybe l r = Maybe.map (adds_vec_bool l) (bool_of_bitU r) +let adds_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec_bool l r)) +let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r)) +let adds_vec_bit l r = maybe_failwith (adds_vec_bit_maybe l r) + +let sub_vec_bool l r = arith_op_bv_bool integerMinus true l r +let sub_vec_bit_maybe l r = Maybe.map (sub_vec_bool l) (bool_of_bitU r) +let sub_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (sub_vec_bool l r)) +let sub_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r)) +let sub_vec_bit l r = maybe_failwith (sub_vec_bit_maybe l r) + +(* TODO +val maybe_mword_of_bits_overflow : forall 'a. Size 'a => (list bitU * bitU * bitU) -> maybe (mword 'a * bitU * bitU) +let maybe_mword_of_bits_overflow (bits, overflow, carry) = + Maybe.map (fun w -> (w, overflow, carry)) (of_bits bits) + +val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val adds_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val subs_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val mults_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +let add_overflow_vec l r = maybe_mword_of_bits_overflow (add_overflow_bv l r) +let adds_overflow_vec l r = maybe_mword_of_bits_overflow (adds_overflow_bv l r) +let sub_overflow_vec l r = maybe_mword_of_bits_overflow (sub_overflow_bv l r) +let subs_overflow_vec l r = maybe_mword_of_bits_overflow (subs_overflow_bv l r) +let mult_overflow_vec l r = maybe_mword_of_bits_overflow (mult_overflow_bv l r) +let mults_overflow_vec l r = maybe_mword_of_bits_overflow (mults_overflow_bv l r) val add_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) val add_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) @@ -128,36 +198,40 @@ val sub_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mw let add_overflow_vec_bit = add_overflow_bv_bit let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed let sub_overflow_vec_bit = sub_overflow_bv_bit -let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed +let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*) val shiftl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -let shiftl = shiftl_bv -let shiftr = shiftr_bv -let arith_shiftr = arith_shiftr_bv -let rotl = rotl_bv -let rotr = rotr_bv - -val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -let mod_vec = mod_bv -let quot_vec = quot_bv -let quot_vec_signed = quot_bv_signed +let shiftl = shiftl_mword +let shiftr = shiftr_mword +let arith_shiftr = arith_shiftr_mword +let rotl = rotl_mword +let rotr = rotr_mword + +val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +val quots_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +let mod_vec = mod_mword +let quot_vec = quot_mword +let quots_vec = quots_mword val mod_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -let mod_vec_int = mod_bv_int -let quot_vec_int = quot_bv_int +let mod_vec_int = mod_mword_int +let quot_vec_int = quot_mword_int val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -let replicate_bits = replicate_bits_bv +let replicate_bits v count = wordFromBitlist (repeat (bitlistFromWord v) count) -val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a -let duplicate = duplicate_bit_bv +val duplicate_bool : forall 'a. Size 'a => bool -> integer -> mword 'a +let duplicate_bool b n = wordFromBitlist (repeat [b] n) +let duplicate_maybe b n = Maybe.map (fun b -> duplicate_bool b n) (bool_of_bitU b) +let duplicate_fail b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_bool b n)) +let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n)) +let duplicate b n = maybe_failwith (duplicate_maybe b n) val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool @@ -169,13 +243,13 @@ val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -let eq_vec = eq_bv -let neq_vec = neq_bv -let ult_vec = ult_bv -let slt_vec = slt_bv -let ugt_vec = ugt_bv -let sgt_vec = sgt_bv -let ulteq_vec = ulteq_bv -let slteq_vec = slteq_bv -let ugteq_vec = ugteq_bv -let sgteq_vec = sgteq_bv +let eq_vec = eq_mword +let neq_vec = neq_mword +let ult_vec = ucmp_mword (<) +let slt_vec = scmp_mword (<) +let ugt_vec = ucmp_mword (>) +let sgt_vec = scmp_mword (>) +let ulteq_vec = ucmp_mword (<=) +let slteq_vec = scmp_mword (<=) +let ugteq_vec = ucmp_mword (>=) +let sgteq_vec = scmp_mword (>=) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index edb8da88..238ebe58 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,5 +1,3 @@ -(* Version of sail_values.lem that uses Lem's machine words library *) - open import Pervasives_extra open import Machine_word (*open import Sail_impl_base*) @@ -8,8 +6,11 @@ open import Machine_word type ii = integer type nn = natural +val nat_of_int : integer -> nat +let nat_of_int i = if i < 0 then 0 else natFromInteger i + val pow : integer -> integer -> integer -let pow m n = m ** (natFromInteger n) +let pow m n = m ** (nat_of_int n) let pow2 n = pow 2 n @@ -31,7 +32,7 @@ let mult_int l r = integerMult l r let div_int l r = integerDiv l r let div_nat l r = natDiv l r let power_int_nat l r = integerPow l r -let power_int_int l r = integerPow l (natFromInteger r) +let power_int_int l r = integerPow l (nat_of_int r) let negate_int i = integerNegate i let min_int l r = integerMin l r let max_int l r = integerMax l r @@ -50,8 +51,8 @@ let xor_bool l r = xor l r let append_list l r = l ++ r let length_list xs = integerFromNat (List.length xs) -let take_list n xs = List.take (natFromInteger n) xs -let drop_list n xs = List.drop (natFromInteger n) xs +let take_list n xs = List.take (nat_of_int n) xs +let drop_list n xs = List.drop (nat_of_int n) xs val repeat : forall 'a. list 'a -> integer -> list 'a let rec repeat xs n = @@ -99,6 +100,29 @@ let min_8 = (0 - 128 : integer) let max_5 = (31 : integer) let min_5 = (0 - 32 : integer) +(* 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 l = match l with + | [] -> Just [] + | (x :: xs) -> + match (x, just_list xs) with + | (Just x, Just xs) -> Just (x :: xs) + | (_, _) -> Nothing + end + 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))) + +val maybe_failwith : forall 'a. maybe 'a -> 'a +let maybe_failwith = function + | Just a -> a + | Nothing -> failwith "maybe_failwith" +end + (*** Bits *) type bitU = B0 | B1 | BU @@ -118,6 +142,25 @@ instance (Show bitU) let show = showBitU end +val compare_bitU : bitU -> bitU -> ordering +let compare_bitU l r = match (l, r) with + | (BU, BU) -> EQ + | (B0, B0) -> EQ + | (B1, B1) -> EQ + | (BU, _) -> LT + | (_, BU) -> GT + | (B0, _) -> LT + | (_, _) -> GT +end + +instance (Ord bitU) + let compare = compare_bitU + let (<) l r = (compare_bitU l r) = LT + let (<=) l r = (compare_bitU l r) <> GT + let (>) l r = (compare_bitU l r) = GT + let (>=) l r = (compare_bitU l r) <> LT +end + class (BitU 'a) val to_bitU : 'a -> bitU val of_bitU : bitU -> 'a @@ -129,44 +172,20 @@ instance (BitU bitU) end let bool_of_bitU = function - | B0 -> false - | B1 -> true - | BU -> failwith "bool_of_bitU applied to BU" + | B0 -> Just false + | B1 -> Just true + | BU -> Nothing end let bitU_of_bool b = if b then B1 else B0 -instance (BitU bool) +(*instance (BitU bool) let to_bitU = bitU_of_bool let of_bitU = bool_of_bitU -end +end*) let cast_bit_bool = bool_of_bitU -(*let bit_lifted_of_bitU = function - | B0 -> Bitl_zero - | B1 -> Bitl_one - | BU -> Bitl_undef - end - -let bitU_of_bit = function - | Bitc_zero -> B0 - | Bitc_one -> B1 - end - -let bit_of_bitU = function - | B0 -> Bitc_zero - | B1 -> Bitc_one - | BU -> failwith "bit_of_bitU: BU" - end - -let bitU_of_bit_lifted = function - | Bitl_zero -> B0 - | Bitl_one -> B1 - | Bitl_undef -> BU - | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" - end*) - let not_bit = function | B1 -> B0 | B0 -> B1 @@ -177,20 +196,33 @@ val is_one : integer -> bitU let is_one i = if i = 1 then B1 else B0 -let binop_bit op x y = match (x, y) with - | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) - | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) - | (x,y) -> bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y)) - end - val and_bit : bitU -> bitU -> bitU -let and_bit = binop_bit (&&) +let and_bit x y = + match (x, y) with + | (B0, _) -> B0 + | (_, B0) -> B0 + | (B1, B1) -> B1 + | (_, _) -> BU + end val or_bit : bitU -> bitU -> bitU -let or_bit = binop_bit (||) +let or_bit x y = + match (x, y) with + | (B1, _) -> B1 + | (_, B1) -> B1 + | (B0, B0) -> B0 + | (_, _) -> BU + end val xor_bit : bitU -> bitU -> bitU -let xor_bit = binop_bit xor +let xor_bit x y= + match (x, y) with + | (B0, B0) -> B0 + | (B0, B1) -> B1 + | (B1, B0) -> B1 + | (B1, B1) -> B0 + | (_, _) -> BU + end val (&.) : bitU -> bitU -> bitU let inline (&.) x y = and_bit x y @@ -202,81 +234,134 @@ val (+.) : bitU -> bitU -> bitU let inline (+.) x y = xor_bit x y -(*** Bit lists ***) +(*** Bool lists ***) -val bits_of_nat_aux : natural -> list bitU -let rec bits_of_nat_aux x = +val bools_of_nat_aux : natural -> list bool +let rec bools_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) + else (if x mod 2 = 1 then true else false) :: bools_of_nat_aux (x / 2) +declare {isabelle} termination_argument bools_of_nat_aux = automatic +let bools_of_nat n = List.reverse (bools_of_nat_aux n) -val nat_of_bits_aux : natural -> list bitU -> natural -let rec nat_of_bits_aux acc bs = match bs with +val nat_of_bools_aux : natural -> list bool -> natural +let rec nat_of_bools_aux acc bs = match bs with | [] -> acc - | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs - | B0 :: bs -> nat_of_bits_aux (2 * acc) bs - | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits" + | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs + | false :: bs -> nat_of_bools_aux (2 * acc) bs end -declare {isabelle} termination_argument nat_of_bits_aux = automatic -let nat_of_bits bits = nat_of_bits_aux 0 bits +declare {isabelle} termination_argument nat_of_bools_aux = automatic +let nat_of_bools bs = nat_of_bools_aux 0 bs + +val unsigned_of_bools : list bool -> integer +let unsigned_of_bools bs = integerFromNatural (nat_of_bools bs) + +val signed_of_bools : list bool -> integer +let signed_of_bools bs = + match bs with + | true :: _ -> 0 - (1 + (unsigned_of_bools (List.map not bs))) + | false :: _ -> unsigned_of_bools bs + | [] -> 0 (* Treat empty list as all zeros *) + end -let not_bits = List.map not_bit +val int_of_bools : bool -> list bool -> integer +let int_of_bools sign bs = if sign then signed_of_bools bs else unsigned_of_bools bs -let binop_bits op bsl bsr = - foldr (fun (bl, br) acc -> binop_bit op bl br :: acc) [] (zip bsl bsr) +val pad_list : forall 'a. 'a -> list 'a -> integer -> list 'a +let rec pad_list x xs n = + if n <= 0 then xs else pad_list x (x :: xs) (n - 1) +declare {isabelle} termination_argument pad_list = automatic -let and_bits = binop_bits (&&) -let or_bits = binop_bits (||) -let xor_bits = binop_bits xor +let ext_list pad len xs = + let longer = len - (integerFromNat (List.length xs)) in + if longer < 0 then drop (nat_of_int (abs (longer))) xs + else pad_list pad xs longer -val unsigned_of_bits : list bitU -> integer -let unsigned_of_bits bs = integerFromNatural (nat_of_bits bs) +let extz_bools len bs = ext_list false len bs +let exts_bools len bs = + match bs with + | true :: _ -> ext_list true len bs + | _ -> ext_list false len bs + end -val signed_of_bits : list bitU -> integer -let signed_of_bits bits = - match bits with - | B1 :: _ -> 0 - (1 + (unsigned_of_bits (not_bits bits))) - | B0 :: _ -> unsigned_of_bits bits - | BU :: _ -> failwith "signed_of_bits applied to list with undefined bits" - | [] -> failwith "signed_of_bits applied to empty list" +let rec add_one_bool_ignore_overflow_aux bits = match bits with + | [] -> [] + | false :: bits -> true :: bits + | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits +end +declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic + +let add_one_bool_ignore_overflow bits = + List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits)) + +let bool_list_of_int n = + let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in + if n >= (0 : integer) then bs_abs + else add_one_bool_ignore_overflow (List.map not bs_abs) +let bools_of_int len n = exts_bools len (bool_list_of_int n) + +(*** Bit lists ***) + +val has_undefined_bits : list bitU -> bool +let has_undefined_bits bs = List.any (function BU -> true | _ -> false end) bs + +let bits_of_nat n = List.map bitU_of_bool (bools_of_nat n) + +let nat_of_bits bits = + match (just_list (List.map bool_of_bitU bits)) with + | Just bs -> Just (nat_of_bools bs) + | Nothing -> Nothing + end + +let not_bits = List.map not_bit + +val binop_list : forall 'a. ('a -> 'a -> 'a) -> list 'a -> list 'a -> list 'a +let binop_list op xs ys = + foldr (fun (x, y) acc -> op x y :: acc) [] (zip xs ys) + +let unsigned_of_bits bits = + match (just_list (List.map bool_of_bitU bits)) with + | Just bs -> Just (unsigned_of_bools bs) + | Nothing -> Nothing end -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 signed_of_bits bits = + match (just_list (List.map bool_of_bitU bits)) with + | Just bs -> Just (signed_of_bools bs) + | Nothing -> Nothing + end -let ext_bits pad len bits = - let longer = len - (integerFromNat (List.length bits)) in - if longer < 0 then drop (natFromInteger (abs (longer))) bits - else pad_bitlist pad bits longer +val int_of_bits : bool -> list bitU -> maybe integer +let int_of_bits sign bs = if sign then signed_of_bits bs else unsigned_of_bits bs -let extz_bits len bits = ext_bits B0 len bits +let extz_bits len bits = ext_list B0 len bits let exts_bits len bits = match bits with - | BU :: _ -> failwith "exts_bits: undefined bit" - | B1 :: _ -> ext_bits B1 len bits - | _ -> ext_bits B0 len bits + | BU :: _ -> ext_list BU len bits + | B1 :: _ -> ext_list B1 len bits + | _ -> ext_list B0 len bits end let rec add_one_bit_ignore_overflow_aux bits = match bits with | [] -> [] | B0 :: bits -> B1 :: bits | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits - | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" + | BU :: bits -> BU :: List.map (fun _ -> BU) bits 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)) -let bitlist_of_int n = - let bits_abs = B0 :: bits_of_nat (naturalFromInteger (abs n)) in - if n >= (0 : integer) then bits_abs - else add_one_bit_ignore_overflow (not_bits bits_abs) +let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n) +let bits_of_int len n = exts_bits len (bit_list_of_int n) -let bits_of_int len n = exts_bits len (bitlist_of_int n) +val arith_op_bits : + (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU +let arith_op_bits op sign l r = + match (int_of_bits sign l, int_of_bits sign r) with + | (Just li, Just ri) -> bits_of_int (length_list l) (op li ri) + | (_, _) -> repeat [BU] (length_list l) + end let char_of_nibble = function | (B0, B0, B0, B0) -> Just #'0' @@ -322,8 +407,8 @@ let inline (^^) = append_list val subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a let subrange_list_inc xs i j = - let (toJ,_suffix) = List.splitAt (natFromInteger j + 1) xs in - let (_prefix,fromItoJ) = List.splitAt (natFromInteger i) toJ in + let (toJ,_suffix) = List.splitAt (nat_of_int (j + 1)) xs in + let (_prefix,fromItoJ) = List.splitAt (nat_of_int i) toJ in fromItoJ val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a @@ -336,8 +421,8 @@ let subrange_list is_inc xs i j = if is_inc then subrange_list_inc xs i j else s val update_subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a let update_subrange_list_inc xs i j xs' = - let (toJ,suffix) = List.splitAt (natFromInteger j + 1) xs in - let (prefix,_fromItoJ) = List.splitAt (natFromInteger i) toJ in + let (toJ,suffix) = List.splitAt (nat_of_int (j + 1)) xs in + let (prefix,_fromItoJ) = List.splitAt (nat_of_int i) toJ in prefix ++ xs' ++ suffix val update_subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a @@ -350,7 +435,7 @@ let update_subrange_list is_inc xs i j xs' = if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs' val access_list_inc : forall 'a. list 'a -> integer -> 'a -let access_list_inc xs n = List_extra.nth xs (natFromInteger n) +let access_list_inc xs n = List_extra.nth xs (nat_of_int n) val access_list_dec : forall 'a. list 'a -> integer -> 'a let access_list_dec xs n = @@ -362,7 +447,7 @@ let access_list is_inc xs n = if is_inc then access_list_inc xs n else access_list_dec xs n val update_list_inc : forall 'a. list 'a -> integer -> 'a -> list 'a -let update_list_inc xs n x = List.update xs (natFromInteger n) x +let update_list_inc xs n x = List.update xs (nat_of_int n) x val update_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a let update_list_dec xs n x = @@ -373,36 +458,19 @@ val update_list : forall 'a. bool -> list 'a -> integer -> 'a -> list 'a let update_list is_inc xs n x = if is_inc then update_list_inc xs n x else update_list_dec xs n x -let extract_only_element = function - | [] -> failwith "extract_only_element called for empty list" +let extract_only_bit = function + | [] -> BU | [e] -> e - | _ -> failwith "extract_only_element called for list with more elements" + | _ -> BU 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 l = match l with - | [] -> Just [] - | (x :: xs) -> - match (x, just_list xs) with - | (Just x, Just xs) -> Just (x :: xs) - | (_, _) -> Nothing - end - 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 let length_mword w = integerFromNat (word_length w) val slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -let slice_mword_dec w i j = word_extract (natFromInteger i) (natFromInteger j) w +let slice_mword_dec w i j = word_extract (nat_of_int i) (nat_of_int j) w val slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b let slice_mword_inc w i j = @@ -413,7 +481,7 @@ val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword let slice_mword is_inc w i j = if is_inc then slice_mword_inc w i j else slice_mword_dec w i j val update_slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_slice_mword_dec w i j w' = word_update w (natFromInteger i) (natFromInteger j) w' +let update_slice_mword_dec w i j w' = word_update w (nat_of_int i) (nat_of_int j) w' val update_slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a let update_slice_mword_inc w i j w' = @@ -425,7 +493,7 @@ let update_slice_mword is_inc w i j w' = if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w' val access_mword_dec : forall 'a. mword 'a -> integer -> bitU -let access_mword_dec w n = bitU_of_bool (getBit w (natFromInteger n)) +let access_mword_dec w n = bitU_of_bool (getBit w (nat_of_int n)) val access_mword_inc : forall 'a. mword 'a -> integer -> bitU let access_mword_inc w n = @@ -436,22 +504,19 @@ val access_mword : forall 'a. bool -> mword 'a -> integer -> bitU let access_mword is_inc w n = if is_inc then access_mword_inc w n else access_mword_dec w n -val update_mword_dec : forall 'a. mword 'a -> integer -> bitU -> mword 'a -let update_mword_dec w n b = setBit w (natFromInteger n) (bool_of_bitU b) +val update_mword_bool_dec : forall 'a. mword 'a -> integer -> bool -> mword 'a +let update_mword_bool_dec w n b = setBit w (nat_of_int n) b +let update_mword_dec w n b = Maybe.map (update_mword_bool_dec w n) (bool_of_bitU b) -val update_mword_inc : forall 'a. mword 'a -> integer -> bitU -> mword 'a -let update_mword_inc w n b = +val update_mword_bool_inc : forall 'a. mword 'a -> integer -> bool -> mword 'a +let update_mword_bool_inc w n b = let top = (length_mword w) - 1 in - update_mword_dec w (top - n) b - -val update_mword : forall 'a. bool -> mword 'a -> integer -> bitU -> mword 'a -let update_mword is_inc w n b = - if is_inc then update_mword_inc w n b else update_mword_dec w n b + update_mword_bool_dec w (top - n) b +let update_mword_inc w n b = Maybe.map (update_mword_bool_inc w n) (bool_of_bitU b) -val mword_of_int : forall 'a. Size 'a => integer -> integer -> mword 'a -let mword_of_int len n = - let w = wordFromInteger n in - if (length_mword w = len) then w else failwith "unexpected word length" +val int_of_mword : forall 'a. bool -> mword 'a -> integer +let int_of_mword sign w = + if sign then signedIntegerFromWord w else unsignedIntegerFromWord w (* Translating between a type level number (itself 'n) and an integer *) @@ -461,68 +526,71 @@ let size_itself_int x = integerFromNat (size_itself x) the actual integer is ignored. *) val make_the_value : forall 'n. integer -> itself 'n -let inline make_the_value x = the_value +let inline make_the_value = (fun _ -> the_value) (*** Bitvectors *) class (Bitvector 'a) val bits_of : 'a -> list bitU - val of_bits : list bitU -> 'a - (* The first parameter specifies the desired length of the bitvector *) - val of_int : integer -> integer -> 'a + (* We allow of_bits to be partial, as not all bitvector representations + support undefined bits *) + val of_bits : list bitU -> maybe 'a + val of_bools : list bool -> 'a val length : 'a -> integer - val unsigned : 'a -> integer - val signed : 'a -> integer - (* The first parameter specifies the indexing order (true is increasing) *) - val get_bit : bool -> 'a -> integer -> bitU - val set_bit : bool -> 'a -> integer -> bitU -> 'a - val get_bits : bool -> 'a -> integer -> integer -> list bitU - val set_bits : bool -> 'a -> integer -> integer -> list bitU -> 'a + (* of_int: the first parameter specifies the desired length of the bitvector *) + val of_int : integer -> integer -> 'a + (* Conversion to integers is undefined if any bit is undefined *) + val unsigned : 'a -> maybe integer + val signed : 'a -> maybe integer + (* Lifting of integer operations to bitvectors: The boolean flag indicates + whether to treat the bitvectors as signed (true) or not (false). *) + val arith_op_bv : (integer -> integer -> integer) -> bool -> 'a -> 'a -> 'a end +val of_bits_failwith : forall 'a. Bitvector 'a => list bitU -> 'a +let of_bits_failwith bits = maybe_failwith (of_bits bits) + +let int_of_bv sign = if sign then signed else unsigned + instance forall 'a. BitU 'a => (Bitvector (list 'a)) let bits_of v = List.map to_bitU v - let of_bits v = List.map of_bitU v + let of_bits v = Just (List.map of_bitU v) + let of_bools v = List.map of_bitU (List.map bitU_of_bool v) let of_int len n = List.map of_bitU (bits_of_int len n) let length = length_list let unsigned v = unsigned_of_bits (List.map to_bitU v) let signed v = signed_of_bits (List.map to_bitU v) - let get_bit is_inc v n = to_bitU (access_list is_inc v n) - let set_bit is_inc v n b = update_list is_inc v n (of_bitU b) - let get_bits is_inc v i j = List.map to_bitU (subrange_list is_inc v i j) - let set_bits is_inc v i j v' = update_subrange_list is_inc v i j (List.map of_bitU v') + let arith_op_bv op sign l r = List.map of_bitU (arith_op_bits op sign (List.map to_bitU l) (List.map to_bitU r)) end instance forall 'a. Size 'a => (Bitvector (mword 'a)) - let bits_of v = List.map to_bitU (bitlistFromWord v) - let of_bits v = wordFromBitlist (List.map of_bitU v) - let of_int = mword_of_int + let bits_of v = List.map bitU_of_bool (bitlistFromWord v) + let of_bits v = Maybe.map wordFromBitlist (just_list (List.map bool_of_bitU v)) + let of_bools v = wordFromBitlist v + let of_int = (fun _ n -> wordFromInteger n) let length v = integerFromNat (word_length v) - let unsigned = unsignedIntegerFromWord - let signed = signedIntegerFromWord - let get_bit = access_mword - let set_bit = update_mword - let get_bits is_inc v i j = get_bits is_inc (bitlistFromWord v) i j - let set_bits is_inc v i j v' = wordFromBitlist (set_bits is_inc (bitlistFromWord v) i j v') + let unsigned v = Just (unsignedIntegerFromWord v) + let signed v = Just (signedIntegerFromWord v) + let arith_op_bv op sign l r = wordFromInteger (op (int_of_mword sign l) (int_of_mword sign r)) end -let access_bv_inc v n = get_bit true v n -let access_bv_dec v n = get_bit false v n +let access_bv_inc v n = access_list true (bits_of v) n +let access_bv_dec v n = access_list false (bits_of v) n -let update_bv_inc v n b = set_bit true v n b -let update_bv_dec v n b = set_bit false v n b +let update_bv_inc v n b = update_list true (bits_of v) n b +let update_bv_dec v n b = update_list false (bits_of v) n b -let subrange_bv_inc v i j = of_bits (get_bits true v i j) -let subrange_bv_dec v i j = of_bits (get_bits false v i j) +let subrange_bv_inc v i j = subrange_list true (bits_of v) i j +let subrange_bv_dec v i j = subrange_list false (bits_of v) i j -let update_subrange_bv_inc v i j v' = set_bits true v i j (bits_of v') -let update_subrange_bv_dec v i j v' = set_bits false v i j (bits_of v') +let update_subrange_bv_inc v i j v' = update_subrange_list true (bits_of v) i j (bits_of v') +let update_subrange_bv_dec v i j v' = update_subrange_list false (bits_of v) i j (bits_of v') -val extz_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b -let extz_bv n v = of_bits (extz_bits n (bits_of v)) +val extz_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU +let extz_bv n v = extz_bits n (bits_of v) -val exts_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b -let exts_bv n v = of_bits (exts_bits n (bits_of v)) +val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU +let exts_bv n v = exts_bits n (bits_of v) val string_of_bv : forall 'a. Bitvector 'a => 'a -> string let string_of_bv v = show_bitlist (bits_of v) @@ -543,8 +611,8 @@ 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 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 bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> list bitU +let bits_of_bytes bs = List.concat (List.map bits_of bs) let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs) let bits_of_mem_bytes bs = bits_of_bytes (List.reverse bs) @@ -596,9 +664,6 @@ let rec reverse_endianness_list bits = if List.length bits <= 8 then bits else reverse_endianness_list (drop_list 8 bits) ++ take_list 8 bits -val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a -let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v)) - (*** Registers *) @@ -760,10 +825,10 @@ let internal_mem_value bytes = val foreach : forall 'a 'vars. (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars let rec foreach l vars body = -match l with -| [] -> vars -| (x :: xs) -> foreach xs (body x vars) body -end + match l with + | [] -> vars + | (x :: xs) -> foreach xs (body x vars) body + end declare {isabelle} termination_argument foreach = automatic @@ -783,13 +848,6 @@ let rec until vars cond body = if cond vars then vars else until (body vars) cond body -let assert' b msg_opt = - let msg = match msg_opt with - | Just msg -> msg - | Nothing -> "unspecified error" - end in - if b then () else failwith msg - (* convert numbers unsafely to naturals *) class (ToNatural 'a) val toNatural : 'a -> natural end diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 9fcbd5ce..8253b800 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -120,14 +120,21 @@ let try_catchSR m h = | Right e -> h e end) +val maybe_failS : forall 'regs 'a 'e. string -> maybe 'a -> monadS 'regs 'a 'e +let maybe_failS msg = function + | Just a -> returnS a + | Nothing -> failS msg +end + val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e let read_tagS addr = - readS (fun s -> fromMaybe B0 (Map.lookup (unsigned addr) s.tagstate)) + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> + readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate))) (* Read bytes from memory and return in little endian order *) val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e let read_mem_bytesS read_kind addr sz = - let addr = unsigned addr in + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> let sz = integerFromNat sz in let addrs = index_list addr (addr+sz-1) 1 in let read_byte s addr = Map.lookup addr s.memstate in @@ -139,12 +146,12 @@ let read_mem_bytesS read_kind addr sz = else s) >>$ returnS mem_val | Nothing -> failS "read_memS" - end) + end)) val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e let read_memS rk a sz = - read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes -> - returnS (bits_of_mem_bytes bytes)) + read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes -> + maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))) val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e let excl_resultS () = @@ -154,9 +161,9 @@ let excl_resultS () = val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e let write_mem_eaS write_kind addr sz = - let addr = unsigned addr in + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> let sz = integerFromNat sz in - updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>) + updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)) (* Write little-endian list of bytes to previously announced address *) val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e @@ -181,9 +188,9 @@ end val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e let write_tagS addr t = - (*let taddr = addr / cap_alignment in*) - updateS (fun s -> <| s with tagstate = Map.insert (unsigned addr) t s.tagstate |>) >>$ - returnS true + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> + updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$ + returnS true) val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e let read_regS reg = readS (fun s -> reg.read_from s.regstate) diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 254af4d7..d223b07a 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -102,8 +102,8 @@ let doc_effect (BE_aux (e,_)) = | BE_wmem -> "wmem" | BE_wmv -> "wmv" | BE_wmvt -> "wmvt" - | BE_lset -> "lset" - | BE_lret -> "lret" + (*| BE_lset -> "lset" + | BE_lret -> "lret"*) | BE_eamem -> "eamem" | BE_exmem -> "exmem" | BE_barr -> "barr" diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index d347c1bd..eb9feee3 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -148,14 +148,16 @@ let simple_num l n = E_aux ( simple_annot (Parse_ast.Generated l) (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l)))) -let effectful_set = - List.exists +let effectful_set = function + | [] -> false + | _ -> true + (*List.exists (fun (BE_aux (eff,_)) -> match eff with | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet | BE_escape -> true - | _ -> false) + | _ -> false)*) let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs @@ -362,7 +364,7 @@ let doc_lit_lem (L_aux(lit,l)) = | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> - utf8string "(failwith \"undefined value of unsupported type\")" + utf8string "(return (failwith \"undefined value of unsupported type\"))" | L_string s -> utf8string ("\"" ^ s ^ "\"") | L_real s -> (* Lem does not support decimal syntax, so we translate a string @@ -790,7 +792,7 @@ let doc_exp_lem, doc_let_lem = let epp = brackets expspp in let (epp,aexp_needed) = if is_bit_typ etyp && !opt_mwords then - let bepp = string "of_bits" ^^ space ^^ parens (align epp) in + let bepp = string "of_bits_failwith" ^^ space ^^ parens (align epp) in (bepp ^^ doc_tannot_lem ctxt (env_of full_exp) false t, true) else (epp,aexp_needed) in if aexp_needed then parens (align epp) else epp diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 559c1116..228ddbb8 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -182,8 +182,8 @@ and pp_format_base_effect_lem (BE_aux(e,l)) = | BE_undef -> "BE_undef" | BE_unspec -> "BE_unspec" | BE_nondet -> "BE_nondet" - | BE_lset -> "BE_lset" - | BE_lret -> "BE_lret" + (*| BE_lset -> "BE_lset" + | BE_lret -> "BE_lret"*) | BE_escape -> "BE_escape") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_effects_lem (Effect_aux(e,l)) = diff --git a/src/rewrites.ml b/src/rewrites.ml index 30230710..6e98abb0 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -95,13 +95,13 @@ let simple_num l n = E_aux ( (atom_typ (Nexp_aux (Nexp_constant n, gen_loc l)))) let effectful_effs = function - | Effect_aux (Effect_set effs, _) -> - List.exists + | Effect_aux (Effect_set effs, _) -> not (effs = []) + (*List.exists (fun (BE_aux (be,_)) -> match be with | BE_nondet | BE_unspec | BE_undef | BE_lset -> false | _ -> true - ) effs + ) effs*) let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux)) let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp)) @@ -214,6 +214,26 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = rewrite_typ +let rewrite_bitvector_exps defs = + let e_aux = function + | (E_vector es, ((l, Some (env, typ, eff)) as a)) when is_bitvector_typ typ -> + begin + try + let len = mk_lit_exp (L_num (Big_int.of_int (List.length es))) in + let es = mk_exp (E_list (List.map strip_exp es)) in + let exp = mk_exp (E_app (mk_id "bitvector_of_bitlist", [len; es])) in + check_exp env exp typ + with + | _ -> E_aux (E_vector es, a) + end + | (e_aux, a) -> E_aux (e_aux, a) + in + let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in + if IdSet.mem (mk_id "bitvector_of_bitlist") (Initial_check.val_spec_ids defs) then + rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } defs + else defs + + (* Re-write trivial sizeof expressions - trivial meaning that the value of the sizeof can be directly inferred from the type variables in scope. *) @@ -1555,7 +1575,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f (strip_exp (E_aux (E_var(le', e', block), annot))) (typ_of full_exp) | _ -> rewrite_base full_exp -let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) = +(*let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) = let rewrap le = LEXP_aux(le,annot) in let rewrite_base = rewrite_lexp rewriters in match lexp, annot with @@ -1564,14 +1584,14 @@ let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) = | Unbound | Local _ -> LEXP_aux (lexp, (l, Some (env, typ, union_effects eff (mk_effect [BE_lset])))) | _ -> rewrap lexp) - | _ -> rewrite_base le + | _ -> rewrite_base le*) let rewrite_defs_exp_lift_assign defs = rewrite_defs_base {rewrite_exp = rewrite_exp_lift_assign_intro; rewrite_pat = rewrite_pat; rewrite_let = rewrite_let; - rewrite_lexp = rewrite_lexp_lift_assign_intro; + rewrite_lexp = rewrite_lexp (*_lift_assign_intro*); rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; rewrite_defs = rewrite_defs_base} defs @@ -3075,6 +3095,7 @@ let rewrite_defs_lem = [ ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("guarded_pats", rewrite_defs_guarded_pats); + ("bitvector_exps", rewrite_bitvector_exps); (* ("register_ref_writes", rewrite_register_ref_writes); *) ("fix_val_specs", rewrite_fix_val_specs); ("split_execute", rewrite_split_fun_constr_pats "execute"); |