Fix some interpreter bugs preventing ARM instructions from making progress

4 files changed, 83 insertions, 103 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index da617824..b1ee613d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -837,30 +837,33 @@ let rec to_exp mode env v : (exp tannot * lenv) =
   | V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env)
 end
 
-val env_to_let : interp_mode -> lenv -> (exp tannot) -> (exp tannot)
-let rec env_to_let_help mode env = match env with
-  | [] -> []
+val env_to_let : interp_mode -> lenv -> (exp tannot) -> lenv -> ((exp tannot) * lenv)
+let rec env_to_let_help mode env taint_env = match env with
+  | [] -> ([],taint_env)
   | (i,v)::env -> 
     let t = (val_typ v) in
     let tan = (val_annot t) in
-    let (e,_) = to_exp <| mode with track_values = false |> eenv v in
-    (((P_aux (P_id i) (Unknown,tan)),e),t)::(env_to_let_help mode env)
+    let (e,taint_env) = to_exp mode taint_env v in
+    let (rest,taint_env) = env_to_let_help mode env taint_env in
+    ((((P_aux (P_id i) (Unknown,tan)),e),t)::rest, taint_env)
 end 
 
-let env_to_let mode (LEnv _ env) (E_aux e annot) = 
-  match env_to_let_help mode env with
-    | [] -> E_aux e annot
-    | [((p,e),t)] -> E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot
-    | pts -> let ts = List.map snd pts in
-	     let pes = List.map fst pts in
-	     let ps = List.map fst pes in
-	     let es = List.map snd pes in
-	     let t = T_tup ts in
-	     let tan = val_annot t in
-	     E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan))
-				                   (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
-		           (E_aux e annot))
-	           annot
+let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env = 
+  match env_to_let_help mode env taint_env with
+    | ([],taint_env) -> (E_aux e annot,taint_env)
+    | ([((p,e),t)],tain_env) ->
+      (E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot,taint_env)
+    | (pts,taint_env) ->
+      let ts = List.map snd pts in
+      let pes = List.map fst pts in
+      let ps = List.map fst pes in
+      let es = List.map snd pes in
+      let t = T_tup ts in
+      let tan = val_annot t in
+      (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan))
+			       (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
+		    (E_aux e annot))
+	annot, taint_env)
 end
 
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
@@ -897,7 +900,7 @@ let rec match_pattern (P_aux p _) value_whole =
    if matched_p then
      (matched_p,used_unknown,(LEnv bi ((id,value_whole)::bounds)))
    else (false,false,eenv)
- | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information, but that's looking less useful *)
+ | P_typ typ pat -> match_pattern pat value_whole (* Might like to destructure against the type to get information, but that's looking less useful *)
  | P_id id -> (true, false, (LEnv 0 [(id,value_whole)]))
  | P_app (Id_aux id _) pats -> 
    match value with
@@ -1324,13 +1327,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (fun v lm le ->
           match find_case pats v with
             | [] -> (Error l ("No matching patterns in case for value " ^ (string_of_value v)),lm,le)
-            | [(env,used_unknown,exp)] -> 
+            | [(env,_,exp)] -> 
 	      if mode.eager_eval
 	      then interp_main mode t_level (union_env env l_env) lm exp
 	      else debug_out Nothing Nothing exp t_level lm (union_env env l_env)
 	    | multi_matches ->
-	      let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
-	      interp_main mode t_level l_env lm (E_aux (E_block lets) (l,annot))
+	      let (lets,taint_env) = 
+		List.foldr (fun (env,_,exp) (rst,taint_env) -> 
+		  let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+	      interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
 	 end)
         (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env))))
     | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> 
@@ -1715,7 +1720,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		| [] -> 
 		  (Error l ("No matching pattern for function " ^ name ^
 			       " on value " ^ (string_of_value v)),l_mem,l_env)
-		| [(env,used_unknown,exp)] -> 
+		| [(env,_,exp)] -> 
 		  resolve_outcome 
                     (if mode.eager_eval 
 		     then (interp_main mode t_level env emem exp)
@@ -1726,9 +1731,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 				       (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
 				       t_level l_env l_mem stack)))
                 | multi_matches ->
-                  let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
-                  interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot))
-               end)
+		  let (lets,taint_env) = 
+		    List.foldr (fun (env,_,exp) (rst,taint_env) -> 
+		      let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+		  interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
+	       end)
             | Nothing -> 
 	      (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
 	| Tag_empty -> 
@@ -1788,8 +1795,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
 	  else if has_wmem_effect effects
 	  then 
-	    (*TODO This is wrong, need to split up value or unsplit generally*)
-	    (Action (Write_mem (id_of_string name_ext) v Nothing v) 
+	    let (wv,v) =
+	      match v with
+		| V_tuple params_list ->
+		  let reved = List.reverse params_list in
+		  (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) end in 
+	    (Action (Write_mem (id_of_string name_ext) v Nothing wv) 
 	       (Hole_frame (Id_aux (Id "0") l)
 		  (E_aux (E_id (Id_aux (Id "0") l)) (l, intern_annot annot)) t_level le lm Top),lm,le)
           else 
@@ -2090,8 +2101,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 					   t_level l_env l_mem stack))), l_mem,l_env), Nothing)
 		    | (e,lm,le) -> ((e,lm,le),Nothing) end)
                 | multi_matches ->
-                  let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
-                  (interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot)), Nothing)
+		  let (lets,taint_env) = 
+		    List.foldr (fun (env,_,exp) (rst,taint_env) -> 
+		      let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+		  (interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)), Nothing)
                end)
             | Nothing -> 
 	      ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
@@ -2473,7 +2486,7 @@ let interp mode external_functions defs exp =
 
 let rec resume_with_env mode stack value =
   match (stack,value) with
-  | (Top,_) -> (Error Unknown "Top hit without expression to evaluate",eenv)
+  | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume_with_env",eenv)
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
     match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,e) -> (o,e) end 
   | (Hole_frame id exp t_level env mem stack,Just value) ->
@@ -2503,9 +2516,11 @@ let rec resume_with_env mode stack value =
 
 let rec resume mode stack value =
   match (stack,value) with
-  | (Top,_) -> Error Unknown "Top hit without expression to evaluate"
+  | (Top,_) -> Error Unknown "Top hit without expression to evaluate in resume"
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
     match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,_) -> o end 
