source: src/ResolvExpr/SatisfyAssertions.cpp@ 16ba4a6f

ADT arm-eh ast-experimental enum forall-pointer-decay jacob/cs343-translation new-ast-unique-expr pthread-emulation qualifiedEnum
Last change on this file since 16ba4a6f was 2fb35df, checked in by Fangren Yu <f37yu@…>, 5 years ago

exclude deleted declarations for assertion matching
  • Property mode set to 100644
File size: 18.0 KB
RevLine 
[396037d]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
[cf32116]11// Last Modified By : Andrew Beach
12// Last Modified On : Tue Oct 1 13:56:00 2019
13// Update Count : 2
[396037d]14//
15
16#include "SatisfyAssertions.hpp"
17
[b69233ac]18#include <algorithm>
[396037d]19#include <cassert>
[b69233ac]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"
[396037d]42
43namespace ResolvExpr {
44
[b69233ac]45// in CandidateFinder.cpp; unique ID for assertion satisfaction
46extern UniqueId globalResnSlot;
47
48namespace {
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::DeclWithType * decl;
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::DeclWithType * decl;
80 const ast::AssertionSetValue & info;
81 AssnCandidateList matches;
82
83 DeferItem(
84 const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
85 : decl( 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 { decl, 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 ); }
141 }
142 }
143
144 /// Binds a single assertion, updating satisfaction state
145 void bindAssertion(
146 const ast::DeclWithType * decl, 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 ][ decl->uniqueId ] = ast::ParamEntry{
159 candidate->uniqueId, candidate, match.adjType, decl->get_type(), 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 for ( const ast::SymbolTable::IdData & cdata : sat.symtab.lookupId( assn.first->name ) ) {
170 const ast::DeclWithType * candidate = cdata.id;
171
[2fb35df]172 // ignore deleted candidates.
173 // NOTE: this behavior is different from main resolver.
174 // further investigations might be needed to determine
175 // if we should implement the same rule here
176 // (i.e. error if unique best match is deleted)
177 if (candidate->isDeleted) continue;
178
[b69233ac]179 // build independent unification context for candidate
180 ast::AssertionSet have, newNeed;
181 ast::TypeEnvironment newEnv{ sat.cand->env };
182 ast::OpenVarSet newOpen{ sat.cand->open };
183 ast::ptr< ast::Type > toType = assn.first->get_type();
184 ast::ptr< ast::Type > adjType =
185 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
186
187 // only keep candidates which unify
188 if ( unify( toType, adjType, newEnv, newNeed, have, newOpen, sat.symtab ) ) {
189 // set up binding slot for recursive assertions
190 ast::UniqueId crntResnSlot = 0;
191 if ( ! newNeed.empty() ) {
192 crntResnSlot = ++globalResnSlot;
193 for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
194 }
195
196 matches.emplace_back(
[07d867b]197 cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
[b69233ac]198 std::move( newOpen ), crntResnSlot );
199 }
200 }
201
202 // break if no satisfying match
203 if ( matches.empty() ) return false;
204
205 // defer if too many satisfying matches
206 if ( matches.size() > 1 ) {
207 sat.deferred.emplace_back( assn.first, assn.second, std::move( matches ) );
208 return true;
209 }
210
211 // otherwise bind unique match in ongoing scope
212 AssnCandidate & match = matches.front();
213 addToSymbolTable( match.have, sat.symtab );
214 sat.newNeed.insert( match.need.begin(), match.need.end() );
215 sat.cand->env = std::move( match.env );
216 sat.cand->open = std::move( match.open );
217
218 bindAssertion( assn.first, assn.second, sat.cand, match, sat.inferred );
219 return true;
220 }
221
222 /// Map of candidate return types to recursive assertion satisfaction costs
223 using PruneMap = std::unordered_map< std::string, CostVec >;
224
225 /// Gets the pruning key for a candidate (derived from environment-adjusted return type)
226 std::string pruneKey( const Candidate & cand ) {
227 ast::ptr< ast::Type > resType = cand.expr->result;
228 cand.env.apply( resType );
229 return Mangle::mangle( resType, Mangle::typeMode() );
230 }
231
232 /// Associates inferred parameters with an expression
233 struct InferMatcher final {
234 InferCache & inferred;
235
236 InferMatcher( InferCache & inferred ) : inferred( inferred ) {}
237
[81da70a5]238 const ast::Expr * postvisit( const ast::Expr * expr ) {
[b69233ac]239 // Skip if no slots to find
[07d867b]240 if ( !expr->inferred.hasSlots() ) return expr;
241 // if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr;
242 std::vector<UniqueId> missingSlots;
[b69233ac]243 // find inferred parameters for resolution slots
[07d867b]244 ast::InferredParams * newInferred = new ast::InferredParams();
[b69233ac]245 for ( UniqueId slot : expr->inferred.resnSlots() ) {
246 // fail if no matching assertions found
247 auto it = inferred.find( slot );
248 if ( it == inferred.end() ) {
[81da70a5]249 std::cerr << "missing assertion " << slot << std::endl;
[07d867b]250 missingSlots.push_back(slot);
[81da70a5]251 continue;
[b69233ac]252 }
253
254 // place inferred parameters into new map
255 for ( auto & entry : it->second ) {
256 // recurse on inferParams of resolved expressions
[81da70a5]257 entry.second.expr = postvisit( entry.second.expr );
[07d867b]258 auto res = newInferred->emplace( entry );
[b69233ac]259 assert( res.second && "all assertions newly placed" );
260 }
261 }
262
263 ast::Expr * ret = mutate( expr );
[07d867b]264 ret->inferred.set_inferParams( newInferred );
265 if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots;
[b69233ac]266 return ret;
267 }
268 };
269
270 /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning
271 /// threshold.
272 void finalizeAssertions(
273 CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs,
274 CandidateList & out
275 ) {
276 // prune if cheaper alternative for same key has already been generated
277 std::string key = pruneKey( *cand );
278 auto it = thresholds.find( key );
279 if ( it != thresholds.end() ) {
280 if ( it->second < costs ) return;
281 } else {
282 thresholds.emplace_hint( it, key, std::move( costs ) );
283 }
284
285 // replace resolution slots with inferred parameters, add to output
286 ast::Pass< InferMatcher > matcher{ inferred };
287 cand->expr = cand->expr->accept( matcher );
288 out.emplace_back( cand );
289 }
290
291 /// Combo iterator that combines candidates into an output list, merging their environments.
292 /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h`
293 /// for description of "combo iterator".
294 class CandidateEnvMerger {
295 /// Current list of merged candidates
296 std::vector< DeferRef > crnt;
297 /// Stack of environments to support backtracking
298 std::vector< ast::TypeEnvironment > envs;
299 /// Stack of open variables to support backtracking
300 std::vector< ast::OpenVarSet > opens;
301 /// Symbol table to use for merges
302 const ast::SymbolTable & symtab;
303
304 public:
305 /// The merged environment/open variables and the list of candidates
306 struct OutType {
307 ast::TypeEnvironment env;
308 ast::OpenVarSet open;
309 std::vector< DeferRef > assns;
310 Cost cost;
311
[cf32116]312 OutType(
313 const ast::TypeEnvironment & e, const ast::OpenVarSet & o,
[b69233ac]314 const std::vector< DeferRef > & as, const ast::SymbolTable & symtab )
315 : env( e ), open( o ), assns( as ), cost( Cost::zero ) {
316 // compute combined conversion cost
317 for ( const DeferRef & assn : assns ) {
318 // compute conversion cost from satisfying decl to assertion
[cf32116]319 cost += computeConversionCost(
320 assn.match.adjType, assn.decl->get_type(), false, symtab, env );
321
[b69233ac]322 // mark vars+specialization on function-type assertions
[cf32116]323 const ast::FunctionType * func =
[b69233ac]324 GenPoly::getFunctionType( assn.match.cdata.id->get_type() );
325 if ( ! func ) continue;
326
[954c954]327 for ( const auto & param : func->params ) {
328 cost.decSpec( specCost( param ) );
[b69233ac]329 }
[cf32116]330
[b69233ac]331 cost.incVar( func->forall.size() );
[cf32116]332
[b69233ac]333 for ( const ast::TypeDecl * td : func->forall ) {
334 cost.decSpec( td->assertions.size() );
335 }
336 }
337 }
338
339 bool operator< ( const OutType & o ) const { return cost < o.cost; }
340 };
341
[cf32116]342 CandidateEnvMerger(
343 const ast::TypeEnvironment & env, const ast::OpenVarSet & open,
[b69233ac]344 const ast::SymbolTable & syms )
345 : crnt(), envs{ env }, opens{ open }, symtab( syms ) {}
346
347 bool append( DeferRef i ) {
348 ast::TypeEnvironment env = envs.back();
349 ast::OpenVarSet open = opens.back();
350 mergeOpenVars( open, i.match.open );
351
352 if ( ! env.combine( i.match.env, open, symtab ) ) return false;
353
354 crnt.emplace_back( i );
355 envs.emplace_back( std::move( env ) );
356 opens.emplace_back( std::move( open ) );
357 return true;
358 }
359
360 void backtrack() {
361 crnt.pop_back();
362 envs.pop_back();
363 opens.pop_back();
364 }
365
366 OutType finalize() { return { envs.back(), opens.back(), crnt, symtab }; }
367 };
368
369 /// Limit to depth of recursion of assertion satisfaction
370 static const int recursionLimit = 4;
371 /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
372 static const int deferLimit = 10;
373} // anonymous namespace
374
[396037d]375void satisfyAssertions(
[b69233ac]376 CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out,
[396037d]377 std::vector<std::string> & errors
378) {
[b69233ac]379 // finish early if no assertions to satisfy
380 if ( cand->need.empty() ) {
381 out.emplace_back( cand );
382 return;
383 }
384
385 // build list of possible combinations of satisfying declarations
386 std::vector< SatState > sats{ SatState{ cand, symtab } };
387 std::vector< SatState > nextSats{};
388
389 // pruning thresholds by result type of output candidates.
390 // Candidates *should* be generated in sorted order, so no need to retroactively prune
391 PruneMap thresholds;
392
393 // satisfy assertions in breadth-first order over the recursion tree of assertion satisfaction.
394 // Stop recursion at a limited number of levels deep to avoid infinite loops.
395 for ( unsigned level = 0; level < recursionLimit; ++level ) {
396 // for each current mutually-compatible set of assertions
397 for ( SatState & sat : sats ) {
398 // stop this branch if a better option is already found
399 auto it = thresholds.find( pruneKey( *sat.cand ) );
400 if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
401
402 // make initial pass at matching assertions
403 for ( auto & assn : sat.need ) {
404 // fail early if any assertion is not satisfiable
405 if ( ! satisfyAssertion( assn, sat ) ) {
406 Indenter tabs{ 3 };
407 std::ostringstream ss;
408 ss << tabs << "Unsatisfiable alternative:\n";
409 print( ss, *sat.cand, ++tabs );
410 ss << (tabs-1) << "Could not satisfy assertion:\n";
411 ast::print( ss, assn.first, tabs );
412
413 errors.emplace_back( ss.str() );
414 goto nextSat;
415 }
416 }
417
418 if ( sat.deferred.empty() ) {
419 // either add successful match or push back next state
420 if ( sat.newNeed.empty() ) {
421 finalizeAssertions(
422 sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
423 } else {
424 nextSats.emplace_back( std::move( sat ), IterateState );
425 }
426 } else if ( sat.deferred.size() > deferLimit ) {
427 // too many deferred assertions to attempt mutual compatibility
428 Indenter tabs{ 3 };
429 std::ostringstream ss;
430 ss << tabs << "Unsatisfiable alternative:\n";
431 print( ss, *sat.cand, ++tabs );
432 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
433 for ( const auto & d : sat.deferred ) {
434 ast::print( ss, d.decl, tabs );
435 }
436
437 errors.emplace_back( ss.str() );
438 goto nextSat;
439 } else {
440 // combine deferred assertions by mutual compatibility
441 std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
442 sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
443
444 // fail early if no mutually-compatible assertion satisfaction
445 if ( compatible.empty() ) {
446 Indenter tabs{ 3 };
447 std::ostringstream ss;
448 ss << tabs << "Unsatisfiable alternative:\n";
449 print( ss, *sat.cand, ++tabs );
450 ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
451 for ( const auto& d : sat.deferred ) {
452 ast::print( ss, d.decl, tabs );
453 }
454
455 errors.emplace_back( ss.str() );
456 goto nextSat;
457 }
458
459 // sort by cost (for overall pruning order)
460 std::sort( compatible.begin(), compatible.end() );
461
462 // process mutually-compatible combinations
463 for ( auto & compat : compatible ) {
464 // set up next satisfaction state
465 CandidateRef nextCand = std::make_shared<Candidate>(
466 sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
467 ast::AssertionSet{} /* need moved into satisfaction state */,
468 sat.cand->cost, sat.cand->cvtCost );
469
470 ast::AssertionSet nextNewNeed{ sat.newNeed };
471 InferCache nextInferred{ sat.inferred };
472
473 CostVec nextCosts{ sat.costs };
474 nextCosts.back() += compat.cost;
475
476 ast::SymbolTable nextSymtab{ sat.symtab };
477
478 // add compatible assertions to new satisfaction state
479 for ( DeferRef r : compat.assns ) {
480 AssnCandidate match = r.match;
481 addToSymbolTable( match.have, nextSymtab );
482 nextNewNeed.insert( match.need.begin(), match.need.end() );
483
484 bindAssertion( r.decl, r.info, nextCand, match, nextInferred );
485 }
486
487 // either add successful match or push back next state
488 if ( nextNewNeed.empty() ) {
489 finalizeAssertions(
490 nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
491 } else {
492 nextSats.emplace_back(
493 std::move( nextCand ), std::move( nextNewNeed ),
494 std::move( nextInferred ), std::move( nextCosts ),
495 std::move( nextSymtab ) );
496 }
497 }
498 }
499 nextSat:; }
500
501 // finish or reset for next round
502 if ( nextSats.empty() ) return;
503 sats.swap( nextSats );
504 nextSats.clear();
505 }
506
507 // exceeded recursion limit if reaches here
508 if ( out.empty() ) {
509 SemanticError( cand->expr->location, "Too many recursive assertions" );
510 }
[396037d]511}
512
513} // namespace ResolvExpr
514
515// Local Variables: //
516// tab-width: 4 //
517// mode: c++ //
518// compile-command: "make install" //
[cf32116]519// End: //
Note: See TracBrowser for help on using the repository browser.