Feature nondet array initialization [blocks: #3572]

regression/cbmc/pointer-to-array-function-parameters-max-size/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+void test(int *arr, int sz)
+{
+  assert(sz <= 10);
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}

regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --max-dynamic-array-size 20 --pointer-check --unwind 20 --associated-array-sizes arr:sz
+\[test.assertion.1\] line \d+ assertion sz <= 10: FAILURE
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+EXIT=10
+SIGNAL=0

regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int is_prefix_of(
+  const char *string,
+  int string_size,
+  const char *prefix,
+  int prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+
+  for(int ix = 0; ix < prefix_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.c
+--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 20
+SIGNAL=0
+EXIT=0
+VERIFICATION SUCCESSFUL

regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stddef.h>
+
+int is_prefix_of(
+  const char *string,
+  size_t string_size,
+  const char *prefix,
+  size_t prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+  assert(prefix_size <= string_size);
+  // oh no! we should have used prefix_size here
+  for(int ix = 0; ix < string_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 10
+EXIT=10
+SIGNAL=0
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+VERIFICATION FAILED

regression/cbmc/pointer-to-array-function-parameters-with-size/test.c

@@ -0,0 +1,7 @@
+void test(int *arr, int sz)
+{
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}

regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 10 --associated-array-sizes arr:sz
+EXIT=0
+SIGNAL=0
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS

regression/cbmc/pointer-to-array-function-parameters/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void test(int *arr)
+{
+  // works because the arrays we generate have at least one element
+  arr[0] = 5;
+
+  // doesn't work because our arrays have at most ten elements
+  arr[10] = 10;
+}

regression/cbmc/pointer-to-array-function-parameters/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 20
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.12\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+--

scripts/delete_failing_smt2_solver_tests

@@ -49,6 +49,8 @@ rm Quantifiers-invalid-var-range/test.desc
 rm Quantifiers-type/test.desc
 rm Union_Initialization1/test.desc
 rm address_space_size_limit1/test.desc
+rm address_space_size_limit3/test.desc
+rm argv1/test.desc
 rm array-function-parameters/test.desc
 rm array-tests/test.desc
 rm bounds_check1/test.desc
@@ -68,6 +70,15 @@ rm memory_allocation1/test.desc
 rm pointer-function-parameters-struct-mutual-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion-2/test.desc
+rm pointer-function-parameters-struct-simple-recursion-3/test.desc
+rm pointer-to-array-function-parameters-max-size/test.desc
+rm pointer-to-array-function-parameters-multi-arg-right/test.desc
+rm pointer-to-array-function-parameters-multi-arg-wrong/test.desc
+rm pointer-to-array-function-parameters-with-size/test.desc
+rm pointer-to-array-function-parameters/test.desc
+rm read1/test.desc
+rm realloc1/test.desc
+rm realloc2/test.desc
 rm scanf1/test.desc
 rm stack-trace/test.desc
 rm struct6/test.desc

src/ansi-c/ansi_c_entry_point.cpp

@@ -27,7 +27,7 @@ exprt::operandst build_function_environment(
 {
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
-
+  std::map<irep_idt, irep_idt> deferred_array_sizes;
   for(std::size_t param_number=0;
       param_number<parameters.size();
       param_number++)
@@ -42,7 +42,8 @@ exprt::operandst build_function_environment(
       base_name,
       p.type(),
       p.source_location(),
-      object_factory_parameters);
+      object_factory_parameters,
+      deferred_array_sizes);
   }
 
   return main_arguments;

src/ansi-c/ansi_c_language.h

@@ -22,13 +22,26 @@ Author: Daniel Kroening, [email protected]
 // clang-format off
 #define OPT_ANSI_C_LANGUAGE \
   "(max-nondet-tree-depth):" \
-  "(min-null-tree-depth):"
+  "(min-null-tree-depth):" \
+  "(pointers-to-treat-as-arrays):" \
+  "(associated-array-sizes):" \
+  "(max-dynamic-array-size):" \
 
 #define HELP_ANSI_C_LANGUAGE \
   " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\
   "                              at level N pointers are set to null\n" \
   " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */\
-  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */
+  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */\
+  " --pointers-to-treat-as-arrays <identifier,...>  comma separated list of\n" \
+  "                               identifiers that should be initialized as arrays\n" /* NOLINT(*) */ \
+  " --associated-array-sizes <identifier:identifier...>\n" \
+  "                               comma separated list of colon separated pairs\n" /* NOLINT(*) */ \
+  "                               of identifiers; The first element of the pair \n" /* NOLINT(*) */ \
+  "                               should be the name of an array pointer \n" \
+  "                               (see --pointers-to-treat-as-arrays),\n" \
+  "                               the second an integer parameter that\n" \
+  "                               should hold its size\n" \
+  " --max-dynamic-array-size <size>  max size for dynamically allocated arrays\n" /* NOLINT(*) */
 // clang-format on
 
 class ansi_c_languaget:public languaget