[clang][dataflow] Add flow condition constraints to Environment

This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.

Reviewed-by: ymandel, xazax.hun

Differential Revision: https://reviews.llvm.org/D120711

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

@@ -17,6 +17,7 @@
 
 #include "clang/AST/Decl.h"
 #include "clang/AST/Expr.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
@@ -33,9 +34,19 @@ namespace dataflow {
 /// is used during dataflow analysis.
 class DataflowAnalysisContext {
 public:
-  DataflowAnalysisContext()
-      : TrueVal(takeOwnership(std::make_unique<AtomicBoolValue>())),
-        FalseVal(takeOwnership(std::make_unique<AtomicBoolValue>())) {}
+  /// Constructs a dataflow analysis context.
+  ///
+  /// Requirements:
+  ///
+  ///  `S` must not be null.
+  DataflowAnalysisContext(std::unique_ptr<Solver> S)
+      : S(std::move(S)), TrueVal(createAtomicBoolValue()),
+        FalseVal(createAtomicBoolValue()) {
+    assert(this->S != nullptr);
+  }
+
+  /// Returns the SAT solver instance that is available in this context.
+  Solver &getSolver() const { return *S; }
 
   /// Takes ownership of `Loc` and returns a reference to it.
   ///
@@ -119,7 +130,30 @@ class DataflowAnalysisContext {
     return Value ? TrueVal : FalseVal;
   }
 
+  /// Creates an atomic boolean value.
+  AtomicBoolValue &createAtomicBoolValue() {
+    return takeOwnership(std::make_unique<AtomicBoolValue>());
+  }
+
+  /// Returns a boolean value that represents the conjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &getOrCreateConjunctionValue(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the disjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &getOrCreateDisjunctionValue(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the negation of `Val`. Subsequent
+  /// calls with the same argument will return the same result.
+  BoolValue &getOrCreateNegationValue(BoolValue &Val);
+
 private:
+  std::unique_ptr<Solver> S;
+
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
@@ -134,9 +168,16 @@ class DataflowAnalysisContext {
 
   StorageLocation *ThisPointeeLoc = nullptr;
 
-  // FIXME: Add support for boolean expressions.
   AtomicBoolValue &TrueVal;
   AtomicBoolValue &FalseVal;
+
+  // Indices that are used to avoid recreating the same composite boolean
+  // values.
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+      ConjunctionVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+      DisjunctionVals;
+  llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
 };
 
 } // namespace dataflow

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

@@ -235,6 +235,56 @@ class Environment {
     return DACtx->getBoolLiteralValue(Value);
   }
 
+  /// Returns an atomic boolean value.
+  BoolValue &makeAtomicBoolValue() { return DACtx->createAtomicBoolValue(); }
+
+  /// Returns a boolean value that represents the conjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) {
+    return DACtx->getOrCreateConjunctionValue(LHS, RHS);
+  }
+
+  /// Returns a boolean value that represents the disjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) {
+    return DACtx->getOrCreateDisjunctionValue(LHS, RHS);
+  }
+
+  /// Returns a boolean value that represents the negation of `Val`. Subsequent
+  /// calls with the same argument will return the same result.
+  BoolValue &makeNot(BoolValue &Val) {
+    return DACtx->getOrCreateNegationValue(Val);
+  }
+
+  /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
+  /// the same arguments, regardless of their order, will return the same
+  /// result. If the given boolean values represent the same value, the result
+  /// will be a value that represents the true boolean literal.
+  BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) {
+    return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(LHS), RHS);
+  }
+
+  /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
+  /// the same arguments, regardless of their order, will return the same
+  /// result. If the given boolean values represent the same value, the result
+  /// will be a value that represents the true boolean literal.
+  BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) {
+    return &LHS == &RHS
+               ? getBoolLiteralValue(true)
+               : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
+  }
+
+  /// Adds `Val` to the set of clauses that constitute the flow condition.
+  void addToFlowCondition(BoolValue &Val);
+
+  /// Returns true if and only if the clauses that constitute the flow condition
+  /// imply that `Val` is true.
+  bool flowConditionImplies(BoolValue &Val);
+
 private:
   /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
   /// return null.
@@ -272,7 +322,7 @@ class Environment {
                  std::pair<StructValue *, const ValueDecl *>>
       MemberLocToStruct;
 
-  // FIXME: Add flow condition constraints.
+  llvm::DenseSet<BoolValue *> FlowConditionConstraints;
 };
 
 } // namespace dataflow

clang/lib/Analysis/FlowSensitive/CMakeLists.txt

@@ -1,5 +1,6 @@
 add_clang_library(clangAnalysisFlowSensitive
   ControlFlowContext.cpp
+  DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

@@ -0,0 +1,68 @@
+//===-- DataflowAnalysisContext.cpp -----------------------------*- 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 a DataflowAnalysisContext class that owns objects that
+//  encompass the state of a program and stores context that is used during
+//  dataflow analysis.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include <cassert>
+#include <memory>
+#include <utility>
+
+namespace clang {
+namespace dataflow {
+
+static std::pair<BoolValue *, BoolValue *>
+makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+  auto Res = std::make_pair(&LHS, &RHS);
+  if (&RHS < &LHS)
+    std::swap(Res.first, Res.second);
+  return Res;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
+                                                     BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
+
+  auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
+  return *Res.first->second;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
+                                                     BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
+
+  auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
+  return *Res.first->second;
+}
+
+BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
+  auto Res = NegationVals.try_emplace(&Val, nullptr);
+  if (Res.second)
+    Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
+  return *Res.first->second;
+}
+
+} // namespace dataflow
+} // namespace clang

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

@@ -453,5 +453,24 @@ const StorageLocation &Environment::skip(const StorageLocation &Loc,
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
+void Environment::addToFlowCondition(BoolValue &Val) {
+  FlowConditionConstraints.insert(&Val);
+}
+
+bool Environment::flowConditionImplies(BoolValue &Val) {
+  // Returns true if and only if truth assignment of the flow condition implies
+  // that `Val` is also true. We prove whether or not this property holds by
+  // reducing the problem to satisfiability checking. In other words, we attempt
+  // to show that assuming `Val` is false makes the constraints induced by the
+  // flow condition unsatisfiable.
+  llvm::DenseSet<BoolValue *> Constraints = {
+      &makeNot(Val), &getBoolLiteralValue(true),
+      &makeNot(getBoolLiteralValue(false))};
+  Constraints.insert(FlowConditionConstraints.begin(),
+                     FlowConditionConstraints.end());
+  return DACtx->getSolver().solve(std::move(Constraints)) ==
+         Solver::Result::Unsatisfiable;
+}
+
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/CMakeLists.txt

@@ -4,6 +4,8 @@ set(LLVM_LINK_COMPONENTS
   )
 
 add_clang_unittest(ClangAnalysisFlowSensitiveTests
+  DataflowAnalysisContextTest.cpp
+  DataflowEnvironmentTest.cpp
   MapLatticeTest.cpp
   MultiVarConstantPropagationTest.cpp
   SingleVarConstantPropagationTest.cpp

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

@@ -0,0 +1,93 @@
+//===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp ---===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class DataflowAnalysisContextTest : public ::testing::Test {
+protected:
+  DataflowAnalysisContextTest()
+      : Context(std::make_unique<WatchedLiteralsSolver>()) {}
+
+  DataflowAnalysisContext Context;
+};
+
+TEST_F(DataflowAnalysisContextTest,
+       CreateAtomicBoolValueReturnsDistinctValues) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &XAndX = Context.getOrCreateConjunctionValue(X, X);
+  EXPECT_EQ(&XAndX, &X);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y);
+  auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y);
+  EXPECT_EQ(&XAndY1, &XAndY2);
+
+  auto &YAndX = Context.getOrCreateConjunctionValue(Y, X);
+  EXPECT_EQ(&XAndY1, &YAndX);
+
+  auto &Z = Context.createAtomicBoolValue();
+  auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z);
+  EXPECT_NE(&XAndY1, &XAndZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &XOrX = Context.getOrCreateDisjunctionValue(X, X);
+  EXPECT_EQ(&XOrX, &X);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y);
+  auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y);
+  EXPECT_EQ(&XOrY1, &XOrY2);
+
+  auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X);
+  EXPECT_EQ(&XOrY1, &YOrX);
+
+  auto &Z = Context.createAtomicBoolValue();
+  auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z);
+  EXPECT_NE(&XOrY1, &XOrZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &NotX1 = Context.getOrCreateNegationValue(X);
+  auto &NotX2 = Context.getOrCreateNegationValue(X);
+  EXPECT_EQ(&NotX1, &NotX2);
+
+  auto &Y = Context.createAtomicBoolValue();
+  auto &NotY = Context.getOrCreateNegationValue(Y);
+  EXPECT_NE(&NotX1, &NotY);
+}
+
+} // namespace