Merge pull request #6658 from diffblue/move_goto_check_c

move goto_check_ct to ansi-c/

Author: kroening

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -11,13 +11,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "janalyzer_parse_options.h"
 
-#include <cstdlib> // exit()
-#include <fstream>
-#include <iostream>
-#include <memory>
-
-#include <ansi-c/ansi_c_language.h>
+#include <util/config.h>
+#include <util/exit_codes.h>
+#include <util/options.h>
+#include <util/version.h>
 
+#include <goto-programs/goto_check.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -27,30 +26,26 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/constant_propagator.h>
 #include <analyses/dependence_graph.h>
-#include <analyses/goto_check.h>
 #include <analyses/interval_domain.h>
 #include <analyses/local_may_alias.h>
-
+#include <ansi-c/ansi_c_language.h>
+#include <goto-analyzer/static_show_domain.h>
+#include <goto-analyzer/static_simplifier.h>
+#include <goto-analyzer/static_verifier.h>
+#include <goto-analyzer/taint_analysis.h>
+#include <goto-analyzer/unreachable_instructions.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/lazy_goto_model.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
-
 #include <langapi/language.h>
 #include <langapi/mode.h>
-
 #include <linking/static_lifetime_init.h>
 
-#include <util/config.h>
-#include <util/exit_codes.h>
-#include <util/options.h>
-#include <util/version.h>
-
-#include <goto-analyzer/static_show_domain.h>
-#include <goto-analyzer/static_simplifier.h>
-#include <goto-analyzer/static_verifier.h>
-#include <goto-analyzer/taint_analysis.h>
-#include <goto-analyzer/unreachable_instructions.h>
+#include <cstdlib> // exit()
+#include <fstream>
+#include <iostream>
+#include <memory>
 
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
   : parse_options_baset(

jbmc/src/jbmc/CMakeLists.txt

@@ -8,7 +8,6 @@ add_library(jbmc-lib ${sources})
 generic_includes(jbmc-lib)
 
 target_link_libraries(jbmc-lib
-    analyses
     ansi-c
     big-int
     cbmc-lib

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/xml.h>
 
 #include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/goto_check.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
@@ -31,7 +32,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
 
-#include <analyses/goto_check.h>
 #include <ansi-c/ansi_c_language.h>
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_fault_localization.h>

jbmc/src/jbmc/module_dependencies.txt

@@ -1,4 +1,3 @@
-analyses
 ansi-c # should go away
 goto-checker
 goto-instrument

jbmc/src/jdiff/CMakeLists.txt

@@ -15,7 +15,6 @@ target_link_libraries(jdiff-lib
     goto-diff-lib
     goto-instrument-lib
     goto-programs
-    analyses
     java_bytecode
     langapi
     xml

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -17,6 +17,7 @@ Author: Peter Schrammel
 #include <util/version.h>
 
 #include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/goto_check.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
@@ -28,7 +29,6 @@ Author: Peter Schrammel
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/goto_check.h>
 #include <goto-diff/change_impact.h>
 #include <goto-diff/unified_diff.h>
 #include <goto-instrument/cover.h>

jbmc/src/jdiff/module_dependencies.txt

@@ -1,4 +1,3 @@
-analyses
 java_bytecode
 jdiff
 goto-diff

src/Makefile

@@ -59,6 +59,8 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
 .PHONY: languages
 .PHONY: clean
 
+ansi-c.dir: analyses.dir
+
 cpp.dir: ansi-c.dir linking.dir
 
 crangler.dir: util.dir json.dir

src/analyses/Makefile

@@ -12,8 +12,6 @@ SRC = ai.cpp \
       escape_analysis.cpp \
       flow_insensitive_analysis.cpp \
       global_may_alias.cpp \
-      goto_check.cpp \
-      goto_check_c.cpp \
       goto_rw.cpp \
       guard_bdd.cpp \
       guard_expr.cpp \

src/ansi-c/CMakeLists.txt

@@ -127,4 +127,4 @@ set_source_files_properties(
 
 generic_includes(ansi-c)
 
-target_link_libraries(ansi-c util linking goto-programs assembler)
+target_link_libraries(ansi-c analyses util linking goto-programs assembler)

src/ansi-c/Makefile

@@ -31,6 +31,7 @@ SRC = anonymous_member.cpp \
       expr2c.cpp \
       gcc_types.cpp \
       gcc_version.cpp \
+      goto_check_c.cpp \
       literals/convert_character_literal.cpp \
       literals/convert_float_literal.cpp \
       literals/convert_integer_literal.cpp \

src/analyses/goto_check_c.cpp renamed to src/ansi-c/goto_check_c.cpp

@@ -11,9 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_check_c.h"
 
-#include <algorithm>
-#include <optional>
-
 #include <util/arith_tools.h>
 #include <util/array_name.h>
 #include <util/bitvector_expr.h>
@@ -37,13 +34,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-#include <langapi/language.h>
-#include <langapi/mode.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include "local_bitvector_analysis.h"
+#include <analyses/local_bitvector_analysis.h>
+#include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <algorithm>
+#include <optional>
 
 class goto_check_ct
 {
@@ -986,11 +985,12 @@ void goto_check_ct::integer_overflow_check(
       // a shift of zero isn't overflow;
       // else check the top bits
       add_guarded_property(
-        disjunction({neg_value_shift,
-                     neg_dist_shift,
-                     dist_too_large,
-                     op_zero,
-                     top_bits_zero}),
+        disjunction(
+          {neg_value_shift,
+           neg_dist_shift,
+           dist_too_large,
+           op_zero,
+           top_bits_zero}),
         "arithmetic overflow on signed shl",
         "overflow",
         expr.find_source_location(),
@@ -1554,9 +1554,10 @@ void goto_check_ct::bounds_check_index(
           exprt p_offset =
             pointer_offset(to_dereference_expr(ode.root_object()).pointer());
 
-          effective_offset = plus_exprt{p_offset,
-                                        typecast_exprt::conditional_cast(
-                                          effective_offset, p_offset.type())};
+          effective_offset = plus_exprt{
+            p_offset,
+            typecast_exprt::conditional_cast(
+              effective_offset, p_offset.type())};
         }
 
         exprt zero = from_integer(0, ode.offset().type());
@@ -1825,9 +1826,10 @@ bool goto_check_ct::check_rec_member(
       deref.pointer(), pointer_type(char_type()));
 
     const exprt new_address_casted = typecast_exprt::conditional_cast(
-      plus_exprt{char_pointer,
-                 typecast_exprt::conditional_cast(
-                   member_offset_opt.value(), pointer_diff_type())},
+      plus_exprt{
+        char_pointer,
+        typecast_exprt::conditional_cast(
+          member_offset_opt.value(), pointer_diff_type())},
       new_pointer_type);
 
     dereference_exprt new_deref{new_address_casted};
@@ -2368,8 +2370,9 @@ goto_check_ct::get_pointer_is_null_condition(
   if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
   {
     return {conditiont{
-      or_exprt{is_in_bounds_of_some_explicit_allocation(address, size),
-               not_exprt(null_pointer(address))},
+      or_exprt{
+        is_in_bounds_of_some_explicit_allocation(address, size),
+        not_exprt(null_pointer(address))},
       "pointer NULL"}};
   }
 

src/analyses/goto_check_c.h renamed to src/ansi-c/goto_check_c.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Program Transformation
 
-#ifndef CPROVER_ANALYSES_GOTO_CHECK_C_H
-#define CPROVER_ANALYSES_GOTO_CHECK_C_H
+#ifndef CPROVER_ANSI_C_GOTO_CHECK_C_H
+#define CPROVER_ANSI_C_GOTO_CHECK_C_H
 
 #include <goto-programs/goto_functions.h>
 

src/ansi-c/module_dependencies.txt

@@ -1,3 +1,4 @@
+analyses
 ansi-c
 goto-programs
 langapi # should go away

src/cbmc/CMakeLists.txt

@@ -33,7 +33,19 @@ add_if_library(cbmc-lib jsil)
 
 # Executable
 add_executable(cbmc cbmc_main.cpp)
+if(CMAKE_SYSTEM_NAME STREQUAL "Linux")
+# There is a cyclic dependency between analyses and ansi-c, which the
+# Makefile-based build system resolves by using --start-group, --end-group.
+# CMake lacks direct support (cf.
+# https://gitlab.kitware.com/cmake/cmake/-/issues/21511), so we ensure all
+# object files from libanalyses.a remain present.
+target_link_libraries(cbmc
+  cbmc-lib
+  -Wl,--whole-archive -Wl,${CMAKE_BINARY_DIR}/lib/libanalyses.a -Wl,--no-whole-archive
+)
+else()
 target_link_libraries(cbmc cbmc-lib)
+endif()
 install(TARGETS cbmc DESTINATION ${CMAKE_INSTALL_BINDIR})
 
 # Man page

src/cbmc/cbmc_parse_options.h

@@ -12,29 +12,23 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 
-#include <ansi-c/ansi_c_language.h>
-
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
 #include <util/validation_interface.h>
 
-#include <langapi/language.h>
-
-#include <analyses/goto_check_c.h>
-
-#include <goto-checker/bmc_util.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/goto_trace.h>
 
-#include <solvers/strings/string_refinement.h>
-
+#include <ansi-c/ansi_c_language.h>
+#include <ansi-c/goto_check_c.h>
+#include <goto-checker/bmc_util.h>
+#include <goto-instrument/cover.h>
 #include <json/json_interface.h>
+#include <langapi/language.h>
+#include <solvers/strings/string_refinement.h>
 #include <xmllang/xml_interface.h>
 
-#include <goto-instrument/cover.h>
-
 class optionst;
 
 // clang-format off

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -94,14 +94,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/validation_interface.h>
 
-#include <langapi/language.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/goto_check_c.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
+#include <ansi-c/goto_check_c.h>
+#include <langapi/language.h>
 
 class optionst;
 

src/goto-diff/goto_diff_parse_options.h

@@ -12,15 +12,14 @@ Author: Peter Schrammel
 #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
 #define CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
 
-#include <analyses/goto_check_c.h>
-
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
 
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
+#include <ansi-c/goto_check_c.h>
 #include <goto-instrument/cover.h>
 
 class goto_modelt;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/ensure_one_backedge_per_target.h>
+#include <goto-programs/goto_check.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/interpreter.h>
 #include <goto-programs/label_function_pointer_call_sites.h>
@@ -50,10 +51,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/write_goto_binary.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
-#include <pointer-analysis/show_value_sets.h>
-#include <pointer-analysis/value_set_analysis.h>
-
 #include <analyses/call_graph.h>
 #include <analyses/constant_propagator.h>
 #include <analyses/custom_bitvector_analysis.h>
@@ -69,16 +66,15 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/natural_loops.h>
 #include <analyses/reaching_definitions.h>
 #include <analyses/sese_regions.h>
-
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
-
 #include <assembler/remove_asm.h>
-
 #include <cpp/cprover_library.h>
+#include <pointer-analysis/add_failed_symbols.h>
+#include <pointer-analysis/show_value_sets.h>
+#include <pointer-analysis/value_set_analysis.h>
 
-#include "accelerate/accelerate.h"
 #include "alignment_checks.h"
 #include "branch.h"
 #include "call_sequences.h"
@@ -109,6 +105,8 @@ Author: Daniel Kroening, [email protected]
 #include "unwind.h"
 #include "value_set_fi_fp_removal.h"
 
+#include "accelerate/accelerate.h"
+
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
 {