Limitations

Bounded Verification

perlchecker performs bounded verification, not full inductive verification. Loops are unrolled to a finite depth (default: 5). A “verified” result means the postcondition holds for all inputs that cause the loop to terminate within the unroll bound.

To verify a loop, you must provide a precondition that bounds the number of iterations. For example, # pre: $x >= 0 && $x <= 5 ensures a countdown loop terminates in at most 5 steps.

No Recursion

Direct and indirect recursion is detected and rejected. Functions can only call other functions — not themselves, and not through a cycle.

String Length Bound

Strings are bounded to 32 characters in the SMT model. The verifier cannot reason about strings longer than this. This limit is not configurable.

Path Explosion

Each if/else in a function doubles the number of symbolic execution paths. A function with n independent conditionals has up to 2n paths. The default path budget is 1024 (about 10 independent branches).

Use --max_paths to raise the budget, but be aware that verification time grows with the number of paths.

Single-File Scope

All functions called by a verified function must be defined in the same source file. There is no support for modules, imports, or cross-file verification.

Soundness Guarantees

perlchecker enforces the following soundness invariants:

  • Extern contracts are strict. If an extern function’s precondition or postcondition cannot be evaluated (e.g., references an undefined variable), verification fails with an error rather than silently assuming the contract is satisfied.

  • Array lengths are non-negative. Symbolic array length companions (scalar(@arr)) are constrained to be ≥ 0, matching Perl semantics.

  • Reference aliases propagate. Aliases created in the function body are visible in the postcondition type-check, and aliases created in both branches of an if/else are preserved after the merge.

  • Collection well-definedness. Array and hash return values undergo the same reflexivity check as scalar results, ensuring the SMT expression is evaluable.

  • Counterexample accuracy. When the solver cannot extract a concrete value for a variable in a counterexample, it is reported as <unconstrained> rather than an arbitrary default like 0 or “”.

Unsupported Perl Features

The following Perl features are not supported:

  • Regular expressions (=~, m/pattern/, s/from/to/)

  • References beyond scalar refs (\@arr, \%hash, nested refs)

  • eval and runtime code generation

  • Implicit variables ($_, @ARGV)

  • @_ outside of the initial parameter binding my (...) = @_;

  • Nested data structures (arrays of arrays, hashes of hashes)

  • Object-oriented features (bless, method calls, ->)

  • Modules and use / require statements

  • File I/O and system calls

  • wantarray and context sensitivity

  • Autovivification

  • Global variables

  • local and our declarations

  • Regular subroutine prototypes

  • sort, map, grep

  • foreach loops (only C-style for is supported)

  • Anonymous subroutines and closures

  • sprintf / printf

Solver Timeouts

Complex queries — especially those involving deep string manipulation, nested array operations, or many bitwise operations — may cause the Z3 solver to time out. When this happens, the result is Unknown rather than Verified or Counterexample.

Increase --solver_timeout_ms if you suspect the solver needs more time rather than the query being undecidable.