Skip to content

Commit 2a0429b

Browse files
author
Nikita Kraiouchkine
committed
Implement InvalidMemory1 queries
Modify packages and implement EXP33-C, EXP34-C, and MEM30-C
1 parent 1c3570d commit 2a0429b

33 files changed

+1425
-33
lines changed

.vscode/tasks.json

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -222,6 +222,8 @@
222222
"Includes",
223223
"Initialization",
224224
"IntegerConversion",
225+
"InvalidMemory1",
226+
"InvalidMemory2",
225227
"Invariants",
226228
"Iterators",
227229
"Lambdas",
@@ -230,6 +232,8 @@
230232
"Literals",
231233
"Loops",
232234
"Macros",
235+
"Memory1",
236+
"Memory2",
233237
"Misc",
234238
"MoveForward",
235239
"Naming",

c/cert/src/rules/EXP33-C/DoNotReadUninitializedMemory.md

Lines changed: 418 additions & 0 deletions
Large diffs are not rendered by default.
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/**
2+
* @id c/cert/do-not-read-uninitialized-memory
3+
* @name EXP33-C: Do not read uninitialized memory
4+
* @description Using the value of an object with automatic storage duration while it is
5+
* indeterminate is undefined behavior.
6+
* @kind problem
7+
* @precision medium
8+
* @problem.severity error
9+
* @tags external/cert/id/exp33-c
10+
* correctness
11+
* security
12+
* external/cert/obligation/rule
13+
*/
14+
15+
import cpp
16+
import codingstandards.c.cert
17+
import codingstandards.cpp.rules.readofuninitializedmemory.ReadOfUninitializedMemory
18+
19+
class DoNotReadUninitializedMemoryQuery extends ReadOfUninitializedMemorySharedQuery {
20+
DoNotReadUninitializedMemoryQuery() {
21+
this = InvalidMemory1Package::doNotReadUninitializedMemoryQuery()
22+
}
23+
}

c/cert/src/rules/EXP34-C/DoNotDereferenceNullPointers.md

Lines changed: 220 additions & 0 deletions
Large diffs are not rendered by default.
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
/**
2+
* @id c/cert/do-not-dereference-null-pointers
3+
* @name EXP34-C: Do not dereference null pointers
4+
* @description Dereferencing a null pointer leads to undefined behavior.
5+
* @kind problem
6+
* @precision medium
7+
* @problem.severity error
8+
* @tags external/cert/id/exp34-c
9+
* correctness
10+
* external/cert/obligation/rule
11+
*/
12+
13+
import cpp
14+
import codingstandards.c.cert
15+
import codingstandards.cpp.rules.dereferenceofnullpointer.DereferenceOfNullPointer
16+
17+
class DoNotDereferenceNullPointersQuery extends DereferenceOfNullPointerSharedQuery {
18+
DoNotDereferenceNullPointersQuery() {
19+
this = InvalidMemory1Package::doNotDereferenceNullPointersQuery()
20+
}
21+
}

c/cert/src/rules/MEM30-C/DoNotAccessFreedMemory.md

Lines changed: 258 additions & 0 deletions
Large diffs are not rendered by default.
Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
/**
2+
* @id c/cert/do-not-access-freed-memory
3+
* @name MEM30-C: Do not access freed memory
4+
* @description Accessing memory that has been deallocated is undefined behavior.
5+
* @kind problem
6+
* @precision high
7+
* @problem.severity error
8+
* @tags external/cert/id/mem30-c
9+
* correctness
10+
* security
11+
* external/cert/obligation/rule
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.cert
16+
import codingstandards.cpp.Allocations
17+
import semmle.code.cpp.controlflow.StackVariableReachability
18+
19+
/** `e` is an expression that frees the memory pointed to by `v`. */
20+
predicate isFreeExpr(Expr e, StackVariable v) {
21+
exists(VariableAccess va | va.getTarget() = v and freeExprOrIndirect(e, va, _))
22+
}
23+
24+
/** `e` is an expression that (may) dereference `v`. */
25+
predicate isDerefExpr(Expr e, StackVariable v) {
26+
v.getAnAccess() = e and dereferenced(e)
27+
or
28+
isDerefByCallExpr(_, _, e, v)
29+
}
30+
31+
/**
32+
* `va` is passed by value as (part of) the `i`th argument in
33+
* call `c`. The target function is either a library function
34+
* or a source code function that dereferences the relevant
35+
* parameter.
36+
*/
37+
predicate isDerefByCallExpr(Call c, int i, VariableAccess va, StackVariable v) {
38+
v.getAnAccess() = va and
39+
va = c.getAnArgumentSubExpr(i) and
40+
not c.passesByReference(i, va) and
41+
(c.getTarget().hasEntryPoint() implies isDerefExpr(_, c.getTarget().getParameter(i)))
42+
}
43+
44+
class UseAfterFreeReachability extends StackVariableReachability {
45+
UseAfterFreeReachability() { this = "UseAfterFree" }
46+
47+
override predicate isSource(ControlFlowNode node, StackVariable v) { isFreeExpr(node, v) }
48+
49+
override predicate isSink(ControlFlowNode node, StackVariable v) { isDerefExpr(node, v) }
50+
51+
override predicate isBarrier(ControlFlowNode node, StackVariable v) {
52+
definitionBarrier(v, node) or
53+
isFreeExpr(node, v)
54+
}
55+
}
56+
57+
from UseAfterFreeReachability r, StackVariable v, Expr free, Expr e
58+
where
59+
not isExcluded(e, InvalidMemory1Package::doNotAccessFreedMemoryQuery()) and
60+
r.reaches(free, v, e)
61+
select e,
62+
"Memory pointed to by '" + v.getName().toString() +
63+
"' accessed but may have been previously freed $@.", free, "here"
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
c/common/test/rules/readofuninitializedmemory/ReadOfUninitializedMemory.ql
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
c/common/test/rules/dereferenceofnullpointer/DereferenceOfNullPointer.ql
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
| test.c:11:47:11:47 | p | Memory pointed to by 'p' accessed but may have been previously freed $@. | test.c:12:5:12:8 | call to free | here |
2+
| test.c:25:10:25:12 | buf | Memory pointed to by 'buf' accessed but may have been previously freed $@. | test.c:24:3:24:6 | call to free | here |

0 commit comments

Comments
 (0)