SMTConstraintManager.h

Go to the documentation of this file.

//== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
//  This file defines a SMT generic API, which will be the base class for
//  every SMT solver specific class.
//
//===----------------------------------------------------------------------===//
 
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 
#include "clang/Basic/JsonSupport.h"
#include "clang/Basic/TargetInfo.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
#include <optional>
 
typedef llvm::ImmutableSet<
    std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
    ConstraintSMTType;
REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
 
namespace clang {
namespace ento {
 
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
  mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
 
public:
  SMTConstraintManager(clang::ento::ExprEngine *EE,
                       clang::ento::SValBuilder &SB)
      : SimpleConstraintManager(EE, SB) {
    Solver->setBoolParam("model", true); // Enable model finding
    Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/);
  }
  virtual ~SMTConstraintManager() = default;
 
  //===------------------------------------------------------------------===//
  // Implementation for interface from SimpleConstraintManager.
  //===------------------------------------------------------------------===//
 
  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
                            bool Assumption) override {
    ASTContext &Ctx = getBasicVals().getContext();
 
    QualType RetTy;
    bool hasComparison;
 
    llvm::SMTExprRef Exp =
        SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
 
    // Create zero comparison for implicit boolean cast, with reversed
    // assumption
    if (!hasComparison && !RetTy->isBooleanType())
      return assumeExpr(
          State, Sym,
          SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
 
    return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
  }
 
  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
                                          const llvm::APSInt &From,
                                          const llvm::APSInt &To,
                                          bool InRange) override {
    ASTContext &Ctx = getBasicVals().getContext();
    return assumeExpr(
        State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
  }
 
  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                       bool Assumption) override {
    // Skip anything that is unsupported
    return State;
  }
 
  //===------------------------------------------------------------------===//
  // Implementation for interface from ConstraintManager.
  //===------------------------------------------------------------------===//
 
  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
    ASTContext &Ctx = getBasicVals().getContext();
 
    QualType RetTy;
    // The expression may be casted, so we cannot call getZ3DataExpr() directly
    llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
    llvm::SMTExprRef Exp =
        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
 
    // Negate the constraint
    llvm::SMTExprRef NotExp =
        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
 
    ConditionTruthVal isSat = checkModel(State, Sym, Exp);
    ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
 
    // Zero is the only possible solution
    if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
      return true;
 
    // Zero is not a solution
    if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
      return false;
 
    // Zero may be a solution
    return ConditionTruthVal();
  }
 
  const llvm::APSInt *getSymVal(ProgramStateRef State,
                                SymbolRef Sym) const override {
    BasicValueFactory &BVF = getBasicVals();
    ASTContext &Ctx = BVF.getContext();
 
    if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
      QualType Ty = Sym->getType();
      assert(!Ty->isRealFloatingType());
      llvm::APSInt Value(Ctx.getTypeSize(Ty),
                         !Ty->isSignedIntegerOrEnumerationType());
 
      // TODO: this should call checkModel so we can use the cache, however,
      // this method tries to get the interpretation (the actual value) from
      // the solver, which is currently not cached.
 
      llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
 
      Solver->reset();
      addStateConstraints(State);
 
      // Constraints are unsatisfiable
      std::optional<bool> isSat = Solver->check();
      if (!isSat || !*isSat)
        return nullptr;
 
      // Model does not assign interpretation
      if (!Solver->getInterpretation(Exp, Value))
        return nullptr;
 
      // A value has been obtained, check if it is the only value
      llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
          Solver, Exp, BO_NE,
          Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
                              : Solver->mkBitvector(Value, Value.getBitWidth()),
          /*isSigned=*/false);
 
      Solver->addConstraint(NotExp);
 
      std::optional<bool> isNotSat = Solver->check();
      if (!isNotSat || *isNotSat)
        return nullptr;
 
      // This is the only solution, store it
      return BVF.getValue(Value).get();
    }
 
    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
      SymbolRef CastSym = SC->getOperand();
      QualType CastTy = SC->getType();
      // Skip the void type
      if (CastTy->isVoidType())
        return nullptr;
 
      const llvm::APSInt *Value;
      if (!(Value = getSymVal(State, CastSym)))
        return nullptr;
      return BVF.Convert(SC->getType(), *Value).get();
    }
 
    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
      const llvm::APSInt *LHS, *RHS;
      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
        LHS = getSymVal(State, SIE->getLHS());
        RHS = SIE->getRHS().get();
      } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
        LHS = ISE->getLHS().get();
        RHS = getSymVal(State, ISE->getRHS());
      } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
        // Early termination to avoid expensive call
        LHS = getSymVal(State, SSM->getLHS());
        RHS = LHS ?