#118 seg fault compiling acl2

segfault
closed-invalid
Sam Steingold
clisp (525)
5
2002-06-28
2002-06-27
John Clements
No

I'm trying to use ACL2, the theorem prover. Clisp seg
faults while
trying to compile it. Without any familiarity with the
ACL2 source,
it's going to be difficult for me to help narrow down
the bug, though
I can certainly explain how to reproduce it.

1) Configuration: Macintosh running Darwin/OS X, I
installed
clisp using dselect. Here's the version info:

[osterley:~/acl2/acl2-sources] clements% clisp
--version
GNU CLISP 2.27 (released 2001-07-17) (built on
localhost [127.0.0.1])

2) I downloaded the ACL2 sources, from the following
URL:
<ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-6/acl2.tar.gz>

2) then, i tried to build acl2 using the makefile:

[osterley:~/acl2/acl2-sources] clements% make
LISP=clisp
rm -f acl2-fns.o
if [ "" = "r" ] ; then \ echo '(or (member :non-standard-analysis *features*)
(push :non-standard-analysis *features*))'
> acl2r.lisp ;\ elif [ "" = "" ] ; then \ echo ';(or (member :non-standard-analysis *features*)
(push :non-standard-analysis *features*))
' > acl2r.lisp ;\ else \ echo 'Please supply either r or the empty string for
make variable NONSTD, not .' ;\ exit 1 ;\ fi
date
Thu Jun 27 12:34:13 EDT 2002
rm -f workxxx
echo '(load "init.lsp")' > workxxx
echo '(acl2::check-suitability-for-acl2)' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
clisp < workxxx
i i i i i i i ooooo o ooooooo
ooooo ooooo
I I I I I I I 8 8 8 8 8
o 8 8
I \ `+' / I 8 8 8
8 8 8
\ `-+-' / 8 8 8
ooooo 8oooo
`-__|__-' 8 8 8
8 8
| 8 o 8 8 o
8 8
------+------ ooooo 8oooooo ooo8ooo
ooooo 8

Copyright (c) Bruno Haible, Michael Stoll 1992, 1993
Copyright (c) Bruno Haible, Marcus Daniels 1994-1997
Copyright (c) Bruno Haible, Pierpaolo Bernardi, Sam
Steingold 1998
Copyright (c) Bruno Haible, Sam Steingold 1999-2001

;; Loading file init.lsp ...
;; Loading file acl2r.lisp ...
;; Loading of file acl2r.lisp is finished.
;; Loading file acl2-init.lisp ...
;; Loading file acl2.lisp ...
;; Loading file acl2-fns.lisp ...
;; Loading of file acl2-fns.lisp is finished.
Compiling file
/Users/clements/acl2/acl2-sources/acl2-fns.lisp ...

Compilation of file
/Users/clements/acl2/acl2-sources/acl2-fns.lisp is
finished.
0 errors, 0 warnings
;; Loading file acl2-fns.fas ...
;; Loading of file acl2-fns.fas is finished.
;; Loading of file acl2.lisp is finished.
;; Loading of file acl2-init.lisp is finished.
;; Loading of file init.lsp is finished.
T
;; Loading file acl2-check.lisp ...Check completed.
;; Loading of file acl2-check.lisp is finished.
T
Bye.
rm -f workxxx
rm -f workxxx
rm -f acl2-fns.o acl2-fns.lbin acl2-fns.sbin
acl2-fns.fasl acl2-fns.wfasl \

acl2-fns.fas acl2-fns.lib acl2-fns.sparcf
echo '(load "init.lsp")' > workxxx
echo '(acl2::compile-acl2 t)' >> workxxx
echo '(acl2::exit-lisp)' >> workxxx
clisp < workxxx
i i i i i i i ooooo o ooooooo
ooooo ooooo
I I I I I I I 8 8 8 8 8
o 8 8
I \ `+' / I 8 8 8
8 8 8
\ `-+-' / 8 8 8
ooooo 8oooo
`-__|__-' 8 8 8
8 8
| 8 o 8 8 o
8 8
------+------ ooooo 8oooooo ooo8ooo
ooooo 8

Copyright (c) Bruno Haible, Michael Stoll 1992, 1993
Copyright (c) Bruno Haible, Marcus Daniels 1994-1997
Copyright (c) Bruno Haible, Pierpaolo Bernardi, Sam
Steingold 1998
Copyright (c) Bruno Haible, Sam Steingold 1999-2001

;; Loading file init.lsp ...
;; Loading file acl2r.lisp ...
;; Loading of file acl2r.lisp is finished.
;; Loading file acl2-init.lisp ...
;; Loading file acl2.lisp ...
;; Loading file acl2-fns.lisp ...
;; Loading of file acl2-fns.lisp is finished.
Compiling file
/Users/clements/acl2/acl2-sources/acl2-fns.lisp ...

Compilation of file
/Users/clements/acl2/acl2-sources/acl2-fns.lisp is
finished.
0 errors, 0 warnings
;; Loading file acl2-fns.fas ...
;; Loading of file acl2-fns.fas is finished.
;; Loading of file acl2.lisp is finished.
;; Loading of file acl2-init.lisp is finished.
;; Loading of file init.lsp is finished.
T
;; Loading file axioms.lisp ...
;; Loading of file axioms.lisp is finished.
Compiling file
/Users/clements/acl2/acl2-sources/axioms.lisp ...

