michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/unifier): additional memory checks

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-20 17:37:42 -07:00
parent 28dad944c5
commit eb23a30626
1 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/unifier.cpp
View file

@ -485,7 +485,11 @@ struct unifier_fn {
} }
void check_system() { void check_system() {
check_interrupted(); ::lean::check_system("unifier");
}
void check_full() {
check_system();
if (m_num_steps > m_config.m_max_steps) if (m_num_steps > m_config.m_max_steps)
throw exception(sstream() << "unifier maximum number of steps (" << m_config.m_max_steps << ") exceeded, " << throw exception(sstream() << "unifier maximum number of steps (" << m_config.m_max_steps << ") exceeded, " <<
"the maximum number of steps can be increased by setting the option unifier.max_steps " << "the maximum number of steps can be increased by setting the option unifier.max_steps " <<
@ -867,6 +871,11 @@ struct unifier_fn {
expr instantiate_meta(expr e, justification & j) { expr instantiate_meta(expr e, justification & j) {
while (true) { while (true) {
if (auto p = m_subst.expand_metavar_app(e)) { if (auto p = m_subst.expand_metavar_app(e)) {
// The following check_system is defensive programming.
// If the unifier is correct, and no loops are introduced in the substituion,
// then this loop should always terminate.
// Anyway, we may have bugs, and we should interrupt the loop if all resources are being consumed.
check_system();
e = p->first; e = p->first;
j = mk_composite1(j, p->second); j = mk_composite1(j, p->second);
} else { } else {
@ -1112,7 +1121,7 @@ struct unifier_fn {
bool process_constraint(constraint const & c) { bool process_constraint(constraint const & c) {
if (in_conflict()) if (in_conflict())
return false; return false;
check_system(); check_full();
// std::cout << "process: " << c << "\n"; // std::cout << "process: " << c << "\n";
switch (c.kind()) { switch (c.kind()) {
case constraint_kind::Choice: case constraint_kind::Choice:
@ -1163,6 +1172,7 @@ struct unifier_fn {
bool resolve_conflict() { bool resolve_conflict() {
lean_assert(in_conflict()); lean_assert(in_conflict());
while (!m_case_splits.empty()) { while (!m_case_splits.empty()) {
check_system();
justification conflict = *m_conflict; justification conflict = *m_conflict;
std::unique_ptr<case_split> & d = m_case_splits.back(); std::unique_ptr<case_split> & d = m_case_splits.back();
if (!m_config.m_nonchronological || depends_on(conflict, d->m_assumption_idx)) { if (!m_config.m_nonchronological || depends_on(conflict, d->m_assumption_idx)) {