diff --git a/CHANGES.md b/CHANGES.md index bc40d79c5..510c655fe 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -39,6 +39,13 @@ next typechecking (PR#199) - Treat smtlib `:named` annotations as implicit definitions as required by the spec (PR#199) +- Add a warning for unknown attributes in smtlib2. This replaces + the `unbound id` error that some files could raise before when + using non-standard attribtues (PR#207) +- Only type annotations on quantified formulas once. Previously, + these were typed twice so that they can be attached to both the + body of the quantified formula and the quantified formula itself. + (PR#207) ### Loop diff --git a/src/loop/typer.ml b/src/loop/typer.ml index 1245cacbf..e14e44e44 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -361,13 +361,12 @@ let unused_term_variable = print_var_kind kind Dolmen.Std.Expr.Print.id v) ~name:"Unused bound term variable" () -let error_in_attribute = - Report.Warning.mk ~code ~mnemonic:"error-in-attr" - ~message:(fun fmt exn -> - Format.fprintf fmt - "Exception while typing attribute:@ %s" - (Printexc.to_string exn)) - ~name:"Exception while typing an attribute" () +let unknown_attribute = + Report.Warning.mk ~code ~mnemonic:"unknown-attribute" + ~message:(fun fmt id -> + Format.fprintf fmt "Unknown attribute (the attribtue was ignored): %a" + (pp_wrap Dolmen.Std.Id.print) id) + ~name:"Unknown attribute" () let superfluous_destructor = Report.Warning.mk ~code:Code.bug ~mnemonic:"extra-dstr" @@ -1228,20 +1227,24 @@ module Typer(State : State.S) = struct else warn ~input ~loc st unused_term_variable (kind, v) (* *) - | T.Error_in_attribute exn -> - warn ~input ~loc st error_in_attribute exn | T.Superfluous_destructor _ -> warn ~input ~loc st superfluous_destructor () | T.Shadowing (id, old, _cur) -> warn ~input ~loc st shadowing (id, old) | T.Redundant_pattern pattern -> warn ~input ~loc st redundant_pattern pattern + + (* smtlib2 *) + | Smtlib2_Core.Unknown_attribute id -> + warn ~input ~loc st unknown_attribute id | Smtlib2_Arrays.Extension id -> warn ~input ~loc st array_extension id | Smtlib2_Ints.Restriction (config, msg) | Smtlib2_Reals.Restriction (config, msg) | Smtlib2_Reals_Ints.Restriction (config, msg) -> warn ~input ~loc st bad_arith_expr (config, msg) + + (* catch-all *) | _ -> warn ~input ~loc st unknown_warning (Obj.Extension_constructor.(name (of_val w))) diff --git a/src/typecheck/core.ml b/src/typecheck/core.ml index 92a70691a..1822c9eef 100644 --- a/src/typecheck/core.ml +++ b/src/typecheck/core.ml @@ -499,6 +499,9 @@ module Smtlib2 = struct (T : Dolmen.Intf.Term.Smtlib_Base with type t = Type.T.t and type cstr := Type.T.Cstr.t) = struct + type _ Type.warn += + | Unknown_attribute : Dolmen.Std.Id.t -> Dolmen.Std.Term.t Type.warn + type _ Type.err += | Incorrect_sexpression : Dolmen.Intf.Msg.t -> Dolmen.Std.Term.t Type.err | Non_closed_named_term : Type.Ty.Var.t list * Type.T.Var.t list -> Dolmen.Std.Term.t Type.err @@ -641,6 +644,14 @@ module Smtlib2 = struct [Type.Add (Tag.triggers, t)] )) + (* Unknown attributes *) + | Type.Id ({ name = Simple annot; ns = Attr } as id) + when String.length annot > 0 && annot.[0] = ':' -> + Type.builtin_tags (fun ast _args -> + Type._warn env (Ast ast) (Unknown_attribute id); + [] + ) + (* Rewrite rules *) | Type.Id id when Id.equal id Id.rwrt_rule -> Type.builtin_tags (fun _ast _args -> [Type.Set (Tag.rwrt, ())]) diff --git a/src/typecheck/core.mli b/src/typecheck/core.mli index 1f65d5f32..27a5b2042 100644 --- a/src/typecheck/core.mli +++ b/src/typecheck/core.mli @@ -77,6 +77,9 @@ module Smtlib2 : sig (T : Dolmen.Intf.Term.Smtlib_Base with type t = Type.T.t and type cstr := Type.T.Cstr.t) : sig + type _ Type.warn += + | Unknown_attribute : Dolmen.Std.Id.t -> Dolmen.Std.Term.t Type.warn + type _ Type.err += | Incorrect_sexpression : Dolmen.Intf.Msg.t -> Dolmen.Std.Term.t Type.err | Non_closed_named_term : Type.Ty.Var.t list * Type.T.Var.t list -> Dolmen.Std.Term.t Type.err diff --git a/src/typecheck/intf.ml b/src/typecheck/intf.ml index 3dbfa1777..acb7fdc0d 100644 --- a/src/typecheck/intf.ml +++ b/src/typecheck/intf.ml @@ -275,8 +275,6 @@ module type Formulas = sig (** Unused quantified type variable *) | Unused_term_variable : var_kind * term_var -> Dolmen.Std.Term.t warn (** Unused quantified term variable *) - | Error_in_attribute : exn -> Dolmen.Std.Term.t warn - (** An error occurred wile parsing an attribute *) | Superfluous_destructor : Dolmen.Std.Id.t * Dolmen.Std.Id.t * term_cst -> Dolmen.Std.Term.t warn (** The user implementation of typed terms returned a destructor where diff --git a/src/typecheck/thf.ml b/src/typecheck/thf.ml index 1d63884e9..1aedda4c1 100644 --- a/src/typecheck/thf.ml +++ b/src/typecheck/thf.ml @@ -333,8 +333,6 @@ module Make (* Unused bound type variable *) | Unused_term_variable : var_kind * T.Var.t -> Ast.t warn (* Unused bound term variable *) - | Error_in_attribute : exn -> Ast.t warn - (* An error occurred wile parsing an attribute *) | Superfluous_destructor : Id.t * Id.t * T.Const.t -> Ast.t warn (* The user implementation of typed terms returned a destructor where was asked for. This warning can very safely be ignored. *) @@ -674,6 +672,9 @@ module Make (* Convenience functions *) (* ************************************************************************ *) + let _redundant_pattern env ast pat = + _warn env (Ast ast) (Redundant_pattern pat) + let _expected env s t res = _error env (Ast t) (Expected (s, res)) @@ -692,9 +693,6 @@ module Make let _bad_poly_arity env ast ty_vars tys = _error env (Ast ast) (Bad_poly_arity (ty_vars, tys)) - let _redundant_pattern env ast pat = - _warn env (Ast ast) (Redundant_pattern pat) - let _partial_pattern_match env ast missing = _error env (Ast ast) (Partial_pattern_match missing) @@ -1571,16 +1569,16 @@ module Make | Hook f -> f ast res ) res (parse_attrs env [] l) - and parse_attr env ast = - match parse_expr (expect_anything env) ast with - | Tags l -> List.map (fun tag -> ast, tag) l - | res -> _expected env "tag" ast (Some res) - and parse_attrs env acc = function | [] -> acc | a :: r -> parse_attrs env (parse_attr env a @ acc) r + and parse_attr env ast = + match parse_expr (expect_anything env) ast with + | Tags l -> List.map (fun tag -> ast, tag) l + | res -> _expected env "tag" ast (Some res) + and parse_var_in_binding_pos env = function | { Ast.term = Ast.Symbol s; _ } as t -> infer_var_in_binding_pos env t s @@ -1622,10 +1620,7 @@ module Make List.rev ttype_vars, List.rev typed_vars, env' and parse_binder parse_inner mk b env ast ttype_acc ty_acc body_ast = - let [@inline] aux t = - parse_binder_aux parse_inner mk b env ast ttype_acc ty_acc t - in - (wrap_attr[@inlined]) apply_attr env body_ast aux + parse_binder_aux parse_inner mk b env ast ttype_acc ty_acc body_ast and parse_binder_aux parse_inner mk b env ast ttype_acc ty_acc = function | { Ast.term = Ast.Binder (b', vars, f); _ } when b = b' -> diff --git a/tests/typing/warnings/unknown_attribute/dune b/tests/typing/warnings/unknown_attribute/dune new file mode 100644 index 000000000..ec370ba31 --- /dev/null +++ b/tests/typing/warnings/unknown_attribute/dune @@ -0,0 +1,36 @@ +; File auto-generated by gentests.ml + +; Auto-generated part begin +; Test for unknown_attr.smt2 +; Incremental test + +(rule + (target unknown_attr.incremental) + (deps (:input unknown_attr.smt2)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff unknown_attr.expected unknown_attr.incremental))) + +; Full mode test + +(rule + (target unknown_attr.full) + (deps (:input unknown_attr.smt2)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff unknown_attr.expected unknown_attr.full))) + + +; Auto-generated part end diff --git a/tests/typing/warnings/unknown_attribute/flags.dune b/tests/typing/warnings/unknown_attribute/flags.dune new file mode 100644 index 000000000..e69de29bb diff --git a/tests/typing/warnings/unknown_attribute/unknown_attr.expected b/tests/typing/warnings/unknown_attribute/unknown_attr.expected new file mode 100644 index 000000000..c88317979 --- /dev/null +++ b/tests/typing/warnings/unknown_attribute/unknown_attr.expected @@ -0,0 +1,8 @@ +File "tests/typing/warnings/unknown_attribute/unknown_attr.smt2", line 5, character 6-32: +5 | :qid |somefile.ext.161:23| + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning Unknown attribute (the attribtue was ignored): `:qid` +File "tests/typing/warnings/unknown_attribute/unknown_attr.smt2", line 6, character 6-19: +6 | :skolemid |0| + ^^^^^^^^^^^^^ +Warning Unknown attribute (the attribtue was ignored): `:skolemid` diff --git a/tests/typing/warnings/unknown_attribute/unknown_attr.smt2 b/tests/typing/warnings/unknown_attribute/unknown_attr.smt2 new file mode 100644 index 000000000..6ce40d880 --- /dev/null +++ b/tests/typing/warnings/unknown_attribute/unknown_attr.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(assert + (forall ((v Int)) + (! (= v v) + :qid |somefile.ext.161:23| + :skolemid |0| + :pattern (v) + ) + ) +)