Transcript Presentation (PowerPoint File)

SAT-based methods for proving
properties in Reynolds/O'Hearn
Separation Logic
Daniel Kröning
(currently visiting CBL)
Joint work with B. Cook and J. Berdine
10.8.2006
Program Verification
 Goal:
Editor that highlights programming errors
 Not syntax, but semantics
10.8.2006
Daniel Kroening
2
Like what?
10.8.2006
Daniel Kroening
3
Verification Engines
Unwinding
Abstraction
 Bounded Model
Checking (BMC)
 Abstract interpretation
 Predicate abstraction
 No invariant discovery
 Attempting
invariant discovery
 One very large
constraint problem
 Many small constraint
problems
 A lot of case-splitting
 Little case-splitting
10.8.2006
Daniel Kroening
4
Program Analysis: BMC
Progra
m
BMC
CBMC, …
Model
VC
CONSTRAINT SOLVER
SAT solver,
CVC-Lite, Math-SAT, …
10.8.2006
Daniel Kroening
5
BMC Overview
ANSI-C
Program
=
=
parsing
*
*
+

unwind

CNF
SAT
Solver
Constraint
Problem
Parse tree
10.8.2006
+
Daniel Kroening
6
ANSI-C Transformation
1. Preparation



Side effect removal
continue, break replaced by goto
for, do while replaced by while
2. Unwinding


10.8.2006
Loops are unwound
Same for backward goto jumps and
recursive functions
Daniel Kroening
7
Implementation
3. Transformation into Equation

After unwinding: Transform into SSA
Example:

Generate constraints by simply conjoining
equations resulting from assignments

For arrays, use simple lambda notation
10.8.2006
Daniel Kroening
8
Example
10.8.2006
Daniel Kroening
9
Required Theories
 Bit vector 
 Arrays 
 Pointers (pair of object/offset) 
 Floating Point

 If contained in assertion:


10.8.2006
Quantifiers
Data type predicates (lists, trees, …)
Daniel Kroening


