Changeset aca6a54c
- Timestamp:
- Dec 12, 2019, 10:04:08 AM (5 years ago)
- Branches:
- ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, master, new-ast-unique-expr, pthread-emulation, qualifiedEnum
- Children:
- 2fa5bd2
- Parents:
- 3376ec9
- Location:
- src/ResolvExpr
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ResolvExpr/ResolveAssertions.cc
r3376ec9 raca6a54c 390 390 391 391 /// Limit to depth of recursion of assertion satisfaction 392 static const int recursionLimit = 4;392 static const int recursionLimit = 7; 393 393 /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of 394 394 static const int deferLimit = 10; -
src/ResolvExpr/SatisfyAssertions.cpp
r3376ec9 raca6a54c 57 57 ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs 58 58 59 AssnCandidate( 60 const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, 59 AssnCandidate( 60 const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, 61 61 ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs ) 62 : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 62 : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 63 63 need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {} 64 64 }; … … 73 73 const AssnCandidate & match; 74 74 }; 75 76 /// Wrapper for the deferred items from a single assertion satisfaction. 75 76 /// Wrapper for the deferred items from a single assertion satisfaction. 77 77 /// Acts like an indexed list of DeferRef 78 78 struct DeferItem { … … 81 81 AssnCandidateList matches; 82 82 83 DeferItem( 83 DeferItem( 84 84 const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms ) 85 85 : decl( d ), info( i ), matches( std::move( ms ) ) {} … … 117 117 /// Initial satisfaction state for a candidate 118 118 SatState( CandidateRef & c, const ast::SymbolTable & syms ) 119 : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, 119 : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, 120 120 symtab( syms ) { need.swap( c->need ); } 121 121 122 122 /// Update satisfaction state for next step after previous state 123 123 SatState( SatState && o, IterateFlag ) 124 : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), 125 deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), 124 : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), 125 deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), 126 126 symtab( o.symtab ) { costs.emplace_back( Cost::zero ); } 127 127 128 128 /// Field-wise next step constructor 129 129 SatState( 130 CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, 130 CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, 131 131 ast::SymbolTable && syms ) 132 : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), 132 : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), 133 133 inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) ) 134 134 { costs.emplace_back( Cost::zero ); } … … 143 143 144 144 /// Binds a single assertion, updating satisfaction state 145 void bindAssertion( 146 const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 145 void bindAssertion( 146 const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 147 147 AssnCandidate & match, InferCache & inferred 148 148 ) { 149 149 const ast::DeclWithType * candidate = match.cdata.id; 150 assertf( candidate->uniqueId, 150 assertf( candidate->uniqueId, 151 151 "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() ); 152 152 153 153 ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost ); 154 154 varExpr->result = match.adjType; … … 175 175 ast::OpenVarSet newOpen{ sat.cand->open }; 176 176 ast::ptr< ast::Type > toType = assn.first->get_type(); 177 ast::ptr< ast::Type > adjType = 177 ast::ptr< ast::Type > adjType = 178 178 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) ); 179 179 … … 187 187 } 188 188 189 matches.emplace_back( 190 cdata, adjType, std::move( newEnv ), std::move( newNeed ), std::move( have ), 189 matches.emplace_back( 190 cdata, adjType, std::move( newEnv ), std::move( newNeed ), std::move( have ), 191 191 std::move( newOpen ), crntResnSlot ); 192 192 } … … 257 257 }; 258 258 259 /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning 259 /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning 260 260 /// threshold. 261 void finalizeAssertions( 262 CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, 263 CandidateList & out 261 void finalizeAssertions( 262 CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, 263 CandidateList & out 264 264 ) { 265 265 // prune if cheaper alternative for same key has already been generated … … 278 278 } 279 279 280 /// Combo iterator that combines candidates into an output list, merging their environments. 281 /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` 280 /// Combo iterator that combines candidates into an output list, merging their environments. 281 /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` 282 282 /// for description of "combo iterator". 283 283 class CandidateEnvMerger { … … 299 299 Cost cost; 300 300 301 OutType( 302 const ast::TypeEnvironment & e, const ast::OpenVarSet & o, 301 OutType( 302 const ast::TypeEnvironment & e, const ast::OpenVarSet & o, 303 303 const std::vector< DeferRef > & as, const ast::SymbolTable & symtab ) 304 304 : env( e ), open( o ), assns( as ), cost( Cost::zero ) { … … 306 306 for ( const DeferRef & assn : assns ) { 307 307 // compute conversion cost from satisfying decl to assertion 308 cost += computeConversionCost( 308 cost += computeConversionCost( 309 309 assn.match.adjType, assn.decl->get_type(), symtab, env ); 310 310 311 311 // mark vars+specialization on function-type assertions 312 const ast::FunctionType * func = 312 const ast::FunctionType * func = 313 313 GenPoly::getFunctionType( assn.match.cdata.id->get_type() ); 314 314 if ( ! func ) continue; … … 317 317 cost.decSpec( specCost( param->get_type() ) ); 318 318 } 319 319 320 320 cost.incVar( func->forall.size() ); 321 321 322 322 for ( const ast::TypeDecl * td : func->forall ) { 323 323 cost.decSpec( td->assertions.size() ); … … 329 329 }; 330 330 331 CandidateEnvMerger( 332 const ast::TypeEnvironment & env, const ast::OpenVarSet & open, 331 CandidateEnvMerger( 332 const ast::TypeEnvironment & env, const ast::OpenVarSet & open, 333 333 const ast::SymbolTable & syms ) 334 334 : crnt(), envs{ env }, opens{ open }, symtab( syms ) {} … … 357 357 358 358 /// Limit to depth of recursion of assertion satisfaction 359 static const int recursionLimit = 4;359 static const int recursionLimit = 7; 360 360 /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of 361 361 static const int deferLimit = 10; 362 362 } // anonymous namespace 363 363 364 void satisfyAssertions( 365 CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, 364 void satisfyAssertions( 365 CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, 366 366 std::vector<std::string> & errors 367 367 ) { … … 408 408 // either add successful match or push back next state 409 409 if ( sat.newNeed.empty() ) { 410 finalizeAssertions( 410 finalizeAssertions( 411 411 sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out ); 412 412 } else { … … 430 430 std::vector< CandidateEnvMerger::OutType > compatible = filterCombos( 431 431 sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } ); 432 432 433 433 // fail early if no mutually-compatible assertion satisfaction 434 434 if ( compatible.empty() ) { … … 453 453 // set up next satisfaction state 454 454 CandidateRef nextCand = std::make_shared<Candidate>( 455 sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 455 sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 456 456 ast::AssertionSet{} /* need moved into satisfaction state */, 457 457 sat.cand->cost, sat.cand->cvtCost ); … … 459 459 ast::AssertionSet nextNewNeed{ sat.newNeed }; 460 460 InferCache nextInferred{ sat.inferred }; 461 461 462 462 CostVec nextCosts{ sat.costs }; 463 463 nextCosts.back() += compat.cost; 464 464 465 465 ast::SymbolTable nextSymtab{ sat.symtab }; 466 466 … … 476 476 // either add successful match or push back next state 477 477 if ( nextNewNeed.empty() ) { 478 finalizeAssertions( 478 finalizeAssertions( 479 479 nextCand, nextInferred, thresholds, std::move( nextCosts ), out ); 480 480 } else { 481 nextSats.emplace_back( 482 std::move( nextCand ), std::move( nextNewNeed ), 483 std::move( nextInferred ), std::move( nextCosts ), 481 nextSats.emplace_back( 482 std::move( nextCand ), std::move( nextNewNeed ), 483 std::move( nextInferred ), std::move( nextCosts ), 484 484 std::move( nextSymtab ) ); 485 485 } … … 493 493 nextSats.clear(); 494 494 } 495 495 496 496 // exceeded recursion limit if reaches here 497 497 if ( out.empty() ) {
Note: See TracChangeset
for help on using the changeset viewer.