From 11fd589bb7c0c075dc9c5cb1e7a0eecd9eb94ef1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 29 Nov 2016 10:53:17 +0000 Subject: [Z3] Add assertions in Z3 builder to catch underflow with bad widths. --- lib/Solver/Z3Builder.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'lib/Solver') diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index fc826c07..d111c3a0 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -529,6 +529,7 @@ Z3ASTHandle Z3Builder::constructActual(ref e, int *width_out) { if (srcWidth == 1) { return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); } else { + assert(*width_out > srcWidth && "Invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - srcWidth), src), ctx); } @@ -621,12 +622,15 @@ Z3ASTHandle Z3Builder::constructActual(ref e, int *width_out) { uint64_t divisor = CE->getZExtValue(); if (bits64::isPowerOfTwo(divisor)) { - unsigned bits = bits64::indexOfSingleBit(divisor); + // FIXME: This should be unsigned but currently needs to be signed to + // avoid signed-unsigned comparison in assert. + int bits = bits64::indexOfSingleBit(divisor); // special case for modding by 1 or else we bvExtract -1:0 if (bits == 0) { return bvZero(*width_out); } else { + assert(*width_out > bits && "invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - bits), bvExtract(left, bits - 1, 0)), ctx); -- cgit 1.4.1