Static enforcement of provable assertions at compile

Embodiments described herein provide for a non-transitory machine-readable medium storing instructions to cause one or more processors to perform operations 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; and presenting an error condition in response to failing to determine compile-time provability of the condition specified by the assertion, wherein determining 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 detect an expression within the intermediate representation that is non-constant at compile-time.

FIELD

Embodiments described herein relate generally to integrated development environments. More specifically, embodiments related to an integrated development environment that provides static and compile-time enforcement of provable assertions.

BACKGROUND OF THE DESCRIPTION

In conventional programming languages, assertions are used to perform runtime checks of assumptions about system state during the execution of program code. An assert statement can be placed into program code. When the assert statement is executed, a check as to the truth of a Boolean statement is performed. If the condition is true, no operations are performed as a result of the assert statement. If the condition is false, the assert statement immediately terminates the program. The assert statement enables programmers to impose conditions that are assumed to be true at the point of the assertion statement. If those assumptions fail, the continued execution of the program may not be safe.

SUMMARY OF THE DESCRIPTION

Embodiments described herein provide an integrated development environment that includes a compiler and analyzer toolchain that evaluates assertion statements within program code. Assertion statements assert the truth of a Boolean condition, which may be a simple value or expression or may be a Boolean-logic composition of multiple values or expressions. The toolchain of the integrated development environment is configured to determine if the asserted condition of the assertion statement is statically provable at compile-time. A condition is statically provable if and only if every element of a composition of multiple values can be resolved to a constant value at compile-time, or the set of potential values of any non-constant values or expression within the condition can be determined to be sufficiently constrained.

One embodiment provides for a non-transitory machine-readable medium storing instructions to cause one or more processors to perform operations 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, and presenting an error condition in response to failing to determine compile-time provability of the condition specified by the assertion. Determining 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 detect an expression within the intermediate representation that is non-constant at compile-time.

One embodiment provides for a data processing system comprising a memory to store instructions for processing and one or more processors to execute the instructions. 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, and presenting an error condition in response to failing to determine compile-time provability of the condition specified by the assertion, wherein determining 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 detect an expression within the intermediate representation that is non-constant at compile-time.

The above summary does not include an exhaustive list of all embodiments in this disclosure. All systems and methods can be practiced from all suitable combinations of the various aspects and embodiments summarized above, and also those disclosed in the Detailed Description below.

DETAILED DESCRIPTION

Assertions can be used in a variety of situations during the development of a software program and, in some instances, may also be included within production program code. Assertions can be used to verify internal invariants within program code or to verify logical preconditions and/or postconditions for a function or block of program code. An invariant is a condition that can be relied upon as true during the execution of a block of program code. Preconditions for program code include bounds on the logical state that is assumed to be in effect before a function, method, or block of code is to be executed. Postconditions for program code include bounds on the logical state that is assumed to be in effect after function, method, or block of code is executed.

The use of assertions should be limited to conditions that will always be true during runtime. Should an assertion fail, the results of program termination may be severe, as a failed assertion results in the immediate termination of an executing program. However, during program development, some developers may improperly use assertions to check runtime conditions with statements that may evaluate to false during program execution, even if such occurrence may be extremely rare. Should an assertion failure condition occur, the immediate termination of the program code will result. If the assertion failure is rare, the program may survive testing without issue, only to fail unexpectedly in real-word scenarios. Accordingly, in some software development systems, it may be desirable to prevent the use of assertion statements unless those statements can be statically proven at compile-time.

Embodiments described herein pertain to the design of software programming languages and to the compiler that translates a programming language into executable program-code. One embodiment provides for a compiler of a software programming language to enforce the provability of an assertion at compile-time. Techniques described here enhance the programming language arts by enabling the enforcement of “provability criterion” for any assertion. If the assertion is not provable, the compiler will report an error to the programmer at compile-time instead of allowing an unproven assertion to persist in the software program. Enforcement of static provability improves discoverability of error conditions and prevents a malformed assertion from causing unexpected runtime errors. If the programmer wishes to run the program code, the programmer can either rewrite the software so that the assertion can be statically proven or the programmer can remove the assertion. In addition to a compiler, one embodiment provides for an analysis toolchain that can also be used to evaluate the provability of the assertion based on static analysis of program code. In one embodiment the compiler and analysis toolchain can work together to enable cross-module verification of assertions.

Assertion statements assert the truth of a Boolean condition, which may be a simple value or expression or may be a Boolean-logic composition of multiple values or expressions. A condition is statically provable if and only if every element of a composition of multiple values can be resolved to a constant value at compile-time. In one embodiment, a compiler can implement such check by semantically converting the condition specified by the programmer into a Boolean statement, reducing the Boolean statement to an abstract syntax graph, tree, or another intermediate representation, and traversing an abstract syntax graph or tree using a spanning graph traversal algorithm. In one embodiment, the compiler can perform a depth-first search to traverse an abstract syntax tree until a terminal graph node (e.g., leaf node) is discovered that is non-constant at compile-time. The compiler can be configured to enable early termination of the graph search when a non-constant node is found, as the non-constant node indicates that the programmer has represented an unprovable assertion.

In one embodiment, the compiler can present a human-readable error-statement that clearly specifies the contents of the non-constant leaf-node discovered during graph traversal, providing an easy-to-interpret method for the programmer to fix the non-provability condition. In one embodiment, an optimization is provided that enables the re-use of previously-proven assertions during a run of the compiler. The compiler tool can maintain a cached list of previously-evaluated graph traversals that have been found to be statically-provable.

