dasSMT: solver-backed lint (SMT001-SMT008) + SFloat/SDouble; STYLE042 interval merge

CLAUDE.md

@@ -274,6 +274,7 @@ diagnostic in any tier.
 | `def f(var why : string)` written on a path but never read | `var why : string&` - a by-value copy's write never reaches the caller | LINT023 |
 | bare `resize(need)` on an input-scaled buffer (frames, pixels, vocab) | declare it `@exact_size`; then `reserve`/`ensure_capacity` before every `resize` (or size it through `reserve_resize`-style helpers) | PERF032 - the annotation is a lint contract; the guard panics only when the big input arrives |
 | `-const` `-&` `-[]` `-#` `==const` `==&` on a **concrete** cast target | drop the contract | STYLE036: substitution contracts act only while a generic binds - inert on concrete targets |
+| `if (x != 1 && x > 0)` / `if (x > 5 && x > 3)` (one `int` variable) | `if (x >= 2)` / `if (x >= 6)` | STYLE042: the `&&`/`\|\|`/`!` tree is evaluated on an interval lattice, so comparisons that *merge* - not merely subsume - collapse. Silent on two-sided ranges, disjoint unions, >1 variable, non-`int`, already-single comparisons |
 | `slice(s, i, j)` / `chop(s, i, n)` in a loop over an outer string | `peek_data(s) $(d)` and slice the view | PERF031: each call re-strlens the whole source - O(n^2); every haystack op has a byte-view twin |
 
 For path/filename ops use `fio` helpers (`base_name`/`dir_name`/`path_join`/...) - see `skills/daslang/references/files-and-paths.md`. Never hand-roll `rfind("/")` + slice: misses Windows separators.

daslib/lint_config.das

@@ -110,10 +110,12 @@ def public load_lint_config_from_path(path : string; var disabled_codes : table<
     }
 }
 
