summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/power_extras.lem8
-rw-r--r--src/gen_lib/prompt.lem68
-rw-r--r--src/gen_lib/sail_values.lem68
-rw-r--r--src/gen_lib/vector.lem4
4 files changed, 92 insertions, 56 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index 2e255db7..c16b197f 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -25,10 +25,10 @@ let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return ()
let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b)
-val I_Sync : forall 'e unit -> M 'e unit
-val H_Sync : forall 'e unit -> M 'e unit
-val LW_Sync : forall 'e unit -> M 'e unit
-val EIEIO_Sync : forall 'e unit -> M 'e unit
+val I_Sync : forall 'e. unit -> M 'e unit
+val H_Sync : forall 'e. unit -> M 'e unit
+val LW_Sync : forall 'e. unit -> M 'e unit
+val EIEIO_Sync : forall 'e. unit -> M 'e unit
let I_Sync () = barrier Isync
let H_Sync () = barrier Sync
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 02a83d8a..412bfbc1 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,7 +2,6 @@ open import Pervasives_extra
open import Sail_impl_base
open import Vector
open import Sail_values
-open import Arch
val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a
let return a = Done a
@@ -55,8 +54,8 @@ let write_memory_val v =
val read_reg_range : forall 'e. register -> integer -> integer -> M 'e (vector bitU)
let read_reg_range reg i j =
let (i,j) = (natFromInteger i,natFromInteger j) in
- let start = natFromInteger (start_index_reg reg) in
- let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+ let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg)
+ (if i<j then (i,j) else (j,i)) in
let k register_value =
let v = bitvFromRegisterValue register_value in
(Done v,Nothing) in
@@ -68,37 +67,34 @@ let read_reg_bit reg i =
val read_reg : forall 'e. register -> M 'e (vector bitU)
let read_reg reg =
- let start = natFromInteger (start_index_reg reg) in
- let sz = natFromInteger (length_reg reg) in
- let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+ let reg = Reg (name_of_reg reg) (start_of_reg_nat reg)
+ (size_of_reg_nat reg) (dir_of_reg reg) in
let k register_value =
let v = bitvFromRegisterValue register_value in
(Done v,Nothing) in
Read_reg reg k
+
val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bitU)
-let read_reg_field reg rfield =
- let (i,j) =
- let (i,j) = field_indices rfield in
- (natFromInteger i,natFromInteger j) in
- let start = natFromInteger (start_index_reg reg) in
- let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+let read_reg_field reg regfield =
+ let (i,j) = register_field_indices_nat reg regfield in
+ let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg)
+ (if i<j then (i,j) else (j,i)) in
let k register_value =
let v = bitvFromRegisterValue register_value in
(Done v,Nothing) in
Read_reg reg k
-val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bitU
-let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
-
+val read_reg_bitfield : forall 'e. register -> register_field -> M 'e bitU
+let read_reg_bitfield reg rbit =
+ read_reg_bit reg (fst (register_field_indices reg rbit))
val write_reg_range : forall 'e. register -> integer -> integer -> vector bitU -> M 'e unit
let write_reg_range reg i j v =
let rv = registerValueFromBitv v reg in
- let start = natFromInteger (start_index_reg reg) in
let (i,j) = (natFromInteger i,natFromInteger j) in
- let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+ let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg) (i,j) in
Write_reg (reg,rv) (Done (),Nothing)
val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit
@@ -107,16 +103,17 @@ let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true)
val write_reg : forall 'e. register -> vector bitU -> M 'e unit
let write_reg reg v =
let rv = registerValueFromBitv v reg in
- let start = natFromInteger (start_index_reg reg) in
- let sz = natFromInteger (length_reg reg) in
- let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+ let reg = Reg (name_of_reg reg) (start_of_reg_nat reg)
+ (size_of_reg_nat reg) (dir_of_reg reg) in
Write_reg (reg,rv) (Done (),Nothing)
val write_reg_field : forall 'e. register -> register_field -> vector bitU -> M 'e unit
-let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
+let write_reg_field reg regfield =
+ uncurry (write_reg_range reg) (register_field_indices reg regfield)
-val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> M 'e unit
-let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
+val write_reg_bitfield : forall 'e. register -> register_field -> bitU -> M 'e unit
+let write_reg_bitfield reg rbit =
+ write_reg_bit reg (fst (register_field_indices reg rbit))
val barrier : forall 'e. barrier_kind -> M 'e unit
@@ -146,14 +143,23 @@ let rec foreachM_dec (i,stop,by) vars body =
foreachM_dec (i - by,stop,by) vars body
else return vars
-
let write_two_regs r1 r2 vec =
- let size = length_reg r1 in
- let start = get_start vec in
- let vsize = length vec in
- let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in
+ let is_inc =
+ let is_inc_r1 = is_inc_of_reg r1 in
+ let is_inc_r2 = is_inc_of_reg r2 in
+ let () = ensure (is_inc_r1 = is_inc_r2)
+ "write_two_regs called with vectors of different direction" in
+ is_inc_r1 in
+
+ let (size_r1 : integer) = size_of_reg r1 in
+ let (start_vec : integer) = get_start vec in
+ let size_vec = length vec in
+ let r1_v =
+ if is_inc
+ then slice vec start_vec (size_r1 - start_vec - 1)
+ else slice vec start_vec (start_vec - size_r1 - 1) in
let r2_v =
- (slice vec)
- (if defaultDir then size - start else start - size)
- (if defaultDir then vsize - start else start - vsize) in
+ if is_inc
+ then slice vec (size_r1 - start_vec) (size_vec - start_vec)
+ else slice vec (start_vec - size_r1) (start_vec - size_vec) in
write_reg r1 r1_v >> write_reg r2 r2_v
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 98b68e1b..9307ef80 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,11 +1,48 @@
open import Pervasives_extra
open import Sail_impl_base
open import Vector
-open import Arch
type i = integer
type n = natural
+type bitU = O | I | Undef
+
+
+type register_field = string
+type register_field_index = string * (integer * integer) (* name, start and end *)
+
+type register =
+ | Register of string * (* name *)
+ integer * (* length *)
+ integer * (* start index *)
+ bool * (* is increasing *)
+ list register_field_index
+ | UndefinedRegister of integer (* length *)
+ | RegisterPair of register * register
+
+let dir is_inc = if is_inc then D_increasing else D_decreasing
+
+let name_of_reg (Register name _ _ _ _) = name
+let size_of_reg (Register _ size _ _ _) = size
+let start_of_reg (Register _ _ start _ _) = start
+let is_inc_of_reg (Register _ _ _ is_inc _) = is_inc
+let dir_of_reg (Register _ _ _ is_inc _) = dir is_inc
+
+let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
+let start_of_reg_nat reg = natFromInteger (start_of_reg reg)
+
+
+val register_field_indices : register -> register_field -> integer * integer
+let register_field_indices (Register _ _ _ _ rfields) rfield =
+ match List.lookup rfield rfields with
+ | None -> failwith "Invalid register/register-field combination"
+ | Just indices -> indices
+ end
+
+let register_field_indices_nat reg regfield=
+ let (i,j) = register_field_indices reg regfield in
+ (natFromInteger i,natFromInteger j)
+
let to_bool = function
| O -> false
| I -> true
@@ -147,7 +184,7 @@ let rec divide_by_2 bs (i : integer) (n : integer) =
let rec add_one_bit bs co (i : integer) =
if i < 0 then bs
- else match (nth bs i,co) with
+ else match (List_extra.nth bs (natFromInteger i),co) with
| (O,false) -> replace bs (i,I)
| (O,true) -> add_one_bit (replace bs (i,I)) true (i-1)
| (I,false) -> add_one_bit (replace bs (i,O)) true (i-1)
@@ -178,8 +215,6 @@ let to_vec_undef is_inc (len : integer) =
let to_vec_inc_undef = to_vec_undef true
let to_vec_dec_undef = to_vec_undef false
-
-let get_dir (Vector _ _ ord) = ord
let exts (len, vec) = to_vec (get_dir vec) (len,signed vec)
let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec)
@@ -495,16 +530,16 @@ let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))
-val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> vector 'a
-let make_indexed_vector entries default start length =
+val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
+let make_indexed_vector entries default start length dir =
let length = natFromInteger length in
- Vector (List.foldl replace (replicate length default) entries) start defaultDir
+ Vector (List.foldl replace (replicate length default) entries) start dir
val make_bit_vector_undef : integer -> vector bitU
let make_bitvector_undef length =
Vector (replicate (natFromInteger length) Undef) 0 true
-let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n)
+(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
let mask (n,Vector bits start dir) =
let current_size = List.length bits in
@@ -528,7 +563,8 @@ end
val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> vector bitU
let bitv_of_byte_lifteds v =
- Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 defaultDir
+ Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 true
+
val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
let byte_lifteds_of_bitv (Vector bits length is_inc) =
@@ -540,26 +576,22 @@ let address_lifted_of_bitv v =
Address_lifted (byte_lifteds_of_bitv v) Nothing
-let dir is_inc = if is_inc then D_increasing else D_decreasing
-
-
val bitvFromRegisterValue : register_value -> vector bitU
let bitvFromRegisterValue v =
Vector (List.map bitU_of_bit_lifted v.rv_bits)
- (integerFromNat (v.rv_start))
+ (integerFromNat v.rv_start_internal)
(v.rv_dir = D_increasing)
val registerValueFromBitv : vector bitU -> register -> register_value
let registerValueFromBitv (Vector bits start is_inc) reg =
let start = natFromInteger start in
- <| rv_bits = List.map bit_lifted_of_bitU bits;
+ let bit_lifteds =
+ List.map bit_lifted_of_bitU bits in
+ <| rv_bits = bit_lifteds;
rv_dir = dir is_inc;
rv_start_internal = start;
- rv_start = start+1 - (natFromInteger (length_reg reg)) |>
-
-
-
+ rv_start = if is_inc then start else start+1 - (size_of_reg_nat reg) |>
class (ToNatural 'a)
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 6acb4aa0..07238180 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,8 +1,5 @@
open import Pervasives_extra
-(* this is here to avoid circular dependencies when Sail_values imports Arch.lem *)
-type bitU = O | I | Undef
-
(* element list * start * has increasing direction *)
type vector 'a = Vector of list 'a * integer * bool
@@ -13,6 +10,7 @@ let rec nth xs (n : integer) =
end
+let get_dir (Vector _ _ ord) = ord
let get_start (Vector _ s _) = s
let length (Vector bs _ _) = integerFromNat (length bs)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 14:26:55 +0000