C++: Remove the ad-hoc code for keeping track of increments/decrements on pointers in the 'cpp/overrun-write' query.

This commit is contained in:
Mathias Vorreiter Pedersen
2025-07-22 18:21:51 +01:00
parent a1f4246c5f
commit e0eadc75dd
2 changed files with 4 additions and 130 deletions

View File

@@ -88,81 +88,14 @@ module ValidState {
predicate isSink(DataFlow::Node sink) { isSinkPairImpl(_, _, sink, _, _) }
predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
isAdditionalFlowStep2(node1, node2, _)
}
predicate includeHiddenNodes() { any() }
predicate isBarrierOut(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
}
private import DataFlow::Global<ValidStateConfig>
private predicate inLoop(PathNode n) { n.getASuccessor+() = n }
/**
* Holds if `value` is a possible offset for `n`.
*
* To ensure termination, we limit `value` to be in the
* range `[-2, 2]` if the node is part of a loop. Without
* this restriction we wouldn't terminate on an example like:
* ```cpp
* while(unknown()) { size++; }
* ```
*/
private predicate validStateImpl(PathNode n, int value) {
// If the dataflow node depends recursively on itself we restrict the range.
(inLoop(n) implies value = [-2 .. 2]) and
(
// For the dataflow source we have an allocation such as `malloc(size + k)`,
// and the value of the flow-state is then `k`.
hasSize(_, n.getNode(), value)
or
// For a dataflow sink any `value` that is strictly smaller than the delta
// needs to be a valid flow-state. That is, for a snippet like:
// ```
// p = b ? new char[size] : new char[size + 1];
// memset(p, 0, size + 2);
// ```
// the valid flow-states at the `memset` must include the set `{0, 1}` since the
// flow-state at `new char[size]` is `0`, and the flow-state at `new char[size + 1]`
// is `1`.
//
// So we find a valid flow-state at the sink's predecessor, and use the definition
// of our sink predicate to compute the valid flow-states at the sink.
exists(int delta, PathNode n0 |
n0.getASuccessor() = n and
validStateImpl(n0, value) and
isSinkPairImpl(_, _, n.getNode(), delta, _) and
delta > value
)
or
// For a non-source and non-sink node there is two cases to consider.
// 1. A node where we have to update the flow-state, or
// 2. A node that doesn't update the flow-state.
//
// For case 1, we compute the new flow-state by adding the constant operand of the
// `AddInstruction` to the flow-state of any predecessor node.
// For case 2 we simply propagate the valid flow-states from the predecessor node to
// the next one.
exists(PathNode n0, DataFlow::Node node0, DataFlow::Node node, int value0 |
n0.getASuccessor() = n and
validStateImpl(n0, value0) and
node = n.getNode() and
node0 = n0.getNode()
|
exists(int delta |
isAdditionalFlowStep2(node0, node, delta) and
value0 = value + delta
)
or
not isAdditionalFlowStep2(node0, node, _) and
value = value0
)
)
}
predicate validState(DataFlow::Node n, int value) {
validStateImpl(any(PathNode pn | pn.getNode() = n), value)
predicate validState(DataFlow::Node source, DataFlow::Node sink, int value) {
hasSize(_, source, value) and
flow(source, sink)
}
}
@@ -213,16 +146,6 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
}
predicate isBarrierOut2(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
predicate isAdditionalFlowStep2(
DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
) {
validState(node2, state2) and
exists(int delta |
isAdditionalFlowStep2(node1, node2, delta) and
state1 = state2 + delta
)
}
}
module StringSizeFlow = ProductFlow::GlobalWithState<StringSizeConfig>;

View File

