summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasurePremisses.cs
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-13 00:44:20 +0000
committerGravatar tabarbe <unknown>2010-08-13 00:44:20 +0000
commite81605e480d055843132b41a58451e4ab2cf18b0 (patch)
tree6e7cf68fb797da9f29c20f4a8fc853546a36db31 /Source/VCExpr/TypeErasurePremisses.cs
parent85ffcd8f1392bf871e585fe8efb60e38bfdb2f72 (diff)
Boogie: Committing new source code for VCExpr
Diffstat (limited to 'Source/VCExpr/TypeErasurePremisses.cs')
-rw-r--r--Source/VCExpr/TypeErasurePremisses.cs917
1 files changed, 574 insertions, 343 deletions
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 61144209..9d5eef26 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -8,7 +8,7 @@ using System.Text;
using System.IO;
using System.Collections;
using System.Collections.Generic;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
@@ -32,15 +32,26 @@ namespace Microsoft.Boogie.TypeErasure
// of the original function).
internal struct UntypedFunction {
- public readonly Function! Fun;
+ public readonly Function/*!*/ Fun;
// type parameters that can be extracted from the value parameters
- public readonly List<TypeVariable!>! ImplicitTypeParams;
+ public readonly List<TypeVariable/*!*/>/*!*/ ImplicitTypeParams;
// type parameters that have to be given explicitly
- public readonly List<TypeVariable!>! ExplicitTypeParams;
+ public readonly List<TypeVariable/*!*/>/*!*/ ExplicitTypeParams;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Fun != null);
+ Contract.Invariant(cce.NonNullElements(ImplicitTypeParams));
+ Contract.Invariant(cce.NonNullElements(ExplicitTypeParams));
+}
+
- public UntypedFunction(Function! fun,
- List<TypeVariable!>! implicitTypeParams,
- List<TypeVariable!>! explicitTypeParams) {
+ public UntypedFunction(Function/*!*/ fun,
+ List<TypeVariable/*!*/>/*!*/ implicitTypeParams,
+ List<TypeVariable/*!*/>/*!*/ explicitTypeParams) {
+ Contract.Requires(fun != null);
+ Contract.Requires(cce.NonNullElements(implicitTypeParams));
+ Contract.Requires(cce.NonNullElements(explicitTypeParams));
Fun = fun;
ImplicitTypeParams = implicitTypeParams;
ExplicitTypeParams = explicitTypeParams;
@@ -49,20 +60,23 @@ namespace Microsoft.Boogie.TypeErasure
public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU {
- public TypeAxiomBuilderPremisses(VCExpressionGenerator! gen) {
- base(gen);
+ public TypeAxiomBuilderPremisses(VCExpressionGenerator gen)
+ : base(gen) {
+ Contract.Requires(gen != null);
+
TypeFunction = HelperFuns.BoogieFunction("dummy", Type.Int);
- Typed2UntypedFunctions = new Dictionary<Function!, UntypedFunction> ();
+ Typed2UntypedFunctions = new Dictionary<Function/*!*/, UntypedFunction>();
MapTypeAbstracterAttr = null;
}
// constructor to allow cloning
[NotDelayed]
- internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses! builder) {
+ internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses builder)
+ : base(builder) {//TODO: Possible troublespot
+ Contract.Requires(builder != null);
TypeFunction = builder.TypeFunction;
Typed2UntypedFunctions =
- new Dictionary<Function!, UntypedFunction> (builder.Typed2UntypedFunctions);
- base(builder);
+ new Dictionary<Function/*!*/, UntypedFunction>(builder.Typed2UntypedFunctions);
MapTypeAbstracterAttr =
builder.MapTypeAbstracterAttr == null ?
@@ -70,7 +84,8 @@ namespace Microsoft.Boogie.TypeErasure
builder.MapTypeAbstracterAttr);
}
- public override Object! Clone() {
+ public override Object Clone() {
+ Contract.Ensures(Contract.Result<Object>() != null);
return new TypeAxiomBuilderPremisses(this);
}
@@ -83,37 +98,49 @@ namespace Microsoft.Boogie.TypeErasure
// generate axioms of the kind "forall x:U. {Int2U(U2Int(x))}
// type(x)=int ==> Int2U(U2Int(x))==x"
- protected override VCExpr! GenReverseCastAxiom(Function! castToU, Function! castFromU) {
- List<VCTrigger!>! triggers;
- VCExprVar! var;
- VCExpr! eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);
- VCExpr! premiss;
+ protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) {
+ Contract.Requires(castFromU != null);
+ Contract.Requires(castToU != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ List<VCTrigger/*!*/>/*!*/ triggers;
+ VCExprVar/*!*/ var;
+ VCExpr/*!*/ eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);
+ Contract.Assert(cce.NonNullElements(triggers));
+ Contract.Assert(var != null);
+ Contract.Assert(eq != null);
+ VCExpr/*!*/ premiss;
if (CommandLineOptions.Clo.TypeEncodingMethod
== CommandLineOptions.TypeEncoding.None)
premiss = VCExpressionGenerator.True;
else
- premiss = GenVarTypeAxiom(var, ((!)castFromU.OutParams[0]).TypedIdent.Type,
- // we don't have any bindings available
- new Dictionary<TypeVariable!, VCExpr!> ());
- VCExpr! matrix = Gen.ImpliesSimp(premiss, eq);
+ premiss = GenVarTypeAxiom(var, cce.NonNull(castFromU.OutParams[0]).TypedIdent.Type,
+ // we don't have any bindings available
+ new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>());
+ VCExpr/*!*/ matrix = Gen.ImpliesSimp(premiss, eq);
+ Contract.Assert(matrix != null);
return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, matrix);
}
- protected override VCExpr! GenCastTypeAxioms(Function! castToU, Function! castFromU) {
- Type! fromType = ((!)castToU.InParams[0]).TypedIdent.Type;
- return GenFunctionAxiom(castToU, new List<TypeVariable!> (), new List<TypeVariable!> (),
+ protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {
+ Contract.Requires(castFromU != null);
+ Contract.Requires(castToU != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Type/*!*/ fromType = cce.NonNull(castToU.InParams[0]).TypedIdent.Type;
+ return GenFunctionAxiom(castToU, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>(),
HelperFuns.ToList(fromType), fromType);
}
private MapTypeAbstractionBuilderPremisses MapTypeAbstracterAttr;
- internal override MapTypeAbstractionBuilder! MapTypeAbstracter { get {
+ internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter { get {Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
+
if (MapTypeAbstracterAttr == null)
MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses (this, Gen);
return MapTypeAbstracterAttr;
} }
- internal MapTypeAbstractionBuilderPremisses! MapTypeAbstracterPremisses { get {
+ internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses { get {Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
+
return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
} }
@@ -121,9 +148,17 @@ namespace Microsoft.Boogie.TypeErasure
// function that maps individuals to their type
// the field is overwritten with its actual value in "Setup"
- private Function! TypeFunction;
+ private Function/*!*/ TypeFunction;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(TypeFunction != null);
+}
+
- public VCExpr! TypeOf(VCExpr! expr) {
+ public VCExpr TypeOf(VCExpr expr){
+Contract.Requires(expr != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
return Gen.Function(TypeFunction, expr);
}
@@ -131,25 +166,31 @@ namespace Microsoft.Boogie.TypeErasure
// Generate type premisses and type parameter bindings for quantifiers, functions, procedures
// let-bindings to extract the instantiations of type parameters
- public List<VCExprLetBinding!>!
+ public List<VCExprLetBinding/*!*/>/*!*/
GenTypeParamBindings(// the original bound variables and (implicit) type parameters
- List<TypeVariable!>! typeParams, List<VCExprVar!>! oldBoundVars,
+ List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ oldBoundVars,
// VariableBindings to which the translation
// TypeVariable -> VCExprVar is added
- VariableBindings! bindings,
+ VariableBindings/*!*/ bindings,
bool addTypeVarsToBindings) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(cce.NonNullElements(oldBoundVars));
+ Contract.Requires(bindings != null);
+
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
+
// type variables are replaced with ordinary variables that are bound using a
// let-expression
if (addTypeVarsToBindings) {
- foreach (TypeVariable! tvar in typeParams)
- bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));
+ foreach (TypeVariable/*!*/ tvar in typeParams){Contract.Assert(tvar != null);
+ bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));}
}
// extract the values of type variables from the term variables
- List<VCExprVar!>! UtypedVars = new List<VCExprVar!> (oldBoundVars.Count);
- List<Type!>! originalTypes = new List<Type!> (oldBoundVars.Count);
+ List<VCExprVar/*!*/>/*!*/ UtypedVars = new List<VCExprVar/*!*/> (oldBoundVars.Count);
+ List<Type/*!*/>/*!*/ originalTypes = new List<Type/*!*/> (oldBoundVars.Count);
foreach (VCExprVar var in oldBoundVars) {
- VCExprVar! newVar = bindings.VCExprVarBindings[var];
+ VCExprVar/*!*/ newVar = bindings.VCExprVarBindings[var];
if (newVar.Type.Equals(U)) {
UtypedVars.Add(newVar);
originalTypes.Add(var.Type);
@@ -163,16 +204,20 @@ namespace Microsoft.Boogie.TypeErasure
}
- public VCExpr! AddTypePremisses(List<VCExprLetBinding!>! typeVarBindings,
- VCExpr! typePremisses, bool universal,
- VCExpr! body) {
- VCExpr! bodyWithPremisses;
+ public VCExpr/*!*/ AddTypePremisses(List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings,
+ VCExpr/*!*/ typePremisses, bool universal,
+ VCExpr/*!*/ body) {Contract.Requires(cce.NonNullElements(typeVarBindings));
+ Contract.Requires(typePremisses != null);
+ Contract.Requires(body != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr/*!*/ bodyWithPremisses;
if (universal)
bodyWithPremisses = Gen.ImpliesSimp(typePremisses, body);
else
bodyWithPremisses = Gen.AndSimp(typePremisses, body);
- return Gen.Let(typeVarBindings, bodyWithPremisses);
+ return Gen.Let(typeVarBindings, bodyWithPremisses);
}
@@ -181,12 +226,19 @@ namespace Microsoft.Boogie.TypeErasure
// term variables. E.g., for a function f<a>(x : C a), we would extract the
// instantiation of "a" by looking at the concrete type of "x".
- public List<VCExprLetBinding!>!
- BestTypeVarExtractors(List<TypeVariable!>! vars, List<Type!>! types,
- List<VCExprVar!>! concreteTypeSources,
- VariableBindings! bindings) {
- List<VCExprLetBinding!>! typeParamBindings = new List<VCExprLetBinding!> ();
- foreach (TypeVariable! var in vars) {
+ public List<VCExprLetBinding/*!*/>/*!*/
+ BestTypeVarExtractors(List<TypeVariable/*!*/>/*!*/ vars, List<Type/*!*/>/*!*/ types,
+ List<VCExprVar/*!*/>/*!*/ concreteTypeSources,
+ VariableBindings/*!*/ bindings) {
+ Contract.Requires(cce.NonNullElements(vars));
+ Contract.Requires(cce.NonNullElements(types));
+ Contract.Requires(cce.NonNullElements(concreteTypeSources));
+ Contract.Requires(bindings != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
+
+ List<VCExprLetBinding/*!*/>/*!*/ typeParamBindings = new List<VCExprLetBinding/*!*/> ();
+ foreach (TypeVariable/*!*/ var in vars) {
+ Contract.Assert(var != null);
VCExpr extractor = BestTypeVarExtractor(var, types, concreteTypeSources);
if (extractor != null)
typeParamBindings.Add(
@@ -196,9 +248,12 @@ namespace Microsoft.Boogie.TypeErasure
return typeParamBindings;
}
- private VCExpr BestTypeVarExtractor(TypeVariable! var, List<Type!>! types,
- List<VCExprVar!>! concreteTypeSources) {
- List<VCExpr!> allExtractors = TypeVarExtractors(var, types, concreteTypeSources);
+ private VCExpr BestTypeVarExtractor(TypeVariable/*!*/ var, List<Type/*!*/>/*!*/ types,
+ List<VCExprVar/*!*/>/*!*/ concreteTypeSources) {Contract.Requires(var != null);
+ Contract.Requires(cce.NonNullElements(types));
+ Contract.Requires(cce.NonNullElements(concreteTypeSources));
+ List<VCExpr/*!*/> allExtractors = TypeVarExtractors(var, types, concreteTypeSources);
+ Contract.Assert(cce.NonNullElements(allExtractors));
if (allExtractors.Count == 0)
return null;
@@ -215,18 +270,26 @@ namespace Microsoft.Boogie.TypeErasure
return bestExtractor;
}
- private List<VCExpr!>! TypeVarExtractors(TypeVariable! var, List<Type!>! types,
- List<VCExprVar!>! concreteTypeSources)
- requires types.Count == concreteTypeSources.Count; {
- List<VCExpr!>! res = new List<VCExpr!>();
+ private List<VCExpr/*!*/>/*!*/ TypeVarExtractors(TypeVariable/*!*/ var, List<Type/*!*/>/*!*/ types,
+ List<VCExprVar/*!*/>/*!*/ concreteTypeSources)
+ {
+ Contract.Requires(var != null);
+ Contract.Requires(cce.NonNullElements(types));
+ Contract.Requires(cce.NonNullElements(concreteTypeSources));
+ Contract.Requires((types.Count == concreteTypeSources.Count));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+ List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
for (int i = 0; i < types.Count; ++i)
TypeVarExtractors(var, types[i], TypeOf(concreteTypeSources[i]), res);
return res;
}
- private void TypeVarExtractors(TypeVariable! var, Type! completeType,
- VCExpr! innerTerm, List<VCExpr!>! extractors) {
+ private void TypeVarExtractors(TypeVariable var, Type completeType, VCExpr innerTerm, List<VCExpr/*!*/>/*!*/ extractors){
+Contract.Requires(innerTerm != null);
+Contract.Requires(completeType != null);
+Contract.Requires(var != null);
+Contract.Requires(cce.NonNullElements(extractors));
if (completeType.IsVariable) {
if (var.Equals(completeType)) {
extractors.Add(innerTerm);
@@ -234,13 +297,14 @@ namespace Microsoft.Boogie.TypeErasure
} else if (completeType.IsBasic) {
// nothing
} else if (completeType.IsCtor) {
- CtorType! ctorType = completeType.AsCtor;
+ CtorType/*!*/ ctorType = completeType.AsCtor;
if (ctorType.Arguments.Length > 0) {
// otherwise there are no chances of extracting any
// instantiations from this type
TypeCtorRepr repr = GetTypeCtorReprStruct(ctorType.Decl);
for (int i = 0; i < ctorType.Arguments.Length; ++i) {
- VCExpr! newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
+ VCExpr/*!*/ newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
+ Contract.Assert(newInnerTerm != null);
TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors);
}
}
@@ -256,21 +320,28 @@ namespace Microsoft.Boogie.TypeErasure
// Symbols for representing functions
// Globally defined functions
- private readonly IDictionary<Function!, UntypedFunction>! Typed2UntypedFunctions;
+ private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
+void Typed2UntypedFunctionsInvariantMethod(){
+Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));}
// distinguish between implicit and explicit type parameters
- internal static void SeparateTypeParams(List<Type!>! valueArgumentTypes,
- TypeVariableSeq! allTypeParams,
- out List<TypeVariable!>! implicitParams,
- out List<TypeVariable!>! explicitParams) {
- TypeVariableSeq! varsInInParamTypes = new TypeVariableSeq ();
- foreach (Type! t in valueArgumentTypes)
- varsInInParamTypes.AppendWithoutDups(t.FreeVariables);
-
- implicitParams = new List<TypeVariable!> (allTypeParams.Length);
- explicitParams = new List<TypeVariable!> (allTypeParams.Length);
-
- foreach (TypeVariable! var in allTypeParams) {
+ internal static void SeparateTypeParams(List<Type/*!*/>/*!*/ valueArgumentTypes,
+ TypeVariableSeq/*!*/ allTypeParams,
+ out List<TypeVariable/*!*/>/*!*/ implicitParams,
+ out List<TypeVariable/*!*/>/*!*/ explicitParams) {
+ Contract.Requires(cce.NonNullElements(valueArgumentTypes));
+Contract.Requires(allTypeParams != null);
+Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitParams)));
+Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)));
+ TypeVariableSeq/*!*/ varsInInParamTypes = new TypeVariableSeq ();
+ foreach (Type/*!*/ t in valueArgumentTypes){Contract.Assert(t != null);
+ varsInInParamTypes.AppendWithoutDups(t.FreeVariables);}
+
+ implicitParams = new List<TypeVariable/*!*/> (allTypeParams.Length);
+ explicitParams = new List<TypeVariable/*!*/> (allTypeParams.Length);
+
+ foreach (TypeVariable/*!*/ var in allTypeParams) {
+ Contract.Assert(var != null);
if (varsInInParamTypes.Has(var))
implicitParams.Add(var);
else
@@ -278,39 +349,43 @@ namespace Microsoft.Boogie.TypeErasure
}
implicitParams.TrimExcess();
- explicitParams.TrimExcess();
+ explicitParams.TrimExcess();
}
- internal UntypedFunction Typed2Untyped(Function! fun) {
+ internal UntypedFunction Typed2Untyped(Function fun) {
+ Contract.Requires(fun != null);
UntypedFunction res;
if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
- assert fun.OutParams.Length == 1;
+ Contract.Assert(fun.OutParams.Length == 1);
// if all of the parameters are int or bool, the function does
// not have to be changed
- if (forall{Formal f in fun.InParams; UnchangedType(((!)f).TypedIdent.Type)} &&
- UnchangedType(((!)fun.OutParams[0]).TypedIdent.Type) &&
+ if (Contract.ForAll(0,fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
+ UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&
fun.TypeParameters.Length == 0) {
- res = new UntypedFunction(fun, new List<TypeVariable!> (), new List<TypeVariable!> ());
+ res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());
} else {
- List<Type!>! argTypes = new List<Type!> ();
- foreach (Variable! v in fun.InParams)
+ List<Type/*!*/>/*!*/ argTypes = new List<Type/*!*/>();
+ foreach (Variable/*!*/ v in fun.InParams) {
+ Contract.Assert(v != null);
argTypes.Add(v.TypedIdent.Type);
+ }
- List<TypeVariable!>! implicitParams, explicitParams;
+ List<TypeVariable/*!*/>/*!*/ implicitParams, explicitParams;
SeparateTypeParams(argTypes, fun.TypeParameters, out implicitParams, out explicitParams);
- Type[]! types = new Type [explicitParams.Count + fun.InParams.Length + 1];
+ Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Length + 1];
int i = 0;
for (int j = 0; j < explicitParams.Count; ++j) {
types[i] = T;
i = i + 1;
}
for (int j = 0; j < fun.InParams.Length; ++i, ++j)
- types[i] = TypeAfterErasure(((!)fun.InParams[j]).TypedIdent.Type);
- types[types.Length - 1] = TypeAfterErasure(((!)fun.OutParams[0]).TypedIdent.Type);
+ types[i] = TypeAfterErasure(cce.NonNull(fun.InParams[j]).TypedIdent.Type);
+ types[types.Length - 1] = TypeAfterErasure(cce.NonNull(fun.OutParams[0]).TypedIdent.Type);
- Function! untypedFun = HelperFuns.BoogieFunction(fun.Name, types);
+ Function/*!*/ untypedFun = HelperFuns.BoogieFunction(fun.Name, types);
+ Contract.Assert(untypedFun != null);
untypedFun.Attributes = fun.Attributes;
res = new UntypedFunction(untypedFun, implicitParams, explicitParams);
if (U.Equals(types[types.Length - 1]))
@@ -322,60 +397,75 @@ namespace Microsoft.Boogie.TypeErasure
return res;
}
- private VCExpr! GenFunctionAxiom(UntypedFunction fun, Function! originalFun) {
- List<Type!>! originalInTypes = new List<Type!> (originalFun.InParams.Length);
- foreach (Formal! f in originalFun.InParams)
+ private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun){
+Contract.Requires(originalFun != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+ List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/> (originalFun.InParams.Length);
+ foreach (Formal/*!*/ f in originalFun.InParams)
originalInTypes.Add(f.TypedIdent.Type);
return GenFunctionAxiom(fun.Fun, fun.ImplicitTypeParams, fun.ExplicitTypeParams,
originalInTypes,
- ((!)originalFun.OutParams[0]).TypedIdent.Type);
+ cce.NonNull(originalFun.OutParams[0]).TypedIdent.Type);
}
- internal VCExpr! GenFunctionAxiom(Function! fun,
- List<TypeVariable!>! implicitTypeParams,
- List<TypeVariable!>! explicitTypeParams,
- List<Type!>! originalInTypes,
- Type! originalResultType)
- requires originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Length;
+ internal VCExpr/*!*/ GenFunctionAxiom(Function/*!*/ fun,
+ List<TypeVariable/*!*/>/*!*/ implicitTypeParams,
+ List<TypeVariable/*!*/>/*!*/ explicitTypeParams,
+ List<Type/*!*/>/*!*/ originalInTypes,
+ Type/*!*/ originalResultType)
{
+ Contract.Requires(cce.NonNullElements(implicitTypeParams));
+ Contract.Requires(fun != null);
+ Contract.Requires(cce.NonNullElements(explicitTypeParams));
+ Contract.Requires(cce.NonNullElements(originalInTypes));
+ Contract.Requires(originalResultType != null);
+ Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Length);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
return VCExpressionGenerator.True;
}
- List<VCExprVar!>! typedInputVars = new List<VCExprVar!>(originalInTypes.Count);
+ List<VCExprVar/*!*/>/*!*/ typedInputVars = new List<VCExprVar/*!*/>(originalInTypes.Count);
int i = 0;
- foreach (Type! t in originalInTypes) {
+ foreach (Type/*!*/ t in originalInTypes) {Contract.Assert(t != null);
typedInputVars.Add(Gen.Variable("arg" + i, t));
i = i + 1;
}
- VariableBindings! bindings = new VariableBindings ();
+ VariableBindings/*!*/ bindings = new VariableBindings ();
// type parameters that have to be given explicitly are replaced
// with universally quantified type variables
- List<VCExprVar!>! boundVars = new List<VCExprVar!> (explicitTypeParams.Count + typedInputVars.Count);
- foreach (TypeVariable! var in explicitTypeParams) {
- VCExprVar! newVar = Gen.Variable(var.Name, T);
+ List<VCExprVar/*!*/>/*!*/ boundVars = new List<VCExprVar/*!*/> (explicitTypeParams.Count + typedInputVars.Count);
+ foreach (TypeVariable/*!*/ var in explicitTypeParams) {Contract.Assert(var != null);
+ VCExprVar/*!*/ newVar = Gen.Variable(var.Name, T);
boundVars.Add(newVar);
bindings.TypeVariableBindings.Add(var, newVar);
}
// bound term variables are replaced with bound term variables typed in
// a simpler way
- foreach (VCExprVar! var in typedInputVars) {
- Type! newType = TypeAfterErasure(var.Type);
- VCExprVar! newVar = Gen.Variable(var.Name, newType);
+ foreach(VCExprVar/*!*/ var in typedInputVars){
+ Contract.Assert(var != null);
+ Type/*!*/ newType = TypeAfterErasure(var.Type);
+ Contract.Assert(newType != null);
+ VCExprVar/*!*/ newVar = Gen.Variable(var.Name, newType);
+ Contract.Assert(newVar != null);
boundVars.Add(newVar);
bindings.VCExprVarBindings.Add(var, newVar);
}
- List<VCExprLetBinding!> typeVarBindings =
+ List<VCExprLetBinding/*!*/> typeVarBindings =
GenTypeParamBindings(implicitTypeParams, typedInputVars, bindings, true);
+ Contract.Assert(cce.NonNullElements(typeVarBindings));
- VCExpr! funApp = Gen.Function(fun, HelperFuns.ToVCExprList(boundVars));
- VCExpr! conclusion = Gen.Eq(TypeOf(funApp),
+ VCExpr/*!*/ funApp = Gen.Function(fun, HelperFuns.ToVCExprList(boundVars));
+ Contract.Assert(funApp != null);
+ VCExpr/*!*/ conclusion = Gen.Eq(TypeOf(funApp),
Type2Term(originalResultType, bindings.TypeVariableBindings));
+ Contract.Assert(conclusion != null);
VCExpr conclusionWithPremisses =
// leave out antecedents of function type axioms ... they don't appear necessary,
// because a function can always be extended to all U-values (right?)
@@ -383,7 +473,8 @@ namespace Microsoft.Boogie.TypeErasure
Gen.Let(typeVarBindings, conclusion);
if (boundVars.Count > 0) {
- List<VCTrigger!> triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
+ List<VCTrigger/*!*/> triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
+ Contract.Assert(cce.NonNullElements(triggers));
return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, conclusionWithPremisses);
} else {
return conclusionWithPremisses;
@@ -392,17 +483,23 @@ namespace Microsoft.Boogie.TypeErasure
////////////////////////////////////////////////////////////////////////////
- protected override void AddVarTypeAxiom(VCExprVar! var, Type! originalType) {
+ protected override void AddVarTypeAxiom(VCExprVar var, Type originalType){
+Contract.Requires(originalType != null);
+Contract.Requires(var != null);
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;
AddTypeAxiom(GenVarTypeAxiom(var, originalType,
// we don't have any bindings available
- new Dictionary<TypeVariable!, VCExpr!> ()));
+ new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()));
}
- public VCExpr! GenVarTypeAxiom(VCExprVar! var, Type! originalType,
- IDictionary<TypeVariable!, VCExpr!>! varMapping) {
+ public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
+ Contract.Requires(var != null);
+ Contract.Requires(originalType != null);
+ Contract.Requires(cce.NonNullElements(varMapping));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
if (!var.Type.Equals(originalType)) {
- VCExpr! typeRepr = Type2Term(originalType, varMapping);
+ VCExpr/*!*/ typeRepr = Type2Term(originalType, varMapping);
return Gen.Eq(TypeOf(var), typeRepr);
}
return VCExpressionGenerator.True;
@@ -413,19 +510,26 @@ namespace Microsoft.Boogie.TypeErasure
internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder {
- private readonly TypeAxiomBuilderPremisses! AxBuilderPremisses;
+ private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(AxBuilderPremisses != null);
+ }
- internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses! axBuilder,
- VCExpressionGenerator! gen) {
- base(axBuilder, gen);
+
+ internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen) :base(axBuilder, gen){
+ Contract.Requires(gen != null);
+ Contract.Requires(axBuilder != null);
+
this.AxBuilderPremisses = axBuilder;
}
// constructor for cloning
- internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses! axBuilder,
- VCExpressionGenerator! gen,
- MapTypeAbstractionBuilderPremisses! builder) {
- base(axBuilder, gen, builder);
+ internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen, MapTypeAbstractionBuilderPremisses builder):base(axBuilder, gen, builder) {
+ Contract.Requires(builder != null);
+ Contract.Requires(gen != null);
+ Contract.Requires(axBuilder != null);
+
this.AxBuilderPremisses = axBuilder;
}
@@ -437,96 +541,122 @@ namespace Microsoft.Boogie.TypeErasure
// map). These parameters are given as a list of indexes sorted in
// ascending order; the index i refers to the i'th bound variable
// in a type <a0, a1, ..., an>[...]...
- public List<int>! ExplicitSelectTypeParams(MapType! type) {
+ public List<int>/*!*/ ExplicitSelectTypeParams(MapType type) {
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result<List<int>>() != null);
+
List<int> res;
if (!explicitSelectTypeParamsCache.TryGetValue(type, out res)) {
- List<TypeVariable!>! explicitParams, implicitParams;
+ List<TypeVariable/*!*/>/*!*/ explicitParams, implicitParams;
TypeAxiomBuilderPremisses.SeparateTypeParams(type.Arguments.ToList(),
type.TypeParameters,
out implicitParams,
out explicitParams);
- res = new List<int> (explicitParams.Count);
- foreach (TypeVariable! var in explicitParams)
+ res = new List<int>(explicitParams.Count);
+ foreach (TypeVariable/*!*/ var in explicitParams) {
+ Contract.Assert(var != null);
res.Add(type.TypeParameters.IndexOf(var));
+ }
explicitSelectTypeParamsCache.Add(type, res);
}
- return (!)res;
+ return cce.NonNull(res);
+ }
+
+ private IDictionary<MapType/*!*/, List<int>/*!*/>/*!*/ explicitSelectTypeParamsCache =
+ new Dictionary<MapType/*!*/, List<int>/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvarant() {
+ Contract.Invariant(cce.NonNullElements(explicitSelectTypeParamsCache));
}
- private IDictionary<MapType!, List<int>!>! explicitSelectTypeParamsCache =
- new Dictionary<MapType!, List<int>!> ();
////////////////////////////////////////////////////////////////////////////
- protected override void GenSelectStoreFunctions(MapType! abstractedType,
- TypeCtorDecl! synonym,
- out Function! select,
- out Function! store) {
- Type! mapTypeSynonym;
- List<TypeVariable!>! typeParams;
- List<Type!>! originalInTypes;
+ protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonym, out Function/*!*/ select, out Function/*!*/ store) {
+ Contract.Requires(synonym != null);
+ Contract.Requires(abstractedType != null);
+ Contract.Ensures(Contract.ValueAtReturn(out select) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
+ Type/*!*/ mapTypeSynonym;
+ List<TypeVariable/*!*/>/*!*/ typeParams;
+ List<Type/*!*/>/*!*/ originalInTypes;
GenTypeAxiomParams(abstractedType, synonym, out mapTypeSynonym,
out typeParams, out originalInTypes);
// select
- List<TypeVariable!>! explicitSelectParams, implicitSelectParams;
+ List<TypeVariable/*!*/>/*!*/ explicitSelectParams, implicitSelectParams;
select = CreateAccessFun(typeParams, originalInTypes,
abstractedType.Result, synonym.Name + "Select",
out implicitSelectParams, out explicitSelectParams);
-
+
// store, which gets one further argument: the assigned rhs
originalInTypes.Add(abstractedType.Result);
- List<TypeVariable!>! explicitStoreParams, implicitStoreParams;
+ List<TypeVariable/*!*/>/*!*/ explicitStoreParams, implicitStoreParams;
store = CreateAccessFun(typeParams, originalInTypes,
mapTypeSynonym, synonym.Name + "Store",
out implicitStoreParams, out explicitStoreParams);
- // the store function does not have any explicit type parameters
- assert explicitStoreParams.Count == 0;
-
+ // the store function does not have any explicit type parameters
+ Contract.Assert(explicitStoreParams.Count == 0);
+
if (CommandLineOptions.Clo.UseArrayTheory) {
select.AddAttribute("builtin", "select");
store.AddAttribute("builtin", "store");
- } else {
+ } else {
AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
abstractedType.Result,
implicitSelectParams, explicitSelectParams,
originalInTypes));
- AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,
+ AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,
abstractedType.Result,
explicitSelectParams));
}
}
- protected void GenTypeAxiomParams(MapType! abstractedType, TypeCtorDecl! synonymDecl,
- out Type! mapTypeSynonym,
- out List<TypeVariable!>! typeParams,
- out List<Type!>! originalIndexTypes) {
- typeParams = new List<TypeVariable!> (abstractedType.TypeParameters.Length + abstractedType.FreeVariables.Length);
+ protected void GenTypeAxiomParams(MapType/*!*/ abstractedType, TypeCtorDecl/*!*/ synonymDecl,
+ out Type/*!*/ mapTypeSynonym,
+ out List<TypeVariable/*!*/>/*!*/ typeParams,
+ out List<Type/*!*/>/*!*/ originalIndexTypes) {
+ Contract.Requires(abstractedType != null);
+ Contract.Requires(synonymDecl != null);
+ Contract.Ensures(Contract.ValueAtReturn(out mapTypeSynonym) != null);
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out typeParams)));
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out originalIndexTypes)));
+ typeParams = new List<TypeVariable/*!*/>(abstractedType.TypeParameters.Length + abstractedType.FreeVariables.Length);
typeParams.AddRange(abstractedType.TypeParameters.ToList());
typeParams.AddRange(abstractedType.FreeVariables.ToList());
- originalIndexTypes = new List<Type!> (abstractedType.Arguments.Length + 1);
- TypeSeq! mapTypeParams = new TypeSeq ();
- foreach (TypeVariable! var in abstractedType.FreeVariables)
+ originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Length + 1);
+ TypeSeq/*!*/ mapTypeParams = new TypeSeq();
+ foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {
+ Contract.Assert(var != null);
mapTypeParams.Add(var);
-
+ }
+
if (CommandLineOptions.Clo.UseArrayTheory)
mapTypeSynonym = abstractedType;
- else
- mapTypeSynonym = new CtorType (Token.NoToken, synonymDecl, mapTypeParams);
-
+ else
+ mapTypeSynonym = new CtorType(Token.NoToken, synonymDecl, mapTypeParams);
+
originalIndexTypes.Add(mapTypeSynonym);
originalIndexTypes.AddRange(abstractedType.Arguments.ToList());
}
// method to actually create the select or store function
- private Function! CreateAccessFun(List<TypeVariable!>! originalTypeParams,
- List<Type!>! originalInTypes,
- Type! originalResult,
- string! name,
- out List<TypeVariable!>! implicitTypeParams, out List<TypeVariable!>! explicitTypeParams) {
+ private Function/*!*/ CreateAccessFun(List<TypeVariable/*!*/>/*!*/ originalTypeParams,
+ List<Type/*!*/>/*!*/ originalInTypes,
+ Type/*!*/ originalResult,
+ string/*!*/ name,
+ out List<TypeVariable/*!*/>/*!*/ implicitTypeParams, out List<TypeVariable/*!*/>/*!*/ explicitTypeParams) {
+ Contract.Requires(cce.NonNullElements(originalTypeParams));
+ Contract.Requires(cce.NonNullElements(originalInTypes));
+ Contract.Requires(originalResult != null);
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result<Function>() != null);
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitTypeParams)));
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitTypeParams)));
+
// select and store are basically handled like normal functions: the type
// parameters are split into the implicit parameters, and into the parameters
// that have to be given explicitly
@@ -534,28 +664,28 @@ namespace Microsoft.Boogie.TypeErasure
HelperFuns.ToSeq(originalTypeParams),
out implicitTypeParams,
out explicitTypeParams);
-
- Type[]! ioTypes = new Type [explicitTypeParams.Count + originalInTypes.Count + 1];
+
+ Type[]/*!*/ ioTypes = new Type[explicitTypeParams.Count + originalInTypes.Count + 1];
int i = 0;
for (; i < explicitTypeParams.Count; ++i)
ioTypes[i] = AxBuilder.T;
- foreach (Type! type in originalInTypes)
- {
+ foreach (Type/*!*/ type in originalInTypes) {
+ Contract.Assert(type != null);
if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type))
- ioTypes[i] = type;
+ ioTypes[i] = type;
else
- ioTypes[i] = AxBuilder.U;
+ ioTypes[i] = AxBuilder.U;
i++;
}
if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(originalResult))
ioTypes[i] = originalResult;
else
ioTypes[i] = AxBuilder.U;
-
- Function! res = HelperFuns.BoogieFunction(name, ioTypes);
- if (AxBuilder.U.Equals(ioTypes[i]))
- {
+ Function/*!*/ res = HelperFuns.BoogieFunction(name, ioTypes);
+ Contract.Assert(res != null);
+
+ if (AxBuilder.U.Equals(ioTypes[i])) {
AxBuilder.AddTypeAxiom(
AxBuilderPremisses.GenFunctionAxiom(res,
implicitTypeParams, explicitTypeParams,
@@ -567,26 +697,34 @@ namespace Microsoft.Boogie.TypeErasure
///////////////////////////////////////////////////////////////////////////
// The normal axioms of the theory of arrays (without extensionality)
- private VCExpr! Select(Function! select,
- // in general, the select function has to
- // receive explicit type parameters (which
- // are here already represented as VCExpr
- // of type T)
- List<VCExpr!>! typeParams,
- VCExpr! map,
- List<VCExprVar!>! indexes) {
- List<VCExpr!>! selectArgs = new List<VCExpr!> (typeParams.Count + indexes.Count + 1);
+ private VCExpr/*!*/ Select(Function/*!*/ select,
+ // in general, the select function has to
+ // receive explicit type parameters (which
+ // are here already represented as VCExpr
+ // of type T)
+ List<VCExpr/*!*/>/*!*/ typeParams,
+ VCExpr/*!*/ map,
+ List<VCExprVar/*!*/>/*!*/ indexes) {
+ Contract.Requires(select != null);
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Requires(map != null);
+ Contract.Requires(cce.NonNullElements(indexes));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ List<VCExpr/*!*/>/*!*/ selectArgs = new List<VCExpr/*!*/>(typeParams.Count + indexes.Count + 1);
selectArgs.AddRange(typeParams);
selectArgs.Add(map);
selectArgs.AddRange(HelperFuns.ToVCExprList(indexes));
return Gen.Function(select, selectArgs);
}
- private VCExpr! Store(Function! store,
- VCExpr! map,
- List<VCExprVar!>! indexes,
- VCExpr! val) {
- List<VCExpr!>! storeArgs = new List<VCExpr!> (indexes.Count + 2);
+ private VCExpr Store(Function store, VCExpr map, List<VCExprVar/*!*/>/*!*/ indexes, VCExpr val) {
+ Contract.Requires(val != null);
+ Contract.Requires(map != null);
+ Contract.Requires(store != null);
+ Contract.Requires(cce.NonNullElements(indexes));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ List<VCExpr/*!*/>/*!*/ storeArgs = new List<VCExpr/*!*/>(indexes.Count + 2);
storeArgs.Add(map);
storeArgs.AddRange(HelperFuns.ToVCExprList(indexes));
storeArgs.Add(val);
@@ -600,14 +738,17 @@ namespace Microsoft.Boogie.TypeErasure
/// select(store(m, indexes, val), indexes) == val)
/// where the quantifier body is also enclosed in a let that defines portions of T, if needed.
/// </summary>
- private VCExpr! GenMapAxiom0(Function! select, Function! store,
- Type! mapResult,
- List<TypeVariable!>! implicitTypeParamsSelect, List<TypeVariable!>! explicitTypeParamsSelect,
- List<Type!>! originalInTypes)
- {
+ private VCExpr GenMapAxiom0(Function select, Function store, Type mapResult, List<TypeVariable/*!*/>/*!*/ implicitTypeParamsSelect, List<TypeVariable/*!*/>/*!*/ explicitTypeParamsSelect, List<Type/*!*/>/*!*/ originalInTypes) {
+ Contract.Requires(mapResult != null);
+ Contract.Requires(store != null);
+ Contract.Requires(select != null);
+ Contract.Requires(cce.NonNullElements(implicitTypeParamsSelect));
+ Contract.Requires(cce.NonNullElements(originalInTypes));
+ Contract.Requires(cce.NonNullElements(explicitTypeParamsSelect));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
int arity = store.InParams.Length - 2;
- List<VCExprVar!> inParams = new List<VCExprVar!>();
- List<VCExprVar!> quantifiedVars = new List<VCExprVar!>(store.InParams.Length);
+ List<VCExprVar/*!*/> inParams = new List<VCExprVar/*!*/>();
+ List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Length);
VariableBindings bindings = new VariableBindings();
// bound variable: m
@@ -618,16 +759,18 @@ namespace Microsoft.Boogie.TypeErasure
bindings.VCExprVarBindings.Add(typedM, m);
// bound variables: indexes
- List<Type!> origIndexTypes = new List<Type!>(arity);
- List<Type!> indexTypes = new List<Type!>(arity);
- for (int i = 1; i < store.InParams.Length-1; i++) {
+ List<Type/*!*/> origIndexTypes = new List<Type/*!*/>(arity);
+ List<Type/*!*/> indexTypes = new List<Type/*!*/>(arity);
+ for (int i = 1; i < store.InParams.Length - 1; i++) {
origIndexTypes.Add(originalInTypes[i]);
- indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type);
+ indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);
}
- assert arity == indexTypes.Count;
- List<VCExprVar!> typedArgs = HelperFuns.VarVector("arg", origIndexTypes, Gen);
- List<VCExprVar!> indexes = HelperFuns.VarVector("x", indexTypes, Gen);
- assert typedArgs.Count == indexes.Count;
+ Contract.Assert(arity == indexTypes.Count);
+ List<VCExprVar/*!*/> typedArgs = HelperFuns.VarVector("arg", origIndexTypes, Gen);
+ Contract.Assert(cce.NonNullElements(typedArgs));
+ List<VCExprVar/*!*/> indexes = HelperFuns.VarVector("x", indexTypes, Gen);
+ Contract.Assert(cce.NonNullElements(indexes));
+ Contract.Assert(typedArgs.Count == indexes.Count);
inParams.AddRange(typedArgs);
quantifiedVars.AddRange(indexes);
for (int i = 0; i < arity; i++) {
@@ -636,7 +779,7 @@ namespace Microsoft.Boogie.TypeErasure
// bound variable: val
VCExprVar typedVal = Gen.Variable("val", mapResult);
- VCExprVar val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);
+ VCExprVar val = Gen.Variable("val", cce.NonNull(select.OutParams[0]).TypedIdent.Type);
quantifiedVars.Add(val);
bindings.VCExprVarBindings.Add(typedVal, val);
@@ -645,7 +788,7 @@ namespace Microsoft.Boogie.TypeErasure
VCExprVar tVar = Gen.Variable(tp.Name, AxBuilderPremisses.T);
bindings.TypeVariableBindings.Add(tp, tVar);
}
- List<VCExpr!> typeParams = new List<VCExpr!>(explicitTypeParamsSelect.Count);
+ List<VCExpr/*!*/> typeParams = new List<VCExpr/*!*/>(explicitTypeParamsSelect.Count);
foreach (TypeVariable tp in explicitTypeParamsSelect) {
VCExprVar tVar = Gen.Variable(tp.Name, AxBuilderPremisses.T);
bindings.TypeVariableBindings.Add(tp, tVar);
@@ -653,108 +796,134 @@ namespace Microsoft.Boogie.TypeErasure
typeParams.Add(tVar);
}
- VCExpr! storeExpr = Store(store, m, indexes, val);
- VCExpr! selectExpr = Select(select, typeParams, storeExpr, indexes);
+ VCExpr/*!*/ storeExpr = Store(store, m, indexes, val);
+ Contract.Assert(storeExpr != null);
+ VCExpr/*!*/ selectExpr = Select(select, typeParams, storeExpr, indexes);
+ Contract.Assert(selectExpr != null);
// Create let-binding definitions for all type parameters.
// The implicit ones can be phrased in terms of the types of the ordinary in-parameters, and
// we want to make sure that they don't get phrased in terms of the out-parameter, so we pass
// in inParams here.
- List<VCExprLetBinding!> letBindings_Implicit =
+ List<VCExprLetBinding/*!*/> letBindings_Implicit =
AxBuilderPremisses.GenTypeParamBindings(implicitTypeParamsSelect, inParams, bindings, false);
+ Contract.Assert(cce.NonNullElements(letBindings_Implicit));
// The explicit ones, by definition, can only be phrased in terms of the result, so we pass
// in List(typedVal) here.
- List<VCExprLetBinding!> letBindings_Explicit =
+ List<VCExprLetBinding/*!*/> letBindings_Explicit =
AxBuilderPremisses.GenTypeParamBindings(explicitTypeParamsSelect, HelperFuns.ToList(typedVal), bindings, false);
+ Contract.Assert(cce.NonNullElements(letBindings_Explicit));
// generate: select(store(m, indices, val)) == val
- VCExpr! eq = Gen.Eq(selectExpr, val);
+ VCExpr/*!*/ eq = Gen.Eq(selectExpr, val);
+ Contract.Assert(eq != null);
// generate: type(val) == T, where T is the type of val
- VCExpr! ante = Gen.Eq(
+ VCExpr/*!*/ ante = Gen.Eq(
AxBuilderPremisses.TypeOf(val),
AxBuilderPremisses.Type2Term(mapResult, bindings.TypeVariableBindings));
+ Contract.Assert(ante != null);
VCExpr body;
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None ||
- !AxBuilder.U.Equals(((!)select.OutParams[0]).TypedIdent.Type))
- {
+ !AxBuilder.U.Equals(cce.NonNull(select.OutParams[0]).TypedIdent.Type)) {
body = Gen.Let(letBindings_Explicit, eq);
} else {
body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq)));
}
- return Gen.Forall(quantifiedVars, new List<VCTrigger!>(), "mapAx0:" + select.Name, body);
+ return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, body);
}
- private VCExpr! GenMapAxiom1(Function! select, Function! store,
- Type! mapResult,
- List<TypeVariable!>! explicitSelectParams) {
+ private VCExpr GenMapAxiom1(Function select, Function store, Type mapResult, List<TypeVariable/*!*/>/*!*/ explicitSelectParams) {
+ Contract.Requires(mapResult != null);
+ Contract.Requires(store != null);
+ Contract.Requires(select != null);
+ Contract.Requires(cce.NonNullElements(explicitSelectParams));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
int arity = store.InParams.Length - 2;
- List<Type!> indexTypes = new List<Type!>();
- for (int i = 1; i < store.InParams.Length-1; i++)
- {
- indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type);
+ List<Type/*!*/> indexTypes = new List<Type/*!*/>();
+ for (int i = 1; i < store.InParams.Length - 1; i++) {
+ indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);
}
- assert indexTypes.Count == arity;
-
- List<VCExprVar!>! indexes0 = HelperFuns.VarVector("x", indexTypes, Gen);
- List<VCExprVar!>! indexes1 = HelperFuns.VarVector("y", indexTypes, Gen);
- VCExprVar! m = Gen.Variable("m", AxBuilder.U);
- VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);
+ Contract.Assert(indexTypes.Count == arity);
+
+ List<VCExprVar/*!*/>/*!*/ indexes0 = HelperFuns.VarVector("x", indexTypes, Gen);
+ Contract.Assert(cce.NonNullElements(indexes0));
+ List<VCExprVar/*!*/>/*!*/ indexes1 = HelperFuns.VarVector("y", indexTypes, Gen);
+ Contract.Assert(cce.NonNullElements(indexes1));
+ VCExprVar/*!*/ m = Gen.Variable("m", AxBuilder.U);
+ Contract.Assert(m != null);
+ VCExprVar/*!*/ val = Gen.Variable("val", cce.NonNull(select.OutParams[0]).TypedIdent.Type);
+ Contract.Assert(val != null);
// extract the explicit type parameters from the actual result type ...
- VCExprVar! typedVal = Gen.Variable("val", mapResult);
- VariableBindings! bindings = new VariableBindings ();
+ VCExprVar/*!*/ typedVal = Gen.Variable("val", mapResult);
+ Contract.Assert(typedVal != null);
+ VariableBindings/*!*/ bindings = new VariableBindings();
bindings.VCExprVarBindings.Add(typedVal, val);
- List<VCExprLetBinding!>! letBindings =
+ List<VCExprLetBinding/*!*/>/*!*/ letBindings =
AxBuilderPremisses.GenTypeParamBindings(explicitSelectParams,
HelperFuns.ToList(typedVal),
bindings, true);
+ Contract.Assert(cce.NonNullElements(letBindings));
// ... and quantify the introduced term variables for type
// parameters universally
- List<VCExprVar!>! typeParams = new List<VCExprVar!> (explicitSelectParams.Count);
- List<VCExpr!>! typeParamsExpr = new List<VCExpr!> (explicitSelectParams.Count);
- foreach (TypeVariable! var in explicitSelectParams) {
- VCExprVar! newVar = (VCExprVar)bindings.TypeVariableBindings[var];
+ List<VCExprVar/*!*/>/*!*/ typeParams = new List<VCExprVar/*!*/>(explicitSelectParams.Count);
+ List<VCExpr/*!*/>/*!*/ typeParamsExpr = new List<VCExpr/*!*/>(explicitSelectParams.Count);
+ foreach (TypeVariable/*!*/ var in explicitSelectParams) {
+ Contract.Assert(var != null);
+ VCExprVar/*!*/ newVar = (VCExprVar)bindings.TypeVariableBindings[var];
+ Contract.Assert(newVar != null);
typeParams.Add(newVar);
typeParamsExpr.Add(newVar);
}
- VCExpr! storeExpr = Store(store, m, indexes0, val);
- VCExpr! selectWithoutStoreExpr = Select(select, typeParamsExpr, m, indexes1);
- VCExpr! selectExpr = Select(select, typeParamsExpr, storeExpr, indexes1);
+ VCExpr/*!*/ storeExpr = Store(store, m, indexes0, val);
+ Contract.Assert(storeExpr != null);
+ VCExpr/*!*/ selectWithoutStoreExpr = Select(select, typeParamsExpr, m, indexes1);
+ Contract.Assert(selectWithoutStoreExpr != null);
+ VCExpr/*!*/ selectExpr = Select(select, typeParamsExpr, storeExpr, indexes1);
+ Contract.Assert(selectExpr != null);
- VCExpr! selectEq = Gen.Eq(selectExpr, selectWithoutStoreExpr);
+ VCExpr/*!*/ selectEq = Gen.Eq(selectExpr, selectWithoutStoreExpr);
+ Contract.Assert(selectEq != null);
- List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> (indexes0.Count + indexes1.Count + 2);
+ List<VCExprVar/*!*/>/*!*/ quantifiedVars = new List<VCExprVar/*!*/>(indexes0.Count + indexes1.Count + 2);
quantifiedVars.Add(val);
quantifiedVars.Add(m);
quantifiedVars.AddRange(indexes0);
quantifiedVars.AddRange(indexes1);
quantifiedVars.AddRange(typeParams);
- List<VCTrigger!>! triggers = new List<VCTrigger!> ();
+ List<VCTrigger/*!*/>/*!*/ triggers = new List<VCTrigger/*!*/>();
+ Contract.Assert(cce.NonNullElements(triggers));
- VCExpr! axiom = VCExpressionGenerator.True;
+ VCExpr/*!*/ axiom = VCExpressionGenerator.True;
+ Contract.Assert(axiom != null);
// first non-interference criterium: the queried location is
// different from the assigned location
for (int i = 0; i < arity; ++i) {
- VCExpr! indexesEq = Gen.Eq(indexes0[i], indexes1[i]);
- VCExpr! matrix = Gen.Or(indexesEq, selectEq);
- VCExpr! conjunct = Gen.Forall(quantifiedVars, triggers,
+ VCExpr/*!*/ indexesEq = Gen.Eq(indexes0[i], indexes1[i]);
+ VCExpr/*!*/ matrix = Gen.Or(indexesEq, selectEq);
+ VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers,
"mapAx1:" + select.Name + ":" + i, matrix);
+ Contract.Assert(indexesEq != null);
+ Contract.Assert(matrix != null);
+ Contract.Assert(conjunct != null);
axiom = Gen.AndSimp(axiom, conjunct);
}
// second non-interference criterion: the queried type is
// different from the assigned type
- VCExpr! typesEq = VCExpressionGenerator.True;
- foreach (VCExprLetBinding! b in letBindings)
+ VCExpr/*!*/ typesEq = VCExpressionGenerator.True;
+ foreach (VCExprLetBinding/*!*/ b in letBindings) {
+ Contract.Assert(b != null);
typesEq = Gen.AndSimp(typesEq, Gen.Eq(b.V, b.E));
- VCExpr! matrix2 = Gen.Or(typesEq, selectEq);
- VCExpr! conjunct2 = Gen.Forall(quantifiedVars, triggers,
+ }
+ VCExpr/*!*/ matrix2 = Gen.Or(typesEq, selectEq);
+ VCExpr/*!*/ conjunct2 = Gen.Forall(quantifiedVars, triggers,
"mapAx2:" + select.Name, matrix2);
axiom = Gen.AndSimp(axiom, conjunct2);
@@ -767,25 +936,35 @@ namespace Microsoft.Boogie.TypeErasure
public class TypeEraserPremisses : TypeEraser {
- private readonly TypeAxiomBuilderPremisses! AxBuilderPremisses;
+ private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(AxBuilderPremisses != null);
+}
+
private OpTypeEraser OpEraserAttr = null;
- protected override OpTypeEraser! OpEraser { get {
+ protected override OpTypeEraser/*!*/ OpEraser { get {Contract.Ensures(Contract.Result<OpTypeEraser>() != null);
+
if (OpEraserAttr == null)
OpEraserAttr = new OpTypeEraserPremisses(this, AxBuilderPremisses, Gen);
return OpEraserAttr;
} }
- public TypeEraserPremisses(TypeAxiomBuilderPremisses! axBuilder,
- VCExpressionGenerator! gen) {
- base(axBuilder, gen);
+ public TypeEraserPremisses(TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen):base(axBuilder, gen){
+Contract.Requires(gen != null);
+Contract.Requires(axBuilder != null);
+
this.AxBuilderPremisses = axBuilder;
}
////////////////////////////////////////////////////////////////////////////
- public override VCExpr! Visit(VCExprQuantifier! node,
- VariableBindings! oldBindings) {
+ public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings){
+Contract.Requires(oldBindings != null);
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
VariableBindings bindings = oldBindings.Clone();
// determine the bound vars that actually occur in the body or
@@ -796,11 +975,13 @@ namespace Microsoft.Boogie.TypeErasure
coll.Collect(node.Body);
foreach (VCTrigger trigger in node.Triggers) {
if (trigger.Pos)
- foreach (VCExpr! e in trigger.Exprs)
- coll.Collect(e);
+ foreach(VCExpr/*!*/ e in trigger.Exprs){
+Contract.Assert(e != null);
+
+ coll.Collect(e);}
}
- List<VCExprVar!> occurringVars = new List<VCExprVar!> (node.BoundVars.Count);
+ List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/> (node.BoundVars.Count);
foreach (VCExprVar var in node.BoundVars)
if (coll.FreeTermVars.ContainsKey(var))
occurringVars.Add(var);
@@ -809,15 +990,17 @@ namespace Microsoft.Boogie.TypeErasure
// bound term variables are replaced with bound term variables typed in
// a simpler way
- List<VCExprVar!>! newBoundVars =
+ List<VCExprVar/*!*/>/*!*/ newBoundVars =
BoundVarsAfterErasure(occurringVars, bindings);
- VCExpr! newNode = HandleQuantifier(node, occurringVars,
+ Contract.Assert(cce.NonNullElements(newBoundVars));
+ VCExpr/*!*/ newNode = HandleQuantifier(node, occurringVars,
newBoundVars, bindings);
+ Contract.Assert(newNode != null);
if (!(newNode is VCExprQuantifier) || !IsUniversalQuantifier(node))
return newNode;
- VariableBindings! bindings2;
+ VariableBindings bindings2;
if (!RedoQuantifier(node, (VCExprQuantifier)newNode, occurringVars, oldBindings,
out bindings2, out newBoundVars))
return newNode;
@@ -826,30 +1009,41 @@ namespace Microsoft.Boogie.TypeErasure
newBoundVars, bindings2);
}
- private VCExpr! GenTypePremisses(List<VCExprVar!>! oldBoundVars,
- List<VCExprVar!>! newBoundVars,
- IDictionary<TypeVariable!, VCExpr!>!
+ private VCExpr/*!*/ GenTypePremisses(List<VCExprVar/*!*/>/*!*/ oldBoundVars,
+ List<VCExprVar/*!*/>/*!*/ newBoundVars,
+ IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/
typeVarTranslation,
- List<VCExprLetBinding!>! typeVarBindings,
- out List<VCTrigger!>! triggers) {
+ List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings,
+ out List<VCTrigger/*!*/>/*!*/ triggers) {
+ Contract.Requires(cce.NonNullElements(oldBoundVars));
+ Contract.Requires(cce.NonNullElements(newBoundVars));
+ Contract.Requires(cce.NonNullElements(typeVarTranslation));
+ Contract.Requires(cce.NonNullElements(typeVarBindings));
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out triggers)));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
// build a substitution of the type variables that it can be checked
// whether type premisses are trivial
- VCExprSubstitution! typeParamSubstitution = new VCExprSubstitution ();
- foreach (VCExprLetBinding! binding in typeVarBindings)
- typeParamSubstitution[binding.V] = binding.E;
- SubstitutingVCExprVisitor! substituter = new SubstitutingVCExprVisitor (Gen);
+ VCExprSubstitution/*!*/ typeParamSubstitution = new VCExprSubstitution ();
+ foreach(VCExprLetBinding/*!*/ binding in typeVarBindings){
+Contract.Assert(binding != null);
+ typeParamSubstitution[binding.V] = binding.E;}
+ SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor (Gen);
+ Contract.Assert(substituter != null);
- List<VCExpr!>! typePremisses = new List<VCExpr!> (newBoundVars.Count);
- triggers = new List<VCTrigger!> (newBoundVars.Count);
+ List<VCExpr/*!*/>/*!*/ typePremisses = new List<VCExpr/*!*/> (newBoundVars.Count);
+ triggers = new List<VCTrigger/*!*/> (newBoundVars.Count);
for (int i = 0; i < newBoundVars.Count; ++i) {
- VCExprVar! oldVar = oldBoundVars[i];
- VCExprVar! newVar = newBoundVars[i];
+ VCExprVar/*!*/ oldVar = oldBoundVars[i];
+ Contract.Assert(oldVar != null);
+ VCExprVar/*!*/ newVar = newBoundVars[i];
+ Contract.Assert(newVar != null);
- VCExpr! typePremiss =
+ VCExpr/*!*/ typePremiss =
AxBuilderPremisses.GenVarTypeAxiom(newVar, oldVar.Type,
typeVarTranslation);
-
+ Contract.Assert(typePremiss != null);
if (!IsTriviallyTrue(substituter.Mutate(typePremiss,
typeParamSubstitution))) {
typePremisses.Add(typePremiss);
@@ -868,12 +1062,14 @@ namespace Microsoft.Boogie.TypeErasure
// these optimisations should maybe be moved into a separate
// visitor (peep-hole optimisations)
- private bool IsTriviallyTrue(VCExpr! expr) {
+ private bool IsTriviallyTrue(VCExpr expr){
+Contract.Requires(expr != null);
if (expr.Equals(VCExpressionGenerator.True))
return true;
if (expr is VCExprNAry) {
- VCExprNAry! naryExpr = (VCExprNAry)expr;
+ VCExprNAry/*!*/ naryExpr = (VCExprNAry)expr;
+ Contract.Assert(naryExpr != null);
if (naryExpr.Op.Equals(VCExpressionGenerator.EqOp) &&
naryExpr[0].Equals(naryExpr[1]))
return true;
@@ -882,91 +1078,103 @@ namespace Microsoft.Boogie.TypeErasure
return false;
}
- private VCExpr! HandleQuantifier(VCExprQuantifier! node,
- List<VCExprVar!>! occurringVars,
- List<VCExprVar!>! newBoundVars,
- VariableBindings! bindings) {
- List<VCExprLetBinding!>! typeVarBindings =
+ private VCExpr HandleQuantifier(VCExprQuantifier node, List<VCExprVar/*!*/>/*!*/ occurringVars/*!*/, List<VCExprVar/*!*/>/*!*/ newBoundVars, VariableBindings bindings) {
+ Contract.Requires(bindings != null);
+ Contract.Requires(node != null);
+ Contract.Requires(cce.NonNullElements(occurringVars/*!*/));
+ Contract.Requires(cce.NonNullElements(newBoundVars));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings =
AxBuilderPremisses.GenTypeParamBindings(node.TypeParameters, occurringVars, bindings, true);
-
+ Contract.Assert(typeVarBindings != null);
// Check whether some of the type parameters could not be
// determined from the bound variable types. In this case, we
// quantify explicitly over these variables
if (typeVarBindings.Count < node.TypeParameters.Count) {
- foreach (TypeVariable! var in node.TypeParameters) {
- if (!exists{VCExprLetBinding! b in typeVarBindings; b.V.Equals(var)})
+ foreach (TypeVariable/*!*/ var in node.TypeParameters) {
+ Contract.Assert(var != null);
+ if (!Contract.Exists(typeVarBindings, b => b.V.Equals(var)))
newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]);
}
}
// the lists of old and new bound variables for which type
// antecedents are to be generated
- List<VCExprVar!>! varsWithTypeSpecs = new List<VCExprVar!> ();
- List<VCExprVar!>! newVarsWithTypeSpecs = new List<VCExprVar!> ();
+ List<VCExprVar/*!*/>/*!*/ varsWithTypeSpecs = new List<VCExprVar/*!*/>();
+ List<VCExprVar/*!*/>/*!*/ newVarsWithTypeSpecs = new List<VCExprVar/*!*/>();
if (!IsUniversalQuantifier(node) ||
CommandLineOptions.Clo.TypeEncodingMethod
== CommandLineOptions.TypeEncoding.Predicates) {
- foreach (VCExprVar! oldVar in occurringVars) {
+ foreach (VCExprVar/*!*/ oldVar in occurringVars) {
+ Contract.Assert(oldVar != null);
varsWithTypeSpecs.Add(oldVar);
newVarsWithTypeSpecs.Add(bindings.VCExprVarBindings[oldVar]);
}
} // else, no type antecedents are created for any variables
- List<VCTrigger!>! furtherTriggers;
- VCExpr! typePremisses =
+ List<VCTrigger/*!*/>/*!*/ furtherTriggers;
+ VCExpr/*!*/ typePremisses =
GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs,
bindings.TypeVariableBindings,
typeVarBindings, out furtherTriggers);
- List<VCTrigger!>! newTriggers = MutateTriggers(node.Triggers, bindings);
+ Contract.Assert(cce.NonNullElements(furtherTriggers));
+ Contract.Assert(typePremisses != null);
+ List<VCTrigger/*!*/>/*!*/ newTriggers = MutateTriggers(node.Triggers, bindings);
+ Contract.Assert(cce.NonNullElements(newTriggers));
newTriggers.AddRange(furtherTriggers);
newTriggers = AddLets2Triggers(newTriggers, typeVarBindings);
- VCExpr! newBody = Mutate(node.Body, bindings);
+ VCExpr/*!*/ newBody = Mutate(node.Body, bindings);
+ Contract.Assert(newBody != null);
// assemble the new quantified formula
if (CommandLineOptions.Clo.TypeEncodingMethod
== CommandLineOptions.TypeEncoding.None) {
typePremisses = VCExpressionGenerator.True;
- }
+ }
- VCExpr! bodyWithPremisses =
+ VCExpr/*!*/ bodyWithPremisses =
AxBuilderPremisses.AddTypePremisses(typeVarBindings, typePremisses,
node.Quan == Quantifier.ALL,
AxBuilder.Cast(newBody, Type.Bool));
-
+ Contract.Assert(bodyWithPremisses != null);
if (newBoundVars.Count == 0) // might happen that no bound variables are left
return bodyWithPremisses;
- foreach(VCExprVar! v in newBoundVars) {
+ foreach (VCExprVar/*!*/ v in newBoundVars) {
+ Contract.Assert(v != null);
if (v.Type == AxBuilderPremisses.U) {
newTriggers.Add(Gen.Trigger(false, AxBuilderPremisses.Cast(v, Type.Int)));
newTriggers.Add(Gen.Trigger(false, AxBuilderPremisses.Cast(v, Type.Bool)));
}
}
- return Gen.Quantify(node.Quan, new List<TypeVariable!> (), newBoundVars,
+ return Gen.Quantify(node.Quan, new List<TypeVariable/*!*/>(), newBoundVars,
newTriggers, node.Infos, bodyWithPremisses);
}
// check whether we need to add let-binders for any of the type
// parameters to the triggers (otherwise, the triggers will
// contain unbound/dangling variables for such parameters)
- private List<VCTrigger!>! AddLets2Triggers(List<VCTrigger!>! triggers,
- List<VCExprLetBinding!>! typeVarBindings) {
- List<VCTrigger!>! triggersWithLets = new List<VCTrigger!> (triggers.Count);
+ private List<VCTrigger/*!*/>/*!*/ AddLets2Triggers( List<VCTrigger/*!*/>/*!*/ triggers/*!*/, List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings){
+Contract.Requires(cce.NonNullElements(triggers/*!*/));
+Contract.Requires(cce.NonNullElements(typeVarBindings));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
+ List<VCTrigger/*!*/>/*!*/ triggersWithLets = new List<VCTrigger/*!*/> (triggers.Count);
- foreach (VCTrigger! t in triggers) {
- List<VCExpr!>! exprsWithLets = new List<VCExpr!> (t.Exprs.Count);
+ foreach(VCTrigger/*!*/ t in triggers){
+Contract.Assert(t != null);
+ List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/> (t.Exprs.Count);
bool changed = false;
- foreach (VCExpr! e in t.Exprs) {
- Dictionary<VCExprVar!,object>! freeVars =
+ foreach(VCExpr/*!*/ e in t.Exprs){
+Contract.Assert(e != null);
+Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
FreeVariableCollector.FreeTermVariables(e);
-
- if (exists{VCExprLetBinding! b in typeVarBindings;
- freeVars.ContainsKey(b.V)}) {
+Contract.Assert(freeVars!=null&&cce.NonNullElements(freeVars.Keys));
+ if (Contract.Exists(typeVarBindings, b=> freeVars.ContainsKey(b.V))) {
exprsWithLets.Add(Gen.Let(typeVarBindings, e));
changed = true;
} else {
@@ -989,32 +1197,41 @@ namespace Microsoft.Boogie.TypeErasure
public class OpTypeEraserPremisses : OpTypeEraser {
- private TypeAxiomBuilderPremisses! AxBuilderPremisses;
+ private TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(AxBuilderPremisses != null);
+ }
+
- public OpTypeEraserPremisses(TypeEraserPremisses! eraser,
- TypeAxiomBuilderPremisses! axBuilder,
- VCExpressionGenerator! gen) {
- base(eraser, axBuilder, gen);
+ public OpTypeEraserPremisses(TypeEraserPremisses eraser, TypeAxiomBuilderPremisses axBuilder, VCExpressionGenerator gen):base(eraser, axBuilder, gen){
+Contract.Requires(gen != null);
+Contract.Requires(axBuilder != null);
+Contract.Requires(eraser != null);
this.AxBuilderPremisses = axBuilder;
}
- private VCExpr! HandleFunctionOp(Function! newFun,
- List<Type!>! typeArgs,
- IEnumerable<VCExpr!>! oldArgs,
- VariableBindings! bindings) {
+ private VCExpr HandleFunctionOp(Function newFun, List<Type/*!*/>/*!*/ typeArgs/*!*/, IEnumerable<VCExpr/*!*/>/*!*/ oldArgs, VariableBindings bindings){
+Contract.Requires(bindings != null);
+Contract.Requires(newFun != null);
+Contract.Requires(cce.NonNullElements(typeArgs/*!*/));
+Contract.Requires(cce.NonNullElements(oldArgs));
+Contract.Ensures(Contract.Result<VCExpr>() != null);
// UGLY: the code for tracking polarities should be factored out
int oldPolarity = Eraser.Polarity;
Eraser.Polarity = 0;
- List<VCExpr!>! newArgs = new List<VCExpr!> (typeArgs.Count);
+ List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/> (typeArgs.Count);
// translate the explicit type arguments
- foreach (Type! t in typeArgs)
- newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));
+ foreach(Type/*!*/ t in typeArgs){
+Contract.Assert(t != null);
+ newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));}
// recursively translate the value arguments
- foreach (VCExpr! arg in oldArgs) {
- Type! newType = ((!)newFun.InParams[newArgs.Count]).TypedIdent.Type;
+ foreach(VCExpr/*!*/ arg in oldArgs){
+Contract.Assert(arg != null);
+Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), newType));
}
@@ -1022,56 +1239,70 @@ namespace Microsoft.Boogie.TypeErasure
return Gen.Function(newFun, newArgs);
}
- public override VCExpr! VisitSelectOp (VCExprNAry! node,
- VariableBindings! bindings) {
- MapType! mapType = node[0].Type.AsMap;
- TypeSeq! instantiations; // not used
- Function! select =
+ public override VCExpr/*!*/ VisitSelectOp (VCExprNAry/*!*/ node,
+ VariableBindings/*!*/ bindings) {Contract.Requires(node != null);Contract.Requires(bindings != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ MapType/*!*/ mapType = node[0].Type.AsMap;
+ Contract.Assert(mapType != null);
+ TypeSeq/*!*/ instantiations; // not used
+ Function/*!*/ select =
AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations);
+ Contract.Assert(select != null);
- List<int>! explicitTypeParams =
+ List<int>/*!*/ explicitTypeParams =
AxBuilderPremisses.MapTypeAbstracterPremisses
.ExplicitSelectTypeParams(mapType);
- assert select.InParams.Length == explicitTypeParams.Count + node.Arity;
+ Contract.Assert(select.InParams.Length == explicitTypeParams.Count + node.Arity);
- List<Type!>! typeArgs = new List<Type!> (explicitTypeParams.Count);
+ List<Type/*!*/>/*!*/ typeArgs = new List<Type/*!*/>(explicitTypeParams.Count);
foreach (int i in explicitTypeParams)
typeArgs.Add(node.TypeArguments[i]);
return HandleFunctionOp(select, typeArgs, node, bindings);
}
- public override VCExpr! VisitStoreOp (VCExprNAry! node,
- VariableBindings! bindings) {
- TypeSeq! instantiations; // not used
- Function! store =
+ public override VCExpr VisitStoreOp (VCExprNAry node, VariableBindings bindings){
+Contract.Requires(bindings != null);
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+ TypeSeq/*!*/ instantiations; // not used
+ Function/*!*/ store =
AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations);
+ Contract.Assert(store != null);
return HandleFunctionOp(store,
// the store function never has explicit
// type parameters
- new List<Type!> (),
+ new List<Type/*!*/>(),
node, bindings);
}
- public override VCExpr! VisitBoogieFunctionOp (VCExprNAry! node,
- VariableBindings! bindings) {
- Function! oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
+ public override VCExpr VisitBoogieFunctionOp (VCExprNAry node, VariableBindings bindings){
+Contract.Requires(bindings != null);
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Function/*!*/ oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
+ Contract.Assert(oriFun != null);
UntypedFunction untypedFun = AxBuilderPremisses.Typed2Untyped(oriFun);
- assert untypedFun.Fun.InParams.Length ==
- untypedFun.ExplicitTypeParams.Count + node.Arity;
+ Contract.Assert( untypedFun.Fun.InParams.Length ==
+ untypedFun.ExplicitTypeParams.Count + node.Arity);
- List<Type!>! typeArgs =
+ List<Type/*!*/>/*!*/ typeArgs =
ExtractTypeArgs(node,
oriFun.TypeParameters, untypedFun.ExplicitTypeParams);
return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);
}
- private List<Type!>! ExtractTypeArgs(VCExprNAry! node,
- TypeVariableSeq! allTypeParams,
- List<TypeVariable!>! explicitTypeParams) {
- List<Type!>! res = new List<Type!> (explicitTypeParams.Count);
- foreach (TypeVariable! var in explicitTypeParams)
+ private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, TypeVariableSeq allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams){
+Contract.Requires(allTypeParams != null);
+Contract.Requires(node != null);
+Contract.Requires(cce.NonNullElements(explicitTypeParams));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ List<Type/*!*/>/*!*/ res = new List<Type/*!*/> (explicitTypeParams.Count);
+ foreach (TypeVariable/*!*/ var in explicitTypeParams) {
+ Contract.Assert(var != null);
// this lookup could be optimised
res.Add(node.TypeArguments[allTypeParams.IndexOf(var)]);
+ }
return res;
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 23:56:15 +0000