Symbolic Execution Explained: Finding Bugs in Complex Code Paths | Sonar Summit 2026

Understanding the Multiverse of Code

Every conditional statement in a codebase creates branching execution paths, essentially spawning alternative "universes" of what could happen during runtime. As each new if statement and condition is added, the number of possible code paths multiplies exponentially, creating what Tim Pohlmann from Sonar describes as a "multiverse" of potential behaviors. Since static analysis examines code before execution, developers cannot simply run the program with every possible input to verify correctness. Instead, modern code analysis tools employ symbolic execution—a technique that creates a comprehensive map of these code paths and systematically analyzes them for potential problems without requiring concrete execution.

A Real-World Bug in Production Code

To illustrate the power of symbolic execution, Pohlmann examined actual production code from Microsoft's .NET runtime, specifically a method in the SqlMoney class designed to convert monetary values to 64-bit integers. The ToInt64 method performs mathematical calculations and rounding operations that should convert -2.6 to -3. However, a subtle bug exists in how the code handles negative number rounding. The issue stems from the modulo operator's behavior with negative values: while Python returns positive remainders for negative modulo operations, C# preserves the sign, returning negative remainders. In this case, when processing a negative value, the remainder becomes negative and can never satisfy the condition of being equal to or greater than five, causing the rounding logic for negative numbers to never execute. This results in incorrect output—returning -2 instead of the correct -3—yet the bug remained undetected until discovered by Sonar's analyzer.

How Symbolic Execution Detects the Bug

Rather than testing code with arbitrary concrete values, symbolic execution uses symbolic values that represent categories or ranges of numbers—such as positive, negative, or bounded ranges. The analyzer steps through code systematically, tracking how these symbolic values change based on conditions and operations. When it encounters the condition checking if a value is greater than or equal to zero, it branches analysis into two paths: one where the condition is true and one where it is false. For each path, the analyzer tracks the consequences of that assumption. In the SqlMoney case, the analyzer determined that the nested condition for rounding negative numbers (remainder >= 5) could never be true when the outer condition was false, making that code path unreachable. The analyzer reported this impossibility by highlighting the condition and noting that the else branch is unreachable—a clear signal that something is wrong, either a logic error or unnecessary dead code.

The Power of Structural Analysis

The symbolic execution engine does not require understanding the semantic meaning or intent of the code—it does not need to know what ToInt64 means or what the method is supposed to accomplish. Instead, it analyzes the structural properties and logical flow of the code itself. By tracking how values transform through operations and how conditions constrain those values, the analyzer can identify impossible code paths and logical contradictions that humans might easily overlook, especially when those contradictions depend on subtle language-specific behaviors like how different programming languages handle the modulo operator.

Key Takeaways

• Symbolic execution maps code paths by analyzing conditions and tracking symbolic value ranges rather than testing with concrete values, making it feasible to analyze complex branching logic
• Language-specific behaviors matter: The modulo operator's treatment of negative numbers differs across programming languages (Python vs. C#), creating subtle bugs that are difficult for humans to spot through code review
• Unreachable code signals problems: When symbolic execution detects logically impossible code paths, it highlights either genuine bugs or unnecessary dead code that should be removed
• Structural analysis finds what intent-based review misses: The analyzer requires no semantic understanding of code purpose, allowing it to detect issues that depend on technical language details rather than business logic
• Real-world production code is vulnerable: Even critical codebases like .NET runtime can contain subtle logical errors that persist until discovered by advanced static analysis techniques