Steel Bank Common Lisp

failed AVER when compiling a compound type declaration containing an undefined type

Reported by Lutz Euler on 2012-01-07
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
SBCL
Medium
Unassigned

Bug Description

Entering the following expression at the REPL leads to a failed AVER:

(defun f (x)
  (declare (optimize speed)
           (type (and fixnum a) x))
  x)

debugger invoked on a SB-INT:BUG in thread
#<THREAD "initial thread" RUNNING {1002989AE3}>:
    failed AVER: (INTEGER-TYPE-P TYPE)

This is a regression. Bisected:
The first bad commit is 1.0.28.48.

Older versions compile the function and emit a style warning
about an undefined type "A" as expected. See the following
items for the exact output and a backtrace.

I have observed this under x86-64/Linux.

Lutz

Lutz Euler (lutz-euler) wrote :

Output from the newest working version:

This is SBCL 1.0.28.47, an implementation of ANSI Common Lisp.
More information about SBCL is available at <http://www.sbcl.org/>.

SBCL is free software, provided as is, with absolutely no warranty.
It is mostly in the public domain; some portions are provided under
BSD-style licenses. See the CREDITS and COPYING files in the
distribution for more information.
* (defun f (x)
  (declare (optimize speed)
           (type (and fixnum a) x))
  x)

; in: LAMBDA NIL
; (TYPE (AND FIXNUM A) X)
;
; caught STYLE-WARNING:
; undefined type: A
;
; compilation unit finished
; Undefined type:
; A
; caught 1 STYLE-WARNING condition

F

Lutz Euler (lutz-euler) wrote :
Download full text (8.0 KiB)

Output and backtrace from the oldest broken version.
(The backtrace still looks much the same on current
git head, 1.0.54.108.)

This is SBCL 1.0.28.48, an implementation of ANSI Common Lisp.
More information about SBCL is available at <http://www.sbcl.org/>.

SBCL is free software, provided as is, with absolutely no warranty.
It is mostly in the public domain; some portions are provided under
BSD-style licenses. See the CREDITS and COPYING files in the
distribution for more information.
* (defun f (x)
  (declare (optimize speed)
           (type (and fixnum a) x))
  x)

debugger invoked on a SB-INT:BUG:
    failed AVER: (INTEGER-TYPE-P TYPE)
  This is probably a bug in SBCL itself. (Alternatively, SBCL might have been
  corrupted by bad user code, e.g. by an undefined Lisp operation like
  (FMAKUNBOUND 'COMPILE), or by stray pointers from alien code or from unsafe
  Lisp code; or there might be a bug in the OS or hardware that SBCL is running
  on.) If it seems to be a bug in SBCL itself, the maintainers would like to
  know about it. Bug reports are welcome on the SBCL mailing lists, which you
  can find at <http://sbcl.sourceforge.net/>.

Type HELP for debugger help, or (SB-EXT:QUIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [ABORT] Exit debugger, returning to top level.

(SB-INT:BUG "~@<failed AVER: ~2I~_~A~:>")[:EXTERNAL]
0] backtrace

0: (SB-INT:BUG "~@<failed AVER: ~2I~_~A~:>")[:EXTERNAL]
1: (SB-IMPL::%FAILED-AVER (SB-C::INTEGER-TYPE-P TYPE))
2: (SB-C::WEAKEN-INTEGER-TYPE #<SB-KERNEL:INTERSECTION-TYPE (AND FIXNUM A)>)
3: (SB-C::WEAKEN-TYPE #<SB-KERNEL:INTERSECTION-TYPE (AND FIXNUM A)>)
4: (SB-C::MAKE-CAST
    #<SB-C::LVAR 1 {10026BAA51}>
    #<SB-KERNEL:INTERSECTION-TYPE (AND FIXNUM A)>
    ((COMPILATION-SPEED . 1) (DEBUG . 1) (INHIBIT-WARNINGS . 1)
     (SB-C::MERGE-TAIL-CALLS . 3) (SAFETY . 1) (SPACE . 1) (SPEED . 3)))
5: ((FLET SB-C::CLOSURE-NEEDING-IR1-ENVIRONMENT-FROM-NODE))
6: (SB-C::%WITH-IR1-ENVIRONMENT-FROM-NODE
    #<SB-C::COMBINATION
      :FUN #<SB-C::REF :LEAF # {10026BA911}>
      :ARGS (NIL) {10026BA991}>
    #<CLOSURE (FLET SB-C::CLOSURE-NEEDING-IR1-ENVIRONMENT-FROM-NODE) {10026BAEB9}>)
7: (SB-C::ASSERT-LVAR-TYPE
    #<SB-C::LVAR 1 {10026BAA51}>
    #<SB-KERNEL:INTERSECTION-TYPE (AND FIXNUM A)>
    ((COMPILATION-SPEED . 1) (DEBUG . 1) (INHIBIT-WARNINGS . 1)
     (SB-C::MERGE-TAIL-CALLS . 3) (SAFETY . 1) (SPACE . 1) (SPEED . 3)))
8: (SB-C::PROPAGATE-TO-ARGS
    #<SB-C::COMBINATION
      :FUN #<SB-C::REF :LEAF # {10026BA911}>
      :ARGS (NIL) {10026BA991}>
    #<SB-C::CLAMBDA
      :%SOURCE-NAME F
      :%DEBUG-NAME NIL
      :KIND NIL
      :TYPE #<SB-KERNEL:BUILT-IN-CLASSOID FUNCTION (read-only)>
      :WHERE-FROM :DEFINED
      :VARS (X) {10026B62B1}>)
9: (SB-C::CONVERT-CALL
    #<SB-C::REF
      :LEAF #<SB-C::CLAMBDA
              :%SOURCE-NAME F
              :%DEBUG-NAME NIL
              :KIND NIL
              :TYPE #<SB-KERNEL:BUILT-IN-CLASSOID FUNCTION (read-only)>
              :WHERE-FROM :DEFINED
              :VARS (X) {10026B62B1}> {10026BA911}>
    #<SB-C::COMBINATION
      :FUN #<SB-C::REF :LEAF # {10026BA911}>
      :ARGS (NIL) {10026BA991}>
    #<SB-C:...

Read more...

tags: added: compiler regression types
Paul Khuong (pvk) on 2012-01-07
Changed in sbcl:
status: New → In Progress
assignee: nobody → Paul Khuong (pvk)
Paul Khuong (pvk) wrote :

This deserves more thought.

One performance-oriented fix is to weaken intersection types that are subtypes of INTEGER to the tightest INTEGER type possible.

A slightly simpler fix is to defer to the BACKEND-TYPE-PREDICATE logic as soon as a hairy type is involved; this ends being, at best, as weak as the first option.

A more safety-oriented fix punts on weakening types that include any undefined type. We would get the style warning, but it doesn't seem to follow the spirit of WEAKEN-TYPE.

I'm very much inclined to go with the first fix. This is WEAKEN-TYPE, after all. Discuss, but I'll try to commit a fix before release.

Changed in sbcl:
assignee: Paul Khuong (pvk) → nobody
status: In Progress → Confirmed
Changed in sbcl:
assignee: nobody → Nikodemus Siivola (nikodemus)
importance: Undecided → Medium
status: Confirmed → In Progress
Nikodemus Siivola (nikodemus) wrote :

commit 5a2c8811f297b21b5e4142ce29d2c7981cbb2697
Author: Nikodemus Siivola <email address hidden>
Date: Mon Jan 23 14:27:17 2012 +0200

    weakening hairy integer types

     Fixes lp#913232.

     Deal with intersection types and unions including non-integer component
     types, such as:

       (OR (INTEGER * -1) (AND (SATISFIES ODDP) (INTEGER 1)))

Changed in sbcl:
assignee: Nikodemus Siivola (nikodemus) → nobody
status: In Progress → Fix Committed
Changed in sbcl:
status: Fix Committed → Fix Released
To post a comment you must log in.
This report contains Public information  Edit
Everyone can see this information.

Other bug subscribers