Added __CPROVER_array_replace to complement __CPROVER_array_set

Author: tautschnig

src/ansi-c/ansi_c_internal_additions.cpp

@@ -211,7 +211,11 @@ void ansi_c_internal_additions(std::string &code)
     // arrays
     // NOLINTNEXTLINE(whitespace/line_length)
     "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
+    // overwrite all of *dest (possibly using nondet values), even
+    // if *src is smaller
     "void __CPROVER_array_copy(const void *dest, const void *src);\n"
+    // replace at most size-of-*src bytes in *dest
+    "void __CPROVER_array_replace(const void *dest, const void *src);\n"
     "void __CPROVER_array_set(const void *dest, ...);\n"
 
     // k-induction

src/ansi-c/expr2c.cpp

@@ -3826,6 +3826,9 @@ std::string expr2ct::convert_code(
   if(statement==ID_array_copy)
     return convert_code_array_copy(src, indent);
 
+  if(statement==ID_array_replace)
+    return convert_code_array_replace(src, indent);
+
   if(statement=="set_may" ||
      statement=="set_must")
     return
@@ -4227,6 +4230,39 @@ std::string expr2ct::convert_code_array_copy(
 
 /*******************************************************************\
 
+Function: expr2ct::convert_code_array_replace
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2ct::convert_code_array_replace(
+  const codet &src,
+  unsigned indent)
+{
+  std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
+
+  forall_operands(it, src)
+  {
+    unsigned p;
+    std::string arg_str=convert(*it, p);
+
+    if(it!=src.operands().begin())
+      dest+=", ";
+    dest+=arg_str;
+  }
+
+  dest+=");";
+
+  return dest;
+}
+
+/*******************************************************************\
+
 Function: expr2ct::convert_code_assert
 
   Inputs:

src/ansi-c/expr2c_class.h

@@ -204,6 +204,7 @@ class expr2ct
   std::string convert_code_output(const codet &src, unsigned indent);
   std::string convert_code_array_set(const codet &src, unsigned indent);
   std::string convert_code_array_copy(const codet &src, unsigned indent);
+  std::string convert_code_array_replace(const codet &src, unsigned indent);
 
   virtual std::string convert(const exprt &src, unsigned &precedence);
 

src/ansi-c/library/cprover.h

@@ -102,7 +102,8 @@ float __CPROVER_fabsf(float);
 // arrays
 //__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
 void __CPROVER_array_copy(const void *dest, const void *src);
-//void __CPROVER_array_set(const void *dest, ...);
+void __CPROVER_array_set(const void *dest, ...);
+void __CPROVER_array_replace(const void *dest, const void *src);
 
 #if 0
 // k-induction

src/goto-programs/builtin_functions.cpp

@@ -984,7 +984,7 @@ exprt goto_convertt::get_array_argument(const exprt &src)
 
 /*******************************************************************\
 
-Function: goto_convertt::do_array_set
+Function: goto_convertt::do_array_op
 
   Inputs:
 
@@ -994,7 +994,8 @@ Function: goto_convertt::do_array_set
 
 \*******************************************************************/
 
-void goto_convertt::do_array_set(
+void goto_convertt::do_array_op(
+  const irep_idt &id,
   const exprt &lhs,
   const exprt &function,
   const exprt::operandst &arguments,
@@ -1003,47 +1004,16 @@ void goto_convertt::do_array_set(
   if(arguments.size()!=2)
   {
     error().source_location=function.find_source_location();
-    error() << "array_set expects two arguments" << eom;
+    error() << id << " expects two arguments" << eom;
     throw 0;
   }
 
-  codet array_set_statement;
-  array_set_statement.set_statement(ID_array_set);
-  array_set_statement.operands()=arguments;
+  codet array_op_statement;
+  array_op_statement.set_statement(id);
+  array_op_statement.operands()=arguments;
+  array_op_statement.add_source_location()=function.source_location();
 
-  copy(array_set_statement, OTHER, dest);
-}
-
-/*******************************************************************\
-
-Function: goto_convertt::do_array_copy
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void goto_convertt::do_array_copy(
-  const exprt &lhs,
-  const exprt &function,
-  const exprt::operandst &arguments,
-  goto_programt &dest)
-{
-  if(arguments.size()!=2)
-  {
-    error().source_location=function.find_source_location();
-    error() << "array_copy expects two arguments" << eom;
-    throw 0;
-  }
-
-  codet array_copy_statement;
-  array_copy_statement.set_statement(ID_array_copy);
-  array_copy_statement.operands()=arguments;
-
-  copy(array_copy_statement, OTHER, dest);
+  copy(array_op_statement, OTHER, dest);
 }
 
 /*******************************************************************\
@@ -1096,6 +1066,7 @@ void goto_convertt::do_array_equal(
     assignment.lhs()=lhs;
     assignment.rhs()=binary_exprt(
       lhs_array, ID_array_equal, rhs_array, lhs.type());
+    assignment.add_source_location()=function.source_location();
 
     convert(assignment, dest);
   }
@@ -1427,19 +1398,21 @@ void goto_convertt::do_function_call_symbol(
     assignment.add_source_location()=function.source_location();
     copy(assignment, ASSIGN, dest);
   }
-  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "array_set"))
+  else if(identifier==CPROVER_PREFIX "array_equal")
   {
-    do_array_set(lhs, function, arguments, dest);
+    do_array_equal(lhs, function, arguments, dest);
   }
-  else if(identifier==CPROVER_PREFIX "array_equal" ||
-          identifier=="__CPROVER::array_equal")
+  else if(identifier==CPROVER_PREFIX "array_set")
   {
-    do_array_equal(lhs, function, arguments, dest);
+    do_array_op(ID_array_set, lhs, function, arguments, dest);
+  }
+  else if(identifier==CPROVER_PREFIX "array_copy")
+  {
+    do_array_op(ID_array_copy, lhs, function, arguments, dest);
   }
-  else if(identifier==CPROVER_PREFIX "array_copy" ||
-          identifier=="__CPROVER::array_equal")
+  else if(identifier==CPROVER_PREFIX "array_replace")
   {
-    do_array_copy(lhs, function, arguments, dest);
+    do_array_op(ID_array_replace, lhs, function, arguments, dest);
   }
   else if(identifier=="printf")
   /*

src/goto-programs/goto_convert_class.h

@@ -537,7 +537,8 @@ class goto_convertt:public messaget
     const exprt &rhs,
     const exprt::operandst &arguments,
     goto_programt &dest);
-  void do_array_copy(
+  void do_array_op(
+    const irep_idt &id,
     const exprt &lhs,
     const exprt &rhs,
     const exprt::operandst &arguments,

src/goto-symex/symex_other.cpp

@@ -85,7 +85,8 @@ void goto_symext::symex_other(
   {
     // we ignore this for now
   }
-  else if(statement==ID_array_copy)
+  else if(statement==ID_array_copy ||
+          statement==ID_array_replace)
   {
     assert(code.operands().size()==2);
 
@@ -120,11 +121,21 @@ void goto_symext::symex_other(
                      clean_code.op1().type(), ns))
     {
       byte_extract_exprt be(byte_extract_id());
-      be.type()=clean_code.op0().type();
-      be.op()=clean_code.op1();
       be.offset()=from_integer(0, index_type());
 
-      clean_code.op1()=be;
+      if(statement==ID_array_copy)
+      {
+        be.op()=clean_code.op1();
+        be.type()=clean_code.op0().type();
+        clean_code.op1()=be;
+      }
+      else
+      {
+        // ID_array_replace
+        be.op()=clean_code.op0();
+        be.type()=clean_code.op1().type();
+        clean_code.op0()=be;
+      }
     }
 
     code_assignt assignment;

src/pointer-analysis/value_set.cpp

@@ -1802,6 +1802,9 @@ void value_sett::apply_code(
   else if(statement==ID_array_copy)
   {
   }
+  else if(statement==ID_array_replace)
+  {
+  }
   else if(statement==ID_assume)
   {
     guard(to_code_assume(code).op0(), ns);

src/util/irep_ids.def

@@ -804,6 +804,7 @@ IREP_ID_ONE(cprover_string_to_lower_case_func)
 IREP_ID_ONE(cprover_string_to_upper_case_func)
 IREP_ID_ONE(cprover_string_trim_func)
 IREP_ID_ONE(cprover_string_value_of_func)
+IREP_ID_ONE(array_replace)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO