summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasurePremisses.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr/TypeErasurePremisses.cs')
-rw-r--r--Source/VCExpr/TypeErasurePremisses.cs2674
1 files changed, 1337 insertions, 1337 deletions
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index d4b36b68..dc9ad10f 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -1,1337 +1,1337 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Linq;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-// Erasure of types using premisses (forall x :: type(x)=T ==> p(x))
-
-namespace Microsoft.Boogie.TypeErasure
-{
- using Microsoft.Boogie.VCExprAST;
-
- // When using type premisses, we can distinguish two kinds of type
- // parameters of a function or map: parameters that occur in the
- // formal argument types of the function are "implicit" because they
- // can be inferred from the actual argument types; parameters that
- // only occur in the result type of the function are "explicit"
- // because they are not inferrable and have to be given to the
- // function as additional arguments.
- //
- // The following structure is used to store the untyped version of a
- // typed function, together with the lists of implicit and explicit
- // type parameters (in the same order as they occur in the signature
- // of the original function).
-
- internal struct UntypedFunction
- {
- public readonly Function/*!*/ Fun;
- // type parameters that can be extracted from the value parameters
- public readonly List<TypeVariable/*!*/>/*!*/ ImplicitTypeParams;
- // type parameters that have to be given explicitly
- 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) {
- Contract.Requires(fun != null);
- Contract.Requires(cce.NonNullElements(implicitTypeParams));
- Contract.Requires(cce.NonNullElements(explicitTypeParams));
- Fun = fun;
- ImplicitTypeParams = implicitTypeParams;
- ExplicitTypeParams = explicitTypeParams;
- }
- }
-
- public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU
- {
-
- public TypeAxiomBuilderPremisses(VCExpressionGenerator gen)
- : base(gen) {
- Contract.Requires(gen != null);
-
- TypeFunction = HelperFuns.BoogieFunction("dummy", Type.Int);
- Typed2UntypedFunctions = new Dictionary<Function/*!*/, UntypedFunction>();
- MapTypeAbstracterAttr = null;
- }
-
- // constructor to allow cloning
- [NotDelayed]
- internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses builder)
- : base(builder) {
- Contract.Requires(builder != null);
- TypeFunction = builder.TypeFunction;
- Typed2UntypedFunctions =
- new Dictionary<Function/*!*/, UntypedFunction>(builder.Typed2UntypedFunctions);
-
- MapTypeAbstracterAttr =
- builder.MapTypeAbstracterAttr == null ?
- null : new MapTypeAbstractionBuilderPremisses(this, builder.Gen,
- builder.MapTypeAbstracterAttr);
- }
-
- public override Object Clone() {
- Contract.Ensures(Contract.Result<Object>() != null);
- return new TypeAxiomBuilderPremisses(this);
- }
-
- public override void Setup() {
- TypeFunction = HelperFuns.BoogieFunction("type", U, T);
- base.Setup();
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // 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) {
- //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, 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, -1, matrix);
- }
-
- 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 {
- Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
-
- if (MapTypeAbstracterAttr == null)
- MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses(this, Gen);
- return MapTypeAbstracterAttr;
- }
- }
-
- internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses {
- get {
- Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
-
- return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
- }
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // function that maps individuals to their type
- // the field is overwritten with its actual value in "Setup"
- private Function/*!*/ TypeFunction;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(TypeFunction != null);
- }
-
-
- public VCExpr TypeOf(VCExpr expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- return Gen.Function(TypeFunction, expr);
- }
-
- ///////////////////////////////////////////////////////////////////////////
- // Generate type premisses and type parameter bindings for quantifiers, functions, procedures
-
- // let-bindings to extract the instantiations of type parameters
- public List<VCExprLetBinding/*!*/>/*!*/
- GenTypeParamBindings(// the original bound variables and (implicit) type parameters
- List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ oldBoundVars,
- // VariableBindings to which the translation
- // TypeVariable -> VCExprVar is added
- 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) {
- 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);
- foreach (VCExprVar var in oldBoundVars) {
- VCExprVar/*!*/ newVar = bindings.VCExprVarBindings[var];
- if (newVar.Type.Equals(U)) {
- UtypedVars.Add(newVar);
- originalTypes.Add(var.Type);
- }
- }
-
- UtypedVars.TrimExcess();
- originalTypes.TrimExcess();
-
- return BestTypeVarExtractors(typeParams, originalTypes, UtypedVars, bindings);
- }
-
-
- 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);
- }
-
-
- ///////////////////////////////////////////////////////////////////////////
- // Extract the instantiations of type variables from the concrete types of
- // 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) {
- 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(
- Gen.LetBinding((VCExprVar)bindings.TypeVariableBindings[var],
- extractor));
- }
- return typeParamBindings;
- }
-
- 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;
-
- VCExpr bestExtractor = allExtractors[0];
- int bestExtractorSize = SizeComputingVisitor.ComputeSize(bestExtractor);
- for (int i = 1; i < allExtractors.Count; ++i) {
- int newSize = SizeComputingVisitor.ComputeSize(allExtractors[i]);
- if (newSize < bestExtractorSize) {
- bestExtractor = allExtractors[i];
- bestExtractorSize = newSize;
- }
- }
-
- return bestExtractor;
- }
-
- 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) {
- 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);
- } // else nothing
- } else if (completeType.IsBasic) {
- // nothing
- } else if (completeType.IsCtor) {
- CtorType/*!*/ ctorType = completeType.AsCtor;
- if (ctorType.Arguments.Count > 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.Count; ++i) {
- VCExpr/*!*/ newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
- Contract.Assert(newInnerTerm != null);
- TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors);
- }
- }
- } else if (completeType.IsMap) {
- TypeVarExtractors(var, MapTypeAbstracter.AbstractMapType(completeType.AsMap),
- innerTerm, extractors);
- } else {
- System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + completeType);
- }
- }
-
- ////////////////////////////////////////////////////////////////////////////
- // Symbols for representing functions
-
- // Globally defined functions
- private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
- [ContractInvariantMethod]
- void Typed2UntypedFunctionsInvariantMethod() {
- Contract.Invariant(Typed2UntypedFunctions != null);
- }
-
- // distinguish between implicit and explicit type parameters
- internal static void SeparateTypeParams(List<Type/*!*/>/*!*/ valueArgumentTypes,
- List<TypeVariable>/*!*/ 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)));
- List<TypeVariable>/*!*/ varsInInParamTypes = new List<TypeVariable>();
- foreach (Type/*!*/ t in valueArgumentTypes) {
- Contract.Assert(t != null);
- varsInInParamTypes.AppendWithoutDups(t.FreeVariables);
- }
-
- implicitParams = new List<TypeVariable/*!*/>(allTypeParams.Count);
- explicitParams = new List<TypeVariable/*!*/>(allTypeParams.Count);
-
- foreach (TypeVariable/*!*/ var in allTypeParams) {
- Contract.Assert(var != null);
- if (varsInInParamTypes.Contains(var))
- implicitParams.Add(var);
- else
- explicitParams.Add(var);
- }
-
- implicitParams.TrimExcess();
- explicitParams.TrimExcess();
- }
-
- internal UntypedFunction Typed2Untyped(Function fun) {
- Contract.Requires(fun != null);
- UntypedFunction res;
- if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
- Contract.Assert(fun.OutParams.Count == 1);
-
- // if all of the parameters are int or bool, the function does
- // not have to be changed
- if (fun.InParams.All(param => UnchangedType(cce.NonNull(param).TypedIdent.Type)) &&
- UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&
- fun.TypeParameters.Count == 0) {
- res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());
- } else {
- 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;
- SeparateTypeParams(argTypes, fun.TypeParameters, out implicitParams, out explicitParams);
-
- Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Count + 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.Count; ++i, ++j)
- 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);
- Contract.Assert(untypedFun != null);
- untypedFun.Attributes = fun.Attributes;
- res = new UntypedFunction(untypedFun, implicitParams, explicitParams);
- if (U.Equals(types[types.Length - 1]))
- AddTypeAxiom(GenFunctionAxiom(res, fun));
- }
-
- Typed2UntypedFunctions.Add(fun, res);
- }
- return res;
- }
-
- 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.Count);
- foreach (Formal/*!*/ f in originalFun.InParams)
- originalInTypes.Add(f.TypedIdent.Type);
-
- return GenFunctionAxiom(fun.Fun, fun.ImplicitTypeParams, fun.ExplicitTypeParams,
- originalInTypes,
- cce.NonNull(originalFun.OutParams[0]).TypedIdent.Type);
- }
-
- 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.Count);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
- return VCExpressionGenerator.True;
- }
-
- List<VCExprVar/*!*/>/*!*/ typedInputVars = new List<VCExprVar/*!*/>(originalInTypes.Count);
- int i = 0;
- foreach (Type/*!*/ t in originalInTypes) {
- Contract.Assert(t != null);
- typedInputVars.Add(Gen.Variable("arg" + i, t));
- i = i + 1;
- }
-
- 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) {
- 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) {
- 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 =
- GenTypeParamBindings(implicitTypeParams, typedInputVars, bindings, true);
- Contract.Assert(cce.NonNullElements(typeVarBindings));
-
- 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?)
- // AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
- Gen.Let(typeVarBindings, conclusion);
-
- if (boundVars.Count > 0) {
- List<VCTrigger/*!*/> triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
- Contract.Assert(cce.NonNullElements(triggers));
- return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, -1, conclusionWithPremisses);
- } else {
- return conclusionWithPremisses;
- }
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- 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/*!*/>()));
- }
-
- public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
- Contract.Requires(var != null);
- Contract.Requires(originalType != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- if (!var.Type.Equals(originalType)) {
- VCExpr/*!*/ typeRepr = Type2Term(originalType, varMapping);
- return Gen.Eq(TypeOf(var), typeRepr);
- }
- return VCExpressionGenerator.True;
- }
- }
-
- /////////////////////////////////////////////////////////////////////////////
-
- internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder
- {
-
- private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(AxBuilderPremisses != null);
- }
-
-
- 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) {
- Contract.Requires(builder != null);
- Contract.Requires(gen != null);
- Contract.Requires(axBuilder != null);
-
- this.AxBuilderPremisses = axBuilder;
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // Determine the type parameters of a map type that have to be
- // given explicitly when applying the select function (the
- // parameters that only occur in the result type of the
- // 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) {
- Contract.Requires(type != null);
- Contract.Ensures(Contract.Result<List<int>>() != null);
-
- List<int> res;
- if (!explicitSelectTypeParamsCache.TryGetValue(type, out res)) {
- 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) {
- Contract.Assert(var != null);
- res.Add(type.TypeParameters.IndexOf(var));
- }
- explicitSelectTypeParamsCache.Add(type, res);
- }
- return cce.NonNull(res);
- }
-
- private IDictionary<MapType/*!*/, List<int>/*!*/>/*!*/ explicitSelectTypeParamsCache =
- new Dictionary<MapType/*!*/, List<int>/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvarant() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(explicitSelectTypeParamsCache));
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
-
- 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;
- 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;
- store = CreateAccessFun(typeParams, originalInTypes,
- mapTypeSynonym, synonym.Name + "Store",
- out implicitStoreParams, out explicitStoreParams);
-
- // 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 {
- AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
- abstractedType.Result,
- implicitSelectParams, explicitSelectParams,
- originalInTypes));
- 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) {
- 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/*!*/>();
- typeParams.AddRange(abstractedType.TypeParameters);
- typeParams.AddRange(abstractedType.FreeVariables);
-
- originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);
- List<Type>/*!*/ mapTypeParams = new List<Type>();
- foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {
- Contract.Assert(var != null);
- mapTypeParams.Add(var);
- }
-
- if (CommandLineOptions.Clo.MonomorphicArrays)
- mapTypeSynonym = abstractedType;
- 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) {
- 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
- TypeAxiomBuilderPremisses.SeparateTypeParams(originalInTypes,
- new List<TypeVariable>(originalTypeParams),
- out implicitTypeParams,
- out explicitTypeParams);
-
- 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) {
- Contract.Assert(type != null);
- if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type))
- ioTypes[i] = type;
- else
- 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);
- Contract.Assert(res != null);
-
- if (AxBuilder.U.Equals(ioTypes[i])) {
- AxBuilder.AddTypeAxiom(
- AxBuilderPremisses.GenFunctionAxiom(res,
- implicitTypeParams, explicitTypeParams,
- originalInTypes, originalResult));
- }
- return res;
- }
-
- ///////////////////////////////////////////////////////////////////////////
- // 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) {
- 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) {
- 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);
- return Gen.Function(store, storeArgs);
- }
-
- /// <summary>
- /// Generate:
- /// (forall m, indexes, val ::
- /// type(val) == T ==>
- /// 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) {
- 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.Count - 2;
- List<VCExprVar/*!*/> inParams = new List<VCExprVar/*!*/>();
- List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Count);
- VariableBindings bindings = new VariableBindings();
-
- // bound variable: m
- VCExprVar typedM = Gen.Variable("m", originalInTypes[0]);
- VCExprVar m = Gen.Variable("m", AxBuilder.U);
- inParams.Add(typedM);
- quantifiedVars.Add(m);
- 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.Count - 1; i++) {
- origIndexTypes.Add(originalInTypes[i]);
- indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);
- }
- 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++) {
- bindings.VCExprVarBindings.Add(typedArgs[i], indexes[i]);
- }
-
- // bound variable: val
- VCExprVar typedVal = Gen.Variable("val", mapResult);
- VCExprVar val = Gen.Variable("val", cce.NonNull(select.OutParams[0]).TypedIdent.Type);
- quantifiedVars.Add(val);
- bindings.VCExprVarBindings.Add(typedVal, val);
-
- // add all type parameters into bindings
- foreach (TypeVariable tp in implicitTypeParamsSelect) {
- VCExprVar tVar = Gen.Variable(tp.Name, AxBuilderPremisses.T);
- bindings.TypeVariableBindings.Add(tp, tVar);
- }
- 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);
- // ... and record these explicit type-parameter arguments in typeParams
- typeParams.Add(tVar);
- }
-
- 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 =
- 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 =
- 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);
- Contract.Assert(eq != null);
- // generate: type(val) == T, where T is the type of val
- 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(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, 0, body);
- }
-
- 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.Count - 2;
-
- List<Type/*!*/> indexTypes = new List<Type/*!*/>();
- for (int i = 1; i < store.InParams.Count - 1; i++) {
- indexTypes.Add(cce.NonNull(store.InParams[i]).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);
- Contract.Assert(typedVal != null);
- VariableBindings/*!*/ bindings = new VariableBindings();
- bindings.VCExprVarBindings.Add(typedVal, val);
-
- 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) {
- 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);
- 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);
- Contract.Assert(selectEq != null);
-
- 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/*!*/>();
- Contract.Assert(cce.NonNullElements(triggers));
-
- 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, "mapAx1:" + select.Name + ":" + i, 0, 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) {
- 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, "mapAx2:" + select.Name, 0, matrix2);
- axiom = Gen.AndSimp(axiom, conjunct2);
-
- return axiom;
- }
-
- }
-
- /////////////////////////////////////////////////////////////////////////////
-
- public class TypeEraserPremisses : TypeEraser
- {
-
- private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(AxBuilderPremisses != null);
- }
-
-
- private OpTypeEraser OpEraserAttr = null;
- 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) {
- Contract.Requires(gen != null);
- Contract.Requires(axBuilder != null);
-
- this.AxBuilderPremisses = axBuilder;
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- 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
- // in any of the triggers (if some variables do not occur, we
- // need to take special care of type parameters that only occur
- // in the types of such variables)
- FreeVariableCollector coll = new FreeVariableCollector();
- coll.Collect(node.Body);
- foreach (VCTrigger trigger in node.Triggers) {
- if (trigger.Pos)
- foreach (VCExpr/*!*/ e in trigger.Exprs) {
- Contract.Assert(e != null);
-
- coll.Collect(e);
- }
- }
-
- List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/>(node.BoundVars.Count);
- foreach (VCExprVar var in node.BoundVars)
- if (coll.FreeTermVars.ContainsKey(var))
- occurringVars.Add(var);
-
- occurringVars.TrimExcess();
-
- // bound term variables are replaced with bound term variables typed in
- // a simpler way
- List<VCExprVar/*!*/>/*!*/ newBoundVars =
- BoundVarsAfterErasure(occurringVars, bindings);
- 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;
- if (!RedoQuantifier(node, (VCExprQuantifier)newNode, occurringVars, oldBindings,
- out bindings2, out newBoundVars))
- return newNode;
-
- return HandleQuantifier(node, occurringVars,
- newBoundVars, bindings2);
- }
-
- private VCExpr/*!*/ GenTypePremisses(List<VCExprVar/*!*/>/*!*/ oldBoundVars,
- List<VCExprVar/*!*/>/*!*/ newBoundVars,
- IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/
- typeVarTranslation,
- List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings,
- out List<VCTrigger/*!*/>/*!*/ triggers) {
- Contract.Requires(cce.NonNullElements(oldBoundVars));
- Contract.Requires(cce.NonNullElements(newBoundVars));
- Contract.Requires(cce.NonNullDictionaryAndValues(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) {
- 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);
-
- for (int i = 0; i < newBoundVars.Count; ++i) {
- VCExprVar/*!*/ oldVar = oldBoundVars[i];
- Contract.Assert(oldVar != null);
- VCExprVar/*!*/ newVar = newBoundVars[i];
- Contract.Assert(newVar != null);
-
- VCExpr/*!*/ typePremiss =
- AxBuilderPremisses.GenVarTypeAxiom(newVar, oldVar.Type,
- typeVarTranslation);
- Contract.Assert(typePremiss != null);
- if (!IsTriviallyTrue(substituter.Mutate(typePremiss,
- typeParamSubstitution))) {
- typePremisses.Add(typePremiss);
- // generate a negative trigger for the variable occurrence
- // in the type premiss
- triggers.Add(Gen.Trigger(false,
- HelperFuns.ToList(AxBuilderPremisses.TypeOf(newVar))));
- }
- }
-
- typePremisses.TrimExcess();
- triggers.TrimExcess();
-
- return Gen.NAry(VCExpressionGenerator.AndOp, typePremisses);
- }
-
- // these optimisations should maybe be moved into a separate
- // visitor (peep-hole optimisations)
- private bool IsTriviallyTrue(VCExpr expr) {
- Contract.Requires(expr != null);
- if (expr.Equals(VCExpressionGenerator.True))
- return true;
-
- if (expr is VCExprNAry) {
- VCExprNAry/*!*/ naryExpr = (VCExprNAry)expr;
- Contract.Assert(naryExpr != null);
- if (naryExpr.Op.Equals(VCExpressionGenerator.EqOp) &&
- naryExpr[0].Equals(naryExpr[1]))
- return true;
- }
-
- return false;
- }
-
- 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) {
- Contract.Assert(var != null);
- if (typeVarBindings.All(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/*!*/>();
- if (!IsUniversalQuantifier(node) ||
- CommandLineOptions.Clo.TypeEncodingMethod
- == CommandLineOptions.TypeEncoding.Predicates) {
- 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 =
- GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs,
- bindings.TypeVariableBindings,
- typeVarBindings, out furtherTriggers);
-
- 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);
- Contract.Assert(newBody != null);
-
- // assemble the new quantified formula
-
- if (CommandLineOptions.Clo.TypeEncodingMethod
- == CommandLineOptions.TypeEncoding.None) {
- typePremisses = VCExpressionGenerator.True;
- }
-
- 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) {
- 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,
- 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) {
- 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) {
- Contract.Assert(t != null);
- List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/>(t.Exprs.Count);
-
- bool changed = false;
- foreach (VCExpr/*!*/ e in t.Exprs) {
- Contract.Assert(e != null);
- Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
- FreeVariableCollector.FreeTermVariables(e);
- Contract.Assert(freeVars != null && cce.NonNullElements(freeVars.Keys));
- if (typeVarBindings.Any(b => freeVars.ContainsKey(b.V))) {
- exprsWithLets.Add(Gen.Let(typeVarBindings, e));
- changed = true;
- } else {
- exprsWithLets.Add(e);
- }
- }
-
- if (changed)
- triggersWithLets.Add(Gen.Trigger(t.Pos, exprsWithLets));
- else
- triggersWithLets.Add(t);
- }
-
- return triggersWithLets;
- }
-
- }
-
- //////////////////////////////////////////////////////////////////////////////
-
- public class OpTypeEraserPremisses : OpTypeEraser
- {
-
- private TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(AxBuilderPremisses != null);
- }
-
-
- 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) {
- 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);
-
- // translate the explicit type arguments
- 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) {
- Contract.Assert(arg != null);
- Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
- newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), newType));
- }
-
- Eraser.Polarity = oldPolarity;
- return Gen.Function(newFun, newArgs);
- }
-
- 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);
- List<Type>/*!*/ instantiations; // not used
- Function/*!*/ select =
- AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations);
- Contract.Assert(select != null);
-
- List<int>/*!*/ explicitTypeParams =
- AxBuilderPremisses.MapTypeAbstracterPremisses
- .ExplicitSelectTypeParams(mapType);
- Contract.Assert(select.InParams.Count == explicitTypeParams.Count + node.Arity);
-
- 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) {
- Contract.Requires(bindings != null);
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- List<Type>/*!*/ 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/*!*/>(),
- node, bindings);
- }
-
- 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);
- Contract.Assert(untypedFun.Fun.InParams.Count ==
- untypedFun.ExplicitTypeParams.Count + node.Arity);
-
- List<Type/*!*/>/*!*/ typeArgs =
- ExtractTypeArgs(node,
- oriFun.TypeParameters, untypedFun.ExplicitTypeParams);
- return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);
- }
-
- private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, List<TypeVariable> 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;
- }
- }
-
-
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+// Erasure of types using premisses (forall x :: type(x)=T ==> p(x))
+
+namespace Microsoft.Boogie.TypeErasure
+{
+ using Microsoft.Boogie.VCExprAST;
+
+ // When using type premisses, we can distinguish two kinds of type
+ // parameters of a function or map: parameters that occur in the
+ // formal argument types of the function are "implicit" because they
+ // can be inferred from the actual argument types; parameters that
+ // only occur in the result type of the function are "explicit"
+ // because they are not inferrable and have to be given to the
+ // function as additional arguments.
+ //
+ // The following structure is used to store the untyped version of a
+ // typed function, together with the lists of implicit and explicit
+ // type parameters (in the same order as they occur in the signature
+ // of the original function).
+
+ internal struct UntypedFunction
+ {
+ public readonly Function/*!*/ Fun;
+ // type parameters that can be extracted from the value parameters
+ public readonly List<TypeVariable/*!*/>/*!*/ ImplicitTypeParams;
+ // type parameters that have to be given explicitly
+ 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) {
+ Contract.Requires(fun != null);
+ Contract.Requires(cce.NonNullElements(implicitTypeParams));
+ Contract.Requires(cce.NonNullElements(explicitTypeParams));
+ Fun = fun;
+ ImplicitTypeParams = implicitTypeParams;
+ ExplicitTypeParams = explicitTypeParams;
+ }
+ }
+
+ public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU
+ {
+
+ public TypeAxiomBuilderPremisses(VCExpressionGenerator gen)
+ : base(gen) {
+ Contract.Requires(gen != null);
+
+ TypeFunction = HelperFuns.BoogieFunction("dummy", Type.Int);
+ Typed2UntypedFunctions = new Dictionary<Function/*!*/, UntypedFunction>();
+ MapTypeAbstracterAttr = null;
+ }
+
+ // constructor to allow cloning
+ [NotDelayed]
+ internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses builder)
+ : base(builder) {
+ Contract.Requires(builder != null);
+ TypeFunction = builder.TypeFunction;
+ Typed2UntypedFunctions =
+ new Dictionary<Function/*!*/, UntypedFunction>(builder.Typed2UntypedFunctions);
+
+ MapTypeAbstracterAttr =
+ builder.MapTypeAbstracterAttr == null ?
+ null : new MapTypeAbstractionBuilderPremisses(this, builder.Gen,
+ builder.MapTypeAbstracterAttr);
+ }
+
+ public override Object Clone() {
+ Contract.Ensures(Contract.Result<Object>() != null);
+ return new TypeAxiomBuilderPremisses(this);
+ }
+
+ public override void Setup() {
+ TypeFunction = HelperFuns.BoogieFunction("type", U, T);
+ base.Setup();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // 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) {
+ //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, 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, -1, matrix);
+ }
+
+ 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 {
+ Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
+
+ if (MapTypeAbstracterAttr == null)
+ MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses(this, Gen);
+ return MapTypeAbstracterAttr;
+ }
+ }
+
+ internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses {
+ get {
+ Contract.Ensures(Contract.Result<MapTypeAbstractionBuilderPremisses>() != null);
+
+ return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // function that maps individuals to their type
+ // the field is overwritten with its actual value in "Setup"
+ private Function/*!*/ TypeFunction;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(TypeFunction != null);
+ }
+
+
+ public VCExpr TypeOf(VCExpr expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return Gen.Function(TypeFunction, expr);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Generate type premisses and type parameter bindings for quantifiers, functions, procedures
+
+ // let-bindings to extract the instantiations of type parameters
+ public List<VCExprLetBinding/*!*/>/*!*/
+ GenTypeParamBindings(// the original bound variables and (implicit) type parameters
+ List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ oldBoundVars,
+ // VariableBindings to which the translation
+ // TypeVariable -> VCExprVar is added
+ 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) {
+ 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);
+ foreach (VCExprVar var in oldBoundVars) {
+ VCExprVar/*!*/ newVar = bindings.VCExprVarBindings[var];
+ if (newVar.Type.Equals(U)) {
+ UtypedVars.Add(newVar);
+ originalTypes.Add(var.Type);
+ }
+ }
+
+ UtypedVars.TrimExcess();
+ originalTypes.TrimExcess();
+
+ return BestTypeVarExtractors(typeParams, originalTypes, UtypedVars, bindings);
+ }
+
+
+ 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);
+ }
+
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Extract the instantiations of type variables from the concrete types of
+ // 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) {
+ 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(
+ Gen.LetBinding((VCExprVar)bindings.TypeVariableBindings[var],
+ extractor));
+ }
+ return typeParamBindings;
+ }
+
+ 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;
+
+ VCExpr bestExtractor = allExtractors[0];
+ int bestExtractorSize = SizeComputingVisitor.ComputeSize(bestExtractor);
+ for (int i = 1; i < allExtractors.Count; ++i) {
+ int newSize = SizeComputingVisitor.ComputeSize(allExtractors[i]);
+ if (newSize < bestExtractorSize) {
+ bestExtractor = allExtractors[i];
+ bestExtractorSize = newSize;
+ }
+ }
+
+ return bestExtractor;
+ }
+
+ 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) {
+ 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);
+ } // else nothing
+ } else if (completeType.IsBasic) {
+ // nothing
+ } else if (completeType.IsCtor) {
+ CtorType/*!*/ ctorType = completeType.AsCtor;
+ if (ctorType.Arguments.Count > 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.Count; ++i) {
+ VCExpr/*!*/ newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
+ Contract.Assert(newInnerTerm != null);
+ TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors);
+ }
+ }
+ } else if (completeType.IsMap) {
+ TypeVarExtractors(var, MapTypeAbstracter.AbstractMapType(completeType.AsMap),
+ innerTerm, extractors);
+ } else {
+ System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + completeType);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Symbols for representing functions
+
+ // Globally defined functions
+ private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
+ [ContractInvariantMethod]
+ void Typed2UntypedFunctionsInvariantMethod() {
+ Contract.Invariant(Typed2UntypedFunctions != null);
+ }
+
+ // distinguish between implicit and explicit type parameters
+ internal static void SeparateTypeParams(List<Type/*!*/>/*!*/ valueArgumentTypes,
+ List<TypeVariable>/*!*/ 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)));
+ List<TypeVariable>/*!*/ varsInInParamTypes = new List<TypeVariable>();
+ foreach (Type/*!*/ t in valueArgumentTypes) {
+ Contract.Assert(t != null);
+ varsInInParamTypes.AppendWithoutDups(t.FreeVariables);
+ }
+
+ implicitParams = new List<TypeVariable/*!*/>(allTypeParams.Count);
+ explicitParams = new List<TypeVariable/*!*/>(allTypeParams.Count);
+
+ foreach (TypeVariable/*!*/ var in allTypeParams) {
+ Contract.Assert(var != null);
+ if (varsInInParamTypes.Contains(var))
+ implicitParams.Add(var);
+ else
+ explicitParams.Add(var);
+ }
+
+ implicitParams.TrimExcess();
+ explicitParams.TrimExcess();
+ }
+
+ internal UntypedFunction Typed2Untyped(Function fun) {
+ Contract.Requires(fun != null);
+ UntypedFunction res;
+ if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
+ Contract.Assert(fun.OutParams.Count == 1);
+
+ // if all of the parameters are int or bool, the function does
+ // not have to be changed
+ if (fun.InParams.All(param => UnchangedType(cce.NonNull(param).TypedIdent.Type)) &&
+ UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&
+ fun.TypeParameters.Count == 0) {
+ res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());
+ } else {
+ 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;
+ SeparateTypeParams(argTypes, fun.TypeParameters, out implicitParams, out explicitParams);
+
+ Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Count + 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.Count; ++i, ++j)
+ 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);
+ Contract.Assert(untypedFun != null);
+ untypedFun.Attributes = fun.Attributes;
+ res = new UntypedFunction(untypedFun, implicitParams, explicitParams);
+ if (U.Equals(types[types.Length - 1]))
+ AddTypeAxiom(GenFunctionAxiom(res, fun));
+ }
+
+ Typed2UntypedFunctions.Add(fun, res);
+ }
+ return res;
+ }
+
+ 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.Count);
+ foreach (Formal/*!*/ f in originalFun.InParams)
+ originalInTypes.Add(f.TypedIdent.Type);
+
+ return GenFunctionAxiom(fun.Fun, fun.ImplicitTypeParams, fun.ExplicitTypeParams,
+ originalInTypes,
+ cce.NonNull(originalFun.OutParams[0]).TypedIdent.Type);
+ }
+
+ 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.Count);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
+ return VCExpressionGenerator.True;
+ }
+
+ List<VCExprVar/*!*/>/*!*/ typedInputVars = new List<VCExprVar/*!*/>(originalInTypes.Count);
+ int i = 0;
+ foreach (Type/*!*/ t in originalInTypes) {
+ Contract.Assert(t != null);
+ typedInputVars.Add(Gen.Variable("arg" + i, t));
+ i = i + 1;
+ }
+
+ 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) {
+ 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) {
+ 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 =
+ GenTypeParamBindings(implicitTypeParams, typedInputVars, bindings, true);
+ Contract.Assert(cce.NonNullElements(typeVarBindings));
+
+ 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?)
+ // AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
+ Gen.Let(typeVarBindings, conclusion);
+
+ if (boundVars.Count > 0) {
+ List<VCTrigger/*!*/> triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
+ Contract.Assert(cce.NonNullElements(triggers));
+ return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, -1, conclusionWithPremisses);
+ } else {
+ return conclusionWithPremisses;
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ 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/*!*/>()));
+ }
+
+ public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
+ Contract.Requires(var != null);
+ Contract.Requires(originalType != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ if (!var.Type.Equals(originalType)) {
+ VCExpr/*!*/ typeRepr = Type2Term(originalType, varMapping);
+ return Gen.Eq(TypeOf(var), typeRepr);
+ }
+ return VCExpressionGenerator.True;
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////
+
+ internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder
+ {
+
+ private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(AxBuilderPremisses != null);
+ }
+
+
+ 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) {
+ Contract.Requires(builder != null);
+ Contract.Requires(gen != null);
+ Contract.Requires(axBuilder != null);
+
+ this.AxBuilderPremisses = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Determine the type parameters of a map type that have to be
+ // given explicitly when applying the select function (the
+ // parameters that only occur in the result type of the
+ // 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) {
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result<List<int>>() != null);
+
+ List<int> res;
+ if (!explicitSelectTypeParamsCache.TryGetValue(type, out res)) {
+ 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) {
+ Contract.Assert(var != null);
+ res.Add(type.TypeParameters.IndexOf(var));
+ }
+ explicitSelectTypeParamsCache.Add(type, res);
+ }
+ return cce.NonNull(res);
+ }
+
+ private IDictionary<MapType/*!*/, List<int>/*!*/>/*!*/ explicitSelectTypeParamsCache =
+ new Dictionary<MapType/*!*/, List<int>/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvarant() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(explicitSelectTypeParamsCache));
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ 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;
+ 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;
+ store = CreateAccessFun(typeParams, originalInTypes,
+ mapTypeSynonym, synonym.Name + "Store",
+ out implicitStoreParams, out explicitStoreParams);
+
+ // 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 {
+ AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
+ abstractedType.Result,
+ implicitSelectParams, explicitSelectParams,
+ originalInTypes));
+ 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) {
+ 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/*!*/>();
+ typeParams.AddRange(abstractedType.TypeParameters);
+ typeParams.AddRange(abstractedType.FreeVariables);
+
+ originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);
+ List<Type>/*!*/ mapTypeParams = new List<Type>();
+ foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {
+ Contract.Assert(var != null);
+ mapTypeParams.Add(var);
+ }
+
+ if (CommandLineOptions.Clo.MonomorphicArrays)
+ mapTypeSynonym = abstractedType;
+ 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) {
+ 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
+ TypeAxiomBuilderPremisses.SeparateTypeParams(originalInTypes,
+ new List<TypeVariable>(originalTypeParams),
+ out implicitTypeParams,
+ out explicitTypeParams);
+
+ 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) {
+ Contract.Assert(type != null);
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type))
+ ioTypes[i] = type;
+ else
+ 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);
+ Contract.Assert(res != null);
+
+ if (AxBuilder.U.Equals(ioTypes[i])) {
+ AxBuilder.AddTypeAxiom(
+ AxBuilderPremisses.GenFunctionAxiom(res,
+ implicitTypeParams, explicitTypeParams,
+ originalInTypes, originalResult));
+ }
+ return res;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // 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) {
+ 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) {
+ 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);
+ return Gen.Function(store, storeArgs);
+ }
+
+ /// <summary>
+ /// Generate:
+ /// (forall m, indexes, val ::
+ /// type(val) == T ==>
+ /// 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) {
+ 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.Count - 2;
+ List<VCExprVar/*!*/> inParams = new List<VCExprVar/*!*/>();
+ List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Count);
+ VariableBindings bindings = new VariableBindings();
+
+ // bound variable: m
+ VCExprVar typedM = Gen.Variable("m", originalInTypes[0]);
+ VCExprVar m = Gen.Variable("m", AxBuilder.U);
+ inParams.Add(typedM);
+ quantifiedVars.Add(m);
+ 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.Count - 1; i++) {
+ origIndexTypes.Add(originalInTypes[i]);
+ indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);
+ }
+ 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++) {
+ bindings.VCExprVarBindings.Add(typedArgs[i], indexes[i]);
+ }
+
+ // bound variable: val
+ VCExprVar typedVal = Gen.Variable("val", mapResult);
+ VCExprVar val = Gen.Variable("val", cce.NonNull(select.OutParams[0]).TypedIdent.Type);
+ quantifiedVars.Add(val);
+ bindings.VCExprVarBindings.Add(typedVal, val);
+
+ // add all type parameters into bindings
+ foreach (TypeVariable tp in implicitTypeParamsSelect) {
+ VCExprVar tVar = Gen.Variable(tp.Name, AxBuilderPremisses.T);
+ bindings.TypeVariableBindings.Add(tp, tVar);
+ }
+ 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);
+ // ... and record these explicit type-parameter arguments in typeParams
+ typeParams.Add(tVar);
+ }
+
+ 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 =
+ 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 =
+ 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);
+ Contract.Assert(eq != null);
+ // generate: type(val) == T, where T is the type of val
+ 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(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, 0, body);
+ }
+
+ 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.Count - 2;
+
+ List<Type/*!*/> indexTypes = new List<Type/*!*/>();
+ for (int i = 1; i < store.InParams.Count - 1; i++) {
+ indexTypes.Add(cce.NonNull(store.InParams[i]).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);
+ Contract.Assert(typedVal != null);
+ VariableBindings/*!*/ bindings = new VariableBindings();
+ bindings.VCExprVarBindings.Add(typedVal, val);
+
+ 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) {
+ 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);
+ 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);
+ Contract.Assert(selectEq != null);
+
+ 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/*!*/>();
+ Contract.Assert(cce.NonNullElements(triggers));
+
+ 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, "mapAx1:" + select.Name + ":" + i, 0, 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) {
+ 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, "mapAx2:" + select.Name, 0, matrix2);
+ axiom = Gen.AndSimp(axiom, conjunct2);
+
+ return axiom;
+ }
+
+ }
+
+ /////////////////////////////////////////////////////////////////////////////
+
+ public class TypeEraserPremisses : TypeEraser
+ {
+
+ private readonly TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(AxBuilderPremisses != null);
+ }
+
+
+ private OpTypeEraser OpEraserAttr = null;
+ 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) {
+ Contract.Requires(gen != null);
+ Contract.Requires(axBuilder != null);
+
+ this.AxBuilderPremisses = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ 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
+ // in any of the triggers (if some variables do not occur, we
+ // need to take special care of type parameters that only occur
+ // in the types of such variables)
+ FreeVariableCollector coll = new FreeVariableCollector();
+ coll.Collect(node.Body);
+ foreach (VCTrigger trigger in node.Triggers) {
+ if (trigger.Pos)
+ foreach (VCExpr/*!*/ e in trigger.Exprs) {
+ Contract.Assert(e != null);
+
+ coll.Collect(e);
+ }
+ }
+
+ List<VCExprVar/*!*/> occurringVars = new List<VCExprVar/*!*/>(node.BoundVars.Count);
+ foreach (VCExprVar var in node.BoundVars)
+ if (coll.FreeTermVars.ContainsKey(var))
+ occurringVars.Add(var);
+
+ occurringVars.TrimExcess();
+
+ // bound term variables are replaced with bound term variables typed in
+ // a simpler way
+ List<VCExprVar/*!*/>/*!*/ newBoundVars =
+ BoundVarsAfterErasure(occurringVars, bindings);
+ 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;
+ if (!RedoQuantifier(node, (VCExprQuantifier)newNode, occurringVars, oldBindings,
+ out bindings2, out newBoundVars))
+ return newNode;
+
+ return HandleQuantifier(node, occurringVars,
+ newBoundVars, bindings2);
+ }
+
+ private VCExpr/*!*/ GenTypePremisses(List<VCExprVar/*!*/>/*!*/ oldBoundVars,
+ List<VCExprVar/*!*/>/*!*/ newBoundVars,
+ IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/
+ typeVarTranslation,
+ List<VCExprLetBinding/*!*/>/*!*/ typeVarBindings,
+ out List<VCTrigger/*!*/>/*!*/ triggers) {
+ Contract.Requires(cce.NonNullElements(oldBoundVars));
+ Contract.Requires(cce.NonNullElements(newBoundVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(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) {
+ 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);
+
+ for (int i = 0; i < newBoundVars.Count; ++i) {
+ VCExprVar/*!*/ oldVar = oldBoundVars[i];
+ Contract.Assert(oldVar != null);
+ VCExprVar/*!*/ newVar = newBoundVars[i];
+ Contract.Assert(newVar != null);
+
+ VCExpr/*!*/ typePremiss =
+ AxBuilderPremisses.GenVarTypeAxiom(newVar, oldVar.Type,
+ typeVarTranslation);
+ Contract.Assert(typePremiss != null);
+ if (!IsTriviallyTrue(substituter.Mutate(typePremiss,
+ typeParamSubstitution))) {
+ typePremisses.Add(typePremiss);
+ // generate a negative trigger for the variable occurrence
+ // in the type premiss
+ triggers.Add(Gen.Trigger(false,
+ HelperFuns.ToList(AxBuilderPremisses.TypeOf(newVar))));
+ }
+ }
+
+ typePremisses.TrimExcess();
+ triggers.TrimExcess();
+
+ return Gen.NAry(VCExpressionGenerator.AndOp, typePremisses);
+ }
+
+ // these optimisations should maybe be moved into a separate
+ // visitor (peep-hole optimisations)
+ private bool IsTriviallyTrue(VCExpr expr) {
+ Contract.Requires(expr != null);
+ if (expr.Equals(VCExpressionGenerator.True))
+ return true;
+
+ if (expr is VCExprNAry) {
+ VCExprNAry/*!*/ naryExpr = (VCExprNAry)expr;
+ Contract.Assert(naryExpr != null);
+ if (naryExpr.Op.Equals(VCExpressionGenerator.EqOp) &&
+ naryExpr[0].Equals(naryExpr[1]))
+ return true;
+ }
+
+ return false;
+ }
+
+ 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) {
+ Contract.Assert(var != null);
+ if (typeVarBindings.All(b => !b.V.Equals(bindings.TypeVariableBindings[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/*!*/>();
+ if (!IsUniversalQuantifier(node) ||
+ CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.Predicates) {
+ 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 =
+ GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs,
+ bindings.TypeVariableBindings,
+ typeVarBindings, out furtherTriggers);
+
+ 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);
+ Contract.Assert(newBody != null);
+
+ // assemble the new quantified formula
+
+ if (CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.None) {
+ typePremisses = VCExpressionGenerator.True;
+ }
+
+ 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) {
+ 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,
+ 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) {
+ 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) {
+ Contract.Assert(t != null);
+ List<VCExpr/*!*/>/*!*/ exprsWithLets = new List<VCExpr/*!*/>(t.Exprs.Count);
+
+ bool changed = false;
+ foreach (VCExpr/*!*/ e in t.Exprs) {
+ Contract.Assert(e != null);
+ Dictionary<VCExprVar/*!*/, object>/*!*/ freeVars =
+ FreeVariableCollector.FreeTermVariables(e);
+ Contract.Assert(freeVars != null && cce.NonNullElements(freeVars.Keys));
+ if (typeVarBindings.Any(b => freeVars.ContainsKey(b.V))) {
+ exprsWithLets.Add(Gen.Let(typeVarBindings, e));
+ changed = true;
+ } else {
+ exprsWithLets.Add(e);
+ }
+ }
+
+ if (changed)
+ triggersWithLets.Add(Gen.Trigger(t.Pos, exprsWithLets));
+ else
+ triggersWithLets.Add(t);
+ }
+
+ return triggersWithLets;
+ }
+
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class OpTypeEraserPremisses : OpTypeEraser
+ {
+
+ private TypeAxiomBuilderPremisses/*!*/ AxBuilderPremisses;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(AxBuilderPremisses != null);
+ }
+
+
+ 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) {
+ 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);
+
+ // translate the explicit type arguments
+ 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) {
+ Contract.Assert(arg != null);
+ Type/*!*/ newType = cce.NonNull(newFun.InParams[newArgs.Count]).TypedIdent.Type;
+ newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), newType));
+ }
+
+ Eraser.Polarity = oldPolarity;
+ return Gen.Function(newFun, newArgs);
+ }
+
+ 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);
+ List<Type>/*!*/ instantiations; // not used
+ Function/*!*/ select =
+ AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations);
+ Contract.Assert(select != null);
+
+ List<int>/*!*/ explicitTypeParams =
+ AxBuilderPremisses.MapTypeAbstracterPremisses
+ .ExplicitSelectTypeParams(mapType);
+ Contract.Assert(select.InParams.Count == explicitTypeParams.Count + node.Arity);
+
+ 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) {
+ Contract.Requires(bindings != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ List<Type>/*!*/ 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/*!*/>(),
+ node, bindings);
+ }
+
+ 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);
+ Contract.Assert(untypedFun.Fun.InParams.Count ==
+ untypedFun.ExplicitTypeParams.Count + node.Arity);
+
+ List<Type/*!*/>/*!*/ typeArgs =
+ ExtractTypeArgs(node,
+ oriFun.TypeParameters, untypedFun.ExplicitTypeParams);
+ return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);
+ }
+
+ private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, List<TypeVariable> 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-05-02 03:46:40 +0000