Preconditions — Part IV

This is the last post about preconditions. We will try to address concerns about a potential UB connected with expressing preconditions. We will also try to explore how language support for preconditions could look like.

Preconditions and UB-safety

The definition of a precondition I have been trying to advertise somehow threatens us with lots of potential UB situations. You may feel as though I was encouraging you to plant more and more UB. So let me explain myself.

Let’s consider a project where you prefer that whatever wrong happens in the program ‘module’, you want this to be reported via an exception: never crash or stop or enter a UB. One example of such situation is where you have written a server, which is executing tasks: pieces of code written by different users that you have no control over. But you do not want the server to crash only because one of the users has a bug in his code, in his task/module. You want that module to throw exceptions upon any failure; even if that failure is caused by a bug. Another such example is where you do batch job which consists of doing thousands of similar small tasks. The entire process runs for a week. You do not want the failure in one task to stop the entire job (in case UB ends in a crash). You want to skip that task and to proceed to the next one. You are willing to take the risk of entering a UB and having the program do random, uncontrolled things. We will refer to such situation as “no-halt guarantee”.

Before we address the UB concern; if you require the no-halt guarantee, answer this question. In such projects, do you use std::vector’s operator [] or do you dereference raw pointers? Both these operations provide a precondition: vector’s index must be in range; dereferenced pointer must point to a valid object — at minimum it must not be null.

If your answer to this question is “I am not using these”, you probably do not require a language that works ‘close to metal’, and you could use a language based on some virtual machine, which leaves almost no room for a UB at the cost of reduced performance. Such languages do not require preconditions, because the behaviour is always defined. Somewhat simplifying things, C++ provides UB to allow maximum uncompromised run-time efficiency. The ‘UB way’ helps avoid situations where the same ‘precondition’ is checked multiple times for safety. Preconditions described in this series of posts are a generalization of this ‘UB way’ for user defined functions.

If your position is “I am forced to use vector and raw pointers, but for anything else I want a no-UB style”, then quite possibly the preconditions is not the feature for you. Going back to the example from Part III, for the division operator of type BigInt, what should happen if the divisor is 0? If you require a guarantee that the function throws on zero divisor, your division is well-defined for the zero divisor: it is well-defined what is going to happen. This means there is no precondition. Paper N3248 calls such situation a wide contract: any function input is valid. In the case of BigInt, it spoils the mathematical abstraction, but at least provides the no-halt guarantee.

So who needs these preconditions? First, above we only described one possible trade-off between factors like program correctness, efficiency and no-halt guarantee. There are other valid trade-offs. C++ is often used in applications where performance is the top priority. You want to avoid the situation of redundant safety checks: repeated checks for the same condition.

Also, the arguments in favour of using preconditions might become stronger if we had language support for preconditions and compiler which would understand them and could help us find bugs in the code. Below we try to show how such support could look like.

One thing that I want to point out is that just checking every possible “invalid function input” and throwing an exception on it does not necessarily make the program more correct or safe. It only prevents crashes, but not bugs. Bugs, in turn, are a sort of UB on the higher level of abstraction.

A potential language feature

The thing I describe in this section is more like a fantasy. I have never seen a feature like this, although it looks to me it is implementable.

So, how would an ideal support for preconditions look in C++? This would be a facility for helping the compiler in the static analysis of the program code. This would be somewhat similar to how the function argument type checking works. Declaration like:

void fun(string s);

guarantees two things. The compiler will enforce that the callers always pass the argument that is a string. Inside the function, we are guaranteed that the value of s will always contain a valid string. Am I saying too obvious things? Note that some scripting languages do not offer this compile-time guarantee.

How would that work for preconditions? The mechanism would also be twofold. The compiler would verify (as much as possible) if the caller satisfied the precondition. Inside function body, it could apply code optimizations based on the assumption that the precondition holds.

Let’s see how it works by example. We will use fairly well-familiar libraries: Boost.Optional and std::function. Consider the following function.

void apply(function<void(int)> f, optional<int> i)
{
  f(*i);
}

Consciously or not, we made certain assumptions about the states of i and f. You probably do not want to dereference i if it has not been set with an integral value. Similarly, you probably do not wont to invoke f if it has been default-initialized, without any function that could be called.

Accessing the value contained inside optional<int> has a precondition. If we had preconditions in C++ the operation could be declared as:

template <typename T>
T& optional<T>::operator*()
precondition{ bool(*this) };

Optional does not verify the precondition, because it assumes you already made sure it holds, and it does not want to duplicate the check. You should check the precondition not because of “safety issues” but because of the business logic of your program.

In contrast, note that invoking default-constructed std::functions is well defined. It is guaranteed to throw exception of type std::bad_function_call. There is no precondition here. if we wanted to make it very explicit, we could write:

template <typename R, typename... Args>
R function<R(Args...)>::operator()(Args... args)
precondition{ true };

