Automation and Validation in Compiler Technology
Explore the world of compiler technology with a focus on finding and validating bugs, utilizing cross-version validation strategies, and tools like SymDiff, Boogie, and Z3 for efficient code verification and optimization.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Will You Still Compile Me Tomorrow Will You Still Compile Me Tomorrow? ? Static Static Cross Cross- -Version Compiler Version Compiler Validation Validation Chris Hawblitzel, Shuvendu K. Lahiri (Microsoft Research) Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth (Microsoft CLR Test Team)
Finding compiler bugs Testing Validation Verification Source program Source program Automated theorem Interactive theorem prover prover Compiler Compiler Compiler Assembly code Test input Assembly code Output + covers all inputs - false alarms + covers all programs - not automated + high automation - limited coverage
Cross-version validation push ESI mov ESI, EDX Source program Source program mov EAX, EDX and EAX, 255 push EAX mov EDX, 0x100000 call WriteInternalFlag2 and ESI, 255 push ESI mov EDX, 0x100000 call WriteInternalFlag2 Compiler version 4.0 Compiler version 4.5 Assembly code Assembly code pop ESI ret ret Automated theorem prover compare similar code fewer false alarms
Validation across various dimensions Assembly code ARM Assembly code Assembly code ARM +optimizations x86 Assembly code Assembly code Assembly code x86 +optimizations v1 v2 v3 v4 Versions
Tools: SymDiff, Boogie, Z3 Source program Source program Compiler version 4.0 Compiler version 4.5 ... Mem := Store4(...esi...); esp := SUB(esp, imm(4)); ... ... push ESI ... Assembly code Assembly code Boogie program Boogie program Z3 automated theorem prover Boogie program verifier SymDiff equivalence verifier Verification condition Combined Boogie program
Encoding assembly language Encode one method at a time calls are uninterpreted inlining not yet supported Our encoding is not entirely sound mathematical integers vs. 32-bit vectors Z3 supports both, but reasoning about integers is faster non-aliasing assumptions disjoint regions for stack, heap, static data Floating point, switch tables, etc. Complex instructions rep stosb: i. edx i edx+ecx Mem[i] == al
Month-to-month results (ARM) 100% 80% method bodies 60% 40% 20% 0% month2 month3 month4,5 month6 month7 1.1 1.2 2.6 1.4 3.8 3.8 1.8 1.6 3.3 57.9 24.4 19.2 37.8 69.0 71.1 AVG 1.7 2.4 3.0 24.5 68.3 Missing TimeOut Different Equivalent Identical 1.9 2.7 7.0 19.4 69.1 1.8 0.3 1.5 1.9 94.5
Cross-architecture, optimization 100% method bodies 80% 60% 40% 20% 0% x86 opt vs. unopt 1.9 2.0 19.0 77.0 0.0 ARM opt vs. unopt 5.5 1.7 18.8 73.8 0.0 x86 vs. ARM MDIL vs. JIT Missing TimeOut Different Equivalent Identical 3.6 4.7 29.0 62.8 0.0 13.5 1.3 20.0 65.2 0.0
Fault injection (ARM) 100% method bodies 80% 60% 40% 20% 0% month 5 1.9 0.7 86.3 7.5 2.5 month 6 3.1 0.7 83.1 8.8 2.5 month 7 3.3 0.0 81.3 10.0 3.3 m 3,4 AVG Missing TimeOut Different Equiv-correct Equiv-unsound 3.1 0.6 86.9 5.6 3.8 2.9 0.5 84.4 8.0 3.0
Counterexample traces Helps user find where program execution diverged Used by automated root cause analysis
Bucketing Based on root cause analysis Users write bucket descriptions
Conclusions Some statistics: methods analyzed: > 500,000 new bugs found: 12 false alarm rate, month-to-month versions: 2.2% false alarm rate, opt vs. unopt, ARM vs x86: > 20% speed: 13 seconds per method Sources of false alarms: aliasing, run-time system calls, embedded addresses, ... Counterexample traces, root cause analysis essential
