Syntax/Tc: Improving error range for expected failures

When the set of errors do not match the expected set, we will highlight
the @@expect_failure attribute instead of the whole definition.

This works by adding a range to the Sig_fail sigelt, which is modifying
the internal AST. However, since these Sig_fail signatures never make it
to a .checked file, I don't think we need to bump the
cache_version_number.

src/FStarCompiler.fst.config.json

@@ -1,5 +1,5 @@
 {
-  "fstar_exe": "fstar.exe",
+  "fstar_exe": "../bin/fstar.exe",
   "options": [
     "--MLish",
     "--MLish_effect", "FStarC.Compiler.Effect",

src/extraction/FStarC.Extraction.ML.Modul.fst

@@ -171,7 +171,7 @@ let rec extract_meta x : option meta =
                     false x FStarC.Parser.Const.remove_unused_type_parameters_lid)
        with
        | None -> None
-       | Some l -> Some (RemoveUnusedTypeParameters (l, S.range_of_fv fv))
+       | Some (l, _rng) -> Some (RemoveUnusedTypeParameters (l, S.range_of_fv fv))
        end
     | _ -> None
 

src/syntax/FStarC.Syntax.Syntax.fsti

@@ -752,6 +752,7 @@ type sigelt' =
     }
   | Sig_fail                 {
       errs:list int;      // Expected errors (empty for 'any')
+      rng: Range.range;   // range of the `expect_failure`, for error reporting
       fail_in_lax:bool;   // true if should fail in --lax
       ses:list sigelt;    // The sigelts to be checked
   }

src/syntax/FStarC.Syntax.VisitM.fst

@@ -457,9 +457,9 @@ let rec on_sub_sigelt' #m {|d : lvm m |} (se : sigelt') : m sigelt' =
   (* These two below are hardly used, since they disappear after
   typechecking, but are still useful so the desugarer can make use of
   deep_compress_se. *)
-  | Sig_fail {errs; fail_in_lax; ses} ->
+  | Sig_fail {rng; errs; fail_in_lax; ses} ->
     let! ses = ses |> mapM on_sub_sigelt in
-    return <| Sig_fail {errs; fail_in_lax; ses}
+    return <| Sig_fail {rng; errs; fail_in_lax; ses}
 
   | Sig_splice {is_typed; lids; tac} ->
     let! tac = tac |> f_term in
@@ -537,4 +537,4 @@ in
 let lids, _ = Writer.run_writer m in
 BU.print1 "Lids = %s\n" (show lids);
 
-*)
+*)

src/tosyntax/FStarC.ToSyntax.ToSyntax.fst

@@ -644,8 +644,8 @@ let rec generalize_annotated_univs (s:sigelt) :sigelt =
                                         comp=Subst.subst_comp usubst c;
                                         cflags=flags} }
 
-  | Sig_fail {errs; fail_in_lax=lax; ses} ->
-    { s with sigel = Sig_fail {errs;
+  | Sig_fail {errs; rng; fail_in_lax=lax; ses} ->
+    { s with sigel = Sig_fail {errs; rng;
                                fail_in_lax=lax;
                                ses=List.map generalize_annotated_univs ses} }
 
@@ -3260,7 +3260,7 @@ let push_reflect_effect env quals (effect_name:Ident.lid) range =
          Env.push_sigelt env refl_decl // FIXME: Add docs to refl_decl?
     else env
 
-let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int) & bool =
+let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int & Range.range) & bool =
   let warn () =
     if warn then
       Errors.log_issue at Errors.Warning_UnappliedFail
@@ -3271,12 +3271,12 @@ let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int) & bo
    | Tm_fvar fv when S.fv_eq_lid fv head ->
      begin
        match args with
-       | [] -> Some [], true
+       | [] -> Some ([], at.pos), true
        | [(a1, _)] ->
          begin
          match EMB.unembed a1 EMB.id_norm_cb with
          | Some es ->
-           Some (List.map FStarC.BigInt.to_int_fs es), true
+           Some (List.map FStarC.BigInt.to_int_fs es, at.pos), true
          | _ ->
            warn();
            None, true
@@ -3291,27 +3291,27 @@ let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int) & bo
 
 
 // If this is an expect_failure attribute, return the listed errors and whether it's a expect_lax_failure or not
-let get_fail_attr1 warn (at : S.term) : option (list int & bool) =
+let get_fail_attr1 warn (at : S.term) : option (list int & Range.range & bool) =
     let rebind res b =
       match res with
       | None -> None
-      | Some l -> Some (l, b)
+      | Some (l, rng) -> Some (l, rng, b)
     in
     let res, matched = parse_attr_with_list warn at C.fail_attr in
     if matched then rebind res false
     else let res, _ = parse_attr_with_list warn at C.fail_lax_attr in
          rebind res true
 
 // Traverse a list of attributes to find all expect_failures and combine them
