Analysis/FlowSensitive/Solver.h

0001 //===- Solver.h -------------------------------------------------*- C++ -*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  This file defines an interface for a SAT solver that can be used by
0010 //  dataflow analyses.
0011 //
0012 //===----------------------------------------------------------------------===//
0013
0014 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
0015 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
0016
0017 #include "clang/Analysis/FlowSensitive/Formula.h"
0018 #include "clang/Basic/LLVM.h"
0019 #include "llvm/ADT/ArrayRef.h"
0020 #include "llvm/ADT/DenseMap.h"
0021 #include <optional>
0022 #include <vector>
0023
0024 namespace clang {
0025 namespace dataflow {
0026
0027 /// An interface for a SAT solver that can be used by dataflow analyses.
0028 class Solver {
0029 public:
0030   struct Result {
0031     enum class Status {
0032       /// Indicates that there exists a satisfying assignment for a boolean
0033       /// formula.
0034       Satisfiable,
0035
0036       /// Indicates that there is no satisfying assignment for a boolean
0037       /// formula.
0038       Unsatisfiable,
0039
0040       /// Indicates that the solver gave up trying to find a satisfying
0041       /// assignment for a boolean formula.
0042       TimedOut,
0043     };
0044
0045     /// A boolean value is set to true or false in a truth assignment.
0046     enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 };
0047
0048     /// Constructs a result indicating that the queried boolean formula is
0049     /// satisfiable. The result will hold a solution found by the solver.
0050     static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
0051       return Result(Status::Satisfiable, std::move(Solution));
0052     }
0053
0054     /// Constructs a result indicating that the queried boolean formula is
0055     /// unsatisfiable.
0056     static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); }
0057
0058     /// Constructs a result indicating that satisfiability checking on the
0059     /// queried boolean formula was not completed.
0060     static Result TimedOut() { return Result(Status::TimedOut, {}); }
0061
0062     /// Returns the status of satisfiability checking on the queried boolean
0063     /// formula.
0064     Status getStatus() const { return SATCheckStatus; }
0065
0066     /// Returns a truth assignment to boolean values that satisfies the queried
0067     /// boolean formula if available. Otherwise, an empty optional is returned.
0068     std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
0069       return Solution;
0070     }
0071
0072   private:
0073     Result(Status SATCheckStatus,
0074            std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
0075         : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
0076
0077     Status SATCheckStatus;
0078     std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
0079   };
0080
0081   virtual ~Solver() = default;
0082
0083   /// Checks if the conjunction of `Vals` is satisfiable and returns the
0084   /// corresponding result.
0085   ///
0086   /// Requirements:
0087   ///
0088   ///  All elements in `Vals` must not be null.
0089   virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
0090
0091   // Did the solver reach its resource limit?
0092   virtual bool reachedLimit() const = 0;
0093 };
0094
0095 llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
0096 llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
0097
0098 } // namespace dataflow
0099 } // namespace clang
0100
0101 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H