From bbc3f633e97f99158967771fb8e71a4209914a73 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 19 Apr 2018 00:24:12 +0000 Subject: [PATCH 1/3] Note type inconsistencies in solver axioms and avoid simplifying array_poolt::make_char_array_for_char_pointer generates conditional expressions denoting possible array sizes. This results in types without a fixed size, and is used to construct ifthenelse expressions that may have multiple types. This is not permitted, and thus must be filtered out before passing to further processing, such as simplification or flattening. --- .../string_constraint_generator_main.cpp | 2 + src/solvers/strings/string_refinement.cpp | 48 ++++++++++++++++++- 2 files changed, 49 insertions(+), 1 deletion(-) diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 39705e048b2..05e38461bfb 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -120,6 +120,8 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer( if_expr.cond(), to_array_type(t.type()).size(), to_array_type(f.type()).size())); + // BEWARE: this expression is possibly type-inconsistent and must not be + // used for any purposes other than passing it to concretisation return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type)); } const bool is_constant_array = diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 70cd5b45e6b..6c1d5e415e2 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -854,6 +854,49 @@ decision_proceduret::resultt string_refinementt::dec_solve() return resultt::D_ERROR; } +/// In a best-effort manner, try to clean up the type inconsistencies introduced +/// by \ref array_poolt::make_char_array_for_char_pointer, which creates +/// conditional expressions for the size of arrays. The cleanup is achieved by +/// removing branches that are found to be infeasible, and by simplifying the +/// conditional size expressions previously generated. +/// \param expr: Expression to be cleaned +/// \param ns: Namespace +/// \return Cleaned expression +static exprt adjust_if_recursive(exprt expr, const namespacet &ns) +{ + for(auto it = expr.depth_begin(); it != expr.depth_end();) + { + if(it->id() == ID_if) + { + if_exprt if_expr = to_if_expr(*it); + const exprt simp_cond = simplify_expr(if_expr.cond(), ns); + if(simp_cond.is_true()) + { + it.mutate() = adjust_if_recursive(if_expr.true_case(), ns); + it.next_sibling_or_parent(); + } + else if(simp_cond.is_false()) + { + it.mutate() = adjust_if_recursive(if_expr.false_case(), ns); + it.next_sibling_or_parent(); + } + else if( + it->type().id() == ID_array && + to_array_type(it->type()).size().id() == ID_if) + { + simplify(to_array_type(it.mutate().type()).size(), ns); + ++it; + } + else + ++it; + } + else + ++it; + } + + return expr; +} + /// Add the given lemma to the solver. /// \param lemma: a Boolean expression /// \param simplify_lemma: whether the lemma should be simplified before being @@ -869,7 +912,10 @@ void string_refinementt::add_lemma( exprt simple_lemma = lemma; if(simplify_lemma) + { + simple_lemma = adjust_if_recursive(std::move(simple_lemma), ns); simplify(simple_lemma, ns); + } if(simple_lemma.is_true()) { @@ -917,7 +963,7 @@ static optionalt get_array( { const auto eom = messaget::eom; const exprt &size = arr.length(); - exprt arr_val = simplify_expr(super_get(arr), ns); + exprt arr_val = simplify_expr(adjust_if_recursive(super_get(arr), ns), ns); exprt size_val = super_get(size); size_val = simplify_expr(size_val, ns); const typet char_type = arr.type().subtype(); From c564c2cdf6b416965e839ce9625649940698cf4f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 18 Apr 2018 13:10:35 +0100 Subject: [PATCH 2/3] Expression simplification must not alter the type --- src/util/simplify_expr.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 8041720736b..b2275cb421b 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2548,6 +2548,7 @@ bool simplify_exprt::simplify_rec(exprt &expr) if(!result) { + POSTCONDITION(tmp.type() == expr.type()); expr.swap(tmp); #ifdef USE_CACHE From 861658616de5d16a50ffd58d622a20f7cb630f87 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 12:12:32 +0000 Subject: [PATCH 3/3] Simplifier: As we now assert type equality we can remove a safety net If the simplifier receives an expression that isn't type-consistent it might produce a type-inconsistent result, but we will now fail an invariant in that case. --- src/util/simplify_expr_struct.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 63544275632..76452119cff 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -265,8 +265,7 @@ bool simplify_exprt::simplify_member(exprt &expr) if( equivalent_member.has_value() && equivalent_member.value().id() != ID_byte_extract_little_endian && - equivalent_member.value().id() != ID_byte_extract_big_endian && - equivalent_member.value().type() == expr.type()) + equivalent_member.value().id() != ID_byte_extract_big_endian) { expr = equivalent_member.value(); simplify_rec(expr);