C++: move sign analysis to new Operand type

This commit is contained in:
Robert Marsh
2018-11-07 16:07:37 -08:00
parent 9d2d381e68
commit 1d7e802157
2 changed files with 93 additions and 103 deletions

View File

@@ -207,22 +207,20 @@ private predicate unknownSign(Instruction i) {
}
/**
* Holds if `lowerbound` is a lower bound for `bounded` at `pos`. This is restricted
* Holds if `lowerbound` is a lower bound for `bounded``. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(IRGuardCondition comp, Instruction lowerbound, Instruction bounded, Instruction pos, boolean isStrict) {
private predicate lowerBound(IRGuardCondition comp, Operand lowerbound, Operand bounded, boolean isStrict) {
exists(int adjustment, Instruction compared |
valueNumber(bounded) = valueNumber(compared) and
bounded = pos.getAnOperand() and
not unknownSign(lowerbound) and
(
isStrict = true and
adjustment = 0
or
isStrict = false and
adjustment = 1
) and
comp.ensuresLt(lowerbound, compared, adjustment, pos.getBlock(), true)
valueNumber(bounded.getDefinitionInstruction()) = valueNumber(compared) and
(
isStrict = true and
adjustment = 0
or
isStrict = false and
adjustment = 1
) and
comp.ensuresLt(lowerbound.getDefinitionInstruction(), compared, adjustment, bounded.getInstruction().getBlock(), true)
)
}
@@ -231,19 +229,17 @@ private predicate lowerBound(IRGuardCondition comp, Instruction lowerbound, Inst
* Holds if `upperbound` is an upper bound for `bounded` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(IRGuardCondition comp, Instruction upperbound, Instruction bounded, Instruction pos, boolean isStrict) {
private predicate upperBound(IRGuardCondition comp, Operand upperbound, Operand bounded, boolean isStrict) {
exists(int adjustment, Instruction compared |
valueNumber(bounded) = valueNumber(compared) and
bounded = pos.getAnOperand() and
not unknownSign(upperbound) and
(
isStrict = true and
adjustment = 0
or
isStrict = false and
adjustment = 1
) and
comp.ensuresLt(compared, upperbound, adjustment, pos.getBlock(), true)
valueNumber(bounded.getDefinitionInstruction()) = valueNumber(compared) and
(
isStrict = true and
adjustment = 0
or
isStrict = false and
adjustment = 1
) and
comp.ensuresLt(compared, upperbound.getDefinitionInstruction(), adjustment, bounded.getInstruction().getBlock(), true)
)
}
@@ -254,12 +250,10 @@ private predicate upperBound(IRGuardCondition comp, Instruction upperbound, Inst
* - `isEq = true` : `bounded = eqbound`
* - `isEq = false` : `bounded != eqbound`
*/
private predicate eqBound(IRGuardCondition guard, Instruction eqbound, Instruction bounded, Instruction pos, boolean isEq) {
private predicate eqBound(IRGuardCondition guard, Operand eqbound, Operand bounded, boolean isEq) {
exists(Instruction compared |
not unknownSign(eqbound) and
valueNumber(bounded) = valueNumber(compared) and
bounded = pos.getAnOperand() and
guard.ensuresEq(compared, eqbound, 0, pos.getBlock(), isEq)
valueNumber(bounded.getDefinitionInstruction()) = valueNumber(compared) and
guard.ensuresEq(compared, eqbound.getDefinitionInstruction(), 0, bounded.getInstruction().getBlock(), isEq)
)
}
@@ -269,56 +263,56 @@ private predicate eqBound(IRGuardCondition guard, Instruction eqbound, Instructi
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
* order for `v` to be positive.
*/
private predicate posBound(IRGuardCondition comp, Instruction bound, Instruction v, Instruction pos) {
upperBound(comp, bound, v, pos, _) or
eqBound(comp, bound, v, pos, true)
private predicate posBound(IRGuardCondition comp, Operand bound, Operand op) {
upperBound(comp, bound, op, _) or
eqBound(comp, bound, op, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
* order for `v` to be negative.
*/
private predicate negBound(IRGuardCondition comp, Instruction bound, Instruction v, Instruction pos) {
lowerBound(comp, bound, v, pos, _) or
eqBound(comp, bound, v, pos, true)
private predicate negBound(IRGuardCondition comp, Operand bound, Operand op) {
lowerBound(comp, bound, op, _) or
eqBound(comp, bound, op, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(IRGuardCondition comp, Instruction bound, Instruction v, Instruction pos) {
lowerBound(comp, bound, v, pos, _) or
upperBound(comp, bound, v, pos, _) or
eqBound(comp, bound, v, pos, _)
private predicate zeroBound(IRGuardCondition comp, Operand bound, Operand op) {
lowerBound(comp, bound, op, _) or
upperBound(comp, bound, op, _) or
eqBound(comp, bound, op, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(IRGuardCondition comp, Instruction bound, Instruction v, Instruction pos) {
posBound(comp, bound, v, pos) and TPos() = operandSign(comp, bound)
private predicate posBoundOk(IRGuardCondition comp, Operand bound, Operand op) {
posBound(comp, bound, op) and TPos() = operandSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(IRGuardCondition comp, Instruction bound, Instruction v, Instruction pos) {
negBound(comp, bound, v, pos) and TNeg() = operandSign(comp, bound)
private predicate negBoundOk(IRGuardCondition comp, Operand bound, Operand op) {
negBound(comp, bound, op) and TNeg() = operandSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(IRGuardCondition comp, Instruction bound, Instruction v, Instruction pos) {
lowerBound(comp, bound, v, pos, _) and TNeg() = operandSign(comp, bound) or
lowerBound(comp, bound, v, pos, false) and TZero() = operandSign(comp, bound) or
upperBound(comp, bound, v, pos, _) and TPos() = operandSign(comp, bound) or
upperBound(comp, bound, v, pos, false) and TZero() = operandSign(comp, bound) or
eqBound(comp, bound, v, pos, true) and TZero() = operandSign(comp, bound) or
eqBound(comp, bound, v, pos, false) and TZero() != operandSign(comp, bound)
private predicate zeroBoundOk(IRGuardCondition comp, Operand bound, Operand op) {
lowerBound(comp, bound, op, _) and TNeg() = operandSign(bound) or
lowerBound(comp, bound, op, false) and TZero() = operandSign(bound) or
upperBound(comp, bound, op, _) and TPos() = operandSign(bound) or
upperBound(comp, bound, op, false) and TZero() = operandSign(bound) or
eqBound(comp, bound, op, true) and TZero() = operandSign(bound) or
eqBound(comp, bound, op, false) and TZero() != operandSign(bound)
}
private Sign binaryOpLhsSign(Instruction i) {
result = operandSign(i, i.(BinaryInstruction).getLeftOperand())
result = operandSign(i.getAnOperand().(LeftOperand))
}
private Sign binaryOpRhsSign(Instruction i) {
result = operandSign(i, i.(BinaryInstruction).getRightOperand())
result = operandSign(i.getAnOperand().(RightOperand))
}
pragma[noinline]
@@ -327,44 +321,44 @@ private predicate binaryOpSigns(Instruction i, Sign lhs, Sign rhs) {
rhs = binaryOpRhsSign(i)
}
private Sign unguardedOperandSign(Instruction pos, Instruction operand) {
result = instructionSign(operand) and
not hasGuard(operand, pos, result)
private Sign unguardedOperandSign(Operand operand) {
result = instructionSign(operand.getDefinitionInstruction()) and
not hasGuard(operand, result)
}
private Sign guardedOperandSign(Instruction pos, Instruction operand) {
result = instructionSign(operand) and
hasGuard(operand, pos, result)
private Sign guardedOperandSign(Operand operand) {
result = instructionSign(operand.getDefinitionInstruction()) and
hasGuard(operand, result)
}
private Sign guardedOperandSignOk(Instruction pos, Instruction operand) {
result = TPos() and forex(IRGuardCondition guard, Instruction bound | posBound(guard, bound, operand, pos) | posBoundOk(guard, bound, operand, pos)) or
result = TNeg() and forex(IRGuardCondition guard, Instruction bound | negBound(guard, bound, operand, pos) | negBoundOk(guard, bound, operand, pos)) or
result = TZero() and forex(IRGuardCondition guard, Instruction bound | zeroBound(guard, bound, operand, pos) | zeroBoundOk(guard, bound, operand, pos))
private Sign guardedOperandSignOk(Operand operand) {
result = TPos() and forex(IRGuardCondition guard, Operand bound | posBound(guard, bound, operand) | posBoundOk(guard, bound, operand)) or
result = TNeg() and forex(IRGuardCondition guard, Operand bound | negBound(guard, bound, operand) | negBoundOk(guard, bound, operand)) or
result = TZero() and forex(IRGuardCondition guard, Operand bound | zeroBound(guard, bound, operand) | zeroBoundOk(guard, bound, operand))
}
/**
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(Instruction v, Instruction pos, Sign s) {
s = TPos() and posBound(_, _, v, pos)
private predicate hasGuard(Operand op, Sign s) {
s = TPos() and posBound(_, _, op)
or
s = TNeg() and negBound(_, _, v, pos)
s = TNeg() and negBound(_, _, op)
or
s = TZero() and zeroBound(_, _, v, pos)
s = TZero() and zeroBound(_, _, op)
}
cached private module SignAnalysisCached {
cached module SignAnalysisCached {
/**
* Gets a sign that `operand` may have at `pos`, taking guards into account.
*/
cached
Sign operandSign(Instruction pos, Instruction operand) {
result = unguardedOperandSign(pos, operand)
Sign operandSign(Operand operand) {
result = unguardedOperandSign(operand)
or
result = guardedOperandSign(pos, operand) and
result = guardedOperandSignOk(pos, operand)
result = guardedOperandSign(operand) and
result = guardedOperandSignOk(operand)
}
cached
@@ -392,18 +386,14 @@ cached private module SignAnalysisCached {
then fromSigned = true
else fromSigned = false
) and
result = castSign(operandSign(ci, prior), fromSigned, toSigned, getCastKind(ci))
result = castSign(operandSign(ci.getAnOperand()), fromSigned, toSigned, getCastKind(ci))
)
or
exists(Instruction prior |
prior = i.(CopyInstruction).getSourceValue()
|
result = operandSign(i, prior)
)
result = operandSign(i.getAnOperand().(CopySourceOperand))
or
result = operandSign(i, i.(BitComplementInstruction).getOperand()).bitnot()
result = operandSign(i.(BitComplementInstruction).getAnOperand()).bitnot()
or
result = operandSign(i, i.(NegateInstruction).getOperand()).neg()
result = operandSign(i.(NegateInstruction).getAnOperand()).neg()
or
exists(Sign s1, Sign s2 |
binaryOpSigns(i, s1, s2)
@@ -436,58 +426,58 @@ cached private module SignAnalysisCached {
)
or
// use hasGuard here?
result = operandSign(i, i.(PhiInstruction).getAnOperand())
result = operandSign(i.(PhiInstruction).getAnOperand())
)
}
}
/** Holds if `i` can be positive and cannot be negative. */
predicate positive(Instruction i) {
predicate positiveInstruction(Instruction i) {
instructionSign(i) = TPos() and
not instructionSign(i) = TNeg()
}
/** Holds if `i` at `pos` can be positive at and cannot be negative. */
predicate positive(Instruction i, Instruction pos) {
operandSign(pos, i) = TPos() and
not operandSign(pos, i) = TNeg()
predicate positive(Operand op) {
operandSign(op) = TPos() and
not operandSign(op) = TNeg()
}
/** Holds if `i` can be negative and cannot be positive. */
predicate negative(Instruction i) {
predicate negativeInstruction(Instruction i) {
instructionSign(i) = TNeg() and
not instructionSign(i) = TPos()
}
/** Holds if `i` at `pos` can be negative and cannot be positive. */
predicate negative(Instruction i, Instruction pos) {
operandSign(pos, i) = TNeg() and
not operandSign(pos, i) = TPos()
predicate negative(Operand op) {
operandSign(op) = TNeg() and
not operandSign(op) = TPos()
}
/** Holds if `i` is strictly positive. */
predicate strictlyPositive(Instruction i) {
predicate strictlyPositiveInstruction(Instruction i) {
instructionSign(i) = TPos() and
not instructionSign(i) = TNeg() and
not instructionSign(i) = TZero()
}
/** Holds if `i` is strictly positive at `pos`. */
predicate strictlyPositive(Instruction i, Instruction pos) {
operandSign(pos, i) = TPos() and
not operandSign(pos, i) = TNeg() and
not operandSign(pos, i) = TZero()
predicate strictlyPositive(Operand op) {
operandSign(op) = TPos() and
not operandSign(op) = TNeg() and
not operandSign(op) = TZero()
}
/** Holds if `i` is strictly negative. */
predicate strictlyNegative(Instruction i) {
predicate strictlyNegativeInstruction(Instruction i) {
instructionSign(i) = TNeg() and
not instructionSign(i) = TPos() and
not instructionSign(i) = TZero()
}
/** Holds if `i` is strictly negative at `pos`. */
predicate strictlyNegative(Instruction i, Instruction pos) {
operandSign(pos, i) = TNeg() and
not operandSign(pos, i) = TPos() and
not operandSign(pos, i) = TZero()
predicate strictlyNegative(Operand op) {
operandSign(op) = TNeg() and
not operandSign(op) = TPos() and
not operandSign(op) = TZero()
}

View File

@@ -2,16 +2,16 @@ import semmle.code.cpp.rangeanalysis.SignAnalysis
import semmle.code.cpp.ir.IR
string getASignString(Instruction i) {
positive(i) and
positiveInstruction(i) and
result = "positive"
or
negative(i) and
negativeInstruction(i) and
result = "negative"
or
strictlyPositive(i) and
strictlyPositiveInstruction(i) and
result = "strictlyPositive"
or
strictlyNegative(i) and
strictlyNegativeInstruction(i) and
result = "strictlyNegative"
}