From a38904cb4e780d4cc5cba033b141a88ec6850d92 Mon Sep 17 00:00:00 2001
From: Michael Emmi <michael.emmi@icloud.com>
Date: Mon, 17 Feb 2020 20:08:09 -0500
Subject: [PATCH] Enabling string operations. (#131)

* Enabling string operations.

* Preparing for string literals.

* Added regex type.

* Added regex tests.

* Added string literal rule to parser.

* Shallow type for string literals.

* Added string literal test.

* Better regex test.

* Printing string literals.

* Parsing strings from model.
---
 Source/Core/AbsyExpr.cs                     | 41 ++++++++++
 Source/Core/AbsyType.cs                     | 84 ++++++++++++++++++++-
 Source/Core/BoogiePL.atg                    |  1 +
 Source/Core/Parser.cs                       | 14 ++--
 Source/Model/ModelParser.cs                 | 32 +++++---
 Source/Provers/SMTLib/SMTLibLineariser.cs   | 13 +++-
 Source/Provers/SMTLib/TypeDeclCollector.cs  |  2 +-
 Source/VCExpr/Boogie2VCExpr.cs              |  2 +
 Source/VCExpr/TypeErasure.cs                |  8 +-
 Source/VCExpr/VCExprAST.cs                  | 31 ++++++++
 Test/strings/BasicOperators.bpl             | 43 +++++++++++
 Test/strings/BasicOperators.bpl.expect      |  2 +
 Test/strings/BasicRegExOperators.bpl        | 42 +++++++++++
 Test/strings/BasicRegExOperators.bpl.expect |  2 +
 Test/strings/Literals.bpl                   | 47 ++++++++++++
 Test/strings/Literals.bpl.expect            |  2 +
 16 files changed, 345 insertions(+), 21 deletions(-)
 create mode 100644 Test/strings/BasicOperators.bpl
 create mode 100644 Test/strings/BasicOperators.bpl.expect
 create mode 100644 Test/strings/BasicRegExOperators.bpl
 create mode 100644 Test/strings/BasicRegExOperators.bpl.expect
 create mode 100644 Test/strings/Literals.bpl
 create mode 100644 Test/strings/Literals.bpl.expect

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 337347165..7f1b0d5d9 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -373,6 +373,11 @@ public static LiteralExpr Literal(RoundingMode value)
       Contract.Ensures(Contract.Result<LiteralExpr>() != null);
       return new LiteralExpr(Token.NoToken, value);
     }
+    public static LiteralExpr Literal(String value)
+    {
+      Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+      return new LiteralExpr(Token.NoToken, value);
+    }
 
     private static LiteralExpr/*!*/ true_ = Literal(true);
     public static LiteralExpr/*!*/ True {
@@ -645,6 +650,21 @@ public LiteralExpr(IToken/*!*/ tok, RoundingMode v, bool immutable = false)
         CachedHashCode = ComputeHashCode();
     }
 
+    /// <summary>
+    /// Creates a literal expression for the string value "v".
+    /// </summary>
+    /// <param name="tok"></param>
+    /// <param name="v"></param>
+    public LiteralExpr(IToken/*!*/ tok, String v, bool immutable = false)
+      : base(tok, immutable)
+    {
+      Contract.Requires(tok != null);
+      Val = v;
+      Type = Type.String;
+      if (immutable)
+        CachedHashCode = ComputeHashCode();
+    }
+
     [Pure]
     [Reads(ReadsAttribute.Reads.Nothing)]
     public override bool Equals(object obj) {
@@ -675,6 +695,8 @@ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bo
       stream.SetToken(this);
       if (this.Val is bool) {
         stream.Write((bool)this.Val ? "true" : "false"); // correct capitalization
+      } else if (Type.IsString) {
+        stream.Write("\"" + cce.NonNull(this.Val.ToString()) + "\"");
       } else {
         stream.Write(cce.NonNull(this.Val.ToString()));
       }
@@ -710,6 +732,8 @@ public override Type/*!*/ ShallowType {
           return Type.GetBvType(((BvConst)Val).Bits);
         } else if (Val is RoundingMode) {
           return Type.RMode;
+        } else if (Val is String) {
+          return Type.String;
         } else {
           {
             Contract.Assert(false);
@@ -821,6 +845,23 @@ public RoundingMode asRoundingMode
       }
     }
 
+    public bool isString
+    {
+      get
+      {
+        return Val is String;
+      }
+    }
+
+    public String asString
+    {
+      get
+      {
+        Contract.Assert(isString);
+        return (String)cce.NonNull(Val);
+      }
+    }
+
     public override Absy StdDispatch(StandardVisitor visitor) {
       //Contract.Requires(visitor != null);
       Contract.Ensures(Contract.Result<Absy>() != null);
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index e89ce88bc..b72ad47e4 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -259,6 +259,16 @@ public virtual bool IsRMode {
         return false;
       }
     }
+    public virtual bool IsString {
+      get {
+        return false;
+      }
+    }
+    public virtual bool IsRegEx {
+      get {
+        return false;
+      }
+    }
 
     public virtual bool IsVariable {
       get {
@@ -371,6 +381,8 @@ public virtual int BvBits {
     public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real);
     public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool);
     public static readonly Type/*!*/ RMode = new BasicType(SimpleType.RMode);
+    public static readonly Type/*!*/ String = new BasicType(SimpleType.String);
+    public static readonly Type/*!*/ RegEx = new BasicType(SimpleType.RegEx);
     private static BvType[] bvtypeCache;
 
     static public BvType GetBvType(int sz) {
@@ -917,6 +929,10 @@ public override string ToString() {
           return "bool";
         case SimpleType.RMode:
           return "rmode";
+        case SimpleType.String:
+          return "string";
+        case SimpleType.RegEx:
+          return "regex";
       }
       Debug.Assert(false, "bad type " + T);
       {
@@ -1054,6 +1070,20 @@ public override bool IsRMode
         return this.T == SimpleType.RMode;
       }
     }
+    public override bool IsString
+    {
+      get
+      {
+        return this.T == SimpleType.String;
+      }
+    }
+    public override bool IsRegEx
+    {
+      get
+      {
+        return this.T == SimpleType.RegEx;
+      }
+    }
 
     public override Absy StdDispatch(StandardVisitor visitor) {
       //Contract.Requires(visitor != null);
@@ -1501,7 +1531,7 @@ public override int GetHashCode(List<TypeVariable> boundVariables) {
     public override Type ResolveType(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       Contract.Ensures(Contract.Result<Type>() != null);
-      // first case: the type name denotes a bitvector-type, float-type, or rmode-type
+      // first case: the type name denotes a bitvector-type, float-type, rmode-type, string-type, or regex-type
 
       if (Name.StartsWith("bv") && Name.Length > 2) {
         bool is_bv = true;
@@ -1554,6 +1584,28 @@ public override Type ResolveType(ResolutionContext rc) {
         return Type.RMode;
       }
 
+      if (Name.Equals("string"))
+      {
+        if (Arguments.Count > 0)
+        {
+          rc.Error(this,
+                   "string type must not be applied to arguments: {0}",
+                   Name);
+        }
+        return Type.String;
+      }
+
+      if (Name.Equals("regex"))
+      {
+        if (Arguments.Count > 0)
+        {
+          rc.Error(this,
+                   "regex type must not be applied to arguments: {0}",
+                   Name);
+        }
+        return Type.RegEx;
+      }
+
       // second case: the identifier is resolved to a type variable
       TypeVariable var = rc.LookUpTypeBinder(Name);
       if (var != null) {
@@ -2186,6 +2238,22 @@ public override bool IsRMode
         return p != null && p.IsRMode;
       }
     }
+    public override bool IsString
+    {
+      get
+      {
+        Type p = ProxyFor;
+        return p != null && p.IsString;
+      }
+    }
+    public override bool IsRegEx
+    {
+      get
+      {
+        Type p = ProxyFor;
+        return p != null && p.IsRegEx;
+      }
+    }
 
     public override bool IsVariable {
       get {
@@ -3068,6 +3136,16 @@ public override bool IsRMode {
         return ExpandedType.IsRMode;
       }
     }
+    public override bool IsString {
+      get {
+        return ExpandedType.IsString;
+      }
+    }
+    public override bool IsRegEx {
+      get {
+        return ExpandedType.IsRegEx;
+      }
+    }
 
     public override bool IsVariable {
       get {
@@ -3843,7 +3921,9 @@ public enum SimpleType {
     Int,
     Real,
     Bool,
-    RMode
+    RMode,
+    String,
+    RegEx
   };
 
 
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index b5404d24c..cce7776b3 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -1284,6 +1284,7 @@ AtomExpression<out Expr/*!*/ e>
   | Dec<out bd>            (. e = new LiteralExpr(t, bd); .)
 		| Float<out bf>            (. e = new LiteralExpr(t, bf); .)
   | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)
+  | string                  (. e = new LiteralExpr(t, t.val.Trim('"')); .)
 
   | Ident<out x>            (. id = new IdentifierExpr(x, x.val);  e = id; .)
     [ "("
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 014b327f9..77f43760c 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1811,6 +1811,11 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, bn, n); 
 			break;
 		}
+    case 4: {
+      Get();
+      e = new LiteralExpr(t, t.val.Trim('"'));
+      break;
+    }
 		case 1: {
 			Ident(out x);
 			id = new IdentifierExpr(x, x.val);  e = id; 
@@ -2109,7 +2114,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			Get();
 			Expect(1);
 			key = t.val;  parameters = new List<object/*!*/>(); 
-			if (StartOf(16)) {
+			if (StartOf(9)) {
 				AttributeParameter(out param);
 				parameters.Add(param); 
 				while (la.kind == 13) {
@@ -2212,14 +2217,13 @@ public void Parse() {
 		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _T,_T,_x,_T, _x,_x,_T,_T, _T,_T,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _x,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _x,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _x,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
+		{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}
 
 	};
 } // end Parser
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index b966d6493..19e2717d0 100644
--- a/Source/Model/ModelParser.cs
+++ b/Source/Model/ModelParser.cs
@@ -19,7 +19,7 @@ abstract internal class ModelParser
 		internal List<Model> resModels = new List<Model> ();
 		internal System.IO.TextReader rd;
 		string lastLine = "";
-		protected static char[] seps = new char[] { ' ' };
+		protected static Regex seps = new Regex("( |(?=\")|(?<=\"))");
 		protected static Regex bitVec = new Regex (@"\(_ BitVec (\d+)\)");
 		protected static Regex bv = new Regex (@"\(_ bv(\d+) (\d+)\)");
 
@@ -49,7 +49,7 @@ string[] GetWords (string line)
 		{
 			if (line == null)
 				return null;
-			var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			var words = Array.FindAll(seps.Split (line), word => word != "" && word != " ");
 			return words;
 		}
 
@@ -116,24 +116,38 @@ List<object> GetFunctionTokens (string newLine)
 
 			line = line.Replace ("(", " ( ");
 			line = line.Replace (")", " ) ");
-			var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			var tuple = seps.Split (line);
 
 			List<object> newTuple = new List<object> ();
-			Stack<List<object>> wordStack = new Stack<List<object>> ();
+			var wordStack = new Stack<Tuple<string,List<object>>> ();
 			for (int i = 0; i < tuple.Length; i++) {
 				string elem = tuple [i];
-				if (elem == "(") {
-					List<object> ls = new List<object> ();
+
+				if (elem == "" || elem == " ")
+					continue;
+
+				if (elem == "(" || elem == "\"" && (wordStack.Count == 0 || wordStack.Peek().Item1 != "\"")) {
+					var ls = Tuple.Create(elem, new List<object> ());
 					wordStack.Push (ls);
 				} else if (elem == ")") {
-					List<object> ls = wordStack.Pop ();
+					var tup = wordStack.Pop ();
+					if (tup.Item1 != "(")
+						BadModel("unmatched parentheses");
+					var ls = tup.Item2;
 					if (wordStack.Count > 0) {
-						wordStack.Peek ().Add (ls);
+						wordStack.Peek ().Item2.Add (ls);
 					} else {
 						newTuple.Add (ls);
 					}
+				} else if (elem == "\"") {
+					var words = "\"" + String.Join(" ", wordStack.Pop().Item2) + "\"";
+					if (wordStack.Count > 0)
+						wordStack.Peek().Item2.Add(String.Join(" ", words));
+					else
+						newTuple.Add(words);
+
 				} else if (wordStack.Count > 0) {
-					wordStack.Peek ().Add (elem);
+					wordStack.Peek ().Item2.Add (elem);
 				} else {
 					newTuple.Add (elem);
 				}
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 0bbacbf9d..00ac175a0 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -121,7 +121,7 @@ private static void TypeToStringHelper(Type t, StringBuilder sb)
           }
           sb.Append(']');
           TypeToStringHelper(m.Result, sb);
-        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv || t.IsRMode) {
+        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv || t.IsRMode || t.IsString) {
           sb.Append(TypeToString(t));
         } else {
           System.IO.StringWriter buffer = new System.IO.StringWriter();
@@ -149,8 +149,12 @@ public static string TypeToString(Type t)
         return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")";
       else if (t.IsBv)
         return "(_ BitVec " + t.BvBits + ")";
-      else if (t.IsRMode) {
+      else if (t.IsRMode)
         return "RoundingMode";
+      else if (t.IsString)
+        return "String";
+      else if (t.IsRegEx) {
+        return "(RegEx String)";
       } else {
         StringBuilder sb = new StringBuilder();        
         TypeToStringHelper(t, sb);
@@ -218,6 +222,11 @@ public bool Visit(VCExprLiteral node, LineariserOptions options)
         RoundingMode lit = ((VCExprRModeLit)node).Val;
         wr.Write(lit.ToString());
       }
+      else if (node is VCExprStringLit)
+      {
+        String lit = ((VCExprStringLit)node).Val;
+        wr.Write("\"" + lit.ToString() + "\"");
+      }
       else {
         Contract.Assert(false);
         throw new cce.UnreachableException();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 3f60e326d..96dd9e99c 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -316,7 +316,7 @@ private void RegisterType(Type type)
         return;
       }
 
-      if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat || type.IsRMode)
+      if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat || type.IsRMode || type.IsString || type.IsRegEx)
         return;
 
       CtorType ctorType = type as CtorType;
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 99280719f..9d8fcdb70 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -338,6 +338,8 @@ private VCExpr TranslateLiteralExpr(LiteralExpr node) {
         return Gen.Float(node.asBigFloat);
       } else if (node.Val is RoundingMode) {
         return Gen.RMode(node.asRoundingMode);
+      } else if (node.Val is String) {
+        return Gen.String(node.asString);
       }
       else if (node.Val is BvConst) {
         return Gen.Bitvector((BvConst)node.Val);
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index c79ce0a5a..74d16f7c9 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -457,6 +457,8 @@ public virtual void Setup() {
       GetBasicTypeRepr(Type.Real);
       GetBasicTypeRepr(Type.Bool);
       GetBasicTypeRepr(Type.RMode);
+      GetBasicTypeRepr(Type.String);
+      GetBasicTypeRepr(Type.RegEx);
     }
 
     // constructor to allow cloning
@@ -560,6 +562,8 @@ public override void Setup() {
       GetTypeCasts(Type.Real);
       GetTypeCasts(Type.Bool);
       GetTypeCasts(Type.RMode);
+      GetTypeCasts(Type.String);
+      GetTypeCasts(Type.RegEx);
 
     }
 
@@ -681,7 +685,7 @@ public override Type TypeAfterErasure(Type type) {
     [Pure]
     public override bool UnchangedType(Type type) {
       //Contract.Requires(type != null);
-      return type.IsInt || type.IsReal || type.IsBool || type.IsBv || type.IsFloat || type.IsRMode || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
+      return type.IsInt || type.IsReal || type.IsBool || type.IsBv || type.IsFloat || type.IsRMode || type.IsString || type.IsRegEx || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
     }
 
     public VCExpr Cast(VCExpr expr, Type toType) {
@@ -1078,7 +1082,7 @@ public override VCExpr Visit(VCExprLiteral node, VariableBindings bindings) {
       Contract.Requires(bindings != null);
       Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
-      Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real || node.Type == Type.RMode);
+      Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real || node.Type == Type.RMode || node.Type == Type.String || node.Type == Type.RegEx);
       return node;
     }
 
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index d615a1b5d..a39375b0a 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -69,6 +69,13 @@ public VCExpr ControlFlowFunctionApplication(VCExpr e1, VCExpr e2) {
       return new VCExprRModeLit(x);
     }
 
+    public VCExpr/*!*/ String(String x)
+    {
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+      return new VCExprStringLit(x);
+    }
+
     public VCExpr/*!*/ Function(VCExprOp/*!*/ op,
                             List<VCExpr/*!*/>/*!*/ arguments,
                             List<Type/*!*/>/*!*/ typeArguments) {
@@ -938,6 +945,30 @@ public override int GetHashCode()
     }
   }
 
+  public class VCExprStringLit : VCExprLiteral
+  {
+    public readonly String Val;
+    internal VCExprStringLit(String val)
+      : base(Type.RMode)
+    {
+      this.Val = val;
+    }
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override bool Equals(object that)
+    {
+      if (Object.ReferenceEquals(this, that))
+        return true;
+      if (that is VCExprStringLit)
+        return Val == ((VCExprStringLit)that).Val;
+      return false;
+    }
+    [Pure]
+    public override int GetHashCode()
+    {
+      return Val.GetHashCode() * 72321;
+    }
+  }
   /////////////////////////////////////////////////////////////////////////////////
   // Operator expressions with fixed arity
   [ContractClassFor(typeof(VCExprNAry))]
diff --git a/Test/strings/BasicOperators.bpl b/Test/strings/BasicOperators.bpl
new file mode 100644
index 000000000..0403cea40
--- /dev/null
+++ b/Test/strings/BasicOperators.bpl
@@ -0,0 +1,43 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "str.++"} concat(string, string): string;
+function {:builtin "str.len"} len(string): int;
+function {:builtin "str.substr"} substr(string, int, int): string;
+function {:builtin "str.indexof"} indexOf(string, string): int;
+function {:builtin "str.indexof"} indexOfFromOffset(string, string, int): int;
+function {:builtin "str.at"} at(string, int): string;
+function {:builtin "str.contains"} contains(string, string): bool;
+function {:builtin "str.prefixof"} prefixOf(string, string): bool;
+function {:builtin "str.suffixof"} suffixOf(string, string): bool;
+function {:builtin "str.replace"} replace(string, string, string): string;
+function {:builtin "str.to.int"} stringToInt(string): int;
+function {:builtin "int.to.str"} intToString(int): string;
+
+procedure main() {
+    var s1, s2, s3: string;
+
+    assume len(s1) == 3;
+    assume len(s3) == 3;
+    assume concat(s1,s2) == s3;
+
+    assert len(s1) + len(s2) == len(s3);
+
+    assert substr(s3, len(s1), len(s2)) == s2;
+
+    assert indexOf(s3, s1) == 0;
+
+    assert indexOfFromOffset(s3, s1, 0) == 0;
+
+    assert at(s3, 2) == at(s1, 2);
+
+    assert contains(s3, s1);
+
+    assert prefixOf(s1, s3);
+
+    assert suffixOf(s2, s3);
+
+    assert replace(s3, s1, s2) == concat(s2, s2);
+
+    assert intToString(stringToInt(s1)) == s1;
+}
diff --git a/Test/strings/BasicOperators.bpl.expect b/Test/strings/BasicOperators.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/strings/BasicOperators.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/strings/BasicRegExOperators.bpl b/Test/strings/BasicRegExOperators.bpl
new file mode 100644
index 000000000..c68a716fd
--- /dev/null
+++ b/Test/strings/BasicRegExOperators.bpl
@@ -0,0 +1,42 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "str.to.re"} stringToRegEx(string): regex;
+function {:builtin "str.in.re"} stringInRegEx(string, regex): bool;
+function {:builtin "re.allchar"} allChar(): regex;
+function {:builtin "re.nostr"} noString(): regex;
+function {:builtin "re.range"} range(string, string): regex;
+function {:builtin "re.++"} concat(regex, regex): regex;
+function {:builtin "re.*"} star(regex): regex;
+function {:builtin "re.+"} plus(regex): regex;
+function {:builtin "re.opt"} option(regex): regex;
+function {:builtin "re.loop"} loop(regex, int, int): regex;
+function {:builtin "re.union"} union(regex, regex): regex;
+function {:builtin "re.inter"} intersection(regex, regex): regex;
+
+procedure main() {
+    var s1: string;
+    var r1: regex;
+
+    s1 := "abcd";
+    r1 := stringToRegEx(s1);
+
+    assert stringInRegEx(s1, stringToRegEx(s1));
+    assert !stringInRegEx(s1, stringToRegEx("ABCD"));
+
+    assert stringInRegEx(s1, star(allChar()));
+
+    assert !stringInRegEx(s1, noString());
+
+    assert !stringInRegEx(s1, concat(noString(), noString()));
+
+    assert stringInRegEx(s1, option(plus(allChar())));
+
+    assert !stringInRegEx(s1, loop(noString(), 0, 5));
+    assert stringInRegEx(s1, loop(allChar(), 0, 5));
+
+    assert !stringInRegEx(s1, union(noString(), noString()));
+    assert stringInRegEx(s1, intersection(star(allChar()), star(allChar())));
+
+}
+
diff --git a/Test/strings/BasicRegExOperators.bpl.expect b/Test/strings/BasicRegExOperators.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/strings/BasicRegExOperators.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/strings/Literals.bpl b/Test/strings/Literals.bpl
new file mode 100644
index 000000000..51daf8703
--- /dev/null
+++ b/Test/strings/Literals.bpl
@@ -0,0 +1,47 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "str.++"} concat(string, string): string;
+function {:builtin "str.len"} len(string): int;
+function {:builtin "str.substr"} substr(string, int, int): string;
+function {:builtin "str.indexof"} indexOf(string, string): int;
+function {:builtin "str.indexof"} indexOfFromOffset(string, string, int): int;
+function {:builtin "str.at"} at(string, int): string;
+function {:builtin "str.contains"} contains(string, string): bool;
+function {:builtin "str.prefixof"} prefixOf(string, string): bool;
+function {:builtin "str.suffixof"} suffixOf(string, string): bool;
+function {:builtin "str.replace"} replace(string, string, string): string;
+function {:builtin "str.to.int"} stringToInt(string): int;
+function {:builtin "int.to.str"} intToString(int): string;
+
+procedure main() {
+    assert concat("abc", "def") == "abcdef";
+
+    assert len("abcd") == 4;
+
+    assert substr("abcd", 1, 2) == "bc";
+
+    assert indexOf("abcd", "cd") == 2;
+    assert indexOf("abcd", "dc") == -1;
+
+    assert indexOfFromOffset("abcdabcd", "cd", 0) == 2;
+    assert indexOfFromOffset("abcdabcd", "cd", 3) == 6;
+    assert indexOfFromOffset("abcdabcd", "dc", 1) == -1;
+
+    assert at("abcd", 2) == "c";
+
+    assert contains("abcd", "bc");
+    assert !contains("abcd", "BC");
+
+    assert prefixOf("ab", "abcd");
+    assert !prefixOf("AB", "abcd");
+
+    assert suffixOf("cd", "abcd");
+    assert !suffixOf("CD", "abcd");
+
+    assert replace("aBCd", "BC", "bc") == "abcd";
+
+    assert stringToInt("42") == 42;
+
+    assert intToString(42) == "42";
+}
diff --git a/Test/strings/Literals.bpl.expect b/Test/strings/Literals.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/strings/Literals.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors