//-----------------------------------------------------------------------------
//
// 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 System;
using System.Diagnostics.Contracts;
//----------------------------- Expressions -----------------------------
///
/// 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, ...
///
[ContractClass(typeof(IExprContracts))]
public interface IExpr
{
///
/// Execute a visit over the expression.
///
/// The expression visitor.
/// The result of the visit.
[Pure] object DoVisit(ExprVisitor/*!*/ visitor);
// TODO: Type checking of the expressions.
}
[ContractClassFor(typeof(IExpr))]
public abstract class IExprContracts:IExpr{
#region IExpr Members
public object DoVisit(ExprVisitor visitor)
{
Contract.Requires(visitor != null);
throw new System.NotImplementedException();
}
#endregion
}
///
/// An interface for variables.
///
/// This interface should be implemented by the client.
///
[ContractClass(typeof(IVariableContracts))]
public interface IVariable : IExpr
{
string/*!*/ Name { get; } // Each client must define the name for variables
}
[ContractClassFor(typeof(IVariable))]
public abstract class IVariableContracts:IVariable{
string IVariable.Name{get{Contract.Ensures(Contract.Result() != null);throw new NotImplementedException();}
}
#region IExpr Members
object IExpr.DoVisit(ExprVisitor visitor) {
throw new NotImplementedException();
}
#endregion
}
///
/// An interface for function applications.
///
/// This interface should be implemented by the client.
///
///
[ContractClass(typeof(IFunAppContracts))]
public interface IFunApp : IExpr
{
IFunctionSymbol/*!*/ FunctionSymbol { get; }
IList/**//*!*/ Arguments
{
[Pure][Rep] get;
}
///
/// Provides a method to create a new uninterpreted function
/// with the same function symbol but with the arguments with
/// args.
///
/// The new arguments.
/// A copy of the function with the new arguments.
IFunApp/*!*/ CloneWithArguments(IList/**//*!*/ args)
//TODO Contract.Requires(this.Arguments.Count == args.Count);
;
}
[ContractClassFor(typeof(IFunApp))]
public abstract class IFunAppContracts:IFunApp{
#region IFunApp Members
public IFunctionSymbol FunctionSymbol
{
get {Contract.Ensures(Contract.Result() != null);
throw new System.NotImplementedException(); }
}
public IList Arguments
{
get {Contract.Ensures(Contract.Result() != null);
Contract.Ensures(Contract.Result().IsReadOnly);
throw new System.NotImplementedException(); }
}
public IFunApp CloneWithArguments(IList args)
{
Contract.Requires(args != null);
Contract.Ensures(Contract.Result() != null);
throw new System.NotImplementedException();
}
#endregion
#region IExpr Members
object IExpr.DoVisit(ExprVisitor visitor) {
throw new NotImplementedException();
}
#endregion
}
///
/// An interface for anonymous functions (i.e., lambda expressions)
///
[ContractClass(typeof(IFunctionContracts))]
public interface IFunction : IExpr
{
IVariable/*!*/ Param { get; }
AIType/*!*/ ParamType { get; }
IExpr/*!*/ Body { get; }
IFunction/*!*/ CloneWithBody(IExpr/*!*/ body);
}
[ContractClassFor(typeof(IFunction))]
public abstract class IFunctionContracts:IFunction{
#region IFunction Members
IVariable IFunction.Param {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException();
}
}
AIType IFunction.ParamType {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException();
}
}
IExpr IFunction.Body {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException();
}
}
IFunction IFunction.CloneWithBody(IExpr body) {
Contract.Requires(body != null);
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException();
}
#endregion
#region IExpr Members
object IExpr.DoVisit(ExprVisitor visitor) {
throw new NotImplementedException();
}
#endregion
}
///
/// 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.
///
public interface IUnknown : IExpr {}
///
/// An abstract class that provides an interface for expression visitors.
///
[ContractClass(typeof(ExprVisitorContracts))]
public abstract class ExprVisitor
{
public abstract object Default(IExpr/*!*/ expr);
public virtual object VisitVariable(IVariable/*!*/ var){
Contract.Requires(var != null);
return Default(var);
}
public virtual object VisitFunApp(IFunApp/*!*/ funapp){
Contract.Requires(funapp != null);
return Default(funapp);
}
public virtual object VisitFunction(IFunction/*!*/ fun){
Contract.Requires(fun != null);
return Default(fun);
}
}
[ContractClassFor(typeof(ExprVisitor))]
public abstract class ExprVisitorContracts:ExprVisitor{
public override object Default(IExpr expr)
{
Contract.Requires(expr != null); throw new NotImplementedException();
}}
///
/// A utility class for dealing with expressions.
///
public sealed class ExprUtil
{
///
/// Yield an expression that is 'inexpr' with 'var' replaced by 'subst'.
///
/// The expression to substitute.
/// The variable to substitute for.
/// The expression to substitute into.
public static IExpr/*!*/ Substitute(IExpr/*!*/ subst, IVariable/*!*/ var, IExpr/*!*/ inexpr){
Contract.Requires(inexpr != null);
Contract.Requires(var != null);
Contract.Requires(subst != null);
Contract.Ensures(Contract.Result() != null);
IExpr result = null;
if (inexpr is IVariable)
{
result = inexpr.Equals(var) ? subst : inexpr;
}
else if (inexpr is IFunApp)
{
IFunApp/*!*/ funapp = (IFunApp/*!*/)cce.NonNull(inexpr);
IList newargs = null;
var x = new System.Collections.Generic.List();
foreach (IExpr arg in funapp.Arguments){
x.Add(Substitute(subst,var, arg));
}
newargs = new ArrayList(x);
//newargs = new ArrayList{ IExpr/*!*/ arg in funapp.Arguments; Substitute(subst, var, arg) };
result = funapp.CloneWithArguments(newargs);
}
else if (inexpr is IFunction)
{
IFunction/*!*/ fun = (IFunction/*!*/)cce.NonNull(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
{
{Contract.Assert(false);throw new cce.UnreachableException();}
}
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){
Contract.Requires(f != null);
Contract.Requires(expr != null);
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){
Contract.Requires(subs != null);
Contract.Requires(f != null);
Contract.Requires(expr != null);
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
int i = 0; // Note ***0***
foreach(Matcher/*!*/ s in subs){
Contract.Assert(s != null);
if (!s(cce.NonNull((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){
Contract.Requires(subs != null);
Contract.Requires(f != null);
Contract.Requires(expr != null);
arg0 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]);
int i = 1; // Note ***1***
foreach(Matcher/*!*/ s in subs){
Contract.Assert(s != null);
if (!s(cce.NonNull((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){
Contract.Requires(subs != null);
Contract.Requires(sub0 != null);
Contract.Requires(f != null);
Contract.Requires(expr != null);
arg1 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
if (!sub0(cce.NonNull((IExpr/*!*/)app.Arguments[0]))) { return false; }
arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]);
int i = 2; // Note ***2***
foreach(Matcher/*!*/ s in subs){
Contract.Assert(s != null);
if (!s(cce.NonNull((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){
Contract.Requires(subs != null);
Contract.Requires(f != null);
Contract.Requires(expr != null);
arg0 = null;
arg1 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]);
arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]);
int i = 2; // Note ***2***
foreach(Matcher/*!*/ s in subs){
Contract.Assert(s != null);
if (!s(cce.NonNull((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){
Contract.Requires(subs != null);
Contract.Requires(f != null);
Contract.Requires(expr != null);
arg0 = null;
arg1 = null;
arg2 = null;
IFunApp app = MatchFunctionSymbol(expr,f);
if (app != null)
{
arg0 = (IExpr/*!*/)cce.NonNull(app.Arguments[0]);
arg1 = (IExpr/*!*/)cce.NonNull(app.Arguments[1]);
arg2 = (IExpr/*!*/)cce.NonNull(app.Arguments[2]);
int i = 3; // Note ***3***
foreach(Matcher/*!*/ s in subs){
Contract.Assert(s != null);
if (!s(cce.NonNull((IExpr/*!*/)app.Arguments[i]))) { return false; }
i++;
}
return true;
}
else { return false; }
}
///
/// Not intended to be instantiated.
///
private ExprUtil() { }
}
//------------------------------ Symbols --------------------------------
///
/// 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.
///
[ContractClass(typeof(IFunctionSymbolContracts))]
public interface IFunctionSymbol
{
AIType/*!*/ AIType { [Rep][ResultNotNewlyAllocated]
get; }
}
[ContractClassFor(typeof(IFunctionSymbol))]
public abstract class IFunctionSymbolContracts:IFunctionSymbol{
#region IFunctionSymbol Members
AIType IFunctionSymbol.AIType {
get {
Contract.Ensures(Contract.Result() != null);
throw new NotImplementedException();
}
}
#endregion
}
///
/// The type of the arguments to ExprUtil.Match, a poor man's pattern
/// matching.
///
public interface IMatchable
{
}
//-------------------------------- Types --------------------------------
///
/// Types.
///
public interface AIType
{
}
///
/// Function type constructor.
///
public sealed class FunctionType : AIType
{
/*[Own]*/ private readonly IList/**//*!*/ argTypes;
/*[Own]*/ private readonly AIType/*!*/ retType;
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(argTypes != null);
Contract.Invariant(retType != null);
}
public FunctionType(params AIType[]/*!*/ types){
Contract.Requires(types != null);
Contract.Requires(types.Length >= 2);
AIType type = types[types.Length-1];
Contract.Assume(type != null);
this.retType = type;
ArrayList argTypes = new ArrayList();
for (int i = 0; i < types.Length-1; i++)
{
type = types[i];
Contract.Assume(type != null);
argTypes.Add(types);
}
this.argTypes = ArrayList.ReadOnly(argTypes);
}
public IList/**//*!*/ Arguments
{
[Pure][Rep]
get
{
Contract.Ensures(Contract.Result() != null);
Contract.Ensures(Contract.Result().IsReadOnly);
return argTypes;
}
}
public int Arity
{
get { return argTypes.Count; }
}
public AIType/*!*/ ReturnType
{
get {Contract.Ensures(Contract.Result() != null); 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 };
///
/// An interface that specifies a queryable object that can answer
/// whether a predicate holds.
///
///
[ContractClass(typeof(IQueryableContracts))]
public interface IQueryable
{
///
/// Answers the query whether the given predicate holds.
///
/// The given predicate.
/// Yes, No, or Maybe.
Answer CheckPredicate(IExpr/*!*/ pred);
///
/// A simplified interface for disequalities. One can always
/// implement this by calling CheckPredicate, but it may be
/// more efficient with this method.
///
Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2);
}
[ContractClassFor(typeof(IQueryable))]
public abstract class IQueryableContracts : IQueryable {
#region IQueryable Members
public Answer CheckPredicate(IExpr pred) {
Contract.Requires(pred != null);
throw new NotImplementedException();
}
public Answer CheckVariableDisequality(IVariable var1, IVariable var2) {
Contract.Requires(var1 != null);
Contract.Requires(var2 != null);
throw new NotImplementedException();
}
#endregion
}
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 CheckedException : System.Exception {
}
public class TypeError : CheckedException
{
}
}