//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Cci;
using Microsoft.Cci.MetadataReader;
using Microsoft.Cci.MutableCodeModel;
using Microsoft.Cci.Contracts;
using Microsoft.Cci.ILToCodeModel;
using Bpl = Microsoft.Boogie;
namespace BytecodeTranslator {
///
/// Implementations of this interface determine how the heap is represented in
/// the translated Boogie program.
///
public interface IHeap {
///
/// Creates a fresh BPL variable to represent , deciding
/// on its type based on the heap representation.
///
Bpl.Variable CreateFieldVariable(IFieldReference field);
/// Creates a fresh BPL variable to represent , deciding
/// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
///
Bpl.Variable CreateTypeVariable(ITypeReference type, List parents);
Bpl.Variable CreateEventVariable(IEventDefinition e);
///
/// Returns the (typed) BPL expression that corresponds to the value of the field
/// belonging to the object (which should be non-null).
///
/// The expression that represents the object to be dereferenced.
///
/// The field that is used to dereference the object .
///
Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType);
///
/// Returns the BPL command that corresponds to assigning the value
/// to the field of the object (which should be non-null).
///
Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType);
///
/// Returns the BPL expression that corresponds to the value of the dynamic type
/// of the object represented by the expression .
///
Bpl.Expr DynamicType(Bpl.Expr o);
}
public enum AccessType { Array, Heap, Struct };
public abstract class Heap : HeapFactory, IHeap
{
[RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Box;")]
public Bpl.Variable ArrayContentsVariable = null;
[RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]
public Bpl.Function ArrayLengthFunction = null;
public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
public abstract Bpl.Variable BoxField { get; }
#region Boogie Types
[RepresentationFor("Delegate", "type {:datatype} Delegate;")]
public Bpl.TypeCtorDecl DelegateTypeDecl = null;
public Bpl.CtorType DelegateType;
[RepresentationFor("DelegateMultiset", "type DelegateMultiset = [Delegate]int;")]
public Bpl.TypeSynonymDecl DelegateMultisetTypeDecl = null;
public Bpl.TypeSynonymAnnotation DelegateMultisetType;
[RepresentationFor("MultisetEmpty", "const unique MultisetEmpty: DelegateMultiset;")]
public Bpl.Constant MultisetEmpty = null;
[RepresentationFor("MultisetSingleton", "function {:inline} MultisetSingleton(x: Delegate): DelegateMultiset { MultisetEmpty[x := 1] }")]
public Bpl.Function MultisetSingleton = null;
[RepresentationFor("MultisetPlus", "function {:inline} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { mapadd(x, y) }")]
public Bpl.Function MultisetPlus = null;
[RepresentationFor("MultisetMinus", "function {:inline} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0)) }")]
public Bpl.Function MultisetMinus = null;
[RepresentationFor("Field", "type Field;")]
public Bpl.TypeCtorDecl FieldTypeDecl = null;
public Bpl.CtorType FieldType;
[RepresentationFor("Box", "type Box;")]
public Bpl.TypeCtorDecl BoxTypeDecl = null;
public Bpl.CtorType BoxType;
[RepresentationFor("$DefaultBox", "const unique $DefaultBox : Box;")]
public Bpl.Constant DefaultBox;
[RepresentationFor("Ref", "type Ref;")]
public Bpl.TypeCtorDecl RefTypeDecl = null;
public Bpl.CtorType RefType;
[RepresentationFor("null", "const unique null : Ref;")]
public Bpl.Constant NullRef;
[RepresentationFor("Type", "type {:datatype} Type;")]
public Bpl.TypeCtorDecl TypeTypeDecl = null;
public Bpl.CtorType TypeType;
[RepresentationFor("Real", "type Real;")]
protected Bpl.TypeCtorDecl RealTypeDecl = null;
public Bpl.CtorType RealType;
[RepresentationFor("$DefaultReal", "const unique $DefaultReal : Real;")]
public Bpl.Constant DefaultReal;
#endregion
#region Conversions
#region Heap values
[RepresentationFor("Box2Bool", "function Box2Bool(Box): bool;")]
public Bpl.Function Box2Bool = null;
[RepresentationFor("Box2Int", "function Box2Int(Box): int;")]
public Bpl.Function Box2Int = null;
[RepresentationFor("Box2Ref", "function Box2Ref(Box): Ref;")]
public Bpl.Function Box2Ref = null;
[RepresentationFor("Box2Real", "function Box2Real(Box): Real;")]
public Bpl.Function Box2Real = null;
[RepresentationFor("Bool2Box", "function Bool2Box(bool): Box;")]
public Bpl.Function Bool2Box = null;
[RepresentationFor("Int2Box", "function Int2Box(int): Box;")]
public Bpl.Function Int2Box = null;
[RepresentationFor("Ref2Box", "function Ref2Box(Ref): Box;")]
public Bpl.Function Ref2Box = null;
[RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]
public Bpl.Function Real2Box = null;
[RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]
public Bpl.Function Box2Box = null;
public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
Bpl.Function conversion;
if (boogieType == Bpl.Type.Bool)
conversion = this.Bool2Box;
else if (boogieType == Bpl.Type.Int)
conversion = this.Int2Box;
else if (boogieType == RefType)
conversion = this.Ref2Box;
else if (boogieType == RealType)
conversion = this.Real2Box;
else if (boogieType == BoxType)
conversion = this.Box2Box;
else
throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
var callConversion = new Bpl.NAryExpr(
tok,
new Bpl.FunctionCall(conversion),
new Bpl.ExprSeq(expr)
);
return callConversion;
}
public Bpl.Expr Unbox(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
Bpl.Function conversion = null;
if (boogieType == Bpl.Type.Bool)
conversion = this.Box2Bool;
else if (boogieType == Bpl.Type.Int)
conversion = this.Box2Int;
else if (boogieType == RefType)
conversion = this.Box2Ref;
else if (boogieType == RealType)
conversion = this.Box2Real;
else if (boogieType == BoxType)
conversion = this.Box2Box;
else
throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
var callExpr = new Bpl.NAryExpr(
tok,
new Bpl.FunctionCall(conversion),
new Bpl.ExprSeq(expr)
);
callExpr.Type = boogieType;
return callExpr;
}
#endregion
#region Real number conversions
[RepresentationFor("Int2Real", "function Int2Real(int): Real;")]
public Bpl.Function Int2Real = null;
[RepresentationFor("Real2Int", "function Real2Int(Real): int;")]
public Bpl.Function Real2Int = null;
#endregion
#region Real number operations
[RepresentationFor("RealPlus", "function RealPlus(Real, Real): Real;")]
public Bpl.Function RealPlus = null;
[RepresentationFor("RealMinus", "function RealMinus(Real, Real): Real;")]
public Bpl.Function RealMinus = null;
[RepresentationFor("RealTimes", "function RealTimes(Real, Real): Real;")]
public Bpl.Function RealTimes = null;
[RepresentationFor("RealDivide", "function RealDivide(Real, Real): Real;")]
public Bpl.Function RealDivide = null;
[RepresentationFor("RealModulus", "function RealModulus(Real, Real): Real;")]
public Bpl.Function RealModulus = null;
[RepresentationFor("RealLessThan", "function RealLessThan(Real, Real): bool;")]
public Bpl.Function RealLessThan = null;
[RepresentationFor("RealLessThanOrEqual", "function RealLessThanOrEqual(Real, Real): bool;")]
public Bpl.Function RealLessThanOrEqual = null;
[RepresentationFor("RealGreaterThan", "function RealGreaterThan(Real, Real): bool;")]
public Bpl.Function RealGreaterThan = null;
[RepresentationFor("RealGreaterThanOrEqual", "function RealGreaterThanOrEqual(Real, Real): bool;")]
public Bpl.Function RealGreaterThanOrEqual = null;
#endregion
#region Bitwise operations
[RepresentationFor("BitwiseAnd", "function BitwiseAnd(int, int): int;")]
public Bpl.Function BitwiseAnd = null;
[RepresentationFor("BitwiseOr", "function BitwiseOr(int, int): int;")]
public Bpl.Function BitwiseOr = null;
[RepresentationFor("BitwiseExclusiveOr", "function BitwiseExclusiveOr(int, int): int;")]
public Bpl.Function BitwiseExclusiveOr = null;
[RepresentationFor("BitwiseNegation", "function BitwiseNegation(int): int;")]
public Bpl.Function BitwiseNegation = null;
[RepresentationFor("RightShift", "function RightShift(int,int): int;")]
public Bpl.Function RightShift = null;
[RepresentationFor("LeftShift", "function LeftShift(int,int): int;")]
public Bpl.Function LeftShift = null;
#endregion
#endregion
///
/// Creates a fresh BPL variable to represent , deciding
/// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
///
public Bpl.Variable CreateTypeVariable(ITypeReference type, List parents)
{
string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
Bpl.IToken tok = type.Token();
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, this.TypeType);
Bpl.Constant v = new Bpl.Constant(tok, tident, true /*unique*/, parents, false, null);
return v;
}
public Bpl.Function CreateTypeFunction(ITypeReference type, int parameterCount) {
System.Diagnostics.Debug.Assert(parameterCount >= 0);
string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
Bpl.IToken tok = type.Token();
Bpl.VariableSeq inputs = new Bpl.VariableSeq();
//for (int i = 0; i < parameterCount; i++) {
// inputs.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "arg"+i, this.TypeType), true));
//}
foreach (var t in TranslationHelper.ConsolidatedGenericParameters(type)) {
var n = t.Name.Value;
var n2 = TranslationHelper.TurnStringIntoValidIdentifier(n);
inputs.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, n2, this.TypeType), true));
}
Bpl.Variable output = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "result", this.TypeType), false);
Bpl.Function func = new Bpl.Function(tok, typename, inputs, output);
var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "constructor", new List