boogie-org / symbooglix Goto Github PK

View Code? Open in Web Editor NEW

27.0 9.0 4.0 2.31 MB

Symbolic Execution Engine for Boogie

License: MIT License

C# 90.97% Python 0.67% Gnuplot 0.02% Shell 0.39% Dockerfile 0.34% Boogie 7.61%

symbolic-execution symbolic-execution-engine boogie

symbooglix's Introduction

Symbooglix

A symbolic execution engine for Boogie. A paper describing Symbooglix can be accessed here.

This project is currently at the research stage and so is not yet making stable releases.

Docker Image

A Docker image is available at https://hub.docker.com/r/symbooglix/symbooglix/

Dependencies

To build you will need:

Common dependencies

Git
Python
Z3 4.3.1 (avoid Z3 4.3.2, newer versions should be fine)
Boogie (obtained via a Git submodule)
NUnit 2.6.4 (obtained via NuGet on restore)
CommandLine (obtained via NuGet on restore)
System.Collections.Immutable (obtained via NuGet on restore)

If using Linux

Mono and related tools (I advise you use Monodevelop as your IDE)

If using Windows

You should install the "NUnit Test Adapter" in Visual Studio so you can run the unit tests.

Getting started

We use several git submodules for Symbooglix. Before you start you should initialise them by running

$ git submodule init
$ git submodule update

Building in Monodevelop or Visual Studio

You can load the src/Symbooglix.sln file into Visual Studio or Monodevelop and build from there.

We depend on several NuGet packages. Hopefully NuGet will automatically "restore" the packages we depend on but if not you may need to "restore them manually" before building.

Building on the command line (Linux/OSX)

We depend on several NuGet packages. To get these run

$ cd src
$ wget https://dist.nuget.org/win-x86-commandline/v2.8.6/nuget.exe
$ mono nuget.exe restore

Now if everthing went okay you can build Symbooglix by running

$ cd src/ # A symboolgix.sln file should be in this directory
$ mono nuget.exe restore symbooglix.sln
$ xbuild /p:Configuration=<BUILD_TYPE>

where <BUILD_TYPE> is Debug or Release.

Now make a symbolic link (or copy) to the the z3 executable and place it in the following directories:

src/SymbooglixDriver/bin/<BUILD_TYPE>/
src/Symbooglix/bin/<BUILD_TYPE>/

where <BUILD_TYPE> is the build type used to build Symbooglix.

Running your first Boogie program

$ mono src/SymbooglixDriver/<BUILD_TYPE>/Debug/sbx.exe test_programs/basic/symbolic/142.bpl

To see the available Symbooglix driver options run

$ mono src/SymbooglixDriver/<BUILD_TYPE>/Debug/sbx.exe --help

Testing

There are two forms of testing used for Symbooglix

NUnit tests

NUnit is used for unit testing. This comes preinstalled in mono but the version is too old so you need to obtain NUnit 2.6.4. When you built Symbooglix you will have already obtained the newer version of NUnit using NuGet.

These tests are easy to run from within monodevelop or Visual Studio (you need the NUnit Test Adapter add-on installed).

However you can run these tests from the console on Linux. To do so you need to obtain the NUnit.Runners NuGet package and then use a shell script to run the tests. Replace <BUILD_TYPE> with the build type you wish to test.

$ mono ./nuget.exe install -Version 2.6.4 NUnit.Runners
$ utils/run-unit-tests.sh NUnit.Runners.2.6.4/tools/nunit-console.exe <BUILD_TYPE>

Driver tests

The Symbooglix driver is sbx.exe. To test it install the lit and OutputCheck tools

$ pip install lit
$ pip install OutputCheck

Now to run the tests run

$ lit -s test_programs/

Symbooglix Driver Output

When the SymbooglixDriver (sbx.exe) runs it creates a directory named symbooglix-<N> (where is an increasing integer) which contains files detailing various parts of the execution. The can be disabled using --file-logging=0.

Here are some of the files and directories that you will find inside symbooglix-<N>.

instr_stats.callgrind - A file that can be given to KCacheGrind to visualise line coverage and the number of times certain branches were taken.
executor_info.yml - Statistics about the Execution engine.
terminated_states/ contains a file for each reporting how it terminated (emission of successful states can be suppressed using --skip-log-success-states, you may wish to use --skip-log-unsat-assume-states too).
nonterminated_states/ contains a file for each state that had not finished executing (i.e. due to hitting a global timeout).
termination_counters.yml - Reports the number of states by termination type where the termination type is non speculative
termination_counters_ONLY_SPECULATIVE.yml - Same as above but only reports speculative execution state. A speculative execution state is marked as speculative when a solver query fails (i.e. returns unknown or times out) and currently Symbooglix will kill an execution state when this occurs.
program.bpl - The transformed version of the Boogie program that Symbooglix actually executed on.

