From 4f4b930df0306fb57eecd06eea182115f01b94e5 Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Mon, 27 Jun 2016 14:12:21 +0200 Subject: change bitwidth of expr_shpost in MetaSMTBuilder::constructSDivByConstant to 64, so that the first two arguments of the call bvVarRightShift(extend_npm, expr_shpost, 64) have the same bitwidth of 64. --- lib/Solver/MetaSMTBuilder.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/Solver/MetaSMTBuilder.h') diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index ba7ea03b..a166db5a 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -450,7 +450,7 @@ MetaSMTBuilder::constructSDivByConstant( int32_t mprime, dsign, shpost; ComputeSDivConstants32(d, mprime, dsign, shpost); typename SolverContext::result_type expr_dsign = bvConst32(32, dsign); - typename SolverContext::result_type expr_shpost = bvConst32(32, shpost); + typename SolverContext::result_type expr_shpost = bvConst32(64, shpost); // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32) int64_t mprime_64 = (int64_t)mprime; -- cgit 1.4.1 From 5b893715d020165f69062273741b7db99eb47624 Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Tue, 28 Jun 2016 13:18:52 +0200 Subject: add assertions to check the pre-condition of bvVar*Shift that both operands have the same bv width --- lib/Solver/MetaSMTBuilder.h | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'lib/Solver/MetaSMTBuilder.h') diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index a166db5a..ad26f2ed 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -540,6 +540,9 @@ MetaSMTBuilder::bvVarLeftShift( typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + typename SolverContext::result_type res = bvZero(width); // construct a big if-then-elif-elif-... with one case per possible shift @@ -566,6 +569,9 @@ MetaSMTBuilder::bvVarRightShift( typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + typename SolverContext::result_type res = bvZero(width); // construct a big if-then-elif-elif-... with one case per possible shift @@ -593,6 +599,9 @@ MetaSMTBuilder::bvVarArithRightShift( typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + // get the sign bit to fill with typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1); -- cgit 1.4.1