hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-25 00:35:20 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #14697 from MathiasVP/range-analysis-simplify-conversions

Browse Source 
C++: Simplify the definition of `SemExpr` for range analysis
This commit is contained in:
Mathias Vorreiter Pedersen
2023-11-07 14:52:09 +00:00
committed by GitHub
parent b2512eb212 4455ed982d
commit a04830b8b2
7 changed files with 38 additions and 113 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/RangeAnalysis.qll
View File

@@ -17,9 +17,7 @@ private import semmle.code.cpp.valuenumbering.GlobalValueNumbering
* `upper` is true, and can be traced back to a guard represented by `reason`.
*/
predicate bounded(Expr e, Bound b, float delta, boolean upper, Reason reason) {
exists(SemanticExprConfig::Expr semExpr |
semExpr.getUnconverted().getUnconvertedResultExpression() = e
|
exists(SemanticExprConfig::Expr semExpr | semExpr.getUnconvertedResultExpression() = e |
semBounded(semExpr, b, delta, upper, reason)
)
}
@@ -30,9 +28,7 @@ predicate bounded(Expr e, Bound b, float delta, boolean upper, Reason reason) {
* The `Expr` may be a conversion.
*/
predicate convertedBounded(Expr e, Bound b, float delta, boolean upper, Reason reason) {
exists(SemanticExprConfig::Expr semExpr |
semExpr.getConverted().getConvertedResultExpression() = e
|
exists(SemanticExprConfig::Expr semExpr | semExpr.getConvertedResultExpression() = e |
semBounded(semExpr, b, delta, upper, reason)
)
}

4
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll
View File

@@ -100,7 +100,7 @@ predicate exprMightOverflowNegatively(Expr expr) {
lowerBound(expr) < exprMinVal(expr)
or
exists(SemanticExprConfig::Expr semExpr |
semExpr.getUnconverted().getAst() = expr and
semExpr.getAst() = expr and
ConstantStage::potentiallyOverflowingExpr(false, semExpr) and
not ConstantStage::initialBounded(semExpr, _, _, false, _, _, _)
)
@@ -126,7 +126,7 @@ predicate exprMightOverflowPositively(Expr expr) {
upperBound(expr) > exprMaxVal(expr)
or
exists(SemanticExprConfig::Expr semExpr |
semExpr.getUnconverted().getAst() = expr and
semExpr.getAst() = expr and
ConstantStage::potentiallyOverflowingExpr(true, semExpr) and
not ConstantStage::initialBounded(semExpr, _, _, true, _, _, _)
)

16
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExpr.qll
View File

@@ -4,6 +4,7 @@
private import Semantic
private import SemanticExprSpecific::SemanticExprConfig as Specific
private import SemanticType
/**
* An language-neutral expression.
@@ -241,8 +242,21 @@ class SemConvertExpr extends SemUnaryExpr {
SemConvertExpr() { opcode instanceof Opcode::Convert }
}
private import semmle.code.cpp.ir.IR as IR
/** A conversion instruction which is guaranteed to not overflow. */
private class SafeConversion extends IR::ConvertInstruction {
SafeConversion() {
exists(SemType tFrom, SemType tTo |
tFrom = getSemanticType(super.getUnary().getResultIRType()) and
tTo = getSemanticType(super.getResultIRType()) and
conversionCannotOverflow(tFrom, tTo)
)
}
}
class SemCopyValueExpr extends SemUnaryExpr {
SemCopyValueExpr() { opcode instanceof Opcode::CopyValue }
SemCopyValueExpr() { opcode instanceof Opcode::CopyValue or this instanceof SafeConversion }
}
class SemNegateExpr extends SemUnaryExpr {

97
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
View File

@@ -12,87 +12,10 @@ private import semmle.code.cpp.ir.ValueNumbering
module SemanticExprConfig {
class Location = Cpp::Location;
/** 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() }
}
class Expr = IR::Instruction;
SemBasicBlock getExprBasicBlock(Expr e) { result = getSemanticBasicBlock(e.getBlock()) }
@@ -139,12 +62,12 @@ module SemanticExprConfig {
predicate stringLiteral(Expr expr, SemType type, string value) {
anyConstantExpr(expr, type, value) and
expr.getUnconverted() instanceof IR::StringConstantInstruction
expr instanceof IR::StringConstantInstruction
}
predicate binaryExpr(Expr expr, Opcode opcode, SemType type, Expr leftOperand, Expr rightOperand) {
exists(IR::BinaryInstruction instr |
instr = expr.getUnconverted() and
instr = expr and
type = getSemanticType(instr.getResultIRType()) and
leftOperand = getSemanticExpr(instr.getLeft()) and
rightOperand = getSemanticExpr(instr.getRight()) and
@@ -154,14 +77,14 @@ module SemanticExprConfig {
}
predicate unaryExpr(Expr expr, Opcode opcode, SemType type, Expr operand) {
exists(IR::UnaryInstruction instr | instr = expr.getUnconverted() |
exists(IR::UnaryInstruction instr | instr = expr |
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() |
exists(IR::StoreInstruction instr | instr = expr |
type = getSemanticType(instr.getResultIRType()) and
operand = getSemanticExpr(instr.getSourceValue()) and
opcode instanceof Opcode::Store
@@ -170,13 +93,13 @@ module SemanticExprConfig {
predicate nullaryExpr(Expr expr, Opcode opcode, SemType type) {
exists(IR::LoadInstruction load |
load = expr.getUnconverted() and
load = expr and
type = getSemanticType(load.getResultIRType()) and
opcode instanceof Opcode::Load
)
or
exists(IR::InitializeParameterInstruction init |
init = expr.getUnconverted() and
init = expr and
type = getSemanticType(init.getResultIRType()) and
opcode instanceof Opcode::InitializeParameter
)
@@ -290,9 +213,9 @@ module SemanticExprConfig {
}
Expr getAUse(SsaVariable v) {
result.getUnconverted().(IR::LoadInstruction).getSourceValue() = v.asInstruction()
result.(IR::LoadInstruction).getSourceValue() = v.asInstruction()
or
result.getUnconverted() = v.asPointerArithGuard().getAnInstruction()
result = v.asPointerArithGuard().getAnInstruction()
}
SemType getSsaVariableType(SsaVariable v) {
@@ -433,7 +356,7 @@ module SemanticExprConfig {
}
/** Gets the expression associated with `instr`. */
SemExpr getSemanticExpr(IR::Instruction instr) { result = Equiv::getEquivalenceClass(instr) }
SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
}
predicate getSemanticExpr = SemanticExprConfig::getSemanticExpr/1;

14
cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp
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="<=Phi: p | Store: count+1"
range(count); // $ range=<=9 range=>=-9
}
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="<=Store: ... +++0" range="<=Phi: p | Store: count+1"
range(count); // $ range=<=9 range=>=-9
}
range(count); // $ range=>=-9 range=<=9
return count;
@@ -317,7 +317,7 @@ int test_mult01(int a, int b) {
range(b); // $ range=<=23 range=>=-13
int r = a*b; // $ overflow=+- -143 .. 253
range(r);
total += r; // $ overflow=+
total += r; // $ overflow=+-
range(total); // $ MISSING: range=">=... * ...+0"
}
if (3 <= a && a <= 11 && -13 <= b && b <= 0) {
@@ -365,7 +365,7 @@ int test_mult02(int a, int b) {
range(b); // $ range=<=23 range=>=-13
int r = a*b; // $ overflow=+- -143 .. 253
range(r);
total += r; // $ overflow=+
total += r; // $ overflow=+-
range(total); // $ MISSING: range=">=... * ...+0"
}
if (0 <= a && a <= 11 && -13 <= b && b <= 0) {
@@ -460,7 +460,7 @@ int test_mult04(int a, int b) {
range(b); // $ range=<=23 range=>=-13
int r = a*b; // $ overflow=+- -391 .. 221
range(r);
total += r; // $ overflow=-
total += r; // $ overflow=+-
range(total); // $ MISSING: range="<=... * ...+0"
}
if (-17 <= a && a <= 0 && -13 <= b && b <= 0) {
@@ -508,7 +508,7 @@ int test_mult05(int a, int b) {
range(b); // $ range=<=23 range=>=-13
int r = a*b; // $ overflow=+- -391 .. 221
range(r);
total += r; // $ overflow=-
total += r; // $ overflow=+-
range(total); // $ MISSING: range="<=... * ...+0"
}
if (-17 <= a && a <= -2 && -13 <= b && b <= 0) {
@@ -974,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="<=Phi: ... ? ... : ...-1"
range(s2); // $ range=>=-499 range=<=499
}
void test_mod_ternary2(int s, bool b1, bool b2) {

8
cpp/ql/test/query-tests/Security/CWE/CWE-193/InvalidPointerDeref.expected
View File

@@ -30,8 +30,6 @@ edges
| test.cpp:206:17:206:23 | ... + ... | test.cpp:206:17:206:23 | ... + ... |
| test.cpp:206:17:206:23 | ... + ... | test.cpp:213:5:213:13 | ... = ... |
| test.cpp:206:17:206:23 | ... + ... | test.cpp:213:5:213:13 | ... = ... |
| test.cpp:231:18:231:30 | new[] | test.cpp:232:3:232:20 | ... = ... |
| test.cpp:238:20:238:32 | new[] | test.cpp:239:5:239:22 | ... = ... |
| test.cpp:260:13:260:24 | new[] | test.cpp:261:14:261:21 | ... + ... |
| test.cpp:261:14:261:21 | ... + ... | test.cpp:261:14:261:21 | ... + ... |
| test.cpp:261:14:261:21 | ... + ... | test.cpp:264:13:264:14 | * ... |
@@ -135,10 +133,6 @@ nodes
| test.cpp:206:17:206:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:206:17:206:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:213:5:213:13 | ... = ... | semmle.label | ... = ... |
| test.cpp:231:18:231:30 | new[] | semmle.label | new[] |
| test.cpp:232:3:232:20 | ... = ... | semmle.label | ... = ... |
| test.cpp:238:20:238:32 | new[] | semmle.label | new[] |
| test.cpp:239:5:239:22 | ... = ... | semmle.label | ... = ... |
| test.cpp:260:13:260:24 | new[] | semmle.label | new[] |
| test.cpp:261:14:261:21 | ... + ... | semmle.label | ... + ... |
| test.cpp:261:14:261:21 | ... + ... | semmle.label | ... + ... |
@@ -222,8 +216,6 @@ subpaths
| test.cpp:67:9:67:14 | ... = ... | test.cpp:52:19:52:37 | call to malloc | test.cpp:67:9:67:14 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:52:19:52:37 | call to malloc | call to malloc | test.cpp:53:20:53:23 | size | size |
| test.cpp:201:5:201:19 | ... = ... | test.cpp:194:15:194:33 | call to malloc | test.cpp:201:5:201:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:194:15:194:33 | call to malloc | call to malloc | test.cpp:195:21:195:23 | len | len |
| test.cpp:213:5:213:13 | ... = ... | test.cpp:205:15:205:33 | call to malloc | test.cpp:213:5:213:13 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:205:15:205:33 | call to malloc | call to malloc | test.cpp:206:21:206:23 | len | len |
| test.cpp:232:3:232:20 | ... = ... | test.cpp:231:18:231:30 | new[] | test.cpp:232:3:232:20 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:231:18:231:30 | new[] | new[] | test.cpp:232:11:232:15 | index | index |
| test.cpp:239:5:239:22 | ... = ... | test.cpp:238:20:238:32 | new[] | test.cpp:239:5:239:22 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:238:20:238:32 | new[] | new[] | test.cpp:239:13:239:17 | index | index |
| test.cpp:264:13:264:14 | * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len |
| test.cpp:274:5:274:10 | ... = ... | test.cpp:270:13:270:24 | new[] | test.cpp:274:5:274:10 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:270:13:270:24 | new[] | new[] | test.cpp:271:19:271:21 | len | len |
| test.cpp:358:14:358:26 | end_plus_one indirection | test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | end_plus_one indirection | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |

4
cpp/ql/test/query-tests/Security/CWE/CWE-193/test.cpp
View File

@@ -229,14 +229,14 @@ void test15(unsigned index) {
return;
}
int* newname = new int[size];
newname[index] = 0; // $ alloc=L231 deref=L232 // GOOD [FALSE POSITIVE]
newname[index] = 0; // GOOD
}
void test16(unsigned index) {
unsigned size = index + 13;
if(size >= index) {
int* newname = new int[size];
newname[index] = 0; // $ alloc=L238 deref=L239 // GOOD [FALSE POSITIVE]
newname[index] = 0; // GOOD
}
}