From 885fe7d89cf265b2327cf116e4555811293233ae Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 15:34:26 +0000 Subject: [PATCH 1/8] Do not shadow "symbols" There is a class member of the same name, use "symbols_in_constraint" instead. --- src/solvers/refinement/refine_arrays.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index aa67f97c625..2e713b44d39 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -119,9 +119,9 @@ void bv_refinementt::freeze_lazy_constraints() for(const auto &constraint : lazy_array_constraints) { - std::set symbols; - find_symbols(constraint.lazy, symbols); - for(const auto &symbol : symbols) + std::set symbols_in_constraint; + find_symbols(constraint.lazy, symbols_in_constraint); + for(const auto &symbol : symbols_in_constraint) { const bvt bv=convert_bv(symbol); forall_literals(b_it, bv) From fbc56c0a71ff2a373ce3b7c9403de19b9030b9f0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 7 Jan 2019 14:25:33 +0000 Subject: [PATCH 2/8] Do not shadow "result" There is a class member named "result", rename the local variable to "eval_result." --- .../refinement/string_builtin_function.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 51a6e7c1fa7..2da5d89cfa7 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -129,12 +129,12 @@ std::vector string_concatenation_builtin_functiont::eval( ? std::max(std::min(args_value[1], input2_size), start_index) : input2_size; - std::vector result(input1_value); - result.insert( - result.end(), + std::vector eval_result(input1_value); + eval_result.insert( + eval_result.end(), input2_value.begin() + numeric_cast_v(start_index), input2_value.begin() + numeric_cast_v(end_index)); - return result; + return eval_result; } string_constraintst string_concatenation_builtin_functiont::constraints( @@ -458,12 +458,12 @@ std::vector string_insertion_builtin_functiont::eval( ? std::max(std::min(args_value[2], input2_size), mp_integer(0)) : input2_size; - std::vector result(input1_value); - result.insert( - result.begin() + numeric_cast_v(offset), + std::vector eval_result(input1_value); + eval_result.insert( + eval_result.begin() + numeric_cast_v(offset), input2_value.begin() + numeric_cast_v(start), input2_value.begin() + numeric_cast_v(end)); - return result; + return eval_result; } optionalt string_insertion_builtin_functiont::eval( From 2c45dae17d08e03f0a3fc619ae7e65dfb6227274 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 15:49:05 +0000 Subject: [PATCH 3/8] Do not shadow "res" Rename both instances, the first to "initial_result" and the second to "refined_result." --- src/solvers/refinement/string_refinement.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8aa89e992c3..5a91ea9ecc5 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -738,8 +738,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() // Initial try without index set const auto get = [this](const exprt &expr) { return this->get(expr); }; dependencies.clean_cache(); - const decision_proceduret::resultt res=supert::dec_solve(); - if(res==resultt::D_SATISFIABLE) + const decision_proceduret::resultt initial_result = supert::dec_solve(); + if(initial_result == resultt::D_SATISFIABLE) { bool satisfied; std::vector counter_examples; @@ -762,7 +762,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() else { debug() << "check_SAT: got UNSAT or ERROR" << eom; - return res; + return initial_result; } initial_index_set(index_sets, ns, axioms); @@ -776,9 +776,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() while((loop_bound_--)>0) { dependencies.clean_cache(); - const decision_proceduret::resultt res=supert::dec_solve(); + const decision_proceduret::resultt refined_result = supert::dec_solve(); - if(res==resultt::D_SATISFIABLE) + if(refined_result == resultt::D_SATISFIABLE) { bool satisfied; std::vector counter_examples; @@ -833,8 +833,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() } else { - debug() << "check_SAT: default return " << static_cast(res) << eom; - return res; + debug() << "check_SAT: default return " + << static_cast(refined_result) << eom; + return refined_result; } } debug() << "string_refinementt::dec_solve reached the maximum number" From fbd6b58eb51e7312267b8fa684f3484b299bc31c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 15:50:53 +0000 Subject: [PATCH 4/8] Do not shadow "instances" Rename the first use to "initial_instances" --- src/solvers/refinement/string_refinement.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 5a91ea9ecc5..3dbe59ba22b 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -768,9 +768,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() initial_index_set(index_sets, ns, axioms); update_index_set(index_sets, ns, current_constraints); current_constraints.clear(); - const auto instances = + const auto initial_instances = generate_instantiations(index_sets, axioms, not_contain_witnesses); - for(const auto &instance : instances) + for(const auto &instance : initial_instances) add_lemma(instance); while((loop_bound_--)>0) From 04493f3f00e3fce2041455a1d0f59d9cf6d61697 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 15:59:10 +0000 Subject: [PATCH 5/8] Do not shadow "fresh_symbol" There is no need to pass a class member as an argument. --- .../instantiate_not_contains.cpp | 3 +-- src/solvers/refinement/string_builtin_function.cpp | 4 ++-- src/solvers/refinement/string_constraint_generator.h | 3 --- .../refinement/string_constraint_generator_comparison.cpp | 4 ---- src/solvers/refinement/string_constraint_generator_main.cpp | 6 ++---- 5 files changed, 5 insertions(+), 15 deletions(-) diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index b5c936b32f6..86d4ec5c572 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -191,8 +191,7 @@ SCENARIO("instantiate_not_contains", // Generating the corresponding axioms and simplifying, recording info string_constraint_generatort generator(empty_ns); - const auto pair = generator.add_axioms_for_function_application( - generator.fresh_symbol, func); + const auto pair = generator.add_axioms_for_function_application(func); const string_constraintst &constraints = pair.second; std::string axioms; diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 2da5d89cfa7..e82eb5b9487 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -634,8 +634,8 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt( string_constraintst string_builtin_function_with_no_evalt::constraints( string_constraint_generatort &generator) const { - auto pair = generator.add_axioms_for_function_application( - generator.fresh_symbol, function_application); + auto pair = + generator.add_axioms_for_function_application(function_application); pair.second.existential.push_back(equal_exprt(pair.first, return_code)); return pair.second; } diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 3846ff91c4e..3a1d6de2157 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -127,7 +127,6 @@ class string_constraint_generatort final explicit string_constraint_generatort(const namespacet &ns); std::pair add_axioms_for_function_application( - symbol_generatort &fresh_symbol, const function_application_exprt &expr); symbol_generatort fresh_symbol; @@ -150,7 +149,6 @@ class string_constraint_generatort final /// string pointers. /// \deprecated Not tested. std::pair add_axioms_for_intern( - symbol_generatort &fresh_symbol, const function_application_exprt &f); exprt associate_array_to_pointer(const function_application_exprt &f); @@ -161,7 +159,6 @@ class string_constraint_generatort final // The specification is partial: the actual value is not actually computed // but we ensure that hash codes of equal strings are equal. std::pair add_axioms_for_hash_code( - symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool); diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 9fe1b92759a..590557c6306 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -182,13 +182,11 @@ std::pair add_axioms_for_equals_ignore_case( /// These axioms are, for each string `s` on which hash was called: /// * \f$ hash(str)=hash(s) \lor |str| \ne |s| /// \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with argument refined_string `str` /// \param pool: pool of arrays representing strings /// \return integer expression `hash(str)` std::pair string_constraint_generatort::add_axioms_for_hash_code( - symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) { @@ -302,13 +300,11 @@ std::pair add_axioms_for_compare_to( /// Add axioms stating that the return value for two equal string should be the /// same /// \deprecated never tested -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one string argument /// \return a string expression DEPRECATED("never tested") std::pair string_constraint_generatort::add_axioms_for_intern( - symbol_generatort &fresh_symbol, const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 1); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 5f16df11e8b..02da80879fa 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -363,12 +363,10 @@ optionalt string_constraint_generatort::make_array_pointer_association( /// strings contained in this call are converted to objects of type /// `string_exprt`, through adding axioms. Axioms are then added to enforce that /// the result corresponds to the function application. -/// \param fresh_symbol: generator of fresh symbols /// \param expr: an expression containing a function application /// \return expression corresponding to the result of the function application std::pair string_constraint_generatort::add_axioms_for_function_application( - symbol_generatort &fresh_symbol, const function_application_exprt &expr) { const irep_idt &id = get_function_name(expr); @@ -396,7 +394,7 @@ string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_contains_func) return add_axioms_for_contains(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_hash_code_func) - return add_axioms_for_hash_code(fresh_symbol, expr, array_pool); + return add_axioms_for_hash_code(expr, array_pool); else if(id==ID_cprover_string_index_of_func) return add_axioms_for_index_of(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_last_index_of_func) @@ -463,7 +461,7 @@ string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_replace_func) return add_axioms_for_replace(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_intern_func) - return add_axioms_for_intern(fresh_symbol, expr); + return add_axioms_for_intern(expr); else if(id==ID_cprover_string_format_func) return add_axioms_for_format(fresh_symbol, expr, array_pool, message, ns); else if(id == ID_cprover_string_constrain_characters_func) From fcbc9142b70564c4c9440b7616ccf8e04140278e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 16:01:46 +0000 Subject: [PATCH 6/8] Do not shadow "constraints" Rename the method-local ones "intern_constraints" and "hash_constraints." --- .../string_constraint_generator_comparison.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 590557c6306..7c956342ffb 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -191,7 +191,7 @@ string_constraint_generatort::add_axioms_for_hash_code( array_poolt &pool) { PRECONDITION(f.arguments().size() == 1); - string_constraintst constraints; + string_constraintst hash_constraints; const array_string_exprt str = get_string_expr(pool, f.arguments()[0]); const typet &return_type = f.type(); const typet &index_type = str.length().type(); @@ -210,9 +210,9 @@ string_constraint_generatort::add_axioms_for_hash_code( and_exprt( notequal_exprt(str[i], it.first[i]), and_exprt(length_gt(str, i), is_positive(i)))); - constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3))); + hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3))); } - return {hash, std::move(constraints)}; + return {hash, std::move(hash_constraints)}; } /// Lexicographic comparison of two strings @@ -308,7 +308,7 @@ string_constraint_generatort::add_axioms_for_intern( const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 1); - string_constraintst constraints; + string_constraintst intern_constraints; const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); // For now we only enforce content equality and not pointer equality const typet &return_type=f.type(); @@ -326,14 +326,14 @@ string_constraint_generatort::add_axioms_for_intern( exprt::operandst disj; for(auto it : intern_of_string) disj.push_back(equal_exprt(intern, it.second)); - constraints.existential.push_back(disjunction(disj)); + intern_constraints.existential.push_back(disjunction(disj)); // WARNING: the specification may be incomplete or incorrect for(auto it : intern_of_string) if(it.second!=str) { symbol_exprt i = fresh_symbol("index_intern", index_type); - constraints.existential.push_back(or_exprt( + intern_constraints.existential.push_back(or_exprt( equal_exprt(it.second, intern), or_exprt( notequal_exprt(str.length(), it.first.length()), @@ -344,5 +344,5 @@ string_constraint_generatort::add_axioms_for_intern( and_exprt(length_gt(str, i), is_positive(i))))))); } - return {intern, std::move(constraints)}; + return {intern, std::move(intern_constraints)}; } From 4c2f940e5c83fc83b2aea0560146e10a6ba425e5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 16:16:33 +0000 Subject: [PATCH 7/8] Do not shadow parameter "f" Rename container elements to "positive" and "negative." --- .../refinement/string_constraint_generator_float.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index f7937430051..e822e1b5d7f 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -422,10 +422,12 @@ std::pair add_axioms_from_float_scientific_notation( int_type); array_exprt conversion_factor_table( array_typet(float_type, conversion_factor_table_size)); - for(const auto &f : two_power_e_over_ten_power_d_table_negatives) - conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); - for(const auto &f : two_power_e_over_ten_power_d_table) - conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); + for(const auto &negative : two_power_e_over_ten_power_d_table_negatives) + conversion_factor_table.copy_to_operands( + constant_float(negative, float_spec)); + for(const auto &positive : two_power_e_over_ten_power_d_table) + conversion_factor_table.copy_to_operands( + constant_float(positive, float_spec)); // The index in the table, corresponding to exponent e is e+128 plus_exprt shifted_index(bin_exponent, from_integer(128, int_type)); From adde39e177138d3f181fbffa72e46feb666090ce Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 8 Jan 2019 12:06:38 +0000 Subject: [PATCH 8/8] Rename parameter f to float_expr A single-character name is not very descriptive, longer symbol names bear no runtime overhead. --- .../string_constraint_generator_float.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index e822e1b5d7f..6ff6d9ee240 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -337,14 +337,14 @@ std::pair add_axioms_for_fractional_part( /// \todo For now we only consider single precision. /// \param fresh_symbol: generator of fresh symbols /// \param res: string expression representing the float in scientific notation -/// \param f: a float expression, which is positive +/// \param float_expr: a float expression, which is positive /// \param array_pool: pool of arrays representing strings /// \param ns: namespace /// \return a integer expression different from 0 to signal an exception std::pair add_axioms_from_float_scientific_notation( symbol_generatort &fresh_symbol, const array_string_exprt &res, - const exprt &f, + const exprt &float_expr, array_poolt &array_pool, const namespacet &ns) { @@ -359,13 +359,13 @@ std::pair add_axioms_from_float_scientific_notation( exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type); // `bin_exponent` is $e$ in the formulas - exprt bin_exponent=get_exponent(f, float_spec); + exprt bin_exponent = get_exponent(float_expr, float_spec); // $m$ from the formula is a value between 0.0 and 2.0 represented // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000. // `bin_significand_int` represents $m * 0x800000$ - exprt bin_significand_int= - get_significand(f, float_spec, unsignedbv_typet(32)); + exprt bin_significand_int = + get_significand(float_expr, float_spec, unsignedbv_typet(32)); // `bin_significand` represents $m$ and is obtained // by multiplying `binary_significand_as_int` by // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7 @@ -375,7 +375,8 @@ std::pair add_axioms_from_float_scientific_notation( // This is a first approximation of the exponent that will adjust // if the fraction we get is greater than 10 - exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec); + exprt dec_exponent_estimate = + estimate_decimal_exponent(float_expr, float_spec); // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128] std::vector two_power_e_over_ten_power_d_table( @@ -462,7 +463,7 @@ std::pair add_axioms_from_float_scientific_notation( minus_exprt fractional_part( dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); - // shifted_float is floor(f * 1e5) + // shifted_float is floor(float_expr * 1e5) exprt shifting=constant_float(1e5, float_spec); exprt shifted_float= round_expr_to_zero(floatbv_mult(fractional_part, shifting)); @@ -471,7 +472,7 @@ std::pair add_axioms_from_float_scientific_notation( // the exponent notation. exprt max_non_exponent_notation=from_integer(100000, shifted_float.type()); - // fractional_part_shifted is floor(f * 100000) % 100000 + // fractional_part_shifted is floor(float_expr * 100000) % 100000 const mod_exprt fractional_part_shifted( shifted_float, max_non_exponent_notation);