Merge pull request #4676 from mmuesly/feature_nondet_static

Add --nondet-static-except flag to CBMC

Author: karkhaz

regression/goto-instrument/chain.sh

@@ -8,13 +8,24 @@ cbmc=$3
 is_windows=$4
 
 name=${*:$#}
-name=${name%.c}
+
+if [[ x$name == x ]];  then
+  name=${name%.c}
+fi
 
 args=${*:5:$#-5}
 
-if [[ "${is_windows}" == "true" ]]; then
+if [[ "${is_windows}" == "true" && x$name != x ]]; then
+  $goto_cc "main.gb" ${name}
+  name="main"
+  mv "${name}.exe" "${name}.gb"
+elif [[ "${is_windows}" == "true" ]]; then
   $goto_cc "${name}.c"
   mv "${name}.exe" "${name}.gb"
+elif [[ x$name != x ]]; then
+  $goto_cc -o "main.gb" ${name}
+  echo "name: ${name}"
+  name="main"
 else
   $goto_cc -o "${name}.gb" "${name}.c"
 fi

regression/goto-instrument/nondet-static-exclude_subfolder/main.c

@@ -0,0 +1,9 @@
+#include "package1/file.c"
+#include "package2/file.c"
+
+void main()
+{
+  method1();
+  method2();
+  return 0;
+}

regression/goto-instrument/nondet-static-exclude_subfolder/package1/file.c

@@ -0,0 +1,8 @@
+static int myVal = 3;
+static int myVal2 = 4;
+
+void method2()
+{
+  __CPROVER_assert(myVal == 3, "method2 myVal");
+  __CPROVER_assert(myVal2 == 4, "method2 myVal2");
+}

regression/goto-instrument/nondet-static-exclude_subfolder/package2/file.c

@@ -0,0 +1,8 @@
+static int myVal = 3;
+static int myVal2 = 4;
+
+void method1()
+{
+  __CPROVER_assert(myVal == 3, "method1 myVal");
+  __CPROVER_assert(myVal2 == 4, "method1 myVal2");
+}

regression/goto-instrument/nondet-static-exclude_subfolder/test.desc

@@ -0,0 +1,12 @@
+CORE
+package1/file.c package2/file.c main.c
+--nondet-static-exclude package1/file.c:myVal --nondet-static-exclude package2/file.c:myVal2
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+method2 myVal: SUCCESS
+method2 myVal2: FAILURE
+method1 myVal: FAILURE
+method1 myVal2: SUCCESS
+--
+--

regression/goto-instrument/nondet_static_exclude/main.c

@@ -0,0 +1,38 @@
+#define NULL 0
+
+struct aStruct
+{
+  int a;
+  int b;
+};
+
+struct aStruct *test1 = NULL;
+
+struct aStruct test2 = {.a = 5, .b = 2};
+struct aStruct test3 = {.a = 1, .b = 4};
+struct aStruct *test4 = &test3;
+struct aStruct *test5 = &test2;
+
+static int value = 7;
+
+#include "main_1.h"
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  assert(test1 == NULL);
+  assert(test2.a == 5);
+  assert(test3.a == 1);
+  assert(test3.b == 4);
+  assert(test4->a == 1);
+  assert(test4->b == 4);
+
+  assert(test5->a == 5);
+  assert(test5->b == 2);
+
+  assert(value == 7);
+
+  setup();
+
+  return 0;
+}

regression/goto-instrument/nondet_static_exclude/main_1.c

@@ -0,0 +1,9 @@
+static int value = 5;
+
+#include <assert.h>
+
+void setup()
+{
+  assert(value == 5);
+  return 0;
+}

regression/goto-instrument/nondet_static_exclude/main_1.h

@@ -0,0 +1 @@
+void setup();

regression/goto-instrument/nondet_static_exclude/test.desc

@@ -0,0 +1,18 @@
+CORE
+main_1.c main.c 
+--nondet-static --nondet-static-exclude test1 --nondet-static-exclude test3 --nondet-static-exclude test4 --nondet-static-exclude main_1.c:value
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+assertion test1 == (NULL|0): SUCCESS
+assertion test2.a == 5: FAILURE
+assertion test3.a == 1: SUCCESS
+assertion test3.b == 4: SUCCESS
+assertion test4->a == 1: SUCCESS
+assertion test4->b == 4: SUCCESS
+assertion test5->a == 5: FAILURE
+assertion test5->b == 2: FAILURE
+assertion value == 7: FAILURE
+assertion value == 5: SUCCESS
+--
+--

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1228,10 +1228,19 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // ignore default/user-specified initialization of variables with static
   // lifetime
-  if(cmdline.isset("nondet-static"))
+  if(cmdline.isset("nondet-static-exclude"))
   {
-    log.status() << "Adding nondeterministic initialization of static/global "
-                    "variables"
+    log.status() << "Adding nondeterministic initialization "
+                    "of static/global variables except for "
+                    "the specified ones."
+                 << messaget::eom;
+
+    nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
+  }
+  else if(cmdline.isset("nondet-static"))
+  {
+    log.status() << "Adding nondeterministic initialization "
+                    "of static/global variables"
                  << messaget::eom;
     nondet_static(goto_model);
   }
@@ -1631,6 +1640,8 @@ void goto_instrument_parse_optionst::help()
     " --isr <function>             instruments an interrupt service routine\n"
     " --mmio                       instruments memory-mapped I/O\n"
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
+    " --nondet-static-exclude e    same as nondet-static except for the variable e\n" //NOLINT(*)
+    "                              (use multiple times if required)\n"
     " --check-invariant function   instruments invariant checking function\n"
     " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
     " --splice-call caller,callee  prepends a call to callee in the body of caller\n"  // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -63,6 +63,7 @@ Author: Daniel Kroening, [email protected]
   "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \
+  "(nondet-static-exclude):" \
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \

src/goto-instrument/nondet_static.cpp

@@ -46,6 +46,12 @@ bool is_nondet_initializable_static(
 
   const symbolt &symbol = ns.lookup(id);
 
+  // is the symbol explicitly marked as not to be nondet initialized?
+  if(symbol.value.get_bool(ID_C_no_nondet_initialization))
+  {
+    return false;
+  }
+
   // is the type explicitly marked as not to be nondet initialized?
   if(symbol.type.get_bool(ID_C_no_nondet_initialization))
     return false;
@@ -110,24 +116,22 @@ void nondet_static(
         nondet_static(ns, goto_functions, fsym.get_identifier());
     }
   }
+
+  // update counters etc.
+  goto_functions.update();
 }
 
 /// Nondeterministically initializes global scope variables in
 /// CPROVER_initialize function.
 /// \param ns: Namespace for resolving type information.
 /// \param [out] goto_functions: Existing goto-functions to be updated.