-let get_fail_attr warn (ats : list S.term) : option (list int & bool) =
+let get_fail_attr warn (ats : list S.term) : option (list int & Range.range & bool) =
     let comb f1 f2 =
       match f1, f2 with
-      | Some (e1, l1), Some (e2, l2) ->
-        Some (e1@e2, l1 || l2)
+      | Some (e1, rng1, l1), Some (e2, rng2, l2) ->
+        Some (e1@e2, rng1 `Range.union_ranges` rng2, l1 || l2)
 
-      | Some (e, l), None
-      | None, Some (e, l) ->
-        Some (e, l)
+      | Some x, None
+      | None, Some x ->
+        Some x
 
       | _ -> None
     in
@@ -3652,7 +3652,7 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) =
     let attrs = List.map (desugar_term env) d.attrs in
     let attrs = U.deduplicate_terms attrs in
     match get_fail_attr false attrs with
-    | Some (expected_errs, lax) ->
+    | Some (expected_errs, err_rng, lax) ->
       // The `fail` attribute behaves
       // differentrly! We only keep that one on the first new decl.
       let env0 =
@@ -3668,7 +3668,7 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) =
         (* Succeeded desugaring, carry on, but make a Sig_fail *)
         (* Restore attributes, except for fail *)
         let ses = List.map (fun se -> { se with sigattrs = no_fail_attrs attrs }) ses in
-        let se = { sigel = Sig_fail {errs=expected_errs; fail_in_lax=lax; ses};
+        let se = { sigel = Sig_fail {rng=err_rng;errs=expected_errs; fail_in_lax=lax; ses};
                    sigquals = [];
                    sigrng = d.drange;
                    sigmeta = default_sigmeta;
@@ -3695,7 +3695,7 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) =
             let open FStarC.Class.PP in
             let open FStarC.Pprint in
             List.iter Errors.print_issue errs;
-            Errors.log_issue d Errors.Error_DidNotFail [
+            Errors.log_issue err_rng Errors.Error_DidNotFail [
                 prefix 2 1
                   (text "This top-level definition was expected to raise error codes")
                   (pp expected_errs) ^/^

src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti

@@ -54,7 +54,7 @@ val add_modul_to_env: Syntax.modul
                     -> erase_univs:(S.term -> S.term)
                     -> withenv unit
 
-val parse_attr_with_list : bool -> S.term -> lident -> option (list int) & bool
+val parse_attr_with_list : bool -> S.term -> lident -> option (list int & Range.range) & bool
 
-val get_fail_attr1 : bool -> S.term       -> option (list int & bool)
-val get_fail_attr  : bool -> list S.term -> option (list int & bool)
+val get_fail_attr1 : bool -> S.term       -> option (list int & Range.range & bool)
+val get_fail_attr  : bool -> list S.term -> option (list int & Range.range & bool)

src/typechecker/FStarC.TypeChecker.Env.fst

@@ -943,7 +943,7 @@ let fv_has_erasable_attr env fv =
   cache_in_fv_tab env.erasable_types_tab fv f
 
 let fv_has_strict_args env fv =
-  let f () =
+  let f () : bool & option (list int) =
     let attrs = lookup_attrs_of_lid env (S.lid_of_fv fv) in
     match attrs with
     | None -> false, None
@@ -953,7 +953,7 @@ let fv_has_strict_args env fv =
             fst (FStarC.ToSyntax.ToSyntax.parse_attr_with_list
                 false x FStarC.Parser.Const.strict_on_arguments_attr))
       in
-      true, res
+      true, BU.map_opt res fst
   in
   cache_in_fv_tab env.strict_args_tab fv f
 

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -584,7 +584,7 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
         (Print.sigelt_to_string_short se);
     [], [], env
 
-  | Sig_fail {errs=expected_errors; fail_in_lax=lax; ses} ->
+  | Sig_fail {rng=fail_rng; errs=expected_errors; fail_in_lax=lax; ses} ->
     let env' = if lax then { env with admit = true } else env in
     let env' = Env.push env' "expect_failure" in
     (* We need to call push since tc_decls will encode the sigelts that
@@ -626,7 +626,7 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
             let open FStarC.Pprint in
             let open FStarC.Errors.Msg in
             List.iter Errors.print_issue errs;
-            Errors.log_issue se Errors.Error_DidNotFail [
+            Errors.log_issue fail_rng Errors.Error_DidNotFail [
                 prefix 2 1
                   (text "This top-level definition was expected to raise error codes")
                   (pp expected_errors) ^/^