Loop abstraction [depends-on: #2707]

jbmc/unit/Makefile

@@ -126,6 +126,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
+              $(CPROVER_DIR)/src/goto-instrument/abstract_loops$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
               $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \

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 shrunk (so it
+appears in unwinding). Loops with loop variable j are shrunk. The test also
+checks the constraints to the loop variable are 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,17 @@
+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 shrunk (so they
+appear in unwinding). Although the second loop in main is shrinkable, it is not
+in the target loop set provided by --abstractset, thus it shouldn't be shrunk.
+The test also ensures the loop in boo() with loop variable j is shrunk and the
+constraints are correctly applied.

regression/cbmc/abstract-loops3/main.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+#define ROW 10
+
+void boo(int *x)
+{
+  *x = *x + 1;
+}
+
+void main()
+{
+  int *x = (int *)malloc(sizeof(int));
+  int buffer[ROW];
+  *x = 2;
+  // not shrinkable since x has a self-update in boo()
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(x);
+    buffer[*x] = 1;
+  }
+}

regression/cbmc/abstract-loops3/test.desc

@@ -0,0 +1,17 @@
+KNOWNBUG
+main.c
+--bounds-check --pointer-check --abstract-loops --abstractset main.0
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrunk (so they
+appear in unwinding), even when the instruction that makes the loop unshrinkable
+is in another function.
+
+Requires #2646, #2694 to work.

regression/goto-analyzer/dependence-graph13/main.c

@@ -0,0 +1,12 @@
+void bar(int a, int b)
+{
+  int result = b;
+}
+
+void main()
+{
+  int a = 1;
+  int b = 2;
+  int c = 3;
+  bar(a, b + c);
+}

regression/goto-analyzer/dependence-graph13/test.desc

@@ -0,0 +1,26 @@
+CORE
+main.c
+--dependence-graph --show
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+\/\/ ([0-9]+).*\n.*b = 2;(.*\n)*Data dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*result = b
+\/\/ ([0-9]+).*\n.*c = 3;(.*\n)*Data dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*result = b
+--
+^warning: ignoring
+--
+
+The two regular expressions above match output portions like shown below (with
+<N> being a location number). The intention is to check whether a function
+parameter in the callee correctly depends on the caller-provided argument.
+
+      // 3 file main.c line 11 function main
+        b = 2;
+...
+**** 12 file main.c line 5 function bar
+Data dependencies: (<N>,...)|(...,<N>)
+
+        // 12 file main.c line 5 function bar
+        result = b;
+
+The second regex matches for c.

regression/goto-instrument/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/goto-instrument/abstract-loops1/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+ASSUME j < 10
+ASSUME j >= 0
+--
+main\.1
+main\.2
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loop with loop variable i is not shrunk (so it
+appears in unwinding). Loops with loop variable j are shrunk. The test also
+checks the constraints to the loop variable are correctly applied.

regression/goto-instrument/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/goto-instrument/abstract-loops2/test.desc

@@ -0,0 +1,21 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops --abstractset boo.0,main.0
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+main\.1
+ASSUME j < 10
+ASSUME j >= 0
+--
+boo\.0
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrunk (so they
+appear in unwinding). Although the second loop in main is shrinkable, it is not
+in the target loop set provided by --abstractset, thus it shouldn't be shrunk.
+The test also ensures the loop in boo() with loop variable j is shrunk and the
+constraints are correctly applied.

regression/goto-instrument/abstract-loops3/main.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+#define ROW 10
+
+void boo(int *x)
+{
+  *x = *x + 1;
+}
+
+void main()
+{
+  int *x = (int *)malloc(sizeof(int));
+  int buffer[ROW];
+  *x = 2;
+  // not shrinkable since x has a self-update in boo()
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(x);
+    buffer[*x] = 1;
+  }
+}

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

@@ -0,0 +1,17 @@
+KNOWNBUG
+main.c
+--bounds-check --pointer-check --add-library --abstract-loops --abstractset main.0
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrunk (so they
+appear in unwinding), even when the instruction that makes the loop unshrinkable
+is in another function.
+
+Requires #2646, #2694 to work.

src/analyses/dependence_graph.cpp

@@ -238,6 +238,16 @@ void dep_graph_domaint::transform(
   data_dependencies(from, function_to, to, *dep_graph, ns);
 }
 
+dep_graph_domaint::depst dep_graph_domaint::get_data_deps() const
+{
+  return data_deps;
+}
+
+dep_graph_domaint::depst dep_graph_domaint::get_control_deps() const
+{
+  return control_deps;
+}
+
 void dep_graph_domaint::output(
   std::ostream &out,
   const ai_baset &,

src/analyses/dependence_graph.h

@@ -93,6 +93,10 @@ class dep_graph_domaint:public ai_domain_baset
     const ai_baset &ai,
     const namespacet &ns) const final override;
 
+  typedef std::set<goto_programt::const_targett> depst;
+  depst get_data_deps() const;
+  depst get_control_deps() const;
+
   jsont output_json(
     const ai_baset &ai,
     const namespacet &ns) const override;
@@ -182,7 +186,6 @@ class dep_graph_domaint:public ai_domain_baset
   node_indext node_id;
   bool has_changed;
 
-  typedef std::set<goto_programt::const_targett> depst;
 
   // Set of locations with control instructions on which the instruction at this
   // location has a control dependency on

src/analyses/goto_rw.cpp

@@ -493,6 +493,23 @@ void rw_range_sett::add(
 
   static_cast<range_domaint&>(*entry->second).push_back(
     {range_start, range_end});
+
+  // add to the single expression read set
+  if(mode == get_modet::READ && expr_r_range_set.has_value())
+  {
+    objectst::iterator expr_entry =
+      expr_r_range_set
+        ->insert(
+          std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
+            identifier, nullptr))
+        .first;
+
+    if(expr_entry->second == nullptr)
+      expr_entry->second = util_make_unique<range_domaint>();
+
+    static_cast<range_domaint &>(*expr_entry->second)
+      .push_back({range_start, range_end});
+  }
 }
 
 void rw_range_sett::get_objects_rec(