adding a string solver and string refinement code

src/solvers/refinement/bv_refinement.h

@@ -83,8 +83,8 @@ class bv_refinementt:public bv_pointerst
   void get_values(approximationt &approximation);
   bool is_in_conflict(approximationt &approximation);
 
-  void check_SAT();
-  void check_UNSAT();
+  virtual void check_SAT();
+  virtual void check_UNSAT();
   bool progress;
 
   // we refine the theory of arrays

src/solvers/refinement/refined_string_type.cpp

@@ -0,0 +1,76 @@
+/** -*- C++ -*- *****************************************************\
+
+Module: Type of string expressions for PASS algorithm
+        (see the PASS paper at HVC'13)
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include <solvers/refinement/refined_string_type.h>
+#include <ansi-c/string_constant.h>
+
+refined_string_typet::refined_string_typet(unsignedbv_typet char_type) : struct_typet() {
+  components().resize(2);
+  components()[0].set_name("length");
+  components()[0].set_pretty_name("length");
+  components()[0].type()=refined_string_typet::index_type();
+
+  array_typet char_array(char_type,infinity_exprt(refined_string_typet::index_type()));
+  components()[1].set_name("content");
+  components()[1].set_pretty_name("content");
+  components()[1].type()=char_array;
+}
+
+bool refined_string_typet::is_c_string_type(const typet &type)
+{
+  if (type.id() == ID_struct) {
+    irep_idt tag = to_struct_type(type).get_tag();
+    return (tag == irep_idt("__CPROVER_string"));
+  } else return false;
+}
+
+bool refined_string_typet::is_java_string_type(const typet &type)
+{
+  if(type.id() == ID_pointer) {
+    pointer_typet pt = to_pointer_type(type);
+    typet subtype = pt.subtype();
+    return is_java_deref_string_type(subtype);
+  } else return false;
+}
+
+bool refined_string_typet::is_java_deref_string_type(const typet &type)
+{
+  if(type.id() == ID_struct) {
+    irep_idt tag = to_struct_type(type).get_tag();
+    return (tag == irep_idt("java.lang.String"));
+  } 
+  else return false;
+}
+
+bool refined_string_typet::is_java_string_builder_type(const typet &type)
+{
+  if(type.id() == ID_pointer) {
+    pointer_typet pt = to_pointer_type(type);
+    typet subtype = pt.subtype();
+    if(subtype.id() == ID_struct) {
+      irep_idt tag = to_struct_type(subtype).get_tag();
+      return (tag == irep_idt("java.lang.StringBuilder"));
+    } 
+    else return false;
+  } else return false;
+}
+
+bool refined_string_typet::is_java_char_sequence_type(const typet &type)
+{
+  if(type.id() == ID_pointer) {
+    pointer_typet pt = to_pointer_type(type);
+    typet subtype = pt.subtype();
+    if(subtype.id() == ID_struct) {
+      irep_idt tag = to_struct_type(subtype).get_tag();
+      return (tag == irep_idt("java.lang.CharSequence"));
+    } 
+    else return false;
+  } else return false;
+}
+

src/solvers/refinement/refined_string_type.h

@@ -0,0 +1,73 @@
+/** -*- C++ -*- *****************************************************\
+
+Module: Type of string expressions for PASS algorithm
+        (see the PASS paper at HVC'13)
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVER_REFINED_STRING_TYPE_H
+#define CPROVER_SOLVER_REFINED_STRING_TYPE_H
+
+#include <util/std_types.h>
+#include <util/std_expr.h>
+
+#define STRING_SOLVER_INDEX_WIDTH 32
+#define STRING_SOLVER_CHAR_WIDTH 8
+#define JAVA_STRING_SOLVER_CHAR_WIDTH 16
+
+// Internal type used for string refinement
+class refined_string_typet : public struct_typet {
+public:
+  refined_string_typet(unsignedbv_typet char_type);
+
+  // Type for the content (list of characters) of a string
+  inline array_typet get_content_type() 
+  { return to_array_type((to_struct_type(*this)).components()[1].type());}
+
+  // Types used in this refinement
+  static inline unsignedbv_typet char_type() { return unsignedbv_typet(STRING_SOLVER_CHAR_WIDTH);}
+
+  static inline unsignedbv_typet java_char_type() { return unsignedbv_typet(JAVA_STRING_SOLVER_CHAR_WIDTH);}
+
+  static inline signedbv_typet index_type() { return signedbv_typet(STRING_SOLVER_INDEX_WIDTH);}
+
+  static inline exprt index_zero() { return constant_exprt(integer2binary(0, STRING_SOLVER_INDEX_WIDTH), index_type());}
+
+  // For C the unrefined string type is __CPROVER_string, for java it is a 
+  // pointer to a strict with tag java.lang.String
+
+  static bool is_c_string_type(const typet & type);
+
+  static bool is_java_string_type(const typet & type);
+
+  static bool is_java_deref_string_type(const typet & type);
+
+  static bool is_java_string_builder_type(const typet & type);
+
+  static bool is_java_char_sequence_type(const typet & type);
+
+  static inline unsignedbv_typet get_char_type(const exprt & expr) {
+    if(is_c_string_type(expr.type())) return char_type();
+    else return java_char_type();
+  }
+
+  static inline bool is_unrefined_string_type(const typet & type)
+  {  return (is_c_string_type(type) 
+          || is_java_string_type(type) 
+          || is_java_string_builder_type(type)
+          || is_java_char_sequence_type(type)
+	     ); }
+
+  static inline bool is_unrefined_string(const exprt & expr)
+  {  return (is_unrefined_string_type(expr.type())); }
+
+  static inline constant_exprt index_of_int(int i) 
+  {  return constant_exprt(integer2binary(i, STRING_SOLVER_INDEX_WIDTH), 
+			   index_type()); }
+
+};
+
+
+#endif

src/solvers/refinement/string_constraint.cpp

@@ -0,0 +1,67 @@
+/** -*- C++ -*- *****************************************************\
+
+Module: String constraints
+        (see the PASS paper at HVC'13)
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include <solvers/refinement/string_constraint.h>
+
+
+exprt string_constraintt::premise() const {
+  if(form == SIMPLE || form == UNIV_QUANT) {
+    if(id() == ID_implies)
+      return op0();
+    else 
+      return true_exprt();
+  }
+  else {
+    return(*this);
+  }
+}
+
+exprt string_constraintt::body() const {
+  if(form == SIMPLE || form == UNIV_QUANT) {
+    if(id() == ID_implies)
+      return op1();
+    else
+      return(*this);
+  } else throw "string_constraintt::body() should not be applied to NOT_CONTAINS expression";
+}
+
+string_constraintt string_constraintt::forall(const symbol_exprt & univ, const exprt & bound_inf, const exprt & bound_sup)
+{
+  string_constraintt sc(*this);
+  sc.form = UNIV_QUANT;
+  sc.quantified_variable = univ;
+  sc.bounds.push_back(bound_inf);
+  sc.bounds.push_back(bound_sup);
+  return sc;
+}
+
+string_constraintt string_constraintt::not_contains(exprt univ_bound_inf, exprt univ_bound_sup, 
+				 exprt premise, exprt exists_bound_inf, 
+				 exprt exists_bound_sup, exprt s0, exprt s1)
+{ 
+  string_constraintt sc(premise);
+  sc.form = NOT_CONTAINS;
+  sc.bounds.push_back(univ_bound_inf);
+  sc.bounds.push_back(univ_bound_inf);
+  sc.bounds.push_back(univ_bound_sup);
+  sc.bounds.push_back(exists_bound_inf);
+  sc.bounds.push_back(exists_bound_sup);
+  sc.compared_strings.push_back(s0);
+  sc.compared_strings.push_back(s1);
+  return sc;
+}
+
+string_constraintt string_constraintt::exists(const symbol_exprt & exist, const exprt & bound_inf, const exprt & bound_sup)
+{
+  assert(is_simple() || is_string_constant());
+  return string_constraintt
+    (and_exprt(*this, 
+	       and_exprt(binary_relation_exprt(exist, ID_ge, bound_inf),
+			 binary_relation_exprt(exist, ID_lt, bound_sup))));
+}

src/solvers/refinement/string_constraint.h

@@ -0,0 +1,105 @@
+/** -*- C++ -*- *****************************************************\
+
+Module: String constraints
+        (see the PASS paper at HVC'13)
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVER_STRING_CONSTRAINT_H
+#define CPROVER_SOLVER_STRING_CONSTRAINT_H
+
+#include <langapi/language_ui.h>
+#include <solvers/refinement/bv_refinement.h>
+
+class string_constraintt : public exprt 
+{
+private:
+  // String axioms can have 4 different forms:
+  // either a simple expression p, 
+  // or a string constant: forall x in [0,|s|[. s(x) = c(x)
+  // or universally quantified expression: forall x in [lb,ub[. p(x)
+  // or a expression for non containment:
+  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
+  enum {SIMPLE, STRING_CONSTANT, UNIV_QUANT, NOT_CONTAINS} form;
+
+  // Universally quantified symbol
+  symbol_exprt quantified_variable;
+  // Bounds on the quantified variables (alternate between inf and sup)
+  std::vector<exprt> bounds;
+  // Only for NOT_CONTAINS constraints (represent s1 and s2)
+  std::vector<exprt> compared_strings;
+
+public:
+
+// used to store information about witnesses for not_contains constraints
+  symbol_exprt witness;
+
+
+  // True axiom
+  string_constraintt() : exprt(true_exprt()) { form = SIMPLE; }
+
+  // Axiom with no quantification, and no premise
+  string_constraintt(exprt bod, bool is_string_constant=false) : exprt(bod) { form = is_string_constant?SIMPLE:STRING_CONSTANT; }
+
+  // Axiom with no quantification: prem => bod
+  string_constraintt(exprt prem, exprt bod)  : exprt(implies_exprt(prem,bod))
+  { form = SIMPLE; }
+
+  // Add an universal quantifier
+  string_constraintt forall(const symbol_exprt & univ, const exprt & bound_inf, const exprt & bound_sup);
+
+  // Bound a variable that is existentially quantified
+  string_constraintt exists(const symbol_exprt & exist, const exprt & bound_inf, const exprt & bound_sup);
+
+  static string_constraintt not_contains
+  (exprt univ_lower_bound, exprt univ_bound_sup, exprt premise, 
+   exprt exists_bound_inf, exprt exists_bound_sup, exprt s0, exprt s1);
+
+  bool is_simple() const { return (form == SIMPLE); };
+  bool is_string_constant() const { return (form == STRING_CONSTANT); };
+  bool is_univ_quant() const { return (form == UNIV_QUANT); };
+  bool is_not_contains() const { return (form == NOT_CONTAINS); };
+
+  exprt premise() const;
+
+  exprt body() const;
+
+  inline exprt s0() const { assert(is_not_contains()); return compared_strings[0];}
+  inline exprt s1() const { assert(is_not_contains()); return compared_strings[1];}
+
+
+  inline symbol_exprt get_univ_var() const { assert(form==UNIV_QUANT); return quantified_variable;}
+  inline exprt univ_bound_inf() const { return bounds[0]; }
+  inline exprt univ_bound_sup() const { return bounds[1]; }
+  inline exprt univ_within_bounds() const 
+  { return and_exprt(binary_relation_exprt(bounds[0],ID_le,get_univ_var()),
+		     binary_relation_exprt(bounds[1],ID_gt,get_univ_var())); }
+  inline exprt exists_bound_inf() const { return bounds[2]; }
+  inline exprt exists_bound_sup() const { return bounds[3]; }
+
+  inline exprt witness_of(const exprt & univ_val) const { return index_exprt(witness, univ_val); }
+
+
+ // Warning: this assumes a simple form
+ inline string_constraintt operator&&(const exprt & a) {
+   assert(form == SIMPLE);
+   return string_constraintt(and_exprt(*this, a));
+ }
+
+ inline string_constraintt operator||(const exprt & a) {
+   assert(form == SIMPLE);
+   return string_constraintt(or_exprt(*this, a));
+ }
+
+ inline string_constraintt operator!() {
+   assert(form == SIMPLE);
+   return string_constraintt(not_exprt(*this));
+ }
+
+
+};
+
+
+#endif