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 assert(Assumption && "We should know the exact outcome of an assume expr");
49 if (Assumption && Assumption->isZero()) {
50 C.addSink();
51 }
52 }
53}
54
55bool AssumeModelingChecker::evalCall(const CallEvent &Call,
56 CheckerContext &C) const {
57 ProgramStateRef State = C.getState();
58 const auto *FD = dyn_cast_or_null<FunctionDecl>(Val: Call.getDecl());
59 if (!FD)
60 return false;
61
62 if (!llvm::is_contained(Set: {Builtin::BI__builtin_assume, Builtin::BI__assume},
63 Element: FD->getBuiltinID())) {
64 return false;
65 }
66
67 assert(Call.getNumArgs() > 0);
68 SVal Arg = Call.getArgSVal(Index: 0);
69 if (Arg.isUndef())
70 return true; // Return true to model purity.
71
72 State = State->assume(Cond: Arg.castAs<DefinedOrUnknownSVal>(), Assumption: true);
73 if (!State) {
74 C.addSink();
75 return true;
76 }
77
78 C.addTransition(State);
79 return true;
80}
81
82void ento::registerAssumeModeling(CheckerManager &Mgr) {
83 Mgr.registerChecker<AssumeModelingChecker>();
84}
85
86bool ento::shouldRegisterAssumeModeling(const CheckerManager &) { return true; }
87