From 99fdb2e003b7433dc06372d2ffebd6d5111ce46d Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Thu, 6 Oct 2016 17:23:28 +0100 Subject: move type definitions that both interpreter and shallow embedding use to sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome --- src/gen_lib/armv8_extras.lem | 76 +++++++---- src/gen_lib/power_extras.lem | 72 +++++----- src/gen_lib/prompt.lem | 307 +++++++++++++------------------------------ src/gen_lib/sail_values.lem | 98 ++++++++++++-- src/gen_lib/state.lem | 45 +++---- src/gen_lib/vector.lem | 8 +- 6 files changed, 289 insertions(+), 317 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem index fd0fc17b..abab2163 100644 --- a/src/gen_lib/armv8_extras.lem +++ b/src/gen_lib/armv8_extras.lem @@ -1,31 +1,53 @@ open import Pervasives -open import State +open import Sail_impl_base +open import Vector open import Sail_values +open import Prompt -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 >> return () -let wMem_Val_ATOMIC (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return Vector.O - -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 () +val rMem_NORMAL : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) +val rMem_STREAM : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) +val rMem_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) +val rMem_ATOMICL : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) +val rMem_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) + +let rMem_NORMAL (addr,size) = read_memory Read_plain addr size +let rMem_STREAM (addr,size) = read_memory Read_stream addr size +let rMem_ORDERED (addr,size) = read_memory Read_acquire addr size +let rMem_ATOMIC (addr,size) = read_memory Read_exclusive addr size +let rMem_ATOMIC_ORDERED (addr,size) = read_memory Read_exclusive_acquire addr size + +val wMem_Addr_NORMAL : forall 'e. (vector bitU * integer) -> M 'e unit +val wMem_Addr_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit +val wMem_Addr_ATOMIC : forall 'e. (vector bitU * integer) -> M 'e unit +val wMem_Addr_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit + +let wMem_Addr_NORMAL (addr,size) = write_memory_ea Write_plain addr size +let wMem_Addr_ORDERED (addr,size) = write_memory_ea Write_release addr size +let wMem_Addr_ATOMIC (addr,size) = write_memory_ea Write_exclusive addr size +let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_memory_ea Write_exclusive_release addr size + + +val wMem_Val_NORMAL : forall 'e. (integer * vector bitU) -> M 'e unit +val wMem_Val_ATOMIC : forall 'e. (integer * vector bitU) -> M 'e bitU + +let wMem_Val_NORMAL (_,v) = write_memory_val v >>= fun _ -> return () +(* in ARM the status returned is inversed *) +let wMem_Val_ATOMIC (_,v) = write_memory_val v >>= fun b -> return (if b then O else I) + + +val DataMemoryBarrier_Reads : forall 'e. unit -> M 'e unit +val DataMemoryBarrier_Writes : forall 'e. unit -> M 'e unit +val DataMemoryBarrier_All : forall 'e. unit -> M 'e unit +val DataSynchronizationBarrier_Reads : forall 'e. unit -> M 'e unit +val DataSynchronizationBarrier_Writes : forall 'e. unit -> M 'e unit +val DataSynchronizationBarrier_All : forall 'e. unit -> M 'e unit +val InstructionSynchronizationBarrier : forall 'e. unit -> M 'e unit + +let DataMemoryBarrier_Reads () = barrier DMB_LD +let DataMemoryBarrier_Writes () = barrier DMB_ST +let DataMemoryBarrier_All () = barrier DMB +let DataSynchronizationBarrier_Reads () = barrier DSB_LD +let DataSynchronizationBarrier_Writes () = barrier DSB_ST +let DataSynchronizationBarrier_All () = barrier DSB +let InstructionSynchronizationBarrier () = barrier Isync diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem index e08da230..2e255db7 100644 --- a/src/gen_lib/power_extras.lem +++ b/src/gen_lib/power_extras.lem @@ -1,49 +1,47 @@ open import Pervasives +open import Sail_impl_base open import Vector -open import State open import Sail_values +open import Prompt -(* -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_EA (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 I - -let I_Sync () = return () -let H_Sync () = return () -let LW_Sync () = return () -let EIEIO_Sync () = return () - -let recalculate_dependency () = return () +val MEMr : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) +val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU) + +let MEMr (addr,size) = read_memory Read_plain addr size +let MEMr_reserve (addr,size) = read_memory Read_reserve addr size + + +val MEMw_EA : forall 'e. (vector bitU * integer) -> M 'e unit +val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit + +let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size +let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size + + +val MEMw : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit +val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU + +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 + +let I_Sync () = barrier Isync +let H_Sync () = barrier Sync +let LW_Sync () = barrier LwSync +let EIEIO_Sync () = barrier Eieio + +let recalculate_dependency () = footprint 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 *) -val countLeadingZeroes : vector bit * integer -> integer +val countLeadingZeroes : vector bitU * integer -> integer let countLeadingZeroes (Vector bits _ _ ,n) = let (_,bits) = List.splitAt (natFromInteger n) bits in integerFromNat (List.length (takeWhile ((=) O) bits)) diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index e1e8658e..02a83d8a 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -1,251 +1,134 @@ open import Pervasives_extra +open import Sail_impl_base open import Vector +open import Sail_values 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 '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 * (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 * memory_value * (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 * 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 * (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 'e 'a - - (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of outcome 'e 'a - - (* Request to read register *) - | Read_reg of reg_name * (register_value -> outcome 'e 'a) - - (* Request to write register *) - | 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 unit - - (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally - * provide a handler. *) - | 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 - -type M 'e 'a = outcome 'e 'a - -val return : forall 'e 'a. 'a -> M 'e 'a +val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a let return a = Done a -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 k -> Read_mem rk addr sz (fun v -> (k v) >>= f) - | Write_mem wk addr sz v k -> Write_mem wk addr sz v (fun b -> (k b) >>= f) - | Write_ea wk addr sz k -> Write_ea wk addr sz (k >>= f) - | Write_memv v k -> Write_memv v (fun b -> (k b) >>= f) - | Barrier bk k -> Barrier bk (k >>= f) - | 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 () -> Nondet_choice () - | Escape e -> Escape e - end - -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 - | (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" +val bind : forall 's 'e 'a 'b. outcome 's 'e 'a -> ('a -> outcome 's 'e 'b) -> outcome 's 'e 'b +let rec bind m f = match m with + | Done a -> f a + | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt)) + | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (bind o f,opt)) + | Footprint o_s -> Footprint (let (o,opt) = o_s in (bind o f,opt)) + | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (bind o f,opt)) + | Escape o_s -> Escape o_s end -val bitvFromBytes : list byte -> vector bit -let bitvFromBytes v = Vector (foldl (++) [] v) 0 defaultDir -let dir is_inc = if is_inc then D_increasing else D_decreasing +type M 'e 'a = Sail_impl_base.outcome unit 'e 'a -val bitvFromRegisterValue : register_value -> vector bit -let bitvFromRegisterValue v = - Vector (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing) +let (>>=) = bind +val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b +let (>>) m n = m >>= fun _ -> n -val registerValueFromBitv : vector bit -> register -> register_value -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 exit : forall 'a 'e. 'e -> M 'e 'a +let exit e = Escape (Just (return e,Nothing)) -val read_memory : forall 'e. read_kind -> integer -> integer -> M 'e (vector bit) +val read_memory : forall 'e. read_kind -> vector bitU -> integer -> M 'e (vector bitU) let read_memory rk addr sz = + let addr = address_lifted_of_bitv addr in let sz = natFromInteger sz in - Read_mem rk addr sz (compose Done bitvFromBytes) - -val write_memory : forall 'e. write_kind -> integer -> integer -> vector bit -> M 'e bool -let write_memory wk addr sz (Vector v _ _) = + let k memory_value = + let bitv = bitv_of_byte_lifteds memory_value in + (Done bitv,Nothing) in + Read_mem (rk,addr,sz) k + +val write_memory_ea : forall 'e. write_kind -> vector bitU -> integer -> M 'e unit +let write_memory_ea wk addr sz = + let addr = address_lifted_of_bitv addr in let sz = natFromInteger sz in - Write_mem wk addr sz (byte_chunks sz v) Done + Write_ea (wk,addr,sz) (Done (),Nothing) -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_memory_val : forall 'e. vector bitU -> M 'e bool +let write_memory_val v = + let v = byte_lifteds_of_bitv v in + let k successful = (return successful,Nothing) in + Write_memv v k -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 + +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 - Write_reg reg rv (Done ()) + let k register_value = + let v = bitvFromRegisterValue register_value in + (Done v,Nothing) in + Read_reg reg k -val read_reg_bit : forall 'e. register -> integer -> M 'e bit +val read_reg_bit : forall 'e. register -> integer -> M 'e bitU 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)) + read_reg_range reg i i >>= fun v -> return (access v i) -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 : forall 'e. register -> M 'e (vector bit) +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 - Read_reg reg (compose Done bitvFromRegisterValue) - -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 - let sz = natFromInteger (length_reg reg) in - let reg = Reg (register_to_string reg) start sz (dir defaultDir) in - Write_reg reg rv (Done ()) + 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 bit) +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 - Read_reg reg (compose Done bitvFromRegisterValue) - -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) + 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 bit +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 write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M 'e unit + + +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 + Write_reg (reg,rv) (Done (),Nothing) + +val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit +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 + 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) + +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 foreachM_inc : forall 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars + +val barrier : forall 'e. barrier_kind -> M 'e unit +let barrier bk = Barrier bk (Done (), Nothing) + + +val footprint : forall 'e. M 'e unit +let footprint = Footprint (Done (),Nothing) + + +val foreachM_inc : forall 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars let rec foreachM_inc (i,stop,by) vars body = if i <= stop then @@ -254,8 +137,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return vars -val foreachM_dec : forall 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 'e 'vars) -> M 'e 'vars +val foreachM_dec : forall 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars let rec foreachM_dec (i,stop,by) vars body = if i >= stop then diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 46c3a10c..98b68e1b 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,10 +1,36 @@ open import Pervasives_extra +open import Sail_impl_base open import Vector open import Arch type i = integer type n = natural +let to_bool = function + | O -> false + | I -> true + | Undef -> failwith "to_bool applied to Undef" + end + + +let bit_lifted_of_bitU = function + | O -> Bitl_zero + | I -> Bitl_one + | Undef -> Bitl_undef + end + +let bitU_of_bit = function + | Bitc_zero -> O + | Bitc_one -> I + end + +let bitU_of_bit_lifted = function + | Bitl_zero -> O + | Bitl_one -> I + | Bitl_undef -> Undef + | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" + end + let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs let most_significant = function @@ -27,7 +53,7 @@ let pow m n = m ** (natFromInteger n) let bitwise_not (Vector bs start is_inc) = Vector (List.map bitwise_not_bit bs) start is_inc -val is_one : integer -> bit +val is_one : integer -> bitU let is_one i = if i = 1 then I else O @@ -39,22 +65,22 @@ let bitwise_binop_bit op = function | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y)) end -val bitwise_and_bit : bit * bit -> bit +val bitwise_and_bit : bitU * bitU -> bitU let bitwise_and_bit = bitwise_binop_bit (&&) -val bitwise_or_bit : bit * bit -> bit +val bitwise_or_bit : bitU * bitU -> bitU let bitwise_or_bit = bitwise_binop_bit (||) -val bitwise_xor_bit : bit * bit -> bit +val bitwise_xor_bit : bitU * bitU -> bitU let bitwise_xor_bit = bitwise_binop_bit xor -val (&.) : bit -> bit -> bit +val (&.) : bitU -> bitU -> bitU let (&.) x y = bitwise_and_bit (x,y) -val (|.) : bit -> bit -> bit +val (|.) : bitU -> bitU -> bitU let (|.) x y = bitwise_or_bit (x,y) -val (+.) : bit -> bit -> bit +val (+.) : bitU -> bitU -> bitU let (+.) x y = bitwise_xor_bit (x,y) let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) = @@ -474,7 +500,7 @@ let make_indexed_vector entries default start length = let length = natFromInteger length in Vector (List.foldl replace (replicate length default) entries) start defaultDir -val make_bit_vector_undef : integer -> vector bit +val make_bit_vector_undef : integer -> vector bitU let make_bitvector_undef length = Vector (replicate (natFromInteger length) Undef) 0 true @@ -485,6 +511,55 @@ let mask (n,Vector bits start dir) = Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir +let bit_of_bit_lifted = function + | Bitl_zero -> O + | Bitl_one -> I + | Bitl_undef -> Undef + | _ -> failwith "bit_of_bit_lifted: unexpected Bitl_unknown" +end + +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 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 + +val byte_lifteds_of_bitv : vector bitU -> list byte_lifted +let byte_lifteds_of_bitv (Vector bits length is_inc) = + let bits = List.map bit_lifted_of_bitU bits in + byte_lifteds_of_bit_lifteds bits + +val address_lifted_of_bitv : vector bitU -> address_lifted +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)) + (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; + rv_dir = dir is_inc; + rv_start_internal = start; + rv_start = start+1 - (natFromInteger (length_reg reg)) |> + + + class (ToNatural 'a) @@ -533,4 +608,9 @@ let rec foreach_dec (i,stop,by) vars body = foreach_dec (i - by,stop,by) vars body else vars - +let assert' b msg_opt = + let msg = match msg_opt with + | Just msg -> msg + | Nothing -> "unspecified error" + end in + if to_bool b then failwith msg else () diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 5fc59207..1e7b9db4 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -6,7 +6,7 @@ open import Sail_values (* 'a is result type, 'e is error type *) type State 's 'e 'a = 's -> (either 'a 'e * 's) -type memstate = map integer (list bit) +type memstate = map integer (list bitU) type state = <| regstate : regstate; @@ -39,13 +39,6 @@ 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 - | Nothing -> "unspecified error" - end in - if to_bool b then failwith msg else () - val read_writeEA : forall 'e. unit -> State state 'e (integer * integer) let read_writeEA () s = (Left s.writeEA,s) @@ -61,82 +54,82 @@ let rec byte_chunks n l = | _ -> failwith "byte_chunks not given enough bits" end -val read_regstate : state -> register -> vector bit +val read_regstate : state -> register -> vector bitU let read_regstate s = read_regstate_aux s.regstate -val write_regstate : state -> register -> vector bit -> state +val write_regstate : state -> register -> vector bitU -> state let write_regstate s reg v = <| s with regstate = (write_regstate_aux s.regstate reg v) |> -val read_memstate : memstate -> integer -> list bit +val read_memstate : memstate -> integer -> list bitU let read_memstate s addr = findWithDefault addr (replicate 8 Undef) s -val write_memstate : memstate -> (integer * list bit) -> memstate +val write_memstate : memstate -> (integer * list bitU) -> memstate let write_memstate s (addr,bits) = Map.insert addr bits s -val read_memory : forall 'e. integer -> integer -> State state 'e (vector bit) +val read_memory : forall 'e. integer -> integer -> State state 'e (vector bitU) let read_memory addr l s = let bytes = List.map (compose (read_memstate s.memstate) ((+) addr)) (ints l) in (Left (Vector (foldl (++) [] bytes) 0 defaultDir),s) -val write_memory : forall 'e. integer -> integer -> vector bit -> State state 'e unit +val write_memory : forall 'e. integer -> integer -> vector bitU -> State state 'e unit let write_memory addr l (Vector 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)*) -> State state 'e (vector bit) +val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bitU) let read_reg_range reg i j s = let v = slice (read_regstate s reg) i j in (Left v,s) -val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bit +val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bitU let read_reg_bit reg i s = let v = access (read_regstate s reg) i in (Left v,s) -val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> State state 'e unit +val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bitU -> State state 'e unit let write_reg_range reg i j v s = let v' = update (read_regstate s reg) i j v in let s' = write_regstate s reg v' in (Left (),s') -val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> State state 'e unit +val write_reg_bit : forall 'e. register -> integer (*nat*) -> bitU -> State state 'e unit let write_reg_bit reg i bit s = let v = read_regstate s reg in let v' = update_pos v i bit in let s' = write_regstate s reg v' in (Left (),s') -val read_reg : forall 'e. register -> State state 'e (vector bit) +val read_reg : forall 'e. register -> State state 'e (vector bitU) let read_reg reg s = let v = read_regstate s reg in (Left v,s) -val write_reg : forall 'e. register -> vector bit -> State state 'e unit +val write_reg : forall 'e. register -> vector bitU -> State state 'e unit let write_reg reg v s = let s' = write_regstate s reg v in (Left (),s') -val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit) +val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bitU) let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield) -val write_reg_field : forall 'e. register -> register_field -> vector bit -> State state 'e unit +val write_reg_field : forall 'e. register -> register_field -> vector bitU -> State state 'e unit let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield) -val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bit +val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bitU let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) -val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> State state 'e unit +val write_reg_bitfield : forall 'e. register -> register_bitfield -> bitU -> State state 'e unit let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer -> - vector bit -> State state 'e unit + vector bitU -> State state 'e unit let write_reg_field_range reg rfield i j v = let (i',j') = field_indices rfield in write_reg_range reg i' j' v val write_reg_field_bit : forall 'e. register -> register_field -> integer -> - bit -> State state 'e unit + bitU -> State state 'e unit let write_reg_field_bit reg rfield i v = let (i',_) = field_indices rfield in write_reg_bit reg (i + i') v diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index b2d68132..6acb4aa0 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -1,6 +1,7 @@ open import Pervasives_extra -type bit = O | I | Undef +(* 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 @@ -11,11 +12,6 @@ let rec nth xs (n : integer) = | _ -> 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 (Vector _ s _) = s let length (Vector bs _ _) = integerFromNat (length bs) -- cgit v1.2.3