ForbiddenPreconditionInfluence.h

Go to the documentation of this file.

//===-- ForbiddenPreconditionInfluence.h ------------------------*- C++ -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
// Copyright 2026 Project LLZK
// SPDX-License-Identifier: Apache-2.0
//
//===----------------------------------------------------------------------===//
//===----------------------------------------------------------------------===//
 
#pragma once
 
#include "llzk/Dialect/Verif/IR/Ops.h"
 
#include <mlir/Dialect/SCF/IR/SCF.h>
#include <mlir/Interfaces/CallInterfaces.h>
 
#include <llvm/ADT/DenseMap.h>
#include <llvm/ADT/DenseSet.h>
#include <llvm/ADT/SetVector.h>
#include <llvm/ADT/SmallVector.h>
 
#include <optional>
 
namespace llzk::verif {

enum class ForbiddenPreconditionInfluence : uint8_t {
  None = 0,
  StructMember = 1 << 0,
  FunctionReturn = 1 << 1,
};

struct ForbiddenPreconditionInfluenceInfo {
  ForbiddenPreconditionInfluence influence = ForbiddenPreconditionInfluence::None;
  llvm::SmallSetVector<mlir::Location, 2> structMemberLocs = {};
 
  bool operator==(const ForbiddenPreconditionInfluenceInfo &other) const {
    return influence == other.influence && structMemberLocs == other.structMemberLocs;
  }
 
  static ForbiddenPreconditionInfluenceInfo None() { return {}; }
 
  static ForbiddenPreconditionInfluenceInfo StructMember() {
    return {.influence = ForbiddenPreconditionInfluence::StructMember};
  }
 
  static ForbiddenPreconditionInfluenceInfo FunctionReturn() {
    return {.influence = ForbiddenPreconditionInfluence::FunctionReturn};
  }
};
 
inline llvm::hash_code hash_value(const ForbiddenPreconditionInfluenceInfo &info) {
  return llvm::hash_combine(
      info.influence,
      llvm::hash_combine_range(info.structMemberLocs.begin(), info.structMemberLocs.end())
  );
}
 
inline ForbiddenPreconditionInfluence
operator|(ForbiddenPreconditionInfluence lhs, ForbiddenPreconditionInfluence rhs) {
  return static_cast<ForbiddenPreconditionInfluence>(
      static_cast<uint8_t>(lhs) | static_cast<uint8_t>(rhs)
  );
}
 
inline ForbiddenPreconditionInfluence &
operator|=(ForbiddenPreconditionInfluence &lhs, ForbiddenPreconditionInfluence rhs) {
  lhs = lhs | rhs;
  return lhs;
}

inline bool any(ForbiddenPreconditionInfluence influence) {
  return static_cast<uint8_t>(influence) != 0;
}

inline bool
hasInfluence(ForbiddenPreconditionInfluence influence, ForbiddenPreconditionInfluence flag) {
  return (static_cast<uint8_t>(influence) & static_cast<uint8_t>(flag)) != 0;
}

inline ForbiddenPreconditionInfluenceInfo mergeInfluenceInfo(
    ForbiddenPreconditionInfluenceInfo lhs, const ForbiddenPreconditionInfluenceInfo &rhs
) {
  lhs.influence |= rhs.influence;
  lhs.structMemberLocs.insert(rhs.structMemberLocs.begin(), rhs.structMemberLocs.end());
  return lhs;
}
 
template <typename T, typename... Args>
inline ForbiddenPreconditionInfluenceInfo
mergeInfluenceInfo(const T &first, const T &next, Args... others) {
  T merged = mergeInfluenceInfo(first, next);
  return mergeInfluenceInfo(merged, others...);
}
 
namespace detail {
 
using Influence = ForbiddenPreconditionInfluence;
using InfluenceInfo = ForbiddenPreconditionInfluenceInfo;

struct CallableSummaryKey {
  mlir::Operation *callable {};
  llvm::SmallVector<InfluenceInfo> argInfluences;
  unsigned resultNumber {};
 
  bool operator==(const CallableSummaryKey &other) const {
    return callable == other.callable && resultNumber == other.resultNumber &&
           argInfluences == other.argInfluences;
  }
};
 
struct CallableSummaryKeyInfo : llvm::DenseMapInfo<CallableSummaryKey> {
  static CallableSummaryKey getEmptyKey() {
    return {llvm::DenseMapInfo<mlir::Operation *>::getEmptyKey(), {}, 0};
  }
 
