Context Navigation

source: src/ResolvExpr/SatisfyAssertions.cpp @ 46da46b

ast-experimental

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

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

Download in other formats: