From 4e194b7c85dcaf2cbce7a42301727b7d11e9f7b8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 25 Apr 2024 17:21:39 +0200 Subject: [PATCH] Move classes into separate files --- Source/VCExpr/MutatingVCExprVisitor.cs | 340 +++ Source/VCExpr/OpTypeEraserPremisses.cs | 148 ++ Source/VCExpr/TypeErasure.cs | 2107 ----------------- Source/VCExpr/TypeErasure/HelperFuns.cs | 121 + .../TypeErasure/MapTypeAbstractionBuilder.cs | 273 +++ Source/VCExpr/TypeErasure/OpTypeEraser.cs | 409 ++++ Source/VCExpr/TypeErasure/TypeAxiomBuilder.cs | 437 ++++ Source/VCExpr/TypeErasure/TypeEraser.cs | 237 ++ .../VCExpr/TypeErasure/TypeEraserContracts.cs | 22 + .../VCExpr/TypeErasure/TypeEraserPremisses.cs | 335 +++ Source/VCExpr/TypeErasure/TypeErasure.cs | 433 ++++ .../{ => TypeErasure}/TypeErasureArguments.cs | 0 .../{ => TypeErasure}/TypeErasurePremisses.cs | 472 ---- Source/VCExpr/TypeErasure/VariableBindings.cs | 61 + .../TypeErasure/VariableCastCollector.cs | 159 ++ Source/VCExpr/VCExprASTVisitors.cs | 335 --- 16 files changed, 2975 insertions(+), 2914 deletions(-) create mode 100644 Source/VCExpr/MutatingVCExprVisitor.cs create mode 100644 Source/VCExpr/OpTypeEraserPremisses.cs delete mode 100644 Source/VCExpr/TypeErasure.cs create mode 100644 Source/VCExpr/TypeErasure/HelperFuns.cs create mode 100644 Source/VCExpr/TypeErasure/MapTypeAbstractionBuilder.cs create mode 100644 Source/VCExpr/TypeErasure/OpTypeEraser.cs create mode 100644 Source/VCExpr/TypeErasure/TypeAxiomBuilder.cs create mode 100644 Source/VCExpr/TypeErasure/TypeEraser.cs create mode 100644 Source/VCExpr/TypeErasure/TypeEraserContracts.cs create mode 100644 Source/VCExpr/TypeErasure/TypeEraserPremisses.cs create mode 100644 Source/VCExpr/TypeErasure/TypeErasure.cs rename Source/VCExpr/{ => TypeErasure}/TypeErasureArguments.cs (100%) rename Source/VCExpr/{ => TypeErasure}/TypeErasurePremisses.cs (71%) create mode 100644 Source/VCExpr/TypeErasure/VariableBindings.cs create mode 100644 Source/VCExpr/TypeErasure/VariableCastCollector.cs diff --git a/Source/VCExpr/MutatingVCExprVisitor.cs b/Source/VCExpr/MutatingVCExprVisitor.cs new file mode 100644 index 000000000..38ab0f7c9 --- /dev/null +++ b/Source/VCExpr/MutatingVCExprVisitor.cs @@ -0,0 +1,340 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie.VCExprAST; + +public abstract class MutatingVCExprVisitor + : IVCExprVisitor +{ + protected readonly VCExpressionGenerator /*!*/ + Gen; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Gen != null); + } + + public MutatingVCExprVisitor(VCExpressionGenerator gen) + { + Contract.Requires(gen != null); + this.Gen = gen; + } + + public VCExpr Mutate(VCExpr expr, Arg arg) + { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + return expr.Accept(this, arg); + } + + public List /*!*/ MutateSeq(IEnumerable /*!*/ exprs, Arg arg) + { + Contract.Requires(cce.NonNullElements(exprs)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List /*!*/ + res = new List(); + foreach (VCExpr /*!*/ expr in exprs) + { + Contract.Assert(expr != null); + res.Add(expr.Accept(this, arg)); + } + + return res; + } + + private List /*!*/ MutateList(List /*!*/ exprs, Arg arg) + { + Contract.Requires(cce.NonNullElements(exprs)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + bool changed = false; + List /*!*/ + res = new List(); + foreach (VCExpr /*!*/ expr in exprs) + { + Contract.Assert(expr != null); + VCExpr /*!*/ + newExpr = expr.Accept(this, arg); + if (!Object.ReferenceEquals(expr, newExpr)) + { + changed = true; + } + + res.Add(newExpr); + } + + if (!changed) + { + return exprs; + } + + return res; + } + + public virtual VCExpr Visit(VCExprLiteral node, Arg arg) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return node; + } + + //////////////////////////////////////////////////////////////////////////// + + // Special element used to mark the positions in the todo-stack where + // results have to be popped from the result-stack. + private static readonly VCExpr /*!*/ + CombineResultsMarker = new VCExprLiteral(Type.Bool); + + // The todo-stack contains records of the shape + // + // arg0 + // arg1 + // arg2 + // ... + // CombineResultsMarker + // f(arg0, arg1, arg2, ...) (the original expression) + + private readonly Stack /*!*/ + NAryExprTodoStack = new Stack(); + + private readonly Stack /*!*/ + NAryExprResultStack = new Stack(); + + [ContractInvariantMethod] + void ObjectInvarianta() + { + Contract.Invariant(cce.NonNullElements(NAryExprResultStack)); + Contract.Invariant(cce.NonNullElements(NAryExprTodoStack)); + } + + + private void PushTodo(VCExprNAry exprTodo) + { + Contract.Requires(exprTodo != null); + NAryExprTodoStack.Push(exprTodo); + NAryExprTodoStack.Push(CombineResultsMarker); + for (int i = exprTodo.Arity - 1; i >= 0; --i) + { + NAryExprTodoStack.Push(exprTodo[i]); + } + } + + public virtual bool AvoidVisit(VCExprNAry node, Arg arg) + { + return true; + } + + public virtual VCExpr Visit(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + int initialStackSize = NAryExprTodoStack.Count; + int initialResultStackSize = NAryExprResultStack.Count; + + PushTodo(node); + + while (NAryExprTodoStack.Count > initialStackSize) + { + VCExpr /*!*/ + subExpr = NAryExprTodoStack.Pop(); + Contract.Assert(subExpr != null); + + if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) + { + // assemble a result + VCExprNAry /*!*/ + originalExpr = (VCExprNAry) NAryExprTodoStack.Pop(); + Contract.Assert(originalExpr != null); + VCExprOp /*!*/ + op = originalExpr.Op; + bool changed = false; + List /*!*/ + newSubExprs = new List(); + + for (int i = op.Arity - 1; i >= 0; --i) + { + VCExpr /*!*/ + nextSubExpr = NAryExprResultStack.Pop(); + Contract.Assert(nextSubExpr != null); + if (!Object.ReferenceEquals(nextSubExpr, originalExpr[i])) + { + changed = true; + } + + newSubExprs.Insert(0, nextSubExpr); + } + + NAryExprResultStack.Push(UpdateModifiedNode(originalExpr, newSubExprs, changed, arg)); + // + } + else + { + // + VCExprNAry narySubExpr = subExpr as VCExprNAry; + if (narySubExpr != null && this.AvoidVisit(narySubExpr, arg) && + // as in VCExprNAryUniformOpEnumerator, all expressions with + // type parameters are allowed to be inspected more closely + narySubExpr.TypeParamArity == 0) + { + PushTodo(narySubExpr); + } + else + { + NAryExprResultStack.Push(subExpr.Accept(this, arg)); + } + + // + } + } + + Contract.Assert(NAryExprTodoStack.Count == initialStackSize && + NAryExprResultStack.Count == initialResultStackSize + 1); + return NAryExprResultStack.Pop(); + } + + protected virtual VCExpr /*!*/ UpdateModifiedNode(VCExprNAry /*!*/ originalNode, + List /*!*/ newSubExprs, // has any of the subexpressions changed? + bool changed, + Arg arg) + { + Contract.Requires(cce.NonNullElements(newSubExprs)); + Contract.Ensures(Contract.Result() != null); + + if (changed) + { + return Gen.Function(originalNode.Op, + newSubExprs, originalNode.TypeArguments); + } + else + { + return originalNode; + } + } + + //////////////////////////////////////////////////////////////////////////// + + public virtual VCExpr Visit(VCExprVar node, Arg arg) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return node; + } + + protected List /*!*/ MutateTriggers(List /*!*/ triggers, Arg arg) + { + Contract.Requires(cce.NonNullElements(triggers)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List /*!*/ + newTriggers = new List(); + bool changed = false; + foreach (VCTrigger /*!*/ trigger in triggers) + { + Contract.Assert(trigger != null); + List /*!*/ + exprs = trigger.Exprs; + List /*!*/ + newExprs = MutateList(exprs, arg); + + if (Object.ReferenceEquals(exprs, newExprs)) + { + newTriggers.Add(trigger); + } + else + { + newTriggers.Add(Gen.Trigger(trigger.Pos, newExprs)); + changed = true; + } + } + + if (!changed) + { + return triggers; + } + + return newTriggers; + } + + public virtual VCExpr Visit(VCExprQuantifier node, Arg arg) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + bool changed = false; + + VCExpr /*!*/ + body = node.Body; + Contract.Assert(body != null); + VCExpr /*!*/ + newbody = body.Accept(this, arg); + Contract.Assert(newbody != null); + if (!Object.ReferenceEquals(body, newbody)) + { + changed = true; + } + + // visit the trigger expressions as well + List /*!*/ + triggers = node.Triggers; + Contract.Assert(cce.NonNullElements(triggers)); + List /*!*/ + newTriggers = MutateTriggers(triggers, arg); + Contract.Assert(cce.NonNullElements(newTriggers)); + if (!Object.ReferenceEquals(triggers, newTriggers)) + { + changed = true; + } + + if (!changed) + { + return node; + } + + return Gen.Quantify(node.Quan, node.TypeParameters, node.BoundVars, + newTriggers, node.Info, newbody); + } + + public virtual VCExpr Visit(VCExprLet node, Arg arg) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + bool changed = false; + + VCExpr /*!*/ + body = node.Body; + VCExpr /*!*/ + newbody = body.Accept(this, arg); + if (!Object.ReferenceEquals(body, newbody)) + { + changed = true; + } + + List /*!*/ + newbindings = new List(); + for (int i = 0; i < node.Length; ++i) + { + VCExprLetBinding /*!*/ + binding = node[i]; + Contract.Assert(binding != null); + VCExpr /*!*/ + e = binding.E; + VCExpr /*!*/ + newE = e.Accept(this, arg); + if (Object.ReferenceEquals(e, newE)) + { + newbindings.Add(binding); + } + else + { + changed = true; + newbindings.Add(Gen.LetBinding(binding.V, newE)); + } + } + + if (!changed) + { + return node; + } + + return Gen.Let(newbindings, newbody); + } +} \ No newline at end of file diff --git a/Source/VCExpr/OpTypeEraserPremisses.cs b/Source/VCExpr/OpTypeEraserPremisses.cs new file mode 100644 index 000000000..4fcd187af --- /dev/null +++ b/Source/VCExpr/OpTypeEraserPremisses.cs @@ -0,0 +1,148 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +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); + Function /*!*/ + select = + AxBuilder.MapTypeAbstracter.Select(mapType, out var 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.Arguments, bindings); + } + + public override VCExpr VisitStoreOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + Function /*!*/ + store = + AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out var instantiations); + Contract.Assert(store != null); + return HandleFunctionOp(store, + // the store function never has explicit + // type parameters + new List(), + node.Arguments, 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.Arguments, 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; + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs deleted file mode 100644 index f55ec764f..000000000 --- a/Source/VCExpr/TypeErasure.cs +++ /dev/null @@ -1,2107 +0,0 @@ -using System; -using System.Linq; -using System.Collections.Generic; -using System.Diagnostics.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 -{ - // 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) - { - Contract.Requires(types != null); - Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeParams)); - Contract.Requires(types.Length > 0); - Contract.Requires(Contract.ForAll(0, types.Length, i => types[i] != null)); - Contract.Ensures(Contract.Result() != null); - - List args = new List(); - for (int i = 0; i < types.Length - 1; ++i) - { - args.Add(new Formal(Token.NoToken, - new TypedIdent(Token.NoToken, "arg" + i, cce.NonNull(types[i])), - true)); - } - - Formal result = new Formal(Token.NoToken, - new TypedIdent(Token.NoToken, "res", - cce.NonNull(types)[types.Length - 1]), - false); - return new Function(Token.NoToken, name, new List(typeParams), args, result); - } - - public static Function BoogieFunction(string name, params Type[] types) - { - Contract.Requires(types != null); - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); - 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) - { - Contract.Requires(U != null); - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); - 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) - { - Contract.Requires(gen != null); - Contract.Requires(fun != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List /*!*/ - arguments = new List(fun.InParams.Count); - foreach (Formal /*!*/ f in fun.InParams) - { - Contract.Assert(f != null); - VCExprVar /*!*/ - var = gen.Variable(f.Name, f.TypedIdent.Type); - arguments.Add(var); - } - - return arguments; - } - - public static List /*!*/ ToList(params T[] args) where T : class - { - Contract.Requires(cce.NonNullElements(args)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(args); - } - - public static List /*!*/ ToVCExprList(List /*!*/ list) - { - Contract.Requires(cce.NonNullElements(list)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(list); - } - - public static List /*!*/ VarVector(string baseName, int num, Type type, VCExpressionGenerator gen) - { - Contract.Requires(gen != null); - Contract.Requires(type != null); - Contract.Requires(baseName != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - 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) - { - Contract.Requires(gen != null); - Contract.Requires(baseName != null); - Contract.Requires(cce.NonNullElements(types)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - 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; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Ctor != null); - Contract.Invariant(cce.NonNullElements(Dtors)); - } - - - public TypeCtorRepr(Function ctor, List /*!*/ dtors) - { - Contract.Requires(ctor != null); - Contract.Requires(cce.NonNullElements(dtors)); - Contract.Requires(ctor.InParams.Count == 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 syntactic approach). - [ContractClass(typeof(TypeAxiomBuilderContracts))] - public abstract class TypeAxiomBuilder : ICloneable - { - protected readonly VCExpressionGenerator /*!*/ - Gen; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Gen != null); - Contract.Invariant(Ctor != null); - } - - - internal abstract MapTypeAbstractionBuilder /*!*/ MapTypeAbstracter { get; } - - /////////////////////////////////////////////////////////////////////////// - // Type Axioms - - // list in which all typed axioms are collected - private readonly List /*!*/ - AllTypeAxioms; - - [ContractInvariantMethod] - void AllTypeAxiomsInvariantMethod() - { - Contract.Invariant(cce.NonNullElements(AllTypeAxioms)); - } - - // list in which type axioms are incrementally collected - private readonly List /*!*/ - IncTypeAxioms; - - [ContractInvariantMethod] - void IncTypeAxiomsInvariantMethod() - { - Contract.Invariant(cce.NonNullElements(IncTypeAxioms)); - } - - internal void AddTypeAxiom(VCExpr axiom) - { - Contract.Requires(axiom != null); - AllTypeAxioms.Add(axiom); - IncTypeAxioms.Add(axiom); - } - - // Return all axioms that were added since the last time NewAxioms - // was called - public VCExpr GetNewAxioms() - { - Contract.Ensures(Contract.Result() != null); - 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) - { - Contract.Requires(typeRepr != null); - Contract.Ensures(Contract.Result() != null); - - VCExpr res = Gen.Eq(Gen.Function(Ctor, typeRepr), - Gen.Integer(CurrentCtorNum)); - CurrentCtorNum = CurrentCtorNum + BigNum.ONE; - return res; - } - - private VCExpr GenCtorAssignment(Function typeRepr) - { - Contract.Requires(typeRepr != null); - Contract.Ensures(Contract.Result() != null); - - List /*!*/ - quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen); - VCExpr /*!*/ - eq = - GenCtorAssignment(Gen.Function(typeRepr, - HelperFuns.ToVCExprList(quantifiedVars))); - - if (typeRepr.InParams.Count == 0) - { - return eq; - } - - return Gen.Forall(quantifiedVars, new List(), - "ctor:" + typeRepr.Name, 1, eq); - } - - // generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi) - protected VCExpr GenLeftInverseAxiom(Function fun, Function invFun, int dtorNum) - { - Contract.Requires(invFun != null); - Contract.Requires(fun != null); - Contract.Ensures(Contract.Result() != null); - List /*!*/ - quantifiedVars = HelperFuns.GenVarsForInParams(fun, Gen); - Contract.Assert(cce.NonNullElements(quantifiedVars)); - - 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))); - Contract.Assert(cce.NonNullElements(triggers)); - return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, 1, eq); - } - - /////////////////////////////////////////////////////////////////////////// - - // the type of everything that is not int, bool, or a type - [ContractInvariantMethod] - void ObjectInvariant2() - { - Contract.Invariant(UDecl != null); - Contract.Invariant(TDecl != null); - Contract.Invariant(U != null); - Contract.Invariant(T != null); - } - - 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); - - [Pure] - public abstract bool UnchangedType(Type /*!*/ type); - - /////////////////////////////////////////////////////////////////////////// - // Symbols for representing types - - private readonly IDictionary /*!*/ - BasicTypeReprs; - - [ContractInvariantMethod] - void BasicTypeReprsInvariantMethod() - { - Contract.Invariant(cce.NonNullDictionaryAndValues(BasicTypeReprs)); - } - - private VCExpr GetBasicTypeRepr(Type type) - { - Contract.Requires(type != null); - Contract.Requires(type.IsBasic || type.IsBv || type.IsFloat); - Contract.Ensures(Contract.Result() != null); - if (!BasicTypeReprs.TryGetValue(type, out var res)) - { - res = Gen.Function(HelperFuns.BoogieFunction(type.ToString() + "Type", T)); - AddTypeAxiom(GenCtorAssignment(res)); - BasicTypeReprs.Add(type, res); - } - - return cce.NonNull(res); - } - - private readonly IDictionary /*!*/ - TypeCtorReprs; - - [ContractInvariantMethod] - void TypeCtorReprsInvariantMethod() - { - Contract.Invariant(TypeCtorReprs != null); - } - - internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl decl) - { - Contract.Requires(decl != null); - if (!TypeCtorReprs.TryGetValue(decl, out var reprSet)) - { - Function /*!*/ - ctor = HelperFuns.UniformBoogieFunction(decl.Name + "Type", decl.Arity, T); - Contract.Assert(ctor != null); - 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) - { - Contract.Requires(decl != null); - Contract.Ensures(Contract.Result() != null); - return GetTypeCtorReprStruct(decl).Ctor; - } - - public Function GetTypeDtor(TypeCtorDecl decl, int num) - { - Contract.Requires(decl != null); - Contract.Ensures(Contract.Result() != null); - return GetTypeCtorReprStruct(decl).Dtors[num]; - } - - // mapping from free type variables to VCExpr variables - private readonly IDictionary /*!*/ - TypeVariableMapping; - - [ContractInvariantMethod] - void TypeVariableMappingInvariantMethod() - { - Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableMapping)); - } - - public VCExprVar Typed2Untyped(TypeVariable var) - { - Contract.Requires(var != null); - Contract.Ensures(Contract.Result() != null); - if (!TypeVariableMapping.TryGetValue(var, out var res)) - { - res = new VCExprVar(var.Name, T); - TypeVariableMapping.Add(var, res); - } - - return cce.NonNull(res); - } - - - //////////////////////////////////////////////////////////////////////////// - // Symbols for representing variables and constants - - // Globally defined variables - private readonly IDictionary /*!*/ - Typed2UntypedVariables; - - [ContractInvariantMethod] - void Typed2UntypedVariablesInvariantMethod() - { - Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedVariables)); - } - - // This method must only be used for free (unbound) variables - public VCExprVar Typed2Untyped(VCExprVar var) - { - Contract.Requires(var != null); - Contract.Ensures(Contract.Result() != null); - VCExprVar res = TryTyped2Untyped(var); - if (res == null) - { - res = Gen.Variable(var.Name, TypeAfterErasure(var.Type)); - Typed2UntypedVariables.Add(var, res); - AddVarTypeAxiom(res, var.Type); - } - - return cce.NonNull(res); - } - - /// - /// This method is like Typed2Untyped, except in the case where the given variables - /// doesn't exist in the mapping. For that case, this method returns null whereas - /// Typed2Untyped creates a new variable that it adds to the mapping. - /// - /// - /// - public VCExprVar TryTyped2Untyped(VCExprVar var) - { - Contract.Requires(var != null); - if (Typed2UntypedVariables.TryGetValue(var, out var res)) - { - return res; - } - else - { - return null; - } - } - - protected abstract void AddVarTypeAxiom(VCExprVar /*!*/ var, Type /*!*/ originalType); - - /////////////////////////////////////////////////////////////////////////// - // Translation function from types to their term representation - - public VCExpr Type2Term(Type type, IDictionary /*!*/ varMapping) - { - Contract.Requires(type != null); - Contract.Requires(cce.NonNullDictionaryAndValues(varMapping)); - Contract.Ensures(Contract.Result() != null); - // - if (type.IsBasic || type.IsBv || type.IsFloat) - { - // - return GetBasicTypeRepr(type); - // - } - else if (type.IsCtor) - { - // - CtorType ctype = type.AsCtor; - Function /*!*/ - repr = GetTypeCtorRepr(ctype.Decl); - List /*!*/ - args = new List(ctype.Arguments.Count); - foreach (Type /*!*/ t in ctype.Arguments.ToArray()) - { - Contract.Assert(t != null); - args.Add(Type2Term(t, varMapping)); - } - - return Gen.Function(repr, args); - // - } - else if (type.IsVariable) - { - // - if (!varMapping.TryGetValue(type.AsVariable, out var res)) - { - // then the variable is free and we bind it at this point to a term - // variable - res = Typed2Untyped(type.AsVariable); - } - - return cce.NonNull(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); - Contract.Assert(false); - throw new cce.UnreachableException(); // please the compiler - } - } - - //////////////////////////////////////////////////////////////////////////// - - public TypeAxiomBuilder(VCExpressionGenerator gen) - { - Contract.Requires(gen != null); - 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 List()); - U = u; - - TypeCtorDecl /*!*/ - tDecl = new TypeCtorDecl(Token.NoToken, "T", 0); - TDecl = tDecl; - Type /*!*/ - t = new CtorType(Token.NoToken, tDecl, new List()); - T = t; - - Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int); - } - - public virtual void Setup(List usedTypes) - { - foreach (var ty in usedTypes) { - GetBasicTypeRepr(ty); - } - } - - // constructor to allow cloning - internal TypeAxiomBuilder(TypeAxiomBuilder builder) - { - Contract.Requires(builder != null); - 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(); - - public abstract VCExpr Cast(VCExpr expr, Type toType); - } - - [ContractClassFor(typeof(TypeAxiomBuilder))] - public abstract class TypeAxiomBuilderContracts : TypeAxiomBuilder - { - public TypeAxiomBuilderContracts() - : base((VCExpressionGenerator) null) - { - } - - internal override MapTypeAbstractionBuilder MapTypeAbstracter - { - get - { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - public override Type TypeAfterErasure(Type type) - { - Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - - public override bool UnchangedType(Type type) - { - Contract.Requires(type != null); - throw new NotImplementedException(); - } - - protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) - { - Contract.Requires(var != null); - Contract.Requires(originalType != null); - throw new NotImplementedException(); - } - - public override object Clone() - { - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - } - - ////////////////////////////////////////////////////////////////////////////// - - // 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 - - [ContractClass(typeof(TypeAxiomBuilderIntBoolUContracts))] - public abstract class TypeAxiomBuilderIntBoolU : TypeAxiomBuilder - { - public TypeAxiomBuilderIntBoolU(VCExpressionGenerator gen) - : base(gen) - { - Contract.Requires(gen != null); - - TypeCasts = new Dictionary(); - } - - // constructor to allow cloning - internal TypeAxiomBuilderIntBoolU(TypeAxiomBuilderIntBoolU builder) - : base(builder) - { - Contract.Requires(builder != null); - - TypeCasts = new Dictionary(builder.TypeCasts); - } - - public override void Setup(List usedTypes) - { - base.Setup(usedTypes); - - foreach (var ty in usedTypes) { - GetTypeCasts(ty); - } - } - - // 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) - { - Contract.Requires((castFromU != null)); - Contract.Requires((castToU != null)); - Contract.Ensures((cce.NonNullElements(Contract.ValueAtReturn(out triggers)))); - Contract.Ensures(Contract.ValueAtReturn(out var) != null); - Contract.Ensures(Contract.Result() != null); - 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; - - [ContractInvariantMethod] - void TypeCastsInvariantMethod() - { - Contract.Invariant(TypeCasts != null); - } - - private TypeCastSet GetTypeCasts(Type type) - { - Contract.Requires(type != null); - if (!TypeCasts.TryGetValue(type, out var 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; - } - - [Pure] - public Function CastTo(Type type) - { - Contract.Requires(type != null); - Contract.Requires(UnchangedType(type)); - Contract.Ensures(Contract.Result() != null); - return GetTypeCasts(type).CastFromU; - } - - public Function CastFrom(Type type) - { - Contract.Requires(type != null); - Contract.Requires((UnchangedType(type))); - Contract.Ensures(Contract.Result() != null); - return GetTypeCasts(type).CastToU; - } - - private struct TypeCastSet - { - public readonly Function /*!*/ - CastToU; - - public readonly Function /*!*/ - CastFromU; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(CastToU != null); - Contract.Invariant(CastFromU != null); - } - - - public TypeCastSet(Function castToU, Function castFromU) - { - Contract.Requires(castFromU != null); - Contract.Requires(castToU != null); - CastToU = castToU; - CastFromU = castFromU; - } - } - - public bool IsCast(Function fun) - { - Contract.Requires(fun != null); - if (fun.InParams.Count != 1) - { - return false; - } - - Type /*!*/ - inType = cce.NonNull(fun.InParams[0]).TypedIdent.Type; - if (inType.Equals(U)) - { - Type /*!*/ - outType = cce.NonNull(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 = cce.NonNull(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, Type.Real, Type.Bool, and Type.RMode - - public override Type TypeAfterErasure(Type type) - { - //Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); - 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) - { - //Contract.Requires(type != null); - return type.IsInt || type.IsReal || type.IsBool || type.IsBv || type.IsFloat || type.IsRMode || type.IsString || - type.IsRegEx; - } - - public override VCExpr Cast(VCExpr expr, Type toType) - { - Contract.Requires(toType != null); - Contract.Requires(expr != null); - Contract.Requires((expr.Type.Equals(U) || UnchangedType(expr.Type))); - Contract.Requires((toType.Equals(U) || UnchangedType(toType))); - Contract.Ensures(Contract.Result() != null); - if (expr.Type.Equals(toType)) - { - return expr; - } - - if (toType.Equals(U)) - { - return Gen.Function(CastFrom(expr.Type), expr); - } - else - { - Contract.Assert(expr.Type.Equals(U)); - return Gen.Function(CastTo(toType), expr); - } - } - - public List /*!*/ CastSeq(List /*!*/ exprs, Type toType) - { - Contract.Requires(toType != null); - Contract.Requires(cce.NonNullElements(exprs)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List /*!*/ - res = new List(exprs.Count); - foreach (VCExpr /*!*/ expr in exprs) - { - Contract.Assert(expr != null); - res.Add(Cast(expr, toType)); - } - - return res; - } - } - - [ContractClassFor(typeof(TypeAxiomBuilderIntBoolU))] - public abstract class TypeAxiomBuilderIntBoolUContracts : TypeAxiomBuilderIntBoolU - { - public TypeAxiomBuilderIntBoolUContracts() - : base((TypeAxiomBuilderIntBoolU) null) - { - } - - protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) - { - Contract.Requires(castToU != null); - Contract.Requires(castFromU != null); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - - protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) - { - Contract.Requires(castFromU != null); - Contract.Requires(castToU != null); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - - internal override MapTypeAbstractionBuilder MapTypeAbstracter - { - get { throw new NotImplementedException(); } - } - - protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) - { - throw new NotImplementedException(); - } - - public override object Clone() - { - throw new NotImplementedException(); - } - } - - ////////////////////////////////////////////////////////////////////////////// - // 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) - [ContractClass(typeof(MapTypeAbstractionBuilderContracts))] - internal abstract class MapTypeAbstractionBuilder - { - protected readonly TypeAxiomBuilder /*!*/ - AxBuilder; - - protected readonly VCExpressionGenerator /*!*/ - Gen; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(AxBuilder != null); - Contract.Invariant(Gen != null); - } - - - internal MapTypeAbstractionBuilder(TypeAxiomBuilder axBuilder, VCExpressionGenerator gen) - { - Contract.Requires(gen != null); - Contract.Requires(axBuilder != null); - this.AxBuilder = axBuilder; - this.Gen = gen; - AbstractionVariables = new List(); - ClassRepresentations = new Dictionary(); - } - - // constructor for cloning - internal MapTypeAbstractionBuilder(TypeAxiomBuilder axBuilder, VCExpressionGenerator gen, - MapTypeAbstractionBuilder builder) - { - Contract.Requires(builder != null); - Contract.Requires(gen != null); - Contract.Requires(axBuilder != null); - 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; - - [ContractInvariantMethod] - void AbstractionVariablesInvariantMethod() - { - Contract.Invariant(cce.NonNullElements(AbstractionVariables)); - } - - private TypeVariable AbstractionVariable(int num) - { - Contract.Requires((num >= 0)); - Contract.Ensures(Contract.Result() != null); - 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; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(RepresentingType != null); - Contract.Invariant(Select != null); - Contract.Invariant(Store != null); - } - - - public MapTypeClassRepresentation(TypeCtorDecl representingType, Function select, Function store) - { - Contract.Requires(store != null); - Contract.Requires(select != null); - Contract.Requires(representingType != null); - this.RepresentingType = representingType; - this.Select = select; - this.Store = store; - } - } - - private readonly IDictionary /*!*/ - ClassRepresentations; - - [ContractInvariantMethod] - void ClassRepresentationsInvariantMethod() - { - Contract.Invariant(ClassRepresentations != null); - } - - protected MapTypeClassRepresentation GetClassRepresentation(MapType abstractedType) - { - Contract.Requires(abstractedType != null); - if (!ClassRepresentations.TryGetValue(abstractedType, out var res)) - { - int num = ClassRepresentations.Count; - TypeCtorDecl /*!*/ - synonym = - new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Count); - - GenSelectStoreFunctions(abstractedType, synonym, out var @select, out var 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 List instantiations) - { - Contract.Requires((rawType != null)); - Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); - Contract.Ensures(Contract.Result() != null); - return AbstractAndGetRepresentation(rawType, out instantiations).Select; - } - - public Function Store(MapType rawType, out List instantiations) - { - Contract.Requires((rawType != null)); - Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); - Contract.Ensures(Contract.Result() != null); - return AbstractAndGetRepresentation(rawType, out instantiations).Store; - } - - private MapTypeClassRepresentation - AbstractAndGetRepresentation(MapType rawType, out List instantiations) - { - Contract.Requires((rawType != null)); - Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); - instantiations = new List(); - MapType /*!*/ - abstraction = ThinOutMapType(rawType, instantiations); - return GetClassRepresentation(abstraction); - } - - public CtorType AbstractMapType(MapType rawType) - { - Contract.Requires(rawType != null); - Contract.Ensures(Contract.Result() != null); - List /*!*/ - instantiations = new List(); - MapType /*!*/ - abstraction = ThinOutMapType(rawType, instantiations); - - MapTypeClassRepresentation repr = GetClassRepresentation(abstraction); - Contract.Assume(repr.RepresentingType.Arity == instantiations.Count); - return new CtorType(Token.NoToken, repr.RepresentingType, instantiations); - } - - // TODO: cache the result of this operation - protected MapType ThinOutMapType(MapType rawType, List instantiations) - { - Contract.Requires(instantiations != null); - Contract.Requires(rawType != null); - Contract.Ensures(Contract.Result() != null); - List /*!*/ - newArguments = new List(); - foreach (Type /*!*/ subtype in rawType.Arguments.ToList()) - { - Contract.Assert(subtype != null); - newArguments.Add(ThinOutType(subtype, rawType.TypeParameters, - instantiations)); - } - - Type /*!*/ - newResult = ThinOutType(rawType.Result, rawType.TypeParameters, - instantiations); - return new MapType(Token.NoToken, rawType.TypeParameters, newArguments, newResult); - } - - // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables - private Type /*!*/ ThinOutType(Type rawType, List boundTypeParams, List instantiations) - { - Contract.Requires(instantiations != null); - Contract.Requires(boundTypeParams != null); - Contract.Requires(rawType != null); - Contract.Ensures(Contract.Result() != null); - - if (rawType.FreeVariables.All(var => !boundTypeParams.Contains(var))) - { - // Bingo! - // if the type does not contain any bound variables, we can simply - // replace it with a type variable - TypeVariable /*!*/ - abstractionVar = AbstractionVariable(instantiations.Count); - Contract.Assume(!boundTypeParams.Contains(abstractionVar)); - instantiations.Add(rawType); - return abstractionVar; - } - - if (rawType.IsVariable) - { - // - // then the variable has to be bound, we cannot do anything - TypeVariable /*!*/ - rawVar = rawType.AsVariable; - Contract.Assume(boundTypeParams.Contains(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; - List /*!*/ - newArguments = new List(); - foreach (Type /*!*/ subtype in rawCtorType.Arguments.ToList()) - { - Contract.Assert(subtype != null); - 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 - } - } - } - - [ContractClassFor(typeof(MapTypeAbstractionBuilder))] - internal abstract class MapTypeAbstractionBuilderContracts : MapTypeAbstractionBuilder - { - public MapTypeAbstractionBuilderContracts() - : base(null, null) - { - } - - protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonymDecl, - out Function select, out Function store) - { - Contract.Requires(abstractedType != null); - Contract.Requires(synonymDecl != null); - Contract.Ensures(Contract.ValueAtReturn(out select) != null); - Contract.Ensures(Contract.ValueAtReturn(out store) != null); - - throw new NotImplementedException(); - } - } - - - ////////////////////////////////////////////////////////////////////////////// - - public class VariableBindings - { - public readonly IDictionary /*!*/ - VCExprVarBindings; - - public readonly IDictionary /*!*/ - TypeVariableBindings; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullDictionaryAndValues(VCExprVarBindings)); - Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableBindings)); - } - - - public VariableBindings(IDictionary /*!*/ vcExprVarBindings, - IDictionary /*!*/ typeVariableBindings) - { - Contract.Requires(cce.NonNullDictionaryAndValues(vcExprVarBindings)); - Contract.Requires(cce.NonNullDictionaryAndValues(typeVariableBindings)); - this.VCExprVarBindings = vcExprVarBindings; - this.TypeVariableBindings = typeVariableBindings; - } - - public VariableBindings() : - this(new Dictionary(), - new Dictionary()) - { - } - - public VariableBindings Clone() - { - Contract.Ensures(Contract.Result() != null); - IDictionary /*!*/ - newVCExprVarBindings = - new Dictionary(); - foreach (KeyValuePair pair in VCExprVarBindings) - { - Contract.Assert(cce.NonNullElements(pair)); - newVCExprVarBindings.Add(pair); - } - - IDictionary /*!*/ - newTypeVariableBindings = - new Dictionary(); - foreach (KeyValuePair pair in TypeVariableBindings) - { - Contract.Assert(cce.NonNullElements(pair)); - 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. - [ContractClass(typeof(TypeEraserContracts))] - public abstract class TypeEraser : MutatingVCExprVisitor - { - protected readonly TypeAxiomBuilderIntBoolU /*!*/ - AxBuilder; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(AxBuilder != null); - } - - - protected abstract OpTypeEraser /*!*/ OpEraser { get; } - - //////////////////////////////////////////////////////////////////////////// - - public TypeEraser(TypeAxiomBuilderIntBoolU axBuilder, VCExpressionGenerator gen) - : base(gen) - { - Contract.Requires(gen != null); - Contract.Requires(axBuilder != null); - AxBuilder = axBuilder; - } - - public VCExpr Erase(VCExpr expr, int polarity) - { - Contract.Requires(expr != null); - Contract.Requires((polarity >= -1 && polarity <= 1)); - Contract.Ensures(Contract.Result() != null); - 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) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real || - node.Type == Type.RMode || node.Type == Type.String || node.Type == Type.RegEx); - return node; - } - - //////////////////////////////////////////////////////////////////////////// - - public override bool AvoidVisit(VCExprNAry node, VariableBindings arg) - { - return node.Op.Equals(VCExpressionGenerator.AndOp) || - node.Op.Equals(VCExpressionGenerator.OrOp); - } - - public override VCExpr Visit(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - 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) - { - //Contract.Requires(originalNode != null); - //Contract.Requires(cce.NonNullElements(newSubExprs)); - //Contract.Requires(bindings != null); - Contract.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) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - if (!bindings.VCExprVarBindings.TryGetValue(node, out var res)) - { - return AxBuilder.Typed2Untyped(node); - } - - return cce.NonNull(res); - } - - //////////////////////////////////////////////////////////////////////////// - - protected bool IsUniversalQuantifier(VCExprQuantifier node) - { - Contract.Requires(node != null); - 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) - { - Contract.Requires(bindings != null); - Contract.Requires(cce.NonNullElements(oldBoundVars)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - 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) - { - Contract.Requires(node != null); - Contract.Requires(newNode != null); - Contract.Requires(cce.NonNullElements(occurringVars)); - Contract.Requires(oldBindings != null); - Contract.Ensures(Contract.ValueAtReturn(out newBindings) != null); - Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out 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) - { - Contract.Assert(var != null); - Type /*!*/ - newType = - castVariables.Contains(var) - ? AxBuilder.U - : AxBuilder.TypeAfterErasure(var.Type); - Contract.Assert(newType != null); - VCExprVar /*!*/ - newVar = Gen.Variable(var.Name, newType); - Contract.Assert(newVar != null); - newBoundVars.Add(newVar); - newBindings.VCExprVarBindings.Add(var, newVar); - } - - return true; - } - - //////////////////////////////////////////////////////////////////////////// - - public override VCExpr Visit(VCExprLet node, VariableBindings bindings) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - 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]; - Contract.Assert(binding != null); - 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); - } - } - - [ContractClassFor(typeof(TypeEraser))] - public abstract class TypeEraserContracts : TypeEraser - { - public TypeEraserContracts() - : base(null, null) - { - } - - protected override OpTypeEraser OpEraser - { - get - { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - } - - - ////////////////////////////////////////////////////////////////////////////// - - public abstract class OpTypeEraser : StandardVCExprOpVisitor - { - protected readonly TypeAxiomBuilderIntBoolU /*!*/ - AxBuilder; - - protected readonly TypeEraser /*!*/ - Eraser; - - protected readonly VCExpressionGenerator /*!*/ - Gen; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(AxBuilder != null); - Contract.Invariant(Eraser != null); - Contract.Invariant(Gen != null); - } - - - public OpTypeEraser(TypeEraser /*!*/ eraser, TypeAxiomBuilderIntBoolU /*!*/ axBuilder, - VCExpressionGenerator /*!*/ gen) - { - Contract.Requires(eraser != null); - Contract.Requires(axBuilder != null); - Contract.Requires(gen != null); - this.AxBuilder = axBuilder; - this.Eraser = eraser; - this.Gen = gen; - } - - protected override VCExpr StandardResult(VCExprNAry node, VariableBindings bindings) - { - //Contract.Requires(bindings != null); - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node); - Contract.Assert(false); - throw new cce.UnreachableException(); // to please the compiler - } - - private List /*!*/ MutateSeq(VCExprNAry node, VariableBindings bindings, int newPolarity) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - int oldPolarity = Eraser.Polarity; - Eraser.Polarity = newPolarity; - List /*!*/ - newArgs = Eraser.MutateSeq(node.Arguments, bindings); - Eraser.Polarity = oldPolarity; - return newArgs; - } - - private VCExpr CastArguments(VCExprNAry node, Type argType, VariableBindings bindings, int newPolarity) - { - Contract.Requires(bindings != null); - Contract.Requires(argType != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - 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, real, bool, or U) - private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Requires((node.Arity > 0)); - Contract.Ensures(Contract.Result() != null); - - List /*!*/ - newArgs = MutateSeq(node, bindings, newPolarity); - Type /*!*/ - oldType = node[0].Type; - if (AxBuilder.UnchangedType(oldType) && - node.Arguments.Skip(1).All(e => e.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) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Bool, bindings, -Eraser.Polarity); - } - - public override VCExpr VisitEqOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitNeqOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitImpliesOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - // 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) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitIfThenElseOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - 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) - { - Contract.Requires(node != null); - Contract.Requires(bindings != null); - Contract.Ensures(Contract.Result() != null); - - List /*!*/ - newArgs = MutateSeq(node, bindings, 0); - return Gen.Function(node.Op, newArgs); - } - - public override VCExpr VisitAddOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, node.Type, bindings, 0); - } - - public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, node.Type, bindings, 0); - } - - public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, node.Type, bindings, 0); - } - - public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); - } - - public override VCExpr VisitModOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); - } - - public override VCExpr VisitRealDivOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Real, bindings, 0); - } - - /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Float, bindings, 0); - }*/ - public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Real, bindings, 0); - } - - public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArguments(node, AxBuilder.U, bindings, 0); - } - - public override VCExpr VisitToIntOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitToRealOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitFloatNeqOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitBvExtractOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - return CastArgumentsToOldType(node, bindings, 0); - } - - public override VCExpr VisitBvConcatOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires((bindings != null)); - Contract.Requires((node != null)); - Contract.Ensures(Contract.Result() != null); - List /*!*/ - newArgs = MutateSeq(node, bindings, 0); - - // each argument is cast to its old type - Contract.Assert(newArgs.Count == node.Arity && newArgs.Count == 2); - VCExpr /*!*/ - arg0 = AxBuilder.Cast(newArgs[0], node[0].Type); - Contract.Assert(arg0 != null); - VCExpr /*!*/ - arg1 = AxBuilder.Cast(newArgs[1], node[1].Type); - Contract.Assert(arg1 != null); - 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) - { - Contract.Requires((axBuilder != null)); - Contract.Requires((newNode != null)); - Contract.Requires((oldNode != null)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - VariableCastCollector /*!*/ - collector = new VariableCastCollector(axBuilder); - Contract.Assert(collector != null); - if (newNode.Triggers.Any(trigger => trigger.Pos)) - { - // look in the given triggers - foreach (VCTrigger /*!*/ trigger in newNode.Triggers) - { - Contract.Assert(trigger != null); - if (trigger.Pos) - { - foreach (VCExpr /*!*/ expr in trigger.Exprs) - { - Contract.Assert(expr != null); - 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) - { - Contract.Assert(castVar != null); - 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) - { - Contract.Requires(axBuilder != null); - this.AxBuilder = axBuilder; - } - - readonly List /*!*/ - varsInCasts = new List(); - - readonly Dictionary /*!*/ - varsOutsideCasts = new Dictionary(); - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(varsInCasts)); - Contract.Invariant(varsOutsideCasts != null && Contract.ForAll(varsOutsideCasts, voc => voc.Key != null)); - Contract.Invariant(AxBuilder != null); - } - - - readonly TypeAxiomBuilderIntBoolU /*!*/ - AxBuilder; - - protected override bool StandardResult(VCExpr node, bool arg) - { - //Contract.Requires(node != null); - return true; // not used - } - - public override bool Visit(VCExprNAry node, bool arg) - { - Contract.Requires(node != null); - if (node.Op is VCExprBoogieFunctionOp) - { - Function func = ((VCExprBoogieFunctionOp) node.Op).Func; - Contract.Assert(func != null); - 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.Arguments) - { - 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) - { - Contract.Requires(node != null); - if (!varsOutsideCasts.ContainsKey(node)) - { - varsOutsideCasts.Add(node, null); - } - - return true; - } - } -} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/HelperFuns.cs b/Source/VCExpr/TypeErasure/HelperFuns.cs new file mode 100644 index 000000000..179162989 --- /dev/null +++ b/Source/VCExpr/TypeErasure/HelperFuns.cs @@ -0,0 +1,121 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +public class HelperFuns +{ + public static Function BoogieFunction(string name, List /*!*/ typeParams, params Type[] types) + { + Contract.Requires(types != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeParams)); + Contract.Requires(types.Length > 0); + Contract.Requires(Contract.ForAll(0, types.Length, i => types[i] != null)); + Contract.Ensures(Contract.Result() != null); + + List args = new List(); + for (int i = 0; i < types.Length - 1; ++i) + { + args.Add(new Formal(Token.NoToken, + new TypedIdent(Token.NoToken, "arg" + i, cce.NonNull(types[i])), + true)); + } + + Formal result = new Formal(Token.NoToken, + new TypedIdent(Token.NoToken, "res", + cce.NonNull(types)[types.Length - 1]), + false); + return new Function(Token.NoToken, name, new List(typeParams), args, result); + } + + public static Function BoogieFunction(string name, params Type[] types) + { + Contract.Requires(types != null); + Contract.Requires(name != null); + Contract.Ensures(Contract.Result() != null); + 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) + { + Contract.Requires(U != null); + Contract.Requires(name != null); + Contract.Ensures(Contract.Result() != null); + 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) + { + Contract.Requires(gen != null); + Contract.Requires(fun != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List /*!*/ + arguments = new List(fun.InParams.Count); + foreach (Formal /*!*/ f in fun.InParams) + { + Contract.Assert(f != null); + VCExprVar /*!*/ + var = gen.Variable(f.Name, f.TypedIdent.Type); + arguments.Add(var); + } + + return arguments; + } + + public static List /*!*/ ToList(params T[] args) where T : class + { + Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(args); + } + + public static List /*!*/ ToVCExprList(List /*!*/ list) + { + Contract.Requires(cce.NonNullElements(list)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(list); + } + + public static List /*!*/ VarVector(string baseName, int num, Type type, VCExpressionGenerator gen) + { + Contract.Requires(gen != null); + Contract.Requires(type != null); + Contract.Requires(baseName != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + 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) + { + Contract.Requires(gen != null); + Contract.Requires(baseName != null); + Contract.Requires(cce.NonNullElements(types)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List /*!*/ + res = new List(types.Count); + for (int i = 0; i < types.Count; ++i) + { + res.Add(gen.Variable(baseName + i, types[i])); + } + + return res; + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/MapTypeAbstractionBuilder.cs b/Source/VCExpr/TypeErasure/MapTypeAbstractionBuilder.cs new file mode 100644 index 000000000..96f70e643 --- /dev/null +++ b/Source/VCExpr/TypeErasure/MapTypeAbstractionBuilder.cs @@ -0,0 +1,273 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie.TypeErasure; + +[ContractClass(typeof(MapTypeAbstractionBuilderContracts))] +internal abstract class MapTypeAbstractionBuilder +{ + protected readonly TypeAxiomBuilder /*!*/ + AxBuilder; + + protected readonly VCExpressionGenerator /*!*/ + Gen; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(AxBuilder != null); + Contract.Invariant(Gen != null); + } + + + internal MapTypeAbstractionBuilder(TypeAxiomBuilder axBuilder, VCExpressionGenerator gen) + { + Contract.Requires(gen != null); + Contract.Requires(axBuilder != null); + this.AxBuilder = axBuilder; + this.Gen = gen; + AbstractionVariables = new List(); + ClassRepresentations = new Dictionary(); + } + + // constructor for cloning + internal MapTypeAbstractionBuilder(TypeAxiomBuilder axBuilder, VCExpressionGenerator gen, + MapTypeAbstractionBuilder builder) + { + Contract.Requires(builder != null); + Contract.Requires(gen != null); + Contract.Requires(axBuilder != null); + 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; + + [ContractInvariantMethod] + void AbstractionVariablesInvariantMethod() + { + Contract.Invariant(cce.NonNullElements(AbstractionVariables)); + } + + private TypeVariable AbstractionVariable(int num) + { + Contract.Requires((num >= 0)); + Contract.Ensures(Contract.Result() != null); + 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; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(RepresentingType != null); + Contract.Invariant(Select != null); + Contract.Invariant(Store != null); + } + + + public MapTypeClassRepresentation(TypeCtorDecl representingType, Function select, Function store) + { + Contract.Requires(store != null); + Contract.Requires(select != null); + Contract.Requires(representingType != null); + this.RepresentingType = representingType; + this.Select = select; + this.Store = store; + } + } + + private readonly IDictionary /*!*/ + ClassRepresentations; + + [ContractInvariantMethod] + void ClassRepresentationsInvariantMethod() + { + Contract.Invariant(ClassRepresentations != null); + } + + protected MapTypeClassRepresentation GetClassRepresentation(MapType abstractedType) + { + Contract.Requires(abstractedType != null); + if (!ClassRepresentations.TryGetValue(abstractedType, out var res)) + { + int num = ClassRepresentations.Count; + TypeCtorDecl /*!*/ + synonym = + new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Count); + + GenSelectStoreFunctions(abstractedType, synonym, out var @select, out var 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 List instantiations) + { + Contract.Requires((rawType != null)); + Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); + Contract.Ensures(Contract.Result() != null); + return AbstractAndGetRepresentation(rawType, out instantiations).Select; + } + + public Function Store(MapType rawType, out List instantiations) + { + Contract.Requires((rawType != null)); + Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); + Contract.Ensures(Contract.Result() != null); + return AbstractAndGetRepresentation(rawType, out instantiations).Store; + } + + private MapTypeClassRepresentation + AbstractAndGetRepresentation(MapType rawType, out List instantiations) + { + Contract.Requires((rawType != null)); + Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); + instantiations = new List(); + MapType /*!*/ + abstraction = ThinOutMapType(rawType, instantiations); + return GetClassRepresentation(abstraction); + } + + public CtorType AbstractMapType(MapType rawType) + { + Contract.Requires(rawType != null); + Contract.Ensures(Contract.Result() != null); + List /*!*/ + instantiations = new List(); + MapType /*!*/ + abstraction = ThinOutMapType(rawType, instantiations); + + MapTypeClassRepresentation repr = GetClassRepresentation(abstraction); + Contract.Assume(repr.RepresentingType.Arity == instantiations.Count); + return new CtorType(Token.NoToken, repr.RepresentingType, instantiations); + } + + // TODO: cache the result of this operation + protected MapType ThinOutMapType(MapType rawType, List instantiations) + { + Contract.Requires(instantiations != null); + Contract.Requires(rawType != null); + Contract.Ensures(Contract.Result() != null); + List /*!*/ + newArguments = new List(); + foreach (Type /*!*/ subtype in rawType.Arguments.ToList()) + { + Contract.Assert(subtype != null); + newArguments.Add(ThinOutType(subtype, rawType.TypeParameters, + instantiations)); + } + + Type /*!*/ + newResult = ThinOutType(rawType.Result, rawType.TypeParameters, + instantiations); + return new MapType(Token.NoToken, rawType.TypeParameters, newArguments, newResult); + } + + // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables + private Type /*!*/ ThinOutType(Type rawType, List boundTypeParams, List instantiations) + { + Contract.Requires(instantiations != null); + Contract.Requires(boundTypeParams != null); + Contract.Requires(rawType != null); + Contract.Ensures(Contract.Result() != null); + + if (rawType.FreeVariables.All(var => !boundTypeParams.Contains(var))) + { + // Bingo! + // if the type does not contain any bound variables, we can simply + // replace it with a type variable + TypeVariable /*!*/ + abstractionVar = AbstractionVariable(instantiations.Count); + Contract.Assume(!boundTypeParams.Contains(abstractionVar)); + instantiations.Add(rawType); + return abstractionVar; + } + + if (rawType.IsVariable) + { + // + // then the variable has to be bound, we cannot do anything + TypeVariable /*!*/ + rawVar = rawType.AsVariable; + Contract.Assume(boundTypeParams.Contains(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; + List /*!*/ + newArguments = new List(); + foreach (Type /*!*/ subtype in rawCtorType.Arguments.ToList()) + { + Contract.Assert(subtype != null); + 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 + } + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/OpTypeEraser.cs b/Source/VCExpr/TypeErasure/OpTypeEraser.cs new file mode 100644 index 000000000..98d10ccef --- /dev/null +++ b/Source/VCExpr/TypeErasure/OpTypeEraser.cs @@ -0,0 +1,409 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +public abstract class OpTypeEraser : StandardVCExprOpVisitor +{ + protected readonly TypeAxiomBuilderIntBoolU /*!*/ + AxBuilder; + + protected readonly TypeEraser /*!*/ + Eraser; + + protected readonly VCExpressionGenerator /*!*/ + Gen; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(AxBuilder != null); + Contract.Invariant(Eraser != null); + Contract.Invariant(Gen != null); + } + + + public OpTypeEraser(TypeEraser /*!*/ eraser, TypeAxiomBuilderIntBoolU /*!*/ axBuilder, + VCExpressionGenerator /*!*/ gen) + { + Contract.Requires(eraser != null); + Contract.Requires(axBuilder != null); + Contract.Requires(gen != null); + this.AxBuilder = axBuilder; + this.Eraser = eraser; + this.Gen = gen; + } + + protected override VCExpr StandardResult(VCExprNAry node, VariableBindings bindings) + { + //Contract.Requires(bindings != null); + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node); + Contract.Assert(false); + throw new cce.UnreachableException(); // to please the compiler + } + + private List /*!*/ MutateSeq(VCExprNAry node, VariableBindings bindings, int newPolarity) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + int oldPolarity = Eraser.Polarity; + Eraser.Polarity = newPolarity; + List /*!*/ + newArgs = Eraser.MutateSeq(node.Arguments, bindings); + Eraser.Polarity = oldPolarity; + return newArgs; + } + + private VCExpr CastArguments(VCExprNAry node, Type argType, VariableBindings bindings, int newPolarity) + { + Contract.Requires(bindings != null); + Contract.Requires(argType != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + 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, real, bool, or U) + private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Requires((node.Arity > 0)); + Contract.Ensures(Contract.Result() != null); + + List /*!*/ + newArgs = MutateSeq(node, bindings, newPolarity); + Type /*!*/ + oldType = node[0].Type; + if (AxBuilder.UnchangedType(oldType) && + node.Arguments.Skip(1).All(e => e.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) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Bool, bindings, -Eraser.Polarity); + } + + public override VCExpr VisitEqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitNeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitImpliesOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + // 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) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitIfThenElseOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + 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) + { + Contract.Requires(node != null); + Contract.Requires(bindings != null); + Contract.Ensures(Contract.Result() != null); + + List /*!*/ + newArgs = MutateSeq(node, bindings, 0); + return Gen.Function(node.Op, newArgs); + } + + public override VCExpr VisitAddOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, node.Type, bindings, 0); + } + + public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, node.Type, bindings, 0); + } + + public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, node.Type, bindings, 0); + } + + public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Int, bindings, 0); + } + + public override VCExpr VisitModOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Int, bindings, 0); + } + + public override VCExpr VisitRealDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Real, bindings, 0); + } + + /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Float, bindings, 0); + }*/ + public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Real, bindings, 0); + } + + public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, AxBuilder.U, bindings, 0); + } + + public override VCExpr VisitToIntOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitToRealOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitFloatNeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitBvExtractOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + + public override VCExpr VisitBvConcatOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + List /*!*/ + newArgs = MutateSeq(node, bindings, 0); + + // each argument is cast to its old type + Contract.Assert(newArgs.Count == node.Arity && newArgs.Count == 2); + VCExpr /*!*/ + arg0 = AxBuilder.Cast(newArgs[0], node[0].Type); + Contract.Assert(arg0 != null); + VCExpr /*!*/ + arg1 = AxBuilder.Cast(newArgs[1], node[1].Type); + Contract.Assert(arg1 != null); + return Gen.Function(node.Op, arg0, arg1); + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/TypeAxiomBuilder.cs b/Source/VCExpr/TypeErasure/TypeAxiomBuilder.cs new file mode 100644 index 000000000..8a96a9d9c --- /dev/null +++ b/Source/VCExpr/TypeErasure/TypeAxiomBuilder.cs @@ -0,0 +1,437 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.BaseTypes; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +[ContractClass(typeof(TypeAxiomBuilderContracts))] +public abstract class TypeAxiomBuilder : ICloneable +{ + protected readonly VCExpressionGenerator /*!*/ + Gen; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Gen != null); + Contract.Invariant(Ctor != null); + } + + + internal abstract MapTypeAbstractionBuilder /*!*/ MapTypeAbstracter { get; } + + /////////////////////////////////////////////////////////////////////////// + // Type Axioms + + // list in which all typed axioms are collected + private readonly List /*!*/ + AllTypeAxioms; + + [ContractInvariantMethod] + void AllTypeAxiomsInvariantMethod() + { + Contract.Invariant(cce.NonNullElements(AllTypeAxioms)); + } + + // list in which type axioms are incrementally collected + private readonly List /*!*/ + IncTypeAxioms; + + [ContractInvariantMethod] + void IncTypeAxiomsInvariantMethod() + { + Contract.Invariant(cce.NonNullElements(IncTypeAxioms)); + } + + internal void AddTypeAxiom(VCExpr axiom) + { + Contract.Requires(axiom != null); + AllTypeAxioms.Add(axiom); + IncTypeAxioms.Add(axiom); + } + + // Return all axioms that were added since the last time NewAxioms + // was called + public VCExpr GetNewAxioms() + { + Contract.Ensures(Contract.Result() != null); + 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) + { + Contract.Requires(typeRepr != null); + Contract.Ensures(Contract.Result() != null); + + VCExpr res = Gen.Eq(Gen.Function(Ctor, typeRepr), + Gen.Integer(CurrentCtorNum)); + CurrentCtorNum = CurrentCtorNum + BigNum.ONE; + return res; + } + + private VCExpr GenCtorAssignment(Function typeRepr) + { + Contract.Requires(typeRepr != null); + Contract.Ensures(Contract.Result() != null); + + List /*!*/ + quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen); + VCExpr /*!*/ + eq = + GenCtorAssignment(Gen.Function(typeRepr, + HelperFuns.ToVCExprList(quantifiedVars))); + + if (typeRepr.InParams.Count == 0) + { + return eq; + } + + return Gen.Forall(quantifiedVars, new List(), + "ctor:" + typeRepr.Name, 1, eq); + } + + // generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi) + protected VCExpr GenLeftInverseAxiom(Function fun, Function invFun, int dtorNum) + { + Contract.Requires(invFun != null); + Contract.Requires(fun != null); + Contract.Ensures(Contract.Result() != null); + List /*!*/ + quantifiedVars = HelperFuns.GenVarsForInParams(fun, Gen); + Contract.Assert(cce.NonNullElements(quantifiedVars)); + + 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))); + Contract.Assert(cce.NonNullElements(triggers)); + return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, 1, eq); + } + + /////////////////////////////////////////////////////////////////////////// + + // the type of everything that is not int, bool, or a type + [ContractInvariantMethod] + void ObjectInvariant2() + { + Contract.Invariant(UDecl != null); + Contract.Invariant(TDecl != null); + Contract.Invariant(U != null); + Contract.Invariant(T != null); + } + + 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); + + [Pure] + public abstract bool UnchangedType(Type /*!*/ type); + + /////////////////////////////////////////////////////////////////////////// + // Symbols for representing types + + private readonly IDictionary /*!*/ + BasicTypeReprs; + + [ContractInvariantMethod] + void BasicTypeReprsInvariantMethod() + { + Contract.Invariant(cce.NonNullDictionaryAndValues(BasicTypeReprs)); + } + + private VCExpr GetBasicTypeRepr(Type type) + { + Contract.Requires(type != null); + Contract.Requires(type.IsBasic || type.IsBv || type.IsFloat); + Contract.Ensures(Contract.Result() != null); + if (!BasicTypeReprs.TryGetValue(type, out var res)) + { + res = Gen.Function(HelperFuns.BoogieFunction(type.ToString() + "Type", T)); + AddTypeAxiom(GenCtorAssignment(res)); + BasicTypeReprs.Add(type, res); + } + + return cce.NonNull(res); + } + + private readonly IDictionary /*!*/ + TypeCtorReprs; + + [ContractInvariantMethod] + void TypeCtorReprsInvariantMethod() + { + Contract.Invariant(TypeCtorReprs != null); + } + + internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl decl) + { + Contract.Requires(decl != null); + if (!TypeCtorReprs.TryGetValue(decl, out var reprSet)) + { + Function /*!*/ + ctor = HelperFuns.UniformBoogieFunction(decl.Name + "Type", decl.Arity, T); + Contract.Assert(ctor != null); + 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) + { + Contract.Requires(decl != null); + Contract.Ensures(Contract.Result() != null); + return GetTypeCtorReprStruct(decl).Ctor; + } + + public Function GetTypeDtor(TypeCtorDecl decl, int num) + { + Contract.Requires(decl != null); + Contract.Ensures(Contract.Result() != null); + return GetTypeCtorReprStruct(decl).Dtors[num]; + } + + // mapping from free type variables to VCExpr variables + private readonly IDictionary /*!*/ + TypeVariableMapping; + + [ContractInvariantMethod] + void TypeVariableMappingInvariantMethod() + { + Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableMapping)); + } + + public VCExprVar Typed2Untyped(TypeVariable var) + { + Contract.Requires(var != null); + Contract.Ensures(Contract.Result() != null); + if (!TypeVariableMapping.TryGetValue(var, out var res)) + { + res = new VCExprVar(var.Name, T); + TypeVariableMapping.Add(var, res); + } + + return cce.NonNull(res); + } + + + //////////////////////////////////////////////////////////////////////////// + // Symbols for representing variables and constants + + // Globally defined variables + private readonly IDictionary /*!*/ + Typed2UntypedVariables; + + [ContractInvariantMethod] + void Typed2UntypedVariablesInvariantMethod() + { + Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedVariables)); + } + + // This method must only be used for free (unbound) variables + public VCExprVar Typed2Untyped(VCExprVar var) + { + Contract.Requires(var != null); + Contract.Ensures(Contract.Result() != null); + VCExprVar res = TryTyped2Untyped(var); + if (res == null) + { + res = Gen.Variable(var.Name, TypeAfterErasure(var.Type)); + Typed2UntypedVariables.Add(var, res); + AddVarTypeAxiom(res, var.Type); + } + + return cce.NonNull(res); + } + + /// + /// This method is like Typed2Untyped, except in the case where the given variables + /// doesn't exist in the mapping. For that case, this method returns null whereas + /// Typed2Untyped creates a new variable that it adds to the mapping. + /// + /// + /// + public VCExprVar TryTyped2Untyped(VCExprVar var) + { + Contract.Requires(var != null); + if (Typed2UntypedVariables.TryGetValue(var, out var res)) + { + return res; + } + else + { + return null; + } + } + + protected abstract void AddVarTypeAxiom(VCExprVar /*!*/ var, Type /*!*/ originalType); + + /////////////////////////////////////////////////////////////////////////// + // Translation function from types to their term representation + + public VCExpr Type2Term(Type type, IDictionary /*!*/ varMapping) + { + Contract.Requires(type != null); + Contract.Requires(cce.NonNullDictionaryAndValues(varMapping)); + Contract.Ensures(Contract.Result() != null); + // + if (type.IsBasic || type.IsBv || type.IsFloat) + { + // + return GetBasicTypeRepr(type); + // + } + else if (type.IsCtor) + { + // + CtorType ctype = type.AsCtor; + Function /*!*/ + repr = GetTypeCtorRepr(ctype.Decl); + List /*!*/ + args = new List(ctype.Arguments.Count); + foreach (Type /*!*/ t in ctype.Arguments.ToArray()) + { + Contract.Assert(t != null); + args.Add(Type2Term(t, varMapping)); + } + + return Gen.Function(repr, args); + // + } + else if (type.IsVariable) + { + // + if (!varMapping.TryGetValue(type.AsVariable, out var res)) + { + // then the variable is free and we bind it at this point to a term + // variable + res = Typed2Untyped(type.AsVariable); + } + + return cce.NonNull(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); + Contract.Assert(false); + throw new cce.UnreachableException(); // please the compiler + } + } + + //////////////////////////////////////////////////////////////////////////// + + public TypeAxiomBuilder(VCExpressionGenerator gen) + { + Contract.Requires(gen != null); + 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 List()); + U = u; + + TypeCtorDecl /*!*/ + tDecl = new TypeCtorDecl(Token.NoToken, "T", 0); + TDecl = tDecl; + Type /*!*/ + t = new CtorType(Token.NoToken, tDecl, new List()); + T = t; + + Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int); + } + + public virtual void Setup(List usedTypes) + { + foreach (var ty in usedTypes) { + GetBasicTypeRepr(ty); + } + } + + // constructor to allow cloning + internal TypeAxiomBuilder(TypeAxiomBuilder builder) + { + Contract.Requires(builder != null); + 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(); + + public abstract VCExpr Cast(VCExpr expr, Type toType); +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/TypeEraser.cs b/Source/VCExpr/TypeErasure/TypeEraser.cs new file mode 100644 index 000000000..b5818305b --- /dev/null +++ b/Source/VCExpr/TypeErasure/TypeEraser.cs @@ -0,0 +1,237 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +[ContractClass(typeof(TypeEraserContracts))] +public abstract class TypeEraser : MutatingVCExprVisitor +{ + protected readonly TypeAxiomBuilderIntBoolU /*!*/ + AxBuilder; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(AxBuilder != null); + } + + + protected abstract OpTypeEraser /*!*/ OpEraser { get; } + + //////////////////////////////////////////////////////////////////////////// + + public TypeEraser(TypeAxiomBuilderIntBoolU axBuilder, VCExpressionGenerator gen) + : base(gen) + { + Contract.Requires(gen != null); + Contract.Requires(axBuilder != null); + AxBuilder = axBuilder; + } + + public VCExpr Erase(VCExpr expr, int polarity) + { + Contract.Requires(expr != null); + Contract.Requires((polarity >= -1 && polarity <= 1)); + Contract.Ensures(Contract.Result() != null); + 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) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real || + node.Type == Type.RMode || node.Type == Type.String || node.Type == Type.RegEx); + return node; + } + + //////////////////////////////////////////////////////////////////////////// + + public override bool AvoidVisit(VCExprNAry node, VariableBindings arg) + { + return node.Op.Equals(VCExpressionGenerator.AndOp) || + node.Op.Equals(VCExpressionGenerator.OrOp); + } + + public override VCExpr Visit(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + 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) + { + //Contract.Requires(originalNode != null); + //Contract.Requires(cce.NonNullElements(newSubExprs)); + //Contract.Requires(bindings != null); + Contract.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) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + if (!bindings.VCExprVarBindings.TryGetValue(node, out var res)) + { + return AxBuilder.Typed2Untyped(node); + } + + return cce.NonNull(res); + } + + //////////////////////////////////////////////////////////////////////////// + + protected bool IsUniversalQuantifier(VCExprQuantifier node) + { + Contract.Requires(node != null); + 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) + { + Contract.Requires(bindings != null); + Contract.Requires(cce.NonNullElements(oldBoundVars)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + + 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) + { + Contract.Requires(node != null); + Contract.Requires(newNode != null); + Contract.Requires(cce.NonNullElements(occurringVars)); + Contract.Requires(oldBindings != null); + Contract.Ensures(Contract.ValueAtReturn(out newBindings) != null); + Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out 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) + { + Contract.Assert(var != null); + Type /*!*/ + newType = + castVariables.Contains(var) + ? AxBuilder.U + : AxBuilder.TypeAfterErasure(var.Type); + Contract.Assert(newType != null); + VCExprVar /*!*/ + newVar = Gen.Variable(var.Name, newType); + Contract.Assert(newVar != null); + newBoundVars.Add(newVar); + newBindings.VCExprVarBindings.Add(var, newVar); + } + + return true; + } + + //////////////////////////////////////////////////////////////////////////// + + public override VCExpr Visit(VCExprLet node, VariableBindings bindings) + { + Contract.Requires(bindings != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + 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]; + Contract.Assert(binding != null); + 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); + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/TypeEraserContracts.cs b/Source/VCExpr/TypeErasure/TypeEraserContracts.cs new file mode 100644 index 000000000..b1441e931 --- /dev/null +++ b/Source/VCExpr/TypeErasure/TypeEraserContracts.cs @@ -0,0 +1,22 @@ +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie.TypeErasure; + +[ContractClassFor(typeof(TypeEraser))] +public abstract class TypeEraserContracts : TypeEraser +{ + public TypeEraserContracts() + : base(null, null) + { + } + + protected override OpTypeEraser OpEraser + { + get + { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/TypeEraserPremisses.cs b/Source/VCExpr/TypeErasure/TypeEraserPremisses.cs new file mode 100644 index 000000000..c1957bd47 --- /dev/null +++ b/Source/VCExpr/TypeErasure/TypeEraserPremisses.cs @@ -0,0 +1,335 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +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.Contains(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; + } + + if (!RedoQuantifier(node, (VCExprQuantifier) newNode, occurringVars, oldBindings, + out var 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) || + AxBuilderPremisses.Options.TypeEncodingMethod + == CoreOptions.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 + + VCExpr /*!*/ + typePremisses = + GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs, + bindings.TypeVariableBindings, + typeVarBindings, out var furtherTriggers); + + Contract.Assert(cce.NonNullElements(furtherTriggers)); + Contract.Assert(typePremisses != null); + List /*!*/ + newTriggers = new List(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 + + 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.Info, 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); + HashSet freeVars = FreeVariableCollector.FreeTermVariables(e); + Contract.Assert(freeVars != null && cce.NonNullElements(freeVars)); + if (typeVarBindings.Any(b => freeVars.Contains(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; + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/TypeErasure.cs b/Source/VCExpr/TypeErasure/TypeErasure.cs new file mode 100644 index 000000000..e9f7a9128 --- /dev/null +++ b/Source/VCExpr/TypeErasure/TypeErasure.cs @@ -0,0 +1,433 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +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 +{ + // 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?) + + ////////////////////////////////////////////////////////////////////////////// + + 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; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Ctor != null); + Contract.Invariant(cce.NonNullElements(Dtors)); + } + + + public TypeCtorRepr(Function ctor, List /*!*/ dtors) + { + Contract.Requires(ctor != null); + Contract.Requires(cce.NonNullElements(dtors)); + Contract.Requires(ctor.InParams.Count == 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 syntactic approach). + + [ContractClassFor(typeof(TypeAxiomBuilder))] + public abstract class TypeAxiomBuilderContracts : TypeAxiomBuilder + { + public TypeAxiomBuilderContracts() + : base((VCExpressionGenerator) null) + { + } + + internal override MapTypeAbstractionBuilder MapTypeAbstracter + { + get + { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + public override Type TypeAfterErasure(Type type) + { + Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + + public override bool UnchangedType(Type type) + { + Contract.Requires(type != null); + throw new NotImplementedException(); + } + + protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) + { + Contract.Requires(var != null); + Contract.Requires(originalType != null); + throw new NotImplementedException(); + } + + public override object Clone() + { + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + } + + ////////////////////////////////////////////////////////////////////////////// + + // 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 + + [ContractClass(typeof(TypeAxiomBuilderIntBoolUContracts))] + public abstract class TypeAxiomBuilderIntBoolU : TypeAxiomBuilder + { + public TypeAxiomBuilderIntBoolU(VCExpressionGenerator gen) + : base(gen) + { + Contract.Requires(gen != null); + + TypeCasts = new Dictionary(); + } + + // constructor to allow cloning + internal TypeAxiomBuilderIntBoolU(TypeAxiomBuilderIntBoolU builder) + : base(builder) + { + Contract.Requires(builder != null); + + TypeCasts = new Dictionary(builder.TypeCasts); + } + + public override void Setup(List usedTypes) + { + base.Setup(usedTypes); + + foreach (var ty in usedTypes) { + GetTypeCasts(ty); + } + } + + // 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) + { + Contract.Requires((castFromU != null)); + Contract.Requires((castToU != null)); + Contract.Ensures((cce.NonNullElements(Contract.ValueAtReturn(out triggers)))); + Contract.Ensures(Contract.ValueAtReturn(out var) != null); + Contract.Ensures(Contract.Result() != null); + 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; + + [ContractInvariantMethod] + void TypeCastsInvariantMethod() + { + Contract.Invariant(TypeCasts != null); + } + + private TypeCastSet GetTypeCasts(Type type) + { + Contract.Requires(type != null); + if (!TypeCasts.TryGetValue(type, out var 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; + } + + [Pure] + public Function CastTo(Type type) + { + Contract.Requires(type != null); + Contract.Requires(UnchangedType(type)); + Contract.Ensures(Contract.Result() != null); + return GetTypeCasts(type).CastFromU; + } + + public Function CastFrom(Type type) + { + Contract.Requires(type != null); + Contract.Requires((UnchangedType(type))); + Contract.Ensures(Contract.Result() != null); + return GetTypeCasts(type).CastToU; + } + + private struct TypeCastSet + { + public readonly Function /*!*/ + CastToU; + + public readonly Function /*!*/ + CastFromU; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(CastToU != null); + Contract.Invariant(CastFromU != null); + } + + + public TypeCastSet(Function castToU, Function castFromU) + { + Contract.Requires(castFromU != null); + Contract.Requires(castToU != null); + CastToU = castToU; + CastFromU = castFromU; + } + } + + public bool IsCast(Function fun) + { + Contract.Requires(fun != null); + if (fun.InParams.Count != 1) + { + return false; + } + + Type /*!*/ + inType = cce.NonNull(fun.InParams[0]).TypedIdent.Type; + if (inType.Equals(U)) + { + Type /*!*/ + outType = cce.NonNull(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 = cce.NonNull(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, Type.Real, Type.Bool, and Type.RMode + + public override Type TypeAfterErasure(Type type) + { + //Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); + 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) + { + //Contract.Requires(type != null); + return type.IsInt || type.IsReal || type.IsBool || type.IsBv || type.IsFloat || type.IsRMode || type.IsString || + type.IsRegEx; + } + + public override VCExpr Cast(VCExpr expr, Type toType) + { + Contract.Requires(toType != null); + Contract.Requires(expr != null); + Contract.Requires((expr.Type.Equals(U) || UnchangedType(expr.Type))); + Contract.Requires((toType.Equals(U) || UnchangedType(toType))); + Contract.Ensures(Contract.Result() != null); + if (expr.Type.Equals(toType)) + { + return expr; + } + + if (toType.Equals(U)) + { + return Gen.Function(CastFrom(expr.Type), expr); + } + else + { + Contract.Assert(expr.Type.Equals(U)); + return Gen.Function(CastTo(toType), expr); + } + } + + public List /*!*/ CastSeq(List /*!*/ exprs, Type toType) + { + Contract.Requires(toType != null); + Contract.Requires(cce.NonNullElements(exprs)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List /*!*/ + res = new List(exprs.Count); + foreach (VCExpr /*!*/ expr in exprs) + { + Contract.Assert(expr != null); + res.Add(Cast(expr, toType)); + } + + return res; + } + } + + [ContractClassFor(typeof(TypeAxiomBuilderIntBoolU))] + public abstract class TypeAxiomBuilderIntBoolUContracts : TypeAxiomBuilderIntBoolU + { + public TypeAxiomBuilderIntBoolUContracts() + : base((TypeAxiomBuilderIntBoolU) null) + { + } + + protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) + { + Contract.Requires(castToU != null); + Contract.Requires(castFromU != null); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + + protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) + { + Contract.Requires(castFromU != null); + Contract.Requires(castToU != null); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + + internal override MapTypeAbstractionBuilder MapTypeAbstracter + { + get { throw new NotImplementedException(); } + } + + protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) + { + throw new NotImplementedException(); + } + + public override object Clone() + { + throw new NotImplementedException(); + } + } + + ////////////////////////////////////////////////////////////////////////////// + // 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) + + [ContractClassFor(typeof(MapTypeAbstractionBuilder))] + internal abstract class MapTypeAbstractionBuilderContracts : MapTypeAbstractionBuilder + { + public MapTypeAbstractionBuilderContracts() + : base(null, null) + { + } + + protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonymDecl, + out Function select, out Function store) + { + Contract.Requires(abstractedType != null); + Contract.Requires(synonymDecl != null); + Contract.Ensures(Contract.ValueAtReturn(out select) != null); + Contract.Ensures(Contract.ValueAtReturn(out store) != null); + + throw new NotImplementedException(); + } + } + + + ////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////// + + // 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. + + + ////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////// +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasure/TypeErasureArguments.cs similarity index 100% rename from Source/VCExpr/TypeErasureArguments.cs rename to Source/VCExpr/TypeErasure/TypeErasureArguments.cs diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasure/TypeErasurePremisses.cs similarity index 71% rename from Source/VCExpr/TypeErasurePremisses.cs rename to Source/VCExpr/TypeErasure/TypeErasurePremisses.cs index 5729a2642..9e2f75dcb 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasure/TypeErasurePremisses.cs @@ -1117,477 +1117,5 @@ private VCExpr GenMapAxiom1(Function select, Function store, Type mapResult, ///////////////////////////////////////////////////////////////////////////// - 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.Contains(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; - } - - if (!RedoQuantifier(node, (VCExprQuantifier) newNode, occurringVars, oldBindings, - out var 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) || - AxBuilderPremisses.Options.TypeEncodingMethod - == CoreOptions.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 - - VCExpr /*!*/ - typePremisses = - GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs, - bindings.TypeVariableBindings, - typeVarBindings, out var furtherTriggers); - - Contract.Assert(cce.NonNullElements(furtherTriggers)); - Contract.Assert(typePremisses != null); - List /*!*/ - newTriggers = new List(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 - - 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.Info, 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); - HashSet freeVars = FreeVariableCollector.FreeTermVariables(e); - Contract.Assert(freeVars != null && cce.NonNullElements(freeVars)); - if (typeVarBindings.Any(b => freeVars.Contains(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); - Function /*!*/ - select = - AxBuilder.MapTypeAbstracter.Select(mapType, out var 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.Arguments, bindings); - } - - public override VCExpr VisitStoreOp(VCExprNAry node, VariableBindings bindings) - { - Contract.Requires(bindings != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - Function /*!*/ - store = - AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out var instantiations); - Contract.Assert(store != null); - return HandleFunctionOp(store, - // the store function never has explicit - // type parameters - new List(), - node.Arguments, 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.Arguments, 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; - } - } } \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/VariableBindings.cs b/Source/VCExpr/TypeErasure/VariableBindings.cs new file mode 100644 index 000000000..7085846c0 --- /dev/null +++ b/Source/VCExpr/TypeErasure/VariableBindings.cs @@ -0,0 +1,61 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +public class VariableBindings +{ + public readonly IDictionary /*!*/ + VCExprVarBindings; + + public readonly IDictionary /*!*/ + TypeVariableBindings; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullDictionaryAndValues(VCExprVarBindings)); + Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableBindings)); + } + + + public VariableBindings(IDictionary /*!*/ vcExprVarBindings, + IDictionary /*!*/ typeVariableBindings) + { + Contract.Requires(cce.NonNullDictionaryAndValues(vcExprVarBindings)); + Contract.Requires(cce.NonNullDictionaryAndValues(typeVariableBindings)); + this.VCExprVarBindings = vcExprVarBindings; + this.TypeVariableBindings = typeVariableBindings; + } + + public VariableBindings() : + this(new Dictionary(), + new Dictionary()) + { + } + + public VariableBindings Clone() + { + Contract.Ensures(Contract.Result() != null); + IDictionary /*!*/ + newVCExprVarBindings = + new Dictionary(); + foreach (KeyValuePair pair in VCExprVarBindings) + { + Contract.Assert(cce.NonNullElements(pair)); + newVCExprVarBindings.Add(pair); + } + + IDictionary /*!*/ + newTypeVariableBindings = + new Dictionary(); + foreach (KeyValuePair pair in TypeVariableBindings) + { + Contract.Assert(cce.NonNullElements(pair)); + newTypeVariableBindings.Add(pair); + } + + return new VariableBindings(newVCExprVarBindings, newTypeVariableBindings); + } +} \ No newline at end of file diff --git a/Source/VCExpr/TypeErasure/VariableCastCollector.cs b/Source/VCExpr/TypeErasure/VariableCastCollector.cs new file mode 100644 index 000000000..860a509f6 --- /dev/null +++ b/Source/VCExpr/TypeErasure/VariableCastCollector.cs @@ -0,0 +1,159 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.TypeErasure; + +/// +/// 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) + { + Contract.Requires((axBuilder != null)); + Contract.Requires((newNode != null)); + Contract.Requires((oldNode != null)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + VariableCastCollector /*!*/ + collector = new VariableCastCollector(axBuilder); + Contract.Assert(collector != null); + if (newNode.Triggers.Any(trigger => trigger.Pos)) + { + // look in the given triggers + foreach (VCTrigger /*!*/ trigger in newNode.Triggers) + { + Contract.Assert(trigger != null); + if (trigger.Pos) + { + foreach (VCExpr /*!*/ expr in trigger.Exprs) + { + Contract.Assert(expr != null); + 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) + { + Contract.Assert(castVar != null); + 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) + { + Contract.Requires(axBuilder != null); + this.AxBuilder = axBuilder; + } + + readonly List /*!*/ + varsInCasts = new List(); + + readonly Dictionary /*!*/ + varsOutsideCasts = new Dictionary(); + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullElements(varsInCasts)); + Contract.Invariant(varsOutsideCasts != null && Contract.ForAll(varsOutsideCasts, voc => voc.Key != null)); + Contract.Invariant(AxBuilder != null); + } + + + readonly TypeAxiomBuilderIntBoolU /*!*/ + AxBuilder; + + protected override bool StandardResult(VCExpr node, bool arg) + { + //Contract.Requires(node != null); + return true; // not used + } + + public override bool Visit(VCExprNAry node, bool arg) + { + Contract.Requires(node != null); + if (node.Op is VCExprBoogieFunctionOp) + { + Function func = ((VCExprBoogieFunctionOp) node.Op).Func; + Contract.Assert(func != null); + 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.Arguments) + { + 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) + { + Contract.Requires(node != null); + if (!varsOutsideCasts.ContainsKey(node)) + { + varsOutsideCasts.Add(node, null); + } + + return true; + } +} \ No newline at end of file diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 252af77fa..eece56645 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -873,341 +873,6 @@ protected override bool VisitAfterBinding(VCExprLet node, bool arg) // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary // to avoid stack overflows (like in TraversingVCExprVisitor) - public abstract class MutatingVCExprVisitor - : IVCExprVisitor - { - protected readonly VCExpressionGenerator /*!*/ - Gen; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Gen != null); - } - - public MutatingVCExprVisitor(VCExpressionGenerator gen) - { - Contract.Requires(gen != null); - this.Gen = gen; - } - - public VCExpr Mutate(VCExpr expr, Arg arg) - { - Contract.Requires(expr != null); - Contract.Ensures(Contract.Result() != null); - return expr.Accept(this, arg); - } - - public List /*!*/ MutateSeq(IEnumerable /*!*/ exprs, Arg arg) - { - Contract.Requires(cce.NonNullElements(exprs)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List /*!*/ - res = new List(); - foreach (VCExpr /*!*/ expr in exprs) - { - Contract.Assert(expr != null); - res.Add(expr.Accept(this, arg)); - } - - return res; - } - - private List /*!*/ MutateList(List /*!*/ exprs, Arg arg) - { - Contract.Requires(cce.NonNullElements(exprs)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - bool changed = false; - List /*!*/ - res = new List(); - foreach (VCExpr /*!*/ expr in exprs) - { - Contract.Assert(expr != null); - VCExpr /*!*/ - newExpr = expr.Accept(this, arg); - if (!Object.ReferenceEquals(expr, newExpr)) - { - changed = true; - } - - res.Add(newExpr); - } - - if (!changed) - { - return exprs; - } - - return res; - } - - public virtual VCExpr Visit(VCExprLiteral node, Arg arg) - { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - return node; - } - - //////////////////////////////////////////////////////////////////////////// - - // Special element used to mark the positions in the todo-stack where - // results have to be popped from the result-stack. - private static readonly VCExpr /*!*/ - CombineResultsMarker = new VCExprLiteral(Type.Bool); - - // The todo-stack contains records of the shape - // - // arg0 - // arg1 - // arg2 - // ... - // CombineResultsMarker - // f(arg0, arg1, arg2, ...) (the original expression) - - private readonly Stack /*!*/ - NAryExprTodoStack = new Stack(); - - private readonly Stack /*!*/ - NAryExprResultStack = new Stack(); - - [ContractInvariantMethod] - void ObjectInvarianta() - { - Contract.Invariant(cce.NonNullElements(NAryExprResultStack)); - Contract.Invariant(cce.NonNullElements(NAryExprTodoStack)); - } - - - private void PushTodo(VCExprNAry exprTodo) - { - Contract.Requires(exprTodo != null); - NAryExprTodoStack.Push(exprTodo); - NAryExprTodoStack.Push(CombineResultsMarker); - for (int i = exprTodo.Arity - 1; i >= 0; --i) - { - NAryExprTodoStack.Push(exprTodo[i]); - } - } - - public virtual bool AvoidVisit(VCExprNAry node, Arg arg) - { - return true; - } - - public virtual VCExpr Visit(VCExprNAry node, Arg arg) - { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - int initialStackSize = NAryExprTodoStack.Count; - int initialResultStackSize = NAryExprResultStack.Count; - - PushTodo(node); - - while (NAryExprTodoStack.Count > initialStackSize) - { - VCExpr /*!*/ - subExpr = NAryExprTodoStack.Pop(); - Contract.Assert(subExpr != null); - - if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) - { - // assemble a result - VCExprNAry /*!*/ - originalExpr = (VCExprNAry) NAryExprTodoStack.Pop(); - Contract.Assert(originalExpr != null); - VCExprOp /*!*/ - op = originalExpr.Op; - bool changed = false; - List /*!*/ - newSubExprs = new List(); - - for (int i = op.Arity - 1; i >= 0; --i) - { - VCExpr /*!*/ - nextSubExpr = NAryExprResultStack.Pop(); - Contract.Assert(nextSubExpr != null); - if (!Object.ReferenceEquals(nextSubExpr, originalExpr[i])) - { - changed = true; - } - - newSubExprs.Insert(0, nextSubExpr); - } - - NAryExprResultStack.Push(UpdateModifiedNode(originalExpr, newSubExprs, changed, arg)); - // - } - else - { - // - VCExprNAry narySubExpr = subExpr as VCExprNAry; - if (narySubExpr != null && this.AvoidVisit(narySubExpr, arg) && - // as in VCExprNAryUniformOpEnumerator, all expressions with - // type parameters are allowed to be inspected more closely - narySubExpr.TypeParamArity == 0) - { - PushTodo(narySubExpr); - } - else - { - NAryExprResultStack.Push(subExpr.Accept(this, arg)); - } - - // - } - } - - Contract.Assert(NAryExprTodoStack.Count == initialStackSize && - NAryExprResultStack.Count == initialResultStackSize + 1); - return NAryExprResultStack.Pop(); - } - - protected virtual VCExpr /*!*/ UpdateModifiedNode(VCExprNAry /*!*/ originalNode, - List /*!*/ newSubExprs, // has any of the subexpressions changed? - bool changed, - Arg arg) - { - Contract.Requires(cce.NonNullElements(newSubExprs)); - Contract.Ensures(Contract.Result() != null); - - if (changed) - { - return Gen.Function(originalNode.Op, - newSubExprs, originalNode.TypeArguments); - } - else - { - return originalNode; - } - } - - //////////////////////////////////////////////////////////////////////////// - - public virtual VCExpr Visit(VCExprVar node, Arg arg) - { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - return node; - } - - protected List /*!*/ MutateTriggers(List /*!*/ triggers, Arg arg) - { - Contract.Requires(cce.NonNullElements(triggers)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List /*!*/ - newTriggers = new List(); - bool changed = false; - foreach (VCTrigger /*!*/ trigger in triggers) - { - Contract.Assert(trigger != null); - List /*!*/ - exprs = trigger.Exprs; - List /*!*/ - newExprs = MutateList(exprs, arg); - - if (Object.ReferenceEquals(exprs, newExprs)) - { - newTriggers.Add(trigger); - } - else - { - newTriggers.Add(Gen.Trigger(trigger.Pos, newExprs)); - changed = true; - } - } - - if (!changed) - { - return triggers; - } - - return newTriggers; - } - - public virtual VCExpr Visit(VCExprQuantifier node, Arg arg) - { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - bool changed = false; - - VCExpr /*!*/ - body = node.Body; - Contract.Assert(body != null); - VCExpr /*!*/ - newbody = body.Accept(this, arg); - Contract.Assert(newbody != null); - if (!Object.ReferenceEquals(body, newbody)) - { - changed = true; - } - - // visit the trigger expressions as well - List /*!*/ - triggers = node.Triggers; - Contract.Assert(cce.NonNullElements(triggers)); - List /*!*/ - newTriggers = MutateTriggers(triggers, arg); - Contract.Assert(cce.NonNullElements(newTriggers)); - if (!Object.ReferenceEquals(triggers, newTriggers)) - { - changed = true; - } - - if (!changed) - { - return node; - } - - return Gen.Quantify(node.Quan, node.TypeParameters, node.BoundVars, - newTriggers, node.Info, newbody); - } - - public virtual VCExpr Visit(VCExprLet node, Arg arg) - { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - bool changed = false; - - VCExpr /*!*/ - body = node.Body; - VCExpr /*!*/ - newbody = body.Accept(this, arg); - if (!Object.ReferenceEquals(body, newbody)) - { - changed = true; - } - - List /*!*/ - newbindings = new List(); - for (int i = 0; i < node.Length; ++i) - { - VCExprLetBinding /*!*/ - binding = node[i]; - Contract.Assert(binding != null); - VCExpr /*!*/ - e = binding.E; - VCExpr /*!*/ - newE = e.Accept(this, arg); - if (Object.ReferenceEquals(e, newE)) - { - newbindings.Add(binding); - } - else - { - changed = true; - newbindings.Add(Gen.LetBinding(binding.V, newE)); - } - } - - if (!changed) - { - return node; - } - - return Gen.Let(newbindings, newbody); - } - } - //////////////////////////////////////////////////////////////////////////// // Substitutions and a visitor for applying substitutions. A substitution can // substitute both type variables and term variables