Browse Prior Art Database

Method for validation of binary code transformations

IP.com Disclosure Number: IPCOM000146953D
Original Publication Date: 2007-Feb-28
Included in the Prior Art Database: 2007-Feb-28
Document File: 5 page(s) / 156K

Publishing Venue

IBM

Abstract

Optimizing executable code is typically performed using a runtime profile of the code. Different optimization techniques are available, like inlining and code restructuring. However, they all must transform the code to functionally equivalent form. Failing to do so has unpredicable consequences, typically a program crash. Proposed herein is a method that helps validate the correctness of such transformations.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 31% of the total text.

Page 1 of 5

Method for validation of binary code transformations

Optimizing executable code is a known technique to improve the performance of code that has already been linked and is ready for execution. It is typically performed using a runtime profile of the code. Different optimization techniques are available, like inlining and code restructuring. However, they all must transform the code to functionally equivalent form. Failing to do so has unpredictable consequences, typically a program crash. The method proposed here helps validate the correctness of such transformations.

Alternative solutions are described in:
High-level models, with validation done using simulation (derived from


1.


2.
3. US6286130: Software implemented method for automatically validating the correctness of parallel computer programs
4. US5048018: Debugging parallel programs by serialization

    The binary code of the original program and the transform program are analyzed, using various available techniques [...], and a control flow graph of both programs is generated. For each validated function, both graphs are traversed in consistent fashion, creating their linear invariant textual representations. These linear representations can be compared as simple text strings in order to identify incorrect transformation.

    The high-level alternatives are not suitable for validating binary level optimization because high level model is very difficult if not impossible to generate. The low-level approaches are based on exact verification, require very precise architecture models, are used for HW verification, and assume only small sequence of instructions

The proposed method works along the following 4 steps:

STEP1: Program Analysis

    The executable program (the executable below) is analyzed using the FDPR technology [...]. The principal output of this analysis is a sequence of basic units. Basic units are the smallest elements of the program that must stay intact under every reordering. For the purposes of this discussion, the basic units are of two types: basic blocks and data objects. The first contain instructions, while the latter contain data (read-only as well as writable).

Data objects corresponds to the high-level data objects defined in the source program (arrays, structures, or scalars).

A basic block is a sequence of instructions that can be entered only at its beginning and exited only at its end. Figure 1 shows a sequence of three basic blocks, of which two are adjacent.

high-level languages [various papers by Pnueli et al.]

Low-level representation, with validation using format verification [...]

Page 2 of 5

#13b74200 ...

lhz r0,52(r28) A

lwz r3,48(r28)

mr r4,r0

ori r0,r0,4096

andi. r3,r3,1

sth r0,52(r28) bne- 13b74278 lhz r3,74(r29) B andi. r3,r3,4 ori r3,r4,12288

beq- 13b74278


#13b74278 ...
andi. r0,r0,57343 C sth r0,52(r28) b 13b74230

Figure 1: Samp...