Static enforcement of provable assertions at compile

1. A non-transitory machine-readable medium storing instructions to cause one or more processors to perform operations comprising:

processing, in an integrated development environment, a set of program code to identify an assertion within the set of program code;

determining compile-time provability of a condition specified by the assertion, wherein determining the compile-time provability of the condition specified by the assertion includes semantically converting the condition specified by the assertion into a Boolean, reducing the Boolean to an intermediate representation, and processing the intermediate representation to verify that an evaluation chain for the condition is Boolean constant at compile-time; and

presenting an error condition in response to failing to determine the compile-time provability of the condition specified by the assertion, wherein failing to determine the compile-time provability of the condition specified by the assertion includes:

detecting an expression that is Boolean non-constant at the compile-time, the expression being within the intermediate representation associated with the condition specified by the assertion within the set of program code;

analyzing the expression based on evaluation rules configured based on a logical or mathematical characteristic of the expression;

determining whether an output value of the expression is constrained or unconstrained to determine the compile-time provability of the condition specified by the assertion; and

failing to determine that the output value of the expression is constrained.

2. The non-transitory machine-readable medium as in claim 1 , wherein failing to determine the compile-time provability of the condition specified by the assertion includes detecting another expression within the intermediate representation of the evaluation chain for the condition that is Boolean non-constant at the compile-time.

3. The non-transitory machine-readable medium as in claim 1 , wherein the intermediate representation is an abstract syntax graph and the operations additionally include traversing the abstract syntax graph until detection of a value that is non-constant at the compile-time.

4. The non-transitory machine-readable medium as in claim 3 , wherein traversing the abstract syntax graph includes performing a depth-first search to traverse the abstract syntax graph until a terminal graph node is discovered that is non-constant at the compile-time.

5. The non-transitory machine-readable medium as in claim 4 , the operations additionally comprising immediately terminating traversal of the abstract syntax graph in response to discovery of a non-constant terminal graph node.

6. The non-transitory machine-readable medium as in claim 1 , the operations additionally comprising:

determining the compile-time provability of the condition specified by the assertion, the condition associated with a symbol that is unique within the set of program code;

storing a provability result and the symbol in a condition cache; and

reading the provability result from the condition cache during a subsequent verification of the symbol, the provability result having previously been determined for the symbol.

7. The non-transitory machine-readable medium as in claim 6 , wherein the condition cache includes a list of previously evaluated graph traversals that have been found statically provable at the compile-time.

8. The non-transitory machine-readable medium as in claim 1 , the operations additionally comprising:

receiving a specified truth value for a predicate associated with a condition specified by the assertion; and

determining the compile-time provability of the condition based on the specified truth value.

9. The non-transitory machine-readable medium as in claim 8 , wherein the specified truth value is specified via a locally-scoped compiler directive.

10. The non-transitory machine-readable medium as in claim 8 , wherein the specified truth value is received from a static analyzer module.

11. The non-transitory machine-readable medium as in claim 1 , wherein the instructions further cause the one or more processors to perform the operations comprising:

storing a compile-time provability result in a condition cache; and

flushing the condition cache in response to a change in the set of program code.

12. A data processing system comprising:

a memory to store instructions for processing; and

one or more processors to execute the instructions, wherein the instructions, when executed, cause the data processing system to perform operations comprising:

processing, in an integrated development environment, a set of program code to identify an assertion within the set of program code;

determining compile-time provability of a condition specified by the assertion, wherein determining the compile-time provability of the condition specified by the assertion includes semantically converting the condition specified by the assertion into a Boolean, reducing the Boolean to an intermediate representation, and processing the intermediate representation to verify that an evaluation chain for the condition is Boolean constant at compile-time, the evaluation chain including multiple values; and

presenting an error condition in response to failing to determine the compile-time provability of the condition specified by the assertion, wherein failing to determine the compile-time provability of the condition specified by the assertion includes:

detecting an expression that is Boolean non-constant at the compile-time, the expression being within the intermediate representation associated with the condition specified by the assertion within the set of program code;

analyzing the expression based on evaluation rules configured based on a logical or mathematical characteristic of the expression;

determining whether an output value of the expression is constrained or unconstrained to determine the compile-time provability of the condition specified by the assertion; and

failing to determine that the output value of the expression is constrained.

13. The data processing system as in claim 12 , wherein failing to determine the compile-time provability of the condition specified by the assertion includes detecting another expression within the intermediate representation of the evaluation chain of the condition that is Boolean non-constant at the compile-time.

14. The data processing system as in claim 12 , wherein the intermediate representation is an abstract syntax graph and the operations additionally include traversing the abstract syntax graph until detection of a value that is non-constant at the compile-time.

15. The data processing system as in claim 14 , wherein traversing the abstract syntax graph includes performing a depth-first search to traverse the abstract syntax graph until a terminal graph node is discovered that is non-constant at the compile-time.

16. The data processing system as in claim 15 , the operations additionally comprising immediately terminating traversal of the abstract syntax graph in response to discovery of a non-constant terminal graph node.

17. The data processing system as in claim 12 , the operations additionally comprising:

determining the compile-time provability of the condition specified by the assertion, the condition associated with a symbol that is unique within the set of program code;

storing a provability result and the symbol in a condition cache; and

reading the provability result from the condition cache during a subsequent verification of the symbol, the provability result having previously been determined for the symbol, wherein the condition cache includes a list of previously evaluated graph traversals that have been found statically provable at the compile-time.

18. The data processing system as in claim 12 , the operations additionally comprising:

receiving a specified truth value for a predicate associated with a condition specified by the assertion; and

determining the compile-time provability of the condition based on the specified truth value.

19. The data processing system as in claim 18 , wherein the specified truth value is specified via a locally-scoped compiler directive or is received from a static analyzer module.

20. A method comprising:

on a computing device including one or more processors:

processing, in an integrated development environment, a set of program code to identify an assertion within the set of program code;

determining compile-time provability of a condition specified by the assertion, wherein determining the compile-time provability of the condition specified by the assertion includes semantically converting the condition specified by the assertion into a Boolean, reducing the Boolean to an intermediate representation, and processing the intermediate representation to verify that an evaluation chain for the condition is Boolean constant at compile-time; and

presenting an error condition in response to failing to determine the compile-time provability of the condition specified by the assertion, wherein failing to determine the compile-time provability of the condition specified by the assertion includes:

detecting an expression that is Boolean non-constant at the compile-time, the expression being within the intermediate representation associated with the condition specified by the assertion within the set of program code;

analyzing the expression based on evaluation rules configured based on a logical or mathematical characteristic of the expression;

determining whether an output value of the expression is constrained or unconstrained to determine the compile-time provability of the condition specified by the assertion; and

failing to determine that the output value of the expression is constrained.

21. The method as in claim 20 , further comprising:

determining the compile-time provability of the condition specified by the assertion, the condition associated with a symbol that is unique within the set of program code;

storing a provability result and the symbol in a condition cache; and

reading the provability result from the condition cache during a subsequent verification of the symbol, the provability result having previously been determined for the symbol.