diff options
| author |  tabarbe <unknown> | 2010-08-26 23:37:01 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-26 23:37:01 +0000 |
| commit | 47171ab9f9d31dab0d5e0a4c3c95c763452e9295 (patch) | |
| tree | 402d453ee1c63dff1a04d03eabfc2bef32eed4ed /Source/AIFramework/Expr.cs | |
| parent | 8b0392fe672ce820ba07af673fe9177babdee00b (diff) | |
Boogie: Renaming the AIFramework sources in preparation for committal of my port of the project
Diffstat (limited to 'Source/AIFramework/Expr.cs')
| -rw-r--r-- | Source/AIFramework/Expr.cs | 459 |
1 files changed, 459 insertions, 0 deletions
diff --git a/Source/AIFramework/Expr.cs b/Source/AIFramework/Expr.cs new file mode 100644 index 00000000..1f21f84a --- /dev/null +++ b/Source/AIFramework/Expr.cs @@ -0,0 +1,459 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+// This file specifies the expression language used by the Abstract
+// Interpretation Framework.
+//
+// expressions e ::= x variables
+// | f(e1,...,en) uninterpreted functions
+// | \x:t.e lambda expressions
+//
+// types t ::= b user-defined/built-in base types
+// | t1 * ... * tn -> t' function type
+
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using System.Collections;
+ using Microsoft.Contracts;
+
+ //----------------------------- Expressions -----------------------------
+
+ /// <summary>
+ /// An interface for expressions. This expression language is specified
+ /// by interfaces to allow the client to be able to use their existing
+ /// AST nodes as AIF expressions.
+ ///
+ /// This only serves as a place for operations on expressions. Clients
+ /// should implement directly IVariable, IFunApp, ...
+ /// </summary>
+ public interface IExpr
+ {
+ /// <summary>
+ /// Execute a visit over the expression.
+ /// </summary>
+ /// <param name="visitor">The expression visitor.</param>
+ /// <returns>The result of the visit.</returns>
+ [Pure] object DoVisit(ExprVisitor! visitor);
+
+ // TODO: Type checking of the expressions.
+ }
+
+ /// <summary>
+ /// An interface for variables.
+ ///
+ /// This interface should be implemented by the client.
+ /// </summary>
+ public interface IVariable : IExpr
+ {
+ string! Name { get; } // Each client must define the name for variables
+ }
+
+ /// <summary>
+ /// An interface for function applications.
+ ///
+ /// This interface should be implemented by the client.
+ /// </summary>
+ public interface IFunApp : IExpr
+ {
+ IFunctionSymbol! FunctionSymbol { get; }
+ IList/*<IExpr!>*/! Arguments
+ {
+ [Pure][Rep] get
+ ensures result.IsReadOnly;
+ ;
+ }
+
+ /// <summary>
+ /// Provides a method to create a new uninterpreted function
+ /// with the same function symbol but with the arguments with
+ /// args.
+ /// </summary>
+ /// <param name="args">The new arguments.</param>
+ /// <returns>A copy of the function with the new arguments.</returns>
+ IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)
+ //TODO requires this.Arguments.Count == args.Count;
+ ;
+ }
+
+ /// <summary>
+ /// An interface for anonymous functions (i.e., lambda expressions)
+ /// </summary>
+ public interface IFunction : IExpr
+ {
+ IVariable! Param { get; }
+ AIType! ParamType { get; }
+ IExpr! Body { get; }
+
+ IFunction! CloneWithBody(IExpr! body);
+ }
+
+ /// <summary>
+ /// An interface representing an expression that at any moment could, in principle, evaluate
+ /// to a different value. That is, the abstract interpreter should treat these IExpr's
+ /// as unknown values. They are used when there is no other IExpr corresponding to the
+ /// expression to be modeled.
+ /// </summary>
+ public interface IUnknown : IExpr {}
+
+ /// <summary>
+ /// An abstract class that provides an interface for expression visitors.
+ /// </summary>
+ public abstract class ExprVisitor
+ {
+ public abstract object Default(IExpr! expr);
+
+ public virtual object VisitVariable(IVariable! var)
+ {
+ return Default(var);
+ }
+
+ public virtual object VisitFunApp(IFunApp! funapp)
+ {
+ return Default(funapp);
+ }
+
+ public virtual object VisitFunction(IFunction! fun)
+ {
+ return Default(fun);
+ }
+ }
+
+ /// <summary>
+ /// A utility class for dealing with expressions.
+ /// </summary>
+ public sealed class ExprUtil
+ {
+ /// <summary>
+ /// Yield an expression that is 'inexpr' with 'var' replaced by 'subst'.
+ /// </summary>
+ /// <param name="subst">The expression to substitute.</param>
+ /// <param name="var">The variable to substitute for.</param>
+ /// <param name="inexpr">The expression to substitute into.</param>
+ public static IExpr! Substitute(IExpr! subst, IVariable! var, IExpr! inexpr)
+ {
+ IExpr result = null;
+
+ if (inexpr is IVariable)
+ {
+ result = inexpr.Equals(var) ? subst : inexpr;
+ }
+ else if (inexpr is IFunApp)
+ {
+ IFunApp! funapp = (IFunApp!)inexpr;
+ IList newargs = null;
+ newargs = new ArrayList{ IExpr! arg in funapp.Arguments; Substitute(subst, var, arg) };
+ result = funapp.CloneWithArguments(newargs);
+ }
+ else if (inexpr is IFunction)
+ {
+ IFunction! fun = (IFunction!)inexpr;
+
+ if (fun.Param.Equals(var))
+ result = fun;
+ else
+ result = fun.CloneWithBody(Substitute(subst, var, fun.Body));
+ }
+ else if (inexpr is IUnknown)
+ {
+ result = inexpr;
+ }
+ else
+ {
+ assert false;
+ }
+
+ return result;
+ }
+
+
+ //
+ // Poor man's pattern matching.
+ //
+ // The methods below implement pattern matching for AI expressions.
+ //
+ // Example Usage:
+ // Match(e, Prop.Imp,
+ // (Matcher)delegate (IExpr e) { return Match(e, Prop.And, out x, out y); }
+ // out z)
+ // which sees if 'e' matches Prop.Imp(Prop.And(x,y),z) binding x,y,z to the subtrees.
+ //
+ public delegate bool Matcher(IExpr! expr);
+
+ private static IFunApp/*?*/ MatchFunctionSymbol(IExpr! expr, IFunctionSymbol! f)
+ {
+ IFunApp app = expr as IFunApp;
+ if (app != null)
+ {
+ if (app.FunctionSymbol.Equals(f))
+ return app;
+ else
+ return null;
+ }
+ else
+ return null;
+ }
+
+ public static bool Match(IExpr! expr, IFunctionSymbol! f, params Matcher[]! subs)
+ {
+ IFunApp app = MatchFunctionSymbol(expr,f);
+ if (app != null)
+ {
+ int i = 0; // Note ***0***
+ foreach (Matcher! s in subs)
+ {
+ if (!s((IExpr!)app.Arguments[i])) { return false; }
+ i++;
+ }
+ return true;
+ }
+ else { return false; }
+ }
+
+ // Unary Binding
+ public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, params Matcher[]! subs)
+ {
+ arg0 = null;
+
+ IFunApp app = MatchFunctionSymbol(expr,f);
+ if (app != null)
+ {
+ arg0 = (IExpr!)app.Arguments[0];
+
+ int i = 1; // Note ***1***
+ foreach (Matcher! s in subs)
+ {
+ if (!s((IExpr!)app.Arguments[i])) { return false; }
+ i++;
+ }
+ return true;
+ }
+ else { return false; }
+ }
+
+ // Binary Binding
+ public static bool Match(IExpr! expr, IFunctionSymbol! f, Matcher! sub0, out IExpr arg1, params Matcher[]! subs)
+ {
+ arg1 = null;
+
+ IFunApp app = MatchFunctionSymbol(expr,f);
+ if (app != null)
+ {
+ if (!sub0((IExpr!)app.Arguments[0])) { return false; }
+
+ arg1 = (IExpr!)app.Arguments[1];
+
+ int i = 2; // Note ***2***
+ foreach (Matcher! s in subs)
+ {
+ if (!s((IExpr!)app.Arguments[i])) { return false; }
+ i++;
+ }
+ return true;
+ }
+ else { return false; }
+ }
+
+ public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, params Matcher[]! subs)
+ {
+ arg0 = null;
+ arg1 = null;
+
+ IFunApp app = MatchFunctionSymbol(expr,f);
+ if (app != null)
+ {
+ arg0 = (IExpr!)app.Arguments[0];
+ arg1 = (IExpr!)app.Arguments[1];
+
+ int i = 2; // Note ***2***
+ foreach (Matcher! s in subs)
+ {
+ if (!s((IExpr!)app.Arguments[i])) { return false; }
+ i++;
+ }
+ return true;
+ }
+ else { return false; }
+ }
+
+ // Ternary Binding
+ public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]! subs)
+ {
+ arg0 = null;
+ arg1 = null;
+ arg2 = null;
+
+ IFunApp app = MatchFunctionSymbol(expr,f);
+ if (app != null)
+ {
+ arg0 = (IExpr!)app.Arguments[0];
+ arg1 = (IExpr!)app.Arguments[1];
+ arg2 = (IExpr!)app.Arguments[2];
+
+ int i = 3; // Note ***3***
+ foreach (Matcher! s in subs)
+ {
+ if (!s((IExpr!)app.Arguments[i])) { return false; }
+ i++;
+ }
+ return true;
+ }
+ else { return false; }
+ }
+
+ /// <summary>
+ /// Not intended to be instantiated.
+ /// </summary>
+ private ExprUtil() { }
+ }
+
+ //------------------------------ Symbols --------------------------------
+
+ /// <summary>
+ /// An interface for function symbols. Constants are represented by
+ /// 0-ary function symbols.
+ ///
+ /// This interface should be implemented by abstract domains, but client
+ /// expressions need keep track of function symbols.
+ /// </summary>
+ public interface IFunctionSymbol
+ {
+ AIType! AIType { [Rep][ResultNotNewlyAllocated]
+ get; }
+ }
+
+ /// <summary>
+ /// The type of the arguments to ExprUtil.Match, a poor man's pattern
+ /// matching.
+ /// </summary>
+ public interface IMatchable
+ {
+ }
+
+ //-------------------------------- Types --------------------------------
+
+ /// <summary>
+ /// Types.
+ /// </summary>
+ public interface AIType
+ {
+ }
+
+ /// <summary>
+ /// Function type constructor.
+ /// </summary>
+ public sealed class FunctionType : AIType
+ {
+ /*[Own]*/ private readonly IList/*<Type!>*/! argTypes;
+ /*[Own]*/ private readonly AIType! retType;
+
+ public FunctionType(params AIType[]! types)
+ requires types.Length >= 2;
+ {
+ AIType type = types[types.Length-1];
+ assume type != null;
+ this.retType = type;
+ ArrayList argTypes = new ArrayList();
+ for (int i = 0; i < types.Length-1; i++)
+ {
+ type = types[i];
+ assume type != null;
+ argTypes.Add(types);
+ }
+ this.argTypes = ArrayList.ReadOnly(argTypes);
+ }
+
+ public IList/*<AIType!>*/! Arguments
+ {
+ [Pure][Rep]
+ get
+ ensures result.IsReadOnly;
+ {
+ return argTypes;
+ }
+ }
+
+ public int Arity
+ {
+ get { return argTypes.Count; }
+ }
+
+ public AIType! ReturnType
+ {
+ get { return retType; }
+ }
+
+ /* TODO Do we have the invariant that two functions are equal iff they're the same object.
+ public override bool Equals(object o)
+ {
+ if (o != null && o is FunctionType)
+ {
+ FunctionType other = (FunctionType) o;
+
+ if (Arity == other.Arity
+ && ReturnType.Equals(other.ReturnType))
+ {
+ for (int i = 0; i < Arity; i++)
+ {
+ if (!argTypes[i].Equals(other.argTypes[i]))
+ return false;
+ }
+ return true;
+ }
+ else
+ return false;
+ }
+ else
+ return false;
+ }
+ */
+ }
+
+ //------------------------------ Queries -------------------------------
+
+ public enum Answer { Yes, No, Maybe };
+
+ /// <summary>
+ /// An interface that specifies a queryable object that can answer
+ /// whether a predicate holds.
+ /// </summary>
+ public interface IQueryable
+ {
+ /// <summary>
+ /// Answers the query whether the given predicate holds.
+ /// </summary>
+ /// <param name="pred">The given predicate.</param>
+ /// <returns>Yes, No, or Maybe.</returns>
+ Answer CheckPredicate(IExpr! pred);
+
+ /// <summary>
+ /// A simplified interface for disequalities. One can always
+ /// implement this by calling CheckPredicate, but it may be
+ /// more efficient with this method.
+ /// </summary>
+ Answer CheckVariableDisequality(IVariable! var1, IVariable! var2);
+ }
+
+ public static class QueryUtil
+ {
+ public static Answer Negate(Answer ans)
+ {
+ switch (ans)
+ {
+ case Answer.Yes:
+ return Answer.No;
+ case Answer.No:
+ return Answer.Yes;
+ default:
+ return Answer.Maybe;
+ }
+ }
+ }
+
+ //----------------------------- Exceptions -----------------------------
+
+ public class TypeError : CheckedException
+ {
+ }
+}
|