One embodiment provides a technique in which a programmer can temporarily specify a Boolean logic predicate expression that is proven using external methods or the truth of which is being asserted by a developer. The enhancement can be implemented in the firm of a locally-scoped compiler directive that allows the programmer to specify truth-value for a predicate in an assertion condition. One embodiment provides for an assert-verify paradigm in which a programmer can assert the truth of a value and a later verify statement can be used to verify a condition that at least in part includes the previously asserted value.

In various aspects of the embodiments described herein, “compiler” and “analyzer” are used interchangeably, where both terms represent a software tool that translates a high-level language representation into an abstract syntax representation. In one embodiment, a compiler and analyzer toolchain are provided in which some elements of the concepts described herein are implemented by a compiler and other elements are implemented by an analyzer. For example, a compiler can perform compile-time verification of assertions within a programming language module, while an analyzer can verify assertions based on cross-module statements. In one embodiment, Boolean logic predicates can be provided to a compiler by an analyzer to assist the compiler in the verification of assertions. Additionally, different portions or modules of a modular compiler can provide results of compile-time verification of assertion statements to other portions or modules of the modular compiler.

FIG. 1A-1Billustrate an integrated development environment configured for static enforcement of provable assertions at compile-time, according to an embodiment.FIG. 1Aillustrates a user interface110for an integrated development environment (IDE).FIG. 1Billustrates analysis of Boolean condition of an assertion statement to determine compile-time provability of the assertion statement.

As shown inFIG. 1A, an IDE is provided having a user interface110into which files that include software code and/or program statements can be browsed and edited by a programmer. The user interface110includes an editor111that can be used to inter or edit program code or software statements. In addition to the user interface110, the IDE includes a compiler and/or an interpreter, build automation tools, a code analyzer, and a debugger. Examples of IDEs include the Xcode IDE from Apple Inc. of Cupertino, Calif., and the Visual Studio IDE from Microsoft Corp. of Redmond, Wash. Other IDEs are known to those of skill in the art.

The user interface110includes an editor that includes features that facilitate viewing and editing text (e.g., source code, XML, etc.) and/or graphical content (e.g., representations of programming components such as data models or graphical user interface (GUI) components). The editor also includes features that facilitate moving between files and accessing related reference materials (e.g., an application programming interface (API) definition).

Some types of IDEs provide software development capabilities for a specific programming language and have a feature set that is tightly coupled to the programming paradigm for the specific programming language. Other types of IDEs, such that the IDE provided by embodiments described herein, include support for multiple programming languages. Support for multiple programming languages allows a single IDE to be used to develop software for multiple projects spanning multiple programming languages and/or multiple platform, instead of using one IDE per programming language.

In the figures and accompanying description, program code statements are used to illustrate concepts of the embodiments. However, those program code statements are not intended to be specific as to any one programming language or programming paradigm. The concepts described herein can be generally applied to a variety of programming languages for a variety of platforms. Furthermore, the concepts can be implemented within a variety of different types of integrated development environments, compiler toolchains, or static analyzers, as described in further detail below.

The editor111can display or receive entry of a program statement, such as a declaration of a function112. The function112can include program code that can be compiled by a compiler for execution on a target platform. As illustrated, the function112includes a program statement113and an assertion statement114. The assertion statement114includes a condition115that is asserted to be true by the assertion statement114. Example logic to evaluate the assertion statement114and condition115is shown by program statement116, where if the provided condition115is not true, the program will throw or trigger an error, which immediately halts the execution of the program. Assertions differ from exceptions in that the failure of an assertion should not be caught and handled, as the assertion failure may indicate that the program code is in a state where continued execution may result in data corruption or another outcome that is less favorable than the immediate termination of the program.

Because of the severe results of an assertion failure, embodiments described herein provide for an IDE having compile-time logic to enforce the static provability of assertion statements at compile-time. If the assertion statement114cannot be determined to be true for all possible runtime conditions, the compiler will display an error message117via the user interface110. The error message117can indicate the specific assertion statement and condition that failed. For complex assertion statements, the error message117can indicate which portion of the assertion statement cannot be statically verified.

For example, program statement113is a mathematical statement that sets the variable Y to the product of x*x, where x is a parameter of the function112. The assertion statement114asserts the condition115that Y is greater than zero.FIG. 1Billustrates analysis of the assertion statement114, as performed in one embodiment.

As shown inFIG. 1B, in one embodiment the condition115of the assertion statement114is evaluated as a Boolean statement120. The Boolean statement120is analyzed to determine if such statement is statically provable. The Boolean statement120can be converted into an intermediate representation of the statement. In one embodiment, the analysis of the intermediate representation can be performed by generating an abstract syntax tree121based on the intermediate representation. The abstract syntax tree121is a logical structuring of the intermediate representation of the Boolean statement120. The abstract syntax tree121can include an operation122to be performed, with the set of inputs (e.g., first input123, second input124) arranges as child nodes of the operation122. The operation122of the abstract syntax tree121of the Boolean statement120(Y>0) includes a compare operation that is evaluated based on a first input123(Y variable) and a second input124(immediate value zero). The second input124is a constant, so the value of the second input is known at compile-time. The first input123, however, is a variable that may be non-constant at compile-time.

The value of the first input123(variable Y) is determined based on an expression126, which is a mathematical expression (x*x). In one embodiment, a further evaluation of the expression126can be performed to determine if, at the least, a constraint on the value of the first input123can be determined. The further evaluation of the expression126determines that the value of the variable Y is based on a multiply operation126bhaving input126aand input126c, where each input is function parameter x.

Given this scenario, the compiler may or may not have sufficient data regarding the potential values of x to determine that it is provable, at compile-time, that the truth of the Boolean statement120(Y>0) can be determined, for example, based on the potentially unknown value of x, which is a parameter to the function112that contains the assertion statement114. For example, if the value of x is in any way related to an input from a source external to the program, the value of x may be unconstrained. Alternatively, the value of x may be determined based on program code in different program module as the function112, and that value may be out of the scope of values that can be determined during compilation of the program module that contains the function112. In such scenarios, an error message117may be generated and displayed to the programmer that indicates that the assertion statement is not statically provable by the compiler. Alternatively, if the value of x is determined by program code within the same program module (e.g., file, library, etc.) as the function112, it may be possible for the compiler to determine the value of x or at least a constraint on the value of x. In one embodiment, a value of x or a constraint on the value of x may be provided by another module of the compiler or from a program code analyzer that is executing concurrently with the compiler.

In some embodiments, even if one or more individual values associated with a condition115are unknown, some constraints can be determined based on the operation126bthat is evaluated. For example, the expression126includes a multiply operation126bhaving inputs126a,126cthat are identical. Accordingly, the expression126can be evaluated to determine that the set of all potential outputs are greater than or equal to zero for any input value x. Were the condition115was instead (Y>=0) rather than simply (Y×0), the truth of the condition could be determined statically and the assertion would be allowed without triggering an error.

Thus, for at least one embodiment described herein, the assertion evaluation logic can be configured to determine if all inputs that determine the value of the Boolean associated with an assertion statement are constant at compile-time, then if all inputs cannot be determined to be constant, the assertion evaluation logic can then determine if constraints exist on the constituent expressions of the condition that allow the provability of the condition to be statically determined.

The Boolean statement120illustrated is a relatively simple statement and is shown for descriptive and exemplary purposes. However, the conditions of assertion statements to be evaluated may be exceedingly complex. Complex assertion statements may be difficult to craft and error check. In some program code implementations, such as program code that implements computer vision algorithms, portions of the program code may be the result of machine generated and produced as the result of a complex, iterated upper level of software. For such program code, the values of some of the variables are not necessarily human readable or understandable, potentially necessitating a toolchain-based mechanism to verify the provability of assertions having conditions that can be traced back to automatically generated program code.

FIG. 2A-2Billustrate methods200,210to process program code and determine static provability of assertion statements found therein.FIG. 2Aillustrates method200, which is a generalized method of evaluation that can be applied by embodiments described herein.FIG. 2Billustrates method210, which is a more specific method of evaluation, according to embodiments described herein. The operations of method200,210, and other methods described herein can be performed via processing logic that includes hardware (e.g. circuitry, dedicated logic, etc.), software (as instructions on a non-transitory machine-readable storage medium), or a combination of both hardware and software. Although sequential operations are illustrated, it should be appreciated that some of the operations described may be performed in a different order. Moreover, some operations may be performed in parallel rather than sequentially. Additionally, some operations may be indicated as optional and are not performed by all embodiments.

As shown inFIG. 2A, method200includes operation201, which processes, in an integrated development environment, a set of program code to identify an assertion statement. Method200further includes operation202, which determines the compile-time provability of a condition specified by the assertion statement. If method200determines that the condition specified by the assertion statement is compile-time provable, as shown at block203, the method200continues to operation204, which continues processing the set of program code. Otherwise, the method200can perform operation205to trigger a processing error. Method200can be performed by a compiler of an IDE or, in various embodiments, a static analyzer associated with the IDE or a combination of the compiler and static analyzer. In one embodiment, a static analyzer can analyze the set of program code during or in association with compilation of the program code by a compiler or compiler toolchain. In one embodiment, complex assertion statements can be divided into multiple portions, with some portions evaluated by the compiler and other portions evaluated by the analyzer. In one embodiment, a programmer can include compiler directives within program code that explicitly declares the truth of one or more portions of an assertion statement.

Method210illustrates operations that can be used to evaluate the static provability of assertion statements found in program code. Method210, in one embodiment, is used to determine the compile-time provability of the condition specified by the assertion statement, which is performed during operation202. As shown inFIG. 2B, method210includes operation211, which can be performed after operation201of method200. Operation211includes to semantically convert a condition specified by an assertion into a Boolean statement. Method210additionally includes operation212, to reduce the Boolean statement to an intermediate representation. The Boolean statement can include multiple expressions that may be able to be evaluated separately. For example, with reference toFIG. 1B, Boolean statement120includes an expression including a comparison (e.g., operation122). The second input124is an immediate having a constant value, while the first input123is a variable having a value dependent upon an expression126that includes a multiply operation126bhaving multiple inputs126a,126c.

Method210continues to operation213, to process the intermediate presentation to detect an expression that is non-constant at compile-time. In one embodiment, the presence of a non-constant expression within the evaluation chain for the assertion condition can be provided as input to block203, where method200determines whether or not the assertion statement is provable at compile-time. Specifically, if all values used to evaluate the condition are constant at compile-time, the assertion can be stated to be statically provable at compile-time. However, if one or more non-constant values are determined it still may be possible to statically prove the assertion depending on the types of operations that are performed during evaluation of the assertion condition.

