dfinity / motoko

Simple high-level language for writing Internet Computer canisters
Apache License 2.0
514 stars 97 forks source link

Interpreter overflows in Nat.toText #2844

Open crusso opened 3 years ago

crusso commented 3 years ago

https://forum.dfinity.org/t/arithmetic-overflow/7955

osa1 commented 3 years ago

This bug seems to be fixed in current motoko and motoko-base HEAD commits. I tried both of the reproducers, both worked as expected.

rossberg commented 3 years ago

Note that this seems to be in the interpreter, which is even weirder.

osa1 commented 3 years ago

Ah, didn't realize it's in the interpreter. In that case the bug still exists.

ggreif commented 3 years ago

I could eliminate the base dependency by having

import Prim "mo:⛔";

loop {
    Prim.debugPrint(debug_show(136 : Nat32/32));
}

The error appears as:

test/run/overf-bug.mo:4.39-4.53: execution error, arithmetic overflow
ggreif commented 3 years ago

When I change the above to just Prim.debugPrint("4") I get

prim:48.29-48.58: internal error, Stack overflow

On my machine this way it prints 173893 lines to stdout. The above snippet makes it to 173890, which is clearly plausible. This reinforces my hunch that the arithmetic evaluator takes a hit under tight stack conditions.

ggreif commented 3 years ago

Since this is an interpreter-only issue and it is unlikely we can rearchitect the evaluator loop to become tail-recursive, I am inclined to close this as won't-fix.

osa1 commented 3 years ago

Stack overflow in OCaml code causing an "arithmetic overflow" error does not seem right. That should be a bug, separate from the issue with stack overflows in the interpreter. Since OCaml is a "safe" language with checked stack overflows I don't think a stack overflow in the interpreter should manifest itself as something other than a "stack overflow" error.

Re: stack overflow in this repro, I think it's caused by this exception handling in recursive calls in the interpreter: https://github.com/dfinity/motoko/blob/c08dfb83117feab7a88b24e6aba32e7c7dcddc1b/src/mo_interpreter/interpret.ml#L375 In the repro the prim is "print". Every time we call "print" we evaluate the continuation within a new exception handler.

If we move error handling to the prim interpreter then we should be able to call the continuation with the exception handler removed, and the code becomes tail recursive.

In pseudo code, we currently evaluate prims like this:

handle_exceptions (evaluate_prim prim expr k)
...
let evaluate_prim prim value k = let prim_result = <evaluate prim> in k prim_result

I suggest we do it like

evaluate_prim prim value k
...
let evaluate_prim prim value k = let prim_result = handle_exceptions (<evaluate prim>) in k prim_result
osa1 commented 3 years ago

I think it could be simpler if we didn't evaluate prims in continuation-passing style. prim evaluator is not recursive and does not call into expression evaluator, so it doesn't take advantage of CPS. It should be a simple refactoring to make it return the value, and then the refactoring I suggest above would be even simpler.

osa1 commented 3 years ago

Yet another way to fix this would be to pass an "exception continuation" (called with the exception in case of an error) to the prim evaluator.

Personally I would prefer simplifying the prim evaluator (making it non-CPS) and handling exceptions in the call site.

rossberg commented 3 years ago

Yes, that sounds plausible to me.

crusso commented 3 years ago

Aren't some of the prims higher-order and do call into the interpreter? I'm thinking Array_tabulate

https://github.com/dfinity/motoko/blob/c08dfb83117feab7a88b24e6aba32e7c7dcddc1b/src/mo_values/prim.ml#L229

osa1 commented 3 years ago

Hm, right. In that case passing an error or exception continuation will be easier.