diff options
| -rw-r--r-- | Source/Core/AbsyType.ssc | 3 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 3 | ||||
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 144 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 2 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasureArguments.cs | 4 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasurePremisses.cs | 2 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 1 |
7 files changed, 117 insertions, 42 deletions
diff --git a/Source/Core/AbsyType.ssc b/Source/Core/AbsyType.ssc index 3d2ab73a..6079163a 100644 --- a/Source/Core/AbsyType.ssc +++ b/Source/Core/AbsyType.ssc @@ -2131,7 +2131,8 @@ namespace Microsoft.Boogie public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
{
stream.SetToken(this);
- CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
+ ExpandedType.Emit(stream, contextBindingStrength);
+ // CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
}
//----------- Resolution ----------------------------------
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 35e182e6..97167e18 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -153,6 +153,7 @@ namespace Microsoft.Boogie public BvHandling Bitvectors = BvHandling.Z3Native;
public bool UseArrayTheory = false;
+ public bool MonomorphicArrays { get { return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic; } }
public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
public bool DoModSetAnalysis = false; @@ -1324,7 +1325,7 @@ namespace Microsoft.Boogie OwnershipModelEncoding = OwnershipModelOption.Trivial;
}
- if (UseArrayTheory) {
+ if (MonomorphicArrays) {
Monomorphize = true;
}
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs index 3baa1d26..5dfa6468 100644 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ b/Source/Provers/Z3/TypeDeclCollector.cs @@ -132,27 +132,35 @@ void ObjectInvariant() {
Contract.Requires(type != null);
if (KnownTypes.ContainsKey(type)) return;
-
- if (type.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
+
+ if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {
KnownTypes.Add(type, true);
string declString = "";
MapType mapType = type.AsMap;
- Contract.Assert(mapType!=null);
-
- declString += "(DEFTYPE " + TypeToString(type) + " :BUILTIN Array ";
- foreach (Type t in mapType.Arguments) {
- Contract.Assert(t!=null);
- RegisterType(t);
- declString += TypeToString(t);
- declString += " ";
- }
- RegisterType(mapType.Result);
- declString += TypeToString(mapType.Result);
- declString += ")";
- AddDeclaration(declString);
- return;
+ Contract.Assert(mapType != null);
+
+ foreach (Type t in mapType.Arguments) {
+ Contract.Assert(t != null);
+ RegisterType(t);
+ }
+ RegisterType(mapType.Result);
+
+ declString += "(DEFTYPE " + TypeToString(type);
+
+ if (CommandLineOptions.Clo.UseArrayTheory) {
+ declString += " :BUILTIN Array ";
+ foreach (Type t in mapType.Arguments) {
+ declString += TypeToString(t);
+ declString += " ";
+ }
+ declString += TypeToString(mapType.Result);
+ }
+
+ declString += ")";
+ AddDeclaration(declString);
+ return;
}
-
+
if (type.IsBv && NativeBv) {
int bits = type.BvBits;
string name = TypeToString(type);
@@ -212,34 +220,87 @@ void ObjectInvariant() }
//
} else if (node.Op is VCExprStoreOp) {
- //
- RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node[2].Type);
- RegisterType(node.Type);
+ RegisterType(node.Type); // this is the map type, registering it should register also the index and value types
string name = SimplifyLikeExprLineariser.StoreOpName(node);
if (!KnownStoreFunctions.ContainsKey(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node[2].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN store)");
+ string decl = "(DEFOP " + name;
+
+ foreach (VCExpr ch in node) {
+ decl += " " + TypeToString(ch.Type);
+ }
+ decl += " " + TypeToString(node.Type);
+
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ decl += " :BUILTIN store";
+ decl += ")";
+ AddDeclaration(decl);
+
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {
+ var sel = SimplifyLikeExprLineariser.SelectOpName(node);
+
+ if (!KnownSelectFunctions.ContainsKey(name)) {
+ // need to declare it before reference
+ string seldecl = "(DEFOP " + sel;
+ foreach (VCExpr ch in node) {
+ seldecl += " " + TypeToString(ch.Type);
+ }
+ AddDeclaration(seldecl + ")");
+ KnownSelectFunctions.Add(name, true);
+ }
+
+ var eq = "EQ";
+ if (node[node.Arity - 1].Type.IsBool)
+ eq = "IFF";
+
+ string ax1 = "(BG_PUSH (FORALL (";
+ string ax2 = "(BG_PUSH (FORALL (";
+ string argX = "", argY = "";
+ string dist = "";
+ for (int i = 0; i < node.Arity; i++) {
+ var t = " :TYPE " + TypeToString(node[i].Type);
+ var x = " x" + i;
+ var y = " y" + i;
+ ax1 += x + t;
+ ax2 += x + t;
+ if (i != 0 && i != node.Arity - 1) {
+ argX += x;
+ argY += y;
+ ax2 += y + t;
+ dist += " (NEQ" + x + y + ")";
+ }
+ }
+ string v = " x" + (node.Arity - 1);
+ ax1 += ") ";
+ ax1 += "(" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argX + ") " + v + ")";
+ ax1 += "))";
+
+ ax2 += ") ";
+ ax2 += "(IMPLIES (OR " + dist + ") (" + eq + " (" + sel + " (" + name + " x0" + argX + v + ")" + argY + ") (" + sel + " x0" + argY + ")))";
+ ax2 += "))";
+
+ AddDeclaration(ax1);
+ AddDeclaration(ax2);
+ }
+
KnownStoreFunctions.Add(name, true);
}
//
} else if (node.Op is VCExprSelectOp) {
//
RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node.Type);
string name = SimplifyLikeExprLineariser.SelectOpName(node);
if (!KnownSelectFunctions.ContainsKey(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN select)");
+ string decl = "(DEFOP " + name;
+
+ foreach (VCExpr ch in node) {
+ decl += " " + TypeToString(ch.Type);
+ }
+ decl += " " + TypeToString(node.Type);
+
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ decl += " :BUILTIN select";
+ decl += ")";
+ AddDeclaration(decl);
KnownSelectFunctions.Add(name, true);
}
//
@@ -277,7 +338,18 @@ void ObjectInvariant() //
}
- return base.Visit(node, arg);
+ // What happens in base.Visit() just seems wrong. It seems to use some hack to enumerate
+ // recursive children of current node, which doesn't seem to work for nested store expressions
+ // (the store expressions themselves get skipped).
+ var res = StandardResult(node, arg);
+ foreach (VCExpr n in node)
+ {
+ n.Accept(this, arg);
+ }
+
+ return res;
+
+ // return base.Visit(node, arg);
}
private string ExtractBuiltin(Function f) {
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index c4deb76c..5029ba53 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -727,7 +727,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null); [Pure]
public override bool UnchangedType(Type type) {
Contract.Requires(type != null);
- return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.UseArrayTheory);
+ return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
}
public VCExpr Cast(VCExpr expr, Type toType) {
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index c1a32aba..62bc72ea 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -192,7 +192,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); storeTypes[i] = AxBuilder.T;
}
// Fill in the map type
- if (CommandLineOptions.Clo.UseArrayTheory) {
+ if (CommandLineOptions.Clo.MonomorphicArrays) {
selectTypes[i] = abstractedType;
storeTypes[i] = abstractedType;
} else {
@@ -223,7 +223,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); }
i++;
// Fill in the map type which is the output of the store function
- if (CommandLineOptions.Clo.UseArrayTheory)
+ if (CommandLineOptions.Clo.MonomorphicArrays)
storeTypes[i] = abstractedType;
else
storeTypes[i] = AxBuilder.U;
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index 9d5eef26..cf0bcaa4 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -634,7 +634,7 @@ Contract.Requires(var != null); mapTypeParams.Add(var);
}
- if (CommandLineOptions.Clo.UseArrayTheory)
+ if (CommandLineOptions.Clo.MonomorphicArrays)
mapTypeSynonym = abstractedType;
else
mapTypeSynonym = new CtorType(Token.NoToken, synonymDecl, mapTypeParams);
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 4a13cbb5..1675a3a7 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -256,6 +256,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(node != null);
Result res = StandardResult(node, arg);
+
if (node.TypeParamArity == 0) {
Contract.Assert(node.Op != null);
VCExprOp op = node.Op;
|