Merge pull request #6411 from diffblue/validate_code

tautschnig · web-flow · commit e7eff1ea6ea0 · 2021-10-22T22:17:13.000+02:00
Move goto_instruction_code.h to goto-programs/
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.h b/jbmc/src/java_bytecode/character_refine_preprocess.h
@@ -20,7 +20,8 @@ Date:   March 2017
 #ifndef CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
 #define CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/mp_arith.h>
 #include <util/std_code.h>
 
diff --git a/jbmc/src/java_bytecode/code_with_references.cpp b/jbmc/src/java_bytecode/code_with_references.cpp
@@ -9,8 +9,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include "code_with_references.h"
 #include "java_types.h"
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
-#include <util/goto_instruction_code.h>
 
 codet allocate_array(
   const exprt &expr,
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -10,9 +10,10 @@ Date:   June 2017
 
 #include "java_bytecode_instrument.h"
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/goto_instruction_code.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp
@@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_bytecode_typecheck.h"
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/std_code.h>
 
 void java_bytecode_typecheckt::typecheck_code(codet &code)
diff --git a/jbmc/src/java_bytecode/lift_clinit_calls.cpp b/jbmc/src/java_bytecode/lift_clinit_calls.cpp
@@ -12,8 +12,9 @@ Author: Diffblue Ltd.
 
 #include <java_bytecode/java_static_initializers.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/expr_iterator.h>
-#include <util/goto_instruction_code.h>
 
 #include <algorithm>
 
diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h
@@ -9,7 +9,8 @@ Author: Diffblue Ltd.
 /// \file
 /// Utilties for inspecting goto functions
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/optional.h>
 
 #include <regex>
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
@@ -15,8 +15,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <testing-utils/expr_query.h>
 #include <testing-utils/use_catch.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
-#include <util/goto_instruction_code.h>
 #include <util/json.h>
 #include <util/symbol_table.h>
 
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp
@@ -15,8 +15,9 @@ Author: Diffblue Ltd.
 #include <testing-utils/expr_query.h>
 #include <testing-utils/use_catch.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
-#include <util/goto_instruction_code.h>
 #include <util/json.h>
 #include <util/symbol_table.h>
 
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt b/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt
@@ -1,3 +1,4 @@
+goto-programs
 java_bytecode
 testing-utils
 util
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -14,11 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
-#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <atomic>
 
 #include "c_expr.h"
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <unordered_set>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/fresh_symbol.h>
-#include <util/goto_instruction_code.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
@@ -16,9 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_map>
 #include <unordered_set>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
-#include <util/goto_instruction_code.h>
 #include <util/mathematical_expr.h>
 #include <util/std_code.h>
 
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
@@ -11,9 +11,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp
@@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/pointer_expr.h>
 
 bool cpp_typecheckt::find_dtor(const symbolt &symbol) const
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
@@ -11,10 +11,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
-#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 
diff --git a/src/goto-instrument/object_id.cpp b/src/goto-instrument/object_id.cpp
@@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "object_id.h"
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/pointer_expr.h>
 
 enum class get_modet { LHS_R, LHS_W, READ };
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
@@ -21,6 +21,7 @@ SRC = allocate_objects.cpp \
       goto_functions.cpp \
       goto_inline_class.cpp \
       goto_inline.cpp \
+      goto_instruction_code.cpp \
       goto_program.cpp \
       goto_trace.cpp \
       graphml_witness.cpp \
@@ -69,6 +70,7 @@ SRC = allocate_objects.cpp \
       string_instrumentation.cpp \
       structured_trace_util.cpp \
       system_library_symbols.cpp \
+      validate_code.cpp \
       validate_goto_model.cpp \
       vcd_goto_trace.cpp \
       wp.cpp \
diff --git a/src/goto-programs/allocate_objects.h b/src/goto-programs/allocate_objects.h
@@ -9,7 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
 #define CPROVER_UTIL_ALLOCATE_OBJECTS_H
 
-#include <util/goto_instruction_code.h>
+#include "goto_instruction_code.h"
+
 #include <util/namespace.h>
 #include <util/source_location.h>
 #include <util/std_code.h>
diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp
@@ -10,8 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Destructor Calls
 
 #include "destructor.h"
+#include "goto_instruction_code.h"
 
-#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 
 code_function_callt get_destructor(
diff --git a/src/goto-programs/goto_instruction_code.cpp b/src/goto-programs/goto_instruction_code.cpp
@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+Module: Data structures representing instructions in a GOTO program
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Data structures representing instructions in a GOTO program
+
+#include "goto_instruction_code.h"
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/string_constant.h>
+
+code_inputt::code_inputt(
+  std::vector<exprt> arguments,
+  optionalt<source_locationt> location)
+  : codet{ID_input, std::move(arguments)}
+{
+  if(location)
+    add_source_location() = std::move(*location);
+  check(*this, validation_modet::INVARIANT);
+}
+
+code_inputt::code_inputt(
+  const irep_idt &description,
+  exprt expression,
+  optionalt<source_locationt> location)
+  : code_inputt{{address_of_exprt(index_exprt(
+                   string_constantt(description),
+                   from_integer(0, index_type()))),
+                 std::move(expression)},
+                std::move(location)}
+{
+}
+
+void code_inputt::check(const codet &code, const validation_modet vm)
+{
+  DATA_CHECK(
+    vm, code.operands().size() >= 2, "input must have at least two operands");
+}
+
+code_outputt::code_outputt(
+  std::vector<exprt> arguments,
+  optionalt<source_locationt> location)
+  : codet{ID_output, std::move(arguments)}
+{
+  if(location)
+    add_source_location() = std::move(*location);
+  check(*this, validation_modet::INVARIANT);
+}
+
+code_outputt::code_outputt(
+  const irep_idt &description,
+  exprt expression,
+  optionalt<source_locationt> location)
+  : code_outputt{{address_of_exprt(index_exprt(
+                    string_constantt(description),
+                    from_integer(0, index_type()))),
+                  std::move(expression)},
+                 std::move(location)}
+{
+}
+
+void code_outputt::check(const codet &code, const validation_modet vm)
+{
+  DATA_CHECK(
+    vm, code.operands().size() >= 2, "output must have at least two operands");
+}
diff --git a/src/goto-programs/goto_instruction_code.h b/src/goto-programs/goto_instruction_code.h
@@ -9,8 +9,8 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
 #define CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
 
-#include "std_code_base.h"
-#include "std_expr.h"
+#include <util/std_code_base.h>
+#include <util/std_expr.h>
 
 /// A \ref codet representing an assignment in the program.
 /// For example, if an expression `e1` is represented as an \ref exprt `expr1`
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_program.h"
 
+#include "validate_code.h"
+
 #include <iomanip>
 
 #include <util/base_type.h>
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -12,13 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 
+#include "goto_instruction_code.h"
+
 #include <iosfwd>
 #include <set>
 #include <limits>
 #include <string>
 
 #include <util/deprecate.h>
-#include <util/goto_instruction_code.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/source_location.h>
diff --git a/src/goto-programs/validate_code.cpp b/src/goto-programs/validate_code.cpp
@@ -9,12 +9,13 @@ Author: Daniel Poetzl
 #include "validate_code.h"
 
 #ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
-#include <iostream>
+#  include <iostream>
 #endif
 
 #include "goto_instruction_code.h"
-#include "std_code.h"
-#include "validate_helpers.h"
+
+#include <util/std_code.h>
+#include <util/validate_helpers.h>
 
 #define CALL_ON_CODE(code_type)                                                \
   C<codet, code_type>()(code, std::forward<Args>(args)...)
diff --git a/src/goto-programs/validate_code.h b/src/goto-programs/validate_code.h
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
@@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // #include <langapi/language_util.h>
 
-#include <util/goto_instruction_code.h>
-#include <util/pointer_expr.h>
-#include <util/std_code.h>
+#include "goto_instruction_code.h"
 
 #include <util/invariant.h>
+#include <util/pointer_expr.h>
+#include <util/std_code.h>
 
 bool has_nondet(const exprt &dest)
 {
diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp
@@ -11,7 +11,8 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include "jsil_convert.h"
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/message.h>
 #include <util/symbol_table.h>
 
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
@@ -11,8 +11,9 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include "jsil_typecheck.h"
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/bitvector_types.h>
-#include <util/goto_instruction_code.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
@@ -11,7 +11,8 @@ extern char *yyjsiltext;
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
 
-#include <util/goto_instruction_code.h>
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/string_constant.h>
 
 #include "jsil_y.tab.h"
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
@@ -8,10 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "static_lifetime_init.h"
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
-#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp
diff --git a/src/util/Makefile b/src/util/Makefile
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp
diff --git a/src/util/std_code.h b/src/util/std_code.h
diff --git a/src/util/std_code_base.h b/src/util/std_code_base.h
diff --git a/unit/util/format.cpp b/unit/util/format.cpp
