Adding more comments in refined_string_type and string_constraint

Also some comments in string_constraint_generator.cpp
and comments on the string_refinement module

Author: romainbrenguier

src/solvers/refinement/refined_string_type.cpp

@@ -1,7 +1,10 @@
 /** -*- C++ -*- *****************************************************\
 
-Module: Type of string expressions for PASS algorithm
-        (see the PASS paper at HVC'13)
+Module: Type for string expressions used by the string solver.
+        These string expressions contains a field `length`, of type
+	`index_type`, a field `content` of type `content_type`.
+	This module also defines function to recognise the C and java
+	string types.
 
 Author: Romain Brenguier, [email protected]
 
@@ -10,6 +13,13 @@ Author: Romain Brenguier, [email protected]
 #include <solvers/refinement/refined_string_type.h>
 #include <ansi-c/string_constant.h>
 
+/*******************************************************************\
+
+Constructor: refined_string_typet::refined_string_typet
+
+     Inputs: type of characters
+
+\*******************************************************************/
 refined_string_typet::refined_string_typet(unsignedbv_typet char_type)
   :struct_typet()
 {
@@ -25,6 +35,15 @@ refined_string_typet::refined_string_typet(unsignedbv_typet char_type)
   components()[1].type()=char_array;
 }
 
+/*******************************************************************\
+
+Function: refined_string_typet::is_c_string_type
+
+  Inputs: a type
+
+ Outputs: Boolean telling whether the type is that of C strings
+
+\*******************************************************************/
 bool refined_string_typet::is_c_string_type(const typet &type)
 {
   if(type.id()==ID_struct)
@@ -35,18 +54,36 @@ bool refined_string_typet::is_c_string_type(const typet &type)
   return false;
 }
 
-bool refined_string_typet::is_java_string_type(const typet &type)
+/*******************************************************************\
+
+Function: refined_string_typet::is_java_string_pointer_type
+
+  Inputs: a type
+
+ Outputs: Boolean telling whether the type is that of java string pointers
+
+\*******************************************************************/
+bool refined_string_typet::is_java_string_pointer_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);
+    return is_java_string_type(subtype);
   }
   return false;
 }
 
-bool refined_string_typet::is_java_deref_string_type(const typet &type)
+/*******************************************************************\
+
+Function: refined_string_typet::is_java_string_type
+
+  Inputs: a type
+
+ Outputs: Boolean telling whether the type is that of java string
+
+\*******************************************************************/
+bool refined_string_typet::is_java_string_type(const typet &type)
 {
   if(type.id()==ID_symbol)
   {
@@ -61,6 +98,15 @@ bool refined_string_typet::is_java_deref_string_type(const typet &type)
   return false;
 }
 
+/*******************************************************************\
+
+Function: refined_string_typet::is_java_string_builder_type
+
+  Inputs: a type
+
+ Outputs: Boolean telling whether the type is that of java string builder
+
+\*******************************************************************/
 bool refined_string_typet::is_java_string_builder_type(const typet &type)
 {
   if(type.id()==ID_pointer)
@@ -76,6 +122,15 @@ bool refined_string_typet::is_java_string_builder_type(const typet &type)
   return false;
 }
 
+/*******************************************************************\
+
+Function: refined_string_typet::is_java_char_sequence_type
+
+  Inputs: a type
+
+ Outputs: Boolean telling whether the type is that of java char sequence
+
+\*******************************************************************/
 bool refined_string_typet::is_java_char_sequence_type(const typet &type)
 {
   if(type.id()==ID_pointer)

src/solvers/refinement/refined_string_type.h

@@ -1,7 +1,10 @@
 /** -*- C++ -*- *****************************************************\
 
-Module: Type of string expressions for PASS algorithm
-        (see the PASS paper at HVC'13)
+Module: Type for string expressions used by the string solver.
+        These string expressions contains a field `length`, of type
+	`index_type`, a field `content` of type `content_type`.
+	This module also defines function to recognise the C and java
+	string types.
 
 Author: Romain Brenguier, [email protected]
 
@@ -49,9 +52,9 @@ class refined_string_typet: public struct_typet
 
   static bool is_c_string_type(const typet & type);
 
-  static bool is_java_string_type(const typet & type);
+  static bool is_java_string_pointer_type(const typet & type);
 
-  static bool is_java_deref_string_type(const typet & type);
+  static bool is_java_string_type(const typet & type);
 
   static bool is_java_string_builder_type(const typet & type);
 
@@ -68,7 +71,7 @@ class refined_string_typet: public struct_typet
   static inline bool is_unrefined_string_type(const typet & type)
   {
     return (is_c_string_type(type)
-            || is_java_string_type(type)
+            || is_java_string_pointer_type(type)
             || is_java_string_builder_type(type)
             || is_java_char_sequence_type(type));
   }

src/solvers/refinement/string_constraint.cpp

@@ -1,11 +1,15 @@
 /** -*- C++ -*- *****************************************************\
 
-Module: String constraints
-        (see the PASS paper at HVC'13)
+Module: String constraints.
+        These are formulas talking about strings. We implemented two
+        forms of constraints: `string_constraintt` implements formulas
+        of the form $\forall univ_var \in [lb,ub[. premise => body$,
+	and not_contains_constraintt implements those of the form:
+        $\forall x in [lb,ub[. p(x) => \exists y in [lb,ub[.
+	s1[x+y] != s2[y]$.
 
 Author: Romain Brenguier, [email protected]
 
 \*******************************************************************/
 
 #include <solvers/refinement/string_constraint.h>
-

src/solvers/refinement/string_constraint.h

@@ -1,7 +1,12 @@
 /** -*- C++ -*- *****************************************************\
 
-Module: String constraints
-        (see the PASS paper at HVC'13
+Module: String constraints.
+        These are formulas talking about strings. We implemented two
+        forms of constraints: `string_constraintt` implements formulas
+        of the form $\forall univ_var \in [lb,ub[. premise => body$,
+	and not_contains_constraintt implements those of the form:
+        $\forall x in [lb,ub[. p(x) => \exists y in [lb,ub[.
+	s1[x+y] != s2[y]$.
 
 Author: Romain Brenguier, [email protected]
 
@@ -18,7 +23,7 @@ class string_constraintt: public exprt
 {
 public:
   // String constraints are of the form
-  // forall univ_var in [0,bound[. premise => body
+  // forall univ_var in [lower_bound,upper_bound[. premise => body
   // or premise => body
 
   inline const exprt &premise() const
@@ -53,7 +58,6 @@ class string_constraintt: public exprt
     copy_to_operands(true_exprt(), true_exprt());
   }
 
-  // Returns a new constraints with an universal quantifier added
   string_constraintt(
     const symbol_exprt &univ,
     const exprt &bound_inf,

src/solvers/refinement/string_constraint_generator.cpp

@@ -1,7 +1,8 @@
 /** -*- C++ -*- *****************************************************\
 
-Module: Constraint generation from string function calls
-        for the PASS algorithm (see the PASS paper at HVC'13)
+Module: Generates string constraints to link results from string functions
+        with their arguments. This is inspired by the PASS paper at HVC'13
+	which gives examples of constraints for several functions.
 
 Author: Romain Brenguier, [email protected]
 
@@ -71,6 +72,19 @@ symbol_exprt string_constraint_generatort::fresh_boolean
 }
 
 
+/*******************************************************************\
+
+Function: string_constraint_generatort::add_axioms_for_string_expr
+
+  Inputs: an expression of type string 
+
+ Outputs: a string expression that is link to the argument through 
+          axioms that are added to the list
+
+ Purpose: obtain a refined string expression corresponding to string
+          variable of string function call
+
+\*******************************************************************/
 string_exprt string_constraint_generatort::add_axioms_for_string_expr
 (const exprt & unrefined_string)
 {
@@ -144,7 +158,19 @@ string_exprt string_constraint_generatort::find_or_add_string_of_symbol
   return symbol_to_string[id];
 }
 
+/*******************************************************************\
 
+Function: string_constraint_generatort::add_axioms_for_function_application
+
+  Inputs: an expression containing a function application
+
+ Outputs: expression corresponding to the result of the function application
+
+ Purpose: strings contained in this call are converted to objects of type 
+          `string_exprt`, through adding axioms. Axioms are then added to
+          enforce that the result corresponds to the function application.
+
+\*******************************************************************/
 exprt string_constraint_generatort::add_axioms_for_function_application
 (const function_application_exprt & expr)
 {
@@ -159,7 +185,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application
   else if(id==ID_cprover_string_length_func)
     return add_axioms_for_length(expr);
   else if(id==ID_cprover_string_equal_func)
-    return add_axioms_for_equal(expr);
+    return add_axioms_for_equals(expr);
   else if(id==ID_cprover_string_equals_ignore_case_func)
     return add_axioms_for_equals_ignore_case(expr);
   else if(id==ID_cprover_string_is_empty_func)
@@ -1202,7 +1228,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_float
 }
 
 
-exprt string_constraint_generatort::add_axioms_for_equal
+exprt string_constraint_generatort::add_axioms_for_equals
 (const function_application_exprt &f)
 {
   assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
@@ -1720,7 +1746,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of
   else
     assert(false);
 
-  if(refined_string_typet::is_java_string_type(c.type()))
+  if(refined_string_typet::is_java_string_pointer_type(c.type()))
   {
     string_exprt sub=add_axioms_for_string_expr(c);
     return add_axioms_for_index_of_string(str, sub, from_index);
@@ -1788,7 +1814,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of
   else
     assert(false);
 
-  if(refined_string_typet::is_java_string_type(c.type()))
+  if(refined_string_typet::is_java_string_pointer_type(c.type()))
   {
     string_exprt sub=add_axioms_for_string_expr(c);
     return add_axioms_for_last_index_of_string(str, sub, from_index);