add check for division by zero

Gillian-JS/Examples/Cosette/check_div_by_zero.js

@@ -0,0 +1 @@
+var a = 3 / 1;

Gillian-JS/lib/Compiler/JS2JSIL_Compiler.ml

@@ -225,6 +225,10 @@ let make_get_value_call x err =
         [ x_v ] )
   | Some x_v -> (x_v, LBasic Skip, [])
 
+let make_check_nonzero_call x err =
+  let x_n = number_var_of_var x in
+  (x_n, LCall (x_n, Lit (String checkNonZero), [ x ], Some err, None))
+
 let make_to_number_call x x_v err =
   let x_n = number_var_of_var x in
   (x_n, LCall (x_n, Lit (String toNumberName), [ PVar x_v ], Some err, None))
@@ -408,16 +412,25 @@ let translate_multiplicative_binop x1 x2 x1_v x2_v aop err =
     LBasic (Assignment (x_r, BinOp (PVar x1_n, jsil_aop, PVar x2_n)))
   in
 
+  let nonzero_err, nonzero_cmd =
+    match aop with
+    | JS_Parser.Syntax.Div | JS_Parser.Syntax.Mod ->
+        make_check_nonzero_call (PVar x2_n) err
+    | _ -> ("", LBasic Skip)
+  in
+
   let new_cmds =
     [
       (None, cmd_tn_x1);
       (*  x1_n := i__toNumber (x1_v) with err  *)
       (None, cmd_tn_x2);
       (*  x2_n := i__toNumber (x2_v) with err  *)
+      (None, nonzero_cmd);
+      (* x2_n_n := "check_nonzero"(x_2_n) with elab; *)
       (None, cmd_ass_xr) (*  x_r := x1_n * x2_n                   *);
     ]
   in
-  let new_errs = [ x1_n; x2_n ] in
+  let new_errs = [ x1_n; x2_n; nonzero_err ] in
   (new_cmds, new_errs, x_r)
 
 let translate_binop_plus x1 x2 x1_v x2_v err =

Gillian-JS/lib/Compiler/JS2JSIL_Helpers.ml

@@ -198,6 +198,7 @@ let var_args = "x__args"
 let var_er = "x__er"
 let var_er_metadata = "x__er_m"
 let var_sc_first = "x__sc_fst"
+let checkNonZero = "check_nonzero"
 
 let js2jsil_spec_vars =
   [ var_this; var_scope; var_scope_final; var_se; var_te; var_er ]

Gillian-JS/runtime/JS2JSIL/Init.jsil

@@ -523,7 +523,6 @@ proc setupInitialHeap () {
 
 
 
-
 			(* Date object *)
 
 			ret := "create_object_with_call_construct_concrete" ($ldate, "Date_call", "Date_construct", 7);

Gillian-JS/runtime/JS2JSIL/Internals.jsil

@@ -1464,4 +1464,14 @@ proc i__toStringComputed (v) {
 
   rlab: return;
   elab: throw
+};
+
+(* ************************ *)
+(* Check for division by zero *)
+(* ************************ *)
+
+proc check_nonzero (x) {
+   goto [x = 0.] elab rlab;
+   rlab: ret := null; return;
+   elab: ret := null; throw
 };