Merge pull request boogie-org#11 from atomb/better-loop-extract

Extracted loop procedure parameters are a subset of the containing implementation’s in/out parameters and local variables. During extraction, the order of parameters are determined by the name of those variables. This is brittle, because local variable names can differ between translations, therefore ordering them on both sides by name might not lead to a correct alignment. It is also possible that one of the parameters does not exist on the other side, which is easier to detect.

This PR adds a heuristic that tries to compute a mapping of variables using structurally equivalent blocks of the implementation.

The blocks are sorted by the number of commands they have and the heuristic attempts to find structurally equivalent blocks starting from the ones with the most commands (which are more likely to be actually equivalent blocks). The mapping is unchanged on conflicts. It might be that some variables that will become the parameters of the extracted procedure are left unmapped, those variables are ordered by name as before.
Other changes

 * Fixes a bug where the prefixed versions of function names were used instead of the non-prefixed ones during structural equivalence.
 * Small refactoring of structural equivalence code and the configuration class.
 * Use bijective maps during structural equivalence.
 * If the procedure/global names are detected to be different in the compared programs during structural equivalence, a warning is emitted in case the user is using the automatic configuration generation of SymDiff.

Sources/SymDiff/source/BiDictionary.cs

@@ -0,0 +1,194 @@
+using System;
+using System.Collections;
+using System.Linq;
+
+namespace SymDiff.source;
+
+using System.Collections.Generic;
+
+/// <summary>
+/// A bijective (one-to-one) dictionary.
+/// </summary>
+public class BiDictionary<TKey, TValue> : IEnumerable<KeyValuePair<TKey, TValue>>
+{
+    private Dictionary<TKey, TValue> keyToValue;
+    private Dictionary<TValue, TKey> valueToKey;
+
+    public BiDictionary()
+    {
+        keyToValue = new Dictionary<TKey, TValue>();
+        valueToKey = new Dictionary<TValue, TKey>();
+    }
+
+    public BiDictionary(BiDictionary<TKey, TValue> other)
+    {
+        keyToValue = new Dictionary<TKey, TValue>(other.keyToValue);
+        valueToKey = new Dictionary<TValue, TKey>(other.valueToKey);
+    }
+
+    public BiDictionary(Dictionary<TKey, TValue> other)
+    {
+        keyToValue = new Dictionary<TKey, TValue>(other);
+        valueToKey = new Dictionary<TValue, TKey>();
+
+        if (other.Values.Distinct().Count() != other.Count)
+        {
+            throw new ArgumentException("Values must be unique for a bijective mapping.");
+        }
+
+        foreach (var pair in other)
+        {
+            valueToKey.Add(pair.Value, pair.Key);
+        }
+    }
+
+    public bool TryAdd(TKey key, TValue value)
+    {
+        if (keyToValue.ContainsKey(key) || valueToKey.ContainsKey(value))
+        {
+            return false;
+        }
+
+        Add(key, value);
+        return true;
+    }
+
+    public void Add(TKey key, TValue value)
+    {
+        if (keyToValue.ContainsKey(key))
+        {
+            throw new ArgumentException($"The key already exists: ({key}, {keyToValue[key]})." +
+                                        $" Tried to add ({key}, {value})");
+        }
+
+        if (valueToKey.ContainsKey(value))
+        {
+            throw new ArgumentException($"The value already exists: ({valueToKey[value]}, {value})." +
+                                        $" Tried to add ({key}, {value})");
+        }
+
+        keyToValue[key] = value;
+        valueToKey[value] = key;
+    }
+
+    /// <summary>
+    /// Returns true if either the key or the value is matched with a conflicting other.
+    /// Returns false if there is no conflict, or if the pair does not exist in the map.
+    /// </summary>
+    public bool HasConflict(TKey key, TValue value)
+    {
+        var hasKey = keyToValue.TryGetValue(key, out TValue existingValue);
+        var hasValue = valueToKey.TryGetValue(value, out TKey existingKey);
+
+        if (hasKey && !EqualityComparer<TValue>.Default.Equals(value, existingValue))
+        {
+            return true;
+        }
+
+        if (hasValue && !EqualityComparer<TKey>.Default.Equals(key, existingKey))
+        {
+            return true;
+        }
+
+        return false;
+    }
+
+    /// <summary>
+    /// Update the map if the key/value does not exist with a conflicting
+    /// value/key. Returns false if there was a conflict, true otherwise.
+    /// </summary>
+    public bool TryAddIfNoConflict(TKey key, TValue value)
+    {
+        if (HasConflict(key, value))
+        {
+            return false;
+        }
+
+        // No conflict. The update might be redundant but it is safe.
+        keyToValue[key] = value;
+        valueToKey[value] = key;
+        return true;
+    }
+
+    public TValue GetValueByKey(TKey key)
+    {
+        if (!keyToValue.TryGetValue(key, out TValue value))
+        {
+            throw new KeyNotFoundException($"The given key '{key}' was not present in the dictionary.");
+        }
+        return value;
+    }
+
+    public TKey GetKeyByValue(TValue value)
+    {
+        if (!valueToKey.TryGetValue(value, out TKey key))
+        {
+            throw new KeyNotFoundException($"The given value '{value}' was not present in the dictionary.");
+        }
+        return key;
+    }
+
+    public bool TryGetValueByKey(TKey key, out TValue value)
+    {
+        return keyToValue.TryGetValue(key, out value);
+    }
+
+    public bool TryGetKeyByValue(TValue value, out TKey key)
+    {
+        return valueToKey.TryGetValue(value, out key);
+    }
+
+    public bool RemoveByKey(TKey key)
+    {
+        if (!keyToValue.TryGetValue(key, out var value))
+        {
+            return false;
+        }
+
+        keyToValue.Remove(key);
+        valueToKey.Remove(value);
+        return true;
+    }
+
+    public bool RemoveByValue(TValue value)
+    {
+        if (!valueToKey.TryGetValue(value, out var key))
+        {
+            return false;
+        }
+
+        valueToKey.Remove(value);
+        keyToValue.Remove(key);
+        return true;
+    }
+
+    public bool ContainsKey(TKey key)
+    {
+        return keyToValue.ContainsKey(key);
+    }
+
+    public bool ContainsValue(TValue value)
+    {
+        return valueToKey.ContainsKey(value);
+    }
+
+    public void Clear()
+    {
+        keyToValue.Clear();
+        valueToKey.Clear();
+    }
+
+    public Dictionary<TKey, TValue>.KeyCollection Keys => keyToValue.Keys;
+
+    public Dictionary<TKey, TValue>.ValueCollection Values => keyToValue.Values;
+
+    public IEnumerator<KeyValuePair<TKey, TValue>> GetEnumerator()
+    {
+        return keyToValue.GetEnumerator();
+    }
+
+    IEnumerator IEnumerable.GetEnumerator()
+    {
+        return GetEnumerator();
+    }
+}