Static Program Analysis
Part 6 – path sensitivity
http://cs.au.dk/~amoeller/spa/
Anders Møller & Michael I. Schwartzbach Computer Science, Aarhus University
Information in conditions
x = input;
y = 0;
z = 0;
while (x>0) {
z = z+x;
if (17>y) { y = y+1; } x = x-1;
}
The interval analysis (with widening) concludes: x=[-,],y=[0,], z=[-,]
2
Modeling conditions
Add artifical “assert” statements:
The statement assert(E) models that
E is true in the current program state
• it causes a runtime error otherwise
• but we only insert it where the condition will always be true
3
Encoding conditions
x = input;
y = 0;
z = 0;
while (x>0) {
assert(x>0);
z = z+x;
if (17>y) { assert(17>y); y = y+1; } else { assert(!(17>y)); }
x = x-1;
}
assert(!(x>0));
preserves semantics since asserts are guarded by conditions
(alternatively, we could add dataflow constraints on the CFG edges)
4
Constraints for assert
• Atrivialbutsoundconstraint: ⟦v⟧ = JOIN(v)
• Anon-trivialconstraintforassert(x>E): ⟦v⟧ = JOIN(v)[xgt(JOIN(v)(x),eval(JOIN(v),E))]
where
gt([l1,h1],[l2,h2]) = [l1,h1] ⊓ [l2,]
• Similar constraints are defined for the dual cases • Moretrickytodefineforotherconditions…
5
Exploiting conditions
x = input;
y = 0;
z = 0;
while (x>0) {
assert(x>0);
z = z+x;
if (17>y) { assert(17>y); y = y+1; } else { assert(!(17>y)); }
x = x-1;
} assert(!(x>0));
The interval analysis now concludes: x=[-,0],y=[0,17], z=[0,]
6
Branch correlations
• With assert we have a simple form of path sensitivity (sometimes called control sensitivity)
• Butitisinsufficienttohandlecorrelationofbranches:
if (17 > x) { … }
… // statements that do not change x if (17 > x) { … }
…
7
Open and closed files
• Built-in functions open() and close() on a file
• Requirements:
– never close a closed file
– never open an open file open()
closed
close()
• We want a static analysis to check this… (for simplicity, let us assume there is only one file)
open
8
A tricky example
if (condition) {
open();
flag = 1;
} else {
flag = 0; }
…
if (flag) {
close(); }
9
The naive analysis (1/2)
• The lattice models the status of the file:
L = (2{open,closed},)
{open,closed}
• For every CFG node, v, we have a constraint variable ⟦v⟧ denoting the status after v
• JOIN(v) = ⋃ ⟦w⟧ wpred(v)
{open}
{closed}
10
The naive analysis (2/2)
• Constraintsforinterestingstatements: ⟦entry⟧ = {closed}
⟦open()⟧ = {open} ⟦close()⟧ = {closed}
• For all other CFG nodes: ⟦v⟧ = JOIN(v)
• Before the close() statement the analysis concludes that the file is {open,closed}
if (condition) { open();
flag = 1;
} else {
flag = 0; }
…
if (flag) {
close(); }
11
The slightly less naive analysis
• We obviously need to keep track of the flag variable
• Oursecondattemptisthelattice:
L = (2{open,closed}2{flag=0,flag0},)
• Additionally, we add assert(…) to model conditionals
• Even so, we still only know that the file is {open,closed} and that flag is {flag=0,flag0}
if (condition) { open();
flag = 1;
} else {
flag = 0; }
…
if (flag) {
close(); }
12
Enhanced program
if (condition) {
assert(condition);
open();
flag = 1;
} else {
assert(!condition);
flag = 0; }
…
if (flag) {
assert(flag);
close(); } else {
assert(!flag);
}
13
Relational analysis
• Weneedananalysisthatkeepstrackofrelations between variables
• Oneapproachistomaintainmultipleabstractstates per program point, one for each path context
• Forthefileexampleweneedthelattice:
L = Paths 2{open,closed} (note: isomorphic to 2Paths{open,closed})
where Paths = {flag=0,flag0} is the set of path contexts
14
Relational constraints (1/2)
• For the file statements: ⟦entry⟧ = p.{closed}
⟦open()⟧ = p.{open} ⟦closed()⟧ = p.{closed}
• Forflagassignments:
⟦flag = 0⟧ = [flag=0⋃ JOIN(v)(p), flag0]
pP
⟦flag = n⟧ = [flag0⋃ JOIN(v)(p), flag=0]
pP
⟦flag = E⟧ = q. ⋃ JOIN(v)(p) pP
for any other E
where n is a non-0 constant number
”infeasible”
15
Relational constraints (2/2)
• Forassertstatements:
⟦assert(flag)⟧ = [flag0JOIN(v)(flag0), flag=0]
⟦assert(!flag)⟧ = [flag=0JOIN(v)(flag=0), flag0]
• For all other CFG nodes:
⟦v⟧ = JOIN(v) = p. ⋃ ⟦w⟧(p) wpred(v)
16
Generated constraints
⟦entry⟧ = p.{closed}
⟦condition⟧ = ⟦entry⟧
⟦assert(condition)⟧ = ⟦condition⟧
⟦open()⟧ = p.{open}
⟦flag = 1⟧ = [flag0⋃ ⟦open()⟧(p), flag=0]
⟦assert(!condition)⟧ = ⟦condition⟧
cC
⟦flag = 0⟧ = [flag=0⋃ ⟦assert(!condition)⟧(p), flag0]
cC
⟦…⟧ = p.(⟦flag = 1⟧(p) ⋃ ⟦flag = 0⟧(p))
⟦flag⟧ = ⟦…⟧
⟦assert(flag)⟧ = ⟦flag0⟦flag⟧(flag0), flag=0] ⟦close()⟧ = p.{closed}
⟦assert(!flag)⟧ = [flag=0⟦flag⟧(flag=0), flag0] ⟦exit⟧ = p.(⟦close()⟧(p) ⋃ ⟦assert(!flag)⟧(p))
17
Minimal solution
We now know the file is open before close()
flag = 0 flag 0
⟦entry⟧
{closed}
{closed}
⟦condition⟧
{closed}
{closed}
⟦assert(condition)⟧
{closed}
{closed}
⟦open()⟧
{open}
{open}
⟦flag = 1⟧
{open}
⟦assert(!condition)⟧
{closed}
{closed}
⟦flag = 0⟧
{closed}
⟦…⟧
{closed}
{open}
⟦flag⟧
{closed}
{open}
⟦assert(flag)⟧
{open}
⟦close()⟧
{closed}
{closed}
⟦assert(!flag)⟧
{closed}
⟦exit⟧
{closed}
{closed}
18
Challenges
• ThestaticanalysisdesignermustchoosePaths
– often as boolean combinations of predicates from conditionals
– iterative refinement (e.g. counter-example guided abstraction refinement) can be used for gradually finding relevant predicates
• Exponentialblow-up:
– for k predicates, we have 2k different contexts – redundancy often cuts this down
• Reasoningaboutassert:
– how to update the lattice elements with sufficient precision? – possibly involves heavy-weight theorem proving
19
Improvements
• Runauxiliaryanalysesfirst,forexample: – constant propagation
– sign analysis
will help in handling flag assignments
• Deadcodepropagation,change ⟦open()⟧ = p.{open}
into the still sound but more precise
⟦open()⟧ = p.if JOIN(v)(p)= then else {open}
20