[wip]: dasSMT: solver-backed lint (SMT001-SMT008) + SFloat/SDouble; STYLE039 interval merge

[aleksisch]

Four commits: three grow the opt-in dasSMT module into a solver-backed lint, one adds a solver-free style rule that came out of the same work.

SFloat / SDouble over the Z3 FPA theory

smt_expr gains symbolic IEEE floats — the exact model of das float / double, unlike SReal (exact rational, no NaN). Rounded ops use round-nearest-ties-to-even, == is Z3_mk_fpa_eq rather than structural equality (so NaN == NaN is false and +0 == -0 is true, matching runtime), and model readback goes through the IEEE bit pattern so NaN, the infinities and negative zero survive it.

Int↔float conversions are provided but documented as a trap: unbounded Int → Real → FP is not decidable in practice — it times out on trivial goals.

SMT001 / SMT002 — reachability lint

modules/dasSMT/daslib/smt_lint.das is a [lint_macro] that symbolically executes each function body, accumulating a path condition, and asks Z3 whether each branch condition can hold on the paths that reach it. Nothing else in the tree tracks values across branches.

• SMT001 — a branch unsatisfiable on every path that reaches it.
• SMT002 — a condition always true with no else: a redundant guard. Default-off (noisy by nature), seeded via seed_default_disabled.

Only an UNSAT verdict is ever reported. Timeouts, unmodeled types, unproven integer overflow and anything the translation cannot represent all yield silence — the pass under-reports by construction rather than guessing.

SMT003–SMT008, plus three soundness fixes

Sweeping all 2748 .das files showed the pass was analyzing almost nothing, and trusting stale values where it did.

Coverage: a class method's body is with (self) { ... }, and ExprWith was not a statement the walker descended into — so every method body in the tree was skipped. daslib/perf_lint.das went from 0 if-nodes analyzed to 344; daslib/aot_cpp.das from 79 to 552.

Soundness (all three found only by sweeping real code):

• Method calls are ExprInvoke, not ExprCall, so out-params of methods were never havocked — one stale fact then poisoned every later guard in the function (23 false positives across three files).
• Arrays, tables and structs pass by reference without flags.ref set, so testing that flag missed arr |> push(x). Constness is the reliable signal.
• length(v) is memoized per container so two reads agree — but a mutated container's length changes under us, so volatile containers now get a fresh symbol per read.

New codes: division/modulo by a definitely-zero divisor (SMT003), an assert/verify that cannot hold when reached (SMT004), a while whose body never runs (SMT005), a shift count outside 0..31 (SMT006), a definitely-negative subscript (SMT007), and a &&/|| condition that is constant whatever its inputs are (SMT008, judged on a second solver carrying no path condition — always-true-on-its-own is a defect, so it is default-on, unlike the context-relative SMT002).

Each asks "is this ALWAYS broken here", never "could it be" — a merely-possible zero divisor would fire on every unconstrained value.

STYLE039 — condition collapses to a single comparison

x != 1 && x > 0 is x >= 2, and nothing detected that. Solver-free, so unlike the SMT rules it needs no opt-in module and runs in every build and under the CI zero-warning gate.

The &&/||/! tree is evaluated on an interval lattice — the domain LLVM's ConstantRange and Clang's RangeConstraintManager use — and reported only when the result is one one-sided interval, a single point, or the complement of a point. Not subsumption: in x != 1 && x > 0 neither operand implies the other, so dropping an implied literal cannot find it; Z3's own ctx-solver-simplify leaves the pair untouched. Endpoints are int64 so c ± 1 cannot wrap at an int boundary.

Measured over daslib, utils, modules, tests, tutorials, examples and dastest: zero findings — quiet rather than noisy, which is why it is default-on.

Testing

• modules/dasSMT/tests/smt_lint_check.das — fixture driver; each fixture marks expected findings with a trailing // smt_expect <CODE> and the driver fails on both a missed detection and an unexpected one. 7/7, 3/3, 10/10 across the three fixtures. Wired into CMake as an interpreted example run.
• utils/lint/tests/style039_condition_interval_merge.das — expect 31209:5; the full lint fixture suite is 63/63.
• Lint on every changed .das: 0 issues. Full build, tests/ suite (12144 passed / 0 failed), das2rst regeneration and a Sphinx -W build all clean locally.

Notes for review

• The SMT pass runs after optimization, and the optimizer rewrites if (c) { return x } / return y into a ternary — leaving no if-node. Guard-style findings therefore need no_optimizations, the way utils/lint/main.das and the fixture driver compile their inputs. utils/lint/main.das does not run this pass at all: it cannot require an opt-in module.
• Soundness limits and the query budget (250 ms/query, 200 queries/function, depth 64, all overridable per module) are documented in modules/dasSMT/README.md.
• The style rule is numbered 039 because 036–038 landed on master while this branch was open.

🤖 Generated with Claude Code