From 12f1a5a0d7195970ea9422016a48a4f9db977597 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 31 Aug 2023 16:34:40 +0200 Subject: [PATCH 1/2] Refine some arithmetic error/warning messages --- src/bin/options.ml | 2 +- src/loop/typer.ml | 44 ++++++++------ src/loop/typer.mli | 11 +++- src/typecheck/arith.ml | 124 ++++++++++++++++++++-------------------- src/typecheck/arith.mli | 12 ++-- 5 files changed, 104 insertions(+), 89 deletions(-) diff --git a/src/bin/options.ml b/src/bin/options.ml index ffd2ef952..1abc1e2f6 100644 --- a/src/bin/options.ml +++ b/src/bin/options.ml @@ -334,7 +334,7 @@ let reports_opts strict warn_modifiers = let fatal warn conf = Dolmen_loop.Report.Conf.fatal conf warn in conf |> fatal - (`Warning (Dolmen_loop.Report.Any_warn Dolmen_loop.Typer.almost_linear)) + (`Warning (Dolmen_loop.Report.Any_warn Dolmen_loop.Typer.bad_arith_expr)) |> fatal (`Warning (Dolmen_loop.Report.Any_warn Dolmen_loop.Typer.unknown_logic)) end diff --git a/src/loop/typer.ml b/src/loop/typer.ml index b9be2a5f7..4ed7e8ee9 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -255,6 +255,10 @@ let text_hint = function | "" -> None | msg -> Some (Format.dprintf "%a" Format.pp_print_text msg) +let text_hint2 = function + | _, "" -> None + | _, msg -> Some (Format.dprintf "%a" Format.pp_print_text msg) + let poly_hint (c, expected, actual) = let vars, params, _ = Dolmen.Std.Expr.(Ty.poly_sig @@ Term.Const.ty c) in let n_ty = List.length vars in @@ -375,12 +379,13 @@ let redundant_pattern = "This pattern is useless (i.e. it is made redundant by earlier patterns)") ~name:"Redundant pattern" () -let almost_linear = - Report.Warning.mk ~code ~mnemonic:"almost-linear-expr" - ~message:(fun fmt _ -> +let bad_arith_expr = + Report.Warning.mk ~code ~mnemonic:"bad-arith-expr" + ~message:(fun fmt (config, _) -> Format.fprintf fmt - "This is a non-linear expression according to the smtlib spec.") - ~hints:[text_hint] + "This expression does not conform to the specification for %a arithmetic" + Dolmen_type.Arith.Smtlib2.print_config config) + ~hints:[text_hint2] ~name:"Non-linear expression in linear arithmetic" () let array_extension = @@ -834,12 +839,13 @@ let forbidden_array_sort = ~hints:[text_hint] ~name:"Forbidden array sort" () -let non_linear_expression = - Report.Error.mk ~code ~mnemonic:"non-linear-expr" - ~message:(fun fmt _ -> - Format.fprintf fmt "Non-linear expressions are forbidden by the logic.") - ~hints:[text_hint] - ~name:"Non linear expression in linear arithmetic logic" () +let forbidden_arith_expr = + Report.Error.mk ~code ~mnemonic:"forbidden-arith" + ~message:(fun fmt (config, _msg) -> + Format.fprintf fmt "Forbidden expression in %a arithmetic" + Dolmen_type.Arith.Smtlib2.print_config config) + ~hints:[text_hint2] + ~name:"Forbidden arithmetic expression" () let bitvector_app_expected_nat_lit = Report.Error.mk ~code ~mnemonic:"bitvector-app-expected-nat-lit" @@ -1161,10 +1167,10 @@ module Typer(State : State.S) = struct warn ~input ~loc st redundant_pattern pattern | Smtlib2_Arrays.Extension id -> warn ~input ~loc st array_extension id - | Smtlib2_Ints.Restriction msg - | Smtlib2_Reals.Restriction msg - | Smtlib2_Reals_Ints.Restriction msg -> - warn ~input ~loc st almost_linear msg + | 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) | _ -> warn ~input ~loc st unknown_warning (Obj.Extension_constructor.(name (of_val w))) @@ -1278,10 +1284,10 @@ module Typer(State : State.S) = struct | Smtlib2_Arrays.Forbidden msg -> error ~input ~loc st forbidden_array_sort msg (* Smtlib Arithmetic errors *) - | Smtlib2_Ints.Forbidden msg - | Smtlib2_Reals.Forbidden msg - | Smtlib2_Reals_Ints.Forbidden msg -> - error ~input ~loc st non_linear_expression msg + | Smtlib2_Ints.Forbidden (config, msg) + | Smtlib2_Reals.Forbidden (config, msg) + | Smtlib2_Reals_Ints.Forbidden (config, msg) -> + error ~input ~loc st forbidden_arith_expr (config, msg) | Smtlib2_Reals_Ints.Expected_arith_type ty -> error ~input ~loc st expected_arith_type (ty, "The stmlib Reals_Ints theory requires an arithmetic type in order to \ diff --git a/src/loop/typer.mli b/src/loop/typer.mli index 46c984945..aaf061eca 100644 --- a/src/loop/typer.mli +++ b/src/loop/typer.mli @@ -27,8 +27,15 @@ val typer_state : ty_state -> T.state (* {2 Warnings} *) -val almost_linear : string Report.Warning.t -(** Almost linear warning. *) +val forbidden_arith_expr : (Dolmen_type.Arith.Smtlib2.config * string) Report.Error.t +(** Error for arithmetic expressions that do not respect the specification (e.g. + non-linear expressions, expressions not in difference logic, etc...). *) + +val bad_arith_expr : (Dolmen_type.Arith.Smtlib2.config * string) Report.Warning.t +(** Warning for arithmetic expressions that do not strictly conform to the + specification (e.g. linear arithmetic), but are close enough that they + should probably be accepted. *) + val unknown_logic : string Report.Warning.t (** Unknown logic warning *) diff --git a/src/typecheck/arith.ml b/src/typecheck/arith.ml index 19464f74a..13f685eff 100644 --- a/src/typecheck/arith.ml +++ b/src/typecheck/arith.ml @@ -235,11 +235,11 @@ module Smtlib2 = struct let print_config fmt = function | Regular -> Format.fprintf fmt "regular" - | Linear `Large -> Format.fprintf fmt "linear/large" - | Linear `Strict -> Format.fprintf fmt "linear/strict" - | Difference `IDL -> Format.fprintf fmt "idl" - | Difference `RDL -> Format.fprintf fmt "rdl" - | Difference `UFIDL -> Format.fprintf fmt "ufidl" + | Linear `Large -> Format.fprintf fmt "linear (large)" + | Linear `Strict -> Format.fprintf fmt "linear" + | Difference `IDL -> Format.fprintf fmt "IDL" + | Difference `RDL -> Format.fprintf fmt "RDL" + | Difference `UFIDL -> Format.fprintf fmt "UFIDL" (* In order to establish the needed classification and correctly raise warnings or errors, we first need a fine-grained view of terms according to an arithmetic @@ -506,9 +506,11 @@ module Smtlib2 = struct | Numeral _ -> aux non_numeral_seen r | _ -> if non_numeral_seen then - Error (Format.asprintf "subtraction in difference logic (QF_UFIDL version) \ - expects all but at most one of its arguments to be \ - numerals") + Error ( + Format.asprintf + "addition/subtraction in difference logic \ + (in UFIDL/QF_UFIDL) expects all but at most \ + one of its arguments to be numerals") else aux true r end @@ -781,19 +783,19 @@ module Smtlib2 = struct module F = Filter(Type) type _ Type.warn += - | Restriction : string -> Term.t Type.warn + | Restriction : config * string -> Term.t Type.warn type _ Type.err += - | Forbidden : string -> Term.t Type.err + | Forbidden : config * string -> Term.t Type.err - let check env filter ast args = + let check config env filter ast args = match filter args with | Ok -> () - | Warn msg -> Type._warn env (Ast ast) (Restriction msg) - | Error msg -> Type._error env (Ast ast) (Forbidden msg) + | Warn msg -> Type._warn env (Ast ast) (Restriction (config, msg)) + | Error msg -> Type._error env (Ast ast) (Forbidden (config, msg)) - let check1 env filter ast a = check env filter ast [a] - let check2 env filter ast a b = check env filter ast [a; b] + let check1 config env filter ast a = check config env filter ast [a] + let check2 config env filter ast a b = check config env filter ast [a; b] let rec parse ~config version env s = match s with @@ -809,41 +811,41 @@ module Smtlib2 = struct | "-" -> Type.builtin_term (fun ast args -> match args with | [x] -> - check env (F.minus config (parse ~config) version env) ast args; + check config env (F.minus config (parse ~config) version env) ast args; T.minus (Type.parse_term env x) | _ -> Base.term_app_left (module Type) env s T.sub ast args - ~check:(check env (F.sub config (parse ~config) version env)) + ~check:(check config env (F.sub config (parse ~config) version env)) ) | "+" -> Type.builtin_term (Base.term_app_left (module Type) env s T.add - ~check:(check env (F.add config (parse ~config) version env))) + ~check:(check config env (F.add config (parse ~config) version env))) | "*" -> Type.builtin_term (Base.term_app_left (module Type) env s T.mul - ~check:(check env (F.mul config (parse ~config) version env))) + ~check:(check config env (F.mul config (parse ~config) version env))) | "div" -> Type.builtin_term (Base.term_app_left (module Type) env s T.div - ~check:(check env (F.ediv config version))) + ~check:(check config env (F.ediv config version))) ~meta:(`Partial (fun _ _ _ -> T.div')) | "mod" -> Type.builtin_term (Base.term_app2 (module Type) env s T.rem - ~check:(check2 env (F.mod_ config version))) + ~check:(check2 config env (F.mod_ config version))) ~meta:(`Partial (fun _ _ _ -> T.rem')) | "abs" -> Type.builtin_term (Base.term_app1 (module Type) env s T.abs - ~check:(check1 env (F.abs config version))) + ~check:(check1 config env (F.abs config version))) | "<=" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.le - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | "<" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.lt - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | ">=" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.ge - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | ">" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.gt - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | "div0" -> `Reserved ( "completing interpretation of division by zero in models", @@ -861,7 +863,7 @@ module Smtlib2 = struct | "divisible" -> `Unary (function n -> Type.builtin_term (Base.term_app1 (module Type) env s (T.divisible n) - ~check:(check1 env (F.divisible config version))) + ~check:(check1 config env (F.divisible config version))) ) | _ -> `Not_indexed ) @@ -881,16 +883,16 @@ module Smtlib2 = struct module F = Filter(Type) type _ Type.warn += - | Restriction : string -> Term.t Type.warn + | Restriction : config * string -> Term.t Type.warn type _ Type.err += - | Forbidden : string -> Term.t Type.err + | Forbidden : config * string -> Term.t Type.err - let check env filter ast args = + let check config env filter ast args = match filter args with | Ok -> () - | Warn msg -> Type._warn env (Ast ast) (Restriction msg) - | Error msg -> Type._error env (Ast ast) (Forbidden msg) + | Warn msg -> Type._warn env (Ast ast) (Restriction (config, msg)) + | Error msg -> Type._error env (Ast ast) (Forbidden (config, msg)) let rec parse ~config version env s = match s with @@ -906,34 +908,34 @@ module Smtlib2 = struct | "-" -> Type.builtin_term (fun ast args -> match args with | [x] -> - check env (F.minus config (parse ~config) version env) ast args; + check config env (F.minus config (parse ~config) version env) ast args; T.minus (Type.parse_term env x) | _ -> Base.term_app_left (module Type) env s T.sub ast args - ~check:(check env (F.sub config (parse ~config) version env)) + ~check:(check config env (F.sub config (parse ~config) version env)) ) | "+" -> Type.builtin_term (Base.term_app_left (module Type) env s T.add - ~check:(check env (F.add config (parse ~config) version env))) + ~check:(check config env (F.add config (parse ~config) version env))) | "*" -> Type.builtin_term (Base.term_app_left (module Type) env s T.mul - ~check:(check env (F.mul config (parse ~config) version env))) + ~check:(check config env (F.mul config (parse ~config) version env))) | "/" -> Type.builtin_term (Base.term_app_left (module Type) env s T.div - ~check:(check env (F.div config (parse ~config) version env))) + ~check:(check config env (F.div config (parse ~config) version env))) ~meta:(`Partial (fun _ _ _ -> T.div')) | "<=" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.le - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | "<" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.lt - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | ">=" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.ge - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | ">" -> Type.builtin_term (Base.term_app_chain (module Type) env s T.gt - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | "/0" -> `Reserved ( "completing interpretation of division by zero in models", @@ -959,20 +961,20 @@ module Smtlib2 = struct module F = Filter(Type) type _ Type.warn += - | Restriction : string -> Term.t Type.warn + | Restriction : config * string -> Term.t Type.warn type _ Type.err += - | Forbidden : string -> Term.t Type.err + | Forbidden : config * string -> Term.t Type.err | Expected_arith_type : Type.Ty.t -> Term.t Type.err - let check env filter ast args = + let check config env filter ast args = match filter args with | Ok -> () - | Warn msg -> Type._warn env (Ast ast) (Restriction msg) - | Error msg -> Type._error env (Ast ast) (Forbidden msg) + | Warn msg -> Type._warn env (Ast ast) (Restriction (config, msg)) + | Error msg -> Type._error env (Ast ast) (Forbidden (config, msg)) - let check1 env filter ast a = check env filter ast [a] - let check2 env filter ast a b = check env filter ast [a; b] + let check1 config env filter ast a = check config env filter ast [a] + let check2 config env filter ast a b = check config env filter ast [a; b] let dispatch1 env (mk_int, mk_real) ast t = match Ty.view @@ T.ty t with @@ -1018,52 +1020,52 @@ module Smtlib2 = struct | [_] -> Base.term_app1_ast (module Type) env s (dispatch1 env (T.Int.minus, T.Real.minus)) ast args - ~check:(check1 env (F.minus config (parse ~config) version env)) + ~check:(check1 config env (F.minus config (parse ~config) version env)) | _ -> Base.term_app_left_ast (module Type) env s (dispatch2 env (T.Int.sub, T.Real.sub)) ast args - ~check:(check env (F.sub config (parse ~config) version env)) + ~check:(check config env (F.sub config (parse ~config) version env)) ) | "+" -> Type.builtin_term (Base.term_app_left_ast (module Type) env s (dispatch2 env (T.Int.add, T.Real.add)) - ~check:(check env (F.add config (parse ~config) version env))) + ~check:(check config env (F.add config (parse ~config) version env))) | "*" -> Type.builtin_term (Base.term_app_left_ast (module Type) env s (dispatch2 env (T.Int.mul, T.Real.mul)) - ~check:(check env (F.mul config (parse ~config) version env))) + ~check:(check config env (F.mul config (parse ~config) version env))) | "div" -> Type.builtin_term (Base.term_app_left (module Type) env s T.Int.div - ~check:(check env (F.ediv config version))) + ~check:(check config env (F.ediv config version))) ~meta:(`Partial (fun _ _ _ -> T.Int.div')) | "mod" -> Type.builtin_term (Base.term_app2 (module Type) env s T.Int.rem - ~check:(check2 env (F.mod_ config version))) + ~check:(check2 config env (F.mod_ config version))) ~meta:(`Partial (fun _ _ _ -> T.Int.rem')) | "abs" -> Type.builtin_term (Base.term_app1 (module Type) env s T.Int.abs - ~check:(check1 env (F.abs config version))) + ~check:(check1 config env (F.abs config version))) | "/" -> Type.builtin_term (Base.term_app_left_ast (module Type) env s (promote_int_to_real env T.Real.div) - ~check:(check env (F.div config (parse ~config) version env))) + ~check:(check config env (F.div config (parse ~config) version env))) ~meta:(`Partial (fun _ _ _ -> T.Real.div')) | "<=" -> Type.builtin_term (Base.term_app_chain_ast (module Type) env s (dispatch2 env (T.Int.le, T.Real.le)) - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | "<" -> Type.builtin_term (Base.term_app_chain_ast (module Type) env s (dispatch2 env (T.Int.lt, T.Real.lt)) - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | ">=" -> Type.builtin_term (Base.term_app_chain_ast (module Type) env s (dispatch2 env (T.Int.ge, T.Real.ge)) - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | ">" -> Type.builtin_term (Base.term_app_chain_ast (module Type) env s (dispatch2 env (T.Int.gt, T.Real.gt)) - ~check:(check env (F.comp config (parse ~config) version env))) + ~check:(check config env (F.comp config (parse ~config) version env))) | "to_real" -> Type.builtin_term (Base.term_app1 (module Type) env s T.Int.to_real) | "to_int" -> @@ -1094,7 +1096,7 @@ module Smtlib2 = struct | "divisible" -> `Unary (function n -> Type.builtin_term (Base.term_app1 (module Type) env s (T.Int.divisible n) - ~check:(check1 env (F.divisible config version)))) + ~check:(check1 config env (F.divisible config version)))) | _ -> `Not_indexed ) diff --git a/src/typecheck/arith.mli b/src/typecheck/arith.mli index cc3670b68..05eb1bf4a 100644 --- a/src/typecheck/arith.mli +++ b/src/typecheck/arith.mli @@ -41,13 +41,13 @@ module Smtlib2 : sig and type cst := Type.T.Const.t) : sig type _ Type.warn += - | Restriction : string -> Dolmen.Std.Term.t Type.warn + | Restriction : config * string -> Dolmen.Std.Term.t Type.warn (** Warning for expressions which tecnically do not respect the strict spec but respect the large spec. *) (** Arithmetic type-checking warnings *) type _ Type.err += - | Forbidden : string -> Dolmen.Std.Term.t Type.err + | Forbidden : config * string -> Dolmen.Std.Term.t Type.err (** Error for expressions which do not respect the spec. *) (** Arithmetic type-checking errors *) @@ -67,13 +67,13 @@ module Smtlib2 : sig and type cst := Type.T.Const.t) : sig type _ Type.warn += - | Restriction : string -> Dolmen.Std.Term.t Type.warn + | Restriction : config * string -> Dolmen.Std.Term.t Type.warn (** Warning for expressions which tecnically do not respect the strict spec but respect the large spec. *) (** Arithmetic type-checking warnings *) type _ Type.err += - | Forbidden : string -> Dolmen.Std.Term.t Type.err + | Forbidden : config * string -> Dolmen.Std.Term.t Type.err (** Error for expressions which do not respect the spec. *) (** Arithmetic type-checking errors *) @@ -95,13 +95,13 @@ module Smtlib2 : sig and type Real.cst := Type.T.Const.t) : sig type _ Type.warn += - | Restriction : string -> Dolmen.Std.Term.t Type.warn + | Restriction : config * string -> Dolmen.Std.Term.t Type.warn (** Warning for expressions which tecnically do not respect the strict spec but respect the large spec. *) (** Arithmetic type-checking warnings *) type _ Type.err += - | Forbidden : string -> Dolmen.Std.Term.t Type.err + | Forbidden : config * string -> Dolmen.Std.Term.t Type.err (** Error for expressions which do not respect the spec. *) | Expected_arith_type : Type.Ty.t -> Dolmen.Std.Term.t Type.err (** Error raised when an arithmetic type was expected (i.e. either From bb9ff62a91e60ac3aa90b014b8182d5dd40bb68c Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 6 Sep 2023 17:54:37 +0200 Subject: [PATCH 2/2] Update tests for new error messages --- doc/tuto.md | 4 ++-- tests/locs/multi_line.expected | 2 +- tests/locs/too_long.expected | 2 +- tests/typing/errors/arith_linear/test.expected | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/tuto.md b/doc/tuto.md index 74d50d734..f009f2475 100644 --- a/doc/tuto.md +++ b/doc/tuto.md @@ -93,7 +93,7 @@ other_1[0-15]: free_functions : false; datatypes : false; quantifiers : true; - arithmetic : linear/strict; + arithmetic : linear; arrays : all; }; }]} decl_1[16-37]: @@ -116,7 +116,7 @@ prove_1[61-72]: File "typing_error.smt2", line 3, character 13-20: 3 | (assert (= 2 (* x x))) ^^^^^^^ -Error Non-linear expressions are forbidden by the logic. +Error Forbidden expression in linear arithmetic Hint: multiplication in strict linear arithmetic expects an integer or rational literal and a symbol (variable or constant) but was given: - a symbol (or quantified variable) diff --git a/tests/locs/multi_line.expected b/tests/locs/multi_line.expected index fa204813f..594374819 100644 --- a/tests/locs/multi_line.expected +++ b/tests/locs/multi_line.expected @@ -1,7 +1,7 @@ File "tests/locs/multi_line.smt2", line 3, character 7 to line 4, character 6: 3 | .......(* 1 4 | 2) -Fatal Warning This is a non-linear expression according to the smtlib spec. +Fatal Warning This expression does not conform to the specification for linear arithmetic Hint: multiplication in strict linear arithmetic expects an integer or rational literal and a symbol (variable or constant) but was given: - an integer coefficient diff --git a/tests/locs/too_long.expected b/tests/locs/too_long.expected index d83bcb516..1e3bdb276 100644 --- a/tests/locs/too_long.expected +++ b/tests/locs/too_long.expected @@ -1,5 +1,5 @@ File "tests/locs/too_long.smt2", line 2, character 150-157: -Fatal Warning This is a non-linear expression according to the smtlib spec. +Fatal Warning This expression does not conform to the specification for linear arithmetic Hint: multiplication in strict linear arithmetic expects an integer or rational literal and a symbol (variable or constant) but was given: - an integer coefficient diff --git a/tests/typing/errors/arith_linear/test.expected b/tests/typing/errors/arith_linear/test.expected index a517443f9..20c7a34b4 100644 --- a/tests/typing/errors/arith_linear/test.expected +++ b/tests/typing/errors/arith_linear/test.expected @@ -1,7 +1,7 @@ File "tests/typing/errors/arith_linear/test.smt2", line 4, character 13-20: 4 | (assert (= 0 (* a b))) ^^^^^^^ -Error Non-linear expressions are forbidden by the logic. +Error Forbidden expression in linear arithmetic Hint: multiplication in strict linear arithmetic expects an integer or rational literal and a symbol (variable or constant) but was given: - a symbol (or quantified variable)