From 457e4054de66fbcc2d4ff5bd5f678419ea8ebb50 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 14 Nov 2018 20:04:32 +0000 Subject: [PATCH 1/2] pretty formatting of SMT2 types in error messages --- src/solvers/smt2/smt2_parser.cpp | 24 ++++++++++++++++++++---- src/solvers/smt2/smt2_parser.h | 11 +++++++++++ 2 files changed, 31 insertions(+), 4 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index e1cc0260eaa..a23dcfb7a1b 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -10,6 +10,22 @@ Author: Daniel Kroening, kroening@kroening.com #include +std::ostream &operator<<(std::ostream &out, const smt2_parsert::smt2_format &f) +{ + if(f.type.id() == ID_unsignedbv) + out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')'; + else if(f.type.id() == ID_bool) + out << "Bool"; + else if(f.type.id() == ID_integer) + out << "Int"; + else if(f.type.id() == ID_real) + out << "Real"; + else + out << "? " << f.type.id(); + + return out; +} + void smt2_parsert::command_sequence() { exit=false; @@ -360,8 +376,8 @@ exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op) { error() << "expression must have operands with matching types," " but got `" - << op[0].type().pretty() - << "' and `" << op[i].type().pretty() << '\'' << eom; + << smt2_format(op[0].type()) << "' and `" + << smt2_format(op[i].type()) << '\'' << eom; return nil_exprt(); } } @@ -385,8 +401,8 @@ exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op) { error() << "expression must have operands with matching types," " but got `" - << op[0].type().pretty() - << "' and `" << op[1].type().pretty() << '\'' << eom; + << smt2_format(op[0].type()) << "' and `" + << smt2_format(op[1].type()) << '\'' << eom; return nil_exprt(); } diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 1c787bc93d3..19acb751630 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -43,6 +43,15 @@ class smt2_parsert:public smt2_tokenizert using id_mapt=std::map; id_mapt id_map; + struct smt2_format + { + explicit smt2_format(const typet &_type) : type(_type) + { + } + + const typet type; + }; + protected: bool exit; void command_sequence(); @@ -82,4 +91,6 @@ class smt2_parsert:public smt2_tokenizert exprt cast_bv_to_unsigned(const exprt &); }; +std::ostream &operator<<(std::ostream &, const smt2_parsert::smt2_format &); + #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H From be0c33805f887d6831b1d2ba95880e06bd08ae89 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 14 Nov 2018 20:41:05 +0000 Subject: [PATCH 2/2] smt2 parser: check type of body of function definition --- .../function-application1.desc | 7 +++++++ .../function-application1.smt2 | 13 ++++++++++++ .../function-application2.desc | 7 +++++++ .../function-application2.smt2 | 14 +++++++++++++ scripts/delete_failing_smt2_solver_tests | 2 ++ src/solvers/smt2/smt2_parser.cpp | 20 +++++++++++++++++++ 6 files changed, 63 insertions(+) create mode 100644 regression/smt2_solver/function-applications/function-application1.desc create mode 100644 regression/smt2_solver/function-applications/function-application1.smt2 create mode 100644 regression/smt2_solver/function-applications/function-application2.desc create mode 100644 regression/smt2_solver/function-applications/function-application2.smt2 diff --git a/regression/smt2_solver/function-applications/function-application1.desc b/regression/smt2_solver/function-applications/function-application1.desc new file mode 100644 index 00000000000..14e9fea2a27 --- /dev/null +++ b/regression/smt2_solver/function-applications/function-application1.desc @@ -0,0 +1,7 @@ +CORE +function-application1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/function-applications/function-application1.smt2 b/regression/smt2_solver/function-applications/function-application1.smt2 new file mode 100644 index 00000000000..9cc93c33b56 --- /dev/null +++ b/regression/smt2_solver/function-applications/function-application1.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_BV) + +(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8) + (ite (bvule a b) a b)) + +(define-fun p1 () Bool (= (min #x01 #x02) #x01)) +(define-fun p2 () Bool (= (min #xff #xfe) #xfe)) + +; all must be true + +(assert (not (and p1 p2))) + +(check-sat) diff --git a/regression/smt2_solver/function-applications/function-application2.desc b/regression/smt2_solver/function-applications/function-application2.desc new file mode 100644 index 00000000000..4e966694885 --- /dev/null +++ b/regression/smt2_solver/function-applications/function-application2.desc @@ -0,0 +1,7 @@ +CORE +function-application2.smt2 + +^EXIT=134$ +^SIGNAL=0$ +^line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'$ +-- diff --git a/regression/smt2_solver/function-applications/function-application2.smt2 b/regression/smt2_solver/function-applications/function-application2.smt2 new file mode 100644 index 00000000000..7ced63d3a4d --- /dev/null +++ b/regression/smt2_solver/function-applications/function-application2.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_BV) + +; the range type doesn't match! +(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) + (ite (bvule a b) a b)) + +(define-fun p1 () Bool (= (min #x01 #x02) #x01)) +(define-fun p2 () Bool (= (min #xff #xfe) #xfe)) + +; all must be true + +(assert (not (and p1 p2))) + +(check-sat) diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index 75170e43f11..1baaa807bf5 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -58,12 +58,14 @@ rm Float8/test.desc rm Free2/test.desc rm Function1/test.desc rm Function_Pointer3/test.desc +rm Initialization6/test.desc rm Linking4/test.desc rm Linking7/test.desc rm Malloc17/test.desc rm Malloc18/test.desc rm Malloc19/test.desc rm Malloc20/test.desc +rm Malloc21/test.desc rm Malloc23/test.desc rm Malloc24/test.desc rm Memmove1/test.desc diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index a23dcfb7a1b..900900ae6d8 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1203,6 +1203,26 @@ void smt2_parsert::command(const std::string &c) auto signature=function_signature_definition(); exprt body=expression(); + // check type of body + if(signature.id() == ID_mathematical_function) + { + const auto &f_signature = to_mathematical_function_type(signature); + if(body.type() != f_signature.codomain()) + { + error() << "type mismatch in function definition: expected `" + << smt2_format(f_signature.codomain()) << "' but got `" + << smt2_format(body.type()) << '\'' << eom; + return; + } + } + else if(body.type() != signature) + { + error() << "type mismatch in function definition: expected `" + << smt2_format(signature) << "' but got `" + << smt2_format(body.type()) << '\'' << eom; + return; + } + // set up the entry auto &entry=id_map[id]; entry.type=signature;