| /freebsd/contrib/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 29 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, in mkSort() argument
32 return Solver->getBoolSort(); in mkSort()
35 return Solver->getFloatSort(BitWidth); in mkSort()
37 return Solver->getBitvectorSort(BitWidth); in mkSort()
41 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, in fromUnOp() argument
46 return Solver->mkBVNeg(Exp); in fromUnOp()
49 return Solver->mkBVNot(Exp); in fromUnOp()
52 return Solver->mkNot(Exp); in fromUnOp()
60 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, in fromFloatUnOp() argument
65 return Solver->mkFPNeg(Exp); in fromFloatUnOp()
[all …]
|
| H A D | SMTConstraintManager.h | 33 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE() local
39 Solver->setBoolParam("model", true); // Enable model finding in REGISTER_TRAIT_WITH_PROGRAMSTATE()
40 Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
56 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
63 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
65 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
74 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
92 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
94 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
98 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
[all …]
|
| /freebsd/contrib/llvm-project/llvm/lib/Transforms/IPO/ |
| H A D | SCCP.cpp | 52 SCCPSolver &Solver) { in findReturnsToZap() argument
54 if (!Solver.isArgumentTrackedFunction(&F)) in findReturnsToZap()
57 if (Solver.mustPreserveReturn(&F)) { in findReturnsToZap()
68 [&Solver](User *U) { in findReturnsToZap()
70 !Solver.isBlockExecutable(cast<Instruction>(U)->getParent())) in findReturnsToZap()
79 return none_of(Solver.getStructLatticeValueFor(U), in findReturnsToZap()
90 return !SCCPSolver::isOverdefined(Solver.getLatticeValueFor(U)); in findReturnsToZap()
116 SCCPSolver Solver(DL, GetTLI, M.getContext()); in runIPSCCP() local
117 FunctionSpecializer Specializer(Solver, M, FAM, GetBFI, GetTLI, GetTTI, in runIPSCCP()
128 Solver.addPredicateInfo(F, DT, AC); in runIPSCCP()
[all …]
|
| H A D | FunctionSpecialization.cpp | 118 assert(Solver.isBlockExecutable(BB) && "BB already found dead by IPSCCP!"); in estimateBasicBlocks()
146 if (auto *C = Solver.getConstantOrNull(V)) in findConstantFor()
491 const ValueLatticeElement &OtherLV = Solver.getLatticeValueFor(V); in visitCmpInst()
591 if (!Solver.isBlockExecutable(Call->getParent())) in promoteConstantStackValues()
805 Solver.solveWhileResolvedUndefsIn(Clones); in run()
820 if (!Solver.isStructLatticeConstant(F, STy)) in run()
823 auto It = Solver.getTrackedRetVals().find(F); in run()
824 assert(It != Solver.getTrackedRetVals().end() && in run()
834 Solver.resetLatticeValueFor(CS); in run()
840 Solver.solveWhileResolvedUndefs(); in run()
[all …]
|
| H A D | CalledValuePropagation.cpp | 378 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
384 Solver.MarkBlockExecutable(&F.front()); in runCVP()
388 Solver.Solve(); in runCVP()
396 CVPLatticeVal LV = Solver.getExistingValueState(RegI); in runCVP()
|
| /freebsd/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/ |
| H A D | DebugSupport.cpp | 42 Solver::Result::Assignment Assignment) { in operator <<()
44 case Solver::Result::Assignment::AssignedFalse: in operator <<()
46 case Solver::Result::Assignment::AssignedTrue: in operator <<()
52 llvm::StringRef debugString(Solver::Result::Status Status) { in debugString()
54 case Solver::Result::Status::Satisfiable: in debugString()
56 case Solver::Result::Status::Unsatisfiable: in debugString()
58 case Solver::Result::Status::TimedOut: in debugString()
64 llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) { in operator <<()
67 std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = { in operator <<()
|
| H A D | WatchedLiteralsSolver.cpp | 146 std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && { in solve()
150 return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations); in solve()
155 return std::make_pair(Solver::Result::TimedOut(), 0); in solve()
184 return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations); in solve()
241 return std::make_pair(Solver::Result::Satisfiable(buildSolution()), in solve()
247 llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() { in buildSolution()
248 llvm::DenseMap<Atom, Solver::Result::Assignment> Solution; in buildSolution()
255 ? Solver::Result::Assignment::AssignedFalse in buildSolution()
256 : Solver::Result::Assignment::AssignedTrue; in buildSolution()
408 Solver::Result
[all …]
|
| H A D | DataflowAnalysisContext.cpp | 170 Solver::Result DataflowAnalysisContext::querySolver( in querySolver()
341 Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts) in DataflowAnalysisContext()
|
| /freebsd/contrib/llvm-project/llvm/lib/Transforms/Scalar/ |
| H A D | SCCP.cpp | 58 SCCPSolver Solver( in runSCCP() local
65 Solver.addTrackedFunction(&F); in runSCCP()
68 Solver.markBlockExecutable(&F.front()); in runSCCP()
72 Solver.trackValueOfArgument(&AI); in runSCCP()
77 Solver.solve(); in runSCCP()
79 ResolvedUndefs = Solver.resolvedUndefsIn(F); in runSCCP()
91 if (!Solver.isBlockExecutable(&BB)) { in runSCCP()
99 MadeChanges |= Solver.simplifyInstsInBlock(BB, InsertedValues, in runSCCP()
110 MadeChanges |= Solver.removeNonFeasibleEdges(&BB, DTU, NewUnreachableBB); in runSCCP()
116 Solver.inferReturnAttributes(); in runSCCP()
|
| /freebsd/contrib/llvm-project/llvm/include/llvm/CodeGen/PBQP/ |
| H A D | Graph.h | 164 SolverT *Solver = nullptr; variable
357 assert(!Solver && "Solver already set. Call unsetSolver()."); in setSolver()
358 Solver = &S; in setSolver()
360 Solver->handleAddNode(NId); in setSolver()
362 Solver->handleAddEdge(EId); in setSolver()
367 assert(Solver && "Solver not set."); in unsetSolver()
368 Solver = nullptr; in unsetSolver()
379 if (Solver) in addNode()
380 Solver->handleAddNode(NId); in addNode()
398 if (Solver) in addNodeBypassingCostAllocator()
[all …]
|
| /freebsd/contrib/llvm-project/clang/include/clang/Analysis/FlowSensitive/ |
| H A D | DataflowAnalysisContext.h | 67 DataflowAnalysisContext(std::unique_ptr<Solver> S,
78 DataflowAnalysisContext(Solver &S, Options Opts = Options{
186 Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
228 DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver,
244 Solver::Result::Status::Satisfiable; in isSatisfiable()
251 Solver::Result::Status::Unsatisfiable; in isUnsatisfiable()
254 Solver &S;
255 std::unique_ptr<Solver> OwnedSolver;
|
| H A D | Solver.h | 28 class Solver {
81 virtual ~Solver() = default;
95 llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
96 llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
|
| H A D | DebugSupport.h | 31 llvm::StringRef debugString(Solver::Result::Status Status);
|
| H A D | WatchedLiteralsSolver.h | 31 class WatchedLiteralsSolver : public Solver {
|
| H A D | DataflowAnalysis.h | 330 auto Solver = std::make_unique<WatchedLiteralsSolver>(MaxSATIterations); variable
331 DataflowAnalysisContext AnalysisContext(*Solver);
370 if (Solver->reachedLimit())
|
| /freebsd/contrib/llvm-project/llvm/include/llvm/Transforms/IPO/ |
| H A D | FunctionSpecialization.h | 158 const SCCPSolver &Solver; variable
176 SCCPSolver &Solver) in InstCostVisitor() argument
177 : GetBFI(GetBFI), F(F), DL(DL), TTI(TTI), Solver(Solver) {} in InstCostVisitor()
180 return Solver.isBlockExecutable(BB) && !DeadBlocks.contains(BB); in isBlockExecutable()
235 SCCPSolver &Solver; variable
256 SCCPSolver &Solver, Module &M, FunctionAnalysisManager *FAM, in FunctionSpecializer() argument
261 : Solver(Solver), M(M), FAM(FAM), GetBFI(GetBFI), GetTLI(GetTLI), in FunctionSpecializer()
270 return InstCostVisitor(GetBFI, F, M.getDataLayout(), TTI, Solver); in getInstCostVisitorFor()
|
| /freebsd/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/ |
| H A D | Z3CrosscheckVisitor.cpp | 90 auto GetUsedRLimit = [](const llvm::SMTSolverRef &Solver) { in finalizeVisitor() argument
91 return Solver->getStatistics()->getUnsigned("rlimit count"); in finalizeVisitor()
94 auto AttemptOnce = [&](const llvm::SMTSolverRef &Solver) -> Z3Result { in finalizeVisitor() argument
96 unsigned InitialRLimit = GetUsedRLimit(Solver); in finalizeVisitor()
98 std::optional<bool> IsSAT = Solver->check(); in finalizeVisitor()
103 GetUsedRLimit(Solver) - InitialRLimit, in finalizeVisitor()
|
| /freebsd/contrib/llvm-project/llvm/lib/Support/ |
| H A D | Z3Solver.cpp | 270 Z3_solver Solver = [this] { in __anona2cc94240202() member in __anona2cc94240111::Z3Solver
297 Z3_solver_dec_ref(Context.Context, Solver); in ~Z3Solver()
301 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
872 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
886 Z3_solver_set_params(Context.Context, Solver, Params); in check()
887 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
897 void push() override { return Z3_solver_push(Context.Context, Solver); } in push()
900 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates); in pop()
901 return Z3_solver_pop(Context.Context, Solver, NumStates); in pop()
[all …]
|
| /freebsd/contrib/llvm-project/llvm/lib/Transforms/Utils/ |
| H A D | SCCPSolver.cpp | 91 static ConstantRange getRange(Value *Op, SCCPSolver &Solver, in getRange() argument
99 return Solver.getLatticeValueFor(Op).asConstantRange(Op->getType(), in getRange()
104 static bool refineInstruction(SCCPSolver &Solver, in refineInstruction() argument
108 auto GetRange = [&Solver, &InsertedValues](Value *Op) { in refineInstruction()
109 return getRange(Op, Solver, InsertedValues); in refineInstruction()
176 static bool replaceSignedInst(SCCPSolver &Solver, in replaceSignedInst() argument
180 auto isNonNegative = [&Solver, &InsertedValues](Value *V) { in replaceSignedInst()
181 return getRange(V, Solver, InsertedValues).isAllNonNegative(); in replaceSignedInst()
231 Solver.removeLatticeValueFor(&Inst); in replaceSignedInst()
237 static Value *simplifyInstruction(SCCPSolver &Solver, in simplifyInstruction() argument
[all …]
|
| /freebsd/contrib/one-true-awk/testdir/ |
| H A D | funstack.ok | 908 Solver . . . . . . . . . . . . . . . . . 274--274
|
| H A D | funstack.in | 6363 title = "{ACM} Algorithm 423: Linear Equation Solver",
16255 …abstract = "The Designer Problem Solver (DPS) demonstrates that the computer can perform simpl…
|