diff options
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 6671 |
1 files changed, 3351 insertions, 3320 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 6b2e1201..b980a22b 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1,3320 +1,3351 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-//---------------------------------------------------------------------------------------------
-// BoogiePL - Absy.cs
-//---------------------------------------------------------------------------------------------
-
-namespace Microsoft.Boogie {
- using System;
- using System.Collections;
- using System.Diagnostics;
- using System.Collections.Generic;
- using Microsoft.Boogie.AbstractInterpretation;
- using System.Diagnostics.Contracts;
- using System.Linq;
- using Microsoft.Basetypes;
-
- using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables
-
-
- //---------------------------------------------------------------------
- // Expressions
- //
- // For expressions, we override the Equals and GetHashCode method to
- // implement structural equality. Note this is not logical equivalence
- // and is not modulo alpha-renaming.
- //---------------------------------------------------------------------
-
-
- [ContractClass(typeof(ExprContracts))]
- public abstract class Expr : Absy {
- public Expr(IToken/*!*/ tok, bool immutable)
- : base(tok) {
- Contract.Requires(tok != null);
- this.Immutable = immutable;
- }
-
- public void Emit(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- Emit(stream, 0, false);
- }
-
- /// <summary>
- /// If true the client is making a promise that this Expr will be
- /// treated immutably (i.e. once constructed it is never changed).
- /// This is currently not enforced but it should be!
- ///
- /// This allows the Expr's hash code to be cached making calls to
- /// GetHashCode() very cheap.
- /// </summary>
- /// <value><c>true</c> if immutable; otherwise, <c>false</c>.</value>
- public bool Immutable {
- get;
- private set;
- }
-
- /// <summary>
- /// Computes the hash code of this Expr skipping any cache.
- ///
- /// Sub classes should place their implementation of computing their hashcode
- /// here (making sure to call GetHashCode() not ComputeHashCode() on Expr for performance reasons)
- /// and have GetHashCode() use a cached result from ComputeHashCode() if the
- /// Expr was constructed to be immutable.
- /// </summary>
- /// <returns>The hash code.</returns>
- public abstract int ComputeHashCode();
- protected int CachedHashCode = 0;
-
- public abstract void Emit(TokenTextWriter/*!*/ wr, int contextBindingStrength, bool fragileContext);
-
- [Pure]
- public override string ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- System.IO.StringWriter buffer = new System.IO.StringWriter();
- using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false, /*pretty=*/ false)) {
- this.Emit(stream, 0, false);
- }
- return buffer.ToString();
- }
-
- /// <summary>
- /// Add to "freeVars" the free variables in the expression.
- /// </summary>
- public abstract void ComputeFreeVariables(Set /*Variable*//*!*/ freeVars);
-
- /// <summary>
- /// Filled in by the Typecheck method. A value of "null" means a succeeding
- /// call to Typecheck has not taken place (that is, either Typecheck hasn't
- /// been called or Typecheck encountered an error in the expression to be
- /// typechecked).
- /// </summary>
- private Type _Type = null;
- public Type Type {
- get {
- return _Type;
- }
- set {
- if (_Type == null) {
- // Expr has never been type checked so always allow this
- _Type = value;
- } else {
- if (Immutable && !_Type.Equals(value))
- throw new InvalidOperationException("Cannot change the Type of an Immutable Expr");
-
- // Once the Type has been set (i.e. no longer null) we never change the reference
- // if this Expr is immutable, even if the Type is equivalent (i.e. _Type.Equals(newType))
- if (!Immutable)
- _Type = value;
- }
- }
- }
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- Contract.Ensures(Type != null);
- // This body is added only because C# insists on it. It should really be left out, as if TypeCheck still were abstract.
- // The reason for mentioning the method here at all is to give TypeCheck a postcondition for all expressions.
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
-
- /// <summary>
- /// Returns the type of the expression, supposing that all its subexpressions are well typed.
- /// </summary>
- public abstract Type/*!*/ ShallowType {
- get;
- }
-
- // Handy syntactic sugar follows:
-
- public static NAryExpr Unary(IToken x, UnaryOperator.Opcode op, Expr e1) {
- Contract.Requires(e1 != null);
- Contract.Requires(x != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return new NAryExpr(x, new UnaryOperator(x, op), new List<Expr> { e1 });
- }
-
- public static NAryExpr Binary(IToken x, BinaryOperator.Opcode op, Expr e0, Expr e1) {
- Contract.Requires(e1 != null);
- Contract.Requires(e0 != null);
- Contract.Requires(x != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return new NAryExpr(x, new BinaryOperator(x, op), new List<Expr> { e0, e1 });
- }
-
- public static NAryExpr Binary(BinaryOperator.Opcode op, Expr e0, Expr e1) {
- Contract.Requires(e1 != null);
- Contract.Requires(e0 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(Token.NoToken, op, e0, e1);
- }
-
- public static NAryExpr Eq(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Eq, e1, e2);
- }
- public static NAryExpr Neq(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Neq, e1, e2);
- }
- public static NAryExpr Le(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Le, e1, e2);
- }
- public static NAryExpr Ge(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Ge, e1, e2);
- }
- public static NAryExpr Lt(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Lt, e1, e2);
- }
- public static NAryExpr Gt(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Gt, e1, e2);
- }
- public static Expr And(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- if (e1 == true_) {
- return e2;
- } else if (e2 == true_) {
- return e1;
- } else if (e1 == false_ || e2 == false_) {
- return false_;
- } else {
- var res = Binary(BinaryOperator.Opcode.And, e1, e2);
- res.Type = Microsoft.Boogie.Type.Bool;
- res.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- return res;
- }
- }
- public static Expr Or(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- if (e1 == false_) {
- return e2;
- } else if (e2 == false_) {
- return e1;
- } else if (e1 == true_ || e2 == true_) {
- return true_;
- } else {
- return Binary(BinaryOperator.Opcode.Or, e1, e2);
- }
- }
- public static Expr Not(Expr e1) {
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- NAryExpr nary = e1 as NAryExpr;
-
- if (e1 == true_) {
- return false_;
- } else if (e1 == false_) {
- return true_;
- } else if (nary != null) {
- if (nary.Fun is UnaryOperator) {
- UnaryOperator op = (UnaryOperator)nary.Fun;
- if (op.Op == UnaryOperator.Opcode.Not) {
- return cce.NonNull(nary.Args[0]);
- }
- } else if (nary.Fun is BinaryOperator) {
- BinaryOperator op = (BinaryOperator)nary.Fun;
- Expr arg0 = cce.NonNull(nary.Args[0]);
- Expr arg1 = cce.NonNull(nary.Args[1]);
- if (op.Op == BinaryOperator.Opcode.Eq) {
- return Neq(arg0, arg1);
- } else if (op.Op == BinaryOperator.Opcode.Neq) {
- return Eq(arg0, arg1);
- } else if (op.Op == BinaryOperator.Opcode.Lt) {
- return Le(arg1, arg0);
- } else if (op.Op == BinaryOperator.Opcode.Le) {
- return Lt(arg1, arg0);
- } else if (op.Op == BinaryOperator.Opcode.Ge) {
- return Gt(arg1, arg0);
- } else if (op.Op == BinaryOperator.Opcode.Gt) {
- return Ge(arg1, arg0);
- }
- }
- }
-
- return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
- }
-
- public static Expr Neg(Expr e1) {
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- return Unary(Token.NoToken, UnaryOperator.Opcode.Neg, e1);
- }
-
- public static NAryExpr Imp(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Imp, e1, e2);
- }
- public static NAryExpr Iff(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Iff, e1, e2);
- }
- public static NAryExpr Add(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Add, e1, e2);
- }
- public static NAryExpr Sub(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Sub, e1, e2);
- }
- public static NAryExpr Mul(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Mul, e1, e2);
- }
- public static NAryExpr Div(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Div, e1, e2);
- }
- public static NAryExpr Mod(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Mod, e1, e2);
- }
- public static NAryExpr RealDiv(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.RealDiv, e1, e2);
- }
- public static NAryExpr FloatDiv(Expr e1, Expr e2)
- {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.FloatDiv, e1, e2);
- }
- public static NAryExpr Pow(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Pow, e1, e2);
- }
- public static NAryExpr Subtype(Expr e1, Expr e2) {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.Subtype, e1, e2);
- }
-
- public static IdentifierExpr Ident(string name, Type type) {
- Contract.Requires(type != null);
- Contract.Requires(name != null);
- Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
- return new IdentifierExpr(Token.NoToken, name, type);
- }
-
- public static IdentifierExpr Ident(Variable decl) {
- Contract.Requires(decl != null);
- Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
- IdentifierExpr result = new IdentifierExpr(Token.NoToken, decl);
- return result;
- }
-
- public static LiteralExpr Literal(bool value) {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return new LiteralExpr(Token.NoToken, value);
- }
- public static LiteralExpr Literal(int value) {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return new LiteralExpr(Token.NoToken, BigNum.FromInt(value));
- }
- public static LiteralExpr Literal(BigNum value) {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return new LiteralExpr(Token.NoToken, value);
- }
- public static LiteralExpr Literal(BigDec value) {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return new LiteralExpr(Token.NoToken, value);
- }
- public static LiteralExpr Literal(BigFloat value)
- {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return new LiteralExpr(Token.NoToken, value);
- }
-
- private static LiteralExpr/*!*/ true_ = Literal(true);
- public static LiteralExpr/*!*/ True {
- get {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return true_;
- }
- }
-
- private static LiteralExpr/*!*/ false_ = Literal(false);
- public static LiteralExpr/*!*/ False {
- get {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return false_;
- }
- }
-
-
- public static NAryExpr Select(Expr map, params Expr[] args) {
- Contract.Requires(args != null);
- Contract.Requires(map != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return SelectTok(Token.NoToken, map, args);
- }
-
- public static NAryExpr Select(Expr map, List<Expr/*!*/>/*!*/ args) {
- Contract.Requires(map != null);
- Contract.Requires(cce.NonNullElements(args));
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Select(map, args.ToArray());
- }
-
- // use a different name for this variant of the method
- // (-> some bug prevents overloading in this case)
- public static NAryExpr SelectTok(IToken x, Expr map, params Expr[] args) {
- Contract.Requires(args != null);
- Contract.Requires(map != null);
- Contract.Requires(x != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- List<Expr>/*!*/ allArgs = new List<Expr>();
- allArgs.Add(map);
- foreach (Expr/*!*/ a in args) {
- Contract.Assert(a != null);
- allArgs.Add(a);
- }
- return new NAryExpr(x, new MapSelect(Token.NoToken, args.Length), allArgs);
- }
-
- public static NAryExpr Store(Expr map, params Expr[] args) {
- Contract.Requires(args != null);
- Contract.Requires(map != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return StoreTok(Token.NoToken, map, args);
- }
-
- public static NAryExpr Store(Expr map, List<Expr/*!*/>/*!*/ indexes, Expr rhs) {
- Contract.Requires(rhs != null);
- Contract.Requires(map != null);
- Contract.Requires(cce.NonNullElements(indexes));
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- Expr[]/*!*/ allArgs = new Expr[indexes.Count + 1];
- for (int i = 0; i < indexes.Count; ++i)
- allArgs[i] = indexes[i];
- allArgs[indexes.Count] = rhs;
- return Store(map, allArgs);
- }
-
- // use a different name for this variant of the method
- // (-> some bug prevents overloading in this case)
- public static NAryExpr/*!*/ StoreTok(IToken x, Expr map, params Expr[] args) {
- Contract.Requires(args != null);
- Contract.Requires(map != null);
- Contract.Requires(x != null);
- Contract.Requires(args.Length > 0); // zero or more indices, plus the value
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
-
- List<Expr>/*!*/ allArgs = new List<Expr>();
- allArgs.Add(map);
- foreach (Expr/*!*/ a in args) {
- Contract.Assert(a != null);
- allArgs.Add(a);
- }
- return new NAryExpr(x, new MapStore(Token.NoToken, args.Length - 1), allArgs);
- }
-
- public static NAryExpr CoerceType(IToken x, Expr subexpr, Type type) {
- Contract.Requires(type != null);
- Contract.Requires(subexpr != null);
- Contract.Requires(x != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- List<Expr>/*!*/ args = new List<Expr>();
- args.Add(subexpr);
- return new NAryExpr(x, new TypeCoercion(x, type), args);
- }
-
- public static Expr BinaryTreeAnd(List<Expr> terms)
- {
- return BinaryTreeAnd(terms, 0, terms.Count - 1);
- }
-
- private static Expr BinaryTreeAnd(List<Expr> terms, int start, int end)
- {
- if (start > end)
- return Expr.True;
- if (start == end)
- return terms[start];
- if (start + 1 == end)
- return Expr.And(terms[start], terms[start + 1]);
- var mid = (start + end) / 2;
- return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));
- }
- }
- [ContractClassFor(typeof(Expr))]
- public abstract class ExprContracts : Expr {
- public ExprContracts() :base(null, /*immutable=*/ false){
-
- }
- public override void Emit(TokenTextWriter wr, int contextBindingStrength, bool fragileContext) {
- Contract.Requires(wr != null);
- throw new NotImplementedException();
- }
- public override void ComputeFreeVariables(Set freeVars) {
- Contract.Requires(freeVars != null);
- throw new NotImplementedException();
- }
- public override Type ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- throw new NotImplementedException();
- }
- }
- }
-
- public class LiteralExpr : Expr {
- public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Val != null);
- }
-
- /// <summary>
- /// Creates a literal expression for the boolean value "b".
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="b"></param>
- public LiteralExpr(IToken/*!*/ tok, bool b, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Val = b;
- Type = Type.Bool;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- /// <summary>
- /// Creates a literal expression for the integer value "v".
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="v"></param>
- public LiteralExpr(IToken/*!*/ tok, BigNum v, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Val = v;
- Type = Type.Int;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- /// <summary>
- /// Creates a literal expression for the real value "v".
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="v"></param>
- public LiteralExpr(IToken/*!*/ tok, BigDec v, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Val = v;
- Type = Type.Real;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- /// <summary>
- /// Creates a literal expression for the floating point value "v".
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="v"></param>
- public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false)
- : base(tok, immutable)
- {
- Contract.Requires(tok != null);
- Val = v;
- Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- /// <summary>
- /// Creates a literal expression for the bitvector value "v".
- /// </summary>
- public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(0 <= b);
- Val = new BvConst(v, b);
- Type = Type.GetBvType(b);
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is LiteralExpr))
- return false;
-
- LiteralExpr other = (LiteralExpr)obj;
- return object.Equals(this.Val, other.Val);
- }
-
- [Pure]
- public override int GetHashCode() {
- if (Immutable)
- return this.CachedHashCode;
- else
- return ComputeHashCode();
- }
-
- [Pure]
- public override int ComputeHashCode() {
- return this.Val.GetHashCode();
- }
-
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- stream.SetToken(this);
- if (this.Val is bool) {
- stream.Write((bool)this.Val ? "true" : "false"); // correct capitalization
- } else {
- stream.Write(cce.NonNull(this.Val.ToString()));
- }
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- // nothing to resolve
- }
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- // no free variables to add
- }
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- this.Type = ShallowType;
- }
-
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- if (Val is bool) {
- return Type.Bool;
- } else if (Val is BigNum) {
- return Type.Int;
- } else if (Val is BigDec) {
- return Type.Real;
- } else if (Val is BigFloat) {
- BigFloat temp = (BigFloat)Val;
- return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);
- } else if (Val is BvConst) {
- return Type.GetBvType(((BvConst)Val).Bits);
- } else {
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } // like, where did this value come from?!
- }
- }
- }
-
- public bool IsFalse {
- get {
- return Val is bool && ((bool)Val) == false;
- }
- }
- public bool IsTrue {
- get {
- return Val is bool && ((bool)Val) == true;
- }
- }
-
- // should be eliminated after converting everything to BigNums
- private int asInt {
- get {
- return asBigNum.ToIntSafe;
- }
- }
-
- public bool isBigNum {
- get {
- return Val is BigNum;
- }
- }
-
- public BigNum asBigNum {
- get {
- Contract.Assert(isBigNum);
- return (BigNum)cce.NonNull(Val);
- }
- }
-
- public bool isBigDec {
- get {
- return Val is BigDec;
- }
- }
-
- public bool isBigFloat
- {
- get
- {
- return Val is BigFloat;
- }
- }
-
- public BigDec asBigDec {
- get {
- Contract.Assert(isBigDec);
- return (BigDec)cce.NonNull(Val);
- }
- }
-
- public BigFloat asBigFloat {
- get {
- Contract.Assert(isBigFloat);
- return (BigFloat)cce.NonNull(Val);
- }
- }
-
- public bool isBool {
- get {
- return Val is bool;
- }
- }
-
- public bool asBool {
- get {
- Contract.Assert(isBool);
- return (bool)cce.NonNull(Val);
- }
- }
-
- public bool isBvConst {
- get {
- return Val is BvConst;
- }
- }
-
- public BvConst asBvConst {
- get {
- Contract.Assert(isBvConst);
- return (BvConst)cce.NonNull(Val);
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitLiteralExpr(this);
- }
- }
-
- public class BvConst {
- public readonly BigNum Value;
- public readonly int Bits;
-
- public BvConst(BigNum v, int b) {
- Contract.Assert(v.Signum >= 0);
- Value = v;
- Bits = b;
- }
-
- [Pure]
- public override string ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return Value + "bv" + Bits;
- }
-
- [Pure]
- public string ToReadableString() {
- Contract.Ensures(Contract.Result<string>() != null);
- if (Value > BigNum.FromInt(10000)) {
- string val = cce.NonNull(Value.ToString("x"));
- int pos = val.Length % 4;
- string res = "0x" + val.Substring(0, pos);
- Contract.Assert(res != null);
- while (pos < val.Length) {
- res += "." + val.Substring(pos, 4);
- pos += 4;
- }
- return res + ".bv" + Bits;
- } else
- return ToString();
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- BvConst other = obj as BvConst;
- if (other == null)
- return false;
-
- return Bits == other.Bits && Value == other.Value;
- }
-
- [Pure]
- public override int GetHashCode() {
- unchecked {
- return Value.GetHashCode() ^ Bits;
- }
- }
- }
-
- public class IdentifierExpr : Expr {
- private string _Name;
- public string Name { // identifier symbol
- get {
- return _Name;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Cannot change Name on Immutable Expr");
-
- _Name = value;
- }
- }
- private Variable _Decl;
- public Variable Decl { // identifier declaration
- get {
- return _Decl;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Cannot change Decl on Immutable Expr");
-
- _Decl = value;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Name != null);
- }
-
-
- /// <summary>
- /// Creates an unresolved identifier expression. This constructor is intended to be called
- /// only from within the parser; for use inside the translation, use another constructor, which
- /// specifies the type of the expression.
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="name"></param>
- internal IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(name != null);
- _Name = name;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
- /// <summary>
- /// Creates an unresolved identifier expression.
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="name"></param>
- /// <param name="type"></param>
- public IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(name != null);
- Contract.Requires(type != null);
- _Name = name;
- Type = type;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- /// <summary>
- /// Creates a resolved identifier expression.
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="d"></param>
- public IdentifierExpr(IToken/*!*/ tok, Variable/*!*/ d, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(d != null);
- _Name = cce.NonNull(d.Name);
- _Decl = d;
- Type = d.TypedIdent.Type;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is IdentifierExpr))
- return false;
-
- IdentifierExpr other = (IdentifierExpr)obj;
- return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl);
- }
-
- [Pure]
- public override int GetHashCode() {
- if (Immutable)
- return this.CachedHashCode;
- else
- return ComputeHashCode();
- }
-
- [Pure]
- public override int ComputeHashCode() {
- int h = this.Name == null ? 0 : this.Name.GetHashCode();
- h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();
- return h;
- }
-
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- if (CommandLineOptions.Clo.PrintWithUniqueASTIds && !stream.UseForComputingChecksums) {
- stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode());
- }
- stream.Write(this, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- if (Decl != null) {
- // already resolved, but re-resolve type just in case it came from an unresolved type
- if (Type != null) {
- Type = Type.ResolveType(rc);
- }
- return;
- }
- Decl = rc.LookUpVariable(Name);
- if (Decl == null) {
- rc.Error(this, "undeclared identifier: {0}", Name);
- } else if (rc.StateMode == ResolutionContext.State.StateLess && Decl is GlobalVariable) {
- rc.Error(this, "cannot refer to a global variable in this context: {0}", Name);
- }
- if (Type != null) {
- Type = Type.ResolveType(rc);
- }
- }
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- Contract.Assume(this.Decl != null);
- freeVars.Add(Decl);
- }
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- if (this.Decl != null) {
- // sanity check
- if (Type != null && !Type.Equals(Decl.TypedIdent.Type)) {
- tc.Error(this, "internal error, shallow-type assignment was done incorrectly, {0}:{1} != {2}",
- Name, Type, Decl.TypedIdent.Type);
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
- Type = Decl.TypedIdent.Type;
- }
- }
-
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- Contract.Assert(Type != null);
- return Type;
- }
- }
-
- public sealed class ConstantFunApp {
- private IdentifierExpr/*!*/ identifierExpr;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(identifierExpr != null);
- Contract.Invariant(emptyArgs != null);
- }
-
- public IdentifierExpr/*!*/ IdentifierExpr {
- get {
- Contract.Requires(IdentifierExpr != null);
- return identifierExpr;
- }
- }
-
- private static IList/*!*/ emptyArgs = ArrayList.ReadOnly(cce.NonNull((IList/*!*/)new ArrayList()));
- public IList/*!*/ Arguments {
- get {
- Contract.Ensures(Contract.Result<IList>() != null);
- return emptyArgs;
- }
- }
-
- public ConstantFunApp(IdentifierExpr ie, Constant c) {
- Contract.Requires(c != null);
- Contract.Requires(ie != null);
- this.identifierExpr = ie;
- }
-
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitIdentifierExpr(this);
- }
- }
-
- public class OldExpr : Expr
- {
- private Expr _Expr;
- public Expr/*!*/ Expr {
- get {
- return _Expr;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Cannot change Expr of an Immutable OldExpr");
-
- _Expr = value;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Expr != null);
- }
-
- public OldExpr(IToken/*!*/ tok, Expr/*!*/ expr, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(expr != null);
- _Expr = expr;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is OldExpr))
- return false;
-
- OldExpr other = (OldExpr)obj;
- return object.Equals(this.Expr, other.Expr);
- }
- [Pure]
- public override int GetHashCode() {
- if (Immutable)
- return this.CachedHashCode;
- else
- return ComputeHashCode ();
- }
- public override int ComputeHashCode() {
- // FIXME: This is wrong, it's as if the OldExpr node isn't there at all
- return this.Expr == null ? 0 : this.Expr.GetHashCode();
- }
-
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- stream.Write(this, "old(");
- this.Expr.Emit(stream);
- stream.Write(")");
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- if (rc.StateMode != ResolutionContext.State.Two) {
- rc.Error(this, "old expressions allowed only in two-state contexts");
- }
- Expr.Resolve(rc);
- }
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- Expr.ComputeFreeVariables(freeVars);
- }
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- Expr.Typecheck(tc);
- Type = Expr.Type;
- }
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- return Expr.ShallowType;
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitOldExpr(this);
- }
- }
- [ContractClass(typeof(IAppliableVisitorContracts<>))]
- public interface IAppliableVisitor<T> {
- T Visit(UnaryOperator/*!*/ unaryOperator);
- T Visit(BinaryOperator/*!*/ binaryOperator);
- T Visit(FunctionCall/*!*/ functionCall);
- T Visit(MapSelect/*!*/ mapSelect);
- T Visit(MapStore/*!*/ mapStore);
- T Visit(TypeCoercion/*!*/ typeCoercion);
- T Visit(ArithmeticCoercion/*!*/ arithCoercion);
- T Visit(IfThenElse/*!*/ ifThenElse);
- }
- [ContractClassFor(typeof(IAppliableVisitor<>))]
- public abstract class IAppliableVisitorContracts<T> : IAppliableVisitor<T> {
-
- #region IAppliableVisitor<T> Members
-
- public T Visit(UnaryOperator unaryOperator) {
- Contract.Requires(unaryOperator != null);
- throw new NotImplementedException();
- }
-
- public T Visit(BinaryOperator binaryOperator) {
- Contract.Requires(binaryOperator != null);
- throw new NotImplementedException();
- }
-
- public T Visit(FunctionCall functionCall) {
- Contract.Requires(functionCall != null);
- throw new NotImplementedException();
- }
-
- public T Visit(MapSelect mapSelect) {
- Contract.Requires(mapSelect != null);
- throw new NotImplementedException();
- }
-
- public T Visit(MapStore mapStore) {
- Contract.Requires(mapStore != null);
- throw new NotImplementedException();
- }
-
- public T Visit(TypeCoercion typeCoercion) {
- Contract.Requires(typeCoercion != null);
- throw new NotImplementedException();
- }
-
- public T Visit(ArithmeticCoercion arithCoercion) {
- Contract.Requires(arithCoercion != null);
- throw new NotImplementedException();
- }
-
- public T Visit(IfThenElse ifThenElse) {
- Contract.Requires(ifThenElse != null);
- throw new NotImplementedException();
- }
-
- #endregion
- }
-
- [ContractClass(typeof(IAppliableContracts))]
- public interface IAppliable {
- string/*!*/ FunctionName {
- get;
- }
-
- /// <summary>
- /// Emits to "stream" the operator applied to the given arguments.
- /// The length of "args" can be anything that the parser allows for this appliable operator
- /// (but can be nothing else).
- /// </summary>
- /// <param name="args"></param>
- /// <param name="stream"></param>
- /// <param name="contextBindingStrength"></param>
- /// <param name="fragileContext"></param>
- void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext);
-
- void Resolve(ResolutionContext/*!*/ rc, Expr/*!*/ subjectForErrorReporting);
-
- /// <summary>
- /// Requires the object to have been properly resolved.
- /// </summary>
- int ArgumentCount {
- get;
- }
-
- /// <summary>
- /// Typechecks the arguments "args" for the Appliable. If the arguments are
- /// appropriate, returns the result type; otherwise returns null.
- /// As result of the type checking, the values of type parameters of the
- /// appliable can be returned (which are then stored in the NAryExpr and later
- /// also used in the VCExprAST).
- /// Requires the object to have been successfully resolved.
- /// Requires args.Length == ArgumentCount.
- /// Requires all elements of "args" to have a non-null Type field.
- /// </summary>
- /// <param name="args"></param>
- /// <param name="tc"></param>
- Type Typecheck(IList<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);
-
- // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null});
-
- /// <summary>
- /// Returns the result type of the IAppliable, supposing the argument are of the correct types.
- /// </summary>
- Type/*!*/ ShallowType(IList<Expr>/*!*/ args);
-
- T Dispatch<T>(IAppliableVisitor<T>/*!*/ visitor);
- }
- [ContractClassFor(typeof(IAppliable))]
- abstract class IAppliableContracts : IAppliable {
-
- #region IAppliable Members
-
- public string FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- throw new NotImplementedException();
- }
- }
-
- public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- Contract.Requires(args != null);
- Contract.Requires(stream != null);
- throw new NotImplementedException();
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- Contract.Requires(rc != null);
- Contract.Requires(subjectForErrorReporting != null);
- throw new NotImplementedException();
- }
-
- public int ArgumentCount {
- get {
- throw new NotImplementedException();
- }
- }
-
- public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- Contract.Requires(args != null);
- Contract.Requires(tc != null);
- Contract.Ensures(Contract.ValueAtReturn(out args) != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Ensures(args.Count == Contract.OldValue(args.Count));
- throw new NotImplementedException();
- }
-
- public Type ShallowType(IList<Expr> args) {
- Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
-
- throw new NotImplementedException();
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- Contract.Requires(visitor != null);
- throw new NotImplementedException();
- }
-
- #endregion
- }
-
-
- [ContractClass(typeof(IOverloadedAppliableContracts))]
- public interface IOverloadedAppliable {
- void ResolveOverloading(NAryExpr/*!*/ expr);
- bool DoNotResolveOverloading { get; set; }
- }
- [ContractClassFor(typeof(IOverloadedAppliable))]
- public abstract class IOverloadedAppliableContracts : IOverloadedAppliable {
-
- #region IOverloadedAppliable Members
-
- void IOverloadedAppliable.ResolveOverloading(NAryExpr expr) {
- Contract.Requires(expr != null);
- throw new NotImplementedException();
- }
-
- public bool DoNotResolveOverloading
- {
- get
- {
- throw new NotImplementedException();
- }
- set
- {
- throw new NotImplementedException();
- }
- }
-
- #endregion
- }
-
- public class UnaryOperator : IAppliable {
- private IToken/*!*/ tok;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(tok != null);
- }
-
- public enum Opcode {
- Neg,
- Not
- };
- private Opcode op;
- public Opcode Op {
- get {
- return op;
- }
- }
- public UnaryOperator(IToken tok, Opcode op) {
- Contract.Requires(tok != null);
- this.tok = tok;
- this.op = op;
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is UnaryOperator))
- return false;
-
- UnaryOperator other = (UnaryOperator)obj;
- return object.Equals(this.op, other.op);
- }
- [Pure]
- public override int GetHashCode() {
- return (int)this.op;
- }
-
- public string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
-
- switch (this.op) {
- case Opcode.Neg:
- return "-";
- case Opcode.Not:
- return "!";
- }
- System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
- throw new Exception();
- }
- }
-
- public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- //Contract.Requires(args != null);
- stream.SetToken(ref this.tok);
- Contract.Assert(args.Count == 1);
- // determine if parens are needed
- int opBindingStrength = 0x70;
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
-
- if (parensNeeded) {
- stream.Write("(");
- }
- stream.Write(FunctionName);
- cce.NonNull(args[0]).Emit(stream, opBindingStrength, false);
- if (parensNeeded) {
- stream.Write(")");
- }
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- if (rc.TriggerMode && this.op == Opcode.Not) {
- rc.Error(subjectForErrorReporting, "boolean operators are not allowed in triggers");
- }
- }
-
- public int ArgumentCount {
- get {
- return 1;
- }
- }
-
- public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Ensures(Contract.ValueAtReturn(out args) != null);
-
- Contract.Assume(args.Count == 1);
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type);
- switch (this.op) {
- case Opcode.Neg:
- if (arg0type.Unify(Type.Int)) {
- return Type.Int;
- }
- if (arg0type.Unify(Type.Real)) {
- return Type.Real;
- }
- //if (arg0type.Unify(Type.Float)) {
- //return Type.Float;
- //}
- goto BAD_TYPE;
- case Opcode.Not:
- if (arg0type.Unify(Type.Bool)) {
- return Type.Bool;
- }
- goto BAD_TYPE;
- }
- System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- BAD_TYPE:
- tc.Error(this.tok, "invalid argument type ({1}) to unary operator {0}",
- this.FunctionName, arg0type);
- return null;
- }
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- switch (this.op) {
- case Opcode.Neg:
- return cce.NonNull(cce.NonNull(args[0]).Type);
- case Opcode.Not:
- return Type.Bool;
- default: {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } // unexpected unary operator
- }
- }
-
- public object Evaluate(object argument) {
- if (argument == null) {
- return null;
- }
- switch (this.op) {
- case Opcode.Neg:
- if (argument is BigNum) {
- return -((BigNum)argument);
- }
- if (argument is BigDec) {
- return -((BigDec)argument);
- }
- if (argument is BigFloat) {
- return -((BigFloat)argument);
- }
- break;
- case Opcode.Not:
- if (argument is bool) {
- return !((bool)argument);
- }
- throw new System.InvalidOperationException("unary Not only applies to bool");
- }
- return null; // unreachable
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
- }
-
- public class BinaryOperator : IAppliable, IOverloadedAppliable {
- private IToken/*!*/ tok;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(tok != null);
- }
-
- public bool DoNotResolveOverloading { get; set; }
-
- public enum Opcode {
- Add,
- Sub,
- Mul,
- Div,
- Mod,
- RealDiv,
- FloatDiv,
- Pow,
- Eq,
- Neq,
- Gt,
- Ge,
- Lt,
- Le,
- And,
- Or,
- Imp,
- Iff,
- Subtype
- };
- private Opcode op;
- public Opcode Op {
- get {
- return op;
- }
- }
- public BinaryOperator(IToken tok, Opcode op) {
- Contract.Requires(tok != null);
- this.tok = tok;
- this.op = op;
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is BinaryOperator))
- return false;
-
- BinaryOperator other = (BinaryOperator)obj;
- return object.Equals(this.op, other.op);
- }
-
- [Pure]
- public override int GetHashCode() {
- return (int)this.op << 1;
- }
-
- public string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
-
- switch (this.op) {
- case Opcode.Add:
- return "+";
- case Opcode.Sub:
- return "-";
- case Opcode.Mul:
- return "*";
- case Opcode.Div:
- return "div";
- case Opcode.Mod:
- return "mod";
- case Opcode.RealDiv:
- return "/";
- case Opcode.Pow:
- return "**";
- case Opcode.Eq:
- return "==";
- case Opcode.Neq:
- return "!=";
- case Opcode.Gt:
- return ">";
- case Opcode.Ge:
- return ">=";
- case Opcode.Lt:
- return "<";
- case Opcode.Le:
- return "<=";
- case Opcode.And:
- return "&&";
- case Opcode.Or:
- return "||";
- case Opcode.Imp:
- return "==>";
- case Opcode.Iff:
- return "<==>";
- case Opcode.Subtype:
- return "<:";
- }
- System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
- throw new Exception();
- }
- }
-
- public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- //Contract.Requires(args != null);
- stream.SetToken(ref this.tok);
- Contract.Assert(args.Count == 2);
- // determine if parens are needed
- int opBindingStrength;
- bool fragileLeftContext = false; // false means "allow same binding power on left without parens"
- bool fragileRightContext = false; // false means "allow same binding power on right without parens"
- switch (this.op) {
- case Opcode.Add:
- opBindingStrength = 0x40;
- break;
- case Opcode.Sub:
- opBindingStrength = 0x40;
- fragileRightContext = true;
- break;
- case Opcode.Mul:
- opBindingStrength = 0x50;
- break;
- case Opcode.Div:
- opBindingStrength = 0x50;
- fragileRightContext = true;
- break;
- case Opcode.Mod:
- opBindingStrength = 0x50;
- fragileRightContext = true;
- break;
- case Opcode.RealDiv:
- opBindingStrength = 0x50;
- fragileRightContext = true;
- break;
- case Opcode.Pow:
- opBindingStrength = 0x60;
- fragileRightContext = true;
- break;
- case Opcode.Eq:
- case Opcode.Neq:
- case Opcode.Gt:
- case Opcode.Ge:
- case Opcode.Lt:
- case Opcode.Le:
- case Opcode.Subtype:
- opBindingStrength = 0x30;
- fragileLeftContext = fragileRightContext = true;
- break;
- case Opcode.And:
- opBindingStrength = 0x20;
- break;
- case Opcode.Or:
- opBindingStrength = 0x21;
- break;
- case Opcode.Imp:
- opBindingStrength = 0x10;
- fragileLeftContext = true;
- break;
- case Opcode.Iff:
- opBindingStrength = 0x00;
- break;
- default:
- System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
- opBindingStrength = -1; // to please compiler, which refuses to consider whether or not all enumeration cases have been considered!
- break;
- }
- int opBS = opBindingStrength & 0xF0;
- int ctxtBS = contextBindingStrength & 0xF0;
- bool parensNeeded = opBS < ctxtBS ||
- (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
-
- var pop = stream.push(FunctionName);
- if (parensNeeded) {
- stream.Write("(");
- }
- cce.NonNull(args[0]).Emit(stream, opBindingStrength, fragileLeftContext);
- stream.sep();
- stream.Write(" {0} ", FunctionName);
- cce.NonNull(args[1]).Emit(stream, opBindingStrength, fragileRightContext);
- if (parensNeeded) {
- stream.Write(")");
- }
- stream.pop(pop);
- }
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- if (rc.TriggerMode) {
- switch (this.op) {
- case Opcode.Add:
- case Opcode.Sub:
- case Opcode.Mul:
- case Opcode.Div:
- case Opcode.Mod:
- case Opcode.RealDiv:
- case Opcode.Pow:
- case Opcode.Neq: // Neq is allowed, but not Eq
- case Opcode.Subtype:
- // These are fine
- break;
-
- case Opcode.Eq:
- rc.Error(subjectForErrorReporting, "equality is not allowed in triggers");
- break;
-
- case Opcode.Gt:
- case Opcode.Ge:
- case Opcode.Lt:
- case Opcode.Le:
- rc.Error(subjectForErrorReporting, "arithmetic comparisons are not allowed in triggers");
- break;
-
- case Opcode.And:
- case Opcode.Or:
- case Opcode.Imp:
- case Opcode.Iff:
- rc.Error(subjectForErrorReporting, "boolean operators are not allowed in triggers");
- break;
-
- default:
- System.Diagnostics.Debug.Fail("unknown binary operator: " + this.op.ToString());
- break;
- }
- }
- }
- public int ArgumentCount {
- get {
- return 2;
- }
- }
- public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Ensures(args != null);
- Contract.Assert(args.Count == 2);
- // the default; the only binary operator with a type parameter is equality, but right
- // we don't store this parameter because it does not appear necessary
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- Expr arg0 = cce.NonNull(args[0]);
- Expr arg1 = cce.NonNull(args[1]);
- Type arg0type = cce.NonNull(arg0.Type);
- Type arg1type = cce.NonNull(arg1.Type);
- switch (this.op) {
- case Opcode.Add:
- case Opcode.Sub:
- case Opcode.Mul:
- if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
- return Type.Int;
- }
- if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
- return Type.Real;
- }
- if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
- return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
- }
- if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
- return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
- }
- goto BAD_TYPE;
- case Opcode.Div:
- case Opcode.Mod:
- if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
- return Type.Int;
- }
- goto BAD_TYPE;
- case Opcode.RealDiv:
- if ((arg0type.Unify(Type.Int) || arg0type.Unify(Type.Real)) &&
- (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) {
- return Type.Real;
- }
- if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
- return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
- }
- if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
- return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
- }
- goto BAD_TYPE;
- case Opcode.Pow:
- if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
- return Type.Real;
- }
- goto BAD_TYPE;
- case Opcode.Eq:
- case Opcode.Neq:
- // Comparison is allowed if the argument types are unifiable
- // (i.e., if there is any chance that the values of the arguments are
- // in the same domain)
- if (arg0type.Equals(arg1type)) {
- // quick path
- return Type.Bool;
- }
- List<TypeVariable>/*!*/ unifiable = new List<TypeVariable>();
- unifiable.AddRange(arg0type.FreeVariables);
- unifiable.AddRange(arg1type.FreeVariables);
-
- if (arg0type.Unify(arg1type, unifiable, new Dictionary<TypeVariable/*!*/, Type/*!*/>()))
- return Type.Bool;
- goto BAD_TYPE;
- case Opcode.Gt:
- case Opcode.Ge:
- case Opcode.Lt:
- case Opcode.Le:
- if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
- return Type.Bool;
- }
- if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
- return Type.Bool;
- }
- if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) {
- return Type.Bool;
- }
- goto BAD_TYPE;
- case Opcode.And:
- case Opcode.Or:
- case Opcode.Imp:
- case Opcode.Iff:
- if (arg0type.Unify(Type.Bool) && arg1type.Unify(Type.Bool)) {
- return Type.Bool;
- }
- goto BAD_TYPE;
- case Opcode.Subtype:
- // Subtype is polymorphically typed and can compare things of
- // arbitrary types (but both arguments must have the same type)
- if (arg0type.Unify(arg1type)) {
- return Type.Bool;
- }
- goto BAD_TYPE;
- }
- System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- BAD_TYPE:
- tc.Error(this.tok, "invalid argument types ({1} and {2}) to binary operator {0}", this.FunctionName, arg0type, arg1type);
- return null;
- }
-
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- switch (this.op) {
- case Opcode.Add:
- case Opcode.Sub:
- case Opcode.Mul:
- return cce.NonNull(args[0]).ShallowType;
-
- case Opcode.Div:
- case Opcode.Mod:
- return Type.Int;
-
- case Opcode.RealDiv:
- case Opcode.Pow:
- return Type.Real;
-
- case Opcode.Eq:
- case Opcode.Neq:
- case Opcode.Gt:
- case Opcode.Ge:
- case Opcode.Lt:
- case Opcode.Le:
- case Opcode.And:
- case Opcode.Or:
- case Opcode.Imp:
- case Opcode.Iff:
- case Opcode.Subtype:
- return Type.Bool;
-
- default: {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } // unexpected binary operator
- }
- }
-
- public void ResolveOverloading(NAryExpr expr) {
- //Contract.Requires(expr != null);
-
- // immutable Expr must not be modified
- if (DoNotResolveOverloading || expr.Immutable)
- {
- return;
- }
-
- Expr arg0 = cce.NonNull(expr.Args[0]);
- Expr arg1 = cce.NonNull(expr.Args[1]);
- switch (op) {
- case Opcode.Eq:
- if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) {
- expr.Fun = new BinaryOperator(tok, Opcode.Iff);
- }
- break;
- case Opcode.Neq:
- if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) {
- expr.Fun = new BinaryOperator(tok, Opcode.Iff);
- var arg1New = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new List<Expr> { arg1 });
-
- // ugly ... there should be some more general approach,
- // e.g., to typecheck the whole expression again
- arg1New.Type = Type.Bool;
- arg1New.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
-
- expr.Args[1] = arg1New;
- }
- break;
- }
- }
-
- public object Evaluate(object e1, object e2) {
- if (e1 == null || e2 == null) {
- return null;
- }
-
- switch (this.op) {
- case Opcode.Add:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) + ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) + ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) + ((BigFloat)e2);
- }
- break;
- case Opcode.Sub:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) - ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) - ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) - ((BigFloat)e2);
- }
- break;
- case Opcode.Mul:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) * ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) * ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) * ((BigFloat)e2);
- }
- break;
- case Opcode.Div:
- if (e1 is BigNum && e2 is BigNum) {
- return /* TODO: right semantics? */ ((BigNum)e1) / ((BigNum)e2);
- }
- break;
- case Opcode.Mod:
- if (e1 is BigNum && e2 is BigNum) {
- return /* TODO: right semantics? */ ((BigNum)e1) % ((BigNum)e2);
- }
- break;
- case Opcode.RealDiv:
- // TODO: add partial evaluation fro real division
- break;
- case Opcode.FloatDiv:
- //TODO: add float division
- break;
- case Opcode.Pow:
- // TODO: add partial evaluation fro real exponentiation
- break;
- case Opcode.Lt:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) < ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) < ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) < ((BigFloat)e2);
- }
- break;
- case Opcode.Le:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) <= ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) <= ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) <= ((BigFloat)e2);
- }
- break;
- case Opcode.Gt:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) > ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) > ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) > ((BigFloat)e2);
- }
- break;
- case Opcode.Ge:
- if (e1 is BigNum && e2 is BigNum) {
- return ((BigNum)e1) >= ((BigNum)e2);
- }
- if (e1 is BigDec && e2 is BigDec) {
- return ((BigDec)e1) >= ((BigDec)e2);
- }
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) >= ((BigFloat)e2);
- }
- break;
-
- case Opcode.And:
- if (e1 is bool && e2 is bool) {
- return (bool)e1 && (bool)e2;
- }
- break;
- case Opcode.Or:
- if (e1 is bool && e2 is bool) {
- return (bool)e1 || (bool)e2;
- }
- break;
- case Opcode.Imp:
- if (e1 is bool && e2 is bool) {
- return !(bool)e1 || (bool)e2;
- }
- break;
- case Opcode.Iff:
- if (e1 is bool && e2 is bool) {
- return e1 == e2;
- }
- break;
-
- case Opcode.Eq:
- return Equals(e1, e2);
- case Opcode.Neq:
- return !Equals(e1, e2);
-
- case Opcode.Subtype:
- throw new System.NotImplementedException();
- }
- throw new System.InvalidOperationException("bad types to binary operator " + this.op);
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
-
- }
-
- public class FunctionCall : IAppliable {
- private IdentifierExpr/*!*/ name;
- public Function Func;
- public FunctionCall(IdentifierExpr name) {
- Contract.Requires(name != null);
- this.name = name;
- }
- public FunctionCall(Function f) {
- Contract.Requires(f != null);
- this.Func = f;
- this.name = new IdentifierExpr(Token.NoToken, f.Name);
-
- // We need set the type of this IdentifierExpr so ShallowType() works
- Debug.Assert(f.OutParams.Count > 0);
- this.name.Type = f.OutParams[0].TypedIdent.Type;
- }
- public string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
- return this.name.Name;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(name != null);
- }
-
- public FunctionCall createUnresolvedCopy()
- {
- return new FunctionCall(new IdentifierExpr(name.tok, name.Name, name.Type));
- }
-
- [Pure]
- public override string ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return name.Name;
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object other) {
- FunctionCall fc = other as FunctionCall;
- return fc != null && this.Func == fc.Func;
- }
- [Pure]
- public override int GetHashCode() {
- Contract.Assume(this.Func != null);
- return Func.GetHashCode();
- }
-
- virtual public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- //Contract.Requires(args != null);
- this.name.Emit(stream, 0xF0, false);
- if (stream.UseForComputingChecksums)
- {
- var c = Func.DependencyChecksum;
- if (c != null)
- {
- stream.Write(string.Format("[dependency_checksum:{0}]", c));
- }
- }
- stream.Write("(");
- args.Emit(stream);
- stream.Write(")");
- }
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- if (Func != null) {
- // already resolved
- return;
- }
- Func = rc.LookUpProcedure(name.Name) as Function;
- if (Func == null) {
- rc.Error(this.name, "use of undeclared function: {0}", name.Name);
- }
- else if (name.Type == null) {
- // We need set the type of this IdentifierExpr so ShallowType() works
- Debug.Assert(name.Type == null);
- Debug.Assert(Func.OutParams.Count > 0);
- name.Type = Func.OutParams[0].TypedIdent.Type;
- }
- }
- public virtual int ArgumentCount {
- get {
- Contract.Assume(Func != null); // ArgumentCount requires object to be properly resolved.
- return Func.InParams.Count;
- }
- }
- public virtual Type Typecheck(IList<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- //Contract.Requires(actuals != null);
- Contract.Ensures(Contract.ValueAtReturn(out actuals) != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assume(this.Func != null);
- Contract.Assume(actuals.Count == Func.InParams.Count);
- Contract.Assume(Func.OutParams.Count == 1);
-
- List<Type/*!*/>/*!*/ resultingTypeArgs;
- List<Type> actualResultType =
- Type.CheckArgumentTypes(Func.TypeParameters,
- out resultingTypeArgs,
- new List<Type>(Func.InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
- actuals,
- new List<Type>(Func.OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),
- null,
- // we need some token to report a possibly wrong number of
- // arguments
- actuals.Count > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken,
- "application of " + name.Name,
- tc);
-
- if (actualResultType == null) {
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- return null;
- } else {
- Contract.Assert(actualResultType.Count == 1);
- tpInstantiation =
- SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs);
- return actualResultType[0];
- }
- }
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- Contract.Assume(name.Type != null);
- return name.Type;
- }
-
- public virtual T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
- }
-
- public class TypeCoercion : IAppliable {
- private IToken/*!*/ tok;
- public Type/*!*/ Type;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(tok != null);
- }
-
- public TypeCoercion(IToken tok, Type type) {
- Contract.Requires(type != null);
- Contract.Requires(tok != null);
- this.tok = tok;
- this.Type = type;
- }
-
- public override bool Equals(object obj) {
- TypeCoercion other = obj as TypeCoercion;
- if (other == null) {
- return false;
- } else {
- return object.Equals(Type, other.Type);
- }
- }
-
-
-
- public
- string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
-
- return ":";
- }
- }
-
- public void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,
- int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(args != null);
- //Contract.Requires(stream != null);
- stream.SetToken(ref this.tok);
- Contract.Assert(args.Count == 1);
- // determine if parens are needed
- int opBindingStrength = 0x80;
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
-
- if (parensNeeded)
- stream.Write("(");
-
- cce.NonNull(args[0]).Emit(stream, opBindingStrength, false);
- stream.Write("{0} ", FunctionName);
- Type.Emit(stream, 0);
-
- if (parensNeeded)
- stream.Write(")");
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- this.Type = this.Type.ResolveType(rc);
- }
-
- public int ArgumentCount {
- get {
- return 1;
- }
- }
-
- public Type Typecheck(IList<Expr>/*!*/ args,
- out TypeParamInstantiation/*!*/ tpInstantiation,
- TypecheckingContext/*!*/ tc) {
- //Contract.Requires(args != null);
- //Contract.Requires(tc != null);
- Contract.Ensures(args != null);
-
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
-
- Contract.Assume(args.Count == 1);
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
-
- if (!this.Type.Unify(cce.NonNull(cce.NonNull(args[0]).Type)))
- tc.Error(this.tok, "{0} cannot be coerced to {1}",
- cce.NonNull(args[0]).Type, this.Type);
- return this.Type;
- }
-
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- return this.Type;
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
-
- }
-
- public class ArithmeticCoercion : IAppliable {
- public enum CoercionType {
- ToInt,
- ToReal,
- ToFloat
- }
-
- private IToken/*!*/ tok;
- public readonly CoercionType Coercion;
- private readonly string name;
- private readonly Type type;
- private readonly Type argType;
- private readonly Type argType2;
- private readonly int hashCode;
-
- public ArithmeticCoercion(IToken tok, CoercionType coercion) {
- this.tok = tok;
- this.Coercion = coercion;
-
- switch (coercion) {
- case CoercionType.ToInt:
- this.name = "int";
- this.type = Type.Int;
- this.argType = Type.Real;
- this.hashCode = 1;
- break;
- case CoercionType.ToReal:
- this.name = "real";
- this.type = Type.Real;
- this.argType = Type.Int;
- this.hashCode = 2;
- break;
- default:
- Contract.Assert(false);
- break;
- }
- }
-
- [Pure]
- public override string ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return this.name;
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object other) {
- ArithmeticCoercion ac = other as ArithmeticCoercion;
- return ac != null && this.Coercion == ac.Coercion;
- }
-
- [Pure]
- public override int GetHashCode() {
- return this.hashCode;
- }
-
- public string/*!*/ FunctionName {
- get {
- return this.name;
- }
- }
-
- public int ArgumentCount {
- get {
- return 1;
- }
- }
-
- virtual public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- //Contract.Requires(args != null);
- stream.Write(this.name);
- stream.Write("(");
- args.Emit(stream);
- stream.Write(")");
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- }
-
- public virtual Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- //Contract.Requires(args != null);
- Contract.Ensures(args != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
-
- Contract.Assert(args.Count == 1);
-
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
-
- if (!(cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType) || cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType2)))
- {
- tc.Error(this.tok, "argument type {0} does not match expected type {1} or type {2}", cce.NonNull(args[0]).Type, this.argType, this.argType2);
- }
-
- return this.type;
- }
-
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- return this.type;
- }
-
- public virtual T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
- }
-
- public class NAryExpr : Expr {
- [Additive]
- [Peer]
- private IAppliable _Fun;
- public IAppliable/*!*/ Fun {
- get {
- return _Fun;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Cannot change Function used by Immutable NAryExpr");
-
- _Fun = value;
- }
- }
- private List<Expr> _Args;
- public IList<Expr> Args {
- get {
- if (Immutable)
- return _Args.AsReadOnly();
- else
- return _Args;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Cannot change Args of Immutable NAryExpr");
-
- _Args = value as List<Expr>;
- }
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Fun != null);
- Contract.Invariant(Args != null);
- }
-
-
- // The instantiation of type parameters that is determined during type checking.
- // Which type parameters are available depends on the IAppliable
- public TypeParamInstantiation TypeParameters = null;
-
- [Captured]
- public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, IList<Expr>/*!*/ args, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(fun != null);
- Contract.Requires(args != null);
- _Fun = fun;
- Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null));
- if (immutable) {
- // We need to make a new list because the client might be holding
- // references to the list that they gave us which could be used to
- // circumvent the immutability enforcement
- _Args = new List<Expr>(args);
- CachedHashCode = ComputeHashCode();
- } else {
- if (args is List<Expr>) {
- // Preserve NAryExpr's old behaviour, we take ownership of the List<Expr>.
- // We can only do this if the type matches
- _Args = args as List<Expr>;
- }
- else {
- // Otherwise we must make a copy
- _Args = new List<Expr> (args);
- }
- }
- }
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is NAryExpr))
- return false;
-
- NAryExpr other = (NAryExpr)obj;
- return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args);
- }
-
- [Pure]
- public override int GetHashCode() {
- if (Immutable)
- return this.CachedHashCode;
- else
- return ComputeHashCode();
- }
-
- [Pure]
- public override int ComputeHashCode() {
- int h = this.Fun.GetHashCode();
- // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references
- // We want structural equality
- foreach (var arg in Args) {
- h = (97*h) + arg.GetHashCode();
- }
- return h;
- }
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- stream.SetToken(this);
- Fun.Emit(Args, stream, contextBindingStrength, fragileContext);
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- Fun.Resolve(rc, this);
- foreach (Expr/*!*/ e in Args) {
- Contract.Assert(e != null);
- e.Resolve(rc);
- }
- }
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- foreach (Expr/*!*/ e in Args) {
- Contract.Assert(e != null);
- e.ComputeFreeVariables(freeVars);
- }
- // also add the free type variables
- if (TypeParameters != null) {
- foreach (TypeVariable/*!*/ var in TypeParameters.FormalTypeParams) {
- Contract.Assert(var != null);
- foreach (TypeVariable/*!*/ w in TypeParameters[var].FreeVariables) {
- Contract.Assert(w != null);
- freeVars.Add(w);
- }
- }
- }
- }
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- int prevErrorCount = tc.ErrorCount;
- foreach (Expr/*!*/ e in Args) {
- Contract.Assert(e != null);
- e.Typecheck(tc);
- }
- if (Fun.ArgumentCount != Args.Count) {
- tc.Error(this, "wrong number of arguments to function: {0} ({1} instead of {2})",
- Fun.FunctionName, Args.Count, Fun.ArgumentCount);
- } else if (tc.ErrorCount == prevErrorCount &&
- // if the type parameters are set, this node has already been
- // typechecked and does not need to be checked again
- TypeParameters == null) {
- TypeParamInstantiation tpInsts;
- Type = Fun.Typecheck(Args, out tpInsts, tc); // Make sure we pass Args so if this Expr is immutable it is protected
- TypeParameters = tpInsts;
- }
- IOverloadedAppliable oa = Fun as IOverloadedAppliable;
- if (oa != null) {
- oa.ResolveOverloading(this);
- }
- if (Type == null) {
- // set Type to some non-null value
- Type = new TypeProxy(this.tok, "type_checking_error");
- }
- }
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- return Fun.ShallowType(Args);
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitNAryExpr(this);
- }
- }
-
- public class MapSelect : IAppliable {
-
- public readonly int Arity;
- private readonly IToken/*!*/ tok;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(tok != null);
- }
-
-
- public MapSelect(IToken tok, int arity) {
- Contract.Requires(tok != null);
- this.tok = tok;
- this.Arity = arity;
- }
-
- public string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
-
- return "MapSelect";
- }
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (!(obj is MapSelect))
- return false;
-
- MapSelect other = (MapSelect)obj;
- return this.Arity == other.Arity;
- }
-
- [Pure]
- public override int GetHashCode() {
- return Arity.GetHashCode() * 2823;
- }
-
- public void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,
- int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(args != null);
- //Contract.Requires(stream != null);
- Contract.Assume(args.Count == Arity + 1);
- Emit(args, stream, contextBindingStrength, fragileContext, false);
- }
-
- public static void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,
- int contextBindingStrength, bool fragileContext,
- bool withRhs) {
- Contract.Requires(args != null);
- Contract.Requires(stream != null);
- const int opBindingStrength = 0x90;
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
-
- if (parensNeeded) {
- stream.Write("(");
- }
- cce.NonNull(args[0]).Emit(stream, opBindingStrength, false);
- stream.Write("[");
-
- string sep = "";
- int lastIndex = withRhs ? args.Count - 1 : args.Count;
- for (int i = 1; i < lastIndex; ++i) {
- stream.Write(sep);
- sep = ", ";
- cce.NonNull(args[i]).Emit(stream);
- }
-
- if (withRhs) {
- stream.Write(" := ");
- cce.NonNull(args.Last()).Emit(stream);
- }
-
- stream.Write("]");
- if (parensNeeded) {
- stream.Write(")");
- }
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- // PR: nothing?
- }
-
- public int ArgumentCount {
- get {
- return Arity + 1;
- }
- }
-
- // it is assumed that each of the arguments has already been typechecked
- public static Type Typecheck(Type/*!*/ mapType,
- // we just pass an Absy, because in
- // the AssignCmd maps can also be
- // represented by non-expressions
- Absy/*!*/ map,
- List<Expr>/*!*/ indexes,
- // the type parameters, in this context, are the parameters of the
- // potentially polymorphic map type. Because it might happen that
- // the whole map type is unknown and represented using a MapTypeProxy,
- // the instantiations given in the following out-parameter are subject
- // to change if further unifications are done.
- out TypeParamInstantiation/*!*/ tpInstantiation,
- TypecheckingContext/*!*/ tc,
- IToken/*!*/ typeCheckingSubject,
- string/*!*/ opName) {
- Contract.Requires(mapType != null);
- Contract.Requires(map != null);
- Contract.Requires(indexes != null);
- Contract.Requires(tc != null);
- Contract.Requires(typeCheckingSubject != null);
- Contract.Requires(opName != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
-
- mapType = mapType.Expanded;
- if (mapType.IsMap && mapType.MapArity != indexes.Count) {
- tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1} instead of {2}",
- opName, indexes.Count, mapType.MapArity);
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- return null;
- } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Count))) {
- tc.Error(map.tok, "{0} applied to a non-map: {1}", opName, map);
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- return null;
- }
- mapType = TypeProxy.FollowProxy(mapType);
-
- if (mapType is MapType) {
- MapType mt = (MapType)mapType;
- return mt.CheckArgumentTypes(indexes, out tpInstantiation,
- typeCheckingSubject, opName, tc);
- } else {
- MapTypeProxy mt = (MapTypeProxy)mapType;
- return mt.CheckArgumentTypes(indexes, out tpInstantiation,
- typeCheckingSubject, opName, tc);
- }
- }
-
- public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assume(args.Count == Arity + 1);
-
- // FIXME: Wny are we passing a copy?
- List<Expr> actualArgs = new List<Expr>();
- for (int i = 1; i < args.Count; ++i)
- actualArgs.Add(args[i]);
-
- return Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),
- actualArgs, out tpInstantiation, tc, this.tok, "map select");
- }
-
- /// <summary>
- /// Returns the result type of the IAppliable, supposing the argument are of the correct types.
- /// </summary>
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- Expr a0 = cce.NonNull(args[0]);
- Type a0Type = a0.ShallowType;
- if (a0Type == null || !a0Type.IsMap) {
- // we are unable to determine the type of the select, so just return an arbitrary type
- return Type.Int;
- }
- MapType mapType = a0Type.AsMap;
- List<Type> actualArgTypes = new List<Type>();
- for (int i = 1; i < args.Count; ++i) {
- actualArgTypes.Add(cce.NonNull(args[i]).ShallowType);
- }
- return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes);
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
- }
-
- public class MapStore : IAppliable {
-
- public readonly int Arity;
- public readonly IToken/*!*/ tok;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(tok != null);
- }
-
-
- public MapStore(IToken tok, int arity) {
- Contract.Requires(tok != null);
- this.tok = tok;
- this.Arity = arity;
- }
-
- public string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
-
- return "MapStore";
- }
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (!(obj is MapStore))
- return false;
-
- MapStore other = (MapStore)obj;
- return this.Arity == other.Arity;
- }
-
- [Pure]
- public override int GetHashCode() {
- return Arity.GetHashCode() * 28231;
- }
-
- public void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream,
- int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(args != null);
- //Contract.Requires(stream != null);
- Contract.Assert(args.Count == Arity + 2);
- MapSelect.Emit(args, stream, contextBindingStrength, fragileContext, true);
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- // PR: nothing?
- }
-
- public int ArgumentCount {
- get {
- return Arity + 2;
- }
- }
-
- // it is assumed that each of the arguments has already been typechecked
- public static Type Typecheck(IList<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation,
- TypecheckingContext/*!*/ tc,
- IToken/*!*/ typeCheckingSubject,
- string/*!*/ opName) {
- Contract.Requires(args != null);
- Contract.Requires(tc != null);
- Contract.Requires(typeCheckingSubject != null);
- Contract.Requires(opName != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
-
- // part of the type checking works exactly as for MapSelect
- List<Expr> selectArgs = new List<Expr>();
- for (int i = 1; i < args.Count - 1; ++i)
- selectArgs.Add(args[i]);
- Type resultType =
- MapSelect.Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),
- selectArgs, out tpInstantiation, tc, typeCheckingSubject, opName);
-
- // check the the rhs has the right type
- if (resultType == null) {
- // error messages have already been created by MapSelect.Typecheck
- return null;
- }
- Type rhsType = cce.NonNull(cce.NonNull(args.Last()).Type);
- if (!resultType.Unify(rhsType)) {
- tc.Error(cce.NonNull(args.Last()).tok,
- "right-hand side in {0} with wrong type: {1} (expected: {2})",
- opName, rhsType, resultType);
- return null;
- }
-
- return cce.NonNull(args[0]).Type;
- }
-
- public Type Typecheck(IList<Expr>/*!*/ args,
- out TypeParamInstantiation/*!*/ tpInstantiation,
- TypecheckingContext/*!*/ tc) {
- //Contract.Requires(args != null);
- //Contract.Requires(tc != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Ensures(Contract.ValueAtReturn(out args) != null);
- Contract.Assert(args.Count == Arity + 2);
- return Typecheck(args, out tpInstantiation, tc, this.tok, "map store");
- }
-
- /// <summary>
- /// Returns the result type of the IAppliable, supposing the argument are of the correct types.
- /// </summary>
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- return cce.NonNull(args[0]).ShallowType;
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
- }
-
-
- public class IfThenElse : IAppliable {
-
- private IToken/*!*/ _tok;
-
- public IToken/*!*/ tok
- {
- get
- {
- Contract.Ensures(Contract.Result<IToken>() != null);
- return this._tok;
- }
- set
- {
- Contract.Requires(value != null);
- this._tok = value;
- }
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(this._tok != null);
- }
-
- public IfThenElse(IToken tok) {
- Contract.Requires(tok != null);
- this._tok = tok;
- }
-
- public string/*!*/ FunctionName {
- get {
- Contract.Ensures(Contract.Result<string>() != null);
-
- return "if-then-else";
- }
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (!(obj is IfThenElse))
- return false;
- return true;
- }
-
- [Pure]
- public override int GetHashCode() {
- return 1;
- }
-
- public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- //Contract.Requires(args != null);
- stream.SetToken(this);
- Contract.Assert(args.Count == 3);
- stream.push();
- stream.Write("(if ");
- cce.NonNull(args[0]).Emit(stream, 0x00, false);
- stream.sep();
- stream.Write(" then ");
- cce.NonNull(args[1]).Emit(stream, 0x00, false);
- stream.sep();
- stream.Write(" else ");
- cce.NonNull(args[2]).Emit(stream, 0x00, false);
- stream.Write(")");
- stream.pop();
- }
-
- public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
- //Contract.Requires(subjectForErrorReporting != null);
- //Contract.Requires(rc != null);
- // PR: nothing?
- }
-
- public int ArgumentCount {
- get {
- return 3;
- }
- }
-
- public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- //Contract.Requires(args != null);
- Contract.Ensures(args != null);
- Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assert(args.Count == 3);
- // the default; the only binary operator with a type parameter is equality, but right
- // we don't store this parameter because it does not appear necessary
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- Expr arg0 = cce.NonNull(args[0]);
- Expr arg1 = cce.NonNull(args[1]);
- Expr arg2 = cce.NonNull(args[2]);
-
- if (!cce.NonNull(arg0.Type).Unify(Type.Bool)) {
- tc.Error(this.tok, "the first argument to if-then-else should be bool, not {0}", arg0.Type);
- } else if (!cce.NonNull(arg1.Type).Unify(cce.NonNull(arg2.Type))) {
- tc.Error(this.tok, "branches of if-then-else have incompatible types {0} and {1}", arg1.Type, arg2.Type);
- } else {
- return arg1.Type;
- }
-
- return null;
- }
-
- /// <summary>
- /// Returns the result type of the IAppliable, supposing the argument are of the correct types.
- /// </summary>
- public Type ShallowType(IList<Expr> args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Type>() != null);
- return cce.NonNull(args[1]).ShallowType;
- }
-
- public T Dispatch<T>(IAppliableVisitor<T> visitor) {
- //Contract.Requires(visitor != null);
- return visitor.Visit(this);
- }
- }
-
-
-
- public class CodeExpr : Expr {
- public List<Variable>/*!*/ LocVars;
- [Rep]
- public List<Block/*!*/>/*!*/ Blocks;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(LocVars != null);
- Contract.Invariant(cce.NonNullElements(Blocks));
- }
-
- public CodeExpr(List<Variable>/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks, bool immutable=false)
- : base(Token.NoToken, immutable) {
- Contract.Requires(localVariables != null);
- Contract.Requires(cce.NonNullElements(blocks));
- Contract.Requires(0 < blocks.Count);
- LocVars = localVariables;
- Blocks = blocks;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- // FIXME: This seems wrong we don't want reference equality, we want structural equality
- [Pure]
- public override bool Equals(object obj)
- {
- return base.Equals(obj);
- }
-
- [Pure]
- public override int GetHashCode()
- {
- if (Immutable)
- return CachedHashCode;
- else
- return ComputeHashCode();
- }
-
- [Pure]
- public override int ComputeHashCode() {
- return base.GetHashCode();
- }
-
-
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- // Treat a BlockEexpr as if it has no free variables at all
- }
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- //level++;
- int level = 0;
- stream.WriteLine(level, "|{");
-
- if (this.LocVars.Count > 0) {
- stream.Write(level + 1, "var ");
- this.LocVars.Emit(stream, true);
- stream.WriteLine(";");
- }
-
- foreach (Block/*!*/ b in this.Blocks) {
- Contract.Assert(b != null);
- b.Emit(stream, level + 1);
- }
-
- stream.WriteLine();
- stream.WriteLine(level, "}|");
-
- stream.WriteLine();
- stream.WriteLine();
- }
-
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
-
- rc.PushVarContext();
- foreach (Variable/*!*/ v in LocVars) {
- Contract.Assert(v != null);
- v.Register(rc);
- v.Resolve(rc);
- }
-
- rc.PushProcedureContext();
- foreach (Block/*!*/ b in Blocks) {
- Contract.Assert(b != null);
- b.Register(rc);
- }
-
- foreach (Block/*!*/ b in Blocks) {
- Contract.Assert(b != null);
- b.Resolve(rc);
- }
-
- rc.PopProcedureContext();
- rc.PopVarContext();
- }
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- foreach (Variable/*!*/ v in LocVars) {
- Contract.Assert(v != null);
- v.Typecheck(tc);
- }
- foreach (Block/*!*/ b in Blocks) {
- Contract.Assert(b != null);
- b.Typecheck(tc);
- }
- this.Type = Type.Bool;
- }
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- return Type.Bool;
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitCodeExpr(this);
- }
- }
-
- public class BvExtractExpr : Expr {
- private /*readonly--except in StandardVisitor*/ Expr/*!*/ _Bitvector;
- public Expr Bitvector {
- get {
- return _Bitvector;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Cannot change BitVector field of an immutable BvExtractExpr");
-
- _Bitvector = value;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(_Bitvector != null);
- }
-
- public readonly int Start, End;
-
- public BvExtractExpr(IToken/*!*/ tok, Expr/*!*/ bv, int end, int start, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(bv != null);
- _Bitvector = bv;
- Start = start;
- End = end;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is BvExtractExpr))
- return false;
-
- BvExtractExpr other = (BvExtractExpr)obj;
- return object.Equals(this.Bitvector, other.Bitvector) &&
- this.Start.Equals(other.Start) && this.End.Equals(other.End);
- }
-
- [Pure]
- public override int GetHashCode() {
- if (Immutable)
- return CachedHashCode;
- else
- return ComputeHashCode();
- }
-
- [Pure]
- public override int ComputeHashCode() {
- int h = this.Bitvector.GetHashCode();
- h ^= Start * 17 ^ End * 13;
- return h;
- }
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- stream.SetToken(this);
- int opBindingStrength = 0x90;
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
-
- if (parensNeeded) {
- stream.Write("(");
- }
- Bitvector.Emit(stream, opBindingStrength, false);
- stream.Write("[" + End + ":" + Start + "]");
- if (parensNeeded) {
- stream.Write(")");
- }
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- Bitvector.Resolve(rc);
- }
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- Bitvector.ComputeFreeVariables(freeVars);
- }
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- Bitvector.Typecheck(tc);
- Contract.Assert(Bitvector.Type != null); // follows from postcondition of Expr.Typecheck
-
- if (Start < 0) {
- tc.Error(this, "start index in extract must not be negative");
- } else if (End < 0) {
- tc.Error(this, "end index in extract must not be negative");
- } else if (End < Start) {
- tc.Error(this, "start index in extract must be no bigger than the end index");
- } else {
- Type typeConstraint = new BvTypeProxy(this.tok, "extract", End - Start);
- if (typeConstraint.Unify(Bitvector.Type)) {
- Type = Type.GetBvType(End - Start);
- } else {
- tc.Error(this, "extract operand must be a bitvector of at least {0} bits (got {1})", End - Start, Bitvector.Type);
- }
- }
- if (Type == null) {
- Type = new TypeProxy(this.tok, "type_checking_error");
- }
- }
-
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- return Type.GetBvType(End - Start);
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitBvExtractExpr(this);
- }
- }
-
- public class BvConcatExpr : Expr {
- private /*readonly--except in StandardVisitor*/ Expr/*!*/ _E0, _E1;
- public Expr E0 {
- get {
- return _E0;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Can't change E0 reference on immutable Expr");
-
- _E0 = value;
- }
- }
- public Expr E1 {
- get {
- return _E1;
- }
- set {
- if (Immutable)
- throw new InvalidOperationException("Can't change E1 reference on immutable Expr");
-
- _E1 = value;
- }
- }
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(E0 != null);
- Contract.Invariant(E1 != null);
- }
-
-
- public BvConcatExpr(IToken/*!*/ tok, Expr/*!*/ e0, Expr/*!*/ e1, bool immutable=false)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);
- _E0 = e0;
- _E1 = e1;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is BvConcatExpr))
- return false;
-
- BvConcatExpr other = (BvConcatExpr)obj;
- return object.Equals(this.E0, other.E0) && object.Equals(this.E1, other.E1);
- }
-
- [Pure]
- public override int GetHashCode()
- {
- if (Immutable)
- return CachedHashCode;
- else
- return ComputeHashCode();
- }
-
- [Pure]
- public override int ComputeHashCode() {
- int h = this.E0.GetHashCode() ^ this.E1.GetHashCode() * 17;
- return h;
- }
-
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- stream.SetToken(this);
- int opBindingStrength = 0x32;
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
-
- if (parensNeeded) {
- stream.Write("(");
- }
- E0.Emit(stream, opBindingStrength, false);
- stream.Write(" ++ ");
- // while this operator is associative, our incomplete axioms in int translation don't
- // make much use of it, so better stick to the actual tree shape
- E1.Emit(stream, opBindingStrength, true);
- if (parensNeeded) {
- stream.Write(")");
- }
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- E0.Resolve(rc);
- E1.Resolve(rc);
- }
- public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- //Contract.Requires(freeVars != null);
- E0.ComputeFreeVariables(freeVars);
- E1.ComputeFreeVariables(freeVars);
- }
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- E0.Typecheck(tc);
- Contract.Assert(E0.Type != null); // follows from postcondition of Expr.Typecheck
- E1.Typecheck(tc);
- Contract.Assert(E1.Type != null); // follows from postcondition of Expr.Typecheck
-
- if (E0.Type.Unify(new BvTypeProxy(this.tok, "concat0", 0)) && E1.Type.Unify(new BvTypeProxy(this.tok, "concat1", 0))) {
- Type = new BvTypeProxy(this.tok, "concat", E0.Type, E1.Type);
- } else {
- tc.Error(this, "++ operands need to be bitvectors (got {0}, {1})", E0.Type, E1.Type);
- }
- if (Type == null) {
- Type = new TypeProxy(this.tok, "type_checking_error");
- }
- }
-
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- Type t0 = E0.ShallowType;
- Type t1 = E1.ShallowType;
- int len0 = t0.IsBv ? t0.BvBits : /*expression is not type correct, so just pick an arbitrary number of bits*/0;
- int len1 = t1.IsBv ? t1.BvBits : /*expression is not type correct, so just pick an arbitrary number of bits*/0;
- return Type.GetBvType(len0 + len1);
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitBvConcatExpr(this);
- }
- }
-}
-
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +//--------------------------------------------------------------------------------------------- +// BoogiePL - Absy.cs +//--------------------------------------------------------------------------------------------- + +namespace Microsoft.Boogie { + using System; + using System.Collections; + using System.Diagnostics; + using System.Collections.Generic; + using Microsoft.Boogie.AbstractInterpretation; + using System.Diagnostics.Contracts; + using System.Linq; + using Microsoft.Basetypes; + + using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables + + + //--------------------------------------------------------------------- + // Expressions + // + // For expressions, we override the Equals and GetHashCode method to + // implement structural equality. Note this is not logical equivalence + // and is not modulo alpha-renaming. + //--------------------------------------------------------------------- + + + [ContractClass(typeof(ExprContracts))] + public abstract class Expr : Absy { + public Expr(IToken/*!*/ tok, bool immutable) + : base(tok) { + Contract.Requires(tok != null); + this.Immutable = immutable; + } + + public void Emit(TokenTextWriter stream) { + Contract.Requires(stream != null); + Emit(stream, 0, false); + } + + /// <summary> + /// If true the client is making a promise that this Expr will be + /// treated immutably (i.e. once constructed it is never changed). + /// This is currently not enforced but it should be! + /// + /// This allows the Expr's hash code to be cached making calls to + /// GetHashCode() very cheap. + /// </summary> + /// <value><c>true</c> if immutable; otherwise, <c>false</c>.</value> + public bool Immutable { + get; + private set; + } + + /// <summary> + /// Computes the hash code of this Expr skipping any cache. + /// + /// Sub classes should place their implementation of computing their hashcode + /// here (making sure to call GetHashCode() not ComputeHashCode() on Expr for performance reasons) + /// and have GetHashCode() use a cached result from ComputeHashCode() if the + /// Expr was constructed to be immutable. + /// </summary> + /// <returns>The hash code.</returns> + public abstract int ComputeHashCode(); + protected int CachedHashCode = 0; + + public abstract void Emit(TokenTextWriter/*!*/ wr, int contextBindingStrength, bool fragileContext); + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result<string>() != null); + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false, /*pretty=*/ false)) { + this.Emit(stream, 0, false); + } + return buffer.ToString(); + } + + /// <summary> + /// Add to "freeVars" the free variables in the expression. + /// </summary> + public abstract void ComputeFreeVariables(Set /*Variable*//*!*/ freeVars); + + /// <summary> + /// Filled in by the Typecheck method. A value of "null" means a succeeding + /// call to Typecheck has not taken place (that is, either Typecheck hasn't + /// been called or Typecheck encountered an error in the expression to be + /// typechecked). + /// </summary> + private Type _Type = null; + public Type Type { + get { + return _Type; + } + set { + if (_Type == null) { + // Expr has never been type checked so always allow this + _Type = value; + } else { + if (Immutable && !_Type.Equals(value)) + throw new InvalidOperationException("Cannot change the Type of an Immutable Expr"); + + // Once the Type has been set (i.e. no longer null) we never change the reference + // if this Expr is immutable, even if the Type is equivalent (i.e. _Type.Equals(newType)) + if (!Immutable) + _Type = value; + } + } + } + + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + Contract.Ensures(Type != null); + // This body is added only because C# insists on it. It should really be left out, as if TypeCheck still were abstract. + // The reason for mentioning the method here at all is to give TypeCheck a postcondition for all expressions. + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + /// <summary> + /// Returns the type of the expression, supposing that all its subexpressions are well typed. + /// </summary> + public abstract Type/*!*/ ShallowType { + get; + } + + // Handy syntactic sugar follows: + + public static NAryExpr Unary(IToken x, UnaryOperator.Opcode op, Expr e1) { + Contract.Requires(e1 != null); + Contract.Requires(x != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return new NAryExpr(x, new UnaryOperator(x, op), new List<Expr> { e1 }); + } + + public static NAryExpr Binary(IToken x, BinaryOperator.Opcode op, Expr e0, Expr e1) { + Contract.Requires(e1 != null); + Contract.Requires(e0 != null); + Contract.Requires(x != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return new NAryExpr(x, new BinaryOperator(x, op), new List<Expr> { e0, e1 }); + } + + public static NAryExpr Binary(BinaryOperator.Opcode op, Expr e0, Expr e1) { + Contract.Requires(e1 != null); + Contract.Requires(e0 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(Token.NoToken, op, e0, e1); + } + + public static NAryExpr Eq(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Eq, e1, e2); + } + public static NAryExpr Neq(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Neq, e1, e2); + } + public static NAryExpr Le(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Le, e1, e2); + } + public static NAryExpr Ge(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Ge, e1, e2); + } + public static NAryExpr Lt(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Lt, e1, e2); + } + public static NAryExpr Gt(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Gt, e1, e2); + } + public static Expr And(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<Expr>() != null); + if (e1 == true_) { + return e2; + } else if (e2 == true_) { + return e1; + } else if (e1 == false_ || e2 == false_) { + return false_; + } else { + var res = Binary(BinaryOperator.Opcode.And, e1, e2); + res.Type = Microsoft.Boogie.Type.Bool; + res.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + return res; + } + } + public static Expr Or(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<Expr>() != null); + if (e1 == false_) { + return e2; + } else if (e2 == false_) { + return e1; + } else if (e1 == true_ || e2 == true_) { + return true_; + } else { + return Binary(BinaryOperator.Opcode.Or, e1, e2); + } + } + public static Expr Not(Expr e1) { + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<Expr>() != null); + NAryExpr nary = e1 as NAryExpr; + + if (e1 == true_) { + return false_; + } else if (e1 == false_) { + return true_; + } else if (nary != null) { + if (nary.Fun is UnaryOperator) { + UnaryOperator op = (UnaryOperator)nary.Fun; + if (op.Op == UnaryOperator.Opcode.Not) { + return cce.NonNull(nary.Args[0]); + } + } else if (nary.Fun is BinaryOperator) { + BinaryOperator op = (BinaryOperator)nary.Fun; + Expr arg0 = cce.NonNull(nary.Args[0]); + Expr arg1 = cce.NonNull(nary.Args[1]); + if (op.Op == BinaryOperator.Opcode.Eq) { + return Neq(arg0, arg1); + } else if (op.Op == BinaryOperator.Opcode.Neq) { + return Eq(arg0, arg1); + } else if (op.Op == BinaryOperator.Opcode.Lt) { + return Le(arg1, arg0); + } else if (op.Op == BinaryOperator.Opcode.Le) { + return Lt(arg1, arg0); + } else if (op.Op == BinaryOperator.Opcode.Ge) { + return Gt(arg1, arg0); + } else if (op.Op == BinaryOperator.Opcode.Gt) { + return Ge(arg1, arg0); + } + } + } + + return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1); + } + + public static Expr Neg(Expr e1) { + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<Expr>() != null); + return Unary(Token.NoToken, UnaryOperator.Opcode.Neg, e1); + } + + public static NAryExpr Imp(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Imp, e1, e2); + } + public static NAryExpr Iff(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Iff, e1, e2); + } + public static NAryExpr Add(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Add, e1, e2); + } + public static NAryExpr Sub(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Sub, e1, e2); + } + public static NAryExpr Mul(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Mul, e1, e2); + } + public static NAryExpr Div(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Div, e1, e2); + } + public static NAryExpr Mod(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Mod, e1, e2); + } + public static NAryExpr RealDiv(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.RealDiv, e1, e2); + } + public static NAryExpr FloatDiv(Expr e1, Expr e2) + { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.FloatDiv, e1, e2); + } + public static NAryExpr Pow(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Pow, e1, e2); + } + public static NAryExpr Subtype(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.Subtype, e1, e2); + } + + public static IdentifierExpr Ident(string name, Type type) { + Contract.Requires(type != null); + Contract.Requires(name != null); + Contract.Ensures(Contract.Result<IdentifierExpr>() != null); + return new IdentifierExpr(Token.NoToken, name, type); + } + + public static IdentifierExpr Ident(Variable decl) { + Contract.Requires(decl != null); + Contract.Ensures(Contract.Result<IdentifierExpr>() != null); + IdentifierExpr result = new IdentifierExpr(Token.NoToken, decl); + return result; + } + + public static LiteralExpr Literal(bool value) { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return new LiteralExpr(Token.NoToken, value); + } + public static LiteralExpr Literal(int value) { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return new LiteralExpr(Token.NoToken, BigNum.FromInt(value)); + } + public static LiteralExpr Literal(BigNum value) { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return new LiteralExpr(Token.NoToken, value); + } + public static LiteralExpr Literal(BigDec value) { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return new LiteralExpr(Token.NoToken, value); + } + public static LiteralExpr Literal(BigFloat value) + { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return new LiteralExpr(Token.NoToken, value); + } + + private static LiteralExpr/*!*/ true_ = Literal(true); + public static LiteralExpr/*!*/ True { + get { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return true_; + } + } + + private static LiteralExpr/*!*/ false_ = Literal(false); + public static LiteralExpr/*!*/ False { + get { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return false_; + } + } + + + public static NAryExpr Select(Expr map, params Expr[] args) { + Contract.Requires(args != null); + Contract.Requires(map != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return SelectTok(Token.NoToken, map, args); + } + + public static NAryExpr Select(Expr map, List<Expr/*!*/>/*!*/ args) { + Contract.Requires(map != null); + Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Select(map, args.ToArray()); + } + + // use a different name for this variant of the method + // (-> some bug prevents overloading in this case) + public static NAryExpr SelectTok(IToken x, Expr map, params Expr[] args) { + Contract.Requires(args != null); + Contract.Requires(map != null); + Contract.Requires(x != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + List<Expr>/*!*/ allArgs = new List<Expr>(); + allArgs.Add(map); + foreach (Expr/*!*/ a in args) { + Contract.Assert(a != null); + allArgs.Add(a); + } + return new NAryExpr(x, new MapSelect(Token.NoToken, args.Length), allArgs); + } + + public static NAryExpr Store(Expr map, params Expr[] args) { + Contract.Requires(args != null); + Contract.Requires(map != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return StoreTok(Token.NoToken, map, args); + } + + public static NAryExpr Store(Expr map, List<Expr/*!*/>/*!*/ indexes, Expr rhs) { + Contract.Requires(rhs != null); + Contract.Requires(map != null); + Contract.Requires(cce.NonNullElements(indexes)); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + Expr[]/*!*/ allArgs = new Expr[indexes.Count + 1]; + for (int i = 0; i < indexes.Count; ++i) + allArgs[i] = indexes[i]; + allArgs[indexes.Count] = rhs; + return Store(map, allArgs); + } + + // use a different name for this variant of the method + // (-> some bug prevents overloading in this case) + public static NAryExpr/*!*/ StoreTok(IToken x, Expr map, params Expr[] args) { + Contract.Requires(args != null); + Contract.Requires(map != null); + Contract.Requires(x != null); + Contract.Requires(args.Length > 0); // zero or more indices, plus the value + Contract.Ensures(Contract.Result<NAryExpr>() != null); + + List<Expr>/*!*/ allArgs = new List<Expr>(); + allArgs.Add(map); + foreach (Expr/*!*/ a in args) { + Contract.Assert(a != null); + allArgs.Add(a); + } + return new NAryExpr(x, new MapStore(Token.NoToken, args.Length - 1), allArgs); + } + + public static NAryExpr CoerceType(IToken x, Expr subexpr, Type type) { + Contract.Requires(type != null); + Contract.Requires(subexpr != null); + Contract.Requires(x != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + List<Expr>/*!*/ args = new List<Expr>(); + args.Add(subexpr); + return new NAryExpr(x, new TypeCoercion(x, type), args); + } + + public static Expr BinaryTreeAnd(List<Expr> terms) + { + return BinaryTreeAnd(terms, 0, terms.Count - 1); + } + + private static Expr BinaryTreeAnd(List<Expr> terms, int start, int end) + { + if (start > end) + return Expr.True; + if (start == end) + return terms[start]; + if (start + 1 == end) + return Expr.And(terms[start], terms[start + 1]); + var mid = (start + end) / 2; + return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end)); + } + + public static Expr And(IEnumerable<Expr> conjuncts, bool returnNullIfEmpty = false) + { + Expr result = null; + foreach (var c in conjuncts) + { + if (result != null) + { + result = LiteralExpr.And(result, c); + result.Type = Type.Bool; + } + else + { + result = c; + result.Type = Type.Bool; + } + } + if (result == null && !returnNullIfEmpty) + { + result = Expr.True; + } + return result; + } + } + [ContractClassFor(typeof(Expr))] + public abstract class ExprContracts : Expr { + public ExprContracts() :base(null, /*immutable=*/ false){ + + } + public override void Emit(TokenTextWriter wr, int contextBindingStrength, bool fragileContext) { + Contract.Requires(wr != null); + throw new NotImplementedException(); + } + public override void ComputeFreeVariables(Set freeVars) { + Contract.Requires(freeVars != null); + throw new NotImplementedException(); + } + public override Type ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + throw new NotImplementedException(); + } + } + } + + public class LiteralExpr : Expr { + public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Val != null); + } + + /// <summary> + /// Creates a literal expression for the boolean value "b". + /// </summary> + /// <param name="tok"></param> + /// <param name="b"></param> + public LiteralExpr(IToken/*!*/ tok, bool b, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Val = b; + Type = Type.Bool; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + /// <summary> + /// Creates a literal expression for the integer value "v". + /// </summary> + /// <param name="tok"></param> + /// <param name="v"></param> + public LiteralExpr(IToken/*!*/ tok, BigNum v, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Val = v; + Type = Type.Int; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + /// <summary> + /// Creates a literal expression for the real value "v". + /// </summary> + /// <param name="tok"></param> + /// <param name="v"></param> + public LiteralExpr(IToken/*!*/ tok, BigDec v, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Val = v; + Type = Type.Real; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + /// <summary> + /// Creates a literal expression for the floating point value "v". + /// </summary> + /// <param name="tok"></param> + /// <param name="v"></param> + public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false) + : base(tok, immutable) + { + Contract.Requires(tok != null); + Val = v; + Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize); + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + /// <summary> + /// Creates a literal expression for the bitvector value "v". + /// </summary> + public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(0 <= b); + Val = new BvConst(v, b); + Type = Type.GetBvType(b); + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is LiteralExpr)) + return false; + + LiteralExpr other = (LiteralExpr)obj; + return object.Equals(this.Val, other.Val); + } + + [Pure] + public override int GetHashCode() { + if (Immutable) + return this.CachedHashCode; + else + return ComputeHashCode(); + } + + [Pure] + public override int ComputeHashCode() { + return this.Val.GetHashCode(); + } + + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + stream.SetToken(this); + if (this.Val is bool) { + stream.Write((bool)this.Val ? "true" : "false"); // correct capitalization + } else { + stream.Write(cce.NonNull(this.Val.ToString())); + } + } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + // nothing to resolve + } + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + // no free variables to add + } + + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + this.Type = ShallowType; + } + + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + if (Val is bool) { + return Type.Bool; + } else if (Val is BigNum) { + return Type.Int; + } else if (Val is BigDec) { + return Type.Real; + } else if (Val is BigFloat) { + BigFloat temp = (BigFloat)Val; + return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize); + } else if (Val is BvConst) { + return Type.GetBvType(((BvConst)Val).Bits); + } else { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // like, where did this value come from?! + } + } + } + + public bool IsFalse { + get { + return Val is bool && ((bool)Val) == false; + } + } + public bool IsTrue { + get { + return Val is bool && ((bool)Val) == true; + } + } + + // should be eliminated after converting everything to BigNums + private int asInt { + get { + return asBigNum.ToIntSafe; + } + } + + public bool isBigNum { + get { + return Val is BigNum; + } + } + + public BigNum asBigNum { + get { + Contract.Assert(isBigNum); + return (BigNum)cce.NonNull(Val); + } + } + + public bool isBigDec { + get { + return Val is BigDec; + } + } + + public bool isBigFloat + { + get + { + return Val is BigFloat; + } + } + + public BigDec asBigDec { + get { + Contract.Assert(isBigDec); + return (BigDec)cce.NonNull(Val); + } + } + + public BigFloat asBigFloat { + get { + Contract.Assert(isBigFloat); + return (BigFloat)cce.NonNull(Val); + } + } + + public bool isBool { + get { + return Val is bool; + } + } + + public bool asBool { + get { + Contract.Assert(isBool); + return (bool)cce.NonNull(Val); + } + } + + public bool isBvConst { + get { + return Val is BvConst; + } + } + + public BvConst asBvConst { + get { + Contract.Assert(isBvConst); + return (BvConst)cce.NonNull(Val); + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitLiteralExpr(this); + } + } + + public class BvConst { + public readonly BigNum Value; + public readonly int Bits; + + public BvConst(BigNum v, int b) { + Contract.Assert(v.Signum >= 0); + Value = v; + Bits = b; + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return Value + "bv" + Bits; + } + + [Pure] + public string ToReadableString() { + Contract.Ensures(Contract.Result<string>() != null); + if (Value > BigNum.FromInt(10000)) { + string val = cce.NonNull(Value.ToString("x")); + int pos = val.Length % 4; + string res = "0x" + val.Substring(0, pos); + Contract.Assert(res != null); + while (pos < val.Length) { + res += "." + val.Substring(pos, 4); + pos += 4; + } + return res + ".bv" + Bits; + } else + return ToString(); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + BvConst other = obj as BvConst; + if (other == null) + return false; + + return Bits == other.Bits && Value == other.Value; + } + + [Pure] + public override int GetHashCode() { + unchecked { + return Value.GetHashCode() ^ Bits; + } + } + } + + public class IdentifierExpr : Expr { + private string _Name; + public string Name { // identifier symbol + get { + return _Name; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change Name on Immutable Expr"); + + _Name = value; + } + } + private Variable _Decl; + public Variable Decl { // identifier declaration + get { + return _Decl; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change Decl on Immutable Expr"); + + _Decl = value; + } + } + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Name != null); + } + + + /// <summary> + /// Creates an unresolved identifier expression. This constructor is intended to be called + /// only from within the parser; for use inside the translation, use another constructor, which + /// specifies the type of the expression. + /// </summary> + /// <param name="tok"></param> + /// <param name="name"></param> + internal IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + _Name = name; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + /// <summary> + /// Creates an unresolved identifier expression. + /// </summary> + /// <param name="tok"></param> + /// <param name="name"></param> + /// <param name="type"></param> + public IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + _Name = name; + Type = type; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + /// <summary> + /// Creates a resolved identifier expression. + /// </summary> + /// <param name="tok"></param> + /// <param name="d"></param> + public IdentifierExpr(IToken/*!*/ tok, Variable/*!*/ d, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(d != null); + _Name = cce.NonNull(d.Name); + _Decl = d; + Type = d.TypedIdent.Type; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is IdentifierExpr)) + return false; + + IdentifierExpr other = (IdentifierExpr)obj; + return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl); + } + + [Pure] + public override int GetHashCode() { + if (Immutable) + return this.CachedHashCode; + else + return ComputeHashCode(); + } + + [Pure] + public override int ComputeHashCode() { + int h = this.Name == null ? 0 : this.Name.GetHashCode(); + h ^= this.Decl == null ? 0 : this.Decl.GetHashCode(); + return h; + } + + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + if (CommandLineOptions.Clo.PrintWithUniqueASTIds && !stream.UseForComputingChecksums) { + stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode()); + } + stream.Write(this, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); + } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + if (Decl != null) { + // already resolved, but re-resolve type just in case it came from an unresolved type + if (Type != null) { + Type = Type.ResolveType(rc); + } + return; + } + Decl = rc.LookUpVariable(Name); + if (Decl == null) { + rc.Error(this, "undeclared identifier: {0}", Name); + } else if (rc.StateMode == ResolutionContext.State.StateLess && Decl is GlobalVariable) { + rc.Error(this, "cannot refer to a global variable in this context: {0}", Name); + } + if (Type != null) { + Type = Type.ResolveType(rc); + } + } + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + Contract.Assume(this.Decl != null); + freeVars.Add(Decl); + } + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + if (this.Decl != null) { + // sanity check + if (Type != null && !Type.Equals(Decl.TypedIdent.Type)) { + tc.Error(this, "internal error, shallow-type assignment was done incorrectly, {0}:{1} != {2}", + Name, Type, Decl.TypedIdent.Type); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + Type = Decl.TypedIdent.Type; + } + } + + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + Contract.Assert(Type != null); + return Type; + } + } + + public sealed class ConstantFunApp { + private IdentifierExpr/*!*/ identifierExpr; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(identifierExpr != null); + Contract.Invariant(emptyArgs != null); + } + + public IdentifierExpr/*!*/ IdentifierExpr { + get { + Contract.Requires(IdentifierExpr != null); + return identifierExpr; + } + } + + private static IList/*!*/ emptyArgs = ArrayList.ReadOnly(cce.NonNull((IList/*!*/)new ArrayList())); + public IList/*!*/ Arguments { + get { + Contract.Ensures(Contract.Result<IList>() != null); + return emptyArgs; + } + } + + public ConstantFunApp(IdentifierExpr ie, Constant c) { + Contract.Requires(c != null); + Contract.Requires(ie != null); + this.identifierExpr = ie; + } + + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitIdentifierExpr(this); + } + } + + public class OldExpr : Expr + { + private Expr _Expr; + public Expr/*!*/ Expr { + get { + return _Expr; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change Expr of an Immutable OldExpr"); + + _Expr = value; + } + } + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Expr != null); + } + + public OldExpr(IToken/*!*/ tok, Expr/*!*/ expr, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(expr != null); + _Expr = expr; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is OldExpr)) + return false; + + OldExpr other = (OldExpr)obj; + return object.Equals(this.Expr, other.Expr); + } + [Pure] + public override int GetHashCode() { + if (Immutable) + return this.CachedHashCode; + else + return ComputeHashCode (); + } + public override int ComputeHashCode() { + // FIXME: This is wrong, it's as if the OldExpr node isn't there at all + return this.Expr == null ? 0 : this.Expr.GetHashCode(); + } + + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + stream.Write(this, "old("); + this.Expr.Emit(stream); + stream.Write(")"); + } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + if (rc.StateMode != ResolutionContext.State.Two) { + rc.Error(this, "old expressions allowed only in two-state contexts"); + } + Expr.Resolve(rc); + } + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + Expr.ComputeFreeVariables(freeVars); + } + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + Expr.Typecheck(tc); + Type = Expr.Type; + } + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + return Expr.ShallowType; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitOldExpr(this); + } + } + [ContractClass(typeof(IAppliableVisitorContracts<>))] + public interface IAppliableVisitor<T> { + T Visit(UnaryOperator/*!*/ unaryOperator); + T Visit(BinaryOperator/*!*/ binaryOperator); + T Visit(FunctionCall/*!*/ functionCall); + T Visit(MapSelect/*!*/ mapSelect); + T Visit(MapStore/*!*/ mapStore); + T Visit(TypeCoercion/*!*/ typeCoercion); + T Visit(ArithmeticCoercion/*!*/ arithCoercion); + T Visit(IfThenElse/*!*/ ifThenElse); + } + [ContractClassFor(typeof(IAppliableVisitor<>))] + public abstract class IAppliableVisitorContracts<T> : IAppliableVisitor<T> { + + #region IAppliableVisitor<T> Members + + public T Visit(UnaryOperator unaryOperator) { + Contract.Requires(unaryOperator != null); + throw new NotImplementedException(); + } + + public T Visit(BinaryOperator binaryOperator) { + Contract.Requires(binaryOperator != null); + throw new NotImplementedException(); + } + + public T Visit(FunctionCall functionCall) { + Contract.Requires(functionCall != null); + throw new NotImplementedException(); + } + + public T Visit(MapSelect mapSelect) { + Contract.Requires(mapSelect != null); + throw new NotImplementedException(); + } + + public T Visit(MapStore mapStore) { + Contract.Requires(mapStore != null); + throw new NotImplementedException(); + } + + public T Visit(TypeCoercion typeCoercion) { + Contract.Requires(typeCoercion != null); + throw new NotImplementedException(); + } + + public T Visit(ArithmeticCoercion arithCoercion) { + Contract.Requires(arithCoercion != null); + throw new NotImplementedException(); + } + + public T Visit(IfThenElse ifThenElse) { + Contract.Requires(ifThenElse != null); + throw new NotImplementedException(); + } + + #endregion + } + + [ContractClass(typeof(IAppliableContracts))] + public interface IAppliable { + string/*!*/ FunctionName { + get; + } + + /// <summary> + /// Emits to "stream" the operator applied to the given arguments. + /// The length of "args" can be anything that the parser allows for this appliable operator + /// (but can be nothing else). + /// </summary> + /// <param name="args"></param> + /// <param name="stream"></param> + /// <param name="contextBindingStrength"></param> + /// <param name="fragileContext"></param> + void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext); + + void Resolve(ResolutionContext/*!*/ rc, Expr/*!*/ subjectForErrorReporting); + + /// <summary> + /// Requires the object to have been properly resolved. + /// </summary> + int ArgumentCount { + get; + } + + /// <summary> + /// Typechecks the arguments "args" for the Appliable. If the arguments are + /// appropriate, returns the result type; otherwise returns null. + /// As result of the type checking, the values of type parameters of the + /// appliable can be returned (which are then stored in the NAryExpr and later + /// also used in the VCExprAST). + /// Requires the object to have been successfully resolved. + /// Requires args.Length == ArgumentCount. + /// Requires all elements of "args" to have a non-null Type field. + /// </summary> + /// <param name="args"></param> + /// <param name="tc"></param> + Type Typecheck(IList<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc); + + // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null}); + + /// <summary> + /// Returns the result type of the IAppliable, supposing the argument are of the correct types. + /// </summary> + Type/*!*/ ShallowType(IList<Expr>/*!*/ args); + + T Dispatch<T>(IAppliableVisitor<T>/*!*/ visitor); + } + [ContractClassFor(typeof(IAppliable))] + abstract class IAppliableContracts : IAppliable { + + #region IAppliable Members + + public string FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + throw new NotImplementedException(); + } + } + + public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + Contract.Requires(args != null); + Contract.Requires(stream != null); + throw new NotImplementedException(); + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + Contract.Requires(rc != null); + Contract.Requires(subjectForErrorReporting != null); + throw new NotImplementedException(); + } + + public int ArgumentCount { + get { + throw new NotImplementedException(); + } + } + + public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + Contract.Requires(args != null); + Contract.Requires(tc != null); + Contract.Ensures(Contract.ValueAtReturn(out args) != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Ensures(args.Count == Contract.OldValue(args.Count)); + throw new NotImplementedException(); + } + + public Type ShallowType(IList<Expr> args) { + Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + + throw new NotImplementedException(); + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + Contract.Requires(visitor != null); + throw new NotImplementedException(); + } + + #endregion + } + + + [ContractClass(typeof(IOverloadedAppliableContracts))] + public interface IOverloadedAppliable { + void ResolveOverloading(NAryExpr/*!*/ expr); + bool DoNotResolveOverloading { get; set; } + } + [ContractClassFor(typeof(IOverloadedAppliable))] + public abstract class IOverloadedAppliableContracts : IOverloadedAppliable { + + #region IOverloadedAppliable Members + + void IOverloadedAppliable.ResolveOverloading(NAryExpr expr) { + Contract.Requires(expr != null); + throw new NotImplementedException(); + } + + public bool DoNotResolveOverloading + { + get + { + throw new NotImplementedException(); + } + set + { + throw new NotImplementedException(); + } + } + + #endregion + } + + public class UnaryOperator : IAppliable { + private IToken/*!*/ tok; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + } + + public enum Opcode { + Neg, + Not + }; + private Opcode op; + public Opcode Op { + get { + return op; + } + } + public UnaryOperator(IToken tok, Opcode op) { + Contract.Requires(tok != null); + this.tok = tok; + this.op = op; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is UnaryOperator)) + return false; + + UnaryOperator other = (UnaryOperator)obj; + return object.Equals(this.op, other.op); + } + [Pure] + public override int GetHashCode() { + return (int)this.op; + } + + public string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + + switch (this.op) { + case Opcode.Neg: + return "-"; + case Opcode.Not: + return "!"; + } + System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString()); + throw new Exception(); + } + } + + public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //Contract.Requires(args != null); + stream.SetToken(ref this.tok); + Contract.Assert(args.Count == 1); + // determine if parens are needed + int opBindingStrength = 0x70; + bool parensNeeded = opBindingStrength < contextBindingStrength || + (fragileContext && opBindingStrength == contextBindingStrength); + + if (parensNeeded) { + stream.Write("("); + } + stream.Write(FunctionName); + cce.NonNull(args[0]).Emit(stream, opBindingStrength, false); + if (parensNeeded) { + stream.Write(")"); + } + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + if (rc.TriggerMode && this.op == Opcode.Not) { + rc.Error(subjectForErrorReporting, "boolean operators are not allowed in triggers"); + } + } + + public int ArgumentCount { + get { + return 1; + } + } + + public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(args != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Ensures(Contract.ValueAtReturn(out args) != null); + + Contract.Assume(args.Count == 1); + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type); + switch (this.op) { + case Opcode.Neg: + if (arg0type.Unify(Type.Int)) { + return Type.Int; + } + if (arg0type.Unify(Type.Real)) { + return Type.Real; + } + //if (arg0type.Unify(Type.Float)) { + //return Type.Float; + //} + goto BAD_TYPE; + case Opcode.Not: + if (arg0type.Unify(Type.Bool)) { + return Type.Bool; + } + goto BAD_TYPE; + } + System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString()); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + BAD_TYPE: + tc.Error(this.tok, "invalid argument type ({1}) to unary operator {0}", + this.FunctionName, arg0type); + return null; + } + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + switch (this.op) { + case Opcode.Neg: + return cce.NonNull(cce.NonNull(args[0]).Type); + case Opcode.Not: + return Type.Bool; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // unexpected unary operator + } + } + + public object Evaluate(object argument) { + if (argument == null) { + return null; + } + switch (this.op) { + case Opcode.Neg: + if (argument is BigNum) { + return -((BigNum)argument); + } + if (argument is BigDec) { + return -((BigDec)argument); + } + if (argument is BigFloat) { + return -((BigFloat)argument); + } + break; + case Opcode.Not: + if (argument is bool) { + return !((bool)argument); + } + throw new System.InvalidOperationException("unary Not only applies to bool"); + } + return null; // unreachable + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + + public class BinaryOperator : IAppliable, IOverloadedAppliable { + private IToken/*!*/ tok; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + } + + public bool DoNotResolveOverloading { get; set; } + + public enum Opcode { + Add, + Sub, + Mul, + Div, + Mod, + RealDiv, + FloatDiv, + Pow, + Eq, + Neq, + Gt, + Ge, + Lt, + Le, + And, + Or, + Imp, + Iff, + Subtype + }; + private Opcode op; + public Opcode Op { + get { + return op; + } + } + public BinaryOperator(IToken tok, Opcode op) { + Contract.Requires(tok != null); + this.tok = tok; + this.op = op; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BinaryOperator)) + return false; + + BinaryOperator other = (BinaryOperator)obj; + return object.Equals(this.op, other.op); + } + + [Pure] + public override int GetHashCode() { + return (int)this.op << 1; + } + + public string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + + switch (this.op) { + case Opcode.Add: + return "+"; + case Opcode.Sub: + return "-"; + case Opcode.Mul: + return "*"; + case Opcode.Div: + return "div"; + case Opcode.Mod: + return "mod"; + case Opcode.RealDiv: + return "/"; + case Opcode.Pow: + return "**"; + case Opcode.Eq: + return "=="; + case Opcode.Neq: + return "!="; + case Opcode.Gt: + return ">"; + case Opcode.Ge: + return ">="; + case Opcode.Lt: + return "<"; + case Opcode.Le: + return "<="; + case Opcode.And: + return "&&"; + case Opcode.Or: + return "||"; + case Opcode.Imp: + return "==>"; + case Opcode.Iff: + return "<==>"; + case Opcode.Subtype: + return "<:"; + } + System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString()); + throw new Exception(); + } + } + + public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //Contract.Requires(args != null); + stream.SetToken(ref this.tok); + Contract.Assert(args.Count == 2); + // determine if parens are needed + int opBindingStrength; + bool fragileLeftContext = false; // false means "allow same binding power on left without parens" + bool fragileRightContext = false; // false means "allow same binding power on right without parens" + switch (this.op) { + case Opcode.Add: + opBindingStrength = 0x40; + break; + case Opcode.Sub: + opBindingStrength = 0x40; + fragileRightContext = true; + break; + case Opcode.Mul: + opBindingStrength = 0x50; + break; + case Opcode.Div: + opBindingStrength = 0x50; + fragileRightContext = true; + break; + case Opcode.Mod: + opBindingStrength = 0x50; + fragileRightContext = true; + break; + case Opcode.RealDiv: + opBindingStrength = 0x50; + fragileRightContext = true; + break; + case Opcode.Pow: + opBindingStrength = 0x60; + fragileRightContext = true; + break; + case Opcode.Eq: + case Opcode.Neq: + case Opcode.Gt: + case Opcode.Ge: + case Opcode.Lt: + case Opcode.Le: + case Opcode.Subtype: + opBindingStrength = 0x30; + fragileLeftContext = fragileRightContext = true; + break; + case Opcode.And: + opBindingStrength = 0x20; + break; + case Opcode.Or: + opBindingStrength = 0x21; + break; + case Opcode.Imp: + opBindingStrength = 0x10; + fragileLeftContext = true; + break; + case Opcode.Iff: + opBindingStrength = 0x00; + break; + default: + System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString()); + opBindingStrength = -1; // to please compiler, which refuses to consider whether or not all enumeration cases have been considered! + break; + } + int opBS = opBindingStrength & 0xF0; + int ctxtBS = contextBindingStrength & 0xF0; + bool parensNeeded = opBS < ctxtBS || + (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext)); + + var pop = stream.push(FunctionName); + if (parensNeeded) { + stream.Write("("); + } + cce.NonNull(args[0]).Emit(stream, opBindingStrength, fragileLeftContext); + stream.sep(); + stream.Write(" {0} ", FunctionName); + cce.NonNull(args[1]).Emit(stream, opBindingStrength, fragileRightContext); + if (parensNeeded) { + stream.Write(")"); + } + stream.pop(pop); + } + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + if (rc.TriggerMode) { + switch (this.op) { + case Opcode.Add: + case Opcode.Sub: + case Opcode.Mul: + case Opcode.Div: + case Opcode.Mod: + case Opcode.RealDiv: + case Opcode.Pow: + case Opcode.Neq: // Neq is allowed, but not Eq + case Opcode.Subtype: + // These are fine + break; + + case Opcode.Eq: + rc.Error(subjectForErrorReporting, "equality is not allowed in triggers"); + break; + + case Opcode.Gt: + case Opcode.Ge: + case Opcode.Lt: + case Opcode.Le: + rc.Error(subjectForErrorReporting, "arithmetic comparisons are not allowed in triggers"); + break; + + case Opcode.And: + case Opcode.Or: + case Opcode.Imp: + case Opcode.Iff: + rc.Error(subjectForErrorReporting, "boolean operators are not allowed in triggers"); + break; + + default: + System.Diagnostics.Debug.Fail("unknown binary operator: " + this.op.ToString()); + break; + } + } + } + public int ArgumentCount { + get { + return 2; + } + } + public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(args != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Ensures(args != null); + Contract.Assert(args.Count == 2); + // the default; the only binary operator with a type parameter is equality, but right + // we don't store this parameter because it does not appear necessary + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + Expr arg0 = cce.NonNull(args[0]); + Expr arg1 = cce.NonNull(args[1]); + Type arg0type = cce.NonNull(arg0.Type); + Type arg1type = cce.NonNull(arg1.Type); + switch (this.op) { + case Opcode.Add: + case Opcode.Sub: + case Opcode.Mul: + if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) { + return Type.Int; + } + if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { + return Type.Real; + } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + } + goto BAD_TYPE; + case Opcode.Div: + case Opcode.Mod: + if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) { + return Type.Int; + } + goto BAD_TYPE; + case Opcode.RealDiv: + if ((arg0type.Unify(Type.Int) || arg0type.Unify(Type.Real)) && + (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) { + return Type.Real; + } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + } + goto BAD_TYPE; + case Opcode.Pow: + if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { + return Type.Real; + } + goto BAD_TYPE; + case Opcode.Eq: + case Opcode.Neq: + // Comparison is allowed if the argument types are unifiable + // (i.e., if there is any chance that the values of the arguments are + // in the same domain) + if (arg0type.Equals(arg1type)) { + // quick path + return Type.Bool; + } + List<TypeVariable>/*!*/ unifiable = new List<TypeVariable>(); + unifiable.AddRange(arg0type.FreeVariables); + unifiable.AddRange(arg1type.FreeVariables); + + if (arg0type.Unify(arg1type, unifiable, new Dictionary<TypeVariable/*!*/, Type/*!*/>())) + return Type.Bool; + goto BAD_TYPE; + case Opcode.Gt: + case Opcode.Ge: + case Opcode.Lt: + case Opcode.Le: + if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) { + return Type.Bool; + } + if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { + return Type.Bool; + } + if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) { + return Type.Bool; + } + goto BAD_TYPE; + case Opcode.And: + case Opcode.Or: + case Opcode.Imp: + case Opcode.Iff: + if (arg0type.Unify(Type.Bool) && arg1type.Unify(Type.Bool)) { + return Type.Bool; + } + goto BAD_TYPE; + case Opcode.Subtype: + // Subtype is polymorphically typed and can compare things of + // arbitrary types (but both arguments must have the same type) + if (arg0type.Unify(arg1type)) { + return Type.Bool; + } + goto BAD_TYPE; + } + System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString()); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + BAD_TYPE: + tc.Error(this.tok, "invalid argument types ({1} and {2}) to binary operator {0}", this.FunctionName, arg0type, arg1type); + return null; + } + + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + switch (this.op) { + case Opcode.Add: + case Opcode.Sub: + case Opcode.Mul: + return cce.NonNull(args[0]).ShallowType; + + case Opcode.Div: + case Opcode.Mod: + return Type.Int; + + case Opcode.RealDiv: + case Opcode.Pow: + return Type.Real; + + case Opcode.Eq: + case Opcode.Neq: + case Opcode.Gt: + case Opcode.Ge: + case Opcode.Lt: + case Opcode.Le: + case Opcode.And: + case Opcode.Or: + case Opcode.Imp: + case Opcode.Iff: + case Opcode.Subtype: + return Type.Bool; + + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // unexpected binary operator + } + } + + public void ResolveOverloading(NAryExpr expr) { + //Contract.Requires(expr != null); + + // immutable Expr must not be modified + if (DoNotResolveOverloading || expr.Immutable) + { + return; + } + + Expr arg0 = cce.NonNull(expr.Args[0]); + Expr arg1 = cce.NonNull(expr.Args[1]); + switch (op) { + case Opcode.Eq: + if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) { + expr.Fun = new BinaryOperator(tok, Opcode.Iff); + } + break; + case Opcode.Neq: + if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) { + expr.Fun = new BinaryOperator(tok, Opcode.Iff); + var arg1New = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new List<Expr> { arg1 }); + + // ugly ... there should be some more general approach, + // e.g., to typecheck the whole expression again + arg1New.Type = Type.Bool; + arg1New.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + + expr.Args[1] = arg1New; + } + break; + } + } + + public object Evaluate(object e1, object e2) { + if (e1 == null || e2 == null) { + return null; + } + + switch (this.op) { + case Opcode.Add: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) + ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) + ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) + ((BigFloat)e2); + } + break; + case Opcode.Sub: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) - ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) - ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) - ((BigFloat)e2); + } + break; + case Opcode.Mul: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) * ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) * ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) * ((BigFloat)e2); + } + break; + case Opcode.Div: + if (e1 is BigNum && e2 is BigNum) { + return /* TODO: right semantics? */ ((BigNum)e1) / ((BigNum)e2); + } + break; + case Opcode.Mod: + if (e1 is BigNum && e2 is BigNum) { + return /* TODO: right semantics? */ ((BigNum)e1) % ((BigNum)e2); + } + break; + case Opcode.RealDiv: + // TODO: add partial evaluation fro real division + break; + case Opcode.FloatDiv: + //TODO: add float division + break; + case Opcode.Pow: + // TODO: add partial evaluation fro real exponentiation + break; + case Opcode.Lt: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) < ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) < ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) < ((BigFloat)e2); + } + break; + case Opcode.Le: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) <= ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) <= ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) <= ((BigFloat)e2); + } + break; + case Opcode.Gt: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) > ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) > ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) > ((BigFloat)e2); + } + break; + case Opcode.Ge: + if (e1 is BigNum && e2 is BigNum) { + return ((BigNum)e1) >= ((BigNum)e2); + } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) >= ((BigDec)e2); + } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) >= ((BigFloat)e2); + } + break; + + case Opcode.And: + if (e1 is bool && e2 is bool) { + return (bool)e1 && (bool)e2; + } + break; + case Opcode.Or: + if (e1 is bool && e2 is bool) { + return (bool)e1 || (bool)e2; + } + break; + case Opcode.Imp: + if (e1 is bool && e2 is bool) { + return !(bool)e1 || (bool)e2; + } + break; + case Opcode.Iff: + if (e1 is bool && e2 is bool) { + return e1 == e2; + } + break; + + case Opcode.Eq: + return Equals(e1, e2); + case Opcode.Neq: + return !Equals(e1, e2); + + case Opcode.Subtype: + throw new System.NotImplementedException(); + } + throw new System.InvalidOperationException("bad types to binary operator " + this.op); + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + + } + + public class FunctionCall : IAppliable { + private IdentifierExpr/*!*/ name; + public Function Func; + public FunctionCall(IdentifierExpr name) { + Contract.Requires(name != null); + this.name = name; + } + public FunctionCall(Function f) { + Contract.Requires(f != null); + this.Func = f; + this.name = new IdentifierExpr(Token.NoToken, f.Name); + + // We need set the type of this IdentifierExpr so ShallowType() works + Debug.Assert(f.OutParams.Count > 0); + this.name.Type = f.OutParams[0].TypedIdent.Type; + } + public string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + return this.name.Name; + } + } + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(name != null); + } + + public FunctionCall createUnresolvedCopy() + { + return new FunctionCall(new IdentifierExpr(name.tok, name.Name, name.Type)); + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return name.Name; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) { + FunctionCall fc = other as FunctionCall; + return fc != null && this.Func == fc.Func; + } + [Pure] + public override int GetHashCode() { + Contract.Assume(this.Func != null); + return Func.GetHashCode(); + } + + virtual public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //Contract.Requires(args != null); + + if (stream.UseForComputingChecksums && Func.OriginalLambdaExprAsString != null) + { + stream.Write(Func.OriginalLambdaExprAsString); + } + else + { + this.name.Emit(stream, 0xF0, false); + } + if (stream.UseForComputingChecksums) + { + var c = Func.DependencyChecksum; + if (c != null) + { + stream.Write(string.Format("[dependency_checksum:{0}]", c)); + } + } + stream.Write("("); + args.Emit(stream); + stream.Write(")"); + } + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + if (Func != null) { + // already resolved + return; + } + Func = rc.LookUpProcedure(name.Name) as Function; + if (Func == null) { + rc.Error(this.name, "use of undeclared function: {0}", name.Name); + } + else if (name.Type == null) { + // We need set the type of this IdentifierExpr so ShallowType() works + Debug.Assert(name.Type == null); + Debug.Assert(Func.OutParams.Count > 0); + name.Type = Func.OutParams[0].TypedIdent.Type; + } + } + public virtual int ArgumentCount { + get { + Contract.Assume(Func != null); // ArgumentCount requires object to be properly resolved. + return Func.InParams.Count; + } + } + public virtual Type Typecheck(IList<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(actuals != null); + Contract.Ensures(Contract.ValueAtReturn(out actuals) != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Assume(this.Func != null); + Contract.Assume(actuals.Count == Func.InParams.Count); + Contract.Assume(Func.OutParams.Count == 1); + + List<Type/*!*/>/*!*/ resultingTypeArgs; + List<Type> actualResultType = + Type.CheckArgumentTypes(Func.TypeParameters, + out resultingTypeArgs, + new List<Type>(Func.InParams.Select(Item => Item.TypedIdent.Type).ToArray()), + actuals, + new List<Type>(Func.OutParams.Select(Item => Item.TypedIdent.Type).ToArray()), + null, + // we need some token to report a possibly wrong number of + // arguments + actuals.Count > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken, + "application of " + name.Name, + tc); + + if (actualResultType == null) { + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + return null; + } else { + Contract.Assert(actualResultType.Count == 1); + tpInstantiation = + SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs); + return actualResultType[0]; + } + } + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + Contract.Assume(name.Type != null); + return name.Type; + } + + public virtual T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + + public class TypeCoercion : IAppliable { + private IToken/*!*/ tok; + public Type/*!*/ Type; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + } + + public TypeCoercion(IToken tok, Type type) { + Contract.Requires(type != null); + Contract.Requires(tok != null); + this.tok = tok; + this.Type = type; + } + + public override bool Equals(object obj) { + TypeCoercion other = obj as TypeCoercion; + if (other == null) { + return false; + } else { + return object.Equals(Type, other.Type); + } + } + + + + public + string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + + return ":"; + } + } + + public void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, + int contextBindingStrength, bool fragileContext) { + //Contract.Requires(args != null); + //Contract.Requires(stream != null); + stream.SetToken(ref this.tok); + Contract.Assert(args.Count == 1); + // determine if parens are needed + int opBindingStrength = 0x80; + bool parensNeeded = opBindingStrength < contextBindingStrength || + (fragileContext && opBindingStrength == contextBindingStrength); + + if (parensNeeded) + stream.Write("("); + + cce.NonNull(args[0]).Emit(stream, opBindingStrength, false); + stream.Write("{0} ", FunctionName); + Type.Emit(stream, 0); + + if (parensNeeded) + stream.Write(")"); + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + this.Type = this.Type.ResolveType(rc); + } + + public int ArgumentCount { + get { + return 1; + } + } + + public Type Typecheck(IList<Expr>/*!*/ args, + out TypeParamInstantiation/*!*/ tpInstantiation, + TypecheckingContext/*!*/ tc) { + //Contract.Requires(args != null); + //Contract.Requires(tc != null); + Contract.Ensures(args != null); + + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + + Contract.Assume(args.Count == 1); + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + + if (!this.Type.Unify(cce.NonNull(cce.NonNull(args[0]).Type))) + tc.Error(this.tok, "{0} cannot be coerced to {1}", + cce.NonNull(args[0]).Type, this.Type); + return this.Type; + } + + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + return this.Type; + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + + } + + public class ArithmeticCoercion : IAppliable { + public enum CoercionType { + ToInt, + ToReal, + ToFloat + } + + private IToken/*!*/ tok; + public readonly CoercionType Coercion; + private readonly string name; + private readonly Type type; + private readonly Type argType; + private readonly Type argType2; + private readonly int hashCode; + + public ArithmeticCoercion(IToken tok, CoercionType coercion) { + this.tok = tok; + this.Coercion = coercion; + + switch (coercion) { + case CoercionType.ToInt: + this.name = "int"; + this.type = Type.Int; + this.argType = Type.Real; + this.hashCode = 1; + break; + case CoercionType.ToReal: + this.name = "real"; + this.type = Type.Real; + this.argType = Type.Int; + this.hashCode = 2; + break; + default: + Contract.Assert(false); + break; + } + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return this.name; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) { + ArithmeticCoercion ac = other as ArithmeticCoercion; + return ac != null && this.Coercion == ac.Coercion; + } + + [Pure] + public override int GetHashCode() { + return this.hashCode; + } + + public string/*!*/ FunctionName { + get { + return this.name; + } + } + + public int ArgumentCount { + get { + return 1; + } + } + + virtual public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //Contract.Requires(args != null); + stream.Write(this.name); + stream.Write("("); + args.Emit(stream); + stream.Write(")"); + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + } + + public virtual Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(args != null); + Contract.Ensures(args != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + + Contract.Assert(args.Count == 1); + + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + + if (!(cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType) || cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType2))) + { + tc.Error(this.tok, "argument type {0} does not match expected type {1} or type {2}", cce.NonNull(args[0]).Type, this.argType, this.argType2); + } + + return this.type; + } + + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + return this.type; + } + + public virtual T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + + public class NAryExpr : Expr { + [Additive] + [Peer] + private IAppliable _Fun; + public IAppliable/*!*/ Fun { + get { + return _Fun; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change Function used by Immutable NAryExpr"); + + _Fun = value; + } + } + private List<Expr> _Args; + public IList<Expr> Args { + get { + if (Immutable) + return _Args.AsReadOnly(); + else + return _Args; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change Args of Immutable NAryExpr"); + + _Args = value as List<Expr>; + } + } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Fun != null); + Contract.Invariant(Args != null); + } + + + // The instantiation of type parameters that is determined during type checking. + // Which type parameters are available depends on the IAppliable + public TypeParamInstantiation TypeParameters = null; + + [Captured] + public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, IList<Expr>/*!*/ args, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(fun != null); + Contract.Requires(args != null); + _Fun = fun; + Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null)); + if (immutable) { + // We need to make a new list because the client might be holding + // references to the list that they gave us which could be used to + // circumvent the immutability enforcement + _Args = new List<Expr>(args); + CachedHashCode = ComputeHashCode(); + } else { + if (args is List<Expr>) { + // Preserve NAryExpr's old behaviour, we take ownership of the List<Expr>. + // We can only do this if the type matches + _Args = args as List<Expr>; + } + else { + // Otherwise we must make a copy + _Args = new List<Expr> (args); + } + } + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is NAryExpr)) + return false; + + NAryExpr other = (NAryExpr)obj; + return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args); + } + + [Pure] + public override int GetHashCode() { + if (Immutable) + return this.CachedHashCode; + else + return ComputeHashCode(); + } + + [Pure] + public override int ComputeHashCode() { + int h = this.Fun.GetHashCode(); + // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references + // We want structural equality + foreach (var arg in Args) { + h = (97*h) + arg.GetHashCode(); + } + return h; + } + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + stream.SetToken(this); + Fun.Emit(Args, stream, contextBindingStrength, fragileContext); + } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + Fun.Resolve(rc, this); + foreach (Expr/*!*/ e in Args) { + Contract.Assert(e != null); + e.Resolve(rc); + } + } + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + foreach (Expr/*!*/ e in Args) { + Contract.Assert(e != null); + e.ComputeFreeVariables(freeVars); + } + // also add the free type variables + if (TypeParameters != null) { + foreach (TypeVariable/*!*/ var in TypeParameters.FormalTypeParams) { + Contract.Assert(var != null); + foreach (TypeVariable/*!*/ w in TypeParameters[var].FreeVariables) { + Contract.Assert(w != null); + freeVars.Add(w); + } + } + } + } + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + int prevErrorCount = tc.ErrorCount; + foreach (Expr/*!*/ e in Args) { + Contract.Assert(e != null); + e.Typecheck(tc); + } + if (Fun.ArgumentCount != Args.Count) { + tc.Error(this, "wrong number of arguments to function: {0} ({1} instead of {2})", + Fun.FunctionName, Args.Count, Fun.ArgumentCount); + } else if (tc.ErrorCount == prevErrorCount && + // if the type parameters are set, this node has already been + // typechecked and does not need to be checked again + TypeParameters == null) { + TypeParamInstantiation tpInsts; + Type = Fun.Typecheck(Args, out tpInsts, tc); // Make sure we pass Args so if this Expr is immutable it is protected + TypeParameters = tpInsts; + } + IOverloadedAppliable oa = Fun as IOverloadedAppliable; + if (oa != null) { + oa.ResolveOverloading(this); + } + if (Type == null) { + // set Type to some non-null value + Type = new TypeProxy(this.tok, "type_checking_error"); + } + } + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + return Fun.ShallowType(Args); + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitNAryExpr(this); + } + } + + public class MapSelect : IAppliable { + + public readonly int Arity; + private readonly IToken/*!*/ tok; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + } + + + public MapSelect(IToken tok, int arity) { + Contract.Requires(tok != null); + this.tok = tok; + this.Arity = arity; + } + + public string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + + return "MapSelect"; + } + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (!(obj is MapSelect)) + return false; + + MapSelect other = (MapSelect)obj; + return this.Arity == other.Arity; + } + + [Pure] + public override int GetHashCode() { + return Arity.GetHashCode() * 2823; + } + + public void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, + int contextBindingStrength, bool fragileContext) { + //Contract.Requires(args != null); + //Contract.Requires(stream != null); + Contract.Assume(args.Count == Arity + 1); + Emit(args, stream, contextBindingStrength, fragileContext, false); + } + + public static void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, + int contextBindingStrength, bool fragileContext, + bool withRhs) { + Contract.Requires(args != null); + Contract.Requires(stream != null); + const int opBindingStrength = 0x90; + bool parensNeeded = opBindingStrength < contextBindingStrength || + (fragileContext && opBindingStrength == contextBindingStrength); + + if (parensNeeded) { + stream.Write("("); + } + cce.NonNull(args[0]).Emit(stream, opBindingStrength, false); + stream.Write("["); + + string sep = ""; + int lastIndex = withRhs ? args.Count - 1 : args.Count; + for (int i = 1; i < lastIndex; ++i) { + stream.Write(sep); + sep = ", "; + cce.NonNull(args[i]).Emit(stream); + } + + if (withRhs) { + stream.Write(" := "); + cce.NonNull(args.Last()).Emit(stream); + } + + stream.Write("]"); + if (parensNeeded) { + stream.Write(")"); + } + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + // PR: nothing? + } + + public int ArgumentCount { + get { + return Arity + 1; + } + } + + // it is assumed that each of the arguments has already been typechecked + public static Type Typecheck(Type/*!*/ mapType, + // we just pass an Absy, because in + // the AssignCmd maps can also be + // represented by non-expressions + Absy/*!*/ map, + List<Expr>/*!*/ indexes, + // the type parameters, in this context, are the parameters of the + // potentially polymorphic map type. Because it might happen that + // the whole map type is unknown and represented using a MapTypeProxy, + // the instantiations given in the following out-parameter are subject + // to change if further unifications are done. + out TypeParamInstantiation/*!*/ tpInstantiation, + TypecheckingContext/*!*/ tc, + IToken/*!*/ typeCheckingSubject, + string/*!*/ opName) { + Contract.Requires(mapType != null); + Contract.Requires(map != null); + Contract.Requires(indexes != null); + Contract.Requires(tc != null); + Contract.Requires(typeCheckingSubject != null); + Contract.Requires(opName != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + + mapType = mapType.Expanded; + if (mapType.IsMap && mapType.MapArity != indexes.Count) { + tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1} instead of {2}", + opName, indexes.Count, mapType.MapArity); + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + return null; + } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Count))) { + tc.Error(map.tok, "{0} applied to a non-map: {1}", opName, map); + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + return null; + } + mapType = TypeProxy.FollowProxy(mapType); + + if (mapType is MapType) { + MapType mt = (MapType)mapType; + return mt.CheckArgumentTypes(indexes, out tpInstantiation, + typeCheckingSubject, opName, tc); + } else { + MapTypeProxy mt = (MapTypeProxy)mapType; + return mt.CheckArgumentTypes(indexes, out tpInstantiation, + typeCheckingSubject, opName, tc); + } + } + + public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(args != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Assume(args.Count == Arity + 1); + + // FIXME: Wny are we passing a copy? + List<Expr> actualArgs = new List<Expr>(); + for (int i = 1; i < args.Count; ++i) + actualArgs.Add(args[i]); + + return Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]), + actualArgs, out tpInstantiation, tc, this.tok, "map select"); + } + + /// <summary> + /// Returns the result type of the IAppliable, supposing the argument are of the correct types. + /// </summary> + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + Expr a0 = cce.NonNull(args[0]); + Type a0Type = a0.ShallowType; + if (a0Type == null || !a0Type.IsMap) { + // we are unable to determine the type of the select, so just return an arbitrary type + return Type.Int; + } + MapType mapType = a0Type.AsMap; + List<Type> actualArgTypes = new List<Type>(); + for (int i = 1; i < args.Count; ++i) { + actualArgTypes.Add(cce.NonNull(args[i]).ShallowType); + } + return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes); + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + + public class MapStore : IAppliable { + + public readonly int Arity; + public readonly IToken/*!*/ tok; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + } + + + public MapStore(IToken tok, int arity) { + Contract.Requires(tok != null); + this.tok = tok; + this.Arity = arity; + } + + public string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + + return "MapStore"; + } + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (!(obj is MapStore)) + return false; + + MapStore other = (MapStore)obj; + return this.Arity == other.Arity; + } + + [Pure] + public override int GetHashCode() { + return Arity.GetHashCode() * 28231; + } + + public void Emit(IList<Expr>/*!*/ args, TokenTextWriter/*!*/ stream, + int contextBindingStrength, bool fragileContext) { + //Contract.Requires(args != null); + //Contract.Requires(stream != null); + Contract.Assert(args.Count == Arity + 2); + MapSelect.Emit(args, stream, contextBindingStrength, fragileContext, true); + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + // PR: nothing? + } + + public int ArgumentCount { + get { + return Arity + 2; + } + } + + // it is assumed that each of the arguments has already been typechecked + public static Type Typecheck(IList<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, + TypecheckingContext/*!*/ tc, + IToken/*!*/ typeCheckingSubject, + string/*!*/ opName) { + Contract.Requires(args != null); + Contract.Requires(tc != null); + Contract.Requires(typeCheckingSubject != null); + Contract.Requires(opName != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + + // part of the type checking works exactly as for MapSelect + List<Expr> selectArgs = new List<Expr>(); + for (int i = 1; i < args.Count - 1; ++i) + selectArgs.Add(args[i]); + Type resultType = + MapSelect.Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]), + selectArgs, out tpInstantiation, tc, typeCheckingSubject, opName); + + // check the the rhs has the right type + if (resultType == null) { + // error messages have already been created by MapSelect.Typecheck + return null; + } + Type rhsType = cce.NonNull(cce.NonNull(args.Last()).Type); + if (!resultType.Unify(rhsType)) { + tc.Error(cce.NonNull(args.Last()).tok, + "right-hand side in {0} with wrong type: {1} (expected: {2})", + opName, rhsType, resultType); + return null; + } + + return cce.NonNull(args[0]).Type; + } + + public Type Typecheck(IList<Expr>/*!*/ args, + out TypeParamInstantiation/*!*/ tpInstantiation, + TypecheckingContext/*!*/ tc) { + //Contract.Requires(args != null); + //Contract.Requires(tc != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Ensures(Contract.ValueAtReturn(out args) != null); + Contract.Assert(args.Count == Arity + 2); + return Typecheck(args, out tpInstantiation, tc, this.tok, "map store"); + } + + /// <summary> + /// Returns the result type of the IAppliable, supposing the argument are of the correct types. + /// </summary> + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + return cce.NonNull(args[0]).ShallowType; + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + + + public class IfThenElse : IAppliable { + + private IToken/*!*/ _tok; + + public IToken/*!*/ tok + { + get + { + Contract.Ensures(Contract.Result<IToken>() != null); + return this._tok; + } + set + { + Contract.Requires(value != null); + this._tok = value; + } + } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(this._tok != null); + } + + public IfThenElse(IToken tok) { + Contract.Requires(tok != null); + this._tok = tok; + } + + public string/*!*/ FunctionName { + get { + Contract.Ensures(Contract.Result<string>() != null); + + return "if-then-else"; + } + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (!(obj is IfThenElse)) + return false; + return true; + } + + [Pure] + public override int GetHashCode() { + return 1; + } + + public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //Contract.Requires(args != null); + stream.SetToken(this); + Contract.Assert(args.Count == 3); + stream.push(); + stream.Write("(if "); + cce.NonNull(args[0]).Emit(stream, 0x00, false); + stream.sep(); + stream.Write(" then "); + cce.NonNull(args[1]).Emit(stream, 0x00, false); + stream.sep(); + stream.Write(" else "); + cce.NonNull(args[2]).Emit(stream, 0x00, false); + stream.Write(")"); + stream.pop(); + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + // PR: nothing? + } + + public int ArgumentCount { + get { + return 3; + } + } + + public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(args != null); + Contract.Ensures(args != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + Contract.Assert(args.Count == 3); + // the default; the only binary operator with a type parameter is equality, but right + // we don't store this parameter because it does not appear necessary + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + Expr arg0 = cce.NonNull(args[0]); + Expr arg1 = cce.NonNull(args[1]); + Expr arg2 = cce.NonNull(args[2]); + + if (!cce.NonNull(arg0.Type).Unify(Type.Bool)) { + tc.Error(this.tok, "the first argument to if-then-else should be bool, not {0}", arg0.Type); + } else if (!cce.NonNull(arg1.Type).Unify(cce.NonNull(arg2.Type))) { + tc.Error(this.tok, "branches of if-then-else have incompatible types {0} and {1}", arg1.Type, arg2.Type); + } else { + return arg1.Type; + } + + return null; + } + + /// <summary> + /// Returns the result type of the IAppliable, supposing the argument are of the correct types. + /// </summary> + public Type ShallowType(IList<Expr> args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result<Type>() != null); + return cce.NonNull(args[1]).ShallowType; + } + + public T Dispatch<T>(IAppliableVisitor<T> visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + + + + public class CodeExpr : Expr { + public List<Variable>/*!*/ LocVars; + [Rep] + public List<Block/*!*/>/*!*/ Blocks; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(LocVars != null); + Contract.Invariant(cce.NonNullElements(Blocks)); + } + + public CodeExpr(List<Variable>/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks, bool immutable=false) + : base(Token.NoToken, immutable) { + Contract.Requires(localVariables != null); + Contract.Requires(cce.NonNullElements(blocks)); + Contract.Requires(0 < blocks.Count); + LocVars = localVariables; + Blocks = blocks; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + // FIXME: This seems wrong we don't want reference equality, we want structural equality + [Pure] + public override bool Equals(object obj) + { + return base.Equals(obj); + } + + [Pure] + public override int GetHashCode() + { + if (Immutable) + return CachedHashCode; + else + return ComputeHashCode(); + } + + [Pure] + public override int ComputeHashCode() { + return base.GetHashCode(); + } + + + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + // Treat a BlockEexpr as if it has no free variables at all + } + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //level++; + int level = 0; + stream.WriteLine(level, "|{"); + + if (this.LocVars.Count > 0) { + stream.Write(level + 1, "var "); + this.LocVars.Emit(stream, true); + stream.WriteLine(";"); + } + + foreach (Block/*!*/ b in this.Blocks) { + Contract.Assert(b != null); + b.Emit(stream, level + 1); + } + + stream.WriteLine(); + stream.WriteLine(level, "}|"); + + stream.WriteLine(); + stream.WriteLine(); + } + + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + + rc.PushVarContext(); + foreach (Variable/*!*/ v in LocVars) { + Contract.Assert(v != null); + v.Register(rc); + v.Resolve(rc); + } + + rc.PushProcedureContext(); + foreach (Block/*!*/ b in Blocks) { + Contract.Assert(b != null); + b.Register(rc); + } + + foreach (Block/*!*/ b in Blocks) { + Contract.Assert(b != null); + b.Resolve(rc); + } + + rc.PopProcedureContext(); + rc.PopVarContext(); + } + + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + foreach (Variable/*!*/ v in LocVars) { + Contract.Assert(v != null); + v.Typecheck(tc); + } + foreach (Block/*!*/ b in Blocks) { + Contract.Assert(b != null); + b.Typecheck(tc); + } + this.Type = Type.Bool; + } + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + return Type.Bool; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitCodeExpr(this); + } + } + + public class BvExtractExpr : Expr { + private /*readonly--except in StandardVisitor*/ Expr/*!*/ _Bitvector; + public Expr Bitvector { + get { + return _Bitvector; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change BitVector field of an immutable BvExtractExpr"); + + _Bitvector = value; + } + } + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(_Bitvector != null); + } + + public readonly int Start, End; + + public BvExtractExpr(IToken/*!*/ tok, Expr/*!*/ bv, int end, int start, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(bv != null); + _Bitvector = bv; + Start = start; + End = end; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BvExtractExpr)) + return false; + + BvExtractExpr other = (BvExtractExpr)obj; + return object.Equals(this.Bitvector, other.Bitvector) && + this.Start.Equals(other.Start) && this.End.Equals(other.End); + } + + [Pure] + public override int GetHashCode() { + if (Immutable) + return CachedHashCode; + else + return ComputeHashCode(); + } + + [Pure] + public override int ComputeHashCode() { + int h = this.Bitvector.GetHashCode(); + h ^= Start * 17 ^ End * 13; + return h; + } + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + stream.SetToken(this); + int opBindingStrength = 0x90; + bool parensNeeded = opBindingStrength < contextBindingStrength || + (fragileContext && opBindingStrength == contextBindingStrength); + + if (parensNeeded) { + stream.Write("("); + } + Bitvector.Emit(stream, opBindingStrength, false); + stream.Write("[" + End + ":" + Start + "]"); + if (parensNeeded) { + stream.Write(")"); + } + } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + Bitvector.Resolve(rc); + } + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + Bitvector.ComputeFreeVariables(freeVars); + } + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + Bitvector.Typecheck(tc); + Contract.Assert(Bitvector.Type != null); // follows from postcondition of Expr.Typecheck + + if (Start < 0) { + tc.Error(this, "start index in extract must not be negative"); + } else if (End < 0) { + tc.Error(this, "end index in extract must not be negative"); + } else if (End < Start) { + tc.Error(this, "start index in extract must be no bigger than the end index"); + } else { + Type typeConstraint = new BvTypeProxy(this.tok, "extract", End - Start); + if (typeConstraint.Unify(Bitvector.Type)) { + Type = Type.GetBvType(End - Start); + } else { + tc.Error(this, "extract operand must be a bitvector of at least {0} bits (got {1})", End - Start, Bitvector.Type); + } + } + if (Type == null) { + Type = new TypeProxy(this.tok, "type_checking_error"); + } + } + + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + return Type.GetBvType(End - Start); + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitBvExtractExpr(this); + } + } + + public class BvConcatExpr : Expr { + private /*readonly--except in StandardVisitor*/ Expr/*!*/ _E0, _E1; + public Expr E0 { + get { + return _E0; + } + set { + if (Immutable) + throw new InvalidOperationException("Can't change E0 reference on immutable Expr"); + + _E0 = value; + } + } + public Expr E1 { + get { + return _E1; + } + set { + if (Immutable) + throw new InvalidOperationException("Can't change E1 reference on immutable Expr"); + + _E1 = value; + } + } + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(E0 != null); + Contract.Invariant(E1 != null); + } + + + public BvConcatExpr(IToken/*!*/ tok, Expr/*!*/ e0, Expr/*!*/ e1, bool immutable=false) + : base(tok, immutable) { + Contract.Requires(tok != null); + Contract.Requires(e0 != null); + Contract.Requires(e1 != null); + _E0 = e0; + _E1 = e1; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BvConcatExpr)) + return false; + + BvConcatExpr other = (BvConcatExpr)obj; + return object.Equals(this.E0, other.E0) && object.Equals(this.E1, other.E1); + } + + [Pure] + public override int GetHashCode() + { + if (Immutable) + return CachedHashCode; + else + return ComputeHashCode(); + } + + [Pure] + public override int ComputeHashCode() { + int h = this.E0.GetHashCode() ^ this.E1.GetHashCode() * 17; + return h; + } + + public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + stream.SetToken(this); + int opBindingStrength = 0x32; + bool parensNeeded = opBindingStrength < contextBindingStrength || + (fragileContext && opBindingStrength == contextBindingStrength); + + if (parensNeeded) { + stream.Write("("); + } + E0.Emit(stream, opBindingStrength, false); + stream.Write(" ++ "); + // while this operator is associative, our incomplete axioms in int translation don't + // make much use of it, so better stick to the actual tree shape + E1.Emit(stream, opBindingStrength, true); + if (parensNeeded) { + stream.Write(")"); + } + } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + E0.Resolve(rc); + E1.Resolve(rc); + } + public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { + //Contract.Requires(freeVars != null); + E0.ComputeFreeVariables(freeVars); + E1.ComputeFreeVariables(freeVars); + } + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + E0.Typecheck(tc); + Contract.Assert(E0.Type != null); // follows from postcondition of Expr.Typecheck + E1.Typecheck(tc); + Contract.Assert(E1.Type != null); // follows from postcondition of Expr.Typecheck + + if (E0.Type.Unify(new BvTypeProxy(this.tok, "concat0", 0)) && E1.Type.Unify(new BvTypeProxy(this.tok, "concat1", 0))) { + Type = new BvTypeProxy(this.tok, "concat", E0.Type, E1.Type); + } else { + tc.Error(this, "++ operands need to be bitvectors (got {0}, {1})", E0.Type, E1.Type); + } + if (Type == null) { + Type = new TypeProxy(this.tok, "type_checking_error"); + } + } + + public override Type/*!*/ ShallowType { + get { + Contract.Ensures(Contract.Result<Type>() != null); + + Type t0 = E0.ShallowType; + Type t1 = E1.ShallowType; + int len0 = t0.IsBv ? t0.BvBits : /*expression is not type correct, so just pick an arbitrary number of bits*/0; + int len1 = t1.IsBv ? t1.BvBits : /*expression is not type correct, so just pick an arbitrary number of bits*/0; + return Type.GetBvType(len0 + len1); + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitBvConcatExpr(this); + } + } +} + |