diff options
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 20 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 3 |
2 files changed, 16 insertions, 7 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 4aacad5f..67bf42c7 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -43,17 +43,27 @@ let intern_value v = match v with | _ -> Interp.V_unknown end +let byte_list_of_integer size num = + if (num < 0) + then failwith "signed integer given to byte_list_of_integer" + else let internal_value = (Interp_lib.to_vec_inc + (Interp.V_tuple([Interp.V_lit(L_aux (L_num (size * 8)) Interp_ast.Unknown); + Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) in + let num_check = Interp_lib.to_num Interp_lib.Unsigned internal_value in + match (num_check,internal_value) with + | (Interp.V_lit (L_aux (L_num n) _), Interp.V_vector _ _ bits) -> + if num = n + then (to_bytes (from_bits bits)) + else failwith "byte_list_of_integer given an integer larger than given size" + 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 (integerFromNat size)) Interp_ast.Unknown); Interp.V_lit(L_aux (L_num 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 (integerFromNat size)) Interp_ast.Unknown); - Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) with - | Interp.V_vector _ _ bits -> (to_bytes (from_bits bits)) end) + | Bytev -> Bytevector (byte_list_of_integer (integerFromNat (size/8)) num) end let integer_of_byte_list bytes = diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 2e782f65..5c77e807 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -234,8 +234,7 @@ val num_to_bits : nat -> v_kind -> integer -> value val integer_of_byte_list : list word8 -> integer -(** proposed: *) -val nat_to_bytevector : nat -> list word8 +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*) |