det: a float zero divisor is libcob's NaN; a phrase binds to the innermost open statement (#4675, #4676)

docs/language_status/oracle_assumptions.md

@@ -476,8 +476,22 @@ verdict, but it limits what the proof says about inputs outside the scenarios.
   `tests/cobol_mainframe/test_det_size_error.py` (every shape above, both port modes) and a randomized differential
   run (2026-10-07: 56 random programs with zero divisors, DIVIDE and ON SIZE ERROR / NOT ON SIZE ERROR phrases,
   every output equal to the oracle's).
-- **Not modelled.** A zero divisor in floating point (COMP-1 / COMP-2, `Hfp.divide`) still stops the run with an
-  ArithmeticException, a named stop rather than a guess.
+- **Floating point (#4675).** The oracle converts a COMP-1 / COMP-2 operand to a decimal, so a zero divisor behaves
+  as above (measured 2026-10-08): `COMPUTE G = F / FZ`, `DIVIDE FZ INTO G`, `DIVIDE F BY FZ GIVING G` (or a decimal
+  receiver) leave every receiver unchanged and raise the size error, with or without ON SIZE ERROR; ON SIZE ERROR
+  also fires for a decimal receiver too small for a float result (`R = F * 3000`). The det runtime does the same for
+  a division that is the statement's whole value (`Hfp.divide` returns the NaN and raises the size error; the float
+  statements now take ON SIZE ERROR phrases, an HFP exponent overflow is still refused by name). A zero divisor
+  inside a larger float expression is NOT modelled: the oracle's `cob_decimal_align` meets the NaN there
+  (`(F / FZ) * 3` is unchanged but `(F / FZ) * C`, `FM * (F / FZ)` store 0, `2 - (F / FZ)` stores 2) and the HFP model
+  does not replay it, so `Hfp.divideNested` stops the run with an ArithmeticException, a named stop rather than a guess.
+  z/OS leaves the result of a floating-point zero divide undefined (a floating-point exception or a program-defined
+  result), so the oracle's "unchanged" is the same kind of choice as for decimal items.
+- **Phrase scope (#4676).** A conditional phrase belongs to the innermost unterminated statement that can take it,
+  and an END-verb closes the innermost open statement of its verb (measured: `COMPUTE ... ON SIZE ERROR COMPUTE ...
+  NOT ON SIZE ERROR ...` gives the NOT phrase to the inner COMPUTE; with an inner ON/NOT pair of its own the next NOT
+  goes to the outer). `det/stmt.py` binds them that way (`_phrase_owner`, `_end_owner`). A NOT phrase after a
+  statement that already has one, or after a finished one, goes outward; cobc rejects a stray one with a syntax error.
 - **So a proof says:** for a scenario that divides by zero without ON SIZE ERROR, the port does what the oracle
   does (receivers unchanged), which z/OS does not promise: IBM leaves the result undefined and a z/OS run may
   abend. With ON SIZE ERROR both sides agree with IBM (receivers unchanged, the phrase runs), except `0 ** -n`,

gitgalaxy/tools/cobol_to_java/det/cobolrt/Cobol.java

@@ -87,7 +87,7 @@ public static boolean isNan(BigDecimal d) {
         return d.scale() == NAN_SCALE;
     }
 
-    private static BigDecimal nan(BigDecimal d) {
+    static BigDecimal nan(BigDecimal d) {
         return new BigDecimal(d.unscaledValue(), NAN_SCALE);
     }
 
@@ -104,7 +104,7 @@ public static boolean sizeRaised() {
         return SIZE_EC.get()[0];
     }
 
-    private static void raiseSize() {
+    static void raiseSize() {
         SIZE_EC.get()[0] = true;
     }
 

gitgalaxy/tools/cobol_to_java/det/cobolrt/Hfp.java

@@ -216,13 +216,22 @@ public static BigDecimal multiply(BigDecimal a, BigDecimal b, boolean longP) {
         return h == null ? BigDecimal.ZERO : value(h, d);
     }
 
-    /** DIVIDE: the exact quotient truncated. A zero divisor: an ArithmeticException, not modelled in floating point
-     *  (oracle_assumptions C14; Cobol.divide gives libcob's NaN). */
+    /** DIVIDE: the exact quotient truncated. A zero divisor is libcob's NaN with the size error raised, as in
+     *  Cobol.divide (#4675, oracle_assumptions C14): the oracle converts a float to a decimal and divides it, so a
+     *  receiver is left unchanged; z/OS leaves the result undefined. Only a division that is a statement's whole
+     *  value (COMPUTE x = a / b, DIVIDE): inside a larger expression divideNested refuses. */
     public static BigDecimal divide(BigDecimal a, BigDecimal b, boolean longP) {
+        if (b.signum() == 0) {
+            Cobol.raiseSize();
+            return Cobol.nan(a);
+        }
         int d = digits(longP);
         H x = exact(a, d);
         H y = exact(b, d);
-        if (y == null) throw new ArithmeticException("division by zero");
+        if (y == null) { // a divisor that is HFP zero
+            Cobol.raiseSize();
+            return Cobol.nan(a);
+        }
         if (x == null) return BigDecimal.ZERO;
         // (fx 16^(ex-d)) / (fy 16^(ey-d)) = (fx / fy) 16^(ex-ey)
         BigInteger num = x.f;
@@ -234,6 +243,18 @@ public static BigDecimal divide(BigDecimal a, BigDecimal b, boolean longP) {
         return value(h, d);
     }
 
+    /** DIVIDE inside a larger floating-point expression: a zero divisor is refused by name. The oracle's NaN meets
+     *  cob_decimal_align there (NaN * x is 0, 2 - NaN is 2, NaN + 1 unchanged: measured, #4675) and the HFP model
+     *  does not replay that (oracle_assumptions C14). */
+    public static BigDecimal divideNested(BigDecimal a, BigDecimal b, boolean longP) {
+        if (b.signum() == 0) {
+            throw new ArithmeticException("division by zero inside a floating-point expression (oracle_assumptions C14)");
+        }
+        BigDecimal q = divide(a, b, longP);
+        if (Cobol.isNan(q)) throw new ArithmeticException("division by zero inside a floating-point expression (oracle_assumptions C14)");
+        return q;
+    }
+
     // ------------------------------------------------------------------------------------------- storage
 
     /** The item's bytes as an exact value. An unnormalized fraction reads as its value too. */

gitgalaxy/tools/cobol_to_java/det/gen.py

@@ -170,6 +170,7 @@ def __init__(self, prog: Program, structured: bool = False):
         # it (a group holding it, a REDEFINES) -- is refused by name: HFP on z/OS, IEEE on the oracle (register C6)
         self._value_use = 0  # > 0 while value_field asks
         self._init_bytes = 0  # > 0 inside INITIALIZE: a group is walked to its elementary items, never copied
+        self.float_top: int = 0  # id of the COMPUTE expression whose own division may be libcob's NaN (#4675)
         self.fmode: str | None = None  # "LONG" / "SHORT" while num() generates a floating-point expression
         self.float_extents: dict[int, list] = {}  # storage root id -> [(item, first extent, full extent, tables)]
         self.root_of: dict[int, int] = {}  # id(record) -> id(its storage root)
@@ -536,6 +537,9 @@ def fnum(self, e) -> str:
                     "bit; oracle_assumptions.md C6)"
                 )
             fn = {"+": "add", "-": "subtract", "*": "multiply", "/": "divide"}[e.op]
+            literal = isinstance(e.right, E.Lit) and isinstance(e.right.value, Decimal) and e.right.value != 0
+            if fn == "divide" and id(e) != self.float_top and not literal:
+                fn = "divideNested"  # a zero divisor inside a larger expression: refused at run time (#4675)
             return f"Hfp.{fn}({self.fnum(e.left)}, {self.fnum(e.right)}, {lng})"
         if isinstance(e, E.LengthOf):
             with self.floating(None):
@@ -1688,20 +1692,22 @@ def _statement(self, s: S.Stmt, ind: str) -> list[str]:
         if k == "COMPUTE":
             mode = self.float_mode([s.data["expr"]], [t for t, _ in s.data["targets"]])
             if mode is not None:
-                self.float_statement(s, s.data["targets"])
+                self.float_statement(s.data["targets"])
             self.p_scaled_expr(s.data["expr"], False)
             plan = self.plan_arith(s.data["expr"], [t for t, _ in s.data["targets"]])
             plan = {} if mode is not None else plan
+            self.float_top = id(s.data["expr"]) if mode is not None else 0
             with self.floating(mode), self.osvs_plan(plan):
                 value = self.num(s.data["expr"])
-            return [c, *self.store_all(s, s.data["targets"], value, ind, s.data["expr"] if mode is None else None)]
+            self.float_top = 0
+            return [c, *self.store_all(s, s.data["targets"], value, ind, s.data["expr"])]
         if k == "ARITH":
             d = s.data
             receivers = [t for t, _ in d.get("targets") or []] + [t for t, _ in d.get("giving") or []]
             receivers += [d["remainder"]] if d.get("remainder") is not None else []
             mode = self.float_mode(d["operands"], receivers, d["op"] in ("*", "*="))
             if mode is not None:
-                self.float_statement(s, list(d.get("targets") or []) + list(d.get("giving") or []))
+                self.float_statement(list(d.get("targets") or []) + list(d.get("giving") or []))
                 if d.get("remainder") is not None:
                     raise Untranslatable(f"DIVIDE REMAINDER in floating point ({FLOAT_BYTES})")
                 with self.floating(mode):
@@ -1914,11 +1920,9 @@ def display_operand(self, o) -> str:
             return self.text(o)
         raise Untranslatable(f"DISPLAY of {type(o).__name__}")
 
-    def float_statement(self, s: S.Stmt, targets: list) -> None:
-        """What a floating-point statement does not model: ON SIZE ERROR (HFP exponent overflow and underflow are
-        refused by name in the runtime) and ROUNDED into a float (its precision is the rounding)."""
-        if "SIZE-ERROR" in s.phrases or "NOT-SIZE-ERROR" in s.phrases:
-            raise Untranslatable(f"ON SIZE ERROR in a floating-point statement ({FLOAT_BYTES})")
+    def float_statement(self, targets: list) -> None:
+        """What a floating-point statement does not model: ROUNDED into a float (its precision is the rounding).
+        HFP exponent overflow and underflow are refused by name in the runtime; a zero divisor is libcob's NaN (#4675)."""
         for t, rounded in targets:
             if rounded and self.float_item(t) is not None:
                 raise Untranslatable(f"ROUNDED into {t.name}, a floating-point item ({FLOAT_BYTES})")
@@ -1938,19 +1942,42 @@ def arith_float(self, s: S.Stmt, ind: str) -> list[str]:
             else:
                 fn = "multiply" if op == "*" else "divide"
                 val = f"Hfp.{fn}({self.fnum(ops[0])}, {self.fnum(ops[1])}, {lng})"
-            return self.store_all(s, d["giving"], val, ind)
+            nanx = E.Bin("/", ops[0], ops[1]) if op == "/" else None  # a zero divisor: libcob's NaN (#4675)
+            return self.store_all(s, d["giving"], val, ind, nanx)
         total = self.fnum(ops[0]) if ops else "BigDecimal.ZERO"
         for o in ops[1:]:
             total = f"Hfp.add({total}, {self.fnum(o)}, {lng})"
         tsum = self.tmpname("t")
         out = [f"{ind}BigDecimal {tsum} = {total};"]
+        checked = "SIZE-ERROR" in s.phrases or "NOT-SIZE-ERROR" in s.phrases
+        err = self.tmpname("sizeError")
+        if checked:
+            out.append(f"{ind}boolean {err} = false;")
         for tgt, rounded in d["targets"]:
             if not isinstance(tgt, E.Ref):
                 raise Untranslatable("arithmetic target is not a data item")
             cur = self.fnum(tgt)
             val = {"+=": f"Hfp.add({cur}, {tsum}, {lng})", "-=": f"Hfp.subtract({cur}, {tsum}, {lng})",
                    "*=": f"Hfp.multiply({tsum}, {cur}, {lng})", "/=": f"Hfp.divide({cur}, {tsum}, {lng})"}[op]  # fmt: skip
-            out.append(ind + self.store_into(tgt, val, rounded))
+            if checked:
+                out.append(f"{ind}{err} |= Cobol.storeChecked({self.value_field(tgt)}, {val}, {_b(rounded)}, CS);")
+            elif op == "/=":  # a zero divisor: libcob's NaN, the target unchanged (#4675)
+                qv = self.tmpname("q")
+                out += [
+                    f"{ind}BigDecimal {qv} = {val};",
+                    f"{ind}if (!Cobol.isNan({qv})) {self.store_into(tgt, qv, rounded)}",
+                ]
+            else:
+                out.append(ind + self.store_into(tgt, val, rounded))
+        if checked:
+            if "SIZE-ERROR" in s.phrases:
+                out += [f"{ind}if ({err}) {{", *self.phrase_block(s.phrases["SIZE-ERROR"], ind + "    "), f"{ind}}}"]
+            if "NOT-SIZE-ERROR" in s.phrases:
+                out += [
+                    f"{ind}if (!{err}) {{",
+                    *self.phrase_block(s.phrases["NOT-SIZE-ERROR"], ind + "    "),
+                    f"{ind}}}",
+                ]
         return out
 
     def store_all(self, s: S.Stmt, targets: list, value: str, ind: str, expr=None, after=None) -> list[str]:
@@ -1976,14 +2003,19 @@ def store_all(self, s: S.Stmt, targets: list, value: str, ind: str, expr=None, a
         out.append(f"{ind}BigDecimal {v} = {value};")
         out.append(f"{ind}boolean {err} = {'Cobol.sizeRaised()' if sized else 'false'};")
         for t, rounded in targets:
-            out.append(f"{ind}{err} |= Cobol.storeChecked({self.field_expr(t)}, {v}, {_b(rounded)}, CS);")
+            out.append(f"{ind}{err} |= Cobol.storeChecked({self.value_field(t)}, {v}, {_b(rounded)}, CS);")
         out += after(v) if after else []
         if "SIZE-ERROR" in s.phrases:
-            out += [f"{ind}if ({err}) {{", *self.block(s.phrases["SIZE-ERROR"], ind + "    "), f"{ind}}}"]
+            out += [f"{ind}if ({err}) {{", *self.phrase_block(s.phrases["SIZE-ERROR"], ind + "    "), f"{ind}}}"]
         if "NOT-SIZE-ERROR" in s.phrases:
-            out += [f"{ind}if (!{err}) {{", *self.block(s.phrases["NOT-SIZE-ERROR"], ind + "    "), f"{ind}}}"]
+            out += [f"{ind}if (!{err}) {{", *self.phrase_block(s.phrases["NOT-SIZE-ERROR"], ind + "    "), f"{ind}}}"]
         return out
 
+    def phrase_block(self, body: list, ind: str) -> list[str]:
+        """A SIZE ERROR phrase's statements: their own arithmetic mode, never the statement's (#4675)."""
+        with self.floating(None):
+            return self.block(body, ind)
+
     def store_into(self, t: E.Ref, value: str, rounded: bool) -> str:
         """An arithmetic result (no ON SIZE ERROR) stored in a target: a lifted binary item through Cobol.binary."""
         lt = self.lift(t)
@@ -2060,9 +2092,13 @@ def after(v, q=q):
                 out.append(f"{ind}Cobol.store({f}, {val}, {_b(rounded)}, CS);")
         if checked:
             if "SIZE-ERROR" in s.phrases:
-                out += [f"{ind}if ({err}) {{", *self.block(s.phrases["SIZE-ERROR"], ind + "    "), f"{ind}}}"]
+                out += [f"{ind}if ({err}) {{", *self.phrase_block(s.phrases["SIZE-ERROR"], ind + "    "), f"{ind}}}"]
             if "NOT-SIZE-ERROR" in s.phrases:
-                out += [f"{ind}if (!{err}) {{", *self.block(s.phrases["NOT-SIZE-ERROR"], ind + "    "), f"{ind}}}"]
+                out += [
+                    f"{ind}if (!{err}) {{",
+                    *self.phrase_block(s.phrases["NOT-SIZE-ERROR"], ind + "    "),
+                    f"{ind}}}",
+                ]
         return out
 
     def evaluate(self, s: S.Stmt, ind: str) -> list[str]:

gitgalaxy/tools/cobol_to_java/det/stmt.py

@@ -157,6 +157,7 @@ def origin(node) -> int:
     paragraphs: list[Paragraph] = [Paragraph("(MAIN)", None, 0)]
     section: str | None = None
     stack: list[_Frame] = [_Frame("PARA", None, paragraphs[0].body)]
+    closed: set[int] = set()  # id of the statements an END-x has terminated (#4676)
 
     def close_all():
         del stack[1:]
@@ -289,17 +290,25 @@ def node_text(n) -> str:
             continue
         if t in PHRASES:
             name = PHRASES[t]
-            while stack[-1].kind == "PHRASE":
-                stack.pop()
             if t == "at_end" and stack[-1].kind == "SEARCH" and not _node(stack[-1]).whens:
                 # #4462: SEARCH ... AT END (before its WHENs): the SEARCH's own phrase
                 search = _node(stack[-1])
                 stack.append(_Frame("PHRASE", search, search.phrases.setdefault(name, [])))
                 continue
-            owner = next((x for x in reversed(stack[-1].target) if x.kind not in ("HOLE",)), None)
+            # #4676: the innermost unterminated statement that can take the phrase and has not got it yet
+            hit = _phrase_owner(stack, name, closed)
+            owner: Stmt | None
+            if hit is not None:
+                k, owner = hit
+            else:  # no statement can: the old rule, the last statement of the innermost scope
+                while stack[-1].kind == "PHRASE":
+                    stack.pop()
+                k = len(stack) - 1
+                owner = next((x for x in reversed(stack[-1].target) if x.kind != "HOLE"), None)
             if owner is None:
                 stack[-1].target.append(Stmt("HOLE", origin(n), node_text(n), {"why": "phrase with no statement"}))
                 continue
+            del stack[k + 1 :]
             body = owner.phrases.setdefault(name, [])
             stack.append(_Frame("PHRASE", owner, body))
             continue
@@ -317,8 +326,14 @@ def node_text(n) -> str:
             stack.pop()
             continue
         if t in STATEMENT_ENDS:
-            while stack[-1].kind == "PHRASE":
-                stack.pop()
+            # #4676: END-x closes the innermost unterminated statement of its verb (and the phrases it holds open)
+            end = _end_owner(stack, t[4:], closed)
+            if end is None:  # none open: the old rule, close the phrases on top
+                while stack[-1].kind == "PHRASE":
+                    stack.pop()
+            else:
+                del stack[end[0] + 1 :]
+                closed.add(id(end[1]))
             continue
         if t.endswith("_statement") or t.startswith("perform_statement"):
             s = _statement(node_text(n), origin(n))
@@ -402,6 +417,44 @@ def _parser_cache():
     return _PARSER
 
 
+# the statements each phrase can follow (#4676); EXCEPTION is also DISPLAY's and the JSON / XML statements'
+_PHRASE_TAKERS = {"AT-END": {"READ", "RETURN"}, "NOT-AT-END": {"READ", "RETURN"},
+                  "INVALID-KEY": {"READ", "WRITE", "REWRITE", "START"}, "NOT-INVALID-KEY": {"READ", "WRITE", "REWRITE", "START"},
+                  "SIZE-ERROR": {"COMPUTE", "ARITH"}, "NOT-SIZE-ERROR": {"COMPUTE", "ARITH"},
+                  "OVERFLOW": {"CALL", "STRING", "UNSTRING"}, "NOT-OVERFLOW": {"CALL", "STRING", "UNSTRING"},
+                  "EXCEPTION": None, "NOT-EXCEPTION": None, "AT-EOP": {"WRITE"}, "NOT-AT-EOP": {"WRITE"}}  # fmt: skip
+
+
+def _open_last(f: _Frame, closed: set[int]) -> Stmt | None:
+    """The last statement of a scope that is not a hole, and no END-x has terminated."""
+    s = next((x for x in reversed(f.target) if x.kind != "HOLE"), None)
+    return None if s is None or id(s) in closed else s
+
+
+def _phrase_owner(stack: list[_Frame], name: str, closed: set[int]) -> tuple[int, Stmt] | None:
+    """#4676: (stack index, statement) of the innermost unterminated statement that can take the phrase `name` and has
+    not got it -- the last statement of the innermost scope, else of the scope around it, and so on. cobc binds a NOT
+    ON SIZE ERROR after a nested, unterminated COMPUTE to the nested COMPUTE."""
+    takers = _PHRASE_TAKERS[name]
+    for k in range(len(stack) - 1, -1, -1):
+        s = _open_last(stack[k], closed)
+        if s is not None and name not in s.phrases and (takers is None or s.kind in takers):
+            return k, s
+    return None
+
+
+def _end_owner(stack: list[_Frame], verb: str, closed: set[int]) -> tuple[int, Stmt] | None:
+    """#4676: the innermost unterminated statement of `verb` an END-verb closes, looking through the phrases around
+    it only: an enclosing IF / PERFORM scope is not left."""
+    for k in range(len(stack) - 1, -1, -1):
+        s = _open_last(stack[k], closed)
+        if s is not None and s.text.split()[0].upper() == verb:
+            return k, s
+        if stack[k].kind != "PHRASE":
+            return None
+    return None
+
+
 def _node(f: _Frame) -> Stmt:
     if f.node is None:
         raise E.ExprError(f"{f.kind} frame has no statement")