[Gcl-devel] Re: possible GCL/Windows compiler bug

[Camm Maguire]

Greetings!

OK, my suspicion lies with a difficulty in the windows relocation
code, but I'm not yet certain.  Here is how to proceed:

0) run saved_acl2 under gdb 

1) b fasload

2) r

3) Put your match-clause function into a separate file, compile with
   compiler::*c-debug* set to t

4) (load "your_file.o")

5) gdb will break -- type 'finish'

6) Still at gdb prompt, look at start address printed by gcl to
   screen.  Type 'add-symbol-file <your_file.o> <address>

7) c

8) trigger the error

9) gdb will stop, print a backtrace with bt

10) In gdb, type 'p/x *(char *)<address>@1024'

11) In gdb, type 'shell', and then 'objdump -d your_file.o'

12) Send me the results

Take care,


Matt Kaufmann <address@hidden> writes:

> [Resending -- I had a typo in the CC field that may have prevented delivery.]
> 
> Hi --
> 
> Help!?  Sorry to bother you with this email, but I've gone about as far as I
> know how with the problem described below (and I'll spare you the dead ends),
> which I kind of suspect is a problem with GCL/Windows, but might instead be a
> problem with ACL2.  This is a rather long email; please feel free to ask for
> any clarification.
> 
> There appears to be a problem either with GCL on Windows or with ACL2.  I'll
> describe the symptom below.  This symptom doesn't occur on Linux or 
> Sun/Solaris
> for GCL, Allegro CL, CMUCL, or CLISP, and I also haven't seen it on Linux with
> Lispworks or on a Macintosh with OpenMCL; I've only seen it on GCL/Windows.
> But I realize that it still could be a subtle problem with ACL2, so I think we
> need to wait on the ACL2 release until we determine whether or not it's a
> GCL/Windows problem.
> 
> Jared Davis was kind enough to submit the commands below (at the end of this
> email) while standing in directory books/misc/ of the ACL2 distribution, after
> building ACL2 on GCL/Windows 2.6.5.  The result is a hard Lisp error if you do
> *NOT* submit the compile form below: for a transcript, see
> http://www.cs.utexas.edu/users/jared/test.log5 (or equivalently, on the UTCS
> file system, /u/www/users/jared/test.log5).  But *with* the compile form, the
> problem goes away (see test.log4 in the same directory).  We verified that the
> definition being compiled is exactly the same as the one compiled when 
> building
> ACL2.  (I'll explain how if you're interested -- we could insert a call of
> disassemble during the build if you think that would be helpful.)
> 
> You can see the result of :bt and :ihs on a failed run, where some source
> functions are run interpreted (but this doesn't avoid the error since the
> offending function ACL2_*1*_ACL2::MATCH-CLAUSE is still run compiled), in
> test.log in that same directory.  In a moment I'll forward you a related log
> with that info (and also the result of :bl), in case you prefer to see it by
> email.
> 
> By the way, all of the failures Jared came across during the regression run
> were during macroexpansion of ACL2 macro case-match, which calls
> match-clause-list, which calls match-clause -- actually the ACL2 
> macroexpansion
> mechanism causes a call of ACL2_*1*_ACL2::MATCH-CLAUSE-LIST, which calls
> ACL2_*1*_ACL2::MATCH-CLAUSE.
> 
> Also by the way, even if you leave off the compile form below but you add
> (si::use-fast-links nil), the problem goes away.  That seems odd to me so I
> thought I should mention it.
> 
> Here are the commands after starting up ACL2.  Again, omit the compile form to
> see the error -- even though the compile form should be a no-op!
> 
> (rebuild "defpun.lisp" 'arbitrary-tail-recursive-encap)
> :q
> (compile
>  (DEFUN ACL2_*1*_ACL2::MATCH-CLAUSE (X PAT FORMS)
>    (COND
>     ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*)
>      (RETURN-FROM
>       ACL2_*1*_ACL2::MATCH-CLAUSE
>       (MV-LET (TESTS BINDINGS)
>               (ACL2_*1*_ACL2::MATCH-TESTS-AND-BINDINGS X PAT NIL NIL)
>               (LIST (IF (ACL2_*1*_COMMON-LISP::NULL TESTS) T
>                         (CONS 'AND
>                               (ACL2_*1*_COMMON-LISP::REVERSE TESTS)))
>                     (CONS 'LET
>                           (CONS (ACL2_*1*_COMMON-LISP::REVERSE
>                                  BINDINGS)
>                                 FORMS)))))))
>    (MATCH-CLAUSE X PAT FORMS)))
> (lp)
> (defun remove-xargs-domain-and-measure (dcl)
>   (case-match dcl
>     (('declare ('xargs ':domain dom-expr
>                        ':measure measure-expr
>                        . rest))
>      (mv nil dom-expr measure-expr rest))
>     (('declare ('xargs ':gdomain dom-expr
>                        ':measure measure-expr
>                        . rest))
>      (mv t dom-expr measure-expr rest))
>     (& (mv nil nil 0 nil))))
> 
> Thanks much --
> -- Matt
> 
> 
> 

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