Do not activate the sanity (invariant) checks by default

8 files changed, 16 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index e0367d73..88cb7d05 100644
--- a/Makefile
+++ b/Makefile
@@ -30,11 +30,8 @@ CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
 AENEAS_EXE ?= bin/aeneas
 
 # The user can specify additional translation options for Aeneas.
-# By default we do:
-# - unfold all the monadic let bindings to matches (required by F*)
-# - insert calls to the normalizer in the translated code to test the
-#   generated unit functions
-OPTIONS +=
+# By default we activate the (expensive) sanity checks.
+OPTIONS ?= -checks
 
 #
 # The rules use (and update) the following variables
diff --git a/compiler/Config.ml b/compiler/Config.ml
index fe110ee4..48ee0a06 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -35,11 +35,11 @@ let backend = ref FStar
 
 (** {1 Interpreter} *)
 
-(** Check that invariants are maintained whenever we execute a statement
-
-    TODO: rename to sanity_checks.
+(** Activate the sanity checks, and in particular the invariant checks
+    that are performed at every evaluation step. This is very expensive
+    (~100x slow down) but very efficient to catch mistakes early.
  *)
-let check_invariants = ref true
+let sanity_checks = ref false
 
 (** Expand all symbolic values containing borrows upon introduction - allows
     to use restrict ourselves to a simpler model for the projectors over
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 8c9c0e72..2f793f4a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -2155,7 +2155,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
      ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
 
   (* Check that the abstractions are destructured *)
-  if !Config.check_invariants then (
+  if !Config.sanity_checks then (
     let destructure_shared_values = true in
     assert (abs_is_destructured destructure_shared_values ctx abs0);
     assert (abs_is_destructured destructure_shared_values ctx abs1));
@@ -2487,7 +2487,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
   in
 
   (* Sanity check *)
-  if !Config.check_invariants then assert (abs_is_destructured true ctx abs);
+  if !Config.sanity_checks then assert (abs_is_destructured true ctx abs);
   (* Return *)
   abs
 
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 4cc74aae..8d485483 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -714,7 +714,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
         ^ eval_ctx_to_string !joined_ctx));
 
     (* Sanity check *)
-    if !Config.check_invariants then Invariants.check_invariants !joined_ctx;
+    if !Config.sanity_checks then Invariants.check_invariants !joined_ctx;
     (* Return *)
     ctx1
   in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 74f9ba2c..bf459e41 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1580,7 +1580,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
        ^ eval_ctx_to_string tgt_ctx));
 
     (* Sanity check *)
-    if !Config.check_invariants then
+    if !Config.sanity_checks then
       Invariants.check_borrowed_values_invariant tgt_ctx;
 
     (* End all the borrows which appear in the *new* abstractions *)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 729a3577..999b8ab0 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -311,7 +311,7 @@ let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if !Config.check_invariants then
+      if !Config.sanity_checks then
         if ctx1 <> ctx then (
           let msg =
             "Unexpected environment update:\nNew environment:\n"
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index e0e3f354..fa0d7436 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -804,7 +804,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
   M.iter check_info !infos
 
 let check_invariants (ctx : eval_ctx) : unit =
-  if !Config.check_invariants then (
+  if !Config.sanity_checks then (
     log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx));
     check_loans_borrows_relation_invariant ctx;
     check_borrowed_values_invariant ctx;
diff --git a/compiler/Main.ml b/compiler/Main.ml
index e350da8a..7f98f581 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -107,10 +107,10 @@ let () =
         Arg.Set split_files,
         " Split the definitions between different files for types, functions, \
          etc." );
-      ( "-no-check-inv",
-        Arg.Clear check_invariants,
-        " Deactivate the invariant sanity checks performed at every evaluation \
-         step. Dramatically increases speed." );
+      ( "-checks",
+        Arg.Set sanity_checks,
+        " Activate extensive sanity checks (warning: causes a ~100 times slow \
+         down)." );
       ( "-no-gen-lib-entry",
         Arg.Clear generate_lib_entry_point,
         " Do not generate the entry point file for the generated library (only \