  static CallableSummaryKey getTombstoneKey() {
    return {llvm::DenseMapInfo<mlir::Operation *>::getTombstoneKey(), {}, 0};
  }
 
  static unsigned getHashValue(const CallableSummaryKey &key) {
    return llvm::hash_combine(
        key.callable, key.resultNumber,
        llvm::hash_combine_range(key.argInfluences.begin(), key.argInfluences.end())
    );
  }
 
  static bool isEqual(const CallableSummaryKey &lhs, const CallableSummaryKey &rhs) {
    return lhs == rhs;
  }
};

struct IncludedContractFailure {
  std::optional<mlir::Location> preconditionLoc = std::nullopt;
  InfluenceInfo influenceInfo = InfluenceInfo::None();
};

struct IncludedContractSummary {
  llvm::SmallVector<IncludedContractFailure> failures;
 
  explicit operator bool() const { return !failures.empty(); }
};

struct IncludedContractSummaryKey {
  mlir::Operation *contract {};
  llvm::SmallVector<InfluenceInfo> argInfluences;
  InfluenceInfo inheritedControlInfluence = InfluenceInfo::None();
 
  bool operator==(const IncludedContractSummaryKey &other) const {
    return contract == other.contract && argInfluences == other.argInfluences &&
           inheritedControlInfluence == other.inheritedControlInfluence;
  }
};
 
struct IncludedContractSummaryKeyInfo : llvm::DenseMapInfo<IncludedContractSummaryKey> {
  static IncludedContractSummaryKey getEmptyKey() {
    return {llvm::DenseMapInfo<mlir::Operation *>::getEmptyKey(), {}};
  }
 
  static IncludedContractSummaryKey getTombstoneKey() {
    return {llvm::DenseMapInfo<mlir::Operation *>::getTombstoneKey(), {}};
  }
 
  static unsigned getHashValue(const IncludedContractSummaryKey &key) {
    return llvm::hash_combine(
        key.contract, key.inheritedControlInfluence,
        llvm::hash_combine_range(key.argInfluences.begin(), key.argInfluences.end())
    );
  }
 
  static bool
  isEqual(const IncludedContractSummaryKey &lhs, const IncludedContractSummaryKey &rhs) {
    return lhs == rhs;
  }
};

class ForbiddenInfluenceAnalyzer {
public:
  explicit ForbiddenInfluenceAnalyzer(mlir::ModuleOp owningModule) : module(owningModule) {}

  InfluenceInfo analyzeContractValue(verif::ContractOp contract, mlir::Value value);

  InfluenceInfo
  analyzePreconditionOp(verif::ContractOp contract, verif::PreconditionOpInterface preCondOp);

  InfluenceInfo analyzeCallableResult(
      mlir::CallableOpInterface callableOp, llvm::ArrayRef<InfluenceInfo> argInfluences,
      unsigned resultNumber
  );

  IncludedContractSummary analyzeIncludedContract(
      verif::ContractOp calleeContract, llvm::ArrayRef<InfluenceInfo> argInfluences,
      InfluenceInfo inheritedControlInfluence = InfluenceInfo::None()
  );

  IncludedContractSummary analyzeIncludedOp(verif::ContractOp contract, verif::IncludeOp includeOp);
 
private:
  class AnalysisFrame {
  public:
    AnalysisFrame(
        ForbiddenInfluenceAnalyzer &parentAnalyzer, mlir::CallableOpInterface callableOp,
        llvm::ArrayRef<InfluenceInfo> argInfluenceInfos,
        InfluenceInfo inheritedControlInfluence = InfluenceInfo::None()
    );

    InfluenceInfo analyzeValue(mlir::Value value);

    InfluenceInfo analyzePreconditionOp(verif::PreconditionOpInterface preCondOp);

    IncludedContractSummary analyzeIncludeOp(verif::IncludeOp includeOp);
 
  private:
    InfluenceInfo analyzeControlAncestors(mlir::Operation *op);

    InfluenceInfo analyzeAncestorControl(mlir::Operation *ancestor, mlir::Operation *nestedOp);

    InfluenceInfo analyzeBlockArgument(mlir::BlockArgument blockArg);

