diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 03585fe582f..032b18ec3d4 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -93,10 +93,6 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options) else options.set_option("assumptions", true); - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); - // Select a specific analysis if(cmdline.isset("taint")) { @@ -791,7 +787,8 @@ void janalyzer_parse_optionst::help() HELP_SHOW_PROPERTIES "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK_JAVA + " --no-assertions ignore user assertions\n" + " --no-assumptions ignore user assumptions\n" "\n" "Other options:\n" " --version show version and exit\n" diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index 15c0530668b..8aebc6174ed 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -108,11 +108,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include class abstract_goto_modelt; class ai_baset; +class goto_functiont; class goto_model_functiont; class optionst; @@ -127,7 +127,7 @@ class optionst; "(little-endian)(big-endian)" \ OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \ - OPT_GOTO_CHECK_JAVA \ + "(no-assertions)(no-assumptions)" \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)" \ "(show-reachable-properties)(property):" \ diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index c5a4fdf8623..3dd396bf345 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -9,7 +9,6 @@ SRC = assignments_from_json.cpp \ expr2java.cpp \ generic_parameter_specialization_map.cpp \ generic_parameter_specialization_map_keys.cpp \ - goto_check_java.cpp \ jar_file.cpp \ jar_pool.cpp \ java_bmc_util.cpp \ diff --git a/jbmc/src/java_bytecode/goto_check_java.cpp b/jbmc/src/java_bytecode/goto_check_java.cpp deleted file mode 100644 index ebc9a56ace0..00000000000 --- a/jbmc/src/java_bytecode/goto_check_java.cpp +++ /dev/null @@ -1,1639 +0,0 @@ -/*******************************************************************\ - -Module: Checks for Errors in Java Programs - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Checks for Errors in Java Programs - -#include "goto_check_java.h" - -#include - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include -#include - -#include -#include - -#include - -class goto_check_javat -{ -public: - goto_check_javat( - const namespacet &_ns, - const optionst &_options, - message_handlert &_message_handler) - : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler) - { - enable_bounds_check = _options.get_bool_option("bounds-check"); - enable_pointer_check = _options.get_bool_option("pointer-check"); - 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_conversion_check = _options.get_bool_option("conversion-check"); - enable_float_overflow_check = - _options.get_bool_option("float-overflow-check"); - enable_simplify = _options.get_bool_option("simplify"); - enable_nan_check = _options.get_bool_option("nan-check"); - retain_trivial = _options.get_bool_option("retain-trivial-checks"); - enable_assert_to_assume = _options.get_bool_option("assert-to-assume"); - enable_assertions = _options.get_bool_option("assertions"); - enable_built_in_assertions = - _options.get_bool_option("built-in-assertions"); - enable_assumptions = _options.get_bool_option("assumptions"); - error_labels = _options.get_list_option("error-label"); - } - - typedef goto_functionst::goto_functiont goto_functiont; - - void goto_check( - const irep_idt &function_identifier, - goto_functiont &goto_function); - -protected: - const namespacet &ns; - std::unique_ptr local_bitvector_analysis; - goto_programt::const_targett current_target; - messaget log; - - /// Check an address-of expression: - /// if it is a dereference then check the pointer - /// if it is an index then address-check the array and then check the index - /// \param expr: the expression to be checked - void check_rec_address(const exprt &expr); - - /// Check that a member expression is valid: - /// - check the structure this expression is a member of (via pointer of its - /// dereference) - /// - run pointer-validity check on `*(s+member_offset)' instead of - /// `s->member' to avoid checking safety of `s' - /// - check all operands of the expression - /// \param member: the expression to be checked - /// \return true if no more checks are required for \p member or its - /// sub-expressions - bool check_rec_member(const member_exprt &member); - - /// Check that a division is valid: check for division by zero, overflow and - /// NaN (for floating point numbers). - /// \param div_expr: the expression to be checked - void check_rec_div(const div_exprt &div_expr); - - /// Check that an arithmetic operation is valid: overflow check, NaN-check - /// (for floating point numbers), and pointer overflow check. - /// \param expr: the expression to be checked - void check_rec_arithmetic_op(const exprt &expr); - - /// Recursively descend into \p expr and run the appropriate check for each - /// sub-expression, while collecting the condition for the check in \p - /// guard. - /// \param expr: the expression to be checked - void check_rec(const exprt &expr); - - /// Initiate the recursively analysis of \p expr with its `guard' set to TRUE. - /// \param expr: the expression to be checked - void check(const exprt &expr); - - struct conditiont - { - conditiont(const exprt &_assertion, const std::string &_description) - : assertion(_assertion), description(_description) - { - } - - exprt assertion; - std::string description; - }; - - using conditionst = std::list; - - void bounds_check(const exprt &); - void bounds_check_index(const index_exprt &); - void div_by_zero_check(const div_exprt &); - void mod_overflow_check(const mod_exprt &); - - /// Generates VCCs for the validity of the given dereferencing operation. - /// \param expr the expression to be checked - /// \param src_expr The expression as found in the program, - /// prior to any rewriting - void - pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr); - - optionalt - get_pointer_is_null_condition(const exprt &address, const exprt &size); - - conditionst get_pointer_dereferenceable_conditions( - const exprt &address, - const exprt &size); - void integer_overflow_check(const exprt &); - void conversion_check(const exprt &); - void float_overflow_check(const exprt &); - void nan_check(const exprt &); - optionalt rw_ok_check(exprt); - - std::string array_name(const exprt &); - - /// Include the \p asserted_expr in the code conditioned by the \p guard. - /// \param asserted_expr: expression to be asserted - /// \param comment: human readable comment - /// \param property_class: classification of the property - /// \param source_location: the source location of the original expression - /// \param src_expr: the original expression to be included in the comment - void add_property( - const exprt &asserted_expr, - const std::string &comment, - const std::string &property_class, - const source_locationt &source_location, - const exprt &src_expr); - - goto_programt new_code; - typedef std::set> assertionst; - assertionst assertions; - - /// Remove all assertions containing the symbol in \p lhs as well as all - /// assertions containing dereference. - /// \param lhs: the left-hand-side expression whose symbol should be - /// invalidated - void invalidate(const exprt &lhs); - - bool enable_bounds_check; - bool enable_pointer_check; - bool enable_div_by_zero_check; - bool enable_signed_overflow_check; - bool enable_unsigned_overflow_check; - bool enable_pointer_overflow_check; - bool enable_conversion_check; - bool enable_float_overflow_check; - bool enable_simplify; - bool enable_nan_check; - bool retain_trivial; - bool enable_assert_to_assume; - bool enable_assertions; - bool enable_built_in_assertions; - bool enable_assumptions; - - typedef optionst::value_listt error_labelst; - error_labelst error_labels; -}; - -void goto_check_javat::invalidate(const exprt &lhs) -{ - if(lhs.id() == ID_index) - invalidate(to_index_expr(lhs).array()); - else if(lhs.id() == ID_member) - invalidate(to_member_expr(lhs).struct_op()); - else if(lhs.id() == ID_symbol) - { - // clear all assertions about 'symbol' - find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()}; - - for(auto it = assertions.begin(); it != assertions.end();) - { - if( - has_symbol(it->second, find_symbols_set) || - has_subexpr(it->second, ID_dereference)) - { - it = assertions.erase(it); - } - else - ++it; - } - } - else - { - // give up, clear all - assertions.clear(); - } -} - -void goto_check_javat::div_by_zero_check(const div_exprt &expr) -{ - if(!enable_div_by_zero_check) - return; - - // add divison by zero subgoal - - exprt zero = from_integer(0, expr.op1().type()); - const notequal_exprt inequality(expr.op1(), std::move(zero)); - - add_property( - inequality, - "division by zero", - "division-by-zero", - expr.find_source_location(), - expr); -} - -/// check a mod expression for the case INT_MIN % -1 -void goto_check_javat::mod_overflow_check(const mod_exprt &expr) -{ - if(!enable_signed_overflow_check) - return; - - const auto &type = expr.type(); - - if(type.id() == ID_signedbv) - { - // INT_MIN % -1 is, in principle, defined to be zero in - // ANSI C, C99, C++98, and C++11. Most compilers, however, - // fail to produce 0, and in some cases generate an exception. - // C11 explicitly makes this case undefined. - - notequal_exprt int_min_neq( - expr.op0(), to_signedbv_type(type).smallest_expr()); - - notequal_exprt minus_one_neq( - expr.op1(), from_integer(-1, expr.op1().type())); - - add_property( - or_exprt(int_min_neq, minus_one_neq), - "result of signed mod is not representable", - "overflow", - expr.find_source_location(), - expr); - } -} - -void goto_check_javat::conversion_check(const exprt &expr) -{ - if(!enable_conversion_check) - return; - - // First, check type. - const typet &type = expr.type(); - - if(type.id() != ID_signedbv && type.id() != ID_unsignedbv) - return; - - if(expr.id() == ID_typecast) - { - const auto &op = to_typecast_expr(expr).op(); - - // conversion to signed int may overflow - const typet &old_type = op.type(); - - if(type.id() == ID_signedbv) - { - std::size_t new_width = to_signedbv_type(type).get_width(); - - if(old_type.id() == ID_signedbv) // signed -> signed - { - std::size_t old_width = to_signedbv_type(old_type).get_width(); - if(new_width >= old_width) - return; // always ok - - const binary_relation_exprt no_overflow_upper( - op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type)); - - const binary_relation_exprt no_overflow_lower( - op, ID_ge, from_integer(-power(2, new_width - 1), old_type)); - - add_property( - and_exprt(no_overflow_lower, no_overflow_upper), - "arithmetic overflow on signed type conversion", - "overflow", - expr.find_source_location(), - expr); - } - else if(old_type.id() == ID_unsignedbv) // unsigned -> signed - { - std::size_t old_width = to_unsignedbv_type(old_type).get_width(); - if(new_width >= old_width + 1) - return; // always ok - - const binary_relation_exprt no_overflow_upper( - op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type)); - - add_property( - no_overflow_upper, - "arithmetic overflow on unsigned to signed type conversion", - "overflow", - expr.find_source_location(), - expr); - } - else if(old_type.id() == ID_floatbv) // float -> signed - { - // Note that the fractional part is truncated! - ieee_floatt upper(to_floatbv_type(old_type)); - upper.from_integer(power(2, new_width - 1)); - const binary_relation_exprt no_overflow_upper( - op, ID_lt, upper.to_expr()); - - ieee_floatt lower(to_floatbv_type(old_type)); - lower.from_integer(-power(2, new_width - 1) - 1); - const binary_relation_exprt no_overflow_lower( - op, ID_gt, lower.to_expr()); - - add_property( - and_exprt(no_overflow_lower, no_overflow_upper), - "arithmetic overflow on float to signed integer type conversion", - "overflow", - expr.find_source_location(), - expr); - } - } - else if(type.id() == ID_unsignedbv) - { - std::size_t new_width = to_unsignedbv_type(type).get_width(); - - if(old_type.id() == ID_signedbv) // signed -> unsigned - { - std::size_t old_width = to_signedbv_type(old_type).get_width(); - - if(new_width >= old_width - 1) - { - // only need lower bound check - const binary_relation_exprt no_overflow_lower( - op, ID_ge, from_integer(0, old_type)); - - add_property( - no_overflow_lower, - "arithmetic overflow on signed to unsigned type conversion", - "overflow", - expr.find_source_location(), - expr); - } - else - { - // need both - const binary_relation_exprt no_overflow_upper( - op, ID_le, from_integer(power(2, new_width) - 1, old_type)); - - const binary_relation_exprt no_overflow_lower( - op, ID_ge, from_integer(0, old_type)); - - add_property( - and_exprt(no_overflow_lower, no_overflow_upper), - "arithmetic overflow on signed to unsigned type conversion", - "overflow", - expr.find_source_location(), - expr); - } - } - else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned - { - std::size_t old_width = to_unsignedbv_type(old_type).get_width(); - if(new_width >= old_width) - return; // always ok - - const binary_relation_exprt no_overflow_upper( - op, ID_le, from_integer(power(2, new_width) - 1, old_type)); - - add_property( - no_overflow_upper, - "arithmetic overflow on unsigned to unsigned type conversion", - "overflow", - expr.find_source_location(), - expr); - } - else if(old_type.id() == ID_floatbv) // float -> unsigned - { - // Note that the fractional part is truncated! - ieee_floatt upper(to_floatbv_type(old_type)); - upper.from_integer(power(2, new_width) - 1); - const binary_relation_exprt no_overflow_upper( - op, ID_lt, upper.to_expr()); - - ieee_floatt lower(to_floatbv_type(old_type)); - lower.from_integer(-1); - const binary_relation_exprt no_overflow_lower( - op, ID_gt, lower.to_expr()); - - add_property( - and_exprt(no_overflow_lower, no_overflow_upper), - "arithmetic overflow on float to unsigned integer type conversion", - "overflow", - expr.find_source_location(), - expr); - } - } - } -} - -void goto_check_javat::integer_overflow_check(const exprt &expr) -{ - if(!enable_signed_overflow_check && !enable_unsigned_overflow_check) - return; - - // First, check type. - const typet &type = 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) - { - // undefined for signed division INT_MIN/-1 - if(type.id() == ID_signedbv) - { - const auto &div_expr = to_div_expr(expr); - - equal_exprt int_min_eq( - div_expr.dividend(), to_signedbv_type(type).smallest_expr()); - - equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type)); - - add_property( - not_exprt(and_exprt(int_min_eq, minus_one_eq)), - "arithmetic overflow on signed division", - "overflow", - expr.find_source_location(), - expr); - } - - return; - } - else if(expr.id() == ID_unary_minus) - { - if(type.id() == ID_signedbv) - { - // overflow on unary- on signed integers can only happen with the - // smallest representable number 100....0 - - equal_exprt int_min_eq( - to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr()); - - add_property( - not_exprt(int_min_eq), - "arithmetic overflow on signed unary minus", - "overflow", - expr.find_source_location(), - expr); - } - else if(type.id() == ID_unsignedbv) - { - // Overflow on unary- on unsigned integers happens for all operands - // that are not zero. - - notequal_exprt not_eq_zero( - to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr()); - - add_property( - not_eq_zero, - "arithmetic overflow on unsigned unary minus", - "overflow", - expr.find_source_location(), - expr); - } - - return; - } - else if(expr.id() == ID_shl) - { - if(type.id() == ID_signedbv) - { - const auto &shl_expr = to_shl_expr(expr); - const auto &op = shl_expr.op(); - const auto &op_type = to_signedbv_type(type); - const auto op_width = op_type.get_width(); - const auto &distance = shl_expr.distance(); - const auto &distance_type = distance.type(); - - // a left shift of a negative value is undefined; - // yet this isn't an overflow - exprt neg_value_shift; - - if(op_type.id() == ID_unsignedbv) - neg_value_shift = false_exprt(); - else - neg_value_shift = - binary_relation_exprt(op, ID_lt, from_integer(0, op_type)); - - // a shift with negative distance is undefined; - // yet this isn't an overflow - exprt neg_dist_shift; - - if(distance_type.id() == ID_unsignedbv) - neg_dist_shift = false_exprt(); - else - { - neg_dist_shift = binary_relation_exprt( - distance, ID_lt, from_integer(0, distance_type)); - } - - // shifting a non-zero value by more than its width is undefined; - // yet this isn't an overflow - const exprt dist_too_large = binary_predicate_exprt( - distance, ID_gt, from_integer(op_width, distance_type)); - - const exprt op_zero = equal_exprt(op, from_integer(0, op_type)); - - auto new_type = to_bitvector_type(op_type); - new_type.set_width(op_width * 2); - - const exprt op_ext = typecast_exprt(op, new_type); - - const exprt op_ext_shifted = shl_exprt(op_ext, distance); - - // The semantics of signed left shifts are contentious for the case - // that a '1' is shifted into the signed bit. - // Assuming 32-bit integers, 1<<31 is implementation-defined - // in ANSI C and C++98, but is explicitly undefined by C99, - // C11 and C++11. - bool allow_shift_into_sign_bit = true; - - const unsigned number_of_top_bits = - allow_shift_into_sign_bit ? op_width : op_width + 1; - - const exprt top_bits = extractbits_exprt( - op_ext_shifted, - new_type.get_width() - 1, - new_type.get_width() - number_of_top_bits, - unsignedbv_typet(number_of_top_bits)); - - const exprt top_bits_zero = - equal_exprt(top_bits, from_integer(0, top_bits.type())); - - // a negative distance shift isn't an overflow; - // a negative value shift isn't an overflow; - // a shift that's too far isn't an overflow; - // a shift of zero isn't overflow; - // else check the top bits - add_property( - disjunction({neg_value_shift, - neg_dist_shift, - dist_too_large, - op_zero, - top_bits_zero}), - "arithmetic overflow on signed shl", - "overflow", - expr.find_source_location(), - expr); - } - - return; - } - - multi_ary_exprt overflow( - "overflow-" + expr.id_string(), expr.operands(), bool_typet()); - - if(expr.operands().size() >= 3) - { - // The overflow checks are binary! - // We break these up. - - for(std::size_t i = 1; i < expr.operands().size(); i++) - { - exprt tmp; - - if(i == 1) - tmp = to_multi_ary_expr(expr).op0(); - else - { - tmp = expr; - tmp.operands().resize(i); - } - - std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed"; - - add_property( - not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}}, - "arithmetic overflow on " + kind + " " + expr.id_string(), - "overflow", - expr.find_source_location(), - expr); - } - } - else if(expr.operands().size() == 2) - { - std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed"; - - const binary_exprt &bexpr = to_binary_expr(expr); - add_property( - not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}}, - "arithmetic overflow on " + kind + " " + expr.id_string(), - "overflow", - expr.find_source_location(), - expr); - } - else - { - PRECONDITION(expr.id() == ID_unary_minus); - - std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed"; - - add_property( - not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}}, - "arithmetic overflow on " + kind + " " + expr.id_string(), - "overflow", - expr.find_source_location(), - expr); - } -} - -void goto_check_javat::float_overflow_check(const exprt &expr) -{ - if(!enable_float_overflow_check) - return; - - // First, check type. - const typet &type = expr.type(); - - if(type.id() != ID_floatbv) - return; - - // add overflow subgoal - - if(expr.id() == ID_typecast) - { - // Can overflow if casting from larger - // to smaller type. - const auto &op = to_typecast_expr(expr).op(); - if(op.type().id() == ID_floatbv) - { - // float-to-float - or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))}; - - add_property( - std::move(overflow_check), - "arithmetic overflow on floating-point typecast", - "overflow", - expr.find_source_location(), - expr); - } - else - { - // non-float-to-float - add_property( - not_exprt(isinf_exprt(expr)), - "arithmetic overflow on floating-point typecast", - "overflow", - expr.find_source_location(), - expr); - } - - return; - } - else if(expr.id() == ID_div) - { - // Can overflow if dividing by something small - or_exprt overflow_check( - isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr))); - - add_property( - std::move(overflow_check), - "arithmetic overflow on floating-point division", - "overflow", - expr.find_source_location(), - expr); - - return; - } - else if(expr.id() == ID_mod) - { - // Can't overflow - return; - } - else if(expr.id() == ID_unary_minus) - { - // Can't overflow - return; - } - else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus) - { - if(expr.operands().size() == 2) - { - // Can overflow - or_exprt overflow_check( - isinf_exprt(to_binary_expr(expr).op0()), - isinf_exprt(to_binary_expr(expr).op1()), - not_exprt(isinf_exprt(expr))); - - std::string kind = expr.id() == ID_plus - ? "addition" - : expr.id() == ID_minus - ? "subtraction" - : expr.id() == ID_mult ? "multiplication" : ""; - - add_property( - std::move(overflow_check), - "arithmetic overflow on floating-point " + kind, - "overflow", - expr.find_source_location(), - expr); - - return; - } - else if(expr.operands().size() >= 3) - { - DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary"); - - // break up - float_overflow_check(make_binary(expr)); - return; - } - } -} - -void goto_check_javat::nan_check(const exprt &expr) -{ - if(!enable_nan_check) - return; - - // first, check type - if(expr.type().id() != ID_floatbv) - return; - - if( - expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div && - expr.id() != ID_minus) - return; - - // add NaN subgoal - - exprt isnan; - - if(expr.id() == ID_div) - { - const auto &div_expr = to_div_expr(expr); - - // there a two ways to get a new NaN on division: - // 0/0 = NaN and x/inf = NaN - // (note that x/0 = +-inf for x!=0 and x!=inf) - const and_exprt zero_div_zero( - ieee_float_equal_exprt( - div_expr.op0(), from_integer(0, div_expr.dividend().type())), - ieee_float_equal_exprt( - div_expr.op1(), from_integer(0, div_expr.divisor().type()))); - - const isinf_exprt div_inf(div_expr.op1()); - - isnan = or_exprt(zero_div_zero, div_inf); - } - else if(expr.id() == ID_mult) - { - if(expr.operands().size() >= 3) - return nan_check(make_binary(expr)); - - const auto &mult_expr = to_mult_expr(expr); - - // Inf * 0 is NaN - const and_exprt inf_times_zero( - isinf_exprt(mult_expr.op0()), - ieee_float_equal_exprt( - mult_expr.op1(), from_integer(0, mult_expr.op1().type()))); - - const and_exprt zero_times_inf( - ieee_float_equal_exprt( - mult_expr.op1(), from_integer(0, mult_expr.op1().type())), - isinf_exprt(mult_expr.op0())); - - isnan = or_exprt(inf_times_zero, zero_times_inf); - } - else if(expr.id() == ID_plus) - { - if(expr.operands().size() >= 3) - return nan_check(make_binary(expr)); - - const auto &plus_expr = to_plus_expr(expr); - - // -inf + +inf = NaN and +inf + -inf = NaN, - // i.e., signs differ - ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type())); - exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr(); - exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr(); - - isnan = or_exprt( - and_exprt( - equal_exprt(plus_expr.op0(), minus_inf), - equal_exprt(plus_expr.op1(), plus_inf)), - and_exprt( - equal_exprt(plus_expr.op0(), plus_inf), - equal_exprt(plus_expr.op1(), minus_inf))); - } - else if(expr.id() == ID_minus) - { - // +inf - +inf = NaN and -inf - -inf = NaN, - // i.e., signs match - - const auto &minus_expr = to_minus_expr(expr); - - ieee_float_spect spec = - ieee_float_spect(to_floatbv_type(minus_expr.type())); - exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr(); - exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr(); - - isnan = or_exprt( - and_exprt( - equal_exprt(minus_expr.lhs(), plus_inf), - equal_exprt(minus_expr.rhs(), plus_inf)), - and_exprt( - equal_exprt(minus_expr.lhs(), minus_inf), - equal_exprt(minus_expr.rhs(), minus_inf))); - } - else - UNREACHABLE; - - add_property( - boolean_negate(isnan), - "NaN on " + expr.id_string(), - "NaN", - expr.find_source_location(), - expr); -} - -void goto_check_javat::pointer_validity_check( - const dereference_exprt &expr, - const exprt &src_expr) -{ - if(!enable_pointer_check) - return; - - const exprt &pointer = expr.pointer(); - - exprt size; - - if(expr.type().id() == ID_empty) - { - // a dereference *p (with p being a pointer to void) is valid if p points to - // valid memory (of any size). the smallest possible size of the memory - // segment p could be pointing to is 1, hence we use this size for the - // address check - size = from_integer(1, size_type()); - } - else - { - auto size_of_expr_opt = size_of_expr(expr.type(), ns); - CHECK_RETURN(size_of_expr_opt.has_value()); - size = size_of_expr_opt.value(); - } - - auto conditions = get_pointer_dereferenceable_conditions(pointer, size); - - for(const auto &c : conditions) - { - add_property( - c.assertion, - "dereference failure: " + c.description, - "pointer dereference", - src_expr.find_source_location(), - src_expr); - } -} - -goto_check_javat::conditionst -goto_check_javat::get_pointer_dereferenceable_conditions( - const exprt &address, - const exprt &size) -{ - auto maybe_null_condition = get_pointer_is_null_condition(address, size); - - if(maybe_null_condition.has_value()) - return {*maybe_null_condition}; - else - return {}; -} - -std::string goto_check_javat::array_name(const exprt &expr) -{ - return ::array_name(ns, expr); -} - -void goto_check_javat::bounds_check(const exprt &expr) -{ - if(!enable_bounds_check) - return; - - if( - expr.find(ID_C_bounds_check).is_not_nil() && - !expr.get_bool(ID_C_bounds_check)) - { - return; - } - - if(expr.id() == ID_index) - bounds_check_index(to_index_expr(expr)); -} - -void goto_check_javat::bounds_check_index(const index_exprt &expr) -{ - const typet &array_type = expr.array().type(); - - if(array_type.id() == ID_pointer) - throw "index got pointer as array type"; - else if(array_type.id() != ID_array && array_type.id() != ID_vector) - throw "bounds check expected array or vector type, got " + - array_type.id_string(); - - std::string name = array_name(expr.array()); - - const exprt &index = expr.index(); - object_descriptor_exprt ode; - ode.build(expr, ns); - - if(index.type().id() != ID_unsignedbv) - { - // we undo typecasts to signedbv - if( - index.id() == ID_typecast && - to_typecast_expr(index).op().type().id() == ID_unsignedbv) - { - // ok - } - else - { - const auto i = numeric_cast(index); - - if(!i.has_value() || *i < 0) - { - exprt effective_offset = ode.offset(); - - if(ode.root_object().id() == ID_dereference) - { - exprt p_offset = - pointer_offset(to_dereference_expr(ode.root_object()).pointer()); - - effective_offset = plus_exprt{p_offset, - typecast_exprt::conditional_cast( - effective_offset, p_offset.type())}; - } - - exprt zero = from_integer(0, ode.offset().type()); - - // the final offset must not be negative - binary_relation_exprt inequality( - effective_offset, ID_ge, std::move(zero)); - - add_property( - inequality, - name + " lower bound", - "array bounds", - expr.find_source_location(), - expr); - } - } - } - - if(ode.root_object().id() == ID_dereference) - { - const exprt &pointer = to_dereference_expr(ode.root_object()).pointer(); - - const plus_exprt effective_offset{ - ode.offset(), - typecast_exprt::conditional_cast( - pointer_offset(pointer), ode.offset().type())}; - - binary_relation_exprt inequality{ - effective_offset, - ID_lt, - typecast_exprt::conditional_cast( - object_size(pointer), effective_offset.type())}; - - add_property( - inequality, - name + " dynamic object upper bound", - "array bounds", - expr.find_source_location(), - expr); - - return; - } - - const exprt &size = array_type.id() == ID_array - ? to_array_type(array_type).size() - : to_vector_type(array_type).size(); - - if(size.is_nil()) - { - // Linking didn't complete, we don't have a size. - // Not clear what to do. - } - else if(size.id() == ID_infinity) - { - } - else if(size.is_zero() && expr.array().id() == ID_member) - { - // a variable sized struct member - // - // Excerpt from the C standard on flexible array members: - // However, when a . (or ->) operator has a left operand that is (a pointer - // to) a structure with a flexible array member and the right operand names - // that member, it behaves as if that member were replaced with the longest - // array (with the same element type) that would not make the structure - // larger than the object being accessed; [...] - const auto type_size_opt = size_of_expr(ode.root_object().type(), ns); - CHECK_RETURN(type_size_opt.has_value()); - - binary_relation_exprt inequality( - typecast_exprt::conditional_cast( - ode.offset(), type_size_opt.value().type()), - ID_lt, - type_size_opt.value()); - - add_property( - inequality, - name + " upper bound", - "array bounds", - expr.find_source_location(), - expr); - } - else - { - binary_relation_exprt inequality{ - typecast_exprt::conditional_cast(index, size.type()), ID_lt, size}; - - add_property( - inequality, - name + " upper bound", - "array bounds", - expr.find_source_location(), - expr); - } -} - -void goto_check_javat::add_property( - const exprt &asserted_expr, - const std::string &comment, - const std::string &property_class, - const source_locationt &source_location, - const exprt &src_expr) -{ - // first try simplifier on it - exprt simplified_expr = - enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr; - - // throw away trivial properties? - if(!retain_trivial && simplified_expr.is_true()) - return; - - if(assertions.insert(std::make_pair(src_expr, simplified_expr)).second) - { - auto t = new_code.add( - enable_assert_to_assume ? goto_programt::make_assumption( - std::move(simplified_expr), source_location) - : goto_programt::make_assertion( - std::move(simplified_expr), source_location)); - - std::string source_expr_string; - get_language_from_mode(ID_java)->from_expr( - src_expr, source_expr_string, ns); - - t->source_location_nonconst().set_comment( - comment + " in " + source_expr_string); - t->source_location_nonconst().set_property_class(property_class); - } -} - -void goto_check_javat::check_rec_address(const exprt &expr) -{ - // we don't look into quantifiers - if(expr.id() == ID_exists || expr.id() == ID_forall) - return; - - if(expr.id() == ID_dereference) - { - check_rec(to_dereference_expr(expr).pointer()); - } - else if(expr.id() == ID_index) - { - const index_exprt &index_expr = to_index_expr(expr); - check_rec_address(index_expr.array()); - check_rec(index_expr.index()); - } - else - { - for(const auto &operand : expr.operands()) - check_rec_address(operand); - } -} - -bool goto_check_javat::check_rec_member(const member_exprt &member) -{ - const dereference_exprt &deref = to_dereference_expr(member.struct_op()); - - check_rec(deref.pointer()); - - // avoid building the following expressions when pointer_validity_check - // would return immediately anyway - if(!enable_pointer_check) - return true; - - // we rewrite s->member into *(s+member_offset) - // to avoid requiring memory safety of the entire struct - auto member_offset_opt = member_offset_expr(member, ns); - - if(member_offset_opt.has_value()) - { - pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type()); - new_pointer_type.base_type() = member.type(); - - const exprt char_pointer = typecast_exprt::conditional_cast( - deref.pointer(), pointer_type(char_type())); - - const exprt new_address_casted = typecast_exprt::conditional_cast( - plus_exprt{char_pointer, - typecast_exprt::conditional_cast( - member_offset_opt.value(), pointer_diff_type())}, - new_pointer_type); - - dereference_exprt new_deref{new_address_casted}; - new_deref.add_source_location() = deref.source_location(); - pointer_validity_check(new_deref, member); - - return true; - } - return false; -} - -void goto_check_javat::check_rec_div(const div_exprt &div_expr) -{ - div_by_zero_check(to_div_expr(div_expr)); - - if(div_expr.type().id() == ID_signedbv) - integer_overflow_check(div_expr); - else if(div_expr.type().id() == ID_floatbv) - { - nan_check(div_expr); - float_overflow_check(div_expr); - } -} - -void goto_check_javat::check_rec_arithmetic_op(const exprt &expr) -{ - if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv) - { - integer_overflow_check(expr); - } - else if(expr.type().id() == ID_floatbv) - { - nan_check(expr); - float_overflow_check(expr); - } -} - -void goto_check_javat::check_rec(const exprt &expr) -{ - // we don't look into quantifiers - if(expr.id() == ID_exists || expr.id() == ID_forall) - return; - - if(expr.id() == ID_address_of) - { - check_rec_address(to_address_of_expr(expr).object()); - return; - } - else if( - expr.id() == ID_member && - to_member_expr(expr).struct_op().id() == ID_dereference) - { - if(check_rec_member(to_member_expr(expr))) - return; - } - - forall_operands(it, expr) - check_rec(*it); - - if(expr.id() == ID_index) - { - bounds_check(expr); - } - else if(expr.id() == ID_div) - { - check_rec_div(to_div_expr(expr)); - } - else if(expr.id() == ID_shl) - { - if(expr.type().id() == ID_signedbv) - integer_overflow_check(expr); - } - else if(expr.id() == ID_mod) - { - mod_overflow_check(to_mod_expr(expr)); - } - else if( - expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || - expr.id() == ID_unary_minus) - { - check_rec_arithmetic_op(expr); - } - else if(expr.id() == ID_typecast) - conversion_check(expr); - else if(expr.id() == ID_dereference) - { - pointer_validity_check(to_dereference_expr(expr), expr); - } -} - -void goto_check_javat::check(const exprt &expr) -{ - check_rec(expr); -} - -/// expand the r_ok, w_ok and rw_ok predicates -optionalt goto_check_javat::rw_ok_check(exprt expr) -{ - bool modified = false; - - for(auto &op : expr.operands()) - { - auto op_result = rw_ok_check(op); - if(op_result.has_value()) - { - op = *op_result; - modified = true; - } - } - - if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok) - { - // these get an address as first argument and a size as second - DATA_INVARIANT( - expr.operands().size() == 2, "r/w_ok must have two operands"); - - const auto conditions = get_pointer_dereferenceable_conditions( - to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size()); - - exprt::operandst conjuncts; - - for(const auto &c : conditions) - conjuncts.push_back(c.assertion); - - return conjunction(conjuncts); - } - else if(modified) - return std::move(expr); - else - return {}; -} - -void goto_check_javat::goto_check( - const irep_idt &function_identifier, - goto_functiont &goto_function) -{ - const auto &function_symbol = ns.lookup(function_identifier); - - if(function_symbol.mode != ID_java) - return; - - assertions.clear(); - - bool did_something = false; - - local_bitvector_analysis = - util_make_unique(goto_function, ns); - - goto_programt &goto_program = goto_function.body; - - Forall_goto_program_instructions(it, goto_program) - { - current_target = it; - goto_programt::instructiont &i = *it; - - new_code.clear(); - - // we clear all recorded assertions if - // 1) we want to generate all assertions or - // 2) the instruction is a branch target - if(retain_trivial || i.is_target()) - assertions.clear(); - - if(i.has_condition()) - { - check(i.get_condition()); - - if(has_subexpr(i.get_condition(), [](const exprt &expr) { - return expr.id() == ID_r_ok || expr.id() == ID_w_ok || - expr.id() == ID_rw_ok; - })) - { - auto rw_ok_cond = rw_ok_check(i.get_condition()); - if(rw_ok_cond.has_value()) - i.set_condition(*rw_ok_cond); - } - } - - // magic ERROR label? - for(const auto &label : error_labels) - { - if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end()) - { - auto t = new_code.add( - enable_assert_to_assume - ? goto_programt::make_assumption(false_exprt{}, i.source_location()) - : goto_programt::make_assertion( - false_exprt{}, i.source_location())); - - t->source_location_nonconst().set_property_class("error label"); - t->source_location_nonconst().set_comment("error label " + label); - t->source_location_nonconst().set("user-provided", true); - } - } - - if(i.is_other()) - { - const auto &code = i.get_other(); - const irep_idt &statement = code.get_statement(); - - if(statement == ID_expression) - { - check(code); - } - else if(statement == ID_printf) - { - for(const auto &op : code.operands()) - check(op); - } - } - else if(i.is_assign()) - { - const exprt &assign_lhs = i.assign_lhs(); - const exprt &assign_rhs = i.assign_rhs(); - - check(assign_lhs); - check(assign_rhs); - - // the LHS might invalidate any assertion - invalidate(assign_lhs); - - if(has_subexpr(assign_rhs, [](const exprt &expr) { - return expr.id() == ID_r_ok || expr.id() == ID_w_ok || - expr.id() == ID_rw_ok; - })) - { - auto rw_ok_cond = rw_ok_check(assign_rhs); - if(rw_ok_cond.has_value()) - i.assign_rhs_nonconst() = *rw_ok_cond; - } - } - else if(i.is_function_call()) - { - const auto &function = i.call_function(); - - // for Java, need to check whether 'this' is null - // on non-static method invocations - if( - enable_pointer_check && !i.call_arguments().empty() && - function.type().id() == ID_code && - to_code_type(function.type()).has_this()) - { - exprt pointer = i.call_arguments()[0]; - - local_bitvector_analysist::flagst flags = - local_bitvector_analysis->get(current_target, pointer); - - if(flags.is_unknown() || flags.is_null()) - { - notequal_exprt not_eq_null( - pointer, null_pointer_exprt(to_pointer_type(pointer.type()))); - - add_property( - not_eq_null, - "this is null on method invocation", - "pointer dereference", - i.source_location(), - pointer); - } - } - - check(i.call_lhs()); - check(i.call_function()); - - for(const auto &arg : i.call_arguments()) - check(arg); - - // the call might invalidate any assertion - assertions.clear(); - } - else if(i.is_set_return_value()) - { - check(i.return_value()); - // the return value invalidate any assertion - invalidate(i.return_value()); - - if(has_subexpr(i.return_value(), [](const exprt &expr) { - return expr.id() == ID_r_ok || expr.id() == ID_w_ok || - expr.id() == ID_rw_ok; - })) - { - exprt &return_value = i.return_value(); - auto rw_ok_cond = rw_ok_check(return_value); - if(rw_ok_cond.has_value()) - return_value = *rw_ok_cond; - } - } - else if(i.is_throw()) - { - if( - i.get_code().get_statement() == ID_expression && - i.get_code().operands().size() == 1 && - i.get_code().op0().operands().size() == 1) - { - // must not throw NULL - - exprt pointer = to_unary_expr(i.get_code().op0()).op(); - - const notequal_exprt not_eq_null( - pointer, null_pointer_exprt(to_pointer_type(pointer.type()))); - - add_property( - not_eq_null, - "throwing null", - "pointer dereference", - i.source_location(), - pointer); - } - - // this has no successor - assertions.clear(); - } - else if(i.is_assert()) - { - bool is_user_provided = i.source_location().get_bool("user-provided"); - - if( - (is_user_provided && !enable_assertions && - i.source_location().get_property_class() != "error label") || - (!is_user_provided && !enable_built_in_assertions)) - { - i.turn_into_skip(); - did_something = true; - } - } - else if(i.is_assume()) - { - if(!enable_assumptions) - { - i.turn_into_skip(); - did_something = true; - } - } - else if(i.is_dead()) - { - if(enable_pointer_check) - { - const symbol_exprt &variable = i.dead_symbol(); - - // is it dirty? - if(local_bitvector_analysis->dirty(variable)) - { - // need to mark the dead variable as dead - exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - exprt address_of_expr = typecast_exprt::conditional_cast( - address_of_exprt(variable), lhs.type()); - if_exprt rhs( - side_effect_expr_nondett(bool_typet(), i.source_location()), - std::move(address_of_expr), - lhs); - goto_programt::targett t = - new_code.add(goto_programt::make_assignment( - std::move(lhs), std::move(rhs), i.source_location())); - t->code_nonconst().add_source_location() = i.source_location(); - } - - if( - variable.type().id() == ID_pointer && - function_identifier != "alloca" && - (ns.lookup(variable.get_identifier()).base_name == - "return_value___builtin_alloca" || - ns.lookup(variable.get_identifier()).base_name == - "return_value_alloca")) - { - // mark pointer to alloca result as dead - exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - exprt alloca_result = - typecast_exprt::conditional_cast(variable, lhs.type()); - if_exprt rhs( - side_effect_expr_nondett(bool_typet(), i.source_location()), - std::move(alloca_result), - lhs); - goto_programt::targett t = - new_code.add(goto_programt::make_assignment( - std::move(lhs), std::move(rhs), i.source_location())); - t->code_nonconst().add_source_location() = i.source_location(); - } - } - } - - for(auto &instruction : new_code.instructions) - { - if(instruction.source_location().is_nil()) - { - instruction.source_location_nonconst().id(irep_idt()); - - if(!it->source_location().get_file().empty()) - instruction.source_location_nonconst().set_file( - it->source_location().get_file()); - - if(!it->source_location().get_line().empty()) - instruction.source_location_nonconst().set_line( - it->source_location().get_line()); - - if(!it->source_location().get_function().empty()) - instruction.source_location_nonconst().set_function( - it->source_location().get_function()); - - if(!it->source_location().get_column().empty()) - { - instruction.source_location_nonconst().set_column( - it->source_location().get_column()); - } - - if(!it->source_location().get_java_bytecode_index().empty()) - { - instruction.source_location_nonconst().set_java_bytecode_index( - it->source_location().get_java_bytecode_index()); - } - } - } - - // insert new instructions -- make sure targets are not moved - did_something |= !new_code.instructions.empty(); - - while(!new_code.instructions.empty()) - { - goto_program.insert_before_swap(it, new_code.instructions.front()); - new_code.instructions.pop_front(); - it++; - } - } - - if(did_something) - remove_skip(goto_program); -} - -optionalt -goto_check_javat::get_pointer_is_null_condition( - const exprt &address, - const exprt &size) -{ - PRECONDITION(local_bitvector_analysis); - PRECONDITION(address.type().id() == ID_pointer); - const auto &pointer_type = to_pointer_type(address.type()); - local_bitvector_analysist::flagst flags = - local_bitvector_analysis->get(current_target, address); - - if(flags.is_unknown() || flags.is_null()) - { - notequal_exprt not_eq_null(address, null_pointer_exprt{pointer_type}); - return {conditiont{not_eq_null, "reference is null"}}; - } - - return {}; -} - -void goto_check_java( - const irep_idt &function_identifier, - goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - const optionst &options, - message_handlert &message_handler) -{ - goto_check_javat goto_check(ns, options, message_handler); - goto_check.goto_check(function_identifier, goto_function); -} - -void goto_check_java( - const namespacet &ns, - const optionst &options, - goto_functionst &goto_functions, - message_handlert &message_handler) -{ - goto_check_javat goto_check(ns, options, message_handler); - - for(auto &gf_entry : goto_functions.function_map) - { - goto_check.goto_check(gf_entry.first, gf_entry.second); - } -} - -void goto_check_java( - const optionst &options, - goto_modelt &goto_model, - message_handlert &message_handler) -{ - const namespacet ns(goto_model.symbol_table); - goto_check_java(ns, options, goto_model.goto_functions, message_handler); -} diff --git a/jbmc/src/java_bytecode/goto_check_java.h b/jbmc/src/java_bytecode/goto_check_java.h deleted file mode 100644 index 92420870511..00000000000 --- a/jbmc/src/java_bytecode/goto_check_java.h +++ /dev/null @@ -1,94 +0,0 @@ -/*******************************************************************\ - -Module: Checks for Errors in Java Programs - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Check for Errors in Java Programs - -#ifndef CPROVER_ANALYSES_GOTO_CHECK_JAVA_H -#define CPROVER_ANALYSES_GOTO_CHECK_JAVA_H - -#include - -class goto_modelt; -class namespacet; -class optionst; -class message_handlert; - -void goto_check_java( - const namespacet &ns, - const optionst &options, - goto_functionst &goto_functions, - message_handlert &message_handler); - -void goto_check_java( - const irep_idt &function_identifier, - goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - const optionst &options, - message_handlert &message_handler); - -void goto_check_java( - const optionst &options, - goto_modelt &goto_model, - message_handlert &message_handler); - -#define OPT_GOTO_CHECK_JAVA \ - "(bounds-check)(pointer-check)" \ - "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-" \ - "overflow-check)" \ - "(conversion-check)" \ - "(float-overflow-check)(nan-check)(no-built-in-assertions)" \ - "(retain-trivial-checks)" \ - "(error-label):" \ - "(no-assertions)(no-assumptions)" \ - "(assert-to-assume)" - -// clang-format off -#define HELP_GOTO_CHECK_JAVA \ - " --bounds-check enable array bounds checks\n" \ - " --pointer-check enable pointer checks\n" /* NOLINT(whitespace/line_length) */ \ - " --div-by-zero-check enable division by zero checks\n" \ - " --signed-overflow-check enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \ - " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \ - " --conversion-check check whether values can be represented after type cast\n" /* NOLINT(whitespace/line_length) */ \ - " --float-overflow-check check floating-point for +/-Inf\n" \ - " --nan-check check floating-point for NaN\n" \ - " --retain-trivial-checks include checks that are trivially true\n" \ - " --error-label label check that label is unreachable\n" \ - " --no-built-in-assertions ignore assertions in built-in library\n" \ - " --no-assertions ignore user assertions\n" \ - " --no-assumptions ignore user assumptions\n" \ - " --assert-to-assume convert user assertions to assumptions\n" \ - -#define PARSE_OPTIONS_GOTO_CHECK_JAVA(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("enum-range-check", cmdline.isset("enum-range-check")); \ - options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("conversion-check", cmdline.isset("conversion-check")); \ - options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("nan-check", cmdline.isset("nan-check")); \ - options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("retain-trivial-checks", \ - cmdline.isset("retain-trivial-checks")); \ - options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \ - if(cmdline.isset("error-label")) \ - options.set_option("error-label", cmdline.get_values("error-label")); \ - (void)0 -// clang-format on - -#endif // CPROVER_ANALYSES_GOTO_CHECK_JAVA_H diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index fc7fe9f798f..d885a6a0712 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -220,9 +220,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) "self-loops-to-assumptions", !cmdline.isset("no-self-loops-to-assumptions")); - // all checks supported by goto_check_java - PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options); - // unwind loops in java enum static initialization if(cmdline.isset("java-unwind-enum-static")) options.set_option("java-unwind-enum-static", true); @@ -986,7 +983,6 @@ void jbmc_parse_optionst::help() "Program instrumentation options:\n" " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" - " --error-label label check that label is unreachable\n" " --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 0e381c409bf..2e05f5cca5a 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index ccc3f6fc326..6269ed95415 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -65,12 +65,21 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options) cmdline.set("no-refine-strings"); parse_java_language_options(cmdline, options); + // check assertions + if(cmdline.isset("no-assertions")) + options.set_option("assertions", false); + else + options.set_option("assertions", true); + + // use assumptions + if(cmdline.isset("no-assumptions")) + options.set_option("assumptions", false); + else + options.set_option("assumptions", true); + if(cmdline.isset("cover")) parse_cover_options(cmdline, options); - // all checks supported by goto_check - PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options); - options.set_option("show-properties", cmdline.isset("show-properties")); } @@ -251,7 +260,8 @@ void jdiff_parse_optionst::help() " --compact-output output dependencies in compact mode\n" "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK_JAVA + " --no-assertions ignore user assertions\n" + " --no-assumptions ignore user assumptions\n" HELP_COVER "Java Bytecode frontend options:\n" JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index f4ad63c8cf5..f1507991078 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -12,8 +12,6 @@ Author: Peter Schrammel #ifndef CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H #define CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H -#include - #include #include @@ -30,7 +28,7 @@ class goto_modelt; OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \ "(show-loops)" \ - OPT_GOTO_CHECK_JAVA \ + "(no-assertions)(no-assumptions)" \ OPT_COVER \ "(verbosity):(version)" \ "(no-lazy-methods)" /* should go away */ \