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

//===-- Value.h -------------------------------------------------*- 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
//
//===----------------------------------------------------------------------===//
//
// This file defines classes for values computed by abstract interpretation
// during dataflow analysis.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H

#include "clang/AST/Decl.h"
#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
#include <cassert>
#include <utility>

namespace clang {
namespace dataflow {

/// Base class for all values computed by abstract interpretation.
///
/// Don't use `Value` instances by value. All `Value` instances are allocated
/// and owned by `DataflowAnalysisContext`.
class Value { … };

/// An equivalence relation for values. It obeys reflexivity, symmetry and
/// transitivity. It does *not* include comparison of `Properties`.
///
/// Computes equivalence for these subclasses:
/// * PointerValue -- pointee locations are equal. Does not compute deep
///   equality of `Value` at said location.
/// * TopBoolValue -- both are `TopBoolValue`s.
///
/// Otherwise, falls back to pointer equality.
bool areEquivalentValues(const Value &Val1, const Value &Val2);

/// Models a boolean.
class BoolValue : public Value { … };

/// A TopBoolValue represents a boolean that is explicitly unconstrained.
///
/// This is equivalent to an AtomicBoolValue that does not appear anywhere
/// else in a system of formula.
/// Knowing the value is unconstrained is useful when e.g. reasoning about
/// convergence.
class TopBoolValue final : public BoolValue { … };

/// Models an atomic boolean.
///
/// FIXME: Merge this class into FormulaBoolValue.
///        When we want to specify atom identity, use Atom.
class AtomicBoolValue final : public BoolValue { … };

/// Models a compound boolean formula.
class FormulaBoolValue final : public BoolValue { … };

/// Models an integer.
class IntegerValue : public Value { … };

/// Models a symbolic pointer. Specifically, any value of type `T*`.
class PointerValue final : public Value { … };

raw_ostream &operator<<(raw_ostream &OS, const Value &Val);

} // namespace dataflow
} // namespace clang

#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H