Skip to content

Commit f55a357

Browse files
committed
Merge remote-tracking branch 'origin/develop'
2 parents a77c3ec + 56b1689 commit f55a357

File tree

13 files changed

+623
-0
lines changed

13 files changed

+623
-0
lines changed

include/kllvm/binary/ProofTraceParser.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -698,6 +698,8 @@ class proof_trace_parser {
698698

699699
std::optional<llvm_rewrite_trace>
700700
parse_proof_trace_from_file(std::string const &filename);
701+
std::optional<llvm_rewrite_trace> parse_proof_trace_from_shmem(
702+
void *shm_object, sem_t *data_avail, sem_t *space_avail);
701703
std::optional<llvm_rewrite_trace> parse_proof_trace(std::string const &data);
702704

703705
friend class llvm_rewrite_trace_iterator;

include/kllvm/binary/deserializer.h

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,14 @@
22
#define AST_DESERIALIZER_H
33

44
#include <kllvm/ast/AST.h>
5+
#include <kllvm/binary/ringbuffer.h>
56
#include <kllvm/binary/serializer.h>
67
#include <kllvm/binary/version.h>
78

89
#include <cstddef>
910
#include <cstdio>
1011
#include <cstring>
12+
#include <deque>
1113
#include <fstream>
1214
#include <iostream>
1315
#include <vector>
@@ -203,6 +205,155 @@ class proof_trace_file_buffer : public proof_trace_buffer {
203205
}
204206
};
205207

