Merge pull request #13603 from MathiasVP/implement-is-unreachable-in-call-2

This commit is contained in:
Mathias Vorreiter Pedersen
2023-06-30 12:00:15 +01:00
committed by GitHub
3 changed files with 124 additions and 10 deletions

View File

@@ -856,7 +856,73 @@ class DataFlowCall extends CallInstruction {
Function getEnclosingCallable() { result = this.getEnclosingFunction() }
}
predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub implementation
module IsUnreachableInCall {
private import semmle.code.cpp.ir.ValueNumbering
private import semmle.code.cpp.controlflow.IRGuards as G
private class ConstantIntegralTypeArgumentNode extends PrimaryArgumentNode {
int value;
ConstantIntegralTypeArgumentNode() {
value = op.getDef().(IntegerConstantInstruction).getValue().toInt()
}
int getValue() { result = value }
}
pragma[nomagic]
private predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
any(G::IRGuardCondition guard).ensuresEq(left, right, k, block, areEqual)
}
pragma[nomagic]
private predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
any(G::IRGuardCondition guard).ensuresLt(left, right, k, block, areEqual)
}
predicate isUnreachableInCall(Node n, DataFlowCall call) {
exists(
DirectParameterNode paramNode, ConstantIntegralTypeArgumentNode arg,
IntegerConstantInstruction constant, int k, Operand left, Operand right, IRBlock block
|
// arg flows into `paramNode`
DataFlowImplCommon::viableParamArg(call, paramNode, arg) and
left = constant.getAUse() and
right = valueNumber(paramNode.getInstruction()).getAUse() and
block = n.getBasicBlock()
|
// and there's a guard condition which ensures that the result of `left == right + k` is `areEqual`
exists(boolean areEqual |
ensuresEq(pragma[only_bind_into](left), pragma[only_bind_into](right),
pragma[only_bind_into](k), pragma[only_bind_into](block), areEqual)
|
// this block ensures that left = right + k, but it holds that `left != right + k`
areEqual = true and
constant.getValue().toInt() != arg.getValue() + k
or
// this block ensures that or `left != right + k`, but it holds that `left = right + k`
areEqual = false and
constant.getValue().toInt() = arg.getValue() + k
)
or
// or there's a guard condition which ensures that the result of `left < right + k` is `isLessThan`
exists(boolean isLessThan |
ensuresLt(pragma[only_bind_into](left), pragma[only_bind_into](right),
pragma[only_bind_into](k), pragma[only_bind_into](block), isLessThan)
|
isLessThan = true and
// this block ensures that `left < right + k`, but it holds that `left >= right + k`
constant.getValue().toInt() >= arg.getValue() + k
or
// this block ensures that `left >= right + k`, but it holds that `left < right + k`
isLessThan = false and
constant.getValue().toInt() < arg.getValue() + k
)
)
}
}
import IsUnreachableInCall
int accessPathLimit() { result = 5 }

View File

