Merge pull request diffblue#1691 from romainbrenguier/bugfix/getClass#TG-1245

Improve cprover_string_literal argument handling TG-1245

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -164,7 +164,11 @@ class string_constraint_generatort final
     const exprt &end_index);
   exprt add_axioms_for_concat(const function_application_exprt &f);
   exprt add_axioms_for_concat_code_point(const function_application_exprt &f);
-  exprt add_axioms_for_constant(const array_string_exprt &res, irep_idt sval);
+  exprt add_axioms_for_constant(
+    const array_string_exprt &res,
+    irep_idt sval,
+    const exprt &guard = true_exprt());
+
   exprt add_axioms_for_delete(
     const array_string_exprt &res,
     const array_string_exprt &str,
@@ -195,6 +199,11 @@ class string_constraint_generatort final
   exprt add_axioms_for_insert_char(const function_application_exprt &f);
   exprt add_axioms_for_insert_float(const function_application_exprt &f);
   exprt add_axioms_for_insert_double(const function_application_exprt &f);
+
+  exprt add_axioms_for_cprover_string(
+    const array_string_exprt &res,
+    const exprt &arg,
+    const exprt &guard);
   exprt add_axioms_from_literal(const function_application_exprt &f);
   exprt add_axioms_from_int(const function_application_exprt &f);
   exprt add_axioms_from_int(

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -19,10 +19,12 @@ Author: Romain Brenguier, [email protected]
 /// equal.
 /// \param res: array of characters for the result
 /// \param sval: a string constant
+/// \param guard: condition under which the axiom should apply, true by default
 /// \return integer expression equal to zero
 exprt string_constraint_generatort::add_axioms_for_constant(
   const array_string_exprt &res,
-  irep_idt sval)
+  irep_idt sval,
+  const exprt &guard)
 {
   const typet &index_type = res.length().type();
   const typet &char_type = res.content().type().subtype();
@@ -43,12 +45,12 @@ exprt string_constraint_generatort::add_axioms_for_constant(
     const exprt idx = from_integer(i, index_type);
     const exprt c = from_integer(str[i], char_type);
     const equal_exprt lemma(res[idx], c);
-    axioms.push_back(lemma);
+    axioms.push_back(implies_exprt(guard, lemma));
   }
 
   const exprt s_length = from_integer(str.size(), index_type);
 
-  axioms.push_back(res.axiom_for_has_length(s_length));
+  axioms.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
   return from_integer(0, get_return_code_type());
 }
 
@@ -65,6 +67,39 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
   return from_integer(0, get_return_code_type());
 }
 
+/// Convert an expression of type string_typet to a string_exprt
+/// \param res: string expression for the result
+/// \param arg: expression of type string typet
+/// \param guard: condition under which `res` should be equal to arg
+/// \return 0 if constraints were added, 1 if expression could not be handled
+///         and no constraint was added. Expression we can handle are of the
+///         form \f$ e := "<string constant>" | (expr)? e : e \f$
+exprt string_constraint_generatort::add_axioms_for_cprover_string(
+  const array_string_exprt &res,
+  const exprt &arg,
+  const exprt &guard)
+{
+  if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
+  {
+    const and_exprt guard_true(guard, if_expr->cond());
+    const exprt return_code_true =
+      add_axioms_for_cprover_string(res, if_expr->true_case(), guard_true);
+
+    const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
+    const exprt return_code_false =
+      add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false);
+
+    return if_exprt(
+      equal_exprt(return_code_true, from_integer(0, get_return_code_type())),
+      return_code_false,
+      return_code_true);
+  }
+  else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
+    return add_axioms_for_constant(res, constant_expr->get_value(), guard);
+  else
+    return from_integer(1, get_return_code_type());
+}
+
 /// String corresponding to an internal cprover string
 ///
 /// Add axioms ensuring that the returned string expression is equal to the
@@ -79,7 +114,5 @@ exprt string_constraint_generatort::add_axioms_from_literal(
   const function_application_exprt::argumentst &args=f.arguments();
   PRECONDITION(args.size() == 3); // Bad args to string literal?
   const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
-  const exprt &arg = args[2];
-  irep_idt sval=to_constant_expr(arg).get_value();
-  return add_axioms_for_constant(res, sval);
+  return add_axioms_for_cprover_string(res, args[2], true_exprt());
 }