[llvm-bugs] [Bug 37855] New: [Analyzer][Z3] Wrong comparison operation being generated from ranged constraint

[via llvm-bugs]

https://bugs.llvm.org/show_bug.cgi?id=37855

            Bug ID: 37855
           Summary: [Analyzer][Z3] Wrong comparison operation being
                    generated from ranged constraint
           Product: clang
           Version: trunk
          Hardware: PC
                OS: Linux
            Status: NEW
          Severity: normal
          Priority: P
         Component: Static Analyzer
          Assignee: dcoughlin at apple.com
          Reporter: mikhail.ramalho at gmail.com
                CC: llvm-bugs at lists.llvm.org

The following program:

typedef struct o p;
struct o {
  struct {
  } s;
};

void q(*r, p2) {
  r < p2;
}

void k(l, node) {
  struct {
    p *node;
  } * n, *nodep, path[sizeof(void)];
  path->node = l;
  for (n = path; node != l;) {
    q(node, n->node);
    nodep = n;
  }
  if (nodep)
    n[1].node->s;
}

generates the following constraint:

(conj_$1{struct o *}) - (reg_$3<int * r>): [-9223372036854775808, 0]

but the SMT generated is:

(and (bvuge (bvsub $1 $3) #x8000000000000000)
     (bvule (bvsub $1 $3) #x0000000000000000))

The issue is that unsigned comparisons (bvuge and bvule) are being generated
instead of signed comparisons (bvsge and bvsle).

When generating the expressions: 

(conj_$1{p *}) - (reg_$3<int * r>) >= -9223372036854775808

and

(conj_$1{p *}) - (reg_$3<int * r>) <= 0

both -9223372036854775808 and 0 are casted to pointer type and
LTy->isSignedIntegerOrEnumerationType() in Z3ConstraintManager::getZ3BinExpr
only checks if the type is signed, not if it's a pointer.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20180619/4ffced98/attachment.html>