symbooglix's People

Contributors

Stargazers

Watchers

Forkers

shipeng331 soarlab ccadar seanpm2001

symbooglix's Issues

NotImplementedException: (_bvbuiltin not supported!

In issue #25 I reported an ArgumentException I was getting when running the SMACK tool on some test files using Symbooglix. I am also getting another exception on some other test files, which also only occurs when I pass the --bit-precise flag:

System.NotImplementedException: (_ bvbuiltin not supported!
at Symbooglix.BuilderDuplicator.HandleBvBuiltIns (Microsoft.Boogie.FunctionCall fc, System.String builtin, System.Collections.Generic.List`1[T] newArgs) [0x004dd] in <20b9c83e66a741738d0bf72150dda69a>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x0008b] in <20b9c83e66a741738d0bf72150dda69a>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00162] in <20b9c83e66a741738d0bf72150dda69a>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x0001e] in <20b9c83e66a741738d0bf72150dda69a>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00162] in <20b9c83e66a741738d0bf72150dda69a>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x0001e] in <20b9c83e66a741738d0bf72150dda69a>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00162] in <20b9c83e66a741738d0bf72150dda69a>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Symbooglix.Executor.Handle (Microsoft.Boogie.CallCmd c) [0x0008f] in <20b9c83e66a741738d0bf72150dda69a>:0
at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, T0 arg0, T1 arg1) [0x0003e] in <2392cff65f724abaaed9de072f62bc4a>:0
at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
at Symbooglix.Executor.ExecuteInstruction () [0x00091] in <20b9c83e66a741738d0bf72150dda69a>:0
at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, System.Int32 timeout) [0x001ea] in <20b9c83e66a741738d0bf72150dda69a>:0
at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, System.Int32 timeout) [0x0002b] in <20b9c83e66a741738d0bf72150dda69a>:0

Here's the bpl file for one of the failing test files:

mm.zip

The command used run Symbooglix was:

symbooglix mm.bpl --file-logging=0 --entry-points=main --timeout=1200 --max-depth=1

Here's a list of the failing test files (https://github.com/smackers/smack/tree/master/test):

bits/interleave_bits_fail.c
bits/interleave_bits_true.c
bits/mm.c
bits/mm_fail.c
bits/num_conversion_1_fail.c
bits/num_conversion_1_true.c
bits/num_conversion_2_fail.c
bits/num_conversion_2_true.c
bits/pointers4.c
bits/pointers4_fail.c
bits/pointers6.c
bits/pointers7.c
bits/pointers7_fail.c
bits/unaligned_struct.c
bits/unaligned_struct_fail.c

Set up Windows continuous integration build

We may have users under Windows so to ensure that Symbooglix builds we should set up some sort of CI build. Perhaps AppVeyor would be a good choice.

ArgumentException: the decimal value cannot be represented in the requested number of bits

I am currently working on integrating Symbooglix into the SMACK (https://github.com/smackers/smack) tool. To test the integration, I am running SMACK with Symbooglix on an existing set of test files that we have. You can find these tests at the URL (https://github.com/smackers/smack/tree/master/test/basic). On a fraction of the tests, I am getting the following error:

System.ArgumentException: Decimal value cannot be represented in the requested number of bits
at Symbooglix.SimpleExprBuilder.ConstantBV (System.Numerics.BigInteger decimalValue, System.Int32 bitWidth) [0x0004c] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.ConstantCachingExprBuilder.ConstantBV (System.Numerics.BigInteger decimalValue, System.Int32 bitWidth) [0x0003d] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.DecoratorExprBuilder.ConstantBV (System.Numerics.BigInteger decimalValue, System.Int32 bitWidth) [0x00000] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.ConstantFoldingExprBuilder.BVSUB (Microsoft.Boogie.Expr lhs, Microsoft.Boogie.Expr rhs) [0x000ac] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.BuilderDuplicator.HandleBvBuiltIns (Microsoft.Boogie.FunctionCall fc, System.String builtin, System.Collections.Generic.List`1[T] newArgs) [0x00234] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x0008b] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00162] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x0001e] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00162] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x0001e] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) [0x00162] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) [0x00000] in <7d6f451acda54bc3924b6a08150488e4>:0
at Symbooglix.Executor.Handle (Microsoft.Boogie.AssignCmd c) [0x00216] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, T0 arg0, T1 arg1) [0x0003e] in <2392cff65f724abaaed9de072f62bc4a>:0
at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
at Symbooglix.Executor.ExecuteInstruction () [0x00091] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, System.Int32 timeout) [0x001ea] in <74bcd1aa61a246f0ad776e754de5a5c3>:0
at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, System.Int32 timeout) [0x0002b] in <74bcd1aa61a246f0ad776e754de5a5c3>:0

The tests I am getting the error on are:

basic/big_numbers.c
basic/big_numbers_fail.c
basic/func_ptr_alias.c
basic/func_ptr_alias_fail.c
basic/gcd.c
basic/jain_1_true.c
basic/jain_2_true.c
basic/jain_4_true.c
basic/nondet.c
basic/return_label.c
basic/two_arrays2.c
basic/two_arrays3.c
basic/two_arrays4.c
basic/two_arrays5.c
basic/two_arrays6.c
basic/two_arrays6_fail.c
bits/absolute.c
bits/absolute_fail.c

In addition, these tests only get this error when I pass the SMACK flag '--bit-precise', which enables bit precision for non-pointer values. When I do not pass this flag, the tests run without error.

Switching symbooglix to MIT license (instead of BSD-2)

So I am a member of a team what has been working on automatic testing of Dafny programs. We are really interested in potentially rebooting symbooglix to use it in this context. Given that the team involves Amazon employees, to be able to contribute to symbooglix, it would be really helpful if its license would be the same as other Boogie-related projects such as Boogie, Corral, Dafny, which are all under MIT license.

Could we place switch symbooglix to MIT license to make it totally in sync with other related projects?

Please let me know. Thanks!

Throwing System.ArgumentNullException

This is the bpl file in question: driver.zip
This is how I invoke Symbooglix:

symbooglix driver.bpl --file-logging=0 --entry-points=main --timeout=1200 --max-loop-depth=1

This is the exception I get:

System.ArgumentNullException: Value cannot be null.
Parameter name: key
  at System.ThrowHelper.ThrowArgumentNullException (System.ExceptionArgument argument) [0x00006] in <a07d6bf484a54da2861691df910339b1>:0 
  at System.Collections.Generic.Dictionary`2[TKey,TValue].FindEntry (TKey key) [0x00008] in <a07d6bf484a54da2861691df910339b1>:0 
  at System.Collections.Generic.Dictionary`2[TKey,TValue].get_Item (TKey key) [0x00000] in <a07d6bf484a54da2861691df910339b1>:0 
  at Microsoft.Boogie.GraphUtil.Graph`1[Node].Predecessors (Node n) [0x00006] in <693cbe2cdcc8426c908d825c4ff59b0e>:0 
  at Microsoft.Boogie.GraphUtil.DomRelation`1[Node].NewComputeDominators () [0x000a8] in <693cbe2cdcc8426c908d825c4ff59b0e>:0 
  at Microsoft.Boogie.GraphUtil.DomRelation`1[Node]..ctor (Microsoft.Boogie.GraphUtil.Graph`1[Node] g, Microsoft.Boogie.Block source) [0x00014] in <693cbe2cdcc8426c908d825c4ff59b0e>:0 
  at Microsoft.Boogie.GraphUtil.Graph`1[Node].get_DominatorMap () [0x00008] in <693cbe2cdcc8426c908d825c4ff59b0e>:0 
  at Microsoft.Boogie.GraphUtil.Graph`1[Node].ComputeReducible (Microsoft.Boogie.GraphUtil.Graph`1[Node] g, Node source) [0x00000] in <693cbe2cdcc8426c908d825c4ff59b0e>:0 
  at Microsoft.Boogie.GraphUtil.Graph`1[Node].ComputeLoops () [0x00000] in <693cbe2cdcc8426c908d825c4ff59b0e>:0 
  at Symbooglix.ProgramLoopInfo.InitLoopInfo () [0x00022] in <692639236925446fa5df88fd5bc64c13>:0 
  at Symbooglix.ProgramLoopInfo..ctor (Microsoft.Boogie.Program p) [0x00018] in <692639236925446fa5df88fd5bc64c13>:0 
  at Symbooglix.LimitLoopBoundScheduler.ReceiveExecutor (Symbooglix.Executor executor) [0x0000f] in <692639236925446fa5df88fd5bc64c13>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, System.Int32 timeout) [0x000bd] in <692639236925446fa5df88fd5bc64c13>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, System.Int32 timeout) [0x0004f] in <692639236925446fa5df88fd5bc64c13>:0 
  at SymbooglixDriver.Driver.RealMain (System.String[] args) [0x0059f] in <bdc3582f735c4c9c95912485e1b8fe43>:0 
  at SymbooglixDriver.Driver.Main (System.String[] args) [0x0003a] in <bdc3582f735c4c9c95912485e1b8fe43>:0 
Exiting with EXCEPTION_RAISED

Support triggers on quantified expressions

Fix horrible constructors

The constructors of many important classes (e.g. Executor and the solver classes) are a mess. We need to create some sort of config object for each of these so that when we add/remove a parameter it doesn't require massive changes that end up propagating all over the code base.

Fix performance regression on SVCOMP benchmark suite

