NotImplementedException: (_bvbuiltin not supported!

[liammachado]

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

[delcypher]

@liammachado Sorry for the delay. I've found the problem.

The problem is your use of the zero_extend and sign_extend built-ins.

function {:bvbuiltin "(_ zero_extend 8)"} $zext.bv8.bv16(i: bv8) returns (bv16);
function {:bvbuiltin "(_ sign_extend 8)"} $sext.bv8.bv16(i: bv8) returns (bv16);

This is not what Symbooglix expects. It expects

function {:bvbuiltin "zero_extend 8"} $zext.bv8.bv16(i: bv8) returns (bv16);
function {:bvbuiltin "sign_extend 8"} $sext.bv8.bv16(i: bv8) returns (bv16);

The origin of this is because bugle emits zero_extend and sign_extend this way.

Looking at Boogie's current implementation. It looks both forms are supported.

For now I can fix the issue in Symbooglix by teaching it to support both but we really should not have two ways of doing this.

We should pick the right way of doing this and document it. Personally I think it should just be

function {:bvbuiltin "zero_extend"} $zext.bv8.bv16(i: bv8) returns (bv16);
function {:bvbuiltin "sign_extend"} $sext.bv8.bv16(i: bv8) returns (bv16);

because we can infer the 8 by looking at the types used in the function declaration.

@wuestholz @zvonimir @RustanLeino any thoughts on this?

[delcypher]

This is only partially fixed. This benchmark still causes Symbooglix to crash due to the unsupported bv2int built-in. This requires more work because the builders needed to be extended to support this.

It is also debatable whether type conversion should be done this way. Boogie supports doing Arithmetic coercion (i.e. int -> real and real -> int) but currently doesn't allow conversion to and from bitvector types. This seems like something the language ought to allow.

It is also unclear to me whether the bv2int and int2bv functions will works as intended because according to Z3's documentation these functions are uninterpreted.

[zvonimir]

When it comes to support for bvbuiltin, simpler syntax is probably better, and so in that sense I agree with your suggestion @delcypher. Having said that, that might break backward compatibility, which is always tricky.
When it comes to bv2int, you can chose to have them be interpreted in Z3 using SMT.BV.ENABLE_INT2BV. Now, this dramatically influences the performance and scalability of Z3, and we are unsure whether it is the best solution. We do use it though. I think it would be good to see if bv2int is a part of the SMTlib standard. To me it seems it is not, which maybe influenced the fact this conversion is not a part of the language. Someone else should double-check this to make sure.
You could of course always provide your own implementation manually (using bit extraction I guess).