Merge pull request #3050 from FStarLang/nik_3049

Fixing a division by zero in modulus

src/typechecker/FStar.TypeChecker.Cfg.fst

@@ -542,22 +542,23 @@ let built_in_primitive_steps : prim_step_set =
         | _ -> failwith "Unexpected number of arguments"
     in
 
-    (* division is special cased since we must avoid zero denominators *)
-    let division_op : psc -> EMB.norm_cb -> universes -> args -> option term
+    (* division and modulus are special cased since we must avoid zero denominators *)
+    let division_modulus_op op : psc -> EMB.norm_cb -> universes -> args -> option term
       = fun psc _norm_cb _us args ->
         match args with
         | [(a1, None); (a2, None)] ->
             begin match try_unembed_simple EMB.e_int a1,
                         try_unembed_simple EMB.e_int a2 with
             | Some m, Some n ->
               if Z.to_int_fs n <> 0
-              then Some (embed_simple EMB.e_int psc.psc_range (Z.div_big_int m n))
+              then Some (embed_simple EMB.e_int psc.psc_range (op m n))
               else None
 
             | _ -> None
             end
         | _ -> failwith "Unexpected number of arguments"
     in
+
     let bogus_cbs = {
         NBE.iapp = (fun h _args -> h);
         NBE.translate = (fun _ -> failwith "bogus_cbs translate");
@@ -607,8 +608,8 @@ let built_in_primitive_steps : prim_step_set =
          (PC.op_Division,
              2,
              0,
-             division_op,
-             (fun _us -> NBETerm.division_op));
+             division_modulus_op Z.div_big_int,
+             (fun _us -> NBETerm.division_modulus_op Z.div_big_int));
          (PC.op_LT,
              2,
              0,
@@ -632,8 +633,8 @@ let built_in_primitive_steps : prim_step_set =
          (PC.op_Modulus,
              2,
              0,
-             binary_int_op (fun x y -> Z.mod_big_int x y),
-             NBETerm.binary_int_op (fun x y -> Z.mod_big_int x y));
+             division_modulus_op Z.mod_big_int,
+             (fun _us -> NBETerm.division_modulus_op Z.mod_big_int));
          (PC.op_Negation,
              1,
              0,

src/typechecker/FStar.TypeChecker.NBETerm.fst

@@ -939,13 +939,13 @@ let or_op (args:args) : option t =
     end
   | _ -> failwith "Unexpected number of arguments"
 
-let division_op (args:args) : option t =
+let division_modulus_op (op:Z.bigint -> Z.bigint -> Z.bigint) (args:args) : option t =
   match args with
   | [a1; a2] -> begin
     match arg_as_int a1, arg_as_int a2 with
     | Some m, Some n ->
       if Z.to_int_fs n <> 0
-      then Some (embed e_int bogus_cbs (Z.div_big_int m n))
+      then Some (embed e_int bogus_cbs (op m n))
       else None
     | _ -> None
     end

src/typechecker/FStar.TypeChecker.NBETerm.fsti

@@ -363,6 +363,6 @@ val dummy_interp : Ident.lid -> args -> option t
 val prims_to_fstar_range_step : args -> option t
 
 val mk_range : args -> option t
-val division_op : args -> option t
+val division_modulus_op (op:Z.bigint -> Z.bigint -> Z.bigint) : args -> option t
 val and_op : args -> option t
 val or_op : args -> option t

tests/bug-reports/Bug3049.fst

@@ -0,0 +1,4 @@
+module Bug3049
+
+[@@expect_failure [19]]
+let test = 0 % 0