Add a switch for fixed strings on input

Author: Vojtech Forejt

jbmc/regression/jbmc-strings/string-input-value/Test.class

@@ -0,0 +1,12 @@
+public class Test {
+
+    static void checkStringInputValue(String s) {
+      if (s.length() == 2)
+        assert(false);
+      else if (s.length() == 3)
+        assert(false);
+      else if (s.length() == 4)
+        assert(false);
+      assert(false);
+    }
+}

jbmc/regression/jbmc-strings/string-input-value/Test.java

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--verbosity 10 --string-input-value fo --string-input-value barr --function Test.checkStringInputValue
+^EXIT=10$
+^SIGNAL=0$
+assertion.1.*FAILURE
+assertion.2.*SUCCESS
+assertion.3.*FAILURE
+assertion.4.*SUCCESS

jbmc/regression/jbmc-strings/string-input-value/test1.desc

@@ -131,6 +131,21 @@ static void java_static_lifetime_init(
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
   object_factory_parameters.function_id = initialize_symbol.name;
 
+  // If there are strings given using --string-input-value, we need to add
+  // them to the symbol table now, so that they appear in __CPROVER_initialize
+  // and we can refer to them later when we initialise input values.
+  for(const auto &val : object_factory_parameters.string_input_values)
+  {
+    exprt my_literal(ID_java_string_literal);
+    my_literal.set(ID_value, val);
+    // We ignore the return value of the following call, we just need to
+    // make sure the string is in the symbol table.
+    get_or_create_string_literal_symbol(
+      my_literal,
+      symbol_table,
+      string_refinement_enabled);
+  }
+
   // We need to zero out all static variables, or nondet-initialize if they're
   // external. Iterate over a copy of the symtab, as its iterators are
   // invalidated by object_factory:

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -11,13 +11,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_initializer.h>
 #include <util/fresh_symbol.h>
 #include <util/nondet_bool.h>
+#include <util/nondet.h>
 #include <util/pointer_offset_size.h>
 
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
+#include "java_string_literals.h"
 
 class java_object_factoryt
 {
@@ -1010,37 +1012,74 @@ void java_object_factoryt::gen_nondet_struct_init(
         ::implements_java_char_sequence(struct_type);
     bool has_data_length =
       struct_type.has_component("length") && struct_type.has_component("data");
+    // following is true if we were not given fixed string input values
+    // using --string-input-value
+    bool no_input_values =
+      object_factory_parameters.string_input_values.empty();
+
+    if(!is_char_sequence || !has_data_length || no_input_values)
+    { // Either not a string, or user did not specify --string-input-values
+
+      // Add an initial all-zero write. Most of the fields of this will be
+      // overwritten, but it helps to have a whole-structure write that analysis
+      // passes can easily recognise leaves no uninitialised state behind.
+
+      // This code mirrors the `remove_java_new` pass:
+      auto initial_object =
+        zero_initializer(struct_type, source_locationt(), ns);
+      CHECK_RETURN(initial_object.has_value());
+      irep_idt qualified_clsid = "java::" + id2string(class_identifier);
+      set_class_identifier(
+        to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));
+
+      if(is_char_sequence && has_data_length)
+      { // We're dealing with a string
+        skip_special_string_fields = true;
+        initialize_nondet_string_fields(
+          to_struct_expr(*initial_object),
+          assignments,
+          object_factory_parameters.min_nondet_string_length,
+          object_factory_parameters.max_nondet_string_length,
+          loc,
+          object_factory_parameters.function_id,
+          symbol_table,
+          object_factory_parameters.string_printable);
+      }
+      // in the else case we have
+      // '!is_char_sequence || !has_data_length'
+      // and so we are not dealing with a string
 
-    // Add an initial all-zero write. Most of the fields of this will be
-    // overwritten, but it helps to have a whole-structure write that analysis
-    // passes can easily recognise leaves no uninitialised state behind.
+      assignments.add(code_assignt(expr, *initial_object));
+    }
+    else
+    { // We're dealing with a string and we should set fixed input values.
+      skip_special_string_fields = true;
 
-    // This code mirrors the `remove_java_new` pass:
-    auto initial_object =
-      zero_initializer(struct_type, source_locationt(), ns);
-    CHECK_RETURN(initial_object.has_value());
-    irep_idt qualified_clsid = "java::" + id2string(class_identifier);
-    set_class_identifier(
-      to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));
+      // We create a switch statement where each case is an assignment
+      // of one of the fixed input strings to the input variable in question
 
-    if(is_char_sequence && has_data_length)
-    { // we're dealing with a string
-      skip_special_string_fields = true;
-      initialize_nondet_string_fields(
-        to_struct_expr(*initial_object),
-        assignments,
-        object_factory_parameters.min_nondet_string_length,
-        object_factory_parameters.max_nondet_string_length,
-        loc,
-        object_factory_parameters.function_id,
-        symbol_table,
-        object_factory_parameters.string_printable);
-    }
-    // in the else case we have
-    // '!is_char_sequence || !has_data_length'
-    // and so we are not dealing with a string
+      // the following invariant is due to no_input_values==false
+      auto size = object_factory_parameters.string_input_values.size();
+      INVARIANT(size > 0, "No string-input-value parameter given");
 
-    assignments.add(code_assignt(expr, *initial_object));
+      alternate_casest cases;
+      for(const auto &val : object_factory_parameters.string_input_values)
+      {
+        exprt name_literal(ID_java_string_literal);
+        name_literal.set(ID_value, val);
+        symbol_exprt s =
+          get_or_create_string_literal_symbol(name_literal, symbol_table, true);
+        cases.push_back(code_assignt(expr, s));
+      }
+
+       assignments.add(generate_nondet_switch(
+         id2string(object_factory_parameters.function_id),
+         cases,
+         java_int_type(),
+         ID_java,
+         loc,
+         symbol_table));
+    }
   }
 
   for(const auto &component : components)

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -252,11 +252,22 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("string-printable"))
     options.set_option("string-printable", true);
 
