look for sub matches of registers on exhaustive mode

2 files changed, 21 insertions, 4 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 67bf42c7..405c5d2a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -430,14 +430,20 @@ let rec interp_to_outcome mode thunk =
 
 let interp mode i_state = interp_to_outcome mode (fun _ -> Interp.resume mode i_state Nothing)
 
-(*TODO: Only find exact matches, need to look for field/slice sub pieces*)
+(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
 let rec find_reg_name reg = function
   | [] -> Nothing
   | (reg_name,v)::registers ->
     match (reg,reg_name) with
       | (Reg i, Reg n) -> if i = n then (Just v) else find_reg_name reg registers
+      | (Reg_slice i (p1,p2), Reg n) -> if i = n then (Just (slice_value v p1 p2)) else find_reg_name reg registers
+      | (Reg_field i f (p1,p2), Reg n) -> if i = n then (Just (slice_value v p1 p2)) else find_reg_name reg registers
       | (Reg_slice  i (p1,p2), Reg_slice n (p3,p4)) ->
-	if i=n && p1=p3 && p2 = p4 then (Just v) else find_reg_name reg registers
+	if i=n 
+	then if p1=p3 && p2 = p4 then (Just v)
+	     else if p1>=p3 && p2<= p4 then (Just (slice_value v p1 p2))
+	     else find_reg_name reg registers
+	  else find_reg_name reg registers
       | (Reg_field i f _,Reg_field n fn _) ->
 	if i=n && f = fn then (Just v) else find_reg_name reg registers
       | (Reg_f_slice i f _ (p1,p2), Reg_f_slice n fn _ (p3,p4)) ->
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index cd656f1e..483253b6 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -333,7 +333,18 @@ let rec arith_op_vec_no0 op size (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
 end ;;
-
+let rec arith_op_vec_range_no0 op size (V_tuple args) = match args with
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1; v2] ->
+    taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> 
+    taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
+  | [(V_vector _ ord cs as l1);n] ->
+    arith_op_vec_no0 op size (V_tuple [l1;(to_vec ord (List.length cs) n)])
+end ;;
 
 let rec compare_op op (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
@@ -435,7 +446,7 @@ let function_map = [
   ("mult_overload_vec", arith_op_overflow_vec ( * ) 2);
   ("mod", arith_op_no0 (mod));
   ("mod_vec", arith_op_vec_no0 (mod) 1);
-  ("mod_vec_range", arith_op_vec_range (mod) 1);
+  ("mod_vec_range", arith_op_vec_range_no0 (mod) 1);
   ("quot", arith_op_no0 (/));
   ("quot_vec", arith_op_vec_no0 (/) 1);
   ("eq", eq);