blob: d38a37c0c473843febff37d3ca840f9b4e9bd5fe (
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
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
using Microsoft.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>
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)
{
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);
}
}
|
