//===- SolverAnalysis.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
//
//===----------------------------------------------------------------------===//
//====  Copyright (c) 2015 Advanced Micro Devices, Inc.  All rights reserved.
//
//               Developed by: Advanced Micro Devices, Inc.
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// with the Software without restriction, including without limitation the
// rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
// sell copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// Redistributions of source code must retain the above copyright notice, this
// list of conditions and the following disclaimers.
//
// Redistributions in binary form must reproduce the above copyright notice,
// this list of conditions and the following disclaimers in the documentation
// and/or other materials provided with the distribution.
//
// Neither the names of Advanced Micro Devices, Inc., nor the names of its
// contributors may be used to endorse or promote products derived from this
// Software without specific prior written permission.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
// THE SOFTWARE.
//
//===----------------------------------------------------------------------===//
//
// Inline a function based on solver decision
//
//===----------------------------------------------------------------------===//

#ifdef LLVM_WITH_Z3
#ifndef LLVM_ANALYSIS_SOLVERANALYSIS_H
#define LLVM_ANALYSIS_SOLVERANALYSIS_H

#include "z3++.h"
#include "llvm/IR/Instructions.h"
#include "llvm/IR/PassManager.h"
#include "llvm/Pass.h"
#include "llvm/IR/Dominators.h"
#include <map>
#include <queue>
#include <set>
#include <stack>

namespace llvm {
class Module;

class SolverInfo {

public:
#if 0
  std::map<std::pair<std::string, std::string>, int> InlineData;
#else
  std::map<CallInst*, int> InlineData;
#endif
  bool invalidate(Module &M, const PreservedAnalyses &PA,
                  ModuleAnalysisManager::Invalidator &);
};

class SolverAnalysis : public AnalysisInfoMixin<SolverAnalysis>,
                       public SolverInfo {
  friend AnalysisInfoMixin<SolverAnalysis>;
  static AnalysisKey Key;

  unsigned int Profit; // Store profitability of a function.
  unsigned int Count;  // Couter for variable renaming
  unsigned int Depth;  // Track Depth of function calls
  unsigned int BBID; // Track number of basic block for which PC is calculated.
  std::set<Value *> MallocInst;
  std::map<Value *, int> AddrToMap;
  std::map<std::map<std::string, std::string>, int>
      CallSiteCount; // Number of time caller and callee pair visited.
  std::set<Function *>
      Processed; // Set of caller-callee pair which are analyzed.
  std::stack<int> ProfitStack; // For storing profit of a callsite if we
                               // encounter call inside it.
  std::set<Instruction *> Optimized; // Store already optimized instructions.

public:
  using Result = SolverInfo;

  void startFunction(Function *F, FunctionAnalysisManager &);
  std::string findName(std::string, StringRef, Value *);
  bool analyze(Function *, CallInst *, z3::context *, z3::solver, z3::solver,
               FunctionAnalysisManager &);
  z3::expr createExpr(Value *, CallInst *, z3::context *, z3::solver, bool,
                      std::string);
  void visitCall(CallInst *, z3::context *, z3::solver, z3::solver,
                 FunctionAnalysisManager &);
  z3::expr createExprOfIncomingValue(Value *, z3::context *, z3::solver, std::string);
  z3::expr visit(Instruction *, CallInst *, z3::context *, z3::solver, bool, DominatorTree &);
  void updatePathConstraintOnArgs(CallInst *, z3::context *, z3::solver,
                                  z3::solver);
  z3::expr implicationFormula(z3::expr, z3::context *, z3::solver);
  z3::expr visitBasicBlock(BasicBlock *, std::queue<Instruction *> *,
                           std::vector<z3::expr> *,
                           std::map<BasicBlock *, unsigned int> *,
                           z3::context *, z3::solver, z3::solver, DominatorTree &);
  void visitBranchCaller(BranchInst *, std::vector<z3::expr> *,
                         std::map<BasicBlock *, unsigned int> *, z3::context *,
                         z3::solver, z3::solver, DominatorTree &);
  void createPropertyTable(Function *F, CallInst *, z3::context *, z3::solver,
                           z3::solver, FunctionAnalysisManager &);
  void assignBlockExpr(BasicBlock *, std::vector<z3::expr> *,
                       std::map<BasicBlock *, unsigned int> *, z3::expr);

  Result run(Module &M, ModuleAnalysisManager &AM);
};

class SolverInfoWrapperPass : public ModulePass {
  SolverInfo SI;

public:
  static char ID;
};
} // namespace llvm
#endif
#else
#ifndef LLVM_ANALYSIS_SOLVERANALYSIS_H
#define LLVM_ANALYSIS_SOLVERANALYSIS_H
class SolverInfo {};
#endif
#endif
