Context Navigation

source: src/ResolvExpr/SatisfyAssertions.cpp @ 9cd5bd2

ADTast-experimentalpthread-emulation

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

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

Download in other formats: