Extra preconditions in string solver

Author: Lukasz A.J. Wrona

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -127,6 +127,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
 {
   const typet &return_type = f.type();
   PRECONDITION(return_type.id()==ID_signedbv);
+  PRECONDITION(f.arguments().size() == 2);
   const string_exprt str = get_string_expr(f.arguments()[0]);
   const exprt &pos = f.arguments()[1];
 
@@ -186,6 +187,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
 exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const function_application_exprt &f)
 {
+  PRECONDITION(f.arguments().size() == 3);
   const string_exprt str = get_string_expr(f.arguments()[0]);
   const exprt &begin = f.arguments()[1];
   const exprt &end = f.arguments()[2];
@@ -208,6 +210,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count(
 exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const function_application_exprt &f)
 {
+  PRECONDITION(f.arguments().size() == 3);
   const string_exprt str = get_string_expr(f.arguments()[0]);
   const exprt &index = f.arguments()[1];
   const exprt &offset = f.arguments()[2];

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -23,6 +23,7 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   const function_application_exprt &f)
 {
   PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.arguments().size() == 2);
 
   string_exprt s1 = get_string_expr(f.arguments()[0]);
   string_exprt s2 = get_string_expr(f.arguments()[1]);
@@ -100,6 +101,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   const function_application_exprt &f)
 {
   PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.arguments().size() == 2);
   const symbol_exprt eq = fresh_boolean("equal_ignore_case");
   const string_exprt s1 = get_string_expr(f.arguments()[0]);
   const string_exprt s2 = get_string_expr(f.arguments()[1]);
@@ -151,6 +153,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
 exprt string_constraint_generatort::add_axioms_for_hash_code(
   const function_application_exprt &f)
 {
+  PRECONDITION(f.arguments().size() == 1);
   const string_exprt str = get_string_expr(f.arguments()[0]);
   const typet &return_type = f.type();
   const typet &index_type = str.length().type();
@@ -186,7 +189,9 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
 exprt string_constraint_generatort::add_axioms_for_compare_to(
   const function_application_exprt &f)
 {
+  PRECONDITION(f.arguments().size() == 2);
   const typet &return_type=f.type();
+  PRECONDITION(return_type.id() == ID_signedbv);
   const string_exprt &s1 = get_string_expr(f.arguments()[0]);
   const string_exprt &s2 = get_string_expr(f.arguments()[1]);
   const symbol_exprt res = fresh_symbol("compare_to", return_type);

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -231,6 +231,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
+  PRECONDITION(args.size() == 2 || args.size() == 3);
   const string_exprt str = get_string_expr(args[0]);
   const exprt &c=args[1];
   const typet &index_type = str.length().type();
@@ -325,6 +326,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
+  PRECONDITION(args.size() == 2 || args.size() == 3);
   const string_exprt str = get_string_expr(args[0]);
   const exprt c = args[1];
   const typet &index_type = str.length().type();

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -74,6 +74,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
 {
   const function_application_exprt::argumentst &args=f.arguments();
   PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(args.size() == 2 || args.size() == 3);
   const string_exprt s0 = get_string_expr(args[swap_arguments ? 1 : 0]);
   const string_exprt s1 = get_string_expr(args[swap_arguments ? 0 : 1]);
   const exprt offset =
@@ -89,7 +90,7 @@ exprt string_constraint_generatort::add_axioms_for_is_empty(
   const function_application_exprt &f)
 {
   PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
-
+  PRECONDITION(f.arguments().size() == 1);
   // We add axioms:
   // a1 : is_empty => |s0| = 0
   // a2 : s0 => is_empty

src/util/string_expr.h

@@ -62,12 +62,14 @@ class string_exprt: public struct_exprt
   binary_relation_exprt axiom_for_length_ge(
     const exprt &rhs) const
   {
+    PRECONDITION(rhs.type() == length().type());
     return binary_relation_exprt(length(), ID_ge, rhs);
   }
 
   binary_relation_exprt axiom_for_length_gt(
     const exprt &rhs) const
   {
+    PRECONDITION(rhs.type() == length().type());
     return binary_relation_exprt(rhs, ID_lt, length());
   }
 
@@ -91,6 +93,7 @@ class string_exprt: public struct_exprt
   binary_relation_exprt axiom_for_length_le(
     const exprt &rhs) const
   {
+    PRECONDITION(rhs.type() == length().type());
     return binary_relation_exprt(length(), ID_le, rhs);
   }
 
@@ -108,6 +111,7 @@ class string_exprt: public struct_exprt
   binary_relation_exprt axiom_for_length_lt(
     const exprt &rhs) const
   {
+    PRECONDITION(rhs.type() == length().type());
     return binary_relation_exprt(length(), ID_lt, rhs);
   }
 
@@ -119,6 +123,7 @@ class string_exprt: public struct_exprt
 
   equal_exprt axiom_for_has_length(const exprt &rhs) const
   {
+    PRECONDITION(rhs.type() == length().type());
     return equal_exprt(length(), rhs);
   }