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 +- src/lem_interp/extract.mllib | 1 + src/lem_interp/instruction_extractor.lem | 4 +- src/lem_interp/interp.lem | 1 + src/lem_interp/interp_inter_imp.lem | 55 +- src/lem_interp/interp_interface.lem | 1293 +---------------------------- src/lem_interp/printing_functions.ml | 17 +- src/lem_interp/printing_functions.mli | 1 + src/lem_interp/run_interp_model.ml | 67 +- src/lem_interp/sail_impl_base.lem | 1309 ++++++++++++++++++++++++++++++ src/pretty_print.ml | 8 +- src/process_file.ml | 4 +- 17 files changed, 1710 insertions(+), 1656 deletions(-) create mode 100644 src/lem_interp/sail_impl_base.lem (limited to 'src') 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) diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib index 9aa5f97e..467a15ea 100644 --- a/src/lem_interp/extract.mllib +++ b/src/lem_interp/extract.mllib @@ -1,3 +1,4 @@ +Sail_impl_base Interp_ast Interp_utilities Instruction_extractor diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem index 73845fee..074f3bc4 100644 --- a/src/lem_interp/instruction_extractor.lem +++ b/src/lem_interp/instruction_extractor.lem @@ -2,7 +2,7 @@ open import Interp_ast open import Interp_utilities open import Pervasives -type instr_parm_typ = +type instr_param_typ = | IBit | IBitvector of maybe nat | IRange of maybe nat @@ -10,7 +10,7 @@ type instr_parm_typ = | IOther type instruction_form = -| Instr_form of string * list (string * instr_parm_typ) * list base_effect +| Instr_form of string * list (string * instr_param_typ) * list base_effect | Skipped val extract_instructions : string -> defs tannot -> list instruction_form diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 23d5c021..cbde6e8b 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -7,6 +7,7 @@ open import Show_extra (* for 'show' to convert nat to string) *) open import String_extra (* for chr *) import Assert_extra (*For failwith when partiality is known to be unreachable*) +open import Sail_impl_base open import Interp_ast open import Interp_utilities open import Instruction_extractor diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 483968ca..f4904669 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -2,10 +2,11 @@ import Interp import Interp_lib import Instruction_extractor import Set_extra -open import Interp_ast -open import Interp_interface open import Pervasives open import Assert_extra +open import Interp_ast +open import Sail_impl_base +open import Interp_interface val intern_reg_value : register_value -> Interp.value val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value @@ -126,7 +127,7 @@ let intern_ifield_value direction v = let num_to_bits size kind num = (* num_to_bits needed in src_power_get/trans_sail.gen - rather than reengineer the generation, we include a wrapper here *) - Interp_interface.bit_list_of_integer size num + Sail_impl_base.bit_list_of_integer size num let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = match d with @@ -750,7 +751,7 @@ let rec interp_to_outcome mode context thunk = else Error "Memory address for write is not 64 bits" | _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm) | Interp.Write_memv (Id_aux (Id i) _) address_val write_val -> - (match List.lookup i mem_write_vals with + (match List.lookup i mem_write_vals with | (Just (MV parmf return)) -> let (value, v_tracking) = match (Interp.detaint write_val) with @@ -821,6 +822,52 @@ let interp mode (IState interp_state context) = | (o,_) -> o end +val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit unit +val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit unit +let rec outcome_to_outcome mode = function + | Interp_interface.Read_mem rk addr size _ k -> + Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v)) + | Interp_interface.Write_mem rk addr size _ mv _ k -> + failwith "Write_mem not supported anymore" + | Interp_interface.Write_ea wk addr size _ state -> + Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state) + | Interp_interface.Write_memv _ mv _ k -> + Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v)) + | Interp_interface.Barrier bk state -> + Sail_impl_base.Barrier bk (state_to_outcome_s mode state) + | Interp_interface.Footprint state -> + Sail_impl_base.Footprint (state_to_outcome_s mode state) + | Interp_interface.Read_reg r k -> + Sail_impl_base.Read_reg r (fun v -> state_to_outcome_s mode (k v)) + | Interp_interface.Write_reg r rv state -> + Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state) + | Interp_interface.Nondet_choice _ _ -> + failwith "Nondet_choice not supported yet" + | Interp_interface.Escape maybestate _ -> + Sail_impl_base.Escape (Maybe.map (state_to_outcome_s mode) maybestate) + | Interp_interface.Fail maybestring -> + Sail_impl_base.Fail maybestring + | Interp_interface.Internal maybestring maybeprint state -> + Sail_impl_base.Internal (maybestring,maybeprint) (state_to_outcome_s mode state) + | Interp_interface.Analysis_non_det _ _ -> + failwith "Analysis_non_det outcome returned" + | Interp_interface.Done -> + Sail_impl_base.Done () + | Interp_interface.Error message -> + failwith ("Interpreter error: " ^ message) +end + +and state_to_outcome_s mode state = + let next_outcome' = interp mode state in + let next_outcome = outcome_to_outcome mode next_outcome' in + (next_outcome, Just state) + + +let initial_outcome_s_of_instruction context mode instruction = + let state = instruction_to_istate context instruction in + let initial_outcome' = interp mode state in + (outcome_to_outcome mode initial_outcome',Just state) + (*Update slice potentially here*) let reg_size = function diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 18ec74a2..cf8c51a2 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -12,6 +12,7 @@ and change *) +open import Sail_impl_base import Interp open import Interp_ast open import Pervasives @@ -19,21 +20,6 @@ open import Num open import Assert_extra -(* maybe isn't a member of type Ord - this should be in the Lem standard library*) -instance forall 'a. Ord 'a => (Ord (maybe 'a)) - let compare = maybeCompare compare - let (<) r1 r2 = (maybeCompare compare r1 r2) = LT - let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT - let (>) r1 r2 = (maybeCompare compare r1 r2) = GT - let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT -end - -type word8 = nat (* bounded at a byte, for when lem supports it*) - -type end_flag = - | E_big_endian - | E_little_endian - type interpreter_state = Interp.stack (*Deem abstract*) (* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *) type specification = Interp_ast.defs Interp.tannot (*Deem abstract*) @@ -42,402 +28,7 @@ type interp_mode = <| internal_mode: interpreter_mode; endian: end_flag |> val make_mode : (*eager*) bool -> (*tracking*) bool -> end_flag -> interp_mode val tracking_dependencies : interp_mode -> bool -(** basic values *) - -type bit = - | Bitc_zero - | Bitc_one - -type bit_lifted = - | Bitl_zero - | Bitl_one - | Bitl_undef - | Bitl_unknown - -type direction = - | D_increasing - | D_decreasing - -type register_value = <| - rv_bits: list bit_lifted (* 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_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*) - -type instruction_field_value = list bit - -type byte = Byte of list bit (* of length 8 *) (*MSB first everywhere*) - -type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer -(* for both values of end_flag, MSBy first *) - -type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*) - -type memory_value = list memory_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 *) - - - -(* not sure which of these is more handy yet *) -type address = Address of list byte (* of length 8 *) * integer -(* type address = Address of integer *) - -type opcode = Opcode of list byte (* of length 4 *) - -(** typeclass instantiations *) - -let ~{ocaml} bitCompare (b1:bit) (b2:bit) = - match (b1,b2) with - | (Bitc_zero, Bitc_zero) -> EQ - | (Bitc_one, Bitc_one) -> EQ - | (Bitc_zero, _) -> LT - | (_,_) -> GT - end -let inline {ocaml} bitCompare = defaultCompare - -let ~{ocaml} bitLess b1 b2 = bitCompare b1 b2 = LT -let ~{ocaml} bitLessEq b1 b2 = bitCompare b1 b2 <> GT -let ~{ocaml} bitGreater b1 b2 = bitCompare b1 b2 = GT -let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT - -let inline {ocaml} bitLess = defaultLess -let inline {ocaml} bitLessEq = defaultLessEq -let inline {ocaml} bitGreater = defaultGreater -let inline {ocaml} bitGreaterEq = defaultGreaterEq - -instance (Ord bit) - let compare = bitCompare - let (<) = bitLess - let (<=) = bitLessEq - let (>) = bitGreater - let (>=) = bitGreaterEq -end - -let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) = - match (bl1,bl2) with - | (Bitl_zero, Bitl_zero) -> EQ - | (Bitl_one, Bitl_one) -> EQ - | (Bitl_undef,Bitl_undef) -> EQ - | (Bitl_unknown,Bitl_unknown) -> EQ - | (Bitl_zero,_) -> LT - | (Bitl_one, _) -> LT - | (Bitl_undef, _) -> LT - | (_,_) -> GT - end -let inline {ocaml} bit_liftedCompare = defaultCompare - -let ~{ocaml} bit_liftedLess b1 b2 = bit_liftedCompare b1 b2 = LT -let ~{ocaml} bit_liftedLessEq b1 b2 = bit_liftedCompare b1 b2 <> GT -let ~{ocaml} bit_liftedGreater b1 b2 = bit_liftedCompare b1 b2 = GT -let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT - -let inline {ocaml} bit_liftedLess = defaultLess -let inline {ocaml} bit_liftedLessEq = defaultLessEq -let inline {ocaml} bit_liftedGreater = defaultGreater -let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq - -instance (Ord bit_lifted) - let compare = bit_liftedCompare - let (<) = bit_liftedLess - let (<=) = bit_liftedLessEq - let (>) = bit_liftedGreater - let (>=) = bit_liftedGreaterEq -end - -let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2 -let inline {ocaml} byte_liftedCompare = defaultCompare - -let ~{ocaml} byte_liftedLess b1 b2 = byte_liftedCompare b1 b2 = LT -let ~{ocaml} byte_liftedLessEq b1 b2 = byte_liftedCompare b1 b2 <> GT -let ~{ocaml} byte_liftedGreater b1 b2 = byte_liftedCompare b1 b2 = GT -let ~{ocaml} byte_liftedGreaterEq b1 b2 = byte_liftedCompare b1 b2 <> LT - -let inline {ocaml} byte_liftedLess = defaultLess -let inline {ocaml} byte_liftedLessEq = defaultLessEq -let inline {ocaml} byte_liftedGreater = defaultGreater -let inline {ocaml} byte_liftedGreaterEq = defaultGreaterEq - -instance (Ord byte_lifted) - let compare = byte_liftedCompare - let (<) = byte_liftedLess - let (<=) = byte_liftedLessEq - let (>) = byte_liftedGreater - let (>=) = byte_liftedGreaterEq -end - -let ~{ocaml} byteCompare (Byte b1) (Byte b2) = compare b1 b2 -let inline {ocaml} byteCompare = defaultCompare - -let ~{ocaml} byteLess b1 b2 = byteCompare b1 b2 = LT -let ~{ocaml} byteLessEq b1 b2 = byteCompare b1 b2 <> GT -let ~{ocaml} byteGreater b1 b2 = byteCompare b1 b2 = GT -let ~{ocaml} byteGreaterEq b1 b2 = byteCompare b1 b2 <> LT - -let inline {ocaml} byteLess = defaultLess -let inline {ocaml} byteLessEq = defaultLessEq -let inline {ocaml} byteGreater = defaultGreater -let inline {ocaml} byteGreaterEq = defaultGreaterEq - -instance (Ord byte) - let compare = byteCompare - let (<) = byteLess - let (<=) = byteLessEq - let (>) = byteGreater - let (>=) = byteGreaterEq -end - -let (*~{ocaml}*) addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2 -(*let inline {ocaml} addressCompare = defaultCompare*) - -let ~{ocaml} addressLess b1 b2 = addressCompare b1 b2 = LT -let ~{ocaml} addressLessEq b1 b2 = addressCompare b1 b2 <> GT -let ~{ocaml} addressGreater b1 b2 = addressCompare b1 b2 = GT -let ~{ocaml} addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT - -let inline {ocaml} addressLess = defaultLess -let inline {ocaml} addressLessEq = defaultLessEq -let inline {ocaml} addressGreater = defaultGreater -let inline {ocaml} addressGreaterEq = defaultGreaterEq - -instance (Ord address) - let compare = addressCompare - let (<) = addressLess - let (<=) = addressLessEq - let (>) = addressGreater - let (>=) = addressGreaterEq -end - -let {coq} addressEqual a1 a2 = (addressCompare a1 a2) = EQ -let inline ~{coq} addressEqual = unsafe_structural_equality - -let {coq} addressInequal a1 a2 = not (addressEqual a1 a2) -let inline ~{coq} addressInequal = unsafe_structural_inequality - -instance (Eq address) - let (=) = addressEqual - let (<>) = addressInequal -end - -let ~{ocaml} directionCompare d1 d2 = - match (d1, d2) with - | (D_decreasing, D_increasing) -> GT - | (D_increasing, D_decreasing) -> LT - | _ -> EQ - end -let inline {ocaml} directionCompare = defaultCompare - -let ~{ocaml} directionLess b1 b2 = directionCompare b1 b2 = LT -let ~{ocaml} directionLessEq b1 b2 = directionCompare b1 b2 <> GT -let ~{ocaml} directionGreater b1 b2 = directionCompare b1 b2 = GT -let ~{ocaml} directionGreaterEq b1 b2 = directionCompare b1 b2 <> LT - -let inline {ocaml} directionLess = defaultLess -let inline {ocaml} directionLessEq = defaultLessEq -let inline {ocaml} directionGreater = defaultGreater -let inline {ocaml} directionGreaterEq = defaultGreaterEq -instance (Ord direction) - let compare = directionCompare - let (<) = directionLess - let (<=) = directionLessEq - let (>) = directionGreater - let (>=) = directionGreaterEq -end - -let ~{ocaml} register_valueCompare rv1 rv2 = - compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal) - (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal) -let inline {ocaml} register_valueCompare = defaultCompare - -let ~{ocaml} register_valueLess b1 b2 = register_valueCompare b1 b2 = LT -let ~{ocaml} register_valueLessEq b1 b2 = register_valueCompare b1 b2 <> GT -let ~{ocaml} register_valueGreater b1 b2 = register_valueCompare b1 b2 = GT -let ~{ocaml} register_valueGreaterEq b1 b2 = register_valueCompare b1 b2 <> LT - -let inline {ocaml} register_valueLess = defaultLess -let inline {ocaml} register_valueLessEq = defaultLessEq -let inline {ocaml} register_valueGreater = defaultGreater -let inline {ocaml} register_valueGreaterEq = defaultGreaterEq - -instance (Ord register_value) - let compare = register_valueCompare - let (<) = register_valueLess - let (<=) = register_valueLessEq - let (>) = register_valueGreater - let (>=) = register_valueGreaterEq -end - -let ~{ocaml} address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) = - compare (b1,i1) (b2,i2) -let inline {ocaml} address_liftedCompare = defaultCompare - -let ~{ocaml} address_liftedLess b1 b2 = address_liftedCompare b1 b2 = LT -let ~{ocaml} address_liftedLessEq b1 b2 = address_liftedCompare b1 b2 <> GT -let ~{ocaml} address_liftedGreater b1 b2 = address_liftedCompare b1 b2 = GT -let ~{ocaml} address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT - -let inline {ocaml} address_liftedLess = defaultLess -let inline {ocaml} address_liftedLessEq = defaultLessEq -let inline {ocaml} address_liftedGreater = defaultGreater -let inline {ocaml} address_liftedGreaterEq = defaultGreaterEq - -instance (Ord address_lifted) - let compare = address_liftedCompare - let (<) = address_liftedLess - let (<=) = address_liftedLessEq - let (>) = address_liftedGreater - let (>=) = address_liftedGreaterEq -end - -(* Registers *) -type slice = (nat * nat) - -type reg_name = -| Reg of string * nat * nat * direction -(*Name of the register, accessing the entire register, the start and size of this register, and its direction *) - -| Reg_slice of string * nat * direction * slice -(* 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, adjusted -to reflect the correct span direction in the interpreter side. *) - -| Reg_field of string * nat * direction * string * 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_f_slice of string * nat * direction * string * slice * 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 *) - -let register_base_name : reg_name -> string = function - | Reg s _ _ _ -> s - | Reg_slice s _ _ _ -> s - | Reg_field s _ _ _ _ -> s - | Reg_f_slice s _ _ _ _ _ -> s - end - -let slice_of_reg_name : reg_name -> slice = function - | Reg _ start width D_increasing -> (start, start + width -1) - | Reg _ start width D_decreasing -> (start - width - 1, start) - | Reg_slice _ _ _ sl -> sl - | Reg_field _ _ _ _ sl -> sl - | Reg_f_slice _ _ _ _ _ sl -> sl - end - -let reg_name_non_empty_intersection (r: reg_name) (r': reg_name) : bool = - register_base_name r = register_base_name r' && - let (i1, i2) = slice_of_reg_name r in - let (i1', i2') = slice_of_reg_name r' in - i1' <= i2 && i2' >= i1 - - -let reg_nameCompare r1 r2 = - compare (register_base_name r1,slice_of_reg_name r1) - (register_base_name r2,slice_of_reg_name r2) - -let reg_nameLess b1 b2 = reg_nameCompare b1 b2 = LT -let reg_nameLessEq b1 b2 = reg_nameCompare b1 b2 <> GT -let reg_nameGreater b1 b2 = reg_nameCompare b1 b2 = GT -let reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT - -instance (Ord reg_name) - let compare = reg_nameCompare - let (<) = reg_nameLess - let (<=) = reg_nameLessEq - let (>) = reg_nameGreater - let (>=) = reg_nameGreaterEq -end - -let reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ -let reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2) - -instance (Eq reg_name) - let (=) = reg_nameEqual - let (<>) = reg_nameInequal -end - -instance (SetType reg_name) - let setElemCompare = reg_nameCompare -end - -let direction_of_reg_name r = match r with - | Reg _ _ _ d -> d - | Reg_slice _ _ d _ -> d - | Reg_field _ _ d _ _ -> d - | Reg_f_slice _ _ d _ _ _ -> d - end - -let start_of_reg_name r = match r with - | Reg _ start _ _ -> start - | Reg_slice _ start _ _ -> start - | Reg_field _ start _ _ _ -> start - | Reg_f_slice _ start _ _ _ _ -> start -end - -(* Data structures for building up instructions *) - -type read_kind = - (* common reads *) - Read_plain - | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*) - (* Power reads *) - | Read_reserve - (* AArch64 reads *) - | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream - -instance (Show read_kind) - let show = function - | Read_plain -> "Read_plain" - | Read_tag -> "Read_tag" - | Read_reserve -> "Read_reserve" - | Read_acquire -> "Read_acquire" - | Read_exclusive -> "Read_exclusive" - | Read_exclusive_acquire -> "Read_exclusive_acquire" - | Read_stream -> "Read_stream" - end -end - -type write_kind = - (* common writes *) - Write_plain - | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*) - (* 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 instruction_kind = - | IK_barrier of barrier_kind - | IK_mem_read of read_kind - | IK_mem_write of write_kind -(* SS reinstating cond_branches -at present branches are not distinguished in the instruction_kind; -they just have particular nias (and will be IK_simple *) - | IK_cond_branch -(* | IK_uncond_branch *) - | IK_simple (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) type external_functions = list (string * (Interp.value -> Interp.value)) @@ -485,7 +76,7 @@ type outcome = (* List of instruciton states to be run in parrallel, any order permitted *) | Nondet_choice of list instruction_state * instruction_state (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler - The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp*) + The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp *) | Escape of maybe instruction_state * instruction_state (*Result of a failed assert with possible error message to report*) | Fail of maybe string @@ -511,277 +102,6 @@ type event = | E_escape | E_error of string -(* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*) - -let ~{ocaml} read_kindCompare rk1 rk2 = - match (rk1, rk2) with - | (Read_plain, Read_plain) -> EQ - | (Read_plain, Read_reserve) -> LT - | (Read_plain, Read_acquire) -> LT - | (Read_plain, Read_exclusive) -> LT - | (Read_plain, Read_exclusive_acquire) -> LT - | (Read_plain, Read_stream) -> LT - - | (Read_reserve, Read_plain) -> GT - | (Read_reserve, Read_reserve) -> EQ - | (Read_reserve, Read_acquire) -> LT - | (Read_reserve, Read_exclusive) -> LT - | (Read_reserve, Read_exclusive_acquire) -> LT - | (Read_reserve, Read_stream) -> LT - - | (Read_acquire, Read_plain) -> GT - | (Read_acquire, Read_reserve) -> GT - | (Read_acquire, Read_acquire) -> EQ - | (Read_acquire, Read_exclusive) -> LT - | (Read_acquire, Read_exclusive_acquire) -> LT - | (Read_acquire, Read_stream) -> LT - - | (Read_exclusive, Read_plain) -> GT - | (Read_exclusive, Read_reserve) -> GT - | (Read_exclusive, Read_acquire) -> GT - | (Read_exclusive, Read_exclusive) -> EQ - | (Read_exclusive, Read_exclusive_acquire) -> LT - | (Read_exclusive, Read_stream) -> LT - - | (Read_exclusive_acquire, Read_plain) -> GT - | (Read_exclusive_acquire, Read_reserve) -> GT - | (Read_exclusive_acquire, Read_acquire) -> GT - | (Read_exclusive_acquire, Read_exclusive) -> GT - | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ - | (Read_exclusive_acquire, Read_stream) -> GT - - | (Read_stream, Read_plain) -> GT - | (Read_stream, Read_reserve) -> GT - | (Read_stream, Read_acquire) -> GT - | (Read_stream, Read_exclusive) -> GT - | (Read_stream, Read_exclusive_acquire) -> GT - | (Read_stream, Read_stream) -> EQ - end -let inline {ocaml} read_kindCompare = defaultCompare - -let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT -let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT -let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT -let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT - -let inline {ocaml} read_kindLess = defaultLess -let inline {ocaml} read_kindLessEq = defaultLessEq -let inline {ocaml} read_kindGreater = defaultGreater -let inline {ocaml} read_kindGreaterEq = defaultGreaterEq - -instance (Ord read_kind) - let compare = read_kindCompare - let (<) = read_kindLess - let (<=) = read_kindLessEq - let (>) = read_kindGreater - let (>=) = read_kindGreaterEq -end - -let ~{ocaml} write_kindCompare wk1 wk2 = - match (wk1, wk2) with - | (Write_plain, Write_plain) -> EQ - | (Write_plain, Write_conditional) -> LT - | (Write_plain, Write_release) -> LT - | (Write_plain, Write_exclusive) -> LT - | (Write_plain, Write_exclusive_release) -> LT - - | (Write_conditional, Write_plain) -> GT - | (Write_conditional, Write_conditional) -> EQ - | (Write_conditional, Write_release) -> LT - | (Write_conditional, Write_exclusive) -> LT - | (Write_conditional, Write_exclusive_release) -> LT - - | (Write_release, Write_plain) -> GT - | (Write_release, Write_conditional) -> GT - | (Write_release, Write_release) -> EQ - | (Write_release, Write_exclusive) -> LT - | (Write_release, Write_exclusive_release) -> LT - - | (Write_exclusive, Write_plain) -> GT - | (Write_exclusive, Write_conditional) -> GT - | (Write_exclusive, Write_release) -> GT - | (Write_exclusive, Write_exclusive) -> EQ - | (Write_exclusive, Write_exclusive_release) -> LT - - | (Write_exclusive_release, Write_plain) -> GT - | (Write_exclusive_release, Write_conditional) -> GT - | (Write_exclusive_release, Write_release) -> GT - | (Write_exclusive_release, Write_exclusive) -> GT - | (Write_exclusive_release, Write_exclusive_release) -> EQ - end -let inline {ocaml} write_kindCompare = defaultCompare - -let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT -let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT -let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT -let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT - -let inline {ocaml} write_kindLess = defaultLess -let inline {ocaml} write_kindLessEq = defaultLessEq -let inline {ocaml} write_kindGreater = defaultGreater -let inline {ocaml} write_kindGreaterEq = defaultGreaterEq - -instance (Ord write_kind) - let compare = write_kindCompare - let (<) = write_kindLess - let (<=) = write_kindLessEq - let (>) = write_kindGreater - let (>=) = write_kindGreaterEq -end - -let ~{ocaml} barrier_kindCompare bk1 bk2 = - match (bk1, bk2) with - | (Sync, Sync) -> EQ - | (Sync, LwSync) -> LT - | (Sync, Eieio) -> LT - | (Sync, Isync) -> LT - | (Sync, DMB) -> LT - | (Sync, DMB_ST) -> LT - | (Sync, DMB_LD) -> LT - | (Sync, DSB) -> LT - | (Sync, DSB_ST) -> LT - | (Sync, DSB_LD) -> LT - | (Sync, ISB) -> LT - - | (LwSync, Sync) -> GT - | (LwSync, LwSync) -> EQ - | (LwSync, Eieio) -> LT - | (LwSync, Isync) -> LT - | (LwSync, DMB) -> LT - | (LwSync, DMB_ST) -> LT - | (LwSync, DMB_LD) -> LT - | (LwSync, DSB) -> LT - | (LwSync, DSB_ST) -> LT - | (LwSync, DSB_LD) -> LT - | (LwSync, ISB) -> LT - - | (Eieio, Sync) -> GT - | (Eieio, LwSync) -> GT - | (Eieio, Eieio) -> EQ - | (Eieio, Isync) -> LT - | (Eieio, DMB) -> LT - | (Eieio, DMB_ST) -> LT - | (Eieio, DMB_LD) -> LT - | (Eieio, DSB) -> LT - | (Eieio, DSB_ST) -> LT - | (Eieio, DSB_LD) -> LT - | (Eieio, ISB) -> LT - - | (Isync, Sync) -> GT - | (Isync, LwSync) -> GT - | (Isync, Eieio) -> GT - | (Isync, Isync) -> EQ - | (Isync, DMB) -> LT - | (Isync, DMB_ST) -> LT - | (Isync, DMB_LD) -> LT - | (Isync, DSB) -> LT - | (Isync, DSB_ST) -> LT - | (Isync, DSB_LD) -> LT - | (Isync, ISB) -> LT - - | (DMB, Sync) -> GT - | (DMB, LwSync) -> GT - | (DMB, Eieio) -> GT - | (DMB, ISync) -> GT - | (DMB, DMB) -> EQ - | (DMB, DMB_ST) -> LT - | (DMB, DMB_LD) -> LT - | (DMB, DSB) -> LT - | (DMB, DSB_ST) -> LT - | (DMB, DSB_LD) -> LT - | (DMB, ISB) -> LT - - | (DMB_ST, Sync) -> GT - | (DMB_ST, LwSync) -> GT - | (DMB_ST, Eieio) -> GT - | (DMB_ST, ISync) -> GT - | (DMB_ST, DMB) -> GT - | (DMB_ST, DMB_ST) -> EQ - | (DMB_ST, DMB_LD) -> LT - | (DMB_ST, DSB) -> LT - | (DMB_ST, DSB_ST) -> LT - | (DMB_ST, DSB_LD) -> LT - | (DMB_ST, ISB) -> LT - - | (DMB_LD, Sync) -> GT - | (DMB_LD, LwSync) -> GT - | (DMB_LD, Eieio) -> GT - | (DMB_LD, ISync) -> GT - | (DMB_LD, DMB) -> GT - | (DMB_LD, DMB_ST) -> GT - | (DMB_LD, DMB_LD) -> EQ - | (DMB_LD, DSB) -> LT - | (DMB_LD, DSB_ST) -> LT - | (DMB_LD, DSB_LD) -> LT - | (DMB_LD, ISB) -> LT - - | (DSB, Sync) -> GT - | (DSB, LwSync) -> GT - | (DSB, Eieio) -> GT - | (DSB, ISync) -> GT - | (DSB, DMB) -> GT - | (DSB, DMB_ST) -> GT - | (DSB, DMB_LD) -> GT - | (DSB, DSB) -> EQ - | (DSB, DSB_ST) -> LT - | (DSB, DSB_LD) -> LT - | (DSB, ISB) -> LT - - | (DSB_ST, Sync) -> GT - | (DSB_ST, LwSync) -> GT - | (DSB_ST, Eieio) -> GT - | (DSB_ST, ISync) -> GT - | (DSB_ST, DMB) -> GT - | (DSB_ST, DMB_ST) -> GT - | (DSB_ST, DMB_LD) -> GT - | (DSB_ST, DSB) -> GT - | (DSB_ST, DSB_ST) -> EQ - | (DSB_ST, DSB_LD) -> LT - | (DSB_ST, ISB) -> LT - - | (DSB_LD, Sync) -> GT - | (DSB_LD, LwSync) -> GT - | (DSB_LD, Eieio) -> GT - | (DSB_LD, ISync) -> GT - | (DSB_LD, DMB) -> GT - | (DSB_LD, DMB_ST) -> GT - | (DSB_LD, DMB_LD) -> GT - | (DSB_LD, DSB) -> GT - | (DSB_LD, DSB_ST) -> GT - | (DSB_LD, DSB_LD) -> EQ - | (DSB_LD, ISB) -> LT - - | (ISB, Sync) -> GT - | (ISB, LwSync) -> GT - | (ISB, Eieio) -> GT - | (ISB, ISync) -> GT - | (ISB, DMB) -> GT - | (ISB, DMB_ST) -> GT - | (ISB, DMB_LD) -> GT - | (ISB, DSB) -> GT - | (ISB, DSB_ST) -> GT - | (ISB, DSB_LD) -> GT - | (ISB, ISB) -> EQ - end -let inline {ocaml} barrier_kindCompare = defaultCompare - -let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT -let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT -let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT -let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT - -let inline {ocaml} barrier_kindLess = defaultLess -let inline {ocaml} barrier_kindLessEq = defaultLessEq -let inline {ocaml} barrier_kindGreater = defaultGreater -let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq - -instance (Ord barrier_kind) - let compare = barrier_kindCompare - let (<) = barrier_kindLess - let (<=) = barrier_kindLessEq - let (>) = barrier_kindGreater - let (>=) = barrier_kindGreaterEq -end let ~{ocaml} eventCompare e1 e2 = match (e1,e2) with @@ -830,74 +150,12 @@ instance (SetType event) let setElemCompare = compare end + (* Functions to build up the initial state for interpretation *) val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) -(*Type representint the constructor parameters in instruction, other is a type not representable externally*) -type instr_parm_typ = - | Bit (*A single bit, represented as a one element Bitvector as a value*) - | Bvector of maybe nat (* A bitvector type, with length when statically known *) - | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *) - | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*) - | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *) - -let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with - | (Bit,Bit) -> true - | (Bvector i1,Bvector i2) -> i1 = i2 - | (Range i1,Range i2) -> i1 = i2 - | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2 - | (Other,Other) -> true - | _ -> false -end -let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality - -let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2) -let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality - -instance (Eq instr_parm_typ) - let (=) = instr_parm_typEqual - let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2) -end - -let instr_parm_typShow ip = match ip with - | Bit -> "Bit" - | Bvector i -> "Bvector " ^ show i - | Range i -> "Range " ^ show i - | Enum s i -> "Enum " ^ s ^ " " ^ show i - | Other -> "Other" - end - -instance (Show instr_parm_typ) -let show = instr_parm_typShow -end - -(*A representation of the AST node for each instruction in the spec, with concrete values from this call, - and the potential static effects from the funcl clause for this instruction - Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values -*) -type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect) - -let {coq} instructionEqual i1 i2 = match (i1,i2) with - | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2 -end -let inline ~{coq} instructionEqual = unsafe_structural_equality - -let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2) -let inline ~{coq} instructionInequal = unsafe_structural_inequality - -type v_kind = Bitv | Bytev - -type decode_error = - | Unsupported_instruction_error of instruction - | Not_an_instruction_error of opcode - | Internal_error of string - -type instruction_or_decode_error = - | IDE_instr of instruction - | IDE_decode_error of decode_error - (** propose to remove the following type and use the above instead *) type i_state_or_error = | Instr of instruction * instruction_state @@ -930,553 +188,14 @@ val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_ (* As above, but will request register reads: outcome will only be rreg, done, or error *) val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) - -(** operations and coercions on basic values *) - -val word8_to_bitls : word8 -> list bit_lifted -val bitls_to_word8 : list bit_lifted -> word8 - -val integer_of_word8_list : list word8 -> integer -val word8_list_of_integer : integer -> integer -> list word8 - -val concretizable_bitl : bit_lifted -> bool -val concretizable_bytl : byte_lifted -> bool -val concretizable_bytls : list byte_lifted -> bool - -let concretizable_bitl = function - | Bitl_zero -> true - | Bitl_one -> true - | Bitl_undef -> false - | Bitl_unknown -> false -end - -let concretizable_bytl (Byte_lifted bs) = List.all concretizable_bitl bs -let concretizable_bytls = List.all concretizable_bytl - -(* constructing values *) - -val build_register_value : list bit_lifted -> direction -> nat -> nat -> register_value -let build_register_value bs dir width start_index = - <| rv_bits = bs; - rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *) - rv_start_internal = start_index; - rv_start = if dir = D_increasing - then start_index - else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *) - |> - -val register_value : bit_lifted -> direction -> nat -> nat -> register_value -let register_value b dir width start_index = - build_register_value (List.replicate width b) dir width start_index - -val register_value_zeros : direction -> nat -> nat -> register_value -let register_value_zeros dir width start_index = - register_value Bitl_zero dir width start_index - -val register_value_ones : direction -> nat -> nat -> register_value -let register_value_ones dir width start_index = - register_value Bitl_one dir width start_index - -val byte_lifted_undef : byte_lifted -let byte_lifted_undef = Byte_lifted (List.replicate 8 Bitl_undef) - -val byte_lifted_unknown : byte_lifted -let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown) - -val memory_value_unknown : nat (*the number of bytes*) -> memory_value -let memory_value_unknown (width:nat) : memory_value = - List.replicate width byte_lifted_unknown - -val memory_value_undef : nat (*the number of bytes*) -> memory_value -let memory_value_undef (width:nat) : memory_value = - List.replicate width byte_lifted_undef - -(* lengths *) - -val memory_value_length : memory_value -> nat -let memory_value_length (mv:memory_value) = List.length mv - - -(* aux fns *) - -val maybe_all : forall 'a. list (maybe 'a) -> maybe (list 'a) -let rec maybe_all' xs acc = - match xs with - | [] -> Just (List.reverse acc) - | Nothing :: _ -> Nothing - | (Just y)::xs' -> maybe_all' xs' (y::acc) - end -let maybe_all xs = maybe_all' xs [] - -(** coercions *) - -(* bits and bytes *) - -let bit_to_bool = function (* TODO: rename bool_of_bit *) - | Bitc_zero -> false - | Bitc_one -> true -end - - -val bit_lifted_of_bit : bit -> bit_lifted -let bit_lifted_of_bit b = - match b with - | Bitc_zero -> Bitl_zero - | Bitc_one -> Bitl_one - end - -val bit_of_bit_lifted : bit_lifted -> maybe bit -let bit_of_bit_lifted bl = - match bl with - | Bitl_zero -> Just Bitc_zero - | Bitl_one -> Just Bitc_one - | Bitl_undef -> Nothing - | Bitl_unknown -> Nothing - end - - -val byte_lifted_of_byte : byte -> byte_lifted -let byte_lifted_of_byte (Byte bs) : byte_lifted = Byte_lifted (List.map bit_lifted_of_bit bs) - -val byte_of_byte_lifted : byte_lifted -> maybe byte -let byte_of_byte_lifted bl = - match bl with - | Byte_lifted bls -> - match maybe_all (List.map bit_of_bit_lifted bls) with - | Nothing -> Nothing - | Just bs -> Just (Byte bs) - end - end - - -val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*) -let rec bytes_of_bits bits = match bits with - | [] -> [] - | b0::b1::b2::b3::b4::b5::b6::b7::bits -> - (Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits) - | _ -> failwith "bytes_of_bits not given bits divisible by 8" -end - -val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*) -let rec byte_lifteds_of_bit_lifteds bits = match bits with - | [] -> [] - | b0::b1::b2::b3::b4::b5::b6::b7::bits -> - (Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits) - | _ -> failwith "byte_lifteds of bit_lifteds not given bits divisible by 8" -end - - -val byte_of_memory_byte : memory_byte -> maybe byte -let byte_of_memory_byte = byte_of_byte_lifted - -val memory_byte_of_byte : byte -> memory_byte -let memory_byte_of_byte = byte_lifted_of_byte - - -(* to and from nat *) - -(* this natFromBoolList could move to the Lem word.lem library *) -val natFromBoolList : list bool -> nat -let rec natFromBoolListAux (acc : nat) (bl : list bool) = - match bl with - | [] -> acc - | (true :: bl') -> natFromBoolListAux ((acc * 2) + 1) bl' - | (false :: bl') -> natFromBoolListAux (acc * 2) bl' - end -let natFromBoolList bl = - natFromBoolListAux 0 (List.reverse bl) - - -val nat_of_bit_list : list bit -> nat -let nat_of_bit_list b = - natFromBoolList (List.reverse (List.map bit_to_bool b)) - (* natFromBoolList takes a list with LSB first, for consistency with rest of Lem word library, so we reverse it. twice. *) - - -(* to and from integer *) - -val integer_of_bit_list : list bit -> integer -let integer_of_bit_list b = - integerFromBoolList (false,(List.reverse (List.map bit_to_bool b))) - (* integerFromBoolList takes a list with LSB first, so we reverse it *) - -val bit_list_of_integer : nat -> integer -> list bit -let bit_list_of_integer len b = - List.map (fun b -> if b then Bitc_one else Bitc_zero) - (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b))) - -val integer_of_byte_list : list byte -> integer -let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes) - -val byte_list_of_integer : nat -> integer -> list byte -let byte_list_of_integer (len:nat) (a:integer):list byte = - let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits - - -val integer_of_address : address -> integer -let integer_of_address (a:address):integer = - match a with - | Address bs i -> i - end - -val address_of_integer : integer -> address -let address_of_integer (i:integer):address = - Address (byte_list_of_integer 8 i) i - -(* to and from signed-integer *) - -val signed_integer_of_bit_list : list bit -> integer -let signed_integer_of_bit_list b = - match b with - | [] -> failwith "empty bit list" - | Bitc_zero :: b' -> - integerFromBoolList (false,(List.reverse (List.map bit_to_bool b))) - | Bitc_one :: b' -> - let b'_val = integerFromBoolList (false,(List.reverse (List.map bit_to_bool b'))) in - (* integerFromBoolList takes a list with LSB first, so we reverse it *) - let msb_val = integerPow 2 ((List.length b) - 1) in - b'_val - msb_val - end - - -(* regarding a list of int as a list of bytes in memory, MSB lowest-address first, convert to an integer *) -val integer_address_of_int_list : list int -> integer -let rec integerFromIntListAux (acc: integer) (is: list int) = - match is with - | [] -> acc - | (i :: is') -> integerFromIntListAux ((acc * 256) + integerFromInt i) is' - end -let integer_address_of_int_list (is: list int) = - integerFromIntListAux 0 is - -val address_of_byte_list : list byte -> address -let address_of_byte_list bs = - if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else - Address bs (integer_of_byte_list bs) - -(* operations on addresses *) - -val add_address_nat : address -> nat -> address -let add_address_nat (a:address) (i:nat) : address = - address_of_integer ((integer_of_address a) + (integerFromNat i)) - -val clear_low_order_bits_of_address : address -> address -let clear_low_order_bits_of_address a = - match a with - | Address [b0;b1;b2;b3;b4;b5;b6;b7] i -> - match b7 with - | Byte [bt0;bt1;bt2;bt3;bt4;bt5;bt6;bt7] -> - let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in - let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in - Address bytes (integer_of_byte_list bytes) - | _ -> failwith "Byte does not contain 8 bits" - end - | _ -> failwith "Address does not contain 8 bytes" - end - val translate_address : context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address -> maybe address * maybe (list event) -val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) -let byte_list_of_memory_value endian mv = - let mv = if endian = E_big_endian then mv else List.reverse mv in - maybe_all (List.map byte_of_memory_byte mv) - - -val integer_of_memory_value : end_flag -> memory_value -> maybe integer -let integer_of_memory_value endian (mv:memory_value):maybe integer = - match byte_list_of_memory_value endian mv with - | Just bs -> Just (integer_of_byte_list bs) - | Nothing -> Nothing - end - -val memory_value_of_integer : end_flag -> nat -> integer -> memory_value -let memory_value_of_integer endian (len:nat) (i:integer):memory_value = - let mv = List.map (byte_lifted_of_byte) (byte_list_of_integer len i) in - if endian = E_big_endian then mv else List.reverse mv - - -val integer_of_register_value : register_value -> maybe integer -let integer_of_register_value (rv:register_value):maybe integer = - match maybe_all (List.map bit_of_bit_lifted rv.rv_bits) with - | Nothing -> Nothing - | Just bs -> Just (integer_of_bit_list bs) - end - -val register_value_of_integer : nat -> nat -> direction -> integer -> register_value -let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value = - let bs = bit_list_of_integer len i in - build_register_value (List.map bit_lifted_of_bit bs) dir len start - -(* *) - -val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode -let opcode_of_bytes b0 b1 b2 b3 : opcode = Opcode [b0;b1;b2;b3] - -val register_value_of_address : address -> direction -> register_value -let register_value_of_address (Address bytes _) dir : register_value = - let bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes in - <| rv_bits = bits; - rv_dir = dir; - rv_start = 0; - rv_start_internal = if dir = D_increasing then 0 else (List.length bits) - 1 - |> - -val register_value_of_memory_value : memory_value -> direction -> register_value -let register_value_of_memory_value bytes dir : register_value = - let bitls = List.concatMap (fun (Byte_lifted bs) -> bs) bytes in - <| rv_bits = bitls; - rv_dir = dir; - rv_start = 0; - rv_start_internal = if dir = D_increasing then 0 else (List.length bitls) - 1 - |> - -val memory_value_of_register_value: register_value -> memory_value -let memory_value_of_register_value r = - (byte_lifteds_of_bit_lifteds r.rv_bits) - -val address_lifted_of_register_value : register_value -> maybe address_lifted -(* returning Nothing iff the register value is not 64 bits wide, but -allowing Bitl_undef and Bitl_unknown *) -let address_lifted_of_register_value (rv:register_value) : maybe address_lifted = - if List.length rv.rv_bits <> 64 then Nothing - else - Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits) - (if List.all concretizable_bitl rv.rv_bits - then match (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) with - | (Just(bits)) -> Just (integer_of_bit_list bits) - | Nothing -> Nothing end - else Nothing)) - -val address_of_address_lifted : address_lifted -> maybe address -(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *) -let address_of_address_lifted (al:address_lifted): maybe address = - match al with - | Address_lifted bls (Just i)-> - match maybe_all ((List.map byte_of_byte_lifted) bls) with - | Nothing -> Nothing - | Just bs -> Just (Address bs i) - end - | _ -> Nothing -end - -val address_of_register_value : register_value -> maybe address -(* returning Nothing iff the register value is not 64 bits wide, or contains Bitl_undef or Bitl_unknown *) -let address_of_register_value (rv:register_value) : maybe address = - match address_lifted_of_register_value rv with - | Nothing -> Nothing - | Just al -> - match address_of_address_lifted al with - | Nothing -> Nothing - | Just a -> Just a - end - end - -let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address = - match byte_list_of_memory_value endian mv with - | Nothing -> Nothing - | Just bs -> - if List.length bs <> 8 then Nothing else - Just (address_of_byte_list bs) - end - -val byte_of_int : int -> byte -let byte_of_int (i:int) : byte = - Byte (bit_list_of_integer 8 (integerFromInt i)) - -val memory_byte_of_int : int -> memory_byte -let memory_byte_of_int (i:int) : memory_byte = - memory_byte_of_byte (byte_of_int i) - -(* -val int_of_memory_byte : int -> maybe memory_byte -let int_of_memory_byte (mb:memory_byte) : int = - failwith "TODO" -*) - - - - -val memory_value_of_address_lifted : end_flag -> address_lifted -> memory_value -let memory_value_of_address_lifted endian (al:address_lifted) = - match al with - | Address_lifted bs _ -> if endian = E_big_endian then bs else List.reverse bs - end - -val byte_list_of_address : address -> list byte -let byte_list_of_address (a:address) : list byte = - match a with - | Address bs _ -> bs - end - -val memory_value_of_address : end_flag -> address -> memory_value -let memory_value_of_address endian addr = - match addr with - | Address bs _ -> List.map byte_lifted_of_byte (if endian = E_big_endian then bs else List.reverse bs) - end - -val byte_list_of_opcode : opcode -> list byte -let byte_list_of_opcode (opc:opcode) : list byte = - match opc with - | Opcode bs -> bs - end - -(** ****************************************** *) -(** show type class instantiations *) -(** ****************************************** *) - -(* matching printing_functions.ml *) -val stringFromReg_name : reg_name -> string -let stringFromReg_name r = match r with -| Reg s start size dir -> s -| Reg_slice s start dir (first,second) -> - let (first,second) = - match dir with - | D_increasing -> (first,second) - | D_decreasing -> (start - first, start - second) - end in - s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]" -| Reg_field s size dir f (first, second) -> - s ^ "." ^ f -| Reg_f_slice s start dir f (first1,second1) (first,second) -> - let (first,second) = - match dir with - | D_increasing -> (first,second) - | D_decreasing -> (start - first, start - second) - end in - s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]" -end - -instance (Show reg_name) - let show = stringFromReg_name -end - - -(* hex pp of integers, adapting the Lem string_extra.lem code *) -val stringFromNaturalHexHelper : natural -> list char -> list char -let rec stringFromNaturalHexHelper n acc = - if n = 0 then - acc - else - stringFromNaturalHexHelper (n / 16) (String_extra.chr (natFromNatural (let nd = n mod 16 in if nd <=9 then nd + 48 else nd - 10 + 97)) :: acc) - -val stringFromNaturalHex : natural -> string -let (*~{ocaml;hol}*) stringFromNaturalHex n = - if n = 0 then "0" else toString (stringFromNaturalHexHelper n []) - -val stringFromIntegerHex : integer -> string -let (*~{ocaml}*) stringFromIntegerHex i = - if i < 0 then - "-" ^ stringFromNaturalHex (naturalFromInteger i) - else - stringFromNaturalHex (naturalFromInteger i) - - -let stringFromAddress (Address bs i) = - let i' = integer_of_byte_list bs in - if i=i' then -(*TODO: ideally this should be made to match the src/pp.ml pp_address; the following very roughly matches what's used in the ppcmem UI, enough to make exceptions readable *) - if i < 65535 then - show i - else - stringFromIntegerHex i - else - "stringFromAddress bytes and integer mismatch" - -instance (Show address) - let show = stringFromAddress -end - -let stringFromByte_lifted bl = - match byte_of_byte_lifted bl with - | Nothing -> "u?" - | Just (Byte bits) -> - let i = integer_of_bit_list bits in - show i - end - -instance (Show byte_lifted) - let show = stringFromByte_lifted -end - -(* possible next instruction address options *) -type nia = - | NIA_successor - | NIA_concrete_address of address - | NIA_LR (* "LR0:61 || 0b00" in Power pseudocode *) - | NIA_CTR (* "CTR0:61 || 0b00" in Power pseudocode *) - | NIA_register of reg_name (* the address will be in a register, - corresponds to AArch64 BLR, BR, RET - instructions *) - -let niaCompare n1 n2 = match (n1,n2) with - | (NIA_successor,NIA_successor) -> EQ - | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2 - | (NIA_LR,NIA_LR) -> EQ - | (NIA_CTR,NIA_CTR) -> EQ - | (NIA_register r1,NIA_register r2) -> compare r1 r2 - - | (NIA_successor,_) -> LT - | (NIA_concrete_address _,_) -> LT - | (NIA_LR,_) -> LT - | (NIA_CTR,_) -> LT - | (_,_) -> GT - end - -instance (Ord nia) - let compare = niaCompare - let (<) n1 n2 = (niaCompare n1 n2) = LT - let (<=) n1 n2 = (niaCompare n1 n2) <> GT - let (>) n1 n2 = (niaCompare n1 n2) = GT - let (>=) n1 n2 = (niaCompare n1 n2) <> LT -end - -let stringFromNia = function - | NIA_successor -> "NIA_successor" - | NIA_concrete_address a -> "NIA_concrete_address " ^ show a - | NIA_LR -> "NIA_LR" - | NIA_CTR -> "NIA_CTR" - | NIA_register r -> "NIA_register " ^ show r -end - -instance (Show nia) - let show = stringFromNia -end - -type dia = - | DIA_none - | DIA_concrete_address of address - | DIA_register of reg_name - -let diaCompare d1 d2 = match (d1, d2) with - | (DIA_none, DIA_none) -> EQ - | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2 - | (DIA_register r1, DIA_register r2) -> compare r1 r2 - | (DIA_none, _) -> LT - | (DIA_concrete_address _, _) -> LT - | (DIA_register _, _) -> LT -end - -instance (Ord dia) - let compare = diaCompare - let (<) n1 n2 = (diaCompare n1 n2) = LT - let (<=) n1 n2 = (diaCompare n1 n2) <> GT - let (>) n1 n2 = (diaCompare n1 n2) = GT - let (>=) n1 n2 = (diaCompare n1 n2) <> LT -end - -let stringFromDia = function - | DIA_none -> "DIA_none" - | DIA_concrete_address a -> "DIA_concrete_address " ^ show a - | DIA_register r -> "DIA_delayed_register " ^ show r -end - -instance (Show dia) - let show = stringFromDia -end - val instruction_analysis : context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind) + + +val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state string unit diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index a1c49796..d54b7155 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -1,5 +1,6 @@ open Printf ;; open Interp_ast ;; +open Sail_impl_base ;; open Interp_utilities ;; open Interp_interface ;; open Interp_inter_imp ;; @@ -86,10 +87,10 @@ let bits_lifted_homogenous_of_bit_lifteds (bls:bit_lifted list) : bits_lifted_ho bits_lifted_homogenous_of_bit_lifteds' bls' acc0 (*let byte_it_lifted_to_string = function - | Bitl_zero -> "0" - | Bitl_one -> "1" - | Bitl_undef -> "u" - | Bitl_unknown -> "?" + | BL0 -> "0" + | BL1 -> "1" + | BLUndef -> "u" + | BLUnknown -> "?" *) let bit_lifted_to_string = function @@ -103,7 +104,7 @@ let hex_int_to_string i = let bytes_lifted_homogenous_to_string = function | Bitslh_concrete bs -> - let i = to_int (Interp_interface.integer_of_bit_list bs) in + let i = to_int (Sail_impl_base.integer_of_bit_list bs) in hex_int_to_string i | Bitslh_undef -> "uu" | Bitslh_unknown -> "??" @@ -126,7 +127,7 @@ print as lifted hex, otherwise print as lifted bits *) let bit_lifteds_to_string (bls: bit_lifted list) (show_length_and_start:bool) (starto: int option) (abbreviate_zero_to_nine: bool) = let l = List.length bls in if l mod 8 = 0 then (* if List.mem l [8;16;32;64;128] then *) - let bytesl = List.map (fun (Byte_lifted bs) -> bs) (Interp_interface.byte_lifteds_of_bit_lifteds bls) in + let bytesl = List.map (fun (Byte_lifted bs) -> bs) (Sail_impl_base.byte_lifteds_of_bit_lifteds bls) in let byteslhos = List.map bits_lifted_homogenous_of_bit_lifteds bytesl in match maybe_all byteslhos with | None -> (* print as bitvector after all *) @@ -134,7 +135,7 @@ let bit_lifteds_to_string (bls: bit_lifted list) (show_length_and_start:bool) (s | Some (byteslhs: bits_lifted_homogenous list) -> (* if abbreviate_zero_to_nine, all bytes are concrete, and the number is <=9, just print that *) (* (note that that doesn't print the length or start - it's appropriate only for memory values, where we typically have an explicit footprint also printed *) - let nos = List.rev_map (function blh -> match blh with | Bitslh_concrete bs -> Some (Interp_interface.nat_of_bit_list bs) | Bitslh_undef -> None | Bitslh_unknown -> None) byteslhs in + let nos = List.rev_map (function blh -> match blh with | Bitslh_concrete bs -> Some (Sail_impl_base.nat_of_bit_list bs) | Bitslh_undef -> None | Bitslh_unknown -> None) byteslhs in let (lsb,msbs) = ((List.hd nos), List.tl nos) in match (abbreviate_zero_to_nine, List.for_all (fun no -> no=Some 0) msbs, lsb) with | (true, true, Some n) when n <= 9 -> @@ -256,7 +257,7 @@ let dir_to_string = function | D_decreasing -> "dec" let reg_name_to_string = function - | Reg0(s,start,size,d) -> s (*^ "(" ^ (string_of_int start) ^ ", " ^ (string_of_int size) ^ ", " ^ (dir_to_string d) ^ ")"*) + | Reg(s,start,size,d) -> s (*^ "(" ^ (string_of_int start) ^ ", " ^ (string_of_int size) ^ ", " ^ (dir_to_string d) ^ ")"*) | Reg_slice(s,start,dir,(first,second)) -> let first,second = match dir with diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli index c7747b50..2ce2c016 100644 --- a/src/lem_interp/printing_functions.mli +++ b/src/lem_interp/printing_functions.mli @@ -1,5 +1,6 @@ open Interp_utilities;; open Interp_ast ;; +open Sail_impl_base ;; open Interp_interface ;; (*Functions to translate values, registers, or locations strings *) diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index eec87f4f..b536a77d 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -1,5 +1,6 @@ open Printf open Interp_ast +open Sail_impl_base open Interp_interface open Interp_inter_imp @@ -107,22 +108,22 @@ let unit_lit = (L_aux(L_unit,Interp_ast.Unknown)) let rec perform_action ((reg, mem, tagmem) as env) = function (* registers *) - | Read_reg0(Reg0(id,_,_,_), _) -> (Some(Reg.find id reg), env) - | Read_reg0(Reg_slice(id, _, _, range), _) - | Read_reg0(Reg_field(id, _, _, _, range), _) -> (Some(slice (Reg.find id reg) range), env) - | Read_reg0(Reg_f_slice(id, _,_,_, range, mini_range), _) -> + | Read_reg1(Reg(id,_,_,_), _) -> (Some(Reg.find id reg), env) + | Read_reg1(Reg_slice(id, _, _, range), _) + | Read_reg1(Reg_field(id, _, _, _, range), _) -> (Some(slice (Reg.find id reg) range), env) + | Read_reg1(Reg_f_slice(id, _,_,_, range, mini_range), _) -> (Some(slice (slice (Reg.find id reg) range) mini_range),env) - | Write_reg0(Reg0(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem,tagmem)) - | Write_reg0((Reg_slice(id,_,_,range) as reg_n),value, _) - | Write_reg0((Reg_field(id,_,_,_,range) as reg_n),value,_)-> + | Write_reg1(Reg(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem,tagmem)) + | Write_reg1((Reg_slice(id,_,_,range) as reg_n),value, _) + | Write_reg1((Reg_field(id,_,_,_,range) as reg_n),value,_)-> let old_val = Reg.find id reg in let new_val = fupdate_slice reg_n old_val value range in (None, (Reg.add id new_val reg, mem,tagmem)) - | Write_reg0((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value,_) -> + | Write_reg1((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value,_) -> let old_val = Reg.find id reg in let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in (None,(Reg.add id new_val reg,mem,tagmem)) - | Read_mem0(kind,location, length, _,_) -> + | Read_mem1(kind,location, length, _,_) -> let address = match address_of_address_lifted location with | Some a -> a | None -> assert false (*TODO remember how to report an error *)in @@ -160,7 +161,7 @@ let rec perform_action ((reg, mem, tagmem) as env) = function | b::bytes -> writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in (None,(reg,writing naddress length bytes mem,tagmem))) - | Write_memv0(Some location, bytes, _, _) -> + | Write_memv1(Some location, bytes, _, _) -> let address = match address_of_address_lifted location with | Some a -> a | _ -> failwith "Write address not known" in @@ -261,20 +262,20 @@ let run (green act) lhs (blue arrow) rhs in let left = "<-" and right = "->" in let rec loop mode env = function - | Done -> + | Done0 -> interactf "%s: %s\n" (grey name) (blue "done"); (true, mode, !track_dependencies, env) - | Error0 s -> + | Error1 s -> errorf "%s: %s: %s\n" (grey name) (red "error") s; (false, mode, !track_dependencies, env) - | Escape (None, _) -> + | Escape0 (None, _) -> show "exiting current instruction" "" "" ""; interactf "%s: %s\n" (grey name) (blue "done"); (true, mode, !track_dependencies, env) - | Fail0 (Some s) -> + | Fail1 (Some s) -> errorf "%s: %s: %s\n" (grey name) (red "assertion failed") s; (false, mode, !track_dependencies, env) - | Fail0 None -> + | Fail1 None -> errorf "%s: %s: %s\n" (grey name) (red "assertion failed") "No message provided"; (false, mode, !track_dependencies, env) | action -> @@ -290,17 +291,17 @@ let run mode in let (mode', env', next) = (match action with - | Read_reg0(reg,next_thunk) -> + | Read_reg1(reg,next_thunk) -> (match return with | Some(value) -> show "read_reg" (reg_name_to_string reg) right (register_value_to_string value); let next = next_thunk value in (step next, env', next) | None -> assert false) - | Write_reg0(reg,value,next) -> + | Write_reg1(reg,value,next) -> show "write_reg" (reg_name_to_string reg) left (register_value_to_string value); (step next, env', next) - | Read_mem0(kind, (Address_lifted(location,_)), length, tracking, next_thunk) -> + | Read_mem1(kind, (Address_lifted(location,_)), length, tracking, next_thunk) -> (match return with | Some(value) -> show "read_mem" @@ -327,26 +328,26 @@ let run show "write_mem value depended on" (dependencies_to_string vdeps) "" "";); let next = next_thunk true in (step next,env',next) - | Write_memv0(Some(Address_lifted(location,_)),value,_,next_thunk) -> + | Write_memv1(Some(Address_lifted(location,_)),value,_,next_thunk) -> show "write_mem value" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value); let next = next_thunk true in (step next,env',next) - | Write_ea0(_,(Address_lifted(location,_)), size,_,next) -> + | Write_ea1(_,(Address_lifted(location,_)), size,_,next) -> show "write_announce" (memory_value_to_string !default_endian location) left ((string_of_int size) ^ " bytes"); (step next, env, next) - | Barrier0(bkind,next) -> + | Barrier1(bkind,next) -> show "mem_barrier" "" "" ""; (step next, env, next) - | Internal(None,None, next) -> + | Internal0(None,None, next) -> show "stepped" "" "" ""; (step ~force:true next,env',next) - | Internal((Some fn),None,next) -> + | Internal0((Some fn),None,next) -> show "evaluated" fn "" ""; (step ~force:true next, env',next) - | Internal(None,Some vdisp,next) -> + | Internal0(None,Some vdisp,next) -> show "evaluated" (vdisp ()) "" ""; (step ~force:true next,env', next) - | Internal((Some fn),(Some vdisp),next) -> + | Internal0((Some fn),(Some vdisp),next) -> show "evaluated" (fn ^ " " ^ (vdisp ())) "" ""; (step ~force:true next, env', next) | Nondet_choice(nondets, next) -> @@ -369,18 +370,18 @@ let run loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies !default_endian) next)) choose_order (false,mode,!track_dependencies,env'); in (step i_state,env',i_state) end - | Escape(Some e,_) -> + | Escape0(Some e,_) -> show "exiting current evaluation" "" "" ""; step e,env', e - | Escape _ -> assert false - | Error0 _ -> failwith "Internal error" - | Fail0 _ -> failwith "Assertion in program failed" - | Done -> + | Escape0 _ -> assert false + | Error1 _ -> failwith "Internal error" + | Fail1 _ -> failwith "Assertion in program failed" + | Done0 -> show "done evalution" "" "" ""; assert false - | Footprint0 _ -> assert false - | Write_ea0 _ -> assert false - | Write_memv0 _ -> assert false) + | Footprint1 _ -> assert false + | Write_ea1 _ -> assert false + | Write_memv1 _ -> assert false) (*| _ -> assert false*) in loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies !default_endian) next) in diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem new file mode 100644 index 00000000..60c7bf0b --- /dev/null +++ b/src/lem_interp/sail_impl_base.lem @@ -0,0 +1,1309 @@ +open import Pervasives_extra +open import Interp_ast (* only because the instruction type refers to base effect *) + +(* maybe isn't a member of type Ord - this should be in the Lem standard library*) +instance forall 'a. Ord 'a => (Ord (maybe 'a)) + let compare = maybeCompare compare + let (<) r1 r2 = (maybeCompare compare r1 r2) = LT + let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT + let (>) r1 r2 = (maybeCompare compare r1 r2) = GT + let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT +end + +type word8 = nat (* bounded at a byte, for when lem supports it*) + +type end_flag = + | E_big_endian + | E_little_endian + +type bit = + | Bitc_zero + | Bitc_one + +type bit_lifted = + | Bitl_zero + | Bitl_one + | Bitl_undef + | Bitl_unknown + +type direction = + | D_increasing + | D_decreasing + +(* at some point this should probably not mention bit_lifted anymore *) +type register_value = <| + rv_bits: list bit_lifted (* 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_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*) + +type instruction_field_value = list bit + +type byte = Byte of list bit (* of length 8 *) (*MSB first everywhere*) + +type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer +(* for both values of end_flag, MSBy first *) + +type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*) + +type memory_value = list memory_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 *) + + + +(* not sure which of these is more handy yet *) +type address = Address of list byte (* of length 8 *) * integer +(* type address = Address of integer *) + +type opcode = Opcode of list byte (* of length 4 *) + +(** typeclass instantiations *) + +let ~{ocaml} bitCompare (b1:bit) (b2:bit) = + match (b1,b2) with + | (Bitc_zero, Bitc_zero) -> EQ + | (Bitc_one, Bitc_one) -> EQ + | (Bitc_zero, _) -> LT + | (_,_) -> GT + end +let inline {ocaml} bitCompare = defaultCompare + +let ~{ocaml} bitLess b1 b2 = bitCompare b1 b2 = LT +let ~{ocaml} bitLessEq b1 b2 = bitCompare b1 b2 <> GT +let ~{ocaml} bitGreater b1 b2 = bitCompare b1 b2 = GT +let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT + +let inline {ocaml} bitLess = defaultLess +let inline {ocaml} bitLessEq = defaultLessEq +let inline {ocaml} bitGreater = defaultGreater +let inline {ocaml} bitGreaterEq = defaultGreaterEq + +instance (Ord bit) + let compare = bitCompare + let (<) = bitLess + let (<=) = bitLessEq + let (>) = bitGreater + let (>=) = bitGreaterEq +end + +let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) = + match (bl1,bl2) with + | (Bitl_zero, Bitl_zero) -> EQ + | (Bitl_one, Bitl_one) -> EQ + | (Bitl_undef,Bitl_undef) -> EQ + | (Bitl_unknown,Bitl_unknown) -> EQ + | (Bitl_zero,_) -> LT + | (Bitl_one, _) -> LT + | (Bitl_undef, _) -> LT + | (_,_) -> GT + end +let inline {ocaml} bit_liftedCompare = defaultCompare + +let ~{ocaml} bit_liftedLess b1 b2 = bit_liftedCompare b1 b2 = LT +let ~{ocaml} bit_liftedLessEq b1 b2 = bit_liftedCompare b1 b2 <> GT +let ~{ocaml} bit_liftedGreater b1 b2 = bit_liftedCompare b1 b2 = GT +let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT + +let inline {ocaml} bit_liftedLess = defaultLess +let inline {ocaml} bit_liftedLessEq = defaultLessEq +let inline {ocaml} bit_liftedGreater = defaultGreater +let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq + +instance (Ord bit_lifted) + let compare = bit_liftedCompare + let (<) = bit_liftedLess + let (<=) = bit_liftedLessEq + let (>) = bit_liftedGreater + let (>=) = bit_liftedGreaterEq +end + +let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2 +let inline {ocaml} byte_liftedCompare = defaultCompare + +let ~{ocaml} byte_liftedLess b1 b2 = byte_liftedCompare b1 b2 = LT +let ~{ocaml} byte_liftedLessEq b1 b2 = byte_liftedCompare b1 b2 <> GT +let ~{ocaml} byte_liftedGreater b1 b2 = byte_liftedCompare b1 b2 = GT +let ~{ocaml} byte_liftedGreaterEq b1 b2 = byte_liftedCompare b1 b2 <> LT + +let inline {ocaml} byte_liftedLess = defaultLess +let inline {ocaml} byte_liftedLessEq = defaultLessEq +let inline {ocaml} byte_liftedGreater = defaultGreater +let inline {ocaml} byte_liftedGreaterEq = defaultGreaterEq + +instance (Ord byte_lifted) + let compare = byte_liftedCompare + let (<) = byte_liftedLess + let (<=) = byte_liftedLessEq + let (>) = byte_liftedGreater + let (>=) = byte_liftedGreaterEq +end + +let ~{ocaml} byteCompare (Byte b1) (Byte b2) = compare b1 b2 +let inline {ocaml} byteCompare = defaultCompare + +let ~{ocaml} byteLess b1 b2 = byteCompare b1 b2 = LT +let ~{ocaml} byteLessEq b1 b2 = byteCompare b1 b2 <> GT +let ~{ocaml} byteGreater b1 b2 = byteCompare b1 b2 = GT +let ~{ocaml} byteGreaterEq b1 b2 = byteCompare b1 b2 <> LT + +let inline {ocaml} byteLess = defaultLess +let inline {ocaml} byteLessEq = defaultLessEq +let inline {ocaml} byteGreater = defaultGreater +let inline {ocaml} byteGreaterEq = defaultGreaterEq + +instance (Ord byte) + let compare = byteCompare + let (<) = byteLess + let (<=) = byteLessEq + let (>) = byteGreater + let (>=) = byteGreaterEq +end + +let (*~{ocaml}*) addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2 +(*let inline {ocaml} addressCompare = defaultCompare*) + +let ~{ocaml} addressLess b1 b2 = addressCompare b1 b2 = LT +let ~{ocaml} addressLessEq b1 b2 = addressCompare b1 b2 <> GT +let ~{ocaml} addressGreater b1 b2 = addressCompare b1 b2 = GT +let ~{ocaml} addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT + +let inline {ocaml} addressLess = defaultLess +let inline {ocaml} addressLessEq = defaultLessEq +let inline {ocaml} addressGreater = defaultGreater +let inline {ocaml} addressGreaterEq = defaultGreaterEq + +instance (Ord address) + let compare = addressCompare + let (<) = addressLess + let (<=) = addressLessEq + let (>) = addressGreater + let (>=) = addressGreaterEq +end + +let {coq} addressEqual a1 a2 = (addressCompare a1 a2) = EQ +let inline ~{coq} addressEqual = unsafe_structural_equality + +let {coq} addressInequal a1 a2 = not (addressEqual a1 a2) +let inline ~{coq} addressInequal = unsafe_structural_inequality + +instance (Eq address) + let (=) = addressEqual + let (<>) = addressInequal +end + +let ~{ocaml} directionCompare d1 d2 = + match (d1, d2) with + | (D_decreasing, D_increasing) -> GT + | (D_increasing, D_decreasing) -> LT + | _ -> EQ + end +let inline {ocaml} directionCompare = defaultCompare + +let ~{ocaml} directionLess b1 b2 = directionCompare b1 b2 = LT +let ~{ocaml} directionLessEq b1 b2 = directionCompare b1 b2 <> GT +let ~{ocaml} directionGreater b1 b2 = directionCompare b1 b2 = GT +let ~{ocaml} directionGreaterEq b1 b2 = directionCompare b1 b2 <> LT + +let inline {ocaml} directionLess = defaultLess +let inline {ocaml} directionLessEq = defaultLessEq +let inline {ocaml} directionGreater = defaultGreater +let inline {ocaml} directionGreaterEq = defaultGreaterEq + +instance (Ord direction) + let compare = directionCompare + let (<) = directionLess + let (<=) = directionLessEq + let (>) = directionGreater + let (>=) = directionGreaterEq +end + +let ~{ocaml} register_valueCompare rv1 rv2 = + compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal) + (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal) +let inline {ocaml} register_valueCompare = defaultCompare + +let ~{ocaml} register_valueLess b1 b2 = register_valueCompare b1 b2 = LT +let ~{ocaml} register_valueLessEq b1 b2 = register_valueCompare b1 b2 <> GT +let ~{ocaml} register_valueGreater b1 b2 = register_valueCompare b1 b2 = GT +let ~{ocaml} register_valueGreaterEq b1 b2 = register_valueCompare b1 b2 <> LT + +let inline {ocaml} register_valueLess = defaultLess +let inline {ocaml} register_valueLessEq = defaultLessEq +let inline {ocaml} register_valueGreater = defaultGreater +let inline {ocaml} register_valueGreaterEq = defaultGreaterEq + +instance (Ord register_value) + let compare = register_valueCompare + let (<) = register_valueLess + let (<=) = register_valueLessEq + let (>) = register_valueGreater + let (>=) = register_valueGreaterEq +end + +let ~{ocaml} address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) = + compare (b1,i1) (b2,i2) +let inline {ocaml} address_liftedCompare = defaultCompare + +let ~{ocaml} address_liftedLess b1 b2 = address_liftedCompare b1 b2 = LT +let ~{ocaml} address_liftedLessEq b1 b2 = address_liftedCompare b1 b2 <> GT +let ~{ocaml} address_liftedGreater b1 b2 = address_liftedCompare b1 b2 = GT +let ~{ocaml} address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT + +let inline {ocaml} address_liftedLess = defaultLess +let inline {ocaml} address_liftedLessEq = defaultLessEq +let inline {ocaml} address_liftedGreater = defaultGreater +let inline {ocaml} address_liftedGreaterEq = defaultGreaterEq + +instance (Ord address_lifted) + let compare = address_liftedCompare + let (<) = address_liftedLess + let (<=) = address_liftedLessEq + let (>) = address_liftedGreater + let (>=) = address_liftedGreaterEq +end + +(* Registers *) +type slice = (nat * nat) + +type reg_name = + (* do we really need this here if ppcmem already has this information by itself? *) +| Reg of string * nat * nat * direction +(*Name of the register, accessing the entire register, the start and size of this register, and its direction *) + +| Reg_slice of string * nat * direction * slice +(* 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, adjusted +to reflect the correct span direction in the interpreter side. *) + +| Reg_field of string * nat * direction * string * 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_f_slice of string * nat * direction * string * slice * 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 *) + +let register_base_name : reg_name -> string = function + | Reg s _ _ _ -> s + | Reg_slice s _ _ _ -> s + | Reg_field s _ _ _ _ -> s + | Reg_f_slice s _ _ _ _ _ -> s + end + +let slice_of_reg_name : reg_name -> slice = function + | Reg _ start width D_increasing -> (start, start + width -1) + | Reg _ start width D_decreasing -> (start - width - 1, start) + | Reg_slice _ _ _ sl -> sl + | Reg_field _ _ _ _ sl -> sl + | Reg_f_slice _ _ _ _ _ sl -> sl + end + +let reg_name_non_empty_intersection (r: reg_name) (r': reg_name) : bool = + register_base_name r = register_base_name r' && + let (i1, i2) = slice_of_reg_name r in + let (i1', i2') = slice_of_reg_name r' in + i1' <= i2 && i2' >= i1 + +let reg_nameCompare r1 r2 = + compare (register_base_name r1,slice_of_reg_name r1) + (register_base_name r2,slice_of_reg_name r2) + +let reg_nameLess b1 b2 = reg_nameCompare b1 b2 = LT +let reg_nameLessEq b1 b2 = reg_nameCompare b1 b2 <> GT +let reg_nameGreater b1 b2 = reg_nameCompare b1 b2 = GT +let reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT + +instance (Ord reg_name) + let compare = reg_nameCompare + let (<) = reg_nameLess + let (<=) = reg_nameLessEq + let (>) = reg_nameGreater + let (>=) = reg_nameGreaterEq +end + +let reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ +let reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2) + +instance (Eq reg_name) + let (=) = reg_nameEqual + let (<>) = reg_nameInequal +end + +instance (SetType reg_name) + let setElemCompare = reg_nameCompare +end + +let direction_of_reg_name r = match r with + | Reg _ _ _ d -> d + | Reg_slice _ _ d _ -> d + | Reg_field _ _ d _ _ -> d + | Reg_f_slice _ _ d _ _ _ -> d + end + +let start_of_reg_name r = match r with + | Reg _ start _ _ -> start + | Reg_slice _ start _ _ -> start + | Reg_field _ start _ _ _ -> start + | Reg_f_slice _ start _ _ _ _ -> start +end + +(* Data structures for building up instructions *) + +type read_kind = + (* common reads *) + Read_plain + | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*) + (* Power reads *) + | Read_reserve + (* AArch64 reads *) + | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream + +instance (Show read_kind) + let show = function + | Read_plain -> "Read_plain" + | Read_tag -> "Read_tag" + | Read_reserve -> "Read_reserve" + | Read_acquire -> "Read_acquire" + | Read_exclusive -> "Read_exclusive" + | Read_exclusive_acquire -> "Read_exclusive_acquire" + | Read_stream -> "Read_stream" + end +end + +type write_kind = + (* common writes *) + Write_plain + | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*) + (* 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 instruction_kind = + | IK_barrier of barrier_kind + | IK_mem_read of read_kind + | IK_mem_write of write_kind +(* SS reinstating cond_branches +at present branches are not distinguished in the instruction_kind; +they just have particular nias (and will be IK_simple *) + | IK_cond_branch +(* | IK_uncond_branch *) + | IK_simple + +(* the address_lifted types should go away here and be replaced by address *) +type outcome 's 'e 'a = + (* Request to read memory, value is location to read, integer is size to read, + followed by registers that were used in computing that size *) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'e 'a) + (* Tell the system a write is imminent, at address lifted, of size nat *) + | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'e 'a + (* Request to write memory at last signalled address. Memory value should be 8 + times the size given in ea signal *) + | Write_memv of memory_value * (bool -> outcome_s 's 'e 'a) + (* Request a memory barrier *) + | Barrier of barrier_kind * outcome_s 's 'e 'a + (* Tell the system to dynamically recalculate dependency footprint *) + | Footprint of outcome_s 's 'e 'a + (* Request to read register, will track dependency when mode.track_values *) + | Read_reg of reg_name * (register_value -> outcome_s 's 'e 'a) + (* Request to write register *) + | Write_reg of (reg_name * register_value) * (outcome_s 's 'e 'a) + | Escape of maybe (outcome_s 's 'e 'e) + (*Result of a failed assert with possible error message to report*) + | Fail of maybe string + | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'e 'a + | Done of 'a + | Error of string + and outcome_s 's 'e 'a = outcome 's 'e 'a * maybe 's + +let ~{ocaml} read_kindCompare rk1 rk2 = + match (rk1, rk2) with + | (Read_plain, Read_plain) -> EQ + | (Read_plain, Read_reserve) -> LT + | (Read_plain, Read_acquire) -> LT + | (Read_plain, Read_exclusive) -> LT + | (Read_plain, Read_exclusive_acquire) -> LT + | (Read_plain, Read_stream) -> LT + + | (Read_reserve, Read_plain) -> GT + | (Read_reserve, Read_reserve) -> EQ + | (Read_reserve, Read_acquire) -> LT + | (Read_reserve, Read_exclusive) -> LT + | (Read_reserve, Read_exclusive_acquire) -> LT + | (Read_reserve, Read_stream) -> LT + + | (Read_acquire, Read_plain) -> GT + | (Read_acquire, Read_reserve) -> GT + | (Read_acquire, Read_acquire) -> EQ + | (Read_acquire, Read_exclusive) -> LT + | (Read_acquire, Read_exclusive_acquire) -> LT + | (Read_acquire, Read_stream) -> LT + + | (Read_exclusive, Read_plain) -> GT + | (Read_exclusive, Read_reserve) -> GT + | (Read_exclusive, Read_acquire) -> GT + | (Read_exclusive, Read_exclusive) -> EQ + | (Read_exclusive, Read_exclusive_acquire) -> LT + | (Read_exclusive, Read_stream) -> LT + + | (Read_exclusive_acquire, Read_plain) -> GT + | (Read_exclusive_acquire, Read_reserve) -> GT + | (Read_exclusive_acquire, Read_acquire) -> GT + | (Read_exclusive_acquire, Read_exclusive) -> GT + | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ + | (Read_exclusive_acquire, Read_stream) -> GT + + | (Read_stream, Read_plain) -> GT + | (Read_stream, Read_reserve) -> GT + | (Read_stream, Read_acquire) -> GT + | (Read_stream, Read_exclusive) -> GT + | (Read_stream, Read_exclusive_acquire) -> GT + | (Read_stream, Read_stream) -> EQ + end +let inline {ocaml} read_kindCompare = defaultCompare + +let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT +let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT +let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT +let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT + +let inline {ocaml} read_kindLess = defaultLess +let inline {ocaml} read_kindLessEq = defaultLessEq +let inline {ocaml} read_kindGreater = defaultGreater +let inline {ocaml} read_kindGreaterEq = defaultGreaterEq + +instance (Ord read_kind) + let compare = read_kindCompare + let (<) = read_kindLess + let (<=) = read_kindLessEq + let (>) = read_kindGreater + let (>=) = read_kindGreaterEq +end + +let ~{ocaml} write_kindCompare wk1 wk2 = + match (wk1, wk2) with + | (Write_plain, Write_plain) -> EQ + | (Write_plain, Write_conditional) -> LT + | (Write_plain, Write_release) -> LT + | (Write_plain, Write_exclusive) -> LT + | (Write_plain, Write_exclusive_release) -> LT + + | (Write_conditional, Write_plain) -> GT + | (Write_conditional, Write_conditional) -> EQ + | (Write_conditional, Write_release) -> LT + | (Write_conditional, Write_exclusive) -> LT + | (Write_conditional, Write_exclusive_release) -> LT + + | (Write_release, Write_plain) -> GT + | (Write_release, Write_conditional) -> GT + | (Write_release, Write_release) -> EQ + | (Write_release, Write_exclusive) -> LT + | (Write_release, Write_exclusive_release) -> LT + + | (Write_exclusive, Write_plain) -> GT + | (Write_exclusive, Write_conditional) -> GT + | (Write_exclusive, Write_release) -> GT + | (Write_exclusive, Write_exclusive) -> EQ + | (Write_exclusive, Write_exclusive_release) -> LT + + | (Write_exclusive_release, Write_plain) -> GT + | (Write_exclusive_release, Write_conditional) -> GT + | (Write_exclusive_release, Write_release) -> GT + | (Write_exclusive_release, Write_exclusive) -> GT + | (Write_exclusive_release, Write_exclusive_release) -> EQ + end +let inline {ocaml} write_kindCompare = defaultCompare + +let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT +let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT +let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT +let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT + +let inline {ocaml} write_kindLess = defaultLess +let inline {ocaml} write_kindLessEq = defaultLessEq +let inline {ocaml} write_kindGreater = defaultGreater +let inline {ocaml} write_kindGreaterEq = defaultGreaterEq + +instance (Ord write_kind) + let compare = write_kindCompare + let (<) = write_kindLess + let (<=) = write_kindLessEq + let (>) = write_kindGreater + let (>=) = write_kindGreaterEq +end + +let ~{ocaml} barrier_kindCompare bk1 bk2 = + match (bk1, bk2) with + | (Sync, Sync) -> EQ + | (Sync, LwSync) -> LT + | (Sync, Eieio) -> LT + | (Sync, Isync) -> LT + | (Sync, DMB) -> LT + | (Sync, DMB_ST) -> LT + | (Sync, DMB_LD) -> LT + | (Sync, DSB) -> LT + | (Sync, DSB_ST) -> LT + | (Sync, DSB_LD) -> LT + | (Sync, ISB) -> LT + + | (LwSync, Sync) -> GT + | (LwSync, LwSync) -> EQ + | (LwSync, Eieio) -> LT + | (LwSync, Isync) -> LT + | (LwSync, DMB) -> LT + | (LwSync, DMB_ST) -> LT + | (LwSync, DMB_LD) -> LT + | (LwSync, DSB) -> LT + | (LwSync, DSB_ST) -> LT + | (LwSync, DSB_LD) -> LT + | (LwSync, ISB) -> LT + + | (Eieio, Sync) -> GT + | (Eieio, LwSync) -> GT + | (Eieio, Eieio) -> EQ + | (Eieio, Isync) -> LT + | (Eieio, DMB) -> LT + | (Eieio, DMB_ST) -> LT + | (Eieio, DMB_LD) -> LT + | (Eieio, DSB) -> LT + | (Eieio, DSB_ST) -> LT + | (Eieio, DSB_LD) -> LT + | (Eieio, ISB) -> LT + + | (Isync, Sync) -> GT + | (Isync, LwSync) -> GT + | (Isync, Eieio) -> GT + | (Isync, Isync) -> EQ + | (Isync, DMB) -> LT + | (Isync, DMB_ST) -> LT + | (Isync, DMB_LD) -> LT + | (Isync, DSB) -> LT + | (Isync, DSB_ST) -> LT + | (Isync, DSB_LD) -> LT + | (Isync, ISB) -> LT + + | (DMB, Sync) -> GT + | (DMB, LwSync) -> GT + | (DMB, Eieio) -> GT + | (DMB, ISync) -> GT + | (DMB, DMB) -> EQ + | (DMB, DMB_ST) -> LT + | (DMB, DMB_LD) -> LT + | (DMB, DSB) -> LT + | (DMB, DSB_ST) -> LT + | (DMB, DSB_LD) -> LT + | (DMB, ISB) -> LT + + | (DMB_ST, Sync) -> GT + | (DMB_ST, LwSync) -> GT + | (DMB_ST, Eieio) -> GT + | (DMB_ST, ISync) -> GT + | (DMB_ST, DMB) -> GT + | (DMB_ST, DMB_ST) -> EQ + | (DMB_ST, DMB_LD) -> LT + | (DMB_ST, DSB) -> LT + | (DMB_ST, DSB_ST) -> LT + | (DMB_ST, DSB_LD) -> LT + | (DMB_ST, ISB) -> LT + + | (DMB_LD, Sync) -> GT + | (DMB_LD, LwSync) -> GT + | (DMB_LD, Eieio) -> GT + | (DMB_LD, ISync) -> GT + | (DMB_LD, DMB) -> GT + | (DMB_LD, DMB_ST) -> GT + | (DMB_LD, DMB_LD) -> EQ + | (DMB_LD, DSB) -> LT + | (DMB_LD, DSB_ST) -> LT + | (DMB_LD, DSB_LD) -> LT + | (DMB_LD, ISB) -> LT + + | (DSB, Sync) -> GT + | (DSB, LwSync) -> GT + | (DSB, Eieio) -> GT + | (DSB, ISync) -> GT + | (DSB, DMB) -> GT + | (DSB, DMB_ST) -> GT + | (DSB, DMB_LD) -> GT + | (DSB, DSB) -> EQ + | (DSB, DSB_ST) -> LT + | (DSB, DSB_LD) -> LT + | (DSB, ISB) -> LT + + | (DSB_ST, Sync) -> GT + | (DSB_ST, LwSync) -> GT + | (DSB_ST, Eieio) -> GT + | (DSB_ST, ISync) -> GT + | (DSB_ST, DMB) -> GT + | (DSB_ST, DMB_ST) -> GT + | (DSB_ST, DMB_LD) -> GT + | (DSB_ST, DSB) -> GT + | (DSB_ST, DSB_ST) -> EQ + | (DSB_ST, DSB_LD) -> LT + | (DSB_ST, ISB) -> LT + + | (DSB_LD, Sync) -> GT + | (DSB_LD, LwSync) -> GT + | (DSB_LD, Eieio) -> GT + | (DSB_LD, ISync) -> GT + | (DSB_LD, DMB) -> GT + | (DSB_LD, DMB_ST) -> GT + | (DSB_LD, DMB_LD) -> GT + | (DSB_LD, DSB) -> GT + | (DSB_LD, DSB_ST) -> GT + | (DSB_LD, DSB_LD) -> EQ + | (DSB_LD, ISB) -> LT + + | (ISB, Sync) -> GT + | (ISB, LwSync) -> GT + | (ISB, Eieio) -> GT + | (ISB, ISync) -> GT + | (ISB, DMB) -> GT + | (ISB, DMB_ST) -> GT + | (ISB, DMB_LD) -> GT + | (ISB, DSB) -> GT + | (ISB, DSB_ST) -> GT + | (ISB, DSB_LD) -> GT + | (ISB, ISB) -> EQ + end +let inline {ocaml} barrier_kindCompare = defaultCompare + +let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT +let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT +let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT +let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT + +let inline {ocaml} barrier_kindLess = defaultLess +let inline {ocaml} barrier_kindLessEq = defaultLessEq +let inline {ocaml} barrier_kindGreater = defaultGreater +let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq + +instance (Ord barrier_kind) + let compare = barrier_kindCompare + let (<) = barrier_kindLess + let (<=) = barrier_kindLessEq + let (>) = barrier_kindGreater + let (>=) = barrier_kindGreaterEq +end + + + + +(*Type representint the constructor parameters in instruction, other is a type not representable externally*) +type instr_parm_typ = + | Bit (*A single bit, represented as a one element Bitvector as a value*) + | Bvector of maybe nat (* A bitvector type, with length when statically known *) + | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *) + | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*) + | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *) + +let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with + | (Bit,Bit) -> true + | (Bvector i1,Bvector i2) -> i1 = i2 + | (Range i1,Range i2) -> i1 = i2 + | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2 + | (Other,Other) -> true + | _ -> false +end +let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality + +let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2) +let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality + +instance (Eq instr_parm_typ) + let (=) = instr_parm_typEqual + let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2) +end + +let instr_parm_typShow ip = match ip with + | Bit -> "Bit" + | Bvector i -> "Bvector " ^ show i + | Range i -> "Range " ^ show i + | Enum s i -> "Enum " ^ s ^ " " ^ show i + | Other -> "Other" + end + +instance (Show instr_parm_typ) +let show = instr_parm_typShow +end + +(*A representation of the AST node for each instruction in the spec, with concrete values from this call, + and the potential static effects from the funcl clause for this instruction + Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values +*) +type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect) + +let {coq} instructionEqual i1 i2 = match (i1,i2) with + | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2 +end +let inline ~{coq} instructionEqual = unsafe_structural_equality + +let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2) +let inline ~{coq} instructionInequal = unsafe_structural_inequality + +type decode_error = + | Unsupported_instruction_error of instruction + | Not_an_instruction_error of opcode + | Internal_error of string + +type instruction_or_decode_error = + | IDE_instr of instruction + | IDE_decode_error of decode_error + + +(** operations and coercions on basic values *) + +val word8_to_bitls : word8 -> list bit_lifted +val bitls_to_word8 : list bit_lifted -> word8 + +val integer_of_word8_list : list word8 -> integer +val word8_list_of_integer : integer -> integer -> list word8 + +val concretizable_bitl : bit_lifted -> bool +val concretizable_bytl : byte_lifted -> bool +val concretizable_bytls : list byte_lifted -> bool + +let concretizable_bitl = function + | Bitl_zero -> true + | Bitl_one -> true + | Bitl_undef -> false + | Bitl_unknown -> false +end + +let concretizable_bytl (Byte_lifted bs) = List.all concretizable_bitl bs +let concretizable_bytls = List.all concretizable_bytl + +(* constructing values *) + +val build_register_value : list bit_lifted -> direction -> nat -> nat -> register_value +let build_register_value bs dir width start_index = + <| rv_bits = bs; + rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *) + rv_start_internal = start_index; + rv_start = if dir = D_increasing + then start_index + else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *) + |> + +val register_value : bit_lifted -> direction -> nat -> nat -> register_value +let register_value b dir width start_index = + build_register_value (List.replicate width b) dir width start_index + +val register_value_zeros : direction -> nat -> nat -> register_value +let register_value_zeros dir width start_index = + register_value Bitl_zero dir width start_index + +val register_value_ones : direction -> nat -> nat -> register_value +let register_value_ones dir width start_index = + register_value Bitl_one dir width start_index + +val byte_lifted_undef : byte_lifted +let byte_lifted_undef = Byte_lifted (List.replicate 8 Bitl_undef) + +val byte_lifted_unknown : byte_lifted +let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown) + +val memory_value_unknown : nat (*the number of bytes*) -> memory_value +let memory_value_unknown (width:nat) : memory_value = + List.replicate width byte_lifted_unknown + +val memory_value_undef : nat (*the number of bytes*) -> memory_value +let memory_value_undef (width:nat) : memory_value = + List.replicate width byte_lifted_undef + +(* lengths *) + +val memory_value_length : memory_value -> nat +let memory_value_length (mv:memory_value) = List.length mv + + +(* aux fns *) + +val maybe_all : forall 'a. list (maybe 'a) -> maybe (list 'a) +let rec maybe_all' xs acc = + match xs with + | [] -> Just (List.reverse acc) + | Nothing :: _ -> Nothing + | (Just y)::xs' -> maybe_all' xs' (y::acc) + end +let maybe_all xs = maybe_all' xs [] + +(** coercions *) + +(* bits and bytes *) + +let bit_to_bool = function (* TODO: rename bool_of_bit *) + | Bitc_zero -> false + | Bitc_one -> true +end + + +val bit_lifted_of_bit : bit -> bit_lifted +let bit_lifted_of_bit b = + match b with + | Bitc_zero -> Bitl_zero + | Bitc_one -> Bitl_one + end + +val bit_of_bit_lifted : bit_lifted -> maybe bit +let bit_of_bit_lifted bl = + match bl with + | Bitl_zero -> Just Bitc_zero + | Bitl_one -> Just Bitc_one + | Bitl_undef -> Nothing + | Bitl_unknown -> Nothing + end + + +val byte_lifted_of_byte : byte -> byte_lifted +let byte_lifted_of_byte (Byte bs) : byte_lifted = Byte_lifted (List.map bit_lifted_of_bit bs) + +val byte_of_byte_lifted : byte_lifted -> maybe byte +let byte_of_byte_lifted bl = + match bl with + | Byte_lifted bls -> + match maybe_all (List.map bit_of_bit_lifted bls) with + | Nothing -> Nothing + | Just bs -> Just (Byte bs) + end + end + + +val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*) +let rec bytes_of_bits bits = match bits with + | [] -> [] + | b0::b1::b2::b3::b4::b5::b6::b7::bits -> + (Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits) + | _ -> failwith "bytes_of_bits not given bits divisible by 8" +end + +val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*) +let rec byte_lifteds_of_bit_lifteds bits = match bits with + | [] -> [] + | b0::b1::b2::b3::b4::b5::b6::b7::bits -> + (Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits) + | _ -> failwith "byte_lifteds of bit_lifteds not given bits divisible by 8" +end + + +val byte_of_memory_byte : memory_byte -> maybe byte +let byte_of_memory_byte = byte_of_byte_lifted + +val memory_byte_of_byte : byte -> memory_byte +let memory_byte_of_byte = byte_lifted_of_byte + + +(* to and from nat *) + +(* this natFromBoolList could move to the Lem word.lem library *) +val natFromBoolList : list bool -> nat +let rec natFromBoolListAux (acc : nat) (bl : list bool) = + match bl with + | [] -> acc + | (true :: bl') -> natFromBoolListAux ((acc * 2) + 1) bl' + | (false :: bl') -> natFromBoolListAux (acc * 2) bl' + end +let natFromBoolList bl = + natFromBoolListAux 0 (List.reverse bl) + + +val nat_of_bit_list : list bit -> nat +let nat_of_bit_list b = + natFromBoolList (List.reverse (List.map bit_to_bool b)) + (* natFromBoolList takes a list with LSB first, for consistency with rest of Lem word library, so we reverse it. twice. *) + + +(* to and from integer *) + +val integer_of_bit_list : list bit -> integer +let integer_of_bit_list b = + integerFromBoolList (false,(List.reverse (List.map bit_to_bool b))) + (* integerFromBoolList takes a list with LSB first, so we reverse it *) + +val bit_list_of_integer : nat -> integer -> list bit +let bit_list_of_integer len b = + List.map (fun b -> if b then Bitc_one else Bitc_zero) + (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b))) + +val integer_of_byte_list : list byte -> integer +let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes) + +val byte_list_of_integer : nat -> integer -> list byte +let byte_list_of_integer (len:nat) (a:integer):list byte = + let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits + + +val integer_of_address : address -> integer +let integer_of_address (a:address):integer = + match a with + | Address bs i -> i + end + +val address_of_integer : integer -> address +let address_of_integer (i:integer):address = + Address (byte_list_of_integer 8 i) i + +(* to and from signed-integer *) + +val signed_integer_of_bit_list : list bit -> integer +let signed_integer_of_bit_list b = + match b with + | [] -> failwith "empty bit list" + | Bitc_zero :: b' -> + integerFromBoolList (false,(List.reverse (List.map bit_to_bool b))) + | Bitc_one :: b' -> + let b'_val = integerFromBoolList (false,(List.reverse (List.map bit_to_bool b'))) in + (* integerFromBoolList takes a list with LSB first, so we reverse it *) + let msb_val = integerPow 2 ((List.length b) - 1) in + b'_val - msb_val + end + + +(* regarding a list of int as a list of bytes in memory, MSB lowest-address first, convert to an integer *) +val integer_address_of_int_list : list int -> integer +let rec integerFromIntListAux (acc: integer) (is: list int) = + match is with + | [] -> acc + | (i :: is') -> integerFromIntListAux ((acc * 256) + integerFromInt i) is' + end +let integer_address_of_int_list (is: list int) = + integerFromIntListAux 0 is + +val address_of_byte_list : list byte -> address +let address_of_byte_list bs = + if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else + Address bs (integer_of_byte_list bs) + +(* operations on addresses *) + +val add_address_nat : address -> nat -> address +let add_address_nat (a:address) (i:nat) : address = + address_of_integer ((integer_of_address a) + (integerFromNat i)) + +val clear_low_order_bits_of_address : address -> address +let clear_low_order_bits_of_address a = + match a with + | Address [b0;b1;b2;b3;b4;b5;b6;b7] i -> + match b7 with + | Byte [bt0;bt1;bt2;bt3;bt4;bt5;bt6;bt7] -> + let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in + let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in + Address bytes (integer_of_byte_list bytes) + | _ -> failwith "Byte does not contain 8 bits" + end + | _ -> failwith "Address does not contain 8 bytes" + end + + + +val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) +let byte_list_of_memory_value endian mv = + let mv = if endian = E_big_endian then mv else List.reverse mv in + maybe_all (List.map byte_of_memory_byte mv) + + +val integer_of_memory_value : end_flag -> memory_value -> maybe integer +let integer_of_memory_value endian (mv:memory_value):maybe integer = + match byte_list_of_memory_value endian mv with + | Just bs -> Just (integer_of_byte_list bs) + | Nothing -> Nothing + end + +val memory_value_of_integer : end_flag -> nat -> integer -> memory_value +let memory_value_of_integer endian (len:nat) (i:integer):memory_value = + let mv = List.map (byte_lifted_of_byte) (byte_list_of_integer len i) in + if endian = E_big_endian then mv else List.reverse mv + + +val integer_of_register_value : register_value -> maybe integer +let integer_of_register_value (rv:register_value):maybe integer = + match maybe_all (List.map bit_of_bit_lifted rv.rv_bits) with + | Nothing -> Nothing + | Just bs -> Just (integer_of_bit_list bs) + end + +val register_value_of_integer : nat -> nat -> direction -> integer -> register_value +let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value = + let bs = bit_list_of_integer len i in + build_register_value (List.map bit_lifted_of_bit bs) dir len start + +(* *) + +val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode +let opcode_of_bytes b0 b1 b2 b3 : opcode = Opcode [b0;b1;b2;b3] + +val register_value_of_address : address -> direction -> register_value +let register_value_of_address (Address bytes _) dir : register_value = + let bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes in + <| rv_bits = bits; + rv_dir = dir; + rv_start = 0; + rv_start_internal = if dir = D_increasing then 0 else (List.length bits) - 1 + |> + +val register_value_of_memory_value : memory_value -> direction -> register_value +let register_value_of_memory_value bytes dir : register_value = + let bitls = List.concatMap (fun (Byte_lifted bs) -> bs) bytes in + <| rv_bits = bitls; + rv_dir = dir; + rv_start = 0; + rv_start_internal = if dir = D_increasing then 0 else (List.length bitls) - 1 + |> + +val memory_value_of_register_value: register_value -> memory_value +let memory_value_of_register_value r = + (byte_lifteds_of_bit_lifteds r.rv_bits) + +val address_lifted_of_register_value : register_value -> maybe address_lifted +(* returning Nothing iff the register value is not 64 bits wide, but +allowing Bitl_undef and Bitl_unknown *) +let address_lifted_of_register_value (rv:register_value) : maybe address_lifted = + if List.length rv.rv_bits <> 64 then Nothing + else + Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits) + (if List.all concretizable_bitl rv.rv_bits + then match (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) with + | (Just(bits)) -> Just (integer_of_bit_list bits) + | Nothing -> Nothing end + else Nothing)) + +val address_of_address_lifted : address_lifted -> maybe address +(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *) +let address_of_address_lifted (al:address_lifted): maybe address = + match al with + | Address_lifted bls (Just i)-> + match maybe_all ((List.map byte_of_byte_lifted) bls) with + | Nothing -> Nothing + | Just bs -> Just (Address bs i) + end + | _ -> Nothing +end + +val address_of_register_value : register_value -> maybe address +(* returning Nothing iff the register value is not 64 bits wide, or contains Bitl_undef or Bitl_unknown *) +let address_of_register_value (rv:register_value) : maybe address = + match address_lifted_of_register_value rv with + | Nothing -> Nothing + | Just al -> + match address_of_address_lifted al with + | Nothing -> Nothing + | Just a -> Just a + end + end + +let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address = + match byte_list_of_memory_value endian mv with + | Nothing -> Nothing + | Just bs -> + if List.length bs <> 8 then Nothing else + Just (address_of_byte_list bs) + end + +val byte_of_int : int -> byte +let byte_of_int (i:int) : byte = + Byte (bit_list_of_integer 8 (integerFromInt i)) + +val memory_byte_of_int : int -> memory_byte +let memory_byte_of_int (i:int) : memory_byte = + memory_byte_of_byte (byte_of_int i) + +(* +val int_of_memory_byte : int -> maybe memory_byte +let int_of_memory_byte (mb:memory_byte) : int = + failwith "TODO" +*) + + + +val memory_value_of_address_lifted : end_flag -> address_lifted -> memory_value +let memory_value_of_address_lifted endian (Address_lifted bs _ :address_lifted) = + if endian = E_big_endian then bs else List.reverse bs + +val byte_list_of_address : address -> list byte +let byte_list_of_address (Address bs _) : list byte = bs + +val memory_value_of_address : end_flag -> address -> memory_value +let memory_value_of_address endian (Address bs _) = + List.map byte_lifted_of_byte (if endian = E_big_endian then bs else List.reverse bs) + +val byte_list_of_opcode : opcode -> list byte +let byte_list_of_opcode (Opcode bs) : list byte = bs + +(** ****************************************** *) +(** show type class instantiations *) +(** ****************************************** *) + +(* matching printing_functions.ml *) +val stringFromReg_name : reg_name -> string +let stringFromReg_name r = match r with +| Reg s start size dir -> s +| Reg_slice s start dir (first,second) -> + let (first,second) = + match dir with + | D_increasing -> (first,second) + | D_decreasing -> (start - first, start - second) + end in + s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]" +| Reg_field s size dir f (first, second) -> + s ^ "." ^ f +| Reg_f_slice s start dir f (first1,second1) (first,second) -> + let (first,second) = + match dir with + | D_increasing -> (first,second) + | D_decreasing -> (start - first, start - second) + end in + s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]" +end + +instance (Show reg_name) + let show = stringFromReg_name +end + + +(* hex pp of integers, adapting the Lem string_extra.lem code *) +val stringFromNaturalHexHelper : natural -> list char -> list char +let rec stringFromNaturalHexHelper n acc = + if n = 0 then + acc + else + stringFromNaturalHexHelper (n / 16) (String_extra.chr (natFromNatural (let nd = n mod 16 in if nd <=9 then nd + 48 else nd - 10 + 97)) :: acc) + +val stringFromNaturalHex : natural -> string +let (*~{ocaml;hol}*) stringFromNaturalHex n = + if n = 0 then "0" else toString (stringFromNaturalHexHelper n []) + +val stringFromIntegerHex : integer -> string +let (*~{ocaml}*) stringFromIntegerHex i = + if i < 0 then + "-" ^ stringFromNaturalHex (naturalFromInteger i) + else + stringFromNaturalHex (naturalFromInteger i) + + +let stringFromAddress (Address bs i) = + let i' = integer_of_byte_list bs in + if i=i' then +(*TODO: ideally this should be made to match the src/pp.ml pp_address; the following very roughly matches what's used in the ppcmem UI, enough to make exceptions readable *) + if i < 65535 then + show i + else + stringFromIntegerHex i + else + "stringFromAddress bytes and integer mismatch" + +instance (Show address) + let show = stringFromAddress +end + +let stringFromByte_lifted bl = + match byte_of_byte_lifted bl with + | Nothing -> "u?" + | Just (Byte bits) -> + let i = integer_of_bit_list bits in + show i + end + +instance (Show byte_lifted) + let show = stringFromByte_lifted +end + +(* possible next instruction address options *) +type nia = + | NIA_successor + | NIA_concrete_address of address + | NIA_LR (* "LR0:61 || 0b00" in Power pseudocode *) + | NIA_CTR (* "CTR0:61 || 0b00" in Power pseudocode *) + | NIA_register of reg_name (* the address will be in a register, + corresponds to AArch64 BLR, BR, RET + instructions *) + +let niaCompare n1 n2 = match (n1,n2) with + | (NIA_successor,NIA_successor) -> EQ + | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2 + | (NIA_LR,NIA_LR) -> EQ + | (NIA_CTR,NIA_CTR) -> EQ + | (NIA_register r1,NIA_register r2) -> compare r1 r2 + + | (NIA_successor,_) -> LT + | (NIA_concrete_address _,_) -> LT + | (NIA_LR,_) -> LT + | (NIA_CTR,_) -> LT + | (_,_) -> GT + end + +instance (Ord nia) + let compare = niaCompare + let (<) n1 n2 = (niaCompare n1 n2) = LT + let (<=) n1 n2 = (niaCompare n1 n2) <> GT + let (>) n1 n2 = (niaCompare n1 n2) = GT + let (>=) n1 n2 = (niaCompare n1 n2) <> LT +end + +let stringFromNia = function + | NIA_successor -> "NIA_successor" + | NIA_concrete_address a -> "NIA_concrete_address " ^ show a + | NIA_LR -> "NIA_LR" + | NIA_CTR -> "NIA_CTR" + | NIA_register r -> "NIA_register " ^ show r +end + +instance (Show nia) + let show = stringFromNia +end + +type dia = + | DIA_none + | DIA_concrete_address of address + | DIA_register of reg_name + +let diaCompare d1 d2 = match (d1, d2) with + | (DIA_none, DIA_none) -> EQ + | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2 + | (DIA_register r1, DIA_register r2) -> compare r1 r2 + | (DIA_none, _) -> LT + | (DIA_concrete_address _, _) -> LT + | (DIA_register _, _) -> LT +end + +instance (Ord dia) + let compare = diaCompare + let (<) n1 n2 = (diaCompare n1 n2) = LT + let (<=) n1 n2 = (diaCompare n1 n2) <> GT + let (>) n1 n2 = (diaCompare n1 n2) = GT + let (>=) n1 n2 = (diaCompare n1 n2) <> LT +end + +let stringFromDia = function + | DIA_none -> "DIA_none" + | DIA_concrete_address a -> "DIA_concrete_address " ^ show a + | DIA_register r -> "DIA_delayed_register " ^ show r +end + +instance (Show dia) + let show = stringFromDia +end + + +type v_kind = Bitv | Bytev diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 7f9866f4..b73cb6e1 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2079,7 +2079,7 @@ let doc_id_lem_type (Id_aux(i,_)) = let doc_id_lem_ctor (Id_aux(i,_)) = match i with - | Id("bit") -> string "bit" + | Id("bit") -> string "bitU" | Id("int") -> string "integer" | Id("nat") -> string "integer" | Id("Some") -> string "Just" @@ -2145,7 +2145,9 @@ let doc_typ_lem, doc_atomic_typ_lem = if atyp_needed then parens tpp else tpp | _ -> atomic_typ atyp_needed regtypes ty and atomic_typ atyp_needed regtypes ((Typ_aux (t, _)) as ty) = match t with - | Typ_id (Id_aux (Id "bool",_)) -> string "bit" + | Typ_id (Id_aux (Id "bool",_)) -> string "bitU" + | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU" + | Typ_id (Id_aux (Id "bit",_)) -> string "bitU" | Typ_id ((Id_aux (Id name,_)) as id) -> if List.exists ((=) name) regtypes then string "register" @@ -3037,7 +3039,7 @@ let reg_decls (Defs defs) = (separate space [string "type";string "regstate";equals]) (anglebars ((separate_map (semi ^^ break 1)) - (fun (reg,_) -> separate space [string (String.lowercase reg);colon;string "vector bit"]) + (fun (reg,_) -> separate space [string (String.lowercase reg);colon;string "vector bitU"]) regs )) in diff --git a/src/process_file.ml b/src/process_file.ml index d12c1415..f1878609 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -179,7 +179,7 @@ let output1 libpath out_arg filename defs = let ((o2,_, _) as ext_o2) = open_output_with_check_unformatted (f' ^ "embed.lem") in (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename)) - ["Pervasives_extra";"Vector";"State";"Arch";"Sail_values"]; + ["Pervasives_extra";"Vector";"Prompt";"Arch";"Sail_values"]; close_output_with_check ext_o1; close_output_with_check ext_o2 | Lem_out (Some lib) -> @@ -188,7 +188,7 @@ let output1 libpath out_arg filename defs = let ((o2,_, _) as ext_o2) = open_output_with_check_unformatted (f' ^ "embed.lem") in (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename)) - ["Pervasives_extra";"Vector";"State";"Arch";"Sail_values"; lib]; + ["Pervasives_extra";"Vector";"Prompt";"Arch";"Sail_values"; lib]; close_output_with_check ext_o1; close_output_with_check ext_o2 | Ocaml_out None -> -- cgit v1.2.3