Make some potentially non-terminating library functions terminate

4 files changed, 19 insertions, 17 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index f5ac8fc5..23f81f0e 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -158,7 +158,7 @@ let footprint = Footprint (Done (),Nothing)
 val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_inc (i,stop,by) vars body =
-  if i <= stop
+  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then
     body i vars >>= fun vars ->
     foreachM_inc (i + by,stop,by) vars body
@@ -167,11 +167,11 @@ let rec foreachM_inc (i,stop,by) vars body =
 
 val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
-let rec foreachM_dec (i,stop,by) vars body =
-  if i >= stop
+let rec foreachM_dec (stop,i,by) vars body =
+  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then
     body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
+    foreachM_dec (stop,i - by,by) vars body
   else return vars
 
 val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index b94257f0..cbc55367 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -144,7 +144,7 @@ let to_bin n = List.reverse (to_bin_aux n)
 
 val pad_zero : list bitU -> integer -> list bitU
 let rec pad_zero bits n =
-  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+  if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
 
 
 let rec add_one_bit_ignore_overflow_aux bits = match bits with
@@ -439,7 +439,7 @@ let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
-  if n = 0 then []
+  if n <= 0 then []
   else xs ++ repeat xs (n-1)
 
 (* Assumes decreasing bit vectors *)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 48d728bf..97f13c33 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -41,7 +41,7 @@ let list_append (l, r) = l ++ r
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
-  if n = 0 then []
+  if n <= 0 then []
   else xs ++ repeat xs (n-1)
 
 let duplicate_to_list (bit, length) = repeat [bit] length
@@ -167,6 +167,7 @@ let get_dir (Vector _ _ ord) = ord
 let get_start (Vector _ s _) = s
 let get_elems (Vector elems _ _) = elems
 let length (Vector bs _ _) = integerFromNat (length bs)
+let vector_length = length
 
 instance forall 'a. Show 'a => (Show (vector 'a))
   let show = showVector
@@ -566,17 +567,17 @@ let internal_mem_value direction bytes =
 val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
                    (integer -> 'vars -> 'vars) -> 'vars
 let rec foreach_inc (i,stop,by) vars body =
-  if i <= stop
+  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then let vars = body i vars in
        foreach_inc (i + by,stop,by) vars body
   else vars
 
 val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
-  if i >= stop
+let rec foreach_dec (stop,i,by) vars body =
+  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then let vars = body i vars in
-       foreach_dec (i - by,stop,by) vars body
+       foreach_dec (stop,i - by,by) vars body
   else vars
 
 let assert' b msg_opt =
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index dc30a17f..4bbb3647 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -63,8 +63,9 @@ let catch_early_return m s =
     end) (m s)
 
 val range : integer -> integer -> list integer
-let rec range i j = 
-  if i = j then [i]
+let rec range i j =
+  if j < i then []
+  else if i = j then [i]
   else i :: range (i+1) j
 
 val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a
@@ -218,7 +219,7 @@ let footprint = return ()
 val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
 let rec foreachM_inc (i,stop,by) vars body =
-  if i <= stop
+  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then
     body i vars >>= fun vars ->
     foreachM_inc (i + by,stop,by) vars body
@@ -227,11 +228,11 @@ let rec foreachM_inc (i,stop,by) vars body =
 
 val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
-  if i >= stop
+let rec foreachM_dec (stop,i,by) vars body =
+  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then
     body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
+    foreachM_dec (stop,i - by,by) vars body
   else return vars
 
 val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars