move string solver into separate directory

jbmc/src/jbmc/jbmc_parse_options.h

@@ -28,7 +28,9 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
 
-#include <solvers/refinement/string_refinement.h>
+#include <goto-symex/path_storage.h>
+
+#include <solvers/strings/string_refinement.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 

jbmc/src/jbmc/module_dependencies.txt

@@ -11,4 +11,5 @@ langapi # should go away
 linking
 pointer-analysis
 solvers/refinement
+solvers/strings
 util

jbmc/unit/Makefile

@@ -54,9 +54,9 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_virtual_functions/virtual_functions.cpp \
        java_bytecode/load_method_by_regex.cpp \
        pointer-analysis/custom_value_set_analysis.cpp \
-       solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
-       solvers/refinement/string_refinement/dependency_graph.cpp \
-       solvers/refinement/string_refinement/string_symbol_resolution.cpp \
+       solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp \
+       solvers/strings/string_refinement/dependency_graph.cpp \
+       solvers/strings/string_refinement/string_symbol_resolution.cpp \
        util/expr_iterator.cpp \
        util/has_subtype.cpp \
        util/parameter_indices.cpp \

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp → jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -8,28 +8,36 @@ Author: Jesse Sigal, [email protected]
 
 #include <testing-utils/catch.hpp>
 
-#include <numeric>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
+#include <numeric>
 
-#include <langapi/mode.h>
 #include <langapi/language_util.h>
+#include <langapi/mode.h>
 
-#include <solvers/refinement/string_constraint_instantiation.h>
 #include <solvers/sat/satcheck.h>
+#include <solvers/strings/string_constraint_instantiation.h>
 
-#include <util/simplify_expr.h>
 #include <util/config.h>
+#include <util/simplify_expr.h>
 
 /// \class Types used throughout the test. Currently it is impossible to
 /// statically initialize this value, there is a PR to allow this
 /// diffblue/cbmc/pull/1213
 class tt
 {
 public:
-  tt() {}
-  typet char_type() const {return java_char_type();}
-  typet length_type() const {return java_int_type();}
+  tt()
+  {
+  }
+  typet char_type() const
+  {
+    return java_char_type();
+  }
+  typet length_type() const
+  {
+    return java_int_type();
+  }
   array_typet array_type() const
   {
     return array_typet(char_type(), infinity_exprt(length_type()));
@@ -60,7 +68,7 @@ constant_exprt from_integer(const mp_integer &i)
 /// \return corresponding `string_exprt`
 array_string_exprt make_string_exprt(const std::string &str)
 {
-  const constant_exprt length=from_integer(str.length(), t.length_type());
+  const constant_exprt length = from_integer(str.length(), t.length_type());
   array_exprt content({}, array_typet(t.char_type(), length));
 
   for(const char c : str)
@@ -92,7 +100,7 @@ std::set<exprt> full_index_set(const array_string_exprt &s)
 {
   const mp_integer n = numeric_cast_v<mp_integer>(s.length());
   std::set<exprt> ret;
-  for(mp_integer i=0; i<n; ++i)
+  for(mp_integer i = 0; i < n; ++i)
     ret.insert(from_integer(i));
   return ret;
 }
@@ -115,7 +123,7 @@ std::set<std::pair<X, Y>> product(const std::set<X> xs, const std::set<Y> ys)
 exprt combine_lemmas(const std::vector<exprt> &lemmas, const namespacet &ns)
 {
   // Conjunction of new lemmas
-  exprt conj=conjunction(lemmas);
+  exprt conj = conjunction(lemmas);
   // Simplify
   simplify(conj, ns);
 
@@ -137,7 +145,7 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
     get_language_from_mode(ID_java)->from_expr(lemma, lemma_string, ns);
     new_lemmas += lemma_string + "\n\n";
   }
-  return "Instantiated lemmas:\n"+new_lemmas;
+  return "Instantiated lemmas:\n" + new_lemmas;
 }
 
 /// Checks the satisfiability of the given expression.
@@ -148,16 +156,17 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
 {
   satcheck_no_simplifiert sat_check;
   bv_refinementt::infot info;
-  info.ns=&ns;
-  info.prop=&sat_check;
+  info.ns = &ns;
+  info.prop = &sat_check;
   info.output_xml = false;
   bv_refinementt solver(info);
   solver << expr;
   return solver();
 }
 
 // The [!mayfail] tag allows tests to fail while reporting the failure
-SCENARIO("instantiate_not_contains",
+SCENARIO(
+  "instantiate_not_contains",
   "[!mayfail][core][solvers][refinement][string_constraint_instantiation]")
 {
   // For printing expression
@@ -261,10 +270,10 @@ SCENARIO("instantiate_not_contains",
         decision_proceduret::resultt result = check_sat(conj, empty_ns);
 
         // Require SAT
-        if(result==decision_proceduret::resultt::D_ERROR)
+        if(result == decision_proceduret::resultt::D_ERROR)
           INFO("Got an error");
 
-        REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
+        REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
       }
     }
   }
@@ -311,10 +320,10 @@ SCENARIO("instantiate_not_contains",
         decision_proceduret::resultt result = check_sat(conj, empty_ns);
 
         // Require SAT
-        if(result==decision_proceduret::resultt::D_ERROR)
+        if(result == decision_proceduret::resultt::D_ERROR)
           INFO("Got an error");
 
-        REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
+        REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
       }
     }
   }
