@@ -137,6 +137,31 @@ const ANNOTATED: &[(&str, &str, &str, &str)] = &[
137137 // pins that this row disappears once that decision is made.
138138 ( "STOCH" , "diff" , "OPEN: guard tests the pre-scaled range; see #390" , "" ) ,
139139 ( "STOCHF" , "diff" , "OPEN: guard tests the pre-scaled range; see #390" , "" ) ,
140+
141+ // OPEN, reported by the inline arm, and MEASURED on the released library in
142+ // #395: both return TA_SUCCESS with inf/NaN. CCI guards `tempReal2` and divides
143+ // by `0.015*tempReal2` (cci.c:127,129) -- the scaling underflows while the guard
144+ // passes. CORREL guards `ssX` and `ssY` separately and divides by
145+ // `sqrt(ssX*ssY)` (correl.c:234,236) -- the product underflows independently of
146+ // either factor, and where `spXY` is zero the result is NaN, which the [-1,1]
147+ // clamp does not catch because `NaN > 1.0` is false.
148+ ( "CCI" , "0.015*tempReal2" , "OPEN: inline scaling of a guarded operand; see #395" , "" ) ,
149+ ( "CORREL" , "sqrt(ssX*ssY)" , "OPEN: product underflows independently; see #395" , "" ) ,
150+
151+ // OPEN, same shape, REACHABILITY NOT DEMONSTRATED -- by me or by #395, which does
152+ // not mention them. The Hilbert family guards `Im != 0.0 && Re != 0.0` and then
153+ // divides by `atan(Im/Re)*rad2Deg` (ht_dcperiod.c:318-319 and its six twins).
154+ // Both operands being non-zero does not make the quotient representable: a small
155+ // enough `Im/Re` underflows to 0.0 and `atan(0.0)` is exactly 0.0. That is the
156+ // structural argument; I did not construct an input that reaches it, so these
157+ // rows say "shape matches" and nothing stronger.
158+ ( "HT_DCPERIOD" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
159+ ( "HT_DCPHASE" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
160+ ( "HT_PHASOR" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
161+ ( "HT_SINE" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
162+ ( "HT_TRENDLINE" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
163+ ( "HT_TRENDMODE" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
164+ ( "MAMA" , "atan(Im/Re)*rad2Deg" , "OPEN: shape matches, reachability unproven" , "" ) ,
140165] ;
141166
142167/// Variables assigned, inside a loop, from an expression that MULTIPLIES OR DIVIDES
@@ -277,6 +302,86 @@ fn accumulated_in_loop(body: &[Statement], in_loop: bool, out: &mut HashSet<Stri
277302 }
278303}
279304
305+ /// Did a guard attempt ANY lower bound on `var`, sound or not?
306+ fn bounded_below ( cond : & Expr , var : & str ) -> bool {
307+ match cond {
308+ Expr :: BinOp ( l, BinOp :: And | BinOp :: Or , r) => {
309+ bounded_below ( l, var) || bounded_below ( r, var)
310+ }
311+ Expr :: BinOp ( l, BinOp :: Greater | BinOp :: GreaterEq , r) => {
312+ names ( l) . contains ( var) && !names ( r) . contains ( var)
313+ }
314+ Expr :: BinOp ( l, BinOp :: Less | BinOp :: LessEq , r) => {
315+ names ( r) . contains ( var) && !names ( l) . contains ( var)
316+ }
317+ Expr :: BinOp ( l, BinOp :: NotEq | BinOp :: Eq , r) => {
318+ names ( l) . contains ( var) || names ( r) . contains ( var)
319+ }
320+ Expr :: Not ( i) => bounded_below ( i, var) ,
321+ Expr :: FuncCall ( n, args) if n. contains ( "IS_ZERO" ) => {
322+ args. first ( ) . map ( |a| names ( a) . contains ( var) ) . unwrap_or ( false )
323+ }
324+ _ => false ,
325+ }
326+ }
327+
328+ /// Is `e` an inline product or quotient — a value no guard can name?
329+ ///
330+ /// `sqrt(...)` and `fabs(...)` are transparent: the scaling is inside them, and the
331+ /// call itself carries the same zeroness as its argument.
332+ fn inline_scaling ( e : & Expr ) -> bool {
333+ match e {
334+ Expr :: BinOp ( _, BinOp :: Mul | BinOp :: Div , _) => true ,
335+ Expr :: FuncCall ( n, args) if n == "sqrt" || n == "fabs" || n == "std_fabs" => {
336+ args. first ( ) . map ( inline_scaling) . unwrap_or ( false )
337+ }
338+ Expr :: Cast ( _, i) => inline_scaling ( i) ,
339+ _ => false ,
340+ }
341+ }
342+
343+ /// A guard naming the whole expression, not just one of its operands.
344+ fn tests_expr_against_zero ( cond : & Expr , den : & Expr ) -> bool {
345+ fn same ( a : & Expr , b : & Expr ) -> bool {
346+ format ! ( "{a:?}" ) == format ! ( "{b:?}" )
347+ }
348+ match cond {
349+ Expr :: BinOp ( l, BinOp :: And | BinOp :: Or , r) => {
350+ tests_expr_against_zero ( l, den) || tests_expr_against_zero ( r, den)
351+ }
352+ Expr :: BinOp ( l, _, r) => same ( l, den) || same ( r, den) ,
353+ Expr :: Not ( i) => tests_expr_against_zero ( i, den) ,
354+ Expr :: FuncCall ( n, args) if n. contains ( "IS_ZERO" ) => {
355+ args. first ( ) . map ( |a| same ( a, den) ) . unwrap_or ( false )
356+ }
357+ _ => false ,
358+ }
359+ }
360+
361+ /// A short, stable rendering of a divisor expression for the report.
362+ fn render_expr ( e : & Expr ) -> String {
363+ match e {
364+ Expr :: Var ( v) => v. clone ( ) ,
365+ Expr :: Literal ( l) => format ! ( "{l}" ) ,
366+ Expr :: IntLiteral ( i) => format ! ( "{i}" ) ,
367+ Expr :: BinOp ( l, op, r) => {
368+ let o = match op {
369+ BinOp :: Mul => "*" ,
370+ BinOp :: Div => "/" ,
371+ BinOp :: Add => "+" ,
372+ BinOp :: Sub => "-" ,
373+ _ => "?" ,
374+ } ;
375+ format ! ( "{}{}{}" , render_expr( l) , o, render_expr( r) )
376+ }
377+ Expr :: FuncCall ( n, args) => {
378+ format ! ( "{n}({})" , args. iter( ) . map( render_expr) . collect:: <Vec <_>>( ) . join( "," ) )
379+ }
380+ Expr :: Cast ( _, i) => render_expr ( i) ,
381+ _ => "<expr>" . to_string ( ) ,
382+ }
383+ }
384+
280385/// Does `cond` test `var` against ZERO?
281386///
282387/// `TA_IS_ZERO(v)`, `TA_IS_ZERO_SCALED(v, s)`, `v > 0.0`, `v != 0.0`, `v <= 0.0` and
@@ -443,13 +548,18 @@ enum FindingKind {
443548 /// Divisor is a SCALED derivation of a quantity a dominating guard does test —
444549 /// the guard proves the pre-scaled value non-zero, which the divisor is not.
445550 ScaledFromGuarded ,
551+ /// The divisor is an INLINE product or quotient whose operands are guarded but
552+ /// whose value is not. Same defect as `ScaledFromGuarded`, one step earlier: the
553+ /// scaling never lands in a variable, so there is nothing for a guard to name.
554+ InlineScaled ,
446555}
447556
448557impl FindingKind {
449558 fn label ( self ) -> & ' static str {
450559 match self {
451560 FindingKind :: Accumulated => "accumulated, untested" ,
452561 FindingKind :: ScaledFromGuarded => "scaled from a guarded value" ,
562+ FindingKind :: InlineScaled => "inline product/quotient of guarded operands" ,
453563 }
454564 }
455565}
@@ -466,6 +576,30 @@ fn scan_expr(
466576 out : & mut Vec < Finding > ,
467577) {
468578 if let Expr :: BinOp ( num, BinOp :: Div , den) = e {
579+ // Third shape: the divisor is an inline product or quotient. A guard on an
580+ // OPERAND does not establish the value: `0.015*tempReal2` underflows to
581+ // exactly 0.0 while `tempReal2` is still non-zero (cci.c:127,129), and
582+ // `sqrt(ssX*ssY)` underflows independently of either factor guarded
583+ // separately (correl.c:234,236). Only a guard naming the divisor as a whole
584+ // — which for an inline expression cannot exist — would settle it.
585+ if inline_scaling ( den) && !guards. iter ( ) . any ( |g| tests_expr_against_zero ( g, den) ) {
586+ // Deliberately looser than `tests_var_against_zero`: the question here is
587+ // only whether someone TRIED to bound an operand, not whether that bound
588+ // is sound. CORREL guards `ssX > 1e-14*sumX2` — a relative band, not a
589+ // literal floor — and the strict test rejects it, which is right for the
590+ // other arms and wrong for this one. The strict test stays where the ER
591+ // self-test pins it.
592+ let any_operand_guarded = names ( den)
593+ . iter ( )
594+ . any ( |v| guards. iter ( ) . any ( |g| bounded_below ( g, v) ) ) ;
595+ if any_operand_guarded {
596+ out. push ( Finding {
597+ func : func. to_string ( ) ,
598+ divisor : render_expr ( den) ,
599+ kind : FindingKind :: InlineScaled ,
600+ } ) ;
601+ }
602+ }
469603 for v in names ( den) {
470604 let guarded = guards. iter ( ) . any ( |g| {
471605 tests_var_against_zero ( g, & v)
@@ -853,3 +987,69 @@ fn guard_on_diff(body: &mut [Statement]) {
853987 }
854988 }
855989}
990+
991+ /// The inline arm must go quiet when the guard names the whole divisor.
992+ ///
993+ /// Third self-test, same requirement as the other two: a check that flagged every
994+ /// inline product unconditionally would pass the "it found CCI" bar and be worthless.
995+ /// Rewriting CCI's guard to test `0.015*tempReal2` — the divisor itself — must clear
996+ /// the finding.
997+ #[ test]
998+ fn the_inline_arm_clears_when_the_guard_names_the_divisor ( ) {
999+ let funcs = load ( ) ;
1000+ let cci = funcs. iter ( ) . find ( |f| f. name == "CCI" ) . expect ( "CCI is in the tree" ) ;
1001+
1002+ assert ! (
1003+ findings_for( cci) . iter( ) . any( |f| f. kind == FindingKind :: InlineScaled ) ,
1004+ "CCI ships guarding `tempReal2` while dividing by `0.015*tempReal2`"
1005+ ) ;
1006+
1007+ let mut fixed = cci. clone ( ) ;
1008+ guard_the_whole_divisor ( & mut fixed. body ) ;
1009+ guard_the_whole_divisor ( & mut fixed. private_body ) ;
1010+ assert ! (
1011+ !findings_for( & fixed) . iter( ) . any( |f| f. kind == FindingKind :: InlineScaled ) ,
1012+ "the inline arm still flags CCI after the guard was moved onto the divisor \
1013+ itself — it is not reading the guard, it is flagging every inline product"
1014+ ) ;
1015+ }
1016+
1017+ /// Replace CCI's `TA_IS_ZERO_SCALED(tempReal2, ...)` with a test on `0.015*tempReal2`.
1018+ fn guard_the_whole_divisor ( body : & mut [ Statement ] ) {
1019+ fn divisor ( ) -> Expr {
1020+ Expr :: BinOp (
1021+ Box :: new ( Expr :: Literal ( 0.015 ) ) ,
1022+ BinOp :: Mul ,
1023+ Box :: new ( Expr :: Var ( "tempReal2" . to_string ( ) ) ) ,
1024+ )
1025+ }
1026+ fn fix ( e : & Expr ) -> Expr {
1027+ match e {
1028+ Expr :: FuncCall ( n, args)
1029+ if n. contains ( "IS_ZERO" ) && args. iter ( ) . any ( |a| names ( a) . contains ( "tempReal2" ) ) =>
1030+ {
1031+ Expr :: BinOp ( Box :: new ( divisor ( ) ) , BinOp :: Eq , Box :: new ( Expr :: Literal ( 0.0 ) ) )
1032+ }
1033+ Expr :: Not ( i) => Expr :: Not ( Box :: new ( fix ( i) ) ) ,
1034+ Expr :: BinOp ( l, op, r) if matches ! ( op, BinOp :: And | BinOp :: Or ) => {
1035+ Expr :: BinOp ( Box :: new ( fix ( l) ) , op. clone ( ) , Box :: new ( fix ( r) ) )
1036+ }
1037+ _ => e. clone ( ) ,
1038+ }
1039+ }
1040+ for st in body. iter_mut ( ) {
1041+ match st {
1042+ Statement :: If { condition, then_body, else_body, .. } => {
1043+ * condition = fix ( condition) ;
1044+ guard_the_whole_divisor ( then_body) ;
1045+ guard_the_whole_divisor ( else_body) ;
1046+ }
1047+ Statement :: While { body, .. }
1048+ | Statement :: DoWhile { body, .. }
1049+ | Statement :: For { body, .. }
1050+ | Statement :: ForC { body, .. }
1051+ | Statement :: Block { body } => guard_the_whole_divisor ( body) ,
1052+ _ => { }
1053+ }
1054+ }
1055+ }
0 commit comments