Commit 41ec2bc6 authored by Lei Wang's avatar Lei Wang Committed by LeiWang1999
Browse files

[Enhancement] Improve memory access condition checks in GlobalMemChecker (#591)

* [Enhancement] Improve memory access condition checks in GlobalMemChecker

- Updated the condition checks in the GlobalMemChecker to utilize symbolic bounds in the CanProve method, enhancing the accuracy of memory access validations.
- This change ensures that both upper and lower bound conditions are evaluated with improved proof strength, contributing to more robust memory access analysis.

* lintfix
parent 804735bf
...@@ -113,12 +113,14 @@ struct GlobalMemChecker : public StmtExprVisitor { ...@@ -113,12 +113,14 @@ struct GlobalMemChecker : public StmtExprVisitor {
// If analyzer->CanProve(index < shape_dim) returns false, // If analyzer->CanProve(index < shape_dim) returns false,
// it means we cannot prove the access is within bounds. // it means we cannot prove the access is within bounds.
PrimExpr upper_bound_cond = index < shape_dim; PrimExpr upper_bound_cond = index < shape_dim;
if (!analyzer_->CanProve(upper_bound_cond)) { if (!analyzer_->CanProve(upper_bound_cond,
arith::ProofStrength::kSymbolicBound)) {
_conditions.push_back(upper_bound_cond); _conditions.push_back(upper_bound_cond);
} }
// Check if index >= 0 can be proven. // Check if index >= 0 can be proven.
PrimExpr lower_bound_cond = index >= 0; PrimExpr lower_bound_cond = index >= 0;
if (!analyzer_->CanProve(lower_bound_cond)) { if (!analyzer_->CanProve(lower_bound_cond,
arith::ProofStrength::kSymbolicBound)) {
_conditions.push_back(lower_bound_cond); _conditions.push_back(lower_bound_cond);
} }
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment