Merge pull request #4958 from JohnDumbell/jd/feature/symex_complexity

Symex complexity heuristic

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.

jbmc/regression/jbmc/symex_complexity/process.desc

@@ -197,6 +197,19 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("localize-faults"))
     options.set_option("localize-faults", true);
 
+  if(cmdline.isset("symex-complexity-limit"))
+  {
+    options.set_option(
+      "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
+  }
+
+  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
+  {
+    options.set_option(
+      "symex-complexity-failed-child-loops-limit",
+      cmdline.get_value("symex-complexity-failed-child-loops-limit"));
+  }
+
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -61,9 +61,9 @@ Author: Diffblue Ltd
 ///   * [function] get_target() which returns an object that needs:
 ///     * [field] location_number which is an unsigned int.
 template <class P, class T>
-class lexical_loops_templatet : public loop_analysist<P, T>
+class lexical_loops_templatet : public loop_analysist<T>
 {
-  typedef loop_analysist<P, T> parentt;
+  typedef loop_analysist<T> parentt;
 
 public:
   typedef typename parentt::loopt lexical_loopt;
@@ -92,11 +92,13 @@ class lexical_loops_templatet : public loop_analysist<P, T>
       out << "Note not all loops were in lexical loop form\n";
   }
 
+  virtual ~lexical_loops_templatet() = default;
+
 protected:
   void compute(P &program);
   bool compute_lexical_loop(T, T);
 
-  bool all_in_lexical_loop_form;
+  bool all_in_lexical_loop_form = false;
 };
 
 typedef lexical_loops_templatet<
@@ -178,7 +180,7 @@ bool lexical_loops_templatet<P, T>::compute_lexical_loop(
   }
 
   auto insert_result = parentt::loop_map.emplace(
-    loop_head, lexical_loopt{*this, std::move(loop_instructions)});
+    loop_head, lexical_loopt{std::move(loop_instructions)});
 
   // If this isn't a new loop head (i.e. return_result.second is false) then we
   // have multiple backedges targeting one loop header: this is not in simple

src/analyses/lexical_loops.h

@@ -13,47 +13,33 @@ Author: Diffblue Ltd
 #ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
 #define CPROVER_ANALYSES_LOOP_ANALYSIS_H
 
-template <class P, class T>
+#include <memory>
+
+template <class T>
 class loop_analysist;
 
 /// A loop, specified as a set of instructions
-template <class P, class T>
+template <class T>
 class loop_templatet
 {
-  typedef loop_analysist<P, T> parent_analysist;
   typedef std::set<T> loop_instructionst;
   loop_instructionst loop_instructions;
 
-  friend loop_analysist<P, T>;
+  friend loop_analysist<T>;
 
 public:
-  explicit loop_templatet(parent_analysist &loop_analysis)
-    : loop_analysis(loop_analysis)
-  {
-  }
+  loop_templatet() = default;
 
   template <typename InstructionSet>
-  loop_templatet(parent_analysist &loop_analysis, InstructionSet &&instructions)
-    : loop_instructions(std::forward<InstructionSet>(instructions)),
-      loop_analysis(loop_analysis)
+  explicit loop_templatet(InstructionSet &&instructions)
+    : loop_instructions(std::forward<InstructionSet>(instructions))
   {
   }
 
   /// Returns true if \p instruction is in this loop
-  bool contains(const T instruction) const
-  {
-    return loop_analysis.loop_contains(*this, instruction);
-  }
-
-  /// Get the \ref parent_analysist analysis this loop relates to
-  const parent_analysist &get_loop_analysis() const
-  {
-    return loop_analysis;
-  }
-  /// Get the \ref parent_analysist analysis this loop relates to
-  parent_analysist &get_loop_analysis()
+  bool virtual contains(const T instruction) const
   {
-    return loop_analysis;
+    return !loop_instructions.empty() && loop_instructions.count(instruction);
   }
 
   // NOLINTNEXTLINE(readability/identifiers)
@@ -83,58 +69,105 @@ class loop_templatet
     return loop_instructions.empty();
   }
 
-  /// Adds \p instruction to this loop. The caller must verify that the added
-  /// instruction does not alter loop structure; if it does they must discard
-  /// and recompute the related \ref parent_analysist instance.
+  /// Adds \p instruction to this loop.
   /// \return true if the instruction is new
   bool insert_instruction(const T instruction)
   {
     return loop_instructions.insert(instruction).second;
   }
-
-private:
-  parent_analysist &loop_analysis;
 };
 
-template <class P, class T>
+template <class T>
 class loop_analysist
 {
 public:
-  typedef loop_templatet<P, T> loopt;
+  typedef loop_templatet<T> loopt;
   // map loop headers to loops
   typedef std::map<T, loopt> loop_mapt;
 
   loop_mapt loop_map;
 
-  void output(std::ostream &) const;
+  virtual void output(std::ostream &) const;
+
+  /// Returns true if \p instruction is the header of any loop
+  bool is_loop_header(const T instruction) const
+  {
+    return loop_map.count(instruction);
+  }
+
+  loop_analysist() = default;
+};
+
+template <typename T>
+class loop_with_parent_analysis_templatet : loop_templatet<T>
+{
+  typedef loop_analysist<T> parent_analysist;
+
+public:
+  explicit loop_with_parent_analysis_templatet(parent_analysist &loop_analysis)
+    : loop_analysis(loop_analysis)
+  {
+  }
+
+  template <typename InstructionSet>
+  explicit loop_with_parent_analysis_templatet(
+    parent_analysist &loop_analysis,
+    InstructionSet &&instructions)
+    : loop_templatet<T>(std::forward<InstructionSet>(instructions)),
+      loop_analysis(loop_analysis)
+  {
+  }
 
   /// Returns true if \p instruction is in \p loop
-  bool loop_contains(const loopt &loop, const T instruction) const
+  bool loop_contains(
+    const typename loop_analysist<T>::loopt &loop,
+    const T instruction) const
   {
     return loop.loop_instructions.count(instruction);
   }
 
-  /// Returns true if \p instruction is the header of any loop
-  bool is_loop_header(const T instruction) const
+  /// Get the \ref parent_analysist analysis this loop relates to
+  const parent_analysist &get_loop_analysis() const
   {
-    return loop_map.count(instruction);
+    return loop_analysis;
+  }
+  /// Get the \ref parent_analysist analysis this loop relates to
+  parent_analysist &get_loop_analysis()
+  {
+    return loop_analysis;
   }
 
-  loop_analysist() = default;
+private:
+  parent_analysist &loop_analysis;
+};
+
+template <class T>
+class linked_loop_analysist : loop_analysist<T>
+{
+public:
+  linked_loop_analysist() = default;
+
+  /// Returns true if \p instruction is in \p loop
+  bool loop_contains(
+    const typename loop_analysist<T>::loopt &loop,
+    const T instruction) const
+  {
+    return loop.loop_instructions.count(instruction);
+  }
 
   // The loop structures stored in `loop_map` contain back-pointers to this
   // class, so we forbid copying or moving the analysis struct. If this becomes
   // necessary then either add a layer of indirection or update the loop_map
   // back-pointers on copy/move.
-  loop_analysist(const loop_analysist &) = delete;
-  loop_analysist(loop_analysist &&) = delete;
-  loop_analysist &operator=(const loop_analysist &) = delete;
-  loop_analysist &operator=(loop_analysist &&) = delete;
+  linked_loop_analysist(const linked_loop_analysist &) = delete;
+  linked_loop_analysist(linked_loop_analysist &&) = delete;
+  linked_loop_analysist &operator=(const linked_loop_analysist &) = delete;
+  linked_loop_analysist &operator=(linked_loop_analysist &&) = delete;
 };
 
 /// Print all natural loops that were found
-template <class P, class T>
-void loop_analysist<P, T>::output(std::ostream &out) const
+template <class T>
+void loop_analysist<T>::output(std::ostream &out) const
 {
   for(const auto &loop : loop_map)
   {