From c46f1621ef98def07ee642895ee529e807f7cc15 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:23:12 +0100 Subject: [PATCH 1/7] Add building fresh symbols for snapshot temporaries This is needed for example when referring to malloc(ed) variables. These are build as pointing to `tmp` variables. --- .../memory_snapshot_harness_generator.cpp | 40 ++++++++++++++++--- .../memory_snapshot_harness_generator.h | 13 +++++- 2 files changed, 47 insertions(+), 6 deletions(-) diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index b313e8fdc80..324a3b69bcb 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -131,6 +131,23 @@ void memory_snapshot_harness_generatort::add_init_section( goto_program.const_cast_target(entry_location.start_instruction))); } +const symbolt &memory_snapshot_harness_generatort::fresh_symbol_copy( + const symbolt &snapshot_symbol, + symbol_tablet &symbol_table) const +{ + symbolt &tmp_symbol = get_fresh_aux_symbol( + snapshot_symbol.type, + "", // no prefix name + id2string(snapshot_symbol.base_name), + snapshot_symbol.location, + snapshot_symbol.mode, + symbol_table); + tmp_symbol.is_static_lifetime = true; + tmp_symbol.value = snapshot_symbol.value; + + return tmp_symbol; +} + code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals( const symbol_tablet &snapshot, goto_modelt &goto_model) const @@ -141,17 +158,30 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals( code_blockt code; for(const auto &pair : snapshot) { - const symbolt &symbol = pair.second; - if(!symbol.is_static_lifetime) + const symbolt &snapshot_symbol = pair.second; + symbol_tablet &symbol_table = goto_model.symbol_table; + + auto should_get_fresh = [&symbol_table](const symbolt &symbol) { + return symbol_table.lookup(symbol.base_name) == nullptr && + !symbol.is_type; + }; + const symbolt &fresh_or_snapshot_symbol = + should_get_fresh(snapshot_symbol) + ? fresh_symbol_copy(snapshot_symbol, symbol_table) + : snapshot_symbol; + + if(!fresh_or_snapshot_symbol.is_static_lifetime) continue; - if(variables_to_havoc.count(symbol.base_name) == 0) + if(variables_to_havoc.count(fresh_or_snapshot_symbol.base_name) == 0) { - code.add(code_assignt{symbol.symbol_expr(), symbol.value}); + code.add(code_assignt{fresh_or_snapshot_symbol.symbol_expr(), + fresh_or_snapshot_symbol.value}); } else { - recursive_initialization.initialize(symbol.symbol_expr(), 0, {}, code); + recursive_initialization.initialize( + fresh_or_snapshot_symbol.symbol_expr(), 0, {}, code); } } return code; diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index 80181ff0305..1a62d3ec15d 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -221,12 +221,23 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort const symbol_exprt &func_init_done_var, goto_modelt &goto_model) const; + /// Introduce a new symbol into \p symbol_table with the same name and type as + /// \p snapshot_symbol + /// \param snapshot_symbol: the unknown symbol to be introduced + /// \param symbol_table: the symbol table to be updated + /// \return the new symbol + const symbolt &fresh_symbol_copy( + const symbolt &snapshot_symbol, + symbol_tablet &symbol_table) const; + /// For each global symbol in the \p snapshot symbol table either: /// 1) add \ref code_assignt assigning a value from the \p snapshot to the /// symbol /// or /// 2) recursively initialise the symbol to a non-deterministic value of the - /// right type + /// right type. + /// Malloc(ed) pointers point to temporaries which do not exists in the symbol + /// table: for these we introduce fresh symbols. /// \param snapshot: snapshot to load the symbols and their values from /// \param goto_model: model to initialise the havoc-ing /// \return the block of code where the assignments are added From fc87e91a7eb9c100c3bcda18dd6ea175f1f6690c Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:31:06 +0100 Subject: [PATCH 2/7] Add helper for querying offset to pointer_valuet. --- src/memory-analyzer/gdb_api.h | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 6f065c6b47c..1312bebe6fb 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -19,6 +19,7 @@ Author: Malte Mues #define CPROVER_MEMORY_ANALYZER_GDB_API_H #include +#include #include #include @@ -81,6 +82,12 @@ class gdb_apit const std::string pointee; const std::string character; const optionalt string; + + bool has_known_offset() const + { + return std::any_of( + pointee.begin(), pointee.end(), [](char c) { return c == '+'; }); + } }; /// Create a new gdb process for analysing the binary indicated by the member From f060e8614c867bf43ed0e716c8428eb72c6e7ff8 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:31:59 +0100 Subject: [PATCH 3/7] Make pointers-to-member work Change the memory-analyze to produce correct member expressions. Iterate over the offset from gdb, e.g. `st+4` means jump to the second member component inside `st`. --- src/memory-analyzer/analyze_symbol.cpp | 100 ++++++++++++++++++++++++- src/memory-analyzer/analyze_symbol.h | 18 +++++ 2 files changed, 117 insertions(+), 1 deletion(-) diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 30cca4b4010..efcddf6a238 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -13,7 +13,10 @@ Author: Malte Mues #include #include #include +#include +#include #include +#include gdb_value_extractort::gdb_value_extractort( const symbol_tablet &symbol_table, @@ -165,6 +168,84 @@ exprt gdb_value_extractort::get_char_pointer_value( } } +exprt gdb_value_extractort::get_pointer_to_member_value( + const exprt &expr, + const pointer_valuet &pointer_value, + const source_locationt &location) +{ + PRECONDITION(expr.type().id() == ID_pointer); + PRECONDITION(!is_c_char_type(expr.type().subtype())); + const auto &memory_location = pointer_value.address; + std::string memory_location_string = memory_location.string(); + PRECONDITION(memory_location_string != "0x0"); + PRECONDITION(!pointer_value.pointee.empty()); + + std::string struct_name; + size_t member_offset; + if(pointer_value.has_known_offset()) + { + std::string member_offset_string; + split_string( + pointer_value.pointee, '+', struct_name, member_offset_string, true); + member_offset = safe_string2size_t(member_offset_string); + } + else + { + struct_name = pointer_value.pointee; + member_offset = 0; + } + + const symbolt *struct_symbol = symbol_table.lookup(struct_name); + DATA_INVARIANT(struct_symbol != nullptr, "unknown struct"); + const auto maybe_struct_size = + pointer_offset_size(struct_symbol->symbol_expr().type(), ns); + bool found = false; + CHECK_RETURN(maybe_struct_size.has_value()); + for(const auto &value_pair : values) + { + const auto &value_symbol_expr = value_pair.second; + if(to_symbol_expr(value_symbol_expr).get_identifier() == struct_name) + { + found = true; + break; + } + } + + if(!found) + { + const typet target_type = expr.type().subtype(); + + symbol_exprt dummy("tmp", expr.type()); + code_blockt assignments; + + auto emplace_pair = values.emplace( + memory_location, + allocate_objects.allocate_automatic_local_object( + assignments, dummy, target_type)); + const symbol_exprt &new_symbol = to_symbol_expr(emplace_pair.first->second); + + dereference_exprt dereference_expr(expr); + + const auto zero_expr = zero_initializer(target_type, location, ns); + CHECK_RETURN(zero_expr); + + // add assignment of value to newly created symbol + add_assignment(new_symbol, *zero_expr); + + const auto &struct_symbol = values.find(memory_location); + + const auto maybe_member_expr = get_subexpression_at_offset( + struct_symbol->second, member_offset, expr.type().subtype(), ns); + CHECK_RETURN(maybe_member_expr.has_value()); + return *maybe_member_expr; + } + + const auto maybe_member_expr = get_subexpression_at_offset( + struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns); + CHECK_RETURN(maybe_member_expr.has_value()); + return *maybe_member_expr; +} + exprt gdb_value_extractort::get_non_char_pointer_value( const exprt &expr, const memory_addresst &memory_location, @@ -210,6 +291,21 @@ exprt gdb_value_extractort::get_non_char_pointer_value( } } +bool gdb_value_extractort::points_to_member( + const pointer_valuet &pointer_value) const +{ + if(pointer_value.has_known_offset()) + return true; + + const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee); + if(pointee_symbol == nullptr) + return false; + const auto &pointee_type = pointee_symbol->type; + return pointee_type.id() == ID_struct_tag || + pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array || + pointee_type.id() == ID_struct || pointee_type.id() == ID_union; +} + exprt gdb_value_extractort::get_pointer_value( const exprt &expr, const exprt &zero_expr, @@ -234,7 +330,9 @@ exprt gdb_value_extractort::get_pointer_value( else { const exprt target_expr = - get_non_char_pointer_value(expr, memory_location, location); + points_to_member(value) + ? get_pointer_to_member_value(expr, value, location) + : get_non_char_pointer_value(expr, memory_location, location); if(target_expr.id() == ID_nil) { diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h index 8339c84a81f..0df437e3a36 100644 --- a/src/memory-analyzer/analyze_symbol.h +++ b/src/memory-analyzer/analyze_symbol.h @@ -150,6 +150,18 @@ class gdb_value_extractort const exprt &zero_expr, const source_locationt &location); + /// Call \ref get_subexpression_at_offset to get the correct member + /// expression. + /// \param expr: the input pointer expression (needed to get the right type) + /// \param pointer_value: pointer value with structure name and offset as the + /// pointee member + /// \param location: the source location + /// \return \ref member_exprt that the \p pointer_value points to + exprt get_pointer_to_member_value( + const exprt &expr, + const pointer_valuet &pointer_value, + const source_locationt &location); + /// Similar to \ref get_char_pointer_value. Doesn't re-call /// \ref gdb_apit::get_memory, calls \ref get_expr_value on _dereferenced_ /// \p expr (the result of which is assigned to a new symbol). @@ -184,6 +196,12 @@ class gdb_value_extractort /// \param expr: expression to be extracted /// \return the value as a string std::string get_gdb_value(const exprt &expr); + + /// Analyzes the \p pointer_value to decide if it point to a struct or a + /// union (or array) + /// \param pointer_value: pointer value to be analyzed + /// \return true if pointing to a member + bool points_to_member(const pointer_valuet &pointer_value) const; }; #endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H From be9d5b17d4150b401ea1af3a6169e185b9539a55 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:32:27 +0100 Subject: [PATCH 4/7] Implement union values Reuse get_struct_member for unions (copy-paste). --- src/memory-analyzer/analyze_symbol.cpp | 28 +++++++++++++++++++++++++- src/memory-analyzer/analyze_symbol.h | 10 +++++++++ 2 files changed, 37 insertions(+), 1 deletion(-) diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index efcddf6a238..d0a4cbc6037 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -421,7 +421,11 @@ exprt gdb_value_extractort::get_expr_value( return get_pointer_value(expr, zero_expr, location); } - UNIMPLEMENTED; + else if(type.id() == ID_union_tag) + { + return get_union_value(expr, zero_expr, location); + } + UNREACHABLE; } exprt gdb_value_extractort::get_struct_value( @@ -457,6 +461,28 @@ exprt gdb_value_extractort::get_struct_value( return new_expr; } +exprt gdb_value_extractort::get_union_value( + const exprt &expr, + const exprt &zero_expr, + const source_locationt &location) +{ + PRECONDITION(zero_expr.id() == ID_union); + + PRECONDITION(expr.type().id() == ID_union_tag); + PRECONDITION(expr.type() == zero_expr.type()); + + exprt new_expr(zero_expr); + + const union_tag_typet &union_tag_type = to_union_tag_type(expr.type()); + const union_typet &union_type = ns.follow_tag(union_tag_type); + + CHECK_RETURN(new_expr.operands().size() == 1); + const union_typet::componentt &component = union_type.components()[0]; + auto &operand = new_expr.operands()[0]; + operand = get_expr_value(member_exprt{expr, component}, operand, location); + return new_expr; +} + void gdb_value_extractort::process_outstanding_assignments() { for(const auto &pair : outstanding_assignments) diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h index 0df437e3a36..1a199b2e5c7 100644 --- a/src/memory-analyzer/analyze_symbol.h +++ b/src/memory-analyzer/analyze_symbol.h @@ -138,6 +138,16 @@ class gdb_value_extractort const exprt &zero_expr, const source_locationt &location); + /// For each of the members of the struct: call \ref get_expr_value + /// \param expr: struct expression to be analysed + /// \param zero_expr: struct with zero-initialised members + /// \param location: the source location + /// \return the value of the struct from \ref gdb_apit + exprt get_union_value( + const exprt &expr, + const exprt &zero_expr, + const source_locationt &location); + /// Call \ref gdb_apit::get_memory on \p expr then split based on the /// points-to type being `char` type or not. These have dedicated functions. /// \param expr: the input pointer expression From bd1e41d6297ede59d07d024c8d3f5776c172cee4 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:34:41 +0100 Subject: [PATCH 5/7] Add and check type of pointees in memory analyzer GDB does not know (the CBMC) types but the resulting symbol table requires them. We only do this for non-nil ireps (nil ireps can result from getting pointer values for dynamically allocated memory -- will be addressed in later PRs). Also prevents catch-by-value error when compiled with gcc-8. --- src/memory-analyzer/analyze_symbol.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index d0a4cbc6037..7e73e7905f2 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -287,7 +287,14 @@ exprt gdb_value_extractort::get_non_char_pointer_value( } else { - return it->second; + const auto &known_value = it->second; + const auto &expected_type = expr.type().subtype(); + if(known_value.is_not_nil() && known_value.type() != expected_type) + { + return symbol_exprt{to_symbol_expr(known_value).get_identifier(), + expected_type}; + } + return known_value; } } @@ -340,7 +347,9 @@ exprt gdb_value_extractort::get_pointer_value( } else { - return address_of_exprt(target_expr); + const auto result_expr = address_of_exprt(target_expr); + CHECK_RETURN(result_expr.type() == zero_expr.type()); + return result_expr; } } } From dc19f1a9dc8cb8f7b9d5a248ba2ac946ea5772c7 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:36:46 +0100 Subject: [PATCH 6/7] Change the expected output of a regression test but I think is a bit more meaningful now. We do not actually see the value of `p->next` but at least it is consistent (before `p->next` was different from `tmp.next`). --- regression/memory-analyzer/pointer_to_struct_01/test.desc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/regression/memory-analyzer/pointer_to_struct_01/test.desc b/regression/memory-analyzer/pointer_to_struct_01/test.desc index 5e4a6c22c21..17dd6abb2d5 100644 --- a/regression/memory-analyzer/pointer_to_struct_01/test.desc +++ b/regression/memory-analyzer/pointer_to_struct_01/test.desc @@ -2,8 +2,7 @@ CORE main.gb --breakpoint checkpoint --symbols p struct S tmp; -tmp = \{ \.next=\(\(struct S \*\)(NULL|0)\) \}; -p = &tmp; -p->next = &tmp; +tmp = \{ \.next=\(\(struct S \*\)0\) \}; +p = \&tmp; ^EXIT=0$ ^SIGNAL=0$ From e961c89b9f14fbc0acd1c61948615031c2017e87 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:41:53 +0100 Subject: [PATCH 7/7] Add regression tests for snapshot-harness These call memory-analyzer to produce the JSON snapshots and then build the harness similarly to how goto-harness tests work. We currently tests structs, unions, arrays and pointers to all of those. --- regression/CMakeLists.txt | 3 +- regression/Makefile | 3 +- regression/snapshot-harness/CMakeLists.txt | 7 ++++ regression/snapshot-harness/Makefile | 26 ++++++++++++++ regression/snapshot-harness/arrays_01/main.c | 29 ++++++++++++++++ .../snapshot-harness/arrays_01/test.desc | 13 +++++++ regression/snapshot-harness/chain.sh | 32 +++++++++++++++++ regression/snapshot-harness/pointer_01/main.c | 22 ++++++++++++ .../snapshot-harness/pointer_01/test.desc | 9 +++++ regression/snapshot-harness/pointer_02/main.c | 32 +++++++++++++++++ .../snapshot-harness/pointer_02/test.desc | 12 +++++++ regression/snapshot-harness/pointer_03/main.c | 24 +++++++++++++ .../snapshot-harness/pointer_03/test.desc | 8 +++++ regression/snapshot-harness/pointer_04/main.c | 30 ++++++++++++++++ .../snapshot-harness/pointer_04/test.desc | 12 +++++++ regression/snapshot-harness/pointer_05/main.c | 24 +++++++++++++ .../snapshot-harness/pointer_05/test.desc | 9 +++++ regression/snapshot-harness/pointer_06/main.c | 23 +++++++++++++ .../snapshot-harness/pointer_06/test.desc | 9 +++++ .../pointer_to_struct_01/main.c | 34 +++++++++++++++++++ .../pointer_to_struct_01/test.desc | 12 +++++++ regression/snapshot-harness/structs_01/main.c | 32 +++++++++++++++++ .../snapshot-harness/structs_01/test.desc | 12 +++++++ regression/snapshot-harness/union_01/main.c | 31 +++++++++++++++++ .../snapshot-harness/union_01/test.desc | 11 ++++++ 25 files changed, 457 insertions(+), 2 deletions(-) create mode 100644 regression/snapshot-harness/CMakeLists.txt create mode 100644 regression/snapshot-harness/Makefile create mode 100644 regression/snapshot-harness/arrays_01/main.c create mode 100644 regression/snapshot-harness/arrays_01/test.desc create mode 100755 regression/snapshot-harness/chain.sh create mode 100644 regression/snapshot-harness/pointer_01/main.c create mode 100644 regression/snapshot-harness/pointer_01/test.desc create mode 100644 regression/snapshot-harness/pointer_02/main.c create mode 100644 regression/snapshot-harness/pointer_02/test.desc create mode 100644 regression/snapshot-harness/pointer_03/main.c create mode 100644 regression/snapshot-harness/pointer_03/test.desc create mode 100644 regression/snapshot-harness/pointer_04/main.c create mode 100644 regression/snapshot-harness/pointer_04/test.desc create mode 100644 regression/snapshot-harness/pointer_05/main.c create mode 100644 regression/snapshot-harness/pointer_05/test.desc create mode 100644 regression/snapshot-harness/pointer_06/main.c create mode 100644 regression/snapshot-harness/pointer_06/test.desc create mode 100644 regression/snapshot-harness/pointer_to_struct_01/main.c create mode 100644 regression/snapshot-harness/pointer_to_struct_01/test.desc create mode 100644 regression/snapshot-harness/structs_01/main.c create mode 100644 regression/snapshot-harness/structs_01/test.desc create mode 100644 regression/snapshot-harness/union_01/main.c create mode 100644 regression/snapshot-harness/union_01/test.desc diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index fd75d83a4d9..b47c8e5d6ba 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -55,5 +55,6 @@ add_subdirectory(linking-goto-binaries) add_subdirectory(symtab2gb) if(WITH_MEMORY_ANALYZER) -add_subdirectory(memory-analyzer) + add_subdirectory(snapshot-harness) + add_subdirectory(memory-analyzer) endif() diff --git a/regression/Makefile b/regression/Makefile index 2624eb99421..3742ce83e47 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -44,7 +44,8 @@ ifeq ($(detected_OS),Linux) endif ifeq ($(WITH_MEMORY_ANALYZER),1) - DIRS += memory-analyzer + DIRS += snapshot-harness \ + memory-analyzer endif # Run all test directories in sequence diff --git a/regression/snapshot-harness/CMakeLists.txt b/regression/snapshot-harness/CMakeLists.txt new file mode 100644 index 00000000000..e4247acf556 --- /dev/null +++ b/regression/snapshot-harness/CMakeLists.txt @@ -0,0 +1,7 @@ +add_test_pl_tests( + "../chain.sh \ + $ \ + $ \ + $ \ + $ \ + ../../../build/bin/goto-gcc") diff --git a/regression/snapshot-harness/Makefile b/regression/snapshot-harness/Makefile new file mode 100644 index 00000000000..8bb6a0c5c5f --- /dev/null +++ b/regression/snapshot-harness/Makefile @@ -0,0 +1,26 @@ +default: tests.log + +MEMORY_ANALYZER_EXE=../../../src/memory-analyzer/memory-analyzer +GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness +CBMC_EXE=../../../src/cbmc/cbmc +GOTO_CC_EXE=../../../src/goto-cc/goto-cc +GOTO_GCC_EXE=../../../src/goto-cc/goto-gcc + +test: + @../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(MEMORY_ANALYZER_EXE) $(CBMC_EXE) $(GOTO_GCC_EXE)" + +tests.log: ../test.pl + @../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(MEMORY_ANALYZER_EXE) $(CBMC_EXE) $(GOTO_GCC_EXE)" + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + find -name '*.json' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/snapshot-harness/arrays_01/main.c b/regression/snapshot-harness/arrays_01/main.c new file mode 100644 index 00000000000..60700a22f35 --- /dev/null +++ b/regression/snapshot-harness/arrays_01/main.c @@ -0,0 +1,29 @@ +#include + +int array[] = {1, 2, 3}; +int *p; +int *q; + +void initialize() +{ + p = &(array[1]); + q = array + 1; + array[0] = 4; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p == &(array[1])); + assert(p == q); + assert(*p == *q); + assert(array[0] != *p); + *p = 4; + assert(array[0] == *p); +} diff --git a/regression/snapshot-harness/arrays_01/test.desc b/regression/snapshot-harness/arrays_01/test.desc new file mode 100644 index 00000000000..e89b75dbb1c --- /dev/null +++ b/regression/snapshot-harness/arrays_01/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p == \&\(array\[1\]\): SUCCESS +\[main.assertion.2\] line [0-9]+ assertion p == q: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p == \*q: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion array\[0\] != \*p: SUCCESS +\[main.assertion.5\] line [0-9]+ assertion array\[0\] == \*p: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/chain.sh b/regression/snapshot-harness/chain.sh new file mode 100755 index 00000000000..b5b5d6957e3 --- /dev/null +++ b/regression/snapshot-harness/chain.sh @@ -0,0 +1,32 @@ +#!/bin/bash + +set -e + +goto_cc=$1 +goto_harness=$2 +memory_analyzer=$3 +cbmc=$4 +goto_gcc=$5 +entry_point='generated_entry_function' +break_point='checkpoint' + +name=${*:$#} +name=${name%.c} +memory_analyzer_symbols=$6 +goto_harness_args=${*:7:$#-7} + +$goto_cc -o "${name}_cc.gb" "${name}.c" +$goto_gcc -g -std=c11 -o "${name}_gcc.gb" "${name}.c" + +$memory_analyzer --symtab-snapshot --json-ui --breakpoint $break_point --symbols ${memory_analyzer_symbols} "${name}_gcc.gb" > "${name}.json" + +if [ -e "${name}-mod.gb" ] ; then + rm -f "${name}-mod.gb" +fi + +$goto_harness "${name}_cc.gb" "${name}-mod.gb" --harness-function-name $entry_point --memory-snapshot "${name}.json" ${goto_harness_args} +$cbmc --function $entry_point "${name}-mod.gb" \ + --pointer-check `# because we want to see out of bounds errors` \ + --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \ + --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \ + # cbmc args end diff --git a/regression/snapshot-harness/pointer_01/main.c b/regression/snapshot-harness/pointer_01/main.c new file mode 100644 index 00000000000..3c04349bbf3 --- /dev/null +++ b/regression/snapshot-harness/pointer_01/main.c @@ -0,0 +1,22 @@ +#include + +int x; +int *p; + +void initialize() +{ + x = 3; + p = &x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*p == x); +} diff --git a/regression/snapshot-harness/pointer_01/test.desc b/regression/snapshot-harness/pointer_01/test.desc new file mode 100644 index 00000000000..4e6490db712 --- /dev/null +++ b/regression/snapshot-harness/pointer_01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*p == x: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_02/main.c b/regression/snapshot-harness/pointer_02/main.c new file mode 100644 index 00000000000..13502cae8f9 --- /dev/null +++ b/regression/snapshot-harness/pointer_02/main.c @@ -0,0 +1,32 @@ +#include +#include + +int x; +int *p1; +int *p2; +int *p3; + +void initialize() +{ + x = 3; + p1 = malloc(sizeof(int)); + p3 = malloc(sizeof(int)); + p2 = &x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*p2 == x); + assert(p1 != p2); + assert(p1 != p3); + assert(*p1 == x); + *p1 = x; + assert(*p1 == x); +} diff --git a/regression/snapshot-harness/pointer_02/test.desc b/regression/snapshot-harness/pointer_02/test.desc new file mode 100644 index 00000000000..5e6f5fdf768 --- /dev/null +++ b/regression/snapshot-harness/pointer_02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*p2 == x: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion p1 != p2: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion p1 != p3: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion \*p1 == x: FAILURE +\[main.assertion.5\] line [0-9]+ assertion \*p1 == x: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_03/main.c b/regression/snapshot-harness/pointer_03/main.c new file mode 100644 index 00000000000..44c9edf6aa1 --- /dev/null +++ b/regression/snapshot-harness/pointer_03/main.c @@ -0,0 +1,24 @@ +#include + +int x; +void *p; + +void initialize() +{ + x = 3; + p = (void *)&x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*(int *)p == 3); + + return 0; +} diff --git a/regression/snapshot-harness/pointer_03/test.desc b/regression/snapshot-harness/pointer_03/test.desc new file mode 100644 index 00000000000..1f29edb3dfc --- /dev/null +++ b/regression/snapshot-harness/pointer_03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*\(int \*\)p == 3: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_04/main.c b/regression/snapshot-harness/pointer_04/main.c new file mode 100644 index 00000000000..29950c318a8 --- /dev/null +++ b/regression/snapshot-harness/pointer_04/main.c @@ -0,0 +1,30 @@ +#include + +int x; +int *p1; +int **p2; + +void initialize() +{ + x = 3; + p1 = &x; + p2 = &p1; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(&p1 == *p2); + assert(*p2 == p1); + assert(*p1 == 3); + assert(*p2 == &x); + assert(**p2 == x); + + return 0; +} diff --git a/regression/snapshot-harness/pointer_04/test.desc b/regression/snapshot-harness/pointer_04/test.desc new file mode 100644 index 00000000000..c4025bb0f99 --- /dev/null +++ b/regression/snapshot-harness/pointer_04/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \&p1 == \*p2: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \*p2 == p1: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p1 == 3: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion \*p2 == \&x: SUCCESS +\[main.assertion.5\] line [0-9]+ assertion \*\*p2 == x: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_05/main.c b/regression/snapshot-harness/pointer_05/main.c new file mode 100644 index 00000000000..8edd9810a23 --- /dev/null +++ b/regression/snapshot-harness/pointer_05/main.c @@ -0,0 +1,24 @@ +#include + +int x; +int *p1; +int *p2; + +void initialize() +{ + x = 3; + p1 = &x; + p2 = &x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*p1 == *p2); +} diff --git a/regression/snapshot-harness/pointer_05/test.desc b/regression/snapshot-harness/pointer_05/test.desc new file mode 100644 index 00000000000..5fbe74f96a9 --- /dev/null +++ b/regression/snapshot-harness/pointer_05/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*p1 == \*p2: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_06/main.c b/regression/snapshot-harness/pointer_06/main.c new file mode 100644 index 00000000000..af0e19c96f3 --- /dev/null +++ b/regression/snapshot-harness/pointer_06/main.c @@ -0,0 +1,23 @@ +#include +#include + +int *p; +int *q; + +void initialize() +{ + p = malloc(sizeof(int)); + q = p; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p == q); +} diff --git a/regression/snapshot-harness/pointer_06/test.desc b/regression/snapshot-harness/pointer_06/test.desc new file mode 100644 index 00000000000..70452f9ad81 --- /dev/null +++ b/regression/snapshot-harness/pointer_06/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_to_struct_01/main.c b/regression/snapshot-harness/pointer_to_struct_01/main.c new file mode 100644 index 00000000000..8238f850be5 --- /dev/null +++ b/regression/snapshot-harness/pointer_to_struct_01/main.c @@ -0,0 +1,34 @@ +#include +#include + +struct S +{ + struct S *next; +}; + +struct S st; +struct S *p; +struct S *q; + +void initialize() +{ + st.next = &st; + p = &st; + q = malloc(sizeof(struct S)); +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p == &st); + assert(p->next == &st); + assert(p != q); + q->next = &st; + assert(p == q->next); +} diff --git a/regression/snapshot-harness/pointer_to_struct_01/test.desc b/regression/snapshot-harness/pointer_to_struct_01/test.desc new file mode 100644 index 00000000000..7574b741544 --- /dev/null +++ b/regression/snapshot-harness/pointer_to_struct_01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p == \&st: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion p-\>next == \&st: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion p \!= q: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion p == q-\>next: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/structs_01/main.c b/regression/snapshot-harness/structs_01/main.c new file mode 100644 index 00000000000..462006577d9 --- /dev/null +++ b/regression/snapshot-harness/structs_01/main.c @@ -0,0 +1,32 @@ +#include + +struct S +{ + int c1; + int c2; +} st; + +int *p; + +void initialize() +{ + st.c1 = 1; + st.c2 = 3; + p = &(st.c2); +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(st.c1 + 2 == st.c2); + assert(st.c1 + 2 == *p); + assert(*p == st.c2); + *p = st.c2 + 1; + assert(*p == st.c2); +} diff --git a/regression/snapshot-harness/structs_01/test.desc b/regression/snapshot-harness/structs_01/test.desc new file mode 100644 index 00000000000..887f6a44483 --- /dev/null +++ b/regression/snapshot-harness/structs_01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion st.c1 \+ 2 == st.c2: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion st.c1 \+ 2 == \*p: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p == st.c2: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion \*p == st.c2: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/union_01/main.c b/regression/snapshot-harness/union_01/main.c new file mode 100644 index 00000000000..127ea571b31 --- /dev/null +++ b/regression/snapshot-harness/union_01/main.c @@ -0,0 +1,31 @@ +#include + +union Un { + int i; + float f; +} un; + +int *ip; +float *fp; + +void initialize() +{ + un.i = 1; + ip = &un.i; + fp = &un.f; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(ip == &un.i); + assert(*ip == un.i); + *fp = 2.0f; + assert(un.f == 2.0f); +} diff --git a/regression/snapshot-harness/union_01/test.desc b/regression/snapshot-harness/union_01/test.desc new file mode 100644 index 00000000000..beefc7d3d76 --- /dev/null +++ b/regression/snapshot-harness/union_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +un,ip,fp --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion ip == \&un.i: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \*ip == un.i: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion un.f == 2.0f: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring