| /freebsd-14.2/contrib/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 95 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && in fromBinOp()
104 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS); in fromBinOp()
107 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS); in fromBinOp()
121 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS); in fromBinOp()
125 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS); in fromBinOp()
128 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS); in fromBinOp()
131 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS); in fromBinOp()
134 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS); in fromBinOp()
205 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && in fromFloatBinOp()
292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth)); in fromCast()
[all …]
|
| H A D | SMTConstraintManager.h | 32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE() local
128 Solver->reset(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
132 std::optional<bool> isSat = Solver->check(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
137 if (!Solver->getInterpretation(Exp, Value)) in REGISTER_TRAIT_WITH_PROGRAMSTATE()
142 Solver, Exp, BO_NE, in REGISTER_TRAIT_WITH_PROGRAMSTATE()
147 Solver->addConstraint(NotExp); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
149 std::optional<bool> isNotSat = Solver->check(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
268 return Solver->isFPSupported(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
323 Solver->addConstraint(Constraint); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
341 Solver->reset(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
[all …]
|
| /freebsd-14.2/contrib/llvm-project/llvm/lib/Transforms/IPO/ |
| H A D | SCCP.cpp | 54 if (!Solver.isArgumentTrackedFunction(&F)) in findReturnsToZap()
57 if (Solver.mustPreserveReturn(&F)) { in findReturnsToZap()
68 [&Solver](User *U) { in findReturnsToZap()
130 Solver.addPredicateInfo(F, DT, AC); in runIPSCCP()
135 Solver.addTrackedFunction(&F); in runIPSCCP()
140 Solver.addArgumentTrackedFunction(&F); in runIPSCCP()
145 Solver.markBlockExecutable(&F.front()); in runIPSCCP()
149 Solver.markOverdefined(&AI); in runIPSCCP()
158 Solver.trackValueOfGlobalVariable(&G); in runIPSCCP()
162 Solver.solveWhileResolvedUndefsIn(M); in runIPSCCP()
[all …]
|
| H A D | FunctionSpecialization.cpp | 742 Solver.solveWhileResolvedUndefsIn(Clones); in run()
757 if (!Solver.isStructLatticeConstant(F, STy)) in run()
771 Solver.resetLatticeValueFor(CS); in run()
777 Solver.solveWhileResolvedUndefs(); in run()
840 if (!Solver.isBlockExecutable(CS.getParent())) in findSpecializations()
970 Solver.markBlockExecutable(&Clone->front()); in createSpecialization()
971 Solver.addArgumentTrackedFunction(Clone); in createSpecialization()
972 Solver.addTrackedFunction(Clone); in createSpecialization()
1085 C = Solver.getConstantOrNull(V); in getCandidateConstant()
1104 Solver.isBlockExecutable(CS->getParent())) in updateCallSites()
[all …]
|
| H A D | CalledValuePropagation.cpp | 372 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
378 Solver.MarkBlockExecutable(&F.front()); in runCVP()
382 Solver.Solve(); in runCVP()
390 CVPLatticeVal LV = Solver.getExistingValueState(RegI); in runCVP()
|
| /freebsd-14.2/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/ |
| H A D | DebugSupport.cpp | 44 Solver::Result::Assignment Assignment) { in operator <<()
46 case Solver::Result::Assignment::AssignedFalse: in operator <<()
48 case Solver::Result::Assignment::AssignedTrue: in operator <<()
54 llvm::StringRef debugString(Solver::Result::Status Status) { in debugString()
56 case Solver::Result::Status::Satisfiable: in debugString()
58 case Solver::Result::Status::Unsatisfiable: in debugString()
60 case Solver::Result::Status::TimedOut: in debugString()
66 llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) { in operator <<()
69 std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = { in operator <<()
|
| H A D | WatchedLiteralsSolver.cpp | 525 std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && { in solve()
529 return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations); in solve()
534 return std::make_pair(Solver::Result::TimedOut(), 0); in solve()
563 return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations); in solve()
620 return std::make_pair(Solver::Result::Satisfiable(buildSolution()), in solve()
626 llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() { in buildSolution()
627 llvm::DenseMap<Atom, Solver::Result::Assignment> Solution; in buildSolution()
634 ? Solver::Result::Assignment::AssignedFalse in buildSolution()
635 : Solver::Result::Assignment::AssignedTrue; in buildSolution()
786 Solver::Result
[all …]
|
| H A D | DataflowAnalysisContext.cpp | 170 Solver::Result DataflowAnalysisContext::querySolver( in querySolver()
340 DataflowAnalysisContext::DataflowAnalysisContext(std::unique_ptr<Solver> S, in DataflowAnalysisContext()
|
| /freebsd-14.2/contrib/llvm-project/llvm/include/llvm/CodeGen/PBQP/ |
| H A D | Graph.h | 358 Solver = &S; in setSolver()
379 if (Solver) in addNode()
398 if (Solver) in addNodeBypassingCostAllocator()
416 if (Solver) in addEdge()
441 if (Solver) in addEdgeBypassingCostAllocator()
468 if (Solver) in setNodeCosts()
510 if (Solver) in updateEdgeCosts()
586 if (Solver) in removeNode()
626 if (Solver) in disconnectEdge()
647 if (Solver) in reconnectEdge()
[all …]
|
| /freebsd-14.2/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-14.2/contrib/llvm-project/llvm/include/llvm/Transforms/IPO/ |
| H A D | FunctionSpecialization.h | 179 SCCPSolver &Solver; variable
196 TargetTransformInfo &TTI, SCCPSolver &Solver) in InstCostVisitor() argument
197 : DL(DL), BFI(BFI), TTI(TTI), Solver(Solver) {} in InstCostVisitor()
200 return Solver.isBlockExecutable(BB) && !DeadBlocks.contains(BB); in isBlockExecutable()
252 SCCPSolver &Solver; variable
273 SCCPSolver &Solver, Module &M, FunctionAnalysisManager *FAM, in FunctionSpecializer() argument
278 : Solver(Solver), M(M), FAM(FAM), GetBFI(GetBFI), GetTLI(GetTLI), in FunctionSpecializer()
288 return InstCostVisitor(M.getDataLayout(), BFI, TTI, Solver); in getInstCostVisitorFor()
|
| /freebsd-14.2/contrib/llvm-project/clang/include/clang/Analysis/FlowSensitive/ |
| H A D | Solver.h | 28 class Solver {
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 D | DataflowAnalysisContext.h | 93 DataflowAnalysisContext(std::unique_ptr<Solver> S,
198 Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
240 Solver::Result::Status::Satisfiable; in isSatisfiable()
247 Solver::Result::Status::Unsatisfiable; in isUnsatisfiable()
250 std::unique_ptr<Solver> S;
|
| H A D | DebugSupport.h | 31 llvm::StringRef debugString(Solver::Result::Status Status);
|
| H A D | WatchedLiteralsSolver.h | 30 class WatchedLiteralsSolver : public Solver {
|
| /freebsd-14.2/contrib/llvm-project/llvm/lib/Support/ |
| H A D | Z3Solver.cpp | 265 Z3_solver Solver; member in __anon13641eda0111::Z3Solver
274 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { in Z3Solver()
275 Z3_solver_inc_ref(Context.Context, Solver); in Z3Solver()
284 if (Solver) in ~Z3Solver()
285 Z3_solver_dec_ref(Context.Context, Solver); in ~Z3Solver()
289 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
846 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
874 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
888 return Z3_solver_pop(Context.Context, Solver, NumStates); in pop()
894 void reset() override { Z3_solver_reset(Context.Context, Solver); } in reset()
[all …]
|
| /freebsd-14.2/contrib/llvm-project/llvm/lib/Transforms/Utils/ |
| H A D | SCCPSolver.cpp | 107 static bool refineInstruction(SCCPSolver &Solver, in refineInstruction() argument
111 auto GetRange = [&Solver, &InsertedValues](Value *Op) { in refineInstruction()
118 return getConstantRange(Solver.getLatticeValueFor(Op), Op->getType(), in refineInstruction()
155 static bool replaceSignedInst(SCCPSolver &Solver, in replaceSignedInst() argument
159 auto isNonNegative = [&Solver](Value *V) { in replaceSignedInst()
166 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V); in replaceSignedInst()
216 Solver.removeLatticeValueFor(&Inst); in replaceSignedInst()
|
| /freebsd-14.2/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…
|