Skip to content

Commit 07a3b16

Browse files
lcarteylcartey
authored
Merge pull request #188 from github/lcartey/essential-types
Implement `EssentialTypes`
2 parents dcd22fd + 0b984b2 commit 07a3b16

File tree

56 files changed

+3370
-11
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+3370
-11
lines changed

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

Lines changed: 376 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,376 @@
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 essentialType or a typedef of an essentialType.
78+
*/
79+
EssentialTypeCategory getEssentialTypeCategory(Type type) {
80+
exists(Type essentialType |
81+
if type instanceof MisraBoolType
82+
then essentialType = type
83+
else
84+
// If not a bool type, resolve the typedefs to determine the actual type
85+
essentialType = type.getUnspecifiedType()
86+
|
87+
result = EssentiallyBooleanType() and essentialType instanceof MisraBoolType
88+
or
89+
result = EssentiallyCharacterType() and essentialType instanceof PlainCharType
90+
or
91+
result = EssentiallySignedType() and
92+
essentialType.(IntegralType).isSigned() and
93+
not essentialType instanceof PlainCharType
94+
or
95+
result = EssentiallyUnsignedType() and
96+
essentialType.(IntegralType).isUnsigned() and
97+
not essentialType instanceof PlainCharType
98+
or
99+
result = EssentiallyEnumType() and
100+
essentialType instanceof Enum and
101+
not essentialType instanceof MisraBoolType
102+
or
103+
result = EssentiallyFloatingType() and
104+
essentialType instanceof FloatingPointType
105+
)
106+
}
107+
108+
/**
109+
* Gets the essential type of the given expression `e`, considering any explicit conversions.
110+
*/
111+
Type getEssentialType(Expr e) {
112+
if e.hasExplicitConversion()
113+
then
114+
if e.getConversion() instanceof ParenthesisExpr
115+
then
116+
if e.getConversion().(ParenthesisExpr).hasExplicitConversion()
117+
then result = e.getConversion().(ParenthesisExpr).getConversion().getType()
118+
else result = e.getConversion().(ParenthesisExpr).getExpr().(EssentialExpr).getEssentialType()
119+
else result = e.getConversion().getType()
120+
else result = e.(EssentialExpr).getEssentialType()
121+
}
122+
123+
Type getEssentialTypeBeforeConversions(Expr e) { result = e.(EssentialExpr).getEssentialType() }
124+
125+
class EssentialExpr extends Expr {
126+
Type getEssentialType() { result = this.getType() }
127+
128+
Type getStandardType() { result = this.getType() }
129+
}
130+
131+
class EssentialCommaExpr extends EssentialExpr, CommaExpr {
132+
override Type getEssentialType() { result = getEssentialType(getRightOperand()) }
133+
}
134+
135+
class EssentialRelationalOperationExpr extends EssentialExpr, RelationalOperation {
136+
override Type getEssentialType() { result instanceof BoolType }
137+
}
138+
139+
class EssentialBinaryLogicalOperationExpr extends EssentialExpr, BinaryLogicalOperation {
140+
override Type getEssentialType() { result instanceof BoolType }
141+
}
142+
143+
class EssentialEqualityOperationExpr extends EssentialExpr, EqualityOperation {
144+
override Type getEssentialType() { result instanceof BoolType }
145+
}
146+
147+
class EssentialBinaryBitwiseOperationExpr extends EssentialExpr, BinaryBitwiseOperation {
148+
EssentialBinaryBitwiseOperationExpr() {
149+
this instanceof LShiftExpr or
150+
this instanceof RShiftExpr
151+
}
152+
153+
override Type getEssentialType() {
154+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
155+
operandEssentialType = getEssentialType(getLeftOperand()) and
156+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
157+
|
158+
if operandEssentialTypeCategory instanceof EssentiallyUnsignedType
159+
then
160+
if exists(this.getValue())
161+
then result = utlr(this) // If constant and essentially unsigned us the utlr
162+
else result = operandEssentialType
163+
else result = this.getStandardType()
164+
)
165+
}
166+
}
167+
168+
class EssentialBitwiseComplementExpr extends EssentialExpr, ComplementExpr {
169+
override Type getEssentialType() {
170+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
171+
operandEssentialType = getEssentialType(getOperand()) and
172+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
173+
|
174+
if operandEssentialTypeCategory instanceof EssentiallyUnsignedType
175+
then
176+
if exists(this.getValue())
177+
then result = utlr(this) // If constant and essentially unsigned us the utlr
178+
else result = operandEssentialType
179+
else result = this.getStandardType()
180+
)
181+
}
182+
}
183+
184+
class EssentialUnaryPlusExpr extends EssentialExpr, UnaryPlusExpr {
185+
override Type getEssentialType() {
186+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
187+
operandEssentialType = getEssentialType(getOperand()) and
188+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
189+
|
190+
if
191+
operandEssentialTypeCategory =
192+
[EssentiallyUnsignedType().(TEssentialTypeCategory), EssentiallySignedType()]
193+
then result = operandEssentialType
194+
else result = getStandardType()
195+
)
196+
}
197+
}
198+
199+
class EssentialUnaryMinusExpr extends EssentialExpr, UnaryMinusExpr {
200+
override Type getEssentialType() {
201+
exists(Type operandEssentialType, EssentialTypeCategory operandEssentialTypeCategory |
202+
operandEssentialType = getEssentialType(getOperand()) and
203+
operandEssentialTypeCategory = getEssentialTypeCategory(operandEssentialType)
204+
|
205+
if operandEssentialTypeCategory = EssentiallySignedType()
206+
then if exists(this.getValue()) then result = stlr(this) else result = operandEssentialType
207+
else result = getStandardType()
208+
)
209+
}
210+
}
211+
212+
class EssentialConditionalExpr extends EssentialExpr, ConditionalExpr {
213+
override Type getEssentialType() {
214+
exists(Type thenEssentialType, Type elseEssentialType |
215+
thenEssentialType = getEssentialType(getThen()) and
216+
elseEssentialType = getEssentialType(getElse())
217+
|
218+
if thenEssentialType = elseEssentialType
219+
then result = thenEssentialType
220+
else
221+
if
222+
getEssentialTypeCategory(thenEssentialType) = EssentiallySignedType() and
223+
getEssentialTypeCategory(elseEssentialType) = EssentiallySignedType()
224+
then
225+
if thenEssentialType.getSize() > elseEssentialType.getSize()
226+
then result = thenEssentialType
227+
else result = elseEssentialType
228+
else
229+
if
230+
getEssentialTypeCategory(thenEssentialType) = EssentiallyUnsignedType() and
231+
getEssentialTypeCategory(elseEssentialType) = EssentiallyUnsignedType()
232+
then
233+
if thenEssentialType.getSize() > elseEssentialType.getSize()
234+
then result = thenEssentialType
235+
else result = elseEssentialType
236+
else result = this.getStandardType()
237+
)
238+
}
239+
}
240+
241+
class EssentialBinaryArithmeticExpr extends EssentialExpr, BinaryArithmeticOperation {
242+
EssentialBinaryArithmeticExpr() {
243+
// GNU C extension has min/max which we can ignore
244+
not this instanceof MinExpr and
245+
not this instanceof MaxExpr
246+
}
247+
248+
override Type getEssentialType() {
249+
exists(
250+
Type leftEssentialType, Type rightEssentialType,
251+
EssentialTypeCategory leftEssentialTypeCategory,
252+
EssentialTypeCategory rightEssentialTypeCategory
253+
|
254+
leftEssentialType = getEssentialType(getLeftOperand()) and
255+
rightEssentialType = getEssentialType(getRightOperand()) and
256+
leftEssentialTypeCategory = getEssentialTypeCategory(leftEssentialType) and
257+
rightEssentialTypeCategory = getEssentialTypeCategory(rightEssentialType)
258+
|
259+
if
260+
leftEssentialTypeCategory = EssentiallySignedType() and
261+
rightEssentialTypeCategory = EssentiallySignedType()
262+
then
263+
if exists(getValue())
264+
then result = stlr(this)
265+
else (
266+
if leftEssentialType.getSize() > rightEssentialType.getSize()
267+
then result = leftEssentialType
268+
else result = rightEssentialType
269+
)
270+
else
271+
if
272+
leftEssentialTypeCategory = EssentiallyUnsignedType() and
273+
rightEssentialTypeCategory = EssentiallyUnsignedType()
274+
then
275+
if exists(getValue())
276+
then result = utlr(this)
277+
else (
278+
if leftEssentialType.getSize() > rightEssentialType.getSize()
279+
then result = leftEssentialType
280+
else result = rightEssentialType
281+
)
282+
else
283+
if
284+
this instanceof AddExpr and
285+
(
286+
leftEssentialTypeCategory = EssentiallyCharacterType()
287+
or
288+
rightEssentialTypeCategory = EssentiallyCharacterType()
289+
) and
290+
(
291+
leftEssentialTypeCategory =
292+
[EssentiallySignedType(), EssentiallyUnsignedType().(TEssentialTypeCategory)]
293+
or
294+
rightEssentialTypeCategory =
295+
[EssentiallySignedType(), EssentiallyUnsignedType().(TEssentialTypeCategory)]
296+
)
297+
or
298+
this instanceof SubExpr and
299+
leftEssentialTypeCategory = EssentiallyCharacterType() and
300+
rightEssentialTypeCategory =
301+
[EssentiallySignedType(), EssentiallyUnsignedType().(TEssentialTypeCategory)]
302+
then result instanceof PlainCharType
303+
else result = this.getStandardType()
304+
)
305+
}
306+
}
307+
308+
class EssentialEnumConstantAccess extends EssentialExpr, EnumConstantAccess {
309+
override Type getEssentialType() { result = getTarget().getDeclaringEnum() }
310+
}
311+
312+
class EssentialLiteral extends EssentialExpr, Literal {
313+
override Type getEssentialType() {
314+
if this instanceof BooleanLiteral
315+
then result instanceof MisraBoolType
316+
else (
317+
if this.(CharLiteral).getCharacter().length() = 1
318+
then result instanceof PlainCharType
319+
else (
320+
getStandardType().(IntegralType).isSigned() and
321+
result = stlr(this)
322+
or
323+
not getStandardType().(IntegralType).isSigned() and
324+
result = utlr(this)
325+
)
326+
)
327+
}
328+
}
329+
330+
/**
331+
* Holds if `rValue` is assigned to an object of type `lValueEssentialType`.
332+
*
333+
* Assignment is according to "Assignment" in Appendix J of MISRA C 2012, with the inclusion of a
334+
* special case for switch statements as specified for Rule 10.3 and Rule 10.6.
335+
*/
336+
predicate isAssignmentToEssentialType(Type lValueEssentialType, Expr rValue) {
337+
// Special case for Rule 10.3/ Rule 10.6.
338+
exists(SwitchCase sc |
339+
lValueEssentialType = sc.getSwitchStmt().getControllingExpr().getType() and
340+
rValue = sc.getExpr()
341+
)
342+
or
343+
exists(Assignment a |
344+
lValueEssentialType = a.getLValue().getType() and
345+
rValue = a.getRValue()
346+
)
347+
or
348+
exists(FunctionCall fc, int i |
349+
lValueEssentialType = fc.getTarget().getParameter(i).getType() and
350+
rValue = fc.getArgument(i)
351+
)
352+
or
353+
exists(Function f, ReturnStmt rs |
354+
lValueEssentialType = f.getType() and
355+
rs.getEnclosingFunction() = f and
356+
rValue = rs.getExpr()
357+
)
358+
or
359+
// Initializing a non-aggregate type
360+
exists(Initializer i |
361+
lValueEssentialType = i.getDeclaration().(Variable).getType() and
362+
rValue = i.getExpr()
363+
)
364+
or
365+
// Initializing an array
366+
exists(ArrayAggregateLiteral aal |
367+
lValueEssentialType = aal.getElementType() and
368+
rValue = aal.getElementExpr(_)
369+
)
370+
or
371+
// Initializing a struct or union
372+
exists(ClassAggregateLiteral cal, Field field |
373+
lValueEssentialType = field.getType() and
374+
rValue = cal.getFieldExpr(field)
375+
)
376+
}

0 commit comments

Comments
 (0)