aurora-lint 0.4.336

//! INT10-C: Do not assume a positive remainder when using the % operator
//!
//! The C Standard states that if either operand of the modulo (%) operator is negative,
//! the sign of the result is implementation-defined. This means the result can be negative
//! even when you might expect a positive value. This is particularly dangerous when:
//! 1. The result is used as an array index (can cause out-of-bounds access)
//! 2. The result is expected to be positive for algorithm correctness
//!
//! ## Examples:
//!
//! **Non-compliant:**
//! ```c
//! int insert(int index, int *list, int size, int value) {
//!     if (size != 0) {
//!         index = (index + 1) % size;  // Can be negative!
//!         list[index] = value;         // Undefined behavior if negative
//!         return index;
//!     }
//!     return -1;
//! }
//! ```
//!
//! **Non-compliant (abs() is not a fix):**
//! ```c
//! index = abs((index + 1) % size);  // abs(INT_MIN) is undefined behavior
//! ```
//!
//! **Compliant (use unsigned types):**
//! ```c
//! size_t insert(size_t index, int *list, size_t size, int value) {
//!     if (size != 0 && size != SIZE_MAX) {
//!         index = (index + 1) % size;  // Always positive (unsigned)
//!         list[index] = value;
//!         return index;
//!     }
//!     return SIZE_MAX;  // Error indicator
//! }
//! ```

use super::super::{CertRule, RuleViolation};
use crate::analyze::cfg::FunctionCfg;
use crate::analyze::const_eval::{self, MacroConstantMap, VarRangeMap};
use crate::analyze::context::ProjectContext;
use crate::analyze::value_range::RangeAnalysisResult;
use crate::analyze::vra_access;
use crate::manifest::{RuleCategory, Severity};
use crate::utility::cert_c::ast_utils::{get_node_text, misparsed_cast_type_name};
use crate::utility::cert_c::overflow_helpers;
use lang_parsing_substrate::query;
use std::cell::RefCell;
use std::collections::HashMap;
use tree_sitter::Node;

pub struct Int10C {
    /// One-level typedef alias map (`word_t` -> `unsigned long`, `paddr_t` ->
    /// `word_t`, ...), populated project-wide by `set_project_context`.
    /// Resolved recursively by `overflow_helpers::typedef_chain_is_unsigned`
    /// so a multi-level, cross-file typedef family is recognized as
    /// unsigned even though `type_map` only records the alias name as
    /// written (task 657).
    typedef_types: RefCell<HashMap<String, String>>,
    /// Project-wide compile-time constants (enum constants, `#define`s,
    /// file-scope `static const`), populated by `set_project_context` and
    /// merged with per-file constants in `check`. Lets a modulo operand
    /// that's an enum constant with a provably non-negative *value* clear
    /// the check even when its enum *type* is signed (task 673).
    project_macros: RefCell<MacroConstantMap>,
    /// `project_macros` merged with the current file's own `#define`s, kept
    /// for the duration of `check` so the VRA range lookup can resolve
    /// macro-valued identifiers the same way the rest of the rule does.
    current_macros: RefCell<MacroConstantMap>,
    /// Per-function CFGs and value-range results, supplied by the driver
    /// because [`needs_vra`] is true. Used to prove a signed *dividend* is
    /// non-negative at the modulo site -- e.g. a local `int` derived from a
    /// guard-bounded parameter (task 674).
    function_cfgs: RefCell<HashMap<usize, FunctionCfg>>,
    vra_results: RefCell<HashMap<usize, RangeAnalysisResult>>,
}

impl Int10C {
    pub fn new() -> Self {
        Self {
            typedef_types: RefCell::new(HashMap::new()),
            project_macros: RefCell::new(MacroConstantMap::new()),
            current_macros: RefCell::new(MacroConstantMap::new()),
            function_cfgs: RefCell::new(HashMap::new()),
            vra_results: RefCell::new(HashMap::new()),
        }
    }
}

impl CertRule for Int10C {
    fn rule_id(&self) -> &'static str {
        "INT10-C"
    }

    fn description(&self) -> &'static str {
        "Do not assume a positive remainder when using the % operator"
    }

    fn severity(&self) -> Severity {
        Severity::Medium
    }

    fn category(&self) -> RuleCategory {
        RuleCategory::Rule
    }

    fn cert_id(&self) -> &'static str {
        "INT10-C"
    }

    fn set_project_context(&self, context: &ProjectContext) {
        *self.typedef_types.borrow_mut() = context.typedef_types.clone();
        *self.project_macros.borrow_mut() = context.macro_constants.clone();
    }

    fn set_function_cfgs(&self, cfgs: &HashMap<usize, FunctionCfg>) {
        *self.function_cfgs.borrow_mut() = cfgs.clone();
    }

    fn set_vra_results(&self, results: &HashMap<usize, RangeAnalysisResult>) {
        *self.vra_results.borrow_mut() = results.clone();
    }

    fn needs_vra(&self) -> bool {
        true
    }

    fn check(&self, node: &Node, source: &str) -> Vec<RuleViolation> {
        let mut violations = Vec::new();
        let type_map = overflow_helpers::collect_variable_types(node, source);
        *self.current_macros.borrow_mut() =
            const_eval::merged_macro_constants(&self.project_macros.borrow(), node, source);
        // Held immutably for the whole walk; `vra_var_ranges_at` borrows the
        // same cell immutably again, which is fine.
        let macros = self.current_macros.borrow();
        self.check_modulo_usage(node, source, &mut violations, &type_map, &macros);
        drop(macros);
        violations
    }
}

impl Int10C {
    fn check_modulo_usage(
        &self,
        node: &Node,
        source: &str,
        violations: &mut Vec<RuleViolation>,
        type_map: &HashMap<String, String>,
        macros: &MacroConstantMap,
    ) {
        // Scope type_map per function to avoid cross-function name collisions
        // (e.g., a same-named variable of a different signedness in a different
        // function). Memoized per enclosing function_definition node id so it's
        // only computed once even though many candidates share the same function.
        let mut fn_type_maps: HashMap<usize, HashMap<String, String>> = HashMap::new();

        for n in query::find_descendants_of_kind(*node, "binary_expression") {
            if let Some(operator) = n.child_by_field_name("operator") {
                let op_text = get_node_text(&operator, source);

                if op_text == "%" {
                    let scoped_type_map: &HashMap<String, String> =
                        match overflow_helpers::enclosing_function_definition(&n) {
                            Some(func_node) => {
                                fn_type_maps.entry(func_node.id()).or_insert_with(|| {
                                    overflow_helpers::collect_variable_types(&func_node, source)
                                })
                            }
                            None => type_map,
                        };

                    // Check if this is a signed modulo operation
                    if self.is_potentially_signed_modulo(&n, source, scoped_type_map, macros) {
                        violations.push(RuleViolation {
                            rule_id: self.rule_id().to_string(),
                            message: "Modulo operator used with potentially signed operands. \
                                     The result of % with negative operands is implementation-defined \
                                     and can be negative. Use unsigned types (size_t, unsigned int) \
                                     or explicitly handle negative remainders."
                                .to_string(),
                            severity: self.severity(),
                            line: operator.start_position().row + 1,
                            column: operator.start_position().column + 1,
                            file_path: String::new(),
                            suggestion: Some(
                                "Convert operands to unsigned types (size_t, unsigned int) \
                                 or add explicit checks for negative values"
                                    .to_string(),
                            ),
                            requires_manual_review: Some(true),
                        });
                    }
                }
            }
        }
    }

    /// Check if a modulo operation might involve signed operands
    fn is_potentially_signed_modulo(
        &self,
        modulo_node: &Node,
        source: &str,
        type_map: &HashMap<String, String>,
        macros: &MacroConstantMap,
    ) -> bool {
        // Get left and right operands
        let left = modulo_node.child_by_field_name("left");
        let right = modulo_node.child_by_field_name("right");

        if left.is_none() || right.is_none() {
            return false;
        }

        let left_node = left.unwrap();
        let right_node = right.unwrap();

        // Check if either operand appears to be unsigned
        let left_text = get_node_text(&left_node, source);
        let right_text = get_node_text(&right_node, source);

        // If either operand is explicitly unsigned, it's likely safe
        let expr_is_unsigned = self.looks_unsigned(&left_text) || self.looks_unsigned(&right_text);

        if expr_is_unsigned {
            return false;
        }

        // Check type_map for identifiers within each operand
        if self.operand_has_unsigned_type(&left_node, source, type_map)
            || self.operand_has_unsigned_type(&right_node, source, type_map)
        {
            return false;
        }

        // A *dividend* identifier whose value resolves to a compile-time
        // constant (an enum constant, `#define`, or file-scope `static
        // const`) that's non-negative can't produce a negative remainder,
        // regardless of its declared type's signedness -- e.g. an
        // `interrupt_t` enum constant set to a macro like `IRQ_INT_OFFSET`
        // (0x20) is provably non-negative even though the enum itself has
        // an unrelated negative member (`int_invalid = -1`) and is
        // therefore a signed type overall (task 673).
        //
        // DIVIDEND ONLY, for the same reason the VRA check below is: C99
        // 6.5.5p6 truncates toward zero, so `a % b` carries the sign of `a`
        // and a non-negative `b` proves nothing. This used to accept either
        // operand, which silently swallowed the whole `signed % NAMED_CONST`
        // class -- `a % GRANULE` with `a == -5` yields -5, exactly what this
        // rule exists to flag (task 777).
        if self.operand_is_nonnegative_constant(&left_node, source, macros) {
            return false;
        }

        // A signed dividend that VRA can prove non-negative at this point
        // can't yield a negative remainder: C99 6.5.5p6 truncates toward
        // zero, so `a % b` carries the sign of `a` whatever `b`'s sign is.
        // This is what catches a local `int` whose non-negativity comes from
        // enclosing guard flow rather than from its declared type -- e.g.
        // seL4's `int normal_irq = irq - NORMAL_IRQ_OFFSET;` inside an
        // `else if` reached only after `if (irq < NORMAL_IRQ_OFFSET) return;`
        // (task 674). Deliberately dividend-only: a non-negative *divisor*
        // proves nothing (`-5 % 3 == -2`).
        if self.dividend_is_nonnegative_by_vra(&left_node, source, macros) {
            return false;
        }

        // Field expressions (e.g., self->field) — we can't resolve struct member
        // types without struct definitions, so don't assume signed
        if left_node.kind() == "field_expression" || right_node.kind() == "field_expression" {
            return false;
        }

        // Check if we're in a function with size_t parameters
        if self.is_in_function_with_unsigned_params(modulo_node, source) {
            return false;
        }

        true
    }

    /// Check if any identifier in the operand resolves to an unsigned type
    fn operand_has_unsigned_type(
        &self,
        node: &Node,
        source: &str,
        type_map: &HashMap<String, String>,
    ) -> bool {
        let typedef_types = self.typedef_types.borrow();
        query::find_first_descendant(*node, |n| {
            if n.kind() == "identifier" {
                let name = get_node_text(&n, source);
                if let Some(t) = type_map.get(name) {
                    return t.contains("size_t")
                        || t.contains("unsigned")
                        || t.contains("uint")
                        || overflow_helpers::is_short_unsigned_typedef(t)
                        // `t` is the alias name as written (e.g. "word_t",
                        // "paddr_t") -- resolve the full, possibly
                        // cross-file typedef chain before giving up (task
                        // 657).
                        || overflow_helpers::typedef_chain_is_unsigned(t, &typedef_types);
                }
            }
            // `sizeof(...)` always yields `size_t`, regardless of the sized
            // expression's own type.
            if n.kind() == "sizeof_expression" {
                return true;
            }
            // A cast that tree-sitter-c mis-parsed -- `(seL4_Word)&x` comes
            // back as a bitwise AND, `(seL4_Word)(x)` as a call. The name is
            // only a type if the typedef chain resolves it, which is what
            // separates this from a genuine `(mask) & flags` (task 675).
            if let Some(name) = misparsed_cast_type_name(&n, source) {
                if overflow_helpers::typedef_chain_is_unsigned(name, &typedef_types) {
                    return true;
                }
            }
            // An explicit cast to a typedef'd name (e.g. `(seL4_Word)x`) --
            // resolve the cast's target type through the same typedef chain.
            if n.kind() == "cast_expression" {
                if let Some(type_node) = n.child_by_field_name("type") {
                    let cast_type = get_node_text(&type_node, source);
                    if cast_type.contains("unsigned")
                        || overflow_helpers::typedef_chain_is_unsigned(cast_type, &typedef_types)
                    {
                        return true;
                    }
                }
            }
            // For field expressions like self->field, we can't resolve the type
            // but we know it's a struct access — check text heuristic
            if n.kind() == "field_expression" {
                let text = get_node_text(&n, source);
                if self.looks_unsigned(&text) {
                    return true;
                }
            }
            false
        })
        .is_some()
    }

