clang 22.0.0git
SMTConv.h
Go to the documentation of this file.
1//== SMTConv.h --------------------------------------------------*- C++ -*--==//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// This file defines a set of functions to create SMT expressions.
10//
11//===----------------------------------------------------------------------===//
12
13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
15
16#include "clang/AST/Expr.h"
19#include "llvm/Support/SMTAPI.h"
20
21#include <algorithm>
22
23namespace clang {
24namespace ento {
25
26class SMTConv {
27public:
28 // Returns an appropriate sort, given a QualType and it's bit width.
29 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
30 const QualType &Ty, unsigned BitWidth) {
31 if (Ty->isBooleanType())
32 return Solver->getBoolSort();
33
34 if (Ty->isRealFloatingType())
35 return Solver->getFloatSort(BitWidth);
36
37 return Solver->getBitvectorSort(BitWidth);
38 }
39
40 /// Constructs an SMTSolverRef from an unary operator.
41 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
42 const UnaryOperator::Opcode Op,
43 const llvm::SMTExprRef &Exp) {
44 switch (Op) {
45 case UO_Minus:
46 return Solver->mkBVNeg(Exp);
47
48 case UO_Not:
49 return Solver->mkBVNot(Exp);
50
51 case UO_LNot:
52 return Solver->mkNot(Exp);
53
54 default:;
55 }
56 llvm_unreachable("Unimplemented opcode");
57 }
58
59 /// Constructs an SMTSolverRef from a floating-point unary operator.
60 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
61 const UnaryOperator::Opcode Op,
62 const llvm::SMTExprRef &Exp) {
63 switch (Op) {
64 case UO_Minus:
65 return Solver->mkFPNeg(Exp);
66
67 case UO_LNot:
68 return fromUnOp(Solver, Op, Exp);
69
70 default:;
71 }
72 llvm_unreachable("Unimplemented opcode");
73 }
74
75 /// Construct an SMTSolverRef from a n-ary binary operator.
76 static inline llvm::SMTExprRef
77 fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op,
78 const std::vector<llvm::SMTExprRef> &ASTs) {
79 assert(!ASTs.empty());
80
81 if (Op != BO_LAnd && Op != BO_LOr)
82 llvm_unreachable("Unimplemented opcode");
83
84 llvm::SMTExprRef res = ASTs.front();
85 for (std::size_t i = 1; i < ASTs.size(); ++i)
86 res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
87 : Solver->mkOr(res, ASTs[i]);
88 return res;
89 }
90
91 /// Construct an SMTSolverRef from a binary operator.
92 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,
93 const llvm::SMTExprRef &LHS,
95 const llvm::SMTExprRef &RHS,
96 bool isSigned) {
97 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
98 "AST's must have the same sort!");
99
100 switch (Op) {
101 // Multiplicative operators
102 case BO_Mul:
103 return Solver->mkBVMul(LHS, RHS);
104
105 case BO_Div:
106 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
107
108 case BO_Rem:
109 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
110
111 // Additive operators
112 case BO_Add:
113 return Solver->mkBVAdd(LHS, RHS);
114
115 case BO_Sub:
116 return Solver->mkBVSub(LHS, RHS);
117
118 // Bitwise shift operators
119 case BO_Shl:
120 return Solver->mkBVShl(LHS, RHS);
121
122 case BO_Shr:
123 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
124
125 // Relational operators
126 case BO_LT:
127 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
128
129 case BO_GT:
130 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
131
132 case BO_LE:
133 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
134
135 case BO_GE:
136 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
137
138 // Equality operators
139 case BO_EQ:
140 return Solver->mkEqual(LHS, RHS);
141
142 case BO_NE:
143 return fromUnOp(Solver, UO_LNot,
144 fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
145
146 // Bitwise operators
147 case BO_And:
148 return Solver->mkBVAnd(LHS, RHS);
149
150 case BO_Xor:
151 return Solver->mkBVXor(LHS, RHS);
152
153 case BO_Or:
154 return Solver->mkBVOr(LHS, RHS);
155
156 // Logical operators
157 case BO_LAnd:
158 return Solver->mkAnd(LHS, RHS);
159
160 case BO_LOr:
161 return Solver->mkOr(LHS, RHS);
162
163 default:;
164 }
165 llvm_unreachable("Unimplemented opcode");
166 }
167
168 /// Construct an SMTSolverRef from a special floating-point binary
169 /// operator.
170 static inline llvm::SMTExprRef
171 fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
172 const BinaryOperator::Opcode Op,
173 const llvm::APFloat::fltCategory &RHS) {
174 switch (Op) {
175 // Equality operators
176 case BO_EQ:
177 switch (RHS) {
178 case llvm::APFloat::fcInfinity:
179 return Solver->mkFPIsInfinite(LHS);
180
181 case llvm::APFloat::fcNaN:
182 return Solver->mkFPIsNaN(LHS);
183
184 case llvm::APFloat::fcNormal:
185 return Solver->mkFPIsNormal(LHS);
186
187 case llvm::APFloat::fcZero:
188 return Solver->mkFPIsZero(LHS);
189 }
190 break;
191
192 case BO_NE:
193 return fromFloatUnOp(Solver, UO_LNot,
194 fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
195
196 default:;
197 }
198
199 llvm_unreachable("Unimplemented opcode");
200 }
201
202 /// Construct an SMTSolverRef from a floating-point binary operator.
203 static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,
204 const llvm::SMTExprRef &LHS,
205 const BinaryOperator::Opcode Op,
206 const llvm::SMTExprRef &RHS) {
207 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
208 "AST's must have the same sort!");
209
210 switch (Op) {
211 // Multiplicative operators
212 case BO_Mul:
213 return Solver->mkFPMul(LHS, RHS);
214
215 case BO_Div:
216 return Solver->mkFPDiv(LHS, RHS);
217
218 case BO_Rem:
219 return Solver->mkFPRem(LHS, RHS);
220
221 // Additive operators
222 case BO_Add:
223 return Solver->mkFPAdd(LHS, RHS);
224
225 case BO_Sub:
226 return Solver->mkFPSub(LHS, RHS);
227
228 // Relational operators
229 case BO_LT:
230 return Solver->mkFPLt(LHS, RHS);
231
232 case BO_GT:
233 return Solver->mkFPGt(LHS, RHS);
234
235 case BO_LE:
236 return Solver->mkFPLe(LHS, RHS);
237
238 case BO_GE:
239 return Solver->mkFPGe(LHS, RHS);
240
241 // Equality operators
242 case BO_EQ:
243 return Solver->mkFPEqual(LHS, RHS);
244
245 case BO_NE:
246 return fromFloatUnOp(Solver, UO_LNot,
247 fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
248
249 // Logical operators
250 case BO_LAnd:
251 case BO_LOr:
252 return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
253
254 default:;
255 }
256
257 llvm_unreachable("Unimplemented opcode");
258 }
259
260 /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
261 /// and their bit widths.
262 static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,
263 const llvm::SMTExprRef &Exp,
264 QualType ToTy, uint64_t ToBitWidth,
265 QualType FromTy,
266 uint64_t FromBitWidth) {
267 if ((FromTy->isIntegralOrEnumerationType() &&
269 (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
270 (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
271 (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
272
273 if (FromTy->isBooleanType()) {
274 assert(ToBitWidth > 0 && "BitWidth must be positive!");
275 return Solver->mkIte(
276 Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
277 Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
278 }
279
280 if (ToBitWidth > FromBitWidth)
281 return FromTy->isSignedIntegerOrEnumerationType()
282 ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
283 : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
284
285 if (ToBitWidth < FromBitWidth)
286 return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
287
288 // Both are bitvectors with the same width, ignore the type cast
289 return Exp;
290 }
291
292 if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
293 if (ToBitWidth != FromBitWidth)
294 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
295
296 return Exp;
297 }
298
299 if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
300 llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
301 return FromTy->isSignedIntegerOrEnumerationType()
302 ? Solver->mkSBVtoFP(Exp, Sort)
303 : Solver->mkUBVtoFP(Exp, Sort);
304 }
305
306 if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
308 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
309 : Solver->mkFPtoUBV(Exp, ToBitWidth);
310
311 llvm_unreachable("Unsupported explicit type cast!");
312 }
313
314 // Callback function for doCast parameter on APSInt type.
315 static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
316 const llvm::APSInt &V, QualType ToTy,
317 uint64_t ToWidth, QualType FromTy,
318 uint64_t FromWidth) {
319 APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
320 return TargetType.convert(V);
321 }
322
323 /// Construct an SMTSolverRef from a SymbolData.
324 static inline llvm::SMTExprRef
325 fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
326 const SymbolID ID = Sym->getSymbolID();
327 const QualType Ty = Sym->getType();
328 const uint64_t BitWidth = Ctx.getTypeSize(Ty);
329
331 llvm::raw_svector_ostream OS(Str);
332 OS << Sym->getKindStr() << ID;
333 return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
334 }
335
336 // Wrapper to generate SMTSolverRef from SymbolCast data.
337 static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
338 ASTContext &Ctx,
339 const llvm::SMTExprRef &Exp,
340 QualType FromTy, QualType ToTy) {
341 return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
342 Ctx.getTypeSize(FromTy));
343 }
344
345 // Wrapper to generate SMTSolverRef from unpacked binary symbolic
346 // expression. Sets the RetTy parameter. See getSMTSolverRef().
347 static inline llvm::SMTExprRef
348 getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
349 const llvm::SMTExprRef &LHS, QualType LTy,
350 BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
351 QualType RTy, QualType *RetTy) {
352 llvm::SMTExprRef NewLHS = LHS;
353 llvm::SMTExprRef NewRHS = RHS;
354 doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
355
356 // Update the return type parameter if the output type has changed.
357 if (RetTy) {
358 // A boolean result can be represented as an integer type in C/C++, but at
359 // this point we only care about the SMT sorts. Set it as a boolean type
360 // to avoid subsequent SMT errors.
363 *RetTy = Ctx.BoolTy;
364 } else {
365 *RetTy = LTy;
366 }
367
368 // If the two operands are pointers and the operation is a subtraction,
369 // the result is of type ptrdiff_t, which is signed
370 if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
371 *RetTy = Ctx.getPointerDiffType();
372 }
373 }
374
375 return LTy->isRealFloatingType()
376 ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
377 : fromBinOp(Solver, NewLHS, Op, NewRHS,
379 }
380
381 // Wrapper to generate SMTSolverRef from BinarySymExpr.
382 // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
383 static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
384 ASTContext &Ctx,
385 const BinarySymExpr *BSE,
386 bool *hasComparison,
387 QualType *RetTy) {
388 QualType LTy, RTy;
390
391 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
392 llvm::SMTExprRef LHS =
393 getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
394 llvm::APSInt NewRInt;
395 std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
396 llvm::SMTExprRef RHS =
397 Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
398 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
399 }
400
401 if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
402 llvm::APSInt NewLInt;
403 std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
404 llvm::SMTExprRef LHS =
405 Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
406 llvm::SMTExprRef RHS =
407 getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
408 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
409 }
410
411 if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
412 llvm::SMTExprRef LHS =
413 getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
414 llvm::SMTExprRef RHS =
415 getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
416 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
417 }
418
419 llvm_unreachable("Unsupported BinarySymExpr type!");
420 }
421
422 // Recursive implementation to unpack and generate symbolic expression.
423 // Sets the hasComparison and RetTy parameters. See getExpr().
424 static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
425 ASTContext &Ctx, SymbolRef Sym,
426 QualType *RetTy,
427 bool *hasComparison) {
428 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
429 if (RetTy)
430 *RetTy = Sym->getType();
431
432 return fromData(Solver, Ctx, SD);
433 }
434
435 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
436 if (RetTy)
437 *RetTy = Sym->getType();
438
439 QualType FromTy;
440 llvm::SMTExprRef Exp =
441 getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
442
443 // Casting an expression with a comparison invalidates it. Note that this
444 // must occur after the recursive call above.
445 // e.g. (signed char) (x > 0)
446 if (hasComparison)
447 *hasComparison = false;
448 return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
449 }
450
451 if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
452 if (RetTy)
453 *RetTy = Sym->getType();
454
455 QualType OperandTy;
456 llvm::SMTExprRef OperandExp =
457 getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
458 llvm::SMTExprRef UnaryExp =
459 OperandTy->isRealFloatingType()
460 ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
461 : fromUnOp(Solver, USE->getOpcode(), OperandExp);
462
463 // Currently, without the `support-symbolic-integer-casts=true` option,
464 // we do not emit `SymbolCast`s for implicit casts.
465 // One such implicit cast is missing if the operand of the unary operator
466 // has a different type than the unary itself.
467 if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {
468 if (hasComparison)
469 *hasComparison = false;
470 return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
471 }
472 return UnaryExp;
473 }
474
475 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
476 llvm::SMTExprRef Exp =
477 getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
478 // Set the hasComparison parameter, in post-order traversal order.
479 if (hasComparison)
480 *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
481 return Exp;
482 }
483
484 llvm_unreachable("Unsupported SymbolRef type!");
485 }
486
487 // Generate an SMTSolverRef that represents the given symbolic expression.
488 // Sets the hasComparison parameter if the expression has a comparison
489 // operator. Sets the RetTy parameter to the final return type after
490 // promotions and casts.
491 static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
492 ASTContext &Ctx, SymbolRef Sym,
493 QualType *RetTy = nullptr,
494 bool *hasComparison = nullptr) {
495 if (hasComparison) {
496 *hasComparison = false;
497 }
498
499 return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
500 }
501
502 // Generate an SMTSolverRef that compares the expression to zero.
503 static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
504 ASTContext &Ctx,
505 const llvm::SMTExprRef &Exp,
506 QualType Ty, bool Assumption) {
507 if (Ty->isRealFloatingType()) {
508 llvm::APFloat Zero =
509 llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
510 return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
511 Solver->mkFloat(Zero));
512 }
513
515 Ty->isBlockPointerType() || Ty->isReferenceType()) {
516
517 // Skip explicit comparison for boolean types
518 bool isSigned = Ty->isSignedIntegerOrEnumerationType();
519 if (Ty->isBooleanType())
520 return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
521
522 return fromBinOp(
523 Solver, Exp, Assumption ? BO_EQ : BO_NE,
524 Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
525 isSigned);
526 }
527
528 llvm_unreachable("Unsupported type for zero value!");
529 }
530
531 // Wrapper to generate SMTSolverRef from a range. If From == To, an
532 // equality will be created instead.
533 static inline llvm::SMTExprRef
534 getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
535 const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
536 // Convert lower bound
537 QualType FromTy;
538 llvm::APSInt NewFromInt;
539 std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
540 llvm::SMTExprRef FromExp =
541 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
542
543 // Convert symbol
544 QualType SymTy;
545 llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
546
547 // Construct single (in)equality
548 if (From == To)
549 return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
550 FromExp, FromTy, /*RetTy=*/nullptr);
551
552 QualType ToTy;
553 llvm::APSInt NewToInt;
554 std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
555 llvm::SMTExprRef ToExp =
556 Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
557 assert(FromTy == ToTy && "Range values have different types!");
558
559 // Construct two (in)equalities, and a logical and/or
560 llvm::SMTExprRef LHS =
561 getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
562 FromTy, /*RetTy=*/nullptr);
563 llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
564 InRange ? BO_LE : BO_GT, ToExp, ToTy,
565 /*RetTy=*/nullptr);
566
567 return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
569 }
570
571 // Recover the QualType of an APSInt.
572 // TODO: Refactor to put elsewhere
574 const llvm::APSInt &Int) {
575 const QualType Ty =
576 Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
577 if (!Ty.isNull())
578 return Ty;
579 // If Ty is Null, could be because the original type was a _BitInt.
580 // Get the size of the _BitInt type (expressed in bits) and round it up to
581 // the next power of 2 that is at least the bit size of 'char' (usually 8).
582 unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
583 unsigned Pow2DestWidth =
584 std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
585 return Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
586 }
587
588 // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
589 static inline std::pair<llvm::APSInt, QualType>
590 fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
591 llvm::APSInt NewInt;
592 unsigned APSIntBitwidth = Int.getBitWidth();
593 QualType Ty = getAPSIntType(Ctx, Int);
594
595 // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
596 // but the former is not available in Clang. Instead, extend the APSInt
597 // directly.
598 if (APSIntBitwidth == 1 && Ty.isNull())
599 return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
600 getAPSIntType(Ctx, NewInt)};
601 else if (APSIntBitwidth == 1 && !Ty.isNull())
602 return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
603 getAPSIntType(Ctx, NewInt)};
604 if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
605 return {Int, Ty};
606 return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
607 }
608
609 // Perform implicit type conversion on binary symbolic expressions.
610 // May modify all input parameters.
611 // TODO: Refactor to use built-in conversion functions
612 static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
613 ASTContext &Ctx, llvm::SMTExprRef &LHS,
614 llvm::SMTExprRef &RHS, QualType &LTy,
615 QualType &RTy) {
616 assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
617
618 // Perform type conversion
619 if ((LTy->isIntegralOrEnumerationType() &&
621 (LTy->isArithmeticType() && RTy->isArithmeticType())) {
623 Solver, Ctx, LHS, LTy, RHS, RTy);
624 return;
625 }
626
627 if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
629 Solver, Ctx, LHS, LTy, RHS, RTy);
630 return;
631 }
632
633 if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
634 (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
635 (LTy->isReferenceType() || RTy->isReferenceType())) {
636 // TODO: Refactor to Sema::FindCompositePointerType(), and
637 // Sema::CheckCompareOperands().
638
639 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
640 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
641
642 // Cast the non-pointer type to the pointer type.
643 // TODO: Be more strict about this.
644 if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
645 (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
646 (LTy->isReferenceType() ^ RTy->isReferenceType())) {
647 if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
648 LTy->isReferenceType()) {
649 LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
650 LTy = RTy;
651 } else {
652 RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
653 RTy = LTy;
654 }
655 }
656
657 // Cast the void pointer type to the non-void pointer type.
658 // For void types, this assumes that the casted value is equal to the
659 // value of the original pointer, and does not account for alignment
660 // requirements.
661 if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
662 assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
663 "Pointer types have different bitwidths!");
664 if (RTy->isVoidPointerType())
665 RTy = LTy;
666 else
667 LTy = RTy;
668 }
669
670 if (LTy == RTy)
671 return;
672 }
673
674 // Fallback: for the solver, assume that these types don't really matter
675 if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
677 LTy = RTy;
678 return;
679 }
680
681 // TODO: Refine behavior for invalid type casts
682 }
683
684 // Perform implicit integer type conversion.
685 // May modify all input parameters.
686 // TODO: Refactor to use Sema::handleIntegerConversion()
687 template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
688 QualType, uint64_t, QualType, uint64_t)>
689 static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
690 ASTContext &Ctx, T &LHS, QualType &LTy,
691 T &RHS, QualType &RTy) {
692 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
693 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
694
695 assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
696 // Always perform integer promotion before checking type equality.
697 // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
698 if (Ctx.isPromotableIntegerType(LTy)) {
699 QualType NewTy = Ctx.getPromotedIntegerType(LTy);
700 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
701 LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
702 LTy = NewTy;
703 LBitWidth = NewBitWidth;
704 }
705 if (Ctx.isPromotableIntegerType(RTy)) {
706 QualType NewTy = Ctx.getPromotedIntegerType(RTy);
707 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
708 RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
709 RTy = NewTy;
710 RBitWidth = NewBitWidth;
711 }
712
713 if (LTy == RTy)
714 return;
715
716 // Perform integer type conversion
717 // Note: Safe to skip updating bitwidth because this must terminate
718 bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
719 bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
720
721 int order = Ctx.getIntegerTypeOrder(LTy, RTy);
722 if (isLSignedTy == isRSignedTy) {
723 // Same signedness; use the higher-ranked type
724 if (order == 1) {
725 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
726 RTy = LTy;
727 } else {
728 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
729 LTy = RTy;
730 }
731 } else if (order != (isLSignedTy ? 1 : -1)) {
732 // The unsigned type has greater than or equal rank to the
733 // signed type, so use the unsigned type
734 if (isRSignedTy) {
735 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
736 RTy = LTy;
737 } else {
738 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
739 LTy = RTy;
740 }
741 } else if (LBitWidth != RBitWidth) {
742 // The two types are different widths; if we are here, that
743 // means the signed type is larger than the unsigned type, so
744 // use the signed type.
745 if (isLSignedTy) {
746 RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
747 RTy = LTy;
748 } else {
749 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
750 LTy = RTy;
751 }
752 } else {
753 // The signed type is higher-ranked than the unsigned type,
754 // but isn't actually any bigger (like unsigned int and long
755 // on most 32-bit systems). Use the unsigned type corresponding
756 // to the signed type.
757 QualType NewTy =
758 Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
759 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
760 RTy = NewTy;
761 LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
762 LTy = NewTy;
763 }
764 }
765
766 // Perform implicit floating-point type conversion.
767 // May modify all input parameters.
768 // TODO: Refactor to use Sema::handleFloatConversion()
769 template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
770 QualType, uint64_t, QualType, uint64_t)>
771 static inline void
772 doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
773 QualType &LTy, T &RHS, QualType &RTy) {
774 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
775 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
776
777 // Perform float-point type promotion
778 if (!LTy->isRealFloatingType()) {
779 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
780 LTy = RTy;
781 LBitWidth = RBitWidth;
782 }
783 if (!RTy->isRealFloatingType()) {
784 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
785 RTy = LTy;
786 RBitWidth = LBitWidth;
787 }
788
789 if (LTy == RTy)
790 return;
791
792 // If we have two real floating types, convert the smaller operand to the
793 // bigger result
794 // Note: Safe to skip updating bitwidth because this must terminate
795 int order = Ctx.getFloatingTypeOrder(LTy, RTy);
796 if (order > 0) {
797 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
798 RTy = LTy;
799 } else if (order == 0) {
800 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
801 LTy = RTy;
802 } else {
803 llvm_unreachable("Unsupported floating-point type cast!");
804 }
805 }
806};
807} // namespace ento
808} // namespace clang
809
810#endif
#define V(N, I)
Expr * getExpr()
Get 'expr' part of the associated expression/statement.
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition ASTContext.h:188
const llvm::fltSemantics & getFloatTypeSemantics(QualType T) const
Return the APFloat 'semantics' for the specified scalar floating point type.
int getIntegerTypeOrder(QualType LHS, QualType RHS) const
Return the highest ranked integer type, see C99 6.3.1.8p1.
QualType getPointerDiffType() const
Return the unique type for "ptrdiff_t" (C99 7.17) defined in <stddef.h>.
int getFloatingTypeOrder(QualType LHS, QualType RHS) const
Compare the rank of the two specified floating point types, ignoring the domain of the type (i....
CanQualType BoolTy
QualType getIntTypeForBitwidth(unsigned DestWidth, unsigned Signed) const
getIntTypeForBitwidth - sets integer QualTy according to specified details: bitwidth,...
CanQualType CharTy
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
QualType getPromotedIntegerType(QualType PromotableType) const
Return the type that PromotableType will promote to: C99 6.3.1.1p2, assuming that PromotableType is a...
QualType getCorrespondingUnsignedType(QualType T) const
bool isPromotableIntegerType(QualType T) const
More type predicates useful for type checking/promotion.
static bool isLogicalOp(Opcode Opc)
Definition Expr.h:4105
static bool isComparisonOp(Opcode Opc)
Definition Expr.h:4072
bool isComparisonOp() const
Definition Expr.h:4073
BinaryOperatorKind Opcode
Definition Expr.h:3977
A (possibly-)qualified type.
Definition TypeBase.h:937
bool isNull() const
Return true if this QualType doesn't point to a type yet.
Definition TypeBase.h:1004
QualType getCanonicalType() const
Definition TypeBase.h:8337
bool isBlockPointerType() const
Definition TypeBase.h:8542
bool isBooleanType() const
Definition TypeBase.h:9008
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition Type.cpp:2225
bool isVoidPointerType() const
Definition Type.cpp:712
bool isArithmeticType() const
Definition Type.cpp:2337
bool isReferenceType() const
Definition TypeBase.h:8546
bool isIntegralOrEnumerationType() const
Determine whether this type is an integral or enumeration type.
Definition TypeBase.h:8996
bool isObjCObjectPointerType() const
Definition TypeBase.h:8691
bool isRealFloatingType() const
Floating point categories.
Definition Type.cpp:2320
bool isAnyPointerType() const
Definition TypeBase.h:8530
bool isNullPtrType() const
Definition TypeBase.h:8915
UnaryOperatorKind Opcode
Definition Expr.h:2258
A record of the "type" of an APSInt, used for conversions.
Definition APSIntType.h:19
llvm::APSInt convert(const llvm::APSInt &Value) const LLVM_READONLY
Convert and return a new APSInt with the given value, but this type's bit width and signedness.
Definition APSIntType.h:48
Represents a symbolic expression involving a binary operator.
BinaryOperator::Opcode getOpcode() const
static llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, const QualType &Ty, unsigned BitWidth)
Definition SMTConv.h:29
static llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS)
Construct an SMTSolverRef from a floating-point binary operator.
Definition SMTConv.h:203
static QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int)
Definition SMTConv.h:573
static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition SMTConv.h:503
static void doIntTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)
Definition SMTConv.h:689
static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition SMTConv.h:534
static llvm::SMTExprRef fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, const std::vector< llvm::SMTExprRef > &ASTs)
Construct an SMTSolverRef from a n-ary binary operator.
Definition SMTConv.h:77
static llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, bool *hasComparison)
Definition SMTConv.h:424
static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition SMTConv.h:491
static void doTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType &LTy, QualType &RTy)
Definition SMTConv.h:612
static llvm::SMTExprRef fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS)
Construct an SMTSolverRef from a special floating-point binary operator.
Definition SMTConv.h:171
static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)
Construct an SMTSolverRef from a SymbolData.
Definition SMTConv.h:325
static void doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)
Definition SMTConv.h:772
static llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy)
Definition SMTConv.h:383
static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)
Construct an SMTSolverRef from a binary operator.
Definition SMTConv.h:92
static llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType FromTy, QualType ToTy)
Definition SMTConv.h:337
static llvm::SMTExprRef getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, QualType RTy, QualType *RetTy)
Definition SMTConv.h:348
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition SMTConv.h:590
static llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth)
Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths.
Definition SMTConv.h:262
static llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth)
Definition SMTConv.h:315
static llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)
Constructs an SMTSolverRef from a floating-point unary operator.
Definition SMTConv.h:60
static llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)
Constructs an SMTSolverRef from an unary operator.
Definition SMTConv.h:41
virtual QualType getType() const =0
SymbolID getSymbolID() const
Get a unique identifier for this symbol.
Definition SymExpr.h:77
Represents a cast expression.
A symbol representing data which can be stored in a memory location (region).
Definition SymExpr.h:138
virtual StringRef getKindStr() const =0
Get a string representation of the kind of the region.
Represents a symbolic expression involving a unary operator.
BinarySymExprImpl< APSIntPtr, const SymExpr *, SymExpr::Kind::IntSymExprKind > IntSymExpr
Represents a symbolic expression like 3 - 'x'.
const SymExpr * SymbolRef
Definition SymExpr.h:133
BinarySymExprImpl< const SymExpr *, const SymExpr *, SymExpr::Kind::SymSymExprKind > SymSymExpr
Represents a symbolic expression like 'x' + 'y'.
BinarySymExprImpl< const SymExpr *, APSIntPtr, SymExpr::Kind::SymIntExprKind > SymIntExpr
Represents a symbolic expression like 'x' + 3.
@ OS
Indicates that the tracking object is a descendant of a referenced-counted OSObject,...
unsigned SymbolID
Definition SymExpr.h:28
The JSON file list parser is used to communicate input to InstallAPI.
const FunctionProtoType * T