Summary

Scrutinizer produces incorrect procedure types after merge

Metadata

Description

Suppose we get this expression after scrutinizing some code:

 (or (procedure (|#!rest|) noreturn)
     (procedure (* |#!rest|) . *))

At the moment the result of the union is `(procedure (#!rest))` which is clearly wrong because it has arity N >= 0 while the second procedure in the `or` expression has arity N >= 1. Moreover the return type is lost, I'd expect the `noreturn` to be dropped and `*` to be used instead.

The result of the miscalculation of the resulting type may or may not be dangerous.

Changes and comments

[2017-10-10 12:29:32 UTC] sjamaan wrote:

I'm not so sure that the arity is "clearly wrong", because it would be equally incorrect to give a warning when calling the procedure with zero arguments; the procedure might accept zero arguments (if the first alternative is used).

Perhaps the best we can do is not to simplify/merge the procedure, but just keep the or? I don't know what the impact of that would be though.

[2017-10-10 18:42:55 UTC] megane wrote:

My understanding is that it is always safe to go for more general type. In this case `procedure` or even just `*` would be ok too. And N >= 0 is more general than N >= 1.

Notice that `(procedure (#!rest))` does not specify return type. This is different from `*`.

Indeed, it would be interesting to know if there was any downsides if in this case the union was left as it is. Maybe it would make the scrutinizer slower..

[2017-10-12 22:40:05 UTC] evhan changed status from new to assigned

[2017-10-12 22:40:05 UTC] evhan set owner to evhan

[2017-11-06 07:31:04 UTC] evhan wrote:

On what version are you seeing this? The current behaviour in both master and 4.12.0 is, as far as I can tell, to simplify `(or (procedure a (#!rest *) noreturn) (procedure b (* #!rest *) . *))` into `(procedure (#!rest) . *)`, which is correct.

Is there a specific way to trigger this bug, and if so can you share?

[2017-11-10 10:57:25 UTC] LemonBoy wrote:

Sure, I caught this error during the compilation of the `sxpath` egg, to be precise during the compilation of `chicken/context-sxpath-lolevel.scm`. The warnings emitted are reported below:

   Warning: in toplevel procedure `context-sxpath-lolevel#draft:ast-step':
     expected a single result in `let' binding of `axis', but received zero results
 
   Warning: in toplevel procedure `context-sxpath-lolevel#draft:ast-step':
     expected a single result in `let' binding of `axis', but received zero results

You have to start from those warnings and work your way backwards to the source of the type for `axis-lst`. If I still remember correctly the nitty gritty details it's the analysis of `draft:ast-axis-specifier` that gets the type mentioned in the ticket.

Tested right now with CHICKEN Version 4.12.1 (rev 5746f0c1)

[2017-12-02 16:45:37 UTC] sjamaan changed status from assigned to closed

[2017-12-02 16:45:37 UTC] sjamaan set resolution to fixed

[2017-12-02 16:45:37 UTC] sjamaan wrote:

Fixed with 5ea816d and 62d7991.

[2018-05-27 15:25:01 UTC] megane changed status from closed to reopened

[2018-05-27 15:25:01 UTC] megane removed resolution fixed

[2018-05-27 15:25:01 UTC] megane wrote:

LemonBoy's original analysis seems to be correct; the merged type should be `(procedure (* |#!rest|) . *)`. Here is a case that fails at runtime:

 (: f1 (#!rest * -> noreturn))
 (define (f1 #!rest _) (exit))
 
 (: f2 (procedure (* #!rest *) . *))
 (define (f2 a #!rest _) (begin))
 
 (declare (not inline foo))
 (: foo ((#!rest ->) -> *))
 (define (foo f)
   (f))
 
 (print "running")
 (foo (if (the * #f) f1 f2))
 
 ;; The merged type is (procedure (#!rest) . *)
 ;; (compiler-typecase (if (the * #f) f1 f2) ((not *) 1))
 
 ;; Output:
 ;;
 ;; $ csc -O3 1399-case.scm && ./1399-case
 ;; running
 ;;
 ;; Error: too few arguments - received 0 but expected 1: #<procedure (f2 a . _)>
 ;;
 ;; 	Call history:
 ;;
 ;; 	1399-case.scm:12: chicken.base#print
 ;; 	1399-case.scm:13: foo
 ;; 	1399-case.scm:10: f	  	<--

I think the procedure merging could be implemented with a simple algorithm:

 Input: (or P1 P2 ... Pk)
 T1  <- (or P1)
 T_n <- if P_n < T_n-1
          T_n-1
        else
          (or T_n-1 P_n)
 Result is T_k

This would return correct, but not necessarily minimal types.

For `(or (procedure (|#!rest|) noreturn) (procedure (* |#!rest|) . *))` it wouldn't change the type. For `(or (procedure (* |#!rest|) . *) (procedure (|#!rest|) noreturn) )` it would return `(procedure (* |#!rest|) . *)`.

[2018-05-27 15:40:25 UTC] sjamaan changed milestone from 4.13.0 to 5.0

[2018-05-27 15:52:14 UTC] megane wrote:

The idea of merging procedure argument and return types piecemeal, as it's currently done, is fundamentally flawed. See below:

 (: f1 (fixnum -> *))
 (define (f1 a)
   (+ a 1))
 
 (: f2 (string -> *))
 (define (f2 a)
   (string-length a))
 
 (: foo (((or fixnum string) -> *) -> *))
 (define (foo f)
   (print (f 1))
   (print (f "hello")))
 
 ;; (compiler-typecase (if (the * #t) f1 f2) ((not *) 1))
 ;; Error: at toplevel:
 ;;   (procedure-merge-fail.scm:14) no clause applies in `compiler-typecase' for expression of type `(procedure ((or string fixnum)) *)':
 ;;     (not *)
 
 (foo (lambda (a) (if (string? a) (f2 a) (f1 a))))
 (foo (if (the * #t) f2 f1))
 
 ;; $ csc -O3 procedure-merge-fail.scm && ./procedure-merge-fail
 ;; 2
 ;; 5
 ;;
 ;; Error: (string-length) bad argument type: 1
 ;;
 ;; 	Call history:
 ;;
 ;; 	procedure-merge-fail.scm:19: foo
 ;; 	procedure-merge-fail.scm:11: f
 ;; 	procedure-merge-fail.scm:11: chicken.base#print
 ;; 	procedure-merge-fail.scm:12: f
 ;; 	procedure-merge-fail.scm:12: chicken.base#print
 ;; 	procedure-merge-fail.scm:20: foo
 ;; 	procedure-merge-fail.scm:11: f	  	<--

[2018-05-28 11:26:09 UTC] sjamaan changed milestone from 5.0 to 5.1

[2018-05-28 11:26:09 UTC] sjamaan wrote:

Not a blocker for 5.0

[2019-04-07 12:23:24 UTC] sjamaan changed milestone from 5.1 to 5.2

[2019-04-07 12:23:24 UTC] sjamaan wrote:

Getting ready for 5.1, moving tickets which won't make it in to 5.2.

[2019-08-25 18:19:13 UTC] felix changed milestone from 5.2 to 5.3

[2021-04-12 13:43:26 UTC] sjamaan changed milestone from 5.3 to 5.4

[2023-11-06 22:05:01 UTC] felix changed milestone from 5.4 to someday