Issue warnings when options may yield unsound verification results

Also warn about options that aren't unsound by design, but are
experimental in nature.

Author: NlightNFotis

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -187,25 +187,54 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option(
       "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
+    log.warning() << "**** WARNING: Complexity-limited analysis may yield "
+                     "unsound verification results"
+                  << messaget::eom;
   }
 
   if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
   {
     options.set_option(
       "symex-complexity-failed-child-loops-limit",
       cmdline.get_value("symex-complexity-failed-child-loops-limit"));
+    if(!cmdline.isset("symex-complexity-limit"))
+    {
+      log.warning() << "**** WARNING: Complexity-limited analysis may yield "
+                       "unsound verification results"
+                    << messaget::eom;
+    }
   }
 
   if(cmdline.isset("unwind"))
+  {
     options.set_option("unwind", cmdline.get_value("unwind"));
+    if(!cmdline.isset("unwinding-assertions"))
+    {
+      log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
+                       "sound verification results"
+                    << messaget::eom;
+    }
+  }
 
   if(cmdline.isset("depth"))
+  {
     options.set_option("depth", cmdline.get_value("depth"));
+    log.warning()
+      << "**** WARNING: Depth-bounded analysis may yield unsound verification "
+         "results"
+      << messaget::eom;
+  }
 
   if(cmdline.isset("unwindset"))
   {
     options.set_option(
       "unwindset", cmdline.get_comma_separated_values("unwindset"));
+    if(!cmdline.isset("unwinding-assertions"))
+    {
+      log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
+                       "sound verification results"
+                    << messaget::eom;
+    }
   }
 
   // constant propagation
@@ -234,9 +263,13 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("unwinding-assertions", true);
 
   // generate unwinding assumptions otherwise
-  options.set_option(
-    "partial-loops",
-    cmdline.isset("partial-loops"));
+  if(cmdline.isset("partial-loops"))
+  {
+    options.set_option("partial-loops", true);
+    log.warning()
+      << "**** WARNING: --partial-loops may yield unsound verification results"
+      << messaget::eom;
+  }
 
   // remove unused equations
   options.set_option(
@@ -858,6 +891,10 @@ bool jbmc_parse_optionst::process_goto_functions(
   // full slice?
   if(cmdline.isset("full-slice"))
   {
+    log.warning() << "**** WARNING: Experimental option --full-slice, "
+                  << "analysis results may be unsound. See "
+                  << "https://github.com/diffblue/cbmc/issues/260"
+                  << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
       property_slicer(goto_model, cmdline.get_values("property"));

src/cbmc/cbmc_parse_options.cpp

@@ -193,13 +193,26 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("mm", cmdline.get_value("mm"));
 
   if(cmdline.isset("symex-complexity-limit"))
+  {
     options.set_option(
       "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
+    log.warning() << "**** WARNING: Complexity-limited analysis may yield "
+                     "unsound verification results"
+                  << messaget::eom;
+  }
 
   if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
+  {
     options.set_option(
       "symex-complexity-failed-child-loops-limit",
       cmdline.get_value("symex-complexity-failed-child-loops-limit"));
+    if(!cmdline.isset("symex-complexity-limit"))
+    {
+      log.warning() << "**** WARNING: Complexity-limited analysis may yield "
+                       "unsound verification results"
+                    << messaget::eom;
+    }
+  }
 
   if(cmdline.isset("property"))
     options.set_option("property", cmdline.get_values("property"));
@@ -243,10 +256,24 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("localize-faults", true);
 
   if(cmdline.isset("unwind"))
+  {
     options.set_option("unwind", cmdline.get_value("unwind"));
+    if(!cmdline.isset("unwinding-assertions"))
+    {
+      log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
+                       "sound verification results"
+                    << messaget::eom;
+    }
+  }
 
   if(cmdline.isset("depth"))
+  {
     options.set_option("depth", cmdline.get_value("depth"));
+    log.warning()
+      << "**** WARNING: Depth-bounded analysis may yield unsound verification "
+         "results"
+      << messaget::eom;
+  }
 
   if(cmdline.isset("slice-by-trace"))
   {
@@ -258,6 +285,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option(
       "unwindset", cmdline.get_comma_separated_values("unwindset"));
+    if(!cmdline.isset("unwinding-assertions"))
+    {
+      log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
+                       "sound verification results"
+                    << messaget::eom;
+    }
   }
 
   // constant propagation
@@ -280,7 +313,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   if(cmdline.isset("partial-loops"))
+  {
     options.set_option("partial-loops", true);
+    log.warning()
+      << "**** WARNING: --partial-loops may yield unsound verification results"
+      << messaget::eom;
+  }
 
   // remove unused equations
   if(cmdline.isset("slice-formula"))
@@ -840,6 +878,10 @@ bool cbmc_parse_optionst::process_goto_program(
   // full slice?
   if(options.get_bool_option("full-slice"))
   {
+    log.warning() << "**** WARNING: Experimental option --full-slice, "
+                  << "analysis results may be unsound. See "
+                  << "https://github.com/diffblue/cbmc/issues/260"
+                  << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(options.is_set("property"))
       property_slicer(goto_model, options.get_list_option("property"));

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1742,6 +1742,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     do_indirect_call_and_rtti_removal();
     do_remove_returns();
 
+    log.warning() << "**** WARNING: Experimental option --full-slice, "
+                  << "analysis results may be unsound. See "
+                  << "https://github.com/diffblue/cbmc/issues/260"
+                  << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
       property_slicer(goto_model, cmdline.get_values("property"));