From ee7a4e9d9e980f5333d4e9a3039aa34ed7a8d1ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 00:32:53 +0000 Subject: [PATCH 1/5] Avoid unnecessary #include in header file goto_check.h can safely use forward declarations of namespacet and optionst. --- src/analyses/goto_check.cpp | 1 + src/analyses/goto_check.h | 6 +++--- src/goto-diff/goto_diff_parse_options.cpp | 1 + 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 8aa43ba9769..8d808430ee6 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "local_bitvector_analysis.h" #include "goto_check.h" diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 0620ce1560d..605b6151078 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -9,12 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H #define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H -#include -#include - #include #include +class namespacet; +class optionst; + void goto_check( const namespacet &ns, const optionst &options, diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 317da4bf32b..811275e6112 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -16,6 +16,7 @@ Author: Peter Schrammel #include #include #include +#include #include #include From ba50b4c84aa27ab5adad25ea7d0f41100d6a91a2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 00:35:24 +0000 Subject: [PATCH 2/5] Removed goto_check where its options are never set There is no need to #include goto_check.h or call goto_check when none of the *-check (command-line-) options are ever set. --- .../goto_analyzer_parse_options.cpp | 49 ------------------- src/goto-diff/goto_diff_parse_options.cpp | 6 --- src/musketeer/musketeer_parse_options.cpp | 4 -- 3 files changed, 59 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 50622b4d2a5..4b29d4b8548 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -30,7 +30,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -154,54 +153,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) #endif #if 0 - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); - // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 811275e6112..1943c7c5ced 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -37,8 +37,6 @@ Author: Peter Schrammel #include -#include - #include #include @@ -496,10 +494,6 @@ bool goto_diff_parse_optionst::process_goto_program( remove_vector(symbol_table, goto_functions); remove_complex(symbol_table, goto_functions); - // add generic checks - status() << "Generic Property Instrumentation" << eom; - goto_check(ns, options, goto_functions); - // add failed symbols // needs to be done before pointer analysis add_failed_symbols(symbol_table); diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp index 3ac2ba56b37..28accf23fa2 100644 --- a/src/musketeer/musketeer_parse_options.cpp +++ b/src/musketeer/musketeer_parse_options.cpp @@ -32,7 +32,6 @@ Module: Main Module #include #include -#include #include #include @@ -204,9 +203,6 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( namespacet ns(symbol_table); - // add generic checks, if needed - goto_check(ns, options, goto_functions); - if( cmdline.isset("mm") || cmdline.isset("all-shared") || cmdline.isset("volatile") From 8fe5d4193749609c3fcde52bca6deb0034770384 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 00:38:37 +0000 Subject: [PATCH 3/5] Simplify and enable consistent *-check options All invocations of goto_check should support the same set of command-line options. GOTO_CHECK_OPTIONS provides the collection of command-line parameters for parsing, GOTO_CHECK_PARSE_OPTIONS actually performs the command-line parsing, and CHECK_CHECK_HELP provides uniform help text. --- src/aa-symex/symex_parseoptions.cpp | 53 +-------------- src/aa-symex/symex_parseoptions.h | 5 +- src/analyses/goto_check.h | 28 ++++++++ src/cbmc/cbmc_parse_options.cpp | 60 +---------------- src/cbmc/cbmc_parse_options.h | 5 +- src/clobber/clobber_parse_options.cpp | 59 +---------------- src/clobber/clobber_parse_options.h | 6 +- .../goto_instrument_parse_options.cpp | 65 +------------------ .../goto_instrument_parse_options.h | 12 ++-- src/symex/symex_parse_options.cpp | 59 +---------------- src/symex/symex_parse_options.h | 6 +- 11 files changed, 61 insertions(+), 297 deletions(-) diff --git a/src/aa-symex/symex_parseoptions.cpp b/src/aa-symex/symex_parseoptions.cpp index a83ce22223f..e9099b1d568 100644 --- a/src/aa-symex/symex_parseoptions.cpp +++ b/src/aa-symex/symex_parseoptions.cpp @@ -28,8 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include @@ -112,47 +110,8 @@ void symex_parseoptionst::get_command_line_options(optionst &options) if(cmdline.isset("unwindset")) options.set_option("unwindset", cmdline.getval("unwindset")); - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); + // all checks supported by goto_check + GOTO_CHECK_PARSE_OPTIONS(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -811,13 +770,7 @@ void symex_parseoptionst::help() " --round-to-zero IEEE floating point rounding mode\n" "\n" "Program instrumentation options:\n" - " --bounds-check enable array bounds checks\n" - " --div-by-zero-check enable division by zero checks\n" - " --pointer-check enable pointer checks\n" - " --memory-leak-check enable memory leak checks\n" - " --signed-overflow-check enable arithmetic over- and underflow checks\n" - " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" - " --nan-check check floating-point for NaN\n" + GOTO_CHECK_HELP " --show-properties show the properties\n" " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" diff --git a/src/aa-symex/symex_parseoptions.h b/src/aa-symex/symex_parseoptions.h index 4c2ba908088..f70da76dbfe 100644 --- a/src/aa-symex/symex_parseoptions.h +++ b/src/aa-symex/symex_parseoptions.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include "path_search.h" class goto_functionst; @@ -23,8 +25,7 @@ class optionst; "(function):" \ "D:I:" \ "(depth):(context-bound):(unwind):" \ - "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \ - "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \ + GOTO_CHECK_OPTIONS \ "(no-assertions)(no-assumptions)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 605b6151078..5d92c83c9bb 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -29,4 +29,32 @@ void goto_check( const optionst &options, goto_modelt &goto_model); +#define GOTO_CHECK_OPTIONS \ + "(bounds-check)(pointer-check)(memory-leak-check)" \ + "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \ + "(undefined-shift-check)" \ + "(float-overflow-check)(nan-check)" + +#define GOTO_CHECK_HELP \ + " --bounds-check enable array bounds checks\n" \ + " --pointer-check enable pointer checks\n" \ + " --memory-leak-check enable memory leak checks\n" \ + " --div-by-zero-check enable division by zero checks\n" \ + " --signed-overflow-check enable signed arithmetic over- and underflow checks\n" \ + " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" \ + " --undefined-shift-check check shift greater than bit-width\n" \ + " --float-overflow-check check floating-point for +/-Inf\n" \ + " --nan-check check floating-point for NaN\n" \ + +#define GOTO_CHECK_PARSE_OPTIONS(cmdline, options) \ + options.set_option("bounds-check", cmdline.isset("bounds-check")); \ + options.set_option("pointer-check", cmdline.isset("pointer-check")); \ + options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \ + options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \ + options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \ + options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \ + options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \ + options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \ + options.set_option("nan-check", cmdline.isset("nan-check")) + #endif diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 09f2f17812d..0c7027e0dea 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -46,8 +46,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include "cbmc_solvers.h" @@ -218,53 +216,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) else options.set_option("propagation", true); - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); + // all checks supported by goto_check + GOTO_CHECK_PARSE_OPTIONS(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -1137,14 +1090,7 @@ void cbmc_parse_optionst::help() " --show-goto-functions show goto program\n" "\n" "Program instrumentation options:\n" - " --bounds-check enable array bounds checks\n" - " --div-by-zero-check enable division by zero checks\n" - " --pointer-check enable pointer checks\n" - " --memory-leak-check enable memory leak checks\n" - " --signed-overflow-check enable arithmetic over- and underflow checks\n" - " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" - " --float-overflow-check check floating-point for +/-Inf\n" - " --nan-check check floating-point for NaN\n" + GOTO_CHECK_HELP " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 1a4b9477cfd..8f0269d4cb6 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include "xml_interface.h" class bmct; @@ -28,8 +30,7 @@ class optionst; "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \ "(classpath):(cp):(main-class):" \ "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \ - "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \ - "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)(nan-check)" \ + GOTO_CHECK_OPTIONS \ "(no-assertions)(no-assumptions)" \ "(xml-ui)(xml-interface)(json-ui)" \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 8c9fb178dad..ab94bc84cfb 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -30,8 +30,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include @@ -112,53 +110,8 @@ void clobber_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("unwindset")) options.set_option("unwindset", cmdline.getval("unwindset")); - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); + // all checks supported by goto_check + GOTO_CHECK_PARSE_OPTIONS(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -788,13 +741,7 @@ void clobber_parse_optionst::help() " --round-to-zero IEEE floating point rounding mode\n" "\n" "Program instrumentation options:\n" - " --bounds-check enable array bounds checks\n" - " --div-by-zero-check enable division by zero checks\n" - " --pointer-check enable pointer checks\n" - " --memory-leak-check enable memory leak checks\n" - " --signed-overflow-check enable arithmetic over- and underflow checks\n" - " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" - " --nan-check check floating-point for NaN\n" + GOTO_CHECK_HELP " --show-properties show the properties\n" " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h index d00db917084..de74b73ff20 100644 --- a/src/clobber/clobber_parse_options.h +++ b/src/clobber/clobber_parse_options.h @@ -14,14 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + class goto_functionst; class optionst; #define CLOBBER_OPTIONS \ "(depth):(context-bound):(unwind):" \ - "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \ - "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \ - "(float-overflow-check)" \ + GOTO_CHECK_OPTIONS \ "(no-assertions)(no-assumptions)" \ "(error-label):(verbosity):(no-library)" \ "(version)" \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8fd60ad0fb3..4f1d49e74ca 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -43,7 +43,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -783,59 +782,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() else options.set_option("assert-to-assume", false); - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check undefined shifts - if(cmdline.isset("undefined-shift-check")) - options.set_option("undefined-shift-check", true); - else - options.set_option("undefined-shift-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check pointers - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); + // all checks supported by goto_check + GOTO_CHECK_PARSE_OPTIONS(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -1308,14 +1256,7 @@ void goto_instrument_parse_optionst::help() "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" - " --bounds-check add array bounds checks\n" - " --div-by-zero-check add division by zero checks\n" - " --pointer-check add pointer checks\n" - " --memory-leak-check add memory leak checks\n" - " --signed-overflow-check add arithmetic over- and underflow checks\n" - " --unsigned-overflow-check add arithmetic over- and underflow checks\n" - " --undefined-shift-check add range checks for shift distances\n" - " --nan-check add floating-point NaN checks\n" + GOTO_CHECK_HELP " --uninitialized-check add checks for uninitialized locals (experimental)\n" " --error-label label check that label is unreachable\n" " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1123a1ec6e9..da9c266bf86 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -15,20 +15,21 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #define GOTO_INSTRUMENT_OPTIONS \ "(all)" \ "(document-claims-latex)(document-claims-html)" \ "(document-properties-latex)(document-properties-html)" \ "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \ - "(bounds-check)(no-bounds-check)" \ - "(pointer-check)(memory-leak-check)(no-pointer-check)" \ + GOTO_CHECK_OPTIONS \ + /* no-X-check are deprecated and ignored */ \ + "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \ + "(no-nan-check)" \ "(remove-pointers)" \ "(no-simplify)" \ "(assert-to-assume)" \ - "(div-by-zero-check)(no-div-by-zero-check)" \ - "(undefined-shift-check)" \ "(no-assertions)(no-assumptions)(uninitialized-check)" \ - "(nan-check)(no-nan-check)" \ "(race-check)(scc)(one-event-per-cycle)" \ "(minimum-interference)" \ "(mm):(my-events)(unwind):" \ @@ -39,7 +40,6 @@ Author: Daniel Kroening, kroening@kroening.com "(nondet-volatile)(isr):" \ "(stack-depth):(nondet-static)" \ "(function-enter):(function-exit):(branch):" \ - "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)" \ "(show-goto-functions)(show-value-sets)" \ "(show-global-may-alias)" \ "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \ diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index bfd6a24cae5..7a9227e6f58 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -35,8 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include @@ -120,53 +118,8 @@ void symex_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("unwindset")) options.set_option("unwindset", cmdline.get_value("unwindset")); - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); + // all checks supported by goto_check + GOTO_CHECK_PARSE_OPTIONS(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -743,13 +696,7 @@ void symex_parse_optionst::help() " --function name set main function name\n" "\n" "Program instrumentation options:\n" - " --bounds-check enable array bounds checks\n" - " --div-by-zero-check enable division by zero checks\n" - " --pointer-check enable pointer checks\n" - " --memory-leak-check enable memory leak checks\n" - " --signed-overflow-check enable arithmetic over- and underflow checks\n" - " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" - " --nan-check check floating-point for NaN\n" + GOTO_CHECK_HELP " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index b93c937515e..0a84fa98b32 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include "path_search.h" class goto_functionst; @@ -25,9 +27,7 @@ class optionst; "(function):" \ "D:I:" \ "(depth):(context-bound):(branch-bound):(unwind):" \ - "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \ - "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \ - "(float-overflow-check)" \ + GOTO_CHECK_OPTIONS \ "(no-assertions)(no-assumptions)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ From 4906236c628b4ae1c7023242d821f9b03626c556 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 00:43:25 +0000 Subject: [PATCH 4/5] Decouple pointer-check and pointer-arithmetic overflow In 0779bbd70143 additional checks for arithmetic overflow on pointer arithmetic were added, and enabled implicitly when --pointer-check was set. This is now decoupled and a new option --pointer-overflow-check is available. --- src/analyses/goto_check.cpp | 4 +++- src/analyses/goto_check.h | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 8d808430ee6..1fb83d4b6c1 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -40,6 +40,7 @@ class goto_checkt enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check"); enable_signed_overflow_check=_options.get_bool_option("signed-overflow-check"); enable_unsigned_overflow_check=_options.get_bool_option("unsigned-overflow-check"); + enable_pointer_overflow_check=_options.get_bool_option("pointer-overflow-check"); enable_undefined_shift_check=_options.get_bool_option("undefined-shift-check"); enable_float_overflow_check=_options.get_bool_option("float-overflow-check"); enable_simplify=_options.get_bool_option("simplify"); @@ -103,6 +104,7 @@ class goto_checkt bool enable_div_by_zero_check; bool enable_signed_overflow_check; bool enable_unsigned_overflow_check; + bool enable_pointer_overflow_check; bool enable_undefined_shift_check; bool enable_float_overflow_check; bool enable_simplify; @@ -899,7 +901,7 @@ void goto_checkt::pointer_overflow_check( const exprt &expr, const guardt &guard) { - if(!enable_pointer_check) + if(!enable_pointer_overflow_check) return; if(expr.id()==ID_plus || diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 5d92c83c9bb..b5adb72997f 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -32,7 +32,7 @@ void goto_check( #define GOTO_CHECK_OPTIONS \ "(bounds-check)(pointer-check)(memory-leak-check)" \ "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \ - "(undefined-shift-check)" \ + "(pointer-overflow-check)(undefined-shift-check)" \ "(float-overflow-check)(nan-check)" #define GOTO_CHECK_HELP \ @@ -42,6 +42,7 @@ void goto_check( " --div-by-zero-check enable division by zero checks\n" \ " --signed-overflow-check enable signed arithmetic over- and underflow checks\n" \ " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" \ + " --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" \ " --undefined-shift-check check shift greater than bit-width\n" \ " --float-overflow-check check floating-point for +/-Inf\n" \ " --nan-check check floating-point for NaN\n" \ @@ -53,6 +54,7 @@ void goto_check( options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \ options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \ options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \ + options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \ options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \ options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \ options.set_option("nan-check", cmdline.isset("nan-check")) From 8a164ad5bde4bff4592a7869cfb9cc871399e3d3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 00:46:10 +0000 Subject: [PATCH 5/5] Decouple type conversion checks from arithmetic overflow Type conversion has implementation-defined semantics, whereas integer overflow is undefined behavior in C. Thus one my want to check only the latter, in particular in SV-COMP. Fixes #307 --- src/analyses/goto_check.cpp | 58 ++++++++++++++++++++++++++++--------- src/analyses/goto_check.h | 4 ++- 2 files changed, 47 insertions(+), 15 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 1fb83d4b6c1..0bc3a1c7826 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -41,6 +41,7 @@ class goto_checkt enable_signed_overflow_check=_options.get_bool_option("signed-overflow-check"); enable_unsigned_overflow_check=_options.get_bool_option("unsigned-overflow-check"); enable_pointer_overflow_check=_options.get_bool_option("pointer-overflow-check"); + enable_conversion_check=_options.get_bool_option("conversion-check"); enable_undefined_shift_check=_options.get_bool_option("undefined-shift-check"); enable_float_overflow_check=_options.get_bool_option("float-overflow-check"); enable_simplify=_options.get_bool_option("simplify"); @@ -74,6 +75,7 @@ class goto_checkt void pointer_overflow_check(const exprt &expr, const guardt &guard); void pointer_validity_check(const dereference_exprt &expr, const guardt &guard); void integer_overflow_check(const exprt &expr, const guardt &guard); + void conversion_check(const exprt &expr, const guardt &guard); void float_overflow_check(const exprt &expr, const guardt &guard); void nan_check(const exprt &expr, const guardt &guard); @@ -105,6 +107,7 @@ class goto_checkt bool enable_signed_overflow_check; bool enable_unsigned_overflow_check; bool enable_pointer_overflow_check; + bool enable_conversion_check; bool enable_undefined_shift_check; bool enable_float_overflow_check; bool enable_simplify; @@ -305,7 +308,7 @@ void goto_checkt::mod_by_zero_check( /*******************************************************************\ -Function: goto_checkt::integer_overflow_check +Function: goto_checkt::conversion_check Inputs: @@ -315,25 +318,20 @@ Function: goto_checkt::integer_overflow_check \*******************************************************************/ -void goto_checkt::integer_overflow_check( +void goto_checkt::conversion_check( const exprt &expr, const guardt &guard) { - if(!enable_signed_overflow_check && - !enable_unsigned_overflow_check) + if(!enable_conversion_check) return; // First, check type. const typet &type=ns.follow(expr.type()); - if(type.id()==ID_signedbv && !enable_signed_overflow_check) - return; - - if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check) + if(type.id()!=ID_signedbv && + type.id()!=ID_unsignedbv) return; - // add overflow subgoal - if(expr.id()==ID_typecast) { // conversion to signed int may overflow @@ -493,10 +491,41 @@ void goto_checkt::integer_overflow_check( guard); } } + } +} +/*******************************************************************\ + +Function: goto_checkt::integer_overflow_check + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_checkt::integer_overflow_check( + const exprt &expr, + const guardt &guard) +{ + if(!enable_signed_overflow_check && + !enable_unsigned_overflow_check) return; - } - else if(expr.id()==ID_div) + + // First, check type. + const typet &type=ns.follow(expr.type()); + + if(type.id()==ID_signedbv && !enable_signed_overflow_check) + return; + + if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check) + return; + + // add overflow subgoal + + if(expr.id()==ID_div) { assert(expr.operands().size()==2); @@ -1432,8 +1461,7 @@ void goto_checkt::check_rec( } else if(expr.id()==ID_plus || expr.id()==ID_minus || expr.id()==ID_mult || - expr.id()==ID_unary_minus || - expr.id()==ID_typecast) + expr.id()==ID_unary_minus) { if(expr.type().id()==ID_signedbv || expr.type().id()==ID_unsignedbv) @@ -1454,6 +1482,8 @@ void goto_checkt::check_rec( pointer_overflow_check(expr, guard); } } + else if(expr.id()==ID_typecast) + conversion_check(expr, guard); else if(expr.id()==ID_le || expr.id()==ID_lt || expr.id()==ID_ge || expr.id()==ID_gt) pointer_rel_check(expr, guard); diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index b5adb72997f..8aaddcc3e68 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -32,7 +32,7 @@ void goto_check( #define GOTO_CHECK_OPTIONS \ "(bounds-check)(pointer-check)(memory-leak-check)" \ "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \ - "(pointer-overflow-check)(undefined-shift-check)" \ + "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ "(float-overflow-check)(nan-check)" #define GOTO_CHECK_HELP \ @@ -43,6 +43,7 @@ void goto_check( " --signed-overflow-check enable signed arithmetic over- and underflow checks\n" \ " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" \ " --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" \ + " --conversion-check check whether values can be represented after type cast\n" \ " --undefined-shift-check check shift greater than bit-width\n" \ " --float-overflow-check check floating-point for +/-Inf\n" \ " --nan-check check floating-point for NaN\n" \ @@ -55,6 +56,7 @@ void goto_check( options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \ options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \ options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \ + options.set_option("conversion-check", cmdline.isset("conversion-check")); \ options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \ options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \ options.set_option("nan-check", cmdline.isset("nan-check"))