| 174 | } |
| 175 | |
| 176 | std::optional<bool> SymbolicExprAnalyzer::Prove( |
| 177 | const ir::Expr& condition) const { |
| 178 | try { |
| 179 | if (condition.As<ir::EQ>()) { |
| 180 | return ProveEQ(condition.As<ir::EQ>()->a(), condition.As<ir::EQ>()->b()); |
| 181 | } |
| 182 | if (condition.As<ir::NE>()) { |
| 183 | return ProveNE(condition.As<ir::NE>()->a(), condition.As<ir::NE>()->b()); |
| 184 | } |
| 185 | if (condition.As<ir::GE>()) { |
| 186 | return ProveGE(condition.As<ir::GE>()->a(), condition.As<ir::GE>()->b()); |
| 187 | } |
| 188 | if (condition.As<ir::LE>()) { |
| 189 | return ProveLE(condition.As<ir::LE>()->a(), condition.As<ir::LE>()->b()); |
| 190 | } |
| 191 | if (condition.As<ir::GT>()) { |
| 192 | return ProveGT(condition.As<ir::GT>()->a(), condition.As<ir::GT>()->b()); |
| 193 | } |
| 194 | if (condition.As<ir::LT>()) { |
| 195 | return ProveLT(condition.As<ir::LT>()->a(), condition.As<ir::LT>()->b()); |
| 196 | } |
| 197 | return std::nullopt; |
| 198 | } catch (const ::common::enforce::EnforceNotMet& e) { |
| 199 | LOG(WARNING) << "Error occurred during integer calculation: " << e.what() |
| 200 | << ", so SymbolicExprAnalyzer cannot prove anything."; |
| 201 | return std::nullopt; |
| 202 | } |
| 203 | } |
| 204 | |
| 205 | std::optional<bool> SymbolicExprAnalyzer::ProveEQ(const ir::Expr& lhs, |
| 206 | const ir::Expr& rhs) const { |