@@ -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 ;
@@ -657,7 +656,7 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric {
657656    return  state.isCycled (maxCycles);
658657  }
659658  void  increaseLimit () final  {
660-     maxCycles *= 2ULL ;
659+     maxCycles *= 4ULL ;
661660    klee_message (" increased max-cycles to %llu" 
662661  }
663662};
@@ -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