ellipsis-interface.h File Reference

Wrap function declarations such that they provide pre- and post-conditions. More...

Go to the source code of this file.

Macros
#define	ellipsis_invariant(COND, MESSAGE)
#define	ellipsis_postcondition(COND, MESSAGE)
#define	ellipsis_precondition(COND, MESSAGE)
#define	EXBINDING(NAME)
#define	INBINDING(NAME)

Detailed Description

Wrap function declarations such that they provide pre- and post-conditions.

This is a mechanism that is unfortunately not too easy to use, but does its job. Suppose you want to have a function interface

double* minP(double* a, double* b);

that returns the pointer to the object with the minimum value. With C++'s contracts I would like to add pre- and postconditions to that

double* minP(double* a, double* b) pre(a) pre(b) post(r: (r ≡ a) || (r ≡ b));

That is, I want an assertion such that both pointers are non-null on entry and that the return value also is not null and equal to one of both pointer values. With some extensions that we have in eĿlipsis, we can formulate an inline interface of such a function as follows.

inline
double* minP(double* a, double* b) {
   DEFER_TYPE(double*);
   ellipsis_contract_assert(a);
   ellipsis_contract_assert(b);
   defer { ellipsis_contract_assert((defer_return_value ≡ a) || (defer_return_value ≡ b)); };
   extern typeof(minP) minP_Inner;
   return minP_Inner(a, b);
}

The private function minP_Inner would then implement the feature itself, basically what usually would just be the definition of the function minP.

Cooking up such interfaces manually has two disadvantages:

• The pre-condition is not transferred to the callee minP_Inner, so optimization opportunities arising from this information can not be used within the implementation of minP_Inner.
• The post-condition is asserted in the caller. So since the caller has no information what the callee does, this assertion will be checked at each call site. Also, most information about the post-condition is present in minP_Inner, so ideally it would be asserted there, or even omitted if it can be deduced statically.

By using this header here, you may write the above inline function a bit differently such that these disadvantages are avoided:

inline
double* EXBINDING(minP)(double* a, double* b) {
   DEFER_TYPE(double*);
   ellipsis_precondition(a);
   ellipsis_precondition(b);
   ellipsis_postcondition((defer_return_value ≡ a) || (defer_return_value ≡ b));
   extern typeof(EXBINDING(minP)) INBINDING(minP);
   return INBINDING(minP)(a, b);
}

The first minor feature that you can see here is that the use of EXBINDING and INBINDING spares you from inventing your own naming scheme for the externally visible identifier and the internally visible one.

The real strength of this approach comes from the pseudo-macros ellipsis_precondition and ellipsis_postcondition which result in different checks within the external interface and the internal implementation.

• A precondition is (as before) asserted by the caller but additionally the same condition is added as an assumption to the callee. That is, the information that the precondition has been checked when the body of the function is reached is transferred to the definition of the callee. The compiler can use that information to optimized the function body.
• A postcondition is transferred as an post-assertion to the callee. So there it can be checked efficiently at the end of the function body with all information about the function at hand. If the condition can be checked statically at compile time the whole assertion can be optimized out. On the other end, the postcondition is replaced by a post-assumption in the caller (the inline function). Thereby the code after the function call knows that the post-condition without having to check it again.

Ideally, this will lead to an inline function with the following properties:

• preconditions are asserted by the caller. Any deduction of the condition inside the caller can lead to optimization opportunities, in particular in many cases the assertion does not need to be checked at all.
• preconditions are know to hold as assumptions in the callee and can be used to optimize, there.
• postconditions are asserted by the callee, so all information present there can be used to optimize.
• postconditions are know to hold as assumptions after the function call can be used to optimize, there.

The implementation of all of this is a bit tedious still, but working. If your function is to live in mininmal.h (for the declaration) and minimal.c (for the definition) you would have to create two auxiliary files, minimal-interface.h and minimal-implementation.c. In the first you'd place the inline function as given above (with EXBINDING etc) and in the second you'd place the function definition; you'd just also have to put EXBINDING around the function name:

double* EXBINDING(minP)(double* a, double* b) {
 ... your implementation goes here ...
}

In your minimal.h header file you place a special include

#include_source <ellipsis-interface.h> __prefix__(bind HEADERFILE minimal)

and in your minimal.c header file you place a special include

#include_source <ellipsis-implementation.h> __prefix__(bind HEADERFILE minimal)

Here the first would include the file minimal-interface.h several times to create different kind of inline wrappers. The second would include minimal-implementation.c and also minimal-interface.h to propagate the pre- and postconditions to the defined functions.

Remarks

For both includes, the naming (endings in -interface.h and -implementation.c) is crucial.

There is no ABI change: the object file that is produced for the function symbol itself (here minP) is binary compatible with any other implementation that does not use pre- or postconditions.

Evidently this only works if you use eĿlipsis as a preprocessor, either in one go (e.g using the compiler wrapper ellipsis-gnuc.sh) or by producing an intermediate preprocessed source.

See also

ellipsis-implementation.h

ellipsis-contracts.h

Macro Definition Documentation

ellipsis_invariant

#define ellipsis_invariant	(		COND,
			MESSAGE
	)

A condition COND that is a pre- and a postcondition.

The second, optional, parameter is a string literal that should provide information for the case that the condition COND does not hold.

See also

ellipsis_precondition

ellipsis_postcondition

Warning

only use in the context of ellipsis-interface.h.

This macro may not be undefined or changed otherwise

ellipsis_postcondition

#define ellipsis_postcondition	(		COND,
			MESSAGE
	)

A postcondition that is checked (compile time if possible otherwise runtime) in the context of the called function after the body of the function has been run, before a return to the caller.

The second, optional, parameter is a string literal that should provide information for the case that the condition COND does not hold.

After the call, it will be assumed, that the condition holds.

Warning

only use in the context of ellipsis-interface.h.

This macro may not be undefined or changed otherwise

ellipsis_precondition

#define ellipsis_precondition	(		COND,
			MESSAGE
	)

A precondition COND that is checked (compile time if possible otherwise runtime) in the context of the caller before entering the body of the function.

The second, optional, parameter is a string literal that should provide information for the case that the condition COND does not hold.

In the body of the function, it will be assumed, that the condition holds.

Warning

only use in the context of ellipsis-interface.h.

This macro may not be undefined or changed otherwise

EXBINDING

#define EXBINDING

(

NAME

)

The external name of a contracted function.

Warning

only use in the context of ellipsis-interface.h and ellipsis-implementation.h

This macro may not be undefined or changed otherwise

INBINDING

#define INBINDING

(

NAME

)

The internal name of a contracted function.

Warning

only use in the context of ellipsis-interface.h and ellipsis-implementation.h

This macro may not be undefined or changed otherwise