Operating system support for contracts

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.

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 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 first predicate of a first contract corresponding to a first of the plurality of components will always be true at runtime of the first of the plurality of components;
• determine that a second predicate of a second contract corresponding to a second of the plurality of components may not always be true at runtime of the second of the plurality of components;
• and generate executable code for the plurality of components into one or more executable binaries, including:
• when generating the executable code for the first of the plurality of components, generating a first portion of executable code that lacks any executable code corresponding to the first contract and the first predicate, based on having determined that the first predicate will always be true at runtime of the first of the plurality of components;
• and when generating the executable code for the second of the plurality of components, generate a second portion of executable code having a first entry point that allows checking of the second contract to be bypassed at runtime when the second 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 second contract to be checked at runtime when the second component is called by a second set of one or more other components of the plurality of components.