ldv-consumption/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c_.bpl
snapshot-11-effctclone/merged.yml : FinalResultType.BUG_FOUND (/tmp/pbs.1346865.cx1b/wd/workdir-1270) (444.8166378069727 secs)
snapshot-12/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.1346866.cx1b/wd/workdir-1270) (900.0 secs)

Update CI Travis script

CI is failing due to not being able to install Z3. We should update the CI script to a newer version of Ubuntu/Z3, which will likely fix this problem too.

Symbooglix missing a bug

We identified this as an example that it seems causes for Symbooglix to miss a bug:
array2_free_fail.zip

No bugs are reported when Symbooglix is executed on this bpl file like this:

symbooglix array2_free_fail.bpl --file-logging=0 --entry-points=main --timeout=1200 --max-loop-depth=1

On the other hand, Corral does report a bug as expected:

corral array2_free_fail.bpl /noTraceOnDisk /k:1 /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1

This is a fairly simple example, and I do have to wonder if this problem is due to our usage of quantifiers.

Use call graph information in GlobalDDE

We can potentially remove more dead declarations if we first remove all procedures that are not reachable (via calls) from the entry point

Fix performance regression on GPU benchmark suite

Here are some notable changes for the fully explored benchmarks.

Size of uncommon results for all FULLY_EXPLORED: 4
shoc/s3d/qssab/kernel.bpl
snapshot-9-mapconstidx/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.1302100.cx1b/wd/workdir-543) (894.2382166739553 secs)
snapshot-12/merged.yml : FinalResultType.TIMED_OUT (/tmp/pbs.1296550.cx1b/wd/workdir-543) (900.0 secs)

CUDA50/6_Advanced/fastWalshTransform/fwtBatch1Kernel.bpl
snapshot-9-mapconstidx/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.1296547.cx1b/wd/workdir-247) (900.0 secs)
snapshot-12/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.1296550.cx1b/wd/workdir-247) (67.72944867641975 secs)

gpgpu-sim_ispass2009/RAY/renderPixel.bpl
snapshot-9-mapconstidx/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.1296547.cx1b/wd/workdir-385) (14.94364638502399 secs)
snapshot-12/merged.yml : FinalResultType.TIMED_OUT (/tmp/pbs.1296550.cx1b/wd/workdir-385) (900.0 secs)

shoc/devicememory/readGlobalMemoryCoalesced/kernel.bpl
snapshot-9-mapconstidx/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.1296547.cx1b/wd/workdir-498) (21.07033052512755 secs)
snapshot-12/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.1296550.cx1b/wd/workdir-498) (900.0 secs)

GlobalDeadDeclEliminationPass should remove unused procedures/implementations

Currently we don't try to remove procedures and/or implementations. There's no reason we can't do this.

Fix or remove the CachingSymbolicPool

The CachingSymbolicPool was added so that Symbolic variables could be shared between states after they forked. The SimpleSymbolicPool does not share symbolic variables between states after they forked. Sharing Symbolic variables would in principle reduce memory usage and might enable more solver caching hits.

Unfortunately the current implementation is broken and therefore disabled

It works correctly on this example (both states share the same symbolic version of y after forking).

procedure main()
{
    var x:int;
    var y:int;

    if ( x > 0 )
    {
        assert x == x;
    }
    else
    {
        assume x == x;
    }

    havoc y;

    assume x != y;
}

but it fails with this example.

procedure main()
{
var x:int;
var y:int;

if ( x > 0 )
{
   havoc y;
}
else
{
    havoc y;
}

havoc y;

assume x != y;

}

The problem in the second example is that the havoc y commands inside the if and else branch should return the same symbolic in each state but in the existing implementation they don't. The current implementation makes the mistake of trying to use a symbolic creation site as a key for caching symbolics. Really what we need to cache on is just the variable itself.

Examine inconsistency in ICST2016 results

When running all the snapshots there is an inconsistency between the original run on our computing cluster and the run performed at a later date on snapshot-12. Snapshot-12 and the version of Symbooglix used for the tool comparision in the ICST2016 paper are identical versions (using identical mono and Z3 versions). The version of boogie-runner might not be identical though.

Size of uncommon results for all FULLY_EXPLORED: 4
shoc/md/kernel.bpl
../../sbx-processed-results/forth/gv/symbooglix/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.9533759.cx1b/wd/workdir-534) (610.261797192196 secs)
snapshot-12/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.1296550.cx1b/wd/workdir-534) (900.0 secs)

shoc/devicememory/readGlobalMemoryCoalesced/kernel.bpl
../../sbx-processed-results/forth/gv/symbooglix/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.9533757.cx1b/wd/workdir-498) (29.931226284553606 secs)
snapshot-12/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.1296550.cx1b/wd/workdir-498) (900.0 secs)

