Operating system support for contracts

Patent metadata

Field	Value
Publication number	US-9286039-B2
Application number	US-201313829561-A
Country	US
Kind code	B2
Filing date	Mar 14, 2013
Priority date	Mar 14, 2013
Publication date	Mar 15, 2016
Grant date	Mar 15, 2016

Abstract

A front-end compiler compiles source code into intermediate code, that may later be compiled into binary code. The source code defines an execution scope and includes a contract. When a contract is encountered at runtime of an execution scope, further execution of that execution scope is conditioned on whether a predicate associated with the contract is true. The front-end compiler operates so as to preserve the contract so that the contract continues to be semantically structured such that the predicate may be removed from the intermediate language code. The contract may thus continue to be understood by semantic analysis of the contract. Thus, the predicate may be understood by static analysis tools that operate on the intermediate code.

First claim

What is claimed is:

1. A system comprising: one or more hardware processors; and one or more hardware storage devices having stored thereon computer-executable instructions that are executable by the one or more hardware processors and that configure the system to perform at least the following as part of a static analysis of intermediate language program code: identify a plurality of components in the intermediate language program code, each component comprising a different execution scope and including a corresponding contract, each contract conditioning further execution of the corresponding execution scope on whether a predicate of the contract is true when the contract is encountered at runtime of the corresponding execution scope; determine that a particular predicate of a particular contract corresponding to a particular component of the plurality of components may not always be true at runtime of the particular component; and generate executable code for the plurality of components into one or more executable binaries, including: when generating the executable code for the particular component, generate a portion of executable code having a first entry point that allows checking of the particular contract to be bypassed at runtime when the particular component is called by a first set of one or more other components of the plurality of components, and having a second entry point the causes the particular contract to be checked at runtime when the particular component is called by a second set of one or more other components of the plurality of components.

2. The system in accordance with claim 1 , wherein the particular component instructs the system to perform a behavior, and wherein the particular contract is semantically structured in such a way that the checking of the particular contract may be removed without changing the behavior.

3. The system in accordance with claim 1 , wherein each contract is semantically accessible to a caller of the corresponding component using an interface of the corresponding component.

4. The system in accordance with claim 1 , wherein a contract is a pre-condition for a corresponding component.

5. The system in accordance with claim 1 , wherein a contract is a post-condition for a corresponding component.

6. The system in accordance with claim 1 , wherein if the particular predicate is not true when encountered at runtime, the system is configured to run external recovery code outside of the execution scope of the particular component.

7. The system in accordance with claim 1 , wherein if the particular predicate is not true when encountered at runtime, the system is configured to conduct a fast fail for the particular component, such that no recovery code is run in response to the particular predicate not being true.

8. The system in accordance with claim 1 , wherein the system is also configured to detect at least some conditions under which a predicate includes an externally visible side effect.

9. The system in accordance with claim 1 , wherein the system is also configured to store the one or more executable binaries onto a storage device.

10. The system in accordance with claim 1 , wherein the system is also configured to: determine that another predicate of another contract corresponding to another component of the plurality of components will always be true at runtime of the other component; and when generating the executable code for the plurality of components into one or more executable binaries, generating a third portion of executable code for the other component, the third portion of executable code that lacking any executable code corresponding to the other contract and the other predicate, based on having determined that the other predicate will always be true at runtime of the other component.

11. A method, implemented at a computer system that includes one or more hardware processors, for performing a static analysis of intermediate language program code, the method comprising: identifying, at the one or more hardware processors, a plurality of components in the intermediate language program code, each component comprising a different execution scope and including a corresponding contract, each contract conditioning further execution of the corresponding execution scope on whether a predicate of the contract is true when the contract is encountered at runtime of the corresponding execution scope; determining, at the one or more hardware processors, that a particular predicate of a particular contract corresponding to a particular component of the plurality of components may not always be true at runtime of the particular component; and generating, at the one or more hardware processors, executable code for the plurality of components into one or more executable binaries, including: when generating the executable code for the particular component, generating a portion of executable code having a first entry point that allows checking of the particular contract to be bypassed at runtime when the particular component is called by a first set of one or more other components of the plurality of components, and having a second entry point the causes the particular contract to be checked at runtime when the particular component is called by a second set of one or more other components of the plurality of components.

12. The method in accordance with claim 11 , wherein the static analysis is performed by at least one of a refactoring tool, a verification tool, and an automated documentation generator.

13. The method in accordance with claim 11 , wherein a contract is a pre-condition for a corresponding component.

14. The method in accordance with claim 11 , wherein a contract is a post-condition for a corresponding component.

15. The method in accordance with claim 11 , wherein if the particular predicate is not true when encountered at runtime, external recovery code is run outside of the execution scope of the particular component.

16. The method in accordance with claim 11 , wherein if the particular predicate is not true when encountered at runtime, a fast fail is conducted for the particular component, such that no recovery code is run in response to the particular predicate not being true.

17. The method in accordance with claim 11 , further comprising storing, by the one or more hardware processors, the one or more executable binaries onto one or more hardware storage devices.

18. The method in accordance with claim 11 , further comprising: determining that another predicate of another contract corresponding to another component of the plurality of components will always be true at runtime of the other component; and when generating the executable code for the plurality of components into one or more executable binaries, generating a third portion of executable code for the other component, the third portion of executable code that lacking any executable code corresponding to the other contract and the other predicate, based on having determined that the other predicate will always be true at runtime of the other component.

19. A computer program product comprising one or more hardware storage memories having stored thereon computer-executable that are executable by one or more hardware processors of a computer system, and that configure the computer system to perform at least the following as part of a static analysis of intermediate language program code: identify a plurality of components in the intermediate language program code, each component comprising a different execution scope and including a cor

Assignees

• Microsoft Corp
• Microsoft Technology Licensing Llc

Inventors

• Duffy John J
• Parsons Jared Porter
• Gordon Colin Stebbins
• Bromfield Alexander Daniel
• Taillefer Martin
• Bartolomeo David Allen
• Barnett Michael

Classifications

• G06F9/54

  Interprogram communication · CPC title

• G06F8/41 Primary

  Compilation · CPC title

• G06F9/45512

  Command shells · CPC title

• G06F8/436 Primary

  Semantic checking · CPC title

• G06F8/52

  Binary to binary · CPC title