Lecture 11 Abstract Interpretation on Control-Flow Graphs

1 / 8

# Lecture 11 Abstract Interpretation on Control-Flow Graphs - PowerPoint PPT Presentation

Lecture 11 Abstract Interpretation on Control-Flow Graphs. Example. k=1; while(k &lt; 100) { k=k+3 }; assert(k &lt;= 255 ) k=1; loop {assume(k &lt; 100); k=k+3}; assume(k&gt;=100); assert(k &lt;= 255) r = {( k,k ’) | (k &lt; 100 /\ k’ = k + 3) } Approximating sp ({1},r*)

I am the owner, or an agent authorized to act on behalf of the owner, of the copyrighted work described.

## PowerPoint Slideshow about 'Lecture 11 Abstract Interpretation on Control-Flow Graphs' - ataret

Download Policy: Content on the Website is provided to you AS IS for your information and personal use and may not be sold / licensed / shared on other websites without getting consent from its author.While downloading, if for some reason you are not able to download a presentation, the publisher may have deleted the file from their server.

- - - - - - - - - - - - - - - - - - - - - - - - - - E N D - - - - - - - - - - - - - - - - - - - - - - - - - -
Presentation Transcript

### Lecture 11 Abstract Interpretation on Control-Flow Graphs

Example

k=1; while(k < 100) { k=k+3 }; assert(k <= 255)

k=1; loop {assume(k < 100); k=k+3}; assume(k>=100); assert(k <= 255)

r = {(k,k’) | (k < 100 /\ k’ = k + 3) }

Approximating sp({1},r*)

post(P) = {1} U sp(P,r) = {1} U {k+3|k  P, k < 100}

postn({}): {}, {1}, {1,4}, …, {1,…,97},{1,…,97,100}, {1,…,97,100}

Multiple variables

Wish to track an interval for each variable

We track not [L,U] but ([L1,U1],[L2,U2])

If program state is (x,y), define

(([L1,U1],[L2,U2])) = {(x,y) | }

(p) = ([L1,U1],[L2,U2]) L1 = U1 = L2 = U2 =

Product of Partial Orders

(Ai, ≤i) partial orders for iJ

(A, ≤) given by A = {f : J  UiJAi ,  i. f(i)Ai}

f,gA ordered by

f ≤ g   i. f(i)≤ig(i)

example: J={1,2}

Then (A, ≤) is a partial order. Morever:

If (Ai, ≤i) all have lub, then so does (A, ≤).

If (Ai, ≤i) all have glb, then so does (A, ≤).

Example: Counter and a Mode

mode = 1x =0while (-100 < x && x < 100) { if (mode == 1) { x = x + 10 mode = 2 } else { x = x - 1 mode = 1 }}

assert(1 <= mode && mode <= 2 && x <= 109)

Two Counters

x =0

y = 0while (x < 100) {

x = x + 1

y = y + 2}

assert(y <= 200)

Non-relational analysis: tracks each variable separately.

It often loses correlations between them.

Quantifier Elimination for Optimization

F – Presburger arithmetic formula

M = max x such that F(x,y)

David Monniaux: Automatic modular abstractions for linear constraints. POPL 2009: 140-151

Beyond One Loop
• Formulation of one-step relation for a CFG
• Deriving collecting semantics
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}