Changeset 3e5dd913 for src/ResolvExpr/SatisfyAssertions.cpp

Timestamp:

Dec 16, 2020, 2:43:12 PM (4 years ago)

Author:

Fangren Yu <f37yu@…>

Branches:

ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, master, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

53449a4

Parents:

13fece5

Message:

reimplement function type and eliminate deep copy

File:

• src/ResolvExpr/SatisfyAssertions.cpp (modified) (14 diffs)

src/ResolvExpr/SatisfyAssertions.cpp

@@ -69 +69 @@
         /// Reference to a single deferred item
         struct DeferRef {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 const AssnCandidate & match;
@@ -77 +77 @@
         /// Acts like an indexed list of DeferRef
         struct DeferItem {
-                const ast::DeclWithType * decl;
+                const ast::VariableExpr * expr;
                 const ast::AssertionSetValue & info;
                 AssnCandidateList matches;
 
                 DeferItem( 
-                        const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
-                : decl( d ), info( i ), matches( std::move( ms ) ) {}
+                        const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
+                : expr( d ), info( i ), matches( std::move( ms ) ) {}
 
                 bool empty() const { return matches.empty(); }
@@ -89 +89 @@
                 AssnCandidateList::size_type size() const { return matches.size(); }
 
-                DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+                DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
         };
 
@@ -138 +138 @@
         void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
                 for ( auto & i : have ) {
-                        if ( i.second.isUsed ) { symtab.addId( i.first ); }
+                        if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
                 }
         }
@@ -144 +144 @@
         /// Binds a single assertion, updating satisfaction state
         void bindAssertion( 
-                const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 
+                const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 
                 AssnCandidate & match, InferCache & inferred
         ) {
@@ -156 +156 @@
 
                 // place newly-inferred assertion in proper location in cache
-                inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{
-                        candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr };
+                inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
+                        candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
         }
 
@@ -169 +169 @@
 
                 std::vector<ast::SymbolTable::IdData> candidates;
-                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->name);
+                auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
                 if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
                         // prefilter special decls by argument type, if already known
-                        ast::ptr<ast::Type> thisArgType = strict_dynamic_cast<const ast::PointerType *>(assn.first->get_type())->base
+                        ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
                                 .strict_as<ast::FunctionType>()->params[0]
                                 .strict_as<ast::ReferenceType>()->base;
@@ -184 +184 @@
                 }
                 else {
-                        candidates = sat.symtab.lookupId(assn.first->name);
+                        candidates = sat.symtab.lookupId(assn.first->var->name);
                 }
                 for ( const ast::SymbolTable::IdData & cdata : candidates ) {
@@ -200 +200 @@
                         ast::TypeEnvironment newEnv{ sat.cand->env };
                         ast::OpenVarSet newOpen{ sat.cand->open };
-                        ast::ptr< ast::Type > toType = assn.first->get_type();
+                        ast::ptr< ast::Type > toType = assn.first->result;
                         ast::ptr< ast::Type > adjType = 
                                 renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
@@ -337 +337 @@
                                         // compute conversion cost from satisfying decl to assertion
                                         cost += computeConversionCost(
-                                                assn.match.adjType, assn.decl->get_type(), false, symtab, env );
+                                                assn.match.adjType, assn.expr->result, false, symtab, env );
 
                                         // mark vars+specialization on function-type assertions
@@ -350 +350 @@
                                         cost.incVar( func->forall.size() );
 
-                                        for ( const ast::TypeDecl * td : func->forall ) {
-                                                cost.decSpec( td->assertions.size() );
-                                        }
+                                        cost.decSpec( func->assertions.size() );
                                 }
                         }
@@ -451 +449 @@
                                 ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
                                 for ( const auto & d : sat.deferred ) {
-                                        ast::print( ss, d.decl, tabs );
+                                        ast::print( ss, d.expr, tabs );
                                 }
 
@@ -469 +467 @@
                                         ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
                                         for ( const auto& d : sat.deferred ) {
-                                                ast::print( ss, d.decl, tabs );
+                                                ast::print( ss, d.expr, tabs );
                                         }
 
@@ -501 +499 @@
                                                 nextNewNeed.insert( match.need.begin(), match.need.end() );
 
-                                                bindAssertion( r.decl, r.info, nextCand, match, nextInferred );
+                                                bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
                                         }