Prefix interval regex inference

panacekcz · Apr 26, 2017 · c955bb5 · c955bb5
1 parent 82d0c36
commit c955bb5
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 7 deletions.
diff --git a/Microsoft.Research/AbstractInterpretation/Abstract Domains/String/PrefixInterval.cs b/Microsoft.Research/AbstractInterpretation/Abstract Domains/String/PrefixInterval.cs
@@ -294,7 +294,7 @@ public PrefixInterval Insert(WithConstants<PrefixInterval> self, IndexInterval i
             public PrefixInterval Replace(PrefixInterval self, CharInterval from, CharInterval to)
             {
 
-                if (from.IsConstant && to.IsConstant)
+                if (from.IsConstant && to.IsConstant && !self.lowerBound.IsBottom)
                     return For(self.lowerBound.prefix.Replace(from.LowerBound, to.LowerBound), self.upperBound.prefix.Replace(from.LowerBound, to.LowerBound));
                 else
                     return ForUpperBound(prefixOperations.Replace(self.upperBound, from, to));
@@ -613,7 +613,7 @@ public IStringPredicate RegexIsMatch(PrefixInterval self, Variable selfVariable,
             ///<inheritdoc/>
             public IEnumerable<Microsoft.Research.Regex.Model.Element> ToRegex(PrefixInterval self)
             {
-                return prefixOperations.ToRegex(self.upperBound);
+                return new PrefixRegex(self.upperBound).GetRegexWithLowerBound(self.lowerBound);
             }
 
             ///<inheritdoc/>

diff --git a/Microsoft.Research/AbstractInterpretation/Abstract Domains/String/PrefixRegex.cs b/Microsoft.Research/AbstractInterpretation/Abstract Domains/String/PrefixRegex.cs
@@ -72,17 +72,37 @@ public PrefixRegex(Prefix value)
             this.value = value;
         }
 
+        private Concatenation GetRegexElement()
+        {
+            // Sequence of characters preceded by anchor
+            Concatenation sequence = new Concatenation();
+            sequence.Parts.Add(Anchor.Begin);
+            foreach (char c in value.prefix)
+                sequence.Parts.Add(new Character(c));
+
+            return GetRegexElement();
+        }
+
         /// <summary>
         /// Creates a regular expression for the stored prefix.
         /// </summary>
         /// <returns>A single regular expression matching the prefix.</returns>
         public IEnumerable<Element> GetRegex()
         {
-            // Sequence of characters preceded by anchor
-            Concatenation sequence = new Concatenation();
-            sequence.Parts.Add(Anchor.Begin);
-            foreach(char c in value.prefix)
-                sequence.Parts.Add(new Character(c));
+            return new Element[] { GetRegexElement() };
+        }
+
+        public IEnumerable<Element> GetRegexWithLowerBound(Prefix lowerBound)
+        {
+            Concatenation sequence = GetRegexElement();
+
+            if (!lowerBound.IsBottom) {
+                for (int i = value.prefix.Length; i<lowerBound.prefix.Length;++i)
+                {
+                    sequence.Parts.Add(new Loop(new Character(lowerBound.prefix[i]), 0, 1));
+                }
+                sequence.Parts.Add(Anchor.End);
+            }
 
             return new Element[] { sequence };
         }