Skip to content

engine: print_eqn emits stacked unary negatives (--x) that the equation parser rejects #863

Description

@bpowers

Problem

crate::ast::print_eqn and the equation parser (Expr0::new, LexerType::Equation) disagree on stacked unary negatives, so print_eqn can emit XMILE equation text that does not round-trip through the parser.

Minimal repro AST:

Expr0::Op1(Negative, Op1(Negative, App("pi", [])))

print_eqn serializes this as --pi(), but Expr0::new rejects --pi(). The printer is therefore not a total inverse of the parser: for a doubly-negated sub-expression it produces text the parser will not accept.

This is a property of the shared AST printer + equation parser -- independent of the MDL writer (it is not about mdl_bare_keyword / PI() rendering as in #850; the pi() in the repro is incidental, any inner expression triggers it).

Why it matters

Defense-in-depth / correctness of the printer<->parser contract. print_eqn output is expected to re-parse to an equivalent AST. Any consumer that serializes an AST via print_eqn and re-parses (round-trip harnesses, the MDL writer's equation_to_mdl re-parse fallback, potential future tooling) can be tripped by such an AST.

Impact / reachability

Effectively unreachable from real models today. Every stored datamodel equation originated from the parser, which never produces stacked -- (a leading -- is rejected at parse time), so no real equation's AST can contain Op1(Negative, Op1(Negative, _)). The concern is a latent printer/parser asymmetry, not a live data-corruption bug.

  • On the MDL-writer side specifically, equation_to_mdl falls back to raw text when it cannot re-parse. In principle that path could leak unparseable XMILE into MDL output for such an equation -- but since the offending AST cannot arise from a real datamodel equation, this is not reachable in production.

How it was discovered

Surfaced by the MDL-writer property tests (branch `mdl-writer-hardening`, `src/simlin-engine/src/mdl/writer_proptest.rs`). The proptest currently works around it with a `prop_filter` that restricts generated ASTs to those whose `print_eqn` output re-parses.

Component(s)

  • `src/simlin-engine/src/ast.rs` (`print_eqn`)
  • the equation parser (`Expr0::new`, `LexerType::Equation`)

Possible approaches

  • Make `print_eqn` parenthesize or space stacked unary negatives, e.g. emit `-(-x)` instead of `--x`; or
  • Make the equation parser accept `--x` (stacked unary minus).

Either fixes the round-trip contract; the printer-side change is the more conservative option. Once fixed, the `prop_filter` workaround in `writer_proptest.rs` can be removed.

Severity

Low (unreachable from real models; defense-in-depth for the printer/parser contract).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions