[Gcl-devel] Re: address@hidden: More Information]

[Camm Maguire]

Greetings, and thanks!

This should be fixed now.  Please let me kow if problems persist.

There is an old "lfun" list in cmpnew/gcl_lfun.list.lsp which I am
slowly replacing.  The compiler::predicate property was assigned to
functions that should return 'boolean.  Here was the ol list:

(PATHNAMEP STRING-NOT-LESSP PLUSP SIMPLE-STRING-P CHAR= SYMBOLP EQ
    STANDARD-CHAR-P CHAR< ALPHA-CHAR-P >= RANDOM-STATE-P <= CONSTANTP
    /= EQUAL INTEGERP ZEROP STRING-EQUAL EQUALP COMPLEXP STRING<=
    STRING>= STRING/= SIMPLE-BIT-VECTOR-P TREE-EQUAL CHAR-EQUAL LOGBITP
    STRING-NOT-EQUAL ALPHANUMERICP PACKAGEP COMMONP FBOUNDP VECTORP
    ARRAYP STREAMP SIMPLE-VECTOR-P BIT-VECTOR-P STRING-GREATERP TAILP
    CHAR>= CHAR-NOT-LESSP ADJUSTABLE-ARRAY-P READTABLEP CHARACTERP
    STRING-NOT-GREATERP STRINGP CHAR-GREATERP HASH-TABLE-P NUMBERP
    OUTPUT-STREAM-P CHAR-LESSP CHAR<= COMPILED-FUNCTION-P KEYWORDP
    BOUNDP NOT EVENP STRING-CHAR-P MINUSP UPPER-CASE-P NULL STRING>
    FLOATP EQL GRAPHIC-CHAR-P SPECIAL-FORM-P ENDP ODDP LOWER-CASE-P
    BOTH-CASE-P CONSP STRING= FUNCTIONP > = < ATOM STRING-LESSP LISTP
    CHAR-NOT-GREATERP CHAR/= CHAR-NOT-EQUAL CHAR> INPUT-STREAM-P)

I've removed
(string< string<= string> string>= string/=
 string-not-equal string-not-greaterp string-greaterp string-not-lessp
        string-lessp)

Please let me know if I've overlooked anything.

Also, do you have any thoughts about making the gcl and acl2 packages
depend upon X windows as described in my earlier email in an effort to
integrate Gordon Novak's work, (who has been waiting so patiently)?

Take care,



Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
> 
> We have an example where the GCL compiler gets it wrong.  This bug occurs in
> GCL 2.6.5 through 2.6.7 on Linux, but more interesting, it also occurs on a 
> Mac
> using GCL 2.6.8, which I think was recently fetched from CVS.  Below is an
> email from Jared Davis explaining the problem.  The bottom line is that
> compiled code is producing the wrong result in the example below.  A slightly
> simpler example is:
> 
>   >(defun foo (x y)
>      (or (string< x y) nil))
> 
>   FOO
> 
>   >(foo "A" "B")
> 
>   0
> 
>   >(compile 'foo)
> 
>   Compiling gazonk1.lsp.
>   End of Pass 1.  
>   End of Pass 2.  
>   OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
>   Finished compiling gazonk1.lsp.
>   Loading gazonk1.o
>   start address -T 0x83e3000 Finished loading gazonk1.o
>   #<compiled-function FOO>
> 
>   >(foo "A" "B")
> 
>   T
> 
>   >
> 
> By the way, a recent GCL 2.7.0 gets this right, so maybe all that's needed is
> to merge some change there into GCL 2.6.8.  Without such a fix, ACL2 is
> unsound, as discovered by Jared.
> 
> Thanks --
> -- Matt
> From: "Jared C. Davis" <address@hidden>
> Subject: More Information
> To: Matt Kaufmann <address@hidden>
> Date: Thu, 8 Jun 2006 12:22:33 -0500 (CDT)
> 
> Hi,
> 
> Here is some more information.  It looks to me like a GCL bug in its 
> compiler. 
> The function symbol-< is defined here: (minus doc string/guards)
> 
> (defun symbol-< (x y)
>    (let ((x1 (symbol-name x))
>          (y1 (symbol-name y)))
>      (or (string< x1 y1)
>          (and (equal x1 y1)
>               (string< (symbol-package-name x)
>                        (symbol-package-name y))))))
> 
> This, viewed with disassemble, has:
> 
> ;; V5 is x1, V6 is y1
>       V5= symbol_name((V3));
>       V6= symbol_name((V4));
> 
> ;; Push them on the stack, call string_l.
>       base[0]= (V5);
>       base[1]= (V6);
>       vs_top=(vs_base=base+0)+2;
>       Lstring_l();
>       vs_top=sup;
> 
> ;; vs_base[0] now contains the result.  If it's nil, we go do
> ;; something else.
>       if((vs_base[0])==Cnil){
>       goto T3;}
> 
> ;; Otherwise we erroneously return T, instead of returning vs_base[0].
>       {object V7 = Ct;
>       VMR1(V7)}
>       goto T3;
> 
> 
> In fact, here's a script from GCL 2.6.7 CltL1 showing how the compiler
> gets it wrong.
> 
> >(defun symbol-< (x y)
>    (let ((x1 (symbol-name x))
>          (y1 (symbol-name y)))
>      (or (string< x1 y1)
>          (and (equal x1 y1)
>               (string< (symbol-package-name x)
>                        (symbol-package-name y))))))
> 
> SYMBOL-<
> 
> >(symbol-< 'bar 'foo)
> 
> 0
> 
> >(compile 'symbol-<)
> 
> Compiling gazonk1.lsp.
> End of Pass 1.
> End of Pass 2.
> OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
> Finished compiling gazonk1.lsp.
> Loading gazonk1.o
> start address -T 0x83bed30 Finished loading gazonk1.o
> #<compiled-function SYMBOL-<>
> NIL
> NIL
> 
> >(symbol-< 'bar 'foo)
> 
> T
> 
> 
> That's just using /lusr/bin/gcl.
> 
> Thanks!
> 
>     Jared
> 
> - --
> Jared Davis <address@hidden>
> http://www.cs.utexas.edu/users/jared/
> 3600 Greystone Drive #604 - Austin, TX 78731
> (512) 879-3858
> ----------
> 
> 
> 
> 

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