From 554d190af6f26151bf38c99ceeff93923855360e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 20:15:23 +0100 Subject: [PATCH] Convert unit tests to Catch framework and fix compilation issues We had some pre-Catch-era unit tests still lying around unmaintained and unused. Alas, they wouldn't even compile anymore. Compilation issues are now fixed and they are embedded in the Catch framework. Fixes: #879 --- unit/CMakeLists.txt | 10 - unit/Makefile | 6 + unit/cpp/cpp_parser.cpp | 67 +++++++ unit/cpp/cpp_scanner.cpp | 93 +++++++++ unit/cpp/module_dependencies.txt | 3 + unit/cpp_parser.cpp | 31 --- unit/cpp_scanner.cpp | 57 ------ unit/elf_reader.cpp | 33 ---- unit/goto-programs/elf_reader.cpp | 52 +++++ unit/goto-programs/wp.cpp | 145 ++++++++++++++ unit/ieee_float.cpp | 306 ------------------------------ unit/json.cpp | 31 --- unit/smt2_parser.cpp | 114 ----------- unit/solvers/smt2/smt2_parser.cpp | 158 +++++++++++++++ unit/util/ieee_float.cpp | 285 ++++++++++++++++++++++++++++ unit/util/json.cpp | 73 +++++++ unit/wp.cpp | 84 -------- 17 files changed, 882 insertions(+), 666 deletions(-) create mode 100644 unit/cpp/cpp_parser.cpp create mode 100644 unit/cpp/cpp_scanner.cpp create mode 100644 unit/cpp/module_dependencies.txt delete mode 100644 unit/cpp_parser.cpp delete mode 100644 unit/cpp_scanner.cpp delete mode 100644 unit/elf_reader.cpp create mode 100644 unit/goto-programs/elf_reader.cpp create mode 100644 unit/goto-programs/wp.cpp delete mode 100644 unit/ieee_float.cpp delete mode 100644 unit/json.cpp delete mode 100644 unit/smt2_parser.cpp create mode 100644 unit/solvers/smt2/smt2_parser.cpp create mode 100644 unit/util/json.cpp delete mode 100644 unit/wp.cpp diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 6435787eec3..1c016d6122f 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -48,16 +48,6 @@ else() endif() list(REMOVE_ITEM sources - # Don't build - ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/json.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/cpp_parser.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/osx_fat_reader.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/wp.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp - # Will be built into a separate library and linked ${testing_utils} diff --git a/unit/Makefile b/unit/Makefile index a708a86b214..75e13119897 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -53,6 +53,8 @@ SRC += analyses/ai/ai.cpp \ ansi-c/type2name.cpp \ ansi-c/c_typecheck_base.cpp \ big-int/big-int.cpp \ + cpp/cpp_parser.cpp \ + cpp/cpp_scanner.cpp \ compound_block_locations.cpp \ get_goto_model_from_c_test.cpp \ goto-cc/armcc_cmdline.cpp \ @@ -61,6 +63,7 @@ SRC += analyses/ai/ai.cpp \ goto-instrument/cover_instrument.cpp \ goto-instrument/cover/cover_only.cpp \ goto-synthesizer/expr_enumerator/expr_enumerator.cpp \ + goto-programs/elf_reader.cpp \ goto-programs/goto_program_assume.cpp \ goto-programs/goto_program_dead.cpp \ goto-programs/goto_program_declaration.cpp \ @@ -77,6 +80,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/restrict_function_pointers.cpp \ goto-programs/structured_trace_util.cpp \ goto-programs/remove_returns.cpp \ + goto-programs/wp.cpp \ goto-programs/xml_expr.cpp \ goto-symex/apply_condition.cpp \ goto-symex/complexity_limiter.cpp \ @@ -110,6 +114,7 @@ SRC += analyses/ai/ai.cpp \ solvers/sat/satcheck_cadical.cpp \ solvers/sat/satcheck_minisat2.cpp \ solvers/smt2/smt2_conv.cpp \ + solvers/smt2/smt2_parser.cpp \ solvers/smt2/smt2irep.cpp \ solvers/smt2_incremental/ast/smt_commands.cpp \ solvers/smt2_incremental/ast/smt_index.cpp \ @@ -173,6 +178,7 @@ SRC += analyses/ai/ai.cpp \ util/irep.cpp \ util/irep_sharing.cpp \ util/invariant.cpp \ + util/json.cpp \ util/json_array.cpp \ util/json_object.cpp \ util/lazy.cpp \ diff --git a/unit/cpp/cpp_parser.cpp b/unit/cpp/cpp_parser.cpp new file mode 100644 index 00000000000..ee186adb6d1 --- /dev/null +++ b/unit/cpp/cpp_parser.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + +Module: Unit tests for cpp_parser + +Author: Daniel Kroening + +\*******************************************************************/ + +#include +#include + +#include +#include +#include + +#include + +TEST_CASE("Parse empty C++ file", "[core][cpp][cpp_parser]") +{ + temporary_filet temp_file("empty_cpp_", ".cpp"); + std::ofstream out(temp_file().c_str()); + out << ""; + out.close(); + + config.ansi_c.set_ILP32(); + + std::ifstream in(temp_file().c_str()); + + cpp_parsert parser(null_message_handler); + parser.in = ∈ + + REQUIRE(parser.parse() == false); +} + +TEST_CASE("Parse simple C++ code", "[core][cpp][cpp_parser]") +{ + temporary_filet temp_file("simple_cpp_", ".cpp"); + std::ofstream out(temp_file().c_str()); + out << "int main() { return 0; }\n"; + out.close(); + + config.ansi_c.set_ILP32(); + + std::ifstream in(temp_file().c_str()); + + cpp_parsert parser(null_message_handler); + parser.in = ∈ + + REQUIRE(parser.parse() == false); +} + +TEST_CASE("Parse C++ with class", "[core][cpp][cpp_parser]") +{ + temporary_filet temp_file("class_cpp_", ".cpp"); + std::ofstream out(temp_file().c_str()); + out << "class MyClass { public: int x; };\n"; + out.close(); + + config.ansi_c.set_ILP32(); + + std::ifstream in(temp_file().c_str()); + + cpp_parsert parser(null_message_handler); + parser.in = ∈ + + REQUIRE(parser.parse() == false); +} diff --git a/unit/cpp/cpp_scanner.cpp b/unit/cpp/cpp_scanner.cpp new file mode 100644 index 00000000000..7d60d645197 --- /dev/null +++ b/unit/cpp/cpp_scanner.cpp @@ -0,0 +1,93 @@ +/*******************************************************************\ + +Module: Unit tests for CPP lexer/scanner + +Author: Daniel Kroening, 2015 + +\*******************************************************************/ + +#include +#include + +#include +#include +#include +#include +#include + +#include +#include +#include + +TEST_CASE("Scan simple C++ tokens", "[core][cpp][cpp_scanner]") +{ + temporary_filet temp_file("tokens_cpp_", ".cpp"); + std::ofstream out(temp_file().c_str()); + out << "int x = 42;\n"; + out.close(); + + std::ifstream in(temp_file().c_str()); + + config.ansi_c.set_ILP32(); + + ansi_c_scanner_init(); + ansi_c_parser.clear(); + ansi_c_parser.mode = ansi_c_parsert::GCC; + ansi_c_parser.cpp98 = true; + ansi_c_parser.cpp11 = false; + ansi_c_parser.ts_18661_3_Floatn_types = false; + ansi_c_parser.__float128_is_keyword = false; + ansi_c_parser.float16_type = false; + ansi_c_parser.bf16_type = false; + ansi_c_parser.fp16_type = false; + ansi_c_parser.in = ∈ + + cpp_parsert parser(null_message_handler); + parser.in = ∈ + + cpp_tokent tk; + std::vector tokens; + + while(parser.token_buffer.get_token(tk)) + tokens.push_back(tk.text); + + REQUIRE(tokens.size() > 0); + REQUIRE(tokens[0] == "int"); +} + +TEST_CASE("Scan C++ keywords", "[core][cpp][cpp_scanner]") +{ + temporary_filet temp_file("keywords_cpp_", ".cpp"); + std::ofstream out(temp_file().c_str()); + out << "class namespace public private\n"; + out.close(); + + std::ifstream in(temp_file().c_str()); + + config.ansi_c.set_ILP32(); + + ansi_c_scanner_init(); + ansi_c_parser.clear(); + ansi_c_parser.mode = ansi_c_parsert::GCC; + ansi_c_parser.cpp98 = true; + ansi_c_parser.cpp11 = false; + ansi_c_parser.ts_18661_3_Floatn_types = false; + ansi_c_parser.__float128_is_keyword = false; + ansi_c_parser.float16_type = false; + ansi_c_parser.bf16_type = false; + ansi_c_parser.fp16_type = false; + ansi_c_parser.in = ∈ + + cpp_parsert parser(null_message_handler); + parser.in = ∈ + + cpp_tokent tk; + std::vector tokens; + + while(parser.token_buffer.get_token(tk)) + tokens.push_back(tk.text); + + REQUIRE(tokens.size() == 4); + REQUIRE(tokens[0] == "class"); + REQUIRE(tokens[1] == "namespace"); +} diff --git a/unit/cpp/module_dependencies.txt b/unit/cpp/module_dependencies.txt new file mode 100644 index 00000000000..d5e667d2411 --- /dev/null +++ b/unit/cpp/module_dependencies.txt @@ -0,0 +1,3 @@ +testing-utils +cpp +util diff --git a/unit/cpp_parser.cpp b/unit/cpp_parser.cpp deleted file mode 100644 index 6b0501eb2fc..00000000000 --- a/unit/cpp_parser.cpp +++ /dev/null @@ -1,31 +0,0 @@ -#include - -#include - -#include - -/*******************************************************************\ - -Function: main - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int main(int argc, const char *argv[]) -{ - if(argc!=2) return 1; - - config.ansi_c.set_ILP32(); - - std::ifstream in(argv[1]); - cpp_parser.in=∈ - - cpp_parser.parse(); - - return 0; -} diff --git a/unit/cpp_scanner.cpp b/unit/cpp_scanner.cpp deleted file mode 100644 index 4000994f015..00000000000 --- a/unit/cpp_scanner.cpp +++ /dev/null @@ -1,57 +0,0 @@ -/*******************************************************************\ - -Module: CPP lexer test - -Author: Daniel Kroening, 2015 - -\*******************************************************************/ - -#include -#include - -#include -#include - -#include -#include - -/*******************************************************************\ - -Function: main - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int main(int argc, const char *argv[]) -{ - if(argc!=2) return 1; - - std::ifstream in(argv[1]); - - config.ansi_c.set_ILP32(); - - ansi_c_scanner_init(); - ansi_c_parser.clear(); - ansi_c_parser.mode=ansi_c_parsert::GCC; - ansi_c_parser.cpp98=true; - ansi_c_parser.cpp11=false; - ansi_c_parser.ts_18661_3_Floatn_types = false; - ansi_c_parser.__float128_is_keyword = false; - ansi_c_parser.float16_type = false; - ansi_c_parser.bf16_type = false; - ansi_c_parser.fp16_type = false; - ansi_c_parser.in=∈ - cpp_parser.in=∈ - - cpp_tokent tk; - - while(cpp_parser.token_buffer.get_token(tk)) - std::cout << tk.text << '\n'; - - return 0; -} diff --git a/unit/elf_reader.cpp b/unit/elf_reader.cpp deleted file mode 100644 index 8a68c75bf92..00000000000 --- a/unit/elf_reader.cpp +++ /dev/null @@ -1,33 +0,0 @@ -#include -#include - -#include - -int main(int argc, char **argv) -{ - if(argc!=2) - { - std::cerr << "elf_reader_test elf_file" << std::endl; - return 1; - } - - std::ifstream in(argv[1]); - - try - { - elf_readert elf_reader(in); - - // iterate over sections - for(unsigned i=0; i + +#include + +#include + +TEST_CASE( + "ELF reader handles invalid input", + "[core][goto-programs][elf_reader]") +{ + std::istringstream in("not an ELF file"); + + REQUIRE_THROWS_AS(elf_readert(in), const char *); +} + +TEST_CASE("ELF reader basic functionality", "[core][goto-programs][elf_reader]") +{ + // Create a minimal ELF header + std::string elf_data; + + // ELF magic number + elf_data += '\x7f'; + elf_data += 'E'; + elf_data += 'L'; + elf_data += 'F'; + + // Fill with zeros to make a minimal (though potentially invalid) ELF + elf_data.append(60, '\0'); + + std::istringstream in(elf_data); + + // This may throw depending on validation, which is expected + REQUIRE_NOTHROW([&in]() { + try + { + elf_readert elf_reader(in); + // If it doesn't throw, that's fine too + } + catch(const char *) + { + // Expected for malformed ELF + } + }()); +} diff --git a/unit/goto-programs/wp.cpp b/unit/goto-programs/wp.cpp new file mode 100644 index 00000000000..0e227dff5b2 --- /dev/null +++ b/unit/goto-programs/wp.cpp @@ -0,0 +1,145 @@ +/*******************************************************************\ + +Module: Unit tests for weakest precondition + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include + +#include +#include + +#include +#include +#include +#include + +#include +#include + +TEST_CASE("Weakest precondition simple assignment", "[core][goto-programs][wp]") +{ + temporary_filet temp_file("wp_test_", ".c"); + std::ofstream out(temp_file().c_str()); + out << "void f() { int x; x = 1; assert(x == 1); }\n"; + out.close(); + + cmdlinet cmdline; + config.set(cmdline); + + register_language(new_ansi_c_language); + + console_message_handlert message_handler; + ansi_c_languaget language; + language.set_message_handler(message_handler); + + std::ifstream in(temp_file().c_str()); + bool parse_result = language.parse(in, temp_file()); + REQUIRE(parse_result == false); // false means success + + symbol_tablet symbol_table; + bool typecheck_result = language.typecheck(symbol_table, temp_file()); + REQUIRE(typecheck_result == false); // false means success + + goto_functionst goto_functions; + goto_convert(symbol_table, goto_functions, message_handler); + + auto f_it = goto_functions.function_map.find("f"); + REQUIRE(f_it != goto_functions.function_map.end()); + + const goto_programt &p = f_it->second.body; + + // Find the assignment and assertion + bool found_assignment = false; + bool found_assertion = false; + + forall_goto_program_instructions(it, p) + { + if(it->is_end_function()) + break; + + if(it->is_assign()) + { + found_assignment = true; + + auto next_it = it; + next_it++; + + if(next_it != p.instructions.end() && next_it->is_assert()) + { + found_assertion = true; + + codet code = it->code; + exprt post = next_it->guard; + namespacet ns(symbol_table); + + exprt pre = wp(code, post, ns); + + // The weakest precondition should be computable + REQUIRE(!pre.is_nil()); + break; + } + } + } + + REQUIRE(found_assignment); + REQUIRE(found_assertion); +} + +TEST_CASE( + "Weakest precondition with local variable", + "[core][goto-programs][wp]") +{ + temporary_filet temp_file("wp_test2_", ".c"); + std::ofstream out(temp_file().c_str()); + out << "void f() { int y = 5; assert(y > 0); }\n"; + out.close(); + + cmdlinet cmdline; + config.set(cmdline); + + register_language(new_ansi_c_language); + + console_message_handlert message_handler; + ansi_c_languaget language; + language.set_message_handler(message_handler); + + std::ifstream in(temp_file().c_str()); + bool parse_result = language.parse(in, temp_file()); + REQUIRE(parse_result == false); // false means success + + symbol_tablet symbol_table; + bool typecheck_result = language.typecheck(symbol_table, temp_file()); + REQUIRE(typecheck_result == false); // false means success + + goto_functionst goto_functions; + goto_convert(symbol_table, goto_functions, message_handler); + + auto f_it = goto_functions.function_map.find("f"); + REQUIRE(f_it != goto_functions.function_map.end()); + + const goto_programt &p = f_it->second.body; + + // Should be able to process the goto program + bool found_useful_instruction = false; + forall_goto_program_instructions(it, p) + { + if(it->is_end_function()) + break; + + if(it->is_assign() || it->is_assert()) + { + found_useful_instruction = true; + break; + } + } + + REQUIRE(found_useful_instruction); +} diff --git a/unit/ieee_float.cpp b/unit/ieee_float.cpp deleted file mode 100644 index 56c218a7f89..00000000000 --- a/unit/ieee_float.cpp +++ /dev/null @@ -1,306 +0,0 @@ -#include -#include -#include -#include -#include -#include -#include - -#ifdef _WIN32 -#define random() rand() -#define nextafterf(a, b) (throw "no nextafterf", 0); -#endif - -#include - -#define PINF (std::numeric_limits::infinity()) -#define NINF (-std::numeric_limits::infinity()) -#ifndef NZERO -#define NZERO (-0.0f) -#endif -#define PZERO (0.0f) - -#ifndef NAN -# define NAN (std::numeric_limits::quiet_NaN()) -#endif - - -std::string float2binary(float f) -{ - union - { - float f; - int i; - } c; - - c.f = f; - return integer2binary(c.i, 32); -} - -float random_float() -{ - union - { - float f; - unsigned i; - } u; - - - unsigned r = ((unsigned) random()) % 20; - - switch(r) - { - case 0: - return PINF; - break; - case 1: - return NINF; - break; - case 2: - return NAN; - break; - case 3: - return PZERO; - break; - case 4: - return NZERO; - break; - default: - u.i=random(); - u.i=(u.i<<16)^random(); - return u.f; - } - -} - -bool eq(const ieee_floatt &a, const ieee_floatt &b) -{ - if(a.is_NaN() && b.is_NaN()) return true; - if(a.is_infinity() && b.is_infinity() && a.get_sign()==b.get_sign()) return true; - return a==b; -} - -typedef enum { PLUS=0, MINUS=1, MULT=2, DIV=3 } binopt; -typedef enum { EQ=0, NEQ=1, LT=2, LE=3, GT=4, GE=5} binrel; -const char *binopsyms[]={ " + ", " - ", " * ", " / " }; -const char *binrelsyms[]={ " == ", " != ", " < ", " <= ", " > ", " >= "}; - -void check_arithmetic(int i) -{ - ieee_floatt i1, i2, i3, res; - float f1, f2, f3; - - f1=random_float(); - f2=random_float(); - i1.from_float(f1); - i2.from_float(f2); - res=i1; - f3=f1; - - int op=(binopt)i%4; - - switch(op) - { - case PLUS: - f3+=f2; - res+=i2; - break; - - case MINUS: - f3-=f2; - res-=i2; - break; - - case MULT: - f3*=f2; - res*=i2; - break; - - case DIV: - f3/=f2; - res/=i2; - break; - - default:assert(0); - } - - i3.from_float(f3); - - if(!eq(res, i3)) - { - const char *opsym=binopsyms[op]; - std::cout << i1 << opsym << i2 << " != " << res << std::endl; - std::cout << f1 << opsym << f2 << " == " << f3 << std::endl; - std::cout << integer2binary(i1.get_fraction(), i1.spec.f+1) << opsym << - integer2binary(i2.get_fraction(), i1.spec.f+1) << " != " << - integer2binary(res.get_fraction(), i1.spec.f+1) << - " (" << res.get_fraction() << ")" << std::endl; - std::cout << integer2binary(i1.get_fraction(), i1.spec.f+1) << opsym << - integer2binary(i2.get_fraction(), i1.spec.f+1) << " == " << - integer2binary(i3.get_fraction(), i1.spec.f+1) << - " (" << i3.get_fraction() << ")" << std::endl; - std::cout << std::endl; - } -} - -void check_comparison(int i) -{ - ieee_floatt i1, i2; - float f1, f2; - - bool ires, fres; - - f1=random_float(); - f2=random_float(); - i1.from_float(f1); - i2.from_float(f2); - - int op=(binrel)i%6; - - switch(op) - { - case EQ: - ires = ieee_equal(i1, i2); - fres = (f1 == f2); - break; - case NEQ: - ires = ieee_not_equal(i1, i2); - fres = (f1 != f2); - break; - case LT: - ires = (i1 < i2); - fres = (f1 < f2); - break; - case LE: - ires = (i1 <= i2); - fres = (f1 <= f2); - break; - case GT: - ires = (i1 > i2); - fres = (f1 > f2); - break; - case GE: - ires = (i1 >= i2); - fres = (f1 >= f2); - break; - default: - assert(0); - } - - if(ires != fres) - { - const char *opsym=binrelsyms[op]; - std::cout << i1 << opsym << i2 << " != " << ires << std::endl; - std::cout << f1 << opsym << f2 << " == " << fres << std::endl; - std::cout << integer2binary(i1.get_fraction(), i1.spec.f+1) << opsym << - integer2binary(i2.get_fraction(), i1.spec.f+1) << " != " << ires; - std::cout << integer2binary(i1.get_fraction(), i1.spec.f+1) << opsym << - integer2binary(i2.get_fraction(), i1.spec.f+1) << " == " << fres; - std::cout << std::endl; - } - -} - -void check_conversion(int i) -{ - union - { - float f; - unsigned i; - } a, b; - - a.f = random_float(); - - ieee_floatt t; - t.from_float(a.f); - - assert(t.is_float()); - b.f = t.to_float(); - - if(a.i != b.i && !((a.f != a.f) && (b.f != b.f))) - { - std::cout << "conversion failure: " << a.f << " -> " << t << " -> " - << b.f << std::endl; - } -} - -void check_nextafter(int i) -{ - float f1 = random_float(); - float f2 = nextafterf(f1, PINF); - float f3 = nextafterf(f1, NINF); - - ieee_floatt i1, i2, i3; - - i1.from_float(f1); - i2 = i1; - i2.increment(false); - i3 = i1; - i3.decrement(false); - - if((f1 != i1.to_float() && !(f1 != f1 && i1.is_NaN())) || - (f2 != i2.to_float() && !(f2 != f2 && i2.is_NaN())) || - (f3 != i3.to_float() && !(f3 != f3 && i3.is_NaN()))) - { - std::cout << "Incorrect nextafter: " << std::endl - << "mach float: " << f1 << " " << f2 << " " << f3 << std::endl - << "ieee_float: " << i1.to_float() << " " - << i2.to_float() << " " << i3.to_float() << std::endl; - std::cout << "Binary representation: " << std::endl - << "mach float: " << float2binary(f1) << " " - << float2binary(f2) << " " << float2binary(f3) << std::endl - << "ieee_float: " << float2binary(i1.to_float()) << " " - << float2binary(i2.to_float()) - << " " << float2binary(i3.to_float()) << std::endl; - - } -} - -void check_minmax() -{ - float f = 0; - ieee_floatt t; - t.from_float(f); - - t.make_fltmax(); - if(t.to_float() != FLT_MAX) - std::cout << "make_fltmax is broken" << std::endl; - - t.make_fltmin(); - if(t.to_float() != FLT_MIN) - std::cout << "make_fltmin is broken:" - << std::endl << " machine float: " << FLT_MIN - << ", ieee_floatt: " << t.to_float() << "(" - << (t.to_float() == FLT_MIN) << ")" << std::endl; -} - -void check_build_extract() -{ - float f = random_float(); - ieee_floatt t; - t.from_float(f); - - mp_integer old_frac, old_exp; - t.extract_base2(old_frac, old_exp); - mp_integer frac_bak=old_frac, exp_bak=old_exp; - t.build(old_frac, old_exp); - t.extract_base2(old_frac, old_exp); - if(frac_bak != old_frac || exp_bak != old_exp) - std::cout << "extract - build - extract is broken for " << t << std::endl; -} - -int main() -{ - srand(time(0)); - check_minmax(); - - for(unsigned i=0; i<100000; i++) - { - if(i%10000==0) std::cout << "*********** " << i << std::endl; - check_arithmetic(i); - check_comparison(i); - check_conversion(i); - check_nextafter(i); - check_build_extract(); - } -} diff --git a/unit/json.cpp b/unit/json.cpp deleted file mode 100644 index f8f128810c1..00000000000 --- a/unit/json.cpp +++ /dev/null @@ -1,31 +0,0 @@ -#include - -#include - -#include - -int yyjsonlex(); -extern char *yyjsontext; - -int main() -{ - #if 0 - int token; - while((token=yyjsonlex())!=0) - { - std::cout << "token: " << token << "\n"; - std::cout << "yyjsontext: " << yyjsontext << "\n"; - } - #endif - - bool result; - - console_message_handlert message_handler; - - jsont json; - - result=parse_json(std::cin, "", message_handler, json); - - std::cout << "return value: " << result << "\n\n"; - std::cout << json << "\n"; -} diff --git a/unit/smt2_parser.cpp b/unit/smt2_parser.cpp deleted file mode 100644 index 59f894c4bf0..00000000000 --- a/unit/smt2_parser.cpp +++ /dev/null @@ -1,114 +0,0 @@ -// small unit test for parsing SMT 2 files - -#include - -#include - -#include - -/*******************************************************************\ - -Function: smt2_parser_test - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -class smt2_parser_testt:public smt2_parsert -{ -public: - smt2_parser_testt(std::istream &_in, std::ostream &_out): - smt2_parsert(_in), out(_out), first(true) - { - } - -protected: - std::ostream &out; - bool first; - - // overload from smt2_parsert - - virtual void symbol() - { - if(first) - first=false; - else - out << ' '; - - // possibly need to quote - out << buffer; - } - - virtual void keyword() - { - if(first) - first=false; - else - out << ' '; - - out << ':' << buffer; - } - - virtual void string_literal() - { - if(first) - first=false; - else - out << ' '; - - out << '"'; - - for(unsigned i=0; i +#include + +#include + +class smt2_parser_testt : public smt2_parsert +{ +public: + smt2_parser_testt(std::istream &_in, std::ostream &_out) + : smt2_parsert(_in), out(_out), first(true) + { + } + +protected: + std::ostream &out; + bool first; + + // overload from smt2_parsert + + virtual void symbol() + { + if(first) + first = false; + else + out << ' '; + + // possibly need to quote + out << buffer; + } + + virtual void keyword() + { + if(first) + first = false; + else + out << ' '; + + out << ':' << buffer; + } + + virtual void string_literal() + { + if(first) + first = false; + else + out << ' '; + + out << '"'; + + for(unsigned i = 0; i < buffer.size(); i++) + { + char ch = buffer[i]; + if(ch == '"') + out << '"'; + out << ch; + } + + out << '"'; + } + + virtual void numeral() + { + if(first) + first = false; + else + out << ' '; + + out << buffer; + } + + virtual void open_expression() // '(' + { + if(!first) + out << ' '; + + out << '('; + first = true; + } + + virtual void close_expression() // ')' + { + out << ')'; + first = false; + } + + virtual void error(const std::string &message) + { + throw message; + } +}; + +TEST_CASE("Parse simple SMT2 expression", "[core][solvers][smt2_parser]") +{ + std::istringstream in("(assert true)"); + std::ostringstream out; + + smt2_parser_testt parser(in, out); + parser(); + + REQUIRE(out.str() == "(assert true)"); +} + +TEST_CASE("Parse SMT2 with symbols", "[core][solvers][smt2_parser]") +{ + std::istringstream in("(declare-fun x () Int)"); + std::ostringstream out; + + smt2_parser_testt parser(in, out); + parser(); + + std::string result = out.str(); + REQUIRE(result.find("declare-fun") != std::string::npos); + REQUIRE(result.find("x") != std::string::npos); +} + +TEST_CASE("Parse SMT2 with numerals", "[core][solvers][smt2_parser]") +{ + std::istringstream in("(assert (= x 42))"); + std::ostringstream out; + + smt2_parser_testt parser(in, out); + parser(); + + std::string result = out.str(); + REQUIRE(result.find("42") != std::string::npos); +} + +TEST_CASE("Parse SMT2 with keywords", "[core][solvers][smt2_parser]") +{ + std::istringstream in("(set-option :produce-models true)"); + std::ostringstream out; + + smt2_parser_testt parser(in, out); + parser(); + + std::string result = out.str(); + REQUIRE(result.find(":produce-models") != std::string::npos); +} + +TEST_CASE("Parse SMT2 with string literal", "[core][solvers][smt2_parser]") +{ + std::istringstream in(R"((set-info :source "test"))"); + std::ostringstream out; + + smt2_parser_testt parser(in, out); + parser(); + + std::string result = out.str(); + REQUIRE(result.find("test") != std::string::npos); +} diff --git a/unit/util/ieee_float.cpp b/unit/util/ieee_float.cpp index 5d5ddafbd14..45b4f4dd480 100644 --- a/unit/util/ieee_float.cpp +++ b/unit/util/ieee_float.cpp @@ -12,6 +12,22 @@ Author: Daniel Kroening, dkr@amazon.com #include +#ifdef _WIN32 +# define random() rand() +# define nextafterf(a, b) (throw "no nextafterf", 0); +#endif + +#define PINF (std::numeric_limits::infinity()) +#define NINF (-std::numeric_limits::infinity()) +#ifndef NZERO +# define NZERO (-0.0f) +#endif +#define PZERO (0.0f) + +#ifndef NAN +# define NAN (std::numeric_limits::quiet_NaN()) +#endif + TEST_CASE("Make an IEEE 754 one", "[core][util][ieee_float]") { auto spec = ieee_float_spect::single_precision(); @@ -129,3 +145,272 @@ TEST_CASE("round_to_integral", "[unit][util][ieee_float]") REQUIRE(round_to_integral(from_double(0x1.0p+52), away) == 0x1.0p+52); REQUIRE(round_to_integral(from_double(dmax), away) == dmax); } + +std::string float2binary(float f) +{ + union + { + float f; + int i; + } c; + + c.f = f; + return integer2binary(c.i, 32); +} + +float random_float(std::mt19937 &gen) +{ + union + { + float f; + unsigned i; + } u; + + std::uniform_int_distribution dist(0, 19); + unsigned r = dist(gen); + + switch(r) + { + case 0: + return PINF; + break; + case 1: + return NINF; + break; + case 2: + return NAN; + break; + case 3: + return PZERO; + break; + case 4: + return NZERO; + break; + default: + std::uniform_int_distribution rand_dist( + 0, std::numeric_limits::max()); + u.i = rand_dist(gen); + u.i = (u.i << 16) ^ rand_dist(gen); + return u.f; + } +} + +bool eq(const ieee_floatt &a, const ieee_floatt &b) +{ + if(a.is_NaN() && b.is_NaN()) + return true; + if(a.is_infinity() && b.is_infinity() && a.get_sign() == b.get_sign()) + return true; + return a == b; +} + +typedef enum +{ + PLUS = 0, + MINUS = 1, + MULT = 2, + DIV = 3 +} binopt; +typedef enum +{ + EQ = 0, + NEQ = 1, + LT = 2, + LE = 3, + GT = 4, + GE = 5 +} binrel; + +TEST_CASE("IEEE float arithmetic operations", "[core][util][ieee_float]") +{ + std::random_device rd; + std::mt19937 gen(rd()); + + for(unsigned i = 0; i < 1000; i++) + { + ieee_floatt i1, i2, i3, res; + float f1, f2, f3; + + f1 = random_float(gen); + f2 = random_float(gen); + i1.from_float(f1); + i2.from_float(f2); + res = i1; + f3 = f1; + + int op = (binopt)i % 4; + + switch(op) + { + case PLUS: + f3 += f2; + res += i2; + break; + + case MINUS: + f3 -= f2; + res -= i2; + break; + + case MULT: + f3 *= f2; + res *= i2; + break; + + case DIV: + f3 /= f2; + res /= i2; + break; + + default: + REQUIRE(false); + } + + i3.from_float(f3); + REQUIRE(eq(res, i3)); + } +} + +TEST_CASE("IEEE float comparison operations", "[core][util][ieee_float]") +{ + std::random_device rd; + std::mt19937 gen(rd()); + + for(unsigned i = 0; i < 1000; i++) + { + ieee_floatt i1, i2; + float f1, f2; + bool ires, fres; + + f1 = random_float(gen); + f2 = random_float(gen); + i1.from_float(f1); + i2.from_float(f2); + + int op = (binrel)i % 6; + + switch(op) + { + case EQ: + ires = ieee_equal(i1, i2); + fres = (f1 == f2); + break; + case NEQ: + ires = ieee_not_equal(i1, i2); + fres = (f1 != f2); + break; + case LT: + ires = (i1 < i2); + fres = (f1 < f2); + break; + case LE: + ires = (i1 <= i2); + fres = (f1 <= f2); + break; + case GT: + ires = (i1 > i2); + fres = (f1 > f2); + break; + case GE: + ires = (i1 >= i2); + fres = (f1 >= f2); + break; + default: + REQUIRE(false); + } + + REQUIRE(ires == fres); + } +} + +TEST_CASE("IEEE float conversion", "[core][util][ieee_float]") +{ + std::random_device rd; + std::mt19937 gen(rd()); + + for(unsigned i = 0; i < 1000; i++) + { + union + { + float f; + unsigned i; + } a, b; + + a.f = random_float(gen); + + ieee_floatt t; + t.from_float(a.f); + + REQUIRE(t.is_float()); + b.f = t.to_float(); + + bool same = (a.i == b.i) || ((a.f != a.f) && (b.f != b.f)); + REQUIRE(same); + } +} + +#ifndef _WIN32 +TEST_CASE("IEEE float nextafter", "[core][util][ieee_float]") +{ + std::random_device rd; + std::mt19937 gen(rd()); + + for(unsigned i = 0; i < 100; i++) + { + float f1 = random_float(gen); + float f2 = nextafterf(f1, PINF); + float f3 = nextafterf(f1, NINF); + + ieee_floatt i1, i2, i3; + + i1.from_float(f1); + i2 = i1; + i2.increment(false); + i3 = i1; + i3.decrement(false); + + bool match1 = (f1 == i1.to_float()) || (f1 != f1 && i1.is_NaN()); + bool match2 = (f2 == i2.to_float()) || (f2 != f2 && i2.is_NaN()); + bool match3 = (f3 == i3.to_float()) || (f3 != f3 && i3.is_NaN()); + + REQUIRE(match1); + REQUIRE(match2); + REQUIRE(match3); + } +} +#endif + +TEST_CASE("IEEE float min/max", "[core][util][ieee_float]") +{ + float f = 0; + ieee_floatt t; + t.from_float(f); + + t.make_fltmax(); + REQUIRE(t.to_float() == FLT_MAX); + + t.make_fltmin(); + REQUIRE(t.to_float() == FLT_MIN); +} + +TEST_CASE("IEEE float build/extract", "[core][util][ieee_float]") +{ + std::random_device rd; + std::mt19937 gen(rd()); + + for(unsigned i = 0; i < 100; i++) + { + float f = random_float(gen); + ieee_floatt t; + t.from_float(f); + + mp_integer old_frac, old_exp; + t.extract_base2(old_frac, old_exp); + mp_integer frac_bak = old_frac, exp_bak = old_exp; + t.build(old_frac, old_exp); + t.extract_base2(old_frac, old_exp); + + REQUIRE(frac_bak == old_frac); + REQUIRE(exp_bak == old_exp); + } +} diff --git a/unit/util/json.cpp b/unit/util/json.cpp new file mode 100644 index 00000000000..c9da7c583ca --- /dev/null +++ b/unit/util/json.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + +Module: Unit tests for JSON parser + +Author: Daniel Kroening + +\*******************************************************************/ + +#include + +#include +#include + +#include + +TEST_CASE("Parse empty JSON object", "[core][json][json_parser]") +{ + std::istringstream in("{}"); + console_message_handlert message_handler; + jsont json; + + bool result = parse_json(in, "", message_handler, json); + + REQUIRE(result == false); // false means success + REQUIRE(json.is_object()); +} + +TEST_CASE("Parse JSON with string", "[core][json][json_parser]") +{ + std::istringstream in(R"({"key": "value"})"); + console_message_handlert message_handler; + jsont json; + + bool result = parse_json(in, "", message_handler, json); + + REQUIRE(result == false); // false means success + REQUIRE(json.is_object()); +} + +TEST_CASE("Parse JSON array", "[core][json][json_parser]") +{ + std::istringstream in("[1, 2, 3]"); + console_message_handlert message_handler; + jsont json; + + bool result = parse_json(in, "", message_handler, json); + + REQUIRE(result == false); // false means success + REQUIRE(json.is_array()); +} + +TEST_CASE("Parse JSON with number", "[core][json][json_parser]") +{ + std::istringstream in(R"({"number": 42})"); + console_message_handlert message_handler; + jsont json; + + bool result = parse_json(in, "", message_handler, json); + + REQUIRE(result == false); // false means success + REQUIRE(json.is_object()); +} + +TEST_CASE("Parse invalid JSON", "[core][json][json_parser]") +{ + std::istringstream in("{invalid}"); + console_message_handlert message_handler; + jsont json; + + bool result = parse_json(in, "", message_handler, json); + + REQUIRE(result == true); // true means error +} diff --git a/unit/wp.cpp b/unit/wp.cpp deleted file mode 100644 index 3af7a66d1ce..00000000000 --- a/unit/wp.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/// Author: Diffblue Ltd. - -#include - -#include -#include -#include -#include -#include - -#include -#include -#include - -#include -#include - -int main(int argc, const char **argv) -{ - try - { - cmdlinet cmdline; - config.set(cmdline); - - register_language(new_ansi_c_language); - - console_message_handlert message_handler; - ansi_c_languaget language; - language.set_message_handler(message_handler); - - language.parse(std::cin, ""); - - symbol_tablet symbol_table; - language.typecheck(symbol_table, "cin"); - - goto_functionst goto_functions; - - goto_convert(symbol_table, goto_functions, message_handler); - - goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.find("f"); - - if(f_it==goto_functions.function_map.end()) - { - std::cerr << "no function f" << std::endl; - return 2; - } - - const goto_programt &p=f_it->second.body; - - // p.output(namespacet(symbol_table), "f", std::cout); - - forall_goto_program_instructions(it, p) - { - if(it->is_end_function()) break; - codet code=it->code; - - it++; - if(!it->is_assert()) - { - std::cerr << "f is expected to have assertion" << std::endl; - return 4; - } - - exprt post=it->guard; - - namespacet ns(symbol_table); - - exprt pre=wp(code, post, ns); - - std::cout << "CODE: " << expr2c(code, ns) - << "wp(" << expr2c(post, ns) << "): " - << expr2c(pre, ns) << std::endl; - simplify(pre, ns); - std::cout << "Simp: " << expr2c(pre, ns) << std::endl; - std::cout << std::endl; - } - } - - catch(const std::string &s) - { - std::cerr << s << std::endl; - } -}