+  if(cmdline.isset("string-input-value"))
+    options.set_option(
+      "string-input-value",
+      cmdline.get_values("string-input-value"));
+
   if(cmdline.isset("no-refine-strings") && cmdline.isset("string-printable"))
   {
     warning() << "--string-printable ignored due to --no-refine-strings" << eom;
   }
 
+  if(cmdline.isset("no-refine-strings") && cmdline.isset("string-input-value"))
+  {
+    warning() << "--string-input-value ignored due to --no-refine-strings"
+              << eom;
+  }
+
   if(
     cmdline.isset("no-refine-strings") &&
     cmdline.isset("max-nondet-string-length"))

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -33,13 +33,15 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #define OPT_STRING_REFINEMENT \
   "(no-refine-strings)" \
   "(string-printable)" \
+  "(string-input-value):" \
   "(string-non-empty)" \
   "(max-nondet-string-length):"
 
 #define HELP_STRING_REFINEMENT \
   " --no-refine-strings          turn off string refinement\n" \
   " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
   " --string-non-empty           restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
+  " --string-printable st        restrict non-null strings to a fixed value(s)\n" /* NOLINT(*) */ \
   " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */
 
 // The integration of the string solver into CBMC is incomplete. Therefore,

src/solvers/refinement/string_refinement.h

@@ -37,6 +37,10 @@ void object_factory_parameterst::set(const optionst &options)
   {
     string_printable = options.get_bool_option("string-printable");
   }
+  if(options.is_set("string-input-value"))
+  {
+    string_input_values = options.get_list_option("string-input-value");
+  }
   if(options.is_set("min-nondet-string-length"))
   {
     min_nondet_string_length =

src/util/object_factory_parameters.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cstdint>
 #include <limits>
+#include <list>
 
 #include <util/irep.h>
 
@@ -69,6 +70,9 @@ struct object_factory_parameterst
   /// Force string content to be ASCII printable characters when set to true.
   bool string_printable = false;
 
+  /// Force one of finitely many explicitly given input strings
+  std::list<std::string> string_input_values;
+
   /// Function id, used as a prefix for identifiers of temporaries
   irep_idt function_id;