Skip to content

Commit 81374cd

Browse files
kumarakkumarak
committed
support for static contract dialect as attribute
1 parent eaa7c7c commit 81374cd

File tree

15 files changed

+321
-5
lines changed

15 files changed

+321
-5
lines changed

‎include/patchestry/Dialect/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,3 +4,4 @@
44
# LICENSE file found in the root directory of this source tree.
55

66
add_subdirectory(Pcode)
7+
add_subdirectory(Contracts)

‎include/patchestry/Dialect/Contracts/CMakeLists.txt‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
# Copyright (c) 2025, Trail of Bits, Inc.
2+
#
3+
# This source code is licensed in accordance with the terms specified in the
4+
# LICENSE file found in the root directory of this source tree.
5+
6+
set(LLVM_TARGET_DEFINITIONS Contract.td)
7+
mlir_tablegen(contracts/ContractsDialect.h.inc -gen-dialect-decls -dialect=contracts)
8+
mlir_tablegen(contracts/ContractsDialect.cpp.inc -gen-dialect-defs -dialect=contracts)
9+
mlir_tablegen(contracts/ContractsEnums.h.inc -gen-enum-decls)
10+
mlir_tablegen(contracts/ContractsEnums.cpp.inc -gen-enum-defs)
11+
mlir_tablegen(contracts/ContractsAttrs.h.inc -gen-attrdef-decls)
12+
mlir_tablegen(contracts/ContractsAttrs.cpp.inc -gen-attrdef-defs)
13+
add_public_tablegen_target(MLIRContractsIncGen)
14+
15+
if (DEFINED MLIR_BINARY_DIR)
16+
set(MLIR_OLD_ROOT ${MLIR_BINARY_DIR})
17+
endif()
18+
19+
set(MLIR_BINARY_DIR ${PATCHESTRY_BINARY_DIR})
20+
add_mlir_doc(Contract Contracts Dialects/ -gen-dialect-doc -dialect=contracts)
21+
22+
if (DEFINED MLIR_OLD_ROOT)
23+
set(MLIR_BINARY_DIR ${MLIR_OLD_ROOT})
24+
endif()