+  | (Hole_frame id exp t_level env mem Top,Nothing) ->
+    Error Unknown "Top hole frame hit wihtout a value in resume"
   | (Hole_frame id exp t_level env mem stack,Just value) ->
     match resume mode stack (Just value) with
     | Value v -> 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 690f8bcf..da87842d 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -437,7 +437,7 @@ let rec interp_to_outcome mode context thunk =
 	  length tracking value v_tracking 
 	  (fun b -> 
 	    match return with 
-	      | Nothing -> (IState next_state context)
+	      | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
 	      | Just return_bool -> return_bool (IState next_state context) b end)
 	else Error "Memory address on write is not 64 bits"
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index ee141275..4b9cd8b4 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -579,7 +579,9 @@ let mask direction (V_tuple [vsize;v]) = retaint v (match (detaint v,detaint vsi
     let current_size = List.length l in
     V_vector (if is_inc(d) then 0 else (n-1)) d (drop (current_size - n) l) 
   | (V_unknown,V_lit (L_aux (L_num n) _)) -> 
-    V_vector 0 direction (List.replicate (natFromInteger n) V_unknown)
+    let nat_n = natFromInteger n in
+    let start_num = if is_inc(direction) then 0 else nat_n -1 in
+    V_vector start_num direction (List.replicate nat_n V_unknown)
 					  end)
 
 let library_functions direction = [
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 57f3f7c1..d865bcf9 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -3,13 +3,12 @@ open Interp_ast ;;
 open Interp_interface ;;
 open Interp_inter_imp ;;
 
-open Big_int ;;
 open Printing_functions ;;
 
 module Reg = struct
   include Map.Make(struct type t = string let compare = compare end)
   let to_string id v = 
-    sprintf "%s -> %s" id (val_to_string v)
+    sprintf "%s -> %s" id (register_value_to_string v)
   let find id m = 
 (*    eprintf "reg_find called with %s\n" id; *)
     let v = find id m in
@@ -17,13 +16,14 @@ module Reg = struct
     v
 end ;;
 
-let compare_bytes v1 v2 = 
+let compare_addresses v1 v2 = 
   let rec comp v1s v2s = match (v1s,v2s) with
     | ([],[]) -> 0
     | (v1::v1s,v2::v2s) -> 
       match compare v1 v2 with
 	| 0 -> comp v1s v2s
 	| ans -> ans in 
+  
   let l1 = List.length v1 in
   let l2 = List.length v2 in
   if l1 > l2 then 1
@@ -32,8 +32,8 @@ let compare_bytes v1 v2 =
 
 module Mem = struct
   include Map.Make(struct
-    type t = word8 list
-    let compare v1 v2 = compare_bytes v1 v2
+    type t = address_lifted
+    let compare v1 v2 = compare_addresses v1 v2
   end)
   let find idx m = 
 (*    eprintf "mem_find called with %s\n" (val_to_string (Bytevector idx));*)
@@ -45,32 +45,22 @@ module Mem = struct
     add key valu m
 
   let to_string loc v =
-    sprintf "[%s] -> %x" (val_to_string (Bytevector loc)) v
+    sprintf "[%s] -> %s" (memory_value_to_string (memory_value_of_address_lifted loc)) (memory_value_to_string v)
 end ;;
 
-let rec slice bitvector (start,stop) = 
-  match bitvector with
-    | Bitvector(bools, inc, fst) -> 
-      Bitvector ((Interp.from_n_to_n (if inc then (sub_big_int start fst) else (sub_big_int fst start))
-                                    (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bools),
-                 inc,
-                 (if inc then start else (add_big_int (sub_big_int stop start) unit_big_int)))
-                
-    | Bytevector bytes -> 
-      Bytevector((Interp.from_n_to_n start stop bytes)) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
-    | Unknown0 -> Unknown0
-;;
+let slice register_vector (start,stop) = slice_reg_value register_vector start stop
+
+let big_num_unit = Nat_big_num.of_int 1
 
 let rec list_update index start stop e vals =  
  match vals with
     | []      -> []
     | x :: xs -> 
-      if eq_big_int index stop 
+      if Nat_big_num.equal index stop 
       then e :: xs 
-      else if ge_big_int index start
-      then e :: (list_update (add_big_int index unit_big_int) start stop e xs)
-      else x :: (list_update (add_big_int index unit_big_int) start stop e xs)
-;;
+      else if Nat_big_num.greater_equal index start
+      then e :: (list_update (Nat_big_num.add index big_num_unit) start stop e xs)
+      else x :: (list_update (Nat_big_num.add index big_num_unit) start stop e xs)
 
 let rec list_update_list index start stop es vals =
   match vals with
@@ -79,56 +69,29 @@ let rec list_update_list index start stop es vals =
     match es with
     | [] -> xs
     | e::es ->
-      if eq_big_int index stop
+      if Nat_big_num.equal index stop
       then e::xs
-      else if ge_big_int index start
-      then e :: (list_update_list (add_big_int index unit_big_int) start stop es xs)
-      else x :: (list_update_list (add_big_int index unit_big_int) start stop (e::es) xs)
-;;
+      else if Nat_big_num.greater_equal index start
+      then e :: (list_update_list (Nat_big_num.add index big_num_unit) start stop es xs)
+      else x :: (list_update_list (Nat_big_num.add index big_num_unit) start stop (e::es) xs)
 
-let fupdate_slice original e (start,stop) =
-  match original with
-    | Bitvector(bools,inc,fst) -> 
-      (match e with 
-      | Bitvector ([b],_,_) -> 
-        Bitvector((list_update zero_big_int 
-                               (if inc then (sub_big_int start fst) else (sub_big_int fst start))
-                               (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) b bools), inc, fst)
-      | Bitvector(bs,_,_) -> 
-        Bitvector((list_update_list zero_big_int 
-                                    (if inc then (sub_big_int start fst) else (sub_big_int fst start))
-                                    (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bs bools), inc, fst)
-      | _ -> Unknown0)
-    | Bytevector bytes -> (*Can this happen?*)
-      (match e with
-      | Bytevector [byte] -> 
-        Bytevector (list_update zero_big_int start stop byte bytes)
-      | Bytevector bs ->
-        Bytevector (list_update_list zero_big_int start stop bs bytes)
-      | _ -> Unknown0)
-    | Unknown0 -> Unknown0
-;;
+let fupdate_slice original e (start,stop) = assert false
 
-let combine_slices (start, stop) (inner_start,inner_stop) = (add_big_int start inner_start, add_big_int start inner_stop)
-
-let increment bytes = 
-  let adder byte (carry_out, bytes) = 
-    let new_byte = carry_out + byte in 
-    if new_byte > 255 then (1,0::bytes) else (0,new_byte::bytes)
-  in (snd (List.fold_right adder bytes (1,[])))
-;;
-let unit_lit = (L_aux(L_unit,Interp_ast.Unknown))
+let increment address = address (*Need to increment this *)
 
+let combine_slices (start, stop) (inner_start,inner_stop) = 
+  (start + inner_start, start + inner_stop)
 
+let unit_lit = (L_aux(L_unit,Interp_ast.Unknown))
 
 let rec perform_action ((reg, mem) as env) = function
  (* registers *)
- | Read_reg0((Reg0 id), _) -> (Some(Reg.find id reg), env)
+ | Read_reg0(Reg0(id,_), _) -> (Some(Reg.find id reg), env)
  | Read_reg0(Reg_slice(id, range), _)
  | Read_reg0(Reg_field(id, _, range), _) -> (Some(slice (Reg.find id reg) range), env)
  | Read_reg0(Reg_f_slice(id, _, range, mini_range), _) ->
    (Some(slice (slice (Reg.find id reg) range) mini_range),env)
- | Write_reg0(Reg0 id, value, _) -> (None, (Reg.add id value reg,mem))
+ | Write_reg0(Reg0(id,_), value, _) -> (None, (Reg.add id value reg,mem))
  | Write_reg0(Reg_slice(id,range),value, _) 
  | Write_reg0(Reg_field(id,_,range),value,_)->
      let old_val = Reg.find id reg in
@@ -138,20 +101,20 @@ let rec perform_action ((reg, mem) as env) = function
    let old_val = Reg.find id reg in
    let new_val = fupdate_slice old_val value (combine_slices range mini_range) in
    (None,(Reg.add id new_val reg,mem))
- | Read_mem0(_,(Bytevector location), length, _,_) ->
+ | Read_mem0(_,location, length, _,_) ->
    let rec reading location length = 
-     if eq_big_int length zero_big_int 
+     if length = 0 
      then []
-     else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in
-   (Some (Bytevector(reading location length)), env)
- | Write_mem0(_,(Bytevector location), length, _, (Bytevector bytes),_,_) ->
+     else (Mem.find location mem)::(reading (increment location) (length - 1)) in
+   (Some (reading location length), env)
+ | Write_mem0(_,location, length, _, bytes,_,_) ->
    let rec writing location length bytes mem = 
-     if eq_big_int length zero_big_int
+     if length = 0
      then mem
      else match bytes with
        | [] -> mem
        | b::bytes -> 
-	 writing (increment location) (sub_big_int length unit_big_int) bytes (Mem.add location b mem) in
+	 writing (increment location) (length - 1) bytes (Mem.add location b mem) in
    (None,(reg,writing location length bytes mem))
  | _ -> (None, env)
 ;;