Idris2
Idris2 copied to clipboard
Invalid memory reference on Chez backend
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')
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.
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.
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.