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.lem6
-rw-r--r--src/gen_lib/prompt.lem105
-rw-r--r--src/gen_lib/sail_values.lem62
-rw-r--r--src/gen_lib/state.lem78
-rw-r--r--src/gen_lib/vector.lem4
5 files changed, 115 insertions, 140 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index b43c6403..e08da230 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -27,10 +27,10 @@ let MEMr (addr,l) = read_memory (unsigned addr) l
let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
-let MEMw_EA_conditional (addr,l) = write_writeEA (unsigned addr) l
+let MEMw_EA_cond (addr,l) = write_writeEA (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 MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return I
let I_Sync () = return ()
let H_Sync () = return ()
@@ -39,7 +39,7 @@ let EIEIO_Sync () = return ()
let recalculate_dependency () = return ()
-let trap () = exit ()
+let trap () = exit "error"
(* this needs to change, but for that we'd have to make the type checker know about trap
* as an effect *)
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 738a0b20..4cd76156 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,4 +1,4 @@
-open import Pervasves_extra
+open import Pervasives_extra
open import Vector
open import Arch
@@ -83,47 +83,47 @@ type reg_name =
* 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 =
+type outcome 'e '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)
+ (memory_value -> outcome 'e '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)
+ maybe (list reg_name) * (bool -> outcome 'e '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
+ | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'e '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)
+ | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'e '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
+ | Barrier of barrier_kind * outcome 'e 'a
(* Tell the system to dynamically recalculate dependency footprint *)
- | Footprint of outcome 'a
+ | Footprint of outcome 'e 'a
(* Request to read register *)
- | Read_reg of reg_name * (register_value -> outcome 'a)
+ | Read_reg of reg_name * (register_value -> outcome 'e 'a)
(* Request to write register *)
- | Write_reg of reg_name * register_value * outcome 'a
+ | Write_reg of reg_name * register_value * outcome 'e '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)
+ | Nondet_choice of unit
(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally
* provide a handler. *)
- | Escape of (outcome unit) (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
+ | Escape of 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
(* Stop for incremental stepping, function can be used to display function call data *)
| Done of 'a
@@ -133,12 +133,7 @@ type M 'e 'a = outcome 'e 'a
val return : forall 'e 'a. 'a -> M 'e 'a
let return a = Done a
-val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
-val (>>>) : forall 'a 'b 'c. ('a -> M 'b) -> ('b -> M 'c) -> ('a -> M 'c)
-
-val (>>) : forall 'b. M unit -> (unit -> M 'b) -> M 'b
-let (>>) m n = m >>= fun _ -> n
-
+val (>>=) : forall 'e 'a 'b. M 'e 'a -> ('a -> M 'e 'b) -> M 'e 'b
let rec (>>=) m f = match m with
| Done a -> f a
| Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> (k v) >>= f)
@@ -149,12 +144,15 @@ let rec (>>=) m f = match m with
| Footprint k -> Footprint (k >>= f)
| Read_reg reg k -> Read_reg reg (fun v -> (k v) >>= f)
| Write_reg reg v k -> Write_reg reg v (k >>= f)
- | Nondet_choice actions k -> Nondet_choice actions (fun c -> (k c) >>= f)
- | Escape -> Escape
+ | Nondet_choice () -> Nondet_choice ()
+ | Escape e -> Escape e
end
-val exit : forall 'a 'e. 'e -> M 'a
-let exit _ = Escape
+val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
+let (>>) m n = m >>= fun _ -> n
+
+val exit : forall 'a 'e. 'e -> M 'e 'a
+let exit = Escape
val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
let rec byte_chunks n list = match (n,list) with
@@ -164,40 +162,40 @@ let rec byte_chunks n list = match (n,list) with
end
val bitvFromBytes : list byte -> vector bit
-let bitvFromBytes v = V (foldl (++) [] v) 0 defaultDir
+let bitvFromBytes v = Vector (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)
+ Vector (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 registerValueFromBitv (Vector 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)
+val read_memory : forall 'e. read_kind -> integer -> integer -> M 'e (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 _ _) =
+val write_memory : forall 'e. write_kind -> integer -> integer -> vector bit -> M 'e bool
+let write_memory wk addr sz (Vector 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)
+val read_reg_range : forall 'e. register -> (integer * integer) -> M 'e (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
+val write_reg_range : forall 'e. register -> (integer * integer) -> vector bit -> 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
@@ -205,24 +203,24 @@ let write_reg_range reg (i,j) v =
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
+val read_reg_bit : forall 'e. register -> integer -> M 'e 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 write_reg_bit : forall 'e. register -> integer -> bit -> M 'e unit
+let write_reg_bit reg i bit = write_reg_range reg (i,i) (Vector [bit] 0 true)
-val read_reg : register -> M (vector bit)
+val read_reg : forall 'e. register -> M 'e (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
+val write_reg : forall 'e. register -> vector bit -> M 'e unit
let write_reg reg v =
let rv = registerValueFromBitv v reg in
let start = natFromInteger (start_index_reg reg) in
@@ -230,7 +228,7 @@ let write_reg reg v =
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)
+val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bit)
let read_reg_field reg rfield =
let (i,j) =
let (i,j) = field_indices rfield in
@@ -239,36 +237,17 @@ let read_reg_field reg rfield =
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
+val write_reg_field : forall 'e. register -> register_field -> vector bit -> M 'e unit
let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
-val read_reg_bitfield : register -> register_bitfield -> M bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bit
let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
-val write_reg_bitfield : register -> register_bitfield -> bit -> M unit
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M 'e unit
let write_reg_bitfield 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)
+val foreachM_inc : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
+ (nat -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
let rec foreachM_inc (i,stop,by) vars body =
if i <= stop
then
@@ -277,8 +256,8 @@ let rec foreachM_inc (i,stop,by) vars body =
else return ((),vars)
-val foreachM_dec : forall 'vars. (nat * nat * nat) -> 'vars ->
- (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+val foreachM_dec : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
+ (nat -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
let rec foreachM_dec (i,stop,by) vars body =
if i >= stop
then
@@ -287,8 +266,6 @@ let rec foreachM_dec (i,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
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 3914bdef..b9a4fbd1 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -3,12 +3,8 @@ open import Vector
open import Arch
type i = integer
-type number = integer
-
type n = natural
-let length l = integerFromNat (length l)
-
let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs
let most_significant = function
@@ -407,10 +403,9 @@ let duplicate (bit,length) =
Vector (List.replicate (natFromInteger length) bit) 0 true
val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs = function
- | 0 -> []
- | n -> xs ++ repeat xs (n-1)
- end
+let rec repeat xs n =
+ if n = 0 then []
+ else xs ++ repeat xs (n-1)
let duplicate_bits (Vector bits start direction,len) =
let bits' = repeat bits len in
@@ -502,25 +497,52 @@ let mask (n,Vector bits start dir) =
-(* this is for a temporary workaround int/nat/integer/natural issues*)
-
-class (subInteger 'a)
- val toInteger : 'a -> integer
+class (ToNatural 'a)
+ val toNatural : 'a -> natural
end
-instance (subInteger integer)
- let toInteger = id
+instance (ToNatural integer)
+ let toNatural = naturalFromInteger
end
-instance (subInteger int)
- let toInteger = integerFromInt
+instance (ToNatural int)
+ let toNatural = naturalFromInt
end
-instance (subInteger nat)
- let toInteger = integerFromNat
+instance (ToNatural nat)
+ let toNatural = naturalFromNat
end
-instance (subInteger natural)
- let toInteger = integerFromNatural
+instance (ToNatural natural)
+ let toNatural = id
end
+
+
+let toNaturalFiveTup (n1,n2,n3,n4,n5) =
+ (toNatural n1,
+ toNatural n2,
+ toNatural n3,
+ toNatural n4,
+ toNatural n5)
+
+
+
+
+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)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 6db45002..51658d6e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,6 +1,7 @@
open import Pervasives_extra
open import Vector
open import Arch
+open import Sail_values
(* 'a is result type, 'e is error type *)
type State 's 'e 'a = 's -> (either 'a 'e * 's)
@@ -21,23 +22,23 @@ let rec ints_aux acc x =
let ints = ints_aux []
+type M 'e 'a = State state 'e 'a
+
val return : forall 's 'e 'a. 'a -> State 's 'e 'a
let return a s = (Left a,s)
-val bind : forall 's 'e 'a 'b. State 's 'e 'a -> ('a -> State 's 'e 'b) -> State 's 'e 'b
-let bind m f s = match m s with
+val (>>=) : forall 's 'e 'a 'b. State 's 'e 'a -> ('a -> State 's 'e 'b) -> State 's 'e 'b
+let (>>=) m f s = match m s with
| (Left a,s') -> f a s'
| (Right error,s') -> (Right error,s')
end
-val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
-let exit e s = (Right e,s)
-
-let (>>=) = bind
-
val (>>): forall 's 'e 'b. State 's 'e unit -> State 's 'e 'b -> State 's 'e 'b
let (>>) m n = m >>= fun _ -> n
+val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
+let exit e s = (Right e,s)
+
let assert' b msg_opt =
let msg = match msg_opt with
| Just msg -> msg
@@ -115,46 +116,6 @@ val write_reg : forall 'e. register -> vector bit -> State state 'e unit
let write_reg reg v s =
let s' = write_regstate s reg v in
(Left (),s')
-
-
-val foreach_inc : forall 's 'e '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 's 'e '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 's 'e 'vars. (integer * integer * integer) -> 'vars ->
- (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (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 's 'e 'vars. (integer * integer * integer) -> 'vars ->
- (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (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)
val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit)
let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield)
@@ -180,10 +141,6 @@ let write_reg_field_bit reg rfield i v =
let (i',_) = field_indices rfield in
write_reg_bit reg (i + i') v
-
-
-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
@@ -200,4 +157,21 @@ let read_two_regs r1 r2 =
read_reg r2 >>= fun v2 ->
return (v1 ^^ v2)
-type M 'e 'a = State state 'e 'a
+val foreachM_inc : forall 'e 'vars. (i * i * i) -> 'vars ->
+ (i -> 'vars -> M 'e (unit * 'vars)) -> M 'e (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 'e 'vars. (i * i * i) -> 'vars ->
+ (i -> 'vars -> M 'e (unit * 'vars)) -> M 'e (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)
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 72c8b584..7c22e3ba 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,6 +1,8 @@
open import Pervasives_extra
type bit = O | I | Undef
+
+(* element list * start * has increasing direction *)
type vector 'a = Vector of list 'a * integer * bool
let rec nth xs (n : integer) =
@@ -16,7 +18,7 @@ let to_bool = function
end
let get_start (Vector _ s _) = s
-let length (Vector bs _ _) = length bs
+let length (Vector bs _ _) = integerFromNat (length bs)
let rec replace bs ((n : integer),b') = match bs with
| [] -> []
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:07:57 +0000