Practical Verification with Abstract Interpretation
Verification techniques, such as contracts and code contracts, are explored in practical applications. The use of abstract interpretation and related concepts is discussed along with examples and challenges. The benefits of using contracts in programming languages are highlighted, emphasizing the importance of specifying preconditions, postconditions, and object invariants to improve code reliability and quality.
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.
E N D
Presentation Transcript
Practical verification with abstract interpretation Francesco Logozzo Joint work with Manuel Fahndrich http://research.microsoft.com/contracts
Exercise: Specify Abs(int x) public int Abs(int x) { if (x < 0) return -x; else return x; } Little reminder: -(-231)== -231 Precondition? Postcondition?
Specifications via Contracts Precondition What I expect from the caller? e.g. A non-null parameter Postcondition What I ensure to the caller? e.g. The returned value is non-negative Object Invariant What holds in the stable states of an object? e.g. This field is non-null
Contracts Not a new idea Eiffel, JML, Spec# General consensus on their usefulness Even in dynamic languages communities! However, not mainstream (yet). Why??? Two main problems Require changes to the build environment New compiler/language/ Static checking either absent or to painful to use Over-specification
CodeContracts Idea: Use code to specify code public int Abs(int x) { Contract.Requires(x != Int32.MinValue); Contract.Ensures(Contract.Result<int>() >= 0); if (x < 0) return -x; else return x; }
CodeContracts Pragmatic solution to the two problems The Contract Language is a .NET Library No changes in/of the compiler Transparently use C#, VB, F#, Delphi Leverage IDE support Intellisense, type checking The static checker Abs. Interpretation based Infer loop invariants Fine tuning of the algorithms Focuses on the properties of interest Predictable!!!!
CCCheck (aka Clousot) Goal: Prove contracts at static time Abstract interpretation-based Loop invariants inference Tunable Focuses on properties of interest Different from usual WP-based provers Optimistic hypotheses for aliasing Conservative otherwise
Clousot main loop For each assembly, class, method Collect the proof obligations What should I prove? Run the analyses Discover facts about the program Discharge the proof obligations Using the inferred facts On failure, use a more refined analysis Otherwise, report warning
Proof obligations Implicit NonNull checking Bounds checking Divisions by zero, overflows, float comparisons Explicit Assertions When calling a method, its precondition When returning from a method its postcondition its object invariant
Analysis steps Read the bytecode, extract contracts Program transformations: De-Stack CFG Construction De-heap Expression recovery Value Analyses Non-null, numerical, containers, buffers Checking Inference propagation
Why Analyzing Bytecode? Stable, standard format Languages change, bytecode does not C# 2.0 -> C# 3.0 -> C# 4.0 Analyze one instead of many C#, VB, Managed C++, F#, Delphi, Oxygen Leverage the compiler work Type inference, generics Main Drawback: Structure lost Should Reconstruct it!
Base Analysis Stack Expression Reconstruction Heap Analysis Destac k
Heap abstraction public class Alias { int x; public class Alias { public void Foo(bool b) { int svX = -11; assume (b) { svX = 10; } assert (svX >= -20); } } public void Foo(bool b) { Contract.Ensures(tmp.x >= -20); Alias tmp = new Alias(); tmp.x = -11; Alias alias = tmp; if(b) { alias.x = 10; } } } Output: program in scalar form Optimistic assumptions on external aliasing
Value Analyses Built on the top of the stack Non-Null Is this object valid? Numerical Ranges and linear restraints over variables Arrays Compound structure values Enums Which enum values are legal?
Intervals public class Alias { public void Foo(int f, int max) { int x = 0; Infer x [0, +oo] while (x < max) { x++; } No overflow! Contract.Assert(x >= -20); } } Check: Ok!
DisIntervals Disjunctions of intervals public enum ItalianBikeBrand { DeRosa=0, Colnago=2, Pinarello=4, Daccordi=6 } public string CityFor(ItalianBikeBrand bike) { switch(bike) { case ItalianBikeBrand.DeRosa: return "Milan"; case ItalianBikeBrand.Daccordi: return "Pisa"; case ItalianBikeBrand.Pinarello: return "Treviso"; case ItalianBikeBrand.Colnago: return "Milan"; default: Contract.Assert(false); // Should prove unreachable return null; } } DisIntervals infer [- ,-1] [1,1] [3,3] [5,5] [7, + ] Admissible values [0,0] [2,2] [4,4] [6,6] Check:
Basic Numerical domain Reduced product of DisIntervals x [a0, b0] [a1, b1] [an, bn] LT x < { y0, y1, y2 } Leq x { y0, y1, y2 } Linear Equalities a0 x0+ + an xn= b Main advantage: It s fast! Most operations are linear
Example of reduction Intervals infer x [-1, -1] y [100, + ] public static void F() { int x = 5, y = 100; while (x >= 0) { x = x - 1; y = y + 10; } Contract.Assert(y == 160); } Linear equalities 10 * x + y == 150 Check: ok!
SubPolyhedra Often we need the full linear inequalities Polyhedra do not scale up (we tried them) public void Count(int[] values) { int neg = 0, pos = 0, j= 0; foreach (var x in values) { if (x < 0) { neg++; j++; } else if (x > 0) { pos++; j++; } } Contract.Assert(neg + pos == j); Contract.Assert(neg + pos <= values.Length); } Proven by Linear equalities Proven by SubPolyhedra
SubPolyhedra (with V. Laviron) As expressive as Polyhedra Full linear inequalities No templates! Give up some of the inference power Idea: aixi b aixi= [- , b] Combination of Linear Equalities and Intervals Challenge: Join The point wise join is too imprecise Scales up to hundreds of variables
Join algorithm : SubPolyhedra Uniform slack variables Reduce the states Do the pair-wise join Recover precision using hints Deleted equalities Templates 2D Convex Hull Annotations
Example : Join Step 1 Entry State: s0: x - y == , [- , 0] s1: T, x [0,0] y [1,1] Step 1 (uniform slack variables) s 0: x - y == , [- , 0] s 1: x - y == , x [0,0] y [1,1]
Example: Join steps 2-3 Step 2 (Reduction) s 0: x - y == , [- , 0] s 1: x - y == , x [0,0] y [1,1] [-1,-1] Step 3 (Pair-wise join) s2: x - y == , [- , 0]
Example: Join Step 4 Recover lost relations assume x == y x = 0; y = 1 x - y == 0, T T, x [0,0] y [1,1] T, T x - y == , [-1, 0] assert x<= y
Critical operation: Reduction Infer tightest bounds Instance of a Linear programming problem Solution in polynomial time But may still be too expensive We have implemented Simplex Theoretically complete Rounding problems Basis exploration Incomplete No rounding problems
SubPolyhedra: a family of domains Reduction algorithm, . . 2D Convex hull Exact Simplex Semantic hints Simplex with floats Die-Hard Basis exploration No Hint Hints for Join/Widening
Incremental analysis in Clousot First analyze with cheap domains If check is definitive (True, False, Bottom) Done! Otherwise Try a more precise domain On average great performance gains Abstract Domain AD1 Abstract Domain AD2 Abstract Domain AD3
Array Content analysis Needed to prove quantified facts Extensions to enumerators Challenge 1: Effective handling of disjunction public void Init(int N) { Contract.Requires(N > 0); int[] a = new int[N]; int i = 0; If i == 0 then a not initialized else if i > 0 a[0] == a[i] == 222 else impossible while (i < N) { a[i] = 222; i = i + 1; } Challenge 2: Infer all the elements initialized Contract.Assert( k [0, N). a[k] == 222); }
Not the firsts Many approaches using: Human help Under- and over-approximations Templates Theorem provers Model checking We tried some of them in Clousot but not practical Many hidden hypotheses Scalability is an issue
Our idea (with P&R Cousot) Precise and very very fast! More in the POPL 11 Talk & Paper Segment bounds Disjunction Uniform content abstraction 0 [222, 222] i, k ? [0, 0] N 0 i, 0 k i == k i < N, k < N
Inter-method Inference By default, infer getter/setter ensures Reduce the initial annotation burden Do not propagate over assemblies Suggest immediate preconditions public static int[] Factory(int len) { return new int[len]; } Talk @ VMCAI on Tuesday
Caching (with J.-H. Jourdan) Idea: Hash the annotated program Persist output of the analyzer Challenges Caching of Metadata Inheritance, enums, templates Inferred expressions Be conservative Calls to Enum.IsDefined( ) Semantics given via reflection
Warning scoring For each warning, compute a Semantic score Use info from the abstract domains the syntactic algorithm of FindBugs Have thresholds for masking warnings Low, Medium, Hi Found tenth of bugs with Low In production, well-tested code Use scoring to sort warnings
Further Goal direct backward propagation Timeouts The analysis of a method can take too much Message suppression Weakness of the checker? Of the analysis? Selective Verification Start by focusing on most core code
CodeContracts Impact Product Details API in .NET 4.0 Externally available ~14 months >30,000 downloads, very active forum 3 book chapters on CodeContracts Many dozens of blog articles Publications, talks, lectures POPL, ECOOP, OOPSLA, VMCAI, APLAS, SAS, SAC, FoVeOOS Internal usage Integrated into CLR build A few groups Product Details Product Details
Conclusions & Next CCCheck externally available Bing for CodeContracts MSDN Tenths of Thousands of downloads Or try it at http://pexforfun.com/absverified Abstract interpretation-based Automatic Inference: loop invariants, pre/post/invariants Tunable, predicatable Dogfood: Run on itself at each build
Thanks!!!! To the Chairs & VMCAI PC for inviting me To our colleagues M. Barnett, H. Venter & RiSE To the visitors and interns P. & R. Cousot P. Ferrara, V. Laviron, M. Peron, M. Monereau, J.- H. Jourdan To the hundreds of users in the forum To push us to make CCCheck better!
Next Re-architecture to integrate with Z3 To leverage the decision procedures in Z3 To share code E-graph, etc. To improve reasoning on implications Note: from WP-based provers No blind axiomatization Clousot is still in control, uses Z3 as oracle
