From 85ffcd8f1392bf871e585fe8efb60e38bfdb2f72 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 13 Aug 2010 00:43:11 +0000 Subject: Boogie: Renaming VCExpr sources in preparation for port commit --- Source/VCExpr/TypeErasure.cs | 1176 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1176 insertions(+) create mode 100644 Source/VCExpr/TypeErasure.cs (limited to 'Source/VCExpr/TypeErasure.cs') diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs new file mode 100644 index 00000000..e0852071 --- /dev/null +++ b/Source/VCExpr/TypeErasure.cs @@ -0,0 +1,1176 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Collections; +using System.Collections.Generic; +using Microsoft.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; + +// different classes for erasing complex types in VCExprs, replacing them +// with axioms that can be handled by theorem provers and SMT solvers + +namespace Microsoft.Boogie.TypeErasure +{ + using Microsoft.Boogie.VCExprAST; + + // some functionality that is needed in many places (and that should + // really be provided by the Spec# container classes; maybe one + // could integrate the functions in a nicer way?) + public class HelperFuns { + + public static Function! BoogieFunction(string! name, List! typeParams, + params Type[]! types) + requires types.Length > 0; + requires forall{int i in (0:types.Length); types[i] != null}; + { + VariableSeq! args = new VariableSeq (); + for (int i = 0; i < types.Length - 1; ++i) + args.Add(new Formal (Token.NoToken, + new TypedIdent (Token.NoToken, "arg" + i, (!)types[i]), + true)); + Formal! result = new Formal (Token.NoToken, + new TypedIdent (Token.NoToken, "res", + (!)types[types.Length - 1]), + false); + return new Function (Token.NoToken, name, ToSeq(typeParams), args, result); + } + + public static Function! BoogieFunction(string! name, params Type[]! types) { + return BoogieFunction(name, new List (), types); + } + + // boogie function where all arguments and the result have the same type U + public static Function! UniformBoogieFunction(string! name, int arity, Type! U) { + Type[]! types = new Type [arity + 1]; + for (int i = 0; i < arity + 1; ++i) + types[i] = U; + return BoogieFunction(name, types); + } + + public static List! GenVarsForInParams(Function! fun, + VCExpressionGenerator! gen) { + List! arguments = new List (fun.InParams.Length); + foreach (Formal! f in fun.InParams) { + VCExprVar! var = gen.Variable(f.Name, f.TypedIdent.Type); + arguments.Add(var); + } + return arguments; + } + + public static List! ToList (params T[]! args) { + List! res = new List (args.Length); + foreach (T t in args) + res.Add((!)t); + return res; + } + + public static List! ToList(TypeVariableSeq! seq) { + List! res = new List (seq.Length); + foreach (TypeVariable! var in seq) + res.Add(var); + return res; + } + + public static TypeVariableSeq! ToSeq(List! list) { + TypeVariableSeq! res = new TypeVariableSeq (); + foreach (TypeVariable! var in list) + res.Add(var); + return res; + } + + public static List! Intersect(List! a, List! b) { + List! res = new List (Math.Min(a.Count, b.Count)); + foreach (T x in a) + if (b.Contains(x)) + res.Add(x); + res.TrimExcess(); + return res; + } + + public static List>! ToPairList(IDictionary! dict) { + List>! res = new List> (dict); + return res; + } + + public static void AddRangeWithoutDups(IEnumerable! fromList, List! toList) { + foreach (T t in fromList) + if (!toList.Contains(t)) + toList.Add(t); + } + + public static void AddFreeVariablesWithoutDups(Type! type, List! toList) { + foreach (TypeVariable! var in type.FreeVariables) { + if (!toList.Contains(var)) + toList.Add(var); + } + } + + public static List! ToVCExprList(List! list) { + List! res = new List (list.Count); + foreach (VCExprVar! var in list) + res.Add(var); + return res; + } + + public static List! VarVector(string! baseName, int num, Type! type, + VCExpressionGenerator! gen) { + List! res = new List (num); + for (int i = 0; i < num; ++i) + res.Add(gen.Variable(baseName + i, type)); + return res; + } + + public static List! VarVector(string! baseName, List! types, + VCExpressionGenerator! gen) { + List! res = new List (types.Count); + for (int i = 0; i < types.Count; ++i) + res.Add(gen.Variable(baseName + i, types[i])); + return res; + } + } + + ////////////////////////////////////////////////////////////////////////////// + + internal struct TypeCtorRepr { + // function that represents the application of the type constructor + // to smaller types + public readonly Function! Ctor; + // left-inverse functions that extract the subtypes of a compound type + public readonly List! Dtors; + + public TypeCtorRepr(Function! ctor, List! dtors) + requires ctor.InParams.Length == dtors.Count; { + this.Ctor = ctor; + this.Dtors = dtors; + } + } + + ////////////////////////////////////////////////////////////////////////////// + + // The class responsible for creating and keeping track of all + // axioms related to the type system. This abstract class is made + // concrete in two subclasses, one for type erasure with type + // premisses in quantifiers (the semantic approach), and one for + // type erasure with explicit type arguments of polymorphic + // functions (the syntacted approach). + public abstract class TypeAxiomBuilder : ICloneable { + + protected readonly VCExpressionGenerator! Gen; + + internal abstract MapTypeAbstractionBuilder! MapTypeAbstracter { get; } + + /////////////////////////////////////////////////////////////////////////// + // Type Axioms + + // list in which all typed axioms are collected + private readonly List! AllTypeAxioms; + + // list in which type axioms are incrementally collected + private readonly List! IncTypeAxioms; + + internal void AddTypeAxiom(VCExpr! axiom) { + AllTypeAxioms.Add(axiom); + IncTypeAxioms.Add(axiom); + } + + // Return all axioms that were added since the last time NewAxioms + // was called + public VCExpr! GetNewAxioms() { + VCExpr! res = Gen.NAry(VCExpressionGenerator.AndOp, IncTypeAxioms); + IncTypeAxioms.Clear(); + return res; + } + + // mapping from a type to its constructor number/index + private readonly Function! Ctor; + private BigNum CurrentCtorNum; + + private VCExpr! GenCtorAssignment(VCExpr! typeRepr) { + if (CommandLineOptions.Clo.TypeEncodingMethod + == CommandLineOptions.TypeEncoding.None) + return VCExpressionGenerator.True; + + VCExpr! res = Gen.Eq(Gen.Function(Ctor, typeRepr), + Gen.Integer(CurrentCtorNum)); + CurrentCtorNum = CurrentCtorNum + BigNum.ONE; + return res; + } + + private VCExpr! GenCtorAssignment(Function! typeRepr) { + if (CommandLineOptions.Clo.TypeEncodingMethod + == CommandLineOptions.TypeEncoding.None) + return VCExpressionGenerator.True; + + List! quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen); + VCExpr! eq = + GenCtorAssignment(Gen.Function(typeRepr, + HelperFuns.ToVCExprList(quantifiedVars))); + + if (typeRepr.InParams.Length == 0) + return eq; + + return Gen.Forall(quantifiedVars, new List (), + "ctor:" + typeRepr.Name, eq); + } + + // generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi) + protected VCExpr! GenLeftInverseAxiom(Function! fun, Function! invFun, int dtorNum) { + List! quantifiedVars = HelperFuns.GenVarsForInParams(fun, Gen); + + VCExpr! funApp = Gen.Function(fun, HelperFuns.ToVCExprList(quantifiedVars)); + VCExpr! lhs = Gen.Function(invFun, funApp); + VCExpr! rhs = quantifiedVars[dtorNum]; + VCExpr! eq = Gen.Eq(lhs, rhs); + + List! triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp))); + return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, eq); + } + + /////////////////////////////////////////////////////////////////////////// + + // the type of everything that is not int, bool, or a type + private readonly TypeCtorDecl! UDecl; + public readonly Type! U; + + // the type of types + private readonly TypeCtorDecl! TDecl; + public readonly Type! T; + + public abstract Type! TypeAfterErasure(Type! type); + public abstract bool UnchangedType(Type! type); + + /////////////////////////////////////////////////////////////////////////// + // Symbols for representing types + + private readonly IDictionary! BasicTypeReprs; + + private VCExpr! GetBasicTypeRepr(Type! type) + requires type.IsBasic || type.IsBv; { + VCExpr res; + if (!BasicTypeReprs.TryGetValue(type, out res)) { + res = Gen.Function(HelperFuns.BoogieFunction(type.ToString() + "Type", T)); + AddTypeAxiom(GenCtorAssignment(res)); + BasicTypeReprs.Add(type, res); + } + return (!)res; + } + + private readonly IDictionary! TypeCtorReprs; + + internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl! decl) { + TypeCtorRepr reprSet; + if (!TypeCtorReprs.TryGetValue(decl, out reprSet)) { + Function! ctor = HelperFuns.UniformBoogieFunction(decl.Name + "Type", decl.Arity, T); + AddTypeAxiom(GenCtorAssignment(ctor)); + + List! dtors = new List(decl.Arity); + for (int i = 0; i < decl.Arity; ++i) { + Function! dtor = HelperFuns.UniformBoogieFunction(decl.Name + "TypeInv" + i, 1, T); + dtors.Add(dtor); + AddTypeAxiom(GenLeftInverseAxiom(ctor, dtor, i)); + } + + reprSet = new TypeCtorRepr(ctor, dtors); + TypeCtorReprs.Add(decl, reprSet); + } + + return reprSet; + } + + public Function! GetTypeCtorRepr(TypeCtorDecl! decl) { + return GetTypeCtorReprStruct(decl).Ctor; + } + + public Function! GetTypeDtor(TypeCtorDecl! decl, int num) { + return GetTypeCtorReprStruct(decl).Dtors[num]; + } + + // mapping from free type variables to VCExpr variables + private readonly IDictionary! TypeVariableMapping; + + public VCExprVar! Typed2Untyped(TypeVariable! var) { + VCExprVar res; + if (!TypeVariableMapping.TryGetValue(var, out res)) { + res = new VCExprVar (var.Name, T); + TypeVariableMapping.Add(var, res); + } + return (!)res; + } + + + //////////////////////////////////////////////////////////////////////////// + // Symbols for representing variables and constants + + // Globally defined variables + private readonly IDictionary! Typed2UntypedVariables; + + // This method must only be used for free (unbound) variables + public VCExprVar! Typed2Untyped(VCExprVar! var) { + VCExprVar res; + if (!Typed2UntypedVariables.TryGetValue(var, out res)) { + res = Gen.Variable(var.Name, TypeAfterErasure(var.Type)); + Typed2UntypedVariables.Add(var, res); + AddVarTypeAxiom(res, var.Type); + } + return (!)res; + } + + protected abstract void AddVarTypeAxiom(VCExprVar! var, Type! originalType); + + /////////////////////////////////////////////////////////////////////////// + // Translation function from types to their term representation + + public VCExpr! Type2Term(Type! type, + IDictionary! varMapping) { + // + if (type.IsBasic || type.IsBv) { + // + return GetBasicTypeRepr(type); + // + } else if (type.IsCtor) { + // + CtorType ctype = type.AsCtor; + Function! repr = GetTypeCtorRepr(ctype.Decl); + List! args = new List (ctype.Arguments.Length); + foreach (Type! t in ctype.Arguments) + args.Add(Type2Term(t, varMapping)); + return Gen.Function(repr, args); + // + } else if (type.IsVariable) { + // + VCExpr res; + if (!varMapping.TryGetValue(type.AsVariable, out res)) + // then the variable is free and we bind it at this point to a term + // variable + res = Typed2Untyped(type.AsVariable); + return (!)res; + // + } else if (type.IsMap) { + // + return Type2Term(MapTypeAbstracter.AbstractMapType(type.AsMap), varMapping); + // + } else { + System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + type); + assert false; // please the compiler + } + } + + //////////////////////////////////////////////////////////////////////////// + + public TypeAxiomBuilder(VCExpressionGenerator! gen) { + this.Gen = gen; + AllTypeAxioms = new List (); + IncTypeAxioms = new List (); + BasicTypeReprs = new Dictionary (); + CurrentCtorNum = BigNum.ZERO; + TypeCtorReprs = new Dictionary (); + TypeVariableMapping = new Dictionary (); + Typed2UntypedVariables = new Dictionary (); + + TypeCtorDecl! uDecl = new TypeCtorDecl(Token.NoToken, "U", 0); + UDecl = uDecl; + Type! u = new CtorType (Token.NoToken, uDecl, new TypeSeq ()); + U = u; + + TypeCtorDecl! tDecl = new TypeCtorDecl(Token.NoToken, "T", 0); + TDecl = tDecl; + Type! t = new CtorType (Token.NoToken, tDecl, new TypeSeq ()); + T = t; + + Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int); + } + + public virtual void Setup() { + GetBasicTypeRepr(Type.Int); + GetBasicTypeRepr(Type.Bool); + } + + // constructor to allow cloning + internal TypeAxiomBuilder(TypeAxiomBuilder! builder) { + Gen = builder.Gen; + AllTypeAxioms = new List (builder.AllTypeAxioms); + IncTypeAxioms = new List (builder.IncTypeAxioms); + + UDecl = builder.UDecl; + U = builder.U; + + TDecl = builder.TDecl; + T = builder.T; + + Ctor = builder.Ctor; + CurrentCtorNum = builder.CurrentCtorNum; + + BasicTypeReprs = new Dictionary (builder.BasicTypeReprs); + TypeCtorReprs = new Dictionary (builder.TypeCtorReprs); + + TypeVariableMapping = + new Dictionary (builder.TypeVariableMapping); + Typed2UntypedVariables = + new Dictionary (builder.Typed2UntypedVariables); + } + + public abstract Object! Clone(); + } + + ////////////////////////////////////////////////////////////////////////////// + + // Subclass of the TypeAxiomBuilder that provides all functionality + // to deal with native sorts of a theorem prover (that are the only + // types left after erasing all other types). Currently, these are: + // + // U ... sort of all individuals/objects/values + // T ... sort of all types + // int ... integers + // bool ... booleans + + public abstract class TypeAxiomBuilderIntBoolU : TypeAxiomBuilder { + + public TypeAxiomBuilderIntBoolU(VCExpressionGenerator! gen) { + base(gen); + TypeCasts = new Dictionary (); + } + + // constructor to allow cloning + internal TypeAxiomBuilderIntBoolU(TypeAxiomBuilderIntBoolU! builder) { + base(builder); + TypeCasts = new Dictionary (builder.TypeCasts); + } + + public override void Setup() { + base.Setup(); + + GetTypeCasts(Type.Int); + GetTypeCasts(Type.Bool); + } + + // generate inverse axioms for casts (castToU(castFromU(x)) = x, under certain premisses) + protected abstract VCExpr! GenReverseCastAxiom(Function! castToU, Function! castFromU); + + protected VCExpr! GenReverseCastEq(Function! castToU, Function! castFromU, + out VCExprVar! var, out List! triggers) { + var = Gen.Variable("x", U); + + VCExpr inner = Gen.Function(castFromU, var); + VCExpr lhs = Gen.Function(castToU, inner); + triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(inner))); + + return Gen.Eq(lhs, var); + } + + protected abstract VCExpr! GenCastTypeAxioms(Function! castToU, Function! castFromU); + + /////////////////////////////////////////////////////////////////////////// + // storage of type casts for types that are supposed to be left over in the + // VCs (like int, bool, bitvectors) + + private readonly IDictionary! TypeCasts; + + private TypeCastSet GetTypeCasts(Type! type) { + TypeCastSet res; + if (!TypeCasts.TryGetValue(type, out res)) { + Function! castToU = HelperFuns.BoogieFunction(type.ToString() + "_2_U", type, U); + Function! castFromU = HelperFuns.BoogieFunction("U_2_" + type.ToString(), U, type); + + AddTypeAxiom(GenLeftInverseAxiom(castToU, castFromU, 0)); + AddTypeAxiom(GenReverseCastAxiom(castToU, castFromU)); + AddTypeAxiom(GenCastTypeAxioms(castToU, castFromU)); + + res = new TypeCastSet (castToU, castFromU); + TypeCasts.Add(type, res); + } + return res; + } + + public Function! CastTo(Type! type) + requires UnchangedType(type); { + return GetTypeCasts(type).CastFromU; + } + + public Function! CastFrom(Type! type) + requires UnchangedType(type); { + return GetTypeCasts(type).CastToU; + } + + private struct TypeCastSet { + public readonly Function! CastToU; + public readonly Function! CastFromU; + + public TypeCastSet(Function! castToU, Function! castFromU) { + CastToU = castToU; + CastFromU = castFromU; + } + } + + public bool IsCast(Function! fun) { + if (fun.InParams.Length != 1) + return false; + Type! inType = ((!)fun.InParams[0]).TypedIdent.Type; + if (inType.Equals(U)) { + Type! outType = ((!)fun.OutParams[0]).TypedIdent.Type; + if (!TypeCasts.ContainsKey(outType)) + return false; + return fun.Equals(CastTo(outType)); + } else { + if (!TypeCasts.ContainsKey(inType)) + return false; + Type! outType = ((!)fun.OutParams[0]).TypedIdent.Type; + if (!outType.Equals(U)) + return false; + return fun.Equals(CastFrom(inType)); + } + } + + //////////////////////////////////////////////////////////////////////////// + + // the only types that we allow in "untyped" expressions are U, + // Type.Int, and Type.Bool + + public override Type! TypeAfterErasure(Type! type) { + if (UnchangedType(type)) + // these types are kept + return type; + else + // all other types are replaced by U + return U; + } + + [Pure] + public override bool UnchangedType(Type! type) { + return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.UseArrayTheory); + } + + public VCExpr! Cast(VCExpr! expr, Type! toType) + requires expr.Type.Equals(U) || UnchangedType(expr.Type); + requires toType.Equals(U) || UnchangedType(toType); + { + if (expr.Type.Equals(toType)) + return expr; + + if (toType.Equals(U)) { + return Gen.Function(CastFrom(expr.Type), expr); + } else { + assert expr.Type.Equals(U); + return Gen.Function(CastTo(toType), expr); + } + } + + public List! CastSeq(List! exprs, Type! toType) { + List! res = new List (exprs.Count); + foreach (VCExpr! expr in exprs) + res.Add(Cast(expr, toType)); + return res; + } + + + } + + ////////////////////////////////////////////////////////////////////////////// + // Class for computing most general abstractions of map types. An abstraction + // of a map type t is a maptype t' in which closed proper subtypes have been replaced + // with type variables. E.g., an abstraction of [C a, int]a would be [C a, b]a. + // We subsequently consider most general abstractions as ordinary parametrised types, + // i.e., "[C a, b]a" would be considered as a type "M b" with polymorphically typed + // access functions + // + // select(M b, C a, b) returns (a) + // store(M b, C a, b, a) returns (M b) + + internal abstract class MapTypeAbstractionBuilder { + + protected readonly TypeAxiomBuilder! AxBuilder; + protected readonly VCExpressionGenerator! Gen; + + internal MapTypeAbstractionBuilder(TypeAxiomBuilder! axBuilder, + VCExpressionGenerator! gen) { + this.AxBuilder = axBuilder; + this.Gen = gen; + AbstractionVariables = new List (); + ClassRepresentations = new Dictionary (); + } + + // constructor for cloning + internal MapTypeAbstractionBuilder(TypeAxiomBuilder! axBuilder, + VCExpressionGenerator! gen, + MapTypeAbstractionBuilder! builder) { + this.AxBuilder = axBuilder; + this.Gen = gen; + AbstractionVariables = + new List (builder.AbstractionVariables); + ClassRepresentations = + new Dictionary (builder.ClassRepresentations); + } + + /////////////////////////////////////////////////////////////////////////// + // Type variables used in the abstractions. We use the same variables in the + // same order in all abstractions in order to obtain comparable abstractions + // (equals, hashcode) + + private readonly List! AbstractionVariables; + + private TypeVariable! AbstractionVariable(int num) + requires num >= 0; { + while (AbstractionVariables.Count <= num) + AbstractionVariables.Add(new TypeVariable (Token.NoToken, + "aVar" + AbstractionVariables.Count)); + return AbstractionVariables[num]; + } + + /////////////////////////////////////////////////////////////////////////// + // The untyped representation of a class of map types, i.e., of a map type + // [A0, A1, ...] R, where the argument types and the result type + // possibly contain free type variables. For each such class, a separate type + // constructor and separate select/store functions are introduced. + + protected struct MapTypeClassRepresentation { + public readonly TypeCtorDecl! RepresentingType; + public readonly Function! Select; + public readonly Function! Store; + + public MapTypeClassRepresentation(TypeCtorDecl! representingType, + Function! select, Function! store) { + this.RepresentingType = representingType; + this.Select = select; + this.Store = store; + } + } + + private readonly IDictionary! ClassRepresentations; + + protected MapTypeClassRepresentation GetClassRepresentation(MapType! abstractedType) { + MapTypeClassRepresentation res; + if (!ClassRepresentations.TryGetValue(abstractedType, out res)) { + int num = ClassRepresentations.Count; + TypeCtorDecl! synonym = + new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Length); + + Function! select, store; + GenSelectStoreFunctions(abstractedType, synonym, out select, out store); + + res = new MapTypeClassRepresentation(synonym, select, store); + ClassRepresentations.Add(abstractedType, res); + } + return res; + } + + // the actual select and store functions are generated by the + // concrete subclasses of this class + protected abstract void GenSelectStoreFunctions(MapType! abstractedType, + TypeCtorDecl! synonymDecl, + out Function! select, out Function! store); + + /////////////////////////////////////////////////////////////////////////// + + public Function! Select(MapType! rawType, out TypeSeq! instantiations) { + return AbstractAndGetRepresentation(rawType, out instantiations).Select; + } + + public Function! Store(MapType! rawType, out TypeSeq! instantiations) { + return AbstractAndGetRepresentation(rawType, out instantiations).Store; + } + + private MapTypeClassRepresentation + AbstractAndGetRepresentation(MapType! rawType, out TypeSeq! instantiations) { + instantiations = new TypeSeq (); + MapType! abstraction = ThinOutMapType(rawType, instantiations); + return GetClassRepresentation(abstraction); + } + + public CtorType! AbstractMapType(MapType! rawType) { + TypeSeq! instantiations = new TypeSeq (); + MapType! abstraction = ThinOutMapType(rawType, instantiations); + + MapTypeClassRepresentation repr = GetClassRepresentation(abstraction); + assume repr.RepresentingType.Arity == instantiations.Length; + return new CtorType(Token.NoToken, repr.RepresentingType, instantiations); + } + + // TODO: cache the result of this operation + protected MapType! ThinOutMapType(MapType! rawType, + TypeSeq! instantiations) { + TypeSeq! newArguments = new TypeSeq (); + foreach (Type! subtype in rawType.Arguments) + newArguments.Add(ThinOutType(subtype, rawType.TypeParameters, + instantiations)); + Type! newResult = ThinOutType(rawType.Result, rawType.TypeParameters, + instantiations); + return new MapType(Token.NoToken, rawType.TypeParameters, newArguments, newResult); + } + + private Type! ThinOutType(Type! rawType, TypeVariableSeq! boundTypeParams, + // the instantiations of inserted type variables, + // the order corresponds to the order in which + // "AbstractionVariable(int)" delivers variables + TypeSeq! instantiations) { + + if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType)) + return rawType; + + if (forall{TypeVariable! var in rawType.FreeVariables; + !boundTypeParams.Has(var)}) { + // Bingo! + // if the type does not contain any bound variables, we can simply + // replace it with a type variable + TypeVariable! abstractionVar = AbstractionVariable(instantiations.Length); + assume !boundTypeParams.Has(abstractionVar); + instantiations.Add(rawType); + return abstractionVar; + } + + if (rawType.IsVariable) { + // + // then the variable has to be bound, we cannot do anything + TypeVariable! rawVar = rawType.AsVariable; + assume boundTypeParams.Has(rawVar); + return rawVar; + // + } else if (rawType.IsMap) { + // + // recursively abstract this map type and continue abstracting + CtorType! abstraction = AbstractMapType(rawType.AsMap); + return ThinOutType(abstraction, boundTypeParams, instantiations); + // + } else if (rawType.IsCtor) { + // + // traverse the subtypes + CtorType! rawCtorType = rawType.AsCtor; + TypeSeq! newArguments = new TypeSeq (); + foreach (Type! subtype in rawCtorType.Arguments) + newArguments.Add(ThinOutType(subtype, boundTypeParams, + instantiations)); + return new CtorType(Token.NoToken, rawCtorType.Decl, newArguments); + // + } else { + System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + rawType); + return rawType; // compiler appeasement policy + } + } + + } + + ////////////////////////////////////////////////////////////////////////////// + + public class VariableBindings { + public readonly IDictionary! VCExprVarBindings; + public readonly IDictionary! TypeVariableBindings; + + public VariableBindings(IDictionary! vcExprVarBindings, + IDictionary! typeVariableBindings) { + this.VCExprVarBindings = vcExprVarBindings; + this.TypeVariableBindings = typeVariableBindings; + } + + public VariableBindings() { + this (new Dictionary (), + new Dictionary ()); + } + + public VariableBindings! Clone() { + IDictionary! newVCExprVarBindings = + new Dictionary (); + foreach (KeyValuePair pair in VCExprVarBindings) + newVCExprVarBindings.Add(pair); + IDictionary! newTypeVariableBindings = + new Dictionary (); + foreach (KeyValuePair pair in TypeVariableBindings) + newTypeVariableBindings.Add(pair); + return new VariableBindings(newVCExprVarBindings, newTypeVariableBindings); + } + } + + ////////////////////////////////////////////////////////////////////////////// + + // The central class for turning types VCExprs into untyped + // VCExprs. This class makes use of the type axiom builder to manage + // the available types and symbols. + + public abstract class TypeEraser : MutatingVCExprVisitor { + + protected readonly TypeAxiomBuilderIntBoolU! AxBuilder; + + protected abstract OpTypeEraser! OpEraser { get; } + + //////////////////////////////////////////////////////////////////////////// + + public TypeEraser(TypeAxiomBuilderIntBoolU! axBuilder, VCExpressionGenerator! gen) { + base(gen); + AxBuilder = axBuilder; + } + + public VCExpr! Erase(VCExpr! expr, int polarity) + requires polarity >= -1 && polarity <= 1; { + this.Polarity = polarity; + return Mutate(expr, new VariableBindings()); + } + + internal int Polarity = 1; // 1 for positive, -1 for negative, 0 for both + + //////////////////////////////////////////////////////////////////////////// + + public override VCExpr! Visit(VCExprLiteral! node, VariableBindings! bindings) { + assume node.Type == Type.Bool || node.Type == Type.Int; + return node; + } + + //////////////////////////////////////////////////////////////////////////// + + public override VCExpr! Visit(VCExprNAry! node, VariableBindings! bindings) { + VCExprOp! op = node.Op; + if (op == VCExpressionGenerator.AndOp || op == VCExpressionGenerator.OrOp) + // more efficient on large conjunctions/disjunctions + return base.Visit(node, bindings); + + // the visitor that handles all other operators + return node.Accept(OpEraser, bindings); + } + + // this method is called by MutatingVCExprVisitor.Visit(VCExprNAry, ...) + protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode, + List! newSubExprs, + bool changed, + VariableBindings! bindings) { + assume originalNode.Op == VCExpressionGenerator.AndOp || + originalNode.Op == VCExpressionGenerator.OrOp; + return Gen.Function(originalNode.Op, + AxBuilder.Cast(newSubExprs[0], Type.Bool), + AxBuilder.Cast(newSubExprs[1], Type.Bool)); + } + + //////////////////////////////////////////////////////////////////////////// + + public override VCExpr! Visit(VCExprVar! node, VariableBindings! bindings) { + VCExprVar res; + if (!bindings.VCExprVarBindings.TryGetValue(node, out res)) + return AxBuilder.Typed2Untyped(node); + return (!)res; + } + + //////////////////////////////////////////////////////////////////////////// + + protected bool IsUniversalQuantifier(VCExprQuantifier! node) { + return Polarity == 1 && node.Quan == Quantifier.EX || + Polarity == -1 && node.Quan == Quantifier.ALL; + } + + protected List! BoundVarsAfterErasure(List! oldBoundVars, + // the mapping between old and new variables + // is added to this bindings-object + VariableBindings! bindings) { + List! newBoundVars = new List (oldBoundVars.Count); + foreach (VCExprVar! var in oldBoundVars) { + Type! newType = AxBuilder.TypeAfterErasure(var.Type); + VCExprVar! newVar = Gen.Variable(var.Name, newType); + newBoundVars.Add(newVar); + bindings.VCExprVarBindings.Add(var, newVar); + } + return newBoundVars; + } + + // We check whether casts Int2U or Bool2U on the bound variables + // occur in triggers. In case a trigger like f(Int2U(x)) occurs, + // it may be better to give variable x the type U and remove the + // cast. The following method returns true if the quantifier + // should be translated again with a different typing + protected bool RedoQuantifier(VCExprQuantifier! node, + VCExprQuantifier! newNode, + // the bound vars that actually occur in the body or + // in any of the triggers + List! occurringVars, + VariableBindings! oldBindings, + out VariableBindings! newBindings, + out List! newBoundVars) { + List castVariables = + VariableCastCollector.FindCastVariables(node, newNode, AxBuilder); + if (castVariables.Count == 0) { + newBindings = oldBindings; // to make the compiler happy + newBoundVars = newNode.BoundVars; // to make the compiler happy + return false; + } + + // redo everything with a different typing ... + + newBindings = oldBindings.Clone(); + newBoundVars = new List (node.BoundVars.Count); + foreach (VCExprVar! var in node.BoundVars) { + Type! newType = + castVariables.Contains(var) ? AxBuilder.U + : AxBuilder.TypeAfterErasure(var.Type); + VCExprVar! newVar = Gen.Variable(var.Name, newType); + newBoundVars.Add(newVar); + newBindings.VCExprVarBindings.Add(var, newVar); + } + + return true; + } + + //////////////////////////////////////////////////////////////////////////// + + public override VCExpr! Visit(VCExprLet! node, VariableBindings! bindings) { + VariableBindings! newVarBindings = bindings.Clone(); + + List! newBoundVars = new List (node.BoundVars.Count); + foreach (VCExprVar! var in node.BoundVars) { + Type! newType = AxBuilder.TypeAfterErasure(var.Type); + VCExprVar! newVar = Gen.Variable(var.Name, newType); + newBoundVars.Add(newVar); + newVarBindings.VCExprVarBindings.Add(var, newVar); + } + + List! newbindings = new List (node.Length); + for (int i = 0; i < node.Length; ++i) { + VCExprLetBinding! binding = node[i]; + VCExprVar! newVar = newBoundVars[i]; + Type! newType = newVar.Type; + + VCExpr! newE = AxBuilder.Cast(Mutate(binding.E, newVarBindings), newType); + newbindings.Add(Gen.LetBinding(newVar, newE)); + } + + VCExpr! newbody = Mutate(node.Body, newVarBindings); + return Gen.Let(newbindings, newbody); + } + } + + ////////////////////////////////////////////////////////////////////////////// + + public abstract class OpTypeEraser : StandardVCExprOpVisitor { + + protected readonly TypeAxiomBuilderIntBoolU! AxBuilder; + + protected readonly TypeEraser! Eraser; + protected readonly VCExpressionGenerator! Gen; + + public OpTypeEraser(TypeEraser! eraser, TypeAxiomBuilderIntBoolU! axBuilder, + VCExpressionGenerator! gen) { + this.AxBuilder = axBuilder; + this.Eraser = eraser; + this.Gen = gen; + } + + protected override VCExpr! StandardResult(VCExprNAry! node, VariableBindings! bindings) { + System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node); + assert false; // to please the compiler + } + + private List! MutateSeq(VCExprNAry! node, VariableBindings! bindings, + int newPolarity) { + int oldPolarity = Eraser.Polarity; + Eraser.Polarity = newPolarity; + List! newArgs = Eraser.MutateSeq(node, bindings); + Eraser.Polarity = oldPolarity; + return newArgs; + } + + private VCExpr! CastArguments(VCExprNAry! node, Type! argType, VariableBindings! bindings, + int newPolarity) { + return Gen.Function(node.Op, + AxBuilder.CastSeq(MutateSeq(node, bindings, newPolarity), + argType)); + } + + // Cast the arguments of the node to their old type if necessary and possible; otherwise use + // their new type (int, bool, or U) + private VCExpr! CastArgumentsToOldType(VCExprNAry! node, VariableBindings! bindings, + int newPolarity) + requires node.Arity > 0; { + + List! newArgs = MutateSeq(node, bindings, newPolarity); + Type! oldType = node[0].Type; + if (AxBuilder.UnchangedType(oldType) && + forall{int i in (1:node.Arity); node[i].Type.Equals(oldType)}) + return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType)); + else + return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U)); + } + + /////////////////////////////////////////////////////////////////////////// + + public override VCExpr! VisitNotOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Bool, bindings, -Eraser.Polarity); + } + public override VCExpr! VisitEqOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr! VisitNeqOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr! VisitImpliesOp (VCExprNAry! node, VariableBindings! bindings) { + // UGLY: the code for tracking polarities should be factored out + List! newArgs = new List (2); + Eraser.Polarity = -Eraser.Polarity; + newArgs.Add(Eraser.Mutate(node[0], bindings)); + Eraser.Polarity = -Eraser.Polarity; + newArgs.Add(Eraser.Mutate(node[1], bindings)); + return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, Type.Bool)); + } + public override VCExpr! VisitDistinctOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr! VisitLabelOp (VCExprNAry! node, VariableBindings! bindings) { + // argument of the label operator should always be a formula + // (at least for Simplify ... should this be ensured at a later point?) + return CastArguments(node, Type.Bool, bindings, Eraser.Polarity); + } + public override VCExpr! VisitIfThenElseOp (VCExprNAry! node, VariableBindings! bindings) { + List! newArgs = MutateSeq(node, bindings, 0); + newArgs[0] = AxBuilder.Cast(newArgs[0], Type.Bool); + Type t = node.Type; + if (!AxBuilder.UnchangedType(t)) { + t = AxBuilder.U; + } + newArgs[1] = AxBuilder.Cast(newArgs[1], t); + newArgs[2] = AxBuilder.Cast(newArgs[2], t); + return Gen.Function(node.Op, newArgs); + } + public override VCExpr! VisitCustomOp (VCExprNAry! node, VariableBindings! bindings) { + List! newArgs = MutateSeq(node, bindings, 0); + return Gen.Function(node.Op, newArgs); + } + public override VCExpr! VisitAddOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitSubOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitMulOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitDivOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitModOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitLtOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitLeOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitGtOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitGeOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, Type.Int, bindings, 0); + } + public override VCExpr! VisitSubtypeOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArguments(node, AxBuilder.U, bindings, 0); + } + public override VCExpr! VisitBvOp (VCExprNAry! node, VariableBindings! bindings) { + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr! VisitBvExtractOp(VCExprNAry! node, VariableBindings! bindings) { + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr! VisitBvConcatOp (VCExprNAry! node, VariableBindings! bindings) { + List! newArgs = MutateSeq(node, bindings, 0); + + // each argument is cast to its old type + assert newArgs.Count == node.Arity && newArgs.Count == 2; + VCExpr! arg0 = AxBuilder.Cast(newArgs[0], node[0].Type); + VCExpr! arg1 = AxBuilder.Cast(newArgs[1], node[1].Type); + + return Gen.Function(node.Op, arg0, arg1); + } + + } + + ////////////////////////////////////////////////////////////////////////////// + + /// + /// Collect all variables x occurring in expressions of the form Int2U(x) or Bool2U(x), and + /// collect all variables x occurring outside such forms. + /// + internal class VariableCastCollector : TraversingVCExprVisitor { + /// + /// Determine those bound variables in "oldNode" all of whose relevant uses + /// have to be cast in potential triggers in "newNode". It is assume that + /// the bound variables of "oldNode" correspond to the first bound + /// variables of "newNode". + /// + public static List! FindCastVariables(VCExprQuantifier! oldNode, + VCExprQuantifier! newNode, + TypeAxiomBuilderIntBoolU! axBuilder) { + VariableCastCollector! collector = new VariableCastCollector(axBuilder); + if (exists{VCTrigger! trigger in newNode.Triggers; trigger.Pos}) { + // look in the given triggers + foreach (VCTrigger! trigger in newNode.Triggers) + if (trigger.Pos) + foreach (VCExpr! expr in trigger.Exprs) + collector.Traverse(expr, true); + } else { + // look in the body of the quantifier + collector.Traverse(newNode.Body, true); + } + + List! castVariables = new List (collector.varsInCasts.Count); + foreach (VCExprVar! castVar in collector.varsInCasts) { + int i = newNode.BoundVars.IndexOf(castVar); + if (0 <= i && i < oldNode.BoundVars.Count && !collector.varsOutsideCasts.ContainsKey(castVar)) + castVariables.Add(oldNode.BoundVars[i]); + } + return castVariables; + } + + public VariableCastCollector(TypeAxiomBuilderIntBoolU! axBuilder) { + this.AxBuilder = axBuilder; + } + + readonly List! varsInCasts = new List (); + readonly Dictionary! varsOutsideCasts = new Dictionary (); + + readonly TypeAxiomBuilderIntBoolU! AxBuilder; + + protected override bool StandardResult(VCExpr! node, bool arg) { + return true; // not used + } + + public override bool Visit(VCExprNAry! node, bool arg) { + if (node.Op is VCExprBoogieFunctionOp) { + Function! func = ((VCExprBoogieFunctionOp)node.Op).Func; + if ((AxBuilder.IsCast(func)) && node[0] is VCExprVar) { + VCExprVar castVar = (VCExprVar)node[0]; + if (!varsInCasts.Contains(castVar)) + varsInCasts.Add(castVar); + return true; + } + } else if (node.Op is VCExprNAryOp) { + VCExpressionGenerator.SingletonOp op = VCExpressionGenerator.SingletonOpDict[node.Op]; + switch(op) { + // the following operators cannot be used in triggers, so disregard any uses of variables as direct arguments + case VCExpressionGenerator.SingletonOp.NotOp: + case VCExpressionGenerator.SingletonOp.EqOp: + case VCExpressionGenerator.SingletonOp.NeqOp: + case VCExpressionGenerator.SingletonOp.AndOp: + case VCExpressionGenerator.SingletonOp.OrOp: + case VCExpressionGenerator.SingletonOp.ImpliesOp: + case VCExpressionGenerator.SingletonOp.LtOp: + case VCExpressionGenerator.SingletonOp.LeOp: + case VCExpressionGenerator.SingletonOp.GtOp: + case VCExpressionGenerator.SingletonOp.GeOp: + foreach (VCExpr n in node) { + if (!(n is VCExprVar)) { // don't recurse on VCExprVar argument + n.Accept(this, arg); + } + } + return true; + default: + break; + } + } + return base.Visit(node, arg); + } + + public override bool Visit(VCExprVar! node, bool arg) { + if (!varsOutsideCasts.ContainsKey(node)) + varsOutsideCasts.Add(node, null); + return true; + } + } + +} -- cgit v1.2.3