diff options
| author | Kathy Gray | 2014-05-21 17:33:48 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-05-21 17:33:48 +0100 |
| commit | 5d8c5f14f8794501ebe2453d2fc97d51f16d2273 (patch) | |
| tree | 78ef74262818ee59f6decf0970b69af750dc81c9 /src/lem_interp/Interp_interface.lem | |
| parent | 6fbc244259891038bca6356669630eadb6ada7b5 (diff) | |
correct accidental capitalization of Interp in file name
Diffstat (limited to 'src/lem_interp/Interp_interface.lem')
| -rw-r--r-- | src/lem_interp/Interp_interface.lem | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem deleted file mode 100644 index 00c22bbe..00000000 --- a/src/lem_interp/Interp_interface.lem +++ /dev/null @@ -1,53 +0,0 @@ -import Interp -open import Num - -type read_kind = Interp.read_kind -type write_kind = Interp.write_kind -type barrier_kind = Interp.barrier_kind - -type word8 = nat (* bounded at a byte, for when lem supports it*) - -type value = -| Bitvector of list bool (* For register accesses *) -| Bytevector of list word8 (* For memory accesses *) -| Unknown - -type instruction_state = Interp.stack -type context = Interp.top_level - -type slice = (integer * integer) - -type reg_name = -| Reg of string (*Name of the register, accessing the entire register*) -| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*) -| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*) -| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *) - -type outcome = -| Read_mem of read_kind * value * (value -> instruction_state) -| Write_mem of write_kind * value * value * (bool -> instruction_state) -| Barrier of barrier_kind * instruction_state -| Read_reg of reg_name * (value -> instruction_state) -| Write_reg of reg_name * value * instruction_state -| Nondet_choice of list instruction_state -| Internal of instruction_state -| Done -| Error of string - -type event = -| E_read_mem of read_kind * value -| E_write_mem of write_kind * value -| E_barrier of barrier_kind -| E_read_reg of reg_name -| E_write_reg of reg_name -(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*) - - -val build_context : Interp_ast.defs Interp.tannot -> context -val initial_instruction_state : context -> string -> value -> instruction_state - -type interp_mode = <| eager_eval : bool |> -val interp : interp_mode -> instruction_state -> outcome - -val interp_exhaustive : instruction_state -> list event - |
