Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
db55383
feat: Add simple metrics
YazoonDinalt Aug 8, 2024
c3bc233
feat: Add viewing statistics for individual functions
YazoonDinalt Aug 15, 2024
ecd344e
feat: Add a separate statistics function
YazoonDinalt Aug 27, 2024
f3fb9d3
feat: Add print statistics in delta time
YazoonDinalt Sep 6, 2024
049ab98
feat: Change type Calculate Delta function
YazoonDinalt Sep 6, 2024
11fb1fc
feat: Add output of statistics for each function by time delta
YazoonDinalt Sep 17, 2024
2e7c104
fix: Fix bug with incorrect metrics calculation
YazoonDinalt Sep 17, 2024
67dd22e
feat: Add save metrics on server
YazoonDinalt Oct 9, 2024
d7a9128
feat: Moving network interaction into a separate class
YazoonDinalt Oct 14, 2024
58eb576
feat: Remove check all states
YazoonDinalt Oct 23, 2024
b3b1ec7
feat: Add data queue and remove useless function
YazoonDinalt Nov 6, 2024
0d322b3
feat: Add desription in StatisticQueue
YazoonDinalt Nov 6, 2024
70f42b4
feat: Remove useless function and fix bug with collect metrics
YazoonDinalt Nov 13, 2024
43a7fdd
refactor: Remove useless include
YazoonDinalt Nov 13, 2024
840c2db
feat: Add sending only non-zero metrics and removed unnecessary logging
YazoonDinalt Nov 13, 2024
4cca3fb
feat: Fix wrong calculate in main
YazoonDinalt Nov 13, 2024
318462e
feat: Add SolverTime in metrics
YazoonDinalt Nov 13, 2024
ed63878
feat: Fix main problem with data race and init curl on every function…
YazoonDinalt Nov 21, 2024
d385cb8
feat: Move some data to command line option
YazoonDinalt Nov 21, 2024
81a64f5
feat: Change serialize and rename delta class
YazoonDinalt Nov 21, 2024
a138d62
fix: Add localStatisticMap to executor
YazoonDinalt Nov 21, 2024
b816beb
fix: Data race direct solution method
YazoonDinalt Nov 21, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions include/klee/Support/OptionCategories.h
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ extern llvm::cl::OptionCategory SeedingCat;
extern llvm::cl::OptionCategory SolvingCat;
extern llvm::cl::OptionCategory TerminationCat;
extern llvm::cl::OptionCategory TestGenCat;
extern llvm::cl::OptionCategory AgentCat;
} // namespace klee

