Test for complexity limits

This test will fail if any of the features this relies upon has been
broken, but has the side-affect that if things ARE broken it'll take
a long time to fail. Not much to do about that, as this sort of
long-running symex-destroying code is what this feature is meant for.

Author: JohnDumbell

jbmc/regression/jbmc/symex_complexity/ComplexClass.class

@@ -0,0 +1,87 @@
+import java.util.*;
+
+public class ComplexClass {
+
+    public void loopBlacklist(List<String> prop, int increment, int size) {
+        while (size <= 1000)
+        {
+            if (size > 500)
+                branchCancel(prop, increment, size);
+
+            size++;
+        }
+    }
+
+    public void branchCancel(List<String> prop, int increment, int size) {
+        StringBuilder sb = new StringBuilder();
+        for (String str : prop)
+        {
+            if (size >= 50)
+                sb.append(str);
+
+            size+=increment;
+        }
+    }
+
+    private static Properties properties = new Properties();
+
+    public void process(Properties prop) {
+
+        properties = prop;
+
+        for (Enumeration<?> pe = properties.propertyNames(); pe.hasMoreElements(); )
+        {
+            String key = (String)pe.nextElement();
+            String value = recurse(key, properties.getProperty(key), 1);
+            if (value != null)
+            {
+                properties.setProperty(key, value);
+            }
+        }
+    }
+
+    private static String recurse(String key, String value, int level)
+    {
+        if (level > 9)
+            throw new IllegalArgumentException("Recursion level too deep.");
+
+        int from = 0;
+        StringBuffer result = null;
+        while (from < value.length()) {
+            while (from < value.length()) {
+                int start = value.indexOf("[", from);
+                if (start >= 0) {
+                    int end = value.indexOf(']', start);
+                    if (end < 0) {
+                        break;
+                    }
+                    String var = value.substring(start + 1, end);
+                    if (result == null) {
+                        result = new StringBuffer(value.substring(from, start));
+                    } else {
+                        result.append(value.substring(from, start));
+                    }
+                    if (properties.containsKey(var)) {
+                        String val = recurse(var, properties.getProperty(var), level + 1);
+                        if (val != null) {
+                            result.append(val);
+                            properties.setProperty(var, val);
+                        } else {
+                            result.append((properties.getProperty(var)).trim());
+                        }
+                    }
+
+                    from = end + 1;
+                } else {
+                    break;
+                }
+            }
+        }
+
+        if (result != null && from < value.length())
+        {
+            result.append(value.substring(from));
+        }
+        return (result == null) ? null : result.toString();
+    }
+}

jbmc/regression/jbmc/symex_complexity/ComplexClass.java

@@ -0,0 +1,19 @@
+CORE
+ComplexClass.class
+--function ComplexClass.branchCancel --symex-complexity-limit 1 --verbosity 9 --unwind 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^(\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Loop operations considered too complex)
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This tests that we cancel out of a loop with huge unwind and low complexity limit.
+
+The basis here is that the undeterministic incrementor and list mean that symex can't
+work out statically what's going on, and so both pieces of unknowability cause the
+guard to grow. Once that guard has reached a certain number, it'll be killed via
+the complexity module.
+
+If this is broken it means that the heuristics used to generate a 'complexity'
+measure of code is broken and will need to be re-written. See complexity_limitert
+for the main block of code.

jbmc/regression/jbmc/symex_complexity/branchCancel.desc

@@ -0,0 +1,13 @@
+CORE
+ComplexClass.class
+--function ComplexClass.loopBlacklist --symex-complexity-limit 1 --symex-complexity-failed-child-loops-limit 1 --verbosity 9 --unwind 9 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^(\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex)
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This tests that we cancel out of a loop with huge unwind, low complexity limit and low branch failure limit.
+
+Same basis as branchCancel with nondeterministic values, but in this case we have an
+outer loop that we're also running 100 times that will cause the inner to be blacklisted.

jbmc/regression/jbmc/symex_complexity/loopBlacklist.desc

@@ -0,0 +1,18 @@
+CORE
+ComplexClass.class
+--function ComplexClass.process --symex-complexity-limit 2 --verbosity 9 --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This tests that the complexity limits apply correctly and that each level of them are detected correctly:
+
+Branch cancelling.
+Loop cancelling.
+Loop blacklisting.
+
+When these don't work this test may take some time to run (and then fail), which is hard to
+restrict because this is the problem this feature is meant to solve. If this test is running
+slowly, high chance something has gone wrong.