Constant propagate string-solver function results #5129

JohnDumbell · 2019-09-25T12:52:56Z

Allows constant propagation to work on a range of general string operations.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton · 2019-09-25T13:04:14Z

src/goto-symex/goto_symex.cpp

+    int character = std::stoi(id2string(operand.get(ID_value)), nullptr, 16);
+    if (isalpha(character))
+    {
+      char buffer[33];


smowton · 2019-09-25T13:06:04Z

src/goto-symex/goto_symex.cpp

+  auto &operands = string_data.operands();
+  for(auto & operand : operands)
+  {
+    int character = std::stoi(id2string(operand.get(ID_value)), nullptr, 16);


get(ID_value) -> to_constant_expr(...).get_value()

smowton · 2019-09-25T13:08:06Z

src/goto-symex/goto_symex.cpp

+  auto &operands = string_data.operands();
+  for(auto & operand : operands)
+  {
+    int character = std::stoi(id2string(operand.get(ID_value)), nullptr, 16);


Don't parse directly, use numeric_cast_v (

cbmc/src/util/arith_tools.h

Line 149 in 7bbef4a

Target numeric_cast_v(const constant_exprt &arg)

)

smowton · 2019-09-25T13:08:59Z

src/goto-symex/goto_symex.cpp

+        if(islower(character))
+        {
+          sprintf(buffer, "%x", toupper(character));
+          operand.set(ID_value, buffer);


Don't set value, use from_integer (

cbmc/src/util/arith_tools.h

Line 160 in 7bbef4a

constant_exprt from_integer(const mp_integer &int_value, const typet &type);

)

smowton · 2019-09-25T13:09:37Z

src/goto-symex/goto_symex.cpp

+  }
+
+  return true;
+}bool goto_symext::constant_propagate_trim(


Line break after }

smowton · 2019-09-25T13:15:51Z

src/util/simplify_expr.cpp

+    if(last_index)
+    {
+      auto it = std::find_if(
+        std::next(s1_data.operands().rbegin(), starting_index),


Similarly this use of starting-index

smowton · 2019-09-25T13:17:07Z

src/util/simplify_expr.cpp

+  auto &operands = string_data.operands();
+  for(auto &operand : operands)
+  {
+    int character = std::stoi(id2string(operand.get(ID_value)), nullptr, 16);


Use arith-tools

smowton · 2019-09-25T13:17:16Z

src/util/simplify_expr.cpp

+      char buffer[33];
+      if(isupper(character))
+      {
+        sprintf(buffer, "%x", tolower(character));


Use arith-tools

smowton · 2019-09-25T13:17:34Z

src/util/simplify_expr.cpp

+  }
+}
+
+/// Simplify String.startsWith function when arguments are constant


Wrong comment

smowton · 2019-09-25T13:19:48Z

src/util/simplify_expr.cpp

+  lower_case_string_expression(first_value);
+  lower_case_string_expression(second_value);
+
+  // test whether second_value is a prefix of first_value


Given you check the sizes are equal, so this is not a prefix check, surely this is just first_value == second_value

smowton · 2019-09-25T13:21:19Z

Also, tests: these currently only look at the cases where you do expect a change. Make sure to exercise the cases where there should not be a simplification / constant propagation, and to exercise optional arguments like the starting-index for String.find / findLast

danpoe

The tests should also check that constant propagation computes the right result in addition to that there are 0 remaining VCCs after symex.

danpoe · 2019-09-25T13:47:36Z

src/goto-symex/goto_symex.cpp

+      it != operands.end();)
+  {
+    if(it->get_int(ID_value) == 20)
+      operands.erase(it);


Should be it = operands.erase(it)

Don't think it makes a difference the way I'm using it here though?

It might work though according to the documentation it becomes invalid when calling erase(it). So I'd say it's safer to use the returned iterator.

+1, it's just luck that it works here based on how std::vector's iterators happen to work (i.e. being pointers to the data array, and the array not usually being reallocated on an erase). How about

auto expr_is_space = [](const exprt &e) { const auto &constant_value = to_constant_expr(*it); return numeric_cast_v<int>(constant_value) <= ' '; } while(!operands.empty() && expr_is_space(operands.front())) operands.erase(operands.begin()); while(!operands.empty() && expr_is_space(operands.back())) operands.erase(operands.rbegin().base());

Thinking about it the current implementation has n^2 worst case runtime due to the repeated shifting of the vector when erasing elements at the beginning. It might be better to use find_if() to get iterators to the first and last non-space characters, and then copy that segment to a new vector (instead of making a copy of the original vector and then modifying it).

Sure, modified.

danpoe · 2019-09-25T14:00:06Z

src/goto-symex/goto_symex.cpp

+  for(auto it = operands.begin();
+      it != operands.end();)
+  {
+    if(it->get_int(ID_value) == 20)


We should remove whitespace characters other than space as well. Also a space is 20 in hex not in decimal.

danpoe · 2019-09-25T14:11:21Z

src/goto-symex/goto_symex.cpp

+  {
+    if(it->get_int(ID_value) == 20)
+      operands.erase(it.base()),
+      it++;


The erase(it.base()) invalidates the iterator it.

danpoe · 2019-09-25T14:12:07Z

src/goto-symex/goto_symex.h

@@ -610,6 +610,25 @@ class goto_symext
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);

+  /// Attempt to constant propogate trim operations.


propogate -> propagate

danpoe · 2019-09-25T14:12:35Z

src/goto-symex/goto_symex.h

+    const function_application_exprt &f_l1,
+    bool to_upper);
+
+  /// Attempt to constant proagate character replacement.


proagate -> propagate

danpoe · 2019-09-25T14:18:01Z

src/goto-symex/goto_symex.cpp

+    const auto &newChar = to_symbol_expr(old_data);
+
+    const auto new_char_pointer =
+      state.propagation.find(newChar.get_identifier());


Can use try_evaluate_constant() instead which does the lookup in the propagation map and returns an optional constant_exprt.

danpoe · 2019-09-25T14:28:19Z

jbmc/regression/jbmc-strings/ConstantEvaluationContains/test.desc

+CORE
+Main.class
+--function Main.contains --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$


Since --show-vcc is used, the test only prints the VCCs and checks that we have 0 remaining VCCs after symex. We also need to check though that constant propagation does compute the correct result. We should leave off --show-vcc and check that verification succeeded. (also for the other tests)

Also we should check the negative cases, i.e. here if a string doesn't contain another string.

JohnDumbell · 2019-09-25T16:58:30Z

Applied all comments and added more tests.

smowton

Main comment: the tests for negative cases shouldn't just be positive cases with a ! at the start, they should test cases where we give a proper negative response, such as equalsIgnoreCase("abc", "ADC"), for as many different reasons as our code has reasons to reject the comparison (searched-for string too short and contains a mismatch seem like the obvious ones). The goal is to make sure it doesn't accidentally fire every time. Where there are optional index restrictions as for String.compareTo make sure there are cases where the restriction is the reason for it not to work -- e.g. String.lastIndexOf("abc", "abc") == 0 but String.lastIndexOf("abc", "abc", 1) == -1

smowton · 2019-09-25T18:08:08Z

jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java

+
+    public void notContains() {
+        String str = "abcde";
+        assert !str.contains("cd");


This doesn't really test anything more than contains, except that operator! is working -- instead I think you should test some cases where contains should return false. assert !str.contains("fgh"), assert !str.contains("abcdef"), and so on -- things that should evaluate to false for different reasons.

smowton · 2019-09-25T18:08:28Z

jbmc/regression/jbmc-strings/ConstantEvaluationContains/notcontains.desc

+CORE
+Main.class
+--function Main.notContains --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$


As a non-noprop case I expect these should be decided by the simplifier

These cases usually resolve in a VCC but with a directly false guard somewhere. Might be to do with building a trace? Always been like this when I've tested and just assumed that's how things were.

smowton · 2019-09-25T18:08:47Z

jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java

+    }
+
+    public void notEqualsIgnoreCase() {
+        assert !"abc".equalsIgnoreCase("ABC");


As above, test some real negatives, not just verification success vs. failure

smowton · 2019-09-25T18:09:06Z

jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notequals.desc

+CORE
+Main.class
+--function Main.notEqualsIgnoreCase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$


Should be decided

smowton · 2019-09-25T18:11:08Z

src/goto-symex/goto_symex.cpp

+  for(auto &operand : operands)
+  {
+    auto &constant_value = to_constant_expr(operand);
+    char character = numeric_cast_v<int>(constant_value);


Careful, Java chars are 16-bit. It's fine if we only treat ASCII for now, but we should decline to const-prop when we're dealing with e.g. strings of Greek letters, which do have case-change semantics but aren't handled by 8-bit islower etc

Fair point!

smowton · 2019-09-25T18:11:52Z

src/goto-symex/goto_symex.cpp

+        {
+          std::stringstream stream;
+          stream << std::hex << toupper(character);
+          constant_value.set_value(stream.str());


Honestly these are 16-bit ints as far as CBMC is concerned, I'd use from_integer rather than hope you get the expected formatting for constant_exprt's value member

Like this for example:

cbmc/src/solvers/strings/string_constraint_generator_code_points.cpp

Line 40 in 73e410a

exprt hexD800 = from_integer(0xD800, type);

smowton · 2019-09-25T18:13:46Z

src/goto-symex/goto_symex.cpp

+  auto &old_data = f_l1.arguments().at(4);
+
+  // If it's a symbol we're using the replace(Character, Character) overload.
+  // There's another that takes CharSequence which isn't dealt with.


I'm still surprised you're looking for the ID of the expression not the type or the signature of the called function, though. What's going on there, why couldn't a symbol_exprt get passed to the other overload?

Never did in any of my testing, but yes, it's fragile. I've changed it to check for the signature instead, which is also fragile, just in different ways.

I'll get around to adding the other overload if I have time.

smowton · 2019-09-25T18:32:06Z

src/goto-symex/goto_symex.cpp

+      it != operands.end();)
+  {
+    if(it->get_int(ID_value) == 20)
+      operands.erase(it);


+1, it's just luck that it works here based on how std::vector's iterators happen to work (i.e. being pointers to the data array, and the array not usually being reallocated on an erase). How about

auto expr_is_space = [](const exprt &e) { const auto &constant_value = to_constant_expr(*it); return numeric_cast_v<int>(constant_value) <= ' '; } while(!operands.empty() && expr_is_space(operands.front())) operands.erase(operands.begin()); while(!operands.empty() && expr_is_space(operands.back())) operands.erase(operands.rbegin().base());

smowton · 2019-09-25T18:36:14Z

src/util/simplify_expr.cpp

+  for(auto &operand : operands)
+  {
+    auto &constant_value = to_constant_expr(operand);
+    char character = numeric_cast_v<int>(constant_value);


Again, watch out that you're restricting to ASCII here and refuse to const-prop anything outside that range, since we don't have a C++ widget with the same case semantics as Character.toUpperCase

romainbrenguier

I only reviewed until Add String.lastIndexOf(...) but some of the comments could apply to the following commits as well

romainbrenguier · 2019-09-26T15:32:48Z

src/goto-symex/goto_symex.cpp

+    if(character > ' ')
+    {
+      end_iter = it.base();
+      break;


use std::find_if

romainbrenguier · 2019-09-26T15:33:36Z

src/goto-symex/goto_symex.cpp

+  const constant_exprt new_char_array_length =
+    from_integer(new_operands.size(), length_type);
+
+  const array_typet new_char_array_type(char_type, new_char_array_length);


use curly braces {}

Where would those go? (And curious about why)

const array_typet new_char_array_type{char_type, new_char_array_length};
it's the preferred way of constructing an object, here are some reasons why https://stackoverflow.com/questions/18222926/why-is-list-initialization-using-curly-braces-better-than-the-alternatives

romainbrenguier · 2019-09-26T15:33:52Z

src/goto-symex/goto_symex.cpp

+    if(character > ' ')
+    {
+      start_iter = it;
+      break;


use std::find_if

romainbrenguier · 2019-09-26T15:34:32Z

src/goto-symex/goto_symex.h

+  bool constant_propagate_trim(
+    statet &state,
+    symex_assignt &symex_assign,
+    const function_application_exprt &f_l1);


can this be marked const or even static? 🌵

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java

romainbrenguier · 2019-09-26T15:45:24Z

src/goto-symex/goto_symex.cpp

+  for(auto &operand : operands)
+  {
+    auto &constant_value = to_constant_expr(operand);
+    unsigned char character = numeric_cast_v<int>(constant_value);


🚫 should use numeric_cast_v<unsigned char> or if unavailable narrow

romainbrenguier · 2019-09-26T15:46:36Z

src/goto-symex/goto_symex.cpp

+      {
+        if(islower(character))
+        {
+          irept hex_value =


why hex_value? this is actually an exprt

romainbrenguier · 2019-09-26T15:49:07Z

src/util/simplify_expr.cpp

+    {
+      auto starting_offset = 0;
+      if(starting_index > 0)
+        starting_offset = search_string_size - starting_index;


Use ternary if to define starting_offset and make it const. Avoid using auto when the type is not explicit.

romainbrenguier · 2019-09-26T15:52:14Z

src/util/simplify_expr.cpp

+        return from_integer(
+          std::distance(s1_data.operands().begin(), it.base()) - 1,
+          expr.type());
+      }


should return -1 in the other case no? 🍊

Would think so, but no, the other case works fine without it. Assume it's notched along +1 due to the way the reverse iterator works.

Edit: Yeah, something's off with the way the reverse iterator works in this instance, swapped it to use find_end instead.

romainbrenguier · 2019-09-26T15:52:24Z

src/util/simplify_expr.cpp

+
+      if(it != s1_data.operands().end())
+        return from_integer(
+          std::distance(s1_data.operands().begin(), it), expr.type());


romainbrenguier · 2019-09-27T06:56:41Z

src/goto-symex/goto_symex.cpp

+
+  // If it's a symbol we're using the replace(Character, Character) overload.
+  // There's another that takes CharSequence which isn't dealt with.
+  if(target_overload == "java::java.lang.String.replace:(CC)Ljava/lang/String;")


🚫 check the type of the arguments instead

I don't think this should block, either one achieves what's needed

that's java specific code in symex

Doh, right, sure. Use the types, as Romain said.

romainbrenguier · 2019-09-27T06:57:03Z

src/goto-symex/goto_symex.cpp

+
+  irep_idt target_overload = f_l1.source_location().get_function();
+
+  // If it's a symbol we're using the replace(Character, Character) overload.


replace(char, char)

romainbrenguier · 2019-09-27T07:06:38Z

jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notequals.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--


⛏️ missing new line

romainbrenguier · 2019-09-27T07:07:58Z

src/util/simplify_expr.cpp

+    !lower_case_string_expression(second_value))
+    return simplify_exprt::unchanged(expr);
+
+  bool is_equal = first_value == second_value;


const or can be inlined in the next expression

romainbrenguier · 2019-09-27T07:10:33Z

src/goto-symex/goto_symex.cpp

+
+  auto is_not_whitespace = [](const exprt &expr) {
+    auto &constant_value = to_constant_expr(expr);
+    char character = numeric_cast_v<int>(constant_value);


numeric_cast_v if possible otherwise use narrow, but actually the next operation doesn't require a char and could directly be done on an mp_integer

romainbrenguier · 2019-09-27T07:10:46Z

src/goto-symex/goto_symex.cpp

+  auto &operands = string_data.operands();
+
+  auto is_not_whitespace = [](const exprt &expr) {
+    auto &constant_value = to_constant_expr(expr);


⛏️ inline below

romainbrenguier · 2019-09-27T07:11:36Z

src/goto-symex/goto_symex.cpp

+  if(!s_data_opt)
+    return false;
+
+  const array_exprt &string_data = s_data_opt->get();


⛏️ used only once, can be inlined below

romainbrenguier · 2019-09-27T07:13:22Z

src/goto-symex/goto_symex.cpp

+
+  // If we haven't found anything, just want to copy the whole array.
+  if(start_iter == operands.end())
+    start_iter = operands.begin();


🚫 this seems wrong, if there is no character which is not a whitespace, then the result should be empty

This actually is producing an empty string, but it's not obvious (end_iter must have traversed the whole string too, and so equals operands.begin()). Suggest instead do

exprt::operandst new_operands; if(start_iter != operands.end()) new_operands = exprt::operandst{start_iter, end_iter.base()};

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java

JohnDumbell · 2019-09-27T13:37:08Z

Added more tests, added in both character/string replace, did general clean-up pass. If you want any more tests please just list the specific ones.

codecov-io · 2019-10-02T10:30:11Z

Codecov Report

Merging #5129 into develop will decrease coverage by 0.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5129      +/-   ##
===========================================
- Coverage    67.03%   67.01%   -0.02%     
===========================================
  Files         1149     1147       -2     
  Lines        94030    94042      +12     
===========================================
- Hits         63033    63025       -8     
- Misses       30997    31017      +20

Flag	Coverage Δ
#cproversmt2	`42.59% <0%> (-0.12%)`	⬇️
#regression	`63.51% <100%> (-0.01%)`	⬇️
#unit	`31.89% <2.25%> (-0.07%)`	⬇️

Impacted Files	Coverage Δ
src/goto-symex/goto_symex.h	`92.3% <ø> (ø)`	⬆️
src/util/simplify_expr.cpp	`87.52% <100%> (+0.7%)`	⬆️
src/goto-symex/goto_symex.cpp	`99.71% <100%> (+0.07%)`	⬆️
src/goto-instrument/cover_instrument_other.cpp	`63.63% <0%> (-32.2%)`	⬇️
...rs/strings/string_constraint_generator_testing.cpp	`91.86% <0%> (-8.14%)`	⬇️
...bmc/src/java_bytecode/java_static_initializers.cpp	`99.11% <0%> (-0.89%)`	⬇️
src/solvers/strings/string_refinement.cpp	`87.84% <0%> (-0.69%)`	⬇️
...lvers/strings/string_constraint_generator_main.cpp	`83.33% <0%> (-0.58%)`	⬇️
src/goto-symex/symex_goto.cpp	`96.1% <0%> (-0.45%)`	⬇️
src/util/std_expr.h	`89% <0%> (-0.23%)`	⬇️
... and 26 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 633d67a...bdde675. Read the comment docs.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2fe2434).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130009103

smowton

Non-blocking suggestions

smowton · 2019-10-02T13:11:15Z

jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--


Might want to note why this one doesn't work, either here or in a comment in the java file

smowton · 2019-10-02T13:13:08Z

jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.java

+    }
+
+    public void stringReplace() {
+        String str = "abded";


Duplicate of replace

One takes 2 characters, other takes 2 strings.

smowton · 2019-10-02T13:13:48Z

jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.java

+        assert str.equals("ghcdgh");
+    }
+
+    public void stringMultiLargerReplace() {


Larger and Smaller names the wrong way around here

smowton · 2019-10-02T13:15:04Z

jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--


Again mention the missing support, either here or inline in the java file

smowton · 2019-10-02T13:19:09Z

jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc

+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$


Surprising! Pi should be affected by the real JDK method; is our models lib wrong here?

the builtin upper_case and lower_case are only correct for a (small) subset of unicode (I think ascii and latin-1 supplement) so this is incorrect but expected. It sould be marked as knownbug.

smowton · 2019-10-02T13:20:28Z

src/goto-symex/goto_symex.cpp

+  array_exprt characters_to_find(s_data_opt->get().type());
+  array_exprt characters_to_replace(s_data_opt->get().type());
+
+  // Two main ways to perform a replace: characters or strings.


Main ways, or ways? Is there a third unusual one?

smowton · 2019-10-02T13:20:46Z

src/goto-symex/goto_symex.cpp

+  }
+  else
+  {
+    auto &new_char_array = to_string_expr(new_data);


INVARIANT that the types are as you expect (String, String by the sounds of it)

smowton · 2019-10-02T13:24:33Z

src/goto-symex/goto_symex.cpp

+
+  // If we haven't found anything, just want to copy the whole array.
+  if(start_iter == operands.end())
+    start_iter = operands.begin();


This actually is producing an empty string, but it's not obvious (end_iter must have traversed the whole string too, and so equals operands.begin()). Suggest instead do

exprt::operandst new_operands; if(start_iter != operands.end()) new_operands = exprt::operandst{start_iter, end_iter.base()};

smowton · 2019-10-02T13:25:00Z

src/goto-symex/goto_symex.cpp

+  auto start_iter =
+    std::find_if(operands.begin(), operands.end(), is_not_whitespace);
+
+  // If our entire string is empty, our end_iter will be at begin(), so just


"If our entire string is empty" -> "If the entire string is whitespace"

smowton · 2019-10-02T13:26:15Z

src/util/simplify_expr.cpp

-      s2_data.operands().begin(),
-      s2_data.operands().end());
+    // Searching for empty string is a special case and is simply the
+    // first match you find. This needs to take into account starting position


"first match you find" -> "always found at the first searched position"?

JohnDumbell · 2019-10-02T14:39:00Z

@romainbrenguier Mind having another look and seeing if you're blocking issue is dealt with?

romainbrenguier · 2019-10-02T15:21:22Z

src/goto-symex/goto_symex.cpp

+  const function_application_exprt &f_l1)
+{
+  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &length_type = f_type.domain().at(0);


Add a precondition for f_type.domain().size() == 2

romainbrenguier · 2019-10-02T15:22:16Z

src/goto-symex/goto_symex.cpp

+    return character > ' ';
+  };
+
+  // Note the points where a trim would trim too.


romainbrenguier · 2019-10-02T15:28:45Z

jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc

+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$


the builtin upper_case and lower_case are only correct for a (small) subset of unicode (I think ascii and latin-1 supplement) so this is incorrect but expected. It sould be marked as knownbug.

romainbrenguier · 2019-10-02T15:29:53Z

src/goto-symex/goto_symex.cpp

+  bool to_upper)
+{
+  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &length_type = f_type.domain().at(0);


precondition

romainbrenguier · 2019-10-02T15:31:50Z

src/goto-symex/goto_symex.cpp

+  const function_application_exprt &f_l1)
+{
+  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &length_type = f_type.domain().at(0);


precondition

romainbrenguier · 2019-10-02T15:32:44Z

src/goto-symex/goto_symex.h

+  bool constant_propagate_replace(
+    statet &state,
+    symex_assignt &symex_assign,
+    const function_application_exprt &f_l1);


blocking comments addressed

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: b5d8053).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130056711

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: bdde675).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130408178

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: db1f844).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130783671

JohnDumbell requested a review from danpoe September 25, 2019 12:52

JohnDumbell requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 25, 2019 12:52

JohnDumbell self-assigned this Sep 25, 2019

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 2 times, most recently from 6cfc3c8 to 851e709 Compare September 25, 2019 13:01

smowton reviewed Sep 25, 2019

View reviewed changes

danpoe reviewed Sep 25, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 2 times, most recently from 55d333c to 00b4edf Compare September 25, 2019 16:53

smowton reviewed Sep 25, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 2 times, most recently from 4ce1e46 to 047a471 Compare September 26, 2019 14:02

JohnDumbell requested a review from romainbrenguier as a code owner September 26, 2019 14:02

romainbrenguier reviewed Sep 26, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 2 times, most recently from 4ac83a9 to ec2ad44 Compare September 26, 2019 17:08

romainbrenguier suggested changes Sep 27, 2019

View reviewed changes

romainbrenguier previously requested changes Sep 27, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 3 times, most recently from dcc9a76 to f232857 Compare September 27, 2019 13:33

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 2 times, most recently from fae4f4f to c76dd8b Compare September 30, 2019 17:42

JohnDumbell force-pushed the jd/feature/constant_string_functions branch 2 times, most recently from 2630a32 to 2fe2434 Compare October 2, 2019 09:29

allredj reviewed Oct 2, 2019

View reviewed changes

smowton approved these changes Oct 2, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/constant_string_functions branch from 2fe2434 to b5d8053 Compare October 2, 2019 13:47

romainbrenguier reviewed Oct 2, 2019

View reviewed changes

allredj reviewed Oct 2, 2019

View reviewed changes

JohnDumbell force-pushed the jd/feature/constant_string_functions branch from b5d8053 to bdde675 Compare October 4, 2019 11:10

allredj reviewed Oct 4, 2019

View reviewed changes

JohnDumbell added 6 commits October 7, 2019 17:21

Add String.trim()

f27e28c

Add String.contains(...)

030d6a3

Add String.toLowerCase() / String.toUpperCase()

b9b3fea

Add String.lastIndexOf(...)

9e1f258

Add String.replace(...)

79882c6

Add String.equalsIgnoreCase()

db1f844

JohnDumbell force-pushed the jd/feature/constant_string_functions branch from bdde675 to db1f844 Compare October 7, 2019 16:23

allredj reviewed Oct 7, 2019

View reviewed changes

JohnDumbell merged commit 357c1b1 into diffblue:develop Oct 8, 2019

JohnDumbell deleted the jd/feature/constant_string_functions branch October 8, 2019 14:44


		irep_idt target_overload = f_l1.source_location().get_function();

		// If it's a symbol we're using the replace(Character, Character) overload.

Constant propagate string-solver function results #5129

Constant propagate string-solver function results #5129

Uh oh!

Conversation

JohnDumbell commented Sep 25, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 25, 2019

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JohnDumbell commented Sep 25, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

JohnDumbell commented Sep 25, 2019 •

edited

Loading