runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

Refactor proof hint parser #1065

Closed dwightguth closed 1 month ago

dwightguth commented 1 month ago

This is an intermediate step on the way to having a streaming parser for the proof hint. What this is doing is modifying the existing parser so that it no longer loads the entire file into memory prior to parsing it, and so that it abstracts away all the low-level I/O details behind an interface.

This interface is an abstract class that is implemented by classes representing in-memory and file buffers, respectively. In the future we may also have a class representing a memory-mapped file.

In the next PR, I will create a new class that parses and returns events one at a time.