Software analyzer
AssigneeSofCheck, Inc.
InventorsS. Tucker Taft, Robert Duff, Melanie Blower, Mireille Gart, Sheri Bernstein
Life of this patent
Estimating the term…
Abstract
It is possible to identify pre- and post-conditions on a set of machine instructions by determining and analyzing possible value sets for variables and expressions. Stepping forward and backward through the set of instructions and tracking value sets at all points of reference allows for the value sets to be maximally restricted, which, in turn, gives an indication of allowed domains for different variables. These domains can be used to derive pre- and post-conditions for the set of instructions.
Claims34
An automated method of characterizing a set of machine-readable instructions, said method comprising:
- assigning a value number to each expression within the set of instructions;
- and
- tracking possible value sets for each value number at each point of reference.
An automated method of characterizing a set of machine-readable instructions, said method comprising:
- assigning a value number to each expression within the set of instructions;
- determining a value set for a first value number being referenced in an instruction;
- and
- determining a value set for a second value number related to the first value number.
An automated method of deriving preconditions and post-conditions for a procedure, said method comprising:
- computing value sets for a subset of value numbers of the procedure.
A method of assigning a unique identifier to every object reference within a set of instructions and tracking values associated with a subset of these objects, said method comprising:
- identifying all object references within the set of instructions;
- tracking values for objects that are of an integer or pointer type such that the conservative value set for the object includes every value the object might have somewhere within the set of instructions;
- and
- using the tracked values of integer and pointer objects to determine potential aliasing between object references involving at least one of the following:
- array indexing, pointer arithmetic, and pointer dereferencing.
A system for characterization of machine-readable instructions, said system comprising:
- a set of machine-readable instructions;
- a value number assigned to each expression within the set of instructions;
- and
- memory storing possible value sets for each value number at each point of reference.
A system for automatically characterizing a set of machine-readable instructions, said system comprising:
- for a subset of instructions in the set of instructions, memory storing:
- value numbers assigned to expressions within an instruction;
- a value set for a first value number being referenced in the instruction;
- and
- a value set for a second value number related to the first value number.
A machine-readable medium storing instructions for characterizing a set of machine-readable instructions, said instructions comprising:
- instructions for assigning a value-number to each expression within the set of machine-readable instructions;
- instructions for determining a value set for a first value number being referenced in a machine-readable instruction;
- and
- instructions for determining a value set for a second value number related to the first value number.
Dependencies are inferred from the claim text.