From e3298af667a8998b8cdeeeb8f0c3282c625543a7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 08:17:25 +0000 Subject: [PATCH 01/11] Visual Studio does not strip trailing zeros in hexfloat mode, value is in range --- jbmc/unit/java_bytecode/expr2java.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/jbmc/unit/java_bytecode/expr2java.cpp b/jbmc/unit/java_bytecode/expr2java.cpp index c3f6bb10f18..124fd45622d 100644 --- a/jbmc/unit/java_bytecode/expr2java.cpp +++ b/jbmc/unit/java_bytecode/expr2java.cpp @@ -96,21 +96,37 @@ TEST_CASE( SECTION("Hex float to string (print a comment)") { const float value = std::strtod("0x1p+37f", nullptr); +#ifndef _MSC_VER REQUIRE( floating_point_to_java_string(value) == "0x1p+37f /* 1.37439e+11 */"); +#else + REQUIRE( + floating_point_to_java_string(value) == + "0x1.000000p+37f /* 1.37439e+11 */"); +#endif } SECTION("Hex double to string (print a comment)") { const double value = std::strtod("0x1p+37f", nullptr); +#ifndef _MSC_VER REQUIRE( floating_point_to_java_string(value) == "0x1p+37 /* 1.37439e+11 */"); +#else + REQUIRE( + floating_point_to_java_string(value) == + "0x1.000000p+37 /* 1.37439e+11 */"); +#endif } SECTION("Beyond numeric limits") { +#ifndef _MSC_VER REQUIRE( floating_point_to_java_string(-5.56268e-309) .find("/* -5.56268e-309 */") != std::string::npos); +#else + REQUIRE(floating_point_to_java_string(-5.56268e-309) == "-5.56268e-309"); +#endif } } From c570e01c1ca051217b008d5c83e7a08fd9796e01 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Aug 2018 18:10:40 +0000 Subject: [PATCH 02/11] jbmc/unit/Makefile: Lexicographically sort source files --- jbmc/unit/Makefile | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4f6b2ae29d4..3b4885ca761 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -5,26 +5,29 @@ SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \ # Empty last line # Test source files -SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ +SRC += java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ java_bytecode/goto-programs/class_hierarchy_graph.cpp \ + java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \ + java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \ java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ - java_bytecode/java_bytecode_parser/parse_java_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ + java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ + java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ + java_bytecode/java_bytecode_parser/parse_java_class.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ - java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ - java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ java_bytecode/java_types/generic_type_index.cpp \ java_bytecode/java_types/java_generic_symbol_type.cpp \ java_bytecode/java_types/java_type_from_string.cpp \ java_bytecode/java_utils_test.cpp \ + java_bytecode/java_virtual_functions/virtual_functions.cpp \ java_bytecode/load_method_by_regex.cpp \ - java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ pointer-analysis/custom_value_set_analysis.cpp \ solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \ solvers/refinement/string_refinement/dependency_graph.cpp \ @@ -33,9 +36,6 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ util/has_subtype.cpp \ util/parameter_indices.cpp \ util/simplify_expr.cpp \ - java_bytecode/java_virtual_functions/virtual_functions.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ - java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ # Empty last line INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit From 634caa2a332cc157b739c077b0fa3406e7ede308 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Aug 2018 18:11:41 +0000 Subject: [PATCH 03/11] jbmc/unit/Makefile: add missing source files --- jbmc/unit/Makefile | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 3b4885ca761..e6629b8b4ac 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -5,21 +5,41 @@ SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \ # Empty last line # Test source files -SRC += java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ +SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ + java_bytecode/expr2java.cpp \ + java_bytecode/goto_program_generics/generic_bases_test.cpp \ + java_bytecode/goto_program_generics/generic_parameters_test.cpp \ + java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ java_bytecode/goto-programs/class_hierarchy_graph.cpp \ java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \ java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \ + java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \ java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \ + java_bytecode/java_bytecode_convert_method/convert_method.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ + java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ + java_bytecode/java_replace_nondet/replace_nondet.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ java_bytecode/java_types/generic_type_index.cpp \ From 6c91bb4c5be9bd0e3678474f58fe121536ce09ce Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Aug 2018 18:20:07 +0000 Subject: [PATCH 04/11] unit/Makefile: lexicographic sorting and cleanup of redundant entries --- unit/Makefile | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/unit/Makefile b/unit/Makefile index fa9c96aac4b..93337ac5adc 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -6,8 +6,7 @@ SRC = unit_tests.cpp \ # Empty last line # Test source files -SRC += unit_tests.cpp \ - analyses/ai/ai.cpp \ +SRC += analyses/ai/ai.cpp \ analyses/ai/ai_simplify_lhs.cpp \ analyses/call_graph.cpp \ analyses/constant_propagator.cpp \ @@ -16,6 +15,7 @@ SRC += unit_tests.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ goto-programs/goto_trace_output.cpp \ + interpreter/interpreter.cpp \ path_strategies.cpp \ solvers/floatbv/float_utils.cpp \ solvers/refinement/array_pool/array_pool.cpp \ @@ -23,11 +23,11 @@ SRC += unit_tests.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ solvers/refinement/string_refinement/concretize_array.cpp \ - solvers/refinement/string_refinement/substitute_array_list.cpp \ solvers/refinement/string_refinement/sparse_array.cpp \ + solvers/refinement/string_refinement/substitute_array_list.cpp \ solvers/refinement/string_refinement/union_find_replace.cpp \ - util/expr.cpp \ util/expr_cast/expr_cast.cpp \ + util/expr.cpp \ util/file_util.cpp \ util/get_base_name.cpp \ util/graph.cpp \ @@ -36,16 +36,14 @@ SRC += unit_tests.cpp \ util/message.cpp \ util/optional.cpp \ util/replace_symbol.cpp \ - util/sharing_node.cpp \ util/sharing_map.cpp \ + util/sharing_node.cpp \ util/small_map.cpp \ util/small_shared_two_way_ptr.cpp \ util/string_utils/split_string.cpp \ util/string_utils/strip_string.cpp \ util/symbol_table.cpp \ util/unicode.cpp \ - catch_example.cpp \ - interpreter/interpreter.cpp \ # Empty last line INCLUDES= -I ../src/ -I. From 6d24e8d2fd003fc9b4c0c3f3c6f592a02e660a1e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Aug 2018 18:24:15 +0000 Subject: [PATCH 05/11] unit/Makefile: add missing source files --- unit/Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/unit/Makefile b/unit/Makefile index 93337ac5adc..192a76af637 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -10,13 +10,16 @@ SRC += analyses/ai/ai.cpp \ analyses/ai/ai_simplify_lhs.cpp \ analyses/call_graph.cpp \ analyses/constant_propagator.cpp \ + analyses/dependence_graph.cpp \ analyses/disconnect_unreachable_nodes_in_graph.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ goto-programs/goto_trace_output.cpp \ interpreter/interpreter.cpp \ + json/json_parser.cpp \ path_strategies.cpp \ + pointer-analysis/value_set.cpp \ solvers/floatbv/float_utils.cpp \ solvers/refinement/array_pool/array_pool.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ From 1e943d4d30926340017a8a62cc0809778c74ecd4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 09:48:38 +0000 Subject: [PATCH 06/11] Cleanup test log files --- jbmc/regression/jbmc-generics/Makefile | 2 +- jbmc/regression/strings-smoke-tests/Makefile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile index 81024778e07..1639d08dea4 100644 --- a/jbmc/regression/jbmc-generics/Makefile +++ b/jbmc/regression/jbmc-generics/Makefile @@ -20,7 +20,7 @@ show: clean: find -name '*.out' -execdir $(RM) '{}' \; find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log + $(RM) tests.log tests-symex-driven-loading.log %.class: %.java ../../src/org.cprover.jar javac -g -cp ../../src/org.cprover.jar:. $< diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile index 4ff4e5ba834..6a87a176e59 100644 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ b/jbmc/regression/strings-smoke-tests/Makefile @@ -28,4 +28,4 @@ show: clean: find -name '*.out' -execdir $(RM) '{}' \; find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log + $(RM) tests.log tests-symex-driven-loading.log From b289b47888efa8fe54a710a823a9a469ee451005 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 09:49:01 +0000 Subject: [PATCH 07/11] Cleanup dependencies in unit test builds, check number of tests --- jbmc/unit/Makefile | 35 ++++++++++++++++++++++------------- src/ansi-c/Makefile | 2 -- src/cpp/Makefile | 7 +++++-- unit/Makefile | 34 ++++++++++++++++++++++++++-------- 4 files changed, 53 insertions(+), 25 deletions(-) diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index e6629b8b4ac..5bf5f13742e 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -1,4 +1,4 @@ -.PHONY: all cprover.dir jprover.dir testing-utils.dir java-testing-utils.dir test +.PHONY: all jprover.dir test java-testing-utils-clean # Source files for test utilities SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \ @@ -64,18 +64,18 @@ include ../src/config.inc include $(CPROVER_DIR)/src/config.inc include $(CPROVER_DIR)/src/common -cprover.dir: - $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src - jprover.dir: $(MAKE) $(MAKEARGS) -C ../src -cprover-testing-utils.dir: +$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT): jprover.dir $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils -java-testing-utils.dir: +java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir $(MAKE) $(MAKEARGS) -C java-testing-utils +java-testing-utils-clean: + $(MAKE) $(MAKEARGS) -C java-testing-utils clean + # We need to link bmc.o to the unit test, so here's everything it depends on... BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ @@ -138,16 +138,25 @@ OBJ += $(CPROVER_LIBS) \ $(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \ java-testing-utils/java-testing-utils$(LIBEXT) -TESTS = unit_tests$(EXEEXT) \ - # Empty last line +CATCH_TEST = unit_tests$(EXEEXT) +N_CATCH_TESTS = $(shell \ + cat $$(find . -name "*.cpp" ) | \ + grep -c -E "(SCENARIO|TEST_CASE)") + +CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT) + +# only add a dependency for libraries to avoid triggering implicit rules, which +# would cause unnecessary rebuilds +$(filter %$(LIBEXT), CPROVER_LIBS): jprover.dir -CLEANFILES = $(TESTS) +all: $(CATCH_TEST) -all: cprover.dir cprover-testing-utils.dir jprover.dir java-testing-utils.dir - $(MAKE) $(MAKEARGS) $(TESTS) +clean: java-testing-utils-clean -test: all - $(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true +test: $(CATCH_TEST) + if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ + ./$(CATCH_TEST) -l ; fi + ./$(CATCH_TEST) ############################################################################### diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 4e741de9199..d0ccdf84a3a 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -115,8 +115,6 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c %.inc: %.h file_converter$(EXEEXT) ./file_converter$(EXEEXT) < $< > $@ -cprover_library.cpp: cprover_library.inc - ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES) generated_files: \ diff --git a/src/cpp/Makefile b/src/cpp/Makefile index bad4f4030c1..3189c375ba7 100644 --- a/src/cpp/Makefile +++ b/src/cpp/Makefile @@ -59,6 +59,11 @@ all: cpp$(LIBEXT) ############################################################################### +# extra dependencies +cprover_library$(OBJEXT): cprover_library.inc + +############################################################################### + ../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp $(MAKE) -C ../ansi-c library/converter$(EXEEXT) @@ -69,8 +74,6 @@ library_check: library/*.c cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@ -cprover_library.cpp: cprover_library.inc - generated_files: cprover_library.inc ############################################################################### diff --git a/unit/Makefile b/unit/Makefile index 192a76af637..94fbb61a788 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,4 +1,4 @@ -.PHONY: all cprover.dir testing-utils.dir test +.PHONY: all cprover.dir test testing-utils-clean # Source files for test utilities SRC = unit_tests.cpp \ @@ -57,9 +57,12 @@ include ../src/common cprover.dir: $(MAKE) $(MAKEARGS) -C ../src -testing-utils.dir: +testing-utils/testing-utils$(LIBEXT): cprover.dir $(MAKE) $(MAKEARGS) -C testing-utils +testing-utils-clean: + $(MAKE) $(MAKEARGS) -C testing-utils clean + # We need to link bmc.o to the unit test, so here's everything it depends on... BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/bmc$(OBJEXT) \ @@ -108,17 +111,32 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT) -TESTS = unit_tests$(EXEEXT) \ - miniBDD$(EXEEXT) \ +CATCH_TEST = unit_tests$(EXEEXT) +N_CATCH_TESTS = $(shell \ + cat $$(find . -name "*.cpp" \ + -and -not -name "miniBDD_new.cpp" \ + -and -not -name "catch_example.cpp" \ + -a -not -name "expr_undefined_casts.cpp") | \ + grep -c -E "(SCENARIO|TEST_CASE)") + +TESTS = miniBDD$(EXEEXT) \ # Empty last line -CLEANFILES = $(TESTS) +CLEANFILES = $(CATCH_TEST) $(TESTS) testing-utils/testing-utils$(LIBEXT) + +# only add a dependency for libraries to avoid triggering implicit rules, which +# would cause unnecessary rebuilds +$(filter %$(LIBEXT), CPROVER_LIBS): cprover.dir + +all: $(CATCH_TEST) $(TESTS) -all: cprover.dir testing-utils.dir - $(MAKE) $(MAKEARGS) $(TESTS) +clean: testing-utils-clean -test: all +test: $(CATCH_TEST) $(TESTS) $(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true + if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ + ./$(CATCH_TEST) -l ; fi + ./$(CATCH_TEST) ############################################################################### From 5aacb7698ee67c0f51c19b1b3af4f15e0d5528bb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 12:49:30 +0000 Subject: [PATCH 08/11] Remove catch_example.cpp pseudo unit-test We now have ample examples of unit tests. --- unit/Makefile | 2 -- unit/catch_example.cpp | 25 ------------------------- 2 files changed, 27 deletions(-) delete mode 100644 unit/catch_example.cpp diff --git a/unit/Makefile b/unit/Makefile index 94fbb61a788..a8c22462a68 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -2,7 +2,6 @@ # Source files for test utilities SRC = unit_tests.cpp \ - catch_example.cpp \ # Empty last line # Test source files @@ -115,7 +114,6 @@ CATCH_TEST = unit_tests$(EXEEXT) N_CATCH_TESTS = $(shell \ cat $$(find . -name "*.cpp" \ -and -not -name "miniBDD_new.cpp" \ - -and -not -name "catch_example.cpp" \ -a -not -name "expr_undefined_casts.cpp") | \ grep -c -E "(SCENARIO|TEST_CASE)") diff --git a/unit/catch_example.cpp b/unit/catch_example.cpp deleted file mode 100644 index f8cd903d7b7..00000000000 --- a/unit/catch_example.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/*******************************************************************\ - - Module: Example Catch Tests - - Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -unsigned int Factorial(unsigned int number) -{ - return number>1?Factorial(number-1)*number:1; -} - -// This is an example unit test to demonstrate the build system and the -// catch unit test framework. The source code is taken from the documentation -// of catch. -TEST_CASE("Factorials are computed", "[core][factorial]") -{ - REQUIRE(Factorial(1)==1); - REQUIRE(Factorial(2)==2); - REQUIRE(Factorial(3)==6); - REQUIRE(Factorial(10)==3628800); -} From 5e548bc06228a6071fd964cfcba57bdaf71491b1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 13:04:06 +0000 Subject: [PATCH 09/11] Move miniBDD catch-style unit test to proper folder and include in Makefile --- unit/.gitignore | 1 - unit/Makefile | 2 +- unit/{miniBDD_new.cpp => solvers/miniBDD/miniBDD.cpp} | 2 -- unit/solvers/miniBDD/module_dependencies.txt | 4 ++++ 4 files changed, 5 insertions(+), 4 deletions(-) rename unit/{miniBDD_new.cpp => solvers/miniBDD/miniBDD.cpp} (99%) create mode 100644 unit/solvers/miniBDD/module_dependencies.txt diff --git a/unit/.gitignore b/unit/.gitignore index d69e63165b4..326b381fbda 100644 --- a/unit/.gitignore +++ b/unit/.gitignore @@ -1,4 +1,3 @@ # Unit test binaries -miniBDD sharing_node unit_tests diff --git a/unit/Makefile b/unit/Makefile index a8c22462a68..93f630bc38e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,6 +20,7 @@ SRC += analyses/ai/ai.cpp \ path_strategies.cpp \ pointer-analysis/value_set.cpp \ solvers/floatbv/float_utils.cpp \ + solvers/miniBDD/miniBDD.cpp \ solvers/refinement/array_pool/array_pool.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ @@ -113,7 +114,6 @@ OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT) CATCH_TEST = unit_tests$(EXEEXT) N_CATCH_TESTS = $(shell \ cat $$(find . -name "*.cpp" \ - -and -not -name "miniBDD_new.cpp" \ -a -not -name "expr_undefined_casts.cpp") | \ grep -c -E "(SCENARIO|TEST_CASE)") diff --git a/unit/miniBDD_new.cpp b/unit/solvers/miniBDD/miniBDD.cpp similarity index 99% rename from unit/miniBDD_new.cpp rename to unit/solvers/miniBDD/miniBDD.cpp index b38c1207e80..e4c1892a839 100644 --- a/unit/miniBDD_new.cpp +++ b/unit/solvers/miniBDD/miniBDD.cpp @@ -18,8 +18,6 @@ #include #include -#include - class bdd_propt:public propt { public: diff --git a/unit/solvers/miniBDD/module_dependencies.txt b/unit/solvers/miniBDD/module_dependencies.txt new file mode 100644 index 00000000000..05a5cc7502e --- /dev/null +++ b/unit/solvers/miniBDD/module_dependencies.txt @@ -0,0 +1,4 @@ +solvers/miniBDD +solvers/prop +testing-utils +util From 6451ffb3cc278178d1917e2629adc6972ef3a0b6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 13:24:08 +0000 Subject: [PATCH 10/11] Actually use (unicode) operator_str --- src/util/format_expr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 7b087990324..40d895492be 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -88,7 +88,7 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src) if(first) first = false; else - os << ' ' << src.id() << ' '; + os << ' ' << operator_str << ' '; const bool need_parentheses = bracket_subexpression(op, src); From bd55a28bf84cc2853f2cbf26635a8a1a7361d498 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Sep 2018 13:24:25 +0000 Subject: [PATCH 11/11] Make the remaining (relevant) miniBDD catch-style unit tests --- CMakeLists.txt | 1 - unit/CMakeLists.txt | 14 ----- unit/Makefile | 13 +---- unit/miniBDD.cpp | 95 -------------------------------- unit/solvers/miniBDD/miniBDD.cpp | 72 +++++++++++++++++++++++- 5 files changed, 73 insertions(+), 122 deletions(-) delete mode 100644 unit/miniBDD.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index fea650dbac1..0c32e421f01 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -68,7 +68,6 @@ set_target_properties( json langapi linking - miniBDD pointer-analysis solvers test-bigint diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 036cc3ce4c4..6c06a0fc205 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -3,9 +3,6 @@ file(GLOB_RECURSE sources "*.cpp" "*.h") file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h") list(REMOVE_ITEM sources - # Used in executables - ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp - # Don't build ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp @@ -48,14 +45,3 @@ add_test( WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} ) set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC") - -add_executable(miniBDD miniBDD.cpp) -target_include_directories(miniBDD - PUBLIC - ${CBMC_BINARY_DIR} - ${CBMC_SOURCE_DIR} - ${CMAKE_CURRENT_SOURCE_DIR} -) -target_link_libraries(miniBDD solvers ansi-c) -add_test(NAME miniBDD COMMAND $) -set_tests_properties(miniBDD PROPERTIES LABELS "CORE;CBMC") diff --git a/unit/Makefile b/unit/Makefile index 93f630bc38e..bc9800d85a9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -117,21 +117,17 @@ N_CATCH_TESTS = $(shell \ -a -not -name "expr_undefined_casts.cpp") | \ grep -c -E "(SCENARIO|TEST_CASE)") -TESTS = miniBDD$(EXEEXT) \ - # Empty last line - -CLEANFILES = $(CATCH_TEST) $(TESTS) testing-utils/testing-utils$(LIBEXT) +CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) # only add a dependency for libraries to avoid triggering implicit rules, which # would cause unnecessary rebuilds $(filter %$(LIBEXT), CPROVER_LIBS): cprover.dir -all: $(CATCH_TEST) $(TESTS) +all: $(CATCH_TEST) clean: testing-utils-clean -test: $(CATCH_TEST) $(TESTS) - $(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true +test: $(CATCH_TEST) if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ ./$(CATCH_TEST) -l ; fi ./$(CATCH_TEST) @@ -141,6 +137,3 @@ test: $(CATCH_TEST) $(TESTS) unit_tests$(EXEEXT): $(OBJ) $(LINKBIN) - -miniBDD$(EXEEXT): miniBDD$(OBJEXT) $(CPROVER_LIBS) - $(LINKBIN) diff --git a/unit/miniBDD.cpp b/unit/miniBDD.cpp deleted file mode 100644 index bd1eb77eec2..00000000000 --- a/unit/miniBDD.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/*******************************************************************\ - -Module: A minimalistic BDD library, following Bryant's original paper - and Andersen's lecture notes - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include - -#include - -#include - -void test1() -{ - mini_bdd_mgrt mgr; - - mini_bddt x=mgr.Var("x"); - mini_bddt y=mgr.Var("y"); - mini_bddt z=mgr.Var("z"); - mini_bddt f=(x&y&z)|((!x)&(!y)&z); - y.clear(); - x.clear(); - z.clear(); - - // mgr.DumpDot(std::cout); - mgr.DumpTikZ(std::cout); -} - -void test2() -{ - mini_bdd_mgrt mgr; - - mini_bddt a=mgr.Var("a"); - mini_bddt b=mgr.Var("b"); - mini_bddt c=mgr.Var("c"); - mini_bddt d=mgr.Var("d"); - - mini_bddt final=(a==b)&(c==d); - - a.clear(); - b.clear(); - c.clear(); - d.clear(); - - mgr.DumpTikZ(std::cout, true); -} - -void test3() -{ - mini_bdd_mgrt mgr; - - mini_bddt final=mgr.Var("x")&mgr.Var("y"); - - mgr.DumpDot(std::cout); - #if 0 - mgr.DumpTikZ(std::cout); - mgr.DumpTable(std::cout); - #endif -} - -#include -#include -#include - -#include -#include -#include - -#include - -void test4() -{ - symbol_exprt a("a", bool_typet()); - symbol_exprt b("b", bool_typet()); - - or_exprt o(and_exprt(a, b), not_exprt(a)); - - symbol_tablet symbol_table; - namespacet ns(symbol_table); - - std::cout << format(o) << std::endl; - - bdd_exprt t(ns); - t.from_expr(o); - - std::cout << format(t.as_expr()) << std::endl; -} - -int main() -{ - test3(); -} diff --git a/unit/solvers/miniBDD/miniBDD.cpp b/unit/solvers/miniBDD/miniBDD.cpp index e4c1892a839..054bfdb8861 100644 --- a/unit/solvers/miniBDD/miniBDD.cpp +++ b/unit/solvers/miniBDD/miniBDD.cpp @@ -11,12 +11,14 @@ #include -#include #include +#include +#include -#include #include #include +#include +#include class bdd_propt:public propt { @@ -291,4 +293,70 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") REQUIRE(!result.is_constant()); } + + GIVEN("A bdd for x&y") + { + mini_bdd_mgrt mgr; + + mini_bddt x_bdd = mgr.Var("x"); + mini_bddt y_bdd = mgr.Var("y"); + mini_bddt final_bdd = x_bdd & y_bdd; + + std::ostringstream oss; + mgr.DumpDot(oss); + + const std::string dot_string = + "digraph BDD {\n" + "center = true;\n" + "{ rank = same; { node [style=invis]; \"T\" };\n" + " { node [shape=box,fontsize=24]; \"0\"; }\n" + " { node [shape=box,fontsize=24]; \"1\"; }\n" + "}\n" + "\n" + "{ rank=same; { node [shape=plaintext,fontname=" + "\"Times Italic\",fontsize=24] \" x \" }; \"2\"; \"4\"; }\n" + "{ rank=same; { node [shape=plaintext,fontname=" + "\"Times Italic\",fontsize=24] \" y \" }; \"3\"; }\n" + "\n" + "{ edge [style = invis]; \" x \" -> \" y \" -> \"T\"; }\n" + "\n" + "\"2\" -> \"1\" [style=solid,arrowsize=\".75\"];\n" + "\"2\" -> \"0\" [style=dashed,arrowsize=\".75\"];\n" + "\n" + "\"3\" -> \"1\" [style=solid,arrowsize=\".75\"];\n" + "\"3\" -> \"0\" [style=dashed,arrowsize=\".75\"];\n" + "\n" + "\"4\" -> \"3\" [style=solid,arrowsize=\".75\"];\n" + "\"4\" -> \"0\" [style=dashed,arrowsize=\".75\"];\n" + "\n" + "}\n"; + + REQUIRE(oss.str() == dot_string); + } + + GIVEN("A bdd for (a&b)|!a") + { + symbol_exprt a("a", bool_typet()); + symbol_exprt b("b", bool_typet()); + + or_exprt o(and_exprt(a, b), not_exprt(a)); + + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + { + std::ostringstream oss; + oss << format(o); + REQUIRE(oss.str() == "(a ∧ b) ∨ (¬a)"); + } + + bdd_exprt t(ns); + t.from_expr(o); + + { + std::ostringstream oss; + oss << format(t.as_expr()); + REQUIRE(oss.str() == "(¬a) ∨ b"); + } + } }