shoc/devicememory/readConstantMemoryCoalesced/kernel.bpl
../../sbx-processed-results/forth/gv/symbooglix/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.9533757.cx1b/wd/workdir-497) (900.0 secs)
snapshot-12/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.1296550.cx1b/wd/workdir-497) (12.395383157767355 secs)

AMD_SDK/BitonicSort/kernel.bpl
../../sbx-processed-results/forth/gv/symbooglix/merged.yml : FinalResultType.FULLY_EXPLORED (/tmp/pbs.9533757.cx1b/wd/workdir-8) (661.6344245672226 secs)
snapshot-12/merged.yml : FinalResultType.UNKNOWN (/tmp/pbs.1296550.cx1b/wd/workdir-8) (900.0 secs)

missing axiom definition in constraints

I have two version of a program, which are are almost identical except that one program features an additional procedure. This additional procedure involves an axiom, which is present in both versions but used only in one version of them. Executing the equivalent procedure in both versions generates different constraints though. See the following example for details:

Version A:
For procedure someMethodWeWantToExecuteSymbolically in version A, the constraint: [Cmd] assume {:partition} localBoolean; is generated. No information about the axiom is available.

// ---------------------------------------------------------------
// ---------------------------- HEAP -----------------------------
// ---------------------------------------------------------------
type Ref;

type Int;
type Bool;

type BoolHeap = [Ref][Bool] bool;
type IntHeap  = [Ref][Int]  int;
type ObjHeap  = [Ref][Ref]  Ref;

var boolHeap : BoolHeap;
var intHeap  : IntHeap;
var objHeap  : ObjHeap;

var null : Ref;

// ---------------------------------------------------------------
// ---------------------------- CODE -----------------------------
// ---------------------------------------------------------------

// FIELDS

var globalBooleanArray$array : [int] Bool;
var globalBooleanArray$field : Ref;

const globalBooleanArray$size : int;
axiom globalBooleanArray$size == 5;


// METHODS

procedure someMethodWeWantToExecuteSymbolically()
 modifies boolHeap, intHeap, objHeap;
{
 // INIT
 var localBoolean : bool;

 // BODY
 if (localBoolean) {
  localBoolean := false;
 }
}

Version B
Executing procedure someMethodWeWantToExecuteSymbolically in version B, generated the constraints [Cmd] assume {:partition} localBoolean; and [Axiom] globalBooleanArray$size == 5.

// ---------------------------------------------------------------
// ---------------------------- HEAP -----------------------------
// ---------------------------------------------------------------
type Ref;

type Int;
type Bool;

type BoolHeap = [Ref][Bool] bool;
type IntHeap  = [Ref][Int]  int;
type ObjHeap  = [Ref][Ref]  Ref;

var boolHeap : BoolHeap;
var intHeap  : IntHeap;
var objHeap  : ObjHeap;

var null : Ref;

// ---------------------------------------------------------------
// ---------------------------- CODE -----------------------------
// ---------------------------------------------------------------

// FIELDS

var glbalBooleanArray$array : [int] Bool;
var globalBooleanArray$field : Ref;

const globalBooleanArray$size : int;
axiom globalBooleanArray$size == 5;


// METHODS

procedure someMethodWeWantToExecuteSymbolically()
 modifies boolHeap, intHeap, objHeap;
{
 // INIT
 var localBoolean : bool;

 // BODY
 if (localBoolean) {
  localBoolean := false;
 }
}

procedure someOtherMethodWeDoNotWantToExecuteSymbolically()
 modifies boolHeap, intHeap, objHeap;
{
 // INIT
 
 // BODY
 if (globalBooleanArray$size > 0) {
 
 }
}

Is this the desired behaviour? Shouldn't the information about the axiom be present in both version of the program?

Improper use of Boogie Graph class

boogie-org/boogie#92

The issue above seems to be really an issue in Symbooglix.

Fix messed up build types

When doing a release build the platform has to be set to X86 rather than all.

SMTLIBQueryPrinter emits too many spaces when not in human readable mode

SMTLIBQueryPrinter emits too many spaces when not in human readable mode. The problem is that the class conflates separators with new lines. Several tests depend on this behaviour which is going to cause problems. It is also not very efficient to emit spaces for no good reason.

We should fix the design and then fix those tests.

Add patterns to MapProxy

The MapProxy class only looks for non alias expressions that match the pattern <var> + <const> when handling non-aliasing expressions that are used as indices. We can generalise this to

<expr> + <const> and <expr> - <const> (these can co-exist and do not alias). We can also the same for bitvectors provided we check that we don't allow overflowing bitvector constants (I don't think we do).
<expr> * <const> (need to be careful when <const> == 0 as this aliases <expr>)

GlobalDeadDeclEliminationPass leaves unused functions

