llvm/clang/include/clang/Analysis/FlowSensitive/Formula.h

//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H

#include "clang/Basic/LLVM.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseMapInfo.h"
#include "llvm/Support/Allocator.h"
#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <string>

namespace clang::dataflow {

/// Identifies an atomic boolean variable such as "V1".
///
/// This often represents an assertion that is interesting to the analysis but
/// cannot immediately be proven true or false. For example:
/// - V1 may mean "the program reaches this point",
/// - V2 may mean "the parameter was null"
///
/// We can use these variables in formulas to describe relationships we know
/// to be true: "if the parameter was null, the program reaches this point".
/// We also express hypotheses as formulas, and use a SAT solver to check
/// whether they are consistent with the known facts.
enum class Atom : unsigned { … };

/// A boolean expression such as "true" or "V1 & !V2".
/// Expressions may refer to boolean atomic variables. These should take a
/// consistent true/false value across the set of formulas being considered.
///
/// (Formulas are always expressions in terms of boolean variables rather than
/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
///
/// Simple formulas such as "true" and "V1" are self-contained.
/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
/// trailing objects.
/// For this reason, Formulas are Arena-allocated and over-aligned.
class Formula;
class alignas(const Formula *) Formula { … };

// The default names of atoms are V0, V1 etc in order of creation.
inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) { … }
inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) { … }

} // namespace clang::dataflow
namespace llvm {
template <> struct DenseMapInfo<clang::dataflow::Atom> { … };
} // namespace llvm
#endif