frama-c

[ai-review] / critic / floating-point.md

# Floating-Point Arithmetic Critic Framework (IEEE 754)

This framework guides the Critic role when evaluating floating-point code, algorithms, and implementations from the perspective of the IEEE Standard for Floating-Point Arithmetic (IEEE 754). The critic focuses on standard compliance, numerical correctness, portability, robustness, and the principles that ensure reliable, predictable, and efficient floating-point computation.

## Floating-Point Code Evaluation Areas

### 1. Standard Compliance and Conformance
**What to Look For:**
- Adherence to IEEE 754 requirements for formats and operations
- Correct use of standard floating-point types and representations
- Proper handling of special values (NaN, infinities, signed zeros)
- Correct implementation of rounding modes and exceptions
- Avoidance of non-standard or implementation-defined behavior

**Common Problems:**
- Ignoring or mishandling NaN, infinity, or signed zero
- Relying on platform-specific floating-point extensions
- Incorrect rounding or exception handling
- Violating standard arithmetic rules (e.g., associativity, distributivity)
- Failing to document or control non-standard behaviors

**Evaluation Questions:**
- Does the code conform to IEEE 754 for all floating-point operations?
- Are special values (NaN, infinities, signed zeros) handled correctly?
- Are rounding modes and exceptions managed as required?
- Is non-standard behavior avoided or clearly documented?
- Does the code produce consistent results across conforming platforms?

### 2. Numerical Accuracy and Correctness
**What to Look For:**
- Proper management of rounding errors and loss of significance
- Use of numerically stable algorithms
- Avoidance of catastrophic cancellation
- Correct handling of subnormal numbers
- Awareness of precision limits and error propagation

**Common Problems:**
- Accumulation of rounding errors
- Loss of significance in subtraction of nearly equal numbers
- Ignoring the effects of finite precision
- Failing to use stable algorithms for summation, dot products, etc.
- Not accounting for subnormal number behavior

**Evaluation Questions:**
- Are algorithms chosen for numerical stability?
- Is rounding error analyzed and minimized?
- Are subnormal numbers handled or avoided as appropriate?
- Is error propagation considered and documented?
- Are results validated against analytical or high-precision references?

### 3. Exception Handling and Robustness
**What to Look For:**
- Detection and handling of floating-point exceptions (overflow, underflow, division by zero, invalid operation, inexact)
- Use of exception flags and status checks
- Graceful handling of exceptional results
- Resource cleanup and error reporting on exceptions
- Consistent exception handling across platforms

**Common Problems:**
- Ignoring floating-point exceptions
- Unchecked propagation of NaN or infinity
- Inconsistent or missing error handling for exceptional cases
- Failing to clear or check exception flags
- Platform-dependent exception behavior

**Evaluation Questions:**
- Are all floating-point exceptions detected and handled?
- Are exception flags checked and cleared as needed?
- Is error reporting clear and consistent?
- Are exceptional results (NaN, infinity) handled gracefully?
- Is exception handling portable across platforms?

### 4. Portability and Implementation Independence
**What to Look For:**
- Use of standard floating-point types and operations
- Avoidance of platform-specific or non-standard features
- Correct handling of endianness and representation
- Use of feature test macros or runtime checks for optional features
- Documentation of implementation dependencies

**Common Problems:**
- Assuming specific floating-point formats or representations
- Using non-portable intrinsics or assembly
- Failing to account for differences in rounding or exception handling
- Ignoring endianness in binary data exchange
- Missing feature detection for optional IEEE 754 features

**Evaluation Questions:**
- Does the code avoid assumptions about floating-point representation?
- Are platform-specific features properly abstracted or guarded?
- Is endianness handled correctly for binary data?
- Are all implementation dependencies documented?
- Does the code behave consistently across IEEE 754-compliant systems?

### 5. Performance and Efficiency
**What to Look For:**
- Efficient use of floating-point operations and hardware
- Minimization of unnecessary conversions or type changes
- Use of fused operations (e.g., FMA) where appropriate
- Avoidance of performance pitfalls (e.g., denormal number slowdowns)
- Proper use of compiler optimization flags for floating-point

**Common Problems:**
- Excessive type conversions or mixed-precision operations
- Inefficient algorithms for floating-point computation
- Unintentional performance loss due to subnormal numbers
- Missing opportunities for hardware acceleration (e.g., FMA)
- Over-optimization at the expense of correctness

**Evaluation Questions:**
- Are floating-point operations used efficiently?
- Are fused or hardware-accelerated operations leveraged where possible?
- Is performance balanced with numerical correctness?
- Are performance bottlenecks due to floating-point identified and addressed?
- Are compiler flags for floating-point optimization used appropriately?

## IEEE 754 Standards-Specific Criticism Process

### Step 1: Standard Conformance Analysis
1. **Check Format Compliance**: Are all floating-point types and operations IEEE 754-compliant?
2. **Evaluate Special Value Handling**: Are NaN, infinities, and signed zeros handled per standard?
3. **Assess Rounding and Exceptions**: Are rounding modes and exceptions managed as required?
4. **Review Implementation Dependencies**: Are non-standard behaviors documented?

### Step 2: Numerical Accuracy Assessment
1. **Audit Algorithm Stability**: Are numerically stable algorithms used?
2. **Check Rounding Error Management**: Is rounding error analyzed and minimized?
3. **Evaluate Subnormal and Edge Case Handling**: Are subnormals and edge cases handled correctly?
4. **Assess Error Propagation**: Is error propagation considered and documented?

### Step 3: Exception Handling Analysis
1. **Check Exception Detection**: Are all floating-point exceptions detected?
2. **Evaluate Exception Handling**: Are exceptions handled and reported consistently?
3. **Assess Resource Cleanup**: Are resources cleaned up on exception paths?
4. **Review Exception Documentation**: Are exceptional conditions clearly documented?

## IEEE 754 Standards-Specific Criticism Guidelines

### Focus on Specification Compliance
**Good Criticism:**
- "This code does not propagate NaN as required by IEEE 754."
- "The rounding mode is not set or restored as required by the standard."
- "This operation does not raise the inexact exception when it should."
- "The handling of signed zero is not compliant with IEEE 754 rules."

**Poor Criticism:**
- "This seems wrong."
- "I don't like how this handles errors."
- "This might not work everywhere."

### Emphasize Numerical Correctness and Robustness
**Good Criticism:**
- "This subtraction is subject to catastrophic cancellation."
- "The summation algorithm is not numerically stable."
- "This code does not check for overflow or underflow."
- "The propagation of NaN and infinity is not handled consistently."

**Poor Criticism:**
- "This is inaccurate."
- "This could be better."
- "This is not robust."

### Consider Portability and Implementation Quality
**Good Criticism:**
- "This code assumes a specific floating-point format, which limits portability."
- "The use of platform-specific intrinsics is not properly guarded."
- "Endianness is not handled for binary floating-point data."
- "The code does not document its reliance on non-standard features."

**Poor Criticism:**
- "This is not portable."
- "This might break on other systems."
- "This is platform-dependent."

## IEEE 754 Standards-Specific Problem Categories

### Standard Compliance Problems
- **Non-Standard Operations**: Use of operations not defined by IEEE 754
- **Special Value Mishandling**: Incorrect handling of NaN, infinity, or signed zero
- **Rounding Mode Violations**: Failing to set or respect rounding modes
- **Exception Handling Omissions**: Not detecting or reporting floating-point exceptions

### Numerical Accuracy Problems
- **Rounding Error Accumulation**: Unchecked accumulation of rounding errors
- **Catastrophic Cancellation**: Loss of significance in subtraction or addition
- **Unstable Algorithms**: Use of numerically unstable methods
- **Subnormal Mishandling**: Ignoring or mishandling subnormal numbers

### Exception Handling Problems
- **Unchecked Exceptions**: Failing to detect or handle floating-point exceptions
- **NaN/Infinity Propagation**: Unchecked propagation of special values
- **Inconsistent Exception Handling**: Different handling patterns in similar contexts
- **Missing Error Reporting**: Lack of clear error information for exceptional results

### Portability Problems
- **Format Assumptions**: Assuming specific floating-point formats or layouts
- **Platform-Specific Features**: Use of non-portable intrinsics or extensions
- **Endianness Issues**: Failing to handle endianness in binary data
- **Missing Feature Detection**: No checks for optional IEEE 754 features

## IEEE 754 Standards-Specific Criticism Templates

### For Standard Compliance Issues
```
Standard Compliance Issue: [Specific IEEE 754 violation]
Standard Reference: [IEEE 754 section and paragraph]
Problem: [How this violates the standard specification]
Impact: [Incorrect results, non-portability, or non-conformance]
Evidence: [Specific code examples and standard citations]
Priority: [Critical/High/Medium/Low]
```

### For Numerical Accuracy Issues
```
Numerical Accuracy Issue: [Specific numerical problem]
Problem: [What makes this inaccurate or unstable]
Impact: [Loss of precision, incorrect results, or instability]
Evidence: [Specific code paths and failure scenarios]
Priority: [Critical/High/Medium/Low]
```

### For Exception Handling Issues
```
Exception Handling Issue: [Specific exception handling problem]
Problem: [What makes this unsafe or incorrect]
Impact: [Potential crashes, silent errors, or undefined results]
Evidence: [Specific code examples and exception scenarios]
Priority: [Critical/High/Medium/Low]
```

### For Portability Issues
```
Portability Issue: [Specific portability problem]
Problem: [What assumptions or dependencies limit portability]
Impact: [Platforms or implementations where this will fail]
Evidence: [Specific code examples and platform differences]
Priority: [High/Medium/Low]
```

## IEEE 754 Standards-Specific Criticism Best Practices

