Context Navigation

source: src/ResolvExpr/SatisfyAssertions.cpp @ 4558df2

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

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

Download in other formats: