Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83 (MC840302); site boring.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!mit-eddie!genrad!panda!talcott!harvard!seismo!mcvax!boring!steven
From: steven@boring.UUCP
Newsgroups: net.lang
Subject: Re: levelheight: automatic "nil pointer" handling
Message-ID: <6304@boring.UUCP>
Date: Fri, 1-Feb-85 09:37:42 EST
Article-I.D.: boring.6304
Posted: Fri Feb  1 09:37:42 1985
Date-Received: Sun, 3-Feb-85 09:52:41 EST
References: <6881@watdaisy.UUCP> <611@spuxll.UUCP>
Reply-To: steven@boring.UUCP (Steven Pemberton)
Organization: CWI, Amsterdam
Lines: 83
Apparently-To: rnews@mcvax.LOCAL

In article <611@spuxll.UUCP> ech@spuxll.UUCP writes:
> It is most certainly NOT possible to statically (i.e. at compile time) check
> for nil-pointer dereferencing.  To use a somewhat classical argument, suppose
> I have a subroutine that emulates a turing machine for one step each time it
> is called; if the TM halts, it sets a given pointer to a particular value,
> otherwise it leaves it nil.
You can use the same argument to prove that strong typing is impossible.

> Similar arguments (left as an exercise) can be advanced to demonstrate that
> static array bounds checking is impossible in principle, or that one cannot
> identify unreachable code.
There also exist schemes to statically check array bounds.

So many people have claimed that statically checking nil dereferencing is
impossible, that I think I'd better show how it can be done.

The aim is to statically guarantee all pointer dereferences. To this end we
define a new language. 

We introduce a type of pointer that has no nil value, so that (as long as
there are no problems with unassigned variables, which is NOT part of the
scheme) we know that we can always dereference values of this new type.

Then, for variables that may also be nil we introduce a type that says just
that: values of this type may also be nil.

However, values of this second type may NOT be dereferenced, because they
may be nil. Before you dereference such a value, you are forced by the type
system to see if it is nil or a real pointer.

Now, to make this more concrete, here is a whole program to sort a list of
numbers by making a binary tree. I've made the syntax up as I've gone along:

type treenode = record value: integer; left, right: tree end;

type realtree = pointer to treenode; (*there is no nil for this type*);

type tree = optional realtree; (*there is nil for this type*)

var root: tree; (*note: may be nil, since it is of type tree*)
var i: integer;

begin (*program; procedures follow*)
     root:=nil;

     read(i);
     while i>=0 do
          insert(i, root);
          read(i)
     od;
     printtree(root)
end.

procedure insert(i: integer; var t: tree); (*note t may be nil*)
begin
     with t select
     (nil): t:=new(i, nil, nil);
     (rt: realtree):
          if i<rt^.value (*we may dereference rt, since it is a realtree*)
          then insert(i, rt^.left)
          else insert(i, rt^.right)
     end
end;

procedure printtree(t: tree); (*t may be nil*)
begin
     with t select
     (nil): (*do nothing*);
     (rt: realtree):
          printtree(rt^.left); (*again, we may dereference rt*)
          write(rt^.value);
          printtree(rt^.right)
     end
end

The type system thus guarantees that if this compiles, all pointer
dereferences are safe.

Note that it would be fairly easy to make a pre-processor for Pascal or C
that did these checks, and just generated code like "if t=nil" for the "with
t select" statements.

Steven Pemberton, CWI, Amsterdam; steven@mcvax.