Changeset 2b4daf2 for src/ResolvExpr/SatisfyAssertions.cpp

Timestamp:

Jan 7, 2021, 5:06:22 PM (5 years ago)

Author:

Thierry Delisle <tdelisle@…>

Branches:

ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, master, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

5ad381b

Parents:

42f6e07 (diff), 58fe85a (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge branch 'master' of plg.uwaterloo.ca:software/cfa/cfa-cc

File:

• src/ResolvExpr/SatisfyAssertions.cpp (modified) (25 diffs)

src/ResolvExpr/SatisfyAssertions.cpp

@@ -57 +57 @@
                 ast::UniqueId resnSlot;          ///< Slot for any recursive assertion IDs
 
-                AssnCandidate( 
-                        const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, 
+                AssnCandidate(
+                        const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e,
                         ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs )
-                : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 
+                : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ),
                   need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {}
         };
@@ -69 +69 @@
         /// Reference to a single deferred item
         struct DeferRef {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 const AssnCandidate & match;
         };
-        
-        /// Wrapper for the deferred items from a single assertion satisfaction. 
+
+        /// Wrapper for the deferred items from a single assertion satisfaction.
         /// Acts like an indexed list of DeferRef
         struct DeferItem {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 AssnCandidateList matches;
 
-                DeferItem( 
-                        const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
-                : decl( d ), info( i ), matches( std::move( ms ) ) {}
+                DeferItem(
+                        const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
+                : expr( d ), info( i ), matches( std::move( ms ) ) {}
 
                 bool empty() const { return matches.empty(); }
@@ -89 +89 @@
                 AssnCandidateList::size_type size() const { return matches.size(); }
 
-                DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+                DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
         };
 
@@ -117 +117 @@
                 /// Initial satisfaction state for a candidate
                 SatState( CandidateRef & c, const ast::SymbolTable & syms )
-                : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, 
+                : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero },
                   symtab( syms ) { need.swap( c->need ); }
-                
+
                 /// Update satisfaction state for next step after previous state
                 SatState( SatState && o, IterateFlag )
-                : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), 
-                  deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), 
+                : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(),
+                  deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ),
                   symtab( o.symtab ) { costs.emplace_back( Cost::zero ); }
-                
+
                 /// Field-wise next step constructor
                 SatState(
-                        CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, 
+                        CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs,
                         ast::SymbolTable && syms )
-                : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), 
+                : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(),
                   inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) )
                   { costs.emplace_back( Cost::zero ); }
@@ -138 +138 @@
         void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
                 for ( auto & i : have ) {
-                        if ( i.second.isUsed ) { symtab.addId( i.first ); }
+                        if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
                 }
         }
 
         /// Binds a single assertion, updating satisfaction state
-        void bindAssertion( 
-                const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 
+        void bindAssertion(
+                const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand,
                 AssnCandidate & match, InferCache & inferred
         ) {
                 const ast::DeclWithType * candidate = match.cdata.id;
-                assertf( candidate->uniqueId, 
+                assertf( candidate->uniqueId,
                         "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
-                
+
                 ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost );
                 varExpr->result = match.adjType;
@@ -156 +156 @@
 
                 // place newly-inferred assertion in proper location in cache
-                inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{
-                        candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr };
+                inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
+                        candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
         }
 
@@ -169 +169 @@
 
                 std::vector<ast::SymbolTable::IdData> candidates;
-                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->name);
+                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
                 if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
                         // prefilter special decls by argument type, if already known
-                        ast::ptr<ast::Type> thisArgType = strict_dynamic_cast<const ast::PointerType *>(assn.first->get_type())->base
+                        ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
                                 .strict_as<ast::FunctionType>()->params[0]
                                 .strict_as<ast::ReferenceType>()->base;
@@ -184 +184 @@
                 }
                 else {
-                        candidates = sat.symtab.lookupId(assn.first->name);
+                        candidates = sat.symtab.lookupId(assn.first->var->name);
                 }
                 for ( const ast::SymbolTable::IdData & cdata : candidates ) {
@@ -200 +200 @@
                         ast::TypeEnvironment newEnv{ sat.cand->env };
                         ast::OpenVarSet newOpen{ sat.cand->open };
-                        ast::ptr< ast::Type > toType = assn.first->get_type();
-                        ast::ptr< ast::Type > adjType = 
-                                renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
+                        ast::ptr< ast::Type > toType = assn.first->result;
+                        ast::ptr< ast::Type > adjType =
+                                renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
 
                         // only keep candidates which unify
@@ -213 +213 @@
                                 }
 
-                                matches.emplace_back( 
+                                matches.emplace_back(
                                         cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
                                         std::move( newOpen ), crntResnSlot );
@@ -287 +287 @@
         };
 
-        /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning 
+        /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning
         /// threshold.
