From 8f2af62480293b4977ac75c5d9df7f66451cb151 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 26 Apr 2019 12:03:26 -0700 Subject: [PATCH] [sledge] Clamp rational numerator and denominator to bitwidth Summary: When constructing division expressions from rational coefficients of polynomials, the constant numerator and denominator should be clamped to the number of bits in the result type. Reviewed By: mbouaziz Differential Revision: D15098825 fbshipit-source-id: fa448c39a --- sledge/src/llair/exp.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 69b961513..cb8b40a64 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -737,7 +737,11 @@ let rec sum_to_exp typ sum = | _ -> Add {typ; args= sum} ) | _ -> Add {typ; args= sum} -and rational Q.{num; den} typ = simp_div (integer num typ) (integer den typ) +and rational Q.{num; den} typ = + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + simp_div + (integer (Z.clamp ~signed:true bits num) typ) + (integer (Z.clamp ~signed:true bits den) typ) and simp_div x y = match (x, y) with