//===- ConstraintManager.h - Constraints on symbolic values. ----*- 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 defined the interface to manage constraints on symbolic values.
//
//===----------------------------------------------------------------------===//
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
#include "clang/Basic/LLVM.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
#include "llvm/Support/SaveAndRestore.h"
#include <memory>
#include <optional>
#include <utility>
namespace llvm {
class APSInt;
} // namespace llvm
namespace clang {
namespace ento {
class ProgramStateManager;
class ExprEngine;
class SymbolReaper;
class ConditionTruthVal {
std::optional<bool> Val;
public:
/// Construct a ConditionTruthVal indicating the constraint is constrained
/// to either true or false, depending on the boolean value provided.
ConditionTruthVal(bool constraint) : Val(constraint) {}
/// Construct a ConstraintVal indicating the constraint is underconstrained.
ConditionTruthVal() = default;
/// \return Stored value, assuming that the value is known.
/// Crashes otherwise.
bool getValue() const {
return *Val;
}
/// Return true if the constraint is perfectly constrained to 'true'.
bool isConstrainedTrue() const { return Val && *Val; }
/// Return true if the constraint is perfectly constrained to 'false'.
bool isConstrainedFalse() const { return Val && !*Val; }
/// Return true if the constrained is perfectly constrained.
bool isConstrained() const { return Val.has_value(); }
/// Return true if the constrained is underconstrained and we do not know
/// if the constraint is true of value.
bool isUnderconstrained() const { return !Val.has_value(); }
};
class ConstraintManager {
public:
ConstraintManager() = default;
virtual ~ConstraintManager();
virtual bool haveEqualConstraints(ProgramStateRef S1,
ProgramStateRef S2) const = 0;
ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
bool Assumption);
using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
/// Returns a pair of states (StTrue, StFalse) where the given condition is
/// assumed to be true or false, respectively.
/// (Note that these two states might be equal if the parent state turns out
/// to be infeasible. This may happen if the underlying constraint solver is
/// not perfectly precise and this may happen very rarely.)
ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
const llvm::APSInt &From,
const llvm::APSInt &To, bool InBound);
/// Returns a pair of states (StInRange, StOutOfRange) where the given value
/// is assumed to be in the range or out of the range, respectively.
/// (Note that these two states might be equal if the parent state turns out
/// to be infeasible. This may happen if the underlying constraint solver is
/// not perfectly precise and this may happen very rarely.)
ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
const llvm::APSInt &From,
const llvm::APSInt &To);
/// If a symbol is perfectly constrained to a constant, attempt
/// to return the concrete value.
///
/// Note that a ConstraintManager is not obligated to return a concretized
/// value for a symbol, even if it is perfectly constrained.
/// It might return null.
virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
SymbolRef sym) const {
return nullptr;
}
/// Scan all symbols referenced by the constraints. If the symbol is not
/// alive, remove it.
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
SymbolReaper& SymReaper) = 0;
virtual void printJson(raw_ostream &Out, ProgramStateRef State,
const char *NL, unsigned int Space,
bool IsDot) const = 0;
virtual void printValue(raw_ostream &Out, ProgramStateRef State,
SymbolRef Sym) {}
/// Convenience method to query the state to see if a symbol is null or
/// not null, or if neither assumption can be made.
ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
return checkNull(State, Sym);
}
protected:
/// A helper class to simulate the call stack of nested assume calls.
class AssumeStackTy {
public:
void push(const ProgramState *S) { Aux.push_back(S); }
void pop() { Aux.pop_back(); }
bool contains(const ProgramState *S) const {
return llvm::is_contained(Aux, S);
}
private:
llvm::SmallVector<const ProgramState *, 4> Aux;
};
AssumeStackTy AssumeStack;
virtual ProgramStateRef assumeInternal(ProgramStateRef state,
DefinedSVal Cond, bool Assumption) = 0;
virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
NonLoc Value,
const llvm::APSInt &From,
const llvm::APSInt &To,
bool InBound) = 0;
/// canReasonAbout - Not all ConstraintManagers can accurately reason about
/// all SVal values. This method returns true if the ConstraintManager can
/// reasonably handle a given SVal value. This is typically queried by
/// ExprEngine to determine if the value should be replaced with a
/// conjured symbolic value in order to recover some precision.
virtual bool canReasonAbout(SVal X) const = 0;
/// Returns whether or not a symbol is known to be null ("true"), known to be
/// non-null ("false"), or may be either ("underconstrained").
virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
template <typename AssumeFunction>
ProgramStatePair assumeDualImpl(ProgramStateRef &State,
AssumeFunction &Assume);
};
std::unique_ptr<ConstraintManager>
CreateRangeConstraintManager(ProgramStateManager &statemgr,
ExprEngine *exprengine);
std::unique_ptr<ConstraintManager>
CreateZ3ConstraintManager(ProgramStateManager &statemgr,
ExprEngine *exprengine);
} // namespace ento
} // namespace clang
#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H