source: src/ResolvExpr/SatisfyAssertions.cpp@ 9317419

ADT ast-experimental
Last change on this file since 9317419 was 5bf3976, checked in by Andrew Beach <ajbeach@…>, 3 years ago

Header Clean-Up: Created new headers for new AST typeops and moved declarations.
  • Property mode set to 100644
File size: 20.3 KB
Line 
1//
2// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
3//
4// The contents of this file are covered under the licence agreement in the
5// file "LICENCE" distributed with Cforall.
6//
7// SatisfyAssertions.cpp --
8//
9// Author : Aaron B. Moss
10// Created On : Mon Jun 10 17:45:00 2019
11// Last Modified By : Andrew Beach
12// Last Modified On : Tue Oct 1 13:56:00 2019
13// Update Count : 2
14//
15
16#include "SatisfyAssertions.hpp"
17
18#include <algorithm>
19#include <cassert>
20#include <sstream>
21#include <string>
22#include <unordered_map>
23#include <vector>
24
25#include "AdjustExprType.hpp"
26#include "Candidate.hpp"
27#include "CandidateFinder.hpp"
28#include "CommonType.hpp"
29#include "Cost.h"
30#include "RenameVars.h"
31#include "SpecCost.hpp"
32#include "typeops.h"
33#include "Unify.h"
34#include "AST/Decl.hpp"
35#include "AST/Expr.hpp"
36#include "AST/Node.hpp"
37#include "AST/Pass.hpp"
38#include "AST/Print.hpp"
39#include "AST/SymbolTable.hpp"
40#include "AST/TypeEnvironment.hpp"
41#include "FindOpenVars.h"
42#include "Common/FilterCombos.h"
43#include "Common/Indenter.h"
44#include "GenPoly/GenPoly.h"
45#include "SymTab/Mangler.h"
46
47namespace ResolvExpr {
48
49// in CandidateFinder.cpp; unique ID for assertion satisfaction
50extern UniqueId globalResnSlot;
51
52namespace {
53 /// Post-unification assertion satisfaction candidate
54 struct AssnCandidate {
55 ast::SymbolTable::IdData cdata; ///< Satisfying declaration
56 ast::ptr< ast::Type > adjType; ///< Satisfying type
57 ast::TypeEnvironment env; ///< Post-unification environment
58 ast::AssertionSet have; ///< Post-unification have-set
59 ast::AssertionSet need; ///< Post-unification need-set
60 ast::OpenVarSet open; ///< Post-unification open-var-set
61 ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs
62
63 AssnCandidate(
64 const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e,
65 ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs )
66 : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ),
67 need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {}
68 };
69
70 /// List of assertion satisfaction candidates
71 using AssnCandidateList = std::vector< AssnCandidate >;
72
73 /// Reference to a single deferred item
74 struct DeferRef {
75 const ast::VariableExpr * expr;
76 const ast::AssertionSetValue & info;
77 const AssnCandidate & match;
78 };
79
80 /// Wrapper for the deferred items from a single assertion satisfaction.
81 /// Acts like an indexed list of DeferRef
82 struct DeferItem {
83 const ast::VariableExpr * expr;
84 const ast::AssertionSetValue & info;
85 AssnCandidateList matches;
86
87 DeferItem(
88 const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
89 : expr( d ), info( i ), matches( std::move( ms ) ) {}
90
91 bool empty() const { return matches.empty(); }
92
93 AssnCandidateList::size_type size() const { return matches.size(); }
94
95 DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
96 };
97
98 /// List of deferred satisfaction items
99 using DeferList = std::vector< DeferItem >;
100
101 /// Set of assertion satisfactions, grouped by resolution ID
102 using InferCache = std::unordered_map< ast::UniqueId, ast::InferredParams >;
103
104 /// Lexicographically-ordered vector of costs.
105 /// Lexicographic order comes from default operator< on std::vector.
106 using CostVec = std::vector< Cost >;
107
108 /// Flag for state iteration
109 enum IterateFlag { IterateState };
110
111 /// Intermediate state for satisfying a set of assertions
112 struct SatState {
113 CandidateRef cand; ///< Candidate assertion is rooted on
114 ast::AssertionList need; ///< Assertions to find
115 ast::AssertionSet newNeed; ///< Recursive assertions from current satisfied assertions
116 DeferList deferred; ///< Deferred matches
117 InferCache inferred; ///< Cache of already-inferred assertions
118 CostVec costs; ///< Disambiguating costs of recursive assertion satisfaction
119 ast::SymbolTable symtab; ///< Name lookup (depends on previous assertions)
120
121 /// Initial satisfaction state for a candidate
122 SatState( CandidateRef & c, const ast::SymbolTable & syms )
123 : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero },
124 symtab( syms ) { need.swap( c->need ); }
125
126 /// Update satisfaction state for next step after previous state
127 SatState( SatState && o, IterateFlag )
128 : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(),
129 deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ),
130 symtab( o.symtab ) { costs.emplace_back( Cost::zero ); }
131
132 /// Field-wise next step constructor
133 SatState(
134 CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs,
135 ast::SymbolTable && syms )
136 : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(),
137 inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) )
138 { costs.emplace_back( Cost::zero ); }
139 };
140
141 /// Adds a captured assertion to the symbol table
142 void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
143 for ( auto & i : have ) {
144 if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
145 }
146 }
147
148 /// Binds a single assertion, updating satisfaction state
149 void bindAssertion(
150 const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand,
151 AssnCandidate & match, InferCache & inferred
152 ) {
153 const ast::DeclWithType * candidate = match.cdata.id;
154 assertf( candidate->uniqueId,
155 "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
156
157 ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost );
158 varExpr->result = match.adjType;
159 if ( match.resnSlot ) { varExpr->inferred.resnSlots().emplace_back( match.resnSlot ); }
160
161 // place newly-inferred assertion in proper location in cache
162 inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
163 candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
164 }
165
166 /// Satisfy a single assertion
167 bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool allowConversion = false, bool skipUnbound = false) {
168 // skip unused assertions
169 if ( ! assn.second.isUsed ) return true;
170
171 // find candidates that unify with the desired type
172 AssnCandidateList matches;
173
174 std::vector<ast::SymbolTable::IdData> candidates;
175 auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
176 if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
177 // prefilter special decls by argument type, if already known
178 ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
179 .strict_as<ast::FunctionType>()->params[0]
180 .strict_as<ast::ReferenceType>()->base;
181 sat.cand->env.apply(thisArgType);
182
183 std::string otypeKey = "";
184 if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer;
185 else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type | Mangle::NoGenericParams);
186 else if (skipUnbound) return false;
187
188 candidates = sat.symtab.specialLookupId(kind, otypeKey);
189 }
190 else {
191 candidates = sat.symtab.lookupId(assn.first->var->name);
192 }
193 for ( const ast::SymbolTable::IdData & cdata : candidates ) {
194 const ast::DeclWithType * candidate = cdata.id;
195
196 // ignore deleted candidates.
197 // NOTE: this behavior is different from main resolver.
198 // further investigations might be needed to determine
199 // if we should implement the same rule here
200 // (i.e. error if unique best match is deleted)
201 if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue;
202
203 // build independent unification context for candidate
204 ast::AssertionSet have, newNeed;
205 ast::TypeEnvironment newEnv{ sat.cand->env };
206 ast::OpenVarSet newOpen{ sat.cand->open };
207 ast::ptr< ast::Type > toType = assn.first->result;
208 ast::ptr< ast::Type > adjType =
209 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
210
211 // only keep candidates which unify
212
213 ast::OpenVarSet closed;
214 findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed );
215 findOpenVars( adjType, newOpen, closed, newNeed, have, FirstOpen );
216 if ( allowConversion ) {
217 if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {
218 // set up binding slot for recursive assertions
219 ast::UniqueId crntResnSlot = 0;
220 if ( ! newNeed.empty() ) {
221 crntResnSlot = ++globalResnSlot;
222 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
223 }
224
225 matches.emplace_back(
226 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
227 std::move( newOpen ), crntResnSlot );
228 }
229 }
230 else {
231 if ( unifyExact( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {
232 // set up binding slot for recursive assertions
233 ast::UniqueId crntResnSlot = 0;
234 if ( ! newNeed.empty() ) {
235 crntResnSlot = ++globalResnSlot;
236 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
237 }
238
239 matches.emplace_back(
240 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
241 std::move( newOpen ), crntResnSlot );
242 }
243 }
244 }
245
246 // break if no satisfying match
247 if ( matches.empty() ) return false;
248
249 // defer if too many satisfying matches
250 if ( matches.size() > 1 ) {
251 sat.deferred.emplace_back( assn.first, assn.second, std::move( matches ) );
252 return true;
253 }
254
255 // otherwise bind unique match in ongoing scope
256 AssnCandidate & match = matches.front();
257 addToSymbolTable( match.have, sat.symtab );
258 sat.newNeed.insert( match.need.begin(), match.need.end() );
259 sat.cand->env = std::move( match.env );
260 sat.cand->open = std::move( match.open );
261
262 bindAssertion( assn.first, assn.second, sat.cand, match, sat.inferred );
263 return true;
264 }
265
266 /// Map of candidate return types to recursive assertion satisfaction costs
267 using PruneMap = std::unordered_map< std::string, CostVec >;
268
269 /// Gets the pruning key for a candidate (derived from environment-adjusted return type)
270 std::string pruneKey( const Candidate & cand ) {
271 ast::ptr< ast::Type > resType = cand.expr->result;
272 cand.env.apply( resType );
273 return Mangle::mangleType( resType );
274 }
275
276 /// Associates inferred parameters with an expression
277 struct InferMatcher final {
278 InferCache & inferred;
279
280 InferMatcher( InferCache & inferred ) : inferred( inferred ) {}
281
282 const ast::Expr * postvisit( const ast::Expr * expr ) {
283 // Skip if no slots to find
284 if ( !expr->inferred.hasSlots() ) return expr;
285 // if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr;
286 std::vector<UniqueId> missingSlots;
287 // find inferred parameters for resolution slots
288 ast::InferredParams * newInferred = new ast::InferredParams();
289 for ( UniqueId slot : expr->inferred.resnSlots() ) {
290 // fail if no matching assertions found
291 auto it = inferred.find( slot );
292 if ( it == inferred.end() ) {
293 // std::cerr << "missing assertion " << slot << std::endl;
294 missingSlots.push_back(slot);
295 continue;
296 }
297
298 // place inferred parameters into new map
299 for ( auto & entry : it->second ) {
300 // recurse on inferParams of resolved expressions
301 entry.second.expr = postvisit( entry.second.expr );
302 auto res = newInferred->emplace( entry );
303 assert( res.second && "all assertions newly placed" );
304 }
305 }
306
307 ast::Expr * ret = mutate( expr );
308 ret->inferred.set_inferParams( newInferred );
309 if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots;
310 return ret;
311 }
312 };
313
314 /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning
315 /// threshold.
316 void finalizeAssertions(
317 CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs,
318 CandidateList & out
319 ) {
320 // prune if cheaper alternative for same key has already been generated
321 std::string key = pruneKey( *cand );
322 auto it = thresholds.find( key );
323 if ( it != thresholds.end() ) {
324 if ( it->second < costs ) return;
325 } else {
326 thresholds.emplace_hint( it, key, std::move( costs ) );
327 }
328
329 // replace resolution slots with inferred parameters, add to output
330 ast::Pass< InferMatcher > matcher{ inferred };
331 cand->expr = cand->expr->accept( matcher );
332 out.emplace_back( cand );
333 }
334
335 /// Combo iterator that combines candidates into an output list, merging their environments.
336 /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h`
337 /// for description of "combo iterator".
338 class CandidateEnvMerger {
339 /// Current list of merged candidates
340 std::vector< DeferRef > crnt;
341 /// Stack of environments to support backtracking
342 std::vector< ast::TypeEnvironment > envs;
343 /// Stack of open variables to support backtracking
344 std::vector< ast::OpenVarSet > opens;
345 /// Symbol table to use for merges
346 const ast::SymbolTable & symtab;
347
348 public:
349 /// The merged environment/open variables and the list of candidates
350 struct OutType {
351 ast::TypeEnvironment env;
352 ast::OpenVarSet open;
353 std::vector< DeferRef > assns;
354 Cost cost;
355
356 OutType(
357 const ast::TypeEnvironment & e, const ast::OpenVarSet & o,
358 const std::vector< DeferRef > & as, const ast::SymbolTable & symtab )
359 : env( e ), open( o ), assns( as ), cost( Cost::zero ) {
360 // compute combined conversion cost
361 for ( const DeferRef & assn : assns ) {
362 // compute conversion cost from satisfying decl to assertion
363 cost += computeConversionCost(
364 assn.match.adjType, assn.expr->result, false, symtab, env );
365
366 // mark vars+specialization on function-type assertions
367 const ast::FunctionType * func =
368 GenPoly::getFunctionType( assn.match.cdata.id->get_type() );
369 if ( ! func ) continue;
370
371 for ( const auto & param : func->params ) {
372 cost.decSpec( specCost( param ) );
373 }
374
375 cost.incVar( func->forall.size() );
376
377 cost.decSpec( func->assertions.size() );
378 }
379 }
380
381 bool operator< ( const OutType & o ) const { return cost < o.cost; }
382 };
383
384 CandidateEnvMerger(
385 const ast::TypeEnvironment & env, const ast::OpenVarSet & open,
386 const ast::SymbolTable & syms )
387 : crnt(), envs{ env }, opens{ open }, symtab( syms ) {}
388
389 bool append( DeferRef i ) {
390 ast::TypeEnvironment env = envs.back();
391 ast::OpenVarSet open = opens.back();
392 mergeOpenVars( open, i.match.open );
393
394 if ( ! env.combine( i.match.env, open, symtab ) ) return false;
395
396 crnt.emplace_back( i );
397 envs.emplace_back( std::move( env ) );
398 opens.emplace_back( std::move( open ) );
399 return true;
400 }
401
402 void backtrack() {
403 crnt.pop_back();
404 envs.pop_back();
405 opens.pop_back();
406 }
407
408 OutType finalize() { return { envs.back(), opens.back(), crnt, symtab }; }
409 };
410
411 /// Limit to depth of recursion of assertion satisfaction
412 static const int recursionLimit = 8;
413 /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
414 static const int deferLimit = 10;
415} // anonymous namespace
416
417void satisfyAssertions(
418 CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out,
419 std::vector<std::string> & errors
420) {
421 // finish early if no assertions to satisfy
422 if ( cand->need.empty() ) {
423 out.emplace_back( cand );
424 return;
425 }
426
427 // build list of possible combinations of satisfying declarations
428 std::vector< SatState > sats{ SatState{ cand, symtab } };
429 std::vector< SatState > nextSats{};
430
431 // pruning thresholds by result type of output candidates.
432 // Candidates *should* be generated in sorted order, so no need to retroactively prune
433 PruneMap thresholds;
434
435 // satisfy assertions in breadth-first order over the recursion tree of assertion satisfaction.
436 // Stop recursion at a limited number of levels deep to avoid infinite loops.
437 for ( unsigned level = 0; level < recursionLimit; ++level ) {
438 // for each current mutually-compatible set of assertions
439 for ( SatState & sat : sats ) {
440 bool allowConversion = false;
441 // stop this branch if a better option is already found
442 auto it = thresholds.find( pruneKey( *sat.cand ) );
443 if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
444
445 // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen.
446
447 for (unsigned resetCount = 0; ; ++resetCount) {
448 ast::AssertionList next;
449 resetTyVarRenaming();
450 // make initial pass at matching assertions
451 for ( auto & assn : sat.need ) {
452 // fail early if any assertion is not satisfiable
453 if ( ! satisfyAssertion( assn, sat, allowConversion, !next.empty() ) ) {
454 next.emplace_back(assn);
455 // goto nextSat;
456 }
457 }
458 // success
459 if (next.empty()) break;
460 // fail if nothing resolves
461 else if (next.size() == sat.need.size()) {
462 if (allowConversion) {
463 Indenter tabs{ 3 };
464 std::ostringstream ss;
465 ss << tabs << "Unsatisfiable alternative:\n";
466 print( ss, *sat.cand, ++tabs );
467 ss << (tabs-1) << "Could not satisfy assertion:\n";
468 ast::print( ss, next[0].first, tabs );
469
470 errors.emplace_back( ss.str() );
471 goto nextSat;
472 }
473
474 else {
475 allowConversion = true;
476 continue;
477 }
478 }
479 allowConversion = false;
480 sat.need = std::move(next);
481 }
482
483 if ( sat.deferred.empty() ) {
484 // either add successful match or push back next state
485 if ( sat.newNeed.empty() ) {
486 finalizeAssertions(
487 sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
488 } else {
489 nextSats.emplace_back( std::move( sat ), IterateState );
490 }
491 } else if ( sat.deferred.size() > deferLimit ) {
492 // too many deferred assertions to attempt mutual compatibility
493 Indenter tabs{ 3 };
494 std::ostringstream ss;
495 ss << tabs << "Unsatisfiable alternative:\n";
496 print( ss, *sat.cand, ++tabs );
497 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
498 for ( const auto & d : sat.deferred ) {
499 ast::print( ss, d.expr, tabs );
500 }
501
502 errors.emplace_back( ss.str() );
503 goto nextSat;
504 } else {
505 // combine deferred assertions by mutual compatibility
506 std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
507 sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
508
509 // fail early if no mutually-compatible assertion satisfaction
510 if ( compatible.empty() ) {
511 Indenter tabs{ 3 };
512 std::ostringstream ss;
513 ss << tabs << "Unsatisfiable alternative:\n";
514 print( ss, *sat.cand, ++tabs );
515 ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
516 for ( const auto& d : sat.deferred ) {
517 ast::print( ss, d.expr, tabs );
518 }
519
520 errors.emplace_back( ss.str() );
521 goto nextSat;
522 }
523
524 // sort by cost (for overall pruning order)
525 std::sort( compatible.begin(), compatible.end() );
526
527 // process mutually-compatible combinations
528 for ( auto & compat : compatible ) {
529 // set up next satisfaction state
530 CandidateRef nextCand = std::make_shared<Candidate>(
531 sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
532 ast::AssertionSet{} /* need moved into satisfaction state */,
533 sat.cand->cost, sat.cand->cvtCost );
534
535 ast::AssertionSet nextNewNeed{ sat.newNeed };
536 InferCache nextInferred{ sat.inferred };
537
538 CostVec nextCosts{ sat.costs };
539 nextCosts.back() += compat.cost;
540
541 ast::SymbolTable nextSymtab{ sat.symtab };
542
543 // add compatible assertions to new satisfaction state
544 for ( DeferRef r : compat.assns ) {
545 AssnCandidate match = r.match;
546 addToSymbolTable( match.have, nextSymtab );
547 nextNewNeed.insert( match.need.begin(), match.need.end() );
548
549 bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
550 }
551
552 // either add successful match or push back next state
553 if ( nextNewNeed.empty() ) {
554 finalizeAssertions(
555 nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
556 } else {
557 nextSats.emplace_back(
558 std::move( nextCand ), std::move( nextNewNeed ),
559 std::move( nextInferred ), std::move( nextCosts ),
560 std::move( nextSymtab ) );
561 }
562 }
563 }
564 nextSat:; }
565
566 // finish or reset for next round
567 if ( nextSats.empty() ) return;
568 sats.swap( nextSats );
569 nextSats.clear();
570 }
571
572 // exceeded recursion limit if reaches here
573 if ( out.empty() ) {
574 SemanticError( cand->expr->location, "Too many recursive assertions" );
575 }
576}
577
578} // namespace ResolvExpr
579
580// Local Variables: //
581// tab-width: 4 //
582// mode: c++ //
583// compile-command: "make install" //
584// End: //
Note: See TracBrowser for help on using the repository browser.