Merge pull request #2925 from FStarLang/_nik_2705

Making AdmitWithoutDefinition (240) an error, by default
FStarLang · Jul 29, 2023 · 8c37e87 · 8c37e87
2 parents 2129510 + 7478255
commit 8c37e87
Show file tree

Hide file tree

Showing 23 changed files with 54 additions and 88 deletions.
diff --git a/doc/book/code/Universes.fst b/doc/book/code/Universes.fst
@@ -1,4 +1,5 @@
 module Universes
+#push-options "--warn_error -240" //some defs are expected to fail
 
 //SNIPPET_START: ty$
 let ty : Type = Type

diff --git a/doc/tutorial/code/exercises/Makefile b/doc/tutorial/code/exercises/Makefile
@@ -36,6 +36,9 @@ LowStar.Ex3.fst
 
 include ../../../Makefile.include
 
+# exercises have val without definitions, by design
+OTHERFLAGS+=--warn_error -240
+
 verify-%: __force__
 	$(FSTAR) --include $(FSTAR_CONTRIB)/Platform/fst --include $(FSTAR_CONTRIB)/CoreCrypto/fst $*
 

diff --git a/doc/tutorial/code/solutions/Ex12b1.Format.fst b/doc/tutorial/code/solutions/Ex12b1.Format.fst
@@ -95,18 +95,21 @@ let response s t =
    functions---they just return messages---so these three lemmas are
    sufficient *)
 
+assume
 val req_resp_distinct:
   s:string -> s':string16 -> t':string ->
   Lemma (requires True)
         (ensures (request s <> response s' t'))
         [SMTPat (request s); SMTPat (response s' t')]
 
+assume
 val req_injective:
   s0:string -> s1:string ->
   Lemma (requires (b2t (Seq.eq (request s0) (request s1))))
         (ensures  (s0==s1))
         (*[SMTPat (request s0); SMTPat (request s1)]*)
 
+assume
 val resp_injective:
   s0:string16 -> t0:string -> s1:string16 -> t1:string ->
   Lemma (requires (b2t (Seq.eq (response s0 t0) (response s1 t1))))

diff --git a/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml b/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml
diff --git a/src/basic/FStar.Errors.Codes.fst b/src/basic/FStar.Errors.Codes.fst
@@ -256,7 +256,7 @@ let default_settings : list error_setting =
     Unused01                                          , CFatal, 237;
     Warning_PluginNotImplemented                      , CError, 238;
     Warning_AddImplicitAssumeNewQualifier             , CWarning, 239;
-    Warning_AdmitWithoutDefinition                    , CWarning, 240;
+    Error_AdmitWithoutDefinition                      , CError, 240;
     Warning_CachedFile                                , CWarning, 241;
     Warning_DefinitionNotTranslated                   , CWarning, 242;
     Warning_DependencyFound                           , CWarning, 243;

diff --git a/src/basic/FStar.Errors.Codes.fsti b/src/basic/FStar.Errors.Codes.fsti
@@ -266,7 +266,7 @@ type raw_error =
   | Fatal_WhenClauseNotSupported
   | Unused01
   | Warning_AddImplicitAssumeNewQualifier
-  | Warning_AdmitWithoutDefinition
+  | Error_AdmitWithoutDefinition
   | Warning_CachedFile
   | Warning_DefinitionNotTranslated
   | Warning_DependencyFound

diff --git a/src/syntax/FStar.Syntax.DsEnv.fst b/src/syntax/FStar.Syntax.DsEnv.fst
@@ -1111,21 +1111,15 @@ let check_admits env m =
           | _ ->
             if not (Options.interactive ()) then
               FStar.Errors.log_issue (range_of_lid l)
-                (Errors.Warning_AdmitWithoutDefinition, (BU.format1 "Admitting %s without a definition" (Ident.string_of_lid l)));
+                (Errors.Error_AdmitWithoutDefinition, (BU.format1 "%s is declared but no definition was found; add an 'assume' if this is intentional" (Ident.string_of_lid l)));
             let quals = Assumption :: se.sigquals in
             BU.smap_add (sigmap env) (string_of_lid l) ({ se with sigquals = quals }, false);
             l::lids
         end
       | _ -> lids) []
   in
