diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index b4a6c92b..bf6c6779 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -20,6 +20,104 @@ open import Num open import Assert_extra +(*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)) + +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 + + +let decode_error_compare e1 e2 = + match (e1, e2) with + | (Unsupported_instruction_error i1, Unsupported_instruction_error i2) + -> defaultCompare i1 i2 + | (Unsupported_instruction_error _, _) -> LT + | (_, Unsupported_instruction_error _) -> GT + + | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2 + | (Not_an_instruction_error _, _) -> LT + | (_, Not_an_instruction_error _) -> GT + + | (Internal_error s1, Internal_error s2) -> compare s1 s2 + (* | (Internal_error _, _) -> LT *) + (* | (_, Internal_error _) -> GT *) + end + +let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT +let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT +let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT +let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT + +instance (Ord decode_error) + let compare = decode_error_compare + let (<) = decode_error_less + let (<=) = decode_error_less_eq + let (>) = decode_error_greater + let (>=) = decode_error_greater_eq +end + +let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ +let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2) + +instance (Eq decode_error) + let (=) = decode_error_equal + let (<>) = decode_error_inequal +end + + 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*) |