Changeset d3b2c32a


Ignore:
Timestamp:
Jun 6, 2019, 3:39:10 PM (5 years ago)
Author:
Aaron Moss <a3moss@…>
Branches:
ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum
Children:
b7d92b96
Parents:
3cd5fdd
Message:

Add limit to number of recursive assertions tried at once

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ResolvExpr/ResolveAssertions.cc

    r3cd5fdd rd3b2c32a  
    342342
    343343        /// Limit to depth of recursion of assertion satisfaction
    344         static const int recursionLimit = /* 10 */ 4;
     344        static const int recursionLimit = 4;
     345        /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
     346        static const int deferLimit = 10;
    345347
    346348        void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out, std::list<std::string>& errors ) {
     
    369371                                                ss << tabs << "Unsatisfiable alternative:\n";
    370372                                                resn.alt.print( ss, ++tabs );
    371                                                 ss << --tabs << "Could not satisfy assertion:\n";
    372                                                 assn.decl->print( ss, ++tabs );
     373                                                ss << (tabs-1) << "Could not satisfy assertion:\n";
     374                                                assn.decl->print( ss, tabs );
    373375                                               
    374376                                                errors.emplace_back( ss.str() );
     
    384386                                                new_resns.emplace_back( std::move(resn), IterateState );
    385387                                        }
     388                                } else if ( resn.deferred.size() > deferLimit ) {
     389                                        // too many deferred assertions to attempt mutual compatibility
     390                                        Indenter tabs{ 3 };
     391                                        std::ostringstream ss;
     392                                        ss << tabs << "Unsatisfiable alternative:\n";
     393                                        resn.alt.print( ss, ++tabs );
     394                                        ss << (tabs-1) << "Too many non-unique satisfying assignments for "
     395                                                "assertions:\n";
     396                                        for ( const auto& d : resn.deferred ) {
     397                                                d.decl->print( ss, tabs );
     398                                        }
     399
     400                                        errors.emplace_back( ss.str() );
     401                                        goto nextResn;
    386402                                } else {
    387403                                        // resolve deferred assertions by mutual compatibility
     
    395411                                                ss << tabs << "Unsatisfiable alternative:\n";
    396412                                                resn.alt.print( ss, ++tabs );
    397                                                 ss << --tabs << "No mutually-compatible satisfaction for assertions:\n";
    398                                                 ++tabs;
     413                                                ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
    399414                                                for ( const auto& d : resn.deferred ) {
    400415                                                        d.decl->print( ss, tabs );
Note: See TracChangeset for help on using the changeset viewer.