10
Example
int *p, x, y;
cbmc test.c –cvc –outfile test
int main() {
int z;
y=z;
p=&y;
x=*p;
assert(x==z);
}
10.8.2006
Daniel Kroening
11
p0: [# object: INT, offset: BITVECTOR(32) #] =
(# object:=0, offset:=0bin00000000000000000000000000000000 #);
x0: BITVECTOR(32) = 0bin00000000000000000000000000000000;
y0: BITVECTOR(32) = 0bin00000000000000000000000000000000;
z1: BITVECTOR(32);
z0: BITVECTOR(32);
y1: BITVECTOR(32) = z0;
p1: [# object: INT, offset: BITVECTOR(32) #] =
(# object:=3, offset:=0bin00000000000000000000000000000000 #);
x1: BITVECTOR(32) = y1;
l1: BOOLEAN;
ASSERT l1 <=> (x1=z0);
ASSERT (NOT l1);
QUERY FALSE;
10.8.2006
 Download me!
 We have ~300 MB of
benchmark files available
 Soon: SMT-Lib format
Daniel Kroening
12
Program Analysis: Abstraction
Progra
m
PROGRAM ANALYSIS
ENGINE
VCs
, T
Model
CONSTRAINT SOLVER
’
WIDENING
Simplify,
Zapato,
Cogent,
CPLEX, …
10.8.2006
SLAM, …
Pre-, Post-,
Proof-based, …
Daniel Kroening
13
Existing Tools
 Implement
 Fragments
 Maybe
arrays, maybe pointers
 Sometimes
10.8.2006
of linear arithmetic,
float
Daniel Kroening
14
Extending the Assertion Logic
Progra
m
PROGRAM ANALYSIS
ENGINE
VCCs
, T
Model
’
CONSTRAINT SOLVER
WIDENING
Linear Arithmetic,
Arrays, Float, …
Linear Arithmetic,
Arrays, Float, …
10.8.2006
Daniel Kroening
15
Existing Tools
 Biggest challenge for mass-market:
dynamic data structures
 Fix with choice of assertion logic, e.g.,
Reynolds’ Separation Logic
 E.g., add separating conjunction and
predicates for linked list
10.8.2006
Daniel Kroening
16
Separation Logic
 A logic for heap data structures
 NOT the same as the fragment of linear
arithmetic called difference logic
 Due to Reynolds/O’Hearn
10.8.2006
Daniel Kroening
17
Separation Logic
“next” pointer
0
.
.
.
…
…
.
Main problem:
Payload
10.8.2006
Need to specify that all
heap cells are disjoint
Daniel Kroening
18
Separation Logic
 In general, one needs to express constraints
that a data structure does not share cells
with any other data structure
 Key idea: new logical operator
P*Q
“Separating Conjunction”
10.8.2006
Daniel Kroening
19
Separation Logic
 Semantics of expressions defined over
valuations of heaps
(maps from addresses to values)
 Obvious meaning for
State
10.8.2006
Heap
Pointer
Daniel Kroening
Value
20
Separation Logic
 Define disjoint heaps:
 Separating conjunction:
10.8.2006
Daniel Kroening
21
Separation Logic: Lists
 Notation for sequences

: empty sequence

x¢: concatenation
 Define list:
10.8.2006
Daniel Kroening
22
Extending the Assertion Logic
Progra
m
PROGRAM ANALYSIS
ENGINE
VCCs
, T
Model
’
CONSTRAINT SOLVER
WIDENING
Linear Arithmetic,
Arrays, Float, …
+Separation Logic
Linear Arithmetic,
Arrays, Float, …
+Separation Logic
10.8.2006
Daniel Kroening
23
Who does the assertions?
 Manual annotations
 Automatic discovery
 Standard Template Library

Data in containers is implicitly
in separate heap cells
typedef std::hash_map
<std::string, symbolt, string_hash> symbolst;
...
typedef std::vector<nodet> nodest;
10.8.2006
Daniel Kroening
24
Requirements for Constraint Solvers
 Constraint solver must support
very rich logic
 Data types might even be application-specific
 But most queries are simple!
 Extending custom-made constraint solver
is tedious
10.8.2006
Daniel Kroening
25
Proposed Solution
 Assumption: we have a (partial)
axiomatization of all logics
 Goal: high performance constraint solver
1st step: define language for axioms
10.8.2006
Daniel Kroening
26
Example: Equality Logic
equality_transitivity:
A "=" B, B "=" C -> A "=" C;
equality_commutativity:
A "=" B <-> B "=" A;
equality:
A "=" A;
disequality:
A "!=" B <-> NOT A "=" B;
10.8.2006
Daniel Kroening
27
Build a Compiler!
2nd step: build a compiler
VCC
Axioms
10.8.2006
codegen
C++
code
g++
Daniel Kroening
Binary
SAT/UNSAT
28
Multiple Theories
 Note that one can combine multiple theories
 Interfacing through arbitrary propositions,
not just equalities
 Convexity requirement?
10.8.2006
Daniel Kroening
29
What about OR?
 We could build case-splitting into the
generated code
 However, we will never be able to implement

Proper decision heuristics

Non-chronological back-tracking

Learning
10.8.2006
Daniel Kroening
30
What about OR?
 Alternative: produce
reduction to propositional logic
 Generate CNF, and pass formula to SAT
solver
 The formula is unsatisfiable iff there exists a
deduction that shows a contradiction
10.8.2006
Daniel Kroening
31
What about OR?
3nd step: add SAT solver
VCC
Axioms
codegen
C++
code
g++
Binary CNF
SAT
Solver
This is the eager version – lazy version straight-forward.
10.8.2006
Daniel Kroening
32
What about OR?
1. Maintain truth value with
each fact:
2. Set new facts to unknown
3. Assign a literal to each fact
that has truth value unknown
4. For each deduction step,
generate constraint
10.8.2006
Daniel Kroening
33
Separation Logic
disjoint_not_self:
h “!=“ “emp” -> not [h "#“ h];
and:
h "|=" [P "^" Q] <-> h "|=" P, h "|=" Q;
not:
h "|=" ["!" P] <-> not [h "|=" P];
conditional:
h "|=" [P "?" Q ":" R] <->
(h "|=" P -> h "|=" Q), (h "|=" "!" P -> h "|=" R);
10.8.2006
Daniel Kroening
34
Separation Logic
star:
h "|=" [P "*" Q] <->
NEW h0 "|=" P, NEW h1 "|=" Q,
h "=" [NEW h0 "**" NEW h1],
NEW h0 "#" NEW h1;
10.8.2006
Daniel Kroening
35
Obtaining Invariants
 Again, could be custom-made
 Instead: inspect proofs of failed
refutation-attempts

Paper available on doing this for bit-vectors

E.g., for constructing interpolants
10.8.2006
Daniel Kroening
36
Conclusion
 Generic constraint solver with propositional
SAT as backend
 Especially for complicated logics
 Extensions of logic are easy
 All case-splitting is pushed into
propositional SAT solver
10.8.2006
Daniel Kroening
37
Cross-Advertising
 TACAS: this can be used for
–quantification over predicates
 CAV: Predicate abstraction for deep loops
 PDPAR: Completeness

10.8.2006
How to tell for sure that no proof exists?
Daniel Kroening
38