WIP

regression/goto-analyzer/unwind-bound-analysis/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+/*
+ ./goto-analyzer/goto-analyzer ../regression/goto-analyzer/unwind-bound-analysis/main.c --verify --vsd --loop-unwind 258 --recursive-interprocedural --vsd-arrays every-element --vsd-array-max-elements 18 --one-domain-per-history --vsd-values intervals --verbosity 10 | grep -v __CPROVER_ | less
+
+bugs
+- still got a problem with argv
+- when the first branch is not taken, the domain is not pruned enough
+- somehow when the paths exit the interval is off-by-one
+
+*/
+
+#define BUFFERLENGTH 16
+
+int main ()
+{
+  int n;
+  __CPROVER_assume(n < BUFFERLENGTH);
+  int array[BUFFERLENGTH];
+
+  for (int i = 0; i < n; ++i) {
+    array[i] = 0;
+  }
+
+  for (int i = 0; i < n; ++i) {
+    assert(array[i] == 0);
+  }
+
+  return 0;
+}

src/goto-analyzer/unwinding_bounds.cpp

@@ -0,0 +1,13 @@
+/*
+ * 1. Iterate over all functions
+ * 2. Iterate over all instructions
+ * 3. Find back-edges (well, ideally, use the loop finder to find loop
+ * back edges)
+ * 4. goto_program::loop_id(function_id, instruction)
+ * 5. Iterate over the histories, find the max number of consequetive
+ * times this is visited -- but is it that because of nested loops and
+ * if statements in loops
+ *
+ * Not clear where to store information, an unwindsett?
+ */
+

src/goto-analyzer/unwinding_bounds.h

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: goto-analyzer
+
+Author: Martin Brain, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_ANALYZER_UNWINDING_BOUNDS_H
+#define CPROVER_GOTO_ANALYZER_UNWINDING_BOUNDS_H
+
+#include <iosfwd>
+
+class ai_baset;
+class goto_modelt;
+class message_handlert;
+class optionst;
+
+/// Computes, where possible, upper bounds on the number of
+/// unwinding iterations required to fully unwind a loop.
+/// Depending on how the abstract domain is configured
+/// this may find loop bounds that CBMC constant-propagation
+/// unwinder doesn't find
+bool unwinding_bounds(
+  goto_modelt &,
+  const ai_baset &,
+  const optionst &,
+  message_handlert &,
+  std::ostream &);
+
+#endif // CPROVER_GOTO_ANALYZER_UNWINDING_BOUNDS_H