diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 78 |
1 files changed, 45 insertions, 33 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 834f3039..c4dc00f9 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -17,7 +17,7 @@ type read_kind = Read_plain | Read_reserve | Read_acquire type write_kind = Write_plain | Write_conditional | Write_release type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *) -type value = +(*type value = | Bitvector of list bool * bool * integer (* In Bitvector bs b n: - the bs are the bits (true represents 1 and false represents 0) @@ -72,7 +72,7 @@ instance (Eq value) let (=) = valueEqual let (<>) x y = not (valueEqual x y) end - +*) type slice = (integer * integer) @@ -136,20 +136,36 @@ instance (Ord reg_name) let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT end +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; rv_dir: direction; rv_start: integer |> + +type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) + +type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) +type memory_value = list byte_lifted (* arbitrary length, > 1 *) 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 * value * integer * maybe (list reg_name) * (value -> instruction_state) +| Read_mem of read_kind * address_lifted * integer * 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 * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) +| Write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state (* Request to read register, will track dependency when mode.track_values *) -| Read_reg of reg_name * (value -> instruction_state) +| Read_reg of reg_name * (register_value -> instruction_state) (* Request to write register *) -| Write_reg of reg_name * value * instruction_state +| 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 (* Stop for incremental stepping, function can be used to display function call data *) @@ -160,13 +176,13 @@ type outcome = | Error of string type event = -| E_read_mem of read_kind * value * integer * maybe (list reg_name) -| E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) +| E_read_mem of read_kind * address_lifted * integer * maybe (list reg_name) +| E_write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name) | E_barrier of barrier_kind | E_read_reg of reg_name -| E_write_reg of reg_name * value +| E_write_reg of reg_name * register_value +| E_escape | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*) -(*should there be a representation for escape down here?*) (*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*) @@ -204,7 +220,7 @@ instance forall 'a. Ord 'a => (Ord (maybe 'a)) end -let eventCompare e1 e2 = +(*let 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')) @@ -220,17 +236,17 @@ let eventCompare e1 e2 = | _ -> GT end - +*) instance (SetType event) - let setElemCompare = eventCompare + let setElemCompare = defaultCompare end (* Functions to build up the initial state for interpretation *) val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*) -val initial_instruction_state : context -> string -> list value -> instruction_state +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*) @@ -254,7 +270,7 @@ 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 * value) * list base_effect) +type instruction = (string * list (string * instr_parm_typ * register_value) * list base_effect) let instructionEqual i1 i2 = match (i1,i2) with | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2 @@ -264,7 +280,7 @@ type v_kind = Bitv | Bytev type decode_error = | Unsupported_instruction_error of instruction - | Not_an_instruction_error of value + | Not_an_instruction_error of register_value | Internal_error of string type instruction_or_decode_error = @@ -276,7 +292,10 @@ type i_state_or_error = | Instr of instruction * instruction_state | Decode_error of decode_error -val num_to_bits : nat -> v_kind -> integer -> value +(*val num_to_bits : nat -> v_kind -> integer -> value*) + +val byte_to_bits : word8 -> list bit_lifted +val bits_to_byte : list bit_lifted -> word8 val integer_of_byte_list : list word8 -> integer @@ -284,45 +303,38 @@ val byte_list_of_integer : integer -> integer -> list word8 (** propose to remove this: Function to decode an instruction and build the state to run it*) -val decode_to_istate : context -> value -> i_state_or_error +val decode_to_istate : context -> register_value -> 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 -> value -> instruction_or_decode_error +val decode_to_instruction : context -> register_value -> 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 -> i_state_or_error (* Augment an address by the given value *) -val add_to_address : value -> integer -> value +(*val add_to_address : value -> integer -> value (* Coerce a Bitvector value (presumed a multiple of 8 bits long) to a Bytevector value *) val coerce_Bytevector_of_Bitvector : value -> value (* Coerce a Bytevector value to a Bitvector value, increasing and starting at zero *) -val coerce_Bitvector_of_Bytevector : value -> value +val coerce_Bitvector_of_Bytevector : value -> value*) -(* Slice a value into a smaller vector, starting at first number (wrt the indices of the bitvector value, not raw positions in its list of bits) and going to second (inclusive) according to order. - For bytevectors, assumes you are slicing at the byte level, not the bit level *) -val slice_value : value -> nat -> nat -> value +(* 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 -(*append two vectors (bit x byte -> bit) *) -val append_value : value -> value -> value +(*(*append two vectors (bit x byte -> bit) *) +val append_value : value -> value -> 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 * value)) -> instruction_state -> list event +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)) -(*To discuss: Are these functions needed, since the memory requests carry the register dependencies for that request? *) -val mem_read_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory reads to compute the addressses in is*) - -val mem_write_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory writes to compute the address (and value?, in a separate list?)*) - - |