mirror of
https://github.com/elicpeter/nyx.git
synced 2026-06-21 20:18:06 +02:00
Release/0.5.0 (#35)
* feat: Introduce function-scoped variable interning for state analysis with new tests and fixtures * feat: Add Phase 26 symbolic execution enhancements with bitwise operator support, abstract interpretation refinements, and new taint analysis tests * feat: Refine state analysis to handle factory-pattern resource returns with mixed-path tests and leak detection enhancements * feat: Add Phase 27 debug views with symbolic execution, abstract interpretation, SSA, and call graph viewers; integrate with debug layout and styles * feat: Add Phase 31 type-qualified symbolic resolution with receiver-based callee disambiguation and testing * feat: Extend symbolic execution with state iteration, enhanced debug views, and debounced input handling * feat: Add Phase 13 resource and auth pattern extensions with new tests and fixtures * feat: Introduce CFG debug graph renderer with compact mode, toolbar, and DAG layout integration * feat: Add Phase 28 encoding and decoding transform modeling with structural symex enhancements and new taint analysis tests * feat: Extend abstract interpretation with type facts and constant value tracking in debug views and server logic * feat: Add linear path handling and witness extraction to symbolic execution with Phase 28 transform mismatch detection * feat: Refine Go auth and sanitizer handling with enhanced rules, state updates, and benchmark improvements * feat: Enable auth-state analysis by default and update relevant tests in benchmark config * test: Update state_tests to reflect default enablement of auth-state analysis and add auth suppression test * docs: update CHANGELOG.md * feat: Introduce per-index taint tracking in `HeapState` with `HeapSlot`, overflow handling, and revised SSA transfers * feat: Introduce C/C++ language labels and refine heap state tracking in SSA transfers * feat: Implement per-index array slot tracking in symbolic heap with overflow collapse * feat: Add implicit definition handling for uninitialized declarations in SSA value allocation * feat: Refactor function parameters and constants for improved clarity and maintainability * refactor: Reorder module imports and improve formatting for consistency * refactor: Fix formatting erorrs * refactor: Fix clippy warnings * refactor: Fix fmt warnings (again) * chore: Update dependencies and improve feature configuration * Add comprehensive tests for undertested modules (#36) (COPILOT) * Add comprehensive tests for undertested modules Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/f3fc877e-f386-49ba-9793-fc93d3805083 * Add comprehensive tests for ext, project, walk, and errors modules Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/f3fc877e-f386-49ba-9793-fc93d3805083 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> * chore: Update dependencies and improve feature configuration * fix: formatting errors in new tests * chore: Update license list in about.toml * chore: made functions input inline * chore: updated cfg graph to take up the full page * chore: add Prettier configuration and update code formatting * Add frontend test suite with Vitest (111 tests) (#37) * Add Vitest test suite for frontend - 111 tests across utils, components, hooks, and graph utilities Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/7cf0dba2-ecff-4740-ba4d-92717e74a0b7 * ci: add frontend test step to CI workflow Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/5bc0ac9f-0a32-4d03-9cb7-7a15aea53fca --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> * chore: simplify array initialization in test files for consistency * ran typecheck * feat: add AnalysisWorkspace component and integrate it into CfgViewerPage * feat: update routing in AppLayout and improve empty state message in ExplorerPage * feat: enhance scan progress tracking with additional metrics and stages * feat: update license information and add license check script * feat: implement cross-file symbolic execution with callee body persistence * feat: replace dagre graphs with Graphology + ELK + Sigma for more advanced call stack and cfg rendering * feat: ensure CFG function view is scoped to the selected function, preventing bleed into sibling functions * feat: enhance resource tracking with proxy method summaries and improve finding extraction * feat: add terminal function exit detection for accurate resource leak analysis * feat: add warnings for loops and functions without bodies to improve error recovery * feat: update lambda expression handling to ensure proper function classification and control flow * feat: remove bounded formatting/string ops and add JSON.parse sanitizer for improved data handling * feat: add inline return taint analysis and regression tests for improved security checks * feat: add engine version management and migration handling for database schema updates * feat: enhance first_call_ident to skip nested function bodies and add regression tests * feat: enhance callee name resolution with two-segment normalization and disambiguation * feat: add cross-file context flags and debug assertions for taint analysis * feat: refactor taint analysis structure to unify context handling and improve clarity * feat: enhance dead code elimination to preserve Sink, Source, and Sanitizer labels with new tests * docs: updated CHANGELOG.md * fmt: formatting fixes * fix: fixed frontend formatting and lint warnings * fix: optimized ci * fix: optimized ci * Add comprehensive multi-file test coverage to Nyx (#38) * Initial checklist for multi-file test suite expansion Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/e550cb88-9767-4442-94d4-101bf5bb0e23 Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> * Add 12 new multi-file test fixtures with TP/TN/near-miss coverage Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/e550cb88-9767-4442-94d4-101bf5bb0e23 Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> * deleted root repo * rebuilt to test for regressions --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> Co-authored-by: elipeter <elicpeter@gmail.com> * feat: enhance import alias resolution and taint tracking * feat: implement security hardening with CSRF protection and path validation * feat: add support for import alias bindings in Python, PHP, and Rust * feat: enhance CFG analysis modes and improve code readability * feat: add detection for parameterized SQL queries to enhance security * feat: add safe internal redirect handling and enhance session destroy validation * feat: implement security improvements by addressing vulnerabilities in execAsync, session management, and file downloads * feat: enhance taint detection by adding support for inline source member expressions in call arguments * feat: implement pre-emission of Source nodes for inline source member expressions in call arguments * feat: add support for Throw statement in control flow and error handling * feat: add debug and echo endpoints with potential information leakage * feat: implement internal redirect suppression and enhance taint detection * feat: implement module alias tracking for dynamic dispatch in JS/TS * feat: add authorization analysis module with Express support * feat: add authorization analysis module with Express support * feat: add tests for admin guard requirements and clean checks in authorization analysis * feat: integrate Koa and Fastify frameworks into authorization analysis * feat: add Flask and Django support to authorization analysis module * feat: add support for Rails and Sinatra frameworks in authorization analysis * feat: add support for Axum, ActixWeb, and Rocket frameworks in authorization analysis * feat: add support for ActixWeb, Axum, and Rocket frameworks in authorization analysis * feat: add support for Rails and Sinatra in authorization analysis * chore: add .DS_Store to .gitignore * refactor: simplify conditional checks and improve readability in multiple files * refactor: update usage of Option methods for improved clarity and consistency * refactor: improve code readability by simplifying conditional checks and formatting * refactor: improve code formatting and readability by simplifying conditional checks * refactor: simplify conditional checks and improve readability in multiple files * refactor: simplify conditional checks in axum.rs for improved readability * feat: add CodeQL analysis configuration for enhanced security scanning * test: add comprehensive tests for `src/output.rs` SARIF builder (#39) * chore: start test coverage improvement work Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/cd7ff398-134e-4728-a5e7-0353a0744423 Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> * test: add comprehensive tests for src/output.rs SARIF builder Agent-Logs-Url: https://github.com/elicpeter/nyx/sessions/cd7ff398-134e-4728-a5e7-0353a0744423 Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> * refactor: improve code formatting and readability in output.rs --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: elicpeter <54954007+elicpeter@users.noreply.github.com> Co-authored-by: elipeter <elicpeter@gmail.com> * refactor: improve code formatting and readability in output.rs * Potential fix for code scanning alert no. 210: Uncontrolled data used in path expression Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com> * Potential fix for code scanning alert no. 211: Uncontrolled data used in path expression Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com> * refactor: enhance triage file path handling with improved error management and validation * refactor: updated func summaries for richer detail * refactor: update SSA summary extraction to use canonical FuncKey for distinct entries * refactor: enhance callee metadata structure to support arity, receiver, and qualifier for better overload resolution * refactor: add support for keyword arguments in function calls and enhance receiver extraction for method-style calls * refactor: implement new Flask routes for safe and unsafe shell command execution * refactor: separate receiver handling in SSA operations and enhance taint propagation * refactor: improve arity handling by using arg_uses for positional argument count and enhance witness scoring for tainted arguments * refactor: implement auth decorator extraction and classification for multiple languages * refactor: enhance Rust module path resolution and use map handling for cross-file disambiguation * refactor: introduce CalleeQuery struct for structured callee resolution and enhance resolver logic * refactor: implement same-file identity collision handling for `runTask` to ensure correct resolver behavior * refactor: standardize default struct initialization across multiple files * feat: add scripts for formatting checks and auto-fixes with test summaries * refactor: simplify character splitting and enhance namespace qualifier handling * refactor: improve documentation clarity and enhance code readability in resolver logic * refactor: replace default struct initialization with explicit field assignments for clarity * feat: enhance anonymous function naming by deriving context-based bindings * refactor: streamline match expressions for improved readability and performance * refactor: streamline match expressions for improved readability and performance * refactor: replace loop with while let for improved clarity and performance * feat: add SSA constant propagation support to analysis context for improved accuracy * feat: add SSA constant propagation support to analysis context for improved accuracy * feat: implement shell metacharacter validation and bounded-length checks in Rust analysis * feat: add static map analysis for command injection suppression and type safety * refactor: simplify match statements and reduce line breaks for improved readability * feat(summary): phase 1/5 SinkSite data model for primary sink-location attribution Introduce SinkSite (file_rel, line, col, snippet, cap) carrying the primary sink source-location through function summaries. Swap SsaFuncSummary.param_to_sink and FuncSummary.param_to_sink from a coarse Cap map to a deduped SmallVec<[SinkSite; 1]> per parameter, with a backward-compatible cap_sites() helper and serde defaults so pre-phase-1 on-disk rows continue to deserialise cleanly. Extraction: SinkSiteLocator bundles the tree/bytes/file_rel needed by extract_ssa_func_summary; ParsedFile::extract_ssa_artifacts wires the locator in for the persisted pass-1 path, while pass-2 intra-file transient summaries fall back to cap-only sites (behavior unchanged). Merge: GlobalSummaries::insert now unions sink sites with (file_rel, line, col, cap) dedup via shared union_param_sink_sites helper. Database: JSON-serialised summary columns carry the new shape automatically; no schema change needed. Phase 2 will consume SinkSite in build_taint_diag() to overwrite the caller-site Finding.line with the callee's sink line when resolved via summary. Phase 1 keeps behavior unchanged: scanning tests/benchmark/corpus/rust/cmdi/cmdi_indirect.rs still produces the same (wrong) line 10 finding. Adds round-trip tests covering SinkSite solo, SsaFuncSummary with sink sites, legacy-JSON default handling for both summary types, and merge dedup. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * feat(taint): phase 2/5 thread SinkSite into SsaTaintEvent and Finding Plumb Phase 1's SinkSite through the event pipeline into Findings, no output change yet. SsaTaintEvent gains `primary_sink_site: Option<SinkSite>`; when the main or callback sink-emission path has non-empty `param_to_sink_sites`, filter to sites whose `(line != 0) && (cap ∩ sink_caps != ∅)` and emit one event per distinct site — the multi-primary collapse keeps each downstream Finding single-primary. Resolution: ResolvedSummary and SinkInfo gain mirror `param_to_sink_sites` fields, populated from `SsaFuncSummary.param_to_sink` (SSA + callback paths) and `FuncSummary.param_to_sink` (global paths). Label, local-summary, and interop resolution paths leave the field empty — they only ever had cap-level info to begin with. Finding: new `primary_location: Option<SinkLocation>` with `file_rel/line/col`. `ssa_events_to_findings` maps `event.primary_sink_site` → `Finding.primary_location`, filtering cap-only sites (`line == 0`) to `None` so the (0,0) sentinel never leaks to formatters. Dedup key extended with the primary location so multi-site events aren't collapsed back together. Invariants (debug_assert!): * every SinkSite reaching emission has `line != 0 && cap ∩ sink_caps != ∅` — enforced by the pick_primary_sink_sites* filters; * every populated Finding.primary_location has `line != 0` AND non-empty `file_rel` — the cap-only → None translation upstream guarantees this. Deliberately independent of `uses_summary`: that flag tracks whether the *taint chain* used a summary, whereas primary attribution requires only that the *sink* itself was summary-resolved. A local source reaching a cross-file sink produces `uses_summary=false` alongside a populated primary_location — documented on Finding.primary_location, covered by `cross_file_sink_finding_carries_primary_location`. build_taint_diag, SARIF/JSON/explanation formatters, and the benchmark scorer remain untouched: finding.line still comes from `cfg_graph[finding.sink]`, so cmdi_indirect.rs still reports line 10 and the benchmark's rs-cmdi-003 row still shows FN in the LOC column. Tests: `cross_file_sink_finding_carries_primary_location` (proves plumbing via a synthetic FuncSummary carrying a SinkSite at 42:5) and `cross_file_sink_cap_only_site_leaves_primary_location_none` (regression guard against cap-only sites surfacing). All 1566 lib tests + integration tests pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(output): phase 3/5 consume primary sink location in diag + SARIF When a finding's primary_location (populated in phase 2 from a callee summary's SinkSite) names the dangerous instruction inside a callee body, attribute the diagnostic line to that location instead of the caller's call site. The call site is demoted to a Call step in flow_steps, and a synthetic Sink step at the primary location is appended so analysts still see the full trace. Changes: - Add scan_root parameter to build_taint_diag so file_rel can be resolved back to an absolute path via a shared resolve_file_rel helper. Empty file_rel (single-file scans where namespace == "") resolves to the file under analysis. - Extend SinkLocation with snippet, carried from the upstream SinkSite so the formatter needs no second file read. - Relax the ssa_events_to_findings debug_assert to allow empty file_rel, which is valid when scan root equals the file itself. - SARIF: emit data-flow as codeFlows[0].threadFlows[0].locations[]; locations[0] already reflects the primary sink position via the updated diag line/col. Acceptance: scan on tests/benchmark/corpus/rust/cmdi/cmdi_indirect.rs now reports line 5 (Command::new) as the primary sink, with the call site at line 10 visible in flow_steps. Two expect.json fixtures updated (must_match line_range widened): - javascript/taint/context_sensitive_call: 12-14 -> 7-14 (line 8 is the real sink inside run()). - rust/cfg/closure_async: 10-10 -> 10-11 (line 11 is Command::new inside the closure). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(bench): phase 4/5 validate primary sink attribution across corpus Extend the benchmark scorer and ground truth to lock in phase 3's primary-location behavior, and add fixtures that exercise the new capability end-to-end. Scorer (tests/benchmark_test.rs): - Add optional `expected_call_site_lines: Option<Vec<[usize; 2]>>` on Case. When present, score_location_level additionally requires at least one flow_step in the finding's evidence trace to fall within ±2 of the call-site range. When absent, the check is skipped — fully forward-compatible with existing fixtures. - Retain ±2 tolerance on expected_sink_lines (compared against the now-primary Diag.line post-phase-3). Ground truth edits: - rs-cmdi-cross-001: expected_sink_lines [8,8] -> [9,9]. Line 8 is the transform::wrap call site (a cross-file propagator, not a sink); line 9 is Command::new, the real sink. The ±2 tolerance happened to mask this stale attribution but it was semantically wrong — phase 4 is the right time to correct it. Also adds expected_call_site_lines [8,8] so the new field is exercised on an existing cross-file case. - rs-cmdi-003: adds expected_call_site_lines [10,10] (run_cmd call). This fixture's sink (Command::new inside run_cmd at line 5) was the motivating case for phases 1-3; adding the call-site assertion guards against regression to caller-line attribution. New fixtures: - rust/cmdi/cmdi_indirect_multisink.rs (rs-cmdi-009): helper run_both takes two tainted params and invokes two Command sinks on consecutive lines. Locks in that primary line lands inside the helper (lines 5-6), not at the caller (line 12). Notes document that SinkSite is currently one-per-callee so both findings today collapse onto the first sink; expected_sink_lines=[5,6] and expected_call_site_lines=[12,12] stay valid either way. - python/cmdi/cross_indirect_sink/{app.py,helper.py} (py-cmdi-cross- 004): sink os.system lives in helper.py (cross-file), caller in app.py reads env source and calls run_cmd. Verifies phase 3's cross-file primary attribution: Diag.path = helper.py, Diag.line = 5, with app.py:7 recorded in flow_steps as a Call step. Acceptance: - `cargo test --test benchmark_test -- --ignored --nocapture` passes. - rs-cmdi-003 is TP/TP/TP (the target flip FN->TP at LOC). All pre-existing TP/TP/TP fixtures remain TP/TP/TP; 2 new fixtures are TP/TP/TP. - Aggregate rule-level: TP=158 FP=10 FN=1 TN=97, P=0.940 R=0.994 F1=0.966 on the 266-case corpus (was TP=156 FP=10 FN=1 TN=97 on 264 pre-phase-4, delta is the +2 new cases both resolving TP). - Full `cargo test` green (1566 lib tests + all integration tests). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(taint): phase 5/5 lock Finding.primary_location contract via regression test Add a regression test in src/taint/ssa_transfer.rs that wires up a synthetic SsaFuncSummary with a SinkSite at other.rs:42:10 and drives the three emission stages (pick_primary_sink_sites → emit_ssa_taint_events → ssa_events_to_findings) against a minimal caller SSA body. Asserts the resulting Finding.primary_location is exactly that triple. The existing integration tests in src/taint/tests.rs cover the coarse FuncSummary path end-to-end through analyse_file. This test locks in the lower-level SSA-side plumbing so a future refactor that silently drops the site between pick → emit → findings fails here rather than only at the benchmark layer. Also refreshes tests/benchmark/results/latest.json (timestamp only; rs-cmdi-003 remains TP/TP/TP and the aggregate P/R/F1 are unchanged from phase 4). Closes the primary sink-location attribution feature (phases 1-5/5): * Phase 1 — SinkSite data model on summaries. * Phase 2 — SinkSite threaded into SsaTaintEvent and Finding. * Phase 3 — diag + SARIF consume primary_location. * Phase 4 — benchmark validates primary_call_site_lines across corpus. * Phase 5 — regression test locks the event→finding contract. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * refactor: clean up formatting and improve readability in multiple files * refactor: simplify type definition for deduplication key in findings * test(harness): add must_not_match expectation for FP regression guards Extends ExpectedFinding with must_not_match field that asserts a diagnostic must NOT fire — presence is a hard failure. Non-consuming scan so it coexists with must_match entries on the same rule_id. Adds forbidden_violations accumulator and updates summary line. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * feat(regression): update expectations to ensure must_not_match for various taint and resource leak rules * feat: implement auto-seeding for JS/TS handler parameters to enhance taint tracking * feat: update switch statement handling to improve control flow analysis * feat: implement promisify alias handling for JS/TS to enhance taint tracking * feat: enhance taint tracking by refining expectation handling and adding mode filtering * feat: refine SQL handling in stream processing and enhance auto-seeding for handler parameters * feat: update taint tracking rules to enforce full mode matching and improve flow analysis * feat: enhance Ruby subshell handling to improve taint tracking and flow analysis * feat: update xss_response expectations to refine taint flow analysis and enhance regression guarding * feat: refine framework detection and update expectation handling for Echo and Sinatra * feat: implement max_count for taint tracking expectations and deduplicate findings * feat: add strict_unexpected handling for taint-unsanitised-flow in expectation files * feat: enhance deduplication of taint-unsanitised-flow findings by collapsing based on line and severity * feat: add strict_unexpected handling for taint-unsanitised-flow in multiple expectation files * feat: add structural invariant checks for SSA bodies * feat: ensure deterministic phi emission order using BTreeSet * feat: enhance handling of terminators to ensure authoritative flow through successor edges * feat: enhance Goto terminator handling to ensure all successors are marked executable * feat: refactor code for improved readability and organization * feat: simplify predicate checks and enhance readability in SSA handling * feat: implement per-file parse timeout and enhance file size handling * feat: migrate analysis engine toggles from environment variables to configuration file * feat: remove unnecessary whitespace in hostile_input_tests.rs * feat: remove unnecessary whitespace in hostile_input_tests.rs * feat: update dependencies and enhance documentation on language maturity * feat: enhance security headers and improve request body limits * feat: implement sink capability bits for deduplication and enhance evidence tagging * feat: implement dynamic activation handling for gated sinks and enhance validation logic * feat: enhance configuration documentation and clarify inline analysis cache behavior * feat: implement panic recovery during analysis to continue scans past errors * feat: add expectations configuration for taint analysis and performance metrics * feat: enhance error handling and logging during file reading and mutex locking * feat: add cross-file body loading tests and plumbing for CF-1 phase * feat: implement cross-file k=1 context-sensitive inline taint analysis with new tests and fixtures * feat: implement indexed-scan parity in cross-file inline analysis with new dropdown and copy functionality * feat: enhance classification span handling in CFG and AST for improved source attribution * feat: add new Express routes for handling user input and telemetry data * feat: implement ternary expression handling in CFG with diamond structure for JS/TS * feat: implement Phase CF-3 abstract-domain transfer channels in summaries * feat: add support for string-prefix transfer in cross-file calls and update tests * docs: reduce RESULTS.md doc size * feat: implement Phase CF-4 per-return-path summary decomposition with tests * feat: update parameter handling in pass1 and refactor SsaFuncSummary initialization * feat: implement Phase CF-5 for cross-file SCC joint fixed-point convergence with new flags and tests * feat: implement Phase CF-6 with parameter-granularity points-to summaries and associated tests * refactor: update comments and documentation for clarity and consistency * style: format code for consistency and readability * refactor: simplify verdict handling and improve edge checking logic * refactor: optimize path and identifier collection by avoiding unnecessary cloning * chore: update Cargo.toml for Rust version 1.85 and add ignored files; modify CHANGELOG and README for clarity on state analysis defaults * refactor: update documentation and improve clarity in configuration files * refactor: update documentation and improve clarity in configuration files * feat: add JS/TS pass-2 convergence tests and expectations configuration * feat: add Phase 5 regression tests for inline cache origin attribution and update related logic * feat: implement Phase 7 deduplication and alternative path linking for taint findings * feat: implement structural DFS index for anonymous functions and update naming conventions * feat: add Phase 8 regression tests for container-element taint in JS and Python * feat: add engine-depth profiles and explain-engine option for CLI * feat: update expectations and add new README fixtures for multi-file scan regression * feat: implement Phase 11 callback-alias and factory patterns with regression tests * feat: implement Terminator::Switch for multi-way dispatch and add regression tests * feat: add real-CVE benchmark fixtures for CVE-2023-48022, CVE-2019-14939, and CVE-2023-26159 with corresponding patched variants * refactor: extract cfg and ssa_transfer to submodules * refactor: cargo fmt * refactor: remove unnecessary blank line in cfg_tests.rs * refactor: remove unnecessary planning file * chore: update Rust version to 1.88 and bump dependencies in Cargo files * feat: enhance triage UI with new layout and controls, update README for clarity * feat: enhance triage UI with new layout and controls, update README for clarity * chore: remove outdated section from README for version 0.5.0 * docs: improve clarity and consistency in README content * chore: add "GPL-3.0-or-later" to license options in about.toml * chore: update license handling in about.toml and check-licenses.mjs * style: format code for improved readability in TriagePage component * style: format code for improved readability in TriagePage component * chore: enhance license handling and improve body_id scoping in seed lookup * feat: introduce owner and parent body IDs for enhanced seed scoping * feat: implement direction-aware engine provenance with new CLI flag for strict CI gating * feat: add Undef SSA operation for improved control-flow handling * style: improve code formatting for consistency and readability in multiple files * feat: add 16-function chain SCC across multiple files for enhanced analysis * style: simplify code formatting for improved readability in multiple files * fix: update CapHitReason default implementation and improve README clarity * docs: enhance README with detailed explanations of taint analysis and limitations * docs: refine README for clarity and consistency in taint analysis section * style: improve code formatting for better readability in NewScanModal and scans * fix: update cargo-about command to use --offline for deterministic license generation * fix: update cargo-about command to use --offline for deterministic license generation * ci: add step to prime cargo registry cache for deterministic license generation * feat: add support for non-sink collections in authorization analysis * feat: enhance authorization checks with row-level ownership equality and binding tracking * feat: implement self-scoped user handling and enhance ownership checks * refactor: simplify assertions and formatting in authorization analysis tests * fix: normalize line endings in THIRDPARTY-LICENSES.html generation and update README with AI disclosure * docs: update AI disclosure section for clarity and conciseness * feat: add AI Contribution Policy and update contributing guidelines for AI assistance disclosure * feat: enhance authorization analysis with SSA-derived variable type classification * feat: implement auth_finding_to_diag function for enhanced security diagnostics * feat: add args_value_refs to CallSite struct for enhanced argument tracking * feat: add args_value_refs to CallSite struct for enhanced argument tracking * feat: add direction-aware engine provenance with LossDirection classification and new CLI flag * feat: simplify strip_cap_from_call_args call by removing unnecessary line breaks * feat: enhance error message handling in cli_validation_tests for better Windows compatibility * feat: optimize release profile settings in Cargo.toml and update CodeQL configuration * feat: enhance release build process with SBOM generation and SLSA provenance * feat: update actions/checkout and actions/setup-node to v6, enhance CLI options, and improve auth-check summaries * feat: introduce PathFact handling for path safety checks and rejection logic * feat: introduce PathFact handling for path safety checks and rejection logic * feat: update benchmark data and enhance path sanitization logic with new safety checks * feat: document AI assistance in frontend UI development and human review process * feat: add return path facts for enhanced path safety checks and update documentation * chore: update release date for version 0.5.0 in CHANGELOG.md * chore: clean up ci.yml by removing outdated comments and clarifying steps * feat: implement cross-language path sanitizers and validators for enhanced security * feat: enhance SSA value usage tracking by including block terminators and improve path safety checks * feat: enhance switch statement handling by adding per-case path constraints and support for exclusive cases * refactor: simplify conditional formatting and improve code readability in executor and lower modules * feat: add vulnerable examples for various languages demonstrating authentication and sanitization issues * feat: enhance actor context recognition for self-actor identifiers and add support for global non-sink receivers * feat: enhance actor context recognition for self-actor identifiers and add support for global non-sink receivers * feat: add transform classifiers for Java, Go, and Ruby with corresponding tests * refactor: clarify comments on reassign-to-constant idiom and sink behavior in guards.rs --------- Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com> Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
Eli Peter
GitHub
parent
c4ce08b452
commit
41128177d2
2144 changed files with 201812 additions and 8927 deletions
2159
src/symex/executor.rs
Normal file
2159
src/symex/executor.rs
Normal file
File diff suppressed because it is too large
Load diff
777
src/symex/heap.rs
Normal file
777
src/symex/heap.rs
Normal file
|
|
@ -0,0 +1,777 @@
|
|||
//! Symbolic heap: field-sensitive memory model for symbolic execution.
|
||||
//!
|
||||
//! Maps `(HeapObjectId, FieldSlot)` → `SymbolicValue`, enabling the symbolic
|
||||
//! executor to track taint through object property stores/loads and container
|
||||
//! operations. Uses allocation-site identities from `PointsToResult` to
|
||||
//! distinguish different objects.
|
||||
//!
|
||||
//! Design:
|
||||
#![allow(clippy::collapsible_if, clippy::new_without_default)]
|
||||
//! - `FieldSlot::Named` for object properties (per-field precision).
|
||||
//! - `FieldSlot::Elements` for container contents (flow-insensitive union —
|
||||
//! deliberately lower precision than named fields).
|
||||
//! - Bounded: `MAX_HEAP_ENTRIES` total, `MAX_FIELDS_PER_OBJECT` per object.
|
||||
//! Overflow silently drops the store (conservative: subsequent load → `Unknown`).
|
||||
//! - `widen()` sets values to `Unknown` but preserves taint flags.
|
||||
//! - `Clone` for fork-point cloning in multi-path exploration.
|
||||
|
||||
use std::collections::{HashMap, HashSet};
|
||||
|
||||
use crate::ssa::const_prop::ConstLattice;
|
||||
use crate::ssa::heap::{HeapObjectId, PointsToResult};
|
||||
use crate::ssa::ir::{SsaBody, SsaValue};
|
||||
|
||||
use super::value::SymbolicValue;
|
||||
|
||||
/// Maximum total heap entries across all objects.
|
||||
const MAX_HEAP_ENTRIES: usize = 64;
|
||||
|
||||
/// Maximum named/elements fields tracked per individual object.
|
||||
/// `Index(*)` entries are bounded separately by [`MAX_TRACKED_INDICES`].
|
||||
const MAX_FIELDS_PER_OBJECT: usize = 8;
|
||||
|
||||
/// Maximum distinct `Index(n)` slots tracked per heap object.
|
||||
/// When exceeded, all `Index(*)` entries for that object collapse into
|
||||
/// `Elements` (taint unioned, value set to `Unknown`).
|
||||
pub const MAX_TRACKED_INDICES: usize = 16;
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Types
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/// Heap key: allocation-site identity + field slot.
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub struct HeapKey {
|
||||
pub object: HeapObjectId,
|
||||
pub field: FieldSlot,
|
||||
}
|
||||
|
||||
/// Distinguishes named object fields, per-index array slots, and the
|
||||
/// element-insensitive fallback.
|
||||
///
|
||||
/// Ordering: `Elements` < `Index(0)` < `Index(1)` < … < `Named("a")` < …
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub enum FieldSlot {
|
||||
/// Named property: `obj.username`, `config.host`.
|
||||
Named(String),
|
||||
/// Element-insensitive container contents (flow-insensitive union).
|
||||
/// Represents an unknown/dynamic element write that may affect any index.
|
||||
/// `push`/`pop` without a known constant index land here.
|
||||
Elements,
|
||||
/// Concrete per-index slot, proven by constant propagation.
|
||||
/// `arr[0]`, `list.get(1)` when the index resolves to a known integer.
|
||||
Index(u64),
|
||||
}
|
||||
|
||||
impl PartialOrd for FieldSlot {
|
||||
fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
|
||||
Some(self.cmp(other))
|
||||
}
|
||||
}
|
||||
|
||||
impl Ord for FieldSlot {
|
||||
fn cmp(&self, other: &Self) -> std::cmp::Ordering {
|
||||
use std::cmp::Ordering;
|
||||
match (self, other) {
|
||||
(FieldSlot::Elements, FieldSlot::Elements) => Ordering::Equal,
|
||||
(FieldSlot::Elements, _) => Ordering::Less,
|
||||
(_, FieldSlot::Elements) => Ordering::Greater,
|
||||
(FieldSlot::Index(a), FieldSlot::Index(b)) => a.cmp(b),
|
||||
(FieldSlot::Index(_), FieldSlot::Named(_)) => Ordering::Less,
|
||||
(FieldSlot::Named(_), FieldSlot::Index(_)) => Ordering::Greater,
|
||||
(FieldSlot::Named(a), FieldSlot::Named(b)) => a.cmp(b),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Metadata recorded at store/load time for witness generation.
|
||||
///
|
||||
/// Recorded explicitly rather than reconstructed heuristically from `var_name`
|
||||
/// strings, ensuring witness accuracy even when heap loads produce SSA values
|
||||
/// without dotted names.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct FieldAccessRecord {
|
||||
/// Receiver expression text: `"user"`, `"req.body"`.
|
||||
pub object_name: String,
|
||||
/// Field name: `"name"`, `"username"`.
|
||||
pub field_name: String,
|
||||
/// The SSA value that was stored/loaded.
|
||||
pub ssa_value: SsaValue,
|
||||
}
|
||||
|
||||
/// Bounded symbolic heap tracking field-level symbolic values and taint.
|
||||
///
|
||||
/// Cloned at fork points during multi-path exploration. Bounded
|
||||
/// by [`MAX_HEAP_ENTRIES`] total entries and [`MAX_FIELDS_PER_OBJECT`] per
|
||||
/// object to prevent blowup on object-heavy code.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct SymbolicHeap {
|
||||
/// Maps (object, field) → symbolic expression.
|
||||
fields: HashMap<HeapKey, SymbolicValue>,
|
||||
/// Tracks which heap keys carry taint.
|
||||
tainted_keys: HashSet<HeapKey>,
|
||||
/// Field access trace for witness generation.
|
||||
field_accesses: Vec<FieldAccessRecord>,
|
||||
}
|
||||
|
||||
impl SymbolicHeap {
|
||||
/// Create an empty symbolic heap.
|
||||
pub fn new() -> Self {
|
||||
SymbolicHeap {
|
||||
fields: HashMap::new(),
|
||||
tainted_keys: HashSet::new(),
|
||||
field_accesses: Vec::new(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Store a symbolic value into a heap field.
|
||||
///
|
||||
/// Bounded: silently drops the store if [`MAX_HEAP_ENTRIES`] or
|
||||
/// [`MAX_FIELDS_PER_OBJECT`] would be exceeded. `Index(*)` entries are
|
||||
/// bounded by [`MAX_TRACKED_INDICES`] per object; overflow collapses all
|
||||
/// indexed entries into `Elements`.
|
||||
pub fn store(&mut self, key: HeapKey, value: SymbolicValue, tainted: bool) {
|
||||
// Index overflow: collapse to Elements if too many distinct indices.
|
||||
if let FieldSlot::Index(_) = &key.field {
|
||||
if !self.fields.contains_key(&key)
|
||||
&& self.count_indices_for(key.object) >= MAX_TRACKED_INDICES
|
||||
{
|
||||
self.collapse_indices_to_elements(key.object);
|
||||
// Redirect store to Elements.
|
||||
let elem_key = HeapKey {
|
||||
object: key.object,
|
||||
field: FieldSlot::Elements,
|
||||
};
|
||||
// collapse_indices_to_elements already inserted Elements;
|
||||
// update with the new value/taint.
|
||||
self.fields.insert(elem_key.clone(), value);
|
||||
if tainted {
|
||||
self.tainted_keys.insert(elem_key);
|
||||
}
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
// Check bounds (only for new entries).
|
||||
if !self.fields.contains_key(&key) {
|
||||
if self.fields.len() >= MAX_HEAP_ENTRIES {
|
||||
return; // global cap
|
||||
}
|
||||
// Index entries bypass per-object field cap (bounded by MAX_TRACKED_INDICES).
|
||||
if !matches!(key.field, FieldSlot::Index(_))
|
||||
&& self.fields_for_object(key.object) >= MAX_FIELDS_PER_OBJECT
|
||||
{
|
||||
return; // per-object cap for Named/Elements
|
||||
}
|
||||
}
|
||||
|
||||
self.fields.insert(key.clone(), value);
|
||||
if tainted {
|
||||
self.tainted_keys.insert(key);
|
||||
} else {
|
||||
self.tainted_keys.remove(&key);
|
||||
}
|
||||
}
|
||||
|
||||
/// Load the symbolic value for a heap field.
|
||||
///
|
||||
/// For `Index(n)`: returns the precise per-index value if present;
|
||||
/// otherwise falls back to the `Elements` value (conservative).
|
||||
/// Returns `Unknown` if neither is present.
|
||||
pub fn load(&self, key: &HeapKey) -> SymbolicValue {
|
||||
if let FieldSlot::Index(_) = &key.field {
|
||||
// Precise index wins; fall back to Elements.
|
||||
if let Some(val) = self.fields.get(key) {
|
||||
return val.clone();
|
||||
}
|
||||
let elem_key = HeapKey {
|
||||
object: key.object,
|
||||
field: FieldSlot::Elements,
|
||||
};
|
||||
return self
|
||||
.fields
|
||||
.get(&elem_key)
|
||||
.cloned()
|
||||
.unwrap_or(SymbolicValue::Unknown);
|
||||
}
|
||||
self.fields
|
||||
.get(key)
|
||||
.cloned()
|
||||
.unwrap_or(SymbolicValue::Unknown)
|
||||
}
|
||||
|
||||
/// Check if a heap field is tainted.
|
||||
///
|
||||
/// For `Index(n)`: returns `true` if either `Index(n)` or `Elements` is
|
||||
/// tainted. An unknown/dynamic store to `Elements` conservatively poisons
|
||||
/// all indexed reads.
|
||||
pub fn is_tainted(&self, key: &HeapKey) -> bool {
|
||||
if self.tainted_keys.contains(key) {
|
||||
return true;
|
||||
}
|
||||
if let FieldSlot::Index(_) = &key.field {
|
||||
let elem_key = HeapKey {
|
||||
object: key.object,
|
||||
field: FieldSlot::Elements,
|
||||
};
|
||||
return self.tainted_keys.contains(&elem_key);
|
||||
}
|
||||
false
|
||||
}
|
||||
|
||||
/// Iterate over all heap entries (key → value).
|
||||
pub fn entries(&self) -> impl Iterator<Item = (&HeapKey, &SymbolicValue)> {
|
||||
self.fields.iter()
|
||||
}
|
||||
|
||||
/// Record a field access for witness generation.
|
||||
pub fn record_access(&mut self, record: FieldAccessRecord) {
|
||||
self.field_accesses.push(record);
|
||||
}
|
||||
|
||||
/// Get the field access trace for witness generation.
|
||||
pub fn field_accesses(&self) -> &[FieldAccessRecord] {
|
||||
&self.field_accesses
|
||||
}
|
||||
|
||||
/// Compute a compact 64-bit fingerprint of the heap state.
|
||||
///
|
||||
/// Used as part of the interprocedural cache key.
|
||||
/// Deterministic: entries are sorted by key for consistent hashing.
|
||||
pub fn fingerprint(&self) -> u64 {
|
||||
if self.fields.is_empty() {
|
||||
return 0;
|
||||
}
|
||||
// Sort keys deterministically using FieldSlot::Ord.
|
||||
let mut keys: Vec<&HeapKey> = self.fields.keys().collect();
|
||||
keys.sort_by(|a, b| {
|
||||
let obj_a = (a.object.0).0;
|
||||
let obj_b = (b.object.0).0;
|
||||
obj_a.cmp(&obj_b).then_with(|| a.field.cmp(&b.field))
|
||||
});
|
||||
|
||||
let mut h: u64 = 0;
|
||||
for key in keys {
|
||||
let val = &self.fields[key];
|
||||
let tainted: u64 = if self.tainted_keys.contains(key) {
|
||||
1
|
||||
} else {
|
||||
0
|
||||
};
|
||||
let val_tag: u64 = match val {
|
||||
SymbolicValue::Concrete(n) => (*n as u64).wrapping_mul(31),
|
||||
SymbolicValue::ConcreteStr(s) => {
|
||||
let mut sh: u64 = 0;
|
||||
for b in s.bytes().take(8) {
|
||||
sh = sh.wrapping_mul(31).wrapping_add(b as u64);
|
||||
}
|
||||
sh
|
||||
}
|
||||
SymbolicValue::Unknown => 0xFF,
|
||||
_ => 0xFE,
|
||||
};
|
||||
// Include field variant discriminant for Index(n) distinction.
|
||||
let field_tag: u64 = match &key.field {
|
||||
FieldSlot::Elements => 0,
|
||||
FieldSlot::Index(n) => 1u64.wrapping_add(*n),
|
||||
FieldSlot::Named(_) => 2, // name captured in existing hash via val_tag
|
||||
};
|
||||
h = h
|
||||
.wrapping_mul(67)
|
||||
.wrapping_add(val_tag)
|
||||
.wrapping_add(tainted << 32)
|
||||
.wrapping_add(field_tag << 48);
|
||||
}
|
||||
h
|
||||
}
|
||||
|
||||
/// Widen all heap entries to `Unknown`, preserving taint flags.
|
||||
///
|
||||
/// Called at loop heads after bounded unrolling. `Index(*)` entries are
|
||||
/// collapsed into `Elements` first (taint unioned), then all remaining
|
||||
/// values are set to `Unknown`.
|
||||
///
|
||||
/// Post-condition: no `Index(*)` keys in `fields`.
|
||||
pub fn widen(&mut self) {
|
||||
// Collapse all Index entries into Elements per object.
|
||||
let objects_with_indices: HashSet<HeapObjectId> = self
|
||||
.fields
|
||||
.keys()
|
||||
.filter(|k| matches!(k.field, FieldSlot::Index(_)))
|
||||
.map(|k| k.object)
|
||||
.collect();
|
||||
for obj in objects_with_indices {
|
||||
self.collapse_indices_to_elements(obj);
|
||||
}
|
||||
|
||||
// Widen all remaining values to Unknown; preserve taint.
|
||||
for value in self.fields.values_mut() {
|
||||
*value = SymbolicValue::Unknown;
|
||||
}
|
||||
// tainted_keys intentionally NOT cleared.
|
||||
}
|
||||
|
||||
/// Count non-index fields stored for a specific object.
|
||||
///
|
||||
/// Excludes `Index(*)` entries — those are bounded separately by
|
||||
/// [`MAX_TRACKED_INDICES`] via [`count_indices_for`].
|
||||
fn fields_for_object(&self, object: HeapObjectId) -> usize {
|
||||
self.fields
|
||||
.keys()
|
||||
.filter(|k| k.object == object && !matches!(k.field, FieldSlot::Index(_)))
|
||||
.count()
|
||||
}
|
||||
|
||||
/// Count distinct `Index(*)` entries for a specific object.
|
||||
fn count_indices_for(&self, object: HeapObjectId) -> usize {
|
||||
self.fields
|
||||
.keys()
|
||||
.filter(|k| k.object == object && matches!(k.field, FieldSlot::Index(_)))
|
||||
.count()
|
||||
}
|
||||
|
||||
/// Collapse all `Index(*)` entries for `object` into `Elements`.
|
||||
///
|
||||
/// - Taint is unioned: if any `Index(*)` was tainted, `Elements` becomes
|
||||
/// tainted (preserving any pre-existing `Elements` taint).
|
||||
/// - Value is set to `Unknown` (no meaningful union of distinct symbolic
|
||||
/// expressions).
|
||||
/// - All `Index(*)` entries are removed.
|
||||
fn collapse_indices_to_elements(&mut self, object: HeapObjectId) {
|
||||
let index_keys: Vec<HeapKey> = self
|
||||
.fields
|
||||
.keys()
|
||||
.filter(|k| k.object == object && matches!(k.field, FieldSlot::Index(_)))
|
||||
.cloned()
|
||||
.collect();
|
||||
|
||||
let any_tainted = index_keys.iter().any(|k| self.tainted_keys.contains(k));
|
||||
|
||||
for k in &index_keys {
|
||||
self.fields.remove(k);
|
||||
self.tainted_keys.remove(k);
|
||||
}
|
||||
|
||||
let elem_key = HeapKey {
|
||||
object,
|
||||
field: FieldSlot::Elements,
|
||||
};
|
||||
// Union taint: preserve existing Elements taint.
|
||||
if any_tainted {
|
||||
self.tainted_keys.insert(elem_key.clone());
|
||||
}
|
||||
// Value → Unknown (may already exist; overwrite is fine).
|
||||
self.fields.insert(elem_key, SymbolicValue::Unknown);
|
||||
}
|
||||
}
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Helpers
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/// Resolve a container operation index argument to a [`FieldSlot`].
|
||||
///
|
||||
/// When the index SSA value is a provably non-negative integer constant
|
||||
/// within [`MAX_TRACKED_INDICES`], returns `Index(n)`. Otherwise returns
|
||||
/// `Elements` (conservative fallback).
|
||||
pub fn resolve_index_slot(
|
||||
index_val: SsaValue,
|
||||
const_values: &HashMap<SsaValue, ConstLattice>,
|
||||
) -> FieldSlot {
|
||||
if let Some(ConstLattice::Int(n)) = const_values.get(&index_val) {
|
||||
if *n >= 0 && (*n as u64) < MAX_TRACKED_INDICES as u64 {
|
||||
return FieldSlot::Index(*n as u64);
|
||||
}
|
||||
}
|
||||
FieldSlot::Elements
|
||||
}
|
||||
|
||||
/// Parse a dotted define/var_name string into `(receiver, field)`.
|
||||
///
|
||||
/// Splits on the last `.`:
|
||||
/// - `"user.name"` → `Some(("user", "name"))`
|
||||
/// - `"a.b.c"` → `Some(("a.b", "c"))`
|
||||
/// - `"noDot"` → `None`
|
||||
/// - `".field"` → `None` (empty receiver)
|
||||
/// - `"obj."` → `None` (empty field)
|
||||
pub fn split_field_access(dotted: &str) -> Option<(&str, &str)> {
|
||||
let dot_pos = dotted.rfind('.')?;
|
||||
if dot_pos == 0 || dot_pos == dotted.len() - 1 {
|
||||
return None;
|
||||
}
|
||||
Some((&dotted[..dot_pos], &dotted[dot_pos + 1..]))
|
||||
}
|
||||
|
||||
/// Resolve a receiver name to an SSA value by scanning `value_defs` backwards.
|
||||
///
|
||||
/// Finds the most recent definition of `receiver_name` that precedes
|
||||
/// `current_value` (by SSA value index). Returns `None` if not found.
|
||||
pub fn resolve_receiver_ssa(
|
||||
receiver_name: &str,
|
||||
ssa: &SsaBody,
|
||||
current_value: SsaValue,
|
||||
) -> Option<SsaValue> {
|
||||
let limit = (current_value.0 as usize).min(ssa.value_defs.len());
|
||||
for idx in (0..limit).rev() {
|
||||
if let Some(ref name) = ssa.value_defs[idx].var_name {
|
||||
if name == receiver_name {
|
||||
return Some(SsaValue(idx as u32));
|
||||
}
|
||||
}
|
||||
}
|
||||
None
|
||||
}
|
||||
|
||||
/// Resolve an SSA value to a singleton `HeapObjectId` via points-to analysis.
|
||||
///
|
||||
/// Returns `Some` only when the points-to set contains exactly one object.
|
||||
/// May-alias (set size > 1) or unknown (not in result) returns `None` —
|
||||
/// the caller should fall through to existing behavior (sound: never pick
|
||||
/// among ambiguous options).
|
||||
pub fn resolve_singleton_object(
|
||||
ssa_val: SsaValue,
|
||||
points_to: &PointsToResult,
|
||||
) -> Option<HeapObjectId> {
|
||||
let pts = points_to.get(ssa_val)?;
|
||||
if pts.len() == 1 {
|
||||
pts.iter().next().copied()
|
||||
} else {
|
||||
None
|
||||
}
|
||||
}
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Tests
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
|
||||
fn obj(n: u32) -> HeapObjectId {
|
||||
HeapObjectId(SsaValue(n))
|
||||
}
|
||||
|
||||
fn named_key(obj_id: u32, field: &str) -> HeapKey {
|
||||
HeapKey {
|
||||
object: obj(obj_id),
|
||||
field: FieldSlot::Named(field.to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
fn elements_key(obj_id: u32) -> HeapKey {
|
||||
HeapKey {
|
||||
object: obj(obj_id),
|
||||
field: FieldSlot::Elements,
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn store_load_roundtrip() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
let key = named_key(0, "name");
|
||||
let val = SymbolicValue::ConcreteStr("alice".to_string());
|
||||
heap.store(key.clone(), val.clone(), false);
|
||||
assert_eq!(heap.load(&key), val);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn load_missing_returns_unknown() {
|
||||
let heap = SymbolicHeap::new();
|
||||
let key = named_key(0, "name");
|
||||
assert_eq!(heap.load(&key), SymbolicValue::Unknown);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn taint_propagation_through_store_load() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
let key = named_key(0, "name");
|
||||
heap.store(key.clone(), SymbolicValue::Symbol(SsaValue(10)), true);
|
||||
assert!(heap.is_tainted(&key));
|
||||
|
||||
// Overwrite with non-tainted value
|
||||
heap.store(key.clone(), SymbolicValue::Concrete(42), false);
|
||||
assert!(!heap.is_tainted(&key));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn max_heap_entries_eviction() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
// Fill MAX_HEAP_ENTRIES entries across many objects
|
||||
for i in 0..MAX_HEAP_ENTRIES as u32 {
|
||||
let key = named_key(i, "f");
|
||||
heap.store(key, SymbolicValue::Concrete(i as i64), false);
|
||||
}
|
||||
assert_eq!(heap.fields.len(), MAX_HEAP_ENTRIES);
|
||||
|
||||
// 65th store should be silently dropped
|
||||
let overflow_key = named_key(999, "overflow");
|
||||
heap.store(overflow_key.clone(), SymbolicValue::Concrete(999), false);
|
||||
assert_eq!(heap.load(&overflow_key), SymbolicValue::Unknown);
|
||||
assert_eq!(heap.fields.len(), MAX_HEAP_ENTRIES);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn max_fields_per_object_eviction() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
// Fill MAX_FIELDS_PER_OBJECT fields on one object
|
||||
for i in 0..MAX_FIELDS_PER_OBJECT {
|
||||
let key = named_key(0, &format!("field_{i}"));
|
||||
heap.store(key, SymbolicValue::Concrete(i as i64), false);
|
||||
}
|
||||
assert_eq!(heap.fields_for_object(obj(0)), MAX_FIELDS_PER_OBJECT);
|
||||
|
||||
// 9th field on same object should be dropped
|
||||
let overflow_key = named_key(0, "overflow");
|
||||
heap.store(overflow_key.clone(), SymbolicValue::Concrete(99), false);
|
||||
assert_eq!(heap.load(&overflow_key), SymbolicValue::Unknown);
|
||||
assert_eq!(heap.fields_for_object(obj(0)), MAX_FIELDS_PER_OBJECT);
|
||||
|
||||
// But a different object is fine
|
||||
let other_key = named_key(1, "ok");
|
||||
heap.store(other_key.clone(), SymbolicValue::Concrete(1), false);
|
||||
assert_eq!(heap.load(&other_key), SymbolicValue::Concrete(1));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn widen_preserves_taint_clears_values() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
let key = named_key(0, "name");
|
||||
heap.store(
|
||||
key.clone(),
|
||||
SymbolicValue::ConcreteStr("alice".to_string()),
|
||||
true,
|
||||
);
|
||||
|
||||
heap.widen();
|
||||
|
||||
// Value is Unknown after widening
|
||||
assert_eq!(heap.load(&key), SymbolicValue::Unknown);
|
||||
// Taint is preserved
|
||||
assert!(heap.is_tainted(&key));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn split_field_access_cases() {
|
||||
assert_eq!(split_field_access("obj.field"), Some(("obj", "field")));
|
||||
assert_eq!(split_field_access("a.b.c"), Some(("a.b", "c")));
|
||||
assert_eq!(split_field_access("noDot"), None);
|
||||
assert_eq!(split_field_access(".field"), None);
|
||||
assert_eq!(split_field_access("obj."), None);
|
||||
assert_eq!(split_field_access(""), None);
|
||||
assert_eq!(split_field_access("."), None);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn resolve_singleton_returns_none_for_absent() {
|
||||
// PointsToResult::empty() has no entries → None for any query.
|
||||
let pts = PointsToResult::empty();
|
||||
assert_eq!(resolve_singleton_object(SsaValue(0), &pts), None);
|
||||
assert_eq!(resolve_singleton_object(SsaValue(99), &pts), None);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn field_slot_named_vs_elements_distinct() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
let named = named_key(0, "items");
|
||||
let elements = elements_key(0);
|
||||
|
||||
heap.store(named.clone(), SymbolicValue::Concrete(1), false);
|
||||
heap.store(elements.clone(), SymbolicValue::Concrete(2), true);
|
||||
|
||||
assert_eq!(heap.load(&named), SymbolicValue::Concrete(1));
|
||||
assert_eq!(heap.load(&elements), SymbolicValue::Concrete(2));
|
||||
assert!(!heap.is_tainted(&named));
|
||||
assert!(heap.is_tainted(&elements));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn field_access_recording() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
assert!(heap.field_accesses().is_empty());
|
||||
|
||||
heap.record_access(FieldAccessRecord {
|
||||
object_name: "user".to_string(),
|
||||
field_name: "name".to_string(),
|
||||
ssa_value: SsaValue(5),
|
||||
});
|
||||
|
||||
assert_eq!(heap.field_accesses().len(), 1);
|
||||
assert_eq!(heap.field_accesses()[0].object_name, "user");
|
||||
assert_eq!(heap.field_accesses()[0].field_name, "name");
|
||||
}
|
||||
|
||||
// ── Index sensitivity tests ────────────────────────────────
|
||||
|
||||
fn index_key(obj_id: u32, idx: u64) -> HeapKey {
|
||||
HeapKey {
|
||||
object: obj(obj_id),
|
||||
field: FieldSlot::Index(idx),
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn per_index_store_load() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
heap.store(index_key(0, 0), SymbolicValue::Concrete(10), false);
|
||||
|
||||
assert_eq!(heap.load(&index_key(0, 0)), SymbolicValue::Concrete(10));
|
||||
// Different index: not stored → Unknown
|
||||
assert_eq!(heap.load(&index_key(0, 1)), SymbolicValue::Unknown);
|
||||
// Elements: not stored → Unknown
|
||||
assert_eq!(heap.load(&elements_key(0)), SymbolicValue::Unknown);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn index_load_falls_back_to_elements() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
heap.store(elements_key(0), SymbolicValue::Concrete(99), false);
|
||||
|
||||
// Index(0) not stored → falls back to Elements value.
|
||||
assert_eq!(heap.load(&index_key(0, 0)), SymbolicValue::Concrete(99));
|
||||
assert_eq!(heap.load(&index_key(0, 5)), SymbolicValue::Concrete(99));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn index_taint_includes_elements_taint() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
heap.store(elements_key(0), SymbolicValue::Unknown, true);
|
||||
|
||||
// Elements taint poisons all Index reads.
|
||||
assert!(heap.is_tainted(&index_key(0, 0)));
|
||||
assert!(heap.is_tainted(&index_key(0, 7)));
|
||||
// But not a different object.
|
||||
assert!(!heap.is_tainted(&index_key(1, 0)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn index_and_elements_coexist() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
heap.store(index_key(0, 0), SymbolicValue::Concrete(10), false);
|
||||
heap.store(elements_key(0), SymbolicValue::Concrete(99), true);
|
||||
|
||||
// Value: precise Index(0) wins over Elements.
|
||||
assert_eq!(heap.load(&index_key(0, 0)), SymbolicValue::Concrete(10));
|
||||
// Value: Index(1) not stored → falls back to Elements.
|
||||
assert_eq!(heap.load(&index_key(0, 1)), SymbolicValue::Concrete(99));
|
||||
// Taint: Elements taint poisons Index(0) reads.
|
||||
assert!(heap.is_tainted(&index_key(0, 0)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn elements_store_after_index_preserves_value() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
// Step 1: precise store to Index(1).
|
||||
heap.store(
|
||||
index_key(0, 1),
|
||||
SymbolicValue::ConcreteStr("safe".to_string()),
|
||||
false,
|
||||
);
|
||||
// Step 2: unknown/dynamic store to Elements (tainted).
|
||||
heap.store(elements_key(0), SymbolicValue::Unknown, true);
|
||||
|
||||
// Value: Index(1) still wins (precise).
|
||||
assert_eq!(
|
||||
heap.load(&index_key(0, 1)),
|
||||
SymbolicValue::ConcreteStr("safe".to_string())
|
||||
);
|
||||
// Taint: conservative — Elements taint poisons Index(1).
|
||||
assert!(heap.is_tainted(&index_key(0, 1)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn index_overflow_collapses() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
// Fill MAX_TRACKED_INDICES indices, mark last one tainted.
|
||||
for i in 0..MAX_TRACKED_INDICES as u64 {
|
||||
let tainted = i == (MAX_TRACKED_INDICES as u64 - 1);
|
||||
heap.store(index_key(0, i), SymbolicValue::Concrete(i as i64), tainted);
|
||||
}
|
||||
assert_eq!(heap.count_indices_for(obj(0)), MAX_TRACKED_INDICES);
|
||||
|
||||
// One more triggers collapse.
|
||||
heap.store(
|
||||
index_key(0, MAX_TRACKED_INDICES as u64),
|
||||
SymbolicValue::Concrete(999),
|
||||
false,
|
||||
);
|
||||
|
||||
// No Index(*) keys remain.
|
||||
assert_eq!(heap.count_indices_for(obj(0)), 0);
|
||||
// Elements exists and carries taint (from the previously tainted index).
|
||||
assert!(heap.is_tainted(&elements_key(0)));
|
||||
// Elements value is the overflow store's value (collapse wrote Unknown,
|
||||
// then the redirect wrote 999).
|
||||
assert_eq!(heap.load(&elements_key(0)), SymbolicValue::Concrete(999));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn widen_collapses_indices() {
|
||||
let mut heap = SymbolicHeap::new();
|
||||
heap.store(index_key(0, 0), SymbolicValue::Concrete(10), true);
|
||||
heap.store(index_key(0, 1), SymbolicValue::Concrete(20), false);
|
||||
|
||||
heap.widen();
|
||||
|
||||
// No Index keys remain.
|
||||
assert_eq!(heap.count_indices_for(obj(0)), 0);
|
||||
// Elements value is Unknown (widened).
|
||||
assert_eq!(heap.load(&elements_key(0)), SymbolicValue::Unknown);
|
||||
// Elements taint preserved (Index(0) was tainted).
|
||||
assert!(heap.is_tainted(&elements_key(0)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn fingerprint_distinguishes_indices() {
|
||||
let mut h1 = SymbolicHeap::new();
|
||||
h1.store(index_key(0, 0), SymbolicValue::Concrete(42), false);
|
||||
|
||||
let mut h2 = SymbolicHeap::new();
|
||||
h2.store(index_key(0, 1), SymbolicValue::Concrete(42), false);
|
||||
|
||||
assert_ne!(h1.fingerprint(), h2.fingerprint());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn resolve_index_slot_cases() {
|
||||
let mut cv = HashMap::new();
|
||||
cv.insert(SsaValue(0), ConstLattice::Int(3));
|
||||
cv.insert(SsaValue(1), ConstLattice::Int(-1));
|
||||
cv.insert(SsaValue(2), ConstLattice::Int(MAX_TRACKED_INDICES as i64));
|
||||
cv.insert(SsaValue(3), ConstLattice::Str("hello".into()));
|
||||
|
||||
// Known positive int within bounds → Index(3).
|
||||
assert_eq!(resolve_index_slot(SsaValue(0), &cv), FieldSlot::Index(3));
|
||||
// Negative → Elements.
|
||||
assert_eq!(resolve_index_slot(SsaValue(1), &cv), FieldSlot::Elements);
|
||||
// Out of bounds (= MAX_TRACKED_INDICES) → Elements.
|
||||
assert_eq!(resolve_index_slot(SsaValue(2), &cv), FieldSlot::Elements);
|
||||
// Not an int → Elements.
|
||||
assert_eq!(resolve_index_slot(SsaValue(3), &cv), FieldSlot::Elements);
|
||||
// Missing from const_values → Elements.
|
||||
assert_eq!(resolve_index_slot(SsaValue(99), &cv), FieldSlot::Elements);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn field_slot_ordering() {
|
||||
let slots = vec![
|
||||
FieldSlot::Named("b".to_string()),
|
||||
FieldSlot::Index(1),
|
||||
FieldSlot::Elements,
|
||||
FieldSlot::Named("a".to_string()),
|
||||
FieldSlot::Index(0),
|
||||
];
|
||||
let mut sorted = slots.clone();
|
||||
sorted.sort();
|
||||
assert_eq!(
|
||||
sorted,
|
||||
vec![
|
||||
FieldSlot::Elements,
|
||||
FieldSlot::Index(0),
|
||||
FieldSlot::Index(1),
|
||||
FieldSlot::Named("a".to_string()),
|
||||
FieldSlot::Named("b".to_string()),
|
||||
]
|
||||
);
|
||||
}
|
||||
}
|
||||
1589
src/symex/interproc.rs
Normal file
1589
src/symex/interproc.rs
Normal file
File diff suppressed because it is too large
Load diff
996
src/symex/loops.rs
Normal file
996
src/symex/loops.rs
Normal file
|
|
@ -0,0 +1,996 @@
|
|||
//! Loop analysis for the symbolic executor.
|
||||
//!
|
||||
//! Detects back edges, computes natural loop bodies, identifies induction
|
||||
//! variables, and determines loop exit successors. All analysis is computed
|
||||
//! once per `explore_finding()` invocation and shared across all paths.
|
||||
#![allow(clippy::collapsible_if)]
|
||||
|
||||
use std::collections::{HashMap, HashSet};
|
||||
|
||||
use petgraph::Graph;
|
||||
use petgraph::algo::dominators::{Dominators, simple_fast};
|
||||
use petgraph::graph::NodeIndex;
|
||||
|
||||
use crate::ssa::ir::{BlockId, SsaBody, SsaOp, SsaValue, Terminator};
|
||||
|
||||
/// Default loop unrolling bound. After this many visits to a loop head,
|
||||
/// the executor widens and skips to the exit.
|
||||
pub const MAX_LOOP_UNROLL: u8 = 2;
|
||||
|
||||
/// Pre-computed loop information for symex exploration.
|
||||
///
|
||||
/// Computed once per `explore_finding()` invocation, shared across all paths.
|
||||
pub struct LoopInfo {
|
||||
/// Back edges: (latch block, loop head block).
|
||||
pub back_edges: HashSet<(BlockId, BlockId)>,
|
||||
/// Blocks that are loop-head targets of back edges.
|
||||
pub loop_heads: HashSet<BlockId>,
|
||||
/// Natural loop body per loop head: head → set of blocks in the loop.
|
||||
pub loop_bodies: HashMap<BlockId, HashSet<BlockId>>,
|
||||
/// SSA values that are simple induction variables (loop counters).
|
||||
pub induction_vars: HashSet<SsaValue>,
|
||||
/// Dominator tree (retained for exit successor queries).
|
||||
#[allow(dead_code)]
|
||||
doms: Dominators<NodeIndex>,
|
||||
}
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Public API
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/// Analyse loop structure in an SSA body.
|
||||
///
|
||||
/// Builds a petgraph from the SSA blocks, computes dominators, detects back
|
||||
/// edges, natural loop bodies, and induction variables. All results are
|
||||
/// bundled into a [`LoopInfo`] for use by the executor.
|
||||
pub fn analyse_loops(ssa: &SsaBody) -> LoopInfo {
|
||||
let num_blocks = ssa.blocks.len();
|
||||
|
||||
// Build petgraph from SSA block successors
|
||||
let (block_graph, block_nodes, entry_node) = build_block_graph(ssa);
|
||||
|
||||
// Compute dominator tree
|
||||
let doms = simple_fast(&block_graph, entry_node);
|
||||
|
||||
// Detect back edges: (src, tgt) where tgt dominates src
|
||||
let back_edges = detect_back_edges(ssa, &block_nodes, &doms, num_blocks);
|
||||
|
||||
// Extract loop heads
|
||||
let loop_heads: HashSet<BlockId> = back_edges.iter().map(|(_, head)| *head).collect();
|
||||
|
||||
// Compute natural loop bodies
|
||||
let loop_bodies = compute_all_loop_bodies(ssa, &back_edges);
|
||||
|
||||
// Detect induction variables
|
||||
let induction_vars = detect_induction_vars(ssa, &back_edges, &loop_heads);
|
||||
|
||||
LoopInfo {
|
||||
back_edges,
|
||||
loop_heads,
|
||||
loop_bodies,
|
||||
induction_vars,
|
||||
doms,
|
||||
}
|
||||
}
|
||||
|
||||
impl LoopInfo {
|
||||
/// Determine the loop exit successor for a branch at a loop head.
|
||||
///
|
||||
/// Uses natural loop body membership: the exit successor is the one
|
||||
/// whose target is NOT in the loop body. Returns `None` if both
|
||||
/// successors are inside the loop (nested loop) or the block has no
|
||||
/// branch terminator.
|
||||
pub fn loop_exit_successor(&self, ssa: &SsaBody, head: BlockId) -> Option<BlockId> {
|
||||
let body = self.loop_bodies.get(&head)?;
|
||||
let block = ssa.blocks.get(head.0 as usize)?;
|
||||
match &block.terminator {
|
||||
Terminator::Branch {
|
||||
true_blk,
|
||||
false_blk,
|
||||
..
|
||||
} => {
|
||||
let true_in = body.contains(true_blk);
|
||||
let false_in = body.contains(false_blk);
|
||||
match (true_in, false_in) {
|
||||
(true, false) => Some(*false_blk),
|
||||
(false, true) => Some(*true_blk),
|
||||
(false, false) => Some(*true_blk), // both exit — deterministic pick
|
||||
(true, true) => None, // nested: no clear exit
|
||||
}
|
||||
}
|
||||
_ => None, // Goto or Return — no branching exit
|
||||
}
|
||||
}
|
||||
|
||||
/// Check if this LoopInfo has any loops at all (useful for fast skip).
|
||||
pub fn has_loops(&self) -> bool {
|
||||
!self.loop_heads.is_empty()
|
||||
}
|
||||
}
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Internal helpers
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
/// Build a petgraph from SSA block successors.
|
||||
///
|
||||
/// Mirrors the pattern in `src/ssa/lower.rs:build_block_graph`.
|
||||
fn build_block_graph(ssa: &SsaBody) -> (Graph<BlockId, ()>, Vec<NodeIndex>, NodeIndex) {
|
||||
let num_blocks = ssa.blocks.len();
|
||||
let mut g: Graph<BlockId, ()> = Graph::with_capacity(num_blocks, num_blocks * 2);
|
||||
let mut block_nodes: Vec<NodeIndex> = Vec::with_capacity(num_blocks);
|
||||
|
||||
for i in 0..num_blocks {
|
||||
block_nodes.push(g.add_node(BlockId(i as u32)));
|
||||
}
|
||||
|
||||
for block in &ssa.blocks {
|
||||
let src = block_nodes[block.id.0 as usize];
|
||||
for &succ in &block.succs {
|
||||
if (succ.0 as usize) < num_blocks {
|
||||
g.add_edge(src, block_nodes[succ.0 as usize], ());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
let entry_node = block_nodes[ssa.entry.0 as usize];
|
||||
(g, block_nodes, entry_node)
|
||||
}
|
||||
|
||||
/// Check if `dominator` dominates `target` in the dominator tree.
|
||||
///
|
||||
/// Mirrors the pattern in `src/cfg_analysis/dominators.rs:dominates`.
|
||||
fn dominates_block(doms: &Dominators<NodeIndex>, dominator: NodeIndex, target: NodeIndex) -> bool {
|
||||
if dominator == target {
|
||||
return true;
|
||||
}
|
||||
let mut current = target;
|
||||
while let Some(idom) = doms.immediate_dominator(current) {
|
||||
if idom == current {
|
||||
break; // reached root
|
||||
}
|
||||
if idom == dominator {
|
||||
return true;
|
||||
}
|
||||
current = idom;
|
||||
}
|
||||
false
|
||||
}
|
||||
|
||||
/// Detect back edges using dominator analysis.
|
||||
///
|
||||
/// An edge (src, tgt) is a back edge if tgt dominates src in the
|
||||
/// dominator tree. This is sound for all CFG shapes, unlike the
|
||||
/// block-index heuristic used by the taint engine.
|
||||
fn detect_back_edges(
|
||||
ssa: &SsaBody,
|
||||
block_nodes: &[NodeIndex],
|
||||
doms: &Dominators<NodeIndex>,
|
||||
num_blocks: usize,
|
||||
) -> HashSet<(BlockId, BlockId)> {
|
||||
let mut back_edges = HashSet::new();
|
||||
for block in &ssa.blocks {
|
||||
let src_idx = block.id.0 as usize;
|
||||
if src_idx >= num_blocks {
|
||||
continue;
|
||||
}
|
||||
let src_node = block_nodes[src_idx];
|
||||
for &succ in &block.succs {
|
||||
let tgt_idx = succ.0 as usize;
|
||||
if tgt_idx >= num_blocks {
|
||||
continue;
|
||||
}
|
||||
let tgt_node = block_nodes[tgt_idx];
|
||||
if dominates_block(doms, tgt_node, src_node) {
|
||||
back_edges.insert((block.id, succ));
|
||||
}
|
||||
}
|
||||
}
|
||||
back_edges
|
||||
}
|
||||
|
||||
/// Compute the natural loop body for a single back edge (latch → head).
|
||||
///
|
||||
/// The natural loop is {head} ∪ {blocks that can reach latch without
|
||||
/// going through head}. Uses reverse BFS from the latch, stopping at head.
|
||||
fn compute_natural_loop_body(ssa: &SsaBody, head: BlockId, latch: BlockId) -> HashSet<BlockId> {
|
||||
let mut body = HashSet::new();
|
||||
body.insert(head);
|
||||
if head == latch {
|
||||
return body; // single-block loop
|
||||
}
|
||||
body.insert(latch);
|
||||
let mut worklist = vec![latch];
|
||||
while let Some(bid) = worklist.pop() {
|
||||
if let Some(block) = ssa.blocks.get(bid.0 as usize) {
|
||||
for &pred in &block.preds {
|
||||
if pred != head && body.insert(pred) {
|
||||
worklist.push(pred);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
body
|
||||
}
|
||||
|
||||
/// Compute natural loop bodies for all loop heads.
|
||||
///
|
||||
/// When multiple back edges target the same head, their bodies are unioned.
|
||||
fn compute_all_loop_bodies(
|
||||
ssa: &SsaBody,
|
||||
back_edges: &HashSet<(BlockId, BlockId)>,
|
||||
) -> HashMap<BlockId, HashSet<BlockId>> {
|
||||
let mut bodies: HashMap<BlockId, HashSet<BlockId>> = HashMap::new();
|
||||
for &(latch, head) in back_edges {
|
||||
let body = compute_natural_loop_body(ssa, head, latch);
|
||||
bodies
|
||||
.entry(head)
|
||||
.and_modify(|existing| {
|
||||
existing.extend(body.iter());
|
||||
})
|
||||
.or_insert(body);
|
||||
}
|
||||
bodies
|
||||
}
|
||||
|
||||
/// Detect induction variables: phi nodes at loop heads where the back-edge
|
||||
/// operand is a simple increment/decrement of the phi result.
|
||||
///
|
||||
/// Mirrors `detect_induction_phis()` in `src/taint/ssa_transfer.rs`.
|
||||
fn detect_induction_vars(
|
||||
ssa: &SsaBody,
|
||||
back_edges: &HashSet<(BlockId, BlockId)>,
|
||||
loop_heads: &HashSet<BlockId>,
|
||||
) -> HashSet<SsaValue> {
|
||||
let mut induction_vars = HashSet::new();
|
||||
|
||||
for block in &ssa.blocks {
|
||||
if !loop_heads.contains(&block.id) {
|
||||
continue;
|
||||
}
|
||||
for phi in &block.phis {
|
||||
if let SsaOp::Phi(ref operands) = phi.op {
|
||||
if operands.len() != 2 {
|
||||
continue;
|
||||
}
|
||||
|
||||
// Identify which operand comes via back edge
|
||||
let mut back_edge_op = None;
|
||||
let mut init_op = None;
|
||||
for &(pred_blk, operand_val) in operands {
|
||||
if back_edges.contains(&(pred_blk, block.id)) {
|
||||
back_edge_op = Some(operand_val);
|
||||
} else {
|
||||
init_op = Some(operand_val);
|
||||
}
|
||||
}
|
||||
|
||||
if let (Some(back_val), Some(_init_val)) = (back_edge_op, init_op) {
|
||||
if is_simple_increment(ssa, back_val, phi.value) {
|
||||
induction_vars.insert(phi.value);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
induction_vars
|
||||
}
|
||||
|
||||
/// Check if `inc_val` is defined as a simple increment of `phi_val`:
|
||||
/// `inc_val = phi_val + const` or `inc_val = phi_val - const`.
|
||||
///
|
||||
/// Mirrors `is_simple_increment()` in `src/taint/ssa_transfer.rs`.
|
||||
fn is_simple_increment(ssa: &SsaBody, inc_val: SsaValue, phi_val: SsaValue) -> bool {
|
||||
let def = ssa.def_of(inc_val);
|
||||
let block = ssa.block(def.block);
|
||||
for inst in &block.body {
|
||||
if inst.value == inc_val {
|
||||
if let SsaOp::Assign(ref uses) = inst.op {
|
||||
if uses.len() == 2 && uses.contains(&phi_val) {
|
||||
let other = if uses[0] == phi_val { uses[1] } else { uses[0] };
|
||||
let other_def = ssa.def_of(other);
|
||||
let other_block = ssa.block(other_def.block);
|
||||
for other_inst in other_block.phis.iter().chain(other_block.body.iter()) {
|
||||
if other_inst.value == other && matches!(other_inst.op, SsaOp::Const(_)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
false
|
||||
}
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Tests
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use crate::ssa::ir::{SsaBlock, SsaInst, ValueDef};
|
||||
use petgraph::graph::NodeIndex as CfgNodeIndex;
|
||||
use smallvec::smallvec;
|
||||
|
||||
fn dummy_cfg_node() -> CfgNodeIndex {
|
||||
CfgNodeIndex::new(0)
|
||||
}
|
||||
|
||||
fn make_value_def(block: BlockId) -> ValueDef {
|
||||
ValueDef {
|
||||
var_name: None,
|
||||
cfg_node: dummy_cfg_node(),
|
||||
block,
|
||||
}
|
||||
}
|
||||
|
||||
fn make_inst(val: u32, op: SsaOp, _block: BlockId) -> SsaInst {
|
||||
SsaInst {
|
||||
value: SsaValue(val),
|
||||
op,
|
||||
cfg_node: dummy_cfg_node(),
|
||||
var_name: None,
|
||||
span: (0, 0),
|
||||
}
|
||||
}
|
||||
|
||||
// ─── Back-edge detection ─────────────────────────────────────────────
|
||||
|
||||
#[test]
|
||||
fn simple_loop_back_edge() {
|
||||
// B0 → B1 → B2 → B1 (back edge B2→B1)
|
||||
// → B3 (exit)
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(3),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(2)],
|
||||
succs: smallvec![BlockId(2), BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert_eq!(info.back_edges.len(), 1);
|
||||
assert!(info.back_edges.contains(&(BlockId(2), BlockId(1))));
|
||||
assert_eq!(info.loop_heads.len(), 1);
|
||||
assert!(info.loop_heads.contains(&BlockId(1)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn no_loop_linear() {
|
||||
// B0 → B1 → B2
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(2)),
|
||||
preds: smallvec![BlockId(0)],
|
||||
succs: smallvec![BlockId(2)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert!(info.back_edges.is_empty());
|
||||
assert!(info.loop_heads.is_empty());
|
||||
assert!(info.loop_bodies.is_empty());
|
||||
assert!(!info.has_loops());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn nested_loops() {
|
||||
// B0 → B1 (outer head) → B2 (inner head) → B3 → B2 (inner back)
|
||||
// → B4 → B1 (outer back)
|
||||
// B1 → B5 (outer exit)
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(5),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(4)],
|
||||
succs: smallvec![BlockId(2), BlockId(5)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(3),
|
||||
false_blk: BlockId(4),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(1), BlockId(3)],
|
||||
succs: smallvec![BlockId(3), BlockId(4)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(2)),
|
||||
preds: smallvec![BlockId(2)],
|
||||
succs: smallvec![BlockId(2)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(4),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(2)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(5),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert_eq!(info.back_edges.len(), 2);
|
||||
assert!(info.back_edges.contains(&(BlockId(3), BlockId(2)))); // inner
|
||||
assert!(info.back_edges.contains(&(BlockId(4), BlockId(1)))); // outer
|
||||
assert_eq!(info.loop_heads.len(), 2);
|
||||
assert!(info.loop_heads.contains(&BlockId(1)));
|
||||
assert!(info.loop_heads.contains(&BlockId(2)));
|
||||
}
|
||||
|
||||
// ─── Natural loop body ───────────────────────────────────────────────
|
||||
|
||||
#[test]
|
||||
fn natural_body_simple_loop() {
|
||||
// B0 → B1 → B2 → B1, B1 → B3
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(3),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(2)],
|
||||
succs: smallvec![BlockId(2), BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
let body = info.loop_bodies.get(&BlockId(1)).unwrap();
|
||||
assert!(body.contains(&BlockId(1))); // head
|
||||
assert!(body.contains(&BlockId(2))); // body
|
||||
assert!(!body.contains(&BlockId(0))); // pre-loop
|
||||
assert!(!body.contains(&BlockId(3))); // post-loop
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn natural_body_nested_excludes_outer() {
|
||||
// Reuse the nested_loops SSA
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(5),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(4)],
|
||||
succs: smallvec![BlockId(2), BlockId(5)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(3),
|
||||
false_blk: BlockId(4),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(1), BlockId(3)],
|
||||
succs: smallvec![BlockId(3), BlockId(4)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(2)),
|
||||
preds: smallvec![BlockId(2)],
|
||||
succs: smallvec![BlockId(2)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(4),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(2)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(5),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
|
||||
// Inner loop body: {B2, B3}
|
||||
let inner = info.loop_bodies.get(&BlockId(2)).unwrap();
|
||||
assert!(inner.contains(&BlockId(2)));
|
||||
assert!(inner.contains(&BlockId(3)));
|
||||
assert!(!inner.contains(&BlockId(1))); // outer head not in inner
|
||||
assert!(!inner.contains(&BlockId(4))); // exit of inner not in inner
|
||||
|
||||
// Outer loop body: {B1, B2, B3, B4}
|
||||
let outer = info.loop_bodies.get(&BlockId(1)).unwrap();
|
||||
assert!(outer.contains(&BlockId(1)));
|
||||
assert!(outer.contains(&BlockId(2)));
|
||||
assert!(outer.contains(&BlockId(3)));
|
||||
assert!(outer.contains(&BlockId(4)));
|
||||
assert!(!outer.contains(&BlockId(5))); // post-loop not in outer
|
||||
}
|
||||
|
||||
// ─── Exit successor ──────────────────────────────────────────────────
|
||||
|
||||
#[test]
|
||||
fn exit_successor_simple() {
|
||||
// B1 (loop head): true→B2 (body), false→B3 (exit)
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(3),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(2)],
|
||||
succs: smallvec![BlockId(2), BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert_eq!(info.loop_exit_successor(&ssa, BlockId(1)), Some(BlockId(3)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn exit_successor_goto_returns_none() {
|
||||
// Single-block loop: B0 → B1 → B1 (Goto back to self)
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(0), BlockId(1)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert_eq!(info.loop_exit_successor(&ssa, BlockId(1)), None);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn exit_successor_both_in_body_returns_none() {
|
||||
// Nested: outer head B1 branches to B2 (inner head, in outer body) and B3 (also in outer body)
|
||||
// B3 → B1 (outer back edge)
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(3),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(3)],
|
||||
succs: smallvec![BlockId(2), BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(3)),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(1), BlockId(2)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
// Both B2 and B3 are in the loop body for head B1
|
||||
assert_eq!(info.loop_exit_successor(&ssa, BlockId(1)), None);
|
||||
}
|
||||
|
||||
// ─── Induction variables ─────────────────────────────────────────────
|
||||
|
||||
#[test]
|
||||
fn induction_var_simple_counter() {
|
||||
// B0: v0 = Const("0"), v2 = Const("1")
|
||||
// B1: v1 = Phi((B0, v0), (B2, v3)) ← induction var
|
||||
// B2: v3 = Assign([v1, v2]) ← v1 + const
|
||||
// B2 → B1 (back edge)
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![
|
||||
make_inst(0, SsaOp::Const(Some("0".into())), BlockId(0)),
|
||||
make_inst(2, SsaOp::Const(Some("1".into())), BlockId(0)),
|
||||
],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![make_inst(
|
||||
1,
|
||||
SsaOp::Phi(smallvec![
|
||||
(BlockId(0), SsaValue(0)),
|
||||
(BlockId(2), SsaValue(3))
|
||||
]),
|
||||
BlockId(1),
|
||||
)],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(3),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(2)],
|
||||
succs: smallvec![BlockId(2), BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![make_inst(
|
||||
3,
|
||||
SsaOp::Assign(smallvec![SsaValue(1), SsaValue(2)]),
|
||||
BlockId(2),
|
||||
)],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![
|
||||
make_value_def(BlockId(0)), // v0
|
||||
make_value_def(BlockId(1)), // v1
|
||||
make_value_def(BlockId(0)), // v2
|
||||
make_value_def(BlockId(2)), // v3
|
||||
],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert!(info.induction_vars.contains(&SsaValue(1)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn non_induction_phi_not_detected() {
|
||||
// B0: v0 = Source
|
||||
// B1: v1 = Phi((B0, v0), (B2, v2))
|
||||
// B2: v2 = Call("f", [v1]) ← NOT a simple increment
|
||||
// B2 → B1
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![make_inst(0, SsaOp::Source, BlockId(0))],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![make_inst(
|
||||
1,
|
||||
SsaOp::Phi(smallvec![
|
||||
(BlockId(0), SsaValue(0)),
|
||||
(BlockId(2), SsaValue(2))
|
||||
]),
|
||||
BlockId(1),
|
||||
)],
|
||||
body: vec![],
|
||||
terminator: Terminator::Branch {
|
||||
cond: dummy_cfg_node(),
|
||||
true_blk: BlockId(2),
|
||||
false_blk: BlockId(3),
|
||||
condition: None,
|
||||
},
|
||||
preds: smallvec![BlockId(0), BlockId(2)],
|
||||
succs: smallvec![BlockId(2), BlockId(3)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(2),
|
||||
phis: vec![],
|
||||
body: vec![make_inst(
|
||||
2,
|
||||
SsaOp::Call {
|
||||
callee: "f".into(),
|
||||
args: vec![smallvec![SsaValue(1)]],
|
||||
receiver: None,
|
||||
},
|
||||
BlockId(2),
|
||||
)],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(3),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![BlockId(1)],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![
|
||||
make_value_def(BlockId(0)), // v0
|
||||
make_value_def(BlockId(1)), // v1
|
||||
make_value_def(BlockId(2)), // v2
|
||||
],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert!(info.induction_vars.is_empty());
|
||||
}
|
||||
|
||||
// ─── has_loops ───────────────────────────────────────────────────────
|
||||
|
||||
#[test]
|
||||
fn has_loops_with_loop() {
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(1)),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![BlockId(1)],
|
||||
},
|
||||
SsaBlock {
|
||||
id: BlockId(1),
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(BlockId(0)),
|
||||
preds: smallvec![BlockId(0)],
|
||||
succs: smallvec![BlockId(0)],
|
||||
},
|
||||
],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let info = analyse_loops(&ssa);
|
||||
assert!(info.has_loops());
|
||||
}
|
||||
}
|
||||
624
src/symex/mod.rs
Normal file
624
src/symex/mod.rs
Normal file
|
|
@ -0,0 +1,624 @@
|
|||
//! Symbolic execution targeting: candidate selection and constraint analysis
|
||||
//! for taint findings.
|
||||
//!
|
||||
//! After SSA taint analysis produces findings, this module selects candidates
|
||||
//! (non-trivial paths, non-validated) and runs constraint analysis on each
|
||||
//! path to determine feasibility. Results are stored as `SymbolicVerdict` on
|
||||
//! the finding, which flows through to Evidence and confidence scoring.
|
||||
//!
|
||||
//! Symbolic expression trees (`SymbolicValue`) preserve computation structure
|
||||
//! through the path walk, enabling richer witness strings.
|
||||
|
||||
#![allow(
|
||||
clippy::collapsible_if,
|
||||
clippy::manual_ignore_case_cmp,
|
||||
clippy::needless_borrow
|
||||
)]
|
||||
|
||||
pub mod executor;
|
||||
pub mod heap;
|
||||
pub mod interproc;
|
||||
pub mod loops;
|
||||
#[cfg(feature = "smt")]
|
||||
pub mod smt;
|
||||
pub mod state;
|
||||
pub mod strings;
|
||||
pub mod transfer;
|
||||
pub mod value;
|
||||
pub mod witness;
|
||||
|
||||
pub use state::{PathConstraint, SymbolicState};
|
||||
pub use value::{MAX_EXPR_DEPTH, Op, SymbolicValue};
|
||||
|
||||
use std::collections::{HashMap, HashSet};
|
||||
|
||||
use crate::cfg::Cfg;
|
||||
use crate::evidence::{SymbolicVerdict, Verdict};
|
||||
use crate::ssa::const_prop::ConstLattice;
|
||||
use crate::ssa::heap::PointsToResult;
|
||||
use crate::ssa::ir::{BlockId, SsaBody, SsaValue};
|
||||
use crate::ssa::type_facts::TypeFactResult;
|
||||
use crate::summary::GlobalSummaries;
|
||||
use crate::symbol::Lang;
|
||||
use crate::taint::Finding;
|
||||
|
||||
/// Context for symbolic execution analysis.
|
||||
///
|
||||
/// Bundles all parameters needed by the symex pipeline: SSA body, CFG,
|
||||
/// optimization results, and optional cross-file summary context for
|
||||
/// interprocedural symbolic modeling.
|
||||
pub struct SymexContext<'a> {
|
||||
pub ssa: &'a SsaBody,
|
||||
pub cfg: &'a Cfg,
|
||||
pub const_values: &'a HashMap<SsaValue, ConstLattice>,
|
||||
pub type_facts: &'a TypeFactResult,
|
||||
/// Cross-file summaries for interprocedural symbolic modeling.
|
||||
/// When `Some`, callee calls can be modeled via `SsaFuncSummary`
|
||||
/// instead of being treated as opaque `Unknown`.
|
||||
pub global_summaries: Option<&'a GlobalSummaries>,
|
||||
pub lang: Lang,
|
||||
pub namespace: &'a str,
|
||||
/// Points-to analysis results for object identity resolution in the
|
||||
/// field-sensitive symbolic heap.
|
||||
pub points_to: Option<&'a PointsToResult>,
|
||||
/// Pre-lowered intra-file function bodies for interprocedural symbolic
|
||||
/// execution. Keyed by canonical `FuncKey`.
|
||||
pub callee_bodies: Option<
|
||||
&'a std::collections::HashMap<
|
||||
crate::symbol::FuncKey,
|
||||
crate::taint::ssa_transfer::CalleeSsaBody,
|
||||
>,
|
||||
>,
|
||||
/// SCC membership: maps normalized function name → SCC index.
|
||||
/// Used by interprocedural symex for mutual recursion detection.
|
||||
pub scc_membership: Option<&'a HashMap<String, usize>>,
|
||||
/// Cross-file callee bodies for interprocedural symbolic execution.
|
||||
/// Provides body resolution via `GlobalSummaries.resolve_callee_body()`.
|
||||
pub cross_file_bodies: Option<&'a GlobalSummaries>,
|
||||
}
|
||||
|
||||
/// Maximum candidates to analyse per file (budget bound).
|
||||
const MAX_CANDIDATES: usize = 50;
|
||||
|
||||
/// Maximum blocks on a path before we skip symex (too expensive).
|
||||
const MAX_PATH_BLOCKS: usize = 100;
|
||||
|
||||
/// Runtime feature gate for SMT solving. Default ON when compiled with the
|
||||
/// `smt` feature; controlled at runtime by
|
||||
/// `analysis.engine.symex.smt` in `nyx.conf` (or `--smt / --no-smt`).
|
||||
#[cfg(feature = "smt")]
|
||||
pub fn smt_enabled() -> bool {
|
||||
crate::utils::analysis_options::current().symex.smt
|
||||
}
|
||||
|
||||
/// SMT solving is not available without the `smt` compile-time feature.
|
||||
#[cfg(not(feature = "smt"))]
|
||||
pub fn smt_enabled() -> bool {
|
||||
false
|
||||
}
|
||||
|
||||
/// Feature gate: check if cross-file symbolic body execution is enabled.
|
||||
///
|
||||
/// Controlled by `analysis.engine.symex.cross_file` in `nyx.conf` (default
|
||||
/// `true`) or the `--cross-file-symex / --no-cross-file-symex` CLI flag.
|
||||
/// When disabled: body extraction, persistence, loading, and resolution are
|
||||
/// all skipped.
|
||||
pub fn cross_file_symex_enabled() -> bool {
|
||||
crate::utils::analysis_options::current().symex.cross_file
|
||||
}
|
||||
|
||||
/// Feature gate: check if symbolic execution targeting is enabled.
|
||||
///
|
||||
/// Controlled by `analysis.engine.symex.enabled` in `nyx.conf` (default
|
||||
/// `true`) or the `--symex / --no-symex` CLI flag.
|
||||
pub fn is_enabled() -> bool {
|
||||
crate::utils::analysis_options::current().symex.enabled
|
||||
}
|
||||
|
||||
/// Run symex analysis on eligible findings, mutating them in place.
|
||||
///
|
||||
/// Pre-filters: skips path_validated findings and those with fewer than 2
|
||||
/// flow steps. Respects the per-file candidate budget.
|
||||
pub fn annotate_findings(findings: &mut [Finding], ctx: &SymexContext) {
|
||||
let mut budget = MAX_CANDIDATES;
|
||||
for finding in findings.iter_mut() {
|
||||
if budget == 0 {
|
||||
break;
|
||||
}
|
||||
if finding.flow_steps.len() < 2 || finding.path_validated {
|
||||
continue;
|
||||
}
|
||||
finding.symbolic = Some(analyse_finding_path(finding, ctx));
|
||||
budget -= 1;
|
||||
}
|
||||
}
|
||||
|
||||
/// Extract the ordered sequence of SSA blocks along a finding's flow path.
|
||||
///
|
||||
/// Maps `flow_steps` CFG nodes through `ssa.cfg_node_map` to SSA blocks,
|
||||
/// deduplicating consecutive blocks.
|
||||
pub(super) fn extract_path_blocks(finding: &Finding, ssa: &SsaBody) -> Vec<BlockId> {
|
||||
let mut blocks = Vec::new();
|
||||
let mut seen = HashSet::new();
|
||||
for step in &finding.flow_steps {
|
||||
if let Some(&val) = ssa.cfg_node_map.get(&step.cfg_node) {
|
||||
if val.0 < ssa.value_defs.len() as u32 {
|
||||
let block = ssa.value_defs[val.0 as usize].block;
|
||||
if seen.insert(block) {
|
||||
blocks.push(block);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
blocks
|
||||
}
|
||||
|
||||
/// Run constraint and symbolic analysis on a single finding's taint path.
|
||||
///
|
||||
/// Delegates to the multi-path exploration engine which walks the CFG from
|
||||
/// source to sink, forking at branch points where both successors lie on
|
||||
/// some source-to-sink path. Produces an aggregate verdict across all
|
||||
/// explored paths.
|
||||
fn analyse_finding_path(finding: &Finding, ctx: &SymexContext) -> SymbolicVerdict {
|
||||
let path_blocks = extract_path_blocks(finding, ctx.ssa);
|
||||
|
||||
if path_blocks.is_empty() {
|
||||
return SymbolicVerdict {
|
||||
verdict: Verdict::Inconclusive,
|
||||
constraints_checked: 0,
|
||||
paths_explored: 0,
|
||||
witness: None,
|
||||
interproc_call_chains: Vec::new(),
|
||||
cutoff_notes: Vec::new(),
|
||||
};
|
||||
}
|
||||
|
||||
if path_blocks.len() < 2 {
|
||||
// Short path (single block, no branches) — skip the multi-path
|
||||
// explorer but still run a linear transfer to extract a witness.
|
||||
let witness = linear_witness(finding, ctx, &path_blocks);
|
||||
return SymbolicVerdict {
|
||||
verdict: Verdict::Inconclusive,
|
||||
constraints_checked: 0,
|
||||
paths_explored: 1,
|
||||
witness,
|
||||
interproc_call_chains: Vec::new(),
|
||||
cutoff_notes: Vec::new(),
|
||||
};
|
||||
}
|
||||
|
||||
if path_blocks.len() > MAX_PATH_BLOCKS {
|
||||
return SymbolicVerdict {
|
||||
verdict: Verdict::Inconclusive,
|
||||
constraints_checked: 0,
|
||||
paths_explored: 0,
|
||||
witness: Some("path too long for symex budget".into()),
|
||||
interproc_call_chains: Vec::new(),
|
||||
cutoff_notes: Vec::new(),
|
||||
};
|
||||
}
|
||||
|
||||
let result = executor::explore_finding(finding, ctx);
|
||||
result.aggregate_verdict()
|
||||
}
|
||||
|
||||
/// Run a minimal linear symbolic transfer on `path_blocks` and extract
|
||||
/// a witness. Used for short paths (single block, no branches) that
|
||||
/// don't need the full multi-path exploration engine.
|
||||
fn linear_witness(
|
||||
finding: &Finding,
|
||||
ctx: &SymexContext,
|
||||
path_blocks: &[BlockId],
|
||||
) -> Option<String> {
|
||||
let mut sym_state = SymbolicState::new();
|
||||
|
||||
// Seed constants from const_prop
|
||||
sym_state.seed_from_const_values(&ctx.const_values);
|
||||
|
||||
// Seed source flow steps as tainted symbols before transfer.
|
||||
for step in &finding.flow_steps {
|
||||
if let Some(&val) = ctx.ssa.cfg_node_map.get(&step.cfg_node) {
|
||||
if matches!(step.op_kind, crate::evidence::FlowStepKind::Source) {
|
||||
sym_state.set(val, value::SymbolicValue::Symbol(val));
|
||||
sym_state.mark_tainted(val);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Build context structs for transfer
|
||||
let summary_ctx = ctx.global_summaries.map(|gs| transfer::SymexSummaryCtx {
|
||||
global_summaries: gs,
|
||||
lang: ctx.lang,
|
||||
namespace: ctx.namespace,
|
||||
type_facts: Some(ctx.type_facts),
|
||||
});
|
||||
let heap_ctx = ctx.points_to.map(|pts| transfer::SymexHeapCtx {
|
||||
points_to: pts,
|
||||
ssa: ctx.ssa,
|
||||
lang: ctx.lang,
|
||||
const_values: ctx.const_values,
|
||||
});
|
||||
|
||||
// Transfer each block in order
|
||||
for &bid in path_blocks {
|
||||
if let Some(block) = ctx.ssa.blocks.get(bid.0 as usize) {
|
||||
transfer::transfer_block(
|
||||
&mut sym_state,
|
||||
block,
|
||||
ctx.cfg,
|
||||
ctx.ssa,
|
||||
summary_ctx.as_ref(),
|
||||
heap_ctx.as_ref(),
|
||||
None, // no interproc for short paths
|
||||
Some(ctx.lang),
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
// After transfer, mark all Symbol values that appear in the sink
|
||||
// expression as tainted. The transfer builds the expression tree from
|
||||
// base SSA values (parameters, etc.); we mark them tainted so that
|
||||
// witness extraction can identify tainted sub-expressions.
|
||||
if let Some(&sink_val) = ctx.ssa.cfg_node_map.get(&finding.sink) {
|
||||
let sink_sym = sym_state.get(sink_val);
|
||||
mark_symbols_tainted(&sink_sym, &mut sym_state);
|
||||
}
|
||||
|
||||
// Extract witness
|
||||
witness::extract_witness(&sym_state, finding, ctx.ssa, ctx.cfg)
|
||||
.or_else(|| sym_state.get_sink_witness(finding, ctx.ssa))
|
||||
}
|
||||
|
||||
/// Recursively mark all `Symbol(v)` values in an expression tree as tainted.
|
||||
fn mark_symbols_tainted(expr: &value::SymbolicValue, state: &mut SymbolicState) {
|
||||
match expr {
|
||||
value::SymbolicValue::Symbol(v) => {
|
||||
state.mark_tainted(*v);
|
||||
}
|
||||
value::SymbolicValue::BinOp(_, l, r) | value::SymbolicValue::Concat(l, r) => {
|
||||
mark_symbols_tainted(l, state);
|
||||
mark_symbols_tainted(r, state);
|
||||
}
|
||||
value::SymbolicValue::Call(_, args) => {
|
||||
for a in args {
|
||||
mark_symbols_tainted(a, state);
|
||||
}
|
||||
}
|
||||
value::SymbolicValue::Phi(ops) => {
|
||||
for (_, v) in ops {
|
||||
mark_symbols_tainted(v, state);
|
||||
}
|
||||
}
|
||||
value::SymbolicValue::ToLower(s)
|
||||
| value::SymbolicValue::ToUpper(s)
|
||||
| value::SymbolicValue::Trim(s)
|
||||
| value::SymbolicValue::StrLen(s)
|
||||
| value::SymbolicValue::Replace(s, _, _)
|
||||
| value::SymbolicValue::Encode(_, s)
|
||||
| value::SymbolicValue::Decode(_, s) => {
|
||||
mark_symbols_tainted(s, state);
|
||||
}
|
||||
value::SymbolicValue::Substr(s, start, end) => {
|
||||
mark_symbols_tainted(s, state);
|
||||
mark_symbols_tainted(start, state);
|
||||
if let Some(e) = end {
|
||||
mark_symbols_tainted(e, state);
|
||||
}
|
||||
}
|
||||
value::SymbolicValue::Concrete(_)
|
||||
| value::SymbolicValue::ConcreteStr(_)
|
||||
| value::SymbolicValue::Unknown => {}
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use crate::ssa::ir::{BlockId, SsaBlock, SsaBody, SsaValue, Terminator, ValueDef};
|
||||
use crate::ssa::type_facts::TypeFactResult;
|
||||
use petgraph::graph::NodeIndex;
|
||||
use smallvec::smallvec;
|
||||
|
||||
fn empty_type_facts() -> TypeFactResult {
|
||||
TypeFactResult {
|
||||
facts: HashMap::new(),
|
||||
}
|
||||
}
|
||||
|
||||
fn make_value_def(block: BlockId, cfg_node: NodeIndex) -> ValueDef {
|
||||
ValueDef {
|
||||
var_name: None,
|
||||
cfg_node,
|
||||
block,
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn is_enabled_tracks_runtime_default() {
|
||||
// The process-wide runtime is a `OnceLock`; without any prior install,
|
||||
// [`is_enabled`] reflects `AnalysisOptions::default().symex.enabled`.
|
||||
// Flipping the toggle is covered by `analysis_options` unit tests that
|
||||
// don't cross process boundaries.
|
||||
assert_eq!(
|
||||
is_enabled(),
|
||||
crate::utils::AnalysisOptions::default().symex.enabled
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn extract_path_blocks_basic() {
|
||||
use crate::taint::FlowStepRaw;
|
||||
|
||||
let n0 = NodeIndex::new(0);
|
||||
let n1 = NodeIndex::new(1);
|
||||
let b0 = BlockId(0);
|
||||
let b1 = BlockId(1);
|
||||
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: b0,
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(b1),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![b1],
|
||||
},
|
||||
SsaBlock {
|
||||
id: b1,
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![b0],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: b0,
|
||||
value_defs: vec![make_value_def(b0, n0), make_value_def(b1, n1)],
|
||||
cfg_node_map: [(n0, SsaValue(0)), (n1, SsaValue(1))].into_iter().collect(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: n1,
|
||||
source: n0,
|
||||
path: vec![n0, n1],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: false,
|
||||
guard_kind: None,
|
||||
hop_count: 1,
|
||||
cap_specificity: 1,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![
|
||||
FlowStepRaw {
|
||||
cfg_node: n0,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Source,
|
||||
},
|
||||
FlowStepRaw {
|
||||
cfg_node: n1,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Sink,
|
||||
},
|
||||
],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
|
||||
let blocks = extract_path_blocks(&finding, &ssa);
|
||||
assert_eq!(blocks, vec![b0, b1]);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn analyse_no_branches_confirmed() {
|
||||
use crate::taint::FlowStepRaw;
|
||||
|
||||
let n0 = NodeIndex::new(0);
|
||||
let n1 = NodeIndex::new(1);
|
||||
let b0 = BlockId(0);
|
||||
let b1 = BlockId(1);
|
||||
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![
|
||||
SsaBlock {
|
||||
id: b0,
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Goto(b1),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![b1],
|
||||
},
|
||||
SsaBlock {
|
||||
id: b1,
|
||||
phis: vec![],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![b0],
|
||||
succs: smallvec![],
|
||||
},
|
||||
],
|
||||
entry: b0,
|
||||
value_defs: vec![make_value_def(b0, n0), make_value_def(b1, n1)],
|
||||
cfg_node_map: [(n0, SsaValue(0)), (n1, SsaValue(1))].into_iter().collect(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: n1,
|
||||
source: n0,
|
||||
path: vec![n0, n1],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: false,
|
||||
guard_kind: None,
|
||||
hop_count: 1,
|
||||
cap_specificity: 1,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![
|
||||
FlowStepRaw {
|
||||
cfg_node: n0,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Source,
|
||||
},
|
||||
FlowStepRaw {
|
||||
cfg_node: n1,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Sink,
|
||||
},
|
||||
],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
|
||||
let ctx = SymexContext {
|
||||
ssa: &ssa,
|
||||
cfg: &Cfg::new(),
|
||||
const_values: &HashMap::new(),
|
||||
type_facts: &empty_type_facts(),
|
||||
global_summaries: None,
|
||||
lang: crate::symbol::Lang::JavaScript,
|
||||
namespace: "test.js",
|
||||
points_to: None,
|
||||
callee_bodies: None,
|
||||
scc_membership: None,
|
||||
cross_file_bodies: None,
|
||||
};
|
||||
let verdict = analyse_finding_path(&finding, &ctx);
|
||||
assert_eq!(verdict.verdict, Verdict::Confirmed);
|
||||
assert_eq!(verdict.constraints_checked, 0);
|
||||
assert_eq!(verdict.paths_explored, 1);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn annotate_skips_validated() {
|
||||
use crate::taint::FlowStepRaw;
|
||||
|
||||
let n0 = NodeIndex::new(0);
|
||||
let n1 = NodeIndex::new(1);
|
||||
|
||||
let mut finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: n1,
|
||||
source: n0,
|
||||
path: vec![n0, n1],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: true, // should be skipped
|
||||
guard_kind: None,
|
||||
hop_count: 1,
|
||||
cap_specificity: 1,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![
|
||||
FlowStepRaw {
|
||||
cfg_node: n0,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Source,
|
||||
},
|
||||
FlowStepRaw {
|
||||
cfg_node: n1,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Sink,
|
||||
},
|
||||
],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let ctx = SymexContext {
|
||||
ssa: &ssa,
|
||||
cfg: &Cfg::new(),
|
||||
const_values: &HashMap::new(),
|
||||
type_facts: &empty_type_facts(),
|
||||
global_summaries: None,
|
||||
lang: crate::symbol::Lang::JavaScript,
|
||||
namespace: "test.js",
|
||||
points_to: None,
|
||||
callee_bodies: None,
|
||||
scc_membership: None,
|
||||
cross_file_bodies: None,
|
||||
};
|
||||
annotate_findings(std::slice::from_mut(&mut finding), &ctx);
|
||||
// Should remain None — skipped due to path_validated
|
||||
assert!(finding.symbolic.is_none());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn annotate_skips_short_path() {
|
||||
use crate::taint::FlowStepRaw;
|
||||
|
||||
let n0 = NodeIndex::new(0);
|
||||
|
||||
let mut finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: n0,
|
||||
source: n0,
|
||||
path: vec![n0],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: false,
|
||||
guard_kind: None,
|
||||
hop_count: 0,
|
||||
cap_specificity: 1,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![FlowStepRaw {
|
||||
cfg_node: n0,
|
||||
var_name: Some("x".into()),
|
||||
op_kind: crate::evidence::FlowStepKind::Source,
|
||||
}],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let ctx = SymexContext {
|
||||
ssa: &ssa,
|
||||
cfg: &Cfg::new(),
|
||||
const_values: &HashMap::new(),
|
||||
type_facts: &empty_type_facts(),
|
||||
global_summaries: None,
|
||||
lang: crate::symbol::Lang::JavaScript,
|
||||
namespace: "test.js",
|
||||
points_to: None,
|
||||
callee_bodies: None,
|
||||
scc_membership: None,
|
||||
cross_file_bodies: None,
|
||||
};
|
||||
annotate_findings(std::slice::from_mut(&mut finding), &ctx);
|
||||
// Should remain None — only 1 flow step
|
||||
assert!(finding.symbolic.is_none());
|
||||
}
|
||||
}
|
||||
1059
src/symex/smt.rs
Normal file
1059
src/symex/smt.rs
Normal file
File diff suppressed because it is too large
Load diff
551
src/symex/state.rs
Normal file
551
src/symex/state.rs
Normal file
|
|
@ -0,0 +1,551 @@
|
|||
//! Symbolic state tracking per-SSA-value expressions and path constraints.
|
||||
|
||||
use std::collections::{HashMap, HashSet};
|
||||
|
||||
use crate::constraint::ConditionExpr;
|
||||
use crate::ssa::const_prop::ConstLattice;
|
||||
use crate::ssa::ir::{BlockId, SsaBody, SsaValue};
|
||||
use crate::taint::Finding;
|
||||
|
||||
use super::heap::SymbolicHeap;
|
||||
use super::value::SymbolicValue;
|
||||
|
||||
/// A branch constraint collected along the path.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct PathConstraint {
|
||||
/// The block where this branch was taken.
|
||||
pub block: BlockId,
|
||||
/// The structured condition expression.
|
||||
pub condition: ConditionExpr,
|
||||
/// `true` = took the true branch; `false` = took the false branch.
|
||||
pub polarity: bool,
|
||||
}
|
||||
|
||||
/// Symbolic state for a path walk through SSA blocks.
|
||||
///
|
||||
/// Tracks a symbolic expression tree per SSA value, branch constraints
|
||||
/// collected along the path, and a flat taint root-set with eager propagation.
|
||||
///
|
||||
/// `Clone` is required for multi-path exploration: the executor clones the
|
||||
/// state at branch forks to explore both successors independently.
|
||||
#[derive(Clone)]
|
||||
pub struct SymbolicState {
|
||||
/// Symbolic value for each SSA value encountered on the path.
|
||||
values: HashMap<SsaValue, SymbolicValue>,
|
||||
/// Branch constraints collected along the path.
|
||||
path_constraints: Vec<PathConstraint>,
|
||||
/// SSA values known to carry taint. Eagerly propagated during transfer —
|
||||
/// no recursive expression-tree walking needed.
|
||||
tainted_roots: HashSet<SsaValue>,
|
||||
/// Field-sensitive symbolic heap.
|
||||
heap: SymbolicHeap,
|
||||
/// Exception context for catch-path symbolic execution.
|
||||
/// When `Some`, the next `CatchParam` instruction consumes this value and
|
||||
/// marks itself tainted. This is NOT a faithful model of the thrown value —
|
||||
/// it is a taint carrier that signals "this CatchParam was reached via an
|
||||
/// exception edge and should be treated as tainted." The symbolic value is
|
||||
/// `Unknown` because we do not model the exception object's structure.
|
||||
exception_context: Option<SymbolicValue>,
|
||||
}
|
||||
|
||||
impl SymbolicState {
|
||||
/// Create an empty symbolic state.
|
||||
pub fn new() -> Self {
|
||||
SymbolicState {
|
||||
values: HashMap::new(),
|
||||
path_constraints: Vec::new(),
|
||||
tainted_roots: HashSet::new(),
|
||||
heap: SymbolicHeap::new(),
|
||||
exception_context: None,
|
||||
}
|
||||
}
|
||||
|
||||
/// Get the symbolic value for an SSA value.
|
||||
///
|
||||
/// Returns a clone of the mapped value, or `Unknown` if absent.
|
||||
pub fn get(&self, v: SsaValue) -> SymbolicValue {
|
||||
self.values
|
||||
.get(&v)
|
||||
.cloned()
|
||||
.unwrap_or(SymbolicValue::Unknown)
|
||||
}
|
||||
|
||||
/// Set the symbolic value for an SSA value.
|
||||
pub fn set(&mut self, v: SsaValue, val: SymbolicValue) {
|
||||
self.values.insert(v, val);
|
||||
}
|
||||
|
||||
/// Record a branch constraint taken along this path.
|
||||
pub fn add_constraint(&mut self, c: PathConstraint) {
|
||||
self.path_constraints.push(c);
|
||||
}
|
||||
|
||||
/// Get all path constraints accumulated on this path.
|
||||
pub fn path_constraints(&self) -> &[PathConstraint] {
|
||||
&self.path_constraints
|
||||
}
|
||||
|
||||
/// Iterate over all (SsaValue, SymbolicValue) entries in the state.
|
||||
pub fn iter_values(&self) -> impl Iterator<Item = (&SsaValue, &SymbolicValue)> {
|
||||
self.values.iter()
|
||||
}
|
||||
|
||||
/// Mark an SSA value as tainted (adds to the root set).
|
||||
pub fn mark_tainted(&mut self, v: SsaValue) {
|
||||
self.tainted_roots.insert(v);
|
||||
}
|
||||
|
||||
/// Check if an SSA value is tainted (flat set membership).
|
||||
pub fn is_tainted(&self, v: SsaValue) -> bool {
|
||||
self.tainted_roots.contains(&v)
|
||||
}
|
||||
|
||||
/// Get the set of all tainted SSA values.
|
||||
pub fn tainted_values(&self) -> &HashSet<SsaValue> {
|
||||
&self.tainted_roots
|
||||
}
|
||||
|
||||
/// Set the exception context for catch-path CatchParam seeding.
|
||||
pub fn set_exception_context(&mut self, val: SymbolicValue) {
|
||||
self.exception_context = Some(val);
|
||||
}
|
||||
|
||||
/// Consume the exception context. Returns `Some` exactly once per catch block.
|
||||
pub fn take_exception_context(&mut self) -> Option<SymbolicValue> {
|
||||
self.exception_context.take()
|
||||
}
|
||||
|
||||
/// Propagate taint: if any operand is tainted, mark `result` as tainted.
|
||||
pub fn propagate_taint(&mut self, result: SsaValue, operands: &[SsaValue]) {
|
||||
if operands.iter().any(|op| self.tainted_roots.contains(op)) {
|
||||
self.tainted_roots.insert(result);
|
||||
}
|
||||
}
|
||||
|
||||
/// Widen symbolic precision at a loop head after bounded unrolling.
|
||||
///
|
||||
/// Sets all phi-defined values in the block to `Unknown` (we no longer
|
||||
/// know the concrete shape after arbitrary loop iterations), but
|
||||
/// **preserves taint**: if a phi value was tainted before widening, it
|
||||
/// remains tainted. `Unknown + tainted` means "shape unknown but still
|
||||
/// attacker-controlled."
|
||||
/// Get a reference to the symbolic heap.
|
||||
pub fn heap(&self) -> &SymbolicHeap {
|
||||
&self.heap
|
||||
}
|
||||
|
||||
/// Get a mutable reference to the symbolic heap.
|
||||
pub fn heap_mut(&mut self) -> &mut SymbolicHeap {
|
||||
&mut self.heap
|
||||
}
|
||||
|
||||
pub fn widen_at_loop_head(&mut self, block: BlockId, ssa: &SsaBody) {
|
||||
let block_data = &ssa.blocks[block.0 as usize];
|
||||
for phi in &block_data.phis {
|
||||
self.values.insert(phi.value, SymbolicValue::Unknown);
|
||||
// PRESERVE taint — do NOT remove from tainted_roots.
|
||||
}
|
||||
// Widen heap: degrade field symbolic precision, preserve taint.
|
||||
self.heap.widen();
|
||||
}
|
||||
|
||||
/// Seed symbolic values from SSA constant propagation results.
|
||||
///
|
||||
/// Maps `ConstLattice::Int(i)` to `Concrete(i)` and
|
||||
/// `ConstLattice::Str(s)` to `ConcreteStr(s)`. Other lattice values
|
||||
/// (Bool, Null, Top, Varying) are left as `Unknown` (not stored).
|
||||
pub fn seed_from_const_values(&mut self, const_values: &HashMap<SsaValue, ConstLattice>) {
|
||||
for (&v, cl) in const_values {
|
||||
match cl {
|
||||
ConstLattice::Int(i) => {
|
||||
self.values.insert(v, SymbolicValue::Concrete(*i));
|
||||
}
|
||||
ConstLattice::Str(s) => {
|
||||
self.values.insert(v, SymbolicValue::ConcreteStr(s.clone()));
|
||||
}
|
||||
_ => {} // Bool, Null, Top, Varying — not modeled
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Resolve a phi to the operand from a specific predecessor.
|
||||
///
|
||||
/// Returns the symbolic value for the matched predecessor's operand.
|
||||
/// Falls back to full `mk_phi(...)` only when the predecessor is genuinely
|
||||
/// not found among the phi's operands (e.g. unreachable predecessor was
|
||||
/// pruned during SSA construction).
|
||||
pub fn resolve_phi_from_predecessor(
|
||||
&self,
|
||||
operands: &[(BlockId, SsaValue)],
|
||||
predecessor: BlockId,
|
||||
) -> SymbolicValue {
|
||||
for (bid, v) in operands {
|
||||
if *bid == predecessor {
|
||||
return self.get(*v);
|
||||
}
|
||||
}
|
||||
// Fallback: build the full phi expression
|
||||
let phi_ops: Vec<_> = operands
|
||||
.iter()
|
||||
.map(|(bid, v)| (*bid, self.get(*v)))
|
||||
.collect();
|
||||
super::value::mk_phi(phi_ops)
|
||||
}
|
||||
|
||||
/// Generate a witness string for the sink value of a finding.
|
||||
///
|
||||
/// Looks up the sink's SSA value via `cfg_node_map`, retrieves its
|
||||
/// symbolic expression, and formats it. Returns `None` if the value
|
||||
/// is `Unknown` (no useful witness).
|
||||
pub fn get_sink_witness(&self, finding: &Finding, ssa: &SsaBody) -> Option<String> {
|
||||
let ssa_val = ssa.cfg_node_map.get(&finding.sink)?;
|
||||
let sym = self.get(*ssa_val);
|
||||
if matches!(sym, SymbolicValue::Unknown) {
|
||||
return None;
|
||||
}
|
||||
Some(format!("{}", sym))
|
||||
}
|
||||
}
|
||||
|
||||
impl Default for SymbolicState {
|
||||
fn default() -> Self {
|
||||
Self::new()
|
||||
}
|
||||
}
|
||||
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
// Tests
|
||||
// ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
|
||||
#[test]
|
||||
fn get_returns_unknown_for_absent() {
|
||||
let state = SymbolicState::new();
|
||||
assert_eq!(state.get(SsaValue(99)), SymbolicValue::Unknown);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn set_get_round_trip() {
|
||||
let mut state = SymbolicState::new();
|
||||
state.set(SsaValue(1), SymbolicValue::Concrete(42));
|
||||
assert_eq!(state.get(SsaValue(1)), SymbolicValue::Concrete(42));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn set_overwrites() {
|
||||
let mut state = SymbolicState::new();
|
||||
state.set(SsaValue(1), SymbolicValue::Concrete(1));
|
||||
state.set(SsaValue(1), SymbolicValue::Concrete(2));
|
||||
assert_eq!(state.get(SsaValue(1)), SymbolicValue::Concrete(2));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn mark_tainted_and_check() {
|
||||
let mut state = SymbolicState::new();
|
||||
assert!(!state.is_tainted(SsaValue(1)));
|
||||
state.mark_tainted(SsaValue(1));
|
||||
assert!(state.is_tainted(SsaValue(1)));
|
||||
assert!(!state.is_tainted(SsaValue(2)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn propagate_taint_with_tainted_operand() {
|
||||
let mut state = SymbolicState::new();
|
||||
state.mark_tainted(SsaValue(1));
|
||||
state.propagate_taint(SsaValue(3), &[SsaValue(1), SsaValue(2)]);
|
||||
assert!(state.is_tainted(SsaValue(3)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn propagate_taint_with_no_tainted_operand() {
|
||||
let mut state = SymbolicState::new();
|
||||
state.propagate_taint(SsaValue(3), &[SsaValue(1), SsaValue(2)]);
|
||||
assert!(!state.is_tainted(SsaValue(3)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn propagate_taint_chain() {
|
||||
let mut state = SymbolicState::new();
|
||||
state.mark_tainted(SsaValue(0)); // source
|
||||
state.propagate_taint(SsaValue(1), &[SsaValue(0)]); // copy
|
||||
state.propagate_taint(SsaValue(2), &[SsaValue(1), SsaValue(99)]); // binop
|
||||
assert!(state.is_tainted(SsaValue(1)));
|
||||
assert!(state.is_tainted(SsaValue(2)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn seed_from_const_values_int() {
|
||||
let mut state = SymbolicState::new();
|
||||
let mut cv = HashMap::new();
|
||||
cv.insert(SsaValue(1), ConstLattice::Int(42));
|
||||
state.seed_from_const_values(&cv);
|
||||
assert_eq!(state.get(SsaValue(1)), SymbolicValue::Concrete(42));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn seed_from_const_values_str() {
|
||||
let mut state = SymbolicState::new();
|
||||
let mut cv = HashMap::new();
|
||||
cv.insert(SsaValue(2), ConstLattice::Str("hello".into()));
|
||||
state.seed_from_const_values(&cv);
|
||||
assert_eq!(
|
||||
state.get(SsaValue(2)),
|
||||
SymbolicValue::ConcreteStr("hello".into())
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn seed_from_const_values_bool_ignored() {
|
||||
let mut state = SymbolicState::new();
|
||||
let mut cv = HashMap::new();
|
||||
cv.insert(SsaValue(3), ConstLattice::Bool(true));
|
||||
state.seed_from_const_values(&cv);
|
||||
assert_eq!(state.get(SsaValue(3)), SymbolicValue::Unknown);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn seed_from_const_values_null_ignored() {
|
||||
let mut state = SymbolicState::new();
|
||||
let mut cv = HashMap::new();
|
||||
cv.insert(SsaValue(4), ConstLattice::Null);
|
||||
state.seed_from_const_values(&cv);
|
||||
assert_eq!(state.get(SsaValue(4)), SymbolicValue::Unknown);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn get_sink_witness_for_concrete() {
|
||||
let mut state = SymbolicState::new();
|
||||
state.set(
|
||||
SsaValue(5),
|
||||
SymbolicValue::ConcreteStr("SELECT * FROM t".into()),
|
||||
);
|
||||
|
||||
let node = petgraph::graph::NodeIndex::new(10);
|
||||
let finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: node,
|
||||
source: petgraph::graph::NodeIndex::new(0),
|
||||
path: vec![],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: false,
|
||||
guard_kind: None,
|
||||
hop_count: 0,
|
||||
cap_specificity: 0,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: [(node, SsaValue(5))].into_iter().collect(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
let witness = state.get_sink_witness(&finding, &ssa);
|
||||
assert_eq!(witness, Some("\"SELECT * FROM t\"".into()));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn get_sink_witness_unknown_returns_none() {
|
||||
let state = SymbolicState::new();
|
||||
|
||||
let node = petgraph::graph::NodeIndex::new(10);
|
||||
let finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: node,
|
||||
source: petgraph::graph::NodeIndex::new(0),
|
||||
path: vec![],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: false,
|
||||
guard_kind: None,
|
||||
hop_count: 0,
|
||||
cap_specificity: 0,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: [(node, SsaValue(5))].into_iter().collect(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
assert_eq!(state.get_sink_witness(&finding, &ssa), None);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn get_sink_witness_unmapped_node_returns_none() {
|
||||
let state = SymbolicState::new();
|
||||
let finding = Finding {
|
||||
body_id: crate::cfg::BodyId(0),
|
||||
sink: petgraph::graph::NodeIndex::new(99), // not in cfg_node_map
|
||||
source: petgraph::graph::NodeIndex::new(0),
|
||||
path: vec![],
|
||||
source_kind: crate::labels::SourceKind::UserInput,
|
||||
path_validated: false,
|
||||
guard_kind: None,
|
||||
hop_count: 0,
|
||||
cap_specificity: 0,
|
||||
uses_summary: false,
|
||||
flow_steps: vec![],
|
||||
symbolic: None,
|
||||
source_span: None,
|
||||
primary_location: None,
|
||||
engine_notes: smallvec::SmallVec::new(),
|
||||
path_hash: 0,
|
||||
finding_id: String::new(),
|
||||
alternative_finding_ids: smallvec::SmallVec::new(),
|
||||
};
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
assert_eq!(state.get_sink_witness(&finding, &ssa), None);
|
||||
}
|
||||
|
||||
// ─── widen_at_loop_head tests ────────────────────────────────────────
|
||||
|
||||
#[test]
|
||||
fn widen_at_loop_head_sets_phi_to_unknown() {
|
||||
use crate::ssa::ir::{SsaBlock, SsaInst, SsaOp, Terminator};
|
||||
use smallvec::smallvec;
|
||||
|
||||
let mut state = SymbolicState::new();
|
||||
state.set(SsaValue(0), SymbolicValue::Concrete(10));
|
||||
state.set(SsaValue(1), SymbolicValue::Concrete(42));
|
||||
// v1 is defined by a phi in block 0
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![SsaInst {
|
||||
value: SsaValue(1),
|
||||
op: SsaOp::Phi(smallvec![
|
||||
(BlockId(0), SsaValue(0)),
|
||||
(BlockId(1), SsaValue(0))
|
||||
]),
|
||||
cfg_node: petgraph::graph::NodeIndex::new(0),
|
||||
var_name: None,
|
||||
span: (0, 0),
|
||||
}],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![],
|
||||
}],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
state.widen_at_loop_head(BlockId(0), &ssa);
|
||||
|
||||
// Phi value widened to Unknown
|
||||
assert_eq!(state.get(SsaValue(1)), SymbolicValue::Unknown);
|
||||
// Non-phi value preserved
|
||||
assert_eq!(state.get(SsaValue(0)), SymbolicValue::Concrete(10));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn widen_at_loop_head_preserves_taint() {
|
||||
use crate::ssa::ir::{SsaBlock, SsaInst, SsaOp, Terminator};
|
||||
use smallvec::smallvec;
|
||||
|
||||
let mut state = SymbolicState::new();
|
||||
state.set(SsaValue(1), SymbolicValue::Symbol(SsaValue(1)));
|
||||
state.mark_tainted(SsaValue(1));
|
||||
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![SsaInst {
|
||||
value: SsaValue(1),
|
||||
op: SsaOp::Phi(smallvec![
|
||||
(BlockId(0), SsaValue(0)),
|
||||
(BlockId(1), SsaValue(0))
|
||||
]),
|
||||
cfg_node: petgraph::graph::NodeIndex::new(0),
|
||||
var_name: None,
|
||||
span: (0, 0),
|
||||
}],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![],
|
||||
}],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
state.widen_at_loop_head(BlockId(0), &ssa);
|
||||
|
||||
// Symbolic precision degraded
|
||||
assert_eq!(state.get(SsaValue(1)), SymbolicValue::Unknown);
|
||||
// Taint PRESERVED
|
||||
assert!(state.is_tainted(SsaValue(1)));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn widen_at_loop_head_untainted_stays_untainted() {
|
||||
use crate::ssa::ir::{SsaBlock, SsaInst, SsaOp, Terminator};
|
||||
use smallvec::smallvec;
|
||||
|
||||
let mut state = SymbolicState::new();
|
||||
state.set(SsaValue(1), SymbolicValue::Concrete(5));
|
||||
// NOT tainted
|
||||
|
||||
let ssa = SsaBody {
|
||||
blocks: vec![SsaBlock {
|
||||
id: BlockId(0),
|
||||
phis: vec![SsaInst {
|
||||
value: SsaValue(1),
|
||||
op: SsaOp::Phi(smallvec![
|
||||
(BlockId(0), SsaValue(0)),
|
||||
(BlockId(1), SsaValue(0))
|
||||
]),
|
||||
cfg_node: petgraph::graph::NodeIndex::new(0),
|
||||
var_name: None,
|
||||
span: (0, 0),
|
||||
}],
|
||||
body: vec![],
|
||||
terminator: Terminator::Return(None),
|
||||
preds: smallvec![],
|
||||
succs: smallvec![],
|
||||
}],
|
||||
entry: BlockId(0),
|
||||
value_defs: vec![],
|
||||
cfg_node_map: HashMap::new(),
|
||||
exception_edges: vec![],
|
||||
};
|
||||
|
||||
state.widen_at_loop_head(BlockId(0), &ssa);
|
||||
|
||||
assert_eq!(state.get(SsaValue(1)), SymbolicValue::Unknown);
|
||||
assert!(!state.is_tainted(SsaValue(1)));
|
||||
}
|
||||
}
|
||||
1661
src/symex/strings.rs
Normal file
1661
src/symex/strings.rs
Normal file
File diff suppressed because it is too large
Load diff
2427
src/symex/transfer.rs
Normal file
2427
src/symex/transfer.rs
Normal file
File diff suppressed because it is too large
Load diff
1268
src/symex/value.rs
Normal file
1268
src/symex/value.rs
Normal file
File diff suppressed because it is too large
Load diff
1209
src/symex/witness.rs
Normal file
1209
src/symex/witness.rs
Normal file
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue