blob: f46349b733b8de9303dff44e2774c5102e64910c (
plain)
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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
using System.Diagnostics.Contracts;
using System.Collections;
using System.Diagnostics;
//using System.Compiler;
using Microsoft.AbstractInterpretationFramework.Collections;
/// <summary>
/// Interface for a lattice that works on a per-variable basis.
/// </summary>
///
[ContractClass(typeof(MicroLatticeContracts))]
public abstract class MicroLattice : MathematicalLattice
{
/// <summary>
/// Returns the predicate on the given variable for the given
/// lattice element.
/// </summary>
public abstract IExpr/*!*/ ToPredicate(IVariable/*!*/ v, Element/*!*/ e);
/* requires !e.IsBottom && !e.IsTop; */
/// <summary>
/// Allows the lattice to specify whether it understands a particular function symbol.
///
/// The lattice is always allowed to "true" even when it really can't do anything with
/// such functions; however, it is advantageous to say "false" when possible to avoid
/// being called to do certain things.
///
/// The arguments to a function are provided for context so that the lattice can say
/// true or false for the same function symbol in different situations. For example,
/// a lattice may understand the multiplication of a variable and a constant but not
/// of two variables. The implementation of a lattice should not hold on to the
/// arguments.
/// </summary>
/// <param name="f">The function symbol.</param>
/// <param name="args">The argument context.</param>
/// <returns>True if it may understand f, false if it does not understand f.</returns>
public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);
/// <summary>
/// Set this property to true if the implemented MicroLattice can handle basic arithmetic.
/// Stated otherwise this property is set to true if the MicroLattice provides a transfer function for a predicate in a given state
/// </summary>
public virtual bool UnderstandsBasicArithmetics
{
get { return false; }
}
/// <summary>
/// Evaluate the predicate e and a yield the lattice element
/// that is implied by it.
/// </summary>
/// <param name="e">The predicate that is assumed to contain 1 variable.</param>
/// <returns>The most precise lattice element that is implied by the predicate.</returns>
public abstract Element/*!*/ EvaluatePredicate(IExpr/*!*/ e);
/// <summary>
/// Evaluate the predicate e and yield an overapproximation of the predicate under the state that is passed as a parameter
/// Note that unless the subclass implement it, the default behavior is to evaluate the predicate stateless, that implies that it
/// is evaluated in any possible context, i.e. it is an upper approximation
/// </summary>
public virtual Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ e, IFunctionalMap state){
Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
return EvaluatePredicate(e);
}
/// <summary>
/// Give an expression (often a value) that can be used to substitute for
/// the variable.
/// </summary>
/// <param name="e">A lattice element.</param>
/// <returns>The null value if no such expression can be given.</returns>
public abstract IExpr GetFoldExpr(Element/*!*/ e);
}
[ContractClassFor(typeof(MicroLattice))]
public abstract class MicroLatticeContracts : MicroLattice {
public override IExpr ToPredicate(IVariable v, MathematicalLattice.Element e) {
Contract.Requires(v != null);
Contract.Requires(e != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
throw new System.NotImplementedException();
}
public override bool Understands(IFunctionSymbol f, IList args) {
Contract.Requires(f != null);
Contract.Requires(args != null);
throw new System.NotImplementedException();
}
public override Element EvaluatePredicate(IExpr e) {
Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
throw new System.NotImplementedException();
}
public override IExpr GetFoldExpr(MathematicalLattice.Element e) {
Contract.Requires(e != null);
throw new System.NotImplementedException();
}
}
}
|