208+
class proof_trace_ringbuffer : public proof_trace_buffer {
209+
private:
210+
shm_ringbuffer *shm_buffer_;
211+
sem_t *data_avail_;
212+
sem_t *space_avail_;
213+
std::deque<uint8_t> peek_data_;
214+
bool peek_eof_{false};
215+
bool read_eof_{false};
216+
217+
bool read(uint8_t *ptr, size_t len = 1) {
218+
for (size_t i = 0; i < len; i++) {
219+
if (!peek_data_.empty()) {
220+
ptr[i] = peek_data_.front();
221+
peek_data_.pop_front();
222+
continue;
223+
}
224+
225+
if (peek_eof_) {
226+
read_eof_ = true;
227+
return false;
228+
}
229+
230+
if (read_eof_) {
231+
return false;
232+
}
233+
234+
while (int wait_status = sem_trywait(data_avail_)) {
235+
assert(wait_status == -1 && errno == EAGAIN);
236+
if (shm_buffer_->eof()) {
237+
read_eof_ = true;
238+
return false;
239+
}
240+
}
241+
shm_buffer_->get(&ptr[i]);
242+
sem_post(space_avail_);
243+
}
244+
245+
return true;
246+
}
247+
248+
bool peek(uint8_t *ptr, size_t len = 1) {
249+
for (size_t i = 0; i < len; i++) {
250+
if (i < peek_data_.size()) {
251+
ptr[i] = peek_data_[i];
252+
continue;
253+
}
254+
255+
if (peek_eof_) {
256+
return false;
257+
}
258+
259+
if (read_eof_) {
260+
return false;
261+
}
262+
263+
while (int wait_status = sem_trywait(data_avail_)) {
264+
assert(wait_status == -1 && errno == EAGAIN);
265+
if (shm_buffer_->eof()) {
266+
peek_eof_ = true;
267+
return false;
268+
}
269+
}
270+
shm_buffer_->get(&ptr[i]);
271+
sem_post(space_avail_);
272+
peek_data_.push_back(ptr[i]);
273+
}
274+
275+
return true;
276+
}
277+
278+
public:
279+
proof_trace_ringbuffer(
280+
void *shm_object, sem_t *data_avail, sem_t *space_avail)
281+
: shm_buffer_(static_cast<shm_ringbuffer *>(shm_object))
282+
, data_avail_(data_avail)
283+
, space_avail_(space_avail) {
284+
new (shm_buffer_) shm_ringbuffer;
285+
}
286+
287+
~proof_trace_ringbuffer() override { shm_buffer_->~shm_ringbuffer(); }
288+
289+
proof_trace_ringbuffer(proof_trace_ringbuffer const &) = delete;
290+
proof_trace_ringbuffer(proof_trace_ringbuffer &&) = delete;
291+
proof_trace_ringbuffer &operator=(proof_trace_ringbuffer const &) = delete;
292+
proof_trace_ringbuffer &operator=(proof_trace_ringbuffer &&) = delete;
293+
294+
bool read(void *ptr, size_t len) override {
295+
auto *data = static_cast<uint8_t *>(ptr);
296+
return read(data, len);
297+
}
298+
299+
int read() override {
300+
uint8_t c = 0;
301+
if (read(&c)) {
302+
return c;
303+
}
304+
return -1;
305+
}
306+
307+
bool has_word() override {
308+
uint64_t word = 0;
309+
auto *data = reinterpret_cast<uint8_t *>(&word);
310+
return peek(data, sizeof(word));
311+
}
312+
313+
bool eof() override { return peek() == -1; }
314+
315+
int peek() override {
316+
uint8_t c = 0;
317+
if (peek(&c)) {
318+
return c;
319+
}
320+
return -1;
321+
}
322+
323+
uint64_t peek_word() override {
324+
uint64_t word = 0;
325+
auto *data = reinterpret_cast<uint8_t *>(&word);
326+
if (!peek(data, sizeof(word))) {
327+
assert(false);
328+
}
329+
return word;
330+
}
331+
332+
bool read_uint32(uint32_t &i) override { return read(&i, sizeof(i)); }
333+
334+
bool read_uint64(uint64_t &i) override { return read(&i, sizeof(i)); }
335+
336+
bool read_string(std::string &str) override {
337+
str.resize(0);
338+
while (true) {
339+
int c = read();
340+
if (c == -1) {
341+
return false;
342+
}
343+
if ((char)c == '\0') {
344+
break;
345+
}
346+
str.push_back((char)c);
347+
}
348+
return true;
349+
}
350+
351+
bool read_string(std::string &str, size_t len) override {
352+
str.resize(len);
353+
return read(str.data(), len);
354+
}
355+
};
356+
206357
namespace detail {
207358

208359
template <typename It>

include/kllvm/binary/ringbuffer.h

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
#ifndef RINGBUFFER_H
2+
#define RINGBUFFER_H
3+
4+
#include <array>
5+
#include <cstdint>
6+
#include <cstdlib>
7+
#include <semaphore.h>
8+
9+
namespace kllvm {
10+
11+
// Simple ringbuffer class, intended to live in shared memory and operated by a
12+
// reader and a writer process.
13+
14+
class shm_ringbuffer {
15+
public:
16+
// Ringbuffer size in bytes.
17+
// NOTE: In order to easily distinguish between when the buffer is full versus
18+
// empty, we maintain the invariant that the capacity of the buffer is one byte
19+
// less than its size. This way, the buffer is empty iff read_pos == write_pos,
20+
// and it is full iff read_pos == (write_pos+1)%size.
21+
static constexpr size_t size = 1024;
22+
23+
// Ringbuffer capacity in bytes.
24+
// As commented above, the capacity is always equal to size-1.
25+
static constexpr size_t capacity = size - 1;
26+
27+
private:
28+
bool eof_{false};
29+
size_t read_pos_{0};
30+
size_t write_pos_{0};
31+
std::array<uint8_t, size> buffer_;
32+
33+
public:
34+
shm_ringbuffer();
35+
36+
~shm_ringbuffer() = default;
37+
38+
// Returns the current size of the data contained in the ringbuffer.
39+
[[nodiscard]] size_t data_size() const;
40+
41+
// Write EOF to the ring buffer. Further writes after this is called are
42+
// undefined behavior.
43+
void put_eof();
44+
45+
// Returns true when the ringbuffer is empty and the EOF has been written, and
46+
// false otherwise. As commented above, the ringbuffer is empty iff
47+
// read_pos == write_pos.
48+
[[nodiscard]] bool eof() const;
49+
50+
// Add data to the ringbuffer. The behavior is undefined if the buffer does not
51+
// have enough remaining space to fit the data or if EOF has been written to the
52+
// ringbuffer. The behavior is also undefined if the data pointer passed to this
53+
// function does not point to a contiguous memory chunk of the corresponding
54+
// size.
55+
void put(uint8_t const *data, size_t count = 1);
56+
57+
// Get and remove data from the ringbuffer. The behavior is undefined if more
58+
// data is requested than it is currently available in the ringbuffer. The
59+
// behavior is also undefined if the data pointer passed to this function does
60+
// not point to a contiguous memory chunk of the corresponding size.
61+
void get(uint8_t *data, size_t count = 1);
62+
};
63+
64+
} // namespace kllvm
65+
66+
#endif

lib/binary/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ add_library(BinaryKore
22
serializer.cpp
33
deserializer.cpp
44
ProofTraceParser.cpp
5+
ringbuffer.cpp
56
)
67

78
target_link_libraries(BinaryKore

lib/binary/ProofTraceParser.cpp

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
#include <kllvm/binary/ProofTraceParser.h>
2+
#include <kllvm/binary/ringbuffer.h>
23

34
#include <fmt/format.h>
45
#include <fstream>
@@ -231,4 +232,22 @@ proof_trace_parser::parse_proof_trace_from_file(std::string const &filename) {
231232
return trace;
232233
}
233234

235+
std::optional<llvm_rewrite_trace>
236+
proof_trace_parser::parse_proof_trace_from_shmem(
237+
void *shm_object, sem_t *data_avail, sem_t *space_avail) {
238+
proof_trace_ringbuffer buffer(shm_object, data_avail, space_avail);
239+
llvm_rewrite_trace trace;
240+
bool result = parse_trace(buffer, trace);
241+
242+
if (!result || !buffer.eof()) {
243+
return std::nullopt;
244+
}
245+
246+
if (verbose_) {
247+
trace.print(std::cout, expand_terms_);
248+
}
249+
250+
return trace;
251+
}
252+
234253
} // namespace kllvm

lib/binary/ringbuffer.cpp

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
#include <kllvm/binary/ringbuffer.h>
2+
3+
#include <cassert>
4+
#include <cstring>
5+
6+
namespace kllvm {
7+
8+
shm_ringbuffer::shm_ringbuffer()
9+
: buffer_() { }
10+
11+
size_t shm_ringbuffer::data_size() const {
12+
if (write_pos_ < read_pos_) {
13+
return size - (read_pos_ - write_pos_);
14+
}
15+
16+
return write_pos_ - read_pos_;
17+
}
18+
19+
void shm_ringbuffer::put_eof() {
20+
assert(!eof_);
21+
eof_ = true;
22+
}
23+
24+
bool shm_ringbuffer::eof() const {
25+
// NOTE: for synchronization purposes, it is important that the eof_ field is
26+
// checked first. Typically, the reader process will call this, so we want to
27+
// avoid a race where the writer updates buf.writer_pos after the reader has
28+
// accessed it but before the reader has fully evaluated the condition. If
29+
// eof_ is checked first, and due to short-circuiting, we know that if eof_ is
30+
// true, the writer will not do any further updates to the write_pos_ field,
31+
// and if eof_ is false, the reader will not access write_pos_ at all.
32+
return eof_ && write_pos_ == read_pos_;
33+
}
34+
35+
void shm_ringbuffer::put(uint8_t const *data, size_t count) {
36+
assert(!eof_);
37+
assert(data);
38+
39+
// check if we need to wrap to the start of the ringbuffer
40+
size_t no_wrap_size = size - write_pos_;
41+
size_t rest_count = count;
42+
if (count > no_wrap_size) {
43+
// if yes, do a first copy to reach the end of the ringbuffer and wrap to
44+
// start
45+
memcpy(buffer_.data() + write_pos_, data, no_wrap_size);
46+
write_pos_ = 0;
47+
data += no_wrap_size;
48+
rest_count = count - no_wrap_size;
49+
}
50+
51+
// copy the (rest of the) data
52+
memcpy(buffer_.data() + write_pos_, data, rest_count);
53+
write_pos_ += rest_count;
54+
if (write_pos_ == size) {
55+
write_pos_ = 0;
56+
}
57+
}
58+
59+
void shm_ringbuffer::get(uint8_t *data, size_t count) {
60+
assert(data);
61+
62+
// check if we need to wrap to the start of the ringbuffer
63+
size_t no_wrap_size = size - read_pos_;
64+
size_t rest_count = count;
65+
if (count > no_wrap_size) {
66+
// if yes, do a first copy to reach the end of the ringbuffer and wrap to
67+
// start
68+
memcpy(data, buffer_.data() + read_pos_, no_wrap_size);
69+
read_pos_ = 0;
70+
data += no_wrap_size;
71+
rest_count = count - no_wrap_size;
72+
}
73+
74+
// copy the (rest of the) data
75+
memcpy(data, buffer_.data() + read_pos_, rest_count);
76+
read_pos_ += rest_count;
77+
if (read_pos_ == size) {
78+
read_pos_ = 0;
79+
}
80+
}
81+
82+
} // namespace kllvm

0 commit comments

Comments
 (0)