-  //slap on the Assumption qualifier to module declarations that were admitted
-  //the code above does it just for the sigelts in env
-  { m with declarations = m.declarations |> List.map (fun s ->
-      match s.sigel with
-      | Sig_declare_typ {lid} when List.existsb (fun l -> lid_equals l lid) admitted_sig_lids -> { s with sigquals = Assumption::s.sigquals }
-      | _ -> s
-    ) }
-
+  m
+
 let finish env modul =
   modul.declarations |> List.iter (fun se ->
     let quals = se.sigquals in

diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
@@ -2,6 +2,8 @@ FSTAR_HOME=../..
 include $(FSTAR_HOME)/examples/Makefile.include
 include $(FSTAR_HOME)/ulib/ml/Makefile.include
 
+OTHERFLAGS+=--warn_error +240
+
 all: verify iverify not-verify extract
 
 ##################

diff --git a/tests/error-messages/ArgsAndQuals.fst.expected b/tests/error-messages/ArgsAndQuals.fst.expected
@@ -1,6 +1,6 @@
 >> Got issues: [
-ArgsAndQuals.fst(25,16-25,18): (Error 91) Inconsistent implicit argument annotation on argument uu___#182
+ArgsAndQuals.fst(25,16-25,18): (Error 91) Inconsistent implicit argument annotation on argument uu___#74
 >>]
-ArgsAndQuals.fst(23,4-23,9): (Warning 240) Admitting ArgsAndQuals.test1 without a definition
+ArgsAndQuals.fst(23,4-23,9): (Warning 240) ArgsAndQuals.test1 is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: ArgsAndQuals
 All verification conditions discharged successfully
diff --git a/tests/error-messages/Erasable.fst.expected b/tests/error-messages/Erasable.fst.expected
@@ -16,7 +16,7 @@ Erasable.fst(52,0-52,17): (Error 162) Mismatch of attributes between declaration
 >> Got issues: [
 Erasable.fst(59,0-59,29): (Error 162) Mismatch of attributes between declaration and definition: Declaration is marked `erasable` but the definition is not
 >>]
-Erasable.fst(49,4-49,11): (Warning 240) Admitting Erasable.e_nat_2 without a definition
-Erasable.fst(56,4-56,11): (Warning 240) Admitting Erasable.e_nat_3 without a definition
+Erasable.fst(49,4-49,11): (Warning 240) Erasable.e_nat_2 is declared but no definition was found; add an 'assume' if this is intentional
+Erasable.fst(56,4-56,11): (Warning 240) Erasable.e_nat_3 is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: Erasable
 All verification conditions discharged successfully
diff --git a/tests/error-messages/Makefile b/tests/error-messages/Makefile
@@ -6,7 +6,7 @@ FSTAR_FILES=$(wildcard *.fst)
 # 241: "unable to load checked file"
 # 247: "checked file was not written"
 # 333: "unable to read hints"
-OTHERFLAGS+=--warn_error -241-247-333-274
+OTHERFLAGS+=--warn_error -241-247-333-274+240
 
 # Sorry, without this we can get noise in error locations.
 # See issue #1993. Also, warnings from dependencies would

diff --git a/tests/error-messages/NegativeTests.Bug260.fst.expected b/tests/error-messages/NegativeTests.Bug260.fst.expected
@@ -1,6 +1,6 @@
 >> Got issues: [
 NegativeTests.Bug260.fst(26,12-26,19): (Error 19) Subtyping check failed; expected type validity (S (S t)); got type validity (S t); The SMT solver could not prove the query. Use --query_stats for more details. (see also NegativeTests.Bug260.fst(23,37-26,9))
 >>]
-NegativeTests.Bug260.fst(23,4-23,7): (Warning 240) Admitting NegativeTests.Bug260.bad without a definition
+NegativeTests.Bug260.fst(23,4-23,7): (Warning 240) NegativeTests.Bug260.bad is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.Bug260
 All verification conditions discharged successfully
diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected
@@ -7,7 +7,7 @@ NegativeTests.False.fst(30,18-30,41): (Error 12) Expected type "Prims.l_True \/
 NegativeTests.False.fst(30,42-30,66): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right Prims.T" has type "Prims.sum Prims.l_True (*?u6*) _"
 NegativeTests.False.fst(30,42-30,66): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right Prims.T" has type "Prims.sum Prims.l_True Prims.trivial"
 >>]
-NegativeTests.False.fst(21,4-21,7): (Warning 240) Admitting NegativeTests.False.bar without a definition
-NegativeTests.False.fst(28,4-28,10): (Warning 240) Admitting NegativeTests.False.absurd without a definition
+NegativeTests.False.fst(21,4-21,7): (Warning 240) NegativeTests.False.bar is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.False.fst(28,4-28,10): (Warning 240) NegativeTests.False.absurd is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.False
 All verification conditions discharged successfully
diff --git a/tests/error-messages/NegativeTests.Neg.fst.expected b/tests/error-messages/NegativeTests.Neg.fst.expected
@@ -31,10 +31,10 @@ NegativeTests.Neg.fst(59,0-60,17): (Error 309) Type annotation _: Type0{Negative
 >> Got issues: [
 NegativeTests.Neg.fst(63,0-63,32): (Error 309) Type annotation _: Type{Prims.l_False} for inductive NegativeTests.Neg.t2 is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers
 >>]
-NegativeTests.Neg.fst(18,4-18,5): (Warning 240) Admitting NegativeTests.Neg.x without a definition
-NegativeTests.Neg.fst(22,4-22,5): (Warning 240) Admitting NegativeTests.Neg.y without a definition
-NegativeTests.Neg.fst(36,4-36,27): (Warning 240) Admitting NegativeTests.Neg.test_precondition_label without a definition
-NegativeTests.Neg.fst(40,4-40,28): (Warning 240) Admitting NegativeTests.Neg.test_postcondition_label without a definition
-NegativeTests.Neg.fst(44,4-44,17): (Warning 240) Admitting NegativeTests.Neg.bad_projector without a definition
+NegativeTests.Neg.fst(18,4-18,5): (Warning 240) NegativeTests.Neg.x is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Neg.fst(22,4-22,5): (Warning 240) NegativeTests.Neg.y is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Neg.fst(36,4-36,27): (Warning 240) NegativeTests.Neg.test_precondition_label is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Neg.fst(40,4-40,28): (Warning 240) NegativeTests.Neg.test_postcondition_label is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Neg.fst(44,4-44,17): (Warning 240) NegativeTests.Neg.bad_projector is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.Neg
 All verification conditions discharged successfully
diff --git a/tests/error-messages/NegativeTests.Set.fst.expected b/tests/error-messages/NegativeTests.Set.fst.expected
@@ -7,8 +7,8 @@ NegativeTests.Set.fst(33,9-33,67): (Error 19) assertion failed; The SMT solver c
 >> Got issues: [
 NegativeTests.Set.fst(38,9-38,52): (Error 19) assertion failed; The SMT solver could not prove the query. Use --query_stats for more details.
 >>]
-NegativeTests.Set.fst(25,4-25,16): (Warning 240) Admitting NegativeTests.Set.should_fail1 without a definition
-NegativeTests.Set.fst(30,4-30,16): (Warning 240) Admitting NegativeTests.Set.should_fail2 without a definition
-NegativeTests.Set.fst(35,4-35,16): (Warning 240) Admitting NegativeTests.Set.should_fail3 without a definition
+NegativeTests.Set.fst(25,4-25,16): (Warning 240) NegativeTests.Set.should_fail1 is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Set.fst(30,4-30,16): (Warning 240) NegativeTests.Set.should_fail2 is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Set.fst(35,4-35,16): (Warning 240) NegativeTests.Set.should_fail3 is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.Set
 All verification conditions discharged successfully
diff --git a/tests/error-messages/NegativeTests.ShortCircuiting.fst.expected b/tests/error-messages/NegativeTests.ShortCircuiting.fst.expected
@@ -4,7 +4,7 @@ NegativeTests.ShortCircuiting.fst(21,16-21,33): (Error 19) Subtyping check faile
 >> Got issues: [
 NegativeTests.ShortCircuiting.fst(25,11-25,36): (Error 19) assertion failed; The SMT solver could not prove the query. Use --query_stats for more details. (see also prims.fst(430,90-430,102))
 >>]
-NegativeTests.ShortCircuiting.fst(19,4-19,7): (Warning 240) Admitting NegativeTests.ShortCircuiting.bad without a definition
-NegativeTests.ShortCircuiting.fst(23,4-23,6): (Warning 240) Admitting NegativeTests.ShortCircuiting.ff without a definition
+NegativeTests.ShortCircuiting.fst(19,4-19,7): (Warning 240) NegativeTests.ShortCircuiting.bad is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.ShortCircuiting.fst(23,4-23,6): (Warning 240) NegativeTests.ShortCircuiting.ff is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.ShortCircuiting
 All verification conditions discharged successfully
diff --git a/tests/error-messages/NegativeTests.Termination.fst.expected b/tests/error-messages/NegativeTests.Termination.fst.expected
@@ -28,15 +28,15 @@ NegativeTests.Termination.fst(89,29-89,31): (Error 19) Could not prove terminati
 >> Got issues: [
 NegativeTests.Termination.fst(96,20-96,26): (Error 19) Could not prove termination of this recursive call; The SMT solver could not prove the query. Use --query_stats for more details. (see also NegativeTests.Termination.fst(94,2-96,26))
 >>]
-NegativeTests.Termination.fst(18,4-18,9): (Warning 240) Admitting NegativeTests.Termination.bug15 without a definition
-NegativeTests.Termination.fst(23,4-23,18): (Warning 240) Admitting NegativeTests.Termination.repeat_diverge without a definition
-NegativeTests.Termination.fst(31,4-31,17): (Warning 240) Admitting NegativeTests.Termination.ackermann_bad without a definition
-NegativeTests.Termination.fst(38,4-38,14): (Warning 240) Admitting NegativeTests.Termination.length_bad without a definition
-NegativeTests.Termination.fst(50,4-50,18): (Warning 240) Admitting NegativeTests.Termination.strangeZeroBad without a definition
-NegativeTests.Termination.fst(61,4-61,6): (Warning 240) Admitting NegativeTests.Termination.t1 without a definition
-NegativeTests.Termination.fst(69,4-69,8): (Warning 240) Admitting NegativeTests.Termination.plus without a definition
-NegativeTests.Termination.fst(77,4-77,9): (Warning 240) Admitting NegativeTests.Termination.plus' without a definition
-NegativeTests.Termination.fst(84,4-84,9): (Warning 240) Admitting NegativeTests.Termination.minus without a definition
-NegativeTests.Termination.fst(91,4-91,7): (Warning 240) Admitting NegativeTests.Termination.xxx without a definition
+NegativeTests.Termination.fst(18,4-18,9): (Warning 240) NegativeTests.Termination.bug15 is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(23,4-23,18): (Warning 240) NegativeTests.Termination.repeat_diverge is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(31,4-31,17): (Warning 240) NegativeTests.Termination.ackermann_bad is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(38,4-38,14): (Warning 240) NegativeTests.Termination.length_bad is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(50,4-50,18): (Warning 240) NegativeTests.Termination.strangeZeroBad is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(61,4-61,6): (Warning 240) NegativeTests.Termination.t1 is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(69,4-69,8): (Warning 240) NegativeTests.Termination.plus is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(77,4-77,9): (Warning 240) NegativeTests.Termination.plus' is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(84,4-84,9): (Warning 240) NegativeTests.Termination.minus is declared but no definition was found; add an 'assume' if this is intentional
+NegativeTests.Termination.fst(91,4-91,7): (Warning 240) NegativeTests.Termination.xxx is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.Termination
 All verification conditions discharged successfully
diff --git a/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected
@@ -1,6 +1,6 @@
 >> Got issues: [
 NegativeTests.ZZImplicitFalse.fst(20,26-20,27): (Error 66) Failed to resolve implicit argument ?1 of type Prims.l_False introduced for user-provided implicit term at NegativeTests.ZZImplicitFalse.fst(20,26-20,27)
 >>]
-NegativeTests.ZZImplicitFalse.fst(18,4-18,7): (Warning 240) Admitting NegativeTests.ZZImplicitFalse.wtf without a definition
+NegativeTests.ZZImplicitFalse.fst(18,4-18,7): (Warning 240) NegativeTests.ZZImplicitFalse.wtf is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: NegativeTests.ZZImplicitFalse
 All verification conditions discharged successfully
diff --git a/tests/error-messages/PatCoerce.fst.expected b/tests/error-messages/PatCoerce.fst.expected
@@ -1,6 +1,6 @@
 >> Got issues: [
 PatCoerce.fst(25,4-25,8): (Error 114) Type of pattern (Prims.bool) does not match type of scrutinee (Type0)
 >>]
-PatCoerce.fst(20,4-20,7): (Warning 240) Admitting PatCoerce.bla without a definition
+PatCoerce.fst(20,4-20,7): (Warning 240) PatCoerce.bla is declared but no definition was found; add an 'assume' if this is intentional
 Verified module: PatCoerce
 All verification conditions discharged successfully
diff --git a/tests/micro-benchmarks/Erasable.ml.expected b/tests/micro-benchmarks/Erasable.ml.expected
@@ -1,6 +1,4 @@
 open Prims
-type e_nat_2 = unit
-type e_nat_3 = unit
 type e_unit_5 = unit
 type ('a, 'uuuuu) repr = 'a
 let return : 'a . 'a -> ('a, unit) repr = fun x -> x

diff --git a/tests/micro-benchmarks/Makefile b/tests/micro-benchmarks/Makefile
@@ -1,5 +1,5 @@
 FSTAR_HOME=../..
-
+OTHERFLAGS+=--warn_error +240
 FSTAR_FILES = $(wildcard *.fst)
 
 all: verify-all ns-resolution
@@ -18,7 +18,7 @@ verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTA
 $(CACHE_DIR)/MustEraseForExtraction.fst.checked: OTHERFLAGS += --warn_error @318
 
 %.ml: %.fst
-	$(FSTAR) --codegen OCaml --extract $(subst .ml,, $@) $^
+	$(FSTAR) $(OTHERFLAGS) --codegen OCaml --extract $(subst .ml,, $@) $^
 
 %.ml-cmp: %.ml %.ml.expected
 	diff -u --strip-trailing-cr $< $<.expected