diff options
| author | Peter Sewell | 2014-10-07 14:58:57 +0100 |
|---|---|---|
| committer | Peter Sewell | 2014-10-07 14:58:57 +0100 |
| commit | fc6c694210a35c121822cbfd6a8a60501f728309 (patch) | |
| tree | eb95b560e10ba08dbd032618922a2bae7f36f223 /src/lem_interp/interp_interface.lem | |
| parent | 66699a34c469caf667931975ba00775c7f6e8471 (diff) | |
kathy,peter: making decode integration with ppcmem2 typecheck
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index ec863a41..40c34480 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -38,9 +38,9 @@ type reg_name = 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 * maybe (list reg_name) * integer * maybe (list reg_name) * (value -> instruction_state) +| Read_mem of read_kind * value * integer * maybe (list reg_name) * (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 * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) +| Write_mem of write_kind * value * integer * maybe (list reg_name) * 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 *) @@ -57,8 +57,8 @@ type outcome = | Error of string type event = -| E_read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) -| E_write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) +| 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_barrier of barrier_kind | E_read_reg of reg_name | E_write_reg of reg_name * value @@ -71,7 +71,7 @@ val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come val initial_instruction_state : context -> string -> list value -> instruction_state (* string is a function name, list of value are the parameters to that function *) -(*Type representint the constructor parameters in instruction_form, other is a type not representable externally*) +(*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*) | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *) @@ -80,15 +80,15 @@ type instr_parm_typ = (*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_form = (string * list (string * instr_parm_typ * value) * list base_effect) +type instruction = (string * list (string * instr_parm_typ * value) * list base_effect) type decode_error = - | Unsupported_instruction_error of instruction_form + | Unsupported_instruction_error of instruction | Not_an_instruction_error of value | Internal_error of string type i_state_or_error = - | Instr of instruction_form * instruction_state + | Instr of instruction * instruction_state | Decode_error of decode_error |