1//=== AssumeModeling.cpp --------------------------------------------------===//
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 checker evaluates the builting assume functions.
10// This checker also sinks execution paths leaving [[assume]] attributes with
11// false assumptions.
12//
13//===----------------------------------------------------------------------===//
14
15#include "clang/AST/AttrIterator.h"
16#include "clang/Basic/Builtins.h"
17#include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
18#include "clang/StaticAnalyzer/Core/Checker.h"
19#include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
20#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
21#include "llvm/ADT/STLExtras.h"
22
23using namespace clang;
24using namespace ento;
25
26namespace {
27class AssumeModelingChecker
28 : public Checker<eval::Call, check::PostStmt<AttributedStmt>> {
29public:
30 void checkPostStmt(const AttributedStmt *A, CheckerContext &C) const;
31 bool evalCall(const CallEvent &Call, CheckerContext &C) const;
32};
33} // namespace
34
35void AssumeModelingChecker::checkPostStmt(const AttributedStmt *A,
36 CheckerContext &C) const {
37 if (!hasSpecificAttr<CXXAssumeAttr>(container: A->getAttrs()))
38 return;
39
40 for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(container: A->getAttrs())) {
41 SVal AssumptionVal = C.getSVal(S: Attr->getAssumption());
42
43 // The assumption is not evaluated at all if it had sideffects; skip them.
44 if (AssumptionVal.isUnknown())
45 continue;
46
47 const auto *Assumption = AssumptionVal.getAsInteger();
48 if (Assumption && Assumption->isZero()) {
49 C.addSink();
50 }
51 }
52}
53
54bool AssumeModelingChecker::evalCall(const CallEvent &Call,
55 CheckerContext &C) const {
56 ProgramStateRef State = C.getState();
57 const auto *FD = dyn_cast_or_null<FunctionDecl>(Val: Call.getDecl());
58 if (!FD)
59 return false;
60
61 if (!llvm::is_contained(Set: {Builtin::BI__builtin_assume, Builtin::BI__assume},
62 Element: FD->getBuiltinID())) {
63 return false;
64 }
65
66 assert(Call.getNumArgs() > 0);
67 SVal Arg = Call.getArgSVal(Index: 0);
68 if (Arg.isUndef())
69 return true; // Return true to model purity.
70
71 State = State->assume(Cond: Arg.castAs<DefinedOrUnknownSVal>(), Assumption: true);
72 if (!State) {
73 C.addSink();
74 return true;
75 }
76
77 C.addTransition(State);
78 return true;
79}
80
81void ento::registerAssumeModeling(CheckerManager &Mgr) {
82 Mgr.registerChecker<AssumeModelingChecker>();
83}
84
85bool ento::shouldRegisterAssumeModeling(const CheckerManager &) { return true; }
86