‎include/patchestry/Dialect/Contracts/Contract.td‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
/*
2+
* Copyright (c) 2025, Trail of Bits, Inc.
3+
*
4+
* This source code is licensed in accordance with the terms specified in
5+
* the LICENSE file found in the root directory of this source tree.
6+
*/
7+
8+
#ifndef CONTRACT_DIALECT
9+
#define CONTRACT_DIALECT
10+
11+
include "mlir/IR/OpBase.td"
12+
include "mlir/IR/AttrTypeBase.td"
13+
include "mlir/IR/EnumAttr.td"
14+
15+
// Dialect
16+
def Contract_Dialect : Dialect {
17+
let name = "contracts";
18+
let cppNamespace = "contracts";
19+
let summary = "Static contracts as attributes";
20+
let description = [{ Declarative pre/post conditions attached to operations. }];
21+
}
22+
23+
// cmp predicate
24+
def CmpKind : I32EnumAttr<"CmpKind", "comparison predicate", [
25+
I32EnumAttrCase<"eq", 0>,
26+
I32EnumAttrCase<"ne", 1>,
27+
I32EnumAttrCase<"slt", 2>,
28+
I32EnumAttrCase<"sle", 3>,
29+
I32EnumAttrCase<"sgt", 4>,
30+
I32EnumAttrCase<"sge", 5>,
31+
I32EnumAttrCase<"ult", 6>,
32+
I32EnumAttrCase<"ule", 7>,
33+
I32EnumAttrCase<"ugt", 8>,
34+
I32EnumAttrCase<"uge", 9>
35+
]> { let cppNamespace = "::contracts"; }
36+
37+
// Positional operand reference: $0, $1, ...
38+
def VarRefAttr : AttrDef<Contract_Dialect, "varref"> {
39+
let summary = "Positional operand reference";
40+
let parameters = (ins "uint64_t":$index);
41+
let mnemonic = "varref";
42+
let assemblyFormat = "`<` $index `>`";
43+
}
44+
45+
// Integer literal
46+
def ConstIntAttr : AttrDef<Contract_Dialect, "iconst"> {
47+
let summary = "Integer constant";
48+
let parameters = (ins "mlir::IntegerAttr":$value);
49+
let mnemonic = "iconst";
50+
let assemblyFormat = "`<` $value `>`";
51+
}
52+
53+
// cmp clause: (lhs pred rhs) where rhs is var or const
54+
def CmpClauseAttr : AttrDef<Contract_Dialect, "cmp"> {
55+
let summary = "Integer comparison clause";
56+
let parameters = (ins
57+
"::contracts::CmpKind":$pred,
58+
"::contracts::VarRefAttr":$lhs,
59+
OptionalParameter<"::contracts::VarRefAttr">:$rhsVar,
60+
OptionalParameter<"::contracts::ConstIntAttr">:$rhsConst
61+
);
62+
let mnemonic = "cmp";
63+
let genVerifyDecl = 1;
64+
let assemblyFormat = "`<` $pred `,` $lhs (`,` $rhsVar^)? (`,` $rhsConst^)? `>`";
65+
}
66+
67+
// Boolean aggregators
68+
def AllOfAttr : AttrDef<Contract_Dialect, "all_of"> {
69+
let summary = "Conjunction of clauses";
70+
let parameters = (ins ArrayRefParameter<"mlir::Attribute">:$clauses);
71+
let mnemonic = "all_of";
72+
let assemblyFormat = "`<` `[` $clauses `]` `>`";
73+
}
74+
def AnyOfAttr : AttrDef<Contract_Dialect, "any_of"> {
75+
let summary = "Disjunction of clauses";
76+
let parameters = (ins ArrayRefParameter<"mlir::Attribute">:$clauses);
77+
let mnemonic = "any_of";
78+
let assemblyFormat = "`<` `[` $clauses `]` `>`";
79+
}
80+
81+
// Top-level contract you attach to an op
82+
def StaticContractAttr : AttrDef<Contract_Dialect, "static"> {
83+
let summary = "Static contract container";
84+
let parameters = (ins
85+
"mlir::StringAttr":$message,
86+
"mlir::Attribute":$expr // CmpClauseAttr | AllOfAttr | AnyOfAttr
87+
);
88+
let mnemonic = "static";
89+
let genVerifyDecl = 1;
90+
let assemblyFormat = "`<` `message` `=` $message `,` $expr `>`";
91+
}
92+
93+
#endif // CONTRACT_DIALECT

‎include/patchestry/Dialect/Contracts/ContractsDialect.hpp‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/*
2+
* Copyright (c) 2025, Trail of Bits, Inc.
3+
*
4+
* This source code is licensed in accordance with the terms specified in
5+
* the LICENSE file found in the root directory of this source tree.
6+
*/
7+
8+
#pragma once
9+
10+
#include <mlir/IR/BuiltinAttributes.h>
11+
#include <mlir/IR/Dialect.h>
12+
#include <mlir/IR/OpDefinition.h>
13+
14+
namespace contracts {
15+
class ContractsDialect : public mlir::Dialect
16+
{
17+
public:
18+
explicit ContractsDialect(mlir::MLIRContext *context);
19+
20+
static constexpr mlir::StringRef getDialectNamespace() { return "contracts"; }
21+
22+
void initialize();
23+
};
24+
} // namespace contracts
25+
26+
// Pull in the dialect definition.
27+
#include "patchestry/Dialect/Contracts/ContractsDialect.h.inc"
28+
29+
// Pull in enum definitions
30+
#include "patchestry/Dialect/Contracts/contracts/ContractsEnums.h.inc"
31+
32+
// Forward declarations for attributes (before including the generated code)
33+
namespace contracts {
34+
class varrefAttr;
35+
class iconstAttr;
36+
class cmpAttr;
37+
class all_ofAttr;
38+
class any_ofAttr;
39+
class staticAttr;
40+
41+
// Provide aliases matching the generated C++ accessor names.
42+
using VarRefAttr = varrefAttr;
43+
using ConstIntAttr = iconstAttr;
44+
using CmpClauseAttr = cmpAttr;
45+
using AllOfAttr = all_ofAttr;
46+
using AnyOfAttr = any_ofAttr;
47+
using StaticContractAttr = staticAttr;
48+
} // namespace contracts
49+
50+
// Pull in attribute definitions
51+
#define GET_ATTRDEF_CLASSES
52+
#include "patchestry/Dialect/Contracts/contracts/ContractsAttrs.h.inc"

