source: src/ResolvExpr/SatisfyAssertions.cpp @ 7583c02

arm-ehenumforall-pointer-decayjacob/cs343-translationnew-ast-unique-exprpthread-emulationqualifiedEnum
Last change on this file since 7583c02 was 7583c02, checked in by Fangren Yu <f37yu@…>, 2 years ago

partially improve #226: resolver environment size reduced to O(n)

generated code still has exponential size. should cache resolved implicits
and reuse thunks to reduce generated code size.
assertion fails cannot exit early and may have a minor performance
reduction.

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