Skip to content

Commit

Permalink
split analyzer in two separate passes
Browse files Browse the repository at this point in the history
  • Loading branch information
@mwolf76
mwolf76 committed Apr 6, 2013
1 parent e050420 commit 46cf43e
Show file tree
Hide file tree
Showing 2 changed files with 87 additions and 60 deletions.
143 changes: 83 additions & 60 deletions src/model/model_mgr.cc
View file
Expand Up @@ -240,19 +240,12 @@ ModelMgr::ModelMgr()
// // TODO: free memory for symbols... (they've been allocated using new) // // TODO: free memory for symbols... (they've been allocated using new)
// } // }


void ModelMgr::analyze() void ModelMgr::first_pass()
{ {
Model& model(f_model); Model& model(f_model);
const Modules& modules = model.modules();


try { try {
const Modules& modules = model.modules();

DEBUG << "-- first pass (binding)" << endl;
// (binding) For each module m in M, A goes deep in the module
// defs. Every variable decl is resolved either to a native type
// (boolean, ranged int, ...) or to an instance. Due to (1) all
// modules are defined so any unresolved symbol at this point is a
// fatal. Native types are taken care of as well.
for (Modules::const_iterator mod_eye = modules.begin(); for (Modules::const_iterator mod_eye = modules.begin();
mod_eye != modules.end(); mod_eye ++ ) { mod_eye != modules.end(); mod_eye ++ ) {


Expand Down Expand Up @@ -295,76 +288,106 @@ void ModelMgr::analyze()
// f_tm.set_type( FQExpr(ctx, varname), vartype); // f_tm.set_type( FQExpr(ctx, varname), vartype);
} }
} }
} // for modules


// (typechecking) For each module m in M, A inspects FSM exprs: catch (AnalyzerException& ae) {
// INVAR, TRANS, FAIRNESS have all to be boolean formulae; ASSIGNs cerr << ae.what() << endl;
// have to match lvalue type. The type for every expression is }
// inferred using the lazy walker strategy. }
DEBUG << "-- second pass (type checking)" << endl;
for (Modules::const_iterator mod_eye = modules.begin();
mod_eye != modules.end(); mod_eye ++ ) {


Module& module = dynamic_cast <Module&> (*mod_eye->second); void ModelMgr::second_pass()
DEBUG << "processing module '" << module << "' " << endl; {
Model& model(f_model);
const Modules& modules = model.modules();


// Remark: ctx name is MODULE name, not instance's for (Modules::const_iterator mod_eye = modules.begin();
// rationale: you may have several instances but they mod_eye != modules.end(); mod_eye ++ ) {
// all should refer to the same entry on the type map.
Expr_ptr ctx = module.expr();


// const ExprVector params = module.get_formalParams(); Module& module = dynamic_cast <Module&> (*mod_eye->second);
// for (ExprVector::const_iterator param_eye = params.begin(); DEBUG << "processing module '" << module << "' " << endl;
// param_eye != params.end(); param_eye ++) {


// Expr_ptr pname = *param_eye; // Remark: ctx name is MODULE name, not instance's
// tm.reset_type(FQExpr(ctx, pname)); // rationale: you may have several instances but they
// } // all should refer to the same entry on the type map.
Expr_ptr ctx = module.expr();


// TODO: isa decls currently not supported // type inference: defines
const ExprVector isadecls = module.get_isaDecls(); const Defines defines = module.get_localDefs();
assert (isadecls.size() == 0); for (Defines::const_iterator define_eye = defines.begin();
define_eye != defines.end(); define_eye ++) {


// type inference: defines Define& define = dynamic_cast <Define&> (*define_eye->second);
const Defines defines = module.get_localDefs();
for (Defines::const_iterator define_eye = defines.begin();
define_eye != defines.end(); define_eye ++) {


Define& define = dynamic_cast <Define&> (*define_eye->second); Expr_ptr dname = define.expr();
FQExpr fqdn(ctx, dname);


Expr_ptr dname = define.expr(); Expr_ptr dbody = define.body();
FQExpr fqdn(ctx, dname); FQExpr fqdb(ctx, dbody);


Expr_ptr dbody = define.body(); // try to infer type
FQExpr fqdb(ctx, dbody); try {
Type_ptr tmp = type(fqdb);
}
catch (AnalyzerException& ae) {
cerr << "DEFINE " << fqdn << endl
<< ae.what() << endl;
}
} // for defines


Type_ptr tp = type(fqdb); // type inference: FSM
} // for defines const ExprVector init = module.init();
for (ExprVector::const_iterator init_eye = init.begin();
init_eye != init.end(); init_eye ++) {


// type inference: FSM Expr_ptr body = (*init_eye);
const ExprVector init = module.init(); FQExpr fqdn(ctx, body);
for (ExprVector::const_iterator init_eye = init.begin();
init_eye != init.end(); init_eye ++) {


Expr_ptr body = (*init_eye); DEBUG << "processing INIT " << fqdn << endl;
DEBUG << "processing INIT " << ctx << "::" << body << endl;


try {
f_inferrer.process(ctx, body, TP_BOOLEAN); f_inferrer.process(ctx, body, TP_BOOLEAN);
} // for init }
catch (AnalyzerException& ae) {
cerr << "INIT " << fqdn << endl
<< ae.what() << endl;
}

} // for init


const ExprVector trans = module.trans(); const ExprVector trans = module.trans();
for (ExprVector::const_iterator trans_eye = trans.begin(); for (ExprVector::const_iterator trans_eye = trans.begin();
trans_eye != trans.end(); trans_eye ++) { trans_eye != trans.end(); trans_eye ++) {


Expr_ptr body = (*trans_eye); Expr_ptr body = (*trans_eye);
DEBUG << "processing TRANS " << ctx << "::" << body << endl; FQExpr fqdn(ctx, body);
DEBUG << "processing TRANS " << fqdn << endl;


try {
f_inferrer.process(ctx, body, TP_BOOLEAN); f_inferrer.process(ctx, body, TP_BOOLEAN);
} }
} // for trans catch (AnalyzerException& ae) {

cerr << "TRANS " << fqdn << endl
} // for modules << ae.what() << endl;

}
catch (AnalyzerException& ae) { }
cerr << ae.what() << endl;
} }
} }

void ModelMgr::analyze()
{
DEBUG << "-- first pass (binding)" << endl;
// (binding) For each module m in M, A goes deep in the module
// defs. Every variable decl is resolved either to a native type
// (boolean, ranged int, ...) or to an instance. Due to (1) all
// modules are defined so any unresolved symbol at this point is a
// fatal. Native types are taken care of as well.
first_pass();

DEBUG << "-- second pass (type checking)" << endl;
// (typechecking) For each module m in M, A inspects FSM exprs:
// INVAR, TRANS, FAIRNESS have all to be boolean formulae; ASSIGNs
// have to match lvalue type. The type for every expression is
// inferred using the lazy walker strategy.
second_pass();
}

4 changes: 4 additions & 0 deletions src/model/model_mgr.hh
View file
Expand Up @@ -84,6 +84,10 @@ private:


// ref to inferrer (used for model analysis) // ref to inferrer (used for model analysis)
Inferrer& f_inferrer; Inferrer& f_inferrer;

// analyzer passes
void first_pass();
void second_pass();
}; };


#endif #endif

0 comments on commit 46cf43e

Please sign in to comment.