Seal - guide

Getting started with Seal

Introduction

Seal is a research prototype that can infer the potential side-effects of methods in a C# program. The side-effects of a method are the set of heap locations in the program state right before the invocation of the method (referred to as prestate) that are modified (or written) by the method. Intuitively, these are the locations on which the method has an effect and hence can be expected to change after the method invocation. A method with no side-effects is said to be pure. Being a sound static analysis, Seal over-approximates the side-effects of a method but will never miss a true side-effect. However, there are few scenarios in which seal could be unsound (i.e, miss a real side-effect) which are discussed at the end of the tutorial. In the current state, Seal supports many sophisticated (and higher-order) C# features such as LINQ, delegates, event-handler, exceptions and so on.

Input to Seal

Seal takes as input a compilable C# program which need not necessarily be runnable. It is recommended that the programs only refer to types/methods defined in the following 3 .NET libraries (in addition to the types they define): mscorlib.dll, system.dll and system.core.dll. If the programs depend on any other (.NET or external) library then Seal could be unsound.

Understanding the output

Representation of side-effects

Seal outputs for each method in the input program its side-effects in the form of access-paths which is a handle to the modified prestate memory location from the variables live at the entry of the method (namely, parameters and static fields). Eg: load in editor

using System;
class Test {
    Test f;
    String g;
    public void ImpureMethod(Test param){       
        var x = param.f;
        x.g = "Hello";
    }            
}
The above method writes into the g field of the object referred to by the f field of param. In this case, Seal would emit param.f.g as the side-effect of the method. (Try making the param variable a static field !).

In some cases, particularly in the presence of recursive data-structures, a method can modify unbounded number of prestate objects. In such cases, Seal emits only a finite number of accesspaths. For example, try running the following sample program. load in editor

using System;
class Test {
    Test f;
    String g;
    public void ImpureMethod(Test param){              
        var x = param.f;
        while (x != null)
        {
            x.g = "Hello";
            x = x.f;
        }        
    }            
}

Handling of call-backs

In general, the side-effects of a method depends on the behavior of the methods called by it. For example, consider the following program in which the method C calls the methods B, A and writes into the f field of the return value of each of the methods. load in editor

using System;
class Test
{
    private int f = 0;
    public void C(Test param)
    {
        param.A().f = 3;
        param.B().f = 3;
    }
    public Test A()
    {
        return new Test();
    }
    public Test B()
    {
        return this;
    }
}
The method A returns a new object and hence writing its f field will not result in a side-effect whereas writing to the return value of B is basically a write to the parameter object param.

However, since we deal with open programs, it not possible to determine all the methods called by a method (particularly, in the presence of call-backs). Informally, a call-back is an indirect call (which could be a virtual method call, function pointer call or delegate call) whose targets become known only in the context of the callers of the method containing the indirect call. Eg: in the following code, the indirect call param.Equals(temp) is a call-back. load in editor

using System;
class Test
{
    //Object::Equals() method is a call-back which can potentially do anything
    public bool ConditionallyPureMethod(Object param)
    {
        var temp = new Test();
        return param.Equals(temp);
    }
}
Note that the actual target of param.Equals(temp) depends on the concrete type of param which could be inferred only when the callers of the above method are known.

The side-effects of methods having call-backs can be completely inferred only when the targets of the call-backs are known. For such methods, Seal emits all the side-effects inferred for the method (indpendent of the call-back) and also all the call-backs made by the method to indicate that the side-effects list is not complete. In some cases, due to the imprecision in the analysis, Seal can report more call-backs than what actually exist (but it would not miss a call-back).

Reasons for unsoundness

Sometimes you might find that seal is not able to find the side-effects in your code, it might be because of the following reasons:

Reporting Bugs

Seal is an ongoing research project, we are continuously working on ways to make it more robust, efficient and functional. If you come across any bugs/unexpected behavior in Seal please send the code that caused the bug and a brief description of the bug (like the expected output) to the following email address: [t-rakand at microsoft dot com]
Contact Us| Privacy & Cookies | Terms of Use | Trademarks| © 2021 Microsoft