    InfluenceInfo analyzeCallResult(mlir::CallOpInterface call, mlir::OpResult callRes);

    InfluenceInfo analyzeIfResult(mlir::scf::IfOp ifOp, mlir::OpResult ifRes);

    InfluenceInfo analyzeForResult(mlir::scf::ForOp forOp, mlir::OpResult forRes);

    InfluenceInfo
    analyzeExecuteRegionResult(mlir::scf::ExecuteRegionOp execOp, mlir::OpResult execRes);

    InfluenceInfo analyzeWhileResult(mlir::scf::WhileOp whileOp, mlir::OpResult whileRes);
 
    ForbiddenInfluenceAnalyzer &analyzer;
    llvm::DenseMap<mlir::Value, InfluenceInfo> valueCache;
    llvm::DenseMap<mlir::Operation *, InfluenceInfo> controlAncestorCache;
    llvm::DenseSet<mlir::Value> activeValues;
    InfluenceInfo inheritedControlInfluence = InfluenceInfo::None();
  };

  static InfluenceInfo
  classifyContractArgument(verif::ContractOp contract, mlir::BlockArgument arg);
 
  mlir::ModuleOp module;
  llvm::DenseMap<CallableSummaryKey, InfluenceInfo, CallableSummaryKeyInfo> callableSummaryCache;
  llvm::DenseSet<CallableSummaryKey, CallableSummaryKeyInfo> activeSummaries;
  llvm::DenseMap<
      IncludedContractSummaryKey, IncludedContractSummary, IncludedContractSummaryKeyInfo>
      includedContractSummaryCache;
  llvm::DenseSet<IncludedContractSummaryKey, IncludedContractSummaryKeyInfo>
      activeIncludedSummaries;
  llvm::DenseMap<ContractOp, AnalysisFrame> cachedFrames;
};
 
} // namespace detail

inline ForbiddenPreconditionInfluenceInfo analyzeForbiddenPreconditionInfluenceInfo(
    mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value
) {
  return detail::ForbiddenInfluenceAnalyzer(module).analyzeContractValue(contract, value);
}

inline ForbiddenPreconditionInfluenceInfo analyzeForbiddenPreconditionOpInfluenceInfo(
    mlir::ModuleOp module, verif::ContractOp contract, verif::PreconditionOpInterface preCondOp
) {
  return detail::ForbiddenInfluenceAnalyzer(module).analyzePreconditionOp(contract, preCondOp);
}

inline ForbiddenPreconditionInfluence analyzeForbiddenPreconditionInfluence(
    mlir::ModuleOp module, verif::ContractOp contract, mlir::Value value
) {
  return analyzeForbiddenPreconditionInfluenceInfo(module, contract, value).influence;
}

inline ForbiddenPreconditionInfluenceInfo analyzeForbiddenPreconditionCallableResultInfo(
    mlir::ModuleOp module, mlir::CallableOpInterface callableOp,
    llvm::ArrayRef<ForbiddenPreconditionInfluenceInfo> argInfluences, unsigned resultNumber
) {
  return detail::ForbiddenInfluenceAnalyzer(module).analyzeCallableResult(
      callableOp, argInfluences, resultNumber
  );
}

inline ForbiddenPreconditionInfluence analyzeForbiddenPreconditionCallableResult(
    mlir::ModuleOp module, mlir::CallableOpInterface callableOp,
    llvm::ArrayRef<ForbiddenPreconditionInfluenceInfo> argInfluences, unsigned resultNumber
) {
  return analyzeForbiddenPreconditionCallableResultInfo(
             module, callableOp, argInfluences, resultNumber
  )
      .influence;
}

inline detail::IncludedContractSummary analyzeForbiddenIncludedContractSummary(
    mlir::ModuleOp module, verif::ContractOp calleeContract,
    llvm::ArrayRef<ForbiddenPreconditionInfluenceInfo> argInfluences
) {
  return detail::ForbiddenInfluenceAnalyzer(module).analyzeIncludedContract(
      calleeContract, argInfluences
  );
}

inline detail::IncludedContractSummary analyzeForbiddenIncludedOpSummary(
    mlir::ModuleOp module, verif::ContractOp contract, verif::IncludeOp includeOp
) {
  return detail::ForbiddenInfluenceAnalyzer(module).analyzeIncludedOp(contract, includeOp);
}
 
} // namespace llzk::verif