X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=constgen.cc;h=82042af420bedfdd4b7b29c084f64aeeb33c081d;hb=bd644b5504a9bfc394bf245dc7a8579ebed9254a;hp=4f4ec3a65bee2e42d0db39233fe0de5314335df1;hpb=9031836d066385fcd527a2e6dc7e065473096f10;p=satcheck.git

diff --git a/constgen.cc b/constgen.cc
index 4f4ec3a..82042af 100644
--- a/constgen.cc
+++ b/constgen.cc
@@ -38,6 +38,7 @@ ConstGen::ConstGen(MCExecution *e) :
 	rpt(new RecPairTable()),
 	numconstraints(0),
 	goalset(new ModelVector<Constraint *>()),
+	yieldlist(new ModelVector<EPRecord *>()),
 	goalvararray(NULL),
 	vars(new ModelVector<Constraint *>()),
 	branchtable(new BranchTable()),
@@ -45,9 +46,11 @@ ConstGen::ConstGen(MCExecution *e) :
 	equalstable(new EqualsTable()),
 	schedulebuilder(new ScheduleBuilder(e, this)),
 	nonlocaltrans(new RecordSet()),
+	incompleteexploredbranch(new RecordSet()),
 	execcondtable(new LoadHashTable()),
 	solver(NULL),
 	rectoint(new RecToIntTable()),
+	yieldtable(new RecToConsTable()),
 	varindex(1),
 	schedule_graph(0),
 	has_untaken_branches(false)
@@ -80,14 +83,17 @@ ConstGen::~ConstGen() {
 	delete threadactions;
 	delete rpt;
 	delete goalset;
+	delete yieldlist;
 	delete vars;
 	delete branchtable;
 	delete functiontable;
 	delete equalstable;
 	delete schedulebuilder;
 	delete nonlocaltrans;
+	delete incompleteexploredbranch;
 	delete execcondtable;
 	delete rectoint;
+	delete yieldtable;
 }
 
 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
@@ -128,8 +134,11 @@ void ConstGen::reset() {
 	rpt->resetanddelete();
 	resetstoreloadtable(storeloadtable);
 	nonlocaltrans->reset();
+	incompleteexploredbranch->reset();
 	threadactions->clear();
 	rectoint->reset();
+	yieldtable->reset();
+	yieldlist->clear();
 	goalset->clear();
 	varindex=1;
 	numconstraints=0;
@@ -1138,8 +1147,12 @@ bool ConstGen::isAlwaysExecuted(EPRecord *record) {
 void ConstGen::insertBranch(EPRecord *record) {
 	uint numvalue=record->numValues();
 	/** need one value for new directions */
-	if (numvalue<record->getLen())
+	if (numvalue<record->getLen()) {
 		numvalue++;
+		if (model->params.noexecyields) {
+			incompleteexploredbranch->add(record);
+		}
+	}
 	/** need extra value to represent that branch wasn't executed. **/
 	bool alwaysexecuted=isAlwaysExecuted(record);
 	if (!alwaysexecuted)
@@ -1471,13 +1484,84 @@ void ConstGen::processStore(EPRecord *record) {
 	processAddresses(record);
 }
 
+/** **/
+
+void ConstGen::computeYieldCond(EPRecord *record) {
+	ExecPoint *yieldep=record->getEP();
+	EPRecord *prevyield=NULL;
+	ExecPoint *prevyieldep=NULL;
+	
+	for(int i=(int)(yieldlist->size()-1);i>=0;i--) {
+		EPRecord *tmpyield=(*yieldlist)[i];
+		ExecPoint *tmpep=tmpyield->getEP();
+		//Do we have a previous yield operation
+		if (yieldep->compare(tmpep)==CR_BEFORE) {
+			//Yes
+			prevyield=tmpyield;
+			prevyieldep=prevyield->getEP();
+			break;
+		}
+	}
+	
+	yieldlist->push_back(record);
+
+	ModelVector<Constraint *> * novel_branches=new ModelVector<Constraint *>();
+	RecordIterator *sri=incompleteexploredbranch->iterator();
+	while(sri->hasNext()) {
+		EPRecord * unexploredbranch=sri->next();
+		ExecPoint * branchep=unexploredbranch->getEP();
+		if (yieldep->compare(branchep)!=CR_BEFORE) {
+			//Branch does not occur before yield, so skip
+			continue;
+		}
+
+		//See if the previous yield already accounts for this branch
+		if (prevyield != NULL &&
+				prevyieldep->compare(branchep)==CR_BEFORE) {
+			//Branch occurs before previous yield, so we can safely skip this branch
+						continue;
+		}
+
+		//This is a branch that could prevent this yield from being executed
+		BranchRecord *br=branchtable->get(unexploredbranch);
+		Constraint * novel_branch=br->getNewBranch();
+		novel_branches->push_back(novel_branch);
+	}
+
+	int num_constraints=((prevyield==NULL)?0:1)+novel_branches->size();
+	Constraint *carray[num_constraints];
+	int arr_index=0;
+	
+	if (prevyield!=NULL) {
+		carray[arr_index++]=yieldtable->get(prevyield);//get constraint for old yield
+	}
+	for(uint i=0;i<novel_branches->size();i++) {
+		carray[arr_index++]=(*novel_branches)[i];
+	}
+	
+	Constraint *cor=num_constraints!=0?new Constraint(OR, num_constraints, carray):&cfalse;
+
+	Constraint *var=getNewVar();
+	//If the variable is true, then we need to have taken some branch
+	//ahead of the yield
+	Constraint *implies=new Constraint(IMPLIES, var, cor);
+	ADDCONSTRAINT(implies, "possiblebranchnoyield");
+	yieldtable->put(record, var);
+	
+	delete novel_branches;
+	delete sri;
+}
+
+
 /** Handle yields by just forbidding them via the SAT formula. */
 
 void ConstGen::processYield(EPRecord *record) {
-	if (model->params.noyields &&
-			record->getBranch()!=NULL) {
-		Constraint * noyield=getExecutionConstraint(record)->negate();
-		ADDCONSTRAINT(noyield, "noyield");
+	if (model->params.noexecyields) {
+		computeYieldCond(record);
+		Constraint * noexecyield=getExecutionConstraint(record)->negate();
+		Constraint * branchaway=yieldtable->get(record);
+		Constraint * avoidbranch=new Constraint(OR, noexecyield, branchaway);
+		ADDCONSTRAINT(avoidbranch, "noexecyield");
 	}
 }
 
@@ -1732,6 +1816,9 @@ void ConstGen::processFence(EPRecord *record) {
 }
 #endif
 
+/** processRecord performs actions on second traversal of event
+		graph. */
+
 void ConstGen::processRecord(EPRecord *record) {
 	switch (record->getType()) {
 	case FUNCTION:
@@ -1775,6 +1862,9 @@ void ConstGen::processRecord(EPRecord *record) {
 	}
 }
 
+/** visitRecord performs actions done on first traversal of event
+ *	graph. */
+
 void ConstGen::visitRecord(EPRecord *record) {
 	switch (record->getType()) {
 	case EQUALS:
@@ -1890,6 +1980,9 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
 		if (record->getType()==NONLOCALTRANS) {
 			return;
 		}
+		if (record->getType()==YIELD && model->params.noexecyields) {
+			return;
+		}
 		if (record->getType()==LOOPEXIT) {
 			return;
 		}