source: src/ResolvExpr/ResolveAssertions.cc@ 043a5b6

ADT arm-eh ast-experimental enum forall-pointer-decay jacob/cs343-translation jenkins-sandbox new-ast new-ast-unique-expr pthread-emulation qualifiedEnum
Last change on this file since 043a5b6 was c519942, checked in by Aaron Moss <a3moss@…>, 6 years ago

Fix bugs in assertion satisfaction costing

  • Calculate vars/spec cost based on satisfying decl not assn decl
  • Correct caching behaviour for defer combo costs
  • Property mode set to 100644
File size: 16.0 KB
RevLine 
[6d6e829]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// ResolveAssertions.cc --
8//
9// Author : Aaron B. Moss
10// Created On : Fri Oct 05 13:46:00 2018
11// Last Modified By : Aaron B. Moss
12// Last Modified On : Fri Oct 05 13:46:00 2018
13// Update Count : 1
14//
15
16#include "ResolveAssertions.h"
17
[b3bd772]18#include <algorithm> // for sort
[83ab931]19#include <cassert> // for assertf
20#include <list> // for list
[b3bd772]21#include <memory> // for unique_ptr
[4d2d45f9]22#include <sstream> // for ostringstream
23#include <string> // for string
[83ab931]24#include <unordered_map> // for unordered_map, unordered_multimap
25#include <utility> // for move
26#include <vector> // for vector
27
28#include "Alternative.h" // for Alternative, AssertionItem, AssertionList
29#include "Common/FilterCombos.h" // for filterCombos
[4d2d45f9]30#include "Common/Indenter.h" // for Indenter
[83ab931]31#include "Common/utility.h" // for sort_mins
32#include "ResolvExpr/RenameVars.h" // for renameTyVars
33#include "SymTab/Indexer.h" // for Indexer
[b3bd772]34#include "SymTab/Mangler.h" // for Mangler
[83ab931]35#include "SynTree/Expression.h" // for InferredParams
36#include "TypeEnvironment.h" // for TypeEnvironment, etc.
[052cd71]37#include "typeops.h" // for adjustExprType, specCost
[83ab931]38#include "Unify.h" // for unify
[6d6e829]39
40namespace ResolvExpr {
41 /// Unified assertion candidate
42 struct AssnCandidate {
43 SymTab::Indexer::IdData cdata; ///< Satisfying declaration
44 Type* adjType; ///< Satisfying type
45 TypeEnvironment env; ///< Post-unification environment
46 AssertionSet have; ///< Post-unification have-set
47 AssertionSet need; ///< Post-unification need-set
48 OpenVarSet openVars; ///< Post-unification open-var set
[0b00df0]49 UniqueId resnSlot; ///< Slot for any recursive assertion IDs
[6d6e829]50
51 AssnCandidate( const SymTab::Indexer::IdData& cdata, Type* adjType, TypeEnvironment&& env,
[0b00df0]52 AssertionSet&& have, AssertionSet&& need, OpenVarSet&& openVars, UniqueId resnSlot )
[6d6e829]53 : cdata(cdata), adjType(adjType), env(std::move(env)), have(std::move(have)),
[0b00df0]54 need(std::move(need)), openVars(std::move(openVars)), resnSlot(resnSlot) {}
[6d6e829]55 };
56
57 /// List of candidate assertion resolutions
58 using CandidateList = std::vector<AssnCandidate>;
59
60 /// Reference to single deferred item
61 struct DeferRef {
[052cd71]62 const DeclarationWithType* decl;
63 const AssertionSetValue& info;
[6d6e829]64 const AssnCandidate& match;
65 };
66
67 /// Wrapper for the deferred items from a single assertion resolution.
68 /// Acts like indexed list of DeferRef
69 struct DeferItem {
[052cd71]70 const DeclarationWithType* decl;
71 const AssertionSetValue& info;
72 CandidateList matches;
[6d6e829]73
[052cd71]74 DeferItem( DeclarationWithType* decl, const AssertionSetValue& info, CandidateList&& matches )
75 : decl(decl), info(info), matches(std::move(matches)) {}
[6d6e829]76
[052cd71]77 bool empty() const { return matches.empty(); }
[6d6e829]78
[052cd71]79 CandidateList::size_type size() const { return matches.size(); }
[4d2d45f9]80
[052cd71]81 DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
[6d6e829]82 };
83
84 /// List of deferred resolution items
85 using DeferList = std::vector<DeferItem>;
86
87 /// Combo iterator that combines candidates into an output list, merging their environments.
88 /// Rejects an appended candidate if the environments cannot be merged.
89 class CandidateEnvMerger {
90 /// Current list of merged candidates
91 std::vector<DeferRef> crnt;
92 /// Stack of environments to support backtracking
93 std::vector<TypeEnvironment> envs;
94 /// Stack of open variables to support backtracking
95 std::vector<OpenVarSet> varSets;
96 /// Indexer to use for merges
97 const SymTab::Indexer& indexer;
98
99 public:
100 /// The merged environment/open variables and the list of candidates
101 struct OutType {
102 TypeEnvironment env;
103 OpenVarSet openVars;
104 std::vector<DeferRef> assns;
[c519942]105 Cost cost;
[6d6e829]106
107 OutType( const TypeEnvironment& env, const OpenVarSet& openVars,
108 const std::vector<DeferRef>& assns )
[c519942]109 : env(env), openVars(openVars), assns(assns), cost(Cost::infinity) {}
[6d6e829]110 };
111
112 CandidateEnvMerger( const TypeEnvironment& env, const OpenVarSet& openVars,
113 const SymTab::Indexer& indexer )
114 : crnt(), envs{ env }, varSets{ openVars }, indexer(indexer) {}
115
116 bool append( DeferRef i ) {
117 TypeEnvironment env = envs.back();
118 OpenVarSet openVars = varSets.back();
119 mergeOpenVars( openVars, i.match.openVars );
120
121 if ( ! env.combine( i.match.env, openVars, indexer ) ) return false;
122
123 crnt.emplace_back( i );
124 envs.emplace_back( env );
125 varSets.emplace_back( openVars );
126 return true;
127 }
128
129 void backtrack() {
130 crnt.pop_back();
131 envs.pop_back();
132 varSets.pop_back();
133 }
134
135 OutType finalize() { return { envs.back(), varSets.back(), crnt }; }
136 };
137
[fbecee5]138 /// Comparator for CandidateEnvMerger outputs that sums their costs and caches the stored
139 /// sums
140 struct CandidateCost {
141 using Element = CandidateEnvMerger::OutType;
142 private:
143 const SymTab::Indexer& indexer; ///< Indexer for costing
144
145 public:
146 CandidateCost( const SymTab::Indexer& indexer ) : indexer(indexer) {}
147
148 /// reports the cost of an element
[c519942]149 Cost get( Element& x ) const {
150 // check cached cost
151 if ( x.cost != Cost::infinity ) return x.cost;
152
153 // generate cost
154 Cost k = Cost::zero;
155 for ( const auto& assn : x.assns ) {
156 k += computeConversionCost(
157 assn.match.adjType, assn.decl->get_type(), indexer, x.env );
158
159 // mark vars+specialization cost on function-type assertions
160 Type* assnType = assn.match.cdata.id->get_type();
161 FunctionType* func;
162 if ( PointerType* ptr = dynamic_cast< PointerType* >( assnType ) ) {
163 func = dynamic_cast< FunctionType* >( ptr->base );
164 } else {
165 func = dynamic_cast< FunctionType* >( assnType );
166 }
167 if ( ! func ) continue;
168
169 for ( DeclarationWithType* formal : func->parameters ) {
170 k.decSpec( specCost( formal->get_type() ) );
171 }
172 k.incVar( func->forall.size() );
173 for ( TypeDecl* td : func->forall ) {
174 k.decSpec( td->assertions.size() );
[fbecee5]175 }
176 }
[c519942]177
178 // cache and return
179 x.cost = k;
180 return k;
[fbecee5]181 }
182
183 /// compares elements by cost
[c519942]184 bool operator() ( Element& a, Element& b ) const {
[fbecee5]185 return get( a ) < get( b );
186 }
187 };
188
[0b00df0]189 /// Set of assertion resolutions, grouped by resolution ID
190 using InferCache = std::unordered_map< UniqueId, InferredParams >;
191
[6d6e829]192 /// Flag for state iteration
193 enum IterateFlag { IterateState };
194
195 /// State needed to resolve a set of assertions
196 struct ResnState {
[0b00df0]197 Alternative alt; ///< Alternative assertion is rooted on
198 AssertionList need; ///< Assertions to find
199 AssertionSet newNeed; ///< New assertions for current resolutions
200 DeferList deferred; ///< Deferred matches
201 InferCache inferred; ///< Cache of already-inferred parameters
202 SymTab::Indexer& indexer; ///< Name lookup (depends on previous assertions)
[6d6e829]203
204 /// Initial resolution state for an alternative
205 ResnState( Alternative& a, SymTab::Indexer& indexer )
[0b00df0]206 : alt(a), need(), newNeed(), deferred(), inferred(), indexer(indexer) {
[6d6e829]207 need.swap( a.need );
208 }
209
210 /// Updated resolution state with new need-list
211 ResnState( ResnState&& o, IterateFlag )
212 : alt(std::move(o.alt)), need(o.newNeed.begin(), o.newNeed.end()), newNeed(), deferred(),
[0b00df0]213 inferred(std::move(o.inferred)), indexer(o.indexer) {}
[6d6e829]214 };
215
216 /// Binds a single assertion, updating resolution state
217 void bindAssertion( const DeclarationWithType* decl, AssertionSetValue info, Alternative& alt,
[0b00df0]218 AssnCandidate& match, InferCache& inferred ) {
[6d6e829]219
220 DeclarationWithType* candidate = match.cdata.id;
221 assertf( candidate->get_uniqueId(), "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
222
223 Expression* varExpr = match.cdata.combine( alt.cvtCost );
[2c187378]224 delete varExpr->result;
225 varExpr->result = match.adjType->clone();
[0b00df0]226 if ( match.resnSlot ) { varExpr->resnSlots.push_back( match.resnSlot ); }
[6d6e829]227
[0b00df0]228 // place newly-inferred assertion in proper place in cache
229 inferred[ info.resnSlot ][ decl->get_uniqueId() ] = ParamEntry{
[9aaacc27]230 candidate->get_uniqueId(), match.adjType->clone(), decl->get_type()->clone(),
231 varExpr };
[6d6e829]232 }
233
234 /// Adds a captured assertion to the symbol table
235 void addToIndexer( AssertionSet &assertSet, SymTab::Indexer &indexer ) {
[e1f7eef]236 for ( auto& i : assertSet ) {
237 if ( i.second.isUsed ) {
238 indexer.addId( i.first );
[6d6e829]239 }
240 }
241 }
242
[0b00df0]243 // in AlternativeFinder.cc; unique ID for assertion resolutions
244 extern UniqueId globalResnSlot;
245
[6d6e829]246 /// Resolve a single assertion, in context
[052cd71]247 bool resolveAssertion( AssertionItem& assn, ResnState& resn ) {
[6d6e829]248 // skip unused assertions
249 if ( ! assn.info.isUsed ) return true;
250
[052cd71]251 // lookup candidates for this assertion
252 std::list< SymTab::Indexer::IdData > candidates;
253 resn.indexer.lookupId( assn.decl->name, candidates );
254
255 // find the candidates that unify with the desired type
256 CandidateList matches;
257 for ( const auto& cdata : candidates ) {
258 DeclarationWithType* candidate = cdata.id;
259
260 // build independent unification context for candidate
261 AssertionSet have, newNeed;
262 TypeEnvironment newEnv{ resn.alt.env };
263 OpenVarSet newOpenVars{ resn.alt.openVars };
264 Type* adjType = candidate->get_type()->clone();
265 adjustExprType( adjType, newEnv, resn.indexer );
266 renameTyVars( adjType );
267
268 // keep unifying candidates
269 if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars,
270 resn.indexer ) ) {
271 // set up binding slot for recursive assertions
272 UniqueId crntResnSlot = 0;
273 if ( ! newNeed.empty() ) {
274 crntResnSlot = ++globalResnSlot;
275 for ( auto& a : newNeed ) {
276 a.second.resnSlot = crntResnSlot;
[0b00df0]277 }
[2fd9f24]278 }
[e1f7eef]279
[052cd71]280 matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have),
281 std::move(newNeed), std::move(newOpenVars), crntResnSlot );
282 } else {
283 delete adjType;
284 }
[6d6e829]285 }
286
287 // break if no suitable assertion
288 if ( matches.empty() ) return false;
289
290 // defer if too many suitable assertions
291 if ( matches.size() > 1 ) {
[052cd71]292 resn.deferred.emplace_back( assn.decl, assn.info, std::move(matches) );
[6d6e829]293 return true;
294 }
295
296 // otherwise bind current match in ongoing scope
297 AssnCandidate& match = matches.front();
298 addToIndexer( match.have, resn.indexer );
299 resn.newNeed.insert( match.need.begin(), match.need.end() );
[052cd71]300 resn.alt.env = std::move(match.env);
301 resn.alt.openVars = std::move(match.openVars);
[6d6e829]302
[0b00df0]303 bindAssertion( assn.decl, assn.info, resn.alt, match, resn.inferred );
[6d6e829]304 return true;
305 }
306
[0b00df0]307 /// Associates inferred parameters with an expression
308 struct InferMatcher {
309 InferCache& inferred;
310
311 InferMatcher( InferCache& inferred ) : inferred( inferred ) {}
312
313 Expression* postmutate( Expression* expr ) {
[40290497]314 // defer missing inferred parameters until they are hopefully found later
315 std::vector<UniqueId> missingSlots;
[0b00df0]316 // place inferred parameters into resolution slots
317 for ( UniqueId slot : expr->resnSlots ) {
318 // fail if no matching parameters found
[40290497]319 auto it = inferred.find( slot );
320 if ( it == inferred.end() ) {
321 missingSlots.push_back( slot );
322 continue;
323 }
324 InferredParams& inferParams = it->second;
[0b00df0]325
326 // place inferred parameters into proper place in expression
327 for ( auto& entry : inferParams ) {
328 // recurse on inferParams of resolved expressions
329 entry.second.expr = postmutate( entry.second.expr );
330 // xxx - look at entry.second.inferParams?
331 expr->inferParams[ entry.first ] = entry.second;
332 }
333 }
334
335 // clear resolution slots and return
[40290497]336 expr->resnSlots.swap( missingSlots );
[0b00df0]337 return expr;
338 }
339 };
340
341 void finalizeAssertions( Alternative& alt, InferCache& inferred, AltList& out ) {
342 PassVisitor<InferMatcher> matcher{ inferred };
343 alt.expr = alt.expr->acceptMutator( matcher );
344 out.emplace_back( alt );
345 }
346
347 /// Limit to depth of recursion of assertion satisfaction
[6d6e829]348 static const int recursionLimit = /* 10 */ 4;
349
[4d2d45f9]350 void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out, std::list<std::string>& errors ) {
[6d6e829]351 // finish early if no assertions to resolve
352 if ( alt.need.empty() ) {
353 out.emplace_back( alt );
354 return;
355 }
356
357 // build list of possible resolutions
358 using ResnList = std::vector<ResnState>;
359 SymTab::Indexer root_indexer{ indexer };
360 ResnList resns{ ResnState{ alt, root_indexer } };
361 ResnList new_resns{};
362
363 // resolve assertions in breadth-first-order up to a limited number of levels deep
364 for ( unsigned level = 0; level < recursionLimit; ++level ) {
365 // scan over all mutually-compatible resolutions
366 for ( auto& resn : resns ) {
367 // make initial pass at matching assertions
368 for ( auto& assn : resn.need ) {
369 // fail early if any assertion is not resolvable
[052cd71]370 if ( ! resolveAssertion( assn, resn ) ) {
[4d2d45f9]371 Indenter tabs{ Indenter::tabsize, 3 };
372 std::ostringstream ss;
373 ss << tabs << "Unsatisfiable alternative:\n";
374 resn.alt.print( ss, ++tabs );
375 ss << --tabs << "Could not satisfy assertion:\n";
376 assn.decl->print( ss, ++tabs );
377
378 errors.emplace_back( ss.str() );
379 goto nextResn;
380 }
[6d6e829]381 }
382
383 if ( resn.deferred.empty() ) {
384 // either add successful match or push back next state
385 if ( resn.newNeed.empty() ) {
[0b00df0]386 finalizeAssertions( resn.alt, resn.inferred, out );
[6d6e829]387 } else {
388 new_resns.emplace_back( std::move(resn), IterateState );
389 }
390 } else {
[b3bd772]391 // resolve deferred assertions by mutual compatibility
[6d6e829]392 std::vector<CandidateEnvMerger::OutType> compatible = filterCombos(
393 resn.deferred,
394 CandidateEnvMerger{ resn.alt.env, resn.alt.openVars, resn.indexer } );
[4d2d45f9]395 // fail early if no mutually-compatible assertion satisfaction
396 if ( compatible.empty() ) {
397 Indenter tabs{ Indenter::tabsize, 3 };
398 std::ostringstream ss;
399 ss << tabs << "Unsatisfiable alternative:\n";
400 resn.alt.print( ss, ++tabs );
401 ss << --tabs << "No mutually-compatible satisfaction for assertions:\n";
402 ++tabs;
403 for ( const auto& d : resn.deferred ) {
[052cd71]404 d.decl->print( ss, tabs );
[4d2d45f9]405 }
406
407 errors.emplace_back( ss.str() );
408 goto nextResn;
409 }
[b3bd772]410 // sort by cost
411 CandidateCost coster{ resn.indexer };
412 std::sort( compatible.begin(), compatible.end(), coster );
413
414 // keep map of detected options
415 std::unordered_map<std::string, Cost> found;
416 for ( auto& compat : compatible ) {
417 // filter by environment-adjusted result type, keep only cheapest option
418 Type* resType = alt.expr->result->clone();
419 compat.env.apply( resType );
420 // skip if cheaper alternative already processed with same result type
421 Cost resCost = coster.get( compat );
422 auto it = found.emplace( SymTab::Mangler::mangleType( resType ), resCost );
[aeb8f70]423 delete resType;
[b3bd772]424 if ( it.second == false && it.first->second < resCost ) continue;
425
426 // proceed with resolution step
[6d6e829]427 ResnState new_resn = resn;
428
429 // add compatible assertions to new resolution state
430 for ( DeferRef r : compat.assns ) {
431 AssnCandidate match = r.match;
432 addToIndexer( match.have, new_resn.indexer );
433 new_resn.newNeed.insert( match.need.begin(), match.need.end() );
434
[052cd71]435 bindAssertion( r.decl, r.info, new_resn.alt, match, new_resn.inferred );
[6d6e829]436 }
437
438 // set mutual environment into resolution state
439 new_resn.alt.env = std::move(compat.env);
440 new_resn.alt.openVars = std::move(compat.openVars);
441
442 // either add sucessful match or push back next state
443 if ( new_resn.newNeed.empty() ) {
[0b00df0]444 finalizeAssertions( new_resn.alt, new_resn.inferred, out );
[6d6e829]445 } else {
446 new_resns.emplace_back( std::move(new_resn), IterateState );
447 }
448 }
449 }
450 nextResn:; }
451
452 // finish or reset for next round
453 if ( new_resns.empty() ) return;
454 resns.swap( new_resns );
455 new_resns.clear();
456 }
457
458 // exceeded recursion limit if reaches here
459 if ( out.empty() ) {
460 SemanticError( alt.expr->location, "Too many recursive assertions" );
461 }
462 }
463} // namespace ResolvExpr
464
465// Local Variables: //
466// tab-width: 4 //
467// mode: c++ //
468// compile-command: "make install" //
469// End: //
Note: See TracBrowser for help on using the repository browser.