source: src/ResolvExpr/SatisfyAssertions.cpp @ 9cd5bd2

ADTast-experimentalpthread-emulation
Last change on this file since 9cd5bd2 was ef1da0e2, checked in by Fangren Yu <f37yu@…>, 2 years ago

try to make parameter qualifier conversion work for assertions

  • Property mode set to 100644
File size: 20.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 "FindOpenVars.h"
39#include "Common/FilterCombos.h"
40#include "Common/Indenter.h"
41#include "GenPoly/GenPoly.h"
42#include "SymTab/Mangler.h"
43
44namespace ResolvExpr {
45
46// in CandidateFinder.cpp; unique ID for assertion satisfaction
47extern UniqueId globalResnSlot;
48
49namespace {
50        /// Post-unification assertion satisfaction candidate
51        struct AssnCandidate {
52                ast::SymbolTable::IdData cdata;  ///< Satisfying declaration
53                ast::ptr< ast::Type > adjType;   ///< Satisfying type
54                ast::TypeEnvironment env;        ///< Post-unification environment
55                ast::AssertionSet have;          ///< Post-unification have-set
56                ast::AssertionSet need;          ///< Post-unification need-set
57                ast::OpenVarSet open;            ///< Post-unification open-var-set
58                ast::UniqueId resnSlot;          ///< Slot for any recursive assertion IDs
59
60                AssnCandidate(
61                        const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e,
62                        ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs )
63                : cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ),
64                  need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {}
65        };
66
67        /// List of assertion satisfaction candidates
68        using AssnCandidateList = std::vector< AssnCandidate >;
69
70        /// Reference to a single deferred item
71        struct DeferRef {
72                const ast::VariableExpr * expr;
73                const ast::AssertionSetValue & info;
74                const AssnCandidate & match;
75        };
76
77        /// Wrapper for the deferred items from a single assertion satisfaction.
78        /// Acts like an indexed list of DeferRef
79        struct DeferItem {
80                const ast::VariableExpr * expr;
81                const ast::AssertionSetValue & info;
82                AssnCandidateList matches;
83
84                DeferItem(
85                        const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
86                : expr( d ), info( i ), matches( std::move( ms ) ) {}
87
88                bool empty() const { return matches.empty(); }
89
90                AssnCandidateList::size_type size() const { return matches.size(); }
91
92                DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
93        };
94
95        /// List of deferred satisfaction items
96        using DeferList = std::vector< DeferItem >;
97
98        /// Set of assertion satisfactions, grouped by resolution ID
99        using InferCache = std::unordered_map< ast::UniqueId, ast::InferredParams >;
100
101        /// Lexicographically-ordered vector of costs.
102        /// Lexicographic order comes from default operator< on std::vector.
103        using CostVec = std::vector< Cost >;
104
105        /// Flag for state iteration
106        enum IterateFlag { IterateState };
107
108        /// Intermediate state for satisfying a set of assertions
109        struct SatState {
110                CandidateRef cand;          ///< Candidate assertion is rooted on
111                ast::AssertionList need;    ///< Assertions to find
112                ast::AssertionSet newNeed;  ///< Recursive assertions from current satisfied assertions
113                DeferList deferred;         ///< Deferred matches
114                InferCache inferred;        ///< Cache of already-inferred assertions
115                CostVec costs;              ///< Disambiguating costs of recursive assertion satisfaction
116                ast::SymbolTable symtab;    ///< Name lookup (depends on previous assertions)
117
118                /// Initial satisfaction state for a candidate
119                SatState( CandidateRef & c, const ast::SymbolTable & syms )
120                : cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero },
121                  symtab( syms ) { need.swap( c->need ); }
122
123                /// Update satisfaction state for next step after previous state
124                SatState( SatState && o, IterateFlag )
125                : cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(),
126                  deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ),
127                  symtab( o.symtab ) { costs.emplace_back( Cost::zero ); }
128
129                /// Field-wise next step constructor
130                SatState(
131                        CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs,
132                        ast::SymbolTable && syms )
133                : cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(),
134                  inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) )
135                  { costs.emplace_back( Cost::zero ); }
136        };
137
138        /// Adds a captured assertion to the symbol table
139        void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
140                for ( auto & i : have ) {
141                        if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
142                }
143        }
144
145        /// Binds a single assertion, updating satisfaction state
146        void bindAssertion(
147                const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand,
148                AssnCandidate & match, InferCache & inferred
149        ) {
150                const ast::DeclWithType * candidate = match.cdata.id;
151                assertf( candidate->uniqueId,
152                        "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
153
154                ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost );
155                varExpr->result = match.adjType;
156                if ( match.resnSlot ) { varExpr->inferred.resnSlots().emplace_back( match.resnSlot ); }
157
158                // place newly-inferred assertion in proper location in cache
159                inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
160                        candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
161        }
162
163        /// Satisfy a single assertion
164        bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat, bool allowConversion = false, bool skipUnbound = false) {
165                // skip unused assertions
166                if ( ! assn.second.isUsed ) return true;
167
168                // find candidates that unify with the desired type
169                AssnCandidateList matches;
170
171                std::vector<ast::SymbolTable::IdData> candidates;
172                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
173                if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
174                        // prefilter special decls by argument type, if already known
175                        ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
176                                .strict_as<ast::FunctionType>()->params[0]
177                                .strict_as<ast::ReferenceType>()->base;
178                        sat.cand->env.apply(thisArgType);
179
180                        std::string otypeKey = "";
181                        if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer;
182                        else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type | Mangle::NoGenericParams);
183                        else if (skipUnbound) return false;
184
185                        candidates = sat.symtab.specialLookupId(kind, otypeKey);
186                }
187                else {
188                        candidates = sat.symtab.lookupId(assn.first->var->name);
189                }
190                for ( const ast::SymbolTable::IdData & cdata : candidates ) {
191                        const ast::DeclWithType * candidate = cdata.id;
192
193                        // ignore deleted candidates.
194                        // NOTE: this behavior is different from main resolver.
195                        // further investigations might be needed to determine
196                        // if we should implement the same rule here
197                        // (i.e. error if unique best match is deleted)
198                        if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue;
199
200                        // build independent unification context for candidate
201                        ast::AssertionSet have, newNeed;
202                        ast::TypeEnvironment newEnv{ sat.cand->env };
203                        ast::OpenVarSet newOpen{ sat.cand->open };
204                        ast::ptr< ast::Type > toType = assn.first->result;
205                        ast::ptr< ast::Type > adjType =
206                                renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
207
208                        // only keep candidates which unify
209
210                        ast::OpenVarSet closed;
211                        findOpenVars( toType, newOpen, closed, newNeed, have, FirstClosed );
212                        findOpenVars( adjType, newOpen, closed, newNeed, have, FirstOpen );
213                        if ( allowConversion ) {
214                                if ( auto c = commonType( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {
215                                        // set up binding slot for recursive assertions
216                                        ast::UniqueId crntResnSlot = 0;
217                                        if ( ! newNeed.empty() ) {
218                                                crntResnSlot = ++globalResnSlot;
219                                                for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
220                                        }
221
222                                        matches.emplace_back(
223                                                cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
224                                                std::move( newOpen ), crntResnSlot );
225                                }
226                        }
227                        else {
228                                if ( unifyExact( toType, adjType, newEnv, newNeed, have, newOpen, WidenMode {true, true}, sat.symtab ) ) {
229                                        // set up binding slot for recursive assertions
230                                        ast::UniqueId crntResnSlot = 0;
231                                        if ( ! newNeed.empty() ) {
232                                                crntResnSlot = ++globalResnSlot;
233                                                for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
234                                        }
235
236                                        matches.emplace_back(
237                                                cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
238                                                std::move( newOpen ), crntResnSlot );
239                                }
240                        }
241                }
242
243                // break if no satisfying match
244                if ( matches.empty() ) return false;
245
246                // defer if too many satisfying matches
247                if ( matches.size() > 1 ) {
248                        sat.deferred.emplace_back( assn.first, assn.second, std::move( matches ) );
249                        return true;
250                }
251
252                // otherwise bind unique match in ongoing scope
253                AssnCandidate & match = matches.front();
254                addToSymbolTable( match.have, sat.symtab );
255                sat.newNeed.insert( match.need.begin(), match.need.end() );
256                sat.cand->env = std::move( match.env );
257                sat.cand->open = std::move( match.open );
258
259                bindAssertion( assn.first, assn.second, sat.cand, match, sat.inferred );
260                return true;
261        }
262
263        /// Map of candidate return types to recursive assertion satisfaction costs
264        using PruneMap = std::unordered_map< std::string, CostVec >;
265
266        /// Gets the pruning key for a candidate (derived from environment-adjusted return type)
267        std::string pruneKey( const Candidate & cand ) {
268                ast::ptr< ast::Type > resType = cand.expr->result;
269                cand.env.apply( resType );
270                return Mangle::mangle( resType, Mangle::typeMode() );
271        }
272
273        /// Associates inferred parameters with an expression
274        struct InferMatcher final {
275                InferCache & inferred;
276
277                InferMatcher( InferCache & inferred ) : inferred( inferred ) {}
278
279                const ast::Expr * postvisit( const ast::Expr * expr ) {
280                        // Skip if no slots to find
281                        if ( !expr->inferred.hasSlots() ) return expr;
282                        // if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr;
283                        std::vector<UniqueId> missingSlots;
284                        // find inferred parameters for resolution slots
285                        ast::InferredParams * newInferred = new ast::InferredParams();
286                        for ( UniqueId slot : expr->inferred.resnSlots() ) {
287                                // fail if no matching assertions found
288                                auto it = inferred.find( slot );
289                                if ( it == inferred.end() ) {
290                                        // std::cerr << "missing assertion " << slot << std::endl;
291                                        missingSlots.push_back(slot);
292                                        continue;
293                                }
294
295                                // place inferred parameters into new map
296                                for ( auto & entry : it->second ) {
297                                        // recurse on inferParams of resolved expressions
298                                        entry.second.expr = postvisit( entry.second.expr );
299                                        auto res = newInferred->emplace( entry );
300                                        assert( res.second && "all assertions newly placed" );
301                                }
302                        }
303
304                        ast::Expr * ret = mutate( expr );
305                        ret->inferred.set_inferParams( newInferred );
306                        if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots;
307                        return ret;
308                }
309        };
310
311        /// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning
312        /// threshold.
313        void finalizeAssertions(
314                CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs,
315                CandidateList & out
316        ) {
317                // prune if cheaper alternative for same key has already been generated
318                std::string key = pruneKey( *cand );
319                auto it = thresholds.find( key );
320                if ( it != thresholds.end() ) {
321                        if ( it->second < costs ) return;
322                } else {
323                        thresholds.emplace_hint( it, key, std::move( costs ) );
324                }
325
326                // replace resolution slots with inferred parameters, add to output
327                ast::Pass< InferMatcher > matcher{ inferred };
328                cand->expr = cand->expr->accept( matcher );
329                out.emplace_back( cand );
330        }
331
332        /// Combo iterator that combines candidates into an output list, merging their environments.
333        /// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h`
334        /// for description of "combo iterator".
335        class CandidateEnvMerger {
336                /// Current list of merged candidates
337                std::vector< DeferRef > crnt;
338                /// Stack of environments to support backtracking
339                std::vector< ast::TypeEnvironment > envs;
340                /// Stack of open variables to support backtracking
341                std::vector< ast::OpenVarSet > opens;
342                /// Symbol table to use for merges
343                const ast::SymbolTable & symtab;
344
345        public:
346                /// The merged environment/open variables and the list of candidates
347                struct OutType {
348                        ast::TypeEnvironment env;
349                        ast::OpenVarSet open;
350                        std::vector< DeferRef > assns;
351                        Cost cost;
352
353                        OutType(
354                                const ast::TypeEnvironment & e, const ast::OpenVarSet & o,
355                                const std::vector< DeferRef > & as, const ast::SymbolTable & symtab )
356                        : env( e ), open( o ), assns( as ), cost( Cost::zero ) {
357                                // compute combined conversion cost
358                                for ( const DeferRef & assn : assns ) {
359                                        // compute conversion cost from satisfying decl to assertion
360                                        cost += computeConversionCost(
361                                                assn.match.adjType, assn.expr->result, false, symtab, env );
362
363                                        // mark vars+specialization on function-type assertions
364                                        const ast::FunctionType * func =
365                                                GenPoly::getFunctionType( assn.match.cdata.id->get_type() );
366                                        if ( ! func ) continue;
367
368                                        for ( const auto & param : func->params ) {
369                                                cost.decSpec( specCost( param ) );
370                                        }
371
372                                        cost.incVar( func->forall.size() );
373
374                                        cost.decSpec( func->assertions.size() );
375                                }
376                        }
377
378                        bool operator< ( const OutType & o ) const { return cost < o.cost; }
379                };
380
381                CandidateEnvMerger(
382                        const ast::TypeEnvironment & env, const ast::OpenVarSet & open,
383                        const ast::SymbolTable & syms )
384                : crnt(), envs{ env }, opens{ open }, symtab( syms ) {}
385
386                bool append( DeferRef i ) {
387                        ast::TypeEnvironment env = envs.back();
388                        ast::OpenVarSet open = opens.back();
389                        mergeOpenVars( open, i.match.open );
390
391                        if ( ! env.combine( i.match.env, open, symtab ) ) return false;
392
393                        crnt.emplace_back( i );
394                        envs.emplace_back( std::move( env ) );
395                        opens.emplace_back( std::move( open ) );
396                        return true;
397                }
398
399                void backtrack() {
400                        crnt.pop_back();
401                        envs.pop_back();
402                        opens.pop_back();
403                }
404
405                OutType finalize() { return { envs.back(), opens.back(), crnt, symtab }; }
406        };
407
408        /// Limit to depth of recursion of assertion satisfaction
409        static const int recursionLimit = 8;
410        /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
411        static const int deferLimit = 10;
412} // anonymous namespace
413
414void satisfyAssertions(
415        CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out,
416        std::vector<std::string> & errors
417) {
418        // finish early if no assertions to satisfy
419        if ( cand->need.empty() ) {
420                out.emplace_back( cand );
421                return;
422        }
423
424        // build list of possible combinations of satisfying declarations
425        std::vector< SatState > sats{ SatState{ cand, symtab } };
426        std::vector< SatState > nextSats{};
427
428        // pruning thresholds by result type of output candidates.
429        // Candidates *should* be generated in sorted order, so no need to retroactively prune
430        PruneMap thresholds;
431
432        // satisfy assertions in breadth-first order over the recursion tree of assertion satisfaction.
433        // Stop recursion at a limited number of levels deep to avoid infinite loops.
434        for ( unsigned level = 0; level < recursionLimit; ++level ) {
435                // for each current mutually-compatible set of assertions
436                for ( SatState & sat : sats ) {
437                        bool allowConversion = false;
438                        // stop this branch if a better option is already found
439                        auto it = thresholds.find( pruneKey( *sat.cand ) );
440                        if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
441
442                        // should a limit be imposed? worst case here is O(n^2) but very unlikely to happen.
443
444                        for (unsigned resetCount = 0; ; ++resetCount) {
445                                ast::AssertionList next;
446                                resetTyVarRenaming();
447                                // make initial pass at matching assertions
448                                for ( auto & assn : sat.need ) {
449                                        // fail early if any assertion is not satisfiable
450                                        if ( ! satisfyAssertion( assn, sat, allowConversion, !next.empty() ) ) {
451                                                next.emplace_back(assn);
452                                                // goto nextSat;
453                                        }
454                                }
455                                // success
456                                if (next.empty()) break;
457                                // fail if nothing resolves
458                                else if (next.size() == sat.need.size()) {
459                                        if (allowConversion) {
460                                                Indenter tabs{ 3 };
461                                                std::ostringstream ss;
462                                                ss << tabs << "Unsatisfiable alternative:\n";
463                                                print( ss, *sat.cand, ++tabs );
464                                                ss << (tabs-1) << "Could not satisfy assertion:\n";
465                                                ast::print( ss, next[0].first, tabs );
466
467                                                errors.emplace_back( ss.str() );
468                                                goto nextSat;
469                                        }
470
471                                        else {
472                                                allowConversion = true;
473                                                continue;
474                                        }
475                                }
476                                allowConversion = false;
477                                sat.need = std::move(next);
478                        }
479
480                        if ( sat.deferred.empty() ) {
481                                // either add successful match or push back next state
482                                if ( sat.newNeed.empty() ) {
483                                        finalizeAssertions(
484                                                sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
485                                } else {
486                                        nextSats.emplace_back( std::move( sat ), IterateState );
487                                }
488                        } else if ( sat.deferred.size() > deferLimit ) {
489                                // too many deferred assertions to attempt mutual compatibility
490                                Indenter tabs{ 3 };
491                                std::ostringstream ss;
492                                ss << tabs << "Unsatisfiable alternative:\n";
493                                print( ss, *sat.cand, ++tabs );
494                                ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
495                                for ( const auto & d : sat.deferred ) {
496                                        ast::print( ss, d.expr, tabs );
497                                }
498
499                                errors.emplace_back( ss.str() );
500                                goto nextSat;
501                        } else {
502                                // combine deferred assertions by mutual compatibility
503                                std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
504                                        sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
505
506                                // fail early if no mutually-compatible assertion satisfaction
507                                if ( compatible.empty() ) {
508                                        Indenter tabs{ 3 };
509                                        std::ostringstream ss;
510                                        ss << tabs << "Unsatisfiable alternative:\n";
511                                        print( ss, *sat.cand, ++tabs );
512                                        ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
513                                        for ( const auto& d : sat.deferred ) {
514                                                ast::print( ss, d.expr, tabs );
515                                        }
516
517                                        errors.emplace_back( ss.str() );
518                                        goto nextSat;
519                                }
520
521                                // sort by cost (for overall pruning order)
522                                std::sort( compatible.begin(), compatible.end() );
523
524                                // process mutually-compatible combinations
525                                for ( auto & compat : compatible ) {
526                                        // set up next satisfaction state
527                                        CandidateRef nextCand = std::make_shared<Candidate>(
528                                                sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
529                                                ast::AssertionSet{} /* need moved into satisfaction state */,
530                                                sat.cand->cost, sat.cand->cvtCost );
531
532                                        ast::AssertionSet nextNewNeed{ sat.newNeed };
533                                        InferCache nextInferred{ sat.inferred };
534
535                                        CostVec nextCosts{ sat.costs };
536                                        nextCosts.back() += compat.cost;
537
538                                        ast::SymbolTable nextSymtab{ sat.symtab };
539
540                                        // add compatible assertions to new satisfaction state
541                                        for ( DeferRef r : compat.assns ) {
542                                                AssnCandidate match = r.match;
543                                                addToSymbolTable( match.have, nextSymtab );
544                                                nextNewNeed.insert( match.need.begin(), match.need.end() );
545
546                                                bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
547                                        }
548
549                                        // either add successful match or push back next state
550                                        if ( nextNewNeed.empty() ) {
551                                                finalizeAssertions(
552                                                        nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
553                                        } else {
554                                                nextSats.emplace_back(
555                                                        std::move( nextCand ), std::move( nextNewNeed ),
556                                                        std::move( nextInferred ), std::move( nextCosts ),
557                                                        std::move( nextSymtab ) );
558                                        }
559                                }
560                        }
561                nextSat:; }
562
563                // finish or reset for next round
564                if ( nextSats.empty() ) return;
565                sats.swap( nextSats );
566                nextSats.clear();
567        }
568
569        // exceeded recursion limit if reaches here
570        if ( out.empty() ) {
571                SemanticError( cand->expr->location, "Too many recursive assertions" );
572        }
573}
574
575} // namespace ResolvExpr
576
577// Local Variables: //
578// tab-width: 4 //
579// mode: c++ //
580// compile-command: "make install" //
581// End: //
Note: See TracBrowser for help on using the repository browser.