@@ -40,10 +40,7 @@ edges
| test.cpp:159:25:159:29 | array | test.cpp:161:5:161:10 | access to array |
| test.cpp:159:25:159:29 | array | test.cpp:162:5:162:10 | access to array |
| test.cpp:175:30:175:30 | p | test.cpp:191:27:191:30 | access to array |
| test.cpp:198:14:198:20 | buffer1 | test.cpp:175:30:175:30 | p |
| test.cpp:198:14:198:20 | buffer1 | test.cpp:198:14:198:20 | buffer1 |
| test.cpp:201:14:201:20 | buffer2 | test.cpp:175:30:175:30 | p |
| test.cpp:201:14:201:20 | buffer2 | test.cpp:201:14:201:20 | buffer2 |
| test.cpp:175:30:175:30 | p | test.cpp:191:27:191:30 | access to array |
| test.cpp:204:14:204:20 | buffer3 | test.cpp:175:30:175:30 | p |
| test.cpp:204:14:204:20 | buffer3 | test.cpp:204:14:204:20 | buffer3 |
| test.cpp:207:35:207:35 | p | test.cpp:208:14:208:14 | p |
@@ -113,11 +110,8 @@ nodes
| test.cpp:161:5:161:10 | access to array | semmle.label | access to array |
| test.cpp:162:5:162:10 | access to array | semmle.label | access to array |
| test.cpp:175:30:175:30 | p | semmle.label | p |
| test.cpp:175:30:175:30 | p | semmle.label | p |
| test.cpp:191:27:191:30 | access to array | semmle.label | access to array |
| test.cpp:198:14:198:20 | buffer1 | semmle.label | buffer1 |
| test.cpp:198:14:198:20 | buffer1 | semmle.label | buffer1 |
| test.cpp:201:14:201:20 | buffer2 | semmle.label | buffer2 |
| test.cpp:201:14:201:20 | buffer2 | semmle.label | buffer2 |
| test.cpp:204:14:204:20 | buffer3 | semmle.label | buffer3 |
| test.cpp:204:14:204:20 | buffer3 | semmle.label | buffer3 |
| test.cpp:207:35:207:35 | p | semmle.label | p |
@@ -144,5 +138,4 @@ subpaths
| test.cpp:136:9:136:16 | PointerAdd: ... += ... | test.cpp:143:18:143:21 | asdf | test.cpp:138:13:138:15 | arr | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:142:10:142:13 | asdf | asdf | test.cpp:138:12:138:15 | Load: * ... | read |
| test.cpp:151:5:151:11 | PointerAdd: access to array | test.cpp:148:23:148:28 | buffer | test.cpp:151:5:151:11 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:147:19:147:24 | buffer | buffer | test.cpp:151:5:151:15 | Store: ... = ... | write |
| test.cpp:162:5:162:10 | PointerAdd: access to array | test.cpp:159:25:159:29 | array | test.cpp:162:5:162:10 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:158:10:158:14 | array | array | test.cpp:162:5:162:19 | Store: ... = ... | write |
| test.cpp:191:27:191:30 | PointerAdd: access to array | test.cpp:201:14:201:20 | buffer2 | test.cpp:191:27:191:30 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:200:19:200:25 | buffer2 | buffer2 | test.cpp:191:27:191:30 | Load: access to array | read |
| test.cpp:191:27:191:30 | PointerAdd: access to array | test.cpp:216:19:216:25 | buffer2 | test.cpp:191:27:191:30 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:215:19:215:25 | buffer2 | buffer2 | test.cpp:191:27:191:30 | Load: access to array | read |

View File

@@ -734,3 +734,58 @@ void test_does_not_write_source_to_dereference()
does_not_write_source_to_dereference(&x);
sink(x); // $ ast,ir=733:7 SPURIOUS: ast,ir=726:11
}
void sometimes_calls_sink_eq(int x, int n) {
if(n == 0) {
sink(x); // $ ast,ir=751:27 ast,ir=755:32 SPURIOUS: ast=749:27 ast,ir=753:32 // IR spurious results because we only have call contexts of depth 1
}
}
void call_sometimes_calls_sink_eq(int x, int n) {
sometimes_calls_sink_eq(x, n);
}
void test_sometimes_calls_sink_eq_1() {
sometimes_calls_sink_eq(source(), 1);
sometimes_calls_sink_eq(0, 0);
sometimes_calls_sink_eq(source(), 0);
call_sometimes_calls_sink_eq(source(), 1);
call_sometimes_calls_sink_eq(0, 0);
call_sometimes_calls_sink_eq(source(), 0);
}
void sometimes_calls_sink_lt(int x, int n) {
if(n < 10) {
sink(x); // $ ast,ir=771:27 ast,ir=775:32 SPURIOUS: ast=769:27 ast,ir=773:32 // IR spurious results because we only have call contexts of depth 1
}
}
void call_sometimes_calls_sink_lt(int x, int n) {
sometimes_calls_sink_lt(x, n);
}
void test_sometimes_calls_sink_lt() {
sometimes_calls_sink_lt(source(), 10);
sometimes_calls_sink_lt(0, 0);
sometimes_calls_sink_lt(source(), 2);
call_sometimes_calls_sink_lt(source(), 10);
call_sometimes_calls_sink_lt(0, 0);
call_sometimes_calls_sink_lt(source(), 2);
}
void sometimes_calls_sink_switch(int x, int n) {
switch(n) {
case 0:
sink(x); // $ ast,ir=790:31 SPURIOUS: ast,ir=788:31 // IR spurious results because IRGuard doesn't understand switch statements.
break;
}
}
void test_sometimes_calls_sink_switch() {
sometimes_calls_sink_switch(source(), 1);
sometimes_calls_sink_switch(0, 0);
sometimes_calls_sink_switch(source(), 0);
}