Handling many register reads, writes, and memory reads.

There are problems that warrant discussion about handling special registers that hold records or data structures previously.

4 files changed, 26 insertions, 8 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index bbcec75b..0bba3b7e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -2214,6 +2214,13 @@ let rec resume mode stack value =
     | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
     | Error l s -> Error l s
     end  
+  | (Hole_frame id exp t_level env mem stack, Nothing) ->
+    match resume mode stack Nothing with
+      | Value v ->
+	match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,_) -> o end
+      | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
+      | Error l s -> Error l s
+    end
   | (Thunk_frame exp t_level env mem Top,_) ->
     match interp_main mode t_level env mem exp with | (o,_,_) -> o end
   | (Thunk_frame exp t_level env mem stack,value) ->
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index ba501577..908b008f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -19,15 +19,17 @@ let to_bits l = (List.map (fun b -> match b with
 let from_bits l = (List.map (fun b -> match b with
                                  | Interp.V_lit (L_aux L_zero _) -> false
 				 | _ -> true end) l) 
-let rec to_bytes l = match l with
+let rec to_bytes l = match (List.reverse l) with
   | [] -> []
   | (a::b::c::d::e::f::g::h::rest) ->
-    (natFromInteger(integerFromBoolList (true,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
+    (natFromInteger(integerFromBoolList (false,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
 end
 		   
 let intern_value v = match v with
   | Bitvector bs -> Interp.V_vector 0 true  (to_bits bs)
-  | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))
+  | Bytevector bys -> Interp.V_vector 0 true 
+    (to_bits (List.reverse
+		(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
   | Unknown -> Interp.V_unknown
 end
 
@@ -40,11 +42,11 @@ end
 let extern_value mode for_mem v = match v with
   | Interp.V_vector _ true bits ->
     if for_mem 
-    then (Bytevector (to_bytes (from_bits bits)), Nothing)
+    then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing)
     else (Bitvector (from_bits bits), Nothing)
   | Interp.V_track (Interp.V_vector _ true bits) regs ->
     if for_mem
-    then (Bytevector (to_bytes (from_bits bits)), 
+    then (Bytevector (List.reverse (to_bytes (from_bits bits))), 
           if (mode.Interp.track_values) 
           then (Just (List.map (fun r -> extern_reg r Nothing) regs))
           else Nothing)
@@ -72,13 +74,20 @@ type mem_function = (string *
   Should probably be expanded into a parameter to mode as with above
 *)
 let memory_functions =
-  [ ("MEM", (Just(Read_plain), Just(Write_plain), 
+  [ ("MEMr", (Just(Read_plain), Nothing, 
 	     (fun mode v -> match v with
 	       | Interp.V_tuple [location;length] ->
 		 match length with
 		   | Interp.V_lit (L_aux (L_num len) _) ->
 		     let (v,regs) = extern_value mode true location in
 		     (v,len,regs) end end)));
+    ("MEMw", (Nothing, Just(Write_plain), 
+	      (fun mode v -> match v with
+		| Interp.V_tuple [location;length] ->
+		  match length with
+		    | Interp.V_lit (L_aux (L_num len) _) ->
+		      let (v,regs) = extern_value mode true location in
+		      (v,len,regs) end end)));
   ]
 
 let rec interp_to_outcome mode thunk = 
diff --git a/src/test/power.sail b/src/test/power.sail
index 5f1f532b..9a89c9e4 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -333,8 +333,8 @@ register (bit[64]) NIA (* next instruction address *)
 register (bit[64]) CIA (* current instruction address *)
 
 
-val extern forall Nat 'n. ( nat , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
-val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
 
 (* XXX effect for trap? *)
 val extern unit -> unit effect pure trap
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 667792c0..70cf5d4b 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -33,7 +33,9 @@ let mem = ref Mem.empty ;;
 
 let add_mem byte addr =
   assert(byte >= 0 && byte < 256);
+  (*Printf.printf "adder is %s, byte is %s\n" (Big_int.string_of_big_int addr) (string_of_int byte);*)
   let addr = big_int_to_vec true addr (Big_int.big_int_of_int 64) in
+  (*Printf.printf "adder is %s byte is %s\n" (val_to_string addr) (string_of_int byte);*)
   match addr with
     | Bytevector addr -> mem := Mem.add addr byte !mem
 ;;