Corrects MC models

include/lrumc/features.h

@@ -35,6 +35,7 @@ extern otawa::p::id<DUCategory> DU_CATEGORY;
 enum class CacheModelKind
 {
 	YOUNGER_SET,
+	YOUNGER_SET_BOUNDED_BITVECTOR,
 	YOUNGER_SET_BITVECTOR,
 	YOUNGER_SET_CLOSED_BITVECTOR,
 	MAP_BLOCK_AGE,

src/lrumc/MC/lrumc_MCAnalysis.cpp

@@ -36,7 +36,7 @@ public:
 		_nuxmvPath(),
 		_nuxmvWorkspacePath(),
 		_programSlicing(ProgramSlicing::ACCESS_SLICING),
-		_cacheModelKind(CacheModelKind::YOUNGER_SET_BITVECTOR),
+		_cacheModelKind(CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR),
 		_instance(nullptr)
 	{
 	}
@@ -166,7 +166,7 @@ protected:
 			_cacheModelKind,
 			_coll->cache()->wayCount(),
 			programModel.nbBlocks(),
-			programModel.getAccessId(access));
+			programModel.getBlockId(lb));
 
 		if(refreshModel) {
 			std::ostringstream modelPath, dotPath;
@@ -242,7 +242,7 @@ p::declare MCAnalysis::reg = p::init("lrumc::MCAnalysis", Version(1, 0, 0))
  * Feature performing instruction cache analysis with a model checker.
  */
 p::feature MODEL_CHECKING_ANALYSIS_FEATURE("lrumc::MODEL_CHECKING_ANALYSIS_FEATURE", p::make<MCAnalysis>());
-p::id<CacheModelKind> CACHE_MODEL_KIND("lrumc::CACHE_MODEL_KIND", CacheModelKind::YOUNGER_SET_BITVECTOR);
+p::id<CacheModelKind> CACHE_MODEL_KIND("lrumc::CACHE_MODEL_KIND", CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR);
 p::id<ProgramSlicing> PROGRAM_SLICING("lrumc::PROGRAM_SLICING", ProgramSlicing::ACCESS_SLICING);
 
 p::id<elm::String> NUXMV_PATH("lrumc::NUXMV_PATH", "");
@@ -258,6 +258,8 @@ namespace otawa
 			v = lrumc::CacheModelKind::YOUNGER_SET;
 		else if(s == "YOUNGER_SET_BITVECTOR")
 			v = lrumc::CacheModelKind::YOUNGER_SET_BITVECTOR;
+		else if(s == "YOUNGER_SET_BOUNDED_BITVECTOR")
+			v = lrumc::CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR;
 		else if(s == "YOUNGER_SET_CLOSED_BITVECTOR")
 			v = lrumc::CacheModelKind::YOUNGER_SET_CLOSED_BITVECTOR;
 		else if(s == "MAP_BLOCK_AGE")

src/lrumc/MC/lrumc_MCCacheModel.cpp

@@ -19,7 +19,7 @@ MCCacheModel::MCCacheModel(
 
 void MCCacheModel::printSMV(elm::io::Output& output, Check check)
 {
-	if(_kind == CacheModelKind::YOUNGER_SET_BITVECTOR) {
+	if(_kind == CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR) {
 		output << "MODULE cache_set(block)\n";
 
 
@@ -29,7 +29,7 @@ void MCCacheModel::printSMV(elm::io::Output& output, Check check)
 		// Variable age stores the cardinal of the younger set
 		// _ways is a special value used when the tracked block is outside the cache
 		output << "\t\tage : 0.." << _ways << ";\n";
-		// Variable younger_set is the younger_set abstraction. All indexes beyond the value of age are set to FALSE
+		// Variable younger_set is the younger_set abstraction.
 		output << "\t\tblocks_in : array 0.." << _numberOfBlocks - 1 << " of boolean;\n";
 
 
@@ -82,6 +82,90 @@ void MCCacheModel::printSMV(elm::io::Output& output, Check check)
 			output << "\t\t\tesac;\n";
 		}
 	}
+	else if(_kind == CacheModelKind::YOUNGER_SET_BITVECTOR) {
+		output << "MODULE cache_set(block)\n";
+
+		//////// VARIABLE DECLARATION ////////
+		output << "\tVAR\n";
+
+		// The bitvector indicating which blocks are younger than the tracked block
+		output << "\t\tyounger_set : array 0.." << _numberOfBlocks - 1 << " of boolean;\n";
+
+
+		// Helpers definition
+		output << "\tDEFINE\n";
+		// The tracked block
+		output << "\t\ttracked_block := " << _trackedBlock << ";\n";
+		// Boolean indicating that the tracked block is the accessed block
+		output << "\t\thit := (tracked_block = block);\n";
+		// Special boolean used when there is no block accessed
+		output << "\t\tempty_block := (block = -1);\n";
+
+
+		//////// TRANSITION DEFINITION ////////
+		output << "\tASSIGN\n";
+
+		for(int i = 0; i <= _numberOfBlocks - 1; ++i)
+			output << "\t\tinit(younger_set[" << i <<"]) := TRUE;\n";
+
+		// Transition for the younger set
+		for(int i = 0; i <= _numberOfBlocks - 1; ++i) {
+			output << "\t\tnext(younger_set[" << i << "]) :=\n";
+			output << "\t\t\tcase\n";
+			// Does not change if no access is made
+			output << "\t\t\t\tempty_block : younger_set[" << i << "];\n";
+			// Reset younger set on hit
+			output << "\t\t\t\thit : FALSE;\n";
+			// Block is accessed, insert it into the younger set
+			output << "\t\t\t\tblock = " << i << " : TRUE;\n";
+			// Otherwise, keep the old value
+			output << "\t\t\t\tTRUE : younger_set[" << i << "];\n";
+			output << "\t\t\tesac;\n";
+		}
+	}
+	else if(_kind == CacheModelKind::YOUNGER_SET_CLOSED_BITVECTOR) {
+		// elements of the bitvector are allowed to take value FALSE at anytime, because it does not change the hit classification
+		std::string closingTerm = (check == Check::ALWAYS_HIT ? "FALSE" : "TRUE");
+		output << "MODULE cache_set(block)\n";
+
+		//////// VARIABLE DECLARATION ////////
+		output << "\tVAR\n";
+
+		// The bitvector indicating which blocks are younger than the tracked block
+		output << "\t\tyounger_set : array 0.." << _numberOfBlocks - 1 << " of boolean;\n";
+
+
+		// Helpers definition
+		output << "\tDEFINE\n";
+		// The tracked block
+		output << "\t\ttracked_block := " << _trackedBlock << ";\n";
+		// Boolean indicating that the tracked block is the accessed block
+		output << "\t\thit := (tracked_block = block);\n";
+		// Special boolean used when there is no block accessed
+		output << "\t\tempty_block := (block = -1);\n";
+
+
+		//////// TRANSITION DEFINITION ////////
+		output << "\tASSIGN\n";
+
+		for(int i = 0; i <= _numberOfBlocks - 1; ++i)
+			output << "\t\tinit(younger_set[" << i <<"]) := {TRUE, " << closingTerm.c_str() << "};\n";
+
+		// Transition for the younger set
+		for(int i = 0; i <= _numberOfBlocks - 1; ++i) {
+			output << "\t\tnext(younger_set[" << i << "]) :=\n";
+			output << "\t\t\tcase\n";
+			// Does not change if no access is made
+			output << "\t\t\t\tempty_block : {younger_set[" << i << "], " << closingTerm.c_str() << "};\n";
+			// Reset younger set on hit
+			output << "\t\t\t\thit : {FALSE, " << closingTerm.c_str() << "};\n";
+			// Block is accessed, insert it into the younger set
+			output << "\t\t\t\tblock = " << i << " : {TRUE, " << closingTerm.c_str() << "};\n";
+			// Otherwise, keep the old value
+			output << "\t\t\t\tTRUE : {younger_set[" << i << "], " << closingTerm.c_str() << "};\n";
+			output << "\t\t\tesac;\n";
+		}
+	}
 	else if(_kind == CacheModelKind::YOUNGER_SET) {
 		output << "MODULE cache_set(block)\n";
 
@@ -161,7 +245,7 @@ void MCCacheModel::printSMV(elm::io::Output& output, Check check)
 		output << "\tASSIGN\n";
 
 		for(int i = 0; i < _ways; ++i)
-			output << "\t\tinit(lines[" << i << "]) := 0;\n";
+			output << "\t\tinit(lines[" << i << "]) := -1;\n";
 
 		output << "\t\tnext(lines[0]) := (block = -1) ? lines[0] : block;\n";
 		for(int i = 1; i < _ways; ++i) {
@@ -185,9 +269,19 @@ std::string MCCacheModel::in() const
 	switch(_kind)
 	{
 		case CacheModelKind::YOUNGER_SET:
-		case CacheModelKind::YOUNGER_SET_BITVECTOR:
+		case CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR:
 			oss << "cache.age != " << _ways;
 			break;
+		case CacheModelKind::YOUNGER_SET_BITVECTOR:
+		case CacheModelKind::YOUNGER_SET_CLOSED_BITVECTOR:
+			oss << "count(";
+			for(int i = 0; i <= _numberOfBlocks - 1; ++i) {
+				if(i != 0)
+					oss << ", ";
+				oss << "cache.younger_set[" << i << "]";
+			}
+			oss << ") < " << _ways;
+			break;
 		case CacheModelKind::MAP_BLOCK_AGE:
 			oss << "cache.ages[" << _trackedBlock << "] != " << _ways;
 			break;
@@ -207,9 +301,19 @@ std::string MCCacheModel::out() const
 	switch(_kind)
 	{
 		case CacheModelKind::YOUNGER_SET:
-		case CacheModelKind::YOUNGER_SET_BITVECTOR:
+		case CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR:
 			oss << "cache.age = " << _ways;
 			break;
+		case CacheModelKind::YOUNGER_SET_BITVECTOR:
+		case CacheModelKind::YOUNGER_SET_CLOSED_BITVECTOR:
+			oss << "count(";
+			for(int i = 0; i <= _numberOfBlocks - 1; ++i) {
+				if(i != 0)
+					oss << ", ";
+				oss << "cache.younger_set[" << i << "]";
+			}
+			oss << ") >= " << _ways;
+			break;
 		case CacheModelKind::MAP_BLOCK_AGE:
 			oss << "cache.ages[" << _trackedBlock << "] = " << _ways;
 			break;

src/lrumc/MC/lrumc_MCNuxmvCommand.cpp

@@ -104,9 +104,9 @@ void MCCheckInvariantCommand::parseResponse(std::string response)
 	if(firstEndl == std::string::npos)
 		firstEndl = response.length();
 
-	if(response.compare(firstEndl - 7, 7, "is true") == 0)
+	if(firstEndl > 7 && response.compare(firstEndl - 7, 7, "is true") == 0)
 		_hold = true;
-	else if(response.compare(firstEndl - 8, 8, "is false") == 0)
+	else if(firstEndl > 8 && response.compare(firstEndl - 8, 8, "is false") == 0)
 		_hold = false;
 	else {
 		std::string error = "Error when checking invariant \"";

src/lrumc/MC/lrumc_MCQueryManager.cpp

@@ -80,7 +80,9 @@ bool MCQueryManager::refreshNeeded() const
 		return true;
 
 	if(_cacheModelKind == CacheModelKind::YOUNGER_SET ||
-	   _cacheModelKind == CacheModelKind::YOUNGER_SET_BITVECTOR)
+	   _cacheModelKind == CacheModelKind::YOUNGER_SET_BITVECTOR ||
+	   _cacheModelKind == CacheModelKind::YOUNGER_SET_CLOSED_BITVECTOR ||
+	   _cacheModelKind == CacheModelKind::YOUNGER_SET_BOUNDED_BITVECTOR)
 		return true;
 
 	icat3::LBlock* lbCurrent;