From aa00a42fa5510a2de63373047ca463c2f1b704c2 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 21 Aug 2020 22:39:25 +0100 Subject: [PATCH 01/12] Add parse option --show-array-constraints to track array constraints added during post processing Array theory constraints added during post processing might be useful to reason about proof runtimes. This commit adds a new parse option --show-array-constraints that tracks constraints pertaining to arrays added during post processing. --- src/cbmc/cbmc_parse_options.cpp | 5 +++++ src/cbmc/cbmc_parse_options.h | 1 + 2 files changed, 6 insertions(+) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 624c9d5070f..16eb03226e6 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); @@ -1155,6 +1159,7 @@ 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" "\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 \ From 351ece08cdf3177bca9bc905d60aea8cc3a1e1c0 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 21 Aug 2020 22:40:20 +0100 Subject: [PATCH 02/12] Add utility and module to track array constraints and display in json format This commit adds utilities to track array constraints and also the type of constraint being added, eg: ackermann constraint, array_of etc. Added a new enum class constraint_typet which is an extension of lazy_typet. This enum class includes a separate value for constraints added for other indices array_with, constraints added for the 'true' and 'false branches of if etc in addition to those available in lazy_typet. Also define a new member of type std::map that tracks mapping between type of constraint and the constraint itself. Currently support json output. --- src/solvers/flattening/arrays.cpp | 98 ++++++++++++++++++++++++++++++- src/solvers/flattening/arrays.h | 29 ++++++++- 2 files changed, 124 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index d7cd86bebf0..a249c2cf0b7 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -14,6 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include +#include #include @@ -26,11 +29,14 @@ 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 = _get_array_constraints; } void arrayst::record_array_index(const index_exprt &index) @@ -365,6 +371,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_ACKERMANN].push_back(lazy.lazy); #if 0 // old code for adding, not significantly faster prop.lcnf(!indices_equal_lit, convert(values_equal)); @@ -451,6 +459,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_EQUALITY].push_back(equality_expr); } } @@ -511,6 +521,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_TYPECAST].push_back(lazy.lazy); } } else if(expr.id()==ID_index) @@ -549,6 +561,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_WITH].push_back(lazy.lazy); updated_indices.insert(index); } @@ -582,7 +596,10 @@ 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_constraints_map[ + constraint_typet::ARRAY_WITH_OTHER].push_back(lazy.lazy); #if 0 // old code for adding, not significantly faster { @@ -678,6 +695,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_OF].push_back(lazy.lazy); } } @@ -713,6 +732,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_CONSTANT].push_back(lazy.lazy); } else { @@ -755,6 +776,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_NON_CONSTANT].push_back(lazy.lazy); } } } @@ -778,7 +801,10 @@ 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_constraints_map[ + constraint_typet::ARRAY_COMPREHENSION].push_back(lazy.lazy); } } @@ -806,6 +832,8 @@ 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_constraints_map[ + constraint_typet::ARRAY_IF_TRUE].push_back(lazy.lazy); #if 0 // old code for adding, not significantly faster prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2))); @@ -825,9 +853,75 @@ 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_constraints_map[ + constraint_typet::ARRAY_IF_FALSE].push_back(lazy.lazy); #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_EQUALITY: + return "arrayEquality"; + case constraint_typet::ARRAY_WITH: + return "arrayWith"; + case constraint_typet::ARRAY_WITH_OTHER: + return "arrayWithOther"; + case constraint_typet::ARRAY_IF_TRUE: + return "arrayIfTrue"; + case constraint_typet::ARRAY_IF_FALSE: + return "arrayIfFalse"; + 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_NON_CONSTANT: + return "arrayNonConstant"; + case constraint_typet::ARRAY_COMPREHENSION: + return "arrayComprehension"; + default: + UNREACHABLE; + } +} + +void arrayst::display_constraints() +{ + json_objectt json_result; + json_objectt &json_array_theory = + json_result["arrayConstraints"].make_object(); + + size_t num_constraints = 0; + + array_constraints_mapt::iterator it = array_constraints_map.begin(); + while(it != array_constraints_map.end()) + { + std::string contraint_type_string = enum_to_string(it->first); + json_arrayt &json_constraint_list = + json_array_theory[contraint_type_string].make_array(); + + array_constraintst::iterator constraint_it = it->second.begin(); + while(constraint_it != it->second.end()) + { + std::stringstream ss; + ss << format(*constraint_it); + json_constraint_list.push_back(json_stringt(ss.str())); + + constraint_it++; + num_constraints++; + } + 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..16b10c3205c 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_constraints(); } // 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() { @@ -77,6 +82,27 @@ class arrayst:public equalityt typedef std::map index_mapt; index_mapt index_map; + enum class constraint_typet + { + ARRAY_ACKERMANN, + ARRAY_EQUALITY, + ARRAY_WITH, + ARRAY_WITH_OTHER, + ARRAY_IF_TRUE, + ARRAY_IF_FALSE, + ARRAY_OF, + ARRAY_TYPECAST, + ARRAY_CONSTANT, + ARRAY_NON_CONSTANT, + ARRAY_COMPREHENSION + }; + + typedef std::list array_constraintst; + typedef std::map array_constraints_mapt; + array_constraints_mapt array_constraints_map; + void display_constraints(); + std::string enum_to_string(constraint_typet); + // adds array constraints lazily enum class lazy_typet { @@ -103,6 +129,7 @@ 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; From 1075782073cf70f7d917dd7bde853467c309d746 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 21 Aug 2020 22:42:05 +0100 Subject: [PATCH 03/12] Modify boolbvt and bv_pointerst to incorporate get_array_constraints boolean option used in arrayst class Add an additional boolean argument to the class constrcutor to propagate the setting of parse option --show-array-constraints to true to the arrayst class. The entry point for this is in the default invocation of solver factory. --- src/goto-checker/solver_factory.cpp | 3 ++- src/solvers/flattening/boolbv.h | 5 +++-- src/solvers/flattening/bv_pointers.cpp | 5 +++-- src/solvers/flattening/bv_pointers.h | 3 ++- 4 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 1c162b3fd6b..7bbee110a54 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -219,8 +219,9 @@ std::unique_ptr solver_factoryt::get_default() solver->set_prop(make_satcheck_prop(message_handler, options)); } + bool get_array_constraints = options.get_bool_option("show-array-constraints"); auto bv_pointers = - util_make_unique(ns, solver->prop(), message_handler); + 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/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..de27c0ee900 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -82,8 +82,9 @@ 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; From 30dc217824c992f662956582bca8c85750468b9b Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 26 Aug 2020 19:58:32 +0100 Subject: [PATCH 04/12] Regression test for --show-array-constraints --json-ui --- regression/cbmc/array-constraint/main.c | 12 ++++++++++++ regression/cbmc/array-constraint/test.desc | 10 ++++++++++ 2 files changed, 22 insertions(+) create mode 100644 regression/cbmc/array-constraint/main.c create mode 100644 regression/cbmc/array-constraint/test.desc diff --git a/regression/cbmc/array-constraint/main.c b/regression/cbmc/array-constraint/main.c new file mode 100644 index 00000000000..9ad7c14f7ff --- /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..6941135df50 --- /dev/null +++ b/regression/cbmc/array-constraint/test.desc @@ -0,0 +1,10 @@ +CORE +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. From 4f5f2a6310b409de0b1408156849c58b2fec4329 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 21 Aug 2020 22:40:20 +0100 Subject: [PATCH 05/12] Add utility and module to track array constraints and display in json format This commit adds utilities to track array constraints and also the type of constraint being added, eg: ackermann constraint, array_of etc. Added a new enum class constraint_typet which is an extension of lazy_typet. This enum class includes a separate value for constraints added for other indices array_with, constraints added for the 'true' and 'false branches of if etc in addition to those available in lazy_typet. Also define a new member of type std::map that tracks mapping between type of constraint and the constraint itself. Currently support json output. clang format arrays.cpp --- src/solvers/flattening/arrays.cpp | 98 +++++++++++++++---------------- 1 file changed, 49 insertions(+), 49 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index a249c2cf0b7..097ce99ba82 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -10,12 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include #include #include -#include -#include + #include #include @@ -31,7 +32,9 @@ arrayst::arrayst( propt &_prop, message_handlert &_message_handler, bool _get_array_constraints) - : equalityt(_prop, _message_handler), ns(_ns), log(_message_handler), + : 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 @@ -371,8 +374,8 @@ 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_constraints_map[ - constraint_typet::ARRAY_ACKERMANN].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_ACKERMANN].push_back( + lazy.lazy); #if 0 // old code for adding, not significantly faster prop.lcnf(!indices_equal_lit, convert(values_equal)); @@ -459,8 +462,8 @@ 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_constraints_map[ - constraint_typet::ARRAY_EQUALITY].push_back(equality_expr); + array_constraints_map[constraint_typet::ARRAY_EQUALITY].push_back( + equality_expr); } } @@ -521,8 +524,8 @@ 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_constraints_map[ - constraint_typet::ARRAY_TYPECAST].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_TYPECAST].push_back( + lazy.lazy); } } else if(expr.id()==ID_index) @@ -561,8 +564,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_constraints_map[ - constraint_typet::ARRAY_WITH].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_WITH].push_back(lazy.lazy); updated_indices.insert(index); } @@ -598,8 +600,8 @@ void arrayst::add_array_constraints_with( literal_exprt(guard_lit))); add_array_constraint(lazy, false); // added immediately - array_constraints_map[ - constraint_typet::ARRAY_WITH_OTHER].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_WITH_OTHER].push_back( + lazy.lazy); #if 0 // old code for adding, not significantly faster { @@ -695,8 +697,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_constraints_map[ - constraint_typet::ARRAY_OF].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_OF].push_back(lazy.lazy); } } @@ -732,8 +733,8 @@ 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_constraints_map[ - constraint_typet::ARRAY_CONSTANT].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_CONSTANT].push_back( + lazy.lazy); } else { @@ -776,8 +777,8 @@ 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_constraints_map[ - constraint_typet::ARRAY_NON_CONSTANT].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_NON_CONSTANT].push_back( + lazy.lazy); } } } @@ -803,8 +804,8 @@ void arrayst::add_array_constraints_comprehension( equal_exprt(index_expr, comprehension_body)); add_array_constraint(lazy, false); // added immediately - array_constraints_map[ - constraint_typet::ARRAY_COMPREHENSION].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_COMPREHENSION].push_back( + lazy.lazy); } } @@ -832,8 +833,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_constraints_map[ - constraint_typet::ARRAY_IF_TRUE].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_IF_TRUE].push_back(lazy.lazy); #if 0 // old code for adding, not significantly faster prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2))); @@ -853,8 +853,8 @@ 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_constraints_map[ - constraint_typet::ARRAY_IF_FALSE].push_back(lazy.lazy); + array_constraints_map[constraint_typet::ARRAY_IF_FALSE].push_back( + lazy.lazy); #if 0 // old code for adding, not significantly faster prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2))); @@ -866,30 +866,30 @@ std::string arrayst::enum_to_string(constraint_typet type) { switch(type) { - case constraint_typet::ARRAY_ACKERMANN: - return "arrayAckermann"; - case constraint_typet::ARRAY_EQUALITY: - return "arrayEquality"; - case constraint_typet::ARRAY_WITH: - return "arrayWith"; - case constraint_typet::ARRAY_WITH_OTHER: - return "arrayWithOther"; - case constraint_typet::ARRAY_IF_TRUE: - return "arrayIfTrue"; - case constraint_typet::ARRAY_IF_FALSE: - return "arrayIfFalse"; - 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_NON_CONSTANT: - return "arrayNonConstant"; - case constraint_typet::ARRAY_COMPREHENSION: - return "arrayComprehension"; - default: - UNREACHABLE; + case constraint_typet::ARRAY_ACKERMANN: + return "arrayAckermann"; + case constraint_typet::ARRAY_EQUALITY: + return "arrayEquality"; + case constraint_typet::ARRAY_WITH: + return "arrayWith"; + case constraint_typet::ARRAY_WITH_OTHER: + return "arrayWithOther"; + case constraint_typet::ARRAY_IF_TRUE: + return "arrayIfTrue"; + case constraint_typet::ARRAY_IF_FALSE: + return "arrayIfFalse"; + 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_NON_CONSTANT: + return "arrayNonConstant"; + case constraint_typet::ARRAY_COMPREHENSION: + return "arrayComprehension"; + default: + UNREACHABLE; } } From a7bf2b642b3ed9edf26ae9c4605c6f9ccce8d241 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 21 Aug 2020 22:42:05 +0100 Subject: [PATCH 06/12] Modify boolbvt and bv_pointerst to incorporate get_array_constraints boolean option used in arrayst class Add an additional boolean argument to the class constrcutor to propagate the setting of parse option --show-array-constraints to true to the arrayst class. The entry point for this is in the default invocation of solver factory. clang format solver_factory and bv_pointers --- src/goto-checker/solver_factory.cpp | 7 ++++--- src/solvers/flattening/bv_pointers.cpp | 3 ++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 7bbee110a54..11a0220a0b1 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -219,9 +219,10 @@ std::unique_ptr solver_factoryt::get_default() solver->set_prop(make_satcheck_prop(message_handler, options)); } - 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); + 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/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index de27c0ee900..91662c593f8 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -84,7 +84,8 @@ bv_pointerst::bv_pointerst( propt &_prop, message_handlert &message_handler, bool get_array_constraints) - : boolbvt(_ns, _prop, message_handler, get_array_constraints), pointer_logic(_ns) + : 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())); From bbac08ffef09dfb35fe97993e421a84d85d712da Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 26 Aug 2020 19:58:32 +0100 Subject: [PATCH 07/12] Regression test for --show-array-constraints --json-ui clang format regression test Adding KNOWNBUG flag to ignore failed test The --smt2 option does not go over arrayst class so no output is generated. The current test thus fails on test-cprover-smt2. --- regression/cbmc/array-constraint/main.c | 14 +++++++------- regression/cbmc/array-constraint/test.desc | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/cbmc/array-constraint/main.c b/regression/cbmc/array-constraint/main.c index 9ad7c14f7ff..d08401acc64 100644 --- a/regression/cbmc/array-constraint/main.c +++ b/regression/cbmc/array-constraint/main.c @@ -1,12 +1,12 @@ -#include +#include int main() { - size_t array_size; - int a[array_size]; + size_t array_size; + int a[array_size]; - unsigned int index; - a[index] = 1; + unsigned int index; + a[index] = 1; - assert(a[index] == 1); - return 0; + assert(a[index] == 1); + return 0; } diff --git a/regression/cbmc/array-constraint/test.desc b/regression/cbmc/array-constraint/test.desc index 6941135df50..00d63a4c686 100644 --- a/regression/cbmc/array-constraint/test.desc +++ b/regression/cbmc/array-constraint/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --show-array-constraints --json-ui activate-multi-line-match From 3df482f54ed2ef02b2a450fb3c1aa6c9b19eb6ce Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 21 Aug 2020 22:39:25 +0100 Subject: [PATCH 08/12] Add parse option --show-array-constraints to track array constraints added during post processing Array theory constraints added during post processing might be useful to reason about proof runtimes. This commit adds a new parse option --show-array-constraints that tracks constraints pertaining to arrays added during post processing. fix command line argument to display error message of xml or plain format is used --- src/cbmc/cbmc_parse_options.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 16eb03226e6..cf1c034c6a2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -581,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 @@ -1160,6 +1171,8 @@ void cbmc_parse_optionst::help() " --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 } From 56158febeca4cd53f2ba52ab6a930966f2de5650 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Thu, 3 Sep 2020 20:54:35 +0100 Subject: [PATCH 09/12] track number of constraints of different types rather than the actual constraints --- src/solvers/flattening/arrays.cpp | 67 ++++++++++--------------------- src/solvers/flattening/arrays.h | 40 +++++++++--------- 2 files changed, 40 insertions(+), 67 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 097ce99ba82..4945051f5d4 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - #include #include @@ -39,6 +38,7 @@ arrayst::arrayst( { 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; } @@ -374,8 +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_constraints_map[constraint_typet::ARRAY_ACKERMANN].push_back( - lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++; #if 0 // old code for adding, not significantly faster prop.lcnf(!indices_equal_lit, convert(values_equal)); @@ -462,8 +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_constraints_map[constraint_typet::ARRAY_EQUALITY].push_back( - equality_expr); + array_constraint_count[constraint_typet::ARRAY_EQUALITY]++; } } @@ -524,8 +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_constraints_map[constraint_typet::ARRAY_TYPECAST].push_back( - lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_TYPECAST]++; } } else if(expr.id()==ID_index) @@ -564,7 +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_constraints_map[constraint_typet::ARRAY_WITH].push_back(lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_WITH]++; updated_indices.insert(index); } @@ -600,8 +597,7 @@ void arrayst::add_array_constraints_with( literal_exprt(guard_lit))); add_array_constraint(lazy, false); // added immediately - array_constraints_map[constraint_typet::ARRAY_WITH_OTHER].push_back( - lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_WITH]++; #if 0 // old code for adding, not significantly faster { @@ -697,7 +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_constraints_map[constraint_typet::ARRAY_OF].push_back(lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_OF]++; } } @@ -733,8 +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_constraints_map[constraint_typet::ARRAY_CONSTANT].push_back( - lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; } else { @@ -777,8 +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_constraints_map[constraint_typet::ARRAY_NON_CONSTANT].push_back( - lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; } } } @@ -804,8 +798,7 @@ void arrayst::add_array_constraints_comprehension( equal_exprt(index_expr, comprehension_body)); add_array_constraint(lazy, false); // added immediately - array_constraints_map[constraint_typet::ARRAY_COMPREHENSION].push_back( - lazy.lazy); + array_constraint_count[constraint_typet::ARRAY_COMPREHENSION]++; } } @@ -833,7 +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_constraints_map[constraint_typet::ARRAY_IF_TRUE].push_back(lazy.lazy); + 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))); @@ -853,8 +846,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_constraints_map[constraint_typet::ARRAY_IF_FALSE].push_back( - lazy.lazy); + 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))); @@ -868,32 +860,26 @@ std::string arrayst::enum_to_string(constraint_typet type) { case constraint_typet::ARRAY_ACKERMANN: return "arrayAckermann"; - case constraint_typet::ARRAY_EQUALITY: - return "arrayEquality"; case constraint_typet::ARRAY_WITH: return "arrayWith"; - case constraint_typet::ARRAY_WITH_OTHER: - return "arrayWithOther"; - case constraint_typet::ARRAY_IF_TRUE: - return "arrayIfTrue"; - case constraint_typet::ARRAY_IF_FALSE: - return "arrayIfFalse"; + 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_NON_CONSTANT: - return "arrayNonConstant"; case constraint_typet::ARRAY_COMPREHENSION: return "arrayComprehension"; + case constraint_typet::ARRAY_EQUALITY: + return "arrayEquality"; default: UNREACHABLE; } } -void arrayst::display_constraints() +void arrayst::display_array_constraint_count() { json_objectt json_result; json_objectt &json_array_theory = @@ -901,23 +887,14 @@ void arrayst::display_constraints() size_t num_constraints = 0; - array_constraints_mapt::iterator it = array_constraints_map.begin(); - while(it != array_constraints_map.end()) + 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_arrayt &json_constraint_list = - json_array_theory[contraint_type_string].make_array(); - - array_constraintst::iterator constraint_it = it->second.begin(); - while(constraint_it != it->second.end()) - { - std::stringstream ss; - ss << format(*constraint_it); - json_constraint_list.push_back(json_stringt(ss.str())); + json_array_theory[contraint_type_string] = + json_numbert(std::to_string(it->second)); - constraint_it++; - num_constraints++; - } + num_constraints += it->second; it++; } diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 16b10c3205c..a7ee9096269 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -41,7 +41,7 @@ class arrayst:public equalityt post_process_arrays(); SUB::post_process(); if(get_array_constraints) - display_constraints(); + display_array_constraint_count(); } // NOLINTNEXTLINE(readability/identifiers) @@ -82,27 +82,6 @@ class arrayst:public equalityt typedef std::map index_mapt; index_mapt index_map; - enum class constraint_typet - { - ARRAY_ACKERMANN, - ARRAY_EQUALITY, - ARRAY_WITH, - ARRAY_WITH_OTHER, - ARRAY_IF_TRUE, - ARRAY_IF_FALSE, - ARRAY_OF, - ARRAY_TYPECAST, - ARRAY_CONSTANT, - ARRAY_NON_CONSTANT, - ARRAY_COMPREHENSION - }; - - typedef std::list array_constraintst; - typedef std::map array_constraints_mapt; - array_constraints_mapt array_constraints_map; - void display_constraints(); - std::string enum_to_string(constraint_typet); - // adds array constraints lazily enum class lazy_typet { @@ -134,6 +113,23 @@ class arrayst:public equalityt 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(); From ecb0a5d01154cae53c6ed37f9e01a2c8185415b7 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 11 Sep 2020 15:21:08 +0100 Subject: [PATCH 10/12] Regression tests for --xml-ui and plain --- regression/cbmc/array-constraint/test.desc | 10 ++++------ regression/cbmc/array-constraint/test_json.desc | 10 ++++++++++ regression/cbmc/array-constraint/test_xml.desc | 8 ++++++++ 3 files changed, 22 insertions(+), 6 deletions(-) create mode 100644 regression/cbmc/array-constraint/test_json.desc create mode 100644 regression/cbmc/array-constraint/test_xml.desc diff --git a/regression/cbmc/array-constraint/test.desc b/regression/cbmc/array-constraint/test.desc index 00d63a4c686..e28e1481fd4 100644 --- a/regression/cbmc/array-constraint/test.desc +++ b/regression/cbmc/array-constraint/test.desc @@ -1,10 +1,8 @@ -KNOWNBUG +CORE main.c ---show-array-constraints --json-ui -activate-multi-line-match -^EXIT=0$ +--show-array-constraints +^EXIT=1$ ^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. +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. \ No newline at end of file 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..7b860f7f538 --- /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. \ No newline at end of file From fbe04066eb1c8c7c8824f1f054316ee4c1cc409b Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 11 Sep 2020 15:21:08 +0100 Subject: [PATCH 11/12] Regression tests for --xml-ui and plain --- regression/cbmc/array-constraint/test_xml.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/array-constraint/test_xml.desc b/regression/cbmc/array-constraint/test_xml.desc index 7b860f7f538..8a5e92b42b1 100644 --- a/regression/cbmc/array-constraint/test_xml.desc +++ b/regression/cbmc/array-constraint/test_xml.desc @@ -5,4 +5,4 @@ main.c ^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. \ No newline at end of file +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. From 04341a8fdfe217a5b016fa7d8fa33c8a77239f83 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 11 Sep 2020 15:21:08 +0100 Subject: [PATCH 12/12] Regression tests for --xml-ui and plain add newline to test.desc --- regression/cbmc/array-constraint/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/array-constraint/test.desc b/regression/cbmc/array-constraint/test.desc index e28e1481fd4..f450ca322fb 100644 --- a/regression/cbmc/array-constraint/test.desc +++ b/regression/cbmc/array-constraint/test.desc @@ -5,4 +5,4 @@ main.c ^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. \ No newline at end of file +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.