Skip to content

Commit 5ea652b

Browse files
committed
Refine into path-problem
1 parent fe2a3c4 commit 5ea652b

File tree

2 files changed

+110
-56
lines changed

2 files changed

+110
-56
lines changed

cpp/misra/src/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql

Lines changed: 18 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
* @name RULE-8-7-1: Pointer arithmetic shall not form an invalid pointer.
44
* @description Pointers obtained as result of performing arithmetic should point to an initialized
55
* object, or an element right next to the last element of an array.
6-
* @kind problem
6+
* @kind path-problem
77
* @precision very-high
88
* @problem.severity error
99
* @tags external/misra/id/rule-8-7-1
@@ -14,7 +14,7 @@
1414

1515
import cpp
1616
import codingstandards.cpp.misra
17-
import semmle.code.cpp.dataflow.new.DataFlow
17+
import semmle.code.cpp.dataflow.new.TaintTracking
1818
import semmle.code.cpp.security.BufferAccess
1919

2020
class ArrayDeclaration extends VariableDeclarationEntry {
@@ -135,14 +135,11 @@ class PointerFormation extends TPointerFormation {
135135
}
136136

137137
Expr asExpr() {
138-
result = this.asArrayExpr() or
138+
result = this.asArrayExpr() or // This needs to be array base, as we are only dealing with pointers here.
139139
result = this.asPointerArithmetic()
140140
}
141141

142-
DataFlow::Node getNode() {
143-
result.asExpr() = this.asExpr() or
144-
result.asIndirectExpr() = this.asExpr()
145-
}
142+
DataFlow::Node getNode() { result.asExpr() = this.asExpr() }
146143

147144
Location getLocation() {
148145
result = this.asArrayExpr().getLocation() or
@@ -160,40 +157,31 @@ module TrackArrayConfig implements DataFlow::ConfigSig {
160157
}
161158
}
162159

163-
import semmle.code.cpp.dataflow.new.TaintTracking
164160
module TrackArray = TaintTracking::Global<TrackArrayConfig>;
165161

166-
private predicate arrayDeclarationAndAccess(
167-
DataFlow::Node arrayDeclarationNode, DataFlow::Node pointerFormationNode
168-
) {
169-
TrackArray::flow(arrayDeclarationNode, pointerFormationNode)
170-
}
171-
172162
private predicate arrayIndexExceedsOutOfBounds(
173163
DataFlow::Node arrayDeclarationNode, DataFlow::Node pointerFormationNode
174164
) {
175165
/* 1. Ensure the array access is reachable from the array declaration. */
176-
arrayDeclarationAndAccess(arrayDeclarationNode, pointerFormationNode) and
166+
TrackArray::flow(arrayDeclarationNode, pointerFormationNode) and
167+
/* 2. Cases where a pointer formation becomes illegal. */
177168
exists(ArrayAllocation arrayAllocation, PointerFormation pointerFormation |
178-
arrayDeclarationNode.asExpr() = arrayAllocation.asStackAllocation().getInitExpr() and
169+
arrayDeclarationNode = arrayAllocation.getNode() and
179170
pointerFormationNode = pointerFormation.getNode()
180171
|
181-
/* 2. Cases where a pointer formation becomes illegal. */
182-
(
183-
/* 2-1. An offset cannot be negative. */
184-
pointerFormation.getOffset() < 0
185-
or
186-
/* 2-2. The offset should be at most (number of elements) + 1 = (the declared length). */
187-
arrayAllocation.getLength() < pointerFormation.getOffset()
188-
)
172+
/* 2-1. An offset cannot be negative. */
173+
pointerFormation.getOffset() < 0
174+
or
175+
/* 2-2. The offset should be at most (number of elements) + 1 = (the declared length). */
176+
arrayAllocation.getLength() < pointerFormation.getOffset()
189177
)
190178
}
191179

192-
from PointerFormation pointerFormation
180+
import TrackArray::PathGraph
181+
182+
from TrackArray::PathNode source, TrackArray::PathNode sink
193183
where
194-
not isExcluded(pointerFormation.asExpr(),
184+
not isExcluded(sink.getNode().asExpr(),
195185
Memory1Package::pointerArithmeticFormsAnInvalidPointerQuery()) and
196-
exists(DataFlow::Node pointerFormationNode | pointerFormationNode = pointerFormation.getNode() |
197-
arrayIndexExceedsOutOfBounds(_, pointerFormationNode)
198-
)
199-
select pointerFormation, "TODO"
186+
arrayIndexExceedsOutOfBounds(source.getNode(), sink.getNode())
187+
select sink, source, sink, "TODO"
Lines changed: 92 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
#include <cstdlib>
22

3-
void f1(int *array) {
3+
void stack_allocation_pointer_arithmetic(int *array) {
44
/* 1. Pointer formed from performing arithmetic */
55
int *valid1 = array; // COMPLIANT: pointer is within boundary
66
int *valid2 = array + 1; // COMPLIANT: pointer is within boundary
@@ -13,7 +13,7 @@ void f1(int *array) {
1313
int *invalid2 = array - 1; // NON_COMPLIANT: pointer is outside boundary
1414
}
1515

16-
void f2(int *array) {
16+
void stack_allocation_array_access(int *array) {
1717
/* 2. Array Access (entails pointer arithmetic) */
1818
int valid1 = array[0]; // COMPLIANT: pointer is within boundary
1919
int valid2 = array[1]; // COMPLIANT: pointer is within boundary
@@ -25,37 +25,103 @@ void f2(int *array) {
2525
int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
2626
}
2727

28-
void f1_realloc(int *array) {
28+
void malloc_pointer_arithmetic(int *array) { // [1, 4]
2929
/* 1. Pointer formed from performing arithmetic */
30-
int *valid1 = array; // COMPLIANT: pointer is within boundary
31-
int *valid2 = array + 1; // COMPLIANT: pointer is within boundary
32-
int *valid3 = array + 2; // COMPLIANT: pointer is within boundary
33-
int *valid4 =
34-
array + 3; // COMPLIANT: pointer points one beyond the last element
35-
int *invalid1 =
36-
array +
37-
4; // NON_COMPLIANT: pointer points more than one beyond the last element
30+
int *valid1 = array; // COMPLIANT: pointer is within boundary (lower bound: 1)
31+
int *valid2 = array + 1; // COMPLIANT: pointer points more than one beyond the
32+
// last element (lower bound: 1)
33+
int *valid3 = array + 2; // NON_COMPLIANT: pointer points more than one beyond
34+
// the last element (lower bound: 1)
35+
int *valid4 = array + 3; // NON_COMPLIANT: pointer points more than one beyond
36+
// the last element (lower bound: 1)
37+
int *invalid1 = array + 4; // NON_COMPLIANT: pointer points more than one
38+
// beyond the last element (lower bound: 1)
39+
int *invalid2 = array + 5; // NON_COMPLIANT: pointer points more than one
40+
// beyond the last element (lower bound: 1)
41+
int *invalid3 = array - 1; // NON_COMPLIANT: pointer is outside boundary
42+
}
43+
44+
void malloc_array_access(int *array) { // [1, 4]
45+
/* 2. Array Access (entails pointer arithmetic) */
46+
int valid1 =
47+
array[0]; // COMPLIANT: pointer is within boundary (lower bound: 1)
48+
int valid2 = array[1]; // COMPLIANT: pointer points more than one beyond the
49+
// last element, but non-compliant to Rule 4.1.3 (lower
50+
// bound: 1)
51+
int valid3 = array[2]; // NON_COMPLIANT: pointer points more than one beyond
52+
// the last element (lower bound: 1)
53+
int valid4 = array[3]; // NON_COMPLIANT: pointer points more than one beyond
54+
// the last element (lower bound: 1)
55+
int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one beyond
56+
// the last element (lower bound: 1)
57+
int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
58+
}
59+
60+
void calloc_pointer_arithmetic(int *array) { // [2, 5]
61+
/* 1. Pointer formed from performing arithmetic */
62+
int *valid1 = array; // COMPLIANT: pointer is within boundary (lower bound: 2)
63+
int *valid2 =
64+
array + 1; // COMPLIANT: pointer is within boundary (lower bound: 2)
65+
int *valid3 = array + 2; // COMPLIANT: pointer points more than one beyond the
66+
// last element, but non-compliant to Rule 4.1.3
67+
// (lower bound: 2)
68+
int *valid4 = array + 3; // NON_COMPLIANT: pointer points more than one beyond
69+
// the last element (lower bound: 2)
70+
int *invalid1 = array + 4; // NON_COMPLIANT: pointer points more than one
71+
// beyond the last element (lower bound: 2)
3872
int *invalid2 = array - 1; // NON_COMPLIANT: pointer is outside boundary
3973
}
4074

41-
void f2_realloc(int *array) {
75+
void calloc_array_access(int *array) { // [2, 5]
4276
/* 2. Array Access (entails pointer arithmetic) */
4377
int valid1 = array[0]; // COMPLIANT: pointer is within boundary
4478
int valid2 = array[1]; // COMPLIANT: pointer is within boundary
45-
int valid3 = array[2]; // COMPLIANT: pointer points one beyond the last
46-
int invalid1 = array[3]; // NON_COMPLIANT: pointer points one beyond the last
47-
// element, but non-compliant to Rule 4.1.3
48-
int invalid2 = array[4]; // NON_COMPLIANT: pointer points more than one beyond
49-
// the last element
50-
int invalid3 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
79+
int valid3 = array[2]; // COMPLIANT: pointer points more than one beyond the
80+
// last element, but non-compliant to Rule 4.1.3
81+
// (lower bound: 2)
82+
int valid4 = array[3]; // NON_COMPLIANT: pointer points more than one beyond
83+
// the last element (lower bound: 2)
84+
int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one
85+
// beyond the last element (lower bound: 2)
86+
int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
87+
}
88+
89+
void realloc_pointer_arithmetic(int *array) { // [3, 6]
90+
/* 1. Pointer formed from performing arithmetic */
91+
int *valid1 = array; // COMPLIANT: pointer is within boundary (lower bound: 3)
92+
int *valid2 =
93+
array + 1; // COMPLIANT: pointer is within boundary (lower bound: 3)
94+
int *valid3 =
95+
array + 2; // COMPLIANT: pointer is within boundary (lower bound: 3)
96+
int *valid4 = array + 3; // COMPLIANT: pointer points one beyond the last
97+
// element (lower bound: 3)
98+
int *invalid1 = array + 4; // NON_COMPLIANT: pointer points more than one
99+
// beyond the last element (lower bound: 3)
100+
int *invalid2 = array - 1; // NON_COMPLIANT: pointer is outside boundary
101+
}
102+
103+
void realloc_array_access(int *array) { // [3, 6]
104+
/* 2. Array Access (entails pointer arithmetic) */
105+
int valid1 =
106+
array[0]; // COMPLIANT: pointer is within boundary (lower bound: 3)
107+
int valid2 =
108+
array[1]; // COMPLIANT: pointer is within boundary (lower bound: 3)
109+
int valid3 =
110+
array[2]; // COMPLIANT: pointer is within boundary (lower bound: 3)
111+
int valid4 =
112+
array[3]; // COMPLIANT: pointer points one beyond the last
113+
// element, but non-compliant to Rule 4.1.3 (lower bound: 3)
114+
int invalid1 = array[4]; // NON_COMPLIANT: pointer points more than one beyond
115+
// the last element (lower bound: 3)
116+
int invalid2 = array[-1]; // NON_COMPLIANT: pointer is outside boundary
51117
}
52118

53119
int main(int argc, char *argv[]) {
54120
/* 1. Array initialized on the stack */
55121
int array[3] = {0, 1, 2};
56122

57-
f1(array);
58-
f2(array);
123+
stack_allocation_pointer_arithmetic(array);
124+
stack_allocation_array_access(array);
59125

60126
/* 2. Array initialized on the heap */
61127
int num_of_elements_malloc;
@@ -78,14 +144,14 @@ int main(int argc, char *argv[]) {
78144
int *array_realloc =
79145
(int *)realloc(array_malloc, num_of_elements_realloc * sizeof(int));
80146

81-
f1(array_malloc);
82-
f2(array_malloc);
147+
malloc_pointer_arithmetic(array_malloc);
148+
malloc_array_access(array_malloc);
83149

84-
f1(array_calloc);
85-
f2(array_calloc);
150+
calloc_pointer_arithmetic(array_calloc);
151+
calloc_array_access(array_calloc);
86152

87-
f1_realloc(array_realloc);
88-
f2_realloc(array_realloc);
153+
realloc_pointer_arithmetic(array_realloc);
154+
realloc_array_access(array_realloc);
89155

90156
return 0;
91157
}

0 commit comments

Comments
 (0)