summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/armv8_extras.lem50
-rw-r--r--src/gen_lib/power_extras.lem35
-rw-r--r--src/gen_lib/prompt.lem299
-rw-r--r--src/gen_lib/sail_values.lem20
-rw-r--r--src/gen_lib/state.lem56
-rw-r--r--src/gen_lib/vector.lem22
6 files changed, 462 insertions, 20 deletions
diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem
new file mode 100644
index 00000000..54304225
--- /dev/null
+++ b/src/gen_lib/armv8_extras.lem
@@ -0,0 +1,50 @@
+open import Pervasives
+open import State
+open import Sail_values
+import Set_extra
+
+(*
+let memory_parameter_transformer mode v =
+ let mode = <|mode with endian = E_big_endian|> in
+ match v with
+ | Interp.V_tuple [location;length] ->
+ match length with
+ | Interp.V_lit (L_aux (L_num len) _) ->
+ let (v,regs) = extern_mem_value mode location in
+ (v,(natFromInteger len),regs)
+ | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+ let (v,loc_regs) = extern_mem_value mode location in
+ match loc_regs with
+ | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+ | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+ end
+ end
+ end
+ *)
+let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
+let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
+let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
+let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
+let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l
+
+let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
+let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
+let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
+let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
+
+let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
+let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
+let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
+let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l
+
+let wMem_Val_NORMAL l v = read_writeEA () >>= fun (addr,_) -> write_memory addr l v
+let wMem_Val_ATOMIC l v = read_writeEA () >>= fun (addr,_) -> write_memory addr l v
+
+let DataMemoryBarrier_Reads = return ()
+let DataMemoryBarrier_Writes = return ()
+let DataMemoryBarrier_All = return ()
+let DataSynchronizationBarrier_Reads = return ()
+let DataSynchronizationBarrier_Writes = return ()
+let DataSynchronizationBarrier_All = return ()
+let InstructionSynchronizationBarrier = return ()
+
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
new file mode 100644
index 00000000..f2941aff
--- /dev/null
+++ b/src/gen_lib/power_extras.lem
@@ -0,0 +1,35 @@
+open import Pervasives
+open import State
+open import Sail_values
+
+(*
+let rec countLeadingZeros_helper bits =
+((match bits with
+ | (Interp.V_lit (L_aux( L_zero, _)))::bits ->
+ let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
+ Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
+ | _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
+))
+let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
+ | [Interp.V_track( v, r);Interp.V_track( v2, r2)] ->
+ Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
+ | [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
+ | [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
+ | [Interp.V_unknown;_] -> Interp.V_unknown
+ | [_;Interp.V_unknown] -> Interp.V_unknown
+ | [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] ->
+ countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
+))
+ *)
+
+let MEMr (addr,l) = read_memory (unsigned addr) l
+let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
+
+let MEMw (addr,l,value) = write_memory (unsigned addr) l value
+let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
+
+let I_Sync () = return ()
+let H_Sync () = return ()
+let LW_Sync () = return ()
+let EIEIO_Sync () = return ()
+
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
new file mode 100644
index 00000000..0b616b7e
--- /dev/null
+++ b/src/gen_lib/prompt.lem
@@ -0,0 +1,299 @@
+open import Pervasives_extra
+open import Vector
+open import Arch
+
+let compose f g x = f (g x)
+
+type end_flag =
+ | E_big_endian
+ | E_little_endian
+
+type direction =
+ | D_increasing
+ | D_decreasing
+
+type register_value = <|
+ rv_bits: list bit (* MSB first, smallest index number *);
+ rv_dir: direction;
+ rv_start: nat ;
+ rv_start_internal: nat;
+ (*when dir is increasing, rv_start = rv_start_internal.
+ Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
+ |>
+
+type byte = list bit (* of length 8 *) (*MSB first everywhere*)
+
+type address = integer
+type address_lifted = address
+
+type memory_value = list byte
+(* the list is of length >=1 *)
+(* for both big-endian (Power) and little-endian (ARM), the head of the
+ list is the byte stored at the lowest address *)
+(* for big-endian Power the head of the list is the most-significant
+ byte, in both the interpreter and machineDef* code. *)
+(* For little-endian ARM, the head of the list is the
+ least-significant byte in machineDef* code and the
+ most-significant byte in interpreter code, with the switch over
+ (a list-reverse) being done just inside the interpreter interface*)
+(* In other words, in the machineDef* code the lowest-address byte is first,
+ and in the interpreter code the most-significant byte is first *)
+
+type opcode = Opcode of list byte (* of length 4 *)
+
+type read_kind =
+ (* common reads *)
+ | Read_plain
+ (* Power reads *)
+ | Read_reserve
+ (* AArch64 reads *)
+ | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+
+type write_kind =
+ (* common writes *)
+ | Write_plain
+ (* Power writes *)
+ | Write_conditional
+ (* AArch64 writes *)
+ | Write_release | Write_exclusive | Write_exclusive_release
+
+type barrier_kind =
+ (* Power barriers *)
+ | Sync | LwSync | Eieio | Isync
+ (* AArch64 barriers *)
+ | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB
+
+type slice = (nat * nat)
+
+type reg_name =
+ (* Name of the register, accessing the entire register, the start and size of this register,
+ * and its direction *)
+ | Reg of string * nat * nat * direction
+
+ (* Name of the register, accessing from the bit indexed by the first
+ * to the bit indexed by the second integer of the slice, inclusive. For
+ * machineDef* the first is a smaller number or equal to the second. *)
+ | Reg_slice of string * nat * direction * slice
+
+ (* Name of the register, start and direction, and name of the field of the register
+ * accessed. The slice specifies where this field is in the register*)
+ | Reg_field of string * nat * direction * string * slice
+
+ (* The first four components are as in Reg_field; the final slice
+ * specifies a part of the field, indexed w.r.t. the register as a whole *)
+ | Reg_f_slice of string * nat * direction * string * slice * slice
+
+type outcome 'a =
+ (* Request to read memory, value is location to read followed by registers that location depended
+ * on when mode.track_values, integer is size to read, followed by registers that were used in
+ * computing that size *)
+ (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
+ | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *
+ (memory_value -> outcome 'a)
+
+ (* Request to write memory, first value and dependent registers is location, second is the value
+ * to write *)
+ | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value *
+ maybe (list reg_name) * (bool -> outcome 'a)
+
+ (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
+ | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'a
+
+ (* Request to write memory at last signaled address. Memory value should be 8* the size given in
+ * ea signal *)
+ | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'a)
+
+ (* Request a memory barrier *)
+ (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't
+ * need that *)
+ | Barrier of barrier_kind * outcome 'a
+
+ (* Tell the system to dynamically recalculate dependency footprint *)
+ | Footprint of outcome 'a
+
+ (* Request to read register *)
+ | Read_reg of reg_name * (register_value -> outcome 'a)
+
+ (* Request to write register *)
+ | Write_reg of reg_name * register_value * outcome 'a
+
+ (* List of instruction states to be run in parrallel, any order permitted.
+ Expects concurrency model to choose an order: a permutation of the original list *)
+ | Nondet_choice of list (outcome unit) * (list (outcome unit) -> outcome 'a)
+
+ (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally
+ * provide a handler. *)
+ | Escape (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
+
+ (* Stop for incremental stepping, function can be used to display function call data *)
+ | Done of 'a
+
+type M 'a = outcome 'a
+
+val return : forall 'a. 'a -> M 'a
+let return a = Done a
+
+val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
+let rec bind m f = match m with
+ | Done a -> f a
+ | Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> bind (k v) f)
+ | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> bind (k b) f)
+ | Write_ea wk addr sz rs k -> Write_ea wk addr sz rs (bind k f)
+ | Write_memv v rs k -> Write_memv v rs (fun b -> bind (k b) f)
+ | Barrier bk k -> Barrier bk (bind k f)
+ | Footprint k -> Footprint (bind k f)
+ | Read_reg reg k -> Read_reg reg (fun v -> bind (k v) f)
+ | Write_reg reg v k -> Write_reg reg v (bind k f)
+ | Nondet_choice actions k -> Nondet_choice actions (fun c -> bind (k c) f)
+ | Escape -> Escape
+ end
+
+val exit : forall 'a 'e. 'e -> M 'a
+let exit _ = Escape
+
+let (>>=) = bind
+let (>>) m n = m >>= fun _ -> n
+
+val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
+let rec byte_chunks n list = match (n,list) with
+ | (0,_) -> []
+ | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
+ | _ -> failwith "byte_chunks not given enough bits"
+end
+
+val bitvFromBytes : list byte -> vector bit
+let bitvFromBytes v = V (foldl (++) [] v) 0 defaultDir
+
+let dir is_inc = if is_inc then D_increasing else D_decreasing
+
+val bitvFromRegisterValue : register_value -> vector bit
+let bitvFromRegisterValue v =
+ V (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
+
+val registerValueFromBitv : vector bit -> register -> register_value
+let registerValueFromBitv (V bits start is_inc) reg =
+ let start = natFromInteger start in
+ <| rv_bits = bits;
+ rv_dir = dir is_inc;
+ rv_start_internal = start;
+ rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+
+val read_memory : read_kind -> integer -> integer -> M (vector bit)
+let read_memory rk addr sz =
+ let sz = natFromInteger sz in
+ Read_mem rk addr sz Nothing (compose Done bitvFromBytes)
+
+val write_memory : write_kind -> integer -> integer -> vector bit -> M bool
+let write_memory wk addr sz (V v _ _) =
+ let sz = natFromInteger sz in
+ Write_mem wk addr sz Nothing (byte_chunks sz v) Nothing Done
+
+val read_reg_range : register -> (integer * integer) -> M (vector bit)
+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
+ Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg_range : register -> (integer * integer) -> vector bit -> M 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
+ Write_reg reg rv (Done ())
+
+val read_reg_bit : register -> integer -> M bit
+let read_reg_bit reg i =
+ let i = natFromInteger i in
+ let start = natFromInteger (start_index_reg reg) in
+ let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
+ Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))
+
+val write_reg_bit : register -> integer -> bit -> M unit
+let write_reg_bit reg i bit = write_reg_range reg (i,i) (V [bit] 0 true)
+
+val read_reg : register -> M (vector bit)
+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
+ Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg : register -> vector bit -> M 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
+ Write_reg reg rv (Done ())
+
+val read_reg_field : register -> register_field -> M (vector bit)
+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
+ Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg_field : register -> register_field -> vector bit -> M unit
+let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+
+val read_reg_field_bit : register -> register_field_bit -> M bit
+let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)
+
+val write_reg_field_bit : register -> register_field_bit -> bit -> M unit
+let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit)
+
+val foreach_inc : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+ (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_inc (i,stop,by) vars body =
+ if i <= stop
+ then
+ let (_,vars) = body i vars in
+ foreach_inc (i + by,stop,by) vars body
+ else ((),vars)
+
+val foreach_dec : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+ (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_dec (i,stop,by) vars body =
+ if i >= stop
+ then
+ let (_,vars) = body i vars in
+ foreach_dec (i - by,stop,by) vars body
+ else ((),vars)
+
+
+val foreachM_inc : forall 'vars. (nat * nat * nat) -> 'vars ->
+ (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+let rec foreachM_inc (i,stop,by) vars body =
+ if i <= stop
+ then
+ body i vars >>= fun (_,vars) ->
+ foreachM_inc (i + by,stop,by) vars body
+ else return ((),vars)
+
+
+val foreachM_dec : forall 'vars. (nat * nat * nat) -> 'vars ->
+ (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+let rec foreachM_dec (i,stop,by) vars body =
+ if i >= stop
+ then
+ body i vars >>= fun (_,vars) ->
+ foreachM_dec (i - by,stop,by) vars body
+ else return ((),vars)
+
+
+let length l = integerFromNat (length l)
+
+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 r2_v =
+ (slice vec)
+ (if defaultDir then size - start else start - size)
+ (if defaultDir then vsize - start else start - vsize) 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 aa0578b2..b02e47cb 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,4 +1,4 @@
-open import Pervasives
+open import Pervasives_extra
open import State
open import Vector
open import Arch
@@ -9,7 +9,10 @@ let length l = integerFromNat (length l)
let has_undef (V bs _ _) = List.any (function Undef -> true | _ -> false end) bs
-let most_significant (V bs _ _) = let (b :: _) = bs in b
+let most_significant = function
+ | (V (b :: _) _ _) -> b
+ | _ -> failwith "most_significant applied to empty vector"
+ end
let bitwise_not_bit = function
| I -> O
@@ -57,16 +60,15 @@ let bitwise_or = bitwise_binop (||)
let bitwise_xor = bitwise_binop xor
let unsigned (V bs _ _ as v) : integer =
- match has_undef v with
- | true ->
- fst (List.foldl
- (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)
- end
+ if has_undef v then failwith "unsigned applied to vector with undefined bits" else
+ fst (List.foldl
+ (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)
let signed v : integer =
match most_significant v with
| I -> 0 - (1 + (unsigned (bitwise_not v)))
| O -> unsigned v
+ | _ -> failwith "signed applied to vector with undefined bits"
end
let to_num sign = if sign then signed else unsigned
@@ -114,6 +116,7 @@ let rec add_one_bit bs co (i : integer) =
| (O,true) -> add_one_bit (replace bs (natFromInteger i,I)) true (i-1)
| (I,false) -> add_one_bit (replace bs (natFromInteger i,O)) true (i-1)
| (I,true) -> add_one_bit bs true (i-1)
+ | _ -> failwith "add_one_bit applied to list with undefined bit"
(* | Vundef,_ -> assert false*)
end
@@ -215,7 +218,7 @@ let add_VII = arith_op_vec_range_range integerAdd false
let addS_VII = arith_op_vec_range_range integerAdd true
let minus_VII = arith_op_vec_range_range integerMinus false
-let arith_op_vec_vec_range op sign (V _ _ is_inc as l) r =
+let arith_op_vec_vec_range op sign l r =
let (l',r') = (to_num sign l,to_num sign r) in
op l' r'
@@ -276,6 +279,7 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
let (n,nu,changed) = match r_bit with
| I -> (op l' 1, op l_u 1, true)
| O -> (l',l_u,false)
+ | _ -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
end in
(* | _ -> assert false *)
let correct_size_num = to_vec is_inc (act_size,n) in
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index ac65a347..eeff4717 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,10 +1,26 @@
-open import Pervasives
+open import Pervasives_extra
open import Vector
open import Arch
(* 'a is result type, 'e is error type *)
type M 's 'e 'a = 's -> (either 'a 'e * 's)
+type memstate = map integer (list bit)
+
+type state =
+ <| regstate : regstate;
+ memstate : memstate;
+ writeEA : integer * integer|>
+
+let compose f g x = f (g x)
+
+val ints_aux : list integer -> integer -> list integer
+let rec ints_aux acc x =
+ if x = 0 then []
+ else ints_aux ((x - 1) :: acc) (x - 1)
+
+let ints = ints_aux []
+
val return : forall 's 'e 'a. 'a -> M 's 'e 'a
let return a s = (Left a,s)
@@ -20,6 +36,44 @@ let exit e s = (Right e,s)
let (>>=) = bind
let (>>) m n = m >>= fun _ -> n
+val read_writeEA : forall 'e. unit -> M state 'e (integer * integer)
+let read_writeEA () s = (Left s.writeEA,s)
+
+val write_writeEA : forall 'e. integer -> integer -> M state 'e unit
+let write_writeEA addr l s = (Left (), <| s with writeEA = (addr,l) |>)
+
+val byte_chunks : forall 'a. integer -> list 'a -> list (list 'a)
+let rec byte_chunks n l =
+ if n = 0 then []
+ else
+ match l with
+ | a::b::c::d::e::f::g::h::rest -> [a;b;c;d;e;f;g;h] :: byte_chunks (n - 1) rest
+ | _ -> failwith "byte_chunks not given enough bits"
+ end
+
+val read_regstate : state -> register -> vector bit
+let read_regstate s = read_regstate_aux s.regstate
+
+val write_regstate : state -> register -> vector bit -> state
+let write_regstate s reg v = <| s with regstate = (write_regstate_aux s.regstate reg v) |>
+
+val read_memstate : memstate -> integer -> list bit
+let read_memstate s addr = findWithDefault addr (replicate 8 Undef) s
+
+val write_memstate : memstate -> (integer * list bit) -> memstate
+let write_memstate s (addr,bits) = Map.insert addr bits s
+
+val read_memory : forall 'e. integer -> integer -> M state 'e (vector bit)
+let read_memory addr l s =
+ let bytes = List.map (compose (read_memstate s.memstate) ((+) addr)) (ints l) in
+ (Left (V (foldl (++) [] bytes) 0 defaultDir),s)
+
+val write_memory : forall 'e. integer -> integer -> vector bit -> M state 'e unit
+let write_memory addr l (V bits _ _) s =
+ let addrs = List.map ((+) addr) (ints l) in
+ let bytes = byte_chunks l bits in
+ (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>)
+
val read_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> M state 'e (vector bit)
let read_reg_range reg (i,j) s =
let v = slice (read_regstate s reg) i j in
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 9efae768..ad0ba1db 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,17 +1,18 @@
-open import Pervasives
+open import Pervasives_extra
type bit = O | I | Undef
type vector 'a = V of list 'a * integer * bool
-let rec nth xs (n : integer) = match (n,xs) with
- | (0,x :: xs) -> x
- | (n + 1,x :: xs) -> nth xs n
-end
-
+let rec nth xs (n : integer) =
+ match xs with
+ | x :: xs -> if n = 0 then x else nth xs (n - 1)
+ | _ -> failwith "nth applied to empty list"
+ end
let to_bool = function
| O -> false
| I -> true
+ | Undef -> failwith "to_bool applied to Undef"
end
let get_start (V _ s _) = s
@@ -24,8 +25,10 @@ let rec replace bs ((n : nat),b') = match (n,bs) with
end
let make_indexed_vector_reg entries default start length =
- let (Just v) = default in
- V (List.foldl replace (replicate length v) entries) start
+ match default with
+ | Just v -> V (List.foldl replace (replicate length v) entries) start
+ | Nothing -> failwith "make_indexed_vector used without default value"
+ end
let make_indexed_vector_bit entries default start length =
let default = match default with Nothing -> Undef | Just v -> v end in
@@ -60,9 +63,6 @@ let update (V bs start is_inc) n m (V bs' _ _) =
let start = integerFromNat start in
V (prefix ++ (List.take length bs') ++ suffix) start is_inc
-let hd (x :: _) = x
-
-
val access : forall 'a. vector 'a -> (*nat*) integer -> 'a
let access (V bs start is_inc) n =
if is_inc then nth bs (n - start) else nth bs (start - n)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:26:25 +0000