Python points-to. Track bitwise or-ing of small integer flags.

This commit is contained in:
Mark Shannon
2019-04-17 15:26:52 +01:00
parent 96eaf815da
commit 8a2fb54c49
2 changed files with 30 additions and 5 deletions

View File

@@ -658,6 +658,16 @@ class BinaryExprNode extends ControlFlowNode {
result = this.getNode().getOp()
}
/** Whether left and right are a pair of operands for this binary expression */
predicate operands(ControlFlowNode left, Operator op, ControlFlowNode right) {
exists(BinaryExpr b, Expr eleft, Expr eright |
this.getNode() = b and left.getNode() = eleft and right.getNode() = eright |
eleft = b.getLeft() and eright = b.getRight() and op = b.getOp()
) and
left.getBasicBlock().dominates(this.getBasicBlock()) and
right.getBasicBlock().dominates(this.getBasicBlock())
}
}
/** A control flow node corresponding to a boolean shortcut (and/or) operation */

View File

@@ -1119,11 +1119,26 @@ module Expressions {
*/
pragma [noinline]
predicate binaryPointsTo(BinaryExprNode b, PointsToContext context, ObjectInternal value, ControlFlowNode origin, ControlFlowNode operand, ObjectInternal opvalue) {
// TO DO...
// Track some integer values through `|` and the types of some objects
operand = b.getAnOperand() and
PointsToInternal::pointsTo(operand, context, opvalue, _) and
value = ObjectInternal::unknown() and origin = b
origin = b and
exists(ControlFlowNode left, Operator op, ControlFlowNode right |
b.operands(left, op, right)
|
not op instanceof BitOr and
(operand = left or operand = right) and
PointsToInternal::pointsTo(operand, context, opvalue, _) and
value = ObjectInternal::unknown()
or
op instanceof BitOr and
exists(ObjectInternal lobj, ObjectInternal robj |
PointsToInternal::pointsTo(left, context, lobj, _) and
PointsToInternal::pointsTo(right, context, robj, _) and
value = TInt(lobj.intValue().bitOr(robj.intValue()))
|
left = operand and opvalue = lobj
or
right = operand and opvalue = robj
)
)
}
pragma [noinline]