[Gcl-devel] Re: GCL bug in NTH

[Camm Maguire]

Greetings, and thanks for the report!

GCL limits sequence lengths to some large fraction of the word size,
which is always twice most-positive-fixnum, as these quantities refer
in principle to the maximum amount of memory addressable in the
system, which obviously limits the length of sequences.  This is quite
important in compiler optimizations.  Nevertheless, the GCL behavior
below is obviously in error.

I propose nth returning nil immediately (i.e. no list dereferencing)
on positive integer greater than the limit.  When compiling (with
safety 0 by default, by the way, which will always eliminate error
throwing), we should return nil on any non-fixnum input.  

If this is agreeable, I'll get this into 2.6.8 before release.

When inlining nth, we can more than pay for the type detection of the
argument, leading to a net gain of about 2.5% and about 200 bytes
extra of code.  I take it this is worth it.

Take care,

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
> 
> The Common Lisp spec seems to imply that the first argument of NTH is any
> non-negative integer (http://www.lisp.org/HyperSpec/Body/acc_nth.html#nth), 
> yet
> GCL expects it to be a fixnum.  Yet we can actually get GCL to give an
> incorrect answer if NTH is called from another function with a bignum 
> argument.
> This is all illustrated below (the log is from a Mac, but I had the same
> problem on Ubuntu with GCL 2.6.6).
> 
>   bbh:~/acl2/v2-9-4 kaufmann$ gcl
>   GCL (GNU Common Lisp)  2.6.8 CLtL1    Jan  5 2006 17:46:08
>   Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
>   Binary License:  GPL due to GPL'ed components: (READLINE BFD UNEXEC)
>   Modifications of this banner must retain notice of a compatible license
>   Dedicated to the memory of W. Schelter
> 
>   Use (help) to get some basic information on how to use GCL.
>   Temporary directory for compiler files set to /tmp/
> 
>   >(nth (expt 2 40) '(1 2 3 4))
> 
>   Error: Expected a FIXNUM 
>   Fast links are on: do (si::use-fast-links nil) for debugging
>   Error signalled by NTH.
>   Broken at NTH.  Type :H for Help.
>   >>:q
> 
>   Top level.
>   >(defun foo (n x) (nth n x))
> 
>   FOO
> 
>   >(foo (expt 2 40) '(1 2 3 4))
> 
>   Error: Expected a FIXNUM 
>   Fast links are on: do (si::use-fast-links nil) for debugging
>   Error signalled by NTH.
>   Broken at NTH.  Type :H for Help.
>   >>:q
> 
>   Top level.
>   >(compile 'foo)
> 
>   Compiling /tmp/gazonk_24167_0.lsp.
>   End of Pass 1.  
>   End of Pass 2.  
>   OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
>   Finished compiling /tmp/gazonk_24167_0.lsp.
>   Loading /tmp/gazonk_24167_0.o
>   start address -T 0x9e7e80 Finished loading /tmp/gazonk_24167_0.o
>   #<compiled-function FOO>
>   NIL
>   NIL
> 
>   >(foo (expt 2 40) '(1 2 3 4))
> 
>   3
> 
>   >
> 
> There's no particular urgency on this that I know of, though I'm sure you'll
> want to fix it.  Actually, this bug renders ACL2 unsound:
> 
> (defun foo (n x) (nth n x))
> 
> (defthm nth-of-large
>   (implies (and (integerp n) (> n (len lst)))
>          (equal (nth n lst) nil))
>   :rule-classes nil)
> 
> (thm nil
>      :hints
>      (("Goal" :use ((:instance nth-of-large
>                              (n (expt 2 40))
>                              (lst '(1 2 3 4)))
>                   (:theorem (equal (foo (expt 2 40) '(1 2 3 4)) 3))))))
> 
> Thanks --
> -- Matt
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah