In Jolden appears a rethrow instruction. We should add test about that feature.

try{

....

}
catch 
{
rethrow
}

Jolden required the implementation of boxing. I have not implemented yet the unboxing neither tests.

Not sure if this keyword is supported, neither how it should be implemented.

BCT models Real type as a new type declared in their Prelude. In TinyBCT we are using the real type supported by the Boogie language.

Not sure if we have seen how BCT works on this type.

Please add the file.

Are there bugs related with these two analyses? If that is the case, could @rcastano report it to Edgar?

https://github.com/m7nu3l/TinyBCT/blob/ca54386a6065d2213d5ac3344c299df4b7e523f4/TinyBCT/Traverser/Traverser.cs#L55

Exceptions in Boogie are handled with a global variable. Therefore you may have to pay attention about it being initialized.

After a call method the global exception variable is checked in order to propagate exceptions.

TinyBCT creates for each main method a wrapper, in which global variables are initialized (in addition static constructors are called).

The following test will document the behavior when a no main method is used as an entry point.

class ExceptionTestInitializeExceptionVariable
{
    // if this method is used as an entry point
    // global exception variable won't be initialized
    // after safe() is called, the exception variable could be on
    // because it was not initialized

    // TinyBCT generates a wrapper for each main method found 
    // wrappers initialize global variables

    public static void test()
    {
        try
        {
            safe();
        } catch (Exception ex)
        {
            Contract.Assert(false);
        }
    }
    public static void safe() {}
}

The example is in our test suite

    [TestMethod, Timeout(10000)]
    [TestCategory("Manu")]
    public void ExceptionTestInitializeExceptionVariable()
    {
        var corralResult = CorralTestHelper("Exceptions", "Test.ExceptionTestInitializeExceptionVariable.test", 10);
        Assert.IsTrue(corralResult.AssertionFails());
    }

Corral reports that the assertion can fail.

This was reported a while back by @m7nu3l and I'm not sure whether it was fixed. @m7nu3l, would you please add a repro or close this issue?

The following test (or a minor variation) causes Corral to produce a solver error.

https://github.com/m7nu3l/TinyBCT/blob/2c07a942196c350377a23670cb8e3b0742c7f2c0/TinyBCT/Tests/Tests.cs#L1471-L1477

We need to investigate the causes and file a bug report if necessary.

Currently we model casts as havocs in all cases. But we could avoid that for all casts among integers types or among floating point types (but not across).

String format for numbers greater than 1000 might fail.

While adding support for less frequent instructions, we often decide to approximate the desired behavior until the need for further precision/soundness arises.
We've also taken implementation decisions that are catered to the use cases we currently have in mind (angelic verification and generating enabledness preserving abstractions) but could lead to undesired results under other use cases.

It'd be ideal to find a way to gather all those implementation decisions and document them in one place.

Having CI set up within the repository would help us maintain a working version at all times and detect problems earlier.

This method can return null, check every dependency on that value. We want to eliminate the dependency on null values.

So far we've been directly generating strings to prototype and iterate quickly. At this point it'd help us to modularize the code and use the Boogie API.

Currently we model casts with havocs, but we don't consider the possibility of an InvalidCastException being thrown. We should consider whether we want to generate this in our translation.

We're making a number of changes in how we handle subtypes and dynamic dispatch. After we finish them we need to make sure our treatment of null values is correct.

This may already be supported, but make sure we have a test for it.

One of our use cases, EPA (enabledness preserving abstraction) generation, does not currently model dynamic dispatch soundly.
Also, the way we model dynamic dispatch is still fragile, so we might want to be able to isolate those issues from the rest of TinyBCT.

Current support is very rudimentary. It'd be ideal to find and document cases where it breaks, paying special attention to interactions with generics

