about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-11-29 10:53:17 +0000
committerDan Liew <delcypher@gmail.com>2017-06-01 11:36:09 +0100
commit11fd589bb7c0c075dc9c5cb1e7a0eecd9eb94ef1 (patch)
tree86c85d82d3345ebf939d197b32e4eb8861dfbaea /lib/Solver
parent4498d8c08511afa201cdedc9bb9b2fdfadab8384 (diff)
downloadklee-11fd589bb7c0c075dc9c5cb1e7a0eecd9eb94ef1.tar.gz
[Z3] Add assertions in Z3 builder to catch underflow with bad widths.
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/Z3Builder.cpp6
1 files changed, 5 insertions, 1 deletions
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<Expr> 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<Expr> 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);