Support for static contracts embedding pre/post condition during instrumentation pass #107
Conversation
There was a problem hiding this comment.
Pull Request Overview
This PR adds comprehensive support for static contracts during the instrumentation pass, extending the existing runtime contract system. It introduces a new Contracts dialect with MLIR attributes to embed pre/post conditions directly into operations, enabling compile-time contract verification alongside runtime validation.
- Support for both static and runtime contract types with type-specific processing
- New Contracts MLIR dialect with attributes for static contract specifications
- Refactored patch and contract operation implementations into separate modules for better maintainability
Reviewed Changes
Copilot reviewed 25 out of 25 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
tools/*/CMakeLists.txt |
Added MLIRContracts library linking to all tools |
tools/patchir-transform/main.cpp |
Added Contracts dialect registration and context initialization |
test/patchir-transform/contracts/usb_security_contracts.yaml |
Extended test contracts with static contract examples |
test/patchir-transform/bl_usb__send_message_before_patch.yaml |
Updated test to use static contract ID |
lib/patchestry/Passes/PatchOperationImpl.* |
New implementation module for patch operations |
lib/patchestry/Passes/ContractOperationImpl.* |
New implementation module for contract operations |
lib/patchestry/Passes/InstrumentationPass.cpp |
Refactored to use new implementation modules and support static contracts |
lib/patchestry/Dialect/Contracts/* |
New Contracts dialect with attributes and tablegen definitions |
include/patchestry/YAML/ContractSpec.hpp |
Extended contract specification to support static contracts |
include/patchestry/YAML/BaseSpec.hpp |
Added ContractType enum for runtime/static distinction |
include/patchestry/Passes/*.hpp |
Updated headers for refactored implementation structure |
Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.
There was a problem hiding this comment.
Pull Request Overview
Copilot reviewed 27 out of 27 changed files in this pull request and generated 5 comments.
Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.
|
|
||
| default: | ||
| LOG(ERROR) << "Unsupported contract mode for static contracts: " | ||
| << infoModeToString(mode) << "\n"; |
There was a problem hiding this comment.
The function infoModeToString is called but it's not in scope. It should be contract::infoModeToString(mode) to use the function from the contract namespace.
| << infoModeToString(mode) << "\n"; | |
| << contracts::infoModeToString(mode) << "\n"; |
| const cl::opt< std::string > output_filename( // NOLINT(cert-err58-cpp) | ||
| "o", llvm::cl::desc("Output filename for the patched CIR"), llvm::cl::value_desc("filename"), | ||
| llvm::cl::init("-"), cl::cat(category) | ||
| "o", llvm::cl::desc("Output filename for the patched CIR"), | ||
| llvm::cl::value_desc("filename"), llvm::cl::init("-"), cl::cat(category) | ||
| ); |
There was a problem hiding this comment.
[nitpick] The line break changes appear to be only formatting changes that don't affect functionality. Consider using a consistent formatting style throughout the file.
| auto contracts_file_path = | ||
| ConfigurationFile::getInstance().resolve_path(spec.implementation.code_file); | ||
| ConfigurationFile::getInstance().resolve_path(spec.implementation->code_file); |
There was a problem hiding this comment.
Potential null pointer dereference. The code accesses spec.implementation->code_file without verifying that spec.implementation is not null, even though there's a check for !spec.implementation just above. The logic should be restructured to avoid this inconsistency.
| std::string severity; | ||
| Implementation implementation; | ||
| std::optional< std::string > contract_module; | ||
| ContractType type; // "STATIC" or "RUNTIME" |
There was a problem hiding this comment.
The comment should be updated to reflect that type is an enum value, not a string. It should read // ContractType::STATIC or ContractType::RUNTIME
| ContractType type; // "STATIC" or "RUNTIME" | |
| ContractType type; // ContractType::STATIC or ContractType::RUNTIME |
| targetAttr = ::contracts::TargetAttr::get( | ||
| ctx, pred.target, *pred.arg_index, mlir::FlatSymbolRefAttr() | ||
| ); | ||
| targetAttr.dump(); |
There was a problem hiding this comment.
This debug statement targetAttr.dump() should be removed as it appears to be leftover debugging code that will produce unwanted output in production.
| targetAttr.dump(); |
kumarak
force-pushed
the
static_contract
branch
from
73d0c79 to
9ba4bba
Compare
No description provided.