From 53e380772ae23d229054b3106a1000a4f416f9c3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 28 Aug 2018 00:44:01 +0100 Subject: [PATCH 1/2] Remove jbmc-cover tests --- jbmc/regression/CMakeLists.txt | 1 - jbmc/regression/Makefile | 1 - jbmc/regression/jbmc-cover/CMakeLists.txt | 3 -- jbmc/regression/jbmc-cover/Makefile | 34 ---------------- .../jbmc-cover/covered1/covered1.class | Bin 750 -> 0 bytes .../jbmc-cover/covered1/covered1.java | 37 ------------------ jbmc/regression/jbmc-cover/covered1/test.desc | 33 ---------------- .../jbmc-cover/json_trace2/Test.class | Bin 292 -> 0 bytes .../jbmc-cover/json_trace2/Test.java | 7 ---- .../jbmc-cover/json_trace2/test.desc | 10 ----- 10 files changed, 126 deletions(-) delete mode 100644 jbmc/regression/jbmc-cover/CMakeLists.txt delete mode 100644 jbmc/regression/jbmc-cover/Makefile delete mode 100644 jbmc/regression/jbmc-cover/covered1/covered1.class delete mode 100644 jbmc/regression/jbmc-cover/covered1/covered1.java delete mode 100644 jbmc/regression/jbmc-cover/covered1/test.desc delete mode 100644 jbmc/regression/jbmc-cover/json_trace2/Test.class delete mode 100644 jbmc/regression/jbmc-cover/json_trace2/Test.java delete mode 100644 jbmc/regression/jbmc-cover/json_trace2/test.desc diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 65da4bee9a9..33d5ce64a0f 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/jbmc/regression/CMakeLists.txt @@ -10,5 +10,4 @@ add_subdirectory(jdiff) add_subdirectory(janalyzer-taint) add_subdirectory(jbmc-concurrency) add_subdirectory(jbmc-inheritance) -add_subdirectory(jbmc-cover) add_subdirectory(jbmc-generics) diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile index 17b0e94bb01..42a479942e2 100644 --- a/jbmc/regression/Makefile +++ b/jbmc/regression/Makefile @@ -4,7 +4,6 @@ DIRS = janalyzer-taint \ jbmc \ jbmc-concurrency \ - jbmc-cover \ jbmc-inheritance \ jbmc-strings \ jdiff \ diff --git a/jbmc/regression/jbmc-cover/CMakeLists.txt b/jbmc/regression/jbmc-cover/CMakeLists.txt deleted file mode 100644 index afe0ea5761a..00000000000 --- a/jbmc/regression/jbmc-cover/CMakeLists.txt +++ /dev/null @@ -1,3 +0,0 @@ -add_test_pl_tests( - "$" -) diff --git a/jbmc/regression/jbmc-cover/Makefile b/jbmc/regression/jbmc-cover/Makefile deleted file mode 100644 index ad6e5381fff..00000000000 --- a/jbmc/regression/jbmc-cover/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -default: tests.log - -include ../../src/config.inc - -test: - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - -tests.log: ../$(CPROVER_DIR)/regression/test.pl - @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log - -%.class: %.java ../../src/org.cprover.jar - javac -g -cp ../../src/org.cprover.jar:. $< - -nondet_java_files := $(shell find . -name "Nondet*.java") -nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) - -.PHONY: nondet-class-files -nondet-class-files: $(nondet_class_files) - -.PHONY: clean-nondet-class-files -clean-nondet-class-files: - -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-cover/covered1/covered1.class b/jbmc/regression/jbmc-cover/covered1/covered1.class deleted file mode 100644 index 7cb91496b7df5bc0b1e7f8b6db0aa9a4992bd947..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 750 zcmYk4TWb?h6ouEBOJ*jSCQa%+wf9SU)TC(>1*uXHiUBVVl?py}G8x*`n3Rwf?N9N^ zw?5lA2nzlHf0VlRp`r}?+xwiuIcx3B{QULp2Y?11WKlpRKptxXEx04NE4U}93TlFN zL0zyR*c3E8G(Fr`Q12Nn#s|ikf_1jeB4V@^>_Ml)>WysI1sj4*K||0~$ZU1{-O*zO zx6*2@?I}1<2AxEq@T}WUUYxvZC&O1!yT_f0-BA?3eI6Z~HT4zzt+;o2-LA;x?C#)X z7$-Yjb0Hp_Cc~stuO3CGQHU8VhnPe$L`g6uxGA_LC<|^2t_rRRt_ZHw`A%h|$M8{-GG5hkKSyRDeikN*$m^Iy)OhYEqlR2ll zS<@b~#hAe?6y{ichs_Uot-nHPCxxZm6t>Q!aHMjj%4jczr~MSZE>9n(2$=R$Wc3#W z' -^EXIT=0$ -^SIGNAL=0$ -.*\"coveredLines\": \"22\",$ -(.*\"coveredLines\": \"4\")|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"6\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"7\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"23\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"24\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"25\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"31\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"32\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"33\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"36\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ -.*\"coveredLines\": \"26\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"28\",$ -.*\"coveredLines\": \"29\",$ -.*\"coveredLines\": \"18\",$ -.*\"coveredLines\": \"18\",$ -.*\"coveredLines\": \"35\",$ --- -^warning: ignoring --- -The alternation between the grouped and ungrouped reporting formats for coveredLines accommodates the -difference between symex-driven-lazy-loading (which currently causes jbmc to use the grouped format) -and normal loading (which uses the ungrouped format). -The cause of the difference appears to be symex-driven loading being more pessimistic about possible -exceptions coming from callees, which in turn changes the shape of the CFG. diff --git a/jbmc/regression/jbmc-cover/json_trace2/Test.class b/jbmc/regression/jbmc-cover/json_trace2/Test.class deleted file mode 100644 index 68771db843ab17d0c80c4dbea1b7f72f1f9c2b9f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 292 zcmZ8bJx{|h6ucMPNfY|DFm_-|i$sOQ24bni)Rv(Y1Dg{plu}YuTz*v-CM1TgNcrKZ8OiK{r895MNbw<*x-QAKnS{Wb@zzy=hgu`R=)J+odhm zRJ3=mUT~aGSN6@0*S3Bf-xe!Z`pe Date: Mon, 27 Aug 2018 23:37:48 +0100 Subject: [PATCH 2/2] Remove --cover option from JBMC --- jbmc/src/jbmc/jbmc_parse_options.cpp | 42 ++++------------------------ jbmc/src/jbmc/jbmc_parse_options.h | 4 +-- 2 files changed, 6 insertions(+), 40 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index a4474d1edd5..7d134f4dfff 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -121,9 +121,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("show-vcc")) options.set_option("show-vcc", true); - if(cmdline.isset("cover")) - parse_cover_options(cmdline, options); - if(cmdline.isset("nondet-static")) options.set_option("nondet-static", true); @@ -189,14 +186,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("assumptions", false); // generate unwinding assertions - if(cmdline.isset("cover")) - options.set_option("unwinding-assertions", false); - else - { - options.set_option( - "unwinding-assertions", - cmdline.isset("unwinding-assertions")); - } + if(cmdline.isset("unwinding-assertions")) + options.set_option("unwinding-assertions", true); // generate unwinding assumptions otherwise options.set_option( @@ -559,12 +550,6 @@ int jbmc_parse_optionst::doit() // particular function: add_failed_symbols(lazy_goto_model.symbol_table); - // If applicable, parse the coverage instrumentation configuration, which - // will be used in process_goto_function: - cover_config = - get_cover_config( - options, lazy_goto_model.symbol_table, get_message_handler()); - // Provide show-goto-functions and similar dump functions after symex // executes. If --paths is active, these dump routines run after every // paths iteration. Its return value indicates that if we ran any dump @@ -782,20 +767,12 @@ void jbmc_parse_optionst::process_goto_function( symbol_table); } - // If using symex-driven function loading we must insert the coverage goals + // If using symex-driven function loading we must label the assertions // now so symex sees its targets; otherwise we leave this until // process_goto_functions, as we haven't run remove_exceptions yet, and that // pass alters the CFG. if(using_symex_driven_loading) { - // instrument cover goals - if(cmdline.isset("cover")) - { - INVARIANT( - cover_config != nullptr, "cover config should have been parsed"); - instrument_cover_goals(*cover_config, function, get_message_handler()); - } - // label the assertions label_properties(goto_function.body); @@ -916,17 +893,9 @@ bool jbmc_parse_optionst::process_goto_functions( remove_unused_functions(goto_model, get_message_handler()); } - // remove skips such that trivial GOTOs are deleted and not considered - // for coverage annotation: + // remove skips such that trivial GOTOs are deleted remove_skip(goto_model); - // instrument cover goals - if(cmdline.isset("cover")) - { - if(instrument_cover_goals(options, goto_model, get_message_handler())) - return true; - } - // label the assertions // This must be done after adding assertions and // before using the argument of the "property" option. @@ -970,7 +939,7 @@ bool jbmc_parse_optionst::process_goto_functions( full_slicer(goto_model); } - // remove any skips introduced since coverage instrumentation + // remove any skips introduced remove_skip(goto_model); } @@ -1079,7 +1048,6 @@ void jbmc_parse_optionst::help() " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" - " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) HELP_REACHABILITY_SLICER " --full-slice run full slicer (experimental)\n" // NOLINT(*) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index d0c5ad3d094..69d7f5a0a8b 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -69,7 +68,7 @@ class optionst; "(verbosity):" \ "(nondet-static)" \ "(version)" \ - "(cover):(symex-coverage-report):" \ + "(symex-coverage-report):" \ OPT_TIMESTAMP \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \ "(ppc-macos)" \ @@ -120,7 +119,6 @@ class jbmc_parse_optionst: protected: ui_message_handlert ui_message_handler; - std::unique_ptr cover_config; path_strategy_choosert path_strategy_chooser; object_factory_parameterst object_factory_params; bool stub_objects_are_not_null;