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

Author: MathiasVP

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll

@@ -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 }
 

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected

@@ -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 |

cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp

@@ -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);
+}