source: src/ResolvExpr/SatisfyAssertions.cpp@ 7f995d70

Last change on this file since 7f995d70 was b86dd969, checked in by Peter A. Buhr <pabuhr@…>, 3 months ago

remove unused loop-counter resetCount causing a warning
  • Property mode set to 100644
File size: 20.8 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 : Thu Jul 31 18:04:31 2025
13// Update Count : 6
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
48namespace ResolvExpr {
49
50// in CandidateFinder.cpp; unique ID for assertion satisfaction
51extern ast::UniqueId globalResnSlot;
52
53namespace {
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
429void 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 ( ;; ) {
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 }
478 }
479 // success
480 if (next.empty()) break;
481
482 sat.need = std::move(next);
483 }
484
485 if ( sat.deferred.empty() ) {
486 // either add successful match or push back next state
487 if ( sat.newNeed.empty() ) {
488 finalizeAssertions(
489 sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
490 } else {
491 nextSats.emplace_back( std::move( sat ), IterateState );
492 }
493 } else if ( sat.deferred.size() > deferLimit ) {
494 // too many deferred assertions to attempt mutual compatibility
495 Indenter tabs{ 3 };
496 std::ostringstream ss;
497 ss << tabs << "Unsatisfiable alternative:\n";
498 print( ss, *sat.cand, ++tabs );
499 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
500 for ( const auto & d : sat.deferred ) {
501 ast::print( ss, d.expr, tabs );
502 }
503
504 errors.emplace_back( ss.str() );
505 goto nextSat;
506 } else {
507 // combine deferred assertions by mutual compatibility
508 std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
509 sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
510
511 // fail early if no mutually-compatible assertion satisfaction
512 if ( compatible.empty() ) {
513 Indenter tabs{ 3 };
514 std::ostringstream ss;
515 ss << tabs << "Unsatisfiable alternative:\n";
516 print( ss, *sat.cand, ++tabs );
517 ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
518 for ( const auto& d : sat.deferred ) {
519 ast::print( ss, d.expr, tabs );
520 }
521
522 errors.emplace_back( ss.str() );
523 goto nextSat;
524 }
525
526 // sort by cost (for overall pruning order)
527 std::sort( compatible.begin(), compatible.end() );
528
529 // process mutually-compatible combinations
530 for ( auto & compat : compatible ) {
531 // set up next satisfaction state
532 CandidateRef nextCand = std::make_shared<Candidate>(
533 sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
534 ast::AssertionSet{} /* need moved into satisfaction state */,
535 sat.cand->cost );
536
537 ast::AssertionSet nextNewNeed{ sat.newNeed };
538 InferCache nextInferred{ sat.inferred };
539
540 CostVec nextCosts{ sat.costs };
541 nextCosts.back() += compat.cost;
542
543 ast::SymbolTable nextSymtab{ sat.symtab };
544
545 // add compatible assertions to new satisfaction state
546 for ( DeferRef r : compat.assns ) {
547 AssnCandidate match = r.match;
548 // addToSymbolTable( match.have, nextSymtab );
549 nextNewNeed.insert( match.need.begin(), match.need.end() );
550
551 bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
552 }
553
554 // either add successful match or push back next state
555 if ( nextNewNeed.empty() ) {
556 finalizeAssertions(
557 nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
558 } else {
559 nextSats.emplace_back(
560 std::move( nextCand ), std::move( nextNewNeed ),
561 std::move( nextInferred ), std::move( nextCosts ),
562 std::move( nextSymtab ) );
563 }
564 }
565 }
566 nextSat:; }
567
568 // finish or reset for next round
569 if ( nextSats.empty() ) return;
570 sats.swap( nextSats );
571 nextSats.clear();
572 }
573
574 // exceeded recursion limit if reaches here
575 if ( out.empty() ) {
576 SemanticError( cand->expr->location, "Too many recursive assertions, possible cause is circular relationship between a forall assertion and defined function prototype." );
577 }
578}
579
580} // namespace ResolvExpr
581
582// Local Variables: //
583// tab-width: 4 //
584// mode: c++ //
585// compile-command: "make install" //
586// End: //
Note: See TracBrowser for help on using the repository browser.