diff --git a/jbmc/regression/jbmc-strings/ClassName/test.desc b/jbmc/regression/jbmc-strings/ClassName/test.desc index 6a9bd1782a0..7e7dd4c1be3 100644 --- a/jbmc/regression/jbmc-strings/ClassName/test.desc +++ b/jbmc/regression/jbmc-strings/ClassName/test.desc @@ -4,5 +4,3 @@ test.class ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -\[java::test\.main:\(\)V\.assertion\.1\] line 5 assertion at file test\.java line 5 function java::test\.main:\(\)V bytecode-index 8: SUCCESS$ -\[java::test\.main:\(\)V\.assertion\.2\] line 6 assertion at file test\.java line 6 function java::test\.main:\(\)V bytecode-index 19: SUCCESS$ diff --git a/jbmc/regression/jbmc-strings/long_string/test_abort.desc b/jbmc/regression/jbmc-strings/long_string/test_abort.desc index 16e6b93c80d..1bc612712b3 100644 --- a/jbmc/regression/jbmc-strings/long_string/test_abort.desc +++ b/jbmc/regression/jbmc-strings/long_string/test_abort.desc @@ -3,7 +3,7 @@ Test.class --function Test.checkAbort --trace ^EXIT=10$ ^SIGNAL=0$ -dynamic_object[0-9]*=\(assignment removed\) +dynamic_object[0-9]*=.*\?.* -- -- This tests that the object does not appear in the trace, because concretizing diff --git a/jbmc/regression/jbmc-strings/nondet_propagation/Test.class b/jbmc/regression/jbmc-strings/nondet_propagation/Test.class new file mode 100644 index 00000000000..7a3a31f7637 Binary files /dev/null and b/jbmc/regression/jbmc-strings/nondet_propagation/Test.class differ diff --git a/jbmc/regression/jbmc-strings/nondet_propagation/Test.java b/jbmc/regression/jbmc-strings/nondet_propagation/Test.java new file mode 100644 index 00000000000..af67badf200 --- /dev/null +++ b/jbmc/regression/jbmc-strings/nondet_propagation/Test.java @@ -0,0 +1,8 @@ +public class Test { + public String foo() { + final int i = 10; + final String retval = Integer.toHexString(i); + assert(false); + return retval; + } +} diff --git a/jbmc/regression/jbmc-strings/nondet_propagation/test.desc b/jbmc/regression/jbmc-strings/nondet_propagation/test.desc new file mode 100644 index 00000000000..d59f6fa2924 --- /dev/null +++ b/jbmc/regression/jbmc-strings/nondet_propagation/test.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--function Test.foo --trace +^EXIT=10$ +^SIGNAL=0$ +dynamic_object1=\{ 'a' \} +-- +-- +Nondet propagation would previously cause an output like +dynamic_object1=dynamic_object1#2, because the mapping between dynamic_object1#2 +and a nondet-symbol, which was otherwise being used by the string solver, was +not established. diff --git a/regression/cbmc/constant_folding3/main.c b/regression/cbmc/constant_folding3/main.c new file mode 100644 index 00000000000..7e5ea410e30 --- /dev/null +++ b/regression/cbmc/constant_folding3/main.c @@ -0,0 +1,18 @@ +typedef struct _pair +{ + int x; + int y; +} pair; + +int __VERIFIER_nondet_int(); + +int main(void) +{ + pair p1 = {.x = 0, .y = __VERIFIER_nondet_int()}; + pair p2 = {}; + p2.x = __VERIFIER_nondet_int(); + + __CPROVER_assert(p1.x == p2.y, "true by constant propagation"); + + return 0; +} diff --git a/regression/cbmc/constant_folding3/test.desc b/regression/cbmc/constant_folding3/test.desc new file mode 100644 index 00000000000..201dc9bdb6e --- /dev/null +++ b/regression/cbmc/constant_folding3/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +^Generated 1 VCC\(s\), 0 remaining after simplification$ +-- +^warning: ignoring diff --git a/src/goto-symex/goto_symex_is_constant.h b/src/goto-symex/goto_symex_is_constant.h index f218ff53b32..be131025dca 100644 --- a/src/goto-symex/goto_symex_is_constant.h +++ b/src/goto-symex/goto_symex_is_constant.h @@ -45,6 +45,20 @@ class goto_symex_is_constantt : public is_constantt */ return false; } + else if(expr.id() == ID_if) + { + // don't treat nested if_exprt as constant (even when they are!) as this + // may give rise to large expressions that we repeatedly pass to the + // simplifier; this is observable on regression/cbmc-library/memmove-01 + const if_exprt &if_expr = to_if_expr(expr); + if( + if_expr.true_case().id() == ID_if || if_expr.false_case().id() == ID_if) + { + return false; + } + } + else if(expr.id() == ID_nondet_symbol) + return true; return is_constantt::is_constant(expr); } diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index f655298301e..b4e1f0ba9de 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -67,9 +67,20 @@ literalt arrayst::record_array_equality( collect_arrays(op0); collect_arrays(op1); + lhs_rhs_map.emplace(op0, op1); + return array_equalities.back().l; } +exprt arrayst::get(const exprt &expr) const +{ + auto it = lhs_rhs_map.find(expr); + if(it != lhs_rhs_map.end() && it->first != it->second) + return get(it->second); + else + return SUB::get(expr); +} + void arrayst::collect_indices() { for(std::size_t i=0; i array_equalitiest; array_equalitiest array_equalities; + std::unordered_map lhs_rhs_map; // this is used to find the clusters of arrays being compared union_find arrays; diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 548ebfbeea1..2e22180fc3c 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -977,6 +977,8 @@ static optionalt get_array( { const exprt &size = arr.length(); exprt arr_val = simplify_expr(adjust_if_recursive(super_get(arr), ns), ns); + if(arr_val.id() == ID_array) + return std::move(arr_val); exprt size_val = super_get(size); size_val = simplify_expr(size_val, ns); const typet char_type = arr.type().subtype(); diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index acb9dc99dbf..13a4b768ac2 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -241,7 +241,9 @@ bool is_constantt::is_constant(const exprt &expr) const expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union || // byte_update works, byte_extract may be out-of-bounds expr.id() == ID_byte_update_big_endian || - expr.id() == ID_byte_update_little_endian) + expr.id() == ID_byte_update_little_endian || + // member works, index may be out-of-bounds + expr.id() == ID_member || expr.id() == ID_if) { return std::all_of( expr.operands().begin(), expr.operands().end(), [this](const exprt &e) { @@ -276,8 +278,12 @@ bool is_constantt::is_constant_address_of(const exprt &expr) const return is_constant(deref.pointer()); } - else if(expr.id() == ID_string_constant) + else if( + expr.id() == ID_string_constant || expr.id() == ID_array || + expr.id() == ID_struct || expr.id() == ID_union) + { return true; + } return false; }