From a0646971c617f8622f3743e7716db6092a192578 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:50:13 +0100 Subject: [PATCH 01/15] Add parse option to display points-to set information for pointer dereference The points to set information provides some intuition about the complexity of the resulting case split expression in case of a pointer dereference. This commit adds parse option --show-points-to-sets to track the size and contents of the points-to set for pointers. --- src/cbmc/cbmc_parse_options.cpp | 4 ++++ src/goto-checker/bmc_util.h | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7b561f1cacf..b59d98aa26a 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -122,6 +122,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("simplify", true); options.set_option("simplify-if", true); options.set_option("show-goto-symex-steps", false); + options.set_option("show-points-to-sets", false); // Other default options.set_option("arrays-uf", "auto"); @@ -520,6 +521,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("show-goto-symex-steps")) options.set_option("show-goto-symex-steps", true); + if(cmdline.isset("show-points-to-sets")) + options.set_option("show-points-to-sets", true); + PARSE_OPTIONS_GOTO_TRACE(cmdline, options); } diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index a3e87ebcdf5..f89f46cff83 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -177,6 +177,7 @@ void run_property_decider( "(show-loops)" \ "(show-vcc)" \ "(show-goto-symex-steps)" \ + "(show-points-to-sets)" \ "(slice-formula)" \ "(unwinding-assertions)" \ "(no-unwinding-assertions)" \ @@ -203,6 +204,7 @@ void run_property_decider( " --show-symex-strategies list strategies for use with --paths\n" \ " --show-goto-symex-steps show which steps symex travels, includes " \ " diagnostic information\n" \ + " --show-points-to-sets show points-to sets for pointer dereference\n" \ " --program-only only show program expression\n" \ " --show-byte-ops show all byte extracts and updates\n" \ " --show-loops show the loops in the program\n" \ From be9b08629091cfacb67101eff58f998f2404ab1d Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:52:14 +0100 Subject: [PATCH 02/15] Add show_points_to_sets to symex configuration to detect if CBMC parse option holds This commit propagates parse option information to the symex stage. It is then used to display the points-to sets. --- src/goto-symex/symex_config.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-symex/symex_config.h b/src/goto-symex/symex_config.h index 086b1b091b5..b7bd52e83f6 100644 --- a/src/goto-symex/symex_config.h +++ b/src/goto-symex/symex_config.h @@ -46,6 +46,7 @@ struct symex_configt final /// \brief Prints out the path that symex is actively taking during execution, /// includes diagnostic information about call stack and guard size. bool show_symex_steps; + bool show_points_to_sets; /// Maximum sizes for which field sensitivity will be applied to array cells std::size_t max_field_sensitivity_array_size; From bb6f89a632df67d0ca16eb0a73ccb6bfb88619ee Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 20:58:46 +0100 Subject: [PATCH 03/15] Add module to track points-to set information for pointer dereferencing during symex This commit displays the points-to set information in json format. Support for other formats are yet to be added. --- src/goto-symex/symex_clean_expr.cpp | 2 +- src/goto-symex/symex_dereference.cpp | 2 +- src/goto-symex/symex_main.cpp | 1 + .../value_set_dereference.cpp | 60 ++++++++++++++++--- src/pointer-analysis/value_set_dereference.h | 3 +- 5 files changed, 58 insertions(+), 10 deletions(-) diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 9aaa72921f7..6a66563156f 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -136,7 +136,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr) value_set_dereferencet dereference( ns, state.symbol_table, symex_dereference_state, language_mode, false); - expr = dereference.dereference(expr); + expr = dereference.dereference(expr, symex_config.show_points_to_sets); lift_lets(state, expr); ::process_array_expr(expr, symex_config.simplify_opt, ns); diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index af6c8a36c7b..c69470a75e4 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -267,7 +267,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) expr_is_not_null); // std::cout << "**** " << format(tmp1) << '\n'; - exprt tmp2 = dereference.dereference(tmp1); + exprt tmp2 = dereference.dereference(tmp1, symex_config.show_points_to_sets); // std::cout << "**** " << format(tmp2) << '\n'; expr.swap(tmp2); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 68fd360586b..8f6c3db9ee5 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -47,6 +47,7 @@ symex_configt::symex_configt(const optionst &options) debug_level(unsafe_string2int(options.get_option("debug-level"))), run_validation_checks(options.get_bool_option("validate-ssa-equation")), show_symex_steps(options.get_bool_option("show-goto-symex-steps")), + show_points_to_sets(options.get_bool_option("show-points-to-sets")), max_field_sensitivity_array_size( options.is_set("no-array-field-sensitivity") ? 0 diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 6c15e53593d..77296274867 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -11,10 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "value_set_dereference.h" -#ifdef DEBUG #include #include -#endif +#include #include #include @@ -60,7 +59,7 @@ static bool should_use_local_definition_for(const exprt &expr) return false; } -exprt value_set_dereferencet::dereference(const exprt &pointer) +exprt value_set_dereferencet::dereference(const exprt &pointer, bool display_points_to_sets) { if(pointer.type().id()!=ID_pointer) throw "dereference expected pointer type, but got "+ @@ -70,8 +69,8 @@ exprt value_set_dereferencet::dereference(const exprt &pointer) if(pointer.id()==ID_if) { const if_exprt &if_expr=to_if_expr(pointer); - exprt true_case = dereference(if_expr.true_case()); - exprt false_case = dereference(if_expr.false_case()); + exprt true_case = dereference(if_expr.true_case(), display_points_to_sets); + exprt false_case = dereference(if_expr.false_case(), display_points_to_sets); return if_exprt(if_expr.cond(), true_case, false_case); } else if(pointer.id() == ID_typecast) @@ -90,14 +89,22 @@ exprt value_set_dereferencet::dereference(const exprt &pointer) const auto &if_expr = to_if_expr(*underlying); return if_exprt( if_expr.cond(), - dereference(typecast_exprt(if_expr.true_case(), pointer.type())), - dereference(typecast_exprt(if_expr.false_case(), pointer.type()))); + dereference(typecast_exprt(if_expr.true_case(), pointer.type()), display_points_to_sets), + dereference(typecast_exprt(if_expr.false_case(), pointer.type()), display_points_to_sets)); } } // type of the object const typet &type=pointer.type().subtype(); + json_objectt json_result; + if(display_points_to_sets) + { + std::stringstream ss; + ss << format(pointer); + json_result["Pointer"] = json_stringt(ss.str()); + } + #ifdef DEBUG std::cout << "value_set_dereferencet::dereference pointer=" << format(pointer) << '\n'; @@ -107,6 +114,21 @@ exprt value_set_dereferencet::dereference(const exprt &pointer) const std::vector points_to_set = dereference_callback.get_value_set(pointer); + if(display_points_to_sets) + { + json_result["PointsToSetSize"] = json_numbert(std::to_string(points_to_set.size())); + + json_arrayt points_to_set_json; + for(auto p : points_to_set) + { + std::stringstream ss; + ss << format(p); + points_to_set_json.push_back(json_stringt(ss.str())); + } + + json_result["PointsToSet"] = points_to_set_json; + } + #ifdef DEBUG std::cout << "value_set_dereferencet::dereference points_to_set={"; for(auto p : points_to_set) @@ -135,6 +157,21 @@ exprt value_set_dereferencet::dereference(const exprt &pointer) compare_against_pointer = fresh_binder.symbol_expr(); } + if(display_points_to_sets) + { + json_result["RetainedValuesSetSize"] = json_numbert(std::to_string(points_to_set.size())); + + json_arrayt retained_values_set_json; + for(auto &value : retained_values) + { + std::stringstream ss; + ss << format(value); + retained_values_set_json.push_back(json_stringt(ss.str())); + } + + json_result["RetainedValuesSet"] = retained_values_set_json; + } + #ifdef DEBUG std::cout << "value_set_dereferencet::dereference retained_values={"; for(const auto &value : retained_values) @@ -224,6 +261,15 @@ exprt value_set_dereferencet::dereference(const exprt &pointer) if(compare_against_pointer != pointer) value = let_exprt(to_symbol_expr(compare_against_pointer), pointer, value); + if(display_points_to_sets) + { + std::stringstream ss; + ss << format(value); + json_result["Value"] = json_stringt(ss.str()); + + std::cout << ",\n" << json_result; + } + #ifdef DEBUG std::cout << "value_set_derefencet::dereference value=" << format(value) << '\n' diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 4889a7cb362..c37de21f2e2 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -52,7 +52,8 @@ class value_set_dereferencet final /// Dereference the given pointer-expression. Any errors are /// reported to the callback method given in the constructor. /// \param pointer: A pointer-typed expression, to be dereferenced. - exprt dereference(const exprt &pointer); + /// \param display_points_to_sets: Display size and contents of points to sets + exprt dereference(const exprt &pointer, bool display_points_to_sets = false); /// Return value for `build_reference_to`; see that method for documentation. class valuet From 4e7eb3036d915e447a9bcd179079dcf57ae76d3b Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 26 Aug 2020 17:02:27 +0100 Subject: [PATCH 04/15] Regression test for --show-points-to-sets --json-ui --- regression/cbmc/points-to-sets/main.c | 9 +++++++++ regression/cbmc/points-to-sets/test.desc | 10 ++++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/cbmc/points-to-sets/main.c create mode 100644 regression/cbmc/points-to-sets/test.desc diff --git a/regression/cbmc/points-to-sets/main.c b/regression/cbmc/points-to-sets/main.c new file mode 100644 index 00000000000..7446a031b04 --- /dev/null +++ b/regression/cbmc/points-to-sets/main.c @@ -0,0 +1,9 @@ +int main() +{ + unsigned int value; + int *p = (int *) value; + + *p = *p + 1; + assert(1); + return 0; +} diff --git a/regression/cbmc/points-to-sets/test.desc b/regression/cbmc/points-to-sets/test.desc new file mode 100644 index 00000000000..dfc82630769 --- /dev/null +++ b/regression/cbmc/points-to-sets/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show-points-to-sets --json-ui +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\} +-- +-- +To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. \ No newline at end of file From caa506ae37a22923da1c0ddc288fcead5bc59076 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 20:58:46 +0100 Subject: [PATCH 05/15] Add module to track points-to set information for pointer dereferencing during symex This commit displays the points-to set information in json format. Support for other formats are yet to be added. clang format value_set_dereference.cpp symex_dereference.cpp --- src/goto-symex/symex_dereference.cpp | 3 ++- .../value_set_dereference.cpp | 21 +++++++++++++------ 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index c69470a75e4..a57a141d884 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -267,7 +267,8 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) expr_is_not_null); // std::cout << "**** " << format(tmp1) << '\n'; - exprt tmp2 = dereference.dereference(tmp1, symex_config.show_points_to_sets); + exprt tmp2 = + dereference.dereference(tmp1, symex_config.show_points_to_sets); // std::cout << "**** " << format(tmp2) << '\n'; expr.swap(tmp2); diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 77296274867..1273a5ea061 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -59,7 +59,9 @@ static bool should_use_local_definition_for(const exprt &expr) return false; } -exprt value_set_dereferencet::dereference(const exprt &pointer, bool display_points_to_sets) +exprt value_set_dereferencet::dereference( + const exprt &pointer, + bool display_points_to_sets) { if(pointer.type().id()!=ID_pointer) throw "dereference expected pointer type, but got "+ @@ -70,7 +72,8 @@ exprt value_set_dereferencet::dereference(const exprt &pointer, bool display_poi { const if_exprt &if_expr=to_if_expr(pointer); exprt true_case = dereference(if_expr.true_case(), display_points_to_sets); - exprt false_case = dereference(if_expr.false_case(), display_points_to_sets); + exprt false_case = + dereference(if_expr.false_case(), display_points_to_sets); return if_exprt(if_expr.cond(), true_case, false_case); } else if(pointer.id() == ID_typecast) @@ -89,8 +92,12 @@ exprt value_set_dereferencet::dereference(const exprt &pointer, bool display_poi const auto &if_expr = to_if_expr(*underlying); return if_exprt( if_expr.cond(), - dereference(typecast_exprt(if_expr.true_case(), pointer.type()), display_points_to_sets), - dereference(typecast_exprt(if_expr.false_case(), pointer.type()), display_points_to_sets)); + dereference( + typecast_exprt(if_expr.true_case(), pointer.type()), + display_points_to_sets), + dereference( + typecast_exprt(if_expr.false_case(), pointer.type()), + display_points_to_sets)); } } @@ -116,7 +123,8 @@ exprt value_set_dereferencet::dereference(const exprt &pointer, bool display_poi if(display_points_to_sets) { - json_result["PointsToSetSize"] = json_numbert(std::to_string(points_to_set.size())); + json_result["PointsToSetSize"] = + json_numbert(std::to_string(points_to_set.size())); json_arrayt points_to_set_json; for(auto p : points_to_set) @@ -159,7 +167,8 @@ exprt value_set_dereferencet::dereference(const exprt &pointer, bool display_poi if(display_points_to_sets) { - json_result["RetainedValuesSetSize"] = json_numbert(std::to_string(points_to_set.size())); + json_result["RetainedValuesSetSize"] = + json_numbert(std::to_string(points_to_set.size())); json_arrayt retained_values_set_json; for(auto &value : retained_values) From 1a7dceae3f924ac8f1dbb63706f01b584f03957f Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Thu, 27 Aug 2020 20:51:24 +0100 Subject: [PATCH 06/15] Pass message handler to display points-to sets data clang format value_set_derefernce.h --- src/goto-symex/symex_clean_expr.cpp | 2 +- src/goto-symex/symex_dereference.cpp | 3 ++- src/pointer-analysis/goto_program_dereference.h | 2 +- src/pointer-analysis/value_set_dereference.cpp | 2 +- src/pointer-analysis/value_set_dereference.h | 17 +++++++++++------ 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 6a66563156f..49899889f5d 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -134,7 +134,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr) symex_dereference_statet symex_dereference_state(state, ns); value_set_dereferencet dereference( - ns, state.symbol_table, symex_dereference_state, language_mode, false); + ns, state.symbol_table, symex_dereference_state, language_mode, false, log); expr = dereference.dereference(expr, symex_config.show_points_to_sets); lift_lets(state, expr); diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index a57a141d884..65068e9025d 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -264,7 +264,8 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) state.symbol_table, symex_dereference_state, language_mode, - expr_is_not_null); + expr_is_not_null, + log); // std::cout << "**** " << format(tmp1) << '\n'; exprt tmp2 = diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h index 53a35f85f02..236b80c796a 100644 --- a/src/pointer-analysis/goto_program_dereference.h +++ b/src/pointer-analysis/goto_program_dereference.h @@ -36,7 +36,7 @@ class goto_program_dereferencet:protected dereference_callbackt : options(_options), ns(_ns), value_sets(_value_sets), - dereference(_ns, _new_symbol_table, *this, ID_nil, false) + dereference(_ns, _new_symbol_table, *this, ID_nil, false, messaget()) { } diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 1273a5ea061..d6116d145b8 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -276,7 +276,7 @@ exprt value_set_dereferencet::dereference( ss << format(value); json_result["Value"] = json_stringt(ss.str()); - std::cout << ",\n" << json_result; + log.status() << json_result; } #ifdef DEBUG diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index c37de21f2e2..d3ed72f724d 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include "dereference_callback.h" @@ -34,17 +35,20 @@ class value_set_dereferencet final /// dereference failure /// \param _exclude_null_derefs: Ignore value-set entries that indicate a // given dereference may follow a null pointer + /// \param _log: Messaget object for displaying points-to set value_set_dereferencet( const namespacet &_ns, symbol_tablet &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, - bool _exclude_null_derefs): - ns(_ns), - new_symbol_table(_new_symbol_table), - dereference_callback(_dereference_callback), - language_mode(_language_mode), - exclude_null_derefs(_exclude_null_derefs) + bool _exclude_null_derefs, + const messaget &_log) + : ns(_ns), + new_symbol_table(_new_symbol_table), + dereference_callback(_dereference_callback), + language_mode(_language_mode), + exclude_null_derefs(_exclude_null_derefs), + log(_log) { } virtual ~value_set_dereferencet() { } @@ -106,6 +110,7 @@ class value_set_dereferencet final /// Flag indicating whether `value_set_dereferencet::dereference` should /// disregard an apparent attempt to dereference NULL const bool exclude_null_derefs; + const messaget &log; }; #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H From ad928a6ed466155999da5ae30937f10ed5d743bf Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:50:13 +0100 Subject: [PATCH 07/15] Add parse option to display points-to set information for pointer dereference The points to set information provides some intuition about the complexity of the resulting case split expression in case of a pointer dereference. This commit adds parse option --show-points-to-sets to track the size and contents of the points-to set for pointers. cpp lint bmc_util.h --- src/goto-checker/bmc_util.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index f89f46cff83..93badb40fe5 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -204,7 +204,8 @@ void run_property_decider( " --show-symex-strategies list strategies for use with --paths\n" \ " --show-goto-symex-steps show which steps symex travels, includes " \ " diagnostic information\n" \ - " --show-points-to-sets show points-to sets for pointer dereference\n" \ + " --show-points-to-sets show points-to sets for\n" \ + " pointer dereference\n" \ " --program-only only show program expression\n" \ " --show-byte-ops show all byte extracts and updates\n" \ " --show-loops show the loops in the program\n" \ From cafc1435a52162333ca3d849227c6300d696f03b Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 28 Aug 2020 10:18:58 +0100 Subject: [PATCH 08/15] clang format regression test --- regression/cbmc/points-to-sets/main.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/regression/cbmc/points-to-sets/main.c b/regression/cbmc/points-to-sets/main.c index 7446a031b04..70e4856e45a 100644 --- a/regression/cbmc/points-to-sets/main.c +++ b/regression/cbmc/points-to-sets/main.c @@ -1,9 +1,9 @@ int main() { - unsigned int value; - int *p = (int *) value; + unsigned int value; + int *p = (int *)value; - *p = *p + 1; - assert(1); - return 0; + *p = *p + 1; + assert(1); + return 0; } From e7fb35efde3f11298fb16a45053091280de2c592 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 28 Aug 2020 10:18:58 +0100 Subject: [PATCH 09/15] clang format regression test Add regression test for xml and plain output --- regression/cbmc/points-to-sets/test.desc | 13 ++++++++----- regression/cbmc/points-to-sets/test_json.desc | 11 +++++++++++ regression/cbmc/points-to-sets/test_xml.desc | 13 +++++++++++++ 3 files changed, 32 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc/points-to-sets/test_json.desc create mode 100644 regression/cbmc/points-to-sets/test_xml.desc diff --git a/regression/cbmc/points-to-sets/test.desc b/regression/cbmc/points-to-sets/test.desc index dfc82630769..85ef0488987 100644 --- a/regression/cbmc/points-to-sets/test.desc +++ b/regression/cbmc/points-to-sets/test.desc @@ -1,10 +1,13 @@ CORE main.c ---show-points-to-sets --json-ui -activate-multi-line-match -^EXIT=0$ +--show-points-to-sets +^EXIT=(0|127|134|137)$ ^SIGNAL=0$ -\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\} +--- begin invariant violation report --- +Invariant check failed +Condition: false +Reason: Cannot print json data on PLAIN UI -- -- -To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. \ No newline at end of file +To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. +xml-ui and plain output not supported. diff --git a/regression/cbmc/points-to-sets/test_json.desc b/regression/cbmc/points-to-sets/test_json.desc new file mode 100644 index 00000000000..3e62c77d638 --- /dev/null +++ b/regression/cbmc/points-to-sets/test_json.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show-points-to-sets --json-ui +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\} +-- +-- +To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. +xml-ui and plain output not supported. diff --git a/regression/cbmc/points-to-sets/test_xml.desc b/regression/cbmc/points-to-sets/test_xml.desc new file mode 100644 index 00000000000..a8cf15965fe --- /dev/null +++ b/regression/cbmc/points-to-sets/test_xml.desc @@ -0,0 +1,13 @@ +CORE +main.c +--show-points-to-sets --xml-ui +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +Invariant check failed +Condition: false +Reason: Cannot print json data on XML UI +-- +-- +To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. +xml-ui and plain output not supported. From 92a5b759729bae57aa5e6cfd2afb47a80eec80ea Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:50:13 +0100 Subject: [PATCH 10/15] Add parse option to display points-to set information for pointer dereference The points to set information provides some intuition about the complexity of the resulting case split expression in case of a pointer dereference. This commit adds parse option --show-points-to-sets to track the size and contents of the points-to set for pointers. cpp lint bmc_util.h Add error message for plain and xml format output --- src/cbmc/cbmc_parse_options.cpp | 9 +++++++++ src/goto-checker/bmc_util.h | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b59d98aa26a..e30eb51b3ad 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -522,7 +522,16 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-goto-symex-steps", true); if(cmdline.isset("show-points-to-sets")) + { + if(!cmdline.isset("json-ui")) + { + log.error() << "--show-points-to-sets supports only" + " json output. Use --json-ui." + << messaget::eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } options.set_option("show-points-to-sets", true); + } PARSE_OPTIONS_GOTO_TRACE(cmdline, options); } diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 93badb40fe5..f12c07f72b6 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -205,7 +205,7 @@ void run_property_decider( " --show-goto-symex-steps show which steps symex travels, includes " \ " diagnostic information\n" \ " --show-points-to-sets show points-to sets for\n" \ - " pointer dereference\n" \ + " pointer dereference. Requires --json-ui.\n" \ " --program-only only show program expression\n" \ " --show-byte-ops show all byte extracts and updates\n" \ " --show-loops show the loops in the program\n" \ From c1444c9ba8e101b9a073670016a332f70cf9c51a Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Fri, 28 Aug 2020 10:18:58 +0100 Subject: [PATCH 11/15] clang format regression test --- regression/cbmc/points-to-sets/test.desc | 6 +----- regression/cbmc/points-to-sets/test_xml.desc | 6 +----- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/regression/cbmc/points-to-sets/test.desc b/regression/cbmc/points-to-sets/test.desc index 85ef0488987..e95a06651d8 100644 --- a/regression/cbmc/points-to-sets/test.desc +++ b/regression/cbmc/points-to-sets/test.desc @@ -1,12 +1,8 @@ CORE main.c --show-points-to-sets -^EXIT=(0|127|134|137)$ +^EXIT=1$ ^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Condition: false -Reason: Cannot print json data on PLAIN UI -- -- To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. diff --git a/regression/cbmc/points-to-sets/test_xml.desc b/regression/cbmc/points-to-sets/test_xml.desc index a8cf15965fe..d4bf269cbb3 100644 --- a/regression/cbmc/points-to-sets/test_xml.desc +++ b/regression/cbmc/points-to-sets/test_xml.desc @@ -1,12 +1,8 @@ CORE main.c --show-points-to-sets --xml-ui -^EXIT=(0|127|134|137)$ +^EXIT=1$ ^SIGNAL=0$ ---- begin invariant violation report --- -Invariant check failed -Condition: false -Reason: Cannot print json data on XML UI -- -- To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format. From 4642ec7731b71a1f56ec26d795acb08efc89fd87 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:50:13 +0100 Subject: [PATCH 12/15] Add parse option to display points-to set information for pointer dereference The points to set information provides some intuition about the complexity of the resulting case split expression in case of a pointer dereference. This commit adds parse option --show-points-to-sets to track the size and contents of the points-to set for pointers. cpp lint bmc_util.h Add error message for plain and xml format output --- src/cbmc/cbmc_parse_options.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e30eb51b3ad..8652db6bba9 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -575,6 +575,17 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_USAGE_ERROR; } + if(cmdline.isset("show-points-to-sets")) + { + if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui")) + { + log.error() << "--show-points-to-sets supports only" + " json output. Use --json-ui." + << messaget::eom; + return CPROVER_EXIT_USAGE_ERROR; + } + } + register_languages(); // configure gcc, if required From 96c6ac8d0aa92c6132d782851bc5bca72d6470ee Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 2 Sep 2020 23:46:27 +0100 Subject: [PATCH 13/15] Fix parse options handling for --show-points-to-sets --- src/cbmc/cbmc_parse_options.cpp | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8652db6bba9..624c9d5070f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -522,16 +522,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-goto-symex-steps", true); if(cmdline.isset("show-points-to-sets")) - { - if(!cmdline.isset("json-ui")) - { - log.error() << "--show-points-to-sets supports only" - " json output. Use --json-ui." - << messaget::eom; - exit(CPROVER_EXIT_USAGE_ERROR); - } options.set_option("show-points-to-sets", true); - } PARSE_OPTIONS_GOTO_TRACE(cmdline, options); } From 7c70957350c4a190662a7fa6aefcb474e5bdba81 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Thu, 24 Sep 2020 13:58:38 +0100 Subject: [PATCH 14/15] fix #ifdef DEBUG in headers, keep iostream inside DEBUG tags --- src/pointer-analysis/value_set_dereference.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index d6116d145b8..404fb0e1580 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -11,9 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "value_set_dereference.h" +#ifdef DEBUG #include -#include -#include +#endif #include #include @@ -23,8 +23,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include +#include #include #include #include From f179946b7ac106dfed39367b05c835980d87c4fe Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Thu, 24 Sep 2020 13:59:58 +0100 Subject: [PATCH 15/15] Add comment explaining the use if default messaget instance in goto_program_dereferencet --- src/pointer-analysis/goto_program_dereference.h | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h index 236b80c796a..a26a374dc7b 100644 --- a/src/pointer-analysis/goto_program_dereference.h +++ b/src/pointer-analysis/goto_program_dereference.h @@ -28,15 +28,24 @@ class goto_program_dereferencet:protected dereference_callbackt // for the final argument to value_set_dereferencet. // This means that language-inappropriate values such as // (struct A*)some_integer_value in Java, may be returned. + // Note: value_set_dereferencet requires a messaget instance + // as on of its arguments to display the points-to set + // during symex. Display is not done during goto-program + // conversion. To ensure this the display_points_to_sets + // parameter in value_set_dereferencet::dereference() + // is set to false by default and is not changed by the + // goto program conversion modules. Similarly, here we set + // _log to be a default messaget instance. goto_program_dereferencet( const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, - value_setst &_value_sets) + value_setst &_value_sets, + const messaget &_log = messaget()) : options(_options), ns(_ns), value_sets(_value_sets), - dereference(_ns, _new_symbol_table, *this, ID_nil, false, messaget()) + dereference(_ns, _new_symbol_table, *this, ID_nil, false, _log) { }