Skip to content

Commit 79e44e3

Browse files
lcarteylcartey
committed
EssentialTypes: Add essential types library
This module calculates and reports the essential type of each given expression in the program, as defined in the MISRA C:2012 standard. The essential type for an expression is calculated based on the AST type of the expression. Where it differs from the standard type, the calculation is overridden to implement the MISRA definition. Various utility methods related to essential types are included.
1 parent 8423344 commit 79e44e3

File tree

1 file changed

+366
-0
lines changed

1 file changed

+366
-0
lines changed

‎c/misra/src/codingstandards/c/misra/EssentialTypes.qll

Lines changed: 366 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,366 @@
1+
/**
2+
* A module for identifying essential types as defined by MISRA C 2012.
3+
*/
4+
5+
import codingstandards.c.misra
6+
import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
7+
import MisraExpressions
8+
9+
newtype TEssentialTypeCategory =
10+
EssentiallyBooleanType() or
11+
EssentiallyCharacterType() or
12+
EssentiallyEnumType() or
13+
EssentiallySignedType() or
14+
EssentiallyUnsignedType() or
15+
EssentiallyFloatingType()
16+
17+
/** An essential type category, as specified by Appendix D.1. */
18+
class EssentialTypeCategory extends TEssentialTypeCategory {
19+
string toString() {
20+
this = EssentiallyBooleanType() and result = "essentially Boolean type"
21+
or
22+
this = EssentiallyCharacterType() and result = "essentially Character type"
23+
or
24+
this = EssentiallyEnumType() and result = "essentially Enum Type"
25+
or
26+
this = EssentiallySignedType() and result = "essentially Signed type"
27+
or
28+
this = EssentiallyUnsignedType() and result = "essentially Unsigned type"
29+
or
30+
this = EssentiallyFloatingType() and result = "essentially Floating type"
31+
}
32+
}
33+
34+
/**
35+
* Gets the unsigned type of lowest rank that can represent the value of the given expression,
36+
* assuming that the expression is essentially unsigned.
37+
*/
38+
private IntegralType utlr(Expr const) {
39+
getEssentialTypeCategory(const.getType()) = EssentiallyUnsignedType() and
40+
getEssentialTypeCategory(result) = EssentiallyUnsignedType() and
41+
exists(float c | c = const.getValue().toFloat() |
42+
// As with range analysis, we assume two's complement representation
43+
typeLowerBound(result) <= c and
44+
typeUpperBound(result) >= c and
45+
forall(IntegralType it |
46+
getEssentialTypeCategory(it) = EssentiallyUnsignedType() and
47+
typeLowerBound(it) <= c and
48+
typeUpperBound(it) >= c
49+
|
50+
result.getSize() <= it.getSize()
51+
)
52+
)
53+
}
54+
55+
/**
56+
* Gets the signed type of lowest rank that can represent the value of the given expression,
57+
* assuming that the expression is essentially signed.
58+
*/
59+
private IntegralType stlr(Expr const) {
60+
getEssentialTypeCategory(const.getType()) = EssentiallySignedType() and
61+
getEssentialTypeCategory(result) = EssentiallySignedType() and
62+
exists(float c | c = const.getValue().toFloat() |
63+
// As with range analysis, we assume two's complement representation
64+
typeLowerBound(result) <= c and
65+
typeUpperBound(result) >= c and
66+
forall(IntegralType it |
67+
getEssentialTypeCategory(it) = EssentiallySignedType() and
68+
typeLowerBound(it) <= c and
69+
typeUpperBound(it) >= c
70+
|
71+
result.getSize() <= it.getSize()
72+
)
73+
)
74+
}
75+
76+
/**
77+
* Define the essential type category for an IntegralOrEnumType.
78+
*/
79+
EssentialTypeCategory getEssentialTypeCategory(Type at) {
80+
result = EssentiallyBooleanType() and at instanceof MisraBoolType
81+
or
82+
result = EssentiallyCharacterType() and at instanceof PlainCharType
83+
or
84+
result = EssentiallySignedType() and
85+
at.(IntegralType).isSigned() and
86+
not at instanceof PlainCharType
87+
or
88+
result = EssentiallyUnsignedType() and
89+
at.(IntegralType).isUnsigned() and
90+
not at instanceof PlainCharType
91+
or
92+
result = EssentiallyEnumType() and at instanceof Enum and not at instanceof MisraBoolType
93+
or
94+
result = EssentiallyFloatingType() and
95+
at instanceof FloatingPointType
96+
}
97+
98+
/**
99+
* Gets the essential type of the given expression `e`, considering any explicit conversions.
100+
*/
101+
Type getEssentialType(Expr e) {
102+
if e.hasExplicitConversion()
103+
then
104+
if e.getConversion() instanceof ParenthesisExpr
105+
then
106+
if e.getConversion().(ParenthesisExpr).hasExplicitConversion()
107+
then result = e.getConversion().(ParenthesisExpr).getConversion().getType()
108+
else result = e.getConversion().(ParenthesisExpr).getExpr().(EssentialExpr).getEssentialType()
109+
else result = e.getConversion().getType()
110+
else result = e.(EssentialExpr).getEssentialType()
111+
}
112+
113+
Type getEssentialTypeBeforeConversions(Expr e) { result = e.(EssentialExpr).getEssentialType() }
114+
115+
class EssentialExpr extends Expr {
116+
Type getEssentialType() { result = this.getType() }
117+
118+
Type getStandardType() { result = this.getType() }
119+
}
120+
121+
class EssentialCommaExpr extends EssentialExpr, CommaExpr {
122+
override Type getEssentialType() { result = getEssentialType(getRightOperand()) }
123+
}
124+
125+
class EssentialRelationalOperationExpr extends EssentialExpr, RelationalOperation {
126+
override Type getEssentialType() { result instanceof BoolType }
127+
}
128+
129+
class EssentialBinaryLogicalOperationExpr extends EssentialExpr, BinaryLogicalOperation {
130+
override Type getEssentialType() { result instanceof BoolType }
131+
}
132+
133+
class EssentialEqualityOperationExpr extends EssentialExpr, EqualityOperation {
134+
override Type getEssentialType() { result instanceof BoolType }
135+
}
136+
137+
class EssentialBinaryBitwiseOperationExpr extends EssentialExpr, BinaryBitwiseOperation {
138+
EssentialBinaryBitwiseOperationExpr() {
139+
this instanceof LShiftExpr or
140+
this instanceof RShiftExpr
141+
}
142+
143+
override Type getEssentialType() {
144+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
145+
operandEssentialType = getEssentialType(getLeftOperand()) and
146+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
147+
|
148+
if operandEssentialTypeCategory instanceof EssentiallyUnsignedType
149+
then
150+
if exists(this.getValue())
151+
then result = utlr(this) // If constant and essentially unsigned us the utlr
152+
else result = operandEssentialType
153+
else result = this.getStandardType()
154+
)
155+
}
156+
}
157+
158+
class EssentialBitwiseComplementExpr extends EssentialExpr, ComplementExpr {
159+
override Type getEssentialType() {
160+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
161+
operandEssentialType = getEssentialType(getOperand()) and
162+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
163+
|
164+
if operandEssentialTypeCategory instanceof EssentiallyUnsignedType
165+
then
166+
if exists(this.getValue())
167+
then result = utlr(this) // If constant and essentially unsigned us the utlr
168+
else result = operandEssentialType
169+
else result = this.getStandardType()
170+
)
171+
}
172+
}
173+
174+
class EssentialUnaryPlusExpr extends EssentialExpr, UnaryPlusExpr {
175+
override Type getEssentialType() {
176+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
177+
operandEssentialType = getEssentialType(getOperand()) and
178+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
179+
|
180+
if
181+
operandEssentialTypeCategory =
182+
[EssentiallyUnsignedType().(TEssentialTypeCategory), EssentiallySignedType()]
183+
then result = operandEssentialType
184+
else result = getStandardType()
185+
)
186+
}
187+
}
188+
189+
class EssentialUnaryMinusExpr extends EssentialExpr, UnaryMinusExpr {
190+
override Type getEssentialType() {
191+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
192+
operandEssentialType = getEssentialType(getOperand()) and
193+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
194+
|
195+
if operandEssentialTypeCategory = EssentiallySignedType()
196+
then if exists(this.getValue()) then result = stlr(this) else result = operandEssentialType
197+
else result = getStandardType()
198+
)
199+
}
200+
}
201+
202+
class EssentialConditionalExpr extends EssentialExpr, ConditionalExpr {
203+
override Type getEssentialType() {
204+
exists(Type thenEssentialType, Type elseEssentialType |
205+
thenEssentialType = getEssentialType(getThen()) and
206+
elseEssentialType = getEssentialType(getElse())
207+
|
208+
if thenEssentialType = elseEssentialType
209+
then result = thenEssentialType
210+
else
211+
if
212+
getEssentialTypeCategory(thenEssentialType) = EssentiallySignedType() and
213+
getEssentialTypeCategory(elseEssentialType) = EssentiallySignedType()
214+
then
215+
if thenEssentialType.getSize() > elseEssentialType.getSize()
216+
then result = thenEssentialType
217+
else result = elseEssentialType
218+
else
219+
if
220+
getEssentialTypeCategory(thenEssentialType) = EssentiallyUnsignedType() and
221+
getEssentialTypeCategory(elseEssentialType) = EssentiallyUnsignedType()
222+
then
223+
if thenEssentialType.getSize() > elseEssentialType.getSize()
224+
then result = thenEssentialType
225+
else result = elseEssentialType
226+
else result = this.getStandardType()
227+
)
228+
}
229+
}
230+
231+
class EssentialBinaryArithmeticExpr extends EssentialExpr, BinaryArithmeticOperation {
232+
EssentialBinaryArithmeticExpr() {
233+
// GNU C extension has min/max which we can ignore
234+
not this instanceof MinExpr and
235+
not this instanceof MaxExpr
236+
}
237+
238+
override Type getEssentialType() {
239+
exists(
240+
Type leftEssentialType, Type rightEssentialType,
241+
EssentialTypeCategory leftEssentialTypeCategory,
242+
EssentialTypeCategory rightEssentialTypeCategory
243+
|
244+
leftEssentialType = getEssentialType(getLeftOperand()) and
245+
rightEssentialType = getEssentialType(getRightOperand()) and
246+
leftEssentialTypeCategory = getEssentialTypeCategory(leftEssentialType) and
247+
rightEssentialTypeCategory = getEssentialTypeCategory(rightEssentialType)
248+
|
249+
if
250+
leftEssentialTypeCategory = EssentiallySignedType() and
251+
rightEssentialTypeCategory = EssentiallySignedType()
252+
then
253+
if exists(getValue())
254+
then result = stlr(this)
255+
else (
256+
if leftEssentialType.getSize() > rightEssentialType.getSize()
257+
then result = leftEssentialType
258+
else result = rightEssentialType
259+
)
260+
else
261+
if
262+
leftEssentialTypeCategory = EssentiallyUnsignedType() and
263+
rightEssentialTypeCategory = EssentiallyUnsignedType()
264+
then
265+
if exists(getValue())
266+
then result = utlr(this)
267+
else (
268+
if leftEssentialType.getSize() > rightEssentialType.getSize()
269+
then result = leftEssentialType
270+
else result = rightEssentialType
271+
)
272+
else
273+
if
274+
this instanceof AddExpr and
275+
(
276+
leftEssentialTypeCategory = EssentiallyCharacterType()
277+
or
278+
rightEssentialTypeCategory = EssentiallyCharacterType()
279+
) and
280+
(
281+
leftEssentialTypeCategory =
282+
[EssentiallySignedType(), EssentiallyUnsignedType().(TEssentialTypeCategory)]
283+
or
284+
rightEssentialTypeCategory =
285+
[EssentiallySignedType(), EssentiallyUnsignedType().(TEssentialTypeCategory)]
286+
)
287+
or
288+
this instanceof SubExpr and
289+
leftEssentialTypeCategory = EssentiallyCharacterType() and
290+
rightEssentialTypeCategory =
291+
[EssentiallySignedType(), EssentiallyUnsignedType().(TEssentialTypeCategory)]
292+
then result instanceof PlainCharType
293+
else result = this.getStandardType()
294+
)
295+
}
296+
}
297+
298+
class EssentialEnumConstantAccess extends EssentialExpr, EnumConstantAccess {
299+
override Type getEssentialType() { result = getTarget().getDeclaringEnum() }
300+
}
301+
302+
class EssentialLiteral extends EssentialExpr, Literal {
303+
override Type getEssentialType() {
304+
if this instanceof BooleanLiteral
305+
then result instanceof MisraBoolType
306+
else (
307+
if this.(CharLiteral).getCharacter().length() = 1
308+
then result instanceof PlainCharType
309+
else (
310+
getStandardType().(IntegralType).isSigned() and
311+
result = stlr(this)
312+
or
313+
not getStandardType().(IntegralType).isSigned() and
314+
result = utlr(this)
315+
)
316+
)
317+
}
318+
}
319+
320+
/**
321+
* Holds if `rValue` is assigned to an object of type `lValueEssentialType`.
322+
*
323+
* Assignment is according to "Assignment" in Appendix J of MISRA C 2012, with the inclusion of a
324+
* special case for switch statements as specified for Rule 10.3 and Rule 10.6.
325+
*/
326+
predicate isAssignmentToEssentialType(Type lValueEssentialType, Expr rValue) {
327+
// Special case for Rule 10.3/ Rule 10.6.
328+
exists(SwitchCase sc |
329+
lValueEssentialType = sc.getSwitchStmt().getControllingExpr().getType() and
330+
rValue = sc.getExpr()
331+
)
332+
or
333+
exists(Assignment a |
334+
lValueEssentialType = a.getLValue().getType() and
335+
rValue = a.getRValue()
336+
)
337+
or
338+
exists(FunctionCall fc, int i |
339+
lValueEssentialType = fc.getTarget().getParameter(i).getType() and
340+
rValue = fc.getArgument(i)
341+
)
342+
or
343+
exists(Function f, ReturnStmt rs |
344+
lValueEssentialType = f.getType() and
345+
rs.getEnclosingFunction() = f and
346+
rValue = rs.getExpr()
347+
)
348+
or
349+
// Initializing a non-aggregate type
350+
exists(Initializer i |
351+
lValueEssentialType = i.getDeclaration().(Variable).getType() and
352+
rValue = i.getExpr()
353+
)
354+
or
355+
// Initializing an array
356+
exists(ArrayAggregateLiteral aal |
357+
lValueEssentialType = aal.getElementType() and
358+
rValue = aal.getElementExpr(_)
359+
)
360+
or
361+
// Initializing a struct or union
362+
exists(ClassAggregateLiteral cal, Field field |
363+
lValueEssentialType = field.getType() and
364+
rValue = cal.getFieldExpr(field)
365+
)
366+
}

0 commit comments

Comments
 (0)