[cfe-dev] evaluating a LAnd expr in the static checker

[Devin Coughlin via cfe-dev]

> On Jun 3, 2016, at 2:54 PM, McDowell, Raymond C. via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> I am trying to construct a constraint that says 0 <= Offset <= Size, for two SVals Offset and Size.  Here’s what I did:
>  
>   ASTContext &ACtx = ChCtx.getASTContext();
>   SValBuilder &SVBldr = St->getStateManager().getSValBuilder();
>   SVal Zero = SVBldr.makeZeroVal(ACtx.getSizeType());
>   SVal OffsetIsNonNeg = SVBldr.evalBinOpNN(St, BO_LE, Zero.castAs<NonLoc>(), Offset.castAs<NonLoc>(), ACtx.BoolTy);
>   SVal OffsetIsWithinSize = SVBldr.evalBinOpNN(St, BO_LE, Offset.castAs<NonLoc>(), BuffSize.castAs<NonLoc>(), ACtx.BoolTy);
>   SVal OffsetIsWithinBounds = SVBldr.evalBinOpNN(St, BO_LAnd, OffsetIsNonNeg.castAs<NonLoc>(), OffsetIsWithinSize.castAs<NonLoc>(), ACtx.BoolTy);
>  
>  
> When I run this code, it fails with an error: Assertion `false && “Invalid Opcode.”’ failed.  This is coming from evalAPSInt in BasicValueFactory.cpp.  This function contains a comment that says “Land, LOr, Comma are handled specially by higher-level logic.”  Land does not seem to be handled by higher-level logic in this case.  I intend to work around this by asserting these as two separate constraints instead of combining them into one.  But this looks like a bug to me, so thought I should raise the issue here.

Logical And and Logical Or have consequences for control flow (they are short-circuiting) and so are represented in the control flow graph. You can see how they are evaluated in ExprEngine::VisitLogicalExpr(). This is the “higher-level logic” referred to in the comment.

As you noted, you can apply a constraint that is a logical conjunction of OffsetIsNonNeg and OffsetIsWithinSize by using ConstraintManager::assume() to first apply the assumption that OffsetIsNonNeg is true to the current state. Then you can call assume() again on the resultant state to add the second assumption that OffsetIsWithinSize is true.

This also reflects an overall design decision in the analyzer to keep constraints relatively simple so they can be reasoned about very quickly. Rather than track complex, logical symbolic constraints within a single state, the analyzer will eagerly split into multiple states — each of which has simpler, range-based constraints.

For example, if you have:

void foo(int a, int b, int c) {
  assert((a == 1 || b == 2) || c == 3);
  // (*)
}

Rather than produce a single state at (*) with the complex constraint “ ((‘$a’ equals 1 OR ‘$b’ equals ‘2’) OR ‘$c’ equals ‘3’)“ it will produce three separate states: 

1) 
$a: [1,1]

2)
$a: [INT_MIN, 0], [2,INT_MAX]
$b: [2,2]

3)
$a: [INT_MIN, 0], [2,INT_MAX]
$b: [INT_MIN, 1], [3,INT_MAX]
$c: [3,3]

The analyzer will then explore the path from these three states separately. In effect the analyzer has moved the disjunction for the complex constraint out to the state level.

This approach keeps the constraint manager simple and *very* fast, at the cost of eager state splits and imprecision when reasoning about relationships. In particular, the analyzer currently has no way to reason about symbolic constraints involving relationships between unknowns like "a <= b < c” — which would very useful for things like array-bounds checking!

Ryan Govostes and Bhargava Shastry have been working on improving the analyzer’s reasoning about symbolic relational constraints with an SMT solver (STP, in this case). You can see their work at <http://reviews.llvm.org/D15609 <http://reviews.llvm.org/D15609>>.

Devin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20160604/13c7670b/attachment.html>