source: src/ResolvExpr/SatisfyAssertions.cpp @ 3e5dd913

arm-ehjacob/cs343-translationnew-ast-unique-expr
Last change on this file since 3e5dd913 was 3e5dd913, checked in by Fangren Yu <f37yu@…>, 10 months ago

reimplement function type and eliminate deep copy

  • Property mode set to 100644
File size: 18.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 : 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 ) );
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                        // make initial pass at matching assertions
420                        for ( auto & assn : sat.need ) {
421                                // fail early if any assertion is not satisfiable
422                                if ( ! satisfyAssertion( assn, sat ) ) {
423                                        Indenter tabs{ 3 };
424                                        std::ostringstream ss;
425                                        ss << tabs << "Unsatisfiable alternative:\n";
426                                        print( ss, *sat.cand, ++tabs );
427                                        ss << (tabs-1) << "Could not satisfy assertion:\n";
428                                        ast::print( ss, assn.first, tabs );
429
430                                        errors.emplace_back( ss.str() );
431                                        goto nextSat;
432                                }
433                        }
434
435                        if ( sat.deferred.empty() ) {
436                                // either add successful match or push back next state
437                                if ( sat.newNeed.empty() ) {
438                                        finalizeAssertions( 
439                                                sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
440                                } else {
441                                        nextSats.emplace_back( std::move( sat ), IterateState );
442                                }
443                        } else if ( sat.deferred.size() > deferLimit ) {
444                                // too many deferred assertions to attempt mutual compatibility
445                                Indenter tabs{ 3 };
446                                std::ostringstream ss;
447                                ss << tabs << "Unsatisfiable alternative:\n";
448                                print( ss, *sat.cand, ++tabs );
449                                ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
450                                for ( const auto & d : sat.deferred ) {
451                                        ast::print( ss, d.expr, tabs );
452                                }
453
454                                errors.emplace_back( ss.str() );
455                                goto nextSat;
456                        } else {
457                                // combine deferred assertions by mutual compatibility
458                                std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
459                                        sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
460                               
461                                // fail early if no mutually-compatible assertion satisfaction
462                                if ( compatible.empty() ) {
463                                        Indenter tabs{ 3 };
464                                        std::ostringstream ss;
465                                        ss << tabs << "Unsatisfiable alternative:\n";
466                                        print( ss, *sat.cand, ++tabs );
467                                        ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
468                                        for ( const auto& d : sat.deferred ) {
469                                                ast::print( ss, d.expr, tabs );
470                                        }
471
472                                        errors.emplace_back( ss.str() );
473                                        goto nextSat;
474                                }
475
476                                // sort by cost (for overall pruning order)
477                                std::sort( compatible.begin(), compatible.end() );
478
479                                // process mutually-compatible combinations
480                                for ( auto & compat : compatible ) {
481                                        // set up next satisfaction state
482                                        CandidateRef nextCand = std::make_shared<Candidate>(
483                                                sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 
484                                                ast::AssertionSet{} /* need moved into satisfaction state */,
485                                                sat.cand->cost, sat.cand->cvtCost );
486
487                                        ast::AssertionSet nextNewNeed{ sat.newNeed };
488                                        InferCache nextInferred{ sat.inferred };
489                                       
490                                        CostVec nextCosts{ sat.costs };
491                                        nextCosts.back() += compat.cost;
492                                                               
493                                        ast::SymbolTable nextSymtab{ sat.symtab };
494
495                                        // add compatible assertions to new satisfaction state
496                                        for ( DeferRef r : compat.assns ) {
497                                                AssnCandidate match = r.match;
498                                                addToSymbolTable( match.have, nextSymtab );
499                                                nextNewNeed.insert( match.need.begin(), match.need.end() );
500
501                                                bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
502                                        }
503
504                                        // either add successful match or push back next state
505                                        if ( nextNewNeed.empty() ) {
506                                                finalizeAssertions( 
507                                                        nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
508                                        } else {
509                                                nextSats.emplace_back( 
510                                                        std::move( nextCand ), std::move( nextNewNeed ), 
511                                                        std::move( nextInferred ), std::move( nextCosts ), 
512                                                        std::move( nextSymtab ) );
513                                        }
514                                }
515                        }
516                nextSat:; }
517
518                // finish or reset for next round
519                if ( nextSats.empty() ) return;
520                sats.swap( nextSats );
521                nextSats.clear();
522        }
523       
524        // exceeded recursion limit if reaches here
525        if ( out.empty() ) {
526                SemanticError( cand->expr->location, "Too many recursive assertions" );
527        }
528}
529
530} // namespace ResolvExpr
531
532// Local Variables: //
533// tab-width: 4 //
534// mode: c++ //
535// compile-command: "make install" //
536// End: //
Note: See TracBrowser for help on using the repository browser.