//
// This file is distributed under the MIT License. See LICENSE.md for details.
//

#include "revng/Clift/ModuleVisitor.h"
#include "revng/CliftEmitC/CSemantics.h"

using namespace clift;

namespace {

static clift::PointerType getPointerOperationType(mlir::Operation *Op) {
  if (mlir::isa<PtrAddOp, PtrSubOp, AddressofOp>(Op))
    return clift::unwrapped_cast<PointerType>(Op->getResult(0).getType());

  if (mlir::isa<PtrDiffOp, IndirectionOp, SubscriptOp>(Op))
    return clift::unwrapped_cast<PointerType>(Op->getOperand(0).getType());

  if (auto A = mlir::dyn_cast<AccessOp>(Op); A and A.isIndirect())
    return clift::unwrapped_cast<PointerType>(A.getValue().getType());

  if (auto C = mlir::dyn_cast<DecayOp>(Op))
    return clift::unwrapped_cast<PointerType>(C.getResult().getType());

  if (auto C = mlir::dyn_cast<CallOp>(Op)) {
    if (auto T = clift::unwrapped_dyn_cast<PointerType>(C.getFunction()
                                                          .getType()))
      return T;
  }

  return {};
}

class CVerifier : public ModuleVisitor<CVerifier> {
  std::optional<CDataModel> DataModel;

public:
  mlir::LogicalResult visitNestedOp(mlir::Operation *Op) {
    if (auto T = getPointerOperationType(Op)) {
      if (T.getPointerSize() != DataModel->PointerSize)
        return getCurrentOp()->emitOpError() << "Pointer operation is not "
                                                "representable in the target "
                                                "implementation.";
    }

    if (mlir::isa<ImmediateOp>(Op)) {
      if (isPotentiallyPromotingType(Op->getResult(0).getType()))
        return Op->emitOpError() << " is not representable in the target"
                                 << " implementation.";
    }

    if (isPromotingOp(Op)) {
      if (isPotentiallyPromotingType(Op->getResult(0).getType()))
        return Op->emitOpError() << " causes integer promotion in the target"
                                    " implementation.";
    }

    if (isBooleanOp(Op)) {
      if (not isCanonicalBooleanType(Op->getResult(0).getType()))
        return Op->emitOpError() << " - not yielding the canonical boolean type"
                                 << " - is not representable in the target"
                                 << " implementation.";
    }

    return mlir::success();
  }

  mlir::LogicalResult visitModuleOp(mlir::ModuleOp Op) {
    DataModel = getDataModel(Op);
    return mlir::success();
  }

private:
  static bool isPromotingOp(mlir::Operation *Op) {
    return mlir::isa<NegOp,
                     AddOp,
                     SubOp,
                     MulOp,
                     DivOp,
                     RemOp,
                     BitwiseNotOp,
                     BitwiseAndOp,
                     BitwiseOrOp,
                     BitwiseXorOp,
                     ShiftLeftOp,
                     ShiftRightOp>(Op);
  }

  static bool isBooleanOp(mlir::Operation *Op) {
    return mlir::isa<LogicalNotOp,
                     LogicalAndOp,
                     LogicalOrOp,
                     CmpEqOp,
                     CmpNeOp,
                     CmpLtOp,
                     CmpGtOp,
                     CmpLeOp,
                     CmpGeOp>(Op);
  }

  bool isPotentiallyPromotingType(mlir::Type Type) {
    if (auto IntType = clift::unwrapped_dyn_cast<IntegerType>(Type))
      return IntType.getSize() < DataModel->getIntSize();
    return false;
  }

  bool isCanonicalBooleanType(mlir::Type Type) {
    if (auto IntType = clift::unwrapped_dyn_cast<IntegerType>(Type))
      return IntType.getSize() == DataModel->getIntSize();
    return false;
  }
};

} // namespace

mlir::LogicalResult verifyCSemantics(mlir::ModuleOp Module) {
  return CVerifier::visit(Module);
}