We were blocked by an issue on analysis-net (edgardozoppi/analysis-net#4), as mentioned in issue #11, but I don't know if we have tests for this.

When using an open entry point (method with parameters), if we use objects from the heap, there aren´t any assumptions about its type. By propagating information from method parameters and load instructions, we can work around this.

In particular, test which extern methods are created.

Currently we can't handle these language constructs due to a bug in the backend: edgardozoppi/analysis-net#10

That feature is useful for this case: https://github.com/m7nu3l/TinyBCT/blob/6d8755c80785abc32001e3478ce52ce5fb027da6/TinyBCT/Tests/Tests.cs#L1392

Atomic initalization should be false by default, but true for those cases.

If they are not explictly initialized, they are not initialized in the boogie code.

We identified a possible bug but haven't been able to reproduce it yet.
My hypothesis is that the following assumption might lead to unexpected results, but I'm not sure what sort of assertion would be problematic.

void Foo(H<T> x) {
  assume Subtype(DynamicType(x), H($T()))
}

The potential fix would be to use assume TypeConstructor(DynamicType(x)) == H;.

I added a repro as a test:

https://github.com/m7nu3l/TinyBCT/blob/2c02f2670e7d8657e98a7d6ec31a56f3b287036e/TinyBCT/Tests/Tests.cs#L874-L904

We are currently modeling the heap as a single bi-dimensional map. This isn't a convenient representation for subsequent analyses on the Boogie code. The desired representation would emulate the treatment of BCT using the /heap:splitFields command line flag.

C# 7.0 includes ref returns and ref as local variables (pointers?).

More info: https://blogs.msdn.microsoft.com/dotnet/2016/08/24/whats-new-in-csharp-7-0/

We should support code like this:

            int a = 10;
            ref int reflocal = ref a;
            reflocal = 100;

The recent fix for issue #29 causes TinyBCT to generate larger Boogie files (longer axioms). We should try to find a way to resort to shorter axioms when possible.

This might deserve a more involved discussion and evaluation of the actual impact on performance.

Currently we list supported instructions in Helpers.IsInstructionImplemented(). Change the method so that we list unsupported instructions.

Here is an example of a loop translated by TinyBCT in which corral reaches the recursion bound. However the same loop translated by BCT, corral is able to prove no bugs without reaching the recursion bound.

The procedure (name in dll) is STATE$System_Collections2_Queue_ContainsSystem_Object$System_Collections2_Queue_EnqueueSystem_ObjectSystem_Collections2_Queue_ContainsSystem_ObjectSystem_Collections2_Queue_ContainsSystem_Object

It is declared in System.Collections2.Queue

The BCT version that I used is the present in contractor-net dependencies folder.

Queue.zip
Password: tinybct

We need this to try out TinyBCT checking for null dereferences and to later integrate with angelic verification.
We'd like to use the following notation: https://github.com/boogie-org/corral/blob/master/AddOns/PropInst/PropInst/ExampleProperties/nullcheck-razzle.avp

This is documented in the following test:

https://github.com/m7nu3l/TinyBCT/blob/6cf8a703ee6bc8af713ac2a3adb12fd13f954715/TinyBCT/Tests/Tests.cs#L852-L857

The test exercises the code in the following function:

https://github.com/m7nu3l/TinyBCT/blob/6cf8a703ee6bc8af713ac2a3adb12fd13f954715/Test/DynamicDispatch.cs#L309-L325

I think this is already working but we need to add tests.

Missing file in tests:
"Source file 'C:\Users\Doc\repos\TinyBCT\Test\Loops.cs' could not be found."

This was reported a while ago and may have been fixed already. @m7nu3l please add a repro or close this issue.

Test performance of AV with our translation using splitFields.

The following instructions are not implemented and required by Jolden.

• UnaryInstruction
• LoadTokenInstruction
• SwitchInstruction

LoadTokenInstruction appears in the Root class static constructor.

There seems to be a bug in the CHA.

The following test shows the problem:
https://github.com/m7nu3l/TinyBCT/blob/11ec3290ebc90edcdd01b416d06c50454cb6c51f/TinyBCT/Tests/Tests.cs#L754-L782

Derived.Foo appears to be missing from the call chain produced to simulate the dynamic dispatch. My first guess is that this has something to do with the CHA.

Curiously, if I remove the intermediate interface Base2, the problem disappears.

I think BCT uses 'NULL' whereas we use 'null'. This might create issues with angelic verification.

It would be useful to check whether we are creating any extern methods in Boogie for methods missing from the input dll.
Moreover, due to some bugs we found (#31), we also need to know which extern methods are created.

Setting up the project and running the tests require a few non-trivial steps which should be documented.

We also need documentation of the high-level architecture of the project and design/implementation decisions for new contributors.

Ideally we'd want to also have a few smaller 'nice to have' projects that are suitable as a first issue to work on.

Use if (ref != null) assert false; instead of just assert false;.

Model async as a synchronous method call

Currently subtyping axioms allow classes not present in the dll to exist. Another possibility would be to assume that only existing classes can occur.