Merge pull request #3982 from JohnDumbell/jd/enhancement/symex_constant_string_compare

Try to evaluate constant string comparisons in symex

Author: tautschnig

jbmc/regression/jbmc-strings/StartsWithConstantEvalution/RefineStrings.class

@@ -0,0 +1,12 @@
+package string_refinement;
+
+public class RefineStrings {
+    public void constantComparison() {
+        String helloWorld = "Hello world";
+        assert helloWorld.equals(helloWorld());
+    }
+
+    public String helloWorld() {
+        return "Hello world";
+    }
+}

jbmc/regression/jbmc-strings/StartsWithConstantEvalution/RefineStrings.java

@@ -0,0 +1,8 @@
+CORE
+RefineStrings.class
+--function string_refinement.RefineStrings.constantComparison --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+--
+.*cprover_string_startswith_func*.
+--
+All instances of cprover_string_startswith_func can be calculated as false or true, so there should be no instances of this call.

jbmc/regression/jbmc-strings/StartsWithConstantEvalution/constant_equals.desc

@@ -19,12 +19,15 @@ Author: Daniel Kroening, [email protected]
 #include "expr_util.h"
 #include "fixedbv.h"
 #include "invariant.h"
+#include "mathematical_expr.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "rational.h"
 #include "rational_tools.h"
 #include "simplify_utils.h"
 #include "std_expr.h"
+#include "string_expr.h"
+#include "symbol.h"
 #include "type_eq.h"
 
 // #define DEBUGX
@@ -158,6 +161,77 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
   return true;
 }
 
+bool simplify_exprt::simplify_function_application(exprt &expr)
+{
+  const function_application_exprt &function_app =
+    to_function_application_expr(expr);
+  irep_idt func_id =
+    function_app.function().find(ID_expression).get(ID_identifier);
+
+  // Starts-with is used for .equals.
+  if(func_id == ID_cprover_string_startswith_func)
+  {
+    // We want to get both arguments of any starts-with comparison, and
+    // trace them back to the actual string instance. All variables on the
+    // way must be constant for us to be sure this will work.
+    auto &first_argument = to_string_expr(function_app.arguments().at(0));
+    auto &second_argument = to_string_expr(function_app.arguments().at(1));
+
+    if(
+      first_argument.content().id() != ID_address_of ||
+      second_argument.content().id() != ID_address_of)
+    {
+      return true;
+    }
+
+    const address_of_exprt &first_address_of =
+      to_address_of_expr(first_argument.content());
+    const address_of_exprt &second_address_of =
+      to_address_of_expr(second_argument.content());
+
+    // Constants are got via address_of expressions, so this helps filter out
+    // things that are non-constant.
+    if(
+      first_address_of.object().id() != ID_index ||
+      first_address_of.object().id() != ID_index)
+    {
+      return true;
+    }
+
+    const index_exprt &first_index_expression =
+      to_index_expr(first_address_of.object());
+    const index_exprt &second_index_expression =
+      to_index_expr(second_address_of.object());
+
+    const exprt &first_string_array = first_index_expression.array();
+    const exprt &second_string_array = second_index_expression.array();
+
+    // Check if our symbols type is an array.
+    if(
+      first_string_array.type().id() != ID_array ||
+      second_string_array.type().id() != ID_array)
+    {
+      return true;
+    }
+
+    // If so, it'll be a string array that we can use.
+    const array_string_exprt &first_string = to_array_string_expr(
+      ns.lookup(first_string_array.get(ID_identifier)).value);
+
+    const array_string_exprt &second_string = to_array_string_expr(
+      ns.lookup(second_string_array.get(ID_identifier)).value);
+
+    // If the lengths are the same we can do the .equals substitute.
+    if(first_string.length() == second_string.length())
+    {
+      expr = from_integer(first_string == second_string ? 1 : 0, expr.type());
+      return false;
+    }
+  }
+
+  return true;
+}
+
 bool simplify_exprt::simplify_typecast(exprt &expr)
 {
   if(expr.operands().size()!=1)
@@ -2265,6 +2339,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_sign(expr) && result;
   else if(expr.id() == ID_popcount)
     result = simplify_popcount(to_popcount_expr(expr)) && result;
+  else if(expr.id() == ID_function_application)
+    result = simplify_function_application(expr) && result;
 
   #ifdef DEBUGX
   if(!result

src/util/simplify_expr.cpp

@@ -114,6 +114,10 @@ class simplify_exprt
   bool simplify_sign(exprt &expr);
   bool simplify_popcount(popcount_exprt &expr);
 
+  /// Attempt to simplify mathematical function applications if we have
+  /// enough information to do so. Currently focused on constant comparisons.
+  bool simplify_function_application(exprt &expr);
+
   // auxiliary
   bool simplify_if_implies(
     exprt &expr, const exprt &cond, bool truth, bool &new_truth);