phanalist

E0031: Division by Zero

E0031 reports division whose divisor can be zero. It is the division member of Phanalist’s bounded formal verification family (E0031-E0043). The family shares a Z3-backed engine that encodes path conditions and values, so a finding comes with a solver-backed counterexample rather than a heuristic guess.

Proofs are relative to the modeled subset, the configured checks, and the project’s interprocedural summaries. A clean result means no violation was found in that model; it is not a proof that every possible PHP execution is safe.

What it does not prove

• Full PHP semantics. Dynamic features such as eval, reflection, variable variables, dynamic calls and includes, magic methods, and runtime code generation are not modeled.
• Heap, object-state, reference, and alias invariants beyond the supported function summaries. Nested array shapes are tracked only while they remain unambiguous; a write through an untracked path forgets the affected root array. Reference aliases are not tracked: a tracked array is forgotten when it is shared by reference or iterated by reference, which is conservative but can miss findings. Stream lifecycle tracking is limited to direct fopen(), fclose(), fread(), and fwrite() calls; see E0043.
• Arbitrary loop invariants. Loops are unrolled to a configured bound; this finds bugs within that bound but does not prove an inductive invariant for all iterations.
• Arbitrary relationships between the lengths of different arrays. A key from one list is not assumed to index another list even when the source constructs them in parallel. The engine only uses relationships produced by modeled built-ins such as array_diff(), array_map(), and array_merge(), or by explicit guards and assertions.
• Concurrency and persistent-runtime behavior such as Swoole, RoadRunner, or ReactPHP.
• Builtin behavior whose result shape depends on an unmodeled flag. For example, count($value, COUNT_RECURSIVE) is not treated as a flat count, and array_slice() preserves list keys only when the flag is absent or provably false.
• Business, authorization, or security intent. Those properties need to be expressed as assertions or contracts before they can be checked.
• Properties whose values remain Unknown or unverified. With unknown_policy: report, a loop accumulator that is too unknown to model as a divisor is reported as unverified instead of being claimed safe. A numeric accumulator can still be proven nonzero by a subsequent guard such as $count > 0; a strict guard such as $count !== 0 remains unverified because the accumulator may be an integer or a float.

What it checks

• /, /=, and division inside expressions where the divisor can be zero
• Literal zero, symbolic zero, and zero reached through tracked arrays or expressions
• Guarded divisions, including if, switch, match, short-circuit &&, and try/catch/finally paths
• Loop exit values merged with the feasible zero-iteration path, so a counter initialized before a possibly empty loop is still considered possibly zero
• Constant-return, identity, and PHPDoc method/function summaries, including inherited and trait methods and imported class names
• Bounded integer ranges through direct same-class helper calls
• PHP literal array key rules, including duplicate keys and implicit keys after negative integer keys
• Exact array_keys() search lengths for tracked arrays passed directly as a variable, inline literal arrays, and simple array_filter() results. Simple arrow functions and single-return closures are modeled as filters; arbitrary callbacks, array_map()/array_values() results, and unknown comparisons fall back to an upper-bound length
• PHP literal key coercion for array_key() and array_keys(), including bool keys becoming 0/1, float keys being truncated to integers, and null becoming the empty string

Configuration

Each verification code has its own settings block. The relevant check is:

rules:
  E0031:
    php_version: "8.4"
    check_division: true

check_types controls PHPDoc @param/@var refinements. Native PHP type hints are always honoured. php_version is accepted for configuration compatibility; the modelled semantics are the same across PHP 8.0-8.4. loop_strategy: none limits loop bodies to one iteration; every other value uses unroll_depth. unknown_policy: report (the default) reports a solver unknown as an unverified finding so it cannot be mistaken for a proof; ignore suppresses that diagnostic.

Each verification code is enabled, disabled, and configured independently. Settings under E0031 apply only to division-by-zero checks; other codes do not inherit them.

Precision and recall benchmark

The supported_fragment_precision_and_recall test runs a labelled corpus of clean and buggy PHP cases through the verification family, then reports precision and recall for the supported fragment. The corpus includes division, modulo, intdiv(), array, string, nullability, return-contract, assertion, unreachable-code, switch, and loop zero-iteration cases. Dedicated benchmark fixtures live in src/rules/examples/e31/benchmark/.

Current result: 49 labelled cases and 50 expected findings, with 0 false positives and 0 false negatives (100% precision and recall). This is a regression benchmark for the supported fragment, not a random sample of arbitrary PHP projects. Run it with:

cargo test supported_fragment_precision_and_recall -- --nocapture

Pinned analyzer reference

The loop fixtures are database-independent: they take an iterable and never open a connection. Compare them with PHPStan 2.3.2, level max, and no baseline. The pinned configuration is src/rules/examples/e31/benchmark/phpstan.neon; run it with the pinned phar:

curl -L -o /tmp/phpstan-2.3.2.phar \
  https://github.com/phpstan/phpstan/releases/download/2.3.2/phpstan.phar
php /tmp/phpstan-2.3.2.phar analyse \
  --configuration=src/rules/examples/e31/benchmark/phpstan.neon \
  --no-progress --error-format=table

PHPStan does not report the division by zero on the feasible zero-iteration path. E0031 reports division-by-zero on the unguarded fixture and no finding on the guarded one.

For the list fixtures, PHPStan 2.3.2 at level max and Psalm 6.20.1 at errorLevel="1" both report the literal -1 access on non-empty-list<int>, but neither reports $items[count($items)] nor the for ($i = 0; $i <= count($items); $i++) access. E0036 reports all three.

This site is open source. Improve this page.