Memory safety of floating-point computations

• US 8,782,625 B2
• Filed: 06/17/2010
• Issued: 07/15/2014
• Est. Priority Date: 06/17/2010
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Godefroid, Patrice, Kinder, Johannes
• Primary Examiner(s): DAO, THUY CHAN
• Application Number:
  US12/817,227
• Publication Number:
  US 20110314251A1
• Time in Patent Office: 1,489 Days
• US Class Current: 717/151
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 11/3624 by performing operations on the source code, e.g. via a compiler

Abstract

Concepts and technologies are described herein for determining memory safety of floating-point computations. The concepts and technologies described herein analyze code to determine if any floating-point computations exist in the code, and if so, if the floating-point computations are memory safe. The analysis can include identifying floating-point instructions and conditional statements in the code. The code can be symbolically executed, and behavior of the floating-point instructions and the conditional statements can be monitored to determine if a floating point calculation is ever involved in computation of any memory address during the execution of the code.

Claims

1. A computer-implemented method for determining memory safety of floating point instructions, the computer-implemented method comprising performing computer-implemented operations for:

receiving a portion of code at an evaluation engine, the code comprising computer executable instructions corresponding to an application;

analyzing, by a computing device, the portion of the code to determine if the portion of the code comprises a floating-point instruction; and

in response to determining that the portion of the code comprises the floating-point instruction,

generating, by the computing device, a set of memory addresses and registers written during execution of the floating-point instruction,

symbolically executing, by the computing device, the portion of the code,

assigning, by the computing device, a symbolic value into the set for each memory address and register in the set, and

determining, by the computing device, if the symbolic value is used to calculate any memory address during the symbolic execution.

2. The method of claim 1, wherein the symbolic value comprises all possible values for a floating-point calculation made during the symbolic execution of the code.

3. The method of claim 1, further comprising in response to determining that the portion of the code does not comprise the floating-point instruction, analyzing, by the computing device, the portion of code to determine if the portion of code comprises a conditional statement.

4. The method of claim 3, further comprising in response to determining that the portion of the code comprises the conditional statement,

generating, by the computing device, a first set comprising a set of memory addresses and registers written during execution of the conditional statement,

generating, by the computing device, a second set comprising a set of registers that may be used to compute a memory address being read or written to during execution of the conditional statement, and

symbolically executing, by the computing device, the portion of the code.

5. The method of claim 4, further comprising:

in response to determining that the portion of the code does not comprise the floating-point instruction or the conditional statement, obtaining another portion of code to determine if the other portion of code comprises any floating-point instructions or any conditional statements.

6. The method of claim 4, further comprising:

determining, by the computing device, if a register in the second set comprises an input-dependent address or the symbolic value, and

in response to determining that the register in the second set comprises the input-dependent address or the symbolic value, generating an error.

7. The method of claim 6, further comprising:

in response to determining that the register in the second set does not comprise the input-dependent address or the symbolic value, resuming the symbolic execution,

assigning, by the computing device, the symbolic value to each memory address and register in the first set, and

determining, by the computing device, if the symbolic value is used to calculate any memory address during the symbolic execution.

8. The method of claim 7, further comprising:

in response to determining that the symbolic value is used to calculate the memory address during the symbolic execution, generating an error.

9. The method of claim 8, further comprising:

in response to determining that the symbolic value is not used to calculate the memory address during the symbolic execution, obtaining another portion of code to determine if the other portion of code comprises any floating-point instructions or any conditional statements.

10. The method of claim 1, wherein the symbolic value comprises FP-tag, the value of FP-tag comprising all possible values for a floating-point calculation made during execution of the floating point instruction, and wherein assigning the symbolic value further comprises assigning, by the computing device, FP-tag for each value in the set of memory addresses and registers.

11. A computer-implemented method for determining memory safety of floating point instructions, the computer-implemented method comprising performing computer-implemented operations for:

receiving code at an evaluation engine, the code comprising computer executable instructions corresponding to an application;

parsing, by a computing device, the code to extract a portion of the code to evaluate for memory safety of floating-point instructions in the portion of the code;

analyzing, by the computing device, the portion of the code to determine if the portion of the code comprises a floating-point instruction; and

in response to determining that the portion of the code comprises the floating-point instruction,

generating, by the computing device, a set of memory addresses and registers written during execution of the floating-point instruction,

