Symbolic Execution Explained: Finding Bugs in Complex Code Paths

on YouTube ↗18m

" summary

Sonar’s static analyzer uses symbolic execution to simulate execution paths with symbolic ranges (e.g., remainder 0..9 or -9..0) and flags contradictions; it finds a real bug in .NET’s SqlMoney rounding where C#’s negative remainder in C# makes the “round up if remainder ≥ 5” branch unreachable. The engine produces a path map, reports the unreachable branch detected, and the issue is reported to the repo — the analyzer successfully exposes the root cause.

AI-written summary · about

" chapters (27)

1. 0:00Introduction
2. 0:27How Conditionals Create Alternate Code Execution Paths
3. 1:03Using Symbolic Execution to Map Possible Code Paths
4. 1:22Real Bug Example from the .NET Runtime
5. 1:56SqlMoney Conversion and Rounding Logic Explained
6. 3:01How Modulo Behavior Introduces a Hidden Bug
7. 4:27Why C# Modulo Keeps the Negative Sign
8. 4:47Example Demonstrating Incorrect Rounding Behavior
9. 5:34Why This Type of Bug Is Hard to Detect
10. 5:51Static Analyzer Detects Unreachable Code Paths
11. 6:44How Symbolic Execution Works in Static Code Analysis
12. 7:18Symbolic Values Represent Input Ranges
13. 8:03Engine Simulates Different Execution Paths
14. 8:47First Scenario: Positive Value Execution Path
15. 9:18Remainder Range Becomes 0 to 9
16. 10:07Branch Where Remainder Is Less Than 5
17. 10:47Branch Where Remainder Is Greater Than or Equal to 5
18. 11:17Inner Condition Always True in This Scenario
19. 11:53Second Scenario: Negative Value Execution Path
20. 13:15Negative Modulo Produces a Negative Remainder
21. 13:52Why the Condition “Remainder ≥ 5” Becomes Impossible
22. 14:22Missing Execution Scenario Reveals the Bug
23. 15:15Analyzer Detects the Unreachable Code Path
24. 16:16Root Cause: Negative Modulo Behavior in C#
25. 16:33Static Analysis Also Detects Null Dereference Risks
26. 16:45Detecting Index Out-of-Bounds Errors Automatically
27. 16:56How Symbolic Execution Finds Subtle Software Bugs

" related talks

• 01h 01mSymbolic Execution in .NETDmitriy Ivanov, Dmitriy Mordvinov · DotNext 2021 Moscow
• 52mFinding Bugs Using Path-Sensitive Static AnalysisGabor Horvath · CppCon 2021
• 55mCode Analysis with Zero False Positives in JavaDmitriy Ivanov, Dmitriy Mordvinov · Joker 2022
• 20mDerivative-Guided Symbolic ExecutionJulia Belyakova, Zhe Zhou, Suresh Jagannathan, Yongwei Yuan · POPL 2025
• 31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...Xavier Rival, Tamara Rezk, Ignacio Tiraboschi · VMCAI 2023
• 38mStatic Code Analysis - A Behind-the-scenes LookArno Haase · GOTO Amsterdam 2022
• 14mCompatible Branch Coverage Driven Symbolic Execution for Efficient Bug FindingQiuping Yi, Yifan Yu, Guowei Yang · PLDI 2024
• 33mSymbolic value-flow static analysis:deep,precise,complete modeling of Ethereum smartcontractsYannis Smaragdakis, Neville Grech, Ilias Tsatiris, Sifis Lagouvardos, Konstantinos Triantafyllou · SPLASH 2022