diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 3 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 6 | ||||
| -rw-r--r-- | src/rewrites.ml | 52 | ||||
| -rw-r--r-- | src/sail_lib.ml | 4 |
4 files changed, 52 insertions, 13 deletions
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index 9b81e233..edba83ba 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -220,6 +220,9 @@ let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate (bitU_of_bool b) n)) +val reverse_endianness : list bitU -> list bitU +let reverse_endianness v = reverse_endianness_list v + val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool val ult_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 ea7c11cf..e87f4b7c 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -5,9 +5,6 @@ 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 @@ -233,6 +230,9 @@ let duplicate_fail b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_b 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 reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a +let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v)) + val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool diff --git a/src/rewrites.ml b/src/rewrites.ml index 6e98abb0..fbaf1234 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -174,14 +174,50 @@ let find_updated_vars exp = fst (fold_exp { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp) +let lookup_equal_kids env = + let get_eq_kids kid eqs = match KBindings.find_opt kid eqs with + | Some kids -> kids + | None -> KidSet.singleton kid + in + let add_eq_kids kid1 kid2 eqs = + let kids = KidSet.union (get_eq_kids kid2 eqs) (get_eq_kids kid1 eqs) in + eqs + |> KBindings.add kid1 kids + |> KBindings.add kid2 kids + in + let add_nc eqs = function + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _) -> + add_eq_kids kid1 kid2 eqs + | _ -> eqs + in + List.fold_left add_nc KBindings.empty (Env.get_constraints env) + +let lookup_constant_kid env kid = + match KBindings.find_opt kid (lookup_equal_kids env) with + | Some kids -> + let check_nc const nc = match const, nc with + | None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _) + when KidSet.mem kid kids -> + Some i + | _, _ -> const + in + List.fold_left check_nc None (Env.get_constraints env) + | None -> None + let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with -| Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env) -| Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l) -| Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l) -| Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l) -| Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l) -| Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l) -| _ -> nexp_aux + | Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env) + | Nexp_var kid -> + begin + match lookup_constant_kid env kid with + | Some i -> nconstant i + | None -> nexp_aux + end + | Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l) + | Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l) + | Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l) + | Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l) + | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l) + | _ -> nexp_aux let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with @@ -3097,6 +3133,7 @@ let rewrite_defs_lem = [ ("guarded_pats", rewrite_defs_guarded_pats); ("bitvector_exps", rewrite_bitvector_exps); (* ("register_ref_writes", rewrite_register_ref_writes); *) + ("nexp_ids", rewrite_defs_nexp_ids); ("fix_val_specs", rewrite_fix_val_specs); ("split_execute", rewrite_split_fun_constr_pats "execute"); ("recheck_defs", recheck_defs); @@ -3107,7 +3144,6 @@ let rewrite_defs_lem = [ ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); ("early_return", rewrite_defs_early_return); - ("nexp_ids", rewrite_defs_nexp_ids); ("fix_val_specs", rewrite_fix_val_specs); ("remove_blocks", rewrite_defs_remove_blocks); ("letbind_effects", rewrite_defs_letbind_effects); diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 76dec253..96baa279 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -437,11 +437,11 @@ let read_ram (addr_size, data_size, hex_ram, addr) = let tag_ram : bool RAM.t = RAM.create 256 -let write_tag (addr, tag) = +let write_tag_bool (addr, tag) = let addri = uint addr in RAM.add tag_ram addri tag -let read_tag addr = +let read_tag_bool addr = let addri = uint addr in try RAM.find tag_ram addri with Not_found -> false |