Skip to content

Commit 4241abf

Browse files
hyperpolymathclaude
andcommitted
fix(provers): bounded_read_proof_file helper + 25 wrapper migrations
Closes 25 of the 26 panic-attack UnboundedAllocation findings flagged in reports/panic-attack-chunks/src-rust.json (deferred follow-up from 2026-04-25 evening session). Adds src/rust/provers/io.rs with `bounded_read_proof_file` capping proof-file reads at 64 MiB via `AsyncReadExt::take(N+1)` (TOCTOU-safe, errors on overflow rather than truncating). Migrates 25 prover backends from bare `tokio::fs::read_to_string(&path)` to the bounded helper: abella, acl2s, arend, athena, boogie, cameleer, cubical_agda, dedukti, hp_ecosystem, isabelle_zf, lambda_prolog, lean3, matita, mercury, mizar_ar, naproche, nitpick, nunchaku, opensmt, prover9, rocq, smtrat, typed_wasm, uppaal_stratego, zipperposition The 26th finding (integrity/solver_integrity.rs) is a TOML manifest read at startup from an operator-controlled path — different threat shape, deferred to a follow-up. The 47 unflagged backends already pass the panic-attack heuristic (detector treats `read_to_string` as bounded if the file's source contains the word "limit"); migrating them now would be scope creep beyond closing the surfaced findings. Future estate-wide pass can fold them in. io.rs ships with two unit tests (small_file_reads_fully, oversized_file_errors) — both pass under cargo test --lib. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 87f49a4 commit 4241abf

28 files changed

Lines changed: 141 additions & 33 deletions

Cargo.lock

Lines changed: 39 additions & 8 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

src/rust/provers/abella.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ impl ProverBackend for AbellaBackend {
7474
}
7575

7676
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
77-
let content = tokio::fs::read_to_string(&path)
77+
let content = super::bounded_read_proof_file(&path)
7878
.await
7979
.with_context(|| format!("Abella: reading {}", path.display()))?;
8080
self.parse_string(&content).await

src/rust/provers/acl2s.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ impl ProverBackend for Acl2sBackend {
5656
}
5757

5858
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
59-
let content = tokio::fs::read_to_string(&path)
59+
let content = super::bounded_read_proof_file(&path)
6060
.await
6161
.with_context(|| format!("ACL2s: reading {}", path.display()))?;
6262
self.parse_string(&content).await

src/rust/provers/arend.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ impl ProverBackend for ArendBackend {
4747
}
4848
}
4949
async fn parse_file(&self, p: PathBuf) -> Result<ProofState> {
50-
let c = tokio::fs::read_to_string(&p)
50+
let c = super::bounded_read_proof_file(&p)
5151
.await
5252
.with_context(|| format!("Arend: reading {}", p.display()))?;
5353
self.parse_string(&c).await

src/rust/provers/athena.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ impl ProverBackend for AthenaBackend {
4646
}
4747
}
4848
async fn parse_file(&self, p: PathBuf) -> Result<ProofState> {
49-
let c = tokio::fs::read_to_string(&p)
49+
let c = super::bounded_read_proof_file(&p)
5050
.await
5151
.with_context(|| format!("Athena: reading {}", p.display()))?;
5252
self.parse_string(&c).await

src/rust/provers/boogie.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ impl ProverBackend for BoogieBackend {
5959
}
6060

6161
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
62-
let content = tokio::fs::read_to_string(&path)
62+
let content = super::bounded_read_proof_file(&path)
6363
.await
6464
.with_context(|| format!("Boogie: reading {}", path.display()))?;
6565
self.parse_string(&content).await

src/rust/provers/cameleer.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ impl ProverBackend for CameleerBackend {
6363
}
6464

6565
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
66-
let content = tokio::fs::read_to_string(&path)
66+
let content = super::bounded_read_proof_file(&path)
6767
.await
6868
.with_context(|| format!("Cameleer: reading {}", path.display()))?;
6969
self.parse_string(&content).await

src/rust/provers/cubical_agda.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ impl ProverBackend for CubicalAgdaBackend {
7474
}
7575

7676
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
77-
let content = tokio::fs::read_to_string(&path).await?;
77+
let content = super::bounded_read_proof_file(&path).await?;
7878
self.parse_string(&content).await
7979
}
8080

src/rust/provers/dedukti.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ impl ProverBackend for DeduktiBackend {
6969
}
7070

7171
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
72-
let content = tokio::fs::read_to_string(&path)
72+
let content = super::bounded_read_proof_file(&path)
7373
.await
7474
.with_context(|| format!("Dedukti: reading {}", path.display()))?;
7575
self.parse_string(&content).await

src/rust/provers/hp_ecosystem.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ impl ProverBackend for HPEcosystemBackend {
183183
}
184184

185185
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
186-
let content = tokio::fs::read_to_string(&path)
186+
let content = super::bounded_read_proof_file(&path)
187187
.await
188188
.with_context(|| format!("HP ecosystem: reading {}", path.display()))?;
189189
self.parse_string(&content).await

0 commit comments

Comments
 (0)