diff options
| author |  tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
| commit | b617dda87871573b826dada4af73fc48dce94f15 (patch) | |
| tree | 453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/AbsyExpr.cs | |
| parent | 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff) | |
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 2430 |
1 files changed, 2430 insertions, 0 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs new file mode 100644 index 00000000..250820ed --- /dev/null +++ b/Source/Core/AbsyExpr.cs @@ -0,0 +1,2430 @@ +//-----------------------------------------------------------------------------
+//
+// 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 AI = Microsoft.AbstractInterpretationFramework;
+ using Microsoft.Contracts;
+ using Microsoft.Basetypes;
+
+
+ //---------------------------------------------------------------------
+ // 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.
+ //---------------------------------------------------------------------
+
+
+ public abstract class Expr : Absy
+ {
+ public Expr(IToken! tok)
+ : base(tok)
+ {
+ }
+
+ public void Emit (TokenTextWriter! stream)
+ {
+ Emit(stream, 0, false);
+ }
+
+ public abstract void Emit (TokenTextWriter! wr, int contextBindingStrength, bool fragileContext);
+
+ [Pure]
+ public override string! ToString ()
+ {
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, 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>
+ public Type Type;
+
+ public override void Typecheck (TypecheckingContext! tc)
+ 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.
+ assert false;
+ }
+
+ /// <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)
+ {
+ return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1));
+ }
+
+ public static NAryExpr! Binary (IToken! x, BinaryOperator.Opcode op, Expr! e0, Expr! e1)
+ {
+ return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e0, e1));
+ }
+
+ public static NAryExpr! Binary (BinaryOperator.Opcode op, Expr! e0, Expr! e1)
+ {
+ return Binary(Token.NoToken, op, e0, e1);
+ }
+
+ public static NAryExpr! Eq (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Eq, e1, e2); }
+ public static NAryExpr! Neq (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Neq, e1, e2); }
+ public static NAryExpr! Le (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Le, e1, e2); }
+ public static NAryExpr! Ge (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Ge, e1, e2); }
+ public static NAryExpr! Lt (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Lt, e1, e2); }
+ public static NAryExpr! Gt (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Gt, e1, e2); }
+ public static Expr! And (Expr! e1, Expr! e2) {
+ if (e1 == true_) { return e2; }
+ else if (e2 == true_) { return e1; }
+ else if (e1 == false_ || e2 == false_) { return false_; }
+ else { return Binary(BinaryOperator.Opcode.And, e1, e2); }
+ }
+ public static Expr! Or (Expr! e1, Expr! e2) {
+ 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) {
+ 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 (!) nary.Args[0]; }
+ }
+ else if (nary.Fun is BinaryOperator)
+ {
+ BinaryOperator op = (BinaryOperator)nary.Fun;
+ Expr arg0 = (!)nary.Args[0];
+ Expr arg1 = (!)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 Ge(arg0, arg1); }
+ else if (op.Op == BinaryOperator.Opcode.Le) { return Gt(arg0, arg1); }
+ else if (op.Op == BinaryOperator.Opcode.Ge) { return Lt(arg0, arg1); }
+ else if (op.Op == BinaryOperator.Opcode.Gt) { return Le(arg0, arg1); }
+ }
+ }
+
+ return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
+ }
+ public static NAryExpr! Imp (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Imp, e1, e2); }
+ public static NAryExpr! Iff (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Iff, e1, e2); }
+ public static NAryExpr! Add (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Add, e1, e2); }
+ public static NAryExpr! Sub (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Sub, e1, e2); }
+ public static NAryExpr! Mul (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Mul, e1, e2); }
+ public static NAryExpr! Div (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Div, e1, e2); }
+ public static NAryExpr! Mod (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Mod, e1, e2); }
+ public static NAryExpr! Subtype (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Subtype, e1, e2); }
+
+ public static IdentifierExpr! Ident (string! name, Type! type)
+ {
+ return new IdentifierExpr(Token.NoToken, name, type);
+ }
+
+ public static IdentifierExpr! Ident (Variable! decl)
+ {
+ IdentifierExpr result = new IdentifierExpr(Token.NoToken, decl);
+ return result;
+ }
+
+ public static LiteralExpr! Literal (bool value) { return new LiteralExpr(Token.NoToken, value); }
+ public static LiteralExpr! Literal (int value) { return new LiteralExpr(Token.NoToken, BigNum.FromInt(value)); }
+ public static LiteralExpr! Literal (BigNum value) { return new LiteralExpr(Token.NoToken, value); }
+
+ private static LiteralExpr! true_ = Literal(true);
+ public static LiteralExpr! True { get { return true_; } }
+
+ private static LiteralExpr! false_ = Literal(false);
+ public static LiteralExpr! False { get { return false_; } }
+
+
+ public static NAryExpr! Select(Expr! map, params Expr[]! args) {
+ return SelectTok(Token.NoToken, map, args);
+ }
+
+ public static NAryExpr! Select(Expr! map, List<Expr!>! args) {
+ 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)
+ {
+ ExprSeq! allArgs = new ExprSeq ();
+ allArgs.Add(map);
+ foreach (Expr! a in args)
+ allArgs.Add(a);
+ return new NAryExpr(x, new MapSelect(Token.NoToken, args.Length), allArgs);
+ }
+
+ public static NAryExpr! Store(Expr! map, params Expr[]! args) {
+ return StoreTok(Token.NoToken, map, args);
+ }
+
+ public static NAryExpr! Store(Expr! map, List<Expr!>! indexes, Expr! rhs) {
+ 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)
+ requires args.Length > 0; // zero or more indices, plus the value
+ {
+ ExprSeq! allArgs = new ExprSeq ();
+ allArgs.Add(map);
+ foreach (Expr! a in args)
+ 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) {
+ ExprSeq! args = new ExprSeq ();
+ args.Add(subexpr);
+ return new NAryExpr(x, new TypeCoercion(x, type), args);
+ }
+
+
+ /// <summary>
+ /// This property returns a representation for the expression suitable for use
+ /// by the AIFramework. Usually, the property just returns "this", but not
+ /// every Expr is an AI.IExpr (besides, AI.IExpr is to be thought of as an
+ /// abstract interface--any class that implements AI.IExpr is supposed to
+ /// implement some proper subinterface of AI.IExpr).
+ /// The converse operations of this property are found in AbsInt\ExprFactories.ssc.
+ /// </summary>
+ public abstract AI.IExpr! IExpr {
+ [Peer] get;
+ }
+
+ }
+
+ public class LiteralExpr : Expr, AI.IFunApp
+ {
+ public readonly object! Val; // false, true, a BigNum, or a BvConst
+ /// <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)
+ : base(tok)
+ {
+ Val = b;
+ }
+ /// <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)
+ : base(tok)
+ {
+ Val = v;
+ }
+
+ /// <summary>
+ /// Creates a literal expression for the bitvector value "v".
+ /// </summary>
+ public LiteralExpr(IToken! tok, BigNum v, int b)
+ : base(tok)
+ {
+ Val = new BvConst(v, b);
+ }
+
+ [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()
+ {
+ return this.Val.GetHashCode();
+ }
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(this);
+ if (this.Val is bool)
+ {
+ stream.Write((bool)this.Val ? "true" : "false"); // correct capitalization
+ }
+ else
+ {
+ stream.Write((!) this.Val.ToString());
+ }
+ }
+ public override void Resolve(ResolutionContext! rc)
+ {
+ // nothing to resolve
+ }
+ public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ // no free variables to add
+ }
+
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ if (Val is BvConst && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None)
+ tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");
+ this.Type = ShallowType;
+ }
+
+ public override Type! ShallowType {
+ get {
+ if (Val is bool)
+ {
+ return Type.Bool;
+ }
+ else if (Val is BigNum)
+ {
+ return Type.Int;
+ }
+ else if (Val is BvConst)
+ {
+ return Type.GetBvType(((BvConst)Val).Bits);
+ }
+ else
+ {
+ assert false; // 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;
+ }
+ }
+ public override AI.IExpr! IExpr {
+ get {
+ return this;
+ }
+ }
+
+ // 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 {
+ assert isBigNum;
+ return (BigNum)(!)Val;
+ }
+ }
+
+ public bool isBool {
+ get {
+ return Val is bool;
+ }
+ }
+
+ public bool asBool {
+ get {
+ assert isBool;
+ return (bool)(!)Val;
+ }
+ }
+
+ public AI.IFunctionSymbol! FunctionSymbol {
+ get {
+ if (Val is bool)
+ {
+ if ((bool)Val)
+ {
+ return AI.Prop.True;
+ }
+ else
+ {
+ return AI.Prop.False;
+ }
+ }
+ else if (Val is BigNum)
+ {
+ return AI.Int.Const((BigNum)Val);
+ }
+ else if (Val is BvConst)
+ {
+ return AI.Bv.Const(((BvConst)Val).Value, ((BvConst)Val).Bits);
+ }
+ else
+ {
+ assert false; // like, where did this value come from?!
+ }
+ }
+ }
+ public IList/*<AI.IExpr!>*/! Arguments {
+ get {
+ return ArrayList.ReadOnly(new AI.IExpr[0]);
+ }
+ }
+ public Microsoft.AbstractInterpretationFramework.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args) {
+ assert args.Count == 0;
+ return this;
+ }
+ public AI.AIType! AIType {
+ get {
+ if (Val is bool) {
+ return AI.Prop.Type;
+ } else if (Val is BigNum) {
+ return AI.Int.Type;
+ } else if (Val is BvConst) {
+ return AI.Bv.Type;
+ } else {
+ assert false; // like, where did this value come from?!
+ }
+ }
+ }
+ [Pure]
+ public object DoVisit(AI.ExprVisitor! visitor)
+ {
+ return visitor.VisitFunApp(this);
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitLiteralExpr(this);
+ }
+ }
+
+ public class BvConst
+ {
+ public BigNum Value;
+ public int Bits;
+
+ public BvConst(BigNum v, int b)
+ {
+ assert v.Signum >= 0;
+ Value = v;
+ Bits = b;
+ }
+
+ [Pure]
+ public override string! ToString()
+ {
+ return Value + "bv" + Bits;
+ }
+
+ [Pure]
+ public string! ToReadableString()
+ {
+ if (Value > BigNum.FromInt(10000)) {
+ string! val = (!)Value.ToString("x");
+ int pos = val.Length % 4;
+ string! res = "0x" + val.Substring(0, pos);
+ 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 AIVariableExpr : Expr
+ {
+
+ public string Name; // identifier symbol
+ public AI.IVariable! Decl; // identifier declaration
+
+ /// <summary>
+ /// Creates an unresolved identifier expression.
+ /// </summary>
+ /// <param name="tok"></param>
+ /// <param name="name"></param>
+ public AIVariableExpr(IToken! tok, AI.IVariable! var)
+ : base(tok)
+ {
+ Name = var.ToString();
+ Decl = var;
+ }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj)
+ {
+ if (obj == null) return false;
+ if (!(obj is AIVariableExpr)) return false;
+
+ AIVariableExpr other = (AIVariableExpr)obj;
+ return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl);
+ }
+ [Pure]
+ public override int GetHashCode()
+ {
+ 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)
+ {
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds)
+ {
+ stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h"+this.Decl.GetHashCode());
+ }
+ stream.Write(this, "{0}", this.Name);
+ }
+ public override void Resolve(ResolutionContext! rc)
+ {
+ }
+ public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ if (Decl is Variable) {
+ freeVars.Add((Variable)Decl);
+ }
+ }
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ throw new System.NotImplementedException();
+ }
+ public override Type! ShallowType
+ {
+ get { throw new System.NotImplementedException(); }
+ }
+ public override AI.IExpr! IExpr {
+ get {
+ return Decl;
+ }
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitAIVariableExpr(this);
+ }
+ }
+
+ public class IdentifierExpr : Expr
+ {
+ public string! Name; // identifier symbol
+ public Variable Decl; // identifier declaration
+
+ /// <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)
+ : base(tok)
+ {
+ Name = name;
+ // base(tok);
+ }
+ /// <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)
+ : base(tok)
+ {
+ Name = name;
+ Type = type;
+ // base(tok);
+ }
+
+ /// <summary>
+ /// Creates a resolved identifier expression.
+ /// </summary>
+ /// <param name="tok"></param>
+ /// <param name="d"></param>
+ public IdentifierExpr(IToken! tok, Variable! d)
+ : base(tok)
+ {
+ Name = (!) d.Name;
+ Decl = d;
+ Type = d.TypedIdent.Type;
+ // base(tok);
+ }
+ [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()
+ {
+ 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)
+ {
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds)
+ {
+ 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)
+ {
+ 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) {
+ assume this.Decl != null;
+ freeVars.Add(Decl);
+ }
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ 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);
+ assert false;
+ }
+ Type = Decl.TypedIdent.Type;
+ }
+ }
+
+ public override Type! ShallowType {
+ get {
+ assert Type != null;
+ return Type;
+ }
+ }
+
+ public sealed class ConstantFunApp : AI.IFunApp
+ {
+ private IdentifierExpr! identifierExpr;
+ public IdentifierExpr! IdentifierExpr { get { return identifierExpr; } }
+
+ private AI.IFunctionSymbol! symbol;
+ public AI.IFunctionSymbol! FunctionSymbol { get { return symbol; } }
+
+ private static IList! emptyArgs = ArrayList.ReadOnly((IList!)new ArrayList());
+ public IList! Arguments { get { return emptyArgs; } }
+
+ public AI.IFunApp! CloneWithArguments(IList! newargs) { return this; }
+
+ [Pure]
+ public object DoVisit(AI.ExprVisitor! visitor) { return visitor.VisitFunApp(this); }
+
+ public ConstantFunApp(IdentifierExpr! ie, Constant! c)
+ {
+ this.identifierExpr = ie;
+ this.symbol =
+ new AI.NamedSymbol(c.TypedIdent.Name, BoogieFactory.Type2AIType(c.TypedIdent.Type));
+ // base();
+ }
+
+ }
+ private AI.IExpr iexprCache = null;
+ public override AI.IExpr! IExpr {
+ get
+ {
+ if (iexprCache == null)
+ {
+ if (Decl is Constant)
+ iexprCache = new ConstantFunApp(this, (Constant)Decl);
+ else{
+ assume this.Decl != null;
+ iexprCache = Decl;
+ }
+ }
+ return iexprCache;
+ }
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitIdentifierExpr(this);
+ }
+ }
+
+ public class OldExpr : Expr
+ , AI.IFunApp // HACK
+ {
+ public Expr! Expr;
+ public OldExpr(IToken! tok, Expr! expr)
+ : base(tok)
+ {
+ Expr = expr;
+ }
+ [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()
+ {
+ return this.Expr == null ? 0 : this.Expr.GetHashCode();
+ }
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.Write(this, "old(");
+ this.Expr.Emit(stream);
+ stream.Write(")");
+ }
+ public override void Resolve(ResolutionContext! rc)
+ {
+ 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) {
+ Expr.ComputeFreeVariables(freeVars);
+ }
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ Expr.Typecheck(tc);
+ Type = Expr.Type;
+ }
+ public override Type! ShallowType {
+ get {
+ return Expr.ShallowType;
+ }
+ }
+ public override AI.IExpr! IExpr {
+ get {
+// Put back these lines when "HACK" removed
+// // An Old expression has no AI.IExpr representation
+// assert false;
+// throw new System.Exception(); // make compiler shut up
+ return this; // HACK
+ }
+ }
+ [Pure]
+ public object DoVisit(AI.ExprVisitor! visitor)
+ {
+ return visitor.VisitFunApp(this);
+ }
+ public AI.IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)
+ {
+ assume args.Count == 1;
+ AI.IExpr! iexpr = (AI.IExpr!)args[0];
+ return new OldExpr(Token.NoToken, BoogieFactory.IExpr2Expr(iexpr));
+ }
+ private IList/*?*/ argCache = null;
+ public IList/*<IExpr!*/! Arguments
+ {
+ get {
+ if (argCache == null)
+ {
+ IList l = new ArrayList(1);
+ l.Add(Expr.IExpr);
+ argCache = ArrayList.ReadOnly(l);
+ }
+ return argCache;
+ }
+ }
+ private sealed class OldFunctionSymbol : AI.IFunctionSymbol
+ {
+ private static AI.AIType! aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type);
+ public AI.AIType! AIType { get { return aitype; } }
+ private OldFunctionSymbol() { }
+ internal static OldFunctionSymbol! Sym = new OldFunctionSymbol();
+ [Pure]
+ public override string! ToString() { return "old"; }
+ }
+ public AI.IFunctionSymbol! FunctionSymbol
+ {
+ get { return OldFunctionSymbol.Sym; }
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitOldExpr(this);
+ }
+ }
+
+ 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(IfThenElse! ifThenElse);
+ }
+
+ 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(ExprSeq! 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(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc);
+ ensures args.Length == old(args.Length);
+ // 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(ExprSeq! args);
+
+ AI.IFunctionSymbol! AIFunctionSymbol { get; }
+
+ T Dispatch<T>(IAppliableVisitor<T>! visitor);
+ }
+
+ public interface IOverloadedAppliable
+ {
+ void ResolveOverloading(NAryExpr! expr);
+ }
+
+ public class UnaryOperator : IAppliable
+ {
+ private IToken! tok;
+ public enum Opcode { Not };
+ private Opcode op;
+ public Opcode Op { get { return op; } }
+ public UnaryOperator (IToken! tok, Opcode op) { 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
+ {
+ switch (this.op)
+ {
+ case Opcode.Not: return "!";
+ }
+ System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
+ throw new Exception();
+ }
+ }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol {
+ get {
+ switch (this.op) {
+ case Opcode.Not: return AI.Prop.Not;
+ }
+ System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
+ throw new Exception();
+ }
+ }
+
+ public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(ref this.tok);
+ assert args.Length == 1;
+ // determine if parens are needed
+ int opBindingStrength = 0x60;
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded)
+ {
+ stream.Write("(");
+ }
+ stream.Write(FunctionName);
+ ((!)args[0]).Emit(stream, opBindingStrength, false);
+ if (parensNeeded)
+ {
+ stream.Write(")");
+ }
+ }
+
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting)
+ {
+ 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(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
+ {
+ assume args.Length == 1;
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+ Type arg0type = (!)((!)args[0]).Type;
+ switch (this.op)
+ {
+ case Opcode.Not:
+ if (arg0type.Unify(Type.Bool))
+ {
+ return Type.Bool;
+ }
+ goto BAD_TYPE;
+ }
+ System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
+ assert false;
+ BAD_TYPE:
+ tc.Error(this.tok, "invalid argument type ({1}) to unary operator {0}",
+ this.FunctionName, arg0type);
+ return null;
+ }
+ public Type! ShallowType(ExprSeq! args) {
+ switch (this.op) {
+ case Opcode.Not:
+ return Type.Bool;
+ default:
+ assert false; // unexpected unary operator
+ }
+ }
+
+ public object Evaluate (object argument)
+ {
+ if (argument == null) { return null; }
+ switch (this.op)
+ {
+ 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) {
+ return visitor.Visit(this);
+ }
+ }
+
+ public class BinaryOperator : IAppliable, IOverloadedAppliable
+ {
+ private IToken! tok;
+ public enum Opcode { Add, Sub, Mul, Div, Mod, 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) { 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
+ {
+ switch (this.op)
+ {
+ case Opcode.Add: return "+";
+ case Opcode.Sub: return "-";
+ case Opcode.Mul: return "*";
+ case Opcode.Div: return "/";
+ case Opcode.Mod: 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 AI.IFunctionSymbol! AIFunctionSymbol {
+ get {
+ switch (this.op) {
+ case Opcode.Add: return AI.Int.Add;
+ case Opcode.Sub: return AI.Int.Sub;
+ case Opcode.Mul: return AI.Int.Mul;
+ case Opcode.Div: return AI.Int.Div;
+ case Opcode.Mod: return AI.Int.Mod;
+ case Opcode.Eq: return AI.Value.Eq;
+ case Opcode.Neq: return AI.Value.Neq;
+ case Opcode.Gt: return AI.Int.Greater;
+ case Opcode.Ge: return AI.Int.AtLeast;
+ case Opcode.Lt: return AI.Int.Less;
+ case Opcode.Le: return AI.Int.AtMost;
+ case Opcode.And: return AI.Prop.And;
+ case Opcode.Or: return AI.Prop.Or;
+ case Opcode.Imp: return AI.Prop.Implies;
+ case Opcode.Iff: return AI.Value.Eq;
+ case Opcode.Subtype: return AI.Value.Subtype;
+ }
+ System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
+ throw new Exception();
+ }
+ }
+
+ public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(ref this.tok);
+ assert args.Length == 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.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));
+
+ if (parensNeeded)
+ {
+ stream.Write("(");
+ }
+ ((!)args[0]).Emit(stream, opBindingStrength, fragileLeftContext);
+ stream.Write(" {0} ", FunctionName);
+ ((!)args[1]).Emit(stream, opBindingStrength, fragileRightContext);
+ if (parensNeeded)
+ {
+ stream.Write(")");
+ }
+ }
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting)
+ {
+ if (rc.TriggerMode) {
+ switch (this.op)
+ {
+ case Opcode.Add:
+ case Opcode.Sub:
+ case Opcode.Mul:
+ case Opcode.Div:
+ case Opcode.Mod:
+ 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(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
+ {
+ assert args.Length == 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 = (!)args[0];
+ Expr arg1 = (!)args[1];
+ Type arg0type = (!)arg0.Type;
+ Type arg1type = (!)arg1.Type;
+ switch (this.op)
+ {
+ case Opcode.Add:
+ case Opcode.Sub:
+ case Opcode.Mul:
+ case Opcode.Div:
+ case Opcode.Mod:
+ if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
+ return Type.Int;
+ }
+ 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;
+ }
+ TypeVariableSeq! unifiable = new TypeVariableSeq ();
+ 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;
+ }
+ 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());
+ assert false;
+ 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(ExprSeq! args) {
+ switch (this.op)
+ {
+ case Opcode.Add:
+ case Opcode.Sub:
+ case Opcode.Mul:
+ case Opcode.Div:
+ case Opcode.Mod:
+ return Type.Int;
+
+ 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:
+ assert false; // unexpected binary operator
+ }
+ }
+
+ public void ResolveOverloading(NAryExpr! expr)
+ {
+ Expr arg0 = (!) expr.Args[0];
+ Expr arg1 = (!) 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);
+ arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new ExprSeq(arg1));
+
+ // ugly ... there should be some more general approach,
+ // e.g., to typecheck the whole expression again
+ arg1.Type = Type.Bool;
+ ((NAryExpr)arg1).TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+
+ expr.Args[1] = arg1;
+ }
+ 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); }
+ break;
+ case Opcode.Sub:
+ if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)-((BigNum)e2); }
+ break;
+ case Opcode.Mul:
+ if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)*((BigNum)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.Lt:
+ if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)<((BigNum)e2); }
+ break;
+ case Opcode.Le:
+ if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)<=((BigNum)e2); }
+ break;
+ case Opcode.Gt:
+ if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)>((BigNum)e2); }
+ break;
+ case Opcode.Ge:
+ if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)>=((BigNum)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) {
+ return visitor.Visit(this);
+ }
+
+ }
+
+ public class FunctionCall : IAppliable, AI.IFunctionSymbol
+ {
+ private IdentifierExpr! name;
+ public Function Func;
+ public FunctionCall(IdentifierExpr! name) { this.name = name; }
+ public FunctionCall(Function! f) { this.Func = f; this.name = new IdentifierExpr(Token.NoToken, f.Name); }
+ public string! FunctionName { get { return this.name.Name; } }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol {
+ get {
+ if (name.Name == "$typeof") {
+ return AI.Value.Typeof;
+ } else if (name.Name == "$allocated") {
+ return AI.FieldName.Allocated;
+ } else {
+ return this;
+ }
+ }
+ }
+
+ [Pure]
+ public override string! ToString() {
+ 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()
+ {
+ assume this.Func != null;
+ return Func.GetHashCode();
+ }
+
+ public AI.AIType! AIType {
+ get
+ {
+ assume this.Func != null;
+ return AI.Value.FunctionType(this.Func.InParams.Length);
+ }
+ }
+
+ virtual public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ this.name.Emit(stream, 0xF0, false);
+ stream.Write("(");
+ args.Emit(stream);
+ stream.Write(")");
+ }
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting)
+ {
+ 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);
+ }
+ }
+ public virtual int ArgumentCount
+ {
+ get
+ {
+ assume Func != null; // ArgumentCount requires object to be properly resolved.
+ return Func.InParams.Length;
+ }
+ }
+ public virtual Type Typecheck(ref ExprSeq! actuals, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
+ {
+ assume this.Func != null;
+ assume actuals.Length == Func.InParams.Length;
+ assume Func.OutParams.Length == 1;
+
+ List<Type!>! resultingTypeArgs;
+ TypeSeq actualResultType =
+ Type.CheckArgumentTypes(Func.TypeParameters,
+ out resultingTypeArgs,
+ Func.InParams.ToTypeSeq,
+ actuals,
+ Func.OutParams.ToTypeSeq,
+ null,
+ // we need some token to report a possibly wrong number of
+ // arguments
+ actuals.Length > 0 ? ((!)actuals[0]).tok : Token.NoToken,
+ "application of " + name.Name,
+ tc);
+
+ if (actualResultType == null) {
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+ return null;
+ } else {
+ assert actualResultType.Length == 1;
+ tpInstantiation =
+ SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs);
+ return actualResultType[0];
+ }
+ }
+ public Type! ShallowType(ExprSeq! args) {
+ assume name.Type != null;
+ return name.Type;
+ }
+
+ public virtual T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ return visitor.Visit(this);
+ }
+ }
+
+ public class TypeCoercion : IAppliable {
+ private IToken! tok;
+ public Type! Type;
+
+ public TypeCoercion(IToken! tok, Type! type) {
+ this.tok = tok;
+ this.Type = type;
+ }
+
+ public string! FunctionName { get {
+ return ":";
+ } }
+
+ public void Emit(ExprSeq! args, TokenTextWriter! stream,
+ int contextBindingStrength, bool fragileContext) {
+ stream.SetToken(ref this.tok);
+ assert args.Length == 1;
+ // determine if parens are needed
+ int opBindingStrength = 0x90;
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded)
+ stream.Write("(");
+
+ ((!)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) {
+ this.Type = this.Type.ResolveType(rc);
+ }
+
+ public int ArgumentCount { get {
+ return 1;
+ } }
+
+ public Type Typecheck(ref ExprSeq! args,
+ out TypeParamInstantiation! tpInstantiation,
+ TypecheckingContext! tc) {
+ assume args.Length == 1;
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+
+ if (!this.Type.Unify((!)((!)args[0]).Type))
+ tc.Error(this.tok, "{0} cannot be coerced to {1}",
+ ((!)args[0]).Type, this.Type);
+ return this.Type;
+ }
+
+ public Type! ShallowType(ExprSeq! args) {
+ return this.Type;
+ }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol { get {
+ // not really clear what should be returned here ...
+ // should the operation be completely invisible for the abstract interpretation?
+ return AI.Heap.UnsupportedHeapOp;
+ } }
+
+ public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ return visitor.Visit(this);
+ }
+
+ }
+
+ public class NAryExpr : Expr, AI.IFunApp
+ {
+ [Additive] [Peer]
+ public IAppliable! Fun;
+ public ExprSeq! Args;
+
+ // 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, ExprSeq! args)
+ : base(tok)
+ {
+ Fun = fun;
+ Args = args;
+ assert forall{Expr arg in args; arg != null};
+ }
+ [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) && object.Equals(this.Args, other.Args);
+ }
+ [Pure]
+ public override int GetHashCode()
+ {
+ int h = this.Fun.GetHashCode();
+ h ^= this.Args.GetHashCode();
+ return h;
+ }
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(this);
+ Fun.Emit(Args, stream, contextBindingStrength, fragileContext);
+ }
+ public override void Resolve(ResolutionContext! rc)
+ {
+ Fun.Resolve(rc, this);
+ foreach (Expr! e in Args)
+ {
+ e.Resolve(rc);
+ }
+ }
+ public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ foreach (Expr! e in Args) {
+ e.ComputeFreeVariables(freeVars);
+ }
+ // also add the free type variables
+ if (TypeParameters != null) {
+ foreach (TypeVariable! var in TypeParameters.FormalTypeParams)
+ foreach (TypeVariable! w in TypeParameters[var].FreeVariables)
+ freeVars.Add(w);
+ }
+ }
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ int prevErrorCount = tc.ErrorCount;
+ foreach (Expr! e in Args)
+ {
+ e.Typecheck(tc);
+ }
+ if (Fun.ArgumentCount != Args.Length)
+ {
+ tc.Error(this, "wrong number of arguments to function: {0} ({1} instead of {2})",
+ Fun.FunctionName, Args.Length, 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(ref Args, out tpInsts, tc);
+ if (Type != null && Type.IsBv && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) {
+ tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");
+ }
+ 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 {
+ return Fun.ShallowType(Args);
+ }
+ }
+
+ public override AI.IExpr! IExpr {
+ get {
+ return this;
+ }
+ }
+ public AI.IFunctionSymbol! FunctionSymbol {
+ get {
+ return Fun.AIFunctionSymbol;
+ }
+ }
+ public IList/*<AI.IExpr!>*/! Arguments {
+ get {
+ AI.IExpr[] a = new AI.IExpr[Args.Length];
+ for (int i = 0; i < Args.Length; i++) {
+ a[i] = ((!)Args[i]).IExpr;
+ }
+ return ArrayList.ReadOnly(a);
+ }
+ }
+ public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args) {
+ return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args));
+ }
+
+ [Pure]
+ public object DoVisit(AI.ExprVisitor! visitor)
+ {
+ return visitor.VisitFunApp(this);
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitNAryExpr(this);
+ }
+ }
+
+ public class MapSelect : IAppliable, AI.IFunctionSymbol {
+
+ public readonly int Arity;
+ private readonly IToken! tok;
+
+ public MapSelect(IToken! tok, int arity) {
+ this.tok = tok;
+ this.Arity = arity;
+ }
+
+ public string! FunctionName { get {
+ 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(ExprSeq! args, TokenTextWriter! stream,
+ int contextBindingStrength, bool fragileContext) {
+ assume args.Length == Arity + 1;
+ Emit(args, stream, contextBindingStrength, fragileContext, false);
+ }
+
+ public static void Emit(ExprSeq! args, TokenTextWriter! stream,
+ int contextBindingStrength, bool fragileContext,
+ bool withRhs) {
+ const int opBindingStrength = 0x70;
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded)
+ {
+ stream.Write("(");
+ }
+ ((!)args[0]).Emit(stream, opBindingStrength, false);
+ stream.Write("[");
+
+ string sep = "";
+ int lastIndex = withRhs ? args.Length - 1 : args.Length;
+ for (int i = 1; i < lastIndex; ++i) {
+ stream.Write(sep);
+ sep = ", ";
+ ((!)args[i]).Emit(stream);
+ }
+
+ if (withRhs) {
+ stream.Write(" := ");
+ ((!)args.Last()).Emit(stream);
+ }
+
+ stream.Write("]");
+ if (parensNeeded)
+ {
+ stream.Write(")");
+ }
+ }
+
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ // 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,
+ ExprSeq! 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) {
+ mapType = mapType.Expanded;
+ if (mapType.IsMap && mapType.MapArity != indexes.Length) {
+ tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1} instead of {2}",
+ opName, indexes.Length, mapType.MapArity);
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+ return null;
+ } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Length))) {
+ 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(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
+ {
+ assume args.Length == Arity + 1;
+
+ ExprSeq actualArgs = new ExprSeq ();
+ for (int i = 1; i < args.Length; ++i)
+ actualArgs.Add(args[i]);
+
+ return Typecheck((!)((!)args[0]).Type, (!)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(ExprSeq! args) {
+ Expr a0 = (!)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;
+ TypeSeq actualArgTypes = new TypeSeq ();
+ for (int i = 1; i < args.Length; ++i) {
+ actualArgTypes.Add(((!)args[i]).ShallowType);
+ }
+ return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes);
+ }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol { get {
+ switch (Arity) {
+ case 1: return AI.Heap.Select1;
+ case 2: return AI.Heap.Select2;
+ default:
+ // Maps with Arity arguments are not fully supported yet
+ return AI.Heap.UnsupportedHeapOp;
+ }
+ } }
+
+ public AI.AIType! AIType {
+ [Rep][ResultNotNewlyAllocated]
+ get {
+ return AI.Prop.Type; // THAT is a type? PR: no idea whether this makes sense,
+ // but it is the type of select1
+ } }
+
+ public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ return visitor.Visit(this);
+ }
+ }
+
+ public class MapStore : IAppliable, AI.IFunctionSymbol {
+
+ public readonly int Arity;
+ public readonly IToken! tok;
+
+ public MapStore(IToken! tok, int arity) {
+ this.tok = tok;
+ this.Arity = arity;
+ }
+
+ public string! FunctionName { get {
+ 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(ExprSeq! args, TokenTextWriter! stream,
+ int contextBindingStrength, bool fragileContext) {
+ assert args.Length == Arity + 2;
+ MapSelect.Emit(args, stream, contextBindingStrength, fragileContext, true);
+ }
+
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ // 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(ExprSeq! args, out TypeParamInstantiation! tpInstantiation,
+ TypecheckingContext! tc,
+ IToken! typeCheckingSubject,
+ string! opName) {
+ // part of the type checking works exactly as for MapSelect
+ ExprSeq! selectArgs = new ExprSeq ();
+ for (int i = 1; i < args.Length - 1; ++i)
+ selectArgs.Add(args[i]);
+ Type resultType =
+ MapSelect.Typecheck((!)((!)args[0]).Type, (!)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 = (!)((!)args.Last()).Type;
+ if (!resultType.Unify(rhsType)) {
+ tc.Error(((!)args.Last()).tok,
+ "right-hand side in {0} with wrong type: {1} (expected: {2})",
+ opName, rhsType, resultType);
+ return null;
+ }
+
+ return ((!)args[0]).Type;
+ }
+
+ public Type Typecheck(ref ExprSeq! args,
+ out TypeParamInstantiation! tpInstantiation,
+ TypecheckingContext! tc)
+ {
+ assert args.Length == 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(ExprSeq! args) {
+ return ((!)args[0]).ShallowType;
+ }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol { get {
+ switch (Arity) {
+ case 1: return AI.Heap.Update1;
+ case 2: return AI.Heap.Update2;
+ default:
+ // Maps with Arity arguments are not fully supported yet
+ return AI.Heap.UnsupportedHeapOp;
+ }
+ } }
+
+ public AI.AIType! AIType {
+ [Rep][ResultNotNewlyAllocated]
+ get {
+ return AI.Heap.Type;
+ } }
+
+ public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ return visitor.Visit(this);
+ }
+ }
+
+
+ public class IfThenElse : IAppliable, AI.IFunctionSymbol {
+
+ public IToken! tok;
+
+ public IfThenElse(IToken! tok) {
+ this.tok = tok;
+ }
+
+ public string! FunctionName { get {
+ 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(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(ref this.tok);
+ assert args.Length == 3;
+ stream.Write("(if ");
+ ((!)args[0]).Emit(stream, 0x00, false);
+ stream.Write(" then ");
+ ((!)args[1]).Emit(stream, 0x00, false);
+ stream.Write(" else ");
+ ((!)args[2]).Emit(stream, 0x00, false);
+ stream.Write(")");
+ }
+
+ public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ // PR: nothing?
+ }
+
+ public int ArgumentCount { get {
+ return 3;
+ } }
+
+ public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
+ {
+ assert args.Length == 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 = (!)args[0];
+ Expr arg1 = (!)args[1];
+ Expr arg2 = (!)args[2];
+
+ if (!((!)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 (!((!)arg1.Type).Unify((!)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(ExprSeq! args) {
+ return ((!)args[1]).ShallowType;
+ }
+
+ public AI.IFunctionSymbol! AIFunctionSymbol { get { return this; } }
+
+ public AI.AIType! AIType {
+ [Rep][ResultNotNewlyAllocated]
+ get {
+ return AI.Value.FunctionType(3);
+ } }
+
+ public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ return visitor.Visit(this);
+ }
+ }
+
+
+
+ public class CodeExpr : Expr, AI.IUnknown
+ {
+ public VariableSeq! LocVars;
+ [Rep]
+ public List<Block!>! Blocks;
+ public CodeExpr(VariableSeq! localVariables, List<Block!>! blocks)
+ : base(Token.NoToken)
+ requires 0 < blocks.Count;
+ {
+ LocVars = localVariables;
+ Blocks = blocks;
+ }
+
+ public override AI.IExpr! IExpr { get { return this; } }
+ [Pure] public object DoVisit(AI.ExprVisitor! visitor) { return this; }
+
+ public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ // Treat a BlockEexpr as if it has no free variables at all
+ }
+ public override void Emit (TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ //level++;
+ int level = 0;
+ stream.WriteLine(level, "|{");
+
+ if (this.LocVars.Length > 0)
+ {
+ stream.Write(level + 1, "var ");
+ this.LocVars.Emit(stream);
+ stream.WriteLine(";");
+ }
+
+ foreach (Block! b in this.Blocks)
+ {
+ b.Emit(stream, level+1);
+ }
+
+ stream.WriteLine();
+ stream.WriteLine(level, "}|");
+
+ stream.WriteLine();
+ stream.WriteLine();
+ }
+
+ public override void Resolve(ResolutionContext! rc)
+ {
+
+ rc.PushVarContext();
+ foreach (Variable! v in LocVars)
+ {
+ v.Register(rc);
+ v.Resolve(rc);
+ }
+
+ rc.PushProcedureContext();
+ foreach (Block! b in Blocks)
+ {
+ b.Register(rc);
+ }
+
+ foreach (Block! b in Blocks)
+ {
+ b.Resolve(rc);
+ }
+
+ rc.PopProcedureContext();
+ rc.PopVarContext();
+ }
+
+ public override void Typecheck(TypecheckingContext! tc){
+ foreach (Variable! v in LocVars){
+ v.Typecheck(tc);
+ }
+ foreach (Block! b in Blocks){
+ b.Typecheck(tc);
+ }
+ this.Type = Type.Bool;
+ }
+ public override Type! ShallowType {
+ get {
+ return Type.Bool;
+ }
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitCodeExpr(this);
+ }
+ }
+
+
+
+ public class BvExtractExpr : Expr, AI.IFunApp
+ {
+ public /*readonly--except in StandardVisitor*/ Expr! Bitvector;
+ public readonly int Start, End;
+
+ public BvExtractExpr(IToken! tok, Expr! bv, int end, int start)
+ : base(tok)
+ {
+ Bitvector = bv;
+ Start = start;
+ End = end;
+ // base(tok);
+ }
+
+ [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()
+ {
+ int h = this.Bitvector.GetHashCode();
+ h ^= Start * 17 ^ End * 13;
+ return h;
+ }
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ stream.SetToken(this);
+ int opBindingStrength = 0x70;
+ 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)
+ {
+ Bitvector.Resolve(rc);
+ }
+ public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ Bitvector.ComputeFreeVariables(freeVars);
+ }
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ Bitvector.Typecheck(tc);
+ 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 {
+ return Type.GetBvType(End - Start);
+ }
+ }
+
+ public override AI.IExpr! IExpr {
+ get {
+ return this;
+ }
+ }
+ public AI.IFunctionSymbol! FunctionSymbol {
+ get { return AI.Bv.Extract;
+ }
+ }
+ public IList/*<AI.IExpr!>*/! Arguments {
+ get {
+ AI.IExpr[] a = new AI.IExpr[3];
+ a[0] = Bitvector.IExpr;
+ a[1] = new LiteralExpr(Token.NoToken, BigNum.FromInt(End));
+ a[2] = new LiteralExpr(Token.NoToken, BigNum.FromInt(Start));
+ return ArrayList.ReadOnly(a);
+ }
+ }
+ public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
+ {
+ AI.IFunApp! retFun;
+
+ if(args.Count == 3)
+ {
+ retFun = new BvExtractExpr(this.tok,
+ BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),
+ ((LiteralExpr!)args[1]).asBigNum.ToIntSafe,
+ ((LiteralExpr!)args[2]).asBigNum.ToIntSafe);
+ }
+ else
+ {
+ assert false; // If we are something wrong is happended
+ }
+ return retFun;
+ }
+
+ [Pure]
+ public object DoVisit(AI.ExprVisitor! visitor)
+ {
+ return visitor.VisitFunApp(this);
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitBvExtractExpr(this);
+ }
+ }
+
+ public class BvConcatExpr : Expr, AI.IFunApp
+ {
+ public /*readonly--except in StandardVisitor*/ Expr! E0, E1;
+
+ public BvConcatExpr(IToken! tok, Expr! e0, Expr! e1)
+ : base(tok)
+ {
+ E0 = e0;
+ E1 = e1;
+ // base(tok);
+ }
+
+ [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()
+ {
+ int h = this.E0.GetHashCode() ^ this.E1.GetHashCode() * 17;
+ return h;
+ }
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
+ {
+ 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)
+ {
+ E0.Resolve(rc);
+ E1.Resolve(rc);
+ }
+ public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ E0.ComputeFreeVariables(freeVars);
+ E1.ComputeFreeVariables(freeVars);
+ }
+ public override void Typecheck(TypecheckingContext! tc)
+ {
+ E0.Typecheck(tc);
+ assert E0.Type != null; // follows from postcondition of Expr.Typecheck
+ E1.Typecheck(tc);
+ 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 {
+ 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 AI.IExpr! IExpr {
+ get {
+ return this;
+ }
+ }
+ public AI.IFunctionSymbol! FunctionSymbol {
+ get { return AI.Bv.Concat;
+ }
+ }
+ public IList/*<AI.IExpr!>*/! Arguments {
+ get {
+ AI.IExpr[] a = new AI.IExpr[2];
+ a[0] = E0.IExpr;
+ a[1] = E1.IExpr;
+ return ArrayList.ReadOnly(a);
+ }
+ }
+ public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
+ {
+ AI.IFunApp! retFun;
+
+ if(args.Count == 2)
+ {
+ retFun = new BvConcatExpr(this.tok,
+ BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),
+ BoogieFactory.IExpr2Expr((AI.IExpr!)args[1]));
+ }
+ else
+ {
+ assert false; // If we are something wrong is happended
+ }
+ return retFun;
+ }
+
+ [Pure]
+ public object DoVisit(AI.ExprVisitor! visitor)
+ {
+ return visitor.VisitFunApp(this);
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitBvConcatExpr(this);
+ }
+ }
+}
+
|