From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,8a4455177648cb9e
X-Google-Attributes: gid103376,public
From: Markus Kuhn <Markus.Kuhn@cl.cam.ac.uk>
Subject: Re: Idea: Array Boundary Checks on Write Access Only
Date: 1998/06/18
Message-ID: <3588D738.4BB32E5A@cl.cam.ac.uk>#1/1
X-Deja-AN: 363799014
Content-Transfer-Encoding: 7bit
References: <35851B64.5BF271C4@cl.cam.ac.uk> <6m8v02$r2l$1@xenon.inbe.net>
Content-Type: text/plain; charset=us-ascii
Organization: Cambridge University, Computer Laboratory
Mime-Version: 1.0
Newsgroups: comp.lang.ada
Date: 1998-06-18T00:00:00+00:00
List-Id: <comp.lang.ada>


Lieven Marchand wrote:
> About the only commonly used case that most compilers don't handle is
> where you put in the check yourself.

It would be really neat if Ada compilers would keep track not only of
the declared range of a subtype, but also of the effectively possible
range of Integer variables inside a certain program fragment as part
of the flow analysis.

For instance in code such as

  if J > 0 then
     -- compiler notes that here J : range 1 .. J'Last
     if I > J then
        -- compiler notes that here I : range 1 .. I'Last

then the compiler should know that inside the second "if" I > 0 always
holds. This need not be a full blown automatic proof system, just some
logic that understands simple inequalities and monotonic expressions
and that keeps track of the effective maximum and minimum value
of integer variables and supresses most checks accordingly.

It would then also be a nice option if the compiler would be
able to dump a list of all the checks that it still had to insert
to give developers a clue of whether they can by intelligently
placing a manual check at the right place make a large number
of automatically inserted less efficient checks unnecessary.

Markus

-- 
Markus G. Kuhn, Security Group, Computer Lab, Cambridge University, UK
email: mkuhn at acm.org,  home page: <http://www.cl.cam.ac.uk/~mgk25/>