Merge pull request #12622 from MathiasVP/skip-safe-conversions-in-range-analysis

C++: Range analysis on `EquivalenceClass`es
This commit is contained in:
Robert Marsh
2023-03-30 10:08:59 -04:00
committed by GitHub
10 changed files with 183 additions and 72 deletions

View File

@@ -12,12 +12,92 @@ private import semmle.code.cpp.ir.ValueNumbering
module SemanticExprConfig {
class Location = Cpp::Location;
class Expr = IR::Instruction;
/** A `ConvertInstruction` or a `CopyValueInstruction`. */
private class Conversion extends IR::UnaryInstruction {
Conversion() {
this instanceof IR::CopyValueInstruction
or
this instanceof IR::ConvertInstruction
}
/** Holds if this instruction converts a value of type `tFrom` to a value of type `tTo`. */
predicate converts(SemType tFrom, SemType tTo) {
tFrom = getSemanticType(this.getUnary().getResultIRType()) and
tTo = getSemanticType(this.getResultIRType())
}
}
/**
* Gets a conversion-like instruction that consumes `op`, and
* which is guaranteed to not overflow.
*/
private IR::Instruction safeConversion(IR::Operand op) {
exists(Conversion conv, SemType tFrom, SemType tTo |
conv.converts(tFrom, tTo) and
conversionCannotOverflow(tFrom, tTo) and
conv.getUnaryOperand() = op and
result = conv
)
}
/** Holds if `i1 = i2` or if `i2` is a safe conversion that consumes `i1`. */
private predicate idOrSafeConversion(IR::Instruction i1, IR::Instruction i2) {
not i1.getResultIRType() instanceof IR::IRVoidType and
(
i1 = i2
or
i2 = safeConversion(i1.getAUse()) and
i1.getBlock() = i2.getBlock()
)
}
module Equiv = QlBuiltins::EquivalenceRelation<IR::Instruction, idOrSafeConversion/2>;
/**
* The expressions on which we perform range analysis.
*/
class Expr extends Equiv::EquivalenceClass {
/** Gets the n'th instruction in this equivalence class. */
private IR::Instruction getInstruction(int n) {
result =
rank[n + 1](IR::Instruction instr, int i, IR::IRBlock block |
this = Equiv::getEquivalenceClass(instr) and block.getInstruction(i) = instr
|
instr order by i
)
}
/** Gets a textual representation of this element. */
string toString() { result = this.getUnconverted().toString() }
/** Gets the basic block of this expression. */
IR::IRBlock getBlock() { result = this.getUnconverted().getBlock() }
/** Gets the unconverted instruction associated with this expression. */
IR::Instruction getUnconverted() { result = this.getInstruction(0) }
/**
* Gets the final instruction associated with this expression. This
* represents the result after applying all the safe conversions.
*/
IR::Instruction getConverted() {
exists(int n |
result = this.getInstruction(n) and
not exists(this.getInstruction(n + 1))
)
}
/** Gets the type of the result produced by this instruction. */
IR::IRType getResultIRType() { result = this.getConverted().getResultIRType() }
/** Gets the location of the source code for this expression. */
Location getLocation() { result = this.getUnconverted().getLocation() }
}
SemBasicBlock getExprBasicBlock(Expr e) { result = getSemanticBasicBlock(e.getBlock()) }
private predicate anyConstantExpr(Expr expr, SemType type, string value) {
exists(IR::ConstantInstruction instr | instr = expr |
exists(IR::ConstantInstruction instr | getSemanticExpr(instr) = expr |
type = getSemanticType(instr.getResultIRType()) and
value = instr.getValue()
)
@@ -58,41 +138,46 @@ module SemanticExprConfig {
predicate nullLiteral(Expr expr, SemAddressType type) { anyConstantExpr(expr, type, _) }
predicate stringLiteral(Expr expr, SemType type, string value) {
anyConstantExpr(expr, type, value) and expr instanceof IR::StringConstantInstruction
anyConstantExpr(expr, type, value) and
expr.getUnconverted() instanceof IR::StringConstantInstruction
}
predicate binaryExpr(Expr expr, Opcode opcode, SemType type, Expr leftOperand, Expr rightOperand) {
exists(IR::BinaryInstruction instr | instr = expr |
exists(IR::BinaryInstruction instr |
instr = expr.getUnconverted() and
type = getSemanticType(instr.getResultIRType()) and
leftOperand = instr.getLeft() and
rightOperand = instr.getRight() and
leftOperand = getSemanticExpr(instr.getLeft()) and
rightOperand = getSemanticExpr(instr.getRight()) and
// REVIEW: Merge the two `Opcode` types.
opcode.toString() = instr.getOpcode().toString()
)
}
predicate unaryExpr(Expr expr, Opcode opcode, SemType type, Expr operand) {
type = getSemanticType(expr.getResultIRType()) and
(
exists(IR::UnaryInstruction instr | instr = expr |
operand = instr.getUnary() and
// REVIEW: Merge the two operand types.
opcode.toString() = instr.getOpcode().toString()
)
or
exists(IR::StoreInstruction instr | instr = expr |
operand = instr.getSourceValue() and
opcode instanceof Opcode::Store
)
exists(IR::UnaryInstruction instr | instr = expr.getUnconverted() |
type = getSemanticType(instr.getResultIRType()) and
operand = getSemanticExpr(instr.getUnary()) and
// REVIEW: Merge the two operand types.
opcode.toString() = instr.getOpcode().toString()
)
or
exists(IR::StoreInstruction instr | instr = expr.getUnconverted() |
type = getSemanticType(instr.getResultIRType()) and
operand = getSemanticExpr(instr.getSourceValue()) and
opcode instanceof Opcode::Store
)
}
predicate nullaryExpr(Expr expr, Opcode opcode, SemType type) {
type = getSemanticType(expr.getResultIRType()) and
(
expr instanceof IR::LoadInstruction and opcode instanceof Opcode::Load
or
expr instanceof IR::InitializeParameterInstruction and
exists(IR::LoadInstruction load |
load = expr.getUnconverted() and
type = getSemanticType(load.getResultIRType()) and
opcode instanceof Opcode::Load
)
or
exists(IR::InitializeParameterInstruction init |
init = expr.getUnconverted() and
type = getSemanticType(init.getResultIRType()) and
opcode instanceof Opcode::InitializeParameter
)
}
@@ -122,8 +207,10 @@ module SemanticExprConfig {
newtype TSsaVariable =
TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
TSsaOperand(IR::Operand op) { op.isDefinitionInexact() } or
TSsaPointerArithmeticGuard(IR::PointerArithmeticInstruction instr) {
exists(Guard g, IR::Operand use | use = instr.getAUse() |
TSsaPointerArithmeticGuard(ValueNumber instr) {
exists(Guard g, IR::Operand use |
use = instr.getAUse() and use.getIRType() instanceof IR::IRAddressType
|
g.comparesLt(use, _, _, _, _) or
g.comparesLt(_, use, _, _, _) or
g.comparesEq(use, _, _, _, _) or
@@ -138,7 +225,7 @@ module SemanticExprConfig {
IR::Instruction asInstruction() { none() }
IR::PointerArithmeticInstruction asPointerArithGuard() { none() }
ValueNumber asPointerArithGuard() { none() }
IR::Operand asOperand() { none() }
}
@@ -156,15 +243,15 @@ module SemanticExprConfig {
}
class SsaPointerArithmeticGuard extends SsaVariable, TSsaPointerArithmeticGuard {
IR::PointerArithmeticInstruction instr;
ValueNumber vn;
SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(instr) }
SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(vn) }
final override string toString() { result = instr.toString() }
final override string toString() { result = vn.toString() }
final override Location getLocation() { result = instr.getLocation() }
final override Location getLocation() { result = vn.getLocation() }
final override IR::PointerArithmeticInstruction asPointerArithGuard() { result = instr }
final override ValueNumber asPointerArithGuard() { result = vn }
}
class SsaOperand extends SsaVariable, TSsaOperand {
@@ -179,7 +266,9 @@ module SemanticExprConfig {
final override IR::Operand asOperand() { result = op }
}
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v.asInstruction() = sourceExpr }
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) {
getSemanticExpr(v.asInstruction()) = sourceExpr
}
predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }
@@ -192,9 +281,9 @@ module SemanticExprConfig {
}
Expr getAUse(SsaVariable v) {
result.(IR::LoadInstruction).getSourceValue() = v.asInstruction()
result.getUnconverted().(IR::LoadInstruction).getSourceValue() = v.asInstruction()
or
result = valueNumber(v.asPointerArithGuard()).getAnInstruction()
result.getUnconverted() = v.asPointerArithGuard().getAnInstruction()
}
SemType getSsaVariableType(SsaVariable v) {
@@ -236,7 +325,7 @@ module SemanticExprConfig {
final override predicate hasRead(SsaVariable v) {
exists(IR::Operand operand |
operand.getDef() = v.asInstruction() or
operand.getDef() = valueNumber(v.asPointerArithGuard()).getAnInstruction()
operand.getDef() = v.asPointerArithGuard().getAnInstruction()
|
not operand instanceof IR::PhiInputOperand and
operand.getUse().getBlock() = block
@@ -257,7 +346,7 @@ module SemanticExprConfig {
final override predicate hasRead(SsaVariable v) {
exists(IR::PhiInputOperand operand |
operand.getDef() = v.asInstruction() or
operand.getDef() = valueNumber(v.asPointerArithGuard()).getAnInstruction()
operand.getDef() = v.asPointerArithGuard().getAnInstruction()
|
operand.getPredecessorBlock() = pred and
operand.getUse().getBlock() = succ
@@ -303,17 +392,21 @@ module SemanticExprConfig {
}
Expr getBoundExpr(Bound bound, int delta) {
result = bound.(IRBound::Bound).getInstruction(delta)
result = getSemanticExpr(bound.(IRBound::Bound).getInstruction(delta))
}
class Guard = IRGuards::IRGuardCondition;
predicate guard(Guard guard, BasicBlock block) { block = guard.getBlock() }
Expr getGuardAsExpr(Guard guard) { result = guard }
Expr getGuardAsExpr(Guard guard) { result = getSemanticExpr(guard) }
predicate equalityGuard(Guard guard, Expr e1, Expr e2, boolean polarity) {
guard.comparesEq(e1.getAUse(), e2.getAUse(), 0, true, polarity)
exists(IR::Instruction left, IR::Instruction right |
getSemanticExpr(left) = e1 and
getSemanticExpr(right) = e2 and
guard.comparesEq(left.getAUse(), right.getAUse(), 0, true, polarity)
)
}
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock controlled, boolean branch) {
@@ -324,16 +417,17 @@ module SemanticExprConfig {
guard.controlsEdge(bb1, bb2, branch)
}
Guard comparisonGuard(Expr e) { result = e }
Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
none() // TODO
}
/** Gets the expression associated with `instr`. */
SemExpr getSemanticExpr(IR::Instruction instr) { result = Equiv::getEquivalenceClass(instr) }
}
SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
IR::Instruction getCppInstruction(SemExpr e) { e = result }
predicate getSemanticExpr = SemanticExprConfig::getSemanticExpr/1;
SemBasicBlock getSemanticBasicBlock(IR::IRBlock block) { result = block }

View File

@@ -495,7 +495,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
D::Delta oldDelta
|
guardEq = semEqFlowCond(v, semSsaRead(v2, d1), d2, true, eqIsTrue) and
guardEq = semEqFlowCond(v, semSsaRead(pragma[only_bind_into](v2), d1), d2, true, eqIsTrue) and
result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
// guardEq needs to control guard
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue) and

View File

@@ -198,6 +198,16 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
}
}
/** An expression of an unsigned type. */
private class UnsignedExpr extends FlowSignExpr {
UnsignedExpr() { Utils::getTrackedType(this) instanceof SemUnsignedIntegerType }
override Sign getSignRestriction() {
result = TPos() or
result = TZero()
}
}
pragma[nomagic]
private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
binary.getLeftOperand() = left and binary.getRightOperand() = right
@@ -328,10 +338,11 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
* - `isEq = false` : `v != eqbound`
*/
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
exists(SemGuard guard, boolean testIsTrue, boolean polarity |
pos.hasReadOfVar(v) and
semGuardControlsSsaRead(guard, pos, testIsTrue) and
guard.isEquality(eqbound, Utils::semSsaRead(v, D::fromInt(0)), polarity) and
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
pos.hasReadOfVar(pragma[only_bind_into](v)) and
semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and
guard.isEquality(eqbound, e, polarity) and
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
not unknownSign(eqbound)
)

View File

@@ -24,7 +24,7 @@ import DataFlow::PathGraph
pragma[nomagic]
Instruction getABoundIn(SemBound b, IRFunction func) {
result = b.getExpr(0) and
getSemanticExpr(result) = b.getExpr(0) and
result.getEnclosingIRFunction() = func
}
@@ -115,7 +115,7 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
state1 = s1.toString() and
state2 = s2.toString() and
add.hasOperands(node1.asOperand(), op) and
semBounded(op.getDef(), any(SemZeroBound zero), delta, true, _) and
semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
node2.asInstruction() = add and
s1 = s2 + delta
)

View File

@@ -19,7 +19,7 @@ import PointerArithmeticToDerefFlow::PathGraph
pragma[nomagic]
Instruction getABoundIn(SemBound b, IRFunction func) {
result = b.getExpr(0) and
getSemanticExpr(result) = b.getExpr(0) and
result.getEnclosingIRFunction() = func
}

View File

@@ -24,7 +24,7 @@ import semmle.code.cpp.ir.IR
pragma[nomagic]
Instruction getABoundIn(SemBound b, IRFunction func) {
result = b.getExpr(0) and
getSemanticExpr(result) = b.getExpr(0) and
result.getEnclosingIRFunction() = func
}

View File

@@ -5,6 +5,7 @@ import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisImpl
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
import semmle.code.cpp.ir.IR as IR
import TestUtilities.InlineExpectationsTest
@@ -18,7 +19,7 @@ class ModulusAnalysisTest extends InlineExpectationsTest {
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(SemExpr e, IR::CallInstruction call |
call.getArgument(0) = e and
getSemanticExpr(call.getArgument(0)) = e and
call.getStaticCallTarget().hasName("mod") and
tag = "mod" and
element = e.toString() and

View File

@@ -12,7 +12,7 @@ class RangeAnalysisTest extends InlineExpectationsTest {
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(SemExpr e, IR::CallInstruction call |
call.getArgument(0) = e and
getSemanticExpr(call.getArgument(0)) = e and
call.getStaticCallTarget().hasName("range") and
tag = "range" and
element = e.toString() and

View File

@@ -18,7 +18,7 @@ int test2(struct List* p) {
int count = 0;
for (; p; p = p->next) {
count = (count+1) % 10;
range(count); // $ range=>=-9 range=<=9
range(count); // $ range=<=9 range=>=-9 range=<=count:p+1
}
range(count); // $ range=>=-9 range=<=9
return count;
@@ -29,7 +29,7 @@ int test3(struct List* p) {
for (; p; p = p->next) {
range(count++); // $ range=>=-9 range=<=9
count = count % 10;
range(count); // $ range=>=-9 range=<=9
range(count); // $ range=<=9 range=>=-9 range="<=... +++0" range=<=count:p+1
}
range(count); // $ range=>=-9 range=<=9
return count;
@@ -149,7 +149,7 @@ int test11(char *p) {
range(*p);
}
if (c == ':') {
range(c);
range(c); // $ range===58
c = *p;
range(*p);
if (c != '\0') {
@@ -318,7 +318,7 @@ int test_mult01(int a, int b) {
int r = a*b; // -143 .. 253
range(r);
total += r;
range(total);
range(total); // $ MISSING: range=">=... * ...+0"
}
if (3 <= a && a <= 11 && -13 <= b && b <= 0) {
range(a); // $ range=<=11 range=>=3
@@ -366,7 +366,7 @@ int test_mult02(int a, int b) {
int r = a*b; // -143 .. 253
range(r);
total += r;
range(total);
range(total); // $ MISSING: range=">=... * ...+0"
}
if (0 <= a && a <= 11 && -13 <= b && b <= 0) {
range(a); // $ range=<=11 range=>=0
@@ -461,7 +461,7 @@ int test_mult04(int a, int b) {
int r = a*b; // -391 .. 221
range(r);
total += r;
range(total);
range(total); // $ MISSING: range="<=... * ...+0"
}
if (-17 <= a && a <= 0 && -13 <= b && b <= 0) {
range(a); // $ range=<=0 range=>=-17
@@ -509,7 +509,7 @@ int test_mult05(int a, int b) {
int r = a*b; // -391 .. 221
range(r);
total += r;
range(total);
range(total); // $ MISSING: range="<=... * ...+0"
}
if (-17 <= a && a <= -2 && -13 <= b && b <= 0) {
range(a); // $ range=<=-2 range=>=-17
@@ -856,18 +856,18 @@ int notequal_type_endpoint(unsigned n) {
void notequal_refinement(short n) {
if (n < 0) {
range(n);
range(n); // $ range=<=-1
return;
}
if (n == 0) {
range(n); // 0 .. 0
} else {
range(n); // 1 ..
range(n); // $ range=>=1
}
if (n) {
range(n); // 1 ..
range(n); // $ range=>=1
} else {
range(n); // 0 .. 0
}
@@ -883,16 +883,16 @@ void notequal_refinement(short n) {
void notequal_variations(short n, float f) {
if (n != 0) {
if (n >= 0) {
range(n); // 1 .. [BUG: we can't handle `!=` coming first]
range(n); // $ range=>=1
}
}
if (n >= 5) {
if (2 * n - 10 == 0) { // Same as `n == 10/2` (modulo overflow)
range(n);
range(n); // $ range=>=5 MISSING: range===5
return;
}
range(n); // 6 ..
range(n); // $ range=>=5 MISSING: range=>=6
}
if (n != -32768 && n != -32767) {
@@ -900,8 +900,12 @@ void notequal_variations(short n, float f) {
}
if (n >= 0) {
n ? (range(n), n) : (range(n), n); // ? 1.. : 0..0
!n ? (range(n), n) : (range(n), n); // ? 0..0 : 1..
n ?
(range(n), n) // $ range=>=1
: (range(n), n); // $ MISSING: range===0
!n ?
(range(n), n) // $ MISSING: range===0
: (range(n), n); // $ range=>=1
}
}
@@ -917,7 +921,7 @@ void two_bounds_from_one_test(short ss, unsigned short us) {
}
if (ss < 0x8001) { // Lower bound removed in `getDefLowerBounds`
range(ss); // -32768 .. 32767
range(ss); // $ range=<=32768 MISSING: range=>=-32768
}
if ((short)us >= 0) {
@@ -970,7 +974,7 @@ void test_mod_neg(int s) {
void test_mod_ternary(int s, bool b) {
int s2 = s % (b ? 5 : 500);
range(s2); // $ range=>=-499 range=<=499
range(s2); // $ range=>=-499 range=<=499 range="<=... ? ... : ...-1"
}
void test_mod_ternary2(int s, bool b1, bool b2) {

View File

@@ -4,6 +4,7 @@ import experimental.semmle.code.cpp.semantic.Semantic
import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
import semmle.code.cpp.ir.IR as IR
import TestUtilities.InlineExpectationsTest
@@ -16,7 +17,7 @@ class SignAnalysisTest extends InlineExpectationsTest {
override predicate hasActualResult(Location location, string element, string tag, string value) {
exists(SemExpr e, IR::CallInstruction call |
call.getArgument(0) = e and
getSemanticExpr(call.getArgument(0)) = e and
call.getStaticCallTarget().hasName("sign") and
tag = "sign" and
element = e.toString() and