FTYPE declaration badness

Bug #309475 reported by Nikodemus Siivola on 2008-12-18
10
This bug affects 1 person
Affects Status Importance Assigned to Milestone
SBCL
Medium
Unassigned

Bug Description

  The compiler assumes that any time a function of declared FTYPE
  doesn't signal an error, its arguments were of the declared type.
  E.g. compiling and loading
    (DECLAIM (OPTIMIZE (SAFETY 3)))
    (DEFUN FACTORIAL (X) (GAMMA (1+ X)))
    (DEFUN GAMMA (X) X)
    (DECLAIM (FTYPE (FUNCTION (UNSIGNED-BYTE)) FACTORIAL))
    (DEFUN FOO (X)
      (COND ((> (FACTORIAL X) 1.0E6)
             (FORMAT T "too big~%"))
            ((INTEGERP X)
             (FORMAT T "exactly ~S~%" (FACTORIAL X)))
            (T
             (FORMAT T "approximately ~S~%" (FACTORIAL X)))))
  then executing
    (FOO 1.5)
  will cause the INTEGERP case to be selected, giving bogus output a la
    exactly 2.5
  This violates the "declarations are assertions" principle.
  According to the ANSI spec, in the section "System Class FUNCTION",
  this is a case of "lying to the compiler", but the lying is done
  by the code which calls FACTORIAL with non-UNSIGNED-BYTE arguments,
  not by the unexpectedly general definition of FACTORIAL. In any case,
  "declarations are assertions" means that lying to the compiler should
  cause an error to be signalled, and should not cause a bogus
  result to be returned. Thus, the compiler should not assume
  that arbitrary functions check their argument types. (It might
  make sense to add another flag (CHECKED?) to DEFKNOWN to
  identify functions which *do* check their argument types.)
  (Also, verify that the compiler handles declared function
  return types as assertions.)

Changed in sbcl:
importance: Undecided → Medium
status: New → Confirmed
Nikodemus Siivola (nikodemus) wrote :

I'm inclined to think that the correct solution would be to add :TRUSTED as a :WHERE-FROM type to globaldb, and trust only those.

After a function has been compiled, any :DECLARED type it had can be upgraded to :TRUSTED.

Douglas Katzman (dougk) wrote :

There are stopgap measures that would help here:
- if FTYPE of FUN is proclaimed and FUN is already defined, issue a style-warning that if was compiled without the checks.
- when the FTYPE is proclaimed, if FUN's :WHERE-FROM was :ASSUMED, then issue a style-warning that some callers of FUN were not able to use the FTYPE information.

These are significantly easier things than The Right Thing, very nonintrusive to the compiler, and similar in spirit to the warnings about not being able to use inline information because a definition was to late.

Jim Newton (jimka-issy) wrote :

I apparently encountered this same problem in (https://bugs.launchpad.net/sbcl/+bug/1558695).

My case was the following:

(in-package :cl-user)

(defclass B ()
  ())

;; test-function-subtype takes an argument which is a
;; unary function B->B
(defun test-function-subtype (f)
  (declare (type (function (B) B) f)
    (optimize (debug 3) (speed 0) (safety 3)))
  (let ((ret-val (funcall f (make-instance 'B))))
    (format t "ret-val = ~A (typep ret-val 'B)=~A~%" ret-val (typep ret-val 'B))
    (assert (typep ret-val 'B))))

;; But I cannot make the return less specific
(test-function-subtype #'(lambda (b)
      (declare (type B b))
      12))

----------------------------

The compiler apparently replaces (typep ret-val 'B) with t. And at run-time
the value of ret-val is 12, which is NOT of type B.

To post a comment you must log in.
This report contains Public information  Edit
Everyone can see this information.

Duplicates of this bug

Other bug subscribers