cloud9_root/src/cloud9/lib/Core/CacheSideChannel.cpp
// process constraints for cold cache misses
process constraints for cold cache misses
process constraints for cold cache misses
void CacheChannel::processColdMissCnstr(ExecutionState& state, TimingSolver* solver) {
	std::map<int, bool> coldMissMap;
	for (addrT::iterator II = state.memAddrs.begin(); II != state.memAddrs.end(); II++) {
		ref<Expr> address = *II;
		if (address->getKind() == Expr::Constant) {
			ConstantExpr* CE = dyn_cast < ConstantExpr > (address);
			uint64_t addrRaw = CE->getZExtValue();
			int set = CACHE_SET(addrRaw, nset, line);
			if (!coldMissMap.count(set)) {
				coldMissMap[set] = true;
				fixedColdMisses++;
			}
		}
	}
	std::vector<int> remainingSets;
	for (int II = 0; II < nset; II++) {
		if (!coldMissMap.count(II)) remainingSets.push_back(II);
	}
	if (remainingSets.empty()) return;
	std::vector<ref<Expr> > SymSetAddr;
	for (addrT::iterator II = state.memAddrs.begin(); II != state.memAddrs.end(); II++) {
		ref<Expr> address = *II;
		if (address->getKind() == Expr::Constant) continue;
		ref<Expr> blAddr = LShrExpr::create(address, ConstantExpr::alloc(log_base2(line), address->getWidth()));
		ref<Expr> setAddr = AndExpr::create(blAddr, ConstantExpr::alloc(nset - 1, address->getWidth()));
		SymSetAddr.push_back(setAddr);
	}
	if (SymSetAddr.empty()) return;
	ref<Expr> setCheckExpr = NULL;
	for (std::vector<int>::iterator II = remainingSets.begin(); II != remainingSets.end(); II++) {
		int set = *II;
		std::string missStr("cold");
		for (std::vector<ref<Expr> >::iterator IIR = SymSetAddr.begin(); IIR != SymSetAddr.end(); IIR++) {
			ref<Expr> setExpr = *IIR;
			ref<Expr> EqExpr = EqExpr::create(setExpr, ConstantExpr::alloc(set, setExpr->getWidth()));
			bool mustBeFalse = true;
			solver->mustBeFalse(data::SIDE_CHANNEL_ANALYSIS, state, EqExpr, mustBeFalse);
			if (mustBeFalse) {
				continue;
			}
			if (setCheckExpr.isNull()) setCheckExpr = EqExpr;
			else {
				setCheckExpr = OrExpr::create(setCheckExpr, EqExpr);
			}
			atomicCnstr++;
		}
		if (setCheckExpr.isNull()) continue;
		std::ostringstream ss;
		ss << set;
		missStr += ss.str();
		const Array* array = Array::CreateArray(missStr.c_str(), 1);
		ref<Expr> read = Expr::createTempRead(array, 8);
		symCacheMissLog.push_back(read);
		missVars.push_back(array);
		ref<Expr> missEff = EqExpr::create(read, ConstantExpr::alloc(1, read->getWidth()));
		ref<Expr> hitEff = EqExpr::create(read, ConstantExpr::alloc(0, read->getWidth()));
		ref<Expr> notSetCheckExpr = NotExpr::create(setCheckExpr);
		ref<Expr> coldMissCnstr = Expr::createImplies(setCheckExpr, missEff);
		ref<Expr> notColdMissCnstr = Expr::createImplies(notSetCheckExpr, hitEff);
		allConstraintLog.push_back(coldMissCnstr);
		allConstraintLog.push_back(notColdMissCnstr);
	}
}
void CacheChannel :: processColdMissCnstr ( ExecutionState & state , TimingSolver * solver ) { std :: map < int , bool > coldMissMap ; for ( addrT :: iterator II = state . memAddrs . begin ( ) ; II != state . memAddrs . end ( ) ; II ++ ) { ref < Expr > address = * II ; if ( address -> getKind ( ) == Expr :: Constant ) { ConstantExpr * CE = dyn_cast < ConstantExpr > ( address ) ; uint64_t addrRaw = CE -> getZExtValue ( ) ; int set = CACHE_SET ( addrRaw , nset , line ) ; if ( ! coldMissMap . count ( set ) ) { coldMissMap [ set ] = true ; fixedColdMisses ++ ; } } } std :: vector < int > remainingSets ; for ( int II = 0 ; II < nset ; II ++ ) { if ( ! coldMissMap . count ( II ) ) remainingSets . push_back ( II ) ; } if ( remainingSets . empty ( ) ) return ; std :: vector < ref < Expr > > SymSetAddr ; for ( addrT :: iterator II = state . memAddrs . begin ( ) ; II != state . memAddrs . end ( ) ; II ++ ) { ref < Expr > address = * II ; if ( address -> getKind ( ) == Expr :: Constant ) continue ; ref < Expr > blAddr = LShrExpr :: create ( address , ConstantExpr :: alloc ( log_base2 ( line ) , address -> getWidth ( ) ) ) ; ref < Expr > setAddr = AndExpr :: create ( blAddr , ConstantExpr :: alloc ( nset - 1 , address -> getWidth ( ) ) ) ; SymSetAddr . push_back ( setAddr ) ; } if ( SymSetAddr . empty ( ) ) return ; ref < Expr > setCheckExpr = NULL ; for ( std :: vector < int > :: iterator II = remainingSets . begin ( ) ; II != remainingSets . end ( ) ; II ++ ) { int set = * II ; std :: string missStr ( " " ) ; for ( std :: vector < ref < Expr > > :: iterator IIR = SymSetAddr . begin ( ) ; IIR != SymSetAddr . end ( ) ; IIR ++ ) { ref < Expr > setExpr = * IIR ; ref < Expr > EqExpr = EqExpr :: create ( setExpr , ConstantExpr :: alloc ( set , setExpr -> getWidth ( ) ) ) ; bool mustBeFalse = true ; solver -> mustBeFalse ( data :: SIDE_CHANNEL_ANALYSIS , state , EqExpr , mustBeFalse ) ; if ( mustBeFalse ) { continue ; } if ( setCheckExpr . isNull ( ) ) setCheckExpr = EqExpr ; else { setCheckExpr = OrExpr :: create ( setCheckExpr , EqExpr ) ; } atomicCnstr ++ ; } if ( setCheckExpr . isNull ( ) ) continue ; std :: ostringstream ss ; ss << set ; missStr += ss . str ( ) ; const Array * array = Array :: CreateArray ( missStr . c_str ( ) , 1 ) ; ref < Expr > read = Expr :: createTempRead ( array , 8 ) ; symCacheMissLog . push_back ( read ) ; missVars . push_back ( array ) ; ref < Expr > missEff = EqExpr :: create ( read , ConstantExpr :: alloc ( 1 , read -> getWidth ( ) ) ) ; ref < Expr > hitEff = EqExpr :: create ( read , ConstantExpr :: alloc ( 0 , read -> getWidth ( ) ) ) ; ref < Expr > notSetCheckExpr = NotExpr :: create ( setCheckExpr ) ; ref < Expr > coldMissCnstr = Expr :: createImplies ( setCheckExpr , missEff ) ; ref < Expr > notColdMissCnstr = Expr :: createImplies ( notSetCheckExpr , hitEff ) ; allConstraintLog . push_back ( coldMissCnstr ) ; allConstraintLog . push_back ( notColdMissCnstr ) ; } }
process constraints for cold cache misses
process constraints for cold cache misses
/* In the first pass, only handle the constant expressions */ /* address is a constant expression */ /* get the address as a raw 64-bit integer */ /* compute cold miss for this set */ /* optimization: check cold misses in the symbolic expression only for
	 those cache sets that are not touched by constant expressions */ /* no constaint is generated if all cache lines are touched by constant
	 * address expressions */ /* In the second pass, handle the rest of the expressions (i.e. symbolic) */ /* if there does not exist any symbolic address, we are done here */ /* now process the sequence of symbolic addresses set-by-set */ /* symbolic variable, placeholders for cold cache misses */ /* skip if none of the symbolic addresses could be mapped to cache-set "set" */ /* at this moment setCheckExpr contains ((set(s1) = s) \/ (set(s2) = s) \/ .... \/ (set(sn) = s)) */ /* create hit and miss effects depending on the conflicts */ /* add newly generate symbolic cache miss variable to the symbolic variable log */ /* Now join the premise and conclusion: (setCheckExpr)=>(hit/miss) */ /* cold miss constraint */ /* not cold miss constraints */ /* <Cache_Constraint_System>: add these constraints in the constraint log */ /* sudiptac: make sure to add the tag <Cache_Constraint_System> when adding constraints
		 * to allConstraintLog */ /* sudiptac: work with the cold-miss constraint generation is done here */