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

[liammachado]

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.

[shaobo-he]

@liammachado Can you attach a Boogie file as well as options to run Symbooglix? It would make debugging much easier.

[liammachado]

Had to zip the bpl file since github doesn't support uploading that file type. The command I ran: "smack -bpl gcd.bpl gcd.c --verifier=symbooglix --verbose --bit-precise" gcd.zip

[shaobo-he]

Thanks Liam. But it seems that you still don't show the options to run Symbooglix. And flag --verifier=symboolix is not yet supported in the master branch of SMACK.

[liammachado]

Hey @Guoanshisb ,

Here is the symbooglix command that is run when i run the above smack command:

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

[delcypher]

@liammachado Thank you for reporting this bug. I've written a fix and committed it. Please test. If you're still seeing this bug please re open this issue with the input causing the bug and I'll look into it.