From 3d645cc84b733042833d6617e5ccfac214e62a75 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Mar 2014 09:03:18 -0500 Subject: [PATCH] Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan (problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof. --- proofs/lfsc_checker/check.cpp | 124 ++++++++++++++------------- proofs/lfsc_checker/code.cpp | 154 ++++++++++++++++++---------------- proofs/lfsc_checker/expr.cpp | 7 +- proofs/signatures/ex-mem.plf | 68 +++++++++++++++ 4 files changed, 217 insertions(+), 136 deletions(-) create mode 100755 proofs/signatures/ex-mem.plf diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index 8ef114115..b550c58a1 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -101,7 +101,7 @@ void eat_rparen() { } void eat_excess(int prev) { - while(open_parens > prev) + while(open_parens > prev) eat_rparen(); } @@ -110,8 +110,8 @@ void eat_excess(int prev) { 1. expected=0, create is false: check() sets computed to be the classifier of the checked term. -2. expected=0, create is true: check() returns - the checked expression and sets computed to be its classifier. +2. expected=0, create is true: check() returns + the checked expression and sets computed to be its classifier. 3. expected is non-null, create is false: check returns NULL. @@ -119,14 +119,14 @@ void eat_excess(int prev) { was checked. We consume the reference for expected, to enable tail calls in the -application case. +application case. If is_hole is NULL, then the expression parsed may not be a hole. Otherwise, it may be, and we will set *is_hole to true if it is (but leave *is_hole alone if it is not). */ - + bool allow_run = false; int app_rec_level = 0; @@ -143,7 +143,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, open_parens++; - char c = non_ws(); + char c = non_ws(); switch (c) { case EOF: report_error("Unexpected end of file."); @@ -190,7 +190,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, +string("is neither \"type\" nor \"kind\".\n") +string("1. the expected classifier: ") +expected->toString()); - if (create){ + if (create){ CExpr* ret = new CExpr(PI, sym, domain, range); ret->calc_free_in(); return ret; @@ -198,7 +198,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, return 0; } else { - if (create){ + if (create){ CExpr* ret = new CExpr(PI, sym, domain, range); ret->calc_free_in(); return ret; @@ -235,7 +235,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, symbols[id] = sym; symbol_types[id] = expected_domain; #else - pair prevpr = + pair prevpr = symbols->insert(id.c_str(), pair(sym,expected_domain)); Expr *prev = prevpr.first; Expr *prevtp = prevpr.second; @@ -244,7 +244,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, //will clean up local sym name eventually local_sym_names.push_back( std::pair< std::string, std::pair >( id, prevpr ) ); - if (prev) + if (prev) prev->dec(); if (prevtp) prevtp->dec(); @@ -288,21 +288,21 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, +string(" a kind, not a type.\n") +string("1. The expected classifier: ") +expected->toString()); - + /* we need to map the pivar to the new sym, because in our higher-order matching we may have (_ x) to unify with t. The x must be something from an expected type, since only these can have holes. We want to map expected vars x to computed vars y, so that we can set the hole to be \ y t, where t contains ys but not xs. */ - + #ifdef USE_HASH_MAPS Expr *prev = symbols[id]; Expr *prevtp = symbol_types[id]; symbols[id] = sym; symbol_types[id] = expected_domain; #else - pair prevpr = + pair prevpr = symbols->insert(id.c_str(), pair(sym,expected_domain)); Expr *prev = prevpr.first; Expr *prevtp = prevpr.second; @@ -319,7 +319,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, local_sym_names.push_back( std::pair< std::string, std::pair >( id, prevpr ) ); if (prev_pivar_val) prev_pivar_val->dec(); - if (prev) + if (prev) prev->dec(); if (prevtp) prevtp->dec(); @@ -351,7 +351,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, orig_expected->dec(); sym->dec(); // the pivar->val reference - if (create) + if (create) return new CExpr(LAM, sym, range); sym->dec(); // the symbol table reference, otherwise in the new LAM return 0; @@ -364,24 +364,24 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, Expr *code = read_code(); //string errstr = (string("The first argument in a run expression must be") - // +string(" a call to a program.\n1. the argument: ") + // +string(" a call to a program.\n1. the argument: ") // +code->toString()); /* determine expected type of the result term, and make sure the code term is an allowed one. */ #if 0 Expr *progret; - if (code->isArithTerm()) + if (code->isArithTerm()) progret = statMpz; else { if (code->getop() != APP) report_error(errstr); CExpr *call = (CExpr *)code; - + // prog is not known to be a SymExpr yet CExpr *prog = (CExpr *)call->get_head(); - + if (prog->getop() != PROG) report_error(errstr); @@ -389,16 +389,16 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, } #else Expr *progret = NULL; - if (code->isArithTerm()) + if (code->isArithTerm()) progret = statMpz; else { if (code->getop() == APP) { CExpr *call = (CExpr *)code; - + // prog is not known to be a SymExpr yet CExpr *prog = (CExpr *)call->get_head(); - + if (prog->getop() == PROG) progret = prog->kids[0]->get_body(); } @@ -433,7 +433,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, if (!expected) tp->inc(); - + Expr *trm = check(create, tp, NULL, NULL, return_pos); eat_excess(prev); eat_rparen(); @@ -478,14 +478,14 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, symbols[id] = sym; symbol_types[id] = tp_of_trm; #else - pair prevpr = + pair prevpr = symbols->insert(id.c_str(), pair(sym,tp_of_trm)); Expr *prev = prevpr.first; Expr *prevtp = prevpr.second; #endif if (tail_calls && big_check && return_pos && !create) { - if (prev) + if (prev) prev->dec(); if (prevtp) prevtp->dec(); @@ -506,7 +506,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, #endif tp_of_trm->dec(); // because removed from the symbol table now - sym->dec(); + sym->dec(); return body; } } @@ -545,7 +545,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, report_error("Negative sign with expr that is not an int. literal."); } } - else + else return 0; } default: { // the application case @@ -562,7 +562,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, // we must clone Expr *orig_headtp = headtp; headtp = (CExpr *)headtp->clone(); - orig_headtp->dec(); + orig_headtp->dec(); } else headtp->setcloned(); @@ -578,11 +578,11 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, while ((c = non_ws()) != ')') { our_ungetc(c); if (headtp->getop() != PI) - report_error(string("The type of an applied term is not ") + report_error(string("The type of an applied term is not ") + string("a pi-type.\n") + string("\n1. the type of the term: ") + headtp->toString() - + (headtrm ? (string("\n2. the term: ") + + (headtrm ? (string("\n2. the term: ") + headtrm->toString()) : string(""))); SymExpr *headtp_var = (SymExpr *)headtp->kids[0]; @@ -627,7 +627,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, + expected->toString() + string("\n2. The computed type: ") + headtp_range->toString() - + (headtrm ? (string("\n3. the application: ") + + (headtrm ? (string("\n3. the application: ") + headtrm->toString()) : string(""))); expected->dec(); @@ -670,7 +670,11 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, #ifndef USE_FLAT_APP headtrm = new CExpr(APP, headtrm, arg); #else + Expr* orig_headtrm = headtrm; headtrm = Expr::make_app( headtrm, arg ); + if( orig_headtrm->getclass()==CEXPR ){ + orig_headtrm->dec(); + } #endif consumed_arg = true; } @@ -739,7 +743,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, + expected->toString() + string("\n2. The computed type: ") + headtp->toString() - + (headtrm ? (string("\n3. the application: ") + + (headtrm ? (string("\n3. the application: ") + headtrm->toString()) : string(""))); @@ -755,7 +759,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, ret = headtrm; } - /* do this check here to give the defeq() call above a + /* do this check here to give the defeq() call above a chance to fill in some holes */ for (int i = 0, iend = holes.size(); i < iend; i++) { if (!holes[i]->val){ @@ -783,7 +787,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, report_error("Unexpected end of file."); break; - case '_': + case '_': if (!is_hole) report_error("A hole is being used in a disallowed position."); *is_hole = true; @@ -803,7 +807,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, our_ungetc(d); string v; char c; - while (isdigit(c = our_getc())) + while (isdigit(c = our_getc())) v.push_back(c); bool parseMpq = false; string v2; @@ -811,7 +815,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, { parseMpq = true; v.push_back( c ); - while(isdigit(c = our_getc())) + while(isdigit(c = our_getc())) v.push_back(c); } our_ungetc(c); @@ -916,7 +920,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, #ifdef USE_HASH_MAPS void discard_old_symbol(const string &id) { Expr *tmp = symbols[id]; - if (tmp) + if (tmp) tmp->dec(); tmp = symbol_types[id]; if (tmp) @@ -940,7 +944,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { char *f; if (strcmp(_filename,"stdin") == 0) { - curfile = stdin; + curfile = stdin; f = strdup(_filename); } else { @@ -967,7 +971,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { else f = strdup(_filename); curfile = fopen(f,"r"); - if (!curfile) + if (!curfile) report_error(string("Could not open file \"") + string(f) + string("\" for reading.\n")); @@ -985,15 +989,15 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { switch ((d = non_ws())) { case 'd': char b; - if ((b = our_getc()) != 'e') + if ((b = our_getc()) != 'e') report_error(string("Unexpected start of command.")); switch ((b = our_getc())) { case 'f': {// expecting "define" - + if (our_getc() != 'i' || our_getc() != 'n' || our_getc() != 'e') report_error(string("Unexpected start of command.")); - + string id(prefix_id()); Expr *ttp; int prevo = open_parens; @@ -1010,7 +1014,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { symbols[id] = s; symbol_types[id] = ttp; #else - pair prev = + pair prev = symbols->insert(id.c_str(), pair(s,ttp)); if (prev.first) prev.first->dec(); @@ -1020,7 +1024,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { break; } case 'c': {// expecting "declare" - if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' + if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' || our_getc() != 'e') report_error(string("Unexpected start of command.")); @@ -1045,7 +1049,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { symbols[id] = s; symbol_types[id] = t; #else - pair prev = + pair prev = symbols->insert(id.c_str(), pair(s,t)); if( lw ) lw->add_symbol( s, t ); @@ -1056,7 +1060,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { #endif break; } - default: + default: report_error(string("Unexpected start of command.")); } // switch((b = our_getc())) following "de" break; @@ -1105,7 +1109,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { if (our_getc() != 'p' || our_getc() != 'a' || our_getc() != 'q' || our_getc() != 'u' || our_getc() != 'e') report_error(string("Unexpected start of command.")); - + string id(prefix_id()); Expr *ttp; int prevo = open_parens; @@ -1121,7 +1125,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { symbols[id] = s; symbol_types[id] = ttp; #else - pair prev = + pair prev = symbols->insert(id.c_str(), pair(s,ttp)); if (prev.first) prev.first->dec(); @@ -1150,7 +1154,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { break; } case 'p': { // program case - if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g' + if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g' || our_getc() != 'r' || our_getc() != 'a' || our_getc() != 'm') report_error(string("Unexpected start of command.")); @@ -1209,10 +1213,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { symbols->insert(varstr.c_str(), pair(var,tp)); #endif } - + if (!vars.size()) report_error("A program lacks input variables."); - + statType->inc(); int prev = open_parens; Expr *progtp = check(true,statType,&tmp,0, true); @@ -1221,7 +1225,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { if (!progtp->isDatatype()) report_error(string("Return type for a program is not a") +string(" datatype.\n1. the type: ")+progtp->toString()); - + Expr *progcode = read_code(); for (int i = vars.size() - 1, iend = 0; i >= iend; i--) { @@ -1231,10 +1235,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { } // just put the type here for type checking. Make sure progtp is kid 0. - prog->val = new CExpr(PROG, progtp); - + prog->val = new CExpr(PROG, progtp); + check_code(progcode); - + progcode = new CExpr(PROG, progtp, new CExpr(PROGVARS, vars), progcode); //if compiling side condition code, give this code to the side condition code writer if( a.compile_scc ){ @@ -1242,7 +1246,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { scw->add_scc( progstr, (CExpr*)progcode ); } } - + // remove the variables from the symbol table. for (int i = 0, iend = vars.size(); i < iend; i++) { string &s = ((SymSExpr *)vars[i])->s; @@ -1263,10 +1267,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { break; } - default: + default: report_error(string("Unexpected start of command.")); } // switch((d = non_ws()) - + eat_char(')'); } // while else @@ -1350,7 +1354,7 @@ void cleanup() { delete symbols; #endif - // clean up programs + // clean up programs symmap2::iterator j, jend; for (j = progs.begin(), jend = progs.end(); j != jend; j++) { @@ -1378,6 +1382,6 @@ void init() { symbols->insert("type", pair(statType, statKind)); statType->inc(); symbols->insert("mpz", pair(statMpz, statType)); - symbols->insert("mpq", pair(statMpq, statType)); + symbols->insert("mpq", pair(statMpq, statType)); #endif } diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp index 225700580..34c6c133b 100644 --- a/proofs/lfsc_checker/code.cpp +++ b/proofs/lfsc_checker/code.cpp @@ -23,7 +23,7 @@ string *eat_str(const char *str, bool check_end = true) { our_ungetc(d); return s; } - + delete s; return 0; } @@ -76,13 +76,17 @@ Expr *read_case() { prevs.push_back(symbols[varstr]); symbols[varstr] = var; #else - prevs.push_back(symbols->insert(varstr.c_str(), + prevs.push_back(symbols->insert(varstr.c_str(), pair(var,NULL))); #endif #ifndef USE_FLAT_APP pat = new CExpr(APP,pat,var); #else + Expr* orig_pat = pat; pat = Expr::make_app(pat,var); + if( orig_pat->getclass()==CEXPR ){ + orig_pat->dec(); + } #endif } break; @@ -101,7 +105,7 @@ Expr *read_case() { pat = read_ctor(); break; } - + Expr *ret = read_code(); if( pat ) ret = new CExpr(CASE, pat, ret); @@ -124,16 +128,16 @@ Expr *read_code() { string *pref = NULL; char d = non_ws(); switch(d) { - case '(': + case '(': { - char c = non_ws(); - switch (c) + char c = non_ws(); + switch (c) { - case 'd': + case 'd': { our_ungetc('d'); pref = eat_str("do"); - if (pref) + if (pref) break; Expr *ret = read_code(); while ((c = non_ws()) != ')') { @@ -142,11 +146,11 @@ Expr *read_code() { } return ret; } - case 'f': + case 'f': { our_ungetc('f'); pref = eat_str("fail"); - if (pref) + if (pref) break; Expr *c = read_code(); @@ -156,14 +160,14 @@ Expr *read_code() { //if (c->getclass() != SYMS_EXPR || ((SymExpr *)c)->val) // report_error(string("\"fail\" must be used with a (undefined) base ") // +string("type.\n1. the expression used: "+c->toString())); - + return new CExpr(FAIL, c); } - case 'l': + case 'l': { our_ungetc('l'); pref = eat_str("let"); - if (pref) + if (pref) break; string id(prefix_id()); @@ -175,12 +179,12 @@ Expr *read_code() { Expr *prev = symbols[id]; symbols[id] = var; #else - pair prev = + pair prev = symbols->insert(id.c_str(), pair(var,NULL)); #endif Expr *t2 = read_code(); - + #ifdef USE_HASH_MAPS symbols[id] = prev; #else @@ -189,11 +193,11 @@ Expr *read_code() { eat_char(')'); return new CExpr(LET, var, t1, t2); } - case 'i': + case 'i': { our_ungetc('i'); pref = eat_str("ifmarked",false); - if (pref) + if (pref) break; #ifndef MARKVAR_32 Expr *e1 = read_code(); @@ -220,16 +224,16 @@ Expr *read_code() { eat_char(')'); return ret; } - case 'm': + case 'm': { char c; - switch ((c = our_getc())) + switch ((c = our_getc())) { - case 'a': + case 'a': { char cc; switch ((cc = our_getc())) { - case 't': + case 't': { our_ungetc('t'); pref = eat_str("tch"); @@ -253,7 +257,7 @@ Expr *read_code() { } return new CExpr(MATCH,cases); } - case 'r': + case 'r': { our_ungetc('r'); pref = eat_str("rkvar", false); @@ -268,7 +272,7 @@ Expr *read_code() { CExpr* ret = NULL; if( index>=1 && index<=32 ) { - ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() ); + ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() ); } else { @@ -287,7 +291,7 @@ Expr *read_code() { break; } } - case 'p': + case 'p': { our_ungetc('p'); pref = eat_str("p_",false); @@ -297,7 +301,7 @@ Expr *read_code() { } char c = our_getc(); switch(c) { - case 'a': + case 'a': { our_ungetc('a'); pref = eat_str("add"); @@ -311,7 +315,7 @@ Expr *read_code() { eat_char(')'); return ret; } - case 'n': + case 'n': { our_ungetc('n'); pref = eat_str("neg"); @@ -319,12 +323,12 @@ Expr *read_code() { pref->insert(0,"mp_"); break; } - + Expr *ret = new CExpr(NEG, read_code()); eat_char(')'); return ret; } - case 'i': + case 'i': { // mpz_if_neg char c = our_getc(); if( c=='f' ) @@ -439,7 +443,7 @@ Expr *read_code() { { our_ungetc('c'); pref = eat_str("compare"); - if (pref) + if (pref) break; Expr *e1 = read_code(); Expr *e2 = read_code(); @@ -452,21 +456,21 @@ Expr *read_code() { case EOF: report_error("Unexpected end of file."); break; - default: + default: { // the application case our_ungetc(c); break; } } // parse application - if (pref) + if (pref) // we have eaten part of the name of an applied identifier pref->append(prefix_id()); else pref = new string(prefix_id()); Expr *ret = progs[*pref]; - if (!ret) + if (!ret) #ifdef USE_HASH_TABLES ret = symbols[*pref]; #else @@ -486,7 +490,11 @@ Expr *read_code() { ret = new CExpr(APP,ret,read_code()); #else Expr* ke = read_code(); + Expr* orig_ret = ret; ret = Expr::make_app(ret,ke); + if( orig_ret->getclass()==CEXPR ){ + orig_ret->dec(); + } #endif } return ret; @@ -494,7 +502,7 @@ Expr *read_code() { case EOF: report_error("Unexpected end of file."); break; - case '_': + case '_': report_error("Holes may not be used in code."); return NULL; case '0': @@ -506,19 +514,19 @@ Expr *read_code() { case '6': case '7': case '8': - case '9': + case '9': { our_ungetc(d); string v; char c; - while (isdigit(c = our_getc())) + while (isdigit(c = our_getc())) v.push_back(c); bool parseMpq = false; if( c=='/' ) { parseMpq = true; v.push_back(c); - while(isdigit(c = our_getc())) + while(isdigit(c = our_getc())) v.push_back(c); } our_ungetc(c); @@ -540,7 +548,7 @@ Expr *read_code() { return new IntExpr(num); } } - default: + default: { our_ungetc(d); string id(prefix_id()); @@ -550,7 +558,7 @@ Expr *read_code() { pair p = symbols->get(id.c_str()); Expr *ret = p.first; #endif - if (!ret) + if (!ret) ret = progs[id]; if (!ret) report_error(string("Undeclared identifier: ")+id); @@ -609,7 +617,7 @@ Expr *check_code(Expr *_e) { int iend = args.size(); vector argtps(iend); - for (int i = 0; i < iend; i++) + for (int i = 0; i < iend; i++) argtps[i] = check_code(args[i]); #endif @@ -623,18 +631,18 @@ Expr *check_code(Expr *_e) { tp = symbols->get(((SymSExpr *)h)->s.c_str()).second; #endif } - + if (!tp) report_error(string("The head of an application is missing a type in ") +string("code.\n1. the application: ")+e->toString()); - + tp = tp->followDefs(); if (tp->getop() != PI) report_error(string("The head of an application does not have ") +string("functional type in code.") +string("\n1. the application: ")+e->toString()); - + CExpr *cur = (CExpr *)tp; int i = 0; while (cur->getop() == PI) { @@ -661,7 +669,7 @@ Expr *check_code(Expr *_e) { + string("\n5. expected type: ") +cur->kids[1]->toString()); } - + //if (cur->kids[2]->free_in((SymExpr *)cur->kids[0])) if( cur->get_free_in() ){ cur->calc_free_in(); @@ -682,8 +690,8 @@ Expr *check_code(Expr *_e) { +string("arguments in code.\n") +string("1. the application: ")+e->toString() +string("\n2. the head's type: ")+tp->toString()); - - + + return cur; } //is this right? @@ -693,7 +701,7 @@ Expr *check_code(Expr *_e) { case MPQ: return statType; break; - case DO: + case DO: check_code(e->kids[0]); return check_code(e->kids[1]); @@ -706,22 +714,22 @@ Expr *check_code(Expr *_e) { Expr *prevtp = symbol_types[var->s]; symbol_types[var->s] = tp1; #else - pair prev = + pair prev = symbols->insert(var->s.c_str(), pair(NULL,tp1)); #endif Expr *tp2 = check_code(e->kids[2]); - + #ifdef USE_HASH_MAPS symbol_types[var->s] = prevtp; #else symbols->insert(var->s.c_str(), prev); #endif - + return tp2; } - case ADD: + case ADD: case MUL: case DIV: { @@ -732,14 +740,14 @@ Expr *check_code(Expr *_e) { report_error(string("Argument to mp_[arith] does not have type \"mpz\" or \"mpq\".\n") +string("1. the argument: ")+e->kids[0]->toString() +string("\n1. its type: ")+tp0->toString()); - + if (tp0 != tp1) report_error(string("Arguments to mp_[arith] have differing types.\n") +string("1. argument 1: ")+e->kids[0]->toString() +string("\n1. its type: ")+tp0->toString() +string("2. argument 2: ")+e->kids[1]->toString() +string("\n2. its type: ")+tp1->toString()); - + return tp0; } @@ -749,18 +757,18 @@ Expr *check_code(Expr *_e) { report_error(string("Argument to mp_neg does not have type \"mpz\" or \"mpq\".\n") +string("1. the argument: ")+e->kids[0]->toString() +string("\n1. its type: ")+tp0->toString()); - + return tp0; } - case IFNEG: + case IFNEG: case IFZERO: { Expr *tp0 = check_code(e->kids[0]); if (tp0 != statMpz && tp0 != statMpq) report_error(string("Argument to mp_if does not have type \"mpz\" or \"mpq\".\n") +string("1. the argument: ")+e->kids[0]->toString() +string("\n1. its type: ")+tp0->toString()); - + SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]); SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]); if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2) @@ -785,7 +793,7 @@ Expr *check_code(Expr *_e) { } case MARKVAR: { SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]); - + Expr* tptp = NULL; if (tp->getclass() == SYMS_EXPR && !tp->val){ @@ -808,12 +816,12 @@ Expr *check_code(Expr *_e) { return tp; } - case IFMARKED: + case IFMARKED: { SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]); Expr* tptp = NULL; - + if (tp->getclass() == SYMS_EXPR && !tp->val){ #ifdef USE_HASH_MAPS tptp = symbol_types[tp->s]; @@ -821,7 +829,7 @@ Expr *check_code(Expr *_e) { tptp = symbols->get(tp->s.c_str()).second; #endif } - + if (!tptp->isType( statType ) ){ string errstr = (string("\"ifmarked\" is used with an expression which ") +string("cannot be a lambda-bound variable.\n") @@ -877,7 +885,7 @@ Expr *check_code(Expr *_e) { +string("\n4. second expression's type: ")+tp3->toString()); return tp2; } - case MATCH: + case MATCH: { SymSExpr *scruttp = (SymSExpr *)check_code(e->kids[0]); Expr *tptp = NULL; @@ -905,14 +913,14 @@ Expr *check_code(Expr *_e) { while ((c_or_default = *cur++)) { Expr *tp = NULL; CExpr *pat = NULL; - if (c_or_default->getop() != CASE) + if (c_or_default->getop() != CASE) // this is the default of the MATCH tp = check_code(c_or_default); else { // this is a CASE of the MATCH c = (CExpr *)c_or_default; pat = (CExpr *)c->kids[0]; // might be just a SYMS_EXPR - if (pat->getclass() == SYMS_EXPR) + if (pat->getclass() == SYMS_EXPR) tp = check_code(c->kids[1]); else { // extend type context and then check the body of the case @@ -941,7 +949,7 @@ Expr *check_code(Expr *_e) { symbol_types[((SymSExpr *)vars[i])] = curtp->followDefs()->kids[1]; #else prevs.push_back - (symbols->insert(((SymSExpr *)vars[i])->s.c_str(), + (symbols->insert(((SymSExpr *)vars[i])->s.c_str(), pair(NULL, ((CExpr *)(curtp->followDefs()))->kids[1]))); #endif @@ -949,7 +957,7 @@ Expr *check_code(Expr *_e) { } tp = check_code(c->kids[1]); - + for (int i = 0, iend = prevs.size(); i < iend; i++) { #ifdef USE_HASH_MAPS symbol_types[((SymSExpr *)vars[i])->s] = prevs[i]; @@ -974,13 +982,13 @@ Expr *check_code(Expr *_e) { : (string("\n2. type for the body of case for ") +pat->toString())) +string(": ")+tp->toString()); - + } return mtp; } } // end switch - + report_error("Type checking an unrecognized form of code (internal error)."); return NULL; } @@ -1013,12 +1021,12 @@ Expr *run_code(Expr *_e) { return e; case HOLE_EXPR: { Expr *tmp = e->followDefs(); - if (tmp == e) + if (tmp == e) report_error("Encountered an unfilled hole running code."); tmp->inc(); return tmp; } - case SYMS_EXPR: + case SYMS_EXPR: case SYM_EXPR: { Expr *tmp = e->followDefs(); //std::cout << "follow def = "; @@ -1054,7 +1062,7 @@ Expr *run_code(Expr *_e) { r0->dec(); return r1; } - case ADD: + case ADD: case MUL: case DIV: { @@ -1127,7 +1135,7 @@ Expr *run_code(Expr *_e) { return NULL; } } - case IFNEG: + case IFNEG: case IFZERO:{ Expr *r1 = run_code(e->kids[0]); if (!r1) @@ -1142,7 +1150,7 @@ Expr *run_code(Expr *_e) { }else if( r1->getclass() == RAT_EXPR ){ if( e->getop() == IFNEG ) cond = mpq_sgn( ((RatExpr *)r1)->n )<0; - else if( e->getop() == IFZERO ) + else if( e->getop() == IFZERO ) cond = mpq_sgn( ((RatExpr *)r1)->n )==0; } else @@ -1203,7 +1211,7 @@ Expr *run_code(Expr *_e) { _e = e->kids[2]; goto start_run_code; } - //else + //else r2->dec(); _e = e->kids[3]; goto start_run_code; @@ -1283,7 +1291,7 @@ Expr *run_code(Expr *_e) { vector args; Expr *hd = e->collect_args(args); - for (int i = 0, iend = args.size(); i < iend; i++) + for (int i = 0, iend = args.size(); i < iend; i++) if (!(args[i] = run_code(args[i]))) { for (int j = 0; j < i; j++) args[j]->dec(); diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index 7ffc6469a..ae0e49531 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -234,6 +234,7 @@ Expr* Expr::make_app(Expr* e1, Expr* e2 ) counter = 0; while( ((CExpr*)e1)->kids[counter] ){ ret->kids[counter] = ((CExpr*)e1)->kids[counter]; + ret->kids[counter]->inc(); counter++; } ret->kids[counter] = e2; @@ -346,8 +347,8 @@ Expr* CExpr::convert_to_tree_app( Expr* e ) if( e->getop()==APP ) { std::vector< Expr* > kds; - int counter = 1; - while( ((CExpr*)e)->kids[counter] ) + int counter = 1; + while( ((CExpr*)e)->kids[counter] ) { kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) ); counter++; @@ -963,4 +964,4 @@ void SymExpr::smark( int m ) { mark_map[this] = m; } -#endif \ No newline at end of file +#endif diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf new file mode 100755 index 000000000..12c4c3e16 --- /dev/null +++ b/proofs/signatures/ex-mem.plf @@ -0,0 +1,68 @@ +; AJR : proof used for testing memory use of theory lemmas + +(check +(% s sort +(% a (term s) +(% b (term s) +(% c (term s) +(% f (term (arrow s s)) + +; -------------------- declaration of input formula ----------------------------------- + +(% A1 (th_holds (= s a b)) +(% A2 (th_holds (= s b a)) +(% A3 (th_holds (not (= s a a))) + +; ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + +; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ + +(decl_atom (= s a b) (\ v1 (\ a1 +(decl_atom (= s b a) (\ v2 (\ a2 +(decl_atom (= s a a) (\ v3 (\ a3 + +; --------------------------- proof of theory lemma --------------------------------------------- + +(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1 +(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT2 +(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT3 +;...add copies here... + +; -------------------- clausification of input formulas ----------------------------------------- + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(clausify_false + (contra _ A1 l1) +))) (\ C1 +; C1 is the clause ( v1 ) + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + (contra _ A2 l2) +))) (\ C2 +; C2 is the clause ( v2 ) + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(clausify_false + (contra _ l3 A3) +))) (\ C3 +; C3 is the clause ( ~v3 ) + + +; -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ +(R _ _ C2 +(R _ _ C1 CT1 v1) v2) C3 v3) + +(\ x x)) + +))))))))))))))))))))))))))))) +)) -- 2.30.2