Skip to content

Raghav/unsupported warn #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
raghav198 merged 11 commits into from
Sep 1, 2026
Merged

Raghav/unsupported warn #61

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
e7485d2
NOIR fixes
Aug 24, 2026
36c602b
If condition expr
Aug 26, 2026
48e4fe2
Subcmp arg expr
Aug 26, 2026
304656c
Propagate unsupported errors instead of crashing
Aug 26, 2026
e9b3d29
Script reports unsupported separately from errors
Aug 26, 2026
da7fb6a
logAllUnhandledErrors
Aug 26, 2026
ab75364
CR comment
Aug 31, 2026
6c6305f
Merge branch 'raghav/noir-fixes' into raghav/unsupported-warn
Aug 31, 2026
ac5308c
Use exceptions instead
Aug 31, 2026
307a32c
Remove dead function from header
Aug 31, 2026
aee0470
Merge branch 'main' into raghav/unsupported-warn
raghav198 Aug 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions include/Verification/WeakestPrecondition.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#include "Verification/TermUtils.h"
#include <cvc5/cvc5.h>

#include <llvm/Support/Error.h>
#include <llvm/Support/LogicalResult.h>
#include <llvm/Support/raw_ostream.h>
#include <llzk/Dialect/Array/IR/Ops.h>
Expand Down Expand Up @@ -42,9 +43,9 @@ class WeakestPreconditionAnalysis {
TermBuilder builder;
mlir::SymbolTableCollection tables;

void calculateWP(mlir::scf::IfOp ifOp, ConjunctionTerm &postcondition);
void calculateWP(mlir::Operation *op, ConjunctionTerm &postcondition);
void calculateWP(mlir::Block *block, ConjunctionTerm &postcondition);
llvm::Error calculateWP(mlir::scf::IfOp ifOp, ConjunctionTerm &postcondition);
llvm::Error calculateWP(mlir::Operation *op, ConjunctionTerm &postcondition);
llvm::Error calculateWP(mlir::Block *block, ConjunctionTerm &postcondition);

mlir::DenseMap<mlir::Value, cvc5::Term> valueExpressions;

Expand All @@ -58,7 +59,7 @@ class WeakestPreconditionAnalysis {
});
}

llvm::FailureOr<cvc5::Term>
llvm::Expected<cvc5::Term>
computeInvariant(mlir::scf::ForOp loop, const ConjunctionTerm &postcondition);

public:
Expand All @@ -70,7 +71,7 @@ class WeakestPreconditionAnalysis {

ImplicationTerm getPostcondition();
void populateVerificationConditions();
cvc5::Term generateVerificationConditions();
llvm::Expected<cvc5::Term> generateVerificationConditions();

@chatgpt-codex-connector chatgpt-codex-connector Bot Aug 31, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Remove or restore the undefined population API

When downstream code uses the installed WeakestPreconditionAnalysis header and calls populateVerificationConditions(), compilation succeeds but linking now fails because this commit deletes the method's only definition while leaving its public declaration (and associated result fields) intact. Either retain an error-aware implementation or remove the obsolete declaration and state from the public API.

Useful? React with 👍 / 👎.


void applyStructContract(llzk::verif::ContractOp contract);
void addEquivalentMember(llzk::component::MemberDefOp memberDef);
Expand Down
5 changes: 2 additions & 3 deletions lib/Verification/TermUtils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -201,8 +201,7 @@ cvc5::Sort TermBuilder::_sort_of_type(Type type) {
ensure(it != subcmpSorts.end(), "unknown subcomponent type");
return it->second;
}
if (type.isSignlessInteger() &&
dyn_cast<IntegerType>(type).getIntOrFloatBitWidth() == 1) {
if (type.isSignlessInteger(1)) {
return mgr.getBooleanSort();
}
if (auto arrType = dyn_cast<array::ArrayType>(type)) {
Expand Down Expand Up @@ -520,7 +519,7 @@ cvc5::Term TermBuilder::initSubcmp(component::StructDefOp subcmp,
termArgs.reserve(args.size() + 1);

for (auto arg : args) {
termArgs.push_back(getConstant(arg));
termArgs.push_back(getExpression(arg));
}
return mgr.mkTerm(cvc5::Kind::APPLY_UF, termArgs);
}
Expand Down
Loading
Loading