Refactor out havoc utility functions

Author: SaswatPadhi

src/goto-instrument/Makefile

@@ -43,6 +43,7 @@ SRC = accelerate/accelerate.cpp \
       goto_instrument_parse_options.cpp \
       goto_program2code.cpp \
       havoc_loops.cpp \
+      havoc_utils.cpp \
       horn_encoding.cpp \
       insert_final_assert_false.cpp \
       interrupt.cpp \

src/goto-instrument/contracts/assigns.cpp

@@ -13,6 +13,8 @@ Date: July 2021
 
 #include "assigns.h"
 
+#include <goto-instrument/havoc_utils.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_predicates.h>

src/goto-instrument/contracts/contracts.cpp

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Verify and use annotated invariants and pre/post-conditions
+Module: Verify and use annotated loop and function contracts
 
 Author: Michael Tautschnig
 
@@ -9,20 +9,19 @@ Date: February 2016
 \*******************************************************************/
 
 /// \file
-/// Verify and use annotated invariants and pre/post-conditions
+/// Verify and use annotated loop and function contracts
 
 #include "contracts.h"
 
-#include "assigns.h"
-#include "memory_predicates.h"
-
 #include <algorithm>
 #include <map>
 
 #include <analyses/local_may_alias.h>
 
 #include <ansi-c/c_expr.h>
 
+#include <goto-instrument/havoc_utils.h>
+
 #include <goto-programs/remove_skip.h>
 
 #include <util/c_types.h>
@@ -34,6 +33,9 @@ Date: February 2016
 #include <util/pointer_offset_size.h>
 #include <util/replace_symbol.h>
 
+#include "assigns.h"
+#include "memory_predicates.h"
+
 // Create a lexicographic less-than relation between two tuples of variables.
 // This is used in the implementation of multidimensional decreases clauses.
 static exprt create_lexicographic_less_than(
@@ -185,8 +187,8 @@ void code_contractst::check_apply_loop_contracts(
       "Check loop invariant before entry");
   }
 
-  // havoc variables being written to
-  build_havoc_code(loop_head, modifies, havoc_code);
+  // havoc the variables that may be modified
+  append_havoc_code(loop_head->source_location, modifies, havoc_code);
 
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,

src/goto-instrument/havoc_loops.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 
 #include "function_modifies.h"
+#include "havoc_utils.h"
 #include "loop_utils.h"
 
 class havoc_loopst
@@ -67,7 +68,7 @@ void havoc_loopst::havoc_loop(
 
   // build the havocking code
   goto_programt havoc_code;
-  build_havoc_code(loop_head, modifies, havoc_code);
+  append_havoc_code(loop_head->source_location, modifies, havoc_code);
 
   // Now havoc at the loop head. Use insert_swap to
   // preserve jumps to loop head.

src/goto-instrument/havoc_utils.cpp

@@ -0,0 +1,62 @@
+/*******************************************************************\
+
+Module: Utilities for building havoc code for expressions.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: July 2021
+
+\*******************************************************************/
+
+/// \file
+/// Utilities for building havoc code for expressions
+
+#include "havoc_utils.h"
+
+#include <util/expr_util.h>
+#include <util/pointer_expr.h>
+
+void append_object_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest)
+{
+  codet havoc(ID_havoc_object);
+  havoc.add_source_location() = source_location;
+  havoc.add_to_operands(expr);
+  dest.add(goto_programt::make_other(havoc, source_location));
+}
+
+void append_scalar_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest)
+{
+  side_effect_expr_nondett rhs(expr.type(), source_location);
+  goto_programt::targett t = dest.add(
+    goto_programt::make_assignment(expr, std::move(rhs), source_location));
+  t->code_nonconst().add_source_location() = source_location;
+}
+
+void append_havoc_code(
+  const source_locationt source_location,
+  const modifiest &modifies,
+  goto_programt &dest)
+{
+  havoc_utils_is_constantt is_constant(modifies);
+  for(const auto &expr : modifies)
+  {
+    if(expr.id() == ID_index || expr.id() == ID_dereference)
+    {
+      address_of_exprt address_of_expr(expr);
+      if(!is_constant(address_of_expr))
+      {
+        append_object_havoc_code_for_expr(
+          source_location, address_of_expr, dest);
+        continue;
+      }
+    }
+
+    append_scalar_havoc_code_for_expr(source_location, expr, dest);
+  }
+}

src/goto-instrument/havoc_utils.h

@@ -0,0 +1,61 @@
+/*******************************************************************\
+
+Module: Utilities for building havoc code for expressions.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: July 2021
+
+\*******************************************************************/
+
+/// \file
+/// Utilities for building havoc code for expressions
+
+#ifndef CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
+#define CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
+
+#include <set>
+
+#include <goto-programs/goto_program.h>
+
+#include <util/expr_util.h>
+
+typedef std::set<exprt> modifiest;
+
+class havoc_utils_is_constantt : public is_constantt
+{
+public:
+  explicit havoc_utils_is_constantt(const modifiest &mod) : modifies(mod)
+  {
+  }
+
+  bool is_constant(const exprt &expr) const override
+  {
+    // Besides the "usual" constants (checked in is_constantt::is_constant),
+    // we also treat unmodified symbols as constants
+    if(expr.id() == ID_symbol && modifies.find(expr) == modifies.end())
+      return true;
+
+    return is_constantt::is_constant(expr);
+  }
+
+protected:
+  const modifiest &modifies;
+};
+
+void append_havoc_code(
+  const source_locationt source_location,
+  const modifiest &modifies,
+  goto_programt &dest);
+
+void append_object_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest);
+
+void append_scalar_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest);
+
+#endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H

src/goto-instrument/k_induction.cpp

@@ -16,8 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/remove_skip.h>
 
-#include "unwind.h"
+#include "havoc_utils.h"
 #include "loop_utils.h"
+#include "unwind.h"
 
 class k_inductiont
 {
@@ -96,7 +97,7 @@ void k_inductiont::process_loop(
 
     // build the havocking code
     goto_programt havoc_code;
-    build_havoc_code(loop_head, modifies, havoc_code);
+    append_havoc_code(loop_head->source_location, modifies, havoc_code);
 
     // unwind to get k+1 copies
     std::vector<goto_programt::targett> iteration_points;

src/goto-instrument/loop_utils.cpp

@@ -11,33 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "loop_utils.h"
 
-#include <util/expr_util.h>
-#include <util/pointer_expr.h>
-#include <util/std_expr.h>
-
-#include <goto-programs/pointer_arithmetic.h>
-
 #include <analyses/local_may_alias.h>
 
-class loop_utils_is_constantt : public is_constantt
-{
-public:
-  explicit loop_utils_is_constantt(const modifiest &mod) : modifies(mod)
-  {
-  }
-  bool is_constant(const exprt &expr) const override
-  {
-    // Besides the "usual" constants (checked in is_constantt::is_constant),
-    // we also treat unmodified symbols as constants
-    if(expr.id() == ID_symbol && modifies.find(expr) == modifies.end())
-      return true;
-
-    return is_constantt::is_constant(expr);
-  }
+#include <goto-programs/pointer_arithmetic.h>
 
-protected:
-  const modifiest &modifies;
-};
+#include <util/pointer_expr.h>
+#include <util/std_expr.h>
 
 goto_programt::targett get_loop_exit(const loopt &loop)
 {
@@ -57,51 +36,6 @@ goto_programt::targett get_loop_exit(const loopt &loop)
   return ++last;
 }
 
-void build_havoc_code_for_scalar(
-  const goto_programt::targett loop_head,
-  const exprt &lhs,
-  goto_programt &dest)
-{
-  side_effect_expr_nondett rhs(lhs.type(), loop_head->source_location);
-
-  goto_programt::targett t = dest.add(goto_programt::make_assignment(
-    lhs, std::move(rhs), loop_head->source_location));
-  t->code_nonconst().add_source_location() = loop_head->source_location;
-}
-
-void build_havoc_code_for_object(
-  const goto_programt::targett loop_head,
-  const exprt &lhs,
-  goto_programt &dest)
-{
-  codet havoc(ID_havoc_object);
-  havoc.add_source_location() = loop_head->source_location;
-  havoc.add_to_operands(lhs);
-
-  dest.add(goto_programt::make_other(havoc, loop_head->source_location));
-}
-
-void build_havoc_code(
-  const goto_programt::targett loop_head,
-  const modifiest &modifies,
-  goto_programt &dest)
-{
-  loop_utils_is_constantt is_constant(modifies);
-  for(const auto &lhs : modifies)
-  {
-    if(lhs.id() == ID_index || lhs.id() == ID_dereference)
-    {
-      address_of_exprt address_of_lhs(lhs);
-      if(!is_constant(address_of_lhs))
-      {
-        build_havoc_code_for_object(loop_head, address_of_lhs, dest);
-        continue;
-      }
-    }
-
-    build_havoc_code_for_scalar(loop_head, lhs, dest);
-  }
-}
 
 void get_modifies_lhs(
   const local_may_aliast &local_may_alias,

src/goto-instrument/loop_utils.h

@@ -30,11 +30,6 @@ void get_modifies_lhs(
   const exprt &lhs,
   modifiest &modifies);
 
-void build_havoc_code(
-  const goto_programt::targett loop_head,
-  const modifiest &modifies,
-  goto_programt &dest);
-
 goto_programt::targett get_loop_exit(const loopt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H