brili: Problem when deserializing large integer constants from JSON

[keikun555]

To reproduce:

❯ cat test/overflow.bril
@main() {
  x: int = const 9223372036854775807;
  one: int = const 1;
  three: int = const 3;
  y: int = add x one;
  print y;
  y: int = mul x three;
  print y;
}
❯
❯ bril2json < test/overflow.bril | brili
-9223372036854775807
-9223372036854775808
❯ bril2json < test/overflow.bril | brilirs
-9223372036854775808
9223372036854775805
❯

The Bril documentation on integers writes:

int: 64-bit, two’s complement, signed integers.

I wonder which one is correct?

[Pat-Lafon]

The brilirs version is consistent with the Wrapping<i64> type in Rust. https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=24433b06279415b718abed7a1ae3ad55

I would guess brili is doing the multiplication with a larger integer format and then truncating down to 64 bits.

[keikun555]

It might be the JSON parser in typescript truncating the input integer before it can be converted to a bigint

let prog = JSON.parse(await readStdin()) as bril.Program;

[Pat-Lafon]

Try printing out x then to see if the value is different. Might also be interesting to print out val here before it gets converted to bigInt

bril/brili.ts

Line 466 in daaff28

let val = getInt(instr, state.env, 0) * getInt(instr, state.env, 1);

[keikun555]

So looks like it's part of the problem.

❯ cat test/bignumber.bril
@main() {
  x: int = const 9223372036854775807;
  print x;
}
❯ bril2json < test/bignumber.bril | brili
9223372036854775808
❯ bril2json < test/bignumber.bril | brilirs
9223372036854775807

Here's a StackOverflow page that talks about JSON.parse and numbers.

[keikun555]

Also logged the val using this diff

❯ git diff | cat
diff --git a/brili.ts b/brili.ts
index 2a88470..ba00ea6 100644
--- a/brili.ts
+++ b/brili.ts
@@ -464,6 +464,7 @@ function evalInstr(instr: bril.Instruction, state: State): Action {

   case "mul": {
     let val = getInt(instr, state.env, 0) * getInt(instr, state.env, 1);
+    console.log(val);
     val = BigInt.asIntN(64, val);
     state.env.set(instr.dest, val);
     return NEXT;
❯ bril2json < test/bril2z3/overflow.bril | deno run --no-config vendor/bril/brili.ts
-9223372036854775807
27670116110564327424n # <== from the change
-9223372036854775808
❯

[keikun555]

There's also a JS package for JSON parsing with bigints

[sampsyo]

Thanks for reporting this! Fortunately, it's pretty easy to confirm that JSON deserialization is causing the problem; there's no need to observe it "in situ" in the interpreter:

$ deno
JSODeno 1.37.2
exit using ctrl+d, ctrl+c, or close()
REPL is running with all permissions allowed.
To specify permissions, run `deno repl` with allow flags.
> JSON.parse("9223372036854775807")
9223372036854776000

It's too bad that JSON.parse doesn't seem to be flexible enough to fix this. I am not wild about taking a whole new JSON parsing dependency for the interpreter, but it may be the only option until the relevant ECMAScript proposal is adopted. :(

[sampsyo]

Good news: according to MDN, the necessary JavaScript feature is now Stage 3 and is in most JavaScript engines. The outlier is WebKit, but that also just got merged last month: WebKit/WebKit@e2c5cd5

Anyway, we could now use a custom reviver to get BigInts out of JSON. I'd merge a PR if anyone comes up with one.