‎lib/patchestry/Dialect/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,5 @@
33
# This source code is licensed in accordance with the terms specified in the
44
# LICENSE file found in the root directory of this source tree.
55

6+
add_subdirectory(Contracts)
67
add_subdirectory(Pcode)

‎lib/patchestry/Dialect/Contracts/CMakeLists.txt‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
# Copyright (c) 2025, Trail of Bits, Inc.
2+
#
3+
# This source code is licensed in accordance with the terms specified in the
4+
# LICENSE file found in the root directory of this source tree.
5+
6+
add_mlir_dialect_library(MLIRContracts
7+
ContractsDialect.cpp
8+
ContractsAttrs.cpp
9+
10+
ADDITIONAL_HEADER_DIRS
11+
${PROJECT_SOURCE_DIR}/include/patchestry
12+
DEPENDS
13+
MLIRContractsIncGen
14+
LINK_LIBS
15+
patchestry_settings
16+
PUBLIC
17+
MLIRIR
18+
MLIRInferTypeOpInterface
19+
)
20+
21+
target_include_directories(obj.MLIRContracts PRIVATE
22+
${PROJECT_SOURCE_DIR}/include/patchestry/Dialect/Contracts
23+
${PROJECT_BINARY_DIR}/include/patchestry/Dialect/Contracts
24+
)

‎lib/patchestry/Dialect/Contracts/ContractsAttrs.cpp‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
/*
2+
* Copyright (c) 2025, Trail of Bits, Inc.
3+
*
4+
* This source code is licensed in accordance with the terms specified in
5+
* the LICENSE file found in the root directory of this source tree.
6+
*/
7+
8+
#include "patchestry/Dialect/Contracts/ContractsDialect.hpp"
9+
#include "mlir/IR/Diagnostics.h"
10+
11+
using namespace mlir;
12+
using namespace contracts;
13+
14+
// Verify: exactly one of rhsVar or rhsConst
15+
static LogicalResult verifyCmpClauseAttr(
16+
CmpKind pred, VarRefAttr lhs, VarRefAttr rhsVar, ConstIntAttr rhsConst,
17+
function_ref< InFlightDiagnostic() > emitError
18+
) {
19+
bool hasVar = static_cast< bool >(rhsVar);
20+
bool hasConst = static_cast< bool >(rhsConst);
21+
if (hasVar == hasConst) {
22+
return emitError() << "`cmp` needs exactly one of rhsVar or rhsConst";
23+
}
24+
return success();
25+
}
26+
27+
LogicalResult cmpAttr::verify(
28+
function_ref< InFlightDiagnostic() > emitError, CmpKind pred, VarRefAttr lhs,
29+
VarRefAttr rhsVar, ConstIntAttr rhsConst
30+
) {
31+
return verifyCmpClauseAttr(pred, lhs, rhsVar, rhsConst, emitError);
32+
}
33+
34+
LogicalResult staticAttr::verify(
35+
function_ref< InFlightDiagnostic() > emitError, mlir::StringAttr message,
36+
mlir::Attribute expr
37+
) {
38+
if (!llvm::isa< cmpAttr, all_ofAttr, any_ofAttr >(expr)) {
39+
return emitError() << "expr must be cmp/all_of/any_of";
40+
}
41+
if (auto c = llvm::dyn_cast< cmpAttr >(expr)) {
42+
if (failed(verifyCmpClauseAttr(
43+
c.getPred(), c.getLhs(), c.getRhsVar(), c.getRhsConst(), emitError
44+
)))
45+
{
46+
return failure();
47+
}
48+
}
49+
return success();
50+
}

