From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/VCExpr/TypeErasurePremisses.cs | 2674 ++++++++++++++++----------------- 1 file changed, 1337 insertions(+), 1337 deletions(-) (limited to 'Source/VCExpr/TypeErasurePremisses.cs') 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/*!*/ ImplicitTypeParams; - // type parameters that have to be given explicitly - public readonly List/*!*/ ExplicitTypeParams; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Fun != null); - Contract.Invariant(cce.NonNullElements(ImplicitTypeParams)); - Contract.Invariant(cce.NonNullElements(ExplicitTypeParams)); - } - - - public UntypedFunction(Function/*!*/ fun, - List/*!*/ implicitTypeParams, - List/*!*/ 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(); - MapTypeAbstracterAttr = null; - } - - // constructor to allow cloning - [NotDelayed] - internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses builder) - : base(builder) { - Contract.Requires(builder != null); - TypeFunction = builder.TypeFunction; - Typed2UntypedFunctions = - new Dictionary(builder.Typed2UntypedFunctions); - - MapTypeAbstracterAttr = - builder.MapTypeAbstracterAttr == null ? - null : new MapTypeAbstractionBuilderPremisses(this, builder.Gen, - builder.MapTypeAbstracterAttr); - } - - public override Object Clone() { - Contract.Ensures(Contract.Result() != 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() != null); - List/*!*/ 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()); - 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() != null); - Type/*!*/ fromType = cce.NonNull(castToU.InParams[0]).TypedIdent.Type; - return GenFunctionAxiom(castToU, new List(), new List(), - HelperFuns.ToList(fromType), fromType); - } - - private MapTypeAbstractionBuilderPremisses MapTypeAbstracterAttr; - - internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter { - get { - Contract.Ensures(Contract.Result() != null); - - if (MapTypeAbstracterAttr == null) - MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses(this, Gen); - return MapTypeAbstracterAttr; - } - } - - internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses { - get { - Contract.Ensures(Contract.Result() != 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() != 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/*!*/ - GenTypeParamBindings(// the original bound variables and (implicit) type parameters - List/*!*/ typeParams, List/*!*/ 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>())); - - // 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/*!*/ UtypedVars = new List(oldBoundVars.Count); - List/*!*/ originalTypes = new List(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/*!*/ typeVarBindings, - VCExpr/*!*/ typePremisses, bool universal, - VCExpr/*!*/ body) { - Contract.Requires(cce.NonNullElements(typeVarBindings)); - Contract.Requires(typePremisses != null); - Contract.Requires(body != null); - Contract.Ensures(Contract.Result() != 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(x : C a), we would extract the - // instantiation of "a" by looking at the concrete type of "x". - - public List/*!*/ - BestTypeVarExtractors(List/*!*/ vars, List/*!*/ types, - List/*!*/ 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/*!*/ typeParamBindings = new List(); - 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/*!*/ types, - List/*!*/ concreteTypeSources) { - Contract.Requires(var != null); - Contract.Requires(cce.NonNullElements(types)); - Contract.Requires(cce.NonNullElements(concreteTypeSources)); - List 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/*!*/ TypeVarExtractors(TypeVariable/*!*/ var, List/*!*/ types, - List/*!*/ 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/*!*/ res = new List(); - 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/*!*/ 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/*!*/ Typed2UntypedFunctions; - [ContractInvariantMethod] - void Typed2UntypedFunctionsInvariantMethod() { - Contract.Invariant(Typed2UntypedFunctions != null); - } - - // distinguish between implicit and explicit type parameters - internal static void SeparateTypeParams(List/*!*/ valueArgumentTypes, - List/*!*/ allTypeParams, - out List/*!*/ implicitParams, - out List/*!*/ 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/*!*/ varsInInParamTypes = new List(); - foreach (Type/*!*/ t in valueArgumentTypes) { - Contract.Assert(t != null); - varsInInParamTypes.AppendWithoutDups(t.FreeVariables); - } - - implicitParams = new List(allTypeParams.Count); - explicitParams = new List(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(), new List()); - } else { - List/*!*/ argTypes = new List(); - foreach (Variable/*!*/ v in fun.InParams) { - Contract.Assert(v != null); - argTypes.Add(v.TypedIdent.Type); - } - - List/*!*/ 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() != null); - List/*!*/ originalInTypes = new List(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/*!*/ implicitTypeParams, - List/*!*/ explicitTypeParams, - List/*!*/ 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() != null); - - if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) { - return VCExpressionGenerator.True; - } - - List/*!*/ typedInputVars = new List(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/*!*/ boundVars = new List(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 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 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())); - } - - public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary/*!*/ varMapping) { - Contract.Requires(var != null); - Contract.Requires(originalType != null); - Contract.Requires(cce.NonNullDictionaryAndValues(varMapping)); - Contract.Ensures(Contract.Result() != 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 [...]... - public List/*!*/ ExplicitSelectTypeParams(MapType type) { - Contract.Requires(type != null); - Contract.Ensures(Contract.Result>() != null); - - List res; - if (!explicitSelectTypeParamsCache.TryGetValue(type, out res)) { - List/*!*/ explicitParams, implicitParams; - TypeAxiomBuilderPremisses.SeparateTypeParams(type.Arguments.ToList(), - type.TypeParameters, - out implicitParams, - out explicitParams); - res = new List(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/*!*/>/*!*/ explicitSelectTypeParamsCache = - new Dictionary/*!*/>(); - [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/*!*/ typeParams; - List/*!*/ originalInTypes; - GenTypeAxiomParams(abstractedType, synonym, out mapTypeSynonym, - out typeParams, out originalInTypes); - - // select - List/*!*/ 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/*!*/ 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/*!*/ typeParams, - out List/*!*/ 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(); - typeParams.AddRange(abstractedType.TypeParameters); - typeParams.AddRange(abstractedType.FreeVariables); - - originalIndexTypes = new List(abstractedType.Arguments.Count + 1); - List/*!*/ mapTypeParams = new List(); - 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/*!*/ originalTypeParams, - List/*!*/ originalInTypes, - Type/*!*/ originalResult, - string/*!*/ name, - out List/*!*/ implicitTypeParams, out List/*!*/ explicitTypeParams) { - Contract.Requires(cce.NonNullElements(originalTypeParams)); - Contract.Requires(cce.NonNullElements(originalInTypes)); - Contract.Requires(originalResult != null); - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != 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(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/*!*/ typeParams, - VCExpr/*!*/ map, - List/*!*/ indexes) { - Contract.Requires(select != null); - Contract.Requires(cce.NonNullElements(typeParams)); - Contract.Requires(map != null); - Contract.Requires(cce.NonNullElements(indexes)); - Contract.Ensures(Contract.Result() != null); - - List/*!*/ selectArgs = new List(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/*!*/ indexes, VCExpr val) { - Contract.Requires(val != null); - Contract.Requires(map != null); - Contract.Requires(store != null); - Contract.Requires(cce.NonNullElements(indexes)); - Contract.Ensures(Contract.Result() != null); - List/*!*/ storeArgs = new List(indexes.Count + 2); - storeArgs.Add(map); - storeArgs.AddRange(HelperFuns.ToVCExprList(indexes)); - storeArgs.Add(val); - return Gen.Function(store, storeArgs); - } - - /// - /// 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. - /// - private VCExpr GenMapAxiom0(Function select, Function store, Type mapResult, List/*!*/ implicitTypeParamsSelect, List/*!*/ explicitTypeParamsSelect, List/*!*/ 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() != null); - int arity = store.InParams.Count - 2; - List inParams = new List(); - List quantifiedVars = new List(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 origIndexTypes = new List(arity); - List indexTypes = new List(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 typedArgs = HelperFuns.VarVector("arg", origIndexTypes, Gen); - Contract.Assert(cce.NonNullElements(typedArgs)); - List 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 typeParams = new List(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 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 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(), "mapAx0:" + select.Name, 0, body); - } - - private VCExpr GenMapAxiom1(Function select, Function store, Type mapResult, List/*!*/ explicitSelectParams) { - Contract.Requires(mapResult != null); - Contract.Requires(store != null); - Contract.Requires(select != null); - Contract.Requires(cce.NonNullElements(explicitSelectParams)); - Contract.Ensures(Contract.Result() != null); - int arity = store.InParams.Count - 2; - - List indexTypes = new List(); - 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/*!*/ indexes0 = HelperFuns.VarVector("x", indexTypes, Gen); - Contract.Assert(cce.NonNullElements(indexes0)); - List/*!*/ 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/*!*/ 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/*!*/ typeParams = new List(explicitSelectParams.Count); - List/*!*/ typeParamsExpr = new List(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/*!*/ quantifiedVars = new List(indexes0.Count + indexes1.Count + 2); - quantifiedVars.Add(val); - quantifiedVars.Add(m); - quantifiedVars.AddRange(indexes0); - quantifiedVars.AddRange(indexes1); - quantifiedVars.AddRange(typeParams); - - List/*!*/ triggers = new List(); - 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() != 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() != 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 occurringVars = new List(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/*!*/ 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/*!*/ oldBoundVars, - List/*!*/ newBoundVars, - IDictionary/*!*/ - typeVarTranslation, - List/*!*/ typeVarBindings, - out List/*!*/ 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() != 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/*!*/ typePremisses = new List(newBoundVars.Count); - triggers = new List(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/*!*/ occurringVars/*!*/, List/*!*/ 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() != null); - List/*!*/ 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/*!*/ varsWithTypeSpecs = new List(); - List/*!*/ newVarsWithTypeSpecs = new List(); - 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/*!*/ furtherTriggers; - VCExpr/*!*/ typePremisses = - GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs, - bindings.TypeVariableBindings, - typeVarBindings, out furtherTriggers); - - Contract.Assert(cce.NonNullElements(furtherTriggers)); - Contract.Assert(typePremisses != null); - List/*!*/ 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(), 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/*!*/ AddLets2Triggers(List/*!*/ triggers/*!*/, List/*!*/ typeVarBindings) { - Contract.Requires(cce.NonNullElements(triggers/*!*/)); - Contract.Requires(cce.NonNullElements(typeVarBindings)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ triggersWithLets = new List(triggers.Count); - - foreach (VCTrigger/*!*/ t in triggers) { - Contract.Assert(t != null); - List/*!*/ exprsWithLets = new List(t.Exprs.Count); - - bool changed = false; - foreach (VCExpr/*!*/ e in t.Exprs) { - Contract.Assert(e != null); - Dictionary/*!*/ 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/*!*/ typeArgs/*!*/, IEnumerable/*!*/ 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() != null); - // UGLY: the code for tracking polarities should be factored out - int oldPolarity = Eraser.Polarity; - Eraser.Polarity = 0; - - List/*!*/ newArgs = new List(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() != null); - - MapType/*!*/ mapType = node[0].Type.AsMap; - Contract.Assert(mapType != null); - List/*!*/ instantiations; // not used - Function/*!*/ select = - AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations); - Contract.Assert(select != null); - - List/*!*/ explicitTypeParams = - AxBuilderPremisses.MapTypeAbstracterPremisses - .ExplicitSelectTypeParams(mapType); - Contract.Assert(select.InParams.Count == explicitTypeParams.Count + node.Arity); - - List/*!*/ typeArgs = new List(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() != null); - List/*!*/ 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(), - node, bindings); - } - - public override VCExpr VisitBoogieFunctionOp(VCExprNAry node, VariableBindings bindings) { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != 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/*!*/ typeArgs = - ExtractTypeArgs(node, - oriFun.TypeParameters, untypedFun.ExplicitTypeParams); - return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings); - } - - private List/*!*/ ExtractTypeArgs(VCExprNAry node, List allTypeParams, List/*!*/ explicitTypeParams) { - Contract.Requires(allTypeParams != null); - Contract.Requires(node != null); - Contract.Requires(cce.NonNullElements(explicitTypeParams)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ res = new List(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/*!*/ ImplicitTypeParams; + // type parameters that have to be given explicitly + public readonly List/*!*/ ExplicitTypeParams; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Fun != null); + Contract.Invariant(cce.NonNullElements(ImplicitTypeParams)); + Contract.Invariant(cce.NonNullElements(ExplicitTypeParams)); + } + + + public UntypedFunction(Function/*!*/ fun, + List/*!*/ implicitTypeParams, + List/*!*/ 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(); + MapTypeAbstracterAttr = null; + } + + // constructor to allow cloning + [NotDelayed] + internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses builder) + : base(builder) { + Contract.Requires(builder != null); + TypeFunction = builder.TypeFunction; + Typed2UntypedFunctions = + new Dictionary(builder.Typed2UntypedFunctions); + + MapTypeAbstracterAttr = + builder.MapTypeAbstracterAttr == null ? + null : new MapTypeAbstractionBuilderPremisses(this, builder.Gen, + builder.MapTypeAbstracterAttr); + } + + public override Object Clone() { + Contract.Ensures(Contract.Result() != 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() != null); + List/*!*/ 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()); + 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() != null); + Type/*!*/ fromType = cce.NonNull(castToU.InParams[0]).TypedIdent.Type; + return GenFunctionAxiom(castToU, new List(), new List(), + HelperFuns.ToList(fromType), fromType); + } + + private MapTypeAbstractionBuilderPremisses MapTypeAbstracterAttr; + + internal override MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter { + get { + Contract.Ensures(Contract.Result() != null); + + if (MapTypeAbstracterAttr == null) + MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses(this, Gen); + return MapTypeAbstracterAttr; + } + } + + internal MapTypeAbstractionBuilderPremisses/*!*/ MapTypeAbstracterPremisses { + get { + Contract.Ensures(Contract.Result() != 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() != 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/*!*/ + GenTypeParamBindings(// the original bound variables and (implicit) type parameters + List/*!*/ typeParams, List/*!*/ 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>())); + + // 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/*!*/ UtypedVars = new List(oldBoundVars.Count); + List/*!*/ originalTypes = new List(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/*!*/ typeVarBindings, + VCExpr/*!*/ typePremisses, bool universal, + VCExpr/*!*/ body) { + Contract.Requires(cce.NonNullElements(typeVarBindings)); + Contract.Requires(typePremisses != null); + Contract.Requires(body != null); + Contract.Ensures(Contract.Result() != 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(x : C a), we would extract the + // instantiation of "a" by looking at the concrete type of "x". + + public List/*!*/ + BestTypeVarExtractors(List/*!*/ vars, List/*!*/ types, + List/*!*/ 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/*!*/ typeParamBindings = new List(); + 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/*!*/ types, + List/*!*/ concreteTypeSources) { + Contract.Requires(var != null); + Contract.Requires(cce.NonNullElements(types)); + Contract.Requires(cce.NonNullElements(concreteTypeSources)); + List 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/*!*/ TypeVarExtractors(TypeVariable/*!*/ var, List/*!*/ types, + List/*!*/ 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/*!*/ res = new List(); + 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/*!*/ 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/*!*/ Typed2UntypedFunctions; + [ContractInvariantMethod] + void Typed2UntypedFunctionsInvariantMethod() { + Contract.Invariant(Typed2UntypedFunctions != null); + } + + // distinguish between implicit and explicit type parameters + internal static void SeparateTypeParams(List/*!*/ valueArgumentTypes, + List/*!*/ allTypeParams, + out List/*!*/ implicitParams, + out List/*!*/ 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/*!*/ varsInInParamTypes = new List(); + foreach (Type/*!*/ t in valueArgumentTypes) { + Contract.Assert(t != null); + varsInInParamTypes.AppendWithoutDups(t.FreeVariables); + } + + implicitParams = new List(allTypeParams.Count); + explicitParams = new List(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(), new List()); + } else { + List/*!*/ argTypes = new List(); + foreach (Variable/*!*/ v in fun.InParams) { + Contract.Assert(v != null); + argTypes.Add(v.TypedIdent.Type); + } + + List/*!*/ 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() != null); + List/*!*/ originalInTypes = new List(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/*!*/ implicitTypeParams, + List/*!*/ explicitTypeParams, + List/*!*/ 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() != null); + + if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) { + return VCExpressionGenerator.True; + } + + List/*!*/ typedInputVars = new List(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/*!*/ boundVars = new List(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 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 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())); + } + + public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary/*!*/ varMapping) { + Contract.Requires(var != null); + Contract.Requires(originalType != null); + Contract.Requires(cce.NonNullDictionaryAndValues(varMapping)); + Contract.Ensures(Contract.Result() != 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 [...]... + public List/*!*/ ExplicitSelectTypeParams(MapType type) { + Contract.Requires(type != null); + Contract.Ensures(Contract.Result>() != null); + + List res; + if (!explicitSelectTypeParamsCache.TryGetValue(type, out res)) { + List/*!*/ explicitParams, implicitParams; + TypeAxiomBuilderPremisses.SeparateTypeParams(type.Arguments.ToList(), + type.TypeParameters, + out implicitParams, + out explicitParams); + res = new List(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/*!*/>/*!*/ explicitSelectTypeParamsCache = + new Dictionary/*!*/>(); + [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/*!*/ typeParams; + List/*!*/ originalInTypes; + GenTypeAxiomParams(abstractedType, synonym, out mapTypeSynonym, + out typeParams, out originalInTypes); + + // select + List/*!*/ 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/*!*/ 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/*!*/ typeParams, + out List/*!*/ 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(); + typeParams.AddRange(abstractedType.TypeParameters); + typeParams.AddRange(abstractedType.FreeVariables); + + originalIndexTypes = new List(abstractedType.Arguments.Count + 1); + List/*!*/ mapTypeParams = new List(); + 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/*!*/ originalTypeParams, + List/*!*/ originalInTypes, + Type/*!*/ originalResult, + string/*!*/ name, + out List/*!*/ implicitTypeParams, out List/*!*/ explicitTypeParams) { + Contract.Requires(cce.NonNullElements(originalTypeParams)); + Contract.Requires(cce.NonNullElements(originalInTypes)); + Contract.Requires(originalResult != null); + Contract.Requires(name != null); + Contract.Ensures(Contract.Result() != 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(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/*!*/ typeParams, + VCExpr/*!*/ map, + List/*!*/ indexes) { + Contract.Requires(select != null); + Contract.Requires(cce.NonNullElements(typeParams)); + Contract.Requires(map != null); + Contract.Requires(cce.NonNullElements(indexes)); + Contract.Ensures(Contract.Result() != null); + + List/*!*/ selectArgs = new List(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/*!*/ indexes, VCExpr val) { + Contract.Requires(val != null); + Contract.Requires(map != null); + Contract.Requires(store != null); + Contract.Requires(cce.NonNullElements(indexes)); + Contract.Ensures(Contract.Result() != null); + List/*!*/ storeArgs = new List(indexes.Count + 2); + storeArgs.Add(map); + storeArgs.AddRange(HelperFuns.ToVCExprList(indexes)); + storeArgs.Add(val); + return Gen.Function(store, storeArgs); + } + + /// + /// 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. + /// + private VCExpr GenMapAxiom0(Function select, Function store, Type mapResult, List/*!*/ implicitTypeParamsSelect, List/*!*/ explicitTypeParamsSelect, List/*!*/ 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() != null); + int arity = store.InParams.Count - 2; + List inParams = new List(); + List quantifiedVars = new List(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 origIndexTypes = new List(arity); + List indexTypes = new List(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 typedArgs = HelperFuns.VarVector("arg", origIndexTypes, Gen); + Contract.Assert(cce.NonNullElements(typedArgs)); + List 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 typeParams = new List(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 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 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(), "mapAx0:" + select.Name, 0, body); + } + + private VCExpr GenMapAxiom1(Function select, Function store, Type mapResult, List/*!*/ explicitSelectParams) { + Contract.Requires(mapResult != null); + Contract.Requires(store != null); + Contract.Requires(select != null); + Contract.Requires(cce.NonNullElements(explicitSelectParams)); + Contract.Ensures(Contract.Result() != null); + int arity = store.InParams.Count - 2; + + List indexTypes = new List(); + 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/*!*/ indexes0 = HelperFuns.VarVector("x", indexTypes, Gen); + Contract.Assert(cce.NonNullElements(indexes0)); + List/*!*/ 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/*!*/ 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/*!*/ typeParams = new List(explicitSelectParams.Count); + List/*!*/ typeParamsExpr = new List(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/*!*/ quantifiedVars = new List(indexes0.Count + indexes1.Count + 2); + quantifiedVars.Add(val); + quantifiedVars.Add(m); + quantifiedVars.AddRange(indexes0); + quantifiedVars.AddRange(indexes1); + quantifiedVars.AddRange(typeParams); + + List/*!*/ triggers = new List(); + 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() != 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() != 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 occurringVars = new List(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/*!*/ 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/*!*/ oldBoundVars, + List/*!*/ newBoundVars, + IDictionary/*!*/ + typeVarTranslation, + List/*!*/ typeVarBindings, + out List/*!*/ 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() != 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/*!*/ typePremisses = new List(newBoundVars.Count); + triggers = new List(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/*!*/ occurringVars/*!*/, List/*!*/ 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() != null); + List/*!*/ 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/*!*/ varsWithTypeSpecs = new List(); + List/*!*/ newVarsWithTypeSpecs = new List(); + 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/*!*/ furtherTriggers; + VCExpr/*!*/ typePremisses = + GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs, + bindings.TypeVariableBindings, + typeVarBindings, out furtherTriggers); + + Contract.Assert(cce.NonNullElements(furtherTriggers)); + Contract.Assert(typePremisses != null); + List/*!*/ 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(), 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/*!*/ AddLets2Triggers(List/*!*/ triggers/*!*/, List/*!*/ typeVarBindings) { + Contract.Requires(cce.NonNullElements(triggers/*!*/)); + Contract.Requires(cce.NonNullElements(typeVarBindings)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ triggersWithLets = new List(triggers.Count); + + foreach (VCTrigger/*!*/ t in triggers) { + Contract.Assert(t != null); + List/*!*/ exprsWithLets = new List(t.Exprs.Count); + + bool changed = false; + foreach (VCExpr/*!*/ e in t.Exprs) { + Contract.Assert(e != null); + Dictionary/*!*/ 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/*!*/ typeArgs/*!*/, IEnumerable/*!*/ 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() != null); + // UGLY: the code for tracking polarities should be factored out + int oldPolarity = Eraser.Polarity; + Eraser.Polarity = 0; + + List/*!*/ newArgs = new List(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() != null); + + MapType/*!*/ mapType = node[0].Type.AsMap; + Contract.Assert(mapType != null); + List/*!*/ instantiations; // not used + Function/*!*/ select = + AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations); + Contract.Assert(select != null); + + List/*!*/ explicitTypeParams = + AxBuilderPremisses.MapTypeAbstracterPremisses + .ExplicitSelectTypeParams(mapType); + Contract.Assert(select.InParams.Count == explicitTypeParams.Count + node.Arity); + + List/*!*/ typeArgs = new List(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() != null); + List/*!*/ 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(), + node, bindings); + } + + public override VCExpr VisitBoogieFunctionOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != 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/*!*/ typeArgs = + ExtractTypeArgs(node, + oriFun.TypeParameters, untypedFun.ExplicitTypeParams); + return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings); + } + + private List/*!*/ ExtractTypeArgs(VCExprNAry node, List allTypeParams, List/*!*/ explicitTypeParams) { + Contract.Requires(allTypeParams != null); + Contract.Requires(node != null); + Contract.Requires(cce.NonNullElements(explicitTypeParams)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ res = new List(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; + } + } + + +} -- cgit v1.2.3