Searched refs:Solver (Results 1 - 17 of 17) sorted by relevance

/freebsd-current/contrib/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
H A DSMTConv.h27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, argument
30 return Solver->getBoolSort();
33 return Solver->getFloatSort(BitWidth);
35 return Solver->getBitvectorSort(BitWidth);
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, argument
44 return Solver->mkBVNeg(Exp);
47 return Solver->mkBVNot(Exp);
50 return Solver->mkNot(Exp);
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, argument
63 return Solver
75 fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, const std::vector<llvm::SMTExprRef> &ASTs) argument
90 fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned) argument
169 fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS) argument
201 fromFloatBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS) argument
260 fromCast(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth) argument
313 castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth) argument
323 fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) argument
335 getCastExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType FromTy, QualType ToTy) argument
346 getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, QualType RTy, QualType *RetTy) argument
381 getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy) argument
422 getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, bool *hasComparison) argument
489 getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy = nullptr, bool *hasComparison = nullptr) argument
501 getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption) argument
532 getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) argument
595 doTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType &LTy, QualType &RTy) argument
672 doIntTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy) argument
755 doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy) argument
[all...]
H A DSMTConstraintManager.h32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); member in class:clang::ento::SMTConstraintManager
52 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
59 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
61 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
70 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
88 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
90 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
94 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
126 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
128 Solver
[all...]
/freebsd-current/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/
H A DDebugSupport.cpp17 #include "clang/Analysis/FlowSensitive/Solver.h"
44 Solver::Result::Assignment Assignment) {
46 case Solver::Result::Assignment::AssignedFalse:
48 case Solver::Result::Assignment::AssignedTrue:
54 llvm::StringRef debugString(Solver::Result::Status Status) {
56 case Solver::Result::Status::Satisfiable:
58 case Solver::Result::Status::Unsatisfiable:
60 case Solver::Result::Status::TimedOut:
66 llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
69 std::vector<std::pair<Atom, Solver
[all...]
H A DWatchedLiteralsSolver.cpp21 #include "clang/Analysis/FlowSensitive/Solver.h"
525 std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
529 return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);
534 return std::make_pair(Solver::Result::TimedOut(), 0);
563 return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);
620 return std::make_pair(Solver::Result::Satisfiable(buildSolution()),
626 llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
627 llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
634 ? Solver::Result::Assignment::AssignedFalse
635 : Solver
[all...]
H A DDataflowAnalysisContext.cpp170 Solver::Result DataflowAnalysisContext::querySolver(
340 DataflowAnalysisContext::DataflowAnalysisContext(std::unique_ptr<Solver> S,
/freebsd-current/contrib/llvm-project/llvm/lib/Transforms/Scalar/
H A DSCCP.cpp65 SCCPSolver Solver(
70 Solver.markBlockExecutable(&F.front());
74 Solver.markOverdefined(&AI);
79 Solver.solve();
81 ResolvedUndefs = Solver.resolvedUndefsIn(F);
93 if (!Solver.isBlockExecutable(&BB)) {
101 MadeChanges |= Solver.simplifyInstsInBlock(BB, InsertedValues,
112 MadeChanges |= Solver.removeNonFeasibleEdges(&BB, DTU, NewUnreachableBB);
/freebsd-current/contrib/llvm-project/llvm/lib/Transforms/IPO/
H A DSCCP.cpp52 SCCPSolver &Solver) {
54 if (!Solver.isArgumentTrackedFunction(&F))
57 if (Solver.mustPreserveReturn(&F)) {
68 [&Solver](User *U) {
70 !Solver.isBlockExecutable(cast<Instruction>(U)->getParent()))
79 return all_of(Solver.getStructLatticeValueFor(U),
92 return !SCCPSolver::isOverdefined(Solver.getLatticeValueFor(U));
118 SCCPSolver Solver(DL, GetTLI, M.getContext());
119 FunctionSpecializer Specializer(Solver, M, FAM, GetBFI, GetTLI, GetTTI,
130 Solver
50 findReturnsToZap(Function &F, SmallVector<ReturnInst *, 8> &ReturnsToZap, SCCPSolver &Solver) argument
[all...]
H A DFunctionSpecialization.cpp110 // the \p Solver found they were executable prior to specialization, and only
120 // is concerned. They haven't been proven dead yet by the Solver,
553 if (!Solver.isBlockExecutable(Call->getParent()))
742 Solver.solveWhileResolvedUndefsIn(Clones);
757 if (!Solver.isStructLatticeConstant(F, STy))
760 auto It = Solver.getTrackedRetVals().find(F);
761 assert(It != Solver.getTrackedRetVals().end() &&
771 Solver.resetLatticeValueFor(CS);
777 Solver.solveWhileResolvedUndefs();
840 if (!Solver
[all...]
H A DCalledValuePropagation.cpp372 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice);
378 Solver.MarkBlockExecutable(&F.front());
380 // Solver our custom lattice. In doing so, we will also build a set of
382 Solver.Solve();
390 CVPLatticeVal LV = Solver.getExistingValueState(RegI);
/freebsd-current/contrib/llvm-project/clang/include/clang/Analysis/FlowSensitive/
H A DSolver.h1 //===- Solver.h -------------------------------------------------*- C++ -*-===//
28 class Solver { class in namespace:clang::dataflow
81 virtual ~Solver() = default;
92 llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
93 llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
H A DDebugSupport.h20 #include "clang/Analysis/FlowSensitive/Solver.h"
31 llvm::StringRef debugString(Solver::Result::Status Status);
H A DWatchedLiteralsSolver.h18 #include "clang/Analysis/FlowSensitive/Solver.h"
30 class WatchedLiteralsSolver : public Solver {
H A DDataflowAnalysisContext.h23 #include "clang/Analysis/FlowSensitive/Solver.h"
93 DataflowAnalysisContext(std::unique_ptr<Solver> S,
198 Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
240 Solver::Result::Status::Satisfiable;
247 Solver::Result::Status::Unsatisfiable;
250 std::unique_ptr<Solver> S;
/freebsd-current/contrib/llvm-project/llvm/include/llvm/CodeGen/PBQP/
H A DGraph.h164 SolverT *Solver = nullptr; member in class:llvm::PBQP::Graph
357 assert(!Solver && "Solver already set. Call unsetSolver().");
358 Solver = &S;
360 Solver->handleAddNode(NId);
362 Solver->handleAddEdge(EId);
367 assert(Solver && "Solver not set.");
368 Solver = nullptr;
379 if (Solver)
[all...]
/freebsd-current/contrib/llvm-project/llvm/include/llvm/Transforms/IPO/
H A DFunctionSpecialization.h179 SCCPSolver &Solver; member in class:llvm::InstCostVisitor
196 TargetTransformInfo &TTI, SCCPSolver &Solver)
197 : DL(DL), BFI(BFI), TTI(TTI), Solver(Solver) {}
200 return Solver.isBlockExecutable(BB) && !DeadBlocks.contains(BB);
251 /// The IPSCCP Solver.
252 SCCPSolver &Solver; member in class:llvm::FunctionSpecializer
273 SCCPSolver &Solver, Module &M, FunctionAnalysisManager *FAM,
278 : Solver(Solver),
195 InstCostVisitor(const DataLayout &DL, BlockFrequencyInfo &BFI, TargetTransformInfo &TTI, SCCPSolver &Solver) argument
272 FunctionSpecializer( SCCPSolver &Solver, Module &M, FunctionAnalysisManager *FAM, std::function<BlockFrequencyInfo &(Function &)> GetBFI, std::function<const TargetLibraryInfo &(Function &)> GetTLI, std::function<TargetTransformInfo &(Function &)> GetTTI, std::function<AssumptionCache &(Function &)> GetAC) argument
[all...]
/freebsd-current/contrib/llvm-project/llvm/lib/Support/
H A DZ3Solver.cpp265 Z3_solver Solver; member in class:__anon2296::Z3Solver
274 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
275 Z3_solver_inc_ref(Context.Context, Solver);
284 if (Solver)
285 Z3_solver_dec_ref(Context.Context, Solver);
289 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
846 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
860 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
874 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
884 void push() override { return Z3_solver_push(Context.Context, Solver); }
[all...]
/freebsd-current/contrib/llvm-project/llvm/lib/Transforms/Utils/
H A DSCCPSolver.cpp106 /// Try to use \p Inst's value range from \p Solver to infer the NUW flag.
107 static bool refineInstruction(SCCPSolver &Solver, argument
111 auto GetRange = [&Solver, &InsertedValues](Value *Op) {
118 return getConstantRange(Solver.getLatticeValueFor(Op), Op->getType(),
155 static bool replaceSignedInst(SCCPSolver &Solver, argument
159 auto isNonNegative = [&Solver](Value *V) {
166 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V);
216 Solver.removeLatticeValueFor(&Inst);

Completed in 365 milliseconds