1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
//-----------------------------------------------------------------------------
//
// 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 {
/// <summary>
/// Implementations of this interface determine how the heap is represented in
/// the translated Boogie program.
/// </summary>
public interface IHeap {
/// <summary>
/// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
/// on its type based on the heap representation.
/// </summary>
Bpl.Variable CreateFieldVariable(IFieldReference field);
/// <summary>
/// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
/// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
/// </summary>
Bpl.Variable CreateTypeVariable(ITypeReference type);
/// <summary>
/// Returns the (typed) BPL expression that corresponds to the value of the field
/// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
/// <paramref name="o"/> is non-null, otherwise the value of the static field.
/// </summary>
/// <param name="o">The expression that represents the object to be dereferenced.
/// Null if <paramref name="f"/> is a static field.
/// </param>
/// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
/// it is not null. Otherwise the static field whose value should be read.
/// </param>
Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f);
/// <summary>
/// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
/// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
/// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
/// field.
/// </summary>
Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value);
/// <summary>
/// Returns the BPL expression that corresponds to the value of the dynamic type
/// of the object represented by the expression <paramref name="o"/>.
/// </summary>
Bpl.Expr DynamicType(Bpl.Expr o);
}
public abstract class HeapFactory {
/// <summary>
/// Returns two things: an object that determines the heap representation,
/// and (optionally) an initial program that contains declarations needed
/// for the heap representation.
/// </summary>
/// <param name="sink">
/// The heap might need to generate declarations so it needs access to the Sink.
/// </param>
/// <returns>
/// false if and only if an error occurrs and the heap and/or program are not in a
/// good state to be used.
/// </returns>
public abstract bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program);
}
}
|
