//===-- 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/AST/ExprCXX.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;

}

AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {

  AtomicBoolValue &Token = createAtomicBoolValue();

  FlowConditionRemainingConjuncts[&Token] = {};

  FlowConditionFirstConjuncts[&Token] = &Token;

  return Token;

}

void DataflowAnalysisContext::addFlowConditionConstraint(

    AtomicBoolValue &Token, BoolValue &Constraint) {

  FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue(

      Constraint, getOrCreateNegationValue(Token)));

  FlowConditionFirstConjuncts[&Token] =

      &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token],

                                   getOrCreateNegationValue(Constraint));

}

AtomicBoolValue &

DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {

  auto &ForkToken = makeFlowConditionToken();

  FlowConditionDeps[&ForkToken].insert(&Token);

  addFlowConditionConstraint(ForkToken, Token);

  return ForkToken;

}

AtomicBoolValue &

DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,

                                            AtomicBoolValue &SecondToken) {

  auto &Token = makeFlowConditionToken();

  FlowConditionDeps[&Token].insert(&FirstToken);

  FlowConditionDeps[&Token].insert(&SecondToken);

  addFlowConditionConstraint(

      Token, getOrCreateDisjunctionValue(FirstToken, SecondToken));

  return Token;

}

bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,

                                                   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 = {

      &Token,

      &getBoolLiteralValue(true),

      &getOrCreateNegationValue(getBoolLiteralValue(false)),

      &getOrCreateNegationValue(Val),

  };

  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;

  addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);

  return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;

}

bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {

  // Returns true if and only if we cannot prove that the flow condition can

  // ever be false.

  llvm::DenseSet<BoolValue *> Constraints = {

      &getBoolLiteralValue(true),

      &getOrCreateNegationValue(getBoolLiteralValue(false)),

      &getOrCreateNegationValue(Token),

  };

  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;

  addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);

  return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;

}

void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(

    AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,

    llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {

  auto Res = VisitedTokens.insert(&Token);

  if (!Res.second)

    return;

  auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);

  if (FirstConjunctIT != FlowConditionFirstConjuncts.end())

    Constraints.insert(FirstConjunctIT->second);

  auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);

  if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())

    Constraints.insert(RemainingConjunctsIT->second.begin(),

                       RemainingConjunctsIT->second.end());

  auto DepsIT = FlowConditionDeps.find(&Token);

  if (DepsIT != FlowConditionDeps.end()) {

    for (AtomicBoolValue *DepToken : DepsIT->second)

      addTransitiveFlowConditionConstraints(*DepToken, Constraints,

                                            VisitedTokens);

  }

}

} // namespace dataflow

} // namespace clang

using namespace clang;

const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {

  const Expr *Current = &E;

  if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {

    Current = EWC->getSubExpr();

    assert(Current != nullptr);

  }

  Current = Current->IgnoreParens();

  assert(Current != nullptr);

  return *Current;

}

const Stmt &clang::dataflow::ignoreCFGOmittedNodes(const Stmt &S) {

  if (auto *E = dyn_cast<Expr>(&S))

    return ignoreCFGOmittedNodes(*E);

  return S;

}