Global predicates

[klausnat]

Hello,

This is not an issue, more like a question. I want to add global predicates to Gillian-JS

So Gillian-JS will automatically check for runtime errors, such as:

Division by zero (b === 0).

Type errors (if a or b are non-numeric).

in the code below

function divide(a, b) {
  return a / b;
}

var result = divide(10, 0);

So user do not have to write any annotations (assumes, asserts).

What is the best way/path to do it?

[giltho]

Oh, I didn't know Gillian-JS didn't check for division by zero 🤔

So, the way I'd do it is by modifying the JS2JSIL_compiler file
Specifically, this pattern match:

(* line 2946 *)
| JS_Parser.Syntax.BinOp (e1, JS_Parser.Syntax.Arith aop, e2)
    when aop = JS_Parser.Syntax.Times
         || aop = JS_Parser.Syntax.Div || aop = JS_Parser.Syntax.Mod
         || aop = JS_Parser.Syntax.Minus ->

It returns:

... @ annotate_cmds ([ (None, cmd_gv_x2) ] @ new_cmds))

I would create a new function in the runtime called check_nonzero that just does something like
(with approximate syntax)

proc check_nonzero(x) {
   goto [ x = 0. ] fl ctn;
   fl: fail[DivByZero](x);
   ctn: ret := null; return;
}

And then add a call to check_nonzero right before new_cmds if the aop is Div or Mod

That should be enough?

[klausnat]

Thank you very much.