Raghav/unsupported warn - #61
Conversation
|
@codex review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e9b3d2954f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if (auto err = verificationConditions.takeError()) { | ||
| llvm::errs() << err << "\n"; | ||
| return; |
There was a problem hiding this comment.
When an unsupported construct reaches this branch in a build with LLVM_ENABLE_ABI_BREAKING_CHECKS enabled, streaming err only logs its payload; it does not consume the llvm::Error. The still-failing error is then destroyed on return and calls fatalUncheckedError(), so the newly supported graceful path aborts instead. Consume it while reporting, for example with llvm::logAllUnhandledErrors(std::move(err), llvm::errs()).
Useful? React with 👍 / 👎.
|
@codex review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6c6305fc84
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| .Default([this, &postcondition](auto op) { | ||
| auto expression = builder.getExpression(op->getResult(0)); | ||
| postcondition.substitute(builder.getConstant(op->getResult(0)), | ||
| expression); | ||
| // The default case is just an expression op, but we shouldn't have to | ||
| // do anything here because any places that use the result have already | ||
| // called `builder.getExpression()` on the result so there shouldn't be | ||
| // anything to substitute. | ||
| return llvm::Error::success(); |
There was a problem hiding this comment.
When an scf.if condition is produced by an operation such as bool.cmp rather than supplied as a block argument, calculateWP(scf::IfOp) still records it with builder.getConstant(). Making the default expression-op case a no-op means the defining operation never substitutes that constant with its expression, so the SMT condition becomes an unconstrained Boolean and the solver can select a branch independently of the comparison, producing incorrect verification results. Restore the substitution here or use getExpression() when constructing the branch condition.
Useful? React with 👍 / 👎.
| } else if (!call.calleeIsStructProduct()) { | ||
| // Technically a call to @product has already aligned the | ||
| // subcomponent values so there's nothing to prove | ||
| return llvm::createStringError( | ||
| "Unsupported: arbitrary function calls"); |
There was a problem hiding this comment.
When an unsupported value-returning function call feeds an equality, member write, or another expression, reverse traversal processes that user first and builder.getExpression() enters the function::CallOp handler in TermUtils.cpp, whose ensure still aborts for arbitrary callees. Consequently this new Error branch is never reached for the common case where the call result is used, so those inputs still crash instead of taking the intended graceful unsupported path; unsupported calls need to be detected before expression expansion or represented as a propagated error there as well.
Useful? React with 👍 / 👎.
| void populateVerificationConditions(); | ||
| cvc5::Term generateVerificationConditions(); | ||
| llvm::Expected<cvc5::Term> generateVerificationConditions(); |
There was a problem hiding this comment.
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 👍 / 👎.
|
@raghav198 it looks like I'm reviewing some of the same changes as https://github.com/project-llzk/LLEQ/pull/60/changes. Could you either change the base branch here or merge the other approved one to main and main to here so I'm not duplicating effort? |
Done; I realized there was going to be a lot of merge conflicts between the two so I figured I'd try to resolve those first and merge them into here. |
2 participants
No description provided.