Expressive vs. permissive languages: Is that the question?

Static analysis is becoming mainstream, with mature bug-finding tools for C and Java, including products such as Coverity Prevent, Grammatech CodeSonar, and Fortify SCA. These products limit the level of “noise” (false warnings) inherent to such tools to a minimum. However, by carefully selecting those cases for which they report a problem, these bug-finders hide the fact that they are largely uncertain about the overall correctness of the program.

To see this, it is usually sufficient to lower the ranking threshold below which problems are not reported, which immediately returns an extremely long list of possible problems, representing only a fraction of all the potential problems. By “problem” here, I mean any software bug, whether it's an error possibly detected at runtime (leading to an exception) or a mismatch between the programmer's intent and the obtained behavior.

As a developer and user of such tools, I have tried many times to answer a recurring question that most users have: how can I make my program analyzable? To tell the truth, beyond a few tips on features to avoid and idioms to prefer, usually not much can be done because so many decisions are outside the control of the programmer and instead depend upon the features of the programming language itself.

Therefore, the real question is: which language should I choose to make my program analyzable? This can be rephrased as: what does a given programming language offer me “for free”? By free, I mean information available from the source code without further analysis-information that, although not strictly required to express functional behavior, nonetheless captures part of the programmer's intention. Because software analysis is always short of information about the programmer's intent, the information that comes “for free” in a programming language is the most valuable asset available to an analyzer. By this criterion, C ranks quite below Java, which ranks quite below Ada.

Of course, tools for all languages strive to recover missing information, but as layers of missing information pile up, tools struggle harder to recover higher layers. For example, tools that analyze programs in assembly language are largely limited to recovering only declared types and control-flow, whereas tools that analyze C programs more easily recover higher layers too, such as type-safety and memory-safety properties. Similarly, tools that analyze Java programs can often deduce integer ranges and non-nullity of pointers, in addition to the properties recovered from C programs. Tools that analyze Ada programs are best at also recovering “function contracts,” the ultimate goal in software analysis, because so much of this free information is available.

A function contract is made up of a precondition that a caller of the function should satisfy prior to the call and a postcondition that the function should satisfy prior to returning. While user-defined contracts have appeared initially in some pioneering languages (especially Eiffel), they're now available in various widely recognized environments, for example in the .NET platform (Code Contracts) and the GNAT GCC compiler for Ada. Internally, many analyzers are based on generated contracts, also called function summaries , that they compute during the analysis.

I said contracts are the ultimate goal because complete contracts allow analyzing each function in isolation, much like function signatures allow separate compilation. However, only one programming language, SPARK, has gone as far as to require contracts from the programmer. So, in the general case, it's up to the analyzer to generate the contracts.

Now two aspects of a programming language define how much “free” information it provides: expressiveness and permissiveness. Often, these two dimensions are confused, since they both seem to refer to the ability to express the programmer's intent in many different ways. But with analysis in mind, they have quite different meanings, one supporting analysis while the other undermines it.

A language is expressive when it allows a programmer to easily convey his/her intent, with errors detected early. In contrast to assembly languages, C allows one to constrain variables to hold values from specific types, so it is more expressive here. In contrast to C, Java allows to test if a value is within the length a.length of an array a, so it is more expressive here. Contrary to Java, Ada allows one to constrain scalar variables to hold values from specific ranges, so it is more expressive here.

A language is permissive when it allows constructs that interfere with a program's reliability or readability. This degree of permissiveness can be controlled through strong semantics and restrictions. In contrast to assembly languages, C provides structured control-flow statements (if-then-else, loops) and it prevents arbitrary jumps to and from functions, so it is less permissive here. In contrast to C, Java provides default-initialization to null for pointers and prevents conversions between pointers and integers, so it is less permissive here. In contrast to Java, Ada provides modes (in/out/in-out) for subprogram parameters and it detects integer overflows in computations, so it is less permissive here.

A simple example in C/Java/Ada
To see how a more expressive and less permissive language helps in analyzing a piece of software, consider a very simple example in which a function allocates an array of N structures, where N is the number of available processors defined in some configuration.

Listing 1 illustrates straightforward implementations of this functionality in C, Java, and Ada, where I don't detail the types of structures for processors (Proc ) and configurations (Config ).


Click on image to enlarge.

Although each of these implementations is correct when used appropriately, it's still possible that errors occur during the execution of each one, due to the failure of the caller to set up an appropriate environment.

In each case, there might not be enough memory left for the allocation to succeed. In C, malloc returns 0 and the function exits. In Java, an exception OutOfMemoryError is thrown. In Ada, an exception Storage_Error is raised. Notice that in Ada, the maximum number of processors (64) is precisely given by the type Proc_Number , while in C and Java the type of num_proc is a predefined integer type, whose maximal value might be huge.

In each case, the field num_proc may be uninitialized, which results in an arbitrary allocation size being picked.

In C and Java, conf might be a null pointer, in which case the access to its field num_proc fails. In C, a segmentation fault is usually reported. In Java, an exception NullPointerException is thrown. In Ada, the parameter is not passed as a reference at the level of the source text, although the compiler may decide to do so for efficiency, so the possibility of a null reference doesn't arise.

In C, the computation of the size to allocate in bytes may overflow, which results in a very small array being allocated instead of a very large one. This is a common source of security attacks, as an otherwise valid array access may then write beyond the bounds of the array. In Java and Ada, the runtime makes sure there is no overflow here.

In C, conf might be an invalid pointer, either because it was never initialized or because the location it pointed to was freed or went out-of-scope. This usually results in hard-to-diagnose arbitrary behavior depending on the compiler and the program. In Java and Ada, language rules ensure that pointers are default-initialized to null .

Summarizing these findings, this makes a total of five possible errors in C, three in Java, and two in Ada. All this for a very simple function! Now replicate this effort for large functions with complex interactions, and you get C and Java programs that resist the analysis compared with the equivalent Ada programs.

Now, what else do these programs give for free for the analysis from the caller's point of view? In C, the type of the result of alloc_processors is a pointer, which may or may not be initialized, which may or may not be null, which may or may not be pointing to some valid memory. In Java, the type of the result of AllocProcessors is a pointer which may or may not be null. In Ada, the type of the result of Alloc_Processors is a non-null pointer, which may only be initialized to some non-null valid value. Also in Ada, the mode in for parameter Conf informs us that whatever is passed as Conf argument is not modified by calling Alloc_Processors .

This code snippet corresponds to real cases that I encountered repeatedly when searching for security integer overflow bugs in a large Microsoft code base in 2009, using an internal Microsoft analyzer called PREfix. Since this code base was in C, I usually had to rely on variable naming to decide whether or not a possible integer overflow detected by the tool introduced a security hole: while num_proc was not likely to be very large or controlled by an attacker, num_connections could legitimately be. Such reliance on naming schemes for detecting security breaches is unfortunately the best one can do in many cases with a language such as C.

Integers and pointers
The previous example made use of two critical types in programming languages: integers and pointers. It's not surprising that the degrees to which a programming language is expressive or permissive are for a large part tied to the way they treat integers and pointers.