#endif /* KLEE_OPTIONCATEGORIES_H */
8 changes: 8 additions & 0 deletions lib/Core/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,17 @@ add_library(kleeCore
ImpliedValue.cpp
Memory.cpp
MemoryManager.cpp
MetricCollectorAndSerializer.cpp
ObjectManager.cpp
PForest.cpp
MockBuilder.cpp
PTree.cpp
Searcher.cpp
SeedInfo.cpp
SeedMap.cpp
ServerConnection.cpp
SpecialFunctionHandler.cpp
StatisticQueue.cpp
StatsTracker.cpp
TargetCalculator.cpp
TargetedExecutionReporter.cpp
Expand All @@ -52,7 +55,12 @@ target_link_libraries(kleeCore PRIVATE
llvm_config(kleeCore "${USE_LLVM_SHARED}" core executionengine mcjit native support)
target_link_libraries(kleeCore PRIVATE ${SQLite3_LIBRARIES})


find_package(CURL REQUIRED)

target_include_directories(kleeCore SYSTEM PRIVATE ${LLVM_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS})
target_include_directories(kleeCore PRIVATE ${KLEE_INCLUDE_DIRS})
target_compile_options(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
target_compile_definitions(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
target_include_directories(kleeCore SYSTEM PRIVATE ${CURL_INCLUDE_DIRS})
target_link_libraries(kleeCore PRIVATE CURL::libcurl)
93 changes: 82 additions & 11 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@

#include "AddressSpace.h"
#include "CXXTypeSystem/CXXTypeManager.h"
#include "CallPathManager.h"
#include "ConstructStorage.h"
#include "CoreStats.h"
#include "DistanceCalculator.h"
Expand All @@ -20,11 +21,14 @@
#include "ImpliedValue.h"
#include "Memory.h"
#include "MemoryManager.h"
#include "MetricCollectorAndSerializer.h"
#include "PForest.h"
#include "PTree.h"
#include "Searcher.h"
#include "SeedInfo.h"
#include "ServerConnection.h"
#include "SpecialFunctionHandler.h"
#include "StatisticQueue.h"
#include "StatsTracker.h"
#include "TargetCalculator.h"
#include "TargetManager.h"
Expand Down Expand Up @@ -72,6 +76,7 @@
#include "klee/Support/RoundingModeUtil.h"
#include "klee/System/MemoryUsage.h"
#include "klee/System/Time.h"
#include <klee/Statistics/Statistics.h>

#include "CodeEvent.h"
#include "CodeLocation.h"
Expand Down Expand Up @@ -100,6 +105,7 @@

#include <algorithm>
#include <cassert>
#include <curl/curl.h>
#include <cxxabi.h>
#include <iosfwd>
#include <iostream>
Expand Down Expand Up @@ -136,6 +142,9 @@ cl::OptionCategory TestGenCat("Test generation options",
cl::OptionCategory LazyInitCat("Lazy initialization option",
"These options configure lazy initialization.");

cl::OptionCategory AgentCat("Agent options",
"These options specify agent settings.");

cl::opt<bool> UseAdvancedTypeSystem(
"use-advanced-type-system",
cl::desc("Use advanced information about type system from "
Expand Down Expand Up @@ -338,6 +347,25 @@ cl::opt<bool> AllExternalWarnings(
"as opposed to once per function (default=false)"),
cl::cat(ExtCallsCat));

/*** Agent options ***/

cl::opt<std::string> UrlUID("url-uid",
cl::init("http://localhost:8080/new-session"),
cl::desc("The option allows to specify the url "
"from which can get the UID"),
cl::cat(AgentCat));

cl::opt<std::string> MetricsUID(
"metrics-uid", cl::init("http://localhost:8080/metrics"),
cl::desc("The option allows to specify the url where can save metrics"),
cl::cat(AgentCat));

cl::opt<bool>
DeltaTime("delta-time", cl::init(100),
cl::desc("Using the option, you specify the time in milliseconds "
"at which statistics will be sent (default = 100)"),
cl::cat(AgentCat));

/*** Seeding options ***/

cl::opt<bool> AlwaysOutputSeeds(
Expand Down Expand Up @@ -489,9 +517,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
InterpreterHandler *ih)
: Interpreter(opts), interpreterHandler(ih), searcher(nullptr),
externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
pathWriter(0), symPathWriter(0),
specialFunctionHandler(0), timers{time::Span(TimerInterval)},
guidanceKind(opts.Guidance), codeGraphInfo(new CodeGraphInfo()),
pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance),
codeGraphInfo(new CodeGraphInfo()),
distanceCalculator(new DistanceCalculator(*codeGraphInfo)),
targetCalculator(new TargetCalculator(*codeGraphInfo)),
targetManager(new TargetManager(guidanceKind, *distanceCalculator,
Expand Down Expand Up @@ -4697,8 +4725,45 @@ void Executor::run(ExecutionState *initialState) {

objectManager->initialUpdate();

MetricCollectorAndSerializer mc;
std::thread consumer;
std::thread producer;
StatisticQueue StatQ;

ServerConnection scForUID(UrlUID);
scForUID.getUIDFromServer();

ServerConnection sc(MetricsUID);
sc.setUID(scForUID.getUID());

std::atomic<bool> shouldStop = false;
if (sc.getUID() != "ServerNotValid") {
consumer = std::thread([&StatQ, &mc, &sc, &shouldStop]() {
while (!shouldStop) {
if (!StatQ.empty()) {
auto data = StatQ.pop();
sc.PostRequest(mc.GetJson(std::move(data), sc.getUID()));
}
}
});
}
auto startTime = std::chrono::high_resolution_clock::now();

// main interpreter loop
while (!haltExecution && !searcher->empty()) {

if (sc.getUID() != "ServerNotValid") {
auto currentTime = std::chrono::high_resolution_clock::now();
auto elapsedTime = std::chrono::duration_cast<std::chrono::milliseconds>(
currentTime - startTime)
.count();
if (elapsedTime >= 100) {
auto localStatisticMap = objectManager->StatisticMap;
StatQ.push(mc.getCurrentMetric(localStatisticMap));
startTime = currentTime;
}
}

auto action = searcher->selectAction();
executeAction(action);
objectManager->updateSubscribers();
Expand All @@ -4707,6 +4772,14 @@ void Executor::run(ExecutionState *initialState) {
objectManager->updateSubscribers();
}
}
auto a = mc.getCurrentMetric(objectManager->StatisticMap);
StatQ.push(a);

shouldStop = true;
if (sc.getUID() != "ServerNotValid") {
consumer.join();
producer.join();
}

if (guidanceKind == GuidanceKind::ErrorGuidance) {
reportProgressTowardsTargets();
Expand Down Expand Up @@ -6829,8 +6902,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
(!AllowSeedTruncation && obj->numBytes > moSize))) {
std::stringstream msg;
msg << "replace size mismatch: " << mo->name << "[" << moSize
<< "]"
<< " vs " << obj->name << "[" << obj->numBytes << "]"
<< "]" << " vs " << obj->name << "[" << obj->numBytes << "]"
<< " in test\n";

terminateStateOnUserError(state, msg.str());
Expand Down Expand Up @@ -7252,8 +7324,7 @@ void Executor::logState(const ExecutionState &state, int id,
object.first->getSizeExpr()->print(*f);
*f << "\n";
}
*f << state.symbolics.size() << " symbolics total. "
<< "Symbolics:\n";
*f << state.symbolics.size() << " symbolics total. " << "Symbolics:\n";
size_t sc = 0;
for (const auto &symbolic : state.symbolics) {
*f << "Symbolic number " << sc++ << "\n";
Expand Down Expand Up @@ -7503,8 +7574,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
std::back_inserter(symbolics), isReproducible);
}

// we cannot be sure that an irreproducible state proves the presence of an
// error
// we cannot be sure that an irreproducible state proves the presence of
// an error
if (uninitObjects.size() > 0 || state.symbolics.size() != symbolics.size()) {
state.error = ReachWithError::None;
} else if (FunctionCallReproduce != "" &&
Expand Down Expand Up @@ -7586,8 +7657,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {

ref<Expr> symcretizedAddress = sizeSymcrete->addressSymcrete.symcretized;

/* Receive address array linked with this size array to request address
* concretization. */
/* Receive address array linked with this size array to request
* address concretization. */
ref<Expr> condcretized = concretizations.at(symcrete->symcretized);

uint64_t newSize = cast<ConstantExpr>(condcretized)->getZExtValue();
Expand Down
1 change: 1 addition & 0 deletions lib/Core/Executor.h
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,7 @@ class MemoryManager;
class MemoryObject;
class ObjectState;
class PForest;
class Delta;
class Searcher;
class SeedInfo;
class SpecialFunctionHandler;
Expand Down
99 changes: 99 additions & 0 deletions lib/Core/MetricCollectorAndSerializer.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
//===--MetricCollectorAndSerializer.cpp---------------------------*-C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#include "MetricCollectorAndSerializer.h"
#include "CoreStats.h"

using namespace klee;

const double NANOSECONDS_PER_SECOND = 1000000000.0;

std::vector<nlohmann::json> MetricCollectorAndSerializer::GetJson(
const std::unordered_map<const llvm::Function *,
std::unordered_map<std::string, int>> &DelMap,
std::string UID) {

std::vector<nlohmann::json> jsonArray = SerializeDelMap(DelMap, UID);

previousMap = jsonArray;

return jsonArray;
}

std::vector<nlohmann::json> MetricCollectorAndSerializer::SerializeDelMap(
const std::unordered_map<const llvm::Function *,
std::unordered_map<std::string, int>> &DelMap,
const std::string UID) {

std::vector<nlohmann::json> jsonArray;

for (const auto &funPair : DelMap) {
auto funName = funPair.first->getName();
const auto &metricsMap = funPair.second;

for (const auto &metricPair : metricsMap) {
const std::string &metricName = metricPair.first;
uint64_t prev;
auto count = metricPair.second;
for (const auto &jsonObject : previousMap) {
if (jsonObject["params"]["funName"] == funName &&
jsonObject["name"] == metricName) {
prev = jsonObject["params"]["value"];
break;
}
}

if (count - prev != 0) {
if (metricName == "SolverTime") {
double solverCount =
static_cast<double>(count) / NANOSECONDS_PER_SECOND;
solverCount = static_cast<double>(round(solverCount * 100)) / 100;
jsonArray.push_back({{"guid", UID},
{"name", metricName},
{"params",
{{"funName", funName},
{"type", "double"},
{"value", solverCount},
{"transitive", false}}}});
} else {
jsonArray.push_back({{"guid", UID},
{"name", metricName},
{"params",
{{"funName", funName},
{"type", "int"},
{"value", count},
{"transitive", false}}}});
}
}
}
}

return jsonArray;
}

std::unordered_map<const llvm::Function *, std::unordered_map<std::string, int>>
MetricCollectorAndSerializer::getCurrentMetric(
std::unordered_map<CallPathNode *, StatisticRecord *> StatMap) {

std::unordered_map<const llvm::Function *,
std::unordered_map<std::string, int>>
DelMap;

std::lock_guard<std::mutex> lock(StatisticMapMutex);
for (const auto &pair : StatMap) {
CallPathNode *cpn = pair.first;
DelMap[cpn->function]["Instructions"] +=
pair.second->getValue(stats::instructions);
DelMap[cpn->function]["SolverTime"] +=
pair.second->getValue(stats::solverTime);
DelMap[cpn->function]["Forks"] += pair.second->getValue(stats::forks);
}

return DelMap;
}
44 changes: 44 additions & 0 deletions lib/Core/MetricCollectorAndSerializer.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
//===--MetricCollectorAndSerializer.h-----------------------------*-C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#ifndef KLEE_GETDELTA_H
#define KLEE_GETDELTA_H

#include "CallPathManager.h"
#include "nlohmann/json.hpp"
#include "llvm/IR/Function.h"

#include <mutex>

namespace klee {

class MetricCollectorAndSerializer {
private:
std::vector<nlohmann::json> previousMap;
std::mutex StatisticMapMutex;
std::unordered_map<const llvm::Function *, std::map<std::string, int>> Delta;

std::vector<nlohmann::json> SerializeDelMap(
const std::unordered_map<const llvm::Function *,
std::unordered_map<std::string, int>> &DelMap,
const std::string UID);

public:
std::vector<nlohmann::json> GetJson(
const std::unordered_map<const llvm::Function *,
std::unordered_map<std::string, int>> &DelMap,
const std::string UID);

std::unordered_map<const llvm::Function *,
std::unordered_map<std::string, int>>
getCurrentMetric(std::unordered_map<CallPathNode *, StatisticRecord *>);
};
} // namespace klee

#endif /* KLEE_DELTA_H */
Loading