diff --git a/regression/cbmc/array-constraint/main.c b/regression/cbmc/array-constraint/main.c new file mode 100644 index 00000000000..d08401acc64 --- /dev/null +++ b/regression/cbmc/array-constraint/main.c @@ -0,0 +1,12 @@ +#include +int main() +{ + size_t array_size; + int a[array_size]; + + unsigned int index; + a[index] = 1; + + assert(a[index] == 1); + return 0; +} diff --git a/regression/cbmc/array-constraint/test.desc b/regression/cbmc/array-constraint/test.desc new file mode 100644 index 00000000000..f450ca322fb --- /dev/null +++ b/regression/cbmc/array-constraint/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--show-array-constraints +^EXIT=1$ +^SIGNAL=0$ +-- +-- +To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format. diff --git a/regression/cbmc/array-constraint/test_json.desc b/regression/cbmc/array-constraint/test_json.desc new file mode 100644 index 00000000000..00d63a4c686 --- /dev/null +++ b/regression/cbmc/array-constraint/test_json.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--show-array-constraints --json-ui +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +\{\n\s*"arrayConstraints": \{\n\s*"arrayEquality": \[.*\],\n\s*"arrayWith": \[.*\]\n\s*\},\n\s*"numOfConstraints": 4\n\s*\} +-- +-- +To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format. diff --git a/regression/cbmc/array-constraint/test_xml.desc b/regression/cbmc/array-constraint/test_xml.desc new file mode 100644 index 00000000000..8a5e92b42b1 --- /dev/null +++ b/regression/cbmc/array-constraint/test_xml.desc @@ -0,0 +1,8 @@ +CORE +main.c +--show-array-constraints --xml-ui +^EXIT=1$ +^SIGNAL=0$ +-- +-- +To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 624c9d5070f..cf1c034c6a2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -123,6 +123,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("simplify-if", true); options.set_option("show-goto-symex-steps", false); options.set_option("show-points-to-sets", false); + options.set_option("show-array-constraints", false); // Other default options.set_option("arrays-uf", "auto"); @@ -348,6 +349,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("dimacs")) options.set_option("dimacs", true); + if(cmdline.isset("show-array-constraints")) + options.set_option("show-array-constraints", true); + if(cmdline.isset("refine-arrays")) { options.set_option("refine", true); @@ -577,6 +581,17 @@ int cbmc_parse_optionst::doit() } } + if(cmdline.isset("show-array-constraints")) + { + if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui")) + { + log.error() << "--show-array-constraints supports only" + " json output. Use --json-ui." + << messaget::eom; + return CPROVER_EXIT_USAGE_ERROR; + } + } + register_languages(); // configure gcc, if required @@ -1155,6 +1170,9 @@ void cbmc_parse_optionst::help() HELP_TIMESTAMP " --write-solver-stats-to json-file\n" " collect the solver query complexity\n" + " --show-array-constraints show array theory constraints added\n" + " during post processing.\n" + " Requires --json-ui.\n" "\n"; // clang-format on } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 1599aee1bd2..78a7822f289 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -47,6 +47,7 @@ class optionst; "(debug-level):(no-propagation)(no-simplify-if)" \ "(document-subgoals)(outfile):(test-preprocessor)" \ "(write-solver-stats-to):" \ + "(show-array-constraints)" \ "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \ "(object-bits):" \ OPT_GOTO_CHECK \ diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 1c162b3fd6b..11a0220a0b1 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -219,8 +219,10 @@ std::unique_ptr solver_factoryt::get_default() solver->set_prop(make_satcheck_prop(message_handler, options)); } - auto bv_pointers = - util_make_unique(ns, solver->prop(), message_handler); + bool get_array_constraints = + options.get_bool_option("show-array-constraints"); + auto bv_pointers = util_make_unique( + ns, solver->prop(), message_handler, get_array_constraints); if(options.get_option("arrays-uf") == "never") bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE; diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index d7cd86bebf0..4945051f5d4 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -10,10 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include #include #include +#include #include @@ -26,11 +29,17 @@ Author: Daniel Kroening, kroening@kroening.com arrayst::arrayst( const namespacet &_ns, propt &_prop, - message_handlert &message_handler) - : equalityt(_prop, message_handler), ns(_ns) + message_handlert &_message_handler, + bool _get_array_constraints) + : equalityt(_prop, _message_handler), + ns(_ns), + log(_message_handler), + message_handler(_message_handler) { lazy_arrays = false; // will be set to true when --refine is used incremental_cache = false; // for incremental solving + // get_array_constraints is true when --show-array-constraints is used + get_array_constraints = _get_array_constraints; } void arrayst::record_array_index(const index_exprt &index) @@ -365,6 +374,7 @@ void arrayst::add_array_Ackermann_constraints() lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN, implies_exprt(literal_exprt(indices_equal_lit), values_equal)); add_array_constraint(lazy, true); // added lazily + array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++; #if 0 // old code for adding, not significantly faster prop.lcnf(!indices_equal_lit, convert(values_equal)); @@ -451,6 +461,7 @@ void arrayst::add_array_constraints_equality( // equality constraints are not added lazily // convert must be done to guarantee correct update of the index_set prop.lcnf(!array_equality.l, convert(equality_expr)); + array_constraint_count[constraint_typet::ARRAY_EQUALITY]++; } } @@ -511,6 +522,7 @@ void arrayst::add_array_constraints( lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST, equal_exprt(index_expr1, index_expr2)); add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_TYPECAST]++; } } else if(expr.id()==ID_index) @@ -549,6 +561,7 @@ void arrayst::add_array_constraints_with( lazy_constraintt lazy( lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value)); add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_WITH]++; updated_indices.insert(index); } @@ -582,7 +595,9 @@ void arrayst::add_array_constraints_with( // add constraint lazy_constraintt lazy(lazy_typet::ARRAY_WITH, or_exprt(equality_expr, literal_exprt(guard_lit))); + add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_WITH]++; #if 0 // old code for adding, not significantly faster { @@ -678,6 +693,7 @@ void arrayst::add_array_constraints_array_of( lazy_constraintt lazy( lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what())); add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_OF]++; } } @@ -713,6 +729,7 @@ void arrayst::add_array_constraints_array_constant( lazy_constraintt lazy{lazy_typet::ARRAY_CONSTANT, equal_exprt{index_expr, v}}; add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; } else { @@ -755,6 +772,7 @@ void arrayst::add_array_constraints_array_constant( implies_exprt{index_constraint, equal_exprt{index_expr, operands[range.first]}}}; add_array_constraint(lazy, true); // added lazily + array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; } } } @@ -778,7 +796,9 @@ void arrayst::add_array_constraints_comprehension( lazy_constraintt lazy( lazy_typet::ARRAY_COMPREHENSION, equal_exprt(index_expr, comprehension_body)); + add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_COMPREHENSION]++; } } @@ -806,6 +826,7 @@ void arrayst::add_array_constraints_if( or_exprt(literal_exprt(!cond_lit), equal_exprt(index_expr1, index_expr2))); add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_IF]++; #if 0 // old code for adding, not significantly faster prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2))); @@ -825,9 +846,59 @@ void arrayst::add_array_constraints_if( or_exprt(literal_exprt(cond_lit), equal_exprt(index_expr1, index_expr2))); add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_IF]++; #if 0 // old code for adding, not significantly faster prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2))); #endif } } + +std::string arrayst::enum_to_string(constraint_typet type) +{ + switch(type) + { + case constraint_typet::ARRAY_ACKERMANN: + return "arrayAckermann"; + case constraint_typet::ARRAY_WITH: + return "arrayWith"; + case constraint_typet::ARRAY_IF: + return "arrayIf"; + case constraint_typet::ARRAY_OF: + return "arrayOf"; + case constraint_typet::ARRAY_TYPECAST: + return "arrayTypecast"; + case constraint_typet::ARRAY_CONSTANT: + return "arrayConstant"; + case constraint_typet::ARRAY_COMPREHENSION: + return "arrayComprehension"; + case constraint_typet::ARRAY_EQUALITY: + return "arrayEquality"; + default: + UNREACHABLE; + } +} + +void arrayst::display_array_constraint_count() +{ + json_objectt json_result; + json_objectt &json_array_theory = + json_result["arrayConstraints"].make_object(); + + size_t num_constraints = 0; + + array_constraint_countt::iterator it = array_constraint_count.begin(); + while(it != array_constraint_count.end()) + { + std::string contraint_type_string = enum_to_string(it->first); + json_array_theory[contraint_type_string] = + json_numbert(std::to_string(it->second)); + + num_constraints += it->second; + it++; + } + + json_result["numOfConstraints"] = + json_numbert(std::to_string(num_constraints)); + log.status() << ",\n" << json_result; +} diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 9a74d66dd65..a7ee9096269 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -33,12 +33,15 @@ class arrayst:public equalityt arrayst( const namespacet &_ns, propt &_prop, - message_handlert &message_handler); + message_handlert &message_handler, + bool get_array_constraints = false); void post_process() override { post_process_arrays(); SUB::post_process(); + if(get_array_constraints) + display_array_constraint_count(); } // NOLINTNEXTLINE(readability/identifiers) @@ -49,6 +52,8 @@ class arrayst:public equalityt protected: const namespacet &ns; + messaget log; + message_handlert &message_handler; virtual void post_process_arrays() { @@ -103,10 +108,28 @@ class arrayst:public equalityt bool lazy_arrays; bool incremental_cache; + bool get_array_constraints; std::list lazy_array_constraints; void add_array_constraint(const lazy_constraintt &lazy, bool refine = true); std::map expr_map; + enum class constraint_typet + { + ARRAY_ACKERMANN, + ARRAY_WITH, + ARRAY_IF, + ARRAY_OF, + ARRAY_TYPECAST, + ARRAY_CONSTANT, + ARRAY_COMPREHENSION, + ARRAY_EQUALITY + }; + + typedef std::map array_constraint_countt; + array_constraint_countt array_constraint_count; + void display_array_constraint_count(); + std::string enum_to_string(constraint_typet); + // adds all the constraints eagerly void add_array_constraints(); void add_array_Ackermann_constraints(); diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index ad2ebf26b2f..2789ba87660 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -37,8 +37,9 @@ class boolbvt:public arrayst boolbvt( const namespacet &_ns, propt &_prop, - message_handlert &message_handler) - : arrayst(_ns, _prop, message_handler), + message_handlert &message_handler, + bool get_array_constraints = false) + : arrayst(_ns, _prop, message_handler, get_array_constraints), unbounded_array(unbounded_arrayt::U_NONE), boolbv_width(_ns), bv_utils(_prop), diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index a3a6b2eaf34..91662c593f8 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -82,8 +82,10 @@ literalt bv_pointerst::convert_rest(const exprt &expr) bv_pointerst::bv_pointerst( const namespacet &_ns, propt &_prop, - message_handlert &message_handler) - : boolbvt(_ns, _prop, message_handler), pointer_logic(_ns) + message_handlert &message_handler, + bool get_array_constraints) + : boolbvt(_ns, _prop, message_handler, get_array_constraints), + pointer_logic(_ns) { object_bits=config.bv_encoding.object_bits; std::size_t pointer_width = boolbv_width(pointer_type(empty_typet())); diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 8a1a8df97de..8df10de3872 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -20,7 +20,8 @@ class bv_pointerst:public boolbvt bv_pointerst( const namespacet &_ns, propt &_prop, - message_handlert &message_handler); + message_handlert &message_handler, + bool get_array_constraints = false); void post_process() override;