From 33a6b4216a5cfba56e2c17eddb8f4242d1317a6f Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Wed, 19 Nov 2014 10:25:16 +0000
Subject: add byte_list_of_integer

---
 src/lem_interp/interp_inter_imp.lem | 20 +++++++++++++++-----
 src/lem_interp/interp_interface.lem |  3 +--
 2 files changed, 16 insertions(+), 7 deletions(-)

(limited to 'src')

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*)
-- 
cgit v1.2.3