diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-12-19 15:23:37 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-01-19 19:11:33 +0000 |
commit | d9888fcefc216b16404a39ac7b82a8fd8d5f343f (patch) | |
tree | 631796f0078320551c478ea29b24cc13811e9573 | |
parent | 4300ed7cd1ec48292a1983bb80161099f15b2023 (diff) | |
download | klee-d9888fcefc216b16404a39ac7b82a8fd8d5f343f.tar.gz |
Remove statistics limit from istats.
Statistics encoded in `run.istats` were limited to a maximum number of 13 due to encoding in a `uint64_t` variable. This approach has multiple limitations: - a maximum number of 13 statistics were allowed - a subtle bug can be triggered if many more statistics are added - independent of the selected statistics for `run.istats` Depending on the linking order, statistics will get a different ID. Previously, the ID was used to shift a `1` to its position marking the statistic as being used. This will lead to undefined behaviour if more than 63 statistics are used. Using an llvm::SmallBitVector instead fixes both problems.
-rw-r--r-- | lib/Core/StatsTracker.cpp | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index d445eb2a..76ed9e08 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -26,19 +26,20 @@ #include "MemoryManager.h" #include "UserSearcher.h" +#include "llvm/ADT/SmallBitVector.h" #include "llvm/IR/BasicBlock.h" -#include "llvm/IR/CallSite.h" #include "llvm/IR/CFG.h" +#include "llvm/IR/CallSite.h" #include "llvm/IR/Function.h" +#include "llvm/IR/InlineAsm.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/IntrinsicInst.h" -#include "llvm/IR/InlineAsm.h" #include "llvm/IR/Module.h" #include "llvm/IR/Type.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Process.h" -#include "llvm/Support/Path.h" #include "llvm/Support/FileSystem.h" +#include "llvm/Support/Path.h" +#include "llvm/Support/Process.h" #include <fstream> #include <unistd.h> @@ -579,7 +580,6 @@ void StatsTracker::updateStateStatistics(uint64_t addend) { void StatsTracker::writeIStats() { const auto m = executor.kmodule->module.get(); - uint64_t istatsMask = 0; llvm::raw_fd_ostream &of = *istatsFile; // We assume that we didn't move the file pointer @@ -595,26 +595,26 @@ void StatsTracker::writeIStats() { StatisticManager &sm = *theStatisticManager; unsigned nStats = sm.getNumStatistics(); - - // Max is 13, sadly - istatsMask |= 1<<sm.getStatisticID("Queries"); - istatsMask |= 1<<sm.getStatisticID("QueriesValid"); - istatsMask |= 1<<sm.getStatisticID("QueriesInvalid"); - istatsMask |= 1<<sm.getStatisticID("QueryTime"); - istatsMask |= 1<<sm.getStatisticID("ResolveTime"); - istatsMask |= 1<<sm.getStatisticID("Instructions"); - istatsMask |= 1<<sm.getStatisticID("InstructionTimes"); - istatsMask |= 1<<sm.getStatisticID("InstructionRealTimes"); - istatsMask |= 1<<sm.getStatisticID("Forks"); - istatsMask |= 1<<sm.getStatisticID("CoveredInstructions"); - istatsMask |= 1<<sm.getStatisticID("UncoveredInstructions"); - istatsMask |= 1<<sm.getStatisticID("States"); - istatsMask |= 1<<sm.getStatisticID("MinDistToUncovered"); + llvm::SmallBitVector istatsMask(nStats); + + istatsMask.set(sm.getStatisticID("Queries")); + istatsMask.set(sm.getStatisticID("QueriesValid")); + istatsMask.set(sm.getStatisticID("QueriesInvalid")); + istatsMask.set(sm.getStatisticID("QueryTime")); + istatsMask.set(sm.getStatisticID("ResolveTime")); + istatsMask.set(sm.getStatisticID("Instructions")); + istatsMask.set(sm.getStatisticID("InstructionTimes")); + istatsMask.set(sm.getStatisticID("InstructionRealTimes")); + istatsMask.set(sm.getStatisticID("Forks")); + istatsMask.set(sm.getStatisticID("CoveredInstructions")); + istatsMask.set(sm.getStatisticID("UncoveredInstructions")); + istatsMask.set(sm.getStatisticID("States")); + istatsMask.set(sm.getStatisticID("MinDistToUncovered")); of << "positions: instr line\n"; for (unsigned i=0; i<nStats; i++) { - if (istatsMask & (1<<i)) { + if (istatsMask.test(i)) { Statistic &s = sm.getStatistic(i); of << "event: " << s.getShortName() << " : " << s.getName() << "\n"; @@ -623,14 +623,14 @@ void StatsTracker::writeIStats() { of << "events: "; for (unsigned i=0; i<nStats; i++) { - if (istatsMask & (1<<i)) + if (istatsMask.test(i)) of << sm.getStatistic(i).getShortName() << " "; } of << "\n"; // set state counts, decremented after we process so that we don't // have to zero all records each time. - if (istatsMask & (1<<stats::states.getID())) + if (istatsMask.test(stats::states.getID())) updateStateStatistics(1); std::string sourceFile = ""; @@ -669,7 +669,7 @@ void StatsTracker::writeIStats() { of << ii.assemblyLine << " "; of << ii.line << " "; for (unsigned i=0; i<nStats; i++) - if (istatsMask&(1<<i)) + if (istatsMask.test(i)) of << sm.getIndexedValue(sm.getStatistic(i), index) << " "; of << "\n"; @@ -694,7 +694,7 @@ void StatsTracker::writeIStats() { of << ii.assemblyLine << " "; of << ii.line << " "; for (unsigned i=0; i<nStats; i++) { - if (istatsMask&(1<<i)) { + if (istatsMask.test(i)) { Statistic &s = sm.getStatistic(i); uint64_t value; @@ -718,7 +718,7 @@ void StatsTracker::writeIStats() { } } - if (istatsMask & (1<<stats::states.getID())) + if (istatsMask.test(stats::states.getID())) updateStateStatistics((uint64_t)-1); // Clear then end of the file if necessary (no truncate op?). |