symbolically executing, by the computing device, the portion of the code,

assigning, by the computing device, a symbolic value into the set for each memory address and register in the set, and

determining, by the computing device, if the symbolic value is used to calculate any memory address during the symbolic execution.

12. The method of claim 11, further comprising in response to determining that the portion of the code does not comprise the floating-point instruction, analyzing, by the computing device, the portion of code to determine if the portion of code comprises a conditional statement.

13. The method of claim 11, further comprising:

in response to determining that the portion of the code comprises the conditional statement,

generating, by the computing device, a first set comprising a set of memory addresses and registers written during execution of the conditional statement,

generating, by the computing device, a second set comprising a set of registers that may be used to compute a memory address being read or written to during execution of the conditional statement, and

symbolically executing, by the computing device, the portion of the code.

14. The method of claim 11, further comprising:

determining, by the computing device, if a register in the second set comprises an input-dependent address or the symbolic value,

in response to determining that the register in the second set comprises the input-dependent address or the symbolic value, generating an error, and

in response to determining that the register in the second set does not comprise the input-dependent address or the symbolic value,

resuming the symbolic execution,

assigning, by the computing device, the symbolic value to each memory address and register in the first set, and

determining, by the computing device, if the symbolic value is used to calculate any memory address during the symbolic execution.

15. The method of claim 11, further comprising:

in response to determining that the symbolic value is not used to calculate any memory address during the symbolic execution, determining, by the computing device, if another portion of code is available; and

obtaining the other portion of code to determine if the other portion of code comprises a floating-point instruction, in response to determining that the other portion of code is available.

16. The method of claim 11, further comprising:

generating, by the computing device, a pass indication for the code in response to determining that the other portion of the code is not available.

17. The method of claim 11, wherein the symbolic value comprises FP-tag, the value of FP-tag comprising all possible values for a floating-point calculation made during execution of the floating point instruction, and wherein the method further comprises:

in response to determining that FP-tag is used to calculate one or more memory addresses during the symbolic execution, generating an alert; and

in response to determining that FP-tag is not used to calculate any memory address during the symbolic execution,

determining, by the computing device, if another portion of code is available; and

obtaining the other portion of code to determine if the other portion of code comprises floating-point instructions, in response to determining that the other portion of code is available.

18. A computer-readable storage medium having computer readable instructions stored thereupon that, when executed by a computer, cause the computer to:

receive code at an evaluation engine, the code comprising computer executable instructions corresponding to an application;

parse the code to extract a portion of the code to evaluate for memory safety of floating-point instructions in the portion of the code;

analyze the portion of the code to determine if the portion of the code comprises a floating-point instruction; and

in response to determining that the portion of the code comprises the floating-point instruction,

generate a set of memory addresses and registers written during execution of the floating-point instruction,

symbolically execute the portion of the code,

assign a symbolic value to each memory address and register in the set, and

determine if the symbolic value is used to calculate any memory address during the symbolic execution.

19. The computer-readable storage medium of claim 18, wherein the computer readable instructions further comprise instructions, the execution of which cause the computer to:

analyze the portion of the code to determine if the portion of the code comprises a conditional statement; and

in response to determining that the portion of the code comprises the conditional statement,

generate a first set comprising a set of memory addresses and registers written during execution of the conditional statement,

generate a second set comprising a set of registers that may be used to compute a memory address being read or written to during execution of the conditional statement,

symbolically execute the portion of the code,

encounter the conditional statement during the symbolic execution of the code,

determine if a register in the second set comprises an input-dependent address or the symbolic value,

in response to determining that the register in the second set comprises the input-dependent address or the symbolic value, generate an error, and

in response to determining that the register in the second set does not comprise the input-dependent address or the symbolic value,

resume the symbolic execution,

assign the symbolic value to each memory address and register in the first set, and

determine if the symbolic value is used to calculate any memory address during the symbolic execution.

20. The computer-readable storage medium of claim 19, wherein the computer readable instructions further comprise instructions, the execution of which cause the computer to:

in response to determining that the symbolic value is not used to calculate any memory address during the symbolic execution, determine if another portion of code is available;

obtain the other portion of code to determine if the other portion of code comprises floating-point instructions or conditional statements, in response to determining that the other portion of code is available; and

generate a pass indication for the code in response to determining that the other portion of the code is not available.