@@ -362,10 +371,10 @@ SCENARIO("instantiate_not_contains",
         decision_proceduret::resultt result = check_sat(conj, empty_ns);
 
         // Require UNSAT
-        if(result==decision_proceduret::resultt::D_ERROR)
+        if(result == decision_proceduret::resultt::D_ERROR)
           INFO("Got an error");
 
-        REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
+        REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
       }
     }
   }
@@ -414,10 +423,10 @@ SCENARIO("instantiate_not_contains",
         decision_proceduret::resultt result = check_sat(conj, empty_ns);
 
         // Require UNSAT
-        if(result==decision_proceduret::resultt::D_ERROR)
+        if(result == decision_proceduret::resultt::D_ERROR)
           INFO("Got an error");
 
-        REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
+        REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
       }
     }
   }
@@ -465,10 +474,10 @@ SCENARIO("instantiate_not_contains",
         decision_proceduret::resultt result = check_sat(conj, empty_ns);
 
         // Require UNSAT
-        if(result==decision_proceduret::resultt::D_ERROR)
+        if(result == decision_proceduret::resultt::D_ERROR)
           INFO("Got an error");
 
-        REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
+        REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
       }
     }
   }
@@ -517,10 +526,10 @@ SCENARIO("instantiate_not_contains",
         decision_proceduret::resultt result = check_sat(conj, empty_ns);
 
         // Require UNSAT
-        if(result==decision_proceduret::resultt::D_ERROR)
+        if(result == decision_proceduret::resultt::D_ERROR)
           INFO("Got an error");
 
-        REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
+        REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
       }
     }
   }

jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt → jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt

@@ -2,6 +2,7 @@ java_bytecode
 langapi # should go away
 solvers/refinement
 solvers/sat
+solvers/strings
 string_constraint_instantiation
 testing-utils
 util

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp → jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

@@ -9,11 +9,11 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/catch.hpp>
 
+#include <java_bytecode/java_types.h>
+#include <solvers/strings/string_refinement_util.h>
 #include <util/arith_tools.h>
-#include <util/std_types.h>
 #include <util/std_expr.h>
-#include <java_bytecode/java_types.h>
-#include <solvers/refinement/string_refinement_util.h>
+#include <util/std_types.h>
 
 #ifdef DEBUG
 #include <iostream>

jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt → jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt

@@ -2,5 +2,6 @@ java_bytecode
 langapi # should go away
 string_refinement
 solvers/refinement
+solvers/strings
 testing-utils
 util

jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp → jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp

@@ -9,17 +9,19 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/catch.hpp>
 
+#include <solvers/strings/string_refinement.h>
+
+#include <iostream>
+#include <java_bytecode/java_bytecode_language.h>
+#include <langapi/mode.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/std_expr.h>
-#include <solvers/refinement/string_refinement.h>
 #include <util/symbol_table.h>
-#include <langapi/mode.h>
-#include <java_bytecode/java_bytecode_language.h>
-#include <iostream>
 
