Add utility to compute check if strings are within certain edit distance

For now only basic levenshtein distance (delete,insert,modify).  This is
probably good enough for the intended use case (suggesting typo fixes on
the command line).

Author: hannes-steffenhagen-diffblue

src/util/Makefile

@@ -11,6 +11,7 @@ SRC = allocate_objects.cpp \
       cout_message.cpp \
       dstring.cpp \
       endianness_map.cpp \
+      edit_distance.cpp \
       expr.cpp \
       expr_initializer.cpp \
       expr_util.cpp \

src/util/edit_distance.cpp

@@ -0,0 +1,73 @@
+/// \file
+/// \author Diffblue Ltd.
+///
+/// Provides a way to compute edit distance between two strings
+
+#include "edit_distance.h"
+
+levenshtein_automatont::levenshtein_automatont(
+  const std::string &string,
+  std::size_t allowed_errors)
+{
+  const std::size_t layer_offset = string.size() + 1;
+  for(std::size_t i = 0; i <= allowed_errors; ++i)
+  {
+    final_states.push_back(string.size() + layer_offset * i);
+  }
+  for(std::size_t string_index = 0; string_index < string.size();
+      ++string_index)
+  {
+    for(std::size_t error_layer = 0; error_layer <= allowed_errors;
+        ++error_layer)
+    {
+      // position string_index matches
+      nfa.add_transition(
+        error_layer * layer_offset + string_index,
+        string[string_index],
+        error_layer * layer_offset + string_index + 1);
+      if(error_layer < allowed_errors)
+      {
+        // insertion, swap or deletion
+        nfa.add_arbitrary_transition(
+          error_layer * layer_offset + string_index,
+          (error_layer + 1) * layer_offset + string_index);
+        nfa.add_epsilon_transition(
+          error_layer * layer_offset + string_index,
+          (error_layer + 1) * layer_offset + string_index + 1);
+        nfa.add_arbitrary_transition(
+          error_layer * layer_offset + string_index,
+          (error_layer + 1) * layer_offset + string_index + 1);
+      }
+    }
+  }
+  for(std::size_t error_layer = 0; error_layer < allowed_errors; ++error_layer)
+  {
+    // arbitrary transitions between error layers
+    nfa.add_arbitrary_transition(
+      error_layer * layer_offset + string.size(),
+      (error_layer + 1) * layer_offset + string.size());
+  }
+}
+
+bool levenshtein_automatont::matches(const std::string &string) const
+{
+  return get_edit_distance(string).has_value();
+}
+
+optionalt<std::size_t>
+levenshtein_automatont::get_edit_distance(const std::string &string) const
+{
+  auto current = nfa.initial_state(0);
+  for(const auto c : string)
+  {
+    current = nfa.next_state(current, c);
+  }
+  for(std::size_t distance = 0; distance < final_states.size(); ++distance)
+  {
+    if(current.contains(final_states[distance]))
+    {
+      return distance;
+    }
+  }
+  return nullopt;
+}

src/util/edit_distance.h

@@ -0,0 +1,46 @@
+/// \file
+/// \author Diffblue Ltd.
+///
+/// Loosely based on this blog post:
+///   http://blog.notdot.net/2010/07/Damn-Cool-Algorithms-Levenshtein-Automata
+/// Provides a way to compute edit distance between two strings
+///
+/// No conversion to DFA or other optimisations are done here because for our
+/// use case (i.e. suggestions for errors in command line specifications) this
+/// is fast enough without them.
+
+#ifndef CPROVER_UTIL_EDIT_DISTANCE_H
+#define CPROVER_UTIL_EDIT_DISTANCE_H
+
+#include "nfa.h"
+
+#include <cstddef>
+#include <string>
+
+#include <util/optional.h>
+
+/// Simple automaton that can detect whether a string can be transformed into
+/// another with a limited number of deletions, insertions or substitutions.
+/// Not a very fast implementation, but should be good enough for small strings.
+struct levenshtein_automatont
+{
+private:
+  nfat<char> nfa;
+  using state_labelt = nfat<char>::state_labelt;
+  std::vector<state_labelt> final_states;
+
+public:
+  levenshtein_automatont(
+    const std::string &string,
+    std::size_t allowed_errors = 2);
+
+  bool matches(const std::string &string) const;
+  optionalt<std::size_t> get_edit_distance(const std::string &string) const;
+
+  void dump_automaton_dot_to(std::ostream &out)
+  {
+    nfa.dump_automaton_dot_to(out);
+  };
+};
+
+#endif // CPROVER_UTIL_EDIT_DISTANCE_H

src/util/nfa.h

@@ -0,0 +1,167 @@
+/// \file
+/// \author Diffblue Ltd.
+///
+/// A simple NFA implementation
+
+#ifndef CPROVER_UTIL_NFA_H
+#define CPROVER_UTIL_NFA_H
+
+#include <algorithm>
+#include <cstddef>
+#include <fstream>
+#include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+/// Very simple NFA implementation
+/// Not super performant, but should be good enough for our purposes
+template <typename T>
+struct nfat
+{
+  using state_labelt = std::size_t;
+  /// A state is a set of possibly active transitions.
+  /// The automaton itself is stateless, it just contains
+  /// the state transitions.
+  struct statet
+  {
+  private:
+    std::unordered_set<state_labelt> possible_states;
+
+  public:
+    friend struct nfat;
+
+    bool contains(state_labelt state_label) const
+    {
+      return possible_states.count(state_label) != 0;
+    }
+  };
+
+  nfat() = default;
+
+  /// Add a transition from "from" to "to" exactly when "when" is consumed
+  void add_transition(state_labelt from, T when, state_labelt to)
+  {
+    resize_if_necessary(from, to);
+    transitions[from].when[when].insert(to);
+  }
+
+  /// Add a transition from "from" to "to" when any input is consumed
+  /// This is handled a special case so not all inputs need to be enumerated
+  /// for arbitrary transitions
+  void add_arbitrary_transition(state_labelt from, state_labelt to)
+  {
+    resize_if_necessary(from, to);
+    transitions[from].arbitrary.insert(to);
+  }
+
+  /// Add a transition from "from" to "to" that doesn’t consume input
+  void add_epsilon_transition(state_labelt from, state_labelt to)
+  {
+    resize_if_necessary(from, to);
+    transitions[from].epsilon.insert(to);
+  }
+
+  statet initial_state(state_labelt initial) const
+  {
+    statet result{};
+    result.possible_states.insert(initial);
+    follow_epsilon_transitions(result);
+    return result;
+  }
+
+  statet next_state(const statet &current, const T &input) const
+  {
+    statet new_state{};
+    for(const auto label : current.possible_states)
+    {
+      const auto &transition = transitions[label];
+      const auto it = transition.when.find(input);
+      if(it != transition.when.end())
+      {
+        for(const auto result_state : it->second)
+        {
+          new_state.possible_states.insert(result_state);
+        }
+      }
+      for(const auto result_state : transition.arbitrary)
+      {
+        new_state.possible_states.insert(result_state);
+      }
+    }
+    follow_epsilon_transitions(new_state);
+    return new_state;
+  }
+
+  /// Write the automaton structure to out in graphviz dot format.
+  /// Meant for debugging.
+  void dump_automaton_dot_to(std::ostream &out) const
+  {
+    out << "digraph {\n";
+    for(state_labelt from = 0; from < transitions.size(); ++from)
+    {
+      for(const auto to : transitions[from].arbitrary)
+      {
+        out << 'S' << from << " -> S" << to << "[label=\"*\"]\n";
+      }
+      for(const auto to : transitions[from].epsilon)
+      {
+        out << 'S' << from << " -> S" << to << u8"[label=\"ε\"]\n";
+      }
+      for(const auto &pair : transitions[from].when)
+      {
+        const auto &in = pair.first;
+        const auto &tos = pair.second;
+        for(const auto to : tos)
+        {
+          out << 'S' << from << " -> S" << to << "[label=\"(" << in << ")\"]\n";
+        }
+      }
+    }
+    out << "}\n";
+  }
+
+private:
+  void resize_if_necessary(state_labelt from, state_labelt to)
+  {
+    const auto min_size = std::max(from, to) + 1;
+    if(transitions.size() < min_size)
+    {
+      transitions.resize(min_size);
+    }
+  }
+
+  void follow_epsilon_transitions(statet &state) const
+  {
+    std::vector<state_labelt> new_states{};
+    do
+    {
+      new_states.clear();
+      for(const auto from : state.possible_states)
+      {
+        for(const auto to : transitions[from].epsilon)
+        {
+          if(!state.contains(to))
+          {
+            new_states.push_back(to);
+          }
+        }
+      }
+      std::copy(
+        new_states.begin(),
+        new_states.end(),
+        std::inserter(state.possible_states, state.possible_states.end()));
+    } while(!new_states.empty());
+  }
+
+  struct transitiont
+  {
+    std::unordered_set<state_labelt> epsilon;
+    std::unordered_set<state_labelt> arbitrary;
+    std::unordered_map<T, std::unordered_set<state_labelt>> when;
+  };
+
+  std::vector<transitiont> transitions;
+};
+
+#endif // CPROVER_UTIL_NFA_H

unit/Makefile

@@ -73,6 +73,7 @@ SRC += analyses/ai/ai.cpp \
        util/allocate_objects.cpp \
        util/cmdline.cpp \
        util/dense_integer_map.cpp \
+       util/edit_distance.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr.cpp \
        util/expr_iterator.cpp \