Skip to content

Commit

Permalink
Load file from stream to reduce memory usage
Browse files Browse the repository at this point in the history
Loading the log file to a String and parsing that would use a lot of memory, use streams instead
  • Loading branch information
JonasAlaif committed Dec 20, 2023
1 parent c1bbbd4 commit 3cd8199
Show file tree
Hide file tree
Showing 8 changed files with 47 additions and 76 deletions.
6 changes: 3 additions & 3 deletions .github/workflows/continuous_integration.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,14 @@ jobs:

steps:
- uses: actions/checkout@v4
- run: cargo fmt --all -- --check
- run: cargo fmt --workspace -- --check

clippy:
runs-on: ubuntu-latest

steps:
- uses: actions/checkout@v4
- run: cargo clippy --all -- -D warnings
- run: cargo clippy --workspace -- -D warnings

test:
# will wait for new cache on push to main branch, otherwise will run straight away with existing cache
Expand All @@ -35,7 +35,7 @@ jobs:
key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ hashFiles('smt-problems/**/*.smt2') }}
- id: check-logs-cached
run: test -d "logs"
- run: cargo test --all
- run: cargo test --workspace -- --nocapture

# Failure
- run: tar -czf failing_logs.tar.bz2 logs/
Expand Down
3 changes: 2 additions & 1 deletion axiom-profiler-GUI/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ getrandom = { version = "0.2", features = ["js"] }
smt-log-parser = { path = "../smt-log-parser" }
petgraph = "0.6.4"
viz-js = "3.1.0"
wasm-streams = "0.3.0"
wasm-streams = "0.4.0"
yew-hooks = "0.3.0"
fxhash = "0.2.1"
typed-index-collections = "3.1.0"
Expand All @@ -35,6 +35,7 @@ paste = "1.0.14"
yew-agent = "0.2.0"
chrono = "0.4"
indexmap = "2.1.0"
console_error_panic_hook = "0.1.2"

[build-dependencies]
vergen = { version = "8.2", features = ["git", "gitcl"] }
1 change: 1 addition & 0 deletions axiom-profiler-GUI/src/bin/app.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
fn main() {
std::panic::set_hook(Box::new(console_error_panic_hook::hook));
wasm_logger::init(wasm_logger::Config::default());
log::debug!("App is starting");
// yew::Renderer::<Main>::new().render();
Expand Down
99 changes: 34 additions & 65 deletions axiom-profiler-GUI/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,12 @@ pub mod results;
mod utils;
// mod select_dropdown;
pub enum Msg {
LoadedBytes(String, Vec<u8>),
LoadedFile(String, Z3Parser),
Files(Option<FileList>),
}

pub struct FileDataComponent {
files: Vec<String>,
parsers: Vec<ParserData>,
files: Vec<std::rc::Rc<Z3Parser>>,
readers: Vec<FileReader>,
}

Expand All @@ -39,7 +38,6 @@ impl Component for FileDataComponent {
fn create(_ctx: &Context<Self>) -> Self {
Self {
files: Vec::new(),
parsers: Vec::new(),
readers: Vec::new(),
}
}
Expand All @@ -50,60 +48,44 @@ impl Component for FileDataComponent {
let Some(files) = files else {
return false;
};
let mut changed = !self.files.is_empty() || !self.readers.is_empty();
let changed = !self.files.is_empty() || !self.readers.is_empty();
self.files.clear();
self.readers.clear();
log::info!("Files selected: {}", files.len());
for file in files.into_iter() {
let file_name = file.name();
if true {
// Old reader where all files are loaded as strings
let task = {
// Turn into stream
let blob: &web_sys::Blob = file.as_ref();
let stream = ReadableStream::from_raw(blob.stream().unchecked_into());
match stream.try_into_async_read() {
Ok(stream) => {
let link = ctx.link().clone();
gloo_file::callbacks::read_as_bytes(&file, move |res| {
link.send_message(Msg::LoadedBytes(
file_name,
res.expect("failed to read file"),
))
})
};
self.readers.push(task);
} else {
// Turn into stream
let blob: &web_sys::Blob = file.as_ref();
let stream = ReadableStream::from_raw(blob.stream().unchecked_into());
match stream.try_into_async_read() {
Ok(stream) => {
let parser = Z3Parser::from_async(stream.buffer());
self.parsers.push(ParserData::new(parser));
changed = true;
}
Err((_err, _stream)) => {
let link = ctx.link().clone();
let reader =
gloo_file::callbacks::read_as_bytes(file, move |res| {
link.send_message(Msg::LoadedBytes(
file_name,
res.expect("failed to read file"),
))
});
self.readers.push(reader);
}
};
}
let parser = Z3Parser::from_async(stream.buffer());
wasm_bindgen_futures::spawn_local(async move {
log::info!("Parsing: {file_name}");
let parser = parser.process_all().await;
link.send_message(Msg::LoadedFile(file_name, parser))
});
}
Err((_err, _stream)) => {
let link = ctx.link().clone();
let reader =
gloo_file::callbacks::read_as_bytes(file, move |res| {
log::info!("Loading to string: {file_name}");
let text_data = String::from_utf8(res.expect("failed to read file")).unwrap();
log::info!("Parsing: {file_name}");
let parser = Z3Parser::from_str(&text_data).process_all();
link.send_message(Msg::LoadedFile(file_name, parser))
});
self.readers.push(reader);
}
};
}
changed
}
Msg::LoadedBytes(file_name, data) => {
log::info!("Processing: {}", file_name);
if true {
// Old reader where all files are loaded as strings
let text_data = String::from_utf8(data).unwrap();
self.files.push(text_data);
} else {
let parser = Z3Parser::from_async(data.into_async_cursor());
self.parsers.push(ParserData::new(parser));
}
Msg::LoadedFile(file_name, parser) => {
log::info!("Processing: {file_name}");
self.files.push(std::rc::Rc::new(parser));
true
}
}
Expand Down Expand Up @@ -131,31 +113,18 @@ impl Component for FileDataComponent {
</div>
</div>
<div style="display: flex; ">
{ for self.files.iter().map(|f| Self::view_file(f))}
{ for self.files.iter().map(|f| Self::view_file(std::rc::Rc::clone(f)))}
</div>
</div>
}
}
}