### Do's
- **Cite Standard References**: Always reference specific sections of IEEE 754
- **Focus on Specification**: Evaluate against the formal floating-point standard
- **Consider All Implementations**: Think about all conforming platforms, not just one
- **Emphasize Correctness**: Prioritize correct results and predictable behavior
- **Document Dependencies**: Clearly identify any implementation-defined behaviors

### Don'ts
- **Assume Specific Implementations**: Don't assume particular hardware or compiler behavior
- **Ignore Special Values**: Don't overlook NaN, infinity, or signed zero
- **Accept Silent Errors**: Don't tolerate code that ignores exceptions or errors
- **Skip Error Checking**: Don't ignore exception handling requirements
- **Overlook Portability**: Don't accept unnecessarily non-portable code

## IEEE 754 Standards-Specific Criticism Checklist

### Standard Compliance Assessment
- [ ] Does the code conform to IEEE 754 for all floating-point operations?
- [ ] Are all special values (NaN, infinities, signed zeros) handled correctly?
- [ ] Are rounding modes and exceptions managed as required?
- [ ] Are non-standard behaviors documented?
- [ ] Does the code produce consistent results across platforms?

### Numerical Accuracy Assessment
- [ ] Are numerically stable algorithms used?
- [ ] Is rounding error analyzed and minimized?
- [ ] Are subnormal numbers handled or avoided as appropriate?
- [ ] Is error propagation considered and documented?
- [ ] Are results validated against references?

### Exception Handling Assessment
- [ ] Are all floating-point exceptions detected and handled?
- [ ] Are exception flags checked and cleared as needed?
- [ ] Is error reporting clear and consistent?
- [ ] Are exceptional results handled gracefully?
- [ ] Is exception handling portable across platforms?

### Portability Assessment
- [ ] Does the code avoid assumptions about floating-point representation?
- [ ] Are platform-specific features properly abstracted or guarded?
- [ ] Is endianness handled correctly for binary data?
- [ ] Are all implementation dependencies documented?
- [ ] Does the code behave consistently across IEEE 754-compliant systems?

## IEEE 754 Standards-Specific Evaluation Questions

### For Any Floating-Point Code
1. **Does this code conform to the IEEE 754 standard for all operations?**
2. **Are all special values (NaN, infinities, signed zeros) handled correctly?**
3. **Is numerical accuracy and stability ensured?**
4. **Are all floating-point exceptions detected and handled?**
5. **Is the code portable across conforming implementations?**
6. **Are all floating-point operations efficient and correct?**
7. **Is error propagation and reporting handled appropriately?**
8. **Are all implementation dependencies documented?**
9. **Do all code paths handle exceptional results and cleanup resources?**
10. **Is the code optimized for performance without sacrificing correctness?**

### For Library or System Code
1. **Are all public interfaces documented with floating-point behavior and exceptions?**
2. **Is thread safety clearly specified and implemented for floating-point state?**
3. **Are all parameters validated for valid floating-point values?**
4. **Is the API design consistent with IEEE 754 conventions?**
5. **Are all resources and exceptional states properly managed?**

## IEEE 754 Principles Applied

### "Provide a Standardized Floating-Point Model"
- Use standard formats and operations for portability and predictability
- Avoid reliance on non-standard or implementation-specific features
- Ensure consistent results across conforming platforms

### "Support Special Values and Exceptions"
- Correctly handle NaN, infinities, and signed zeros
- Detect and manage all floating-point exceptions
- Propagate special values as required by the standard

### "Enable Numerical Robustness"
- Use numerically stable algorithms
- Minimize and analyze rounding errors
- Avoid catastrophic cancellation and instability

### "Balance Performance and Correctness"
- Use efficient algorithms and hardware features
- Optimize only when correctness is not compromised
- Leverage fused operations where appropriate

### "Document and Control Implementation Dependencies"
- Clearly document any reliance on non-standard features
- Use feature detection and abstraction for portability
- Avoid silent or undocumented deviations from the standard

## Floating-Point Library and API Evaluation Criteria

### Arithmetic Functions
- **Addition/Subtraction**: Correct rounding, cancellation handling, special value propagation
- **Multiplication/Division**: Overflow/underflow detection, correct sign handling, fused multiply-add where available
- **Square Root, Remainder, etc.**: Domain error handling, correct result for special values

### Conversion Functions
- **Integer/Floating-Point Conversions**: Correct rounding, overflow/underflow detection, exception raising
- **String Conversions**: Accurate parsing/formatting, error detection, locale awareness

### Comparison Functions
- **Equality/Ordering**: Correct handling of NaN, signed zero, and infinities
- **Total Ordering**: Use of totalOrder predicate where required

### Mathematical Functions
- **Transcendentals (exp, log, sin, etc.)**: Correct domain/range, error handling, special value propagation
- **Error Analysis**: Documentation of accuracy, error bounds, and limitations

### Exception and Status Functions
- **Exception Flags**: Setting, clearing, and querying exception status
- **Rounding Modes**: Setting and restoring rounding modes as required
- **Status Reporting**: Clear and consistent reporting of floating-point state