idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.52k stars 374 forks source link

Invalid memory reference on Chez backend #1974

Open stefan-hoeck opened 3 years ago

stefan-hoeck commented 3 years ago

The following code behaves correctly on the JS backend but not on the default Chez Scheme backend. This occurred in a larger code base of mine, and breaking it down to the example below took quite some time. It might still not be minimal, though:

Steps to Reproduce

Compile and run the following example:

module MSF

%default total

public export
data MSF : (i : Type) -> (o : Type) -> Type where
  Arr  :  (i -> o) -> MSF i o
  Par  :  MSF i1 o1 -> MSF i2 o2 -> MSF (i1, i2) (o1, o2)
  Fan  :  MSF i o1 -> MSF i o2 -> MSF i (o1, o2)

export
step : i -> MSF i o -> (o, MSF i o)
step v c@(Arr f)    = (f v, c)

step (v1,v2) (Par sf1 sf2)  =
  let (o1,sf1') = step v1 sf1
      (o2,sf2') = step v2 sf2
   in ((o1,o2), Par sf1' sf2')

step v (Fan sf1 sf2)  =
  let (o1,sf1') = step v sf1
      (o2,sf2') = step v sf2
   in ((o1,o2), Fan sf1' sf2')

one : Int
one = 1

main : IO ()
main = printLn . fst $ step one (Fan (Arr id) (Arr id))

Expected Behavior

Prints (1, 1).

Observed Behavior

Fails with: Exception: invalid memory reference. Some debugging context lost

Now, I had a look at the generated Scheme code, and the culprit is the second pattern match in function step (I'll add a properly indented version of it below): Instead of matching against the MSF constructor, the generated Scheme performs a null? check against the pair argument. Pairs are treated as CONS constructors internally, so the Chez codegen performs this check to distinguish the CONS case from the NIL case. However, null? returns #f for everything that is not an empty list (the number we pass as an argument in our case), and the wrong branch is entered, leading to the exception described below.

(define MSF-step
  (lambda (arg-2 arg-3)
    (case (vector-ref arg-3 0)
      ((0)
       (let ((e-17 (vector-ref arg-3 1)))
         (cons (e-17 arg-2) arg-3)))
      (else
        (if (null? arg-2)
          (let ((e-3 (vector-ref arg-3 1)))
            (let ((e-4 (vector-ref arg-3 2)))
              (let ((sc2 (MSF-step arg-2 e-3)))
                (let ((e-2 (car sc2)))
                  (let ((e-5 (cdr sc2)))
                    (let ((sc3 (MSF-step arg-2 e-4)))
                      (let ((e-7 (car sc3)))
                        (let ((e-6 (cdr sc3)))
                          (cons (cons e-2 e-7) (vector 2 e-5 e-6))))))))))
          (let ((e-7 (car arg-2)))
            (let ((e-8 (cdr arg-2)))
              (case (vector-ref arg-3 0)
                ((1)
                 (let ((e-13 (vector-ref arg-3 1)))
                   (let ((e-14 (vector-ref arg-3 2)))
                     (let ((sc2 (MSF-step e-7 e-13)))
                       (let ((e-2 (car sc2)))
                         (let ((e-3 (cdr sc2)))
                           (let ((sc3 (MSF-step e-8 e-14)))
                             (let ((e-5 (car sc3)))
                               (let ((e-4 (cdr sc3)))
                                 (cons (cons e-2 e-5) (vector 1 e-3 e-4)))))))))))
                (else
                  (let ((e-3 (vector-ref arg-3 1)))
                    (let ((e-4 (vector-ref arg-3 2)))
                      (let ((sc2 (MSF-step arg-2 e-3)))
                        (let ((e-2 (car sc2)))
                          (let ((e-5 (cdr sc2)))
                            (let ((sc3 (MSF-step arg-2 e-4)))
                              (let ((e-9 (car sc3)))
                                (let ((e-6 (cdr sc3)))
                                  (cons (cons e-2 e-9) (vector 2 e-5 e-6)))))))))))))))))))

Finally, if I change the implementation of step to the following version, the program runs correctly:


export
step : i -> MSF i o -> (o, MSF i o)
step v c@(Arr f)    = (f v, c)

step p (Par sf1 sf2)  =
  let (o1,sf1') = step (fst p) sf1
      (o2,sf2') = step (snd p) sf2
   in ((o1,o2), Par sf1' sf2')

step v (Fan sf1 sf2)  =
  let (o1,sf1') = step v sf1
      (o2,sf2') = step v sf2
   in ((o1,o2), Fan sf1' sf2')
stefan-hoeck commented 3 years ago

Actually, I don't think this is a bug of the chez backend: The problem is already there when the CExp IR is being generated. The branch should be chosen from the data constructor used in the second argument, not from the one in the first argument, so there shouldn't be any decision making based on the first argument at all. Imagine the same function being called with a two-argument record, which will happen to have the same representation in the IRs as Prelude.Pair: Such a function call will always end up in the wrong branch.

For instance, when I look at the code generated by the JS backend, we were just lucky that it worked correctly in this case.

brainrake commented 2 years ago

I may have hit this on javascript, here's what the error looks like:

/home/ssdd/dev/responsible/build/exec/hello:1225
 const $4 = $1($3);
            ^

TypeError: $1 is not a function
    at Control_App_bindApp (/home/ssdd/dev/responsible/build/exec/hello:1225:13)
    at Control_App_x3ex3ex3d_Monad_x28Appx20x24esx29 (/home/ssdd/dev/responsible/build/exec/hello:1113:9)
    at /home/ssdd/dev/responsible/build/exec/hello:363:407
    at Control_App_bindApp (/home/ssdd/dev/responsible/build/exec/hello:1227:27)
    at Control_App_x3ex3ex3d (/home/ssdd/dev/responsible/build/exec/hello:1237:9)
    at Examples_HelloNode_hello (/home/ssdd/dev/responsible/build/exec/hello:445:9)
    at /home/ssdd/dev/responsible/build/exec/hello:453:345
    at Control_App_bindApp (/home/ssdd/dev/responsible/build/exec/hello:1227:27)
    at Control_App_x3ex3ex3d (/home/ssdd/dev/responsible/build/exec/hello:1237:9)
    at /home/ssdd/dev/responsible/build/exec/hello:1349:10

When compiling with chez backend, I get Invalid memory reference as above. I can't reduce the code to a small example right now. If I remove a putStrLn, the error goes away on both backends.

jutaro commented 1 year ago

I hit this error in my program as well . Not a nice experience. What can be a workaround? In my case it is a recursive function with a LazyList.