I found some unused functions left in the output file processed by this pass. The input file is a Boogie program generated by SMACK. I think the reason is that class FindUsedFunctionAndGlobalVariableVisitor visits functions with bodies first and add function calls to used function hashset. While these functions are not actually used if their callers are not used. (https://github.com/symbooglix/symbooglix/blob/master/src/Symbooglix/Transform/GlobalDeadDeclEliminationPass.cs#L278-L287)

Split Symbooglix.dll

It should be split into separate components.

GlobalDDE fails remove dead functions and axioms involving bitvector functions

This issue was report by @akashlal

Here's an example program that triggers the bug

function {:bvbuiltin "bvadd"} BVADD32(bv32,bv32) returns (bv32);

// GlobalDDE fails to remove this dead function and axiom because
// it conservatively assumes that the used BVADD32 is related to
// ADD_ONE and because BVADD32 is used that the axiom might constrain
// BVADD32's behaviour in someway
function ADD_ONE(bv32) returns (bv32);
axiom (forall x:bv32 :: ADD_ONE(x) == BVADD32(x, 1bv32));


procedure main() {
    var x:bv32;
    var y:bv32;

    x := BVADD32(x, y);
    assert x == BVADD32(x, y);
}

Investigate poor unit test performance

With different versions of mono the time taken to execute the unit tests seems to have significantly regressed.

Mono 4.4.1

Tests run: 256, Errors: 0, Failures: 0, Inconclusive: 0, Time: 173.8809436 seconds
  Not run: 14, Invalid: 0, Ignored: 14, Skipped: 0

Mono 3.4.0

Tests run: 256, Errors: 0, Failures: 0, Inconclusive: 0, Time: 7.9253886 seconds
  Not run: 14, Invalid: 0, Ignored: 14, Skipped: 0

Investigate test failures with Mono 4.4.2

Looks like the TravisCI build is failing.

Symbooglix.Solver.SolverErrorException

I am translating Java code to Boogie code for symbolic execution and run into an issue when using arrays within nested single arity maps.

// ######################################
// #        HEAP & LOCAL VARIABLES      #
// ######################################
type Ref;

type Bool;

type BoolHeap = [Ref][Bool] bool;

var boolHeap : BoolHeap;

// ######################################    
// #              METHODS               #
// ######################################

var array : [int] Bool;

const array$size : int;
axiom array$size == 5;

procedure someFunction(this : Ref) returns ()
{
 var pos   : int;
 var field : Bool;
 var value : bool;

 pos   := 0;
 field := array[pos]
 value := boolHeap[this][field];
  
 if (value) {
  
 }
}

Executing this example throws the following Symbooglix.Solver.SolverErrorException:

Symbooglix.Solver.SolverErrorException: (error "line 3 column 50: Invalid function declaration: unknown sort '@Bool'")(error "line 5 column 39: Invalid function declaration: unknown sort '@Bool'")
  at Symbooglix.Solver.SimpleSMTLIBSolver.ComputeSatisfiability (Symbooglix.Solver.Query query) <0x44ccb10 + 0x003cb> in <filename unknown>:0 
  at Symbooglix.Solver.ConstraintIndependenceSolver.ComputeSatisfiability (Symbooglix.Solver.Query query) <0x44cb070 + 0x00347> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSolver.InternalComputeSatisfiability (Symbooglix.Solver.Query query) <0x44ca958 + 0x000db> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSolver.CheckSatisfiability (Symbooglix.Solver.Query query) <0x44ca8e8 + 0x00027> in <filename unknown>:0 
  at Symbooglix.Executor.LookAheadGotoFork (Microsoft.Boogie.GotoCmd c) <0x44c8998 + 0x0052c> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.GotoCmd c) <0x44c8900 + 0x0003b> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x41fdeb0 + 0x00425> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at Symbooglix.Executor.ExecuteInstruction () <0x41facf8 + 0x001a4> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2d8ed00 + 0x0048b> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2d8e938 + 0x000c3> in <filename unknown>:0 
Exiting with EXCEPTION_RAISED

Add proper query logging mechanism

The current query logging mechanism is inadequate because what gets logged isn't necessarily isn't what gets feed to the solver. We should add a TextWriter wrapper that writes to an underlying TextWriter but also logs to a file to fix this.

AssertionFailingException: Incorrect number of arguments

I want to run Symbooglix to generate traces that show the interaction between two given methods. In the following example, procedure a simply checks the given condition c and returns an output o. The variable v within the abstracted heap is set to 2 if condition c holds; otherwise the abstracted heap remains unchanged. When executing procedure b, the variable v is checked for its value, which results in different calls to procedure a:

// ######################################
// #        HEAP & LOCAL VARIABLES      #
// ######################################

type Ref;
type Int;

type IntHeap = [Ref, Int] int;
var intHeap : IntHeap;

var this : Ref;

var v : Int;

// ######################################    
// #              METHODS               #
// ######################################