‎lib/patchestry/Dialect/Contracts/ContractsDialect.cpp‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/*
2+
* Copyright (c) 2025, Trail of Bits, Inc.
3+
*
4+
* This source code is licensed in accordance with the terms specified in
5+
* the LICENSE file found in the root directory of this source tree.
6+
*/
7+
8+
#include "patchestry/Dialect/Contracts/ContractsDialect.hpp"
9+
#include "mlir/IR/Builders.h"
10+
#include "mlir/IR/DialectImplementation.h"
11+
#include "llvm/ADT/TypeSwitch.h"
12+
13+
// Pull in enum definitions
14+
#include "contracts/ContractsEnums.cpp.inc"
15+
16+
// Pull in attribute definitions
17+
#define GET_ATTRDEF_CLASSES
18+
#include "contracts/ContractsAttrs.cpp.inc"
19+
20+
using namespace mlir;
21+
using namespace contracts;
22+
23+
ContractsDialect::ContractsDialect(MLIRContext *ctx)
24+
: Dialect(getDialectNamespace(), ctx, mlir::TypeID::get< ContractsDialect >()) {
25+
addAttributes<
26+
#define GET_ATTRDEF_LIST
27+
#include "contracts/ContractsAttrs.h.inc"
28+
>();
29+
}
30+
31+
void ContractsDialect::initialize() {
32+
// Nothing else for attributes-only initial bring-up
33+
}

‎lib/patchestry/Passes/CMakeLists.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ set(CLANG_IR_LIBS
1717
)
1818

1919
target_link_libraries(patchestry_passes
20+
PUBLIC
21+
MLIRContracts
2022
PRIVATE
2123
patchestry_settings
2224
patchestry_yaml

‎lib/patchestry/Passes/InstrumentationPass.cpp‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@
5252
#include <mlir/Pass/PassRegistry.h>
5353
#include <mlir/Support/LLVM.h>
5454

55+
#include <patchestry/Dialect/Contracts/ContractsDialect.hpp>
5556
#include <patchestry/Passes/InstrumentationPass.hpp>
5657
#include <patchestry/Passes/OperationMatcher.hpp>
5758
#include <patchestry/Util/Log.hpp>
@@ -1994,6 +1995,31 @@ don't yet pass)
19941995
function_args
19951996
);
19961997

1998+
// Set contract metadata as a dictionary attribute
1999+
auto ctx = target_op->getContext();
2000+
2001+
// Create a dictionary attribute for the contract spec
2002+
llvm::SmallVector< mlir::NamedAttribute > specAttrs;
2003+
specAttrs.push_back(mlir::NamedAttribute(
2004+
mlir::StringAttr::get(ctx, "name"), mlir::StringAttr::get(ctx, spec.name)
2005+
));
2006+
specAttrs.push_back(mlir::NamedAttribute(
2007+
mlir::StringAttr::get(ctx, "id"), mlir::StringAttr::get(ctx, spec.id)
2008+
));
2009+
specAttrs.push_back(mlir::NamedAttribute(
2010+
mlir::StringAttr::get(ctx, "description"),
2011+
mlir::StringAttr::get(ctx, spec.description)
2012+
));
2013+
specAttrs.push_back(mlir::NamedAttribute(
2014+
mlir::StringAttr::get(ctx, "category"), mlir::StringAttr::get(ctx, spec.category)
2015+
));
2016+
specAttrs.push_back(mlir::NamedAttribute(
2017+
mlir::StringAttr::get(ctx, "severity"), mlir::StringAttr::get(ctx, spec.severity)
2018+
));
2019+
2020+
auto specDictAttr = mlir::DictionaryAttr::get(ctx, specAttrs);
2021+
contract_call_op->setAttr("contract.spec", specDictAttr);
2022+
19972023
// Set appropriate attributes based on operation type
19982024
set_instrumentation_call_attributes(contract_call_op, target_op);
19992025

0 commit comments

Comments
 (0)