clean up parser options, set regression test3 as KNOWNBUG

Author: zhixing-xu

regression/cbmc/Abstract-loops3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --bounds-check --pointer-check --abstract-loops --abstractset main.0
 ^EXIT=10$

regression/goto-instrument/abstract-loops3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --bounds-check --pointer-check --add-library --abstract-loops --abstractset main.0
 ^EXIT=10$

src/cbmc/cbmc_parse_options.cpp

@@ -835,7 +835,7 @@ bool cbmc_parse_optionst::process_goto_program(
       loop_mapt target_loop_map;
       if(options.is_set("abstractset"))
         if(parse_absloopset(options.get_option("abstractset"), target_loop_map))
-          throw "Cannot understand input loop";
+          throw "cannot understand input loop";
       abstract_loops(goto_model, target_loop_map);
     }
 
@@ -960,8 +960,8 @@ void cbmc_parse_optionst::help()
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
-    " --abstract-loops             shrink loop into single iter if the assertions are based on single iter (experimental)\n"
-    " --abstractset L,...          only shrink loop L, shrink every loop if the flag is not given\n"
+    " --abstract-loops             shrink loop based on assertion dependency (experimental)\n"
+    " --abstractset L,...          only shrink loop L,...\n"
     "\n"
     "Semantic transformations:\n"
     // NOLINTNEXTLINE(whitespace/line_length)

src/cbmc/cbmc_parse_options.h

@@ -35,7 +35,8 @@ class optionst;
   OPT_BMC \
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
-  "(no-simplify)(full-slice)(abstract-loops)(abstractset):" \
+  "(no-simplify)(full-slice)" \
+  "(abstract-loops)(abstractset):"\
   OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \

src/goto-instrument/abstract_loops.cpp

@@ -54,9 +54,6 @@ class abstract_loopst
 protected:
   // target abstract loop number for each function
   loop_mapt target_loop_map;
-  // set of all leaf dependency nodes for loop variables
-  //nodeset leaf_nodes;
-  //nodeset update_nodes;
   // current function
   irep_idt fn;
   // map from instruction line # to the set of loops it belongs to
@@ -119,7 +116,7 @@ class abstract_loopst
   }
 
   /// Check if a node has self-cycle in data dependency
-  /// Inefficient method, will get updated
+  /// Inefficient method, should get updated
   /// \param target: node location
   /// \param dep_graph: dependency graph for the program
   bool is_in_cycle(unsigned target, const dependence_grapht &dep_graph)
@@ -273,7 +270,6 @@ void abstract_loopst::update_shrinkability(unsigned loc, irep_idt func)
 {
   for(auto loop_n: insloop_map[loc])
   {
-    //irep_idt func = dep_graph[loc].PC->function;
     abstract_loopt *loop_info = &(absloop_map[func].find(loop_n)->second);
     loop_info->shrinkable = false;
 #ifdef DEBUG_ABSTRACT_LOOPS
@@ -328,8 +324,6 @@ void abstract_loopst::check_assertion(unsigned location,
           it != data_deps.end(); ++it)
       {
         add_to_queue(dep_set, dep_queue, (*it)->location_number);
-        //if(is_in_cycle(node, dep_graph))
-          //update_set.insert(node);
         if(ctrl_set.find(node) == ctrl_set.end())
           update_set.insert(node);
       }
@@ -570,9 +564,6 @@ void abstract_loopst::get_loop_info(
     insloop_map[n].insert(last->loop_number);
 
   absloop_map[fn].insert(loopnum_pair(last->loop_number, loop_info));
-  //leaf_nodes.insert(loop_info.var_leaves.begin(), loop_info.var_leaves.end());
-  //update_nodes.insert(loop_info.var_updates.begin(),
-      //loop_info.var_updates.end());
 }
 
 /// Main function for abstraction, has 3 iterations to

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1604,8 +1604,8 @@ void goto_instrument_parse_optionst::help()
     " --havoc-loops                over-approximate all loops\n"
     " --accelerate                 add loop accelerators\n"
     " --skip-loops <loop-ids>      add gotos to skip selected loops during execution\n" // NOLINT(*)
-    " --abstract-loops             shrink loop into single iter if the assertions are based on single iter\n"
-    " --abstractset L,...          only shrink loop L, shrink every loop if the flag is not given\n"
+    " --abstract-loops             shrink loop based on assertion dependency (experimental)\n"
+    " --abstractset L,...          only shrink loop L,...\n"
     "\n"
     "Memory model instrumentations:\n"
     " --mm <tso,pso,rmo,power>     instruments a weak memory model\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -79,7 +79,8 @@ Author: Daniel Kroening, [email protected]
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
   "(cav11)" \
   OPT_TIMESTAMP \
-  "(show-natural-loops)(accelerate)(havoc-loops)(abstract-loops)(abstractset):" \
+  "(show-natural-loops)(accelerate)(havoc-loops)" \
+  "(abstract-loops)(abstractset):" \
   "(error-label):(string-abstraction)" \
   "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
   "(accelerate)(constant-propagator)" \