diff options
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/NameClashResolver.ssc | 14 | ||||
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.ssc | 44 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.ssc | 2 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.ssc | 18 |
4 files changed, 65 insertions, 13 deletions
diff --git a/Source/VCExpr/NameClashResolver.ssc b/Source/VCExpr/NameClashResolver.ssc index 28a974a6..9c281bf8 100644 --- a/Source/VCExpr/NameClashResolver.ssc +++ b/Source/VCExpr/NameClashResolver.ssc @@ -27,6 +27,7 @@ namespace Microsoft.Boogie.VCExprAST { as IDictionary<Object!, string!>);
UsedNames = new Dictionary<string!, bool> ();
CurrentCounters = new Dictionary<string!, int> ();
+ GlobalPlusLocalNames = new Dictionary<Object!, string!> ();
}
private UniqueNamer(UniqueNamer! namer) {
@@ -41,6 +42,7 @@ namespace Microsoft.Boogie.VCExprAST { UsedNames = new Dictionary<string!, bool> (namer.UsedNames);
CurrentCounters = new Dictionary<string!, int> (namer.CurrentCounters);
+ GlobalPlusLocalNames = new Dictionary<Object!, string!>(namer.GlobalPlusLocalNames);
}
public Object! Clone() {
@@ -56,6 +58,7 @@ namespace Microsoft.Boogie.VCExprAST { // (locally or globally)
private readonly IDictionary<string!, bool>! UsedNames;
private readonly IDictionary<string!, int>! CurrentCounters;
+ private readonly IDictionary<Object!, string!>! GlobalPlusLocalNames;
////////////////////////////////////////////////////////////////////////////
@@ -69,7 +72,7 @@ namespace Microsoft.Boogie.VCExprAST { ////////////////////////////////////////////////////////////////////////////
- private string! NextFreeName(string! baseName) {
+ private string! NextFreeName(Object! thingie, string! baseName) {
string! candidate;
int counter;
@@ -89,6 +92,7 @@ namespace Microsoft.Boogie.VCExprAST { UsedNames.Add(candidate, true);
CurrentCounters[baseName] = counter;
+ GlobalPlusLocalNames[thingie] = candidate;
return candidate;
}
@@ -102,7 +106,7 @@ namespace Microsoft.Boogie.VCExprAST { return res;
// if the object is not yet registered, create a name for it
- res = NextFreeName(inherentName);
+ res = NextFreeName(thingie, inherentName);
GlobalNames.Add(thingie, res);
return res;
@@ -121,9 +125,13 @@ namespace Microsoft.Boogie.VCExprAST { } }
public string! GetLocalName(Object! thingie, string! inherentName) {
- string! res = NextFreeName(inherentName);
+ string! res = NextFreeName(thingie, inherentName);
LocalNames[LocalNames.Count - 1][thingie] = res;
return res;
}
+
+ public string! Lookup(Object! thingie) {
+ return GlobalPlusLocalNames[thingie];
+ }
}
}
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index 7085bffe..d3729ab1 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -197,6 +197,13 @@ namespace Microsoft.Boogie.VCExprAST }
}
+ private static string! TypeToStringHelper(Type! t) {
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+ t.Emit(stream);
+ }
+ return buffer.ToString();
+ }
public static string! TypeToString(Type! t) {
if (t.IsBool)
return "$bool";
@@ -204,17 +211,14 @@ namespace Microsoft.Boogie.VCExprAST return "$int";
else if (t.IsBv)
return "$bv" + t.BvBits;
+ else if (t.IsMap)
+ return TypeToStringHelper(t);
else {
// at this point, only the types U, T, and bitvector types should be left
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic)
return "U";
- else {
- System.IO.StringWriter buffer = new System.IO.StringWriter();
- using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
- t.Emit(stream);
- }
- return buffer.ToString();
- }
+ else
+ return TypeToStringHelper(t);
}
}
@@ -231,6 +235,16 @@ namespace Microsoft.Boogie.VCExprAST return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";
}
+ public static string! StoreOpName(VCExprNAry! node)
+ requires node.Op is VCExprStoreOp; {
+ return "Store_" + TypeToString(node[0].Type);
+ }
+
+ public static string! SelectOpName(VCExprNAry! node)
+ requires node.Op is VCExprSelectOp; {
+ return "Select_" + TypeToString(node[0].Type);
+ }
+
internal void WriteId(string! s) {
wr.Write(MakeIdPrintable(s));
}
@@ -679,11 +693,23 @@ namespace Microsoft.Boogie.VCExprAST }
public bool VisitSelectOp (VCExprNAry! node, LineariserOptions! options) {
- assert false; // should not occur in the output
+ wr.Write("(" + SelectOpName(node) + " ");
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(")");
+ return true;
}
public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) {
- assert false; // should not occur in the output
+ wr.Write("(" + StoreOpName(node) + " ");
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[2], options);
+ wr.Write(")");
+ return true;
}
public bool VisitBvOp (VCExprNAry! node, LineariserOptions! options) {
diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc index d41cb887..bbf9d16e 100644 --- a/Source/VCExpr/TypeErasure.ssc +++ b/Source/VCExpr/TypeErasure.ssc @@ -805,7 +805,7 @@ namespace Microsoft.Boogie.TypeErasure public VCExpr! Erase(VCExpr! expr, int polarity)
requires polarity >= -1 && polarity <= 1; {
this.Polarity = polarity;
- return Mutate(expr, new VariableBindings ());
+ return Mutate(expr, new VariableBindings());
}
internal int Polarity = 1; // 1 for positive, -1 for negative, 0 for both
diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc index e08e6138..2b5003a6 100644 --- a/Source/VCExpr/VCExprAST.ssc +++ b/Source/VCExpr/VCExprAST.ssc @@ -24,6 +24,24 @@ namespace Microsoft.Boogie public static readonly VCExpr! False = new VCExprLiteral (Type.Bool);
public static readonly VCExpr! True = new VCExprLiteral (Type.Bool);
+ private Function ControlFlowFunction = null;
+ public VCExpr! ControlFlowFunctionApplication(VCExpr! e1, VCExpr! e2)
+ {
+ if (ControlFlowFunction == null) {
+ Formal! first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
+ Formal! second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
+ VariableSeq! inputs = new VariableSeq();
+ inputs.Add(first);
+ inputs.Add(second);
+ Formal! returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);
+ ControlFlowFunction = new Function(Token.NoToken, "ControlFlow", inputs, returnVar);
+ }
+ List<VCExpr!> args = new List<VCExpr!>();
+ args.Add(e1);
+ args.Add(e2);
+ return Function(BoogieFunctionOp(ControlFlowFunction), args);
+ }
+
public VCExpr! Integer(BigNum x) {
return new VCExprIntLit(x);
}
|