| /freebsd/contrib/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, in mkSort() argument
30 return Solver->getBoolSort(); in mkSort()
33 return Solver->getFloatSort(BitWidth); in mkSort()
35 return Solver->getBitvectorSort(BitWidth); in mkSort()
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, in fromUnOp() argument
44 return Solver->mkBVNeg(Exp); in fromUnOp()
47 return Solver->mkBVNot(Exp); in fromUnOp()
50 return Solver->mkNot(Exp); in fromUnOp()
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, in fromFloatUnOp() argument
63 return Solver->mkFPNeg(Exp); in fromFloatUnOp()
[all …]
|
| H A D | SMTConstraintManager.h | 32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE() local
38 Solver->setBoolParam("model", true); // Enable model finding in REGISTER_TRAIT_WITH_PROGRAMSTATE()
39 Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
55 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
62 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
64 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
73 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
91 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
93 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
97 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 all_of(Solver.getStructLatticeValueFor(U), in findReturnsToZap()
92 return !SCCPSolver::isOverdefined(Solver.getLatticeValueFor(U)); in findReturnsToZap()
118 SCCPSolver Solver(DL, GetTLI, M.getContext()); in runIPSCCP() local
119 FunctionSpecializer Specializer(Solver, M, FAM, GetBFI, GetTLI, GetTTI, in runIPSCCP()
130 Solver.addPredicateInfo(F, DT, AC); in runIPSCCP()
[all …]
|
| H A D | FunctionSpecialization.cpp | 553 if (!Solver.isBlockExecutable(Call->getParent())) in promoteConstantStackValues()
744 Solver.solveWhileResolvedUndefsIn(Clones); in run()
759 if (!Solver.isStructLatticeConstant(F, STy)) in run()
762 auto It = Solver.getTrackedRetVals().find(F); in run()
763 assert(It != Solver.getTrackedRetVals().end() && in run()
773 Solver.resetLatticeValueFor(CS); in run()
779 Solver.solveWhileResolvedUndefs(); in run()
842 if (!Solver.isBlockExecutable(CS.getParent())) in findSpecializations()
948 if (!Solver.isBlockExecutable(&F->getEntryBlock())) in isCandidateFunction()
971 Solver.setLatticeValueForSpecializationArguments(Clone, S.Args); in createSpecialization()
[all …]
|
| H A D | CalledValuePropagation.cpp | 373 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
379 Solver.MarkBlockExecutable(&F.front()); in runCVP()
383 Solver.Solve(); in runCVP()
391 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 | 171 Solver::Result DataflowAnalysisContext::querySolver( in querySolver()
342 Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts) in DataflowAnalysisContext()
|
| /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/llvm/lib/Transforms/Scalar/ |
| H A D | SCCP.cpp | 65 SCCPSolver Solver( in runSCCP() local
70 Solver.markBlockExecutable(&F.front()); in runSCCP()
74 Solver.markOverdefined(&AI); in runSCCP()
79 Solver.solve(); in runSCCP()
81 ResolvedUndefs = Solver.resolvedUndefsIn(F); in runSCCP()
93 if (!Solver.isBlockExecutable(&BB)) { in runSCCP()
101 MadeChanges |= Solver.simplifyInstsInBlock(BB, InsertedValues, in runSCCP()
112 MadeChanges |= Solver.removeNonFeasibleEdges(&BB, DTU, NewUnreachableBB); in runSCCP()
|
| /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 | 346 auto Solver = std::make_unique<WatchedLiteralsSolver>(MaxSATIterations); variable
347 DataflowAnalysisContext AnalysisContext(*Solver);
386 if (Solver->reachedLimit())
|
| /freebsd/contrib/llvm-project/llvm/include/llvm/Transforms/IPO/ |
| H A D | FunctionSpecialization.h | 179 SCCPSolver &Solver; in FunctionSpecializer() argument
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;
273 SCCPSolver &Solver, Module &M, FunctionAnalysisManager *FAM,
278 : Solver(Solver),
126 SCCPSolver &Solver; global() variable
134 InstCostVisitor(const DataLayout & DL,BlockFrequencyInfo & BFI,TargetTransformInfo & TTI,SCCPSolver & Solver) InstCostVisitor() argument
160 SCCPSolver &Solver; global() variable
[all...] |
| /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 | 99 static bool refineInstruction(SCCPSolver &Solver, in refineInstruction() argument
103 auto GetRange = [&Solver, &InsertedValues](Value *Op) { in refineInstruction()
110 return Solver.getLatticeValueFor(Op).asConstantRange( in refineInstruction()
168 static bool replaceSignedInst(SCCPSolver &Solver, in replaceSignedInst() argument
172 auto isNonNegative = [&Solver](Value *V) { in replaceSignedInst()
179 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V); in replaceSignedInst()
232 Solver.removeLatticeValueFor(&Inst); in replaceSignedInst()
|
| /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…
|