Skip to content

Commit 2ced354

Browse files
support write profile file
1 parent c8e629f commit 2ced354

File tree

5 files changed

+160
-24
lines changed

5 files changed

+160
-24
lines changed

benchmarks/pldi2026/btree/compile.py

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ def compile_all(cpp_files=None, flags=None):
4545
cmd = ["g++", str(cpp), "-o", str(out)] + flags
4646
print("Compiling:", cpp.name)
4747
try:
48+
print(" Executing command:")
49+
print(" ", " ".join(cmd))
4850
proc = subprocess.run(cmd, capture_output=True, text=True)
4951
except FileNotFoundError:
5052
print("Error: g++ not found. Install a C++ compiler.")

headers/wasm/concolic_driver.hpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
#include "smt_solver.hpp"
88
#include "symbolic_rt.hpp"
99
#include "utils.hpp"
10+
#include "output_report.hpp"
1011
#include <cassert>
1112
#include <chrono>
1213
#include <functional>
@@ -48,7 +49,7 @@ class ManagedConcolicCleanup {
4849
if (driver.tree_file.has_value())
4950
ExploreTree.dump_graphviz(driver.tree_file.value());
5051

51-
// Clear the symbol bookkeeper
52+
// Clear the symbol bookkeeper
5253
SymBookKeeper.clear();
5354
}
5455
};
@@ -134,8 +135,10 @@ inline void ConcolicDriver::main_exploration_loop() {
134135

135136
inline void ConcolicDriver::run() {
136137
main_exploration_loop();
137-
ExploreTree.print_overall_result();
138+
auto overall = ExploreTree.read_current_overall_result();
139+
overall.print();
138140
Profile.print_summary();
141+
dump_all_summary_json(Profile, overall);
139142
}
140143

141144
static void start_concolic_execution_with(

headers/wasm/output_report.hpp

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
#ifndef WASM_OUTPUT_REPORT_HPP
2+
#define WASM_OUTPUT_REPORT_HPP
3+
4+
#include "profile.hpp"
5+
#include "symbolic_rt.hpp"
6+
#include "config.hpp"
7+
#include <filesystem>
8+
9+
inline void dump_all_summary_json(const Profile_t &profile,
10+
const OverallResult &overall) {
11+
// use environment variable OUTPUT_DIR to config particular output directory
12+
// use environment variable OUTPUT_DIR to config particular output directory
13+
const char *output_dir = std::getenv("OUTPUT_DIR");
14+
if (output_dir == nullptr) {
15+
return;
16+
}
17+
18+
std::filesystem::path outdir(output_dir);
19+
20+
std::filesystem::path report_path =
21+
outdir / std::filesystem::path("concolic_execution_report.json");
22+
23+
auto parent = report_path.parent_path();
24+
if (!parent.empty()) {
25+
std::error_code ec;
26+
std::filesystem::create_directories(parent, ec);
27+
if (ec) {
28+
throw std::runtime_error("Failed to create output directory: " +
29+
ec.message());
30+
}
31+
}
32+
33+
std::ofstream ofs(report_path);
34+
if (!ofs.is_open()) {
35+
throw std::runtime_error("Failed to open " + report_path.string() +
36+
" for writing");
37+
}
38+
39+
// Simple JSON dump (pretty-printed)
40+
ofs << "{\n";
41+
ofs << " \"unexplored_count\": " << overall.unexplored_count << ",\n";
42+
ofs << " \"finished_count\": " << overall.finished_count << ",\n";
43+
ofs << " \"failed_count\": " << overall.failed_count << ",\n";
44+
ofs << " \"not_to_explore_count\": " << overall.not_to_explore_count
45+
<< ",\n";
46+
ofs << " \"unreachable_count\": " << overall.unreachable_count;
47+
if (PROFILE_STEP || PROFILE_TIME) {
48+
ofs << ",\n";
49+
profile.write_as_json(ofs);
50+
}
51+
ofs << "}\n";
52+
ofs.close();
53+
}
54+
#endif // WASM_OUTPUT_REPORT_HPP

headers/wasm/profile.hpp

Lines changed: 59 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,12 +116,70 @@ class Profile_t {
116116
}
117117
}
118118

119+
void write_as_json(std::ostream &os) const {
120+
os << " \"profile_summary\": {\n";
121+
if (PROFILE_STEP) {
122+
os << " \"total_push_operations\": "
123+
<< op_count[static_cast<std::size_t>(StepProfileKind::PUSH)] << ",\n";
124+
os << " \"total_pop_operations\": "
125+
<< op_count[static_cast<std::size_t>(StepProfileKind::POP)] << ",\n";
126+
os << " \"total_peek_operations\": "
127+
<< op_count[static_cast<std::size_t>(StepProfileKind::PEEK)] << ",\n";
128+
os << " \"total_shift_operations\": "
129+
<< op_count[static_cast<std::size_t>(StepProfileKind::SHIFT)] << ",\n";
130+
os << " \"total_set_operations\": "
131+
<< op_count[static_cast<std::size_t>(StepProfileKind::SET)] << ",\n";
132+
os << " \"total_get_operations\": "
133+
<< op_count[static_cast<std::size_t>(StepProfileKind::GET)] << ",\n";
134+
os << " \"total_binary_operations\": "
135+
<< op_count[static_cast<std::size_t>(StepProfileKind::BINARY)]
136+
<< ",\n";
137+
os << " \"total_tree_fill_operations\": "
138+
<< op_count[static_cast<std::size_t>(StepProfileKind::TREE_FILL)]
139+
<< ",\n";
140+
os << " \"total_cursor_move_operations\": "
141+
<< op_count[static_cast<std::size_t>(StepProfileKind::CURSOR_MOVE)]
142+
<< ",\n";
143+
os << " \"total_other_instructions_executed\": " << step_count
144+
<< ",\n";
145+
os << " \"total_mem_grow_operations\": "
146+
<< op_count[static_cast<std::size_t>(StepProfileKind::MEM_GROW)]
147+
<< ",\n";
148+
os << " \"total_snapshot_create_operations\": "
149+
<< op_count[static_cast<std::size_t>(StepProfileKind::SNAPSHOT_CREATE)]
150+
<< ",\n";
151+
os << " \"total_sym_eval_operations\": "
152+
<< op_count[static_cast<std::size_t>(StepProfileKind::SYM_EVAL)]
153+
<< "\n";
154+
}
155+
if (PROFILE_TIME) {
156+
os << " \"total_time_instruction_execution_s\": "
157+
<< std::setprecision(15)
158+
<< time_count[static_cast<std::size_t>(TimeProfileKind::INSTR)]
159+
<< ",\n";
160+
os << " \"total_time_solver_s\": "
161+
<< std::setprecision(15)
162+
<< time_count[static_cast<std::size_t>(TimeProfileKind::SOLVER)]
163+
<< ",\n";
164+
os << " \"total_time_resuming_from_snapshot_s\": "
165+
<< std::setprecision(15)
166+
<< time_count[static_cast<std::size_t>(
167+
TimeProfileKind::RESUME_SNAPSHOT)]
168+
<< ",\n";
169+
os << " \"total_time_counting_symbolic_size_s\": "
170+
<< std::setprecision(15)
171+
<< time_count[static_cast<std::size_t>(
172+
TimeProfileKind::COUNT_SYM_SIZE)]
173+
<< "\n";
174+
}
175+
os << " }\n";
176+
}
177+
119178
// record the time spent in main instruction execution, in seconds
120179
void add_instruction_time(TimeProfileKind kind, double time) {
121180
time_count[static_cast<std::size_t>(kind)] += time;
122181
}
123182

124-
private:
125183
int step_count;
126184
std::array<int, static_cast<std::size_t>(StepProfileKind::OperationCount)>
127185
op_count;

headers/wasm/symbolic_rt.hpp

Lines changed: 40 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
#include <cstddef>
1515
#include <cstdint>
1616
#include <cstdio>
17+
#include <filesystem>
1718
#include <fstream>
1819
#include <iterator>
1920
#include <memory>
@@ -884,6 +885,24 @@ inline int Snapshot_t::cost_of_snapshot() {
884885
return 5.336 *
885886
(cost_of_stack_copy + cost_of_frame_copy + cost_of_memory_copy);
886887
}
888+
889+
struct OverallResult {
890+
int unexplored_count = 0;
891+
int finished_count = 0;
892+
int failed_count = 0;
893+
int not_to_explore_count = 0;
894+
int unreachable_count = 0;
895+
896+
void print() {
897+
std::cout << "Explore Tree Overall Result:" << std::endl;
898+
std::cout << " Unexplored paths: " << unexplored_count << std::endl;
899+
std::cout << " Finished paths: " << finished_count << std::endl;
900+
std::cout << " Failed paths: " << failed_count << std::endl;
901+
std::cout << " Unreachable paths: " << unreachable_count << std::endl;
902+
std::cout << " NotToExplore paths: " << not_to_explore_count << std::endl;
903+
}
904+
};
905+
887906
class ExploreTree_t {
888907
public:
889908
explicit ExploreTree_t()
@@ -1009,6 +1028,16 @@ class ExploreTree_t {
10091028
}
10101029

10111030
std::monostate dump_graphviz(std::string filepath) {
1031+
std::filesystem::path out_path(filepath);
1032+
auto parent = out_path.parent_path();
1033+
if (!parent.empty()) {
1034+
std::error_code ec;
1035+
std::filesystem::create_directories(parent, ec);
1036+
if (ec) {
1037+
throw std::runtime_error("Failed to create output directory: " +
1038+
ec.message());
1039+
}
1040+
}
10121041
std::ofstream ofs(filepath);
10131042
if (!ofs.is_open()) {
10141043
throw std::runtime_error("Failed to open " + filepath + " for writing");
@@ -1017,45 +1046,35 @@ class ExploreTree_t {
10171046
return std::monostate();
10181047
}
10191048

1020-
std::monostate print_overall_result() {
1021-
// Print how many paths have been explored, how many paths are unreachable,
1022-
// how many paths are failed, how many paths are finished successfully
1023-
int unexplored_count = 0;
1024-
int finished_count = 0;
1025-
int failed_count = 0;
1026-
int not_to_explore_count = 0;
1027-
int unreachable_count = 0;
1049+
OverallResult read_current_overall_result() {
1050+
OverallResult result;
10281051
std::function<void(NodeBox *)> dfs = [&](NodeBox *node) {
10291052
if (auto if_else_node = dynamic_cast<IfElseNode *>(node->node.get())) {
10301053
dfs(if_else_node->true_branch.get());
10311054
dfs(if_else_node->false_branch.get());
10321055
} else if (dynamic_cast<UnExploredNode *>(node->node.get())) {
1033-
unexplored_count += 1;
1056+
result.unexplored_count += 1;
10341057
} else if (dynamic_cast<Finished *>(node->node.get())) {
1035-
finished_count += 1;
1058+
result.finished_count += 1;
10361059
} else if (dynamic_cast<Failed *>(node->node.get())) {
1037-
failed_count += 1;
1060+
result.failed_count += 1;
10381061
} else if (dynamic_cast<Unreachable *>(node->node.get())) {
1039-
unreachable_count += 1;
1062+
result.unreachable_count += 1;
10401063
} else if (dynamic_cast<SnapshotNode *>(node->node.get())) {
10411064
// Snapshot node is considered unexplored
1042-
unexplored_count += 1;
1065+
result.unexplored_count += 1;
10431066
} else if (dynamic_cast<NotToExploreNode *>(node->node.get())) {
1044-
not_to_explore_count += 1;
1067+
result.not_to_explore_count += 1;
10451068
} else {
10461069
throw std::runtime_error("Unknown node type in explore tree");
10471070
}
10481071
};
10491072
dfs(root.get());
1050-
std::cout << "Explore Tree Overall Result:" << std::endl;
1051-
std::cout << " Unexplored paths: " << unexplored_count << std::endl;
1052-
std::cout << " Finished paths: " << finished_count << std::endl;
1053-
std::cout << " Failed paths: " << failed_count << std::endl;
1054-
std::cout << " Unreachable paths: " << unreachable_count << std::endl;
1055-
std::cout << " NotToExplore paths: " << not_to_explore_count << std::endl;
1056-
return std::monostate();
1073+
return result;
10571074
}
10581075

1076+
std::monostate print_overall_result() {}
1077+
10591078
NodeBox *pick_unexplored() {
10601079
// Pick an unexplored node from the tree
10611080
// For now, we just iterate through the tree and return the first unexplored

0 commit comments

Comments
 (0)