Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems Johannes Späth, Karim Ali, Eric Bodden 30. 10. 2020 1 / 18 Abstract precise static analyses are context-, flow-, and field-sensitive k-limited access path, access graph do not scale well on recursive data structures context- and field- sensitivity both expressible as CFL reachability problems introducing synchronized push-down system (SPDS) field-sensitive flow-sensitive context-sensitive 2 / 18 Outline data-flow analysis and its properties pushdown systems call-PDS field-PDS SPDS 3 / 18 Data-flow analysis static analysis for each program point: set of computed values flow functions give semantics of instructions join function combines values from multiple predecessors 4 / 18 Data-flow analysis: a simple approach p q · · · i kj · · · Figure: Control flow graph fragment 5 / 18 Data-flow analysis: a simple approach p q · · · i kj · · · Figure: Control flow graph fragment outi = flowi (join(outp, outq, · · · )) 5 / 18 Properties of data-flow analysis Flow-sensitivity control flow paths Context-sensitivity call contexts Field-sensitivity fields of the same object 6 / 18 Push-down systems A push-down system is a triple P = (P, Γ, ∆) where: P: finite set called control locations Γ: finite set called stack alphabet ∆: finite set of rules Configuration is a pair p, w where p ∈ P, w ∈ Γ∗ 7 / 18 Rules ∆ is a set of rules in form: p, γ → p , w p, p ∈ P γ ∈ Γ w ∈ Γ∗ 8 / 18 Rules ∆ is a set of rules in form: p, γ → p , w Types of rules |w| = 0 pop rules |w| = 1 normal rules |w| = 2 push rules Rules with |w| > 2 can be subdivided into multiple push rules. 8 / 18 call-PDS flow-sensitive context-sensitive field-insensitive Intuition push rule ≈ call pop rule ≈ return normal rule ≈ assignment 9 / 18 Construction of call-PDS P = (V, S, ∆S) V: variables S: statements ∆S normal rules – intra-procedural data-flows push,pop rules – inter-procedural data-flows 10 / 18 Analysing call-PDS set of configurations reachable from given configuration where does the value flow? P-automaton AS accepts configuration of PDS start with trivial automaton post*-saturate the trivial automaton IA159 Formal verification methods 11 / 18 field-PDS flow-sensitive context-insensitive field-sensitive Intuition normal rule ≈ no modification, arguments, return push rule ≈ store into field pop rule ≈ load from field 12 / 18 Construction of field-PDS P = (V × S, F, ∆F) V: variables S: statements F: fields configuration x@s, f0 · f1 · · · · 13 / 18 Construction of field-PDS Example rules Push statement 36 | v.f = u rule u@35, ∗ → v@36, f · ∗ Pop statement 37 | x = w.f rule w@36, f → x@37, ε 14 / 18 SPDS Intuition we can compute context-sensitive dataflow we can compute field-sensitive dataflow combination: precise dataflow holds only if it holds in both cases 15 / 18 SPDS A little formally call-PDS configuration: x, s0 · s1 · · · field-PDS configuration: v@s, f0 · f1 · · · SPDS configuration: v · f0 · f1 · · · @ss1·s2··· 0 16 / 18 SPDS Reachability P-automatons AS (call-PDS) and AF (field-PDS) let AF S = (AS, AF) AF S accepts iff both accept 17 / 18 Undecidability context-sensitive data-dependence analysis is generally undecidable :( SPDS over-approximates the fully precise solution 18 / 18 Undecidability context-sensitive data-dependence analysis is generally undecidable :( SPDS over-approximates the fully precise solution what if the configuration is reachable via different CFG paths? let’s look at an example! 18 / 18