Improve floating-point type derivation in some cases

Bug #894498 reported by Lutz Euler
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
SBCL
Fix Released
Undecided
Unassigned

Bug Description

Hi,

in the following function

(defun f (x)
  (declare (type (single-float 0.0) x))
  (when (> x 0)
    (log x)))

the compiler generates a full call to LOG as it can't derive
that LOG's argument can't be zero. I needed to change that to

(defun g (x)
  (declare (type (single-float 0.0) x))
  (when (> x 0)
    (locally (declare (type (single-float (0.0)) x))
      (log x))))

so that the type is honored and a call to the C library "log"
is generated. This seems silly. Moreover, if less is known
about X, the derivation works better:

(defun h (x)
  (declare (type (single-float -1.0) x))
  (when (> x 0)
    (log x)))

This generates a call to the C library "log" as desired.

I have tracked this down to CONSTRAIN-FLOAT-TYPE;
tracing it during compilation of the functions shows

(for f):

0: (SB-C::CONSTRAIN-FLOAT-TYPE
     #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT 0.0)>
     #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT 0.0 0.0)>
     T NIL)
0: SB-C::CONSTRAIN-FLOAT-TYPE returned
     #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT 0.0)>

(for h):

0: (SB-C::CONSTRAIN-FLOAT-TYPE
     #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT -1.0)>
     #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT 0.0 0.0)>
     T NIL)
0: SB-C::CONSTRAIN-FLOAT-TYPE returned
     #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT (0.0))>

So, the patch attached below changes CONSTRAIN-FLOAT-TYPE
to return the openly bounded type,
  #<SB-KERNEL:NUMERIC-TYPE (SINGLE-FLOAT (0.0))>
in the first case above, too.

I have compared the old and the new version of this function
with all combinations of NIL, 0.0, (0.0), 1.0 and (1.0) as
the lower and upper bounds of the first two arguments and with
all combinations of T and NIL for the remaining two, and have
convinced myself that firstly, in the cases where the output
differs, the new version is better, and secondly, that the
function now returns the tightest possible type in all cases.

With the argument list of CONSTRAIN-FLOAT-TYPE being
  (X Y GREATER OR-EQUAL),
without loss of generality taking GREATER = T, the only changed
cases are with OR-EQUAL = NIL and TYPE-BOUND-NUMBER of the lower
bounds of X and Y being equal numbers (using 0.0 below as an
example only), the upper bounds being mostly don't care (using
NIL below), the following two variations:

  X = (SINGLE-FLOAT 0.0)
  Y = (SINGLE-FLOAT 0.0)

and

  X = (SINGLE-FLOAT 0.0)
  Y = (SINGLE-FLOAT (0.0))

In both cases the old result is
  (SINGLE-FLOAT 0.0)
and the new one
  (SINGLE-FLOAT (0.0))

(An upper bound of X that is too low can change the new result
to the empty type where the old result was something like
(SINGLE-FLOAT 0.0 0.0)).

The patched version builds and passes the test suite under
Linux, x86-64.

Greetings,

Lutz

Revision history for this message
Lutz Euler (lutz-euler) wrote :
tags: added: compiler floating-point patch review types
Changed in sbcl:
assignee: nobody → Nikodemus Siivola (nikodemus)
status: New → In Progress
Revision history for this message
Nikodemus Siivola (nikodemus) wrote :

commit 0dda5090b6c16a641000b4eb2dcd479f39b784ca
Author: Lutz Euler <email address hidden>
Date: Wed Nov 23 20:31:09 2011 +0100

    Tighter floating-point type constraints in some cases

    CONSTRAIN-FLOAT-TYPE used to return a closed bound in some cases where
    the corresponding (tighter) open bound would have been derivable,
    leading to missed optimisation opportunities. For example the compiler
    did not derive that x is not zero in the following call to LOG:

    (defun foo (x)
      (declare (type (single-float 0.0) x))
      (when (> x 0.0)
        (log x)))

    Fix CONSTRAIN-FLOAT-TYPE so that it returns the tightest possible result
    in all cases.

    See lp#894498 for details.

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  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.