Merge pull request #3455 from danpoe/feature/nondet-function-argument-targets

Generate function bodies that nondet havoc the function arguments [blocks: #3457]

Author: danpoe

regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void func(int *p);
+
+void main()
+{
+  int *p;
+  p = NULL;
+
+  func(p);
+}

regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --pointer-check
+^SIGNAL=0$
+^EXIT=0$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-simple/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void func(int *p);
+
+void main()
+{
+  int i;
+  i = 0;
+
+  func(&i);
+
+  assert(i == 0);
+}

regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion i == 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st2 *to_st2;
+  int data;
+} st1_t;
+
+typedef struct st2
+{
+  struct st1 *to_st1;
+  int data;
+} st2_t;
+
+st1_t dummy1;
+st2_t dummy2;
+
+void func(st1_t *p);
+
+void main()
+{
+  st1_t st;
+
+  func(&st);
+
+  assert(st.to_st2 != NULL);
+  assert(st.to_st2->to_st1 != NULL);
+  assert(st.to_st2->to_st1->to_st2 == NULL);
+
+  assert(st.to_st2 != &dummy2);
+  assert(st.to_st2->to_st1 != &dummy1);
+}

regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options 'havoc,params:p' --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  int data;
+} st_t;
+
+void func(st_t *p);
+
+void main()
+{
+  st_t st;
+  st.data = 0;
+
+  func(&st);
+
+  assert(st.data == 0);
+}

regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion st.data == 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  struct st *prev;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p);
+
+void main()
+{
+  st_t st;
+
+  func(&st);
+
+  assert(st.prev != NULL);
+  assert(st.prev != &dummy);
+
+  assert(st.next != NULL);
+  assert(st.next != &dummy);
+
+  assert(st.prev->prev == NULL);
+  assert(st.prev->next == NULL);
+  assert(st.next->prev == NULL);
+  assert(st.next->next == NULL);
+}

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p);
+
+void main()
+{
+  st_t st;
+
+  func(&st);
+
+  assert(st.next != NULL);
+  assert(st.next->next != NULL);
+  assert(st.next->next->next == NULL);
+
+  assert(st.next != &dummy);
+  assert(st.next->next != &dummy);
+}

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/ansi-c/ansi_c_entry_point.cpp

@@ -42,7 +42,8 @@ exprt::operandst build_function_environment(
       base_name,
       p.type(),
       p.source_location(),
-      object_factory_parameters);
+      object_factory_parameters,
+      lifetimet::AUTOMATIC_LOCAL);
   }
 
   return main_arguments;

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -25,79 +25,29 @@ Author: Diffblue Ltd.
 
 #include <goto-programs/goto_functions.h>
 
-class symbol_factoryt
-{
-  symbol_tablet &symbol_table;
-  const source_locationt &loc;
-  namespacet ns;
-  const c_object_factory_parameterst &object_factory_params;
-
-  allocate_objectst allocate_objects;
-
-  typedef std::set<irep_idt> recursion_sett;
-
-public:
-  symbol_factoryt(
-    symbol_tablet &_symbol_table,
-    const source_locationt &loc,
-    const c_object_factory_parameterst &object_factory_params)
-    : symbol_table(_symbol_table),
-      loc(loc),
-      ns(_symbol_table),
-      object_factory_params(object_factory_params),
-      allocate_objects(ID_C, loc, loc.get_function(), symbol_table)
-  {}
-
-  void gen_nondet_init(
-    code_blockt &assignments,
-    const exprt &expr,
-    const std::size_t depth = 0,
-    recursion_sett recursion_set = recursion_sett());
-
-  void add_created_symbol(const symbolt *symbol_ptr)
-  {
-    allocate_objects.add_created_symbol(symbol_ptr);
-  }
-
-  void declare_created_symbols(code_blockt &init_code)
-  {
-    allocate_objects.declare_created_symbols(init_code);
-  }
-
-  void mark_created_symbols_as_input(code_blockt &init_code)
-  {
-    allocate_objects.mark_created_symbols_as_input(init_code);
-  }
-
-private:
-  /// Generate initialisation code for each array element
-  /// \param assignments: The code block to add code to
-  /// \param expr: An expression of array type
-  /// \param depth: The struct recursion depth
-  /// \param recursion_set: The struct recursion set
-  /// \see gen_nondet_init For the meaning of the last 2 parameters
-  void gen_nondet_array_init(
-    code_blockt &assignments,
-    const exprt &expr,
-    std::size_t depth,
-    const recursion_sett &recursion_set);
-};
-
 /// Creates a nondet for expr, including calling itself recursively to make
 /// appropriate symbols to point to if expr is a pointer.
 /// \param assignments: The code block to add code to
 /// \param expr: The expression which we are generating a non-determinate value
 ///   for
-/// \param depth: number of pointers followed so far during initialisation
-/// \param recursion_set: names of structs seen so far on current pointer chain
+/// \param depth number of pointers followed so far during initialisation
+/// \param recursion_set names of structs seen so far on current pointer chain
+/// \param assign_const Indicates whether const objects should be nondet
+///   initialized
 void symbol_factoryt::gen_nondet_init(
   code_blockt &assignments,
   const exprt &expr,
   const std::size_t depth,
-  recursion_sett recursion_set)
+  recursion_sett recursion_set,
+  const bool assign_const)
 {
   const typet &type = expr.type();
 
+  if(!assign_const && expr.type().get_bool(ID_C_constant))
+  {
+    return;
+  }
+
   if(type.id()==ID_pointer)
   {
     // dereferenced type
@@ -120,10 +70,10 @@ void symbol_factoryt::gen_nondet_init(
 
     code_blockt non_null_inst;
 
-    exprt init_expr = allocate_objects.allocate_automatic_local_object(
-      non_null_inst, expr, subtype);
+    exprt init_expr =
+      allocate_objects.allocate_object(non_null_inst, expr, subtype, lifetime);
 
-    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set);
+    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
 
     if(depth < object_factory_params.min_null_tree_depth)
     {
@@ -165,12 +115,18 @@ void symbol_factoryt::gen_nondet_init(
     for(const auto &component : struct_type.components())
     {
       const typet &component_type = component.type();
+
+      if(!assign_const && component_type.get_bool(ID_C_constant))
+      {
+        continue;
+      }
+
       const irep_idt name = component.get_name();
 
       member_exprt me(expr, name, component_type);
       me.add_source_location() = loc;
 
-      gen_nondet_init(assignments, me, depth, recursion_set);
+      gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
     }
   }
   else if(type.id() == ID_array)
@@ -221,14 +177,17 @@ void symbol_factoryt::gen_nondet_array_init(
 /// \param loc: The location to assign to generated code
 /// \param object_factory_parameters: configuration parameters for the object
 ///   factory
+/// \param lifetime: Lifetime of the allocated object (AUTOMATIC_LOCAL,
+///   STATIC_GLOBAL, or DYNAMIC)
 /// \return Returns the symbol_exprt for the symbol created
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   const irep_idt base_name,
   const typet &type,
   const source_locationt &loc,
-  const c_object_factory_parameterst &object_factory_parameters)
+  const c_object_factory_parameterst &object_factory_parameters,
+  const lifetimet lifetime)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -247,7 +206,8 @@ symbol_exprt c_nondet_symbol_factory(
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
   CHECK_RETURN(!moving_symbol_failed);
 
-  symbol_factoryt state(symbol_table, loc, object_factory_parameters);
+  symbol_factoryt state(symbol_table, loc, object_factory_parameters, lifetime);
+
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);