diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 13 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 3 |
2 files changed, 16 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 7b96aef5..68076627 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -39,6 +39,19 @@ let intern_value v = match v with | _ -> Interp.V_unknown end +let num_to_bits size kind num = + match kind with + | Bitv -> Bitvector (match (Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown); + Interp.V_lit(L_aux (L_num (integerFromNat num)) + Interp_ast.Unknown)]))) with + | Interp.V_vector _ _ bits -> from_bits bits end) true 0 + | Bytev -> + Bytevector (match (Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown); + Interp.V_lit(L_aux (L_num (integerFromNat num)) + Interp_ast.Unknown)]))) with + | Interp.V_vector _ _ bits -> (to_bytes (from_bits bits)) end) +end + let extern_reg r slice = match (r,slice) with | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2) diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index dca329e9..446c716c 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -99,6 +99,8 @@ Follows the form of the instruction in instruction_extractor, but populates the *) type instruction = (string * list (string * instr_parm_typ * value) * list base_effect) +type v_kind = Bitv | Bytev + type decode_error = | Unsupported_instruction_error of instruction | Not_an_instruction_error of value @@ -108,6 +110,7 @@ type i_state_or_error = | Instr of instruction * instruction_state | Decode_error of decode_error +val num_to_bits : nat -> v_kind -> integer (*Function to decode an instruction and build the state to run it*) val decode_to_istate : context -> value -> i_state_or_error |