FIG. 3A-3Billustrate methods300,310that can be used to evaluate the static provability of an assertion.FIG. 3Aillustrates a method300determining the provability of an assertion statement using an abstract syntax tree.FIG. 3Billustrates a method310of using expression specific rules to evaluate portions of an assertion.

As shown inFIG. 3A, method300includes operation301, which converts an intermediate representation of an assertion into an abstract syntax tree. Method300additionally includes operation302, which performs a depth-first search on the abstract syntax tree to locate a non-constant expression. Method300then proceeds to operation303, which includes, during the depth-first search, to traverse through to a leaf of the abstract syntax tree. Method300then proceeds to operation304. If method300determines that the leaf has a constant value at compile-time at operation304, method300then performs operation308, which proceeds to the next leaf. If method300determines that the leaf is non-constant at operation304, method300proceeds to operation305to determine if the Boolean truth of an expression to be evaluated is determinable with a variable value. Where the truth cannot be determined with a variable value, based on the expression to be evaluated, method300proceeds to operation205of method200, which triggers a processing error. Where operation305determines that the Boolean truth of the expression is determinable with a variable value, method300proceeds to operation306, which evaluates the expression based on characteristics of the expression. Characteristics of the expression include mathematical or logical characteristics associated with details of the expression, where those details include but are not limited to the operation performed by the expression and the data type of the variables within the expression and/or inputs to the expression.

As shown inFIG. 3B, method310includes operation311, which can be performed in association with operation306of method300. Operation311includes to configure evaluation rules based on characteristics of the expression to be evaluated. The evaluation rules can be configured based on mathematical or logical characteristics of rules associated with the expression. In one embodiment the characteristics include the operations associated with an expression, the data type of the variables within the expression, and mathematical and/or logical rules or constraints associated with the operations or data types within the expression. Based on the configured evaluation rules, operation312and313can be performed. Operation312includes evaluating variables within the expression according to evaluation rules for an operation associated with the set of variables. Operation313includes evaluating variables within the expression according to the data types of the variables.

During operation312, variable inputs of a given expression of a condition can be evaluated based on mathematical or logical rules associated with the operation. For example, for a multiplication operation, it can be determined that if one input is known to be zero, the output will be zero without regard to the other inputs. Additionally, multiplying any number by itself will result in either zero or a positive value. The output of some logical operations can also be determined even if one or more inputs are unknown. For a logical OR operation, if it can be determined that one input is true, then the output of the expression will be true without regard to other inputs. For a logic AND operation, if it can be determined that one input is false, then the output of the expression will be false, without regard to the other inputs. In one embodiment, method310can perform operation312in association with depth-first search of an abstract syntax tree generated based on the assertion expression. In such embodiment, method310can determine the operation or operations to be performed within an expression before traversing to the portion of the abstract syntax tree that includes the inputs to the expression. Method310can then dynamically configure the evaluation rules for the inputs based on the expression and evaluate the inputs once the inputs are read from the abstract syntax tree.

During operation313, variable inputs of a given expression of a condition can be evaluated based on the data type of each variable, as some data types can only hold a limited set of values. Depending on the number of bits associated with a data type of a variable, the minimum and maximum number that can be represented by the variable is known. Additionally, unsigned integer variables cannot natively store negative values.

Based on operation312and operation313, method310may be able to determine if the expression to be evaluated is provably non-constant during operation314. If the expression is non-constant, method310proceeds to operation316, which triggers an error. The error can be displayed via a user interface of an IDE and can identify the specific expression of the condition that has a value that cannot be statically determined. If the expression is determined to be constant (e.g., not non-constant) at operation314, method310can proceed to operation315, to determine if the evaluated expression is the last expression of the condition for the assertion. If the evaluated expression is not the last expression, method310proceeds to operation317, which evaluates the next expression in the condition. Once all expressions of a condition have been determined to be constant or constrained to the point that the expression can be evaluated in the context of the overall Boolean condition, method310proceeds to operation318, which allows the assertion statement.

Embodiments described herein primarily focus on determining whether the Boolean value associated with assertion statement can be statically proven at compile-time. In one embodiment, a further evaluation can be performed to specifically determine that the assertion statement can be statically proven to be true at compile-time. In one embodiment, an error can be triggered if the statement associated with an assertion statement can be statically proven, but is statically proven to be false, as an assertion statement that is provably false is almost certain to be unintended by the developer.

FIG. 4A-4Billustrate an IDE400and a system410to evaluate assertion statements using methods provided by embodiments described herein.FIG. 4Aillustrates an IDE400(integrated development environment) including assertion analysis logic.FIG. 4Billustrates a system410associated with the IDE400in which a compiler and analyzer can cooperate to analyze assertion statements within program code.

As shown inFIG. 4A, one embodiment provides an IDE400having an editor402, a modular compiler404, a static analyzer406, and an assertion analysis cache408. The modular compiler404includes an assertion module405that performs compile-time analysis of assertion statement for program code compiled by the IDE400. The static analyzer406also includes an assertion module407that can be used to analyze assertion statements during static analysis of program code edited within the IDE400. Analyzed assertion statements, or portions of assertion statements, can be stored in the assertion analysis cache408by either of the assertion module405of the modular compiler404or the assertion module407of the static analyzer406. Further operational details are illustrated by the system410ofFIG. 4B.

In one embodiment the IDE400includes a system410as shown inFIG. 4B. The system410includes software modules executable by processing logic described herein to analyze program code411that includes an assertion statement412. The assertion statement412can be detected within the program code411by the modular compiler404during compilation of the program code411or during analysis of the program code by the static analyzer406. The static analyzer406can analyze the program code independently or in conjunction with compilation by the modular compiler404.

In one embodiment, the system410provides support for program code411that is written in multiple programming languages. In such embodiment the modular compiler404includes multiple front-end compilers414A-414B, which can be configured to perform front-end compilation for the multiple programming languages of the program code411, where front-end compiler414A compiles program code written in a first programming language, while front-end compiler414B compiles program code written in a second programming language. Likewise, the static analyzer406can include analyzer front end426A, which is configured to analyze the first programming language, and analyzer front end426B, which is configured to analyze a second programming language.

For the modular compiler404, the front-end compilers414A-414B can convert the program code411to an intermediate language that is processed by an intermediate language processor415. The intermediate language processor415can communicate with the assertion module405, which is configured to analyze intermediate language representations of assertion statements412within the program code411. As the assertion module405is configured to analyze intermediate representations of assertion statements412, the assertion module can process assertion statements written in multiple programming languages. Likewise, the static analyzer406includes an analysis engine427coupled with an assertion module407. The analysis engine427can be configured to analyze an intermediate representation of the program code411, allowing multiple languages to be analyzed. The assertion module407can statically analyze an intermediate representation of assertion statement412, which can be written in one of multiple languages.

In one embodiment the assertion module405of the modular compiler404is configured to analyze assertion statements within specific modules or blocks or the program code411during compilation, while the assertion module407of the static analyzer406can be configured to perform analysis across multiple modules of the program code411. Furthermore, the assertion module407may be able to perform a more in-depth analysis of each assertion statement. For example, the analysis engine427of the static analyzer406can be configured as a source code simulator that traces multiple possible paths of execution. The simulation state of the program code411, including multiple possible values of variables and expressions within the program code411, can be stored within a software state database428. In one embodiment the analysis engine427can generate a potential control flow graph of the program code411, which can be used to analyze the potential paths of execution through the program code. The control flow graph can be used to perform operations such as a reachability analysis, to determine which portions of the program code may be executed through the multiple potential execution paths. Thus, in one embodiment, the analysis engine427can enable the assertion module407to perform a more thorough analysis of assertion statements within the program code, potentially at the expense of taking a longer amount of time to perform static analysis than the modular compiler404takes to compile the program code411.

In one embodiment, the assertion module405of the modular compiler404can work in concert with the assertion module407of the static analyzer. For example, the assertion module405can analyze an assertion statement412that has a condition and expressions that are limited to a single program code module (e.g., file, library, etc.), while the assertion module407can analyze an assertion statement412that has a condition or expressions that are based on input or variables that span multiple modules of the program code411.

In some embodiments, assertion module405and assertion module407can directly share information via shared memory buffers or inter-process communication messages. In some embodiments, the assertion module405and assertion module407can each store completed analysis for assertion conditions or expressions within the assertion analysis cache. The completed assertion analysis can be indexed in the assertion analysis cache408based on a symbol associated with the assertion statement or via a hash value that is generated based on the assertion statement or expressions of the condition of the assertion statement. In one embodiment, the analysis results for constituent expressions of an assertion condition can be indexed and stored separately, such that subsequent analysis of those same expressions can be bypassed and the analysis result can be loaded from the assertion analysis cache408by assertion module405and/or assertion module407.

In one embodiment, if the assertion module405determines that all assertion statements412in the program code411are statically provable, one or more back end compilers416A-416B can output compiled software420for one or more target platforms. If the assertion module405does not approve of all of the assertion statements, an error will be generated and displayed via the user interface of the IDE and compiled software420will not be generated. However, the static analyzer406may generate analysis results430that indicate whether each assertion statement412within the program code has been statically proven and can detail provability failures for multiple assertion statements412if multiple statements fail provability analysis. In one embodiment, the assertion module405of the modular compiler404can be configured to re-use the analysis of one or more assertion statements412that are contained within the analysis results430if the program code411has not been changed between the generation of the analysis results430and the compilation of the program code411by the modular compiler404.

In one embodiment, for example, where the program code411includes an assertion statement412that is a cross-module assertion statement that cannot be fully analyzed by the modular compiler404, and where the static analyzer406is not in use, it may be possible for a programmer to include a compiler directive413within the program code that explicitly assigns a value to a variable or expression, where the truth of such expression cannot be explicitly determined by the modular compiler404. During compilation, the assertion module405will assume the truth of statements provided by a compiler directive413. An example of the use of a compiler directive is shown in Table 1 below.

As shown in Table 1, an exemplary compiler directive on line 01 (#pragma assert (x>0)) can be used by a programmer to statically assert the truth of an expression. In one embodiment the directive asserted statement has local scope and, for example, may be limited to the program code file or module in which the directive is found. By using a directive to assert that the value of parameter x will always be greater than zero, the assertion module405,407will determine that the statement assert (Y>0) is statically provable, as Y=x*x.

In one embodiment, the compiler directive413can be replaced with an Assertion and Verification paradigm in which assertion statements are used to explicitly state the truth of certain conditions or variables and verification statements are used in place of the traditional assertion statement. For example, a programmer can assert that an expression or variable has a value and the assertion module405,407of the modular compiler404or static analyzer406will assume the truth of the asserted statement when processing the static provability of a later verify statement. An example of assertion and verification is shown in Table 2 below.

As shown in Table 2, in one embodiment the verify statement of line 04 is used as a global replacement of the assertion statement generally described herein. The assertion statement of line 02 can then be used to provide an expression that will be assumed to be true when verifying the static provability of a subsequent verify statement. In one embodiment, the assert and verify statements are processed such that the statements must be within the same scope, although not all embodiments are limited as such.

FIG. 5illustrates a method500to use cached assertion analysis during provability analysis of an assertion statement, according to an embodiment. Method500can be implemented by a modular compiler or static analyzer as described herein, such as the modular compiler404and static analyzer406ofFIG. 4A-4B.

In one embodiment, method500includes operation501, which identifies an assertion statement in a set of program code. Method500can then proceed to operation502, to assign an identifier to the assertion statement. Method500can then perform operation503, which determines if a provability analysis exists for one or more portions of the assertion statement based on the identifier. The identifier assigned by operation502can be a symbol associated with the assertion statement, a hash value generated based on the assertion statement, or a collection of hash values or symbols for the various constituent expressions of the condition asserted by the assertion statement.

Method500includes operation504, which determines whether a previous analysis exists. The previous analysis can be analysis that is cached within an analysis assertion cache or provided by a cooperating assertion module of a modular compiler or static analyzer. In one embodiment the previous analysis can be derived from analysis results output by a static analyzer. In one embodiment, the previous analysis can be provided by a compiler directive within program code. In one embodiment, where an Assertion and Verification paradigm is in place, the previous analysis for a verification statement can be based on an assertion statement, at least a portion which is being verified by a verify statement.

If operation504determines that a previous analysis exists, method500can proceed to operation505, which loads the existing provability analysis for one or more portions of the assertion statement. The loaded provability analysis can be for the entire condition of the assertion of for one or more expressions that are evaluated during the evaluation of the condition of the assertion statement. After operation505, method500can proceed to operation506, which performs provability analysis for any unanalyzed portions of the assertion statement. If previous results exist for the entire condition of the assertion statement, operation506can be bypassed. After operation506is bypassed or performed, method500can proceed to operation507to determine provability for the assertion statement based on current or previous analysis of the various portions of the condition of the assertion statement.

In one embodiment, where previous analysis is used, the previous analysis is valid only if the program code does not change. If any changes are made to the program code, the assertion analysis cache may be flushed. In one embodiment, the assertion analysis cache is flushed at the beginning of every compilation or analysis cycle even if the program code has not changed.

FIG. 6is a block diagram of a computing device architecture600, according to an embodiment. The computing device architecture600includes a memory interface602, a processing system604, and a platform processing system606. The various components can be coupled by one or more communication buses, fabrics, or signal lines. The various components can be separate logical components or devices or can be integrated in one or more integrated circuits, such as in a system on a chip integrated circuit. The processing system604may include multiple processors and/or co-processors. The various processors within the processing system604can be similar in architecture or the processing system604can be a heterogeneous processing system including processors that differ in instruction set architecture or microarchitecture. In one embodiment, the processing system604is a heterogeneous processing system including one or more data processors, image processors, audio processors, graphics processing units, or neural net processors.

The memory interface602can be coupled to memory650, which can include high-speed random-access memory such as static random-access memory (SRAM) or dynamic random-access memory (DRAM). The memory can store runtime information, data, and/or instructions are persistently stored in non-volatile memory605, such as but not limited to flash memory (e.g., NAND flash, NOR flash, etc.). Additionally, at least a portion of the memory650is non-volatile memory. The connection between the processing system604and memory interface602to the non-volatile memory605can be facilitated via the platform processing system606.

Sensors, devices, and subsystems can be coupled to the platform processing system606to facilitate multiple functionalities. For example, a motion sensor610, a light sensor612, and a proximity sensor614can be coupled to the platform processing system606to facilitate the mobile device functionality. Other sensors616can also be connected to the platform processing system606, such as a positioning system (e.g., GPS receiver), a temperature sensor, a biometric sensor, or other sensing device, to facilitate related functionalities. A camera subsystem620and an optical sensor622, e.g., a charged coupled device (CCD) or a complementary metal-oxide semiconductor (CMOS) optical sensor, can be utilized to facilitate camera functions, such as recording photographs and video clips.

In one embodiment, the platform processing system606can enable a connection to communication peripherals including one or more wireless communication subsystems624, which can include radio frequency receivers and transmitters and/or optical (e.g., infrared) receivers and transmitters. The specific design and implementation of the wireless communication subsystems624can depend on the communication network(s) over which a mobile device is intended to operate. For example, a mobile device including the illustrated computing device architecture600can include wireless communication subsystems624designed to operate over a network using Time Division, Multiple Access (TDMA) protocols, Global System for Mobile Communications (GSM) protocols, Code Division, Multiple Access (CDMA) protocols, Long Term Evolution (LTE) protocols, and/or any other type of wireless communications protocol, including 5G network protocols.

The wireless communication subsystems624can provide a communications mechanism over which a client browser application can retrieve resources from a remote web server. The platform processing system606can also enable an interconnect to an audio subsystem626, which can be coupled to a speaker628and a microphone630to facilitate voice-enabled functions, such as voice recognition, voice replication, digital recording, and telephony functions.

The platform processing system606can enable a connection to an I/O subsystem640that includes a touch screen controller642and/or other input controller(s)645. The touch screen controller642can be coupled to a touch sensitive display system646(e.g., touch screen). The touch sensitive display system646and touch screen controller642can, for example, detect contact and movement and/or pressure using any of a plurality of touch and pressure sensing technologies, including but not limited to capacitive, resistive, infrared, and surface acoustic wave technologies, as well as other proximity sensor arrays or other elements for determining one or more points of contact with a touch sensitive display system646. Display output for the touch sensitive display system646can be generated by a display controller643. In one embodiment, the display controller643can provide frame data to the touch sensitive display system646at a variable frame rate.

In one embodiment, a sensor controller644is included to monitor, control, and/or processes data received from one or more of the motion sensor610, light sensor612, proximity sensor614, or other sensors616. The sensor controller644can include logic to interpret sensor data to determine the occurrence of one of more motion events or activities by analysis of the sensor data from the sensors.

In one embodiment, the platform processing system606can also enable a connection to one or more bio sensor(s)615. A bio sensor can be configured to detect biometric data for a user of computing device. Biometric data may be data that at least quasi-uniquely identifies the user among other humans based on the user's physical or behavioral characteristics. For example, in some embodiments the bio sensor(s)615can include a finger print sensor that captures fingerprint data from the user. In another embodiment, bio sensor(s)615include a camera that captures facial information from a user's face. In some embodiments, the bio sensor(s)615can maintain previously captured biometric data of an authorized user and compare the captured biometric data against newly received biometric data to authenticate a user.

In one embodiment, the I/O subsystem640includes other input controller(s)645that can be coupled to other input/control devices648, such as one or more buttons, rocker switches, thumb-wheel, infrared port, USB port, and/or a pointer device such as a stylus, or control devices such as an up/down button for volume control of the speaker628and/or the microphone630.

In one embodiment, the memory650coupled to the memory interface602can store instructions for an operating system652, including portable operating system interface (POSIX) compliant and non-compliant operating system or an embedded operating system. The operating system652may include instructions for handling basic system services and for performing hardware dependent tasks. In some implementations, the operating system652can be a kernel or micro-kernel based operating system.

The memory650can also store communication instructions654to facilitate communicating with one or more additional devices, one or more computers and/or one or more servers, for example, to retrieve web resources from remote web servers. The memory650can also include user interface instructions656, including graphical user interface instructions to facilitate graphic user interface processing.

Additionally, the memory650can store sensor processing instructions658to facilitate sensor-related processing and functions; telephony instructions660to facilitate telephone-related processes and functions; messaging instructions662to facilitate electronic-messaging related processes and functions; web browser instructions664to facilitate web browsing-related processes and functions; media processing instructions666to facilitate media processing-related processes and functions; location services instructions including GPS and/or navigation instructions668and Wi-Fi based location instructions to facilitate location based functionality; camera instructions670to facilitate camera-related processes and functions; and/or other software instructions672to facilitate other processes and functions, e.g., security processes and functions, and processes and functions related to the systems. The memory650may also store other software instructions such as web video instructions to facilitate web video-related processes and functions; and/or web shopping instructions to facilitate web shopping-related processes and functions. In some implementations, the media processing instructions666are divided into audio processing instructions and video processing instructions to facilitate audio processing-related processes and functions and video processing-related processes and functions, respectively. A mobile equipment identifier, such as an International Mobile Equipment Identity (IMEI)674or a similar hardware identifier can also be stored in memory650.

FIG. 7is a block diagram of a computing system700, according to an embodiment. The illustrated computing system700is intended to represent a range of computing systems (either wired or wireless) including, for example, desktop computer systems, laptop computer systems, tablet computer systems, cellular telephones, personal digital assistants (PDAs) including cellular-enabled PDAs, set top boxes, entertainment systems or other consumer electronic devices, smart appliance devices, or one or more implementations of a smart media playback device. Alternative computing systems may include more, fewer and/or different components. The computing system700can be used to provide the computing device and/or a server device to which the computing device may connect.

The computing system700includes bus735or other communication device to communicate information, and processor(s)710coupled to bus735that may process information. While the computing system700is illustrated with a single processor, the computing system700may include multiple processors and/or co-processors. The computing system700further includes memory720, which may be random access memory (RAM) or other dynamic data storage device coupled to the bus735. The memory720may store information and instructions that may be executed by processor(s)710. Memory720may also be main memory that is used to store temporary variables or other intermediate information during execution of instructions by the processor(s)710.

The computing system700may also include read only memory (ROM)730and/or another data storage device740coupled to the bus735that may store information and instructions for the processor(s)710. The data storage device740can be or include a variety of storage devices, such as a flash memory device, a magnetic disk, or an optical disc and may be coupled to computing system700via the bus735or via a remote peripheral interface.

The computing system700may also be coupled, via the bus735, to a display device750to display information to a user. The computing system700can also include an alphanumeric input device760, including alphanumeric and other keys, which may be coupled to bus735to communicate information and command selections to processor(s)710. Another type of user input device includes a cursor control770device, such as a touchpad, a mouse, a trackball, or cursor direction keys to communicate direction information and command selections to processor(s)710and to control cursor movement on the display device750. The computing system700may also receive user input from a remote device that is communicatively coupled via one or more network interface(s)780.

The computing system700further may include one or more network interface(s)780to provide access to a network, such as a local area network. The network interface(s)780may include, for example, a wireless network interface having antenna785, which may represent one or more antenna(e). The computing system700can include multiple wireless network interfaces such as a combination of Wi-Fi, Bluetooth®, near field communication (NFC), and/or cellular telephony interfaces. The network interface(s)780may also include, for example, a wired network interface to communicate with remote devices via network cable787, which may be, for example, an Ethernet cable, a coaxial cable, a fiber optic cable, a serial cable, or a parallel cable.

In one embodiment, the network interface(s)780may provide access to a local area network, for example, by conforming to IEEE 802.11 standards, and/or the wireless network interface may provide access to a personal area network, for example, by conforming to Bluetooth standards. Other wireless network interfaces and/or protocols can also be supported. In addition to, or instead of, communication via wireless LAN standards, network interface(s)780may provide wireless communications using, for example, Time Division, Multiple Access (TDMA) protocols, Global System for Mobile Communications (GSM) protocols, Code Division, Multiple Access (CDMA) protocols, Long Term Evolution (LTE) protocols, and/or any other type of wireless communications protocol.

The computing system700can further include one or more energy sources705and one or more energy measurement systems745. Energy sources705can include an AC/DC adapter coupled to an external power source, one or more batteries, one or more charge storage devices, a USB charger, or other energy source. Energy measurement systems include at least one voltage or amperage measuring device that can measure energy consumed by the computing system700during a predetermined period of time. Additionally, one or more energy measurement systems can be included that measure, e.g., energy consumed by a display device, cooling subsystem, Wi-Fi subsystem, or other frequently used or high-energy consumption subsystem.

In addition, the hardware-accelerated engines/functions are contemplated to include any implementations in hardware, firmware, or combination thereof, including various configurations which can include hardware/firmware integrated into the SoC as a separate processor, or included as special purpose CPU (or core), or integrated in a coprocessor on the circuit board, or contained on a chip of an extension circuit board, etc.

It should be noted that the term “approximately” or “substantially” may be used herein and may be interpreted as “as nearly as practicable,” “within technical limitations,” and the like. In addition, the use of the term “or” indicates an inclusive or (e.g. and/or) unless otherwise specified.

In the foregoing description, example embodiments of the disclosure have been described. It will be evident that various modifications can be made thereto without departing from the broader spirit and scope of the disclosure. The specification and drawings are, accordingly, to be regarded in an illustrative sense rather than a restrictive sense. The specifics in the descriptions and examples provided may be used anywhere in one or more embodiments. The various features of the different embodiments or examples may be variously combined with some features included and others excluded to suit a variety of different applications. Examples may include subject matter such as a method, means for performing acts of the method, at least one machine-readable medium including instructions that, when performed by a machine cause the machine to perform acts of the method, or of an apparatus or system according to embodiments and examples described herein. Additionally, various components described herein can be a means for performing the operations or functions described herein.

Embodiments described herein provide an integrated development environment that includes a compiler and analyzer toolchain that evaluates assertion statements within program code. Assertion statements assert the truth of a Boolean condition, which may be a simple value or expression or may be a Boolean-logic composition of multiple values or expressions. The toolchain of the integrated development environment is configured to determine if the asserted condition of the assertion statement is statically provable at compile-time. A condition is statically provable if and only if every element of a composition of multiple values can be resolved to a constant value at compile-time, or the set of potential values of any non-constant values or expression within the condition can be determined to be sufficiently constrained.

One embodiment provides for a non-transitory machine-readable medium storing instructions to cause one or more processors to perform operations 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, and presenting an error condition in response to failing to determine compile-time provability of the condition specified by the assertion. Determining 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 detect an expression within the intermediate representation that is non-constant at compile-time. Failing to determine compile-time provability of the condition specified by the assertion includes detecting an expression within the intermediate representation that is non-constant at compile-time. In a further embodiment, failing to determine compile-time provability of the condition specified by the assertion additionally includes, in response to detecting an expression within the intermediate representation that is non-constant at compile-time, analyzing the expression based on evaluation rules configured based on a logical or mathematical characteristic of the expression and failing to determine a constraint on an output value of the expression that enables determination of compile-time provability of the condition specified by the assertion. If the output value of the expression can be sufficiently constrained to allow the overall condition of the assertion statement to be proven, the assertion statement will not trigger an error message. Compilation or analysis can then proceed to other statement.

In one embodiment the intermediate representation is an abstract syntax graph and the operations additionally include traversing the abstract syntax graph until detection of the value that is non-constant at compile-time. Traversing the abstract syntax graph can include performing a depth-first search to traverse the abstract syntax graph until a terminal graph node is discovered that is non-constant at compile-time, although other graph traversal methods can be used in other embodiments. Traversal of the abstract syntax graph can be immediately terminated in response to discovery of a non-constant terminal graph node, or the non-constant node can be further evaluated based on configured evaluation rules.

In one embodiment, the operations additionally comprise determining compile-time provability of the condition specified by the assertion, the condition associated with a symbol that is at least quasi-unique to 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 condition cache can include a list of previously evaluated graph traversals that have been found statically provably at compile-time. In one embodiment, the operations additionally comprise receiving a specified truth value for a predicate associated with a condition specified by the assertion and determining compile-time provability of the condition based on the specified truth value. The truth value can be a locally-scoped compiler directive (e.g., pragma) or can be received from a static analyzer module. In one embodiment, the truth value is included within program code that specifies a condition or expression that is to be assumed to be true upon subsequent evaluation of a program code statement that includes the specified condition or expression.

One embodiment provides for a data processing system comprising a memory to store instructions for processing and one or more processors to execute the instructions. 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, and presenting an error condition in response to failing to determine compile-time provability of the condition specified by the assertion, wherein determining 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 detect an expression within the intermediate representation that is non-constant at compile-time.

Other features of the present embodiments will be apparent from the accompanying drawings and from the detailed description above. Accordingly, the true scope of the embodiments will become apparent to the skilled practitioner upon a study of the drawings, specification, and following claims.