| [a32b204] | 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 | // | 
|---|
| [8c49c0e] | 7 | // FindOpenVars.cc -- | 
|---|
| [a32b204] | 8 | // | 
|---|
|  | 9 | // Author           : Richard C. Bilson | 
|---|
|  | 10 | // Created On       : Sun May 17 09:42:48 2015 | 
|---|
|  | 11 | // Last Modified By : Peter A. Buhr | 
|---|
|  | 12 | // Last Modified On : Sun May 17 09:45:25 2015 | 
|---|
|  | 13 | // Update Count     : 3 | 
|---|
|  | 14 | // | 
|---|
| [51b73452] | 15 |  | 
|---|
|  | 16 | #include "FindOpenVars.h" | 
|---|
| [ea6332d] | 17 |  | 
|---|
|  | 18 | #include <list>                   // for _List_const_iterator, list<>::const... | 
|---|
|  | 19 | #include <map>                    // for map<>::mapped_type | 
|---|
|  | 20 |  | 
|---|
| [9519aba] | 21 | #include "AST/Pass.hpp" | 
|---|
|  | 22 | #include "AST/Type.hpp" | 
|---|
| [ce7ed2c] | 23 | #include "Common/PassVisitor.h" | 
|---|
| [ea6332d] | 24 | #include "SynTree/Declaration.h"  // for TypeDecl, DeclarationWithType (ptr ... | 
|---|
|  | 25 | #include "SynTree/Type.h"         // for Type, Type::ForallList, ArrayType | 
|---|
| [51b73452] | 26 |  | 
|---|
|  | 27 | namespace ResolvExpr { | 
|---|
| [9519aba] | 28 | struct FindOpenVars_old : public WithGuards { | 
|---|
|  | 29 | FindOpenVars_old( OpenVarSet &openVars, OpenVarSet &closedVars, AssertionSet &needAssertions, AssertionSet &haveAssertions, bool firstIsOpen ); | 
|---|
| [a32b204] | 30 |  | 
|---|
| [ce7ed2c] | 31 | void previsit( PointerType * pointerType ); | 
|---|
|  | 32 | void previsit( ArrayType * arrayType ); | 
|---|
|  | 33 | void previsit( FunctionType * functionType ); | 
|---|
|  | 34 | void previsit( TupleType * tupleType ); | 
|---|
| [a32b204] | 35 |  | 
|---|
|  | 36 | void common_action( Type *type ); | 
|---|
| [51b73452] | 37 |  | 
|---|
| [a32b204] | 38 | OpenVarSet &openVars, &closedVars; | 
|---|
|  | 39 | AssertionSet &needAssertions, &haveAssertions; | 
|---|
|  | 40 | bool nextIsOpen; | 
|---|
|  | 41 | }; | 
|---|
| [51b73452] | 42 |  | 
|---|
| [a32b204] | 43 | void findOpenVars( Type *type, OpenVarSet &openVars, OpenVarSet &closedVars, AssertionSet &needAssertions, AssertionSet &haveAssertions, bool firstIsOpen ) { | 
|---|
| [9519aba] | 44 | PassVisitor<FindOpenVars_old> finder( openVars, closedVars, needAssertions, haveAssertions, firstIsOpen ); | 
|---|
| [a32b204] | 45 | type->accept( finder ); | 
|---|
|  | 46 | } | 
|---|
| [51b73452] | 47 |  | 
|---|
| [9519aba] | 48 | FindOpenVars_old::FindOpenVars_old( OpenVarSet &openVars, OpenVarSet &closedVars, AssertionSet &needAssertions, AssertionSet &haveAssertions, bool firstIsOpen ) | 
|---|
| [a32b204] | 49 | : openVars( openVars ), closedVars( closedVars ), needAssertions( needAssertions ), haveAssertions( haveAssertions ), nextIsOpen( firstIsOpen ) { | 
|---|
|  | 50 | } | 
|---|
| [51b73452] | 51 |  | 
|---|
| [9519aba] | 52 | void FindOpenVars_old::common_action( Type *type ) { | 
|---|
| [a32b204] | 53 | if ( nextIsOpen ) { | 
|---|
| [8c49c0e] | 54 | for ( Type::ForallList::const_iterator i = type->get_forall().begin(); i != type->get_forall().end(); ++i ) { | 
|---|
| [2c57025] | 55 | openVars[ (*i)->get_name() ] = TypeDecl::Data{ (*i) }; | 
|---|
| [a32b204] | 56 | for ( std::list< DeclarationWithType* >::const_iterator assert = (*i)->get_assertions().begin(); assert != (*i)->get_assertions().end(); ++assert ) { | 
|---|
| [6c3a988f] | 57 | needAssertions[ *assert ].isUsed = false; | 
|---|
| [a32b204] | 58 | } | 
|---|
| [51b73452] | 59 | ///       cloneAll( (*i)->get_assertions(), needAssertions ); | 
|---|
|  | 60 | ///       needAssertions.insert( needAssertions.end(), (*i)->get_assertions().begin(), (*i)->get_assertions().end() ); | 
|---|
| [a32b204] | 61 | } | 
|---|
|  | 62 | } else { | 
|---|
| [8c49c0e] | 63 | for ( Type::ForallList::const_iterator i = type->get_forall().begin(); i != type->get_forall().end(); ++i ) { | 
|---|
| [2c57025] | 64 | closedVars[ (*i)->get_name() ] = TypeDecl::Data{ (*i) }; | 
|---|
| [a32b204] | 65 | for ( std::list< DeclarationWithType* >::const_iterator assert = (*i)->get_assertions().begin(); assert != (*i)->get_assertions().end(); ++assert ) { | 
|---|
| [6c3a988f] | 66 | haveAssertions[ *assert ].isUsed = false; | 
|---|
| [a32b204] | 67 | } | 
|---|
| [51b73452] | 68 | ///       cloneAll( (*i)->get_assertions(), haveAssertions ); | 
|---|
|  | 69 | ///       haveAssertions.insert( haveAssertions.end(), (*i)->get_assertions().begin(), (*i)->get_assertions().end() ); | 
|---|
| [a32b204] | 70 | } // for | 
|---|
|  | 71 | } // if | 
|---|
| [ce7ed2c] | 72 | ///   std::cerr << "type is "; | 
|---|
|  | 73 | ///   type->print( std::cerr ); | 
|---|
|  | 74 | ///   std::cerr << std::endl << "need is" << std::endl; | 
|---|
|  | 75 | ///   printAssertionSet( needAssertions, std::cerr ); | 
|---|
|  | 76 | ///   std::cerr << std::endl << "have is" << std::endl; | 
|---|
|  | 77 | ///   printAssertionSet( haveAssertions, std::cerr ); | 
|---|
| [a32b204] | 78 | } | 
|---|
| [51b73452] | 79 |  | 
|---|
| [9519aba] | 80 | void FindOpenVars_old::previsit(PointerType *pointerType) { | 
|---|
| [a32b204] | 81 | common_action( pointerType ); | 
|---|
|  | 82 | } | 
|---|
| [51b73452] | 83 |  | 
|---|
| [9519aba] | 84 | void FindOpenVars_old::previsit(ArrayType *arrayType) { | 
|---|
| [a32b204] | 85 | common_action( arrayType ); | 
|---|
|  | 86 | } | 
|---|
| [51b73452] | 87 |  | 
|---|
| [9519aba] | 88 | void FindOpenVars_old::previsit(FunctionType *functionType) { | 
|---|
| [a32b204] | 89 | common_action( functionType ); | 
|---|
|  | 90 | nextIsOpen = ! nextIsOpen; | 
|---|
| [ce7ed2c] | 91 | GuardAction( [this](){ nextIsOpen = ! nextIsOpen; } ); | 
|---|
| [a32b204] | 92 | } | 
|---|
| [51b73452] | 93 |  | 
|---|
| [9519aba] | 94 | void FindOpenVars_old::previsit(TupleType *tupleType) { | 
|---|
| [a32b204] | 95 | common_action( tupleType ); | 
|---|
|  | 96 | } | 
|---|
| [f474e91] | 97 |  | 
|---|
| [9519aba] | 98 | namespace { | 
|---|
|  | 99 | struct FindOpenVars_new final : public ast::WithGuards { | 
|---|
|  | 100 | ast::OpenVarSet & open; | 
|---|
|  | 101 | ast::OpenVarSet & closed; | 
|---|
|  | 102 | ast::AssertionSet & need; | 
|---|
|  | 103 | ast::AssertionSet & have; | 
|---|
|  | 104 | bool nextIsOpen; | 
|---|
|  | 105 |  | 
|---|
|  | 106 | FindOpenVars_new( | 
|---|
|  | 107 | ast::OpenVarSet & o, ast::OpenVarSet & c, ast::AssertionSet & n, | 
|---|
|  | 108 | ast::AssertionSet & h, FirstMode firstIsOpen ) | 
|---|
|  | 109 | : open( o ), closed( c ), need( n ), have( h ), nextIsOpen( firstIsOpen ) {} | 
|---|
|  | 110 |  | 
|---|
|  | 111 | void previsit( const ast::FunctionType * type ) { | 
|---|
|  | 112 | // mark open/closed variables | 
|---|
|  | 113 | if ( nextIsOpen ) { | 
|---|
|  | 114 | for ( const ast::TypeDecl * decl : type->forall ) { | 
|---|
|  | 115 | open[ decl->name ] = ast::TypeDecl::Data{ decl }; | 
|---|
|  | 116 | for ( const ast::DeclWithType * assert : decl->assertions ) { | 
|---|
|  | 117 | need[ assert ].isUsed = false; | 
|---|
|  | 118 | } | 
|---|
|  | 119 | } | 
|---|
|  | 120 | } else { | 
|---|
|  | 121 | for ( const ast::TypeDecl * decl : type->forall ) { | 
|---|
|  | 122 | closed[ decl->name ] = ast::TypeDecl::Data{ decl }; | 
|---|
|  | 123 | for ( const ast::DeclWithType * assert : decl->assertions ) { | 
|---|
|  | 124 | have[ assert ].isUsed = false; | 
|---|
|  | 125 | } | 
|---|
|  | 126 | } | 
|---|
|  | 127 | } | 
|---|
|  | 128 |  | 
|---|
|  | 129 | // flip open variables for contained function types | 
|---|
|  | 130 | nextIsOpen = ! nextIsOpen; | 
|---|
|  | 131 | GuardAction( [this](){ nextIsOpen = ! nextIsOpen; } ); | 
|---|
|  | 132 | } | 
|---|
|  | 133 |  | 
|---|
|  | 134 | }; | 
|---|
|  | 135 | } | 
|---|
|  | 136 |  | 
|---|
| [f474e91] | 137 | void findOpenVars( | 
|---|
|  | 138 | const ast::Type * type, ast::OpenVarSet & open, ast::OpenVarSet & closed, | 
|---|
|  | 139 | ast::AssertionSet & need, ast::AssertionSet & have, FirstMode firstIsOpen ) { | 
|---|
| [9519aba] | 140 | ast::Pass< FindOpenVars_new > finder{ open, closed, need, have, firstIsOpen }; | 
|---|
|  | 141 | type->accept( finder ); | 
|---|
| [f474e91] | 142 | } | 
|---|
| [51b73452] | 143 | } // namespace ResolvExpr | 
|---|
| [a32b204] | 144 |  | 
|---|
|  | 145 | // Local Variables: // | 
|---|
|  | 146 | // tab-width: 4 // | 
|---|
|  | 147 | // mode: c++ // | 
|---|
|  | 148 | // compile-command: "make install" // | 
|---|
|  | 149 | // End: // | 
|---|