(* PS NOTES FOR KATHY: pls also change: decode_to_istate decode_to_instruction to take an opcode as defined above, instead of a value and change *) import Interp open import Interp_ast open import Pervasives 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*) type interpreter_mode = Interp.interp_mode (*Deem abstract*) 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 (b1,i1) (b2,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 ~{ocaml} reg_nameCompare r1 r2 = match (r1,r2) with | (Reg s1 ns1 nz1 l1, Reg s2 ns2 nz2 l2) -> compare (s1,ns1,nz1,l1) (s2,ns2,nz2,l2) | (Reg_slice s1 ns1 d1 sl1, Reg_slice s2 ns2 d2 sl2) -> compare(s1,ns1,d1,sl1) (s2,ns2,d2,sl2) | (Reg_field s1 ns1 d1 f1 sl1, Reg_field s2 ns2 d2 f2 sl2) -> compare ((s1,ns1,d2),f1,sl1) ((s2,ns2,d2),f2,sl2) | (Reg_f_slice s1 ns1 d1 f1 sl1 sl1', Reg_f_slice s2 ns2 d2 f2 sl2 sl2') -> compare ((s1,ns1,d1),(f1,sl1,sl1')) ((s2,ns2,d2),(f2,sl2,sl2')) | (Reg _ _ _ _, _) -> LT | (Reg_slice _ _ _ _, _) -> LT | (Reg_field _ _ _ _ _, _) -> LT | (_, _) -> GT end let inline {ocaml} reg_nameCompare = defaultCompare let ~{ocaml} reg_nameLess b1 b2 = reg_nameCompare b1 b2 = LT let ~{ocaml} reg_nameLessEq b1 b2 = reg_nameCompare b1 b2 <> GT let ~{ocaml} reg_nameGreater b1 b2 = reg_nameCompare b1 b2 = GT let ~{ocaml} reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT let inline {ocaml} reg_nameLess = defaultLess let inline {ocaml} reg_nameLessEq = defaultLessEq let inline {ocaml} reg_nameGreater = defaultGreater let inline {ocaml} reg_nameGreaterEq = defaultGreaterEq instance (Ord reg_name) let compare = reg_nameCompare let (<) = reg_nameLess let (<=) = reg_nameLessEq let (>) = reg_nameGreater let (>=) = reg_nameGreaterEq end let {coq} reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ let inline ~{coq} reg_nameEqual = unsafe_structural_equality let {coq} reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2) let inline ~{coq} reg_nameInequal = unsafe_structural_inequality 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 (*For reading the tag of tagged memory*) (* Power reads *) | Read_reserve (* AArch64 reads *) | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream type write_kind = (* common writes *) Write_plain | Write_tag (*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 (*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)) (*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*) type barriers = list (string * barrier_kind) type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name)) type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) type memory_write_ea = MEA of write_kind * memory_parameter_transformer type memory_write_eas = list (string * memory_write_ea) type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state)) and memory_writes = list (string * memory_write) and memory_write_val = MV of maybe (instruction_state -> bool -> instruction_state) and memory_write_vals = list (string * memory_write_val) (* Definition information needed to run an instruction *) and context = Context of Interp.top_level * direction * memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions (* An instruction in flight *) and instruction_state = IState of interpreter_state * context type outcome = (* 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 *) | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * (memory_value -> instruction_state) (* Request to write memory, first value and dependent registers is location, second is the value to write *) | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state) (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *) | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state (* Request to write memory at last signaled address. Memory value should be 8* the size given in ea signal *) | Write_memv of memory_value * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state (* Tell the system to dynamically recalculate dependency footprint *) | Footprint of instruction_state (* Request to read register, will track dependency when mode.track_values *) | Read_reg of reg_name * (register_value -> instruction_state) (* Request to write register *) | Write_reg of reg_name * register_value * instruction_state (* 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*) | Escape of maybe instruction_state * instruction_state (*Result of a failed assert with possible error message to report*) | Fail of maybe string (* Stop for incremental stepping, function can be used to display function call data *) | Internal of maybe string * maybe (unit -> string) * instruction_state (* Analysis can lead to non_deterministic evaluation, represented with this outcome *) (*Note: this should not be externally visible *) | Analysis_non_det of list instruction_state * instruction_state (*Completed interpreter*) | Done (*Interpreter error*) | Error of string type event = | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name) | E_write_memv of memory_value * maybe (list reg_name) | E_barrier of barrier_kind | E_footprint | E_read_reg of reg_name | E_write_reg of reg_name * register_value | 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 | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> compare ((wk1,v1,i1),(tr1,v1',tr1')) ((wk2,v2,i2),(tr2,v2',tr2')) | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) -> compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2)) | (E_write_memv mv1 tr1, E_write_memv mv2 tr2) -> compare (mv1,tr1) (mv2,tr2) | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2 | (E_read_reg r1, E_read_reg r2) -> compare r1 r2 | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2) | (E_error s1, E_error s2) -> compare s1 s2 | (E_escape,E_escape) -> EQ | (E_read_mem _ _ _ _, _) -> LT | (E_write_mem _ _ _ _ _ _, _) -> LT | (E_write_ea _ _ _ _, _) -> LT | (E_write_memv _ _, _) -> LT | (E_barrier _, _) -> LT | (E_read_reg _, _) -> LT | (E_write_reg _ _, _) -> LT | _ -> GT end let inline {ocaml} eventCompare = defaultCompare let ~{ocaml} eventLess b1 b2 = eventCompare b1 b2 = LT let ~{ocaml} eventLessEq b1 b2 = eventCompare b1 b2 <> GT let ~{ocaml} eventGreater b1 b2 = eventCompare b1 b2 = GT let ~{ocaml} eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT let inline {ocaml} eventLess = defaultLess let inline {ocaml} eventLessEq = defaultLessEq let inline {ocaml} eventGreater = defaultGreater let inline {ocaml} eventGreaterEq = defaultGreaterEq instance (Ord event) let compare = eventCompare let (<) = eventLess let (<=) = eventLessEq let (>) = eventGreater let (>=) = eventGreaterEq end 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 | Decode_error of decode_error (** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*) val decode_to_istate : context -> maybe (list (reg_name * register_value)) -> opcode -> i_state_or_error (** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*) (** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction. This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *) val decode_to_instruction : context -> maybe (list (reg_name * register_value))-> opcode -> instruction_or_decode_error (*Function to generate the state to run from an instruction form; is always an Instr*) val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*) (* Slice a register value into a smaller vector, starting at first number (wrt the indices of the register value, not raw positions in its list of bits) and going to second (inclusive) according to order. *) val slice_reg_value : register_value -> nat -> nat -> register_value (*Create a new register value where the contents of nat to nat are replaced by the second register_value *) val update_reg_value_slice : reg_name -> register_value -> nat -> nat -> register_value -> register_value (* Big step of the interpreter, to the next request for an external action *) (* When interp_mode has eager_eval false, interpreter is (close to) small step *) val interp : interp_mode -> instruction_state -> outcome (* Run the interpreter without external interaction, feeding in Unknown on all reads except for those register values provided *) val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event (* 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 nat 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 *) (** ****************************************** *) let stringFromAddress (Address bs i) = let i' = integer_of_byte_list bs in if i=i' then show i (*TODO: should be made to match the src/pp.ml pp_address*) 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