Compilation of file
/Users/clements/acl2/acl2-sources/axioms.lisp is
finished.
0 errors, 0 warnings
;; Loading file axioms.fas ...
;; Loading of file axioms.fas is finished.
;; Loading file basis.lisp ...make: *** [full-small]
Segmentation fault

So, I did a little work to see if I could find the
problem. I narrowed it down to a smaller set of clisp
instructions and ran clisp in GDB
GDB to see if I could get any good information:

[osterley:~/acl2/acl2-sources] clements% gdb clisp
GNU gdb 5.0-20001113 (Apple version gdb-203) (Wed Nov
7 16:28:57 GMT 2001) (UI_OUT)
Copyright 2000 Free Software Foundation, Inc.
GDB is free software, covered by the GNU General Public
License, and you are
welcome to change it and/or distribute copies of it
under certain conditions.
Type "show copying" to see the conditions.
There is absolutely no warranty for GDB. Type "show
warranty" for details.
This GDB was configured as "powerpc-apple-macos10".
Reading symbols for shared libraries .. done
(gdb) run
Starting program: /sw/bin/clisp
[Switching to thread 1 (process 7266 thread 0x1603)]

Program received signal SIGTRAP, Trace/breakpoint trap.
0x41117988 in __dyld__dyld_start ()
(gdb) c
Continuing.
Reading symbols for shared libraries .. done
i i i i i i i ooooo o ooooooo
ooooo ooooo
I I I I I I I 8 8 8 8 8
o 8 8
I \ `+' / I 8 8 8
8 8 8
\ `-+-' / 8 8 8
ooooo 8oooo
`-__|__-' 8 8 8
8 8
| 8 o 8 8 o
8 8
------+------ ooooo 8oooooo ooo8ooo
ooooo 8

Copyright (c) Bruno Haible, Michael Stoll 1992, 1993
Copyright (c) Bruno Haible, Marcus Daniels 1994-1997
Copyright (c) Bruno Haible, Pierpaolo Bernardi, Sam
Steingold 1998
Copyright (c) Bruno Haible, Sam Steingold 1999-2001

[1]> (load "init.lsp")
;; Loading file init.lsp ...
;; Loading file acl2r.lisp ...
;; Loading of file acl2r.lisp is finished.
;; Loading file acl2-init.lisp ...
;; Loading file acl2.lisp ...
;; Loading file acl2-fns.lisp ...
;; Loading of file acl2-fns.lisp is finished.
Compiling file
/Users/clements/acl2/acl2-sources/acl2-fns.lisp ...

Compilation of file
/Users/clements/acl2/acl2-sources/acl2-fns.lisp is
finished.
0 errors, 0 warnings
;; Loading file acl2-fns.fas ...
;; Loading of file acl2-fns.fas is finished.
;; Loading of file acl2.lisp is finished.
;; Loading of file acl2-init.lisp is finished.
;; Loading of file init.lsp is finished.
T
[2]> (acl2::compile-acl2 t)
;; Loading file axioms.lisp ...
;; Loading of file axioms.lisp is finished.
Compiling file
/Users/clements/acl2/acl2-sources/axioms.lisp ...

Compilation of file
/Users/clements/acl2/acl2-sources/axioms.lisp is
finished.
0 errors, 0 warnings
;; Loading file axioms.fas ...
;; Loading of file axioms.fas is finished.
;; Loading file basis.lisp ...
Program received signal EXC_BAD_ACCESS, Could not
access memory.
0x000129b8 in ?? ()
(gdb) bt
#0 0x000129b8 in ?? ()
#1 0x00013978 in ?? ()
#2 0x00012b64 in ?? ()
#3 0x000139c4 in ?? ()
#4 0x00012fbc in ?? ()
#5 0x00012b64 in ?? ()
#6 0x00013978 in ?? ()
#7 0x00012fbc in ?? ()
#8 0x00012b64 in ?? ()
#9 0x00015760 in ?? ()
#10 0x0001300c in ?? ()
...

So, looks like clisp doesn't use C-like stack
conventions.

Please let me know if I can be of any further
assistance in
tracking down this problem.

Thanks,

john clements

Discussion

  • Sam Steingold
    Sam Steingold
    2002-06-27

    Logged In: YES
    user_id=5735

    2.27 is almost a year old - many bugs have been fixed
    (and new introduced :-).
    please get the current development version from the CVS and
    make sure that the bug is still there. then build it
    --with-debug and you will be able to see the C stack trace
    properly.
    thanks!

     
  • Logged In: NO

    Thanks; I've been spoiled by stack-safe languages like
    Scheme. The
    problem was a stack overflow, and was solved by an
    'unlimit'. I guess
    I've been living in a safe world for too long, but I'm
    appalled that a
    simple tail-recursive loop would cause a seg fault.

    Thanks for your suggestion,

    john clements

     
  • Sam Steingold
    Sam Steingold
    2002-06-28

    • status: open --> closed-invalid
     
  • Sam Steingold
    Sam Steingold
    2002-06-28

    Logged In: YES
    user_id=5735

    CLISP does catch stack overflows on OSX.

    [4]> (defun z (x) (z (1+ x)))
    Z
    [5]> (z 10)
    *** - Lisp stack overflow. RESET

    this is quite weird.
    I would really appreciate it if you could try the current
    CVS version and report your experiences.
    thanks