Consider first integers. In most programming languages (C, C++, Java, C#), a direct mapping occurs between integral types defined in the language and machine integers. This is a source of tricky bit-vector manipulations, where either shifting is synonymous for dividing or a negative quantity might as well be positive (or both). In other languages, integers have the mighty power of mathematics, not being bounded by any sensible quantity, not even the number of atoms in the universe.

Both the machine view and the mathematical view lead to hard-to-analyze software. Integers in programs are quantities, neither bit-vectors nor abstract numbers. For the purpose of analysis, quantities should be appropriately bounded, which corresponds to having a valid range for those integral types, and letting users decide these bounds as they see fit.

This is the case in Ada. Being expressive, Ada lets the programmer define integer types and constraints. Not being permissive, Ada requires the use of compatible types in expressions, or else that appropriate type conversions are added.

Consider now pointers. In most programming languages, there is a unique kind of pointer that serves all purposes, leading to well-known programming hazards. In C, a pointer may refer to stack locations or heap locations, to a single reference or an array or even part of an array. In Java, a reference may refer to objects with very different lifetimes and it may be null.

In Ada the notions of references, arrays, access types, and addresses are carefully distinguished and may be further subdivided according to their use. A reference is of mode in when the corresponding procedure may only read from it; it is of mode out when the corresponding procedure may only write to it; it is of mode in-out when the corresponding procedure may read and write from it. An access type defines a storage pool in its scope, so that pointers of different access types cannot alias, even if they point to the same underlying type. An access type may be marked as non-null, in which case no value of such a type may be null.

I could say much more about the degree of refinement with which Ada treats integers and pointers that makes this language both more expressive and less permissive, but the point should be clear already.

Function contracts
One language, SPARK, is more expressive and less permissive than Ada. Not surprisingly, it's partly built on Ada. SPARK consists in a subset of Ada, with stronger semantics and restrictions, together with contracts expressed as stylized Ada comments, so that a regular Ada compiler can compile SPARK code. While Ada was designed to facilitate program analysis, SPARK was designed to facilitate program verification.

SPARK contracts allow one to express data-flow (global annotation expressing reads and writes of global variables), information-flow (derives annotation), preconditions (pre annotation), and postconditions (post annotation), as the example code in Listing 2 shows.


Click on image to enlarge.

This contract specifies that procedure Linear_Search reads and writes the global variable Counter , that the value of each of its outputs (both out parameters and Counter ) depend upon the value of all its inputs (both in parameters and Counter ), that the procedure shall only be called when Counter is not the maximal integer value and that when the procedure returns with Found being true, the Value searched is indeed at the output Index in the input Table , while the Counter has been incremented with respect to its initial value at procedure entry (denoted Counter~ ).

Analyzers for SPARK allow one to completely prove, statically, that such a contract is respected by the procedure's body, and that there are no runtime errors during its execution. For example, SPARK semantics and restrictions make sure that all reads of uninitialized values are caught by the analyzer, and dynamic allocations are not allowed, so that the errors on the Ada program Alloc_Processors are not possible in SPARK.

Because of these restrictions, SPARK may not be suitable in all contexts. Still, reliance on function contracts may be valuable for other programming languages:

  • Contracts make it possible to analyze a library or a program that uses a library for which you do not have access to the source code;
  • Contracts allow to split the analysis in many small independent ones, which will be collectively much cheaper to run, not mentioning the possibility of running them in parallel on a multicore multiprocessors machine;
  • Contracts allow to split the analysis in many small independent ones, which will be collectively much cheaper to run, not mentioning the possibility of running them in parallel on a multicore multiprocessors machine;
  • Since contracts allow the verification of individual functions, much more powerful techniques may be used, such as the SAT-based exploration performed in modern SMT-provers.

In fact, various analyzers propose their own language extensions for C and Java to make up for what these languages are missing, for example, non-null annotations for Java pointers in Findbugs, in/out modes for C parameters in Splint, size annotations for C array parameters in PREfix, and so forth. These language extensions are mostly user-friendly ways of adding limited function contracts to the language.

As exemplified by SPARK, contract-based analysis is the most direct way to make software analysis as pervasive as compilation in some near future, in particular when associated to a programming language suitable for analysis, being both more expressive and less permissive.

Improving confidence
Applying static analysis to software is a sure way to improve on software correctness, as we do find and correct bugs along the way. When all bugs found have been corrected and the tool returns no more (true) warnings, it remains to be seen if that increases our confidence that the software is correct.

The answer depends more on the programming language chosen than on the tool used or the program analyzed. Indeed, programming languages are far apart when it comes to features that facilitate analysis. Ada and SPARK are languages that are both more expressive and less permissive than C and Java, which greatly facilitates analysis.

According to a study reported in 2003 by Andy German on military systems varying in size from 3,000 lines of code to 300,000 lines of code, these languages are also those in which programmers make less errors, four per thousand lines on average for SPARK, between 4.8 and 50 per thousand lines for Ada, between 12.5 and 500 (sic) per thousand lines for C.1 For further reading, John Barnes' introduction to Ada 2005 gives much insight into why more expressive and less permissive programming languages lead to better software.2

Yannick Moy is a senior software engineer at AdaCore, where he is an expert in software source code analyzers that are used to detect defects or verify safety/security properties. Moy previously worked on source analyzers for PolySpace (now The MathWorks), INRIA Research Labs, Orange Labs, and Microsoft Research.

Endnotes:
1. German, Andy. “Software Static Code Analysis Lessons Learned,” CrossTalk , November 2003.

2. Barnes, John. “Safe and Secure Software,” 2008, www.adacore.com/2008/04/08/gem-30/.

1 thought on “Expressive vs. permissive languages: Is that the question?

  1. @Parkgate: Certainly it is worth using any tool like Splint which can statically detect bugs. However, “it is free” is not true in practice: any static analysis tools requires some adaptation to be effective in your context, and this depends on your codeba

    Log in to Reply

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.