Skip to content

Commit

Permalink
Making proof_trace_parser and llvm_rewrite_trace_iterator use a s…
Browse files Browse the repository at this point in the history
…hared_ptr of `kore_header`
  • Loading branch information
Robertorosmaninho committed Oct 11, 2024
1 parent db7ebd0 commit 4dc3cb2
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 12 deletions.
7 changes: 4 additions & 3 deletions bindings/python/ast.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -459,7 +459,7 @@ void bind_proof_trace(py::module_ &m) {
.def_property_readonly("trace", &llvm_rewrite_trace::get_trace)
.def_static(
"parse",
[](py::bytes const &bytes, kore_header const &header) {
[](py::bytes const &bytes, std::shared_ptr<kore_header> &header) {
proof_trace_parser parser(false, false, header);
auto str = std::string(bytes);
return parser.parse_proof_trace(str, false);
Expand All @@ -486,10 +486,11 @@ void bind_proof_trace(py::module_ &m) {
.def("__repr__", print_repr_adapter<llvm_rewrite_trace_iterator>(true))
.def_static(
"from_file",
[](std::string const &filename, kore_header const &header) {
[](std::string const &filename,
std::shared_ptr<kore_header> const &header) {
std::ifstream file(filename, std::ios_base::binary);
return llvm_rewrite_trace_iterator(
std::make_unique<proof_trace_file_buffer>(std::move(file)),
std::make_shared<proof_trace_file_buffer>(std::move(file)),
header);
},
py::arg("filename"), py::arg("header"))
Expand Down
8 changes: 4 additions & 4 deletions include/kllvm/binary/ProofTraceParser.h
Original file line number Diff line number Diff line change
Expand Up @@ -328,7 +328,7 @@ class proof_trace_parser {
private:
bool verbose_;
bool expand_terms_;
[[maybe_unused]] kore_header const &header_;
[[maybe_unused]] std::shared_ptr<kore_header> header_;
[[maybe_unused]] std::optional<kore_definition> kore_definition_
= std::nullopt;

Expand All @@ -342,7 +342,7 @@ class proof_trace_parser {
|| magic[3] != '2') {
return nullptr;
}
auto result = detail::read_v2(buffer, header_, pattern_len);
auto result = detail::read_v2(buffer, *header_, pattern_len);
pattern_len += 4;
return result;
}
Expand Down Expand Up @@ -701,7 +701,7 @@ class proof_trace_parser {

public:
proof_trace_parser(
bool verbose, bool expand_terms, kore_header const &header,
bool verbose, bool expand_terms, std::shared_ptr<kore_header> header,
std::optional<kore_definition> kore_definition = std::nullopt);

std::optional<llvm_rewrite_trace> parse_proof_trace_from_file(
Expand All @@ -723,7 +723,7 @@ class llvm_rewrite_trace_iterator {

public:
llvm_rewrite_trace_iterator(
std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header);
std::unique_ptr<proof_trace_buffer> buffer, std::shared_ptr<kore_header> header);
[[nodiscard]] uint32_t get_version() const { return version_; }
std::optional<annotated_llvm_event> get_next_event();
void print(
Expand Down
9 changes: 5 additions & 4 deletions lib/binary/ProofTraceParser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -130,9 +130,10 @@ void llvm_event::print(
}

llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator(
std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header)
std::unique_ptr<proof_trace_buffer> buffer,
std::shared_ptr<kore_header> header)
: buffer_(std::move(buffer))
, parser_(false, false, header) {
, parser_(false, false, std::move(header)) {
if (!proof_trace_parser::parse_header(*buffer_, kind_, version_)) {
throw std::runtime_error("invalid header");
}
Expand Down Expand Up @@ -250,11 +251,11 @@ void llvm_rewrite_trace::print(
}

proof_trace_parser::proof_trace_parser(
bool verbose, bool expand_terms, kore_header const &header,
bool verbose, bool expand_terms, std::shared_ptr<kore_header> header,
std::optional<kore_definition> kore_definition)
: verbose_(verbose)
, expand_terms_(expand_terms)
, header_(header)
, header_(std::move(header))
, kore_definition_(std::move(kore_definition)) { }

std::optional<llvm_rewrite_trace> proof_trace_parser::parse_proof_trace(
Expand Down
2 changes: 1 addition & 1 deletion tools/kore-proof-trace/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ int main(int argc, char **argv) {
cl::ParseCommandLineOptions(argc, argv);

FILE *in = fopen(header_path.getValue().c_str(), "r");
kore_header header(in);
auto header = std::make_shared<kore_header>(in);
fclose(in);

if (use_streaming_parser) {
Expand Down

0 comments on commit 4dc3cb2

Please sign in to comment.