procedure a(c : bool) returns (o : int)
 modifies intHeap;
{
 if (c == true) {
  intHeap[this,v] := 2; 
  o := 0;
 } else {
  o := 100;
 }
 return;
}

procedure b() returns (o : int)
 modifies intHeap;
{
 if (intHeap[this,v] == 2) {
  call o := a(false);
 } else {
  call o := a(true);
 }
 return;
}

When I run the example using Symbooglix with procedure b as an entry point, I receive the following exception though:

Symbooglix.AssertionFailingException: Incorrect number of arguments : 
  at Symbooglix.ExceptionThrowingTextWritierTraceListener.Fail (System.String message, System.String detailMessage) <0x45bf940 + 0x00083> in <filename unknown>:0 
  at System.Diagnostics.TraceListener.Fail (System.String message) <0x45df878 + 0x00022> in <filename unknown>:0 
  at Symbooglix.ExceptionThrowingTextWritierTraceListener.Fail (System.String message) <0x45bf8f0 + 0x00017> in <filename unknown>:0 
  at System.Diagnostics.TraceInternal.Fail (System.String message) <0x45df2e8 + 0x00144> in <filename unknown>:0 
  at System.Diagnostics.TraceInternal.Assert (Boolean condition, System.String message) <0x2e28490 + 0x0001b> in <filename unknown>:0 
  at System.Diagnostics.Debug.Assert (Boolean condition, System.String message) <0x2e28460 + 0x0001b> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.PrintBinaryOperator (System.String name, Microsoft.Boogie.NAryExpr e) <0x45dde78 + 0x0003f> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.VisitMapSelect (Microsoft.Boogie.NAryExpr e) <0x45df2c0 + 0x0001f> in <filename unknown>:0 
  at Symbooglix.Traverser.HandleNAry (Microsoft.Boogie.NAryExpr e) <0x45dd6a8 + 0x0050f> in <filename unknown>:0 
  at Symbooglix.Traverser.Visit (Microsoft.Boogie.Expr e) <0x45dd1a8 + 0x00073> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter+SMTLIBTraverser.Traverse (Microsoft.Boogie.Expr root) <0x45dd180 + 0x00017> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.PrintExpr (Microsoft.Boogie.Expr root) <0x45dce20 + 0x000cd> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.PrintBinaryOperator (System.String name, Microsoft.Boogie.NAryExpr e) <0x45dde78 + 0x000e7> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.VisitEq (Microsoft.Boogie.NAryExpr e) <0x45dde48 + 0x0001f> in <filename unknown>:0 
  at Symbooglix.Traverser.HandleNAry (Microsoft.Boogie.NAryExpr e) <0x45dd6a8 + 0x00328> in <filename unknown>:0 
  at Symbooglix.Traverser.Visit (Microsoft.Boogie.Expr e) <0x45dd1a8 + 0x00073> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter+SMTLIBTraverser.Traverse (Microsoft.Boogie.Expr root) <0x45dd180 + 0x00017> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.PrintExpr (Microsoft.Boogie.Expr root) <0x45dce20 + 0x000cd> in <filename unknown>:0 
  at Symbooglix.SMTLIBQueryPrinter.PrintAssert (Microsoft.Boogie.Expr e) <0x45dcb68 + 0x00077> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSMTLIBSolver.ComputeSatisfiability (Symbooglix.Solver.Query query) <0x45da340 + 0x00323> in <filename unknown>:0 
  at Symbooglix.Solver.ConstraintIndependenceSolver.ComputeSatisfiability (Symbooglix.Solver.Query query) <0x45d86f0 + 0x00403> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSolver.InternalComputeSatisfiability (Symbooglix.Solver.Query query) <0x45d7fa8 + 0x000e9> in <filename unknown>:0 
  at Symbooglix.Solver.SimpleSolver.CheckSatisfiability (Symbooglix.Solver.Query query) <0x45d7f38 + 0x00027> in <filename unknown>:0 
  at Symbooglix.Executor.LookAheadGotoFork (Microsoft.Boogie.GotoCmd c) <0x45be820 + 0x00570> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.GotoCmd c) <0x45be728 + 0x0005b> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x431bfb0 + 0x00425> in <filename unknown>:0 
  at Symbooglix.Executor.ExecuteInstruction () <0x430e6f8 + 0x001b4> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2e2e218 + 0x004eb> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2e2de40 + 0x000c3> in <filename unknown>:0

Does Symbooglix allow to identify the trace that procedure a has to be called before procedure b in order to satisfy the conditional statement within procedure b and am I doing it right?

Handle multi-arity maps correctly

I run symbooglix on a programs, i.e., Example.bpl.txt, which abstracts a heap representation. The program looks fine when running it with boogie but throws the following exception related to my heap abstraction and a type mismatching when verifying it using symbooglix.

