曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
If it exists, where is:
°!next ?
¯!next ?
Checker Definition
Says:
For h!next/h!prev,
unfold from h
For p!next/p!prev,
unfold before h
Bor-Yuh Evan Chang - End-User Program Analysis
25
Types make the analysis robust with respect
to how checkers are written
¯
dll(®) dll(¯) dll(¯)
°
Instance
Summary dll(h, p) =
if (h = null) then
true
else
h!prev = p and
dll(h!next, h)
Bor-Yuh Evan Chang - End-User Program Analysis
® ¯ ° null
¯ ° null
Instance
¯
dll0 dll0 dll0
°
Summary
dll0(h) =
if (h!next = null)
then
true
else
h!next!prev = h
and dll0(h!next)
AAlltteerrnnaattiivvee ddoouubbllyy--lliinnkkeedd lliisstt cchheecckkeerr
DDoouubbllyy--lliinnkkeedd lliisstt cchheecckkeerr ((aass bbeeffoorree))
Different
types for
different
unfoldin
g
26
Summary of checker parameter types
Tell where to unfold for which fields
Make analysis robust with respect to how
checkers are written
Learn where in summaries unfolding won’t help
Bor-Yuh Evan Chang - End-User Program Analysis
Can be inferred automatically with a fixedpoint
computation on the checker
definitions
27
Summary of interpreting updates
Splitting of summaries needed for precision
Unfolding checkers is a natural way to do
splitting
When checker traversal matches code traversal
Checker parameter types
Enable, for example, “back pointer” traversal
without blindly guessing where to unfold
Bor-Yuh Evan Chang - End-User Program Analysis
28
Outline
shape analyzer
abstract interpretation
splitting and
interpreting update
summarizing
type
inference
on checker
definitions
Bor-Yuh Evan Chang - End-User Program Analysis
1
2
3
dll(h, p) =
if (h = null) then
true
else
h!prev = prev and
dll(h!next, h)
checkers
29
Summarize
by folding into inductive predicates
last = l;
cur = l!next;
while (cur != null) {
// … cur, last …
if (…) last = cur;
cur = cur! next;
}
list
l, last
next
cur
list
l
next next
last cur
list
l
next next next
last cur
summarize
list
last
next list
cur
list
l
Challenge:
Precision (e.g., last, cur
separated by at least one
step)
Previous approaches
guess where to fold
for each graph.
Bor-Yuh Evan Chang - End-User Program Analysis
Contribution:
Determine where by
comparing graphs
across history
30
Summary:
Given checkers, everything is automatic
shape analyzer
abstract interpretation
splitting and
interpreting update
summarizing
type
inference
on checker
definitions
Bor-Yuh Evan Chang - End-User Program Analysis
dll(h, p) =
if (h = null) then
true
else
h!prev = prev and
dll(h!next, h)
checkers
31
Results: Performance
Benchmark
Max. Num.
Graphs at a
Program Pt
Analysis
Time
(ms)
singly-linked list reverse 1 0.6
doubly-linked list reverse 1 1.4
doubly-linked list copy 2 5.3
doubly-linked list remove 5 6.5
doubly-linked list remove and back 5 6.8
search tree with parent insert 5 8.3
search tree with parent insert and back 5 47.0
two-level skip list rebalance 6 87.0
Linux scull driver (894 loc)
(char arrays ignored, functions inlined)
4 9710.0
Times negligible for data
structure operations
(often in sec or 1/10 sec)
Expressiveness:
Different data
structures
Verified shape invariant as given by the
checker is preserved across the operation.
Bor-Yuh Evan Chang - End-User Program Analysis
TTVVLLAA:: 885500 mss
TTVVLLAA:: 229900 mss
Space Invader
only analyzes lists
(built-in)
32
Demo: Doubly-linked list reversal
http://xisa.cs.berkeley.edu
Body of loop over the elements:
Swaps the next and prev fields
of curr.
Allrreadyy rrevverrssed sseggmentt
Node whose next and
prev fields were swapped
Nott yyett rrevverrssed lliisstt
Bor-Yuh Evan Chang - End-User Program Analysis
33
Experience with the tool
Checkers are easy to write and try out
– Enlightening (e.g., red-black tree checker in 6 lines)
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(51)