-void nondet_static(
-  const namespacet &ns,
-  goto_functionst &goto_functions)
+void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
 {
   nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
-
-  // update counters etc.
-  goto_functions.update();
 }
 
-/// Main entry point of the module. Nondeterministically initializes global
-/// scope variables, except for constants (such as string literals, final
+/// First main entry point of the module. Nondeterministically initializes
+/// global scope variables, except for constants (such as string literals, final
 /// fields) and internal variables (such as CPROVER and symex variables,
 /// language specific internal variables).
 /// \param [out] goto_model: Existing goto-model to be updated.
@@ -136,3 +140,59 @@ void nondet_static(goto_modelt &goto_model)
   const namespacet ns(goto_model.symbol_table);
   nondet_static(ns, goto_model.goto_functions);
 }
+
+/// Second main entry point of the module. Nondeterministically initializes
+/// global scope variables, except for constants (such as string literals, final
+/// fields), internal variables (such as CPROVER and symex variables,
+/// language specific internal variables) and variables passed to except_value.
+/// \param [out] goto_model: Existing goto-model to be updated.
+/// \param except_values: list of symbol names that should not be updated.
+void nondet_static(
+  goto_modelt &goto_model,
+  const optionst::value_listt &except_values)
+{
+  const namespacet ns(goto_model.symbol_table);
+  std::set<std::string> to_exclude;
+
+  for(auto const &except : except_values)
+  {
+    const bool file_prefix_found = except.find(":") != std::string::npos;
+
+    if(file_prefix_found)
+    {
+      to_exclude.insert(except);
+      if(has_prefix(except, "./"))
+      {
+        to_exclude.insert(except.substr(2, except.length() - 2));
+      }
+      else
+      {
+        to_exclude.insert("./" + except);
+      }
+    }
+    else
+    {
+      irep_idt symbol_name(except);
+      symbolt lookup_results = ns.lookup(symbol_name);
+      to_exclude.insert(
+        id2string(lookup_results.location.get_file()) + ":" + except);
+    }
+  }
+
+  symbol_tablet &symbol_table = goto_model.symbol_table;
+
+  for(symbol_tablet::iteratort symbol_it = symbol_table.begin();
+      symbol_it != symbol_table.end();
+      symbol_it++)
+  {
+    symbolt &symbol = symbol_it.get_writeable_symbol();
+    std::string qualified_name = id2string(symbol.location.get_file()) + ":" +
+                                 id2string(symbol.display_name());
+    if(to_exclude.find(qualified_name) != to_exclude.end())
+    {
+      symbol.value.set(ID_C_no_nondet_initialization, 1);
+    }
+  }
+
+  nondet_static(ns, goto_model.goto_functions, INITIALIZE_FUNCTION);
+}

src/goto-instrument/nondet_static.h

@@ -20,6 +20,8 @@ Date: November 2011
 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
 #define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
 
+#include <util/options.h>
+
 class goto_modelt;
 class namespacet;
 class goto_functionst;
@@ -35,4 +37,6 @@ void nondet_static(
 
 void nondet_static(goto_modelt &);
 
+void nondet_static(goto_modelt &, const optionst::value_listt &);
+
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H