Add a num to bits function; start hooking up the power.ml file to the symbol/memory address list.

3 files changed, 37 insertions, 12 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
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 96f64efe..e3fcf182 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -15,6 +15,7 @@ let print_bytes = ref false ;;
 let bytes_file = ref "bytes_out.lem";;
 let test_format = ref false ;;
 let test_file = ref "test.txt";;
+let test_memory_addr = ref (0,[]) ;;
 
 let rec foldli f acc ?(i=0) = function
   | [] -> acc
@@ -77,6 +78,15 @@ let load_memory (bits,addr) =
 	 loop rest (1 + addr)
   in loop bits addr
 
+let rec read_mem loc length = 
+  if length = 0  
+  then []
+  else 
+    let location = big_int_to_vec true loc (big_int_of_int 64) in
+    match location with
+      | Bytevector location ->
+	(Mem.find location !mem)::(read_mem (add_big_int loc unit_big_int) (length - 1))
+
 let get_reg reg name =
   let reg_content = Reg.find name reg in reg_content
 
@@ -277,30 +287,29 @@ let run () =
   end;
   if !eager_eval then Run_interp_model.debug := true;
   if !test_format then Run_interp_model.debug := false;
-  let ((locations,start_address),_) = populate !file in
+  let (((locations,start_address),_),(symbol_map)) = populate_and_obtain_symbol_to_address_mapping !file in
   let total_size = (List.length locations) in
   if not(!test_format)
   then eprintf "Loading binary into memory (%d sections)... %!" total_size;
   let t = time_it (List.iter load_memory) locations in
   if not(!test_format)
   then eprintf "done. (%f seconds)\n%!" t;
-  let rec reading loc length = 
-    if length = 0  
-    then []
-    else 
-      let location = big_int_to_vec true loc (big_int_of_int 64) in
-      match location with
-	| Bytevector location ->
-	  (Mem.find location !mem)::(reading (add_big_int loc unit_big_int) (length - 1)) in
-  let addr = reading (big_int_of_int start_address) 8 in
+  let addr = read_mem (big_int_of_int start_address) 8 in
   let _ = begin
     startaddr := addr;
     mainaddr := "0x" ^ (List.fold_left (^) "" (List.map (Printf.sprintf "%02x") addr));
   end in
-  Printf.printf "start address: %s\n" !mainaddr;
-(*  Printf.printf "%s\n" (Printing_functions.val_to_string (Bytevector !startaddr));*)
+  if not(!test_format) then
+    Printf.printf "start address: %s\n" !mainaddr;
   let my_reg = init_reg () in
   reg := my_reg;
+  if !test_format 
+  then if List.mem_assoc "TEST_MEM" symbol_map
+    then test_memory_addr := 
+      let num = (List.assoc "TEST_MEM" symbol_map) in
+      match big_int_to_vec true (big_int_of_int num) (big_int_of_int 64) with
+	| Bytevector location -> (num,location);
+    else ();
   (* entry point: unit -> unit fde *)
   let funk_name = "fde" in
   let parms = [] in