Primops: MachineInts: fix OP_underspec

src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst

@@ -344,6 +344,7 @@ let is_BitVector_primitive head args =
     | _ -> false
 
 let rec encode_const c env =
+  Errors.with_ctx "While encoding a constant to SMT" (fun () ->
     match c with
     | Const_unit -> mk_Term_unit, []
     | Const_bool true -> boxBool mkTrue, []
@@ -358,7 +359,7 @@ let rec encode_const c env =
     | Const_effect -> mk_Term_type, []
     | Const_real r -> boxReal (mkReal r), []
     | c -> failwith (BU.format1 "Unhandled constant: %s" (Print.const_to_string c))
-
+  )
 and encode_binders (fuel_opt:option term) (bs:Syntax.binders) (env:env_t) :
                             (list fv                       (* translated bound variables *)
                             * list term                    (* guards *)

src/typechecker/FStar.TypeChecker.Primops.MachineInts.fst

@@ -41,7 +41,7 @@ let bounded_arith_ops_for (k : machint_kind) : mymon unit =
   (* Unsigned ints have more operators *)
   let sz = width k in
   let modulus = Z.shift_left_big_int Z.one (Z.of_int_fs sz) in
-  let mod x = Z.mod_big_int x modulus in
+  let mod (x : Z.t) : Z.t = Z.mod_big_int x modulus in
   if is_unsigned k then
     emit [
       (* modulo operators *)
@@ -68,9 +68,9 @@ let bounded_arith_ops_for (k : machint_kind) : mymon unit =
   (* Most unsigneds, except SizeT, have underspec ops *)
   if is_unsigned k && k <> SizeT then
     emit [
-      mk2 0 (nm "add_underspec") (fun (x y : machint k) -> make_as x (Z.add_big_int (v x) (v y)));
-      mk2 0 (nm "sub_underspec") (fun (x y : machint k) -> make_as x (Z.sub_big_int (v x) (v y)));
-      mk2 0 (nm "mul_underspec") (fun (x y : machint k) -> make_as x (Z.mult_big_int (v x) (v y)));
+      mk2 0 (nm "add_underspec") (fun (x y : machint k) -> make_as x (mod (Z.add_big_int (v x) (v y))));
+      mk2 0 (nm "sub_underspec") (fun (x y : machint k) -> make_as x (mod (Z.sub_big_int (v x) (v y))));
+      mk2 0 (nm "mul_underspec") (fun (x y : machint k) -> make_as x (mod (Z.mult_big_int (v x) (v y))));
     ]
   else return ();!
 

tests/micro-benchmarks/Makefile

@@ -29,4 +29,4 @@ clean:
 	rm -rf _cache
 	rm -rf _output
 
-.PRECIOUS: *.ml
+.PRECIOUS: %.ml

ulib/FStar.HyperStack.ST.fsti

@@ -597,3 +597,10 @@ val ralloc_drgn_mm (#a:Type) (#rel:preorder a) (d:drgn) (init:a)
     HS.is_mm r /\
     ralloc_post (rid_of_drgn d) init m0 r m1)
 
+
+(* This causes the verification conditition for the continuation
+of the call to this function to be done in a separate Z3 query. *)
+inline_for_extraction
+let break_vc ()
+  : STATE unit (fun p h -> spinoff (squash (p () h)))
+  = ()