Coverage Report

Created: 2022-07-16 07:03

/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/Analysis/FlowSensitive/Solver.h
Line
Count
Source (jump to first uncovered line)
1
//===- Solver.h -------------------------------------------------*- C++ -*-===//
2
//
3
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4
// See https://llvm.org/LICENSE.txt for license information.
5
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6
//
7
//===----------------------------------------------------------------------===//
8
//
9
//  This file defines an interface for a SAT solver that can be used by
10
//  dataflow analyses.
11
//
12
//===----------------------------------------------------------------------===//
13
14
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
15
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
16
17
#include "clang/Analysis/FlowSensitive/Value.h"
18
#include "llvm/ADT/DenseMap.h"
19
#include "llvm/ADT/DenseSet.h"
20
#include "llvm/ADT/Optional.h"
21
22
namespace clang {
23
namespace dataflow {
24
25
/// An interface for a SAT solver that can be used by dataflow analyses.
26
class Solver {
27
public:
28
  struct Result {
29
    enum class Status {
30
      /// Indicates that there exists a satisfying assignment for a boolean
31
      /// formula.
32
      Satisfiable,
33
34
      /// Indicates that there is no satisfying assignment for a boolean
35
      /// formula.
36
      Unsatisfiable,
37
38
      /// Indicates that the solver gave up trying to find a satisfying
39
      /// assignment for a boolean formula.
40
      TimedOut,
41
    };
42
43
    /// A boolean value is set to true or false in a truth assignment.
44
    enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 };
45
46
    /// Constructs a result indicating that the queried boolean formula is
47
    /// satisfiable. The result will hold a solution found by the solver.
48
    static Result
49
337
    Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
50
337
      return Result(Status::Satisfiable, std::move(Solution));
51
337
    }
52
53
    /// Constructs a result indicating that the queried boolean formula is
54
    /// unsatisfiable.
55
379
    static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); }
56
57
    /// Constructs a result indicating that satisfiability checking on the
58
    /// queried boolean formula was not completed.
59
0
    static Result TimedOut() { return Result(Status::TimedOut, {}); }
60
61
    /// Returns the status of satisfiability checking on the queried boolean
62
    /// formula.
63
716
    Status getStatus() const { return SATCheckStatus; }
64
65
    /// Returns a truth assignment to boolean values that satisfies the queried
66
    /// boolean formula if available. Otherwise, an empty optional is returned.
67
    llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
68
28
    getSolution() const {
69
28
      return Solution;
70
28
    }
71
72
  private:
73
    Result(
74
        enum Status SATCheckStatus,
75
        llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
76
716
        : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
77
78
    Status SATCheckStatus;
79
    llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
80
  };
81
82
447
  virtual ~Solver() = default;
83
84
  /// Checks if the conjunction of `Vals` is satisfiable and returns the
85
  /// corresponding result.
86
  ///
87
  /// Requirements:
88
  ///
89
  ///  All elements in `Vals` must not be null.
90
  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0;
91
};
92
93
} // namespace dataflow
94
} // namespace clang
95
96
#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H