diff --git a/axiom-profiler-GUI/assets/html/style.css b/axiom-profiler-GUI/assets/html/style.css
index 9da7b0f5..e09e5b61 100644
--- a/axiom-profiler-GUI/assets/html/style.css
+++ b/axiom-profiler-GUI/assets/html/style.css
@@ -437,6 +437,7 @@ ul.selected-info {
.dot {
display: inline-block;
position: relative;
+ overflow-x: auto;
}
.dot.scaled {
width: 100%;
diff --git a/axiom-profiler-GUI/src/screen/homepage/file.rs b/axiom-profiler-GUI/src/screen/homepage/file.rs
index 9c14059e..ee3fda77 100644
--- a/axiom-profiler-GUI/src/screen/homepage/file.rs
+++ b/axiom-profiler-GUI/src/screen/homepage/file.rs
@@ -294,7 +294,7 @@ impl Homepage {
let stop_loading = self.stop_loading.clone();
let link = link.clone();
- log::trace!("Selected file \"{}\"", file_info.name);
+ log::debug!("Selected file \"{}\"", file_info.name);
// Turn into stream
let blob: &web_sys::Blob = file.as_ref();
let stream = ReadableStream::from_raw(blob.stream().unchecked_into());
@@ -307,7 +307,7 @@ impl Homepage {
});
}
Err((_err, _stream)) => {
- log::trace!("Loading to string \"{}\"", file_info.name);
+ log::debug!("Loading to string \"{}\"", file_info.name);
link.send_message(HomepageM::LoadingState(LoadingState::ReadingToString));
let reader = gloo::file::callbacks::read_as_text(&file, move |res| {
let text_data = match res {
@@ -320,7 +320,7 @@ impl Homepage {
let remaining_memory =
Self::BROWSER_MEM_LIMIT - text_data.len() - 64 * 1024 * 1024;
- log::trace!("Parsing \"{}\"", file_info.name);
+ log::debug!("Parsing \"{}\"", file_info.name);
link.send_message(HomepageM::LoadingState(LoadingState::StartParsing));
wasm_bindgen_futures::spawn_local(async move {
let parser = Z3Parser::from_str(&text_data);
diff --git a/axiom-profiler-GUI/src/screen/homepage/mod.rs b/axiom-profiler-GUI/src/screen/homepage/mod.rs
index b70deea9..1ad91264 100644
--- a/axiom-profiler-GUI/src/screen/homepage/mod.rs
+++ b/axiom-profiler-GUI/src/screen/homepage/mod.rs
@@ -184,7 +184,7 @@ impl Screen for Homepage {
self.load_example(example, response, link)
}
HomepageM::LoadingState(mut state) => {
- log::trace!("New state \"{state:?}\"");
+ log::debug!("New state \"{state:?}\"");
if let (LoadingState::Parsing(parsing, _), LoadingState::Parsing(old, _)) =
(&mut state, &self.progress)
{
diff --git a/axiom-profiler-GUI/src/screen/inst_graph/render/mod.rs b/axiom-profiler-GUI/src/screen/inst_graph/render/mod.rs
index 6142efe0..2c3551a3 100644
--- a/axiom-profiler-GUI/src/screen/inst_graph/render/mod.rs
+++ b/axiom-profiler-GUI/src/screen/inst_graph/render/mod.rs
@@ -46,7 +46,7 @@ impl Graph {
for (can_select, idx, filter) in cmd.filters() {
let output = filter.apply(graph, parser);
- log::trace!("Applied filter {filter:?} -> {output:?}");
+ log::debug!("Applied filter {filter:?} -> {output:?}");
modified |= output.modified;
if !output.modified {
@@ -125,7 +125,7 @@ impl Graph {
let (selected_nodes, selected_edges) = self.update_selected(&visible);
let dimensions = GraphDimensions::of_graph(&visible);
- log::trace!("Rendering graph with {dimensions:?}");
+ log::debug!("Rendering graph with {dimensions:?}");
let new_permissions = dimensions.max(Self::default_permissions());
self.filter.chain.set_permissions(new_permissions);
@@ -201,7 +201,7 @@ impl Graph {
},
)
);
- // log::trace!("Graph DOT:\n{dot_output}");
+ // log::debug!("Graph DOT:\n{dot_output}");
self.state = Ok(GraphState::RenderingGraph);
let link = link.clone();
wasm_bindgen_futures::spawn_local(async move {
@@ -219,7 +219,7 @@ impl Graph {
}
};
let elapsed = start.elapsed();
- log::trace!(
+ log::debug!(
"Graph: Converting dot-String to SVG took {} seconds",
elapsed.as_secs()
);
diff --git a/axiom-profiler-GUI/src/screen/ml/render.rs b/axiom-profiler-GUI/src/screen/ml/render.rs
index 2a495ea7..c1363860 100644
--- a/axiom-profiler-GUI/src/screen/ml/render.rs
+++ b/axiom-profiler-GUI/src/screen/ml/render.rs
@@ -52,7 +52,7 @@ pub fn MlgRenderer(props: &MlgrProps) -> Html {
};
ctxt.config.font_tag = true;
let dot = MlgRenderer::generate_dot(graph, ctxt, &props.parser.colour_map);
- log::trace!("ML Graph DOT:\n{dot}");
+ log::debug!("ML Graph DOT:\n{dot}");
let warning = if graph.graph_incomplete {
html! { {"⚠️ Incomplete ⚠️"} }
@@ -119,7 +119,7 @@ impl MlgRenderer {
let cluster_fixed = cluster("fixed", "gray96", fixeds.join(join));
let cluster_out = cluster("out", "aliceblue", outputs.join(join));
format!(
- "digraph {{{join}{}{join}{cluster_in}{join}{cluster_fixed}{join}{cluster_out}{join}{}\n}}",
+ "digraph {{{join}{}{join}{cluster_in}{join}{cluster_fixed}{join}{cluster_out}\n{}\n}}",
settings.join(join),
outside.join("\n"),
)
diff --git a/axiom-profiler-GUI/src/utils/graphviz.rs b/axiom-profiler-GUI/src/utils/graphviz.rs
index 95c4c015..df2fd509 100644
--- a/axiom-profiler-GUI/src/utils/graphviz.rs
+++ b/axiom-profiler-GUI/src/utils/graphviz.rs
@@ -35,7 +35,7 @@ pub fn Dot(props: &DotProps) -> Html {
return;
}
};
- log::trace!(
+ log::debug!(
"Converting dot-String to SVG took {}ms",
elapsed.as_millis()
);
diff --git a/smt-log-parser/src/cmd/args.rs b/smt-log-parser/src/cmd/args.rs
index a8c0ccf7..9b4e88de 100644
--- a/smt-log-parser/src/cmd/args.rs
+++ b/smt-log-parser/src/cmd/args.rs
@@ -38,6 +38,9 @@ pub enum Commands {
/// The maximum time to spend parsing each file (in seconds)
#[arg(short, long, default_value_t = 15.0)]
timeout: f32,
+ /// Whether to print out memory usage information
+ #[arg(short, long, default_value_t = false)]
+ memory: bool,
},
/// Try to reconstruct the `.smt2` file
Reconstruct {
diff --git a/smt-log-parser/src/cmd/mod.rs b/smt-log-parser/src/cmd/mod.rs
index 04ec8932..b0ccf66c 100644
--- a/smt-log-parser/src/cmd/mod.rs
+++ b/smt-log-parser/src/cmd/mod.rs
@@ -17,7 +17,11 @@ pub fn run() -> Result<(), String> {
pretty_print,
} => dependencies::run(logfile, depth, pretty_print)?,
args::Commands::Stats { logfile, k } => stats::run(logfile, k)?,
- args::Commands::Test { logfiles, timeout } => test::run(logfiles, timeout)?,
+ args::Commands::Test {
+ logfiles,
+ timeout,
+ memory,
+ } => test::run(logfiles, timeout, memory)?,
args::Commands::Reconstruct { logfile, clean } => reconstruct::run(logfile, clean)?,
}
diff --git a/smt-log-parser/src/cmd/test.rs b/smt-log-parser/src/cmd/test.rs
index f444716a..965783da 100644
--- a/smt-log-parser/src/cmd/test.rs
+++ b/smt-log-parser/src/cmd/test.rs
@@ -9,12 +9,12 @@ use wasm_timer::Instant;
const MB: u64 = 1024_u64 * 1024_u64;
-pub fn run(logfiles: Vec, timeout: f32) -> Result<(), String> {
+pub fn run(logfiles: Vec, timeout: f32, memory: bool) -> Result<(), String> {
for path in logfiles {
let builder = std::thread::Builder::new().stack_size(8 * MB as usize);
let t = builder
.spawn(move || {
- run_file(path, timeout);
+ run_file(path, timeout, memory);
})
.unwrap();
t.join().unwrap();
@@ -22,7 +22,7 @@ pub fn run(logfiles: Vec, timeout: f32) -> Result<(), String> {
Ok(())
}
-fn run_file(path: PathBuf, timeout: f32) {
+fn run_file(path: PathBuf, timeout: f32, memory: bool) {
let path = std::path::Path::new(&path);
let filename = path
.file_name()
@@ -42,8 +42,10 @@ fn run_file(path: PathBuf, timeout: f32) {
let (_metadata, parser) = Z3Parser::from_file(path).unwrap();
let (timeout, mut result) = parser.process_all_timeout(to);
let elapsed_time = time.elapsed();
- #[cfg(feature = "mem_dbg")]
- result.mem_dbg(DbgFlags::default()).ok();
+ if memory {
+ #[cfg(feature = "mem_dbg")]
+ result.mem_dbg(DbgFlags::default()).ok();
+ }
println!(
"{} parsing after {} seconds (timeout {timeout:?})",
if timeout.is_timeout() {
@@ -65,8 +67,10 @@ fn run_file(path: PathBuf, timeout: f32) {
.unwrap()
.map(|q| result[q.quant].kind.debug(&result))
.collect();
- #[cfg(feature = "mem_dbg")]
- inst_graph.mem_dbg(DbgFlags::default()).ok();
+ if memory {
+ #[cfg(feature = "mem_dbg")]
+ inst_graph.mem_dbg(DbgFlags::default()).ok();
+ }
println!(
"Finished analysing after {} seconds. Found {sure_mls} sure mls, {maybe_mls} maybe mls. Quants involved {quants_involved:?}",
(process_time - elapsed_time).as_secs_f32(),