Validation of static analysis tools via comparison of concrete and abstract states

A system for validating a static analysis tool comprising:

• a processing system;
• and
• a computer-readable medium having encoded thereon, computer-readable instructions, that when executed by the processing system, causes the system to perform operations comprising:
• receiving a test program comprising a sequence of instructions and data for initializing the test program;
• computing, by the static analysis tool, an abstract state of the test program for an instruction of the sequence of instructions, wherein the abstract state defines an expected value for the instruction that is identified as valid by the static analysis tool;
• generating, by a concrete implementation executing the test program, a concrete state of the test program for the instruction of the sequence of instructions, wherein the concrete state includes a specific value that is calculated from an execution of the instruction using the data;
• identifying a mismatch between the concrete state and the abstract state at the instruction of the test program, wherein the mismatch is identified by the specific value included in the concrete state being different from the expected value defined by the abstract state;
• and
• in response to identifying the mismatch, generating an alert, wherein the alert identifies the instruction that caused the mismatch between the concrete state and the abstract state.

A computer-readable storage medium having encoded thereon, computer-readable instructions that when executed by a system, cause the system to perform operations comprising:

• receiving a test program comprising a sequence of instructions and data for initializing the test program;
• computing, by the static analysis tool, an abstract state of the test program for an instruction of the sequence of instructions, wherein the abstract state defines an expected value for the instruction that is identified as valid by the static analysis tool;
• generating, by a concrete implementation executing the test program, a concrete state of the test program for the instruction of the sequence of instructions, wherein the concrete state includes a specific value that is calculated from an execution of the instruction using the data;
• identifying a mismatch between the concrete state and the abstract state at the instruction of the test program, wherein the mismatch is identified by the specific value included in the concrete state being different from the expected value defined by the abstract state;
• and
• in response to identifying the mismatch, generating an alert, wherein the alert identifies the instruction that caused the mismatch between the concrete state and the abstract state.