Merge pull request #107 from csmith-project/jxyang.issue104

Update facts for definitive assignment based on number of pointees on…

src/Block.cpp

@@ -535,7 +535,7 @@ Block::visit_facts(vector<const Fact*>& 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<const Fact*> inputs, vector<const Fact*>& post_fa
 		// revisit statements with new inputs
 		for (i=0; i<stms.size(); i++) {
 			int h = g++;
-			if (h == 2585)
+			if (h == 558)
 				BREAK_NOP;		// for debugging
 			if (!stms[i]->analyze_with_edges_in(outputs, cg_context)) {
 				fail_index = i;

src/ExpressionComma.cpp

@@ -94,7 +94,7 @@ bool
 ExpressionComma::visit_facts(vector<const Fact*>& 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);
 }

src/ExpressionVariable.cpp

@@ -250,22 +250,28 @@ ExpressionVariable::visit_facts(vector<const Fact*>& 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;
 	}
 }
 

src/Fact.cpp

@@ -83,7 +83,9 @@ std::vector<const Fact*>
 Fact::abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* expr, const Function* func)
 {
 	Lhs lhs(*func->rv);
-	return abstract_fact_for_assign(facts, &lhs, expr);
+    vector<const Fact*> facts_out;
+	abstract_fact_for_assign(facts, &lhs, expr, facts_out);
+	return facts_out;
 }
 
 vector<const Fact*>
@@ -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<const Fact*> facts = abstract_fact_for_assign(empty, &lhs, v->init);
+	vector<const Fact*> 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<const ArrayVariable*>(v);
 		assert(av);
 		for (size_t i=0; i<av->get_more_init_values().size(); i++) {
 			const Expression* init = av->get_more_init_values()[i];
-			vector<const Fact*> more_facts = abstract_fact_for_assign(empty, &lhs, init);
+			vector<const Fact*> more_facts;
+			abstract_fact_for_assign(empty, &lhs, init, more_facts);
 			merge_facts(facts, more_facts);
 		}
 	}

src/Fact.h

@@ -90,7 +90,11 @@ class Fact
 
 	virtual const Variable* get_var(void) const { return 0;};
 
-	virtual std::vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& /*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<const Fact*>& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector<const Fact*>&) = 0;
 
 	virtual vector<const Fact*> abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* expr, const Function* func);
 

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<FactMgr::meta_facts.size(); i++) {
-        vector<const Fact*> 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.size(); j++) {
-				const Fact* f = facts[j];
-				merge_fact(inputs, f);
+		vector<const Fact*> 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.size(); j++) {
+					const Fact* f = facts[j];
+					merge_fact(inputs, f);
+				}
+			}
+
 			changed = true;
 		}
     }

src/FactPointTo.cpp

@@ -273,17 +273,21 @@ FactPointTo::rhs_to_lhs_transfer(const vector<const Fact*>& facts, const vector<
 	return empty;
 }
 
-std::vector<const Fact*>
-FactPointTo::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs)
+int
+FactPointTo::abstract_fact_for_assign(const std::vector<const Fact*>& facts_in, const Lhs* lhs, const Expression* rhs, std::vector<const Fact*>& facts_out)
 {
-	std::vector<const Fact*> ret_facts;
+	facts_out.clear();
 
 	// find all the pointed variables on LHS
-	vector<const Variable*> lvars = merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts);
-	// return empty set if lhs is not pointer
+	vector<const Variable*> 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; i<lvars.size(); i++) {
 		const Variable* v = lvars[i];
 		if (v->is_inside_union_field()) {
@@ -295,10 +299,10 @@ FactPointTo::abstract_fact_for_assign(const std::vector<const Fact*>& facts, con
 		vector<const Variable*> 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*

src/FactPointTo.h

@@ -70,7 +70,7 @@ class FactPointTo : public Fact
 	bool has_invisible(const Statement* stm) const;
 	int  size() const;
 	std::vector<const Fact*> rhs_to_lhs_transfer(const std::vector<const Fact*>& facts, const vector<const Variable*>& lvars, const Expression* rhs);
-	virtual vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs);
+	virtual int abstract_fact_for_assign(const std::vector<const Fact*>& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector<const Fact*>&);
 
 	FactPointTo* mark_dead_var(const Variable* v);
 	FactPointTo* mark_func_end(const Statement* stm);

src/FactUnion.cpp

@@ -123,37 +123,37 @@ FactUnion::rhs_to_lhs_transfer(const std::vector<const Fact*>& facts, const vect
 }
 
 /* draw facts from an assignment */
-std::vector<const Fact*>
-FactUnion::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs)
+int
+FactUnion::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs, std::vector<const Fact*>& facts_out)
 {
-	std::vector<const Fact*> ret_facts;
-	if (rhs == NULL) return ret_facts;
+	facts_out.clear();
+
 	// find all the pointed variables on LHS
 	std::vector<const Variable*> 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; i<lvars.size(); i++) {
 		const Variable* v = lvars[i];
 		const FactUnion* fu = 0;
 		if (v->is_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*

src/FactUnion.h

@@ -73,7 +73,7 @@ class FactUnion : public Fact
 
 	// transfer functions
 	vector<const Fact*> rhs_to_lhs_transfer(const vector<const Fact*>& facts, const vector<const Variable*>& lvars, const Expression* rhs);
-	virtual vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* /*rhs*/);
+	virtual int abstract_fact_for_assign(const std::vector<const Fact*>& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector<const Fact*>&);
 	//virtual vector<const Fact*> abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* rv, const Function* func);
 	virtual Fact* join_var_facts(const vector<const Fact*>& facts, const vector<const Variable*>& vars) const;
 	virtual Fact* clone(void) const;

src/FunctionInvocation.cpp

@@ -518,10 +518,10 @@ FunctionInvocation::visit_facts(vector<const Fact*>& inputs, CGContext& cg_conte
 			CGContext param_cg_context(cg_context, running_eff_context, &param_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<const Fact*>& 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;
 }
 

src/FunctionInvocationBinary.cpp

@@ -476,7 +476,7 @@ FunctionInvocationBinary::visit_facts(vector<const Fact*>& 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);

src/Lhs.cpp

@@ -334,11 +334,11 @@ Lhs::visit_facts(vector<const Fact*>& 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<const Fact*>& inputs, CGContext& cg_context) const
 		for (size_t i=0; i<subs.size(); i++) {
 			if (subs[i]->term_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<const Fact*>& 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<const Fact*>& 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;
 }
 

src/Statement.cpp

@@ -651,8 +651,6 @@ Statement::stm_visit_facts(vector<const Fact*>& 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<const Fact*>& 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);
 			}

src/Statement.h

@@ -41,6 +41,7 @@
 #endif
 #include <vector>
 #include <ostream>
+#include <sstream>
 #include <string>
 #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<const FunctionInvocationUser*>& funcs) const;
 
 	const FunctionInvocation* get_direct_invocation(void) const;