Re: Idea: Array Boundary Checks on Write Access Only

[Peter Amey <pna@praxis-cs.co.uk>]

Markus Kuhn wrote:
> 
> Here is a suggestion for Ada compiler developers:
> 
> Add a compiler configuration option that suppresses array index
> boundary checks only for *read* access to array elements.
> 
> Array boundary checks in Ada are a major advantage over C/C++
> and add a lot to the safety and debugability of the language.
> However the checks are also a significant performance loss
> unless they are deactivated. A useful compromise would be an
> option that causes the compiler to add boundary checks only
> when an array element is written, but not when it is read.
> Out-of-boundary array write accesses are dangerous because they can
> destroy other data structures and can cause failure inside completely
> unrelated objects. Therefore, in security critical applications,
> it is very desireable to deactivate for performance reasons
> only the checks for the less dangerous read accesses that if
> they go wrong should not cause malfunction within other objects.
> 
> Are there already Ada compilers around that do this?
> 
> Markus

Working in the safety-critical, real-time field I frequently encounter the 
tension between the need for checking and the desire for speed.  Another 
factor is the need to generate very high levels of object-code test coverage 
to satisfy some regulatory regimes; this is rather hard if the compiler has 
inserted run-time checks that in practice are unncessary and therefore 
cannot be externally stimulated.  In this environement I am not very happy 
with the idea that reading out of bounds is any less unsatisfactory than 
writing: both show that the code is broken and may misbehave.  

It was to square this particular circle that we invested so much effort in 
the proof of absence of run-time errors facility in SPARK (Markus, I know 
you are familiar with this...).   Having conducted a proof that code is 
exception free it is possible to turn compiler-generated checks off with a 
clear conscience and get the benefit of smaller, faster code as a bonus.

Peter

-- 
--------------------------------------------------------------------------- 
  
      __         Peter Amey, Product Manager
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/
 --------------------------------------------------------------------------