Skip to content

Commit f98ebdb

Browse files
authored
Merge pull request #204 from mbaluda-org/Contracts6
Contracts6
2 parents c3a6231 + ec548d0 commit f98ebdb

File tree

21 files changed

+609
-8
lines changed

21 files changed

+609
-8
lines changed

.vscode/tasks.json

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,11 @@
193193
"Classes",
194194
"Comments",
195195
"Contracts1",
196+
"Contracts2",
197+
"Contracts3",
198+
"Contracts4",
199+
"Contracts5",
200+
"Contracts6",
196201
"Concurrency",
197202
"Concurrency",
198203
"Concurrency1",
Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
# EXP40-C: Do not modify constant objects
2+
3+
This query implements the CERT-C rule EXP40-C:
4+
5+
> Do not modify constant objects
6+
7+
8+
## Description
9+
10+
The C Standard, 6.7.3, paragraph 6 \[[IS](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IEC9899-2011)[O/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO-IEC9899-2011)\], states
11+
12+
> If an attempt is made to modify an object defined with a `const`-qualified type through use of an [lvalue](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-lvalue) with non-`const`-qualified type, the behavior is undefined.
13+
14+
15+
See also [undefined behavior 64](https://wiki.sei.cmu.edu/confluence/display/c/CC.+Undefined+Behavior#CC.UndefinedBehavior-ub_64).
16+
17+
There are existing compiler [implementations](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation) that allow `const`-qualified objects to be modified without generating a warning message.
18+
19+
Avoid casting away `const` qualification because doing so makes it possible to modify `const`-qualified objects without issuing diagnostics. (See [EXP05-C. Do not cast away a const qualification](https://wiki.sei.cmu.edu/confluence/display/c/EXP05-C.+Do+not+cast+away+a+const+qualification) and [STR30-C. Do not attempt to modify string literals](https://wiki.sei.cmu.edu/confluence/display/c/STR30-C.+Do+not+attempt+to+modify+string+literals) for more details.)
20+
21+
## Noncompliant Code Example
22+
23+
This noncompliant code example allows a constant object to be modified:
24+
25+
```cpp
26+
const int **ipp;
27+
int *ip;
28+
const int i = 42;
29+
30+
void func(void) {
31+
ipp = &ip; /* Constraint violation */
32+
*ipp = &i; /* Valid */
33+
*ip = 0; /* Modifies constant i (was 42) */
34+
}
35+
```
36+
The first assignment is unsafe because it allows the code that follows it to attempt to change the value of the `const` object `i`.
37+
38+
**Implementation Details**
39+
40+
If `ipp`, `ip`, and `i` are declared as automatic variables, this example compiles without warning with Microsoft Visual Studio 2013 when compiled in C mode (`/TC`) and the resulting program changes the value of `i`. GCC 4.8.1 generates a warning but compiles, and the resulting program changes the value of `i`.
41+
42+
If `ipp`, `ip`, and `i` are declared with static storage duration, this program compiles without warning and terminates abnormally with Microsoft Visual Studio 2013, and compiles with warning and terminates abnormally with GCC 4.8.1.
43+
44+
## Compliant Solution
45+
46+
The compliant solution depends on the intent of the programmer. If the intent is that the value of `i` is modifiable, then it should not be declared as a constant, as in this compliant solution:
47+
48+
```cpp
49+
int **ipp;
50+
int *ip;
51+
int i = 42;
52+
53+
void func(void) {
54+
ipp = &ip; /* Valid */
55+
*ipp = &i; /* Valid */
56+
*ip = 0; /* Valid */
57+
}
58+
```
59+
If the intent is that the value of i is not meant to change, then do not write noncompliant code that attempts to modify it.
60+
61+
## Risk Assessment
62+
63+
Modifying constant objects through nonconstant references is [undefined behavior](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-undefinedbehavior).
64+
65+
<table> <tbody> <tr> <th> Rule </th> <th> Severity </th> <th> Likelihood </th> <th> Remediation Cost </th> <th> Priority </th> <th> Level </th> </tr> <tr> <td> EXP40-C </td> <td> Low </td> <td> Unlikely </td> <td> Medium </td> <td> <strong>P2</strong> </td> <td> <strong>L3</strong> </td> </tr> </tbody> </table>
66+
67+
68+
## Automated Detection
69+
70+
<table> <tbody> <tr> <th> Tool </th> <th> Version </th> <th> Checker </th> <th> Description </th> </tr> <tr> <td> <a> Astrée </a> </td> <td> 22.04 </td> <td> <strong>assignment-to-non-modifiable-lvalue</strong> <strong>pointer-qualifier-cast-const</strong> <strong>pointer-qualifier-cast-const-implicit</strong> <strong>write-to-constant-memory</strong> </td> <td> Fully checked </td> </tr> <tr> <td> <a> Axivion Bauhaus Suite </a> </td> <td> 7.2.0 </td> <td> <strong>CertC-EXP40</strong> </td> <td> </td> </tr> <tr> <td> <a> Coverity </a> </td> <td> 2017.07 </td> <td> <strong>PW</strong> <strong>MISRA C 2004 Rule 11.5</strong> </td> <td> Implemented </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2022.3 </td> <td> <strong>C0563</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>582 S</strong> </td> <td> Fully implemented </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2022.1 </td> <td> <strong>CERT_C-EXP40-a</strong> </td> <td> A cast shall not remove any 'const' or 'volatile' qualification from the type of a pointer or reference </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> R2022b </td> <td> <a> CERT C: Rule EXP40-C </a> </td> <td> Checks for write operations on const qualified objects (rule fully covered) </td> </tr> <tr> <td> <a> PRQA QA-C </a> </td> <td> 9.7 </td> <td> <strong>0563</strong> </td> <td> Partially implemented </td> </tr> <tr> <td> <a> RuleChecker </a> </td> <td> 22.04 </td> <td> <strong>assignment-to-non-modifiable-lvalue</strong> <strong>pointer-qualifier-cast-const</strong> <strong>pointer-qualifier-cast-const-implicit</strong> </td> <td> Partially checked </td> </tr> <tr> <td> <a> TrustInSoft Analyzer </a> </td> <td> 1.38 </td> <td> <strong>mem_access</strong> </td> <td> Exhaustively verified (see <a> the compliant and the non-compliant example </a> ). </td> </tr> </tbody> </table>
71+
72+
73+
## Related Vulnerabilities
74+
75+
Search for [vulnerabilities](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-vulnerability) resulting from the violation of this rule on the [CERT website](https://www.kb.cert.org/vulnotes/bymetric?searchview&query=FIELD+KEYWORDS+contains+EXP40-C).
76+
77+
## Related Guidelines
78+
79+
[Key here](https://wiki.sei.cmu.edu/confluence/display/c/How+this+Coding+Standard+is+Organized#HowthisCodingStandardisOrganized-RelatedGuidelines) (explains table format and definitions)
80+
81+
<table> <tbody> <tr> <th> Taxonomy </th> <th> Taxonomy item </th> <th> Relationship </th> </tr> <tr> <td> <a> CERT C Secure Coding Standard </a> </td> <td> <a> EXP05-C. Do not cast away a const qualification </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> <tr> <td> <a> CERT C Secure Coding Standard </a> </td> <td> <a> STR30-C. Do not attempt to modify string literals </a> </td> <td> Prior to 2018-01-12: CERT: Unspecified Relationship </td> </tr> </tbody> </table>
82+
83+
84+
## Bibliography
85+
86+
<table> <tbody> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> Subclause 6.7.3, "Type Qualifiers" </td> </tr> </tbody> </table>
87+
88+
89+
## Implementation notes
90+
91+
The implementation does not consider pointer aliasing via multiple indirection.
92+
93+
## References
94+
95+
* CERT-C: [EXP40-C: Do not modify constant objects](https://wiki.sei.cmu.edu/confluence/display/c)
Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/**
2+
* @id c/cert/do-not-modify-constant-objects
3+
* @name EXP40-C: Do not modify constant objects
4+
* @description Do not modify constant objects. This may result in undefined behavior.
5+
* @kind path-problem
6+
* @precision high
7+
* @problem.severity error
8+
* @tags external/cert/id/exp40-c
9+
* correctness
10+
* external/cert/obligation/rule
11+
*/
12+
13+
import cpp
14+
import codingstandards.c.cert
15+
import semmle.code.cpp.dataflow.DataFlow
16+
import DataFlow::PathGraph
17+
import codingstandards.cpp.SideEffect
18+
19+
class ConstRemovingCast extends Cast {
20+
ConstRemovingCast() {
21+
this.getExpr().getType().(DerivedType).getBaseType*().isConst() and
22+
not this.getType().(DerivedType).getBaseType*().isConst()
23+
}
24+
}
25+
26+
class MaybeReturnsStringLiteralFunctionCall extends FunctionCall {
27+
MaybeReturnsStringLiteralFunctionCall() {
28+
getTarget().getName() in [
29+
"strpbrk", "strchr", "strrchr", "strstr", "wcspbrk", "wcschr", "wcsrchr", "wcsstr",
30+
"memchr", "wmemchr"
31+
]
32+
}
33+
}
34+
35+
class MyDataFlowConfCast extends DataFlow::Configuration {
36+
MyDataFlowConfCast() { this = "MyDataFlowConfCast" }
37+
38+
override predicate isSource(DataFlow::Node source) {
39+
source.asExpr().getFullyConverted() instanceof ConstRemovingCast
40+
or
41+
source.asExpr().getFullyConverted() = any(MaybeReturnsStringLiteralFunctionCall c)
42+
}
43+
44+
override predicate isSink(DataFlow::Node sink) {
45+
sink.asExpr() = any(Assignment a).getLValue().(PointerDereferenceExpr).getOperand()
46+
}
47+
}
48+
49+
from MyDataFlowConfCast conf, DataFlow::PathNode src, DataFlow::PathNode sink
50+
where
51+
conf.hasFlowPath(src, sink)
52+
or
53+
sink.getNode()
54+
.asExpr()
55+
.(VariableEffect)
56+
.getTarget()
57+
.getType()
58+
.(DerivedType)
59+
.getBaseType*()
60+
.isConst()
61+
select sink, src, sink, "Const variable assigned with non const-value."
Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
edges
2+
| test.c:5:8:5:9 | & ... | test.c:6:4:6:5 | aa |
3+
| test.c:26:15:26:15 | a | test.c:27:4:27:4 | a |
4+
| test.c:34:13:34:14 | & ... | test.c:39:7:39:8 | p1 |
5+
| test.c:39:7:39:8 | p1 | test.c:26:15:26:15 | a |
6+
| test.c:40:7:40:9 | * ... | test.c:26:15:26:15 | a |
7+
| test.c:59:7:59:8 | & ... | test.c:60:4:60:4 | p |
8+
| test.c:79:11:79:16 | call to strchr | test.c:81:6:81:12 | ... ++ |
9+
nodes
10+
| test.c:5:8:5:9 | & ... | semmle.label | & ... |
11+
| test.c:6:4:6:5 | aa | semmle.label | aa |
12+
| test.c:26:15:26:15 | a | semmle.label | a |
13+
| test.c:27:4:27:4 | a | semmle.label | a |
14+
| test.c:34:13:34:14 | & ... | semmle.label | & ... |
15+
| test.c:39:7:39:8 | p1 | semmle.label | p1 |
16+
| test.c:40:7:40:9 | * ... | semmle.label | * ... |
17+
| test.c:59:7:59:8 | & ... | semmle.label | & ... |
18+
| test.c:60:4:60:4 | p | semmle.label | p |
19+
| test.c:74:12:74:12 | s | semmle.label | s |
20+
| test.c:79:11:79:16 | call to strchr | semmle.label | call to strchr |
21+
| test.c:81:6:81:12 | ... ++ | semmle.label | ... ++ |
22+
subpaths
23+
#select
24+
| test.c:6:4:6:5 | aa | test.c:5:8:5:9 | & ... | test.c:6:4:6:5 | aa | Const variable assigned with non const-value. |
25+
| test.c:27:4:27:4 | a | test.c:34:13:34:14 | & ... | test.c:27:4:27:4 | a | Const variable assigned with non const-value. |
26+
| test.c:27:4:27:4 | a | test.c:40:7:40:9 | * ... | test.c:27:4:27:4 | a | Const variable assigned with non const-value. |
27+
| test.c:60:4:60:4 | p | test.c:59:7:59:8 | & ... | test.c:60:4:60:4 | p | Const variable assigned with non const-value. |
28+
| test.c:74:12:74:12 | s | test.c:74:12:74:12 | s | test.c:74:12:74:12 | s | Const variable assigned with non const-value. |
29+
| test.c:81:6:81:12 | ... ++ | test.c:79:11:79:16 | call to strchr | test.c:81:6:81:12 | ... ++ | Const variable assigned with non const-value. |
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/EXP40-C/DoNotModifyConstantObjects.ql

c/cert/test/rules/EXP40-C/test.c

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
void f1() {
2+
const int a = 3;
3+
int *aa;
4+
5+
aa = &a;
6+
*aa = 100; // NON_COMPLIANT
7+
}
8+
9+
void f1a() {
10+
const int a = 3;
11+
int *aa;
12+
13+
aa = &a; // COMPLIANT
14+
}
15+
16+
void f2() {
17+
int a = 3;
18+
int *aa;
19+
a = 3;
20+
21+
aa = &a;
22+
*aa = a;
23+
*aa = &a;
24+
}
25+
26+
void f4a(int *a) {
27+
*a = 100; // NON_COMPLIANT
28+
}
29+
30+
void f4b(int *a) {}
31+
32+
void f4() {
33+
const int a = 100;
34+
int *p1 = &a; // COMPLIANT
35+
const int **p2;
36+
37+
*p2 = &a; // COMPLIANT
38+
39+
f4a(p1); // COMPLIANT
40+
f4a(*p2); // COMPLIANT
41+
}
42+
43+
void f5() {
44+
const int a = 100;
45+
int *p1 = &a; // COMPLIANT
46+
const int **p2;
47+
48+
*p2 = &a; // COMPLIANT
49+
50+
f4b(p1);
51+
f4b(*p2);
52+
}
53+
54+
#include <string.h>
55+
56+
void f6a() {
57+
char *p;
58+
const char c = 'A';
59+
p = &c;
60+
*p = 0; // NON_COMPLIANT
61+
}
62+
63+
void f6b() {
64+
const char **cpp;
65+
char *p;
66+
const char c = 'A';
67+
cpp = &p;
68+
*cpp = &c;
69+
*p = 0; // NON_COMPLIANT[FALSE_NEGATIVE]
70+
}
71+
72+
const char s[] = "foo"; // source
73+
void f7() {
74+
*(char *)s = '\0'; // NON_COMPLIANT
75+
}
76+
77+
const char *f8(const char *pathname) {
78+
char *slash;
79+
slash = strchr(pathname, '/');
80+
if (slash) {
81+
*slash++ = '\0'; // NON_COMPLIANT
82+
return slash;
83+
}
84+
return pathname;
85+
}
Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
/**
2+
* @id c/misra/array-function-argument-number-of-elements
3+
* @name RULE-17-5: An array founction argument shall have an appropriate number of elements
4+
* @description The function argument corresponding to an array parameter shall have an appropriate
5+
* number of elements.
6+
* @kind problem
7+
* @precision high
8+
* @problem.severity error
9+
* @tags external/misra/id/rule-17-5
10+
* correctness
11+
* external/misra/obligation/advisory
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.misra
16+
import semmle.code.cpp.dataflow.DataFlow
17+
18+
/**
19+
* Models a function parameter of type array with specified size
20+
* ```
21+
* void f1(int ar[3]);
22+
* ```
23+
*/
24+
class ArrayParameter extends Parameter {
25+
ArrayParameter() { this.getType().(ArrayType).hasArraySize() }
26+
27+
Expr getAMatchingArgument() {
28+
exists(FunctionCall fc |
29+
this.getFunction() = fc.getTarget() and
30+
result = fc.getArgument(this.getIndex())
31+
)
32+
}
33+
34+
int getArraySize() { result = this.getType().(ArrayType).getArraySize() }
35+
}
36+
37+
/**
38+
* The number of initialized elements in an ArrayAggregateLiteral.
39+
* In the following examples the result=2
40+
* ```
41+
* int arr3[3] = {1, 2};
42+
* int arr2[2] = {1, 2, 3};
43+
* ```
44+
*/
45+
int countElements(ArrayAggregateLiteral l) { result = count(l.getElementExpr(_)) }
46+
47+
class SmallArrayConfig extends DataFlow::Configuration {
48+
SmallArrayConfig() { this = "SmallArrayConfig" }
49+
50+
override predicate isSource(DataFlow::Node src) { src.asExpr() instanceof ArrayAggregateLiteral }
51+
52+
override predicate isSink(DataFlow::Node sink) {
53+
sink.asExpr() = any(ArrayParameter p).getAMatchingArgument()
54+
}
55+
}
56+
57+
from Expr arg, ArrayParameter p
58+
where
59+
not isExcluded(arg, Contracts6Package::arrayFunctionArgumentNumberOfElementsQuery()) and
60+
exists(SmallArrayConfig config | arg = p.getAMatchingArgument() |
61+
// the argument is a value and not an arrey
62+
not arg.getType() instanceof DerivedType
63+
or
64+
// the argument is an array too small
65+
arg.getType().(ArrayType).getArraySize() < p.getArraySize()
66+
or
67+
// the argument is a pointer and its value does not come from a literal of the correct
68+
arg.getType() instanceof PointerType and
69+
not exists(ArrayAggregateLiteral l |
70+
config.hasFlow(DataFlow::exprNode(l), DataFlow::exprNode(arg)) and
71+
countElements(l) >= p.getArraySize()
72+
)
73+
)
74+
select arg,
75+
"The function argument does not have a sufficient number or elements declared in the $@.", p,
76+
"parameter"
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/**
2+
* @id c/misra/value-returned-by-a-function-not-used
3+
* @name RULE-17-7: Return values should be used or cast to void
4+
* @description The value returned by a function having non-void return type shall be used or cast
5+
* to void.
6+
* @kind problem
7+
* @precision very-high
8+
* @problem.severity error
9+
* @tags external/misra/id/rule-17-7
10+
* correctness
11+
* external/misra/obligation/required
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.misra
16+
import semmle.code.cpp.dataflow.DataFlow
17+
18+
from Call c
19+
where
20+
not isExcluded(c, Contracts6Package::valueReturnedByAFunctionNotUsedQuery()) and
21+
// Calls in `ExprStmt`s indicate that the return value is ignored
22+
c.getParent() instanceof ExprStmt and
23+
// Ignore calls to void functions or where the return value is cast to `void`
24+
not c.getActualType() instanceof VoidType and
25+
// Exclude cases where the function call is generated within a macro, as the user of the macro is
26+
// not necessarily able to address thoes results
27+
not c.isAffectedByMacro()
28+
select c, "The value returned by this call shall be used or cast to `void`."

0 commit comments

Comments
 (0)