Symbooglix.ExprTypeCheckException: Type mismatch at index 0 expected type Ref but was type Field int
  at Symbooglix.MapProxy.TypeCheckIndices (IList`1 indices) <0x46bcb98 + 0x0028f> in <filename unknown>:0 
  at Symbooglix.MapProxy.ReadMapAt (IList`1 indices) <0x46bc988 + 0x00023> in <filename unknown>:0 
  at Symbooglix.SimpleVariableStore.ReadMap (Microsoft.Boogie.Variable mapVariable, IList`1 indicies) <0x46bc888 + 0x0006b> in <filename unknown>:0 
  at Symbooglix.ExecutionState.ReadMapVariableInScopeAt (Microsoft.Boogie.Variable v, IList`1 indices) <0x46bc7a8 + 0x00080> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x46bb1e8 + 0x00327> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x2df1e00 + 0x0001a> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x2f16808 + 0x00017> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x46a4c28 + 0x00017> in <filename unknown>:0 
  at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x46bb658 + 0x000a0> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x46bb1e8 + 0x00343> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x2df1e00 + 0x0001a> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x2f16808 + 0x00017> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x46a4c28 + 0x00017> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.AssignCmd c) <0x46ba000 + 0x0097e> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x4400000 + 0x00425> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at Symbooglix.Executor.ExecuteInstruction () <0x43f0718 + 0x001b4> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2f13b48 + 0x004eb> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2f13770 + 0x000c3> in <filename unknown>:0

Support reporting reasons for solver responding with UNKNOWN

Right now if the solver times out this information is not communicated. We should provide an interface for getting this information and report when this happens to aid debugging.

Fix driver test under release build and enable Travis release build

Fix

basic/concrete/infeasible_ensures.bpl

under release build and enable release build under TravisCI.

Adding support for specifying loop/recursion unroll bounds

We have made (mainly @liammachado) some traction on integration symbooglix into the SMACK toolflow. One annoying issue that we identified is that symbooglix does not support specifying loop/recursion unroll bounds as a command line argument.
This was already discussed here:
https://github.com/smackers/smack/pull/155/files/98852f442e711acc042ad7285d7b2864754e127f#r58845496
This is quite inconvenient since at this point we do not have the same (or at least very similar) unroll semantics between Corral and symbooglix. So I am wondering if someone could maybe implement this features, it would be really helpful.

Allow polymorphic map types created using type constructors

Symbooglix cannot currently run this

// ######################################
// #         HEAP INITIALISATION        #
// ######################################
type Ref;
type Field a;
type Heap = <a> [Ref, Field a] a;

const unique null : Ref;
const unique alloc : Field bool;

var heap : Heap;

// ######################################    
// #          LOCAL VARIABLES           #
// ######################################

var this : Ref;
var time : Field int;
var value : Field int;
var error : Field bool;

// ######################################    
// #             SYMBOOGLIX             #
// ######################################

procedure main(i : int)
{
 var o : int;
 call o := getElapsedTime(i);
}

// ######################################    
// #              METHODS               #
// ######################################

procedure getElapsedTime(t : int) returns (r : int)
 ensures heap == old(heap);
{
 r := heap[this,time] - t;
}

This is not supported by the MapProxy and causes an exception to be raised when type checking

Symbooglix.ExprTypeCheckException: Type mismatch at index 1 expected type Field a but was type Field int
  at Symbooglix.MapProxy.TypeCheckIndices (IList`1 indices) <0x40c3b140 + 0x002c7> in <filename unknown>:0 
  at Symbooglix.MapProxy.ReadMapAt (IList`1 indices) <0x40c3af10 + 0x00037> in <filename unknown>:0 
  at Symbooglix.SimpleVariableStore.ReadMap (Microsoft.Boogie.Variable mapVariable, IList`1 indicies) <0x40c3ae00 + 0x00077> in <filename unknown>:0 
  at Symbooglix.ExecutionState.ReadMapVariableInScopeAt (Microsoft.Boogie.Variable v, IList`1 indices) <0x40c3acf0 + 0x00092> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c391f0 + 0x003db> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x40b98d60 + 0x00020> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x40bb79f0 + 0x0001d> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x40c348f0 + 0x00017> in <filename unknown>:0 
  at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c39760 + 0x000ec> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c391f0 + 0x003f7> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x40b98d60 + 0x00020> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x40bb79f0 + 0x0001d> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x40c348f0 + 0x00017> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.AssignCmd c) <0x40c38000 + 0x00884> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x40bd47f0 + 0x0053b> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at Symbooglix.Executor.ExecuteInstruction () <0x40bcff40 + 0x001c3> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x40bb46b0 + 0x0059b> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x40bb4040 + 0x0015f> in <filename unknown>:0 
Exiting with EXCEPTION_RAISED