Skip to content

Commit f172c61

Browse files
committed
Merge remote-tracking branch 'origin/develop'
2 parents 9f340e1 + c202d7c commit f172c61

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

73 files changed

+3
-936
lines changed

include/kllvm/binary/ProofTraceParser.h

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -698,8 +698,6 @@ 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);
703701
std::optional<llvm_rewrite_trace> parse_proof_trace(std::string const &data);
704702

705703
friend class llvm_rewrite_trace_iterator;

include/kllvm/binary/deserializer.h

Lines changed: 0 additions & 255 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
#define AST_DESERIALIZER_H
33

44
#include <kllvm/ast/AST.h>
5-
#include <kllvm/binary/ringbuffer.h>
65
#include <kllvm/binary/serializer.h>
76
#include <kllvm/binary/version.h>
87

@@ -205,260 +204,6 @@ class proof_trace_file_buffer : public proof_trace_buffer {
205204
}
206205
};
207206

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-
214-
std::deque<uint8_t> peek_data_;
215-
std::array<uint8_t, shm_ringbuffer::buffered_access_sz> buffer_;
216-
size_t buffer_data_size_{0};
217-
size_t buffer_data_start_{0};
218-
219-
bool peek_eof_{false};
220-
bool buffered_eof_{false};
221-
bool read_eof_{false};
222-
223-
// Helper function that reads from the shared memory ringbuffer into the
224-
// buffer_. It tries to read shm_ringbuffer::buffered_access_sz bytes of data.
225-
// It assumes that buffer_ is empty.
226-
void read_from_shared_memory() {
227-
assert(buffer_data_size_ == 0);
228-
assert(buffer_data_start_ == 0);
229-
230-
if (buffered_eof_) {
231-
return;
232-
}
233-
234-
sem_wait(data_avail_);
235-
236-
if (shm_buffer_->eof()) {
237-
// EOF has been written to the ringbuffer. Check if this is the last chunk
238-
// of data to be read.
239-
size_t remaining_data_sz = shm_buffer_->data_size();
240-
if (remaining_data_sz < shm_ringbuffer::buffered_access_sz) {
241-
// This is the last chunk of data to be read from the ringbuffer.
242-
shm_buffer_->get(buffer_.data(), remaining_data_sz);
243-
sem_post(space_avail_);
244-
245-
buffer_data_size_ = remaining_data_sz;
246-
buffered_eof_ = true;
247-
248-
return;
249-
}
250-
}
251-
252-
// Else, either EOF has not been written or EOF has been written but there
253-
// are remaining full chunks to be read. In any case, we can read a full
254-
// chunk.
255-
shm_buffer_->get(buffer_.data());
256-
sem_post(space_avail_);
257-
258-
buffer_data_size_ = shm_ringbuffer::buffered_access_sz;
259-
}
260-
261-
bool read(uint8_t *ptr, size_t len = 1) {
262-
// Check if we have read EOF already.
263-
if (read_eof_) {
264-
return false;
265-
}
266-
267-
// Consume peeked data.
268-
while (len > 0 && !peek_data_.empty()) {
269-
*ptr = peek_data_.front();
270-
peek_data_.pop_front();
271-
ptr++;
272-
len--;
273-
}
274-
275-
// Consume peeked EOF.
276-
if (len > 0 && peek_eof_) {
277-
read_eof_ = true;
278-
return false;
279-
}
280-
281-
// Peeked data has been fully consumed. If more data is requested, we need
282-
// to read from buffer_ and/or shared memory.
283-
while (len > 0) {
284-
// If buffer_ is empty, try to fetch more data from the shared memory
285-
// ringbuffer.
286-
if (buffer_data_size_ == 0) {
287-
// Check for and conusme buffered EOF.
288-
if (buffered_eof_) {
289-
read_eof_ = true;
290-
return false;
291-
}
292-
293-
assert(buffer_data_start_ == 0);
294-
read_from_shared_memory();
295-
}
296-
297-
// Read available data from the buffer_.
298-
assert(buffer_data_start_ < shm_ringbuffer::buffered_access_sz);
299-
assert(
300-
buffer_data_start_ + buffer_data_size_
301-
<= shm_ringbuffer::buffered_access_sz);
302-
size_t size_to_read_from_buffer = std::min(len, buffer_data_size_);
303-
memcpy(
304-
ptr, buffer_.data() + buffer_data_start_, size_to_read_from_buffer);
305-
ptr += size_to_read_from_buffer;
306-
len -= size_to_read_from_buffer;
307-
308-
buffer_data_start_ += size_to_read_from_buffer;
309-
buffer_data_size_ -= size_to_read_from_buffer;
310-
if (buffer_data_start_ == shm_ringbuffer::buffered_access_sz) {
311-
assert(buffer_data_size_ == 0);
312-
buffer_data_start_ = 0;
313-
}
314-
}
315-
316-
assert(len == 0);
317-
return true;
318-
}
319-
320-
bool peek(uint8_t *ptr, size_t len = 1) {
321-
// Check if we have read EOF already.
322-
if (read_eof_) {
323-
return false;
324-
}
325-
326-
// Copy already peeked data.
327-
size_t i = 0;
328-
while (len > 0 && i < peek_data_.size()) {
329-
*ptr = peek_data_[i];
330-
ptr++;
331-
i++;
332-
len--;
333-
}
334-
335-
// Check for already peeked EOF.
336-
if (len > 0 && peek_eof_) {
337-
return false;
338-
}
339-
340-
// Already peeked data has been fully copied. If more data is requested, we
341-
// need to peek from buffer_ and/or shared memory.
342-
while (len > 0) {
343-
// If buffer_ is empty, try to fetch more data from the shared memory
344-
// ringbuffer.
345-
if (buffer_data_size_ == 0) {
346-
// Check for buffered EOF.
347-
if (buffered_eof_) {
348-
peek_eof_ = true;
349-
return false;
350-
}
351-
352-
assert(buffer_data_start_ == 0);
353-
read_from_shared_memory();
354-
}
355-
356-
// Peek available data from the buffer_.
357-
assert(buffer_data_start_ < shm_ringbuffer::buffered_access_sz);
358-
assert(
359-
buffer_data_start_ + buffer_data_size_
360-
<= shm_ringbuffer::buffered_access_sz);
361-
size_t size_to_peek_from_buffer = std::min(len, buffer_data_size_);
362-
memcpy(
363-
ptr, buffer_.data() + buffer_data_start_, size_to_peek_from_buffer);
364-
peek_data_.insert(
365-
peek_data_.end(), buffer_.begin() + buffer_data_start_,
366-
buffer_.begin() + buffer_data_start_ + size_to_peek_from_buffer);
367-
ptr += size_to_peek_from_buffer;
368-
len -= size_to_peek_from_buffer;
369-
370-
buffer_data_start_ += size_to_peek_from_buffer;
371-
buffer_data_size_ -= size_to_peek_from_buffer;
372-
if (buffer_data_start_ == shm_ringbuffer::buffered_access_sz) {
373-
assert(buffer_data_size_ == 0);
374-
buffer_data_start_ = 0;
375-
}
376-
}
377-
378-
assert(len == 0);
379-
return true;
380-
}
381-
382-
public:
383-
proof_trace_ringbuffer(
384-
void *shm_object, sem_t *data_avail, sem_t *space_avail)
385-
: shm_buffer_(static_cast<shm_ringbuffer *>(shm_object))
386-
, data_avail_(data_avail)
387-
, space_avail_(space_avail)
388-
, buffer_() {
389-
new (shm_buffer_) shm_ringbuffer;
390-
}
391-
392-
~proof_trace_ringbuffer() override { shm_buffer_->~shm_ringbuffer(); }
393-
394-
proof_trace_ringbuffer(proof_trace_ringbuffer const &) = delete;
395-
proof_trace_ringbuffer(proof_trace_ringbuffer &&) = delete;
396-
proof_trace_ringbuffer &operator=(proof_trace_ringbuffer const &) = delete;
397-
proof_trace_ringbuffer &operator=(proof_trace_ringbuffer &&) = delete;
398-
399-
bool read(void *ptr, size_t len) override {
400-
auto *data = static_cast<uint8_t *>(ptr);
401-
return read(data, len);
402-
}
403-
404-
int read() override {
405-
uint8_t c = 0;
406-
if (read(&c)) {
407-
return c;
408-
}
409-
return -1;
410-
}
411-
412-
bool has_word() override {
413-
uint64_t word = 0;
414-
auto *data = reinterpret_cast<uint8_t *>(&word);
415-
return peek(data, sizeof(word));
416-
}
417-
418-
bool eof() override { return peek() == -1; }
419-
420-
int peek() override {
421-
uint8_t c = 0;
422-
if (peek(&c)) {
423-
return c;
424-
}
425-
return -1;
426-
}
427-
428-
uint64_t peek_word() override {
429-
uint64_t word = 0;
430-
auto *data = reinterpret_cast<uint8_t *>(&word);
431-
if (!peek(data, sizeof(word))) {
432-
assert(false);
433-
}
434-
return word;
435-
}
436-
437-
bool read_uint32(uint32_t &i) override { return read(&i, sizeof(i)); }
438-
439-
bool read_uint64(uint64_t &i) override { return read(&i, sizeof(i)); }
440-
441-
bool read_string(std::string &str) override {
442-
str.resize(0);
443-
while (true) {
444-
int c = read();
445-
if (c == -1) {
446-
return false;
447-
}
448-
if ((char)c == '\0') {
449-
break;
450-
}
451-
str.push_back((char)c);
452-
}
453-
return true;
454-
}
455-
456-
bool read_string(std::string &str, size_t len) override {
457-
str.resize(len);
458-
return read(str.data(), len);
459-
}
460-
};
461-
462207
namespace detail {
463208

464209
template <typename It>

include/kllvm/binary/ringbuffer.h

Lines changed: 0 additions & 69 deletions
This file was deleted.

include/kllvm/binary/serializer.h

Lines changed: 0 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
#define AST_SERIALIZER_H
33

44
#include <kllvm/ast/AST.h>
5-
#include <kllvm/binary/ringbuffer.h>
65
#include <kllvm/binary/version.h>
76

87
#include <array>
@@ -182,41 +181,6 @@ class proof_trace_file_writer : public proof_trace_writer {
182181
void write_eof() override { }
183182
};
184183

185-
class proof_trace_ringbuffer_writer : public proof_trace_writer {
186-
private:
187-
shm_ringbuffer *shm_buffer_;
188-
sem_t *data_avail_;
189-
sem_t *space_avail_;
190-
191-
std::array<uint8_t, shm_ringbuffer::buffered_access_sz> buffer_;
192-
size_t buffer_data_size_{0};
193-
194-
void write(uint8_t const *ptr, size_t len = 1);
195-
196-
public:
197-
proof_trace_ringbuffer_writer(
198-
void *shm_object, sem_t *data_avail, sem_t *space_avail)
199-
: shm_buffer_(reinterpret_cast<shm_ringbuffer *>(shm_object))
200-
, data_avail_(data_avail)
201-
, space_avail_(space_avail)
202-
, buffer_() { }
203-
204-
~proof_trace_ringbuffer_writer() override { shm_buffer_->~shm_ringbuffer(); }
205-
206-
proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer const &) = delete;
207-
proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer &&) = delete;
208-
proof_trace_ringbuffer_writer &
209-
operator=(proof_trace_ringbuffer_writer const &)
210-
= delete;
211-
proof_trace_ringbuffer_writer &operator=(proof_trace_ringbuffer_writer &&)
212-
= delete;
213-
214-
void write(void const *ptr, size_t len) override;
215-
void write_string(char const *str, size_t len) override;
216-
void write_string(char const *str) override;
217-
void write_eof() override;
218-
};
219-
220184
} // namespace kllvm
221185

222186
#endif

0 commit comments

Comments
 (0)