    /// Check if any identifier in the operand resolves, via compile-time
    /// constant folding, to a known non-negative value. Deliberately
    /// scoped to *identifier* operands only (an enum constant, `#define`,
    /// or `static const` name) — not to bare integer literals written
    /// directly in the modulo expression, since a literal on one side
    /// (e.g. `x % 60`) says nothing about whether the *other*, unresolved
    /// operand can be negative, and treating it as safe would suppress
    /// genuine findings (task 673).
    fn operand_is_nonnegative_constant(
        &self,
        node: &Node,
        source: &str,
        macros: &MacroConstantMap,
    ) -> bool {
        query::find_first_descendant(*node, |n| {
            if n.kind() == "identifier" {
                let name = get_node_text(&n, source);
                if let Some(&value) = macros.get(name) {
                    return value >= 0;
                }
            }
            false
        })
        .is_some()
    }

    /// True when value-range analysis proves the modulo's *dividend* is
    /// non-negative at this expression. Returns false whenever VRA is
    /// unavailable (no CFG for the enclosing function, no converged range for
    /// an operand identifier) or the range is only partially known, so the
    /// rule's behavior is unchanged wherever the ranges aren't there.
    fn dividend_is_nonnegative_by_vra(
        &self,
        left_node: &Node,
        source: &str,
        macros: &MacroConstantMap,
    ) -> bool {
        let var_ranges = match self.vra_var_ranges_at(left_node, source) {
            Some(r) => r,
            None => return false,
        };
        match const_eval::try_evaluate_range(left_node, source, macros, &var_ranges) {
            Some(range) => range.min >= 0,
            None => false,
        }
    }

    /// VRA-derived variable ranges in effect at `expr_node`, replaying the
    /// containing block so an assignment earlier in the same block (the
    /// common `int t = a - b; ... t % n` shape) is visible here.
    fn vra_var_ranges_at(&self, expr_node: &Node, source: &str) -> Option<VarRangeMap> {
        vra_access::var_ranges_replay_at(
            &self.function_cfgs.borrow(),
            &self.vra_results.borrow(),
            expr_node,
            source,
            &self.current_macros.borrow(),
        )
    }

    /// Check if an expression appears to use unsigned types
    fn looks_unsigned(&self, text: &str) -> bool {
        // Common unsigned type patterns
        text.contains("size_t")
            || text.contains("unsigned")
            || text.contains("SIZE_MAX")
            || text.contains("UINT_MAX")
            // Unsigned literal suffix
            || text.ends_with('u')
            || text.ends_with('U')
            || text.ends_with("ul")
            || text.ends_with("UL")
            || text.ends_with("ull")
            || text.ends_with("ULL")
    }

    /// Check if node is within a function that has unsigned type parameters
    fn is_in_function_with_unsigned_params(&self, node: &Node, source: &str) -> bool {
        let mut current = node.parent();

        while let Some(parent) = current {
            if parent.kind() == "function_definition" {
                // Look for parameter list
                if let Some(declarator) = parent.child_by_field_name("declarator") {
                    let params_text = get_node_text(&declarator, source);
                    // Check if parameters contain unsigned types
                    if params_text.contains("size_t") || params_text.contains("unsigned") {
                        return true;
                    }
                }
                break;
            }
            current = parent.parent();
        }

        false
    }
}