Unsound analysis with regards to assemblies not referenced as input

Oct 6, 2013 at 8:45 PM
In the documentation for SEAL, one of the causes of unsound analysis is stated as referencing libraries other than the 3 standard .NET libraries and not specifying them as input.

My question is why SEAL is not conservative in its decision to mark a method as pure when that method includes a call to another method in an assembly that hasn't been specified as input.

For example, if I had MyExe.exe and Library.dll, and MyExe.exe depends on Library.dll the call to SEAL would need to look like this:
Checker.exe /in Library.dll /in MyExe.exe
In the case where either
Checker.exe /in MyExe.exe
Checker.exe /in MyExe.exe /in Library.dll
is specified instead, the results are incorrect. In particular, calls from MyExe.exe into Library.dll will be marked as pure even though they are not. That is, it doesn't appear SEAL is conservative when marking methods as pure when that method calls into an assembly it has not examined. It is one thing for the analysis to be incomplete, but it is another for the analysis to be wrong. I would expect SEAL to not make any judgments on methods that call into other assemblies that haven't been analyzed.

More concretely, if I have:
void UnpureFunction()
and Library is not specified or is out of order, UnpureFunction will be marked as pure by SEAL, even though it is not.

Is there a way to turn this behavior off? That is, in the example above, make it so SEAL wouldn't make a decision on UnpureFunction because it hasn't analyzed Library?

Oct 12, 2013 at 11:45 AM
Edited Oct 12, 2013 at 11:46 AM

Find below some general comments on handling calls to "unanalyzable procedures" which are procedures for which there exist no summary, and also some specific answers to your questions:

Conceptually, in the seal setting, there are 3 ways to handle unanalyzable procedure calls. For lack of a better name, I will refer to them as (a) optimistic (b) pessimistic (c) Lazy.

Optimistic Strategy:

The optimistic summary for a procedure assumes that the procedure is pure and returns a newly created object. This is the default behavior of seal. This is ofcouse unsound.

Pessimistic (Conservative) Strategy:

This is actually application dependent.
If one is interested only in purity then a pessimistic summary for a procedure shall assume that the procedure writes into some static field. This strategy will produce the most conservative answer for purity. It will mark all the transitive callers of the procedure as impure.
If one is also interested in conservatively estimating the side-effects then a conservative summary should consider all objects in the footprint of the procedure as written and should non-deterministically return any object belonging to the footprint.
If one is interested in the "points-to relations", then a conservative summary is very hard to construct. One heuristic would be to make every object in the footprint point to every other object but this is not the most conservative approximation (since the procedure may actually create new objects and assign them to the parameters).

But I hope these examples already illustrate that using a conservative summary (on real world programs) will in fact make the analysis results almost completely useless.
This broadly applies to many static analyses not just seal.

Lazy Strategy (unique to seal):

An alternative would be to treat the "unanalyzable procedure call" as an "indirect call" (see the tutorials for more details on how seal handles indirect calls).
In this strategy, the call will not be resolved and will be stored (along with the pointers to the arguments) in the summaries of the callers. The final side-effects output will actually list the call as an unresolved call. The clients can interpret these outputs as they wish ( pessimistically or optimistically).

However, the best way is to provide the library that contains the unanalyzable procedure or provide stubs that approximate the effects of the procedure.
You can also look at the "dllname-unanalyzable-calls.txt" to find the list of unanalyzable procedure calls encountered during the analysis and link the libraries (or stubs) that contain their implementation.

Changing the default behavior of seal

For this you have to modify the source code.
The method "SafetyAnalysis.Purity.Summaries.SummaryTemplates:: GetUnanalyzableCallSummary" (inside the directory StubManangers) creates a summary for the unanalyzable procedures. This method has to be modified appropriately. We already have support for a few heuristics.

The method "SummaryTemplates:: WriteGlobalObject" modifies a given summary so that it writes into a static field (passed as input). The method "ApplyReturnsStaticObjectSummary" modifies a given summary so that it returns a static field.
For eg:
the following code creates a summary of an unanalyzable procedure that writes into a static field and returns a static field.

public static PurityAnalysisData
    GetUnanalyzableCallSummary(string methodname, string containingType) 
        var data = SummaryTemplates.CreatePureData();

        var field = NamedField.New("Some-field","Some-Type")
        SummaryTemplates.ApplyReturnsStaticObjectSummary(data, field, methodname)

        return data;

Oct 12, 2013 at 2:36 PM
A correction to my earlier point regarding conservatively estimating the side-effects. On reflection, I think that is also very hard. Whatever I have described could also be unsound in some situations. So, in essence, it is only possible to conservatively estimate the purity information.
Oct 13, 2013 at 6:58 AM
Great response. Thank you. I may have follow up questions later but not at this moment.