Summary
strata laurelAnalyze enters an infinite loop (spewing thousands of PANIC messages and consuming unbounded CPU/memory) when a Laurel program contains a procedure with a modifies clause that references a global variable.
Reproducer
Save as repro.lr.st:
var g: int;
procedure inc(x: int) returns (r: int)
modifies g
{
r := x + 1;
g := r;
}
procedure main() {
var a: int := 42;
assert a > 0;
}
Run either:
strata laurelAnalyze repro.lr.st
Observed behavior
The process enters an infinite loop, emitting hundreds of PANIC messages per second:
PANIC at Strata.DialectMap.decl! Strata.DDM.AST:1672:12: Unknown dialect
PANIC at Strata.Elab.elabOperation Strata.DDM.Elab.Core:1013:11: Missing position info ...
Unknown operation .
In a 3-second CPU time window, ~840 PANIC messages were emitted. Without a CPU time limit, the process consumed 14+ GB of memory before being killed.
Expected behavior
The command should either:
- Successfully translate the program, or
- Fail with a clear error message
Trigger conditions
The issue requires both:
- A global variable declaration (
var g: int)
- A
modifies clause referencing that global (modifies g)
The following variations do not trigger the bug:
- Procedure with
requires/ensures but no modifies (works fine)
- Procedure with
if/else but no modifies on a global (works fine)
- Procedure with
modifies on an output parameter only (different error, but no infinite loop)
Adding if/else or ensures to the reproducer does not change the behavior — the infinite loop is triggered by modifies + global variable alone.
Environment
- macOS (arm64)
- Branch:
tautschnig/ToCProverGOTO-Stmt (also likely affects main)
Workaround
Use ulimit -t <seconds> to bound CPU time when invoking strata:
bash -c 'ulimit -t 20; strata laurelAnalyze repro.lr.st'
Summary
strata laurelAnalyzeenters an infinite loop (spewing thousands of PANIC messages and consuming unbounded CPU/memory) when a Laurel program contains a procedure with amodifiesclause that references a global variable.Reproducer
Save as
repro.lr.st:Run either:
Observed behavior
The process enters an infinite loop, emitting hundreds of PANIC messages per second:
In a 3-second CPU time window, ~840 PANIC messages were emitted. Without a CPU time limit, the process consumed 14+ GB of memory before being killed.
Expected behavior
The command should either:
Trigger conditions
The issue requires both:
var g: int)modifiesclause referencing that global (modifies g)The following variations do not trigger the bug:
requires/ensuresbut nomodifies(works fine)if/elsebut nomodifieson a global (works fine)modifieson an output parameter only (different error, but no infinite loop)Adding
if/elseorensuresto the reproducer does not change the behavior — the infinite loop is triggered bymodifies+ global variable alone.Environment
tautschnig/ToCProverGOTO-Stmt(also likely affectsmain)Workaround
Use
ulimit -t <seconds>to bound CPU time when invokingstrata:bash -c 'ulimit -t 20; strata laurelAnalyze repro.lr.st'