In C++11 our function apply compiles fine, and works somehow. We have to be careful what we pass to it, but — what is important now — it compiles. With the hypothetical support for preconditions this function would not compile, or at minimum, the compiler would issue a warning message (which you can turn into an error with compiler switches). The message would indicate that we attempted to use a function (operator*) but it cannot be guaranteed that its precondition would always hold. This would be an indication to the programmer that he needs to change something about this code, so that a reasonable guarantee is given. He could do it in a couple of ways.

First, — and this is least preferred way because it usually hides a more serious logic error — we can just check for the precondition using an if-statement:

void apply1(function<void(int)> f, optional<int> i)
{
  if (i) {
     f(*i); // ok
  }
}

Static analyser can be sure that the precondition is satisfied. We are inside the branch that is guarded by expression that is exactly our precondition. Object i has not been modified between the check and the invocation of operator*. Note that expression bool(i) that we are implicitly invoking is also a function whose precondition, in general, should be checked. However, bool(i) has a wide contract (has no precondition).

Second, we can rely on other function’s postcondition. Here, we are changing the semantics of the function significantly, but the goal is to provide you with the overview of the feature.

void apply2(function<void(int)> f, optional<int> i)
{
  i = 0;
  f(*i); // ok
}

Optional’s assignment from T (int in our case) has a postcondition. The function would probably be defined as:

template <typename T>
optional& optional<T>::operator=(T&&)
postcondition{ bool(*this) };

If preconditions are supported, postconditions will likely be supported as well. In function apply2, the function that most recently modified i (the assignment) guarantees that it leaves the object in the state that meets predicate bool(i). This is the predicate that is exactly required by operator*. Analyser should be able to detect that. For a more practical example consider that algorithm std::sort propagates a property (its postcondition) std::is_sorted to functions like std::binary_search.

Let’s try to modify our function, so that it is closer to the original:

void apply2(function<void(int)> f, optional<int> i)
{
  if (!i) { i = 0; }
  f(*i); // ok
}

If the expression inside the if-statement were bool(i) the analyser could make some conclusions. But how is it supposed to know that expression !i is a compliment of bool(i)? We would need to have a yet another language feature to be able to express ‘relationships’ between predicates, or expressions in general. A language like this has already been considered for C++ in form of concept axioms. With axiom syntax (as described in “Design of Concept Libraries for C++”) we could express the relation as:

template <typename T>
axiom(optional<T> o)
{
  !o <=> !bool(o);
}

This reads that for each object o of type optional<T> expression !o is equivalent to expression !bool(o): one can be substituted for the other without affecting the program’s semantics.

Once the static analyser is taught this equivalence, it can transform the body of apply2 to:

  if (!bool(i)) { i = 0; }
  f(*i); // ok

and then to:

  if (bool(i)) {} else { i = 0; }
  f(*i); // ok

From the last one (if this is not already obvious from the previous) it can gather that either the precondition is already satisfied, or we call the assignment that guarantees our precondition as its postcondition.

Third option to silence the “potentially broken precondition” warning is to declare your own precondition:

void apply3(function<void(int)> f, optional<int> i)
precondition{ bool(i) }
{
  f(*i);
}

Now, the verification of the precondition is moved to the higher level. This would usually be the preferred way of handling the preconditions.

Last, although it is not very elegant, it will often be useful to locally disable the precondition check:

void apply4(function<void(int)> f, optional<int> i)
{
  [[satisfied(bool(i))]] f(*i);
}

Here satisfied is an attribute that tells the compiler/analyser that it should assume the precondition holds, even though it cannot verify it. It says “trust the programmer.” While not very safe, it is useful when migrating the legacy code, when we cannot afford to set all precondition checks right in one go.

This also shows a model usage of attributes. Attributes in C++ have a limited usage compared to other languages. Their addition or removal must not affect the semantics of the program. Their addition or removal must not render a valid program invalid. They can be used to give hints to the compiler. Turning warnings on and off is a good example of such hint.

Note that f does not get this additional compiler safety check, because it does not specify a precondition. The decision for std::function’s operator() was to avoid any UB, and be well defined when it is default-constructed.

Thus described functionality makes preconditions similar to concept axioms. Also, similarly to axioms, compilers and other tools can make use of the assumptions expressed in preconditions and optimize the code based on them. In places where static analysis cannot be performed, concepts would still render run-time checks. Such checks would still be superior to manually planted asserts inside function body for a couple of reasons:

1. Preconditions would be evaluated in the caller rather than inside the function. This way core dumps or other diagnostic tools would correctly report that the error is in the caller.
2. All preconditions can be globally enabled or disabled even in third party precompiled code, without the necessity to recompile each function with narrow contract (with preconditions). N1800 describes how it works.
3. Compiler can easily detect and warn us if predicates in preconditions have side effects.
4. constexpr functions evaluated at compile-time could make use of preconditions and report failures at compile-time also.

Such a support for preconditions would be a very helpful feature. But let’s not fantasize too much. For now the best thing we can do is to use assertions and comments — a very useful and often underestimated language feature.