Transcript slides

Regression-Verification
Benny Godlin
Ofer Strichman
Technion
1
The goal of Regression Verification

The goal: formally verify the equivalence of two similar
programs.

Pros:


Does not require formal specification.
Computationally easier than functional verification


Ideally, the complexity should depend on the semantic
difference between the programs, and not on their size.
Cons:

Defines a weaker notion of correctness.
2
Previous work

In the theorem-proving world (mostly @ ACL2 community):



Not dealing with realistic programs / realistic programming
languages
Not utilizing the equivalence of most of the code for simplifying
the computational challenge
Industrial / realistic programs:

Code free of: loops, recursion, dynamic-memory allocation
 microcode @ Intel,
 embedded code @ Feng & Hu,
 symbolic simulation @ Matsumoto et al.
3
Our notion of equivalence
Partial equivalence


Executions of P1 and P2 on equal inputs

…which terminate,

result in equal outputs.
Undecidable
4
Partial equivalence

Consider the call graphs:


A
B
Side 1
Side 2
… where A,B have:
 same prototype
 no loops
Prove partial equivalence of A, B

How shall we handle the recursion ?
5
Hoare’s Rule for Recursion
Let A be a recursive function.
“… The solution... is simple and dramatic: to permit the use of the
desired conclusion as a hypothesis in the proof of the body itself.” [H’71]
6
Hoare’s Rule for Recursion
// {p}
A( . . . )
{
. . .
// {p}
call A(. . .);
// {q}
. . .
}
// {q}
7
Rule 1: Proving partial equivalence
//in[A]
A( . . . )
{
. . .
//in[call A]
call A(. . .);
//out[call A]
. . .
}
//out[A]
A
//in[B]
B( . . . )
{
. . .
// in[call B]
call B(. . .);
//out[call B]
. . .
}
//out[B]
B
8
Rule 1: Proving partial equivalence


Q: How can a verification condition for the premise look like?
A: Replace the recursive calls with calls to functions that



over-approximate A, B, and
are partially equivalent by construction
Natural candidates: Uninterpreted Functions
9
Proving partial equivalence



Let A,B be recursive functions as defined earlier
Let AUF , BUF be A,B, after replacing the recursive call with a
call to (the same) uninterpreted function.
We can now rewrite the rule:
The premise is
Decidable
10
Using (PART-EQ-1): example
unsigned gcd1UF
(unsigned a, unsigned b)
b)
{ unsigned g;
if (b == 0)
g = a;
else {
a = a % b;
g = gcd1(b,
a);
U
}
return g;
}
unsigned gcd2UF
(unsigned x, unsigned y)
{ unsigned z;
z = x;
if (y > 0)
z = gcd2(y,
z % y);
U
}
return z;
z;
}
?
=
Transitions:
Tgcd1
Tgcd2
Inputs:
a,b
x,y
outputs:
g
z
11
Rule 1: example
side 1
side 2
Transition functions
Tgcd1
Tgcd2
Inputs
a,b
x,y
Outputs
g
z
Equal
inputs
Equal
outputs
12
Partial equivalence: Generalization

Assume:



no loops;
1-1 mapping map between the recursive functions of both sides
 Mapped functions have the same prototype
Define:

For a function f, UF(f) is an uninterpreted function such that
 f and UF(f) have the same prototype

(f,g) 2 map , UF(f) = UF(g).
13
Partial equivalence: Generalization

Definition:
is called in A]
14
Partial equivalence: Example
{(g,g’),(f,f’)} 2 map
g
g’
f
f’
Side 2
Side 1
Need to prove:
UF
f
=
UF
f’
Notation:
Call to UF
g
UF
=
g’
UF
15
Partial equivalence: Example
{(g,g’),(f,f’)} 2 map
g
g’
f
f’
Side 2
Side 1
Need to prove:
g
f
=
g’
f’
Notation:
Call to UF
g
f
=
g’
f’
16
Partial equivalence: extensions
h’
g
f
Side 1
Side 2
Find a subset S of the mapped pairs that intersect all cycles in
both sides



f’
X
X

g’
S = {(g,g’)}
Replace calls to S functions with calls to uninterpreted functions.
Inline the rest
Prove equivalence of S pairs.
17
Partial equivalence: extensions
h’
g
f
g’
f’
X
X
X
X
Side 2
Side 1
g
S = {(g,g’)}
S = {(g,g’),(f,f’)}
f
g’
f’
h’
g
f
g’
f’
18
Partial equivalence: extensions

Recall: S is a set of pairs of function

Let mS denote the set of functions that appear in an S pair.

Let
is called in A]
19
Partial equivalence: bottom-up
g
h
f
g’
f’
h’
Connected SCCs are proved bottom-up

Abstract partially-equivalent functions with uninterpreted
functions

Inline
20
PART-EQ: Soundness

Proved soundness for a simple programming language (LPL)


Covers most features of modern imperative languages
…but does not allow
 call by reference, and
 address manipulation.
21
What (PART-EQ) cannot prove...
returns n + nondet()
returns n + n -1 + nondet()
22
What (PART-EQ) cannot prove...
when n == 1 :
returns 1

returns 1 + nondet()
Many of these problems can be solved with unrolling +
function summaries
23
Decomposition algorithm (with SCCs)
Legend:
Equivalent pair
Equivalence undecided yet
Could not prove equivalent
Syntactically equivalent pair
Equivalent if MSCC
A:
CBMC
B:
f1()
f2() U
U f3()
f1’()
f2’()
U
U f5()
U f4()
f6()
U
U f3’()
U f5’()
U f4’()
f6’()
24
25