Shape Analysis — heapdagi dinamik pointer tuzilmalar list, tree, cycle yoki umumiy graph shaklini qanday hosil qilishini statik ravishda baholaydigan tahlil. U oddiy points-to to‘plamdan ko‘ra obyektlar orasidagi aloqani boyroq tasvirlaydi.
Abstract heap
Analyzer ko‘p concrete heapni bitta abstract heap graphga jamlaydi. Abstract node bitta yoki ko‘p obyektni ifodalashi, edge esa field reference’ni ko‘rsatishi mumkin. summary node sabab aniqlik yo‘qolsa three-valued logic orqali edge albatta bor, albatta yo‘q yoki noma’lum deb belgilanadi.
List misoli
Linked list traversalda joriy pointer oldidagi segment va qolgan segment alohida abstractlanishi mumkin. Materialization summary node’dan joriy concrete elementni ajratadi; pointer oldinga siljigach, eski element yana summaryga qo‘shiladi. Shu yo‘l bilan uzunligi cheklanmagan list finite holatlar bilan tahlil qilinadi.
Shape invariantlar
Shape invariantlar acycliclik, reachability, sharing va disjointnessni ifodalaydi. Tree update noto‘g‘ri edge qo‘shib cycle yaratmasligini yoki free qilingan node qayta ishlatilmasligini tekshirish mumkin. Umumiy graph va arbitrary pointer arithmetic tahlilni ancha qimmat yoki noaniq qiladi.
Formal yondashuvlar
Separation logic asosidagi analyzer heap qismlarining disjointligini formulalar bilan tasvirlaydi; TVLA kabi yondashuvlar three-valued logical structure ishlatadi. Widening fixed pointni kafolatlaydi, lekin juda erta widening muhim shape farqlarini yo‘qotishi mumkin.
Sinov
Sinov list insert/delete, cycle creation, shared tail, null edge va use-after-free patternlarini qamraydi. Analyzer topgan invariant runtime heap checker bilan kichik boundlarda solishtiriladi. False positive soni precisionni, o‘tkazib yuborilgan real xato esa soundness muammosini ko‘rsatadi.
Shape Analysis bo‘yicha tahlil natijasi faqat yakuniy xulosa bilan emas, uni hosil qilgan IR versiyasi, target xususiyatlari va qo‘llangan taxminlar bilan birga saqlanadi. Compiler passlari ketma-ket o‘zgarganda oldingi natija avtomatik ravishda haqiqiy deb olinmaydi: tegishli dependencylar invalidatsiya qilinib, zarur qism qayta hisoblanadi. Debug rejimida asosiy invariant buzilgan nuqta va undan oldingi transformatsiya qayd etiladi; release rejimida esa tekshiruvlarning arzon qismi qoldiriladi. Shu yondashuv nazariy jihatdan qonuniy qoida implementatsiya xatosi yoki noto‘g‘ri cost model sabab zararli qarorga aylangan holatni ajratishga yordam beradi.
Kengaytirilgan jihatlar
Shape analysis assertionlari dastur nuqtasida list(x) * tree(y) kabi ajratilgan heap segmentlarini tasvirlashi mumkin. Procedure summary kirish preconditioni va chiqish postconditionini saqlab, caller heapiga frame rule bilan qo‘llanadi. Abduction yetishmayotgan preconditionni topishda ishlatiladi. Memory allocator modeli freed node’ni alohida holatga o‘tkazadi; faqat reachabilityni yo‘qotish free bo‘lganini anglatmaydi. Concurrencyda boshqa thread heap edge’larini o‘zgartirishi mumkin, shu sabab ownership yoki lock invariant kerak. Analyzer proof trace bersa, foydalanuvchi false positive sababini abstract graph bo‘yicha ko‘ra oladi.
Shape invariant xato topganda concrete counterexample ishlab chiqarish har doim mumkin emas, chunki abstract state ko‘p heapni birlashtiradi. Bounded model checking abstract yo‘lni concrete qilishga urinadi. Invariant proof qayta foydalanilganda procedure body, summary va allocator model versiyasi tekshiriladi; eskirgan proof yangi kodga tatbiq etilmaydi.
Katta heap modelida time yoki state limiti oshsa, analyzer xulosani “isbotlanmadi” deb belgilaydi. Bunday natija property noto‘g‘ri degani emas va alohida talqin qilinadi.
Bog‘liq tushunchalar
heap analysis, points-to analysis, separation logic, abstract interpretation, reachability, linked list