Merge pull request #5440 from thomasspriggs/tas/goto-cc-object-bits-size

Add `--object-bits` option to goto-cc

Author: thomasspriggs

doc/cprover-manual/goto-cc.md

@@ -112,6 +112,9 @@ most important architectural parameters are:
     `sizeof(long int)` on various machines.
 -   The width of pointers; for example, compare the value of `sizeof(int *)` on
     various machines.
+-   The number of bits in a pointer which are used to differentiate between
+    different objects. The remaining bits of a pointer are used for offsets
+    within objects.
 -   The [endianness](http://en.wikipedia.org/wiki/Endianness) of
     the architecture.
 
@@ -129,6 +132,8 @@ following command-line arguments can be passed to the CPROVER tools:
 -   The word-width can be set with `--16`, `--32`, `--64`.
 -   The endianness can be defined with `--little-endian` and
     `--big-endian`.
+-   The number of bits in a pointer used to differentiate between different
+    objects can be set using `--object-bits x`. Where `x` is the number of bits.
 
 When using a goto binary, CBMC and the other tools read the
 configuration from the binary. The setting when running goto-cc is

regression/CMakeLists.txt

@@ -47,6 +47,7 @@ else()
   add_subdirectory(goto-cl)
 endif()
 add_subdirectory(goto-cc-cbmc)
+add_subdirectory(goto-cc-cbmc-shared-options)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(statement-list)

regression/goto-cc-cbmc-shared-options/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/goto-cc-cbmc-shared-options/Makefile

@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-cbmc-shared-options/chain.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+options=${*:4:$#-4}
+name=${*:$#}
+base_name=${name%.c}
+base_name=${base_name%.cpp}
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" "${name}" ${options}
+  mv "${base_name}.exe" "${base_name}.gb"
+else
+  "${goto_cc}" "${name}" -o "${base_name}.gb" ${options}
+fi
+
+"${cbmc}" "${base_name}.gb" ${options}

regression/goto-cc-cbmc-shared-options/object-bits/default_bits.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--function main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion object_bits != 6: SUCCESS
+assertion object_bits != 8: FAILURE
+assertion object_bits != 10: SUCCESS
+--
+^warning: ignoring
+--
+Test that the default value for object-bits is 8.

regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--function main --object-bits 6
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion object_bits != 6: FAILURE
+assertion object_bits != 8: SUCCESS
+assertion object_bits != 10: SUCCESS
+--
+^warning: ignoring
+--
+Test test running with fewer bits than usual results in correct setup of
+intrinsic constants.

regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--function main --object-bits 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion object_bits != 6: SUCCESS
+assertion object_bits != 8: SUCCESS
+assertion object_bits != 10: FAILURE
+--
+^warning: ignoring
+--
+Test test running with more bits than usual results in correct setup of
+intrinsic constants.

regression/goto-cc-cbmc-shared-options/object-bits/test.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+size_t
+find_first_set(const size_t max_malloc_size, const size_t bits_accumulator)
+{
+  if(max_malloc_size & 1)
+    return bits_accumulator;
+  return find_first_set(max_malloc_size >> 1, bits_accumulator + 1);
+}
+
+size_t calculate_object_bits()
+{
+  const size_t ptr_size = sizeof(void *) * 8;
+  return ptr_size - find_first_set(__CPROVER_max_malloc_size, 1);
+}
+
+int main()
+{
+  void *temp = malloc(2);
+  size_t object_bits = calculate_object_bits();
+  assert(object_bits != 6);
+  assert(object_bits != 8);
+  assert(object_bits != 10);
+  __CPROVER_assume("end of main.");
+}

regression/goto-cc-cbmc-shared-options/readme.md

@@ -0,0 +1,4 @@
+This directory is for tests where we -
+ 1) Run `goto-cc` on the specified input file, with the specified options.
+ 2) Run `cbmc` on the goto binary produced in step 1. Using the same options
+    from the `.desc` file as were specified in step 1.

src/goto-cc/gcc_cmdline.cpp

@@ -28,6 +28,7 @@ const char *goto_cc_options_with_separated_argument[]=
   "--native-linker",
   "--print-rejected-preprocessed-source",
   "--mangle-suffix",
+  "--object-bits",
   nullptr
 };
 

src/goto-cc/goto_cc_mode.cpp

@@ -66,6 +66,7 @@ void goto_cc_modet::help()
   " --native-assembler cmd      command to invoke as assembler (goto-as only)\n"
   " --print-rejected-preprocessed-source file\n"
   "                             copy failing (preprocessed) source to file\n"
+  " --object-bits               number of bits used for object addresses\n"
   "\n";
   // clang-format on
 }