曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
analysis to use those as specifications?”
Bor-Yuh Evan Chang - End-User Program Analysis
9
Summary of overview
Challenge in analysis: Finding a good abstraction
precise enough but not more than necessary
Powerful, generic abstractions
expensive, hard to use and understand
Built-in, default abstractions
often not precise enough (e.g., data structures)
End-user approach:
Must involve the user in abstraction
without expecting the user to be a program analysis
expert
Bor-Yuh Evan Chang - End-User Program Analysis
10
Overview of contributions
Extensible Inductive Shape Analysis [POPL’08,SAS’07]
Precise inference of data structure properties
Able to check, for instance, the locking example
Targeted to software developers
Uses data structure checking code for guidance
Turns testing code into a specification for static
analysis
Efficient
~10-100x speed-up over generic approaches
Builds abstraction out of developer-supplied
checking code
Bor-Yuh Evan Chang - End-User Program Analysis
Extensible Inductive
Shape Analysis
Precise inference of
data structure properties
End--usserr apprroacch
[POPL’08, SAS’07]
…
12
Shape analysis is a fundamental analysis
Data structures are at the core of
– Traditional languages (C, C++, Java)
– Emerging web scripting languages
Improves verifiers that try to
– Eliminate resource usage bugs
(locks, file handles)
– Eliminate memory errors (leaks, dangling pointers)
– Eliminate concurrency errors (data races)
– Validate developer assertions
Enables program transformations
– Compile-time garbage collection
– Data structure refactorings
…
Bor-Yuh Evan Chang - End-User Program Analysis
13
Shape analysis by example:
Removing duplicates
// l is a sorted doubly-linked list
for each node cur in list l {
remove cur if duplicate;
}
assertl is sorted, doubly-linked
with no duplicates;
Example/Testing Code Review/Static Analysis
l “no duplicates”
l “sorted dl list”
prroggrram--sspecciiffiicc
l 2 2 4 4
l 2 4 4
cur
l 2 4
l “sorted dl list”
“segment with
no duplicates”
cur
intermediate state
more complicated
Bor-Yuh Evan Chang - End-User Program Analysis
14
Shape analysis is not yet practical
Choosing the heap abstraction difficult for precision
Parametric in high-level,
developer-oriented predicates
+ Extensible
Xisa + Targeted to developers
Built-in high-level predicates
- Hard to extend
+ No additional user effort (if
precise enough)
Parametric in low-level,
analyzer-oriented predicates
+ Very general and expressive
- Hard for non-expert 89
Bor-Yuh Evan Chang - End-User Program Analysis
Traditional approaches:
End-user approach:
Space Invader
[Distefano et al.]
TVLA
[Sagiv et al.]
15
Key insight
for being developer-friendly and efficient
Utilize “run-time checking code” as specification
for static analysis.
assert(sorted_dll(l,…));
for each node cur in list l {
remove cur if duplicate;
}
assert(sorted_dll_nodup(l,…));
l
l
cur
l
Bor-Yuh Evan Chang - End-User Program Analysis
dll(h, p) =
if (h = null) then
true
else
h!prev = p and
dll(h!next, h)
checker
Contribution:
Automatically
generalize checkers
for complicated
intermediate states
Contribution:
Build the abstraction
for analysis out of
developer-specified
checking code
• p specifies where
prev should point
16
Our framework is …
• Extensible and targeted for developers
– Parametric in developer-supplied checkers
• Precise yet compact abstraction for efficiency
– Data structure-specific based on properties of interest
to the developer
An automated shape analysis with a precise memory
abstraction based around invariant checkers.
shape analyzer
dll(h, p) =
if (h = null) then
true
else
h!prev = prev and
dll(h!next, h)
checkers
Bor-Yuh Evan Chang - End-User Program Analysis
17
Splitting of summaries
To reflect updates precisely
And summarizing for termination
Shape analysis is an abstract interpretation
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(49)
