From 13ccc773e20dba04ae74e5f6cf97c2faa08c3159 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 6 Aug 2019 07:32:08 +0100 Subject: [PATCH 01/21] Add L1_WITH_CONSTANT_PROPAGATION mode to goto_symex_statet::rename This allows applying constant propagation without upgrading non-constant symbols to L2, which is useful for the dereferencing logic, as the value-set used to resolve pointer aliasing is indexed by L1 names. --- src/goto-symex/goto_symex_state.cpp | 25 ++++++++++++++++++++++--- src/goto-symex/renamed.h | 3 ++- 2 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index ffc43d3f409..5e44de1bf5e 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -171,9 +171,15 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) { // rename all the symbols with their last known value + static_assert( + level == L0 || level == L1 || level == L1_WITH_CONSTANT_PROPAGATION || + level == L2, + "must handle all renaming levels"); + if(expr.id()==ID_symbol && expr.get_bool(ID_C_SSA_symbol)) { + exprt original_expr = expr; ssa_exprt &ssa=to_ssa_expr(expr); if(level == L0) @@ -186,7 +192,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) return renamedt{ std::move(rename_ssa(std::move(ssa), ns).value())}; } - else if(level==L2) + else { ssa = set_indices(std::move(ssa), ns).get(); rename(expr.type(), ssa.get_identifier(), ns); @@ -195,7 +201,14 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) // renaming taken care of by l2_thread_encoding, or already at L2 if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty()) { - return renamedt(std::move(ssa)); + if(level == L1_WITH_CONSTANT_PROPAGATION) + { + // Don't actually rename to L2 -- we just used `ssa` to check whether + // constant-propagation was applicable + return renamedt(std::move(original_expr)); + } + else + return renamedt(std::move(ssa)); } else { @@ -209,7 +222,8 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) } else { - ssa = set_indices(std::move(ssa), ns).get(); + if(level == L2) + ssa = set_indices(std::move(ssa), ns).get(); return renamedt(std::move(ssa)); } } @@ -261,6 +275,11 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) } } +// Explicitly instantiate the one version of this function without an explicit +// caller in this file: +template renamedt +goto_symex_statet::rename(exprt expr, const namespacet &ns); + exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns) { rename(lvalue.type(), irep_idt(), ns); diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h index 58fe9ed9818..34bbc4e8188 100644 --- a/src/goto-symex/renamed.h +++ b/src/goto-symex/renamed.h @@ -16,7 +16,8 @@ enum levelt { L0 = 0, L1 = 1, - L2 = 2 + L1_WITH_CONSTANT_PROPAGATION = 2, + L2 = 3 }; /// Wrapper for expressions or types which have been renamed up to a given From 1f334015c24ad2af553b9dee6e127a6a24d89403 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 6 Aug 2019 07:32:11 +0100 Subject: [PATCH 02/21] Symex: enable array cell sensitivity --- src/goto-symex/field_sensitivity.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index fc05ad82213..06828bb7960 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -16,7 +16,7 @@ Author: Michael Tautschnig #include "goto_symex_state.h" #include "symex_target.h" -// #define ENABLE_ARRAY_FIELD_SENSITIVITY +#define ENABLE_ARRAY_FIELD_SENSITIVITY exprt field_sensitivityt::apply( const namespacet &ns, From da30884721bfd3e14b85001a6e49da69825c940c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 6 Aug 2019 07:32:13 +0100 Subject: [PATCH 03/21] Array cell sensitivity: tolerate zero-length arrays --- src/goto-symex/field_sensitivity.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 06828bb7960..69e771db1ff 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -267,8 +267,7 @@ void field_sensitivityt::field_assignments_rec( { const std::size_t array_size = numeric_cast_v(to_constant_expr(type->size())); - PRECONDITION( - lhs_fs.has_operands() && lhs_fs.operands().size() == array_size); + PRECONDITION(lhs_fs.operands().size() == array_size); exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin(); for(std::size_t i = 0; i < array_size; ++i) From 026a5104abe798fdd7f7fae73d2b0ffb664e6342 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 6 Aug 2019 07:32:16 +0100 Subject: [PATCH 04/21] Resolve array indices before dereferencing This may lead to application of array-cell-sensitivity (i.e. querying the symbol some_array[[1]] instead of some_array[some_index]), leading to higher precision. Some tests must be amended because better constant propagation causes some test behaviour to change as symex has better knowledge regarding the targets of pointers. --- regression/cbmc/address_space_size_limit3/main.i | 5 +++++ regression/cbmc/trace-values/trace-values.desc | 5 ++++- src/goto-symex/symex_dereference.cpp | 15 ++++++++++++++- 3 files changed, 23 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/address_space_size_limit3/main.i b/regression/cbmc/address_space_size_limit3/main.i index ab817d9e0bb..7d4d08cd2ed 100644 --- a/regression/cbmc/address_space_size_limit3/main.i +++ b/regression/cbmc/address_space_size_limit3/main.i @@ -92,6 +92,11 @@ void f__L_0x3c6_0() int main() { + int unknown; + // Avoid constant propagation solving for pointer-offsets of esp, + // which prevent demonstrating the object-size limitation this test + // intends to exhibit: + esp -= (unknown & 1); L_0x3fe_0: esp-=0x4; L_0x3fe_1: *(uint32_t*)(esp)=ebp; L_0x3ff_0: ebp=esp; diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc index b64fd79b8bf..a6e947db6f6 100644 --- a/regression/cbmc/trace-values/trace-values.desc +++ b/regression/cbmc/trace-values/trace-values.desc @@ -9,10 +9,13 @@ trace-values.c ^ local_var=3 .*$ ^ my_nested\[0.*\].array\[1.*\]=4 .*$ ^ my_nested\[1.*\].f=5 .*$ -^ null\$object=6 .*$ ^ junk\$object=7 .*$ ^ dynamic_object1\[1.*\]=8 .*$ ^ my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$ ^VERIFICATION FAILED$ -- ^warning: ignoring +-- +Note the assignment to "null" is not included because an assignment direct to +a certainly-null pointer goes to symex::invalid_object, not null$object, and is +hidden from the --trace output. diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index bef9746738f..8377ad1f8df 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -230,6 +231,18 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) // (x == &o1 ? o1..field : o2..field). value_set_dereferencet can then // apply the dereference operation to each of o1..field and o2..field // independently, as it special-cases the ternary conditional operator. + // There may also be index operators in tmp1 which can now be resolved to + // constant array cell references, so we replace symbols with constants + // first, hoping for a transformation such as + // (x == &o1 ? o1 : o2)[idx] => + // (x == &o1 ? o1 : o2)[2] => + // (x == &o1 ? o1[[2]] : o2[[2]]) + // Note we don't L2 rename non-constant symbols at this point, because the + // value-set works in terms of L1 names and we don't want to ask it to + // dereference an L2 pointer, which it would not have an entry for. + + tmp1 = state.rename(tmp1, ns).get(); + do_simplify(tmp1); if(symex_config.run_validation_checks) @@ -241,7 +254,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) "simplify re-introduced dereferencing"); } - tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), write); + tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), false); // we need to set up some elaborate call-backs symex_dereference_statet symex_dereference_state(state, ns); From 7b958bf4c9e450a222503b5c6ed03b7a78d4d178 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:19 +0100 Subject: [PATCH 05/21] Set a limit size for array cell propagation The use of field_sensitivity for arrays can be expensive for big arrays so we have to set a limit on the size of constant arrays which get processed. The value 64 was determined by changing the size of the array in the test regression/cbmc/variable-access-to-constant-array and reducing it until there was no significant difference in execution time between the versions of CBMC with and without array cell propagation. For the chosen value the execution time was around 0.05 second in both cases (for comparison with size 1024 the time with propagation was 0.5 sec, against 0.1 without). --- src/goto-symex/field_sensitivity.cpp | 33 +++++++++++++++++++--------- src/goto-symex/field_sensitivity.h | 2 ++ src/util/magic.h | 4 ++++ 3 files changed, 29 insertions(+), 10 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 69e771db1ff..a08af7810e5 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -97,14 +97,19 @@ exprt field_sensitivityt::apply( // SSA expression ssa_exprt tmp = to_ssa_expr(index.array()); bool was_l2 = !tmp.get_level_2().empty(); - - tmp.remove_level_2(); - index.array() = tmp.get_original_expr(); - tmp.set_expression(index); - if(was_l2) - return state.rename(std::move(tmp), ns).get(); - else - return std::move(tmp); + if( + l2_size.id() == ID_constant && + numeric_cast_v(to_constant_expr(l2_size)) <= + MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + { + tmp.remove_level_2(); + index.array() = tmp.get_original_expr(); + tmp.set_expression(index); + if(was_l2) + return state.rename(std::move(tmp), ns).get(); + else + return std::move(tmp); + } } } #endif // ENABLE_ARRAY_FIELD_SENSITIVITY @@ -147,7 +152,10 @@ exprt field_sensitivityt::get_fields( #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY else if( ssa_expr.type().id() == ID_array && - to_array_type(ssa_expr.type()).size().id() == ID_constant) + to_array_type(ssa_expr.type()).size().id() == ID_constant && + numeric_cast_v( + to_constant_expr(to_array_type(ssa_expr.type()).size())) <= + MAX_FIELD_SENSITIVITY_ARRAY_SIZE) { const array_typet &type = to_array_type(ssa_expr.type()); const std::size_t array_size = @@ -269,6 +277,9 @@ void field_sensitivityt::field_assignments_rec( numeric_cast_v(to_constant_expr(type->size())); PRECONDITION(lhs_fs.operands().size() == array_size); + if(array_size > MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + return; + exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin(); for(std::size_t i = 0; i < array_size; ++i) { @@ -308,7 +319,9 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr) #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY if( expr.type().id() == ID_array && - to_array_type(expr.type()).size().id() == ID_constant) + to_array_type(expr.type()).size().id() == ID_constant && + numeric_cast_v(to_constant_expr( + to_array_type(expr.type()).size())) <= MAX_FIELD_SENSITIVITY_ARRAY_SIZE) { return true; } diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index 8846285b1b5..eca87d93c19 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -9,6 +9,8 @@ Author: Michael Tautschnig #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H +#include + class exprt; class ssa_exprt; class namespacet; diff --git a/src/util/magic.h b/src/util/magic.h index 2f086f6cbff..3eaac31a99a 100644 --- a/src/util/magic.h +++ b/src/util/magic.h @@ -16,4 +16,8 @@ const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26; // The top end of the range of integers for which dstrings are precomputed constexpr std::size_t DSTRING_NUMBERS_MAX = 64; +/// Limit the size of arrays for which field_sensitivity gets applied. +/// Necessary because large constant arrays slow-down the process. +constexpr std::size_t MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64; + #endif From 08a71e928476ad2ea15ffd87f59f2147369baa9b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:20 +0100 Subject: [PATCH 06/21] Attempt to get missing array size from symbol table In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: https://github.com/diffblue/cbmc/issues/5022 --- src/goto-symex/field_sensitivity.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index a08af7810e5..3cf6f7ab87e 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -97,10 +97,23 @@ exprt field_sensitivityt::apply( // SSA expression ssa_exprt tmp = to_ssa_expr(index.array()); bool was_l2 = !tmp.get_level_2().empty(); + + exprt array_size_expr = to_array_type(l2_array.get().type()).size(); + if(array_size_expr.is_nil() && index.array().id() == ID_symbol) + { + // In case the array type was incomplete, attempt to retrieve it from + // the symbol table. + const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup( + to_symbol_expr(index.array()).get_identifier()); + if(array_from_symbol_table != nullptr) + array_size_expr = to_array_type(array_from_symbol_table->type).size(); + } + if( - l2_size.id() == ID_constant && - numeric_cast_v(to_constant_expr(l2_size)) <= - MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + array_size_expr.id() == ID_constant && + numeric_cast_v(to_constant_expr(array_size_expr)) <= + MAX_FIELD_SENSITIVITY_ARRAY_SIZE && + index.id() == ID_constant) { tmp.remove_level_2(); index.array() = tmp.get_original_expr(); From 22f35703657c081e820d9c08de8d7a80a6049eb7 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:47 +0100 Subject: [PATCH 07/21] Rename size to L2 in field_sensitivity::apply This is to allow constant propagation to take place and know whether the size is actually constant, which can allow field sensitivity to apply. --- src/goto-symex/field_sensitivity.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 3cf6f7ab87e..5f577ce3824 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -97,21 +97,21 @@ exprt field_sensitivityt::apply( // SSA expression ssa_exprt tmp = to_ssa_expr(index.array()); bool was_l2 = !tmp.get_level_2().empty(); - - exprt array_size_expr = to_array_type(l2_array.get().type()).size(); - if(array_size_expr.is_nil() && index.array().id() == ID_symbol) + exprt l2_size = + state.rename(to_array_type(index.array().type()).size(), ns).get(); + if(l2_size.is_nil() && index.array().id() == ID_symbol) { // In case the array type was incomplete, attempt to retrieve it from // the symbol table. const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup( to_symbol_expr(index.array()).get_identifier()); if(array_from_symbol_table != nullptr) - array_size_expr = to_array_type(array_from_symbol_table->type).size(); + l2_size = to_array_type(array_from_symbol_table->type).size(); } if( - array_size_expr.id() == ID_constant && - numeric_cast_v(to_constant_expr(array_size_expr)) <= + l2_size.id() == ID_constant && + numeric_cast_v(to_constant_expr(l2_size)) <= MAX_FIELD_SENSITIVITY_ARRAY_SIZE && index.id() == ID_constant) { From d11beceb3880c431daccab747d570a1b1db91fa2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:49 +0100 Subject: [PATCH 08/21] Make field_sensitivity::apply handle non-constant index When the index is not constant when accessing a constant size array, we should expand the expression into `{array[0]; array[1];...}[index]` so that the relation with field sensitivity expressions `array[[0]]`, `array[[1]]`, etc, is not lost. --- src/goto-symex/field_sensitivity.cpp | 33 ++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 9 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 5f577ce3824..b66ec82dde5 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -96,6 +96,8 @@ exprt field_sensitivityt::apply( // place the entire index expression, not just the array operand, in an // SSA expression ssa_exprt tmp = to_ssa_expr(index.array()); + auto l2_index = state.rename(index.index(), ns); + l2_index.simplify(ns); bool was_l2 = !tmp.get_level_2().empty(); exprt l2_size = state.rename(to_array_type(index.array().type()).size(), ns).get(); @@ -112,16 +114,29 @@ exprt field_sensitivityt::apply( if( l2_size.id() == ID_constant && numeric_cast_v(to_constant_expr(l2_size)) <= - MAX_FIELD_SENSITIVITY_ARRAY_SIZE && - index.id() == ID_constant) + MAX_FIELD_SENSITIVITY_ARRAY_SIZE) { - tmp.remove_level_2(); - index.array() = tmp.get_original_expr(); - tmp.set_expression(index); - if(was_l2) - return state.rename(std::move(tmp), ns).get(); - else - return std::move(tmp); + if(l2_index.get().id() == ID_constant) + { + // place the entire index expression, not just the array operand, + // in an SSA expression + ssa_exprt ssa_array = to_ssa_expr(index.array()); + ssa_array.remove_level_2(); + index.array() = ssa_array.get_original_expr(); + index.index() = l2_index.get(); + tmp.set_expression(index); + if(was_l2) + return state.rename(std::move(tmp), ns).get(); + else + return std::move(tmp); + } + else if(!write) + { + // Expand the array and return `{array[0]; array[1]; ...}[index]` + exprt expanded_array = + get_fields(ns, state, to_ssa_expr(index.array())); + return index_exprt{std::move(expanded_array), index.index()}; + } } } } From 33e00378c68f08efaa03bf06365bf3ffd3385389 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:51 +0100 Subject: [PATCH 09/21] Only apply field_sensitivity to dereferenced object This is important to consider dereferenced object as read value. --- src/goto-symex/symex_dereference.cpp | 32 +++++++++++++++++++++------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 8377ad1f8df..af6c8a36c7b 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -344,6 +344,20 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) } } +static exprt +apply_to_objects_in_dereference(exprt e, const std::function &f) +{ + if(auto deref = expr_try_dynamic_cast(e)) + { + deref->op() = f(std::move(deref->op())); + return *deref; + } + + for(auto &sub : e.operands()) + sub = apply_to_objects_in_dereference(std::move(sub), f); + return e; +} + /// Replace all dereference operations within \p expr with explicit references /// to the objects they may refer to. For example, the expression `*p1 + *p2` /// might be rewritten to `obj1 + (p2 == &obj2 ? obj2 : obj3)` in the case where @@ -383,19 +397,21 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write) /// See \ref auto_objects.cpp for details. void goto_symext::dereference(exprt &expr, statet &state, bool write) { - // The expression needs to be renamed to level 1 - // in order to distinguish addresses of local variables - // from different frames. Would be enough to rename - // symbols whose address is taken. PRECONDITION(!state.call_stack().empty()); - exprt l1_expr = state.field_sensitivity.apply( - ns, state, state.rename(expr, ns).get(), write); + + // Symbols whose address is taken need to be renamed to level 1 + // in order to distinguish addresses of local variables + // from different frames. + expr = apply_to_objects_in_dereference(std::move(expr), [&](exprt e) { + return state.field_sensitivity.apply( + ns, state, state.rename(std::move(e), ns).get(), false); + }); // start the recursion! - dereference_rec(l1_expr, state, write); + dereference_rec(expr, state, write); // dereferencing may introduce new symbol_exprt // (like __CPROVER_memory) - expr = state.rename(std::move(l1_expr), ns).get(); + expr = state.rename(std::move(expr), ns).get(); // Dereferencing is likely to introduce new member-of-if constructs -- // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field." From e86810e6b293d0442c29d0fc2108e03c578a79c0 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:53 +0100 Subject: [PATCH 10/21] Apply field sensitivity in symex_printf This may be necessary for constant propagation of the format string. An example of that is in regression/cbmc/printf1 --- src/goto-symex/symex_builtin_functions.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 1db7524e09e..0ea755bc06d 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -394,6 +394,7 @@ void goto_symext::symex_printf( else { clean_expr(*va_args, state, false); + *va_args = field_sensitivityt{}.apply(ns, state, *va_args, false); *va_args = state.rename(*va_args, ns).get(); if(va_args->id() != ID_array) { From 91de1649a0107cbf08d30aabfafae0d8be94b805 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:55 +0100 Subject: [PATCH 11/21] Allow trace to assign in two steps With field sensitivity on arrays, the element can be initialized in two steps, first the field f then the field array. --- regression/cbmc/trace-values/trace-values.desc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc index a6e947db6f6..c9a7e9a3cac 100644 --- a/regression/cbmc/trace-values/trace-values.desc +++ b/regression/cbmc/trace-values/trace-values.desc @@ -11,7 +11,8 @@ trace-values.c ^ my_nested\[1.*\].f=5 .*$ ^ junk\$object=7 .*$ ^ dynamic_object1\[1.*\]=8 .*$ -^ my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$ +^ my_nested\[1.*\](=\{ )?.f=0[ ,] +^ my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \} ^VERIFICATION FAILED$ -- ^warning: ignoring From d857648bfd606de36812592b4f3d7ba4750a5c2e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:57 +0100 Subject: [PATCH 12/21] Adapt double_deref test for array cell sensitivity Propagatiof of values of array cells lead to different expressions in VCC. --- .../cbmc/double_deref/double_deref_with_pointer_arithmetic.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc index 22f1388d331..df655168340 100644 --- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc +++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc @@ -1,7 +1,7 @@ CORE double_deref_with_pointer_arithmetic.c --show-vcc -^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = symex_dynamic::dynamic_object1#3\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\] +^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\] ^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\) ^EXIT=0$ ^SIGNAL=0$ From 162abbd18afed5aae2e99df796fb62aaebdb05ae Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:59 +0100 Subject: [PATCH 13/21] Tag test failing with SMT backend This is failing because of this bug: https://github.com/diffblue/cbmc/issues/4749 --- regression/cbmc/Multi_Dimensional_Array3/test.desc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/Multi_Dimensional_Array3/test.desc b/regression/cbmc/Multi_Dimensional_Array3/test.desc index 9efefbc7362..ba46c0308cf 100644 --- a/regression/cbmc/Multi_Dimensional_Array3/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend main.c ^EXIT=0$ @@ -6,3 +6,6 @@ main.c ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +-- +With the SMT backend this incorrect result because of the bug documented here: +https://github.com/diffblue/cbmc/issues/4749 From c3fdc330837f078315981b4836d20425e8df70c1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:33:01 +0100 Subject: [PATCH 14/21] Simplify lhs in build goto trace Avoid lhs of the form `{array[0], array[1]}[0]` --- src/goto-symex/build_goto_trace.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 60be0403b6e..5b1a243a5da 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -370,11 +370,13 @@ void build_goto_trace( if(SSA_step.original_full_lhs.is_not_nil()) { - goto_trace_step.full_lhs = build_full_lhs_rec( - decision_procedure, - ns, - SSA_step.original_full_lhs, - SSA_step.ssa_full_lhs); + goto_trace_step.full_lhs = simplify_expr( + build_full_lhs_rec( + decision_procedure, + ns, + SSA_step.original_full_lhs, + SSA_step.ssa_full_lhs), + ns); replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure); } From c93c1ca9ff1947b17695bbf8cd5e6c6c4cdae1b1 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 6 Aug 2019 07:33:03 +0100 Subject: [PATCH 15/21] Add tests for array-cell sensitivity Most are for C, then a couple are duplicated for Java to check whether its use of a structure to represent all arrays makes any difference. --- .../jbmc/array-cell-sensitivity1/Test.class | Bin 0 -> 642 bytes .../jbmc/array-cell-sensitivity1/Test.java | 10 ++++++ .../jbmc/array-cell-sensitivity1/test.desc | 22 ++++++++++++ .../jbmc/array-cell-sensitivity2/Test.class | Bin 0 -> 1179 bytes .../jbmc/array-cell-sensitivity2/Test.java | 21 ++++++++++++ .../jbmc/array-cell-sensitivity2/test.desc | 14 ++++++++ .../cbmc/array-cell-sensitivity1/test.c | 9 +++++ .../cbmc/array-cell-sensitivity1/test.desc | 21 ++++++++++++ .../cbmc/array-cell-sensitivity10/test.c | 16 +++++++++ .../cbmc/array-cell-sensitivity10/test.desc | 32 ++++++++++++++++++ .../cbmc/array-cell-sensitivity11/test.c | 15 ++++++++ .../cbmc/array-cell-sensitivity11/test.desc | 12 +++++++ .../cbmc/array-cell-sensitivity12/test.c | 15 ++++++++ .../cbmc/array-cell-sensitivity12/test.desc | 15 ++++++++ .../cbmc/array-cell-sensitivity13/test.c | 21 ++++++++++++ .../cbmc/array-cell-sensitivity13/test.desc | 13 +++++++ .../cbmc/array-cell-sensitivity14/test.c | 22 ++++++++++++ .../cbmc/array-cell-sensitivity14/test.desc | 14 ++++++++ .../cbmc/array-cell-sensitivity2/test.c | 9 +++++ .../cbmc/array-cell-sensitivity2/test.desc | 13 +++++++ .../cbmc/array-cell-sensitivity3/test.c | 10 ++++++ .../cbmc/array-cell-sensitivity3/test.desc | 23 +++++++++++++ .../cbmc/array-cell-sensitivity4/test.c | 10 ++++++ .../cbmc/array-cell-sensitivity4/test.desc | 21 ++++++++++++ .../cbmc/array-cell-sensitivity5/test.c | 10 ++++++ .../cbmc/array-cell-sensitivity5/test.desc | 22 ++++++++++++ .../cbmc/array-cell-sensitivity6/test.c | 11 ++++++ .../cbmc/array-cell-sensitivity6/test.desc | 23 +++++++++++++ .../cbmc/array-cell-sensitivity7/test.c | 11 ++++++ .../cbmc/array-cell-sensitivity7/test.desc | 23 +++++++++++++ .../cbmc/array-cell-sensitivity8/test.c | 11 ++++++ .../cbmc/array-cell-sensitivity8/test.desc | 30 ++++++++++++++++ .../cbmc/array-cell-sensitivity9/test.c | 15 ++++++++ .../cbmc/array-cell-sensitivity9/test.desc | 32 ++++++++++++++++++ 34 files changed, 546 insertions(+) create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/Test.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/Test.java create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/test.desc create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity2/Test.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity2/Test.java create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity2/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity1/test.c create mode 100644 regression/cbmc/array-cell-sensitivity1/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity10/test.c create mode 100644 regression/cbmc/array-cell-sensitivity10/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity11/test.c create mode 100644 regression/cbmc/array-cell-sensitivity11/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity12/test.c create mode 100644 regression/cbmc/array-cell-sensitivity12/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity13/test.c create mode 100644 regression/cbmc/array-cell-sensitivity13/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity14/test.c create mode 100644 regression/cbmc/array-cell-sensitivity14/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity2/test.c create mode 100644 regression/cbmc/array-cell-sensitivity2/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity3/test.c create mode 100644 regression/cbmc/array-cell-sensitivity3/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity4/test.c create mode 100644 regression/cbmc/array-cell-sensitivity4/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity5/test.c create mode 100644 regression/cbmc/array-cell-sensitivity5/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity6/test.c create mode 100644 regression/cbmc/array-cell-sensitivity6/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity7/test.c create mode 100644 regression/cbmc/array-cell-sensitivity7/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity8/test.c create mode 100644 regression/cbmc/array-cell-sensitivity8/test.desc create mode 100644 regression/cbmc/array-cell-sensitivity9/test.c create mode 100644 regression/cbmc/array-cell-sensitivity9/test.desc diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..57c9912d5717ec487cb350fe476f2aadae84af14 GIT binary patch literal 642 zcmZWlO-~d-5PdZ>yS+OMvMjpdiYN;jbQAW%O=2{t3CZdnASB?acebMg!;F~^^|x^G z=vhr9QKNT%lQF&?5Duo(T~)8EUcIVcf4=?zu#P)E6c(DO;fBJZ4;KpxH+|f~l0r`~ zx1#ghWJQ!F`Qs?pa0FQ9`r2Ww}(D946^o0PeQR89Unoh2;P% zxGiX1WRAuMCM-DF1+*D+DT2<#FdE_OZmBD(+ZX^R_!Z7h=Wm4Hyk* zg|>F@1oDxNgK56?3KU$TADkv&1}#QS%%V-i7MCP*XqQ|5cYoOLdZWJA9esjxjCS8! z>%Pa-H@JHz@P1lqx1#P)5&QAfNv4Q3(4!*Ts&h(*Ib5!C7IB4`;3}gAc8+W3 l`qwLQz-+tr1@&Vn?*lydGo1ftu_QG(!9zQ7mw|)pe*x}bZCL;S literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java new file mode 100644 index 00000000000..dacca2ec6fc --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java @@ -0,0 +1,10 @@ +public class Test { + + public static void main(int unknown) { + + int[] x = new int[10]; + x[unknown] = 1; + x[1] = unknown; + assert (x[1] == unknown); + } +} diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc new file mode 100644 index 00000000000..25c7ce03e0e --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc @@ -0,0 +1,22 @@ +CORE +Test.class +--function Test.main --show-vcc +symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\] +symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\] +symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\] +symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\] +symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\] +symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\] +symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\] +symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\] +symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\] +symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\] +symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1 +^EXIT=0$ +^SIGNAL=0$ +-- +symex_dynamic::dynamic_2_array#3\[\[[023456789]\]\] = +-- +This checks that a write to a Java array with an unknown index uses a whole-array +write followed by array-cell expansion, but one targeting a constant index uses +a single-cell symbol without expansion. diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..ae3d24793dc7256a0dad28f2e22c9a0f3ecfa12c GIT binary patch literal 1179 zcmb_cOHUI~7(I99&P-dTP{8u?t*C_-klNHlh>xHqBn6EnB;sn?PGq3WkZG&_1mn^r z3t77Mfg}=jum4FrcUma!T-Y}Ee&4xgzQ_6Q^ylxd-vJa*NFafXg^4&cOeVNwl$BLW z&cajz7BUG;W5&XD0aj zcWb1t37GSq?=^1==$VOC23iPeu0UVO^WEjvR>cih6j@-P6jYu1suOz3?|`zo?llP?h`R#T`O-dEwaT#{i=!z(x|iHhN&&=tD|iL@{RSj{kh- z-jN;;!Y~Le%-YC<=~G?GqsoR`W!ZgQXrWFW1%_&F!wcQoaS#^UZ1I31uHhnQl;9L~ z2$h=_+d(go8c}6*PFN=KL3(rK3+~CueTYfp8?-&>9|&kT#Z?Vog^>KFY1wTuhA>Po zjuDKu18FHTV#Ib;jM4$Lr~8mgoqaj0=gL_*RnC2eu8$epJFs%^(E;R`*#)K|M(l4u zj-{+Fq8Fts8nS5WMJt<@c|MUgqScI6D=+t8e1y4!K_)chE_x1Nv7p!w)tVl)R-`Uq z$p+g}p4*}ZCJL=lk= Q1~mIF|08gfaWq`}1H4JKL;wH) literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java new file mode 100644 index 00000000000..b58d9705aaf --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java @@ -0,0 +1,21 @@ +public class Test { + + public int data; + public Test[] children = new Test[2]; + + public static void main(int unknown) { + + Test[] root = new Test[2]; + Test node1 = new Test(); + Test node2 = new Test(); + root[0] = node1; + root[1] = node2; + node1.children[0] = unknown % 2 == 0 ? node1 : node2; + node1.children[1] = unknown % 3 == 0 ? node1 : node2; + node2.children[0] = unknown % 5 == 0 ? node1 : node2; + node2.children[1] = unknown % 7 == 0 ? node1 : node2; + int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0; + root[idx1].children[idx2].children[idx3].children[idx4].data = 1; + assert (node1.data == 1); + } +} diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc new file mode 100644 index 00000000000..92df9c81c8a --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--function Test.main --show-vcc +symex_dynamic::dynamic_object6#3\.\.data = +symex_dynamic::dynamic_object3#3\.\.data = +^EXIT=0$ +^SIGNAL=0$ +-- +symex_dynamic::dynamic_object6#3\.\.data = symex_dynamic::dynamic_object6#3\.data +symex_dynamic::dynamic_object3#3\.\.data = symex_dynamic::dynamic_object3#3\.data +-- +This checks that a write using a mix of field and array accessors uses a field-sensitive +symbol (the data field of the possible ultimate target objects) rather than using +a whole-struct write followed by an expansion. diff --git a/regression/cbmc/array-cell-sensitivity1/test.c b/regression/cbmc/array-cell-sensitivity1/test.c new file mode 100644 index 00000000000..5f10a1405d8 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity1/test.c @@ -0,0 +1,9 @@ +#include + +int main(int argc, char **argv) +{ + int array[10]; + array[argc] = 1; + array[1] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity1/test.desc b/regression/cbmc/array-cell-sensitivity1/test.desc new file mode 100644 index 00000000000..89d5291e18f --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity1/test.desc @@ -0,0 +1,21 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\] +main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\] +main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\] +main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\] +main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\] +main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\] +main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\] +main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\] +main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\] +main::1::array!0@1#3\[\[1\]\] = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::array!0@1#[2-9]\[[0-9]+\] +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol diff --git a/regression/cbmc/array-cell-sensitivity10/test.c b/regression/cbmc/array-cell-sensitivity10/test.c new file mode 100644 index 00000000000..6c961d9219c --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity10/test.c @@ -0,0 +1,16 @@ +#include + +struct A +{ + int x; + int y; +}; + +int main(int argc, char **argv) +{ + struct A array[10]; + struct A *ptr = argc % 2 ? (struct A *)&argc : &array[0]; + ptr[argc].x = 1; + ptr[1].x = argc; + assert(array[1].x == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity10/test.desc b/regression/cbmc/array-cell-sensitivity10/test.desc new file mode 100644 index 00000000000..1061132428e --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity10/test.desc @@ -0,0 +1,32 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x +main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x +main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x +main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x +main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x +main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x +main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x +main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x +main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x +main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x +main::1::array!0@1#3\[\[1\]\]..x = +main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y +main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y +main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y +main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y +main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y +main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y +main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y +main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y +main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y +main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, for the case where +the array element is struct-typed and accessed via a pointer. diff --git a/regression/cbmc/array-cell-sensitivity11/test.c b/regression/cbmc/array-cell-sensitivity11/test.c new file mode 100644 index 00000000000..0507205a8aa --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity11/test.c @@ -0,0 +1,15 @@ +#include + +struct A +{ + int x; + int y; +}; + +int main(int argc, char **argv) +{ + struct A array[10]; + int *ptr = argc % 2 ? &argc : &array[0].y; + *ptr = argc; + assert(array[1].y == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity11/test.desc b/regression/cbmc/array-cell-sensitivity11/test.desc new file mode 100644 index 00000000000..876777e3cf6 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity11/test.desc @@ -0,0 +1,12 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[0\]\]..y = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::array!0@1#[2-9]\[\[[1-9]\]\] +main::1::array!0@1#[3-9]\[\[[0-9]\]\] +-- +This checks that an array access made via a pointer to a member of the array's +element struct type is executed using a field-sensitive symbol. diff --git a/regression/cbmc/array-cell-sensitivity12/test.c b/regression/cbmc/array-cell-sensitivity12/test.c new file mode 100644 index 00000000000..d960831e1a2 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity12/test.c @@ -0,0 +1,15 @@ +#include + +struct A +{ + int x; + int y; +}; + +int main(int argc, char **argv) +{ + struct A array[10]; + int *ptr = argc % 2 ? &array[0].x : &array[0].y; + *ptr = argc; + assert(array[0].y == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity12/test.desc b/regression/cbmc/array-cell-sensitivity12/test.desc new file mode 100644 index 00000000000..2392541df5a --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity12/test.desc @@ -0,0 +1,15 @@ +FUTURE +test.c +--show-vcc +main::1::array!0@1#2\[\[0\]\]..x = +main::1::array!0@1#2\[\[0\]\]..y = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::array!0@1#[2-9]\[\[[1-9]\]\] +main::1::array!0@1#[3-9]\[\[[0-9]\]\] +-- +Ideally we should handle accesses to a pointer with a finite set of possible +referents precisely, but because value_sett regards &array[0].x and &array[0].y +as two different offsets into the same allocation and discards the precise offsets +they point to, this is currently handled imprecisely with a byte_update operation. diff --git a/regression/cbmc/array-cell-sensitivity13/test.c b/regression/cbmc/array-cell-sensitivity13/test.c new file mode 100644 index 00000000000..160aff9c05f --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity13/test.c @@ -0,0 +1,21 @@ +#include + +struct A +{ + int data; + struct A *children[2]; +}; + +int main(int argc, char **argv) +{ + struct A root; + struct A node1, node2; + root.children[0] = argc % 2 ? &node1 : &node2; + root.children[1] = argc % 3 ? &node1 : &node2; + node1.children[0] = argc % 5 ? &node1 : &node2; + node1.children[1] = argc % 7 ? &node1 : &node2; + node2.children[0] = argc % 11 ? &node1 : &node2; + node2.children[1] = argc % 13 ? &node1 : &node2; + root.children[0]->children[1]->children[1]->children[0]->data = 1; + assert(node1.data == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity13/test.desc b/regression/cbmc/array-cell-sensitivity13/test.desc new file mode 100644 index 00000000000..36d5cc34e1a --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity13/test.desc @@ -0,0 +1,13 @@ +CORE +test.c +--show-vcc +main::1::node1!0@1#2\.\.data = +main::1::node2!0@1#2\.\.data = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::node1!0@1#[3-9]\.\.children\[\[[01]\]\] = +-- +This checks that mixed array and field accesses are executed using a field-sensitive +symbol (main::1::node1!0@1#2..data) rather than by assigning the whole struct and +expanding into field symbols (which would assign main::1::node1!0@1#3..children\[\[[01]\]\]) diff --git a/regression/cbmc/array-cell-sensitivity14/test.c b/regression/cbmc/array-cell-sensitivity14/test.c new file mode 100644 index 00000000000..597c8fbef86 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity14/test.c @@ -0,0 +1,22 @@ +#include + +struct A +{ + int data; + struct A *children[2]; +}; + +int main(int argc, char **argv) +{ + struct A root; + struct A node1, node2; + root.children[0] = argc % 2 ? &node1 : &node2; + root.children[1] = argc % 3 ? &node1 : &node2; + node1.children[0] = argc % 5 ? &node1 : &node2; + node1.children[1] = argc % 7 ? &node1 : &node2; + node2.children[0] = argc % 11 ? &node1 : &node2; + node2.children[1] = argc % 13 ? &node1 : &node2; + int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0; + root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data = 1; + assert(node1.data == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity14/test.desc b/regression/cbmc/array-cell-sensitivity14/test.desc new file mode 100644 index 00000000000..3395875c67d --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity14/test.desc @@ -0,0 +1,14 @@ +CORE +test.c +--show-vcc +main::1::node1!0@1#2\.\.data = +main::1::node2!0@1#2\.\.data = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::node1!0@1#[3-9]\.\.children\[\[[01]\]\] = +-- +This checks that mixed array and field accesses are executed using a field-sensitive +symbol (main::1::node1!0@1#2..data) rather than by assigning the whole struct and +expanding into field symbols (which would assign main::1::node1!0@1#3..children\[\[[01]\]\]), +for the case where the array indices only become constant after propagation. diff --git a/regression/cbmc/array-cell-sensitivity2/test.c b/regression/cbmc/array-cell-sensitivity2/test.c new file mode 100644 index 00000000000..729ef6bd682 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity2/test.c @@ -0,0 +1,9 @@ +#include + +int main(int argc, char **argv) +{ + int array[argc]; + array[argc - 1] = 1; + array[1] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc new file mode 100644 index 00000000000..92a0b40af63 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity2/test.desc @@ -0,0 +1,13 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(-1 \+ main::argc!0@1#1, signedbv\[64\]\), 1\) +main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\) +^EXIT=0$ +^SIGNAL=0$ +-- +\[\[[0-9]+\]\] +-- +This checks that arrays of uncertain size are always treated as aggregates and +are not expanded into individual cell symbols (which use the [[index]] notation +to distinguish them from the index operator (array[index])) diff --git a/regression/cbmc/array-cell-sensitivity3/test.c b/regression/cbmc/array-cell-sensitivity3/test.c new file mode 100644 index 00000000000..f6efa33f5da --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity3/test.c @@ -0,0 +1,10 @@ +#include + +int main(int argc, char **argv) +{ + int array[10]; + int *ptr = argc % 2 ? &argc : &array[0]; + ptr[argc] = 1; + ptr[1] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity3/test.desc b/regression/cbmc/array-cell-sensitivity3/test.desc new file mode 100644 index 00000000000..da0a7025fda --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity3/test.desc @@ -0,0 +1,23 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[0]\] = main::1::array!0@1#1\[0\] +main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\] +main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\] +main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\] +main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\] +main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\] +main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\] +main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\] +main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\] +main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\] +main::1::array!0@1#3\[\[1\]\] = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::array!0@1#[2-9]\[[0-9]+\] +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, even when the +array is accessed via a pointer with other possible aliases. diff --git a/regression/cbmc/array-cell-sensitivity4/test.c b/regression/cbmc/array-cell-sensitivity4/test.c new file mode 100644 index 00000000000..99dae61d3e9 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity4/test.c @@ -0,0 +1,10 @@ +#include + +int main(int argc, char **argv) +{ + int array[10]; + int x = 1; + array[argc] = 1; + array[x] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity4/test.desc b/regression/cbmc/array-cell-sensitivity4/test.desc new file mode 100644 index 00000000000..9f7da1d30cc --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity4/test.desc @@ -0,0 +1,21 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\] +main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\] +main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\] +main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\] +main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\] +main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\] +main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\] +main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\] +main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\] +main::1::array!0@1#3\[\[1\]\] = +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, even when the +constant index is only revealed as constant after propagation. diff --git a/regression/cbmc/array-cell-sensitivity5/test.c b/regression/cbmc/array-cell-sensitivity5/test.c new file mode 100644 index 00000000000..1d0d3b14ece --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity5/test.c @@ -0,0 +1,10 @@ +#include +#include + +int main(int argc, char **argv) +{ + int *array = malloc(sizeof(int) * 10); + array[argc] = 1; + array[1] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity5/test.desc b/regression/cbmc/array-cell-sensitivity5/test.desc new file mode 100644 index 00000000000..923d28fc391 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity5/test.desc @@ -0,0 +1,22 @@ +CORE +test.c +--show-vcc +symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\] +symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\] +symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\] +symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\] +symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\] +symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\] +symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\] +symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\] +symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\] +symex_dynamic::dynamic_object1#3\[\[1\]\] = +^EXIT=0$ +^SIGNAL=0$ +-- +symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\] +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, even when the array +in question is dynamically allocated. diff --git a/regression/cbmc/array-cell-sensitivity6/test.c b/regression/cbmc/array-cell-sensitivity6/test.c new file mode 100644 index 00000000000..fc36a10f6f2 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity6/test.c @@ -0,0 +1,11 @@ +#include +#include + +int main(int argc, char **argv) +{ + int x = 10; + int *array = malloc(sizeof(int) * x); + array[argc] = 1; + array[1] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity6/test.desc b/regression/cbmc/array-cell-sensitivity6/test.desc new file mode 100644 index 00000000000..cdbfa2c3aac --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity6/test.desc @@ -0,0 +1,23 @@ +CORE +test.c +--show-vcc +symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\] +symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\] +symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\] +symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\] +symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\] +symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\] +symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\] +symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\] +symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\] +symex_dynamic::dynamic_object1#3\[\[1\]\] = +^EXIT=0$ +^SIGNAL=0$ +-- +symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\] +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, even when the array +in question is dynamically allocated and the constancy of its size depends on +constant propagation. diff --git a/regression/cbmc/array-cell-sensitivity7/test.c b/regression/cbmc/array-cell-sensitivity7/test.c new file mode 100644 index 00000000000..f009e8cee5e --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity7/test.c @@ -0,0 +1,11 @@ +#include +#include + +int main(int argc, char **argv) +{ + int array[10]; + char *ptr = argc % 2 ? (char *)&array[0] : (char *)&argc; + ptr[argc] = 'a'; + ptr[1] = (char)argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity7/test.desc b/regression/cbmc/array-cell-sensitivity7/test.desc new file mode 100644 index 00000000000..ffd25206574 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity7/test.desc @@ -0,0 +1,23 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\] +main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\] +main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\] +main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\] +main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\] +main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\] +main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\] +main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\] +main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\] +main::1::array!0@1#3\[\[0\]\] = +^EXIT=0$ +^SIGNAL=0$ +-- +main::1::array!0@1#[2-9]\[[0-9]+\] +main::1::array!0@1#3\[\[[1-9]\]\] = +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, even when the array +is addressed via a pointer cast to a smaller type. diff --git a/regression/cbmc/array-cell-sensitivity8/test.c b/regression/cbmc/array-cell-sensitivity8/test.c new file mode 100644 index 00000000000..68dada43a88 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity8/test.c @@ -0,0 +1,11 @@ +#include +#include + +int main(int argc, char **argv) +{ + int array[10]; + long long *ptr = argc % 2 ? (long long *)&array[0] : (long long *)&argc; + ptr[argc] = 1; + ptr[1] = argc; + assert(array[1] == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity8/test.desc b/regression/cbmc/array-cell-sensitivity8/test.desc new file mode 100644 index 00000000000..da8e78103f9 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity8/test.desc @@ -0,0 +1,30 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\] +main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\] +main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\] +main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\] +main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\] +main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\] +main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\] +main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\] +main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\] +main::1::array!0@1#2 =.*byte_extract_little_endian +main::1::array!0@1#3\[\[0\]\] = main::1::array!0@1#2\[0\] +main::1::array!0@1#3\[\[1\]\] = main::1::array!0@1#2\[1\] +main::1::array!0@1#3\[\[2\]\] = main::1::array!0@1#2\[2\] +main::1::array!0@1#3\[\[3\]\] = main::1::array!0@1#2\[3\] +main::1::array!0@1#3\[\[4\]\] = main::1::array!0@1#2\[4\] +main::1::array!0@1#3\[\[5\]\] = main::1::array!0@1#2\[5\] +main::1::array!0@1#3\[\[6\]\] = main::1::array!0@1#2\[6\] +main::1::array!0@1#3\[\[7\]\] = main::1::array!0@1#2\[7\] +main::1::array!0@1#3\[\[8\]\] = main::1::array!0@1#2\[8\] +main::1::array!0@1#3\[\[9\]\] = main::1::array!0@1#2\[9\] +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This checks that when an array cell is accessed via a pointer to a large enough +type that multiple cells are required then whole-array operations are used, +rather than attempting to operate on single cell symbols. diff --git a/regression/cbmc/array-cell-sensitivity9/test.c b/regression/cbmc/array-cell-sensitivity9/test.c new file mode 100644 index 00000000000..d675d409c81 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity9/test.c @@ -0,0 +1,15 @@ +#include + +struct A +{ + int x; + int y; +}; + +int main(int argc, char **argv) +{ + struct A array[10]; + array[argc].x = 1; + array[1].x = argc; + assert(array[1].x == argc); +} diff --git a/regression/cbmc/array-cell-sensitivity9/test.desc b/regression/cbmc/array-cell-sensitivity9/test.desc new file mode 100644 index 00000000000..1a7d5937ac2 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity9/test.desc @@ -0,0 +1,32 @@ +CORE +test.c +--show-vcc +main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x +main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x +main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x +main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x +main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x +main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x +main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x +main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x +main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x +main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x +main::1::array!0@1#3\[\[1\]\]..x = +main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y +main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y +main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y +main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y +main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y +main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y +main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y +main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y +main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y +main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This checks that a write with a non-constant index leads to a whole-array +operation followed by expansion into individual array cells, while a write with +a constant index leads to direct use of a single cell symbol, for the case where +the array element is struct-typed. From ca78842ca6e08e55f9ba5dbadf2d8c23105abc85 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:33:05 +0100 Subject: [PATCH 16/21] Document how arrays are handled by field sensitivity This explains how field sensitivity transforms instructions that contain array operations. --- src/goto-symex/field_sensitivity.h | 31 +++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index eca87d93c19..3ff2bc80550 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -28,9 +28,10 @@ class symex_targett; /// Note that field sensitivity is not applied as a single pass over the /// whole goto program but instead applied as the symbolic execution unfolds. /// -/// On a high level, field sensitivity replaces member operators with atomic -/// symbols representing a field when possible. In cases where this is not -/// immediately possible, like struct assignments, some things need to be added. +/// On a high level, field sensitivity replaces member operators, and array +/// accesses with atomic symbols representing a field when possible. +/// In cases where this is not immediately possible, like struct assignments, +/// some things need to be added. /// The possible cases are described below. /// /// ### Member access @@ -52,6 +53,30 @@ class symex_targett; /// `struct_expr..field_name1 = other_struct..field_name1;` /// `struct_expr..field_name2 = other_struct..field_name2;` etc. /// See \ref field_sensitivityt::field_assignments. +/// +/// ### Array access +/// An index expression `array[index]` when index is constant and array has +/// constant size is replaced by the symbol `array[[index]]`; note the use +/// of `[[` and `]]` to visually distinguish the symbol from the index +/// expression. +/// When `index` is not a constant, `array[index]` is replaced by +/// `{array[[0]]; array[[1]]; …index]`. +/// Note that this process does not apply to arrays whose size is not constant, +/// and arrays whose size exceed the bound \ref MAX_FIELD_SENSITIVITY_ARRAY_SIZE +/// See \ref field_sensitivityt::apply. +/// +/// ### Symbols representing arrays +/// In an rvalue, a symbol `array` which has array type will be replaced by +/// `{array[[0]]; array[[1]]; …}[index]`. +/// See \ref field_sensitivityt::get_fields. +/// +/// ### Assignment to an array +/// When the array symbol is on the left-hand-side, for instance for +/// an assignment `array = other_array`, the assignment is replaced by a +/// sequence of assignments: +/// `array[[0]] = other_array[[0]]`; +/// `array[[1]] = other_array[[1]]`; etc. +/// See \ref field_sensitivityt::field_assignments. class field_sensitivityt { public: From 08d43f9271f9ff6ff09b8ae0883f01f1f38a7fe5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 16:53:49 +0100 Subject: [PATCH 17/21] Activate regression tests previously KNOWNBUG These tests can now be executed in our test suite. --- regression/cbmc-concurrency/norace_array1/test.desc | 2 +- regression/cbmc-concurrency/norace_array2/test.desc | 2 +- regression/cbmc-concurrency/struct_and_array1/test.desc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-concurrency/norace_array1/test.desc b/regression/cbmc-concurrency/norace_array1/test.desc index c239dca4b31..8ecf05b6d5c 100644 --- a/regression/cbmc-concurrency/norace_array1/test.desc +++ b/regression/cbmc-concurrency/norace_array1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG pthread +CORE pthread main.c ^EXIT=0$ diff --git a/regression/cbmc-concurrency/norace_array2/test.desc b/regression/cbmc-concurrency/norace_array2/test.desc index c239dca4b31..8ecf05b6d5c 100644 --- a/regression/cbmc-concurrency/norace_array2/test.desc +++ b/regression/cbmc-concurrency/norace_array2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG pthread +CORE pthread main.c ^EXIT=0$ diff --git a/regression/cbmc-concurrency/struct_and_array1/test.desc b/regression/cbmc-concurrency/struct_and_array1/test.desc index 52168c7eba4..8ecf05b6d5c 100644 --- a/regression/cbmc-concurrency/struct_and_array1/test.desc +++ b/regression/cbmc-concurrency/struct_and_array1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE pthread main.c ^EXIT=0$ From 869f2cd94bf50917969c8a0a0e202f9215e67e0c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 8 Aug 2019 17:37:12 +0100 Subject: [PATCH 18/21] Add execution tests for array-cell-sensitivity These are companions to the existing tests that check the show-vcc output, and serve to check that the formulas generated appear to behave properly. --- .../cbmc/array-cell-sensitivity1/test_execution.desc | 10 ++++++++++ regression/cbmc/array-cell-sensitivity10/test.c | 4 +++- .../array-cell-sensitivity10/test_execution.desc | 12 ++++++++++++ regression/cbmc/array-cell-sensitivity11/test.c | 1 + .../array-cell-sensitivity11/test_execution.desc | 12 ++++++++++++ regression/cbmc/array-cell-sensitivity12/test.c | 1 + .../array-cell-sensitivity12/test_execution.desc | 12 ++++++++++++ regression/cbmc/array-cell-sensitivity13/test.c | 1 + .../array-cell-sensitivity13/test_execution.desc | 12 ++++++++++++ regression/cbmc/array-cell-sensitivity14/test.c | 3 +++ .../array-cell-sensitivity14/test_execution.desc | 12 ++++++++++++ .../cbmc/array-cell-sensitivity2/test_execution.desc | 10 ++++++++++ regression/cbmc/array-cell-sensitivity3/test.c | 1 + .../cbmc/array-cell-sensitivity3/test_execution.desc | 12 ++++++++++++ .../cbmc/array-cell-sensitivity4/test_execution.desc | 10 ++++++++++ .../cbmc/array-cell-sensitivity5/test_execution.desc | 10 ++++++++++ .../cbmc/array-cell-sensitivity6/test_execution.desc | 10 ++++++++++ regression/cbmc/array-cell-sensitivity7/test.c | 3 ++- .../cbmc/array-cell-sensitivity7/test_execution.desc | 12 ++++++++++++ regression/cbmc/array-cell-sensitivity8/test.c | 4 +++- .../cbmc/array-cell-sensitivity8/test_execution.desc | 12 ++++++++++++ .../cbmc/array-cell-sensitivity9/test_execution.desc | 10 ++++++++++ 22 files changed, 171 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/array-cell-sensitivity1/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity10/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity11/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity12/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity13/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity14/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity2/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity3/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity4/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity5/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity6/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity7/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity8/test_execution.desc create mode 100644 regression/cbmc/array-cell-sensitivity9/test_execution.desc diff --git a/regression/cbmc/array-cell-sensitivity1/test_execution.desc b/regression/cbmc/array-cell-sensitivity1/test_execution.desc new file mode 100644 index 00000000000..9280dcb19be --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity1/test_execution.desc @@ -0,0 +1,10 @@ +CORE +test.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity10/test.c b/regression/cbmc/array-cell-sensitivity10/test.c index 6c961d9219c..3c00351e5bf 100644 --- a/regression/cbmc/array-cell-sensitivity10/test.c +++ b/regression/cbmc/array-cell-sensitivity10/test.c @@ -9,8 +9,10 @@ struct A int main(int argc, char **argv) { struct A array[10]; - struct A *ptr = argc % 2 ? (struct A *)&argc : &array[0]; + struct A other[2]; + struct A *ptr = argc % 2 ? &other : &array[0]; ptr[argc].x = 1; ptr[1].x = argc; + assert(ptr[1].x == argc); assert(array[1].x == argc); } diff --git a/regression/cbmc/array-cell-sensitivity10/test_execution.desc b/regression/cbmc/array-cell-sensitivity10/test_execution.desc new file mode 100644 index 00000000000..1e8aa561e48 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity10/test_execution.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 16.*SUCCESS$ +^\[main.assertion\.2\] line 17.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity11/test.c b/regression/cbmc/array-cell-sensitivity11/test.c index 0507205a8aa..2db85d1c016 100644 --- a/regression/cbmc/array-cell-sensitivity11/test.c +++ b/regression/cbmc/array-cell-sensitivity11/test.c @@ -11,5 +11,6 @@ int main(int argc, char **argv) struct A array[10]; int *ptr = argc % 2 ? &argc : &array[0].y; *ptr = argc; + assert(*ptr == argc); assert(array[1].y == argc); } diff --git a/regression/cbmc/array-cell-sensitivity11/test_execution.desc b/regression/cbmc/array-cell-sensitivity11/test_execution.desc new file mode 100644 index 00000000000..d33e4045438 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity11/test_execution.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 14.*SUCCESS$ +^\[main.assertion\.2\] line 15.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity12/test.c b/regression/cbmc/array-cell-sensitivity12/test.c index d960831e1a2..91000e7e791 100644 --- a/regression/cbmc/array-cell-sensitivity12/test.c +++ b/regression/cbmc/array-cell-sensitivity12/test.c @@ -11,5 +11,6 @@ int main(int argc, char **argv) struct A array[10]; int *ptr = argc % 2 ? &array[0].x : &array[0].y; *ptr = argc; + assert(*ptr == argc); assert(array[0].y == argc); } diff --git a/regression/cbmc/array-cell-sensitivity12/test_execution.desc b/regression/cbmc/array-cell-sensitivity12/test_execution.desc new file mode 100644 index 00000000000..d33e4045438 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity12/test_execution.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 14.*SUCCESS$ +^\[main.assertion\.2\] line 15.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity13/test.c b/regression/cbmc/array-cell-sensitivity13/test.c index 160aff9c05f..bb1e71dcdc0 100644 --- a/regression/cbmc/array-cell-sensitivity13/test.c +++ b/regression/cbmc/array-cell-sensitivity13/test.c @@ -17,5 +17,6 @@ int main(int argc, char **argv) node2.children[0] = argc % 11 ? &node1 : &node2; node2.children[1] = argc % 13 ? &node1 : &node2; root.children[0]->children[1]->children[1]->children[0]->data = 1; + assert(root.children[0]->children[1]->children[1]->children[0]->data == 1); assert(node1.data == argc); } diff --git a/regression/cbmc/array-cell-sensitivity13/test_execution.desc b/regression/cbmc/array-cell-sensitivity13/test_execution.desc new file mode 100644 index 00000000000..f3dc42bc691 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity13/test_execution.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 20.*SUCCESS$ +^\[main.assertion\.2\] line 21.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity14/test.c b/regression/cbmc/array-cell-sensitivity14/test.c index 597c8fbef86..ddec5e9b295 100644 --- a/regression/cbmc/array-cell-sensitivity14/test.c +++ b/regression/cbmc/array-cell-sensitivity14/test.c @@ -18,5 +18,8 @@ int main(int argc, char **argv) node2.children[1] = argc % 13 ? &node1 : &node2; int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0; root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data = 1; + assert( + root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data == + 1); assert(node1.data == argc); } diff --git a/regression/cbmc/array-cell-sensitivity14/test_execution.desc b/regression/cbmc/array-cell-sensitivity14/test_execution.desc new file mode 100644 index 00000000000..5b84583d54a --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity14/test_execution.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 21.*SUCCESS$ +^\[main.assertion\.2\] line 24.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity2/test_execution.desc b/regression/cbmc/array-cell-sensitivity2/test_execution.desc new file mode 100644 index 00000000000..9280dcb19be --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity2/test_execution.desc @@ -0,0 +1,10 @@ +CORE +test.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity3/test.c b/regression/cbmc/array-cell-sensitivity3/test.c index f6efa33f5da..cc33ade48c7 100644 --- a/regression/cbmc/array-cell-sensitivity3/test.c +++ b/regression/cbmc/array-cell-sensitivity3/test.c @@ -6,5 +6,6 @@ int main(int argc, char **argv) int *ptr = argc % 2 ? &argc : &array[0]; ptr[argc] = 1; ptr[1] = argc; + assert(ptr[1] == argc); assert(array[1] == argc); } diff --git a/regression/cbmc/array-cell-sensitivity3/test_execution.desc b/regression/cbmc/array-cell-sensitivity3/test_execution.desc new file mode 100644 index 00000000000..52bf413ffd9 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity3/test_execution.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 9.*SUCCESS$ +^\[main.assertion\.2\] line 10.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity4/test_execution.desc b/regression/cbmc/array-cell-sensitivity4/test_execution.desc new file mode 100644 index 00000000000..9280dcb19be --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity4/test_execution.desc @@ -0,0 +1,10 @@ +CORE +test.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity5/test_execution.desc b/regression/cbmc/array-cell-sensitivity5/test_execution.desc new file mode 100644 index 00000000000..9280dcb19be --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity5/test_execution.desc @@ -0,0 +1,10 @@ +CORE +test.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity6/test_execution.desc b/regression/cbmc/array-cell-sensitivity6/test_execution.desc new file mode 100644 index 00000000000..9280dcb19be --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity6/test_execution.desc @@ -0,0 +1,10 @@ +CORE +test.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity7/test.c b/regression/cbmc/array-cell-sensitivity7/test.c index f009e8cee5e..48f8f85a7e6 100644 --- a/regression/cbmc/array-cell-sensitivity7/test.c +++ b/regression/cbmc/array-cell-sensitivity7/test.c @@ -7,5 +7,6 @@ int main(int argc, char **argv) char *ptr = argc % 2 ? (char *)&array[0] : (char *)&argc; ptr[argc] = 'a'; ptr[1] = (char)argc; - assert(array[1] == argc); + assert(ptr[1] == (char)argc); + assert(array[1] == (char)argc); } diff --git a/regression/cbmc/array-cell-sensitivity7/test_execution.desc b/regression/cbmc/array-cell-sensitivity7/test_execution.desc new file mode 100644 index 00000000000..62502389e48 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity7/test_execution.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 10.*SUCCESS$ +^\[main.assertion\.2\] line 11.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity8/test.c b/regression/cbmc/array-cell-sensitivity8/test.c index 68dada43a88..8874633f1fa 100644 --- a/regression/cbmc/array-cell-sensitivity8/test.c +++ b/regression/cbmc/array-cell-sensitivity8/test.c @@ -4,8 +4,10 @@ int main(int argc, char **argv) { int array[10]; - long long *ptr = argc % 2 ? (long long *)&array[0] : (long long *)&argc; + long long other; + long long *ptr = argc % 2 ? (long long *)&array[0] : &other; ptr[argc] = 1; ptr[1] = argc; + assert(ptr[1] == argc); assert(array[1] == argc); } diff --git a/regression/cbmc/array-cell-sensitivity8/test_execution.desc b/regression/cbmc/array-cell-sensitivity8/test_execution.desc new file mode 100644 index 00000000000..96db1c25647 --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity8/test_execution.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend +test.c + +^VERIFICATION FAILED$ +^\[main.assertion\.1\] line 11.*SUCCESS$ +^\[main.assertion\.2\] line 12.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. diff --git a/regression/cbmc/array-cell-sensitivity9/test_execution.desc b/regression/cbmc/array-cell-sensitivity9/test_execution.desc new file mode 100644 index 00000000000..9280dcb19be --- /dev/null +++ b/regression/cbmc/array-cell-sensitivity9/test_execution.desc @@ -0,0 +1,10 @@ +CORE +test.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The real test is in test.desc; this is a companion to check that the program under +test actually behaves as expected. From 163d6b421825c836314fb4ecad599239cf1fa628 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Aug 2019 15:44:50 +0100 Subject: [PATCH 19/21] Make field sensitivity max array size configurable This will allow the user of symex to set this limit as needed instead of fixing it to an arbitrary value. --- src/goto-instrument/accelerate/scratch_program.cpp | 1 + src/goto-symex/field_sensitivity.cpp | 10 +++++----- src/goto-symex/field_sensitivity.h | 13 +++++++++++-- src/goto-symex/goto_symex.h | 7 +++++++ src/goto-symex/goto_symex_state.cpp | 6 ++++-- src/goto-symex/goto_symex_state.h | 6 ++++-- src/goto-symex/symex_assign.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_goto.cpp | 2 +- src/goto-symex/symex_main.cpp | 5 ++++- src/util/magic.h | 2 +- unit/goto-symex/goto_symex_state.cpp | 4 +++- unit/goto-symex/symex_assign.cpp | 4 +++- .../goto-symex/try_evaluate_pointer_comparisons.cpp | 5 +++-- 14 files changed, 49 insertions(+), 20 deletions(-) diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 608dd300605..63b9b4cc863 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -38,6 +38,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager) symex_state = util_make_unique( symex_targett::sourcet(goto_functionst::entry_point(), *this), + symex.field_sensitivity, guard_manager, [this](const irep_idt &id) { return path_storage.get_unique_l2_index(id); diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index b66ec82dde5..0e5cbd09c14 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -114,7 +114,7 @@ exprt field_sensitivityt::apply( if( l2_size.id() == ID_constant && numeric_cast_v(to_constant_expr(l2_size)) <= - MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + max_field_sensitivity_array_size) { if(l2_index.get().id() == ID_constant) { @@ -183,7 +183,7 @@ exprt field_sensitivityt::get_fields( to_array_type(ssa_expr.type()).size().id() == ID_constant && numeric_cast_v( to_constant_expr(to_array_type(ssa_expr.type()).size())) <= - MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + max_field_sensitivity_array_size) { const array_typet &type = to_array_type(ssa_expr.type()); const std::size_t array_size = @@ -305,7 +305,7 @@ void field_sensitivityt::field_assignments_rec( numeric_cast_v(to_constant_expr(type->size())); PRECONDITION(lhs_fs.operands().size() == array_size); - if(array_size > MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + if(array_size > max_field_sensitivity_array_size) return; exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin(); @@ -339,7 +339,7 @@ void field_sensitivityt::field_assignments_rec( } } -bool field_sensitivityt::is_divisible(const ssa_exprt &expr) +bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const { if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag) return true; @@ -349,7 +349,7 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr) expr.type().id() == ID_array && to_array_type(expr.type()).size().id() == ID_constant && numeric_cast_v(to_constant_expr( - to_array_type(expr.type()).size())) <= MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + to_array_type(expr.type()).size())) <= max_field_sensitivity_array_size) { return true; } diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index 3ff2bc80550..0b791ce694a 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -62,7 +62,7 @@ class symex_targett; /// When `index` is not a constant, `array[index]` is replaced by /// `{array[[0]]; array[[1]]; …index]`. /// Note that this process does not apply to arrays whose size is not constant, -/// and arrays whose size exceed the bound \ref MAX_FIELD_SENSITIVITY_ARRAY_SIZE +/// and arrays whose size exceed the bound \c max_field_sensitivity_array_size. /// See \ref field_sensitivityt::apply. /// /// ### Symbols representing arrays @@ -80,6 +80,13 @@ class symex_targett; class field_sensitivityt { public: + /// \param max_array_size: maximum size for which field sensitivity will be + /// applied to array cells + explicit field_sensitivityt(std::size_t max_array_size) + : max_field_sensitivity_array_size(max_array_size) + { + } + /// Assign to the individual fields of a non-expanded symbol \p lhs. This is /// required whenever prior steps have updated the full object rather than /// individual fields, e.g., in case of assignments to an array at an unknown @@ -133,12 +140,14 @@ class field_sensitivityt /// \param expr: the expression to evaluate /// \return False, if and only if, \p expr would be a single field-sensitive /// SSA expression. - static bool is_divisible(const ssa_exprt &expr); + bool is_divisible(const ssa_exprt &expr) const; private: /// whether or not to invoke \ref field_sensitivityt::apply bool run_apply = true; + const std::size_t max_field_sensitivity_array_size; + void field_assignments_rec( const namespacet &ns, goto_symex_statet &state, diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 920b3b1e699..ab3c36bdbae 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -70,6 +70,9 @@ struct symex_configt final /// includes diagnostic information about call stack and guard size. bool show_symex_steps; + /// Maximum sizes for which field sensitivity will be applied to array cells + std::size_t max_field_sensitivity_array_size; + /// \brief Construct a symex_configt using options specified in an /// \ref optionst explicit symex_configt(const optionst &options); @@ -104,6 +107,7 @@ class goto_symext guard_managert &guard_manager) : should_pause_symex(false), symex_config(options), + field_sensitivity(symex_config.max_field_sensitivity_array_size), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table), guard_manager(guard_manager), @@ -259,6 +263,9 @@ class goto_symext /// if we know the source language in use, irep_idt() otherwise. irep_idt language_mode; + /// Functor controling granularity of object accesses + field_sensitivityt field_sensitivity; + protected: /// The symbol table associated with the goto-program being executed. /// This symbol table will not have objects that are dynamically created as diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 5e44de1bf5e..84e40be36cc 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -34,10 +34,12 @@ static void get_l1_name(exprt &expr); goto_symex_statet::goto_symex_statet( const symex_targett::sourcet &_source, + field_sensitivityt &field_sensitivity, guard_managert &manager, std::function fresh_l2_name_provider) : goto_statet(manager), source(_source), + field_sensitivity(field_sensitivity), guard_manager(manager), symex_target(nullptr), record_events({true}), @@ -370,7 +372,7 @@ bool goto_symex_statet::l2_thread_read_encoding( } // only continue if an indivisible object is being accessed - if(field_sensitivityt::is_divisible(expr)) + if(field_sensitivity.is_divisible(expr)) return false; const ssa_exprt ssa_l1 = remove_level_2(expr); @@ -498,7 +500,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared( } // only continue if an indivisible object is being accessed - if(field_sensitivityt::is_divisible(expr)) + if(field_sensitivity.is_divisible(expr)) return write_is_shared_resultt::NOT_SHARED; if(atomic_section_id != 0) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 7149ca8583f..4007a503657 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -47,6 +47,7 @@ class goto_symex_statet final : public goto_statet public: goto_symex_statet( const symex_targett::sourcet &, + field_sensitivityt &field_sensitivity, guard_managert &manager, std::function fresh_l2_name_provider); ~goto_symex_statet(); @@ -67,6 +68,9 @@ class goto_symex_statet final : public goto_statet /// for error traces even after symbolic execution has finished. symbol_tablet symbol_table; + /// Reference to the functor, owned by goto_symext, used for renaming. + field_sensitivityt &field_sensitivity; + // Manager is required to be able to resize the thread vector guard_managert &guard_manager; symex_target_equationt *symex_target; @@ -120,8 +124,6 @@ class goto_symex_statet final : public goto_statet bool record_value, bool allow_pointer_unsoundness = false); - field_sensitivityt field_sensitivity; - protected: template void rename_address(exprt &expr, const namespacet &ns); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 817affa9301..1160835ec17 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -204,7 +204,7 @@ void symex_assignt::assign_non_struct_symbol( current_assignment_type); const ssa_exprt &l1_lhs = assignment.lhs; - if(field_sensitivityt::is_divisible(l1_lhs)) + if(state.field_sensitivity.is_divisible(l1_lhs)) { // Split composite symbol lhs into its components state.field_sensitivity.field_assignments( diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 0ea755bc06d..2f6d9da4dc6 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -394,7 +394,7 @@ void goto_symext::symex_printf( else { clean_expr(*va_args, state, false); - *va_args = field_sensitivityt{}.apply(ns, state, *va_args, false); + *va_args = field_sensitivity.apply(ns, state, *va_args, false); *va_args = state.rename(*va_args, ns).get(); if(va_args->id() != ID_array) { diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 535f2eefd23..6a1c5ab50ce 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -618,7 +618,7 @@ static void merge_names( } // field sensitivity: only merge on individual fields - if(field_sensitivityt::is_divisible(ssa)) + if(dest_state.field_sensitivity.is_divisible(ssa)) return; // shared variables are renamed on every access anyway, we don't need to diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index f2cd4c77a70..1641583eefd 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -44,7 +44,9 @@ symex_configt::symex_configt(const optionst &options) partial_loops(options.get_bool_option("partial-loops")), 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_symex_steps(options.get_bool_option("show-goto-symex-steps")), + max_field_sensitivity_array_size( + options.get_unsigned_int_option("max-field-sensitivity-array-size")) { } @@ -347,6 +349,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( // create and prepare the state auto state = util_make_unique( symex_targett::sourcet(entry_point_id, start_function->body), + field_sensitivity, guard_manager, [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); }); diff --git a/src/util/magic.h b/src/util/magic.h index 3eaac31a99a..5fb4d986a4b 100644 --- a/src/util/magic.h +++ b/src/util/magic.h @@ -18,6 +18,6 @@ constexpr std::size_t DSTRING_NUMBERS_MAX = 64; /// Limit the size of arrays for which field_sensitivity gets applied. /// Necessary because large constant arrays slow-down the process. -constexpr std::size_t MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64; +constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64; #endif diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp index 46858ce15ad..bb310223568 100644 --- a/unit/goto-symex/goto_symex_state.cpp +++ b/unit/goto-symex/goto_symex_state.cpp @@ -35,12 +35,14 @@ SCENARIO( // Initialize goto state std::list target; symex_targett::sourcet source{"fun", target.begin()}; + field_sensitivityt field_sensitivity{ + DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE}; guard_managert manager; std::size_t fresh_name_count = 1; auto fresh_name = [&fresh_name_count](const irep_idt &) { return fresh_name_count++; }; - goto_symex_statet state{source, manager, fresh_name}; + goto_symex_statet state{source, field_sensitivity, manager, fresh_name}; // Initialize dirty field of state incremental_dirtyt dirty; diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index ffa69c1b772..3615d9538d2 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -43,12 +43,14 @@ SCENARIO( // Initialize goto state std::list target; symex_targett::sourcet source{"fun", target.begin()}; + field_sensitivityt field_sensitivity{ + DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE}; guard_managert manager; std::size_t fresh_name_count = 1; auto fresh_name = [&fresh_name_count](const irep_idt &) { return fresh_name_count++; }; - goto_symex_statet state{source, manager, fresh_name}; + goto_symex_statet state{source, field_sensitivity, manager, fresh_name}; // Initialize dirty field of state incremental_dirtyt dirty; diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index 60b7aa47432..3955740c6ad 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -52,10 +52,12 @@ SCENARIO( // Initialize goto state std::list target; symex_targett::sourcet source{"fun", target.begin()}; + field_sensitivityt field_sensitivity{ + DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE}; guard_managert guard_manager; std::size_t count = 0; auto fresh_name = [&count](const irep_idt &) { return count++; }; - goto_symex_statet state{source, guard_manager, fresh_name}; + goto_symex_statet state{source, field_sensitivity, guard_manager, fresh_name}; GIVEN("A value set in which pointer symbol `ptr1` only points to `&value1`") { @@ -246,7 +248,6 @@ SCENARIO( // struct_symbol..pointer_field <- &value1 { - field_sensitivityt field_sensitivity; const exprt index_fs = field_sensitivity.apply(ns, state, member_l1.get(), true); value_set.assign(index_fs, address1_l1.get(), ns, false, false); From ab8fd3bd7e3120f84eff75efa2f5ad49a5a58458 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Aug 2019 08:13:19 +0100 Subject: [PATCH 20/21] Add max-field-sensitivity-array-size option together with no-array-field-sensitivity, this makes it possible to control the maximum size for which the transformation is applied and totally deactivate field sensitivity for arrays if needed. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 19 +++++++++++++++++++ src/cbmc/cbmc_parse_options.cpp | 19 +++++++++++++++++++ src/goto-checker/bmc_util.h | 12 +++++++++++- src/goto-symex/symex_main.cpp | 7 ++++++- 4 files changed, 55 insertions(+), 2 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ebd9ffc2988..2be68f579eb 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -135,6 +135,25 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) parse_java_language_options(cmdline, options); parse_java_object_factory_options(cmdline, options); + if(cmdline.isset("max-field-sensitivity-array-size")) + { + options.set_option( + "max-field-sensitivity-array-size", + cmdline.get_value("max-field-sensitivity-array-size")); + } + + if(cmdline.isset("no-array-field-sensitivity")) + { + if(cmdline.isset("max-field-sensitivity-array-size")) + { + log.error() + << "--no-array-field-sensitivity and --max-field-sensitivity-array-size" + << " must not be given together" << messaget::eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + options.set_option("no-array-field-sensitivity", true); + } + if(cmdline.isset("show-symex-strategies")) { log.status() << show_path_strategies() << messaget::eom; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2c74dd4a826..48e3df60fe1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -147,6 +147,25 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } + if(cmdline.isset("max-field-sensitivity-array-size")) + { + options.set_option( + "max-field-sensitivity-array-size", + cmdline.get_value("max-field-sensitivity-array-size")); + } + + if(cmdline.isset("no-array-field-sensitivity")) + { + if(cmdline.isset("max-field-sensitivity-array-size")) + { + log.error() + << "--no-array-field-sensitivity and --max-field-sensitivity-array-size" + << " must not be given together" << messaget::eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + options.set_option("no-array-field-sensitivity", true); + } + if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions")) { log.error() diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 3eaf779efdd..99c17dd0f47 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -186,7 +186,8 @@ void run_property_decider( "(show-symex-strategies)" \ "(depth):" \ "(unwind):" \ - "(unwindset):" \ + "(max-field-sensitivity-array-size):" \ + "(no-array-field-sensitivity)" \ "(graphml-witness):" \ "(unwindset):" @@ -198,6 +199,15 @@ void run_property_decider( " --program-only only show program expression\n" \ " --show-loops show the loops in the program\n" \ " --depth nr limit search depth\n" \ + " --max-field-sensitivity-array-size M\n" \ + " maximum size M of arrays for which field\n" \ + " sensitivity will be applied to array,\n" \ + " the default is 64\n" \ + " --no-array-field-sensitivity\n" \ + " deactivate field sensitivity for arrays, " \ + "this is\n" \ + " equivalent to setting the maximum field \n" \ + " sensitivity size for arrays to 0\n" \ " --unwind nr unwind nr times\n" \ " --unwindset L:B,... unwind loop L with a bound of B\n" \ " (use --show-loops to get the loop IDs)\n" \ diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 1641583eefd..51e26804668 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -46,7 +46,12 @@ symex_configt::symex_configt(const optionst &options) run_validation_checks(options.get_bool_option("validate-ssa-equation")), show_symex_steps(options.get_bool_option("show-goto-symex-steps")), max_field_sensitivity_array_size( - options.get_unsigned_int_option("max-field-sensitivity-array-size")) + options.is_set("no-array-field-sensitivity") + ? 0 + : options.is_set("max-field-sensitivity-array-size") + ? options.get_unsigned_int_option( + "max-field-sensitivity-array-size") + : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE) { } From 9684a255babce72113948da9246201f5919abdb2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Aug 2019 08:20:57 +0100 Subject: [PATCH 21/21] Add tests for field sensitivity options This checks that field sensitivity applies or not to arrays depending on their size and the value of the option. --- .../test-max-array-size-10.desc | 20 +++++++++++++++++++ .../test-max-array-size-9.desc | 11 ++++++++++ .../test-no-array-field-sensitivity.desc | 11 ++++++++++ 3 files changed, 42 insertions(+) create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc new file mode 100644 index 00000000000..9526f00fcb0 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc @@ -0,0 +1,20 @@ +CORE +Test.class +--function Test.main --show-vcc --max-field-sensitivity-array-size 10 +symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\] +symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\] +symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\] +symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\] +symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\] +symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\] +symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\] +symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\] +symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\] +symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\] +symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1 +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This checks that field sensitvity is still applied to an array of size 10 +when the max is set to 10. \ No newline at end of file diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc new file mode 100644 index 00000000000..1ebf5798464 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--function Test.main --show-vcc --max-field-sensitivity-array-size 9 +^EXIT=0$ +^SIGNAL=0$ +symex_dynamic::dynamic_2_array#[0-9]\[1\] +-- +symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\] +-- +This checks that field sensitvity is not applied to an array of size 10 +when the max is set to 9. \ No newline at end of file diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc new file mode 100644 index 00000000000..fbc5a83f0f5 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--function Test.main --show-vcc --no-array-field-sensitivity +^EXIT=0$ +^SIGNAL=0$ +symex_dynamic::dynamic_2_array#[0-9]\[1\] +-- +symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\] +-- +This checks that field sensitvity is not applied to arrays when +no-array-field-sensitivity is used. \ No newline at end of file