Skip to content

Commit 0bd67b6

Browse files
lcarteylcartey
authored
Merge pull request #512 from github/lcartey/contracts
Add C `Contracts` package
2 parents 1544a28 + 932a8d6 commit 0bd67b6

28 files changed

+609
-59
lines changed

‎c/cert/src/rules/FLP32-C/UncheckedRangeDomainPoleErrors.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -345,7 +345,7 @@ Independent( INT34-C, FLP32-C, INT33-C) CWE-682 = Union( FLP32-C, list) where li
345345

346346
## Implementation notes
347347

348-
None
348+
This query identifies possible domain, pole and range errors on a selection of C standard library fuctions from math.h.
349349

350350
## References
351351

‎c/cert/src/rules/MSC40-C/DoNotViolateInLineLinkageConstraints.md

+210
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
# MSC40-C: Do not violate inline linkage constraints
2+
3+
This query implements the CERT-C rule MSC40-C:
4+
5+
> Do not violate constraints
6+
7+
8+
## Description
9+
10+
According to the C Standard, 3.8 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO%2FIEC9899-2011)\], a constraint is a "restriction, either syntactic or semantic, by which the exposition of language elements is to be interpreted." Despite the similarity of the terms, a runtime constraint is not a kind of constraint.
11+
12+
Violating any *shall* statement within a constraint clause in the C Standard requires an [implementation](https://wiki.sei.cmu.edu/confluence/display/c/BB.+Definitions#BB.Definitions-implementation) to issue a diagnostic message, the C Standard, 5.1.1.3 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO%2FIEC9899-2011)\] states
13+
14+
> A conforming implementation shall produce at least one diagnostic message (identified in an implementation-defined manner) if a preprocessing translation unit or translation unit contains a violation of any syntax rule or constraint, even if the behavior is also explicitly specified as undefined or implementation-defined. Diagnostic messages need not be produced in other circumstances.
15+
16+
17+
The C Standard further explains in a footnote
18+
19+
> The intent is that an implementation should identify the nature of, and where possible localize, each violation. Of course, an implementation is free to produce any number of diagnostics as long as a valid program is still correctly translated. It may also successfully translate an invalid program.
20+
21+
22+
Any constraint violation is a violation of this rule because it can result in an invalid program.
23+
24+
## Noncompliant Code Example (Inline, Internal Linkage)
25+
26+
The C Standard, 6.7.4, paragraph 3 \[[ISO/IEC 9899:2011](https://wiki.sei.cmu.edu/confluence/display/c/AA.+Bibliography#AA.Bibliography-ISO%2FIEC9899-2011)\], states
27+
28+
> An inline definition of a function with external linkage shall not contain a definition of a modifiable object with static or thread storage duration, and shall not contain a reference to an identifier with internal linkage.
29+
30+
31+
The motivation behind this constraint lies in the semantics of inline definitions. Paragraph 7 of subclause 6.7.4 reads, in part:
32+
33+
> An inline definition provides an alternative to an external definition, which a translator may use to implement any call to the function in the same translation unit. It is unspecified whether a call to the function uses the inline definition or the external definition.
34+
35+
36+
That is, if a function has an external and inline definition, implementations are free to choose which definition to invoke (two distinct invocations of the function may call different definitions, one the external definition, the other the inline definition). Therefore, issues can arise when these definitions reference internally linked objects or mutable objects with static or thread storage duration.
37+
38+
This noncompliant code example refers to a static variable with file scope and internal linkage from within an external inline function:
39+
40+
```cpp
41+
static int I = 12;
42+
extern inline void func(int a) {
43+
int b = a * I;
44+
/* ... */
45+
}
46+
47+
```
48+
49+
## Compliant Solution (Inline, Internal Linkage)
50+
51+
This compliant solution omits the `static` qualifier; consequently, the variable `I` has external linkage by default:
52+
53+
```cpp
54+
int I = 12;
55+
extern inline void func(int a) {
56+
int b = a * I;
57+
/* ... */
58+
}
59+
60+
```
61+
62+
## Noncompliant Code Example (inline, Modifiable Static)
63+
64+
This noncompliant code example defines a modifiable `static` variable within an `extern inline` function.
65+
66+
```cpp
67+
extern inline void func(void) {
68+
static int I = 12;
69+
/* Perform calculations which may modify I */
70+
}
71+
72+
```
73+
74+
## Compliant Solution (Inline, Modifiable Static)
75+
76+
This compliant solution removes the `static` keyword from the local variable definition. If the modifications to `I` must be retained between invocations of `func()`, it must be declared at file scope so that it will be defined with external linkage.
77+
78+
```cpp
79+
extern inline void func(void) {
80+
int I = 12;
81+
/* Perform calculations which may modify I */
82+
}
83+
```
84+
85+
## Noncompliant Code Example (Inline, Modifiable static)
86+
87+
This noncompliant code example includes two translation units: `file1.c` and `file2.c`. The first file, `file1.c`, defines a pseudorandom number generation function:
88+
89+
```cpp
90+
/* file1.c */
91+
92+
/* Externally linked definition of the function get_random() */
93+
extern unsigned int get_random(void) {
94+
/* Initialize the seeds */
95+
static unsigned int m_z = 0xdeadbeef;
96+
static unsigned int m_w = 0xbaddecaf;
97+
98+
/* Compute the next pseudorandom value and update the seeds */
99+
m_z = 36969 * (m_z & 65535) + (m_z >> 16);
100+
m_w = 18000 * (m_w & 65535) + (m_w >> 16);
101+
return (m_z << 16) + m_w;
102+
}
103+
104+
```
105+
The left-shift operation in the last line may wrap, but this is permitted by exception INT30-C-EX3 to rule [INT30-C. Ensure that unsigned integer operations do not wrap](https://wiki.sei.cmu.edu/confluence/display/c/INT30-C.+Ensure+that+unsigned+integer+operations+do+not+wrap).
106+
107+
The second file, `file2.c`, defines an `inline` version of this function that references mutable `static` objects—namely, objects that maintain the state of the pseudorandom number generator. Separate invocations of the `get_random()` function can call different definitions, each operating on separate static objects, resulting in a faulty pseudorandom number generator.
108+
109+
```cpp
110+
/* file2.c */
111+
112+
/* Inline definition of get_random function */
113+
inline unsigned int get_random(void) {
114+
/*
115+
* Initialize the seeds
116+
* Constraint violation: static duration storage referenced
117+
* in non-static inline definition
118+
*/
119+
static unsigned int m_z = 0xdeadbeef;
120+
static unsigned int m_w = 0xbaddecaf;
121+
122+
/* Compute the next pseudorandom value and update the seeds */
123+
m_z = 36969 * (m_z & 65535) + (m_z >> 16);
124+
m_w = 18000 * (m_w & 65535) + (m_w >> 16);
125+
return (m_z << 16) + m_w;
126+
}
127+
128+
int main(void) {
129+
unsigned int rand_no;
130+
for (int ii = 0; ii < 100; ii++) {
131+
/*
132+
* Get a pseudorandom number. Implementation defined whether the
133+
* inline definition in this file or the external definition
134+
* in file2.c is called.
135+
*/
136+
rand_no = get_random();
137+
/* Use rand_no... */
138+
}
139+
140+
/* ... */
141+
142+
/*
143+
* Get another pseudorandom number. Behavior is
144+
* implementation defined.
145+
*/
146+
rand_no = get_random();
147+
/* Use rand_no... */
148+
return 0;
149+
}
150+
151+
```
152+
153+
## Compliant Solution (Inline, Modifiable static)
154+
155+
This compliant solution adds the `static` modifier to the `inline` function definition in `file2.c`, giving it internal linkage. All references to `get_random()` in `file.2.c` will now reference the internally linked definition. The first file, which was not changed, is not shown here.
156+
157+
```cpp
158+
/* file2.c */
159+
160+
/* Static inline definition of get_random function */
161+
static inline unsigned int get_random(void) {
162+
/*
163+
* Initialize the seeds.
164+
* No more constraint violation; the inline function is now
165+
* internally linked.
166+
*/
167+
static unsigned int m_z = 0xdeadbeef;
168+
static unsigned int m_w = 0xbaddecaf;
169+
170+
/* Compute the next pseudorandom value and update the seeds */
171+
m_z = 36969 * (m_z & 65535) + (m_z >> 16);
172+
m_w = 18000 * (m_w & 65535) + (m_w >> 16);
173+
return (m_z << 16) + m_w;
174+
}
175+
176+
int main(void) {
177+
/* Generate pseudorandom numbers using get_random()... */
178+
return 0;
179+
}
180+
181+
```
182+
183+
## Risk Assessment
184+
185+
Constraint violations are a broad category of error that can result in unexpected control flow and corrupted data.
186+
187+
<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> MSC40-C </td> <td> Low </td> <td> Unlikely </td> <td> Medium </td> <td> <strong>P2</strong> </td> <td> <strong>L3</strong> </td> </tr> </tbody> </table>
188+
189+
190+
## Automated Detection
191+
192+
<table> <tbody> <tr> <th> Tool </th> <th> Version </th> <th> Checker </th> <th> Description </th> </tr> <tr> <td> <a> Astrée </a> </td> <td> 23.04 </td> <td> <strong>alignas-extended</strong> <strong>assignment-to-non-modifiable-lvalue</strong> <strong>cast-pointer-void-arithmetic-implicit</strong> <strong>element-type-incomplete</strong> <strong>function-pointer-integer-cast-implicit</strong> <strong>function-return-type</strong> <strong>inappropriate-pointer-cast-implicit</strong> <strong>incompatible-function-pointer-conversion</strong> <strong>incompatible-object-pointer-conversion</strong> <strong>initializer-excess</strong> <strong>invalid-array-size</strong> <strong>non-constant-static-assert</strong> <strong>parameter-match-type</strong> <strong>pointer-integral-cast-implicit</strong> <strong>pointer-qualifier-cast-const-implicit</strong> <strong>pointer-qualifier-cast-volatile-implicit</strong> <strong>redeclaration</strong> <strong>return-empty</strong> <strong>return-non-empty</strong> <strong>static-assert</strong> <strong>type-compatibility</strong> <strong>type-compatibility-link</strong> <strong>type-specifier</strong> <strong>undeclared-parameter</strong> <strong>unnamed-parameter</strong> </td> <td> Partially checked </td> </tr> <tr> <td> <a> Helix QAC </a> </td> <td> 2023.4 </td> <td> <strong>C0232, C0233, C0244, C0268, C0321, C0322, C0338, C0422, C0423, C0426, C0427, C0429, C0430, C0431, C0432, C0435, C0436, C0437, C0446, C0447, C0448, C0449, C0451, C0452, C0453, C0454, C0456, C0457, C0458, C0460, C0461, C0462, C0463, C0466, C0467, C0468, C0469, C0476, C0477, C0478, C0481, C0482, C0483, C0484, C0485, C0486, C0487, C0493, C0494, C0495, C0496, C0497, C0513, C0514, C0515, C0536, C0537, C0540, C0541, C0542, C0546, C0547, C0550, C0554, C0555, C0556, C0557, C0558, C0559, C0560, C0561, C0562, C0563, C0564, C0565, C0580, C0588, C0589, C0590, C0591, C0605, C0616, C0619, C0620, C0621, C0622, C0627, C0628, C0629, C0631, C0638, C0640, C0641, C0642, C0643, C0644, C0645, C0646, C0649, C0650, C0651, C0653, C0655, C0656, C0657, C0659, C0664, C0665, C0669, C0671, C0673, C0674, C0675, C0677, C0682, C0683, C0684, C0685, C0690, C0698, C0699, C0708, C0709, C0736, C0737, C0738, C0746, C0747, C0755, C0756, C0757, C0758, C0766, C0767, C0768, C0774, C0775, C0801, C0802, C0803, C0804, C0811, C0821, C0834, C0835, C0844, C0845, C0851, C0852, C0866, C0873, C0877, C0940, C0941, C0943, C0944, C1023, C1024, C1025, C1033, C1047, C1048, C1050, C1061, C1062, C3236, C3237, C3238, C3244</strong> <strong>C++4122</strong> </td> <td> </td> </tr> <tr> <td> <a> Klocwork </a> </td> <td> 2023.4 </td> <td> <strong>MISRA.FUNC.STATIC.REDECL</strong> </td> <td> </td> </tr> <tr> <td> <a> LDRA tool suite </a> </td> <td> 9.7.1 </td> <td> <strong>21 S, 145 S, 323 S, 345 S, 387 S, 404 S, 481 S, 580 S, 612 S, 615 S, 646 S</strong> </td> <td> </td> </tr> <tr> <td> <a> Parasoft C/C++test </a> </td> <td> 2023.1 </td> <td> <strong>CERT_C-MSC40-a</strong> </td> <td> An inline definition of a function with external linkage shall not contain definitions and uses of static objects </td> </tr> <tr> <td> <a> Polyspace Bug Finder </a> </td> <td> </td> <td> <a> CERT C: Rule MSC40-C </a> </td> <td> Checks for inline constraint not respected (rule partially covered) </td> </tr> <tr> <td> <a> RuleChecker </a> </td> <td> 23.04 </td> <td> <strong>alignas-extended</strong> <strong>assignment-to-non-modifiable-lvalue</strong> <strong>cast-pointer-void-arithmetic-implicit</strong> <strong>element-type-incomplete</strong> <strong>function-pointer-integer-cast-implicit</strong> <strong>function-return-type</strong> <strong>inappropriate-pointer-cast-implicit</strong> <strong>incompatible-function-pointer-conversion</strong> <strong>incompatible-object-pointer-conversion</strong> <strong>initializer-excess</strong> <strong>invalid-array-size</strong> <strong>non-constant-static-assert</strong> <strong>parameter-match-type</strong> <strong>pointer-integral-cast-implicit</strong> <strong>pointer-qualifier-cast-const-implicit</strong> <strong>pointer-qualifier-cast-volatile-implicit</strong> <strong>redeclaration</strong> <strong>return-empty</strong> <strong>return-non-empty</strong> <strong>static-assert</strong> <strong>type-compatibility</strong> <strong>type-compatibility-link</strong> <strong>type-specifier</strong> <strong>undeclared-parameter</strong> <strong>unnamed-parameter</strong> </td> <td> Partially checked </td> </tr> </tbody> </table>
193+
194+
195+
## Related Vulnerabilities
196+
197+
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+MSC40-C).
198+
199+
## Bibliography
200+
201+
<table> <tbody> <tr> <td> \[ <a> ISO/IEC 9899:2011 </a> \] </td> <td> 4, "Conformance" 5.1.1.3, "Diagnostics" 6.7.4, "Function Specifiers" </td> </tr> </tbody> </table>
202+
203+
204+
## Implementation notes
205+
206+
This query only considers the constraints related to inline extern functions.
207+
208+
## References
209+
210+
* CERT-C: [MSC40-C: Do not violate constraints](https://wiki.sei.cmu.edu/confluence/display/c)

‎c/cert/src/rules/MSC40-C/DoNotViolateInLineLinkageConstraints.ql

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
/**
2+
* @id c/cert/do-not-violate-in-line-linkage-constraints
3+
* @name MSC40-C: Do not violate inline linkage constraints
4+
* @description Inlined external functions are prohibited by the language standard from defining
5+
* modifiable static or thread storage objects, or referencing identifiers with
6+
* internal linkage.
7+
* @kind problem
8+
* @precision very-high
9+
* @problem.severity error
10+
* @tags external/cert/id/msc40-c
11+
* correctness
12+
* external/cert/obligation/rule
13+
*/
14+
15+
import cpp
16+
import codingstandards.c.cert
17+
import codingstandards.cpp.Linkage
18+
19+
/*
20+
* This is C specific, because in C++ all extern function definitions must be identical.
21+
* Only in C is it permitted for an extern function to be defined in multiple translation
22+
* units with different implementations, when using the inline keyword.
23+
*/
24+
25+
from Element accessOrDecl, Variable v, Function f, string message
26+
where
27+
not isExcluded(f, ContractsPackage::doNotViolateInLineLinkageConstraintsQuery()) and
28+
f.isInline() and
29+
hasExternalLinkage(f) and
30+
// Pre-emptively exclude compiler generated functions
31+
not f.isCompilerGenerated() and
32+
// This rule does not apply to C++, but exclude C++ specific cases anyway
33+
not f instanceof MemberFunction and
34+
not f.isFromUninstantiatedTemplate(_) and
35+
(
36+
// There exists a modifiable local variable which is static or thread local
37+
exists(LocalVariable lsv, string storageModifier |
38+
lsv.isStatic() and storageModifier = "Static"
39+
or
40+
lsv.isThreadLocal() and storageModifier = "Thread-local"
41+
|
42+
lsv.getFunction() = f and
43+
not lsv.isConst() and
44+
accessOrDecl = lsv and
45+
message = storageModifier + " local variable $@ declared" and
46+
v = lsv
47+
)
48+
or
49+
// References an identifier with internal linkage
50+
exists(GlobalOrNamespaceVariable gv |
51+
accessOrDecl = v.getAnAccess() and
52+
accessOrDecl.(VariableAccess).getEnclosingFunction() = f and
53+
hasInternalLinkage(v) and
54+
message = "Identifier $@ with internal linkage referenced" and
55+
v = gv
56+
)
57+
)
58+
select accessOrDecl, message + " in the extern inlined function $@.", v, v.getName(), f,
59+
f.getQualifiedName()

‎c/cert/test/rules/MSC40-C/DoNotViolateInLineLinkageConstraints.expected

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
| test.c:6:14:6:14 | i | Static local variable $@ declared in the extern inlined function $@. | test.c:6:14:6:14 | i | i | test.c:5:20:5:24 | test1 | test1 |
2+
| test.c:7:3:7:4 | g1 | Identifier $@ with internal linkage referenced in the extern inlined function $@. | test.c:1:12:1:13 | g1 | g1 | test.c:5:20:5:24 | test1 | test1 |
3+
| test.c:9:3:9:4 | g3 | Identifier $@ with internal linkage referenced in the extern inlined function $@. | test.c:3:11:3:12 | g3 | g3 | test.c:5:20:5:24 | test1 | test1 |
4+
| test.c:27:14:27:14 | i | Static local variable $@ declared in the extern inlined function $@. | test.c:27:14:27:14 | i | i | test.c:26:13:26:17 | test4 | test4 |
5+
| test.c:28:3:28:4 | g1 | Identifier $@ with internal linkage referenced in the extern inlined function $@. | test.c:1:12:1:13 | g1 | g1 | test.c:26:13:26:17 | test4 | test4 |
6+
| test.c:30:3:30:4 | g3 | Identifier $@ with internal linkage referenced in the extern inlined function $@. | test.c:3:11:3:12 | g3 | g3 | test.c:26:13:26:17 | test4 | test4 |

‎c/cert/test/rules/MSC40-C/DoNotViolateInLineLinkageConstraints.qlref

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/MSC40-C/DoNotViolateInLineLinkageConstraints.ql

‎c/cert/test/rules/MSC40-C/test.c

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
static int g1 = 0;
2+
extern int g2 = 1;
3+
const int g3 = 1; // defaults to internal linkage
4+
5+
extern inline void test1() {
6+
static int i = 0; // NON_COMPLIANT
7+
g1++; // NON_COMPLIANT
8+
g2++; // COMPLIANT
9+
g3; // NON_COMPLIANT
10+
}
11+
12+
extern void test2() {
13+
static int i = 0; // COMPLIANT
14+
g1++; // COMPLIANT
15+
g2++; // COMPLIANT
16+
g3; // COMPLIANT
17+
}
18+
19+
void test3() {
20+
static int i = 0; // COMPLIANT
21+
g1++; // COMPLIANT
22+
g2++; // COMPLIANT
23+
g3; // COMPLIANT
24+
}
25+
26+
inline void test4() {
27+
static int i = 0; // NON_COMPLIANT
28+
g1++; // NON_COMPLIANT
29+
g2++; // COMPLIANT
30+
g3; // NON_COMPLIANT
31+
}

‎c/common/test/rules/functionerroneousreturnvaluenottested/FunctionErroneousReturnValueNotTested.expected

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
| test.c:16:3:16:8 | call to remove | Return value from remove is not tested for errors. |

‎c/common/test/rules/functionerroneousreturnvaluenottested/FunctionErroneousReturnValueNotTested.ql

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
// GENERATED FILE - DO NOT MODIFY
2+
import codingstandards.cpp.rules.functionerroneousreturnvaluenottested.FunctionErroneousReturnValueNotTested
3+
4+
class TestFileQuery extends FunctionErroneousReturnValueNotTestedSharedQuery, TestQuery { }

‎cpp/autosar/test/rules/M0-3-2/test.cpp renamed to ‎c/common/test/rules/functionerroneousreturnvaluenottested/test.c

File renamed without changes.

‎c/misra/src/rules/DIR-4-11/CheckMathLibraryFunctionParameters.ql

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/**
2+
* @id c/misra/check-math-library-function-parameters
3+
* @name DIR-4-11: The validity of values passed to `math.h` library functions shall be checked
4+
* @description Range, domain or pole errors in math functions may return unexpected values, trigger
5+
* floating-point exceptions or set unexpected error modes.
6+
* @kind problem
7+
* @precision high
8+
* @problem.severity error
9+
* @tags external/misra/id/dir-4-11
10+
* correctness
11+
* external/misra/c/2012/third-edition-first-revision
12+
* external/misra/obligation/required
13+
*/
14+
15+
import cpp
16+
import codingstandards.c.misra
17+
import codingstandards.cpp.rules.uncheckedrangedomainpoleerrors.UncheckedRangeDomainPoleErrors
18+
19+
class CheckMathLibraryFunctionParametersQuery extends UncheckedRangeDomainPoleErrorsSharedQuery {
20+
CheckMathLibraryFunctionParametersQuery() {
21+
this = ContractsPackage::checkMathLibraryFunctionParametersQuery()
22+
}
23+
}

0 commit comments

Comments
 (0)