-//! Seeds ``disabled_codes`` with the canonical default-off rule set (currently just STYLE005). Call before ``load_lint_config`` so that a ``STYLE005 = true`` directive in ``.lint_config`` can re-enable it.
+//! Seeds ``disabled_codes`` with the canonical default-off rule set (STYLE005, and SMT002 from the opt-in ``smt`` module). Call before ``load_lint_config`` so that a ``STYLE005 = true`` directive in ``.lint_config`` can re-enable it.
 def public seed_default_disabled(var disabled_codes : table<string>) : void {
-    if (!key_exists(disabled_codes, "STYLE005")) {
-        disabled_codes |> insert("STYLE005")
+    for (code in ["STYLE005", "SMT002"]) {
+        if (!key_exists(disabled_codes, code)) {
+            disabled_codes |> insert(code)
+        }
     }
 }
 

daslib/style_lint.das

@@ -48,6 +48,7 @@ module style_lint shared private
 //!   STYLE040 — a run of statements duplicated elsewhere in the module that a helper function could absorb (on by default under daslib/ and utils/, override per module with 'options _duplicate_regions'; thresholds via 'options _dupe_min_nodes' / '_dupe_min_statements'; suppress with '// nolint:STYLE040' on the reported line)
 //!   STYLE039 — non-ASCII byte in a string literal (on by default under daslib/ and modules/, override per module with 'options _ascii_strings'; suppress with '// nolint:STYLE039') — emitted strings and error messages must be ASCII unless intended
 //!   STYLE041 — bool flag initialized false, set true on terminal paths, then consumed by a single 'if (flag) return ...' — a return value in disguise; return directly at each set site (walk-abort callbacks, negative polarity, non-terminal sets, and init-true flags are exempt)
+//!   STYLE042 — a &&/||/! condition over one int variable that an interval lattice collapses to a single comparison ('x != 1 && x > 0' is 'x >= 2')
 
 require daslib/ast_boost
 require daslib/dupe_detect
@@ -56,6 +57,16 @@ require daslib/lint_config
 require math
 require strings
 
+let private INT64_MIN_V = -9223372036854775807l - 1l
+let private INT64_MAX_V = 9223372036854775807l
+
+// One inclusive interval of the STYLE042 value lattice. int64 endpoints so `c - 1`
+// and `c + 1` cannot wrap at an int boundary.
+struct private Ivl {
+    lo : int64
+    hi : int64
+}
+
 // STYLE033 arity caps — never suggest a call shape with no matching overload.
 let MAX_CONCAT_ARITY = 8
 let MAX_VARIADIC_PUSH_ARITY = 4
@@ -879,9 +890,201 @@ class StyleLintVisitor : AstVisitor {
         return null
     }
 
+    // --- STYLE042: a condition equivalent to one simpler comparison ---
+    // Interval lattice over one int variable: && intersects, || unites, ! complements.
+    // Why subsumption misses it: doc/source/reference/language/lint.rst.
+
+    def private ivl_full() : array<Ivl> {
+        var r : array<Ivl>
+        r |> push(Ivl(lo = INT64_MIN_V, hi = INT64_MAX_V))
+        return <- r
+    }
+
+    //! Value set for `x <op> c`, as a sorted list of disjoint inclusive intervals.
+    def private ivl_from_cmp(op : string; c : int64) : array<Ivl> {
+        var r : array<Ivl>
+        if (op == "==") {
+            r |> push(Ivl(lo = c, hi = c))
+        } elif (op == "!=") {
+            if (c > INT64_MIN_V) {
+                r |> push(Ivl(lo = INT64_MIN_V, hi = c - 1l))
+            }
+            if (c < INT64_MAX_V) {
+                r |> push(Ivl(lo = c + 1l, hi = INT64_MAX_V))
+            }
+        } elif (op == "<") {
+            if (c > INT64_MIN_V) {
+                r |> push(Ivl(lo = INT64_MIN_V, hi = c - 1l))
+            }
+        } elif (op == "<=") {
+            r |> push(Ivl(lo = INT64_MIN_V, hi = c))
+        } elif (op == ">") {
+            if (c < INT64_MAX_V) {
+                r |> push(Ivl(lo = c + 1l, hi = INT64_MAX_V))
+            }
+        } elif (op == ">=") {
+            r |> push(Ivl(lo = c, hi = INT64_MAX_V))
+        }
+        return <- r
+    }
+
+    def private ivl_isect(a, b : array<Ivl>) : array<Ivl> {
+        var r : array<Ivl>
+        for (x in a) {
+            for (y in b) {
+                let lo = max(x.lo, y.lo)
+                let hi = min(x.hi, y.hi)
+                if (lo <= hi) {
+                    r |> push(Ivl(lo = lo, hi = hi))
+                }
+            }
+        }
+        return <- ivl_normalize(r)
+    }
+
+    def private ivl_unite(a, b : array<Ivl>) : array<Ivl> {
+        var r : array<Ivl> // nolint:STYLE033 — concat would pull daslib/linq into this module
+        r |> push_from(a)
+        r |> push_from(b)
+        return <- ivl_normalize(r)
+    }
+
+    // sort by lo, then merge overlapping or adjacent runs
+    def private ivl_normalize(var v : array<Ivl>) : array<Ivl> {
+        var out : array<Ivl>
+        if (empty(v)) return <- out
+        v |> sort() $(p, q) => p.lo < q.lo
+        var cur = v[0]
+        for (i in range(1, length(v))) {
+            let nx = v[i]
+            if (nx.lo <= cur.hi || (cur.hi < INT64_MAX_V && nx.lo == cur.hi + 1l)) {
+                cur = Ivl(lo = cur.lo, hi = max(cur.hi, nx.hi))
+            } else {
+                out |> push(cur)
+                cur = nx
+            }
+        }
+        out |> push(cur)
+        return <- out
+    }
+
+    def private ivl_invert(a : array<Ivl>) : array<Ivl> {
+        var r : array<Ivl>
+        var at = INT64_MIN_V
+        var first = true
+        for (x in a) {
+            if (x.lo > at || (first && x.lo > INT64_MIN_V)) {
+                if (x.lo > INT64_MIN_V && at <= x.lo - 1l) {
+                    r |> push(Ivl(lo = at, hi = x.lo - 1l))
+                }
+            }
+            first = false
+            if (x.hi >= INT64_MAX_V) return <- ivl_normalize(r)
+            at = x.hi + 1l
+        }
+        r |> push(Ivl(lo = at, hi = INT64_MAX_V))
+        return <- ivl_normalize(r)
+    }
+
+    //! The simplest single comparison equal to this value set, or "" when none is.
+    def private ivl_render(a : array<Ivl>; vname : string) : string {
+        if (length(a) == 1) {
+            let x = a[0]
+            if (x.lo == INT64_MIN_V && x.hi == INT64_MAX_V) return ""       // STYLE010's job
+            if (x.lo == x.hi) return "{vname} == {x.lo}"
+            if (x.lo == INT64_MIN_V) return "{vname} <= {x.hi}"
+            if (x.hi == INT64_MAX_V) return "{vname} >= {x.lo}"
+            return ""                                                       // two-sided
+        }
+        // exactly one hole is `!=`
+        if (length(a) == 2 && a[0].lo == INT64_MIN_V && a[1].hi == INT64_MAX_V
+            && a[1].lo - a[0].hi == 2l) {
+            return "{vname} != {a[0].hi + 1l}"
+        }
+        return ""
+    }
+
+    // A comparison leaf `v <op> const` (or the Yoda form). Returns false for any other
+    // shape, or for a second distinct variable — the lattice is single-variable.
+    def private style042_leaf(e : Expression? const; var vr : Variable?&; var vs : array<Ivl>) : bool {
+        let ex = peel_ref2value_const(e)
+        if (ex == null || !(ex is ExprOp2)) return false
+        let o2 = ex as ExprOp2
+        var op = "{o2.op}"
+        var lhs = peel_ref2value_const(o2.left)
+        var rhs = peel_ref2value_const(o2.right)
+        if (lhs == null || rhs == null) return false
+        var cval = 0l
+        var v : Variable? = null
+        if (lhs is ExprVar && rhs is ExprConstInt) {
+            v = (lhs as ExprVar).variable
+            cval = int64((rhs as ExprConstInt).value)
+        } elif (rhs is ExprVar && lhs is ExprConstInt) {
+            v = (rhs as ExprVar).variable
+            cval = int64((lhs as ExprConstInt).value)
+            if (op == "<") {
+                op = ">"
+            } elif (op == "<=") {
+                op = ">="
+            } elif (op == ">") {
+                op = "<"
+            } elif (op == ">=") {
+                op = "<="
+            }
+        } else {
+            return false
+        }
+        if (v == null || v._type == null || v._type.baseType != Type.tInt
+            || (op != "==" && op != "!=" && op != "<" && op != "<=" && op != ">" && op != ">=")
+            || (vr != null && vr != v)) return false
+        vr = v
+        vs <- ivl_from_cmp(op, cval)   // nolint:PERF030 — out-param; every caller hands in a freshly declared empty array
+        return true
+    }
+
+    // Folds the &&/||/! tree into one value set. leaves counts the comparisons seen, so
+    // a single comparison is never "simplified" into itself.
+    def private style042_eval(e : Expression? const; var vr : Variable?&;
+                              var leaves : int&; var vs : array<Ivl>) : bool {
+        let ex = peel_ref2value_const(e)
+        if (ex == null) return false
+        if (ex is ExprOp1 && "{(ex as ExprOp1).op}" == "!") {
+            var inner : array<Ivl>
+            if (!style042_eval((ex as ExprOp1).subexpr, vr, leaves, inner)) return false
+            vs <- ivl_invert(inner)   // nolint:PERF030 — out-param, empty on entry
+            return true
+        }
+        if (ex is ExprOp2) {
+            let op = "{(ex as ExprOp2).op}"
+            if (op == "&&" || op == "||") {
+                var l : array<Ivl>
+                var r : array<Ivl>
+                if (!style042_eval((ex as ExprOp2).left, vr, leaves, l)
+                    || !style042_eval((ex as ExprOp2).right, vr, leaves, r)) return false
+                vs <- op == "&&" ? ivl_isect(l, r) : ivl_unite(l, r)   // nolint:PERF030 — out-param, empty on entry
+                return true
+            }
+        }
+        if (!style042_leaf(ex, vr, vs)) return false
+        leaves++
+        return true
+    }
+
+    def private check_style042(ifte : ExprIfThenElse?) : void {
+        var vr : Variable? = null
+        var leaves = 0
+        var vs : array<Ivl>
+        if (!style042_eval(ifte.cond, vr, leaves, vs) || leaves < 2 || vr == null) return
+        let simpler = ivl_render(vs, "{vr.name}")
+        if (!empty(simpler)) {
+            style_warning("STYLE042: this condition is equivalent to '{simpler}'; the comparisons collapse over the integers", ifte.at)
+        }
+    }
+
     def override preVisitExprIfThenElse(ifte : ExprIfThenElse?) : void {
         if (ifte.if_flags.isStatic || ifte.genFlags.generated) return
         st037_bump()
+        check_style042(ifte)
         var cond = ifte.cond
         if (cond is ExprConstBool) {
             var cbool = cond as ExprConstBool

doc/source/reference/language/lint.rst

@@ -3189,6 +3189,70 @@ set site, and any reference the analysis cannot classify — a capture, a
 Init-``true`` separator flags never match. Suppress a deliberate keep with
 ``// nolint:STYLE041`` on the declaration line.
 
+STYLE042 — condition collapses to a single comparison
+======================================================
+
+A chain of comparisons on one ``int`` variable often describes a simpler range
+than it looks::
+
+    // Bad
+    if (x != 1 && x > 0) { ... }      // STYLE042
+    if (x > 5 && x > 3)  { ... }      // STYLE042
+    if (x > 0 && x < 2)  { ... }      // STYLE042
+
+    // Good
+    if (x >= 2) { ... }
+    if (x >= 6) { ... }
+    if (x == 1) { ... }
+
+This is **not** a redundant operand: in ``x != 1 && x > 0`` neither operand
+implies the other, so subsumption cannot find it. The merge is an integer-range
+fact — ``x > 0`` and ``x != 1`` leave exactly ``x >= 2``.
+
+The rule evaluates the ``&&`` / ``||`` / ``!`` tree on an interval lattice, the
+same domain LLVM's ``ConstantRange`` and Clang's ``RangeConstraintManager`` use:
+each comparison becomes a set of allowed values (``x > 0`` is ``[1, MAX]``,
+``x != 1`` is ``[MIN, 0] + [2, MAX]``), ``&&`` intersects, ``||`` unites, ``!``
+complements. If the result is one interval bounded on a single side, one point,
+or the complement of one point, it is reported as that comparison. No solver
+involved.
+
+Silent when: the result is a genuine two-sided range or two disjoint intervals
+(no single comparison is equivalent), more than one variable appears, the
+condition is already a single comparison, or the operands are not ``int``. An
+always-true condition belongs to STYLE010, not here.
+
+------------------------------------------------------
+SMT001–SMT008 — solver-backed reachability and defects
+------------------------------------------------------
+
+Eight further codes live outside this module, in the opt-in ``smt`` module
+(``-DDAS_SMT_DISABLED=OFF``), because they need a Z3 solver:
+
+* ``SMT001`` — a branch whose condition is unsatisfiable on every path that
+  reaches it.
+* ``SMT002`` — a condition that is always true with no ``else``: a redundant
+  guard. Default-off, seeded by ``seed_default_disabled``.
+* ``SMT003`` — division or modulo whose divisor is zero on every path reaching it.
+* ``SMT004`` — an ``assert``/``verify`` that cannot hold when reached.
+* ``SMT005`` — a ``while`` whose body can never run.
+* ``SMT006`` — a shift count outside ``0..31`` on every path reaching it.
+* ``SMT007`` — a subscript whose index is always negative.
+* ``SMT008`` — a ``&&``/``||`` condition that is constant whatever its inputs
+  are (the operands contradict, or the author meant the other operator).
+
+They are produced by ``modules/dasSMT/daslib/smt_lint.das``, report under the
+same ``31209`` code as the style rules, and honor ``// nolint:SMT001``. Unlike
+every rule above, they track values across branches: a symbolic executor
+accumulates a path condition and asks the solver whether each branch can hold.
+
+``utils/lint/main.das`` does **not** run them — it cannot ``require`` an opt-in
+module. Enable them with ``require smt/daslib/smt_lint``, and note that
+guard-style findings need optimizations off (the optimizer rewrites
+``if (c) { return x }`` / ``return y`` into a ternary, leaving no if-node to
+analyze). See ``modules/dasSMT/README.md`` for the soundness limits and the
+query budget.
+
 -----
 Tests
 -----
@@ -3203,4 +3267,5 @@ Lint tests are in ``utils/lint/tests/``::
     ``daslib/perf_lint.das`` (performance lint source),
     ``daslib/style_lint.das`` (style lint source),
     ``daslib/dupe_detect.das`` (STYLE040 duplicate-region engine),
+    ``modules/dasSMT/daslib/smt_lint.das`` (SMT reachability lint source),
     ``utils/lint/main.das`` (unified standalone utility)

modules/dasSMT/.das_module

@@ -5,7 +5,7 @@ require daslib/fio
 [export]
 def initialize(project_path : string) {
     let daslib_paths = [
-        "smt_boost", "smt_expr", "smt_macro"
+        "smt_boost", "smt_expr", "smt_macro", "smt_lint"
     ]
     let bindings_paths = [
         "z3_const", "z3_enum", "z3_func", "z3_struct"

modules/dasSMT/CMakeLists.txt

@@ -144,5 +144,6 @@ struct.pack_into('<qQ',d,o+z[0]*16,16,0); open(sys.argv[1],'wb').write(d)
     ADD_EXAMPLE_RUN(modules/dasSMT/examples/entity_placement.das)
     ADD_EXAMPLE_RUN(modules/dasSMT/examples/theorems.das)
     ADD_EXAMPLE_RUN(modules/dasSMT/examples/smt_fn_errors.das FALSE)
+    ADD_EXAMPLE_RUN(modules/dasSMT/tests/smt_lint_check.das FALSE)
 
 ENDIF()