Add the method to cbmc

Author: zhixing-xu

regression/cbmc/Abstract-loops1/main.c

@@ -0,0 +1,23 @@
+#define ROW 10
+#define COL 10
+
+void main()
+{
+  int sum;
+  int image[ROW][COL];
+
+  // shrinkable
+  for(int j = 0; j < COL; j++)
+    image[0][j] = 0;
+
+  sum = 0;
+  // outer loop unshrinkable
+  // inner loop shrinkable
+  for(int i = 0; i < ROW; i++)
+  {
+    image[i][0] = 0;
+    sum = sum + i;
+    for(int j = 0; j < COL; j++)
+      image[sum][j] = 0;
+  }
+}

regression/cbmc/Abstract-loops1/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+ASSUME j < 10
+ASSUME j >= 0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loop with loop variable i is not shrinked (so it
+appears in unwinding). And loops with loop variable j are shrinked. It also
+checks the constraints to the loop variable is correctly applied. 

regression/cbmc/Abstract-loops2/main.c

@@ -0,0 +1,36 @@
+#define ROW 3
+#define COL 10
+
+void boo(int r)
+{
+  int val = 0;
+  int image[ROW][COL];;
+  // shrinkable, and set as shrink target
+  for(int j = 0; j < COL; j++)
+  {
+    int c = j + val;
+    image[r][c] = val;
+  }
+}
+
+
+void main()
+{
+  int r;
+  int buffer[ROW];
+  // not shrinkable since r is used in mem-safe assertion in boo()
+  // and r update itself in loop
+  for(int i = 0; i < ROW; i++)
+  {
+    r = r + i;
+    boo(r);
+    buffer[i];
+  }
+
+  // shrinkable
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(i);
+    buffer[i];
+  }
+}

regression/cbmc/Abstract-loops2/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops --abstractset boo.0,main.0 --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+ASSUME j < 10
+ASSUME j >= 0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrinked (so 
+they appears in unwinding). Although the second loop in main is shrinkable, but
+it's not in the target loop set provided by --abstractset, so it shouldn't be
+shrinked. 
+It also ensures the loop in boo() with loop variable j is shrinked and the 
+constraints are correctly applied. 

src/cbmc/Makefile

@@ -40,6 +40,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/abstract_loops$(OBJEXT) \
       ../goto-instrument/unwindset$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \

src/cbmc/cbmc_parse_options.cpp

@@ -69,6 +69,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>
+#include <goto-instrument/abstract_loops.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
 
@@ -159,6 +160,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("full-slice"))
     options.set_option("full-slice", true);
 
+  if(cmdline.isset("abstract-loops"))
+    options.set_option("abstract-loops", true);
+
+  if(cmdline.isset("abstractset"))
+    options.set_option("abstractset", cmdline.get_value("abstractset"));
+
   if(cmdline.isset("show-symex-strategies"))
   {
     status() << show_path_strategies() << eom;
@@ -892,6 +899,18 @@ bool cbmc_parse_optionst::process_goto_program(
         reachability_slicer(goto_model);
     }
 
+    if(options.get_bool_option("abstract-loops"))
+    {
+      // prevent other flag from messing up with location number
+      goto_model.goto_functions.update();
+      log.status() << "Abstracting loops" << eom;
+      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";
+      abstract_loops(goto_model, target_loop_map);
+    }
+
     // full slice?
     if(options.get_bool_option("full-slice"))
     {
@@ -990,6 +1009,8 @@ void cbmc_parse_optionst::help()
     HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     " --drop-unused-functions      drop functions trivially unreachable from main function\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"
     "\n"
     "Semantic transformations:\n"
     // NOLINTNEXTLINE(whitespace/line_length)

src/cbmc/cbmc_parse_options.h

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