@@ -181,8 +181,7 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) {
181181 return weight;
182182 }
183183 auto distRes = distanceCalculator.getDistance (*es, target->getBlock ());
184- weight = klee::util::ulog2 (distRes.weight + es->steppedMemoryInstructions +
185- 1 ); // [0, 32)
184+ weight = klee::util::ulog2 (distRes.weight + 1 ); // [0, 32)
186185 if (!distRes.isInsideFunction ) {
187186 weight += 32 ; // [32, 64)
188187 }
@@ -193,12 +192,12 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) {
193192
194193ExecutionState &GuidedSearcher::selectState () {
195194 unsigned size = historiesAndTargets.size ();
196- index = theRNG. getInt32 () % (size + 1 ) ;
195+ interleave ^= 1 ;
197196 ExecutionState *state = nullptr ;
198- if (index == size) {
197+ if (interleave || ! size) {
199198 state = &baseSearcher->selectState ();
200199 } else {
201- index = index % size;
200+ index = theRNG. getInt32 () % size;
202201 auto &historyTargetPair = historiesAndTargets[index];
203202 ref<const TargetsHistory> history = historyTargetPair.first ;
204203 ref<Target> target = historyTargetPair.second ;
@@ -763,3 +762,124 @@ void InterleavedSearcher::printName(llvm::raw_ostream &os) {
763762 searcher->printName (os);
764763 os << " </InterleavedSearcher>\n " ;
765764}
765+
766+ // /
767+
768+ BlockLevelSearcher::BlockLevelSearcher (RNG &rng) : theRNG{rng} {}
769+
770+ ExecutionState &BlockLevelSearcher::selectState () {
771+ unsigned rnd = 0 ;
772+ unsigned index = 0 ;
773+ unsigned mod = 10 ;
774+ unsigned border = 9 ;
775+
776+ auto kfi = data.begin ();
777+ index = theRNG.getInt32 () % data.size ();
778+ std::advance (kfi, index);
779+ auto &sizesTo = kfi->second ;
780+
781+ for (auto &sizesSize : sizesTo) {
782+ rnd = theRNG.getInt32 ();
783+ if (rnd % mod < border) {
784+ for (auto &size : sizesSize.second ) {
785+ rnd = theRNG.getInt32 ();
786+ if (rnd % mod < border) {
787+ auto lbi = size.second .begin ();
788+ index = theRNG.getInt32 () % size.second .size ();
789+ std::advance (lbi, index);
790+ auto &level = *lbi;
791+ auto si = level.second .begin ();
792+ index = theRNG.getInt32 () % level.second .size ();
793+ std::advance (si, index);
794+ auto &state = *si;
795+ return *state;
796+ }
797+ }
798+ }
799+ }
800+
801+ return **(sizesTo.begin ()->second .begin ()->second .begin ()->second .begin ());
802+ }
803+
804+ void BlockLevelSearcher::clear (ExecutionState &state) {
805+ KFunction *kf = state.initPC ->parent ->parent ;
806+ BlockLevel &bl = stateToBlockLevel[&state];
807+ auto &sizeTo = data[kf];
808+ auto &sizesTo = sizeTo[bl.sizeOfLevel ];
809+ auto &levelTo = sizesTo[bl.sizesOfFrameLevels ];
810+ auto &states = levelTo[bl.maxMultilevel ];
811+
812+ states.erase (&state);
813+ if (states.size () == 0 ) {
814+ levelTo.erase (bl.maxMultilevel );
815+ }
816+ if (levelTo.size () == 0 ) {
817+ sizesTo.erase (bl.sizesOfFrameLevels );
818+ }
819+ if (sizesTo.size () == 0 ) {
820+ sizeTo.erase (bl.sizeOfLevel );
821+ }
822+ if (sizeTo.size () == 0 ) {
823+ data.erase (kf);
824+ }
825+ }
826+
827+ void BlockLevelSearcher::update (ExecutionState *current,
828+ const StateIterable &addedStates,
829+ const StateIterable &removedStates) {
830+ if (current && std::find (removedStates.begin (), removedStates.end (),
831+ current) == removedStates.end ()) {
832+ KFunction *kf = current->initPC ->parent ->parent ;
833+ BlockLevel &bl = stateToBlockLevel[current];
834+ sizes.clear ();
835+ unsigned long long maxMultilevel = 0u ;
836+ for (auto &infoFrame : current->stack .infoStack ()) {
837+ sizes.push_back (infoFrame.level .size ());
838+ maxMultilevel = std::max (maxMultilevel, infoFrame.maxMultilevel );
839+ }
840+ for (auto &kfLevel : current->stack .multilevel ) {
841+ maxMultilevel = std::max (maxMultilevel, kfLevel.second );
842+ }
843+ if (sizes != bl.sizesOfFrameLevels ||
844+ current->level .size () != bl.sizeOfLevel ||
845+ maxMultilevel != bl.maxMultilevel ) {
846+ clear (*current);
847+
848+ data[kf][current->level .size ()][sizes][maxMultilevel].insert (current);
849+
850+ stateToBlockLevel[current] =
851+ BlockLevel (kf, current->level .size (), sizes, maxMultilevel);
852+ }
853+ }
854+
855+ for (const auto state : addedStates) {
856+ KFunction *kf = state->initPC ->parent ->parent ;
857+
858+ sizes.clear ();
859+ unsigned long long maxMultilevel = 0u ;
860+ for (auto &infoFrame : state->stack .infoStack ()) {
861+ sizes.push_back (infoFrame.level .size ());
862+ maxMultilevel = std::max (maxMultilevel, infoFrame.maxMultilevel );
863+ }
864+ for (auto &kfLevel : state->stack .multilevel ) {
865+ maxMultilevel = std::max (maxMultilevel, kfLevel.second );
866+ }
867+
868+ data[kf][state->level .size ()][sizes][maxMultilevel].insert (state);
869+
870+ stateToBlockLevel[state] =
871+ BlockLevel (kf, state->level .size (), sizes, maxMultilevel);
872+ }
873+
874+ // remove states
875+ for (const auto state : removedStates) {
876+ clear (*state);
877+ stateToBlockLevel.erase (state);
878+ }
879+ }
880+
881+ bool BlockLevelSearcher::empty () { return stateToBlockLevel.empty (); }
882+
883+ void BlockLevelSearcher::printName (llvm::raw_ostream &os) {
884+ os << " BlockLevelSearcher\n " ;
885+ }
0 commit comments