fix three different copies of the hardware_quot function to do proper trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0.

3 files changed, 27 insertions, 16 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4fded5a1..38f7d512 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -257,12 +257,16 @@ let hardware_mod (a: integer) (b:integer) : integer =
  then (a mod b) - b
  else a mod b
 
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
 let hardware_quot (a:integer) (b:integer) : integer = 
-  if a < 0 && b < 0
-  then (abs a) / (abs b)
-  else if (a < 0 && b > 0) 
-  then (a/b) + 1
-  else a/b
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
 
 let quot_signed = hardware_quot
 
diff --git a/src/gen_lib/sail_values_word.lem b/src/gen_lib/sail_values_word.lem
index ef7b03b9..048bf30a 100644
--- a/src/gen_lib/sail_values_word.lem
+++ b/src/gen_lib/sail_values_word.lem
@@ -327,12 +327,16 @@ let hardware_mod (a: integer) (b:integer) : integer =
  then (a mod b) - b
  else a mod b
 
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
 let hardware_quot (a:integer) (b:integer) : integer = 
-  if a < 0 && b < 0
-  then (abs a) / (abs b)
-  else if (a < 0 && b > 0) 
-  then (a/b) + 1
-  else a/b
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
 
 let quot_signed = hardware_quot
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index fe87c9e1..dd39373d 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -66,13 +66,16 @@ let hardware_mod (a: integer) (b:integer) : integer =
  then (a mod b) - b
  else a mod b
 
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
 let hardware_quot (a:integer) (b:integer) : integer = 
-  if a < 0 && b < 0
-  then (abs a) / (abs b)
-  else if (a < 0 && b > 0) 
-  then (a/b) + 1
-  else a/b
-
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
 
 let (max_64u : integer) = integerFromNat ((natPow 2 64) - 1)
 let (max_64  : integer) = integerFromNat ((natPow 2 63) - 1)