impl FileDataComponent {
fn view_file(data: &str) -> Html {
fn view_file(data: std::rc::Rc<Z3Parser>) -> Html {
log::debug!("Viewing file");
html! {
<SVGResult trace_file_text={AttrValue::from(data.to_string())}/>
}
}
}

pub struct ParserData {
parser: AsyncParser<'static, Z3Parser>,
parsed: Option<Z3Parser>,
}
impl ParserData {
pub fn new(parser: AsyncParser<'static, Z3Parser>) -> Self {
Self {
parser,
parsed: None,
<SVGResult parser={data}/>
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion axiom-profiler-GUI/src/results/filters/filter_chain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ pub struct FilterChainProps {
pub apply_filter: Callback<Filter>,
pub reset_graph: Callback<()>,
pub render_graph: Callback<UserPermission>,
pub dependency: AttrValue,
pub dependency: *const smt_log_parser::Z3Parser,
pub weak_link: WeakComponentLink<FilterChain>,
}

Expand Down
2 changes: 1 addition & 1 deletion axiom-profiler-GUI/src/results/filters/graph_filters.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ impl Filter {
#[derive(Properties, PartialEq)]
pub struct GraphFilterProps {
pub add_filters: Callback<Vec<Filter>>,
pub dependency: AttrValue,
pub dependency: *const smt_log_parser::Z3Parser,
}

#[function_component(GraphFilter)]
Expand Down
8 changes: 4 additions & 4 deletions axiom-profiler-GUI/src/results/svg_result.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ pub struct SVGResult {

#[derive(Properties, PartialEq)]
pub struct SVGProps {
pub trace_file_text: AttrValue,
pub parser: std::rc::Rc<Z3Parser>,
}

impl Component for SVGResult {
Expand All @@ -87,7 +87,7 @@ impl Component for SVGResult {

fn create(ctx: &Context<Self>) -> Self {
log::debug!("Creating SVGResult component");
let parser = Z3Parser::from_str(&ctx.props().trace_file_text).process_all();
let parser = std::rc::Rc::clone(&ctx.props().parser);
let inst_graph = InstGraph::from(&parser);
let (quant_count, non_quant_insts) = parser.quant_count_incl_theory_solving();
let colour_map = QuantIdxToColourMap::from(quant_count, non_quant_insts);
Expand All @@ -102,7 +102,7 @@ impl Component for SVGResult {
inst_graph.get_edge_info(edge, parser, ignore_ids)
}});
Self {
parser: Rc::new(parser),
parser,
colour_map,
inst_graph,
svg_text: AttrValue::default(),
Expand Down Expand Up @@ -320,7 +320,7 @@ impl Component for SVGResult {
reset_graph={reset_graph.clone()}
render_graph={render_graph.clone()}
weak_link={self.filter_chain_link.clone()}
dependency={ctx.props().trace_file_text.clone()}
dependency={ctx.props().parser.as_ref() as *const _}
/>
</ContextProvider<Vec<InstInfo>>>
{async_graph_and_filter_chain_warning}
Expand Down
2 changes: 1 addition & 1 deletion axiom-profiler-GUI/src/utils/input_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ impl Reducible for InputValue {
#[derive(Properties, PartialEq)]
pub struct UsizeInputProps {
pub label: AttrValue,
pub dependency: AttrValue,
pub dependency: *const smt_log_parser::Z3Parser,
pub input_value: UseReducerHandle<InputValue>,
pub default_value: usize,
pub placeholder: AttrValue,
Expand Down

0 comments on commit 3cd8199

Please sign in to comment.