From 7e0873373529f7d7d393a48384e0afa7b2d368af Mon Sep 17 00:00:00 2001 From: Xuejun Yang Date: Fri, 27 Nov 2020 17:34:58 -0800 Subject: [PATCH] Update facts for definitive assignment based on number of pointees on LHS Also: 1) Add Statement::to_string for better debugging 2) Force all analysis failures to be reported via log_analysis_fail Fix #104 --- src/Block.cpp | 4 ++-- src/ExpressionComma.cpp | 2 +- src/ExpressionVariable.cpp | 12 +++++++++--- src/Fact.cpp | 12 +++++++++--- src/Fact.h | 6 +++++- src/FactMgr.cpp | 27 +++++++++++++++------------ src/FactPointTo.cpp | 22 +++++++++++++--------- src/FactPointTo.h | 2 +- src/FactUnion.cpp | 30 +++++++++++++++--------------- src/FactUnion.h | 2 +- src/FunctionInvocation.cpp | 7 +++++-- src/FunctionInvocationBinary.cpp | 2 +- src/Lhs.cpp | 13 ++++++++----- src/Statement.cpp | 9 --------- src/Statement.h | 8 ++++++++ src/StatementArrayOp.cpp | 8 ++++---- src/StatementAssign.cpp | 5 +++-- src/StatementBreak.cpp | 2 +- src/StatementContinue.cpp | 2 +- src/StatementExpr.cpp | 3 +++ src/StatementFor.cpp | 4 ++-- src/StatementGoto.cpp | 4 ++-- src/StatementIf.cpp | 6 +++--- src/StatementReturn.cpp | 4 ++-- src/util.cpp | 8 ++++++++ src/util.h | 3 ++- 26 files changed, 124 insertions(+), 83 deletions(-) diff --git a/src/Block.cpp b/src/Block.cpp index 798f2765b..564f89969 100644 --- a/src/Block.cpp +++ b/src/Block.cpp @@ -535,7 +535,7 @@ Block::visit_facts(vector& inputs, CGContext& cg_context) const Effect pre_effect = cg_context.get_accum_effect(); if (!find_fixed_point(inputs, dummy_facts, cg_context, dummy, false)) { cg_context.reset_effect_accum(pre_effect); - return false; + return log_analysis_fail("Block. reason can't converge to fixed point"); } inputs = fm->map_facts_out[this]; fm->map_visited[this] = true; @@ -615,7 +615,7 @@ Block::find_fixed_point(vector inputs, vector& post_fa // revisit statements with new inputs for (i=0; ianalyze_with_edges_in(outputs, cg_context)) { fail_index = i; diff --git a/src/ExpressionComma.cpp b/src/ExpressionComma.cpp index e518e6463..ce7ebc868 100644 --- a/src/ExpressionComma.cpp +++ b/src/ExpressionComma.cpp @@ -94,7 +94,7 @@ bool ExpressionComma::visit_facts(vector& inputs, CGContext& cg_context) const { if (!lhs.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("ExpressionComma"); } return rhs.visit_facts(inputs, cg_context); } diff --git a/src/ExpressionVariable.cpp b/src/ExpressionVariable.cpp index d215586ac..c0ebe8f5d 100644 --- a/src/ExpressionVariable.cpp +++ b/src/ExpressionVariable.cpp @@ -250,22 +250,28 @@ ExpressionVariable::visit_facts(vector& inputs, CGContext& cg_conte const Variable* v = get_var(); if (deref_level > 0) { if (!FactPointTo::is_valid_ptr(v, inputs)) { - return false; + return log_analysis_fail(v->name + " with ExpressionVariable. reason invalid pointer"); } // Yang: do we need to consider the deref_level? bool valid = cg_context.check_read_var(v, inputs) && cg_context.read_pointed(this, inputs) && cg_context.check_deref_volatile(v, deref_level); + + if (!valid) + return log_analysis_fail(v->name + " with ExpressionVariable. reason invalid read through pointer"); return valid; } // we filter out bitfield if (deref_level < 0) { if (v->isBitfield_) - return false; + return log_analysis_fail(v->name + " with ExpressionVariable. reason bitfield"); // it's actually valid to take address of a null/dead pointer return true; } else { - return cg_context.check_read_var(v, inputs); + bool valid = cg_context.check_read_var(v, inputs); + if (!valid) + return log_analysis_fail(v->name + " with ExpressionVariable. reason invalid read"); + return valid; } } diff --git a/src/Fact.cpp b/src/Fact.cpp index c2f38c294..1448f92c0 100644 --- a/src/Fact.cpp +++ b/src/Fact.cpp @@ -83,7 +83,9 @@ std::vector Fact::abstract_fact_for_return(const std::vector& facts, const ExpressionVariable* expr, const Function* func) { Lhs lhs(*func->rv); - return abstract_fact_for_assign(facts, &lhs, expr); + vector facts_out; + abstract_fact_for_assign(facts, &lhs, expr, facts_out); + return facts_out; } vector @@ -94,13 +96,17 @@ Fact::abstract_fact_for_var_init(const Variable* v) if (v->type == NULL || (v->type->eType != ePointer && v->type->eType != eUnion)) return empty; Lhs lhs(*v); - vector facts = abstract_fact_for_assign(empty, &lhs, v->init); + vector facts; + int lvar_cnt = abstract_fact_for_assign(empty, &lhs, v->init, facts); + assert(lvar_cnt == 1); + if (v->isArray) { const ArrayVariable* av = dynamic_cast(v); assert(av); for (size_t i=0; iget_more_init_values().size(); i++) { const Expression* init = av->get_more_init_values()[i]; - vector more_facts = abstract_fact_for_assign(empty, &lhs, init); + vector more_facts; + abstract_fact_for_assign(empty, &lhs, init, more_facts); merge_facts(facts, more_facts); } } diff --git a/src/Fact.h b/src/Fact.h index cdad85d3d..fa93f5cce 100644 --- a/src/Fact.h +++ b/src/Fact.h @@ -90,7 +90,11 @@ class Fact virtual const Variable* get_var(void) const { return 0;}; - virtual std::vector abstract_fact_for_assign(const std::vector& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/) = 0; + /// Given existing facts, LHS and RHS of the assignment, derive the new facts, + /// and return the number of possible assignees. In most cases that's 1. But + /// if LHS is a pointer dereference, the number of assignees could > 1 depending + /// on the points-to analysis. + virtual int abstract_fact_for_assign(const std::vector& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector&) = 0; virtual vector abstract_fact_for_return(const std::vector& facts, const ExpressionVariable* expr, const Function* func); diff --git a/src/FactMgr.cpp b/src/FactMgr.cpp index 4e87714bd..8feeeb006 100644 --- a/src/FactMgr.cpp +++ b/src/FactMgr.cpp @@ -387,19 +387,22 @@ FactMgr::update_fact_for_assign(const Lhs* lhs, const Expression* rhs, FactVec& { bool changed = false; for (size_t i=0; i facts = FactMgr::meta_facts[i]->abstract_fact_for_assign(inputs, lhs, rhs); - if (facts.size() == 1 && !facts[0]->get_var()->isArray) { - // for must-point-to fact concerning no-array variable, just renew the old fact - renew_fact(inputs, facts[0]); - } - else { - // for may-point-to facts (which means pointer on LHS is uncertain), merge them with old facts - for (size_t j=0; j facts; + int lvar_cnt = FactMgr::meta_facts[i]->abstract_fact_for_assign(inputs, lhs, rhs, facts); + if (facts.size() > 0) + { + if (lvar_cnt == 1 && !facts[0]->get_var()->isArray) { + // for definitive assignment to a no-array variable, just renew the old fact. + renew_fact(inputs, facts[0]); } - } - if (facts.size() > 0) { + else { + // for may-point-to facts (which means pointer on LHS is uncertain), merge them with old facts + for (size_t j=0; j& facts, const vector< return empty; } -std::vector -FactPointTo::abstract_fact_for_assign(const std::vector& facts, const Lhs* lhs, const Expression* rhs) +int +FactPointTo::abstract_fact_for_assign(const std::vector& facts_in, const Lhs* lhs, const Expression* rhs, std::vector& facts_out) { - std::vector ret_facts; + facts_out.clear(); // find all the pointed variables on LHS - vector lvars = merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts); - // return empty set if lhs is not pointer + vector lvars = merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts_in); + + // Handle points-to facts if (lhs->get_type().eType == ePointer) { - return rhs_to_lhs_transfer(facts, lvars, rhs); + facts_out = rhs_to_lhs_transfer(facts_in, lvars, rhs); + return lvars.size(); } + + // Handle union field facts for (size_t i=0; iis_inside_union_field()) { @@ -295,10 +299,10 @@ FactPointTo::abstract_fact_for_assign(const std::vector& facts, con vector pointers; v->find_pointer_fields(pointers); // transfer facts for pointer fields - FactVec new_facts = rhs_to_lhs_transfer(facts, pointers, rhs); - ret_facts.insert(ret_facts.end(), new_facts.begin(), new_facts.end()); + FactVec new_facts = rhs_to_lhs_transfer(facts_in, pointers, rhs); + facts_out.insert(facts_out.end(), new_facts.begin(), new_facts.end()); } - return ret_facts; + return lvars.size(); } Fact* diff --git a/src/FactPointTo.h b/src/FactPointTo.h index e986767a7..d1d25d64b 100644 --- a/src/FactPointTo.h +++ b/src/FactPointTo.h @@ -70,7 +70,7 @@ class FactPointTo : public Fact bool has_invisible(const Statement* stm) const; int size() const; std::vector rhs_to_lhs_transfer(const std::vector& facts, const vector& lvars, const Expression* rhs); - virtual vector abstract_fact_for_assign(const std::vector& facts, const Lhs* lhs, const Expression* rhs); + virtual int abstract_fact_for_assign(const std::vector& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector&); FactPointTo* mark_dead_var(const Variable* v); FactPointTo* mark_func_end(const Statement* stm); diff --git a/src/FactUnion.cpp b/src/FactUnion.cpp index 131195cb6..56ad6fcb1 100644 --- a/src/FactUnion.cpp +++ b/src/FactUnion.cpp @@ -123,37 +123,37 @@ FactUnion::rhs_to_lhs_transfer(const std::vector& facts, const vect } /* draw facts from an assignment */ -std::vector -FactUnion::abstract_fact_for_assign(const std::vector& facts, const Lhs* lhs, const Expression* rhs) +int +FactUnion::abstract_fact_for_assign(const std::vector& facts, const Lhs* lhs, const Expression* rhs, std::vector& facts_out) { - std::vector ret_facts; - if (rhs == NULL) return ret_facts; + facts_out.clear(); + // find all the pointed variables on LHS std::vector lvars = FactPointTo::merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts); if (lhs->get_type().eType == eUnion) { - return rhs_to_lhs_transfer(facts, lvars, rhs); + facts_out = rhs_to_lhs_transfer(facts, lvars, rhs); + return lvars.size(); } + if (rhs == NULL) + return lvars.size(); + for (size_t i=0; iis_union_field()) { - if (lvars.size() > 1) { - // if writing to an union field is uncertain (due to dereference of a pointer which may points to an - // union field or something else), We mark the union as unreadable - fu = make_fact(v->field_var_of, BOTTOM); - } else { - fu = make_fact(v->field_var_of, v->get_field_id()); - } - } else if (v->is_inside_union_field() && (v->type->has_padding() || v->is_packed_after_bitfield())) { + // If one of the lvars is a union field, we report the fact and let FactMgr decides what to do. + fu = make_fact(v->field_var_of, v->get_field_id()); + } + else if (v->is_inside_union_field() && (v->type->has_padding() || v->is_packed_after_bitfield())) { fu = make_fact(v->get_container_union(), BOTTOM); } if (fu) { - ret_facts.push_back(fu); + facts_out.push_back(fu); } } - return ret_facts; + return lvars.size(); } Fact* diff --git a/src/FactUnion.h b/src/FactUnion.h index 34b497bf3..ca1c6008b 100644 --- a/src/FactUnion.h +++ b/src/FactUnion.h @@ -73,7 +73,7 @@ class FactUnion : public Fact // transfer functions vector rhs_to_lhs_transfer(const vector& facts, const vector& lvars, const Expression* rhs); - virtual vector abstract_fact_for_assign(const std::vector& facts, const Lhs* lhs, const Expression* /*rhs*/); + virtual int abstract_fact_for_assign(const std::vector& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector&); //virtual vector abstract_fact_for_return(const std::vector& facts, const ExpressionVariable* rv, const Function* func); virtual Fact* join_var_facts(const vector& facts, const vector& vars) const; virtual Fact* clone(void) const; diff --git a/src/FunctionInvocation.cpp b/src/FunctionInvocation.cpp index c47668c58..aa99588be 100644 --- a/src/FunctionInvocation.cpp +++ b/src/FunctionInvocation.cpp @@ -518,10 +518,10 @@ FunctionInvocation::visit_facts(vector& inputs, CGContext& cg_conte CGContext param_cg_context(cg_context, running_eff_context, ¶m_eff_accum); // the parameters might be function calls const Expression* value = param_value[i]; - if (h == 236) + if (h == 2684) BREAK_NOP; // for debugging if (!value->visit_facts(inputs, param_cg_context)) { - return false; + return log_analysis_fail(std::string("Parameter ") + std::to_string(i) + " with FunctionInvocation"); } // Update the "running effect context": the context that we must use // when we generate subsequent parameters within this invocation. @@ -550,6 +550,9 @@ FunctionInvocation::visit_facts(vector& inputs, CGContext& cg_conte func_effect.add_external_effect(*new_context.get_effect_accum(), cg_context.call_chain); } } + + if (!ok) + log_analysis_fail("FunctionInvocation"); return ok; } diff --git a/src/FunctionInvocationBinary.cpp b/src/FunctionInvocationBinary.cpp index 17f680c3e..e20dcff9a 100644 --- a/src/FunctionInvocationBinary.cpp +++ b/src/FunctionInvocationBinary.cpp @@ -476,7 +476,7 @@ FunctionInvocationBinary::visit_facts(vector& inputs, CGContext& cg return true; } } - return false; + return log_analysis_fail("FunctionInvocationBinary"); } // for other binary invocations, use the standard visitor return FunctionInvocation::visit_facts(inputs, cg_context); diff --git a/src/Lhs.cpp b/src/Lhs.cpp index 62ec8e324..e24845c0c 100644 --- a/src/Lhs.cpp +++ b/src/Lhs.cpp @@ -334,11 +334,11 @@ Lhs::visit_facts(vector& inputs, CGContext& cg_context) const if (for_compound_assign) { ExpressionVariable ev(*v, type); if (!ev.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail(v->name + " with Lhs. reason rhs"); } } if (!visit_indices(inputs, cg_context)) { - return false; + return log_analysis_fail(v->name + " with Lhs. reason indices"); } // avoid a.x = a.y (or any RHS that evaluates to a.y) where x and y are partially overlapping fields if (cg_context.curr_rhs) { @@ -347,7 +347,7 @@ Lhs::visit_facts(vector& inputs, CGContext& cg_context) const for (size_t i=0; iterm_type == eVariable || subs[i]->term_type == eLhs) { if (have_overlapping_fields(subs[i], this, inputs)) { - return false; + return log_analysis_fail(v->name + " with Lhs. reason lhs and rhs overlap"); } } } @@ -356,10 +356,10 @@ Lhs::visit_facts(vector& inputs, CGContext& cg_context) const int deref_level = get_indirect_level(); if (deref_level > 0) { if (!FactPointTo::is_valid_ptr(v, inputs)) { - return false; + return log_analysis_fail(v->name + " with Lhs. reason invalid lhs pointer"); } if (ptr_modified_in_rhs(inputs, cg_context)) { - return false; + return log_analysis_fail(v->name + " with Lhs. reason lhs modified in rhs"); } valid = cg_context.check_read_var(v, inputs) && cg_context.write_pointed(this, inputs) && cg_context.check_deref_volatile(v, deref_level); @@ -373,6 +373,9 @@ Lhs::visit_facts(vector& inputs, CGContext& cg_context) const eff->set_lhs_write_vars(eff->get_write_vars()); } } + + if (!valid) + return log_analysis_fail(v->name + " with Lhs."); return valid; } diff --git a/src/Statement.cpp b/src/Statement.cpp index e747e5841..66f9b62e0 100644 --- a/src/Statement.cpp +++ b/src/Statement.cpp @@ -651,8 +651,6 @@ Statement::stm_visit_facts(vector& inputs, CGContext& cg_context) c cg_context.get_effect_stm().clear(); cg_context.curr_blk = parent; FactMgr* fm = get_fact_mgr(&cg_context); - //static int g = 0; - //int h = g++; bool ok = visit_facts(inputs, cg_context); @@ -925,13 +923,6 @@ Statement::post_creation_analysis(vector& pre_facts, const Effect& if (has_uncertain_call_recursive()) { FactVec outputs = pre_facts; cg_context.reset_effect_accum(pre_effect); - //if (stm_id == 573) - /*if (this->eType == eAssign) { - ((const StatementAssign*)this)->get_rhs()->indented_output(cout, 0); - } - cout << endl; - Output(cout, fm);*/ - //} if (!validate_and_update_facts(outputs, cg_context)) { assert(0); } diff --git a/src/Statement.h b/src/Statement.h index 166fb4629..7b5ffa529 100644 --- a/src/Statement.h +++ b/src/Statement.h @@ -41,6 +41,7 @@ #endif #include #include +#include #include #include "Probabilities.h" using namespace std; @@ -100,6 +101,13 @@ class Statement eStatementType get_type(void) const { return eType; } + std::string to_string(void) const + { + ostringstream oss; + Output(oss); + return oss.str(); + } + void get_called_funcs(std::vector& funcs) const; const FunctionInvocation* get_direct_invocation(void) const; diff --git a/src/StatementArrayOp.cpp b/src/StatementArrayOp.cpp index 6bc1ef132..2dd955eff 100644 --- a/src/StatementArrayOp.cpp +++ b/src/StatementArrayOp.cpp @@ -297,7 +297,7 @@ StatementArrayOp::visit_facts(vector& inputs, CGContext& cg_context for (i=0; iget_dimension(); i++) { const Variable *cv = ctrl_vars[i]; if (!cg_context.check_write_var(cv, inputs)) { - return false; + return log_analysis_fail("StatementArrayOp cv"); } } FactMgr* fm = get_fact_mgr(&cg_context); @@ -306,7 +306,7 @@ StatementArrayOp::visit_facts(vector& inputs, CGContext& cg_context FactVec facts_copy = inputs; Effect eff = cg_context.get_effect_stm(); if (!body->visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementArrayOp body"); } // if body must return, means the control reached end of for-loop with pre-loop env if (body->must_return()) { @@ -329,10 +329,10 @@ StatementArrayOp::visit_facts(vector& inputs, CGContext& cg_context else if (init_value) { Lhs lhs(*array_var); if (!init_value->visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementArrayOp init value"); } if (!lhs.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementArrayOp lhs"); } FactMgr::update_fact_for_assign(&lhs, init_value, inputs); fm->map_stm_effect[this] = cg_context.get_effect_stm(); diff --git a/src/StatementAssign.cpp b/src/StatementAssign.cpp index cdbe4367a..172613f34 100644 --- a/src/StatementAssign.cpp +++ b/src/StatementAssign.cpp @@ -196,6 +196,7 @@ StatementAssign::make_random(CGContext &cg_context, const Type* type, const CVQu else { lhs = Lhs::make_random(lhs_cg_context, type, &qfer, op != eSimpleAssign, need_no_rhs(op)); } + if (qf) CGOptions::match_exact_qualifiers(prev_flag); // restore flag ERROR_GUARD_AND_DEL2(NULL, e, lhs); @@ -335,7 +336,7 @@ StatementAssign::visit_facts(vector& inputs, CGContext& cg_context) Effect rhs_accum, lhs_accum; CGContext rhs_cg_context(cg_context, running_eff_context, &rhs_accum); if (!expr.visit_facts(inputs, rhs_cg_context)) { - return false; + return log_analysis_fail("StatementAssign rhs"); } // for compound assignment, LHS needs to be evaluated in the effect context of RHS @@ -351,7 +352,7 @@ StatementAssign::visit_facts(vector& inputs, CGContext& cg_context) lhs_cg_context.get_effect_stm() = rhs_cg_context.get_effect_stm(); lhs_cg_context.curr_rhs = &expr; if (!lhs.visit_facts(inputs, lhs_cg_context)) { - return false; + return log_analysis_fail("StatementAssign lhs"); } cg_context.merge_param_context(lhs_cg_context, true); //cg_context.get_effect_stm() = lhs_cg_context.get_effect_stm(); diff --git a/src/StatementBreak.cpp b/src/StatementBreak.cpp index 490cda5cc..bbce085e8 100644 --- a/src/StatementBreak.cpp +++ b/src/StatementBreak.cpp @@ -141,7 +141,7 @@ StatementBreak::visit_facts(vector& inputs, CGContext& cg_context) { // evaludate condition first if (!test.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementBreak"); } FactMgr* fm = get_fact_mgr(&cg_context); fm->map_stm_effect[this] = cg_context.get_effect_stm(); diff --git a/src/StatementContinue.cpp b/src/StatementContinue.cpp index b7d4f71c8..3a08212ef 100644 --- a/src/StatementContinue.cpp +++ b/src/StatementContinue.cpp @@ -141,7 +141,7 @@ StatementContinue::visit_facts(vector& inputs, CGContext& cg_contex { // evaludate condition first if (!test.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementContinue"); } FactMgr* fm = get_fact_mgr(&cg_context); fm->map_stm_effect[this] = cg_context.get_effect_stm(); diff --git a/src/StatementExpr.cpp b/src/StatementExpr.cpp index 94c7e1ee7..f80639909 100644 --- a/src/StatementExpr.cpp +++ b/src/StatementExpr.cpp @@ -119,6 +119,9 @@ StatementExpr::visit_facts(vector& inputs, CGContext& cg_context) c // save effect FactMgr* fm = get_fact_mgr(&cg_context); fm->map_stm_effect[this] = cg_context.get_effect_stm(); + + if (!ok) + return log_analysis_fail("StatementExpr"); return ok; } diff --git a/src/StatementFor.cpp b/src/StatementFor.cpp index 30fb7c167..364349936 100644 --- a/src/StatementFor.cpp +++ b/src/StatementFor.cpp @@ -420,7 +420,7 @@ StatementFor::visit_facts(vector& inputs, CGContext& cg_context) co { // walk the initializing statement if (!init.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementFor init"); } //print_facts(inputs); FactVec facts_copy = inputs; @@ -436,7 +436,7 @@ StatementFor::visit_facts(vector& inputs, CGContext& cg_context) co if (!body.visit_facts(inputs, cg_context)) { // remove IV from context cg_context.iv_bounds.erase(iv); - return false; + return log_analysis_fail("StatementFor loop body"); } FactMgr* fm = get_fact_mgr(&cg_context); // if body must return, means the control reached end of for-loop with pre-loop env diff --git a/src/StatementGoto.cpp b/src/StatementGoto.cpp index 73073a4f8..c60320eca 100644 --- a/src/StatementGoto.cpp +++ b/src/StatementGoto.cpp @@ -371,12 +371,12 @@ StatementGoto::visit_facts(vector& inputs, CGContext& cg_context) c { // evaludate condition first if (!test.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementGoto condition"); } size_t i; for (i=0; i& inputs, CGContext& cg_context) con vector inputs_copy = inputs; // evaludate condition first if (!test.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementIf condition"); } Effect eff = cg_context.get_effect_stm(); FactVec inputs_true = inputs; if (!if_true.visit_facts(inputs_true, cg_context)) { - return false; + return log_analysis_fail("StatementIf true-branch"); } FactVec inputs_false = inputs; if (!if_false.visit_facts(inputs_false, cg_context)) { - return false; + return log_analysis_fail("StatementIf false-branch"); } // compute accumulated effect for this statement set_accumulated_effect_after_block(eff, &if_true, cg_context); diff --git a/src/StatementReturn.cpp b/src/StatementReturn.cpp index 91d2d72f6..3eb47447b 100644 --- a/src/StatementReturn.cpp +++ b/src/StatementReturn.cpp @@ -87,12 +87,12 @@ StatementReturn::visit_facts(vector& inputs, CGContext& cg_context) const Block* b = cg_context.curr_blk; assert(b); if (FactPointTo::is_pointing_to_locals(v, b, indirection, inputs)) { - return false; + return log_analysis_fail("StatementReturn 1"); } } if (!var.visit_facts(inputs, cg_context)) { - return false; + return log_analysis_fail("StatementReturn 2"); } FactMgr::update_fact_for_return(this, inputs); FactMgr* fm = get_fact_mgr(&cg_context); diff --git a/src/util.cpp b/src/util.cpp index a8f09b980..b10b9fdf2 100644 --- a/src/util.cpp +++ b/src/util.cpp @@ -80,6 +80,14 @@ gensym(const string& basename) return ss.str(); } +static std::string errlog; + +bool log_analysis_fail(std::string msg) +{ + errlog += "Analysis failed at " + msg + "\n"; + return false; +} + /* * permute an integer array * return: all possible permutations of input integer array diff --git a/src/util.h b/src/util.h index a56010857..7b5adfb87 100644 --- a/src/util.h +++ b/src/util.h @@ -34,7 +34,7 @@ #include #include -#include +#include typedef std::vector intvec; @@ -50,6 +50,7 @@ void output_tab(std::ostream &out, int indent); void output_print_str(std::ostream& out, std::string str, std::string str_value, int indent); void output_open_encloser(const char* symbol, std::ostream &out, int& indent); void output_close_encloser(const char* symbol, std::ostream &out, int& indent, bool no_newline = false); +bool log_analysis_fail(std::string msg); ///////////////////////////////////////////////////////////////////////////////