86 lines · cpp
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-exception6//7//===----------------------------------------------------------------------===//8//9// This checker evaluates the builting assume functions.10// This checker also sinks execution paths leaving [[assume]] attributes with11// 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 AssumeModelingChecker28 : 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} // namespace34 35void AssumeModelingChecker::checkPostStmt(const AttributedStmt *A,36 CheckerContext &C) const {37 if (!hasSpecificAttr<CXXAssumeAttr>(A->getAttrs()))38 return;39 40 for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {41 SVal AssumptionVal = C.getSVal(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>(Call.getDecl());58 if (!FD)59 return false;60 61 if (!llvm::is_contained({Builtin::BI__builtin_assume, Builtin::BI__assume},62 FD->getBuiltinID())) {63 return false;64 }65 66 assert(Call.getNumArgs() > 0);67 SVal Arg = Call.getArgSVal(0);68 if (Arg.isUndef())69 return true; // Return true to model purity.70 71 State = State->assume(Arg.castAs<DefinedOrUnknownSVal>(), 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