Abstract Domains and Numeric Semantics Overview

Concepts of abstract domains, numeric semantics, arithmetic expressions, and operational semantics in the context of program analysis and verification. Covering inductive invariants, array bounds, termination analysis, and pointer arithmetic. Includes concrete operational semantics examples and details on semantics of expressions and commands.

• Abstract Domains
• Numeric Semantics
• Program Analysis
• Semantics
• Verification

ehack Follow

Uploaded on Feb 26, 2025 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. Numeric Abstract Domains Mooly Sagiv http://www.cs.tau.ac.il/~msagiv/courses/pa16.html Tel Aviv University 640-6706 Adapted from Antoine Mine 1

2. Subjects

3. Goals Infer inductive invariants on numeric values Abstract sets of points in P(Rn) Applications: Array bound Termination infer ranking functions with value in N Cost Analysis time, memory consumption are numeric quantities Pointer analysis with pointer arithmetic pointer offest String analysis in C Length, index

4. Numeric Semantics

5. Arithmetic Expressions & Commands V Var| <exp> ::= V | - <exp> | <exp> op <exp> | [c, c ] <com> ::= V := <exp> | assume <exp> relop 0 | assert <exp> relop 0 op {+, -, , /}| c, c R {- , } V Var relop {=, , <,>, , } Control Flow Graph G(N, E, s) where E N N is annotated with commands s N is the start node

6. Example Program 1 1: X := [1, 10] ; X := [1, 10] 2: Y := 100; 2 while 3: X>= 0 do { Y := [100, 100] 4: X := X 1; assume X<0 3 6 5: Y := Y + 10 assume X 0 } Y := Y +10 4 6: X := X -1 5

7. Concrete Operational Semantics

8. Semantics of Expressions States = Var R Semantics E E V = V E c, c = { x R | c x c } E -<exp> = { - x | x E <exp> } E <exp> op <exp > ={x op x | x E <exp> , : <exp> R x E <exp > } op {+, -, } E <exp> / <exp > =

9. Semantics of Commands States = Var R Semantics C C V := <exp> Z = { [V x] | Z, : <com> P( ) P( ) x E <exp> } C assume <exp> relop 0 Z ={ | Z, x E <exp> : x relop 0 } C assert <exp> relop 0 Z

10. Distributivity C exp is distributive C exp ( Z) = ZC exp { }

11. Concrete Semantics of Programs G(s, N, E) : P( ) N P( ) The set of reachable states D = <P( ), , , , , ) The smallest simultaneous solution to the set of equations G(s, N, E) CSs= CSn= <m, c, n> E C c CSm s n Uniquely defined from Tarski s theorem but not computable

12. Numeric Abstract Domains Representation: a set D#of representable abstract values <D#, relating the amount of information given by abstract values A concretization function : D# D = P( ) = P(Var R) Required algebraic properties: need to be monotonic: d # d d # d Strictness need not be one-to-one #, #, #, #, #) # = #= Var R

13. Numeric Abstract Domain Examples y y y y x x x x signs intervals octagons polyhedra x 0 x [a, b] x y c aixi c

14. Requirements on abstract operators Algorithmic requirements For each c <cmd>, c#c : D# D#is computable Algorithm for # Used for merging control paths and iterations Algorithm for Used for assume Algorithm for # Used for checking termination

15. Abstract Semantics of Programs G(s, N, E) : D# N D# The set of reachable abstract states D#= <D#, The smallest simultaneous solution to the set of equations G(s, N, E) ASs= # ASn= #<m, c, n> E C# c ASm s #, #, #, #, #) # # n Uniquely defined from Tarski s theorem

16. Soundness The smallest simultaneous solution to the set of equations G(s, N, E) CS CSs= CSn= <m, c, n> E C c CSm n s Any solution AS set of equations G(s, N, E)# # ASs= # ASn= #<m, c, n> E C# c ASm n s CSn ASnfor all n N

17. Soundness requirement # For each c <cmd>, d D#, c c ( d) (c# c d) command c C c Set of states Set of states Set of states command c D# D# C#c

18. Optimality (induced operation) Requires existence of abstraction : D D#such that < , > form a Galois connection Define c c#= d. (c c ( d) may not exist c c# may be hard to compute

19. Widening Accelerate the termination of Chaotic iterations by computing a more conservative solution Can handle lattices of infinite heights : D# D# D# such that d #d d d For every increasing chain d#1 The sequence s0 = d#0and si+1= si d#iis finite d#2 ,

20. Chaotic Iterations with widening for each n in N do AS[v] := # AS[s] = # WL = {s} while (WL ) do select and remove an element m WL for each n, such that. (m, c, n) E do temp = c c#AS[m] if m is a loop header then new := AS(n) temp else new := AS(n) #temp if (new AS[n]) then AS[n] := new; WL := WL {n}

21. Non-Relational Abstractions

22. Cartezian Abstraction (independent attribute) Forget the relationship between variables

23. Example Program 1 X := [1, 10] 2 Y := [100, 100] assume X<0 3 assume X 0 Y := Y +10 4 X := X -1 5

24. The Interval Domain

25. The Interval Domain [Moore66, Cousot 76] D#= {[a, b] | a b R or a=- or b= } #= [- , ] d # d = if d = #then d else if d = #then d else let d=[a, b] and d =[c, d] in [min(a, c), max(b, d)] d # d = if d = #then # else if d = #then # else let d=[a, b] and d =[c, d] in let l = max(a, c) and u= min(b, d) if l > u then # else [l, u] d d = if d = #then d else else let d=[a, b] and d =[c, d] in [if a c then a else - , if b d then b else ] #

26. Galois Connection

27. Abstract Expressions

28. Abstract Assignments

29. Optimality (Induced)

30. Abstract Assume

31. Example Program 1 X := 0 assume X 40 2 assume X<40 X := X+1 3

32. Relational Domains

33. The need for relational domains Non-relation domains cannot represent variable relationships Y :=0; X: input signal Y: output signal S: last output R: Y-S D: max allowed for |R| while true do { X:=[-128,128]; D:=[0,16]; S:=Y; Y:=X; R:=X-S; if R<=-D then Y:=S-D fi; if R>=D then Y:=S+D fi }

34. The need for relational domains Infer strong enough inductive invariants X:=0; I:=1; while I<5000 do { if then X:=X+1 else X:=X-1 fi; I:=I+1 }

35. The need for relational domains Modular analysis of procedures Z :=X ; if Y > Z then Z :=Y ; if Z < 0 then Z :=0;

36. Weakly Relational Domains

37. The Zone Domain [Shacham00, Mine01] Constrains of the form Vi Vj c Vi c

38. Machine Representation A potential constraint has the form Vi Vj c Represented as a directed graph G Nodes are labeled with variables An arc with weight c from Vi to Vjfor each constraint Vi Vj c Difference Bound Matrix (DBM) Adjacency matrix m of G mij = c < Vi Vj c mij = No such constraints Concretization

39. Machine Representation (cont) Unary constraints Add another variable V0 m has size n+1 n+1 Vi c is denoted as Vi-V0 c, i.e., mi,0= c Vi c is denoted as V0- Vi -c, i.e., m0,i= -c m = { (v1, v2, , vn) | (0, v1, v2, , vn) m} V0 + -1 -1 V1 4 + 1 V2 3 + + V0 V1 V2

40. The DBM Lattice

41. Relational Domains

42. The Polyhedra Domain [CH78] i j ai, jxi, j ci

43. Summary Numerical Domains are Powerful Infer interesting invariants Cost is an issue Need to combine with other domains Next week some applications