equivalence of program segments

I'm looking for references to articles/books which discuss the problem of
proving the equivalence of two segments of programs. Actually, my problem
deals with segments of assembly language, but I'm sure that results for
programs would help me too.


Actually, I have no problems with straight-line code--I just use symbolic
evaluation, simplification to canonical form, and matching. Now I'd like
to do segments containing branches and very simple loops. For segments
with branches, but no loops, I include a "condition" term in the symbolic
state and each trace through the code will have it's own state along with
the condition under which that trace will be executed. Loops cannot be
handled this way, since one gets an infinite number of state/conditions.
Has anyone proven that the state/conditions need only match (between the
two code segments that are being checked for equality) for a finite number
of traces? Perhaps some examples will make my problem more clear.


Straight-line code:


add r1,r2,r3 %% r3 is the destination register
st r3,(r4+8) %% r3 is stored to address (r4+8)
ld (r6-4),r9


symbolically reduces to:


cond/true,
r3/(r1+r2),
r9/mem(r6-4),
mem(r4+8)/(r1+r2).


Note that I'm ignoring, for time being, representing the ordering of
memory operations in the symbolic state.


Code with a conditional branch:


ld (r3+12),r4
btgeq 2,r4,label2 %% if (r4<31:28> == 2) branch to label2
%% annul next instruction if branch taken
add r4,8,r5
label1:
....
label2:
....


symbolically reduces to:


cond/(tag(mem(r3+12)) == 2),
pc/label2,
r4/mem(r3+12),
r5/r5


and


cond/(tag(mem(r3+12)) != 2),
pc/label1,
r4/mem(r3+12),
r5/(mem(r3+12)+8).


Note that tag(X) refers to the most significant four bits of X.


Finally, if we have an instruction with a simple loop in it:


dref r1 %% dereference the value in r1, that is,
%% if (tag(r1) == 1) {
%% tmp = r1;
%% r1 = mem(r1);
%% while (tmp != r1 && tag(r1) == 1) {
%% tmp = r1;
                                                %% r1 = mem(r1);
%% }
%% }
%% where tmp is a temporary (non-architectural) value


symbolically reduces to an infinite set of states, some of which are:


cond/(tag(r1) != 1)
r1/r1


and


cond/(((tag(r1) == 1) && (r1 == mem(r1))) ||
                            ((tag(r1) == 1) && (tag(mem(r1)) != 1))),
r1/mem(r1)


and


cond/(((tag(r1) == 1) && (tag(mem(r1)) == 1) && (r1 != mem(r1)) &&
                                                                (mem(r1) == mem(mem(r1)))) ||
((tag(r1) == 1) && (tag(mem(r1)) == 1) && (r1 != mem(r1)) &&
                                                                (tag(mem(mem(r1))) != 1))),
r1/mem(mem(r1)).


Ideally, I would like to prove equivalence of short code segments that
contain one or two dref instructions with other code segments written
using a different instruction set which may not have a dref instruction
(so the dereference would be done with an explicit loop of instructions).


Any comments, suggestions, or references would be most helpful.


Thanks,
Bruce Holmer
holmer@eecs.nwu.edu
--

Return to the comp.compilers page.
Search the comp.compilers archives again.