-SCENARIO("string_identifiers_resolution_from_equations",
-"[core][solvers][refinement][string_refinement]")
+SCENARIO(
+  "string_identifiers_resolution_from_equations",
+  "[core][solvers][refinement][string_refinement]")
 {
   // For printing expression
   register_language(new_java_bytecode_language);
@@ -50,8 +52,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
     WHEN("There is no function call")
     {
       union_find_replacet symbol_resolve =
-        string_identifiers_resolution_from_equations(
-          equations, ns, stream);
+        string_identifiers_resolution_from_equations(equations, ns, stream);
 
       THEN("The symbol resolution structure is empty")
       {
@@ -69,8 +70,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
       symbol_exprt bool_sym("bool_b", bool_typet());
       equations.emplace_back(bool_sym, fun);
       union_find_replacet symbol_resolve =
-        string_identifiers_resolution_from_equations(
-          equations, ns, stream);
+        string_identifiers_resolution_from_equations(equations, ns, stream);
 
       THEN("Equations that depend on it should be added")
       {

src/cbmc/cbmc_parse_options.h

@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_trace.h>
 
-#include <solvers/refinement/string_refinement.h>
+#include <solvers/strings/string_refinement.h>
 
 #include "bmc.h"
 #include "xml_interface.h"

src/goto-checker/solver_factory.cpp

@@ -28,9 +28,9 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 #include <solvers/refinement/bv_refinement.h>
-#include <solvers/refinement/string_refinement.h>
 #include <solvers/sat/dimacs_cnf.h>
 #include <solvers/sat/satcheck.h>
+#include <solvers/strings/string_refinement.h>
 
 solver_factoryt::solver_factoryt(
   const optionst &_options,

src/solvers/Makefile

@@ -161,23 +161,23 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/bv_refinement_loop.cpp \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
-      refinement/string_builtin_function.cpp \
-      refinement/string_refinement.cpp \
-      refinement/string_refinement_util.cpp \
-      refinement/string_constraint.cpp \
-      refinement/string_constraint_generator_code_points.cpp \
-      refinement/string_constraint_generator_comparison.cpp \
-      refinement/string_constraint_generator_concat.cpp \
-      refinement/string_constraint_generator_constants.cpp \
-      refinement/string_constraint_generator_indexof.cpp \
-      refinement/string_constraint_generator_insert.cpp \
-      refinement/string_constraint_generator_float.cpp \
-      refinement/string_constraint_generator_format.cpp \
-      refinement/string_constraint_generator_main.cpp \
-      refinement/string_constraint_generator_testing.cpp \
-      refinement/string_constraint_generator_transformation.cpp \
-      refinement/string_constraint_generator_valueof.cpp \
-      refinement/string_constraint_instantiation.cpp \
+      strings/string_builtin_function.cpp \
+      strings/string_refinement.cpp \
+      strings/string_refinement_util.cpp \
+      strings/string_constraint.cpp \
+      strings/string_constraint_generator_code_points.cpp \
+      strings/string_constraint_generator_comparison.cpp \
+      strings/string_constraint_generator_concat.cpp \
+      strings/string_constraint_generator_constants.cpp \
+      strings/string_constraint_generator_indexof.cpp \
+      strings/string_constraint_generator_insert.cpp \
+      strings/string_constraint_generator_float.cpp \
+      strings/string_constraint_generator_format.cpp \
+      strings/string_constraint_generator_main.cpp \
+      strings/string_constraint_generator_testing.cpp \
+      strings/string_constraint_generator_transformation.cpp \
+      strings/string_constraint_generator_valueof.cpp \
+      strings/string_constraint_instantiation.cpp \
       sat/cnf.cpp \
       sat/cnf_clause_list.cpp \
       sat/dimacs_cnf.cpp \

src/solvers/refinement/refine_arithmetic.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/arith_tools.h>
 
-#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/floatbv/float_utils.h>
 
 // Parameters
@@ -167,10 +166,7 @@ void bv_refinementt::check_SAT(approximationt &a)
 
   if(type.id()==ID_floatbv)
   {
-    // these are all ternary
-    INVARIANT(
-      a.expr.operands().size()==3,
-      string_refinement_invariantt("all floatbv typed exprs are ternary"));
+    const auto &float_op = to_ieee_float_op_expr(a.expr);
 
     if(a.over_state==MAX_STATE)
       return;
@@ -182,7 +178,7 @@ void bv_refinementt::check_SAT(approximationt &a)
     o1.unpack(a.op1_value);
 
     // get actual rounding mode
-    exprt rounding_mode_expr = get(a.expr.op2());
+    exprt rounding_mode_expr = get(float_op.rounding_mode());
     const std::size_t rounding_mode_int =
       numeric_cast_v<std::size_t>(rounding_mode_expr);
     ieee_floatt::rounding_modet rounding_mode =
@@ -279,8 +275,7 @@ void bv_refinementt::check_SAT(approximationt &a)
   {
     // these are all binary
     INVARIANT(
-      a.expr.operands().size()==2,
-      string_refinement_invariantt("all (un)signedbv typed exprs are binary"));
+      a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary");
 
     // already full interpretation?
     if(a.over_state>0)