-        void finalizeAssertions( 
-                CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, 
-                CandidateList & out 
+        void finalizeAssertions(
+                CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs,
+                CandidateList & out
         ) {
                 // prune if cheaper alternative for same key has already been generated
@@ -308 +308 @@
         }
 
-        /// Combo iterator that combines candidates into an output list, merging their environments. 
-        /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` 
+        /// Combo iterator that combines candidates into an output list, merging their environments.
+        /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h`
         /// for description of "combo iterator".
         class CandidateEnvMerger {
@@ -337 +337 @@
                                         // compute conversion cost from satisfying decl to assertion
                                         cost += computeConversionCost(
-                                                assn.match.adjType, assn.decl->get_type(), false, symtab, env );
+                                                assn.match.adjType, assn.expr->result, false, symtab, env );
 
                                         // mark vars+specialization on function-type assertions
@@ -350 +350 @@
                                         cost.incVar( func->forall.size() );
 
-                                        for ( const ast::TypeDecl * td : func->forall ) {
-                                                cost.decSpec( td->assertions.size() );
-                                        }
+                                        cost.decSpec( func->assertions.size() );
                                 }
                         }
@@ -387 +385 @@
 
         /// Limit to depth of recursion of assertion satisfaction
-        static const int recursionLimit = 4;
+        static const int recursionLimit = 8;
         /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
         static const int deferLimit = 10;
 } // anonymous namespace
 
-void satisfyAssertions( 
-        CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, 
+void satisfyAssertions(
+        CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out,
         std::vector<std::string> & errors
 ) {
@@ -419 +417 @@
                         if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
 
-                        // make initial pass at matching assertions
-                        for ( auto & assn : sat.need ) {
-                                // fail early if any assertion is not satisfiable
-                                if ( ! satisfyAssertion( assn, sat ) ) {
+                        // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen.
+                        for (unsigned resetCount = 0; ; ++resetCount) {
+                                ast::AssertionList next;
+                                resetTyVarRenaming();
+                                // make initial pass at matching assertions
+                                for ( auto & assn : sat.need ) {
+                                        // fail early if any assertion is not satisfiable
+                                        if ( ! satisfyAssertion( assn, sat ) ) {
+                                                next.emplace_back(assn);
+                                                // goto nextSat;
+                                        }
+                                }
+                                // success
+                                if (next.empty()) break;
+                                // fail if nothing resolves
+                                else if (next.size() == sat.need.size()) {
                                         Indenter tabs{ 3 };
                                         std::ostringstream ss;
@@ -428 +438 @@
                                         print( ss, *sat.cand, ++tabs );
                                         ss << (tabs-1) << "Could not satisfy assertion:\n";
-                                        ast::print( ss, assn.first, tabs );
+                                        ast::print( ss, next[0].first, tabs );
 
                                         errors.emplace_back( ss.str() );
                                         goto nextSat;
                                 }
+                                sat.need = std::move(next);
                         }
 
@@ -438 +449 @@
                                 // either add successful match or push back next state
                                 if ( sat.newNeed.empty() ) {
-                                        finalizeAssertions( 
+                                        finalizeAssertions(
                                                 sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
                                 } else {
@@ -451 +462 @@
                                 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
                                 for ( const auto & d : sat.deferred ) {
-                                        ast::print( ss, d.decl, tabs );
+                                        ast::print( ss, d.expr, tabs );
                                 }
 
@@ -460 +471 @@
                                 std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
                                         sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
-                                
+
                                 // fail early if no mutually-compatible assertion satisfaction
                                 if ( compatible.empty() ) {
@@ -469 +480 @@
                                         ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
                                         for ( const auto& d : sat.deferred ) {
-                                                ast::print( ss, d.decl, tabs );
+                                                ast::print( ss, d.expr, tabs );
                                         }
 
@@ -483 +494 @@
                                         // set up next satisfaction state
                                         CandidateRef nextCand = std::make_shared<Candidate>(
-                                                sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 
+                                                sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
                                                 ast::AssertionSet{} /* need moved into satisfaction state */,
                                                 sat.cand->cost, sat.cand->cvtCost );
@@ -489 +500 @@
                                         ast::AssertionSet nextNewNeed{ sat.newNeed };
                                         InferCache nextInferred{ sat.inferred };
-                                        
+
                                         CostVec nextCosts{ sat.costs };
                                         nextCosts.back() += compat.cost;
-                                                                
+
                                         ast::SymbolTable nextSymtab{ sat.symtab };
 
@@ -501 +512 @@
                                                 nextNewNeed.insert( match.need.begin(), match.need.end() );
 
-                                                bindAssertion( r.decl, r.info, nextCand, match, nextInferred );
+                                                bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
                                         }
 
                                         // either add successful match or push back next state
                                         if ( nextNewNeed.empty() ) {
-                                                finalizeAssertions( 
+                                                finalizeAssertions(
                                                         nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
                                         } else {
-                                                nextSats.emplace_back( 
-                                                        std::move( nextCand ), std::move( nextNewNeed ), 
-                                                        std::move( nextInferred ), std::move( nextCosts ), 
+                                                nextSats.emplace_back(
+                                                        std::move( nextCand ), std::move( nextNewNeed ),
+                                                        std::move( nextInferred ), std::move( nextCosts ),
                                                         std::move( nextSymtab ) );
                                         }
@@ -523 +534 @@
                 nextSats.clear();
         }
-        
+
         // exceeded recursion limit if reaches here
         if ( out.empty() ) {