@@ -12,19 +12,6 @@ edges
| test.cpp:42:13:42:15 | *str [string] | test.cpp:42:18:42:23 | string | provenance | |
| test.cpp:72:17:72:19 | *str [string] | test.cpp:72:22:72:27 | string | provenance | |
| test.cpp:80:17:80:19 | *str [string] | test.cpp:80:22:80:27 | string | provenance | |
| test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | provenance | |
| test.cpp:90:5:90:7 | *str [post update] [string] | test.cpp:91:5:91:7 | *str [string] | provenance | |
| test.cpp:90:5:90:34 | ... = ... | test.cpp:90:5:90:7 | *str [post update] [string] | provenance | |
| test.cpp:90:19:90:24 | call to malloc | test.cpp:90:5:90:34 | ... = ... | provenance | |
| test.cpp:91:5:91:7 | *str [string] | test.cpp:92:12:92:14 | *str [string] | provenance | |
| test.cpp:92:12:92:14 | *str [string] | test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | provenance | |
| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | provenance | |
| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:99:13:99:15 | *str [string] | provenance | |
| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:129:17:129:19 | *str [string] | provenance | |
| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:137:17:137:19 | *str [string] | provenance | |
| test.cpp:99:13:99:15 | *str [string] | test.cpp:99:18:99:23 | string | provenance | |
| test.cpp:129:17:129:19 | *str [string] | test.cpp:129:22:129:27 | string | provenance | |
| test.cpp:137:17:137:19 | *str [string] | test.cpp:137:22:137:27 | string | provenance | |
| test.cpp:147:5:147:7 | *str [post update] [string] | test.cpp:148:5:148:7 | *str [string] | provenance | |
| test.cpp:147:5:147:34 | ... = ... | test.cpp:147:5:147:7 | *str [post update] [string] | provenance | |
| test.cpp:147:19:147:24 | call to malloc | test.cpp:147:5:147:34 | ... = ... | provenance | |
@@ -46,12 +33,6 @@ edges
| test.cpp:199:17:199:19 | *str [string] | test.cpp:199:22:199:27 | string | provenance | |
| test.cpp:203:17:203:19 | *str [string] | test.cpp:203:22:203:27 | string | provenance | |
| test.cpp:207:17:207:19 | *str [string] | test.cpp:207:22:207:27 | string | provenance | |
| test.cpp:214:24:214:24 | p | test.cpp:216:10:216:10 | p | provenance | |
| test.cpp:220:27:220:54 | call to malloc | test.cpp:220:27:220:54 | call to malloc | provenance | |
| test.cpp:220:27:220:54 | call to malloc | test.cpp:222:15:222:20 | buffer | provenance | |
| test.cpp:222:15:222:20 | buffer | test.cpp:214:24:214:24 | p | provenance | |
| test.cpp:228:27:228:54 | call to malloc | test.cpp:228:27:228:54 | call to malloc | provenance | |
| test.cpp:228:27:228:54 | call to malloc | test.cpp:232:10:232:15 | buffer | provenance | |
| test.cpp:235:40:235:45 | buffer | test.cpp:236:5:236:26 | ... = ... | provenance | |
| test.cpp:236:5:236:9 | *p_str [post update] [string] | test.cpp:235:27:235:31 | *p_str [Return] [string] | provenance | |
| test.cpp:236:5:236:9 | *p_str [post update] [string] | test.cpp:235:27:235:31 | *p_str [string] | provenance | |
@@ -64,8 +45,6 @@ edges
| test.cpp:243:12:243:14 | *str [string] | test.cpp:243:12:243:21 | string | provenance | |
| test.cpp:249:14:249:33 | call to my_alloc | test.cpp:249:14:249:33 | call to my_alloc | provenance | |
| test.cpp:249:14:249:33 | call to my_alloc | test.cpp:250:12:250:12 | p | provenance | |
| test.cpp:256:5:256:25 | ... = ... | test.cpp:257:12:257:12 | p | provenance | |
| test.cpp:256:9:256:25 | call to malloc | test.cpp:256:5:256:25 | ... = ... | provenance | |
| test.cpp:262:15:262:30 | call to malloc | test.cpp:262:15:262:30 | call to malloc | provenance | |
| test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | provenance | |
| test.cpp:264:9:264:30 | ... = ... | test.cpp:266:12:266:12 | p | provenance | |
@@ -87,20 +66,6 @@ nodes
| test.cpp:72:22:72:27 | string | semmle.label | string |
| test.cpp:80:17:80:19 | *str [string] | semmle.label | *str [string] |
| test.cpp:80:22:80:27 | string | semmle.label | string |
| test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | semmle.label | **mk_string_t_plus_one [string] |
| test.cpp:90:5:90:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
| test.cpp:90:5:90:34 | ... = ... | semmle.label | ... = ... |
| test.cpp:90:19:90:24 | call to malloc | semmle.label | call to malloc |
| test.cpp:91:5:91:7 | *str [string] | semmle.label | *str [string] |
| test.cpp:92:12:92:14 | *str [string] | semmle.label | *str [string] |
| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | semmle.label | *call to mk_string_t_plus_one [string] |
| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | semmle.label | *call to mk_string_t_plus_one [string] |
| test.cpp:99:13:99:15 | *str [string] | semmle.label | *str [string] |
| test.cpp:99:18:99:23 | string | semmle.label | string |
| test.cpp:129:17:129:19 | *str [string] | semmle.label | *str [string] |
| test.cpp:129:22:129:27 | string | semmle.label | string |
| test.cpp:137:17:137:19 | *str [string] | semmle.label | *str [string] |
| test.cpp:137:22:137:27 | string | semmle.label | string |
| test.cpp:147:5:147:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
| test.cpp:147:5:147:34 | ... = ... | semmle.label | ... = ... |
| test.cpp:147:19:147:24 | call to malloc | semmle.label | call to malloc |
@@ -123,14 +88,6 @@ nodes
| test.cpp:203:22:203:27 | string | semmle.label | string |
| test.cpp:207:17:207:19 | *str [string] | semmle.label | *str [string] |
| test.cpp:207:22:207:27 | string | semmle.label | string |
| test.cpp:214:24:214:24 | p | semmle.label | p |
| test.cpp:216:10:216:10 | p | semmle.label | p |
| test.cpp:220:27:220:54 | call to malloc | semmle.label | call to malloc |
| test.cpp:220:27:220:54 | call to malloc | semmle.label | call to malloc |
| test.cpp:222:15:222:20 | buffer | semmle.label | buffer |
| test.cpp:228:27:228:54 | call to malloc | semmle.label | call to malloc |
| test.cpp:228:27:228:54 | call to malloc | semmle.label | call to malloc |
| test.cpp:232:10:232:15 | buffer | semmle.label | buffer |
| test.cpp:235:27:235:31 | *p_str [Return] [string] | semmle.label | *p_str [Return] [string] |
| test.cpp:235:27:235:31 | *p_str [string] | semmle.label | *p_str [string] |
| test.cpp:235:40:235:45 | buffer | semmle.label | buffer |
@@ -145,9 +102,6 @@ nodes
| test.cpp:249:14:249:33 | call to my_alloc | semmle.label | call to my_alloc |
| test.cpp:249:14:249:33 | call to my_alloc | semmle.label | call to my_alloc |
| test.cpp:250:12:250:12 | p | semmle.label | p |
| test.cpp:256:5:256:25 | ... = ... | semmle.label | ... = ... |
| test.cpp:256:9:256:25 | call to malloc | semmle.label | call to malloc |
| test.cpp:257:12:257:12 | p | semmle.label | p |
| test.cpp:262:15:262:30 | call to malloc | semmle.label | call to malloc |
| test.cpp:262:15:262:30 | call to malloc | semmle.label | call to malloc |
| test.cpp:264:9:264:30 | ... = ... | semmle.label | ... = ... |
@@ -163,9 +117,6 @@ subpaths
| test.cpp:42:5:42:11 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:42:18:42:23 | string | This write may overflow $@ by 1 element. | test.cpp:42:18:42:23 | string | string |
| test.cpp:72:9:72:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:72:22:72:27 | string | This write may overflow $@ by 1 element. | test.cpp:72:22:72:27 | string | string |
| test.cpp:80:9:80:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:80:22:80:27 | string | This write may overflow $@ by 2 elements. | test.cpp:80:22:80:27 | string | string |
| test.cpp:99:5:99:11 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:99:18:99:23 | string | This write may overflow $@ by 1 element. | test.cpp:99:18:99:23 | string | string |
| test.cpp:129:9:129:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:129:22:129:27 | string | This write may overflow $@ by 1 element. | test.cpp:129:22:129:27 | string | string |
| test.cpp:137:9:137:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:137:22:137:27 | string | This write may overflow $@ by 2 elements. | test.cpp:137:22:137:27 | string | string |
| test.cpp:152:5:152:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:152:18:152:23 | string | This write may overflow $@ by 1 element. | test.cpp:152:18:152:23 | string | string |
| test.cpp:154:5:154:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:154:18:154:23 | string | This write may overflow $@ by 1 element. | test.cpp:154:18:154:23 | string | string |
| test.cpp:156:5:156:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:156:18:156:23 | string | This write may overflow $@ by 2 elements. | test.cpp:156:18:156:23 | string | string |