Context Navigation

SatisfyAssertions.cpp @ 7583c02

arm-ehenumforall-pointer-decayjacob/cs343-translationnew-ast-unique-exprpthread-emulationqualifiedEnum

Last change on this file since 7583c02 was 7583c02, checked in by Fangren Yu <f37yu@…>, 2 years ago

partially improve #226: resolver environment size reduced to O(n)

generated code still has exponential size. should cache resolved implicits
and reuse thunks to reduce generated code size.
assertion fails cannot exit early and may have a minor performance
reduction.

Property mode set to 100644

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

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: src/ResolvExpr/SatisfyAssertions.cpp @ 7583c02

Download in other formats: