1

Closed

Using latest stable Z3 (Z3 4.3.2) breaks GPUVerify

description

$ gpuverify --blockDim=1024 --gridDim=1 --no-inline --debug testsuite/CUDA/function_pointers/basic_argument_fail/kernel.cu 


Prover error: line 18 column 23: the parameter 'relevancy' was renamed to 'smt.relevancy', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.relevancy' for the full description of the parameter

Prover error: line 19 column 20: unknown parameter 'solver', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list

Prover error: line 14 column 23: the parameter 'relevancy' was renamed to 'smt.relevancy', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.relevancy' for the full description of the parameter

Prover error: line 15 column 20: unknown parameter 'solver', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list

Prover error: line 138 column 23: the parameter 'relevancy' was renamed to 'smt.relevancy', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.relevancy' for the full description of the parameter

Prover error: line 139 column 20: unknown parameter 'solver', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list

Prover error: line 270 column 23: the parameter 'relevancy' was renamed to 'smt.relevancy', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.relevancy' for the full description of the parameter

Prover error: line 271 column 20: unknown parameter 'solver', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list

Exception thrown in GPUVerifyBoogieDriver
System.NotImplementedException: The requested feature is not implemented.
  at Microsoft.Boogie.Model+Element.AsInt () [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.GetThreadOne (Microsoft.Boogie.Model model, Boolean withSpaces) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.GetThreadsAndGroupsFromModel (Microsoft.Boogie.Model model, System.String& thread1, System.String& thread2, System.String& group1, System.String& group2, Boolean withSpaces) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportThreadSpecificFailure (Microsoft.Boogie.AssertCounterexample err, System.String messagePrefix) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportFailingBadPointerAccess (Microsoft.Boogie.AssertCounterexample err) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportCounterexample (Microsoft.Boogie.Counterexample error) [0x00000] in <filename unknown>:0 
  at GPUVerify.KernelAnalyser.ProcessOutcome (Microsoft.Boogie.Program program, System.String implName, Outcome outcome, System.Collections.Generic.List`1 errors, System.String timeIndication, System.Int32& errorCount, System.Int32& verified, System.Int32& inconclusives, System.Int32& timeOuts, System.Int32& outOfMemories) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.VerifyProgram (Microsoft.Boogie.Program program) [0x001d2] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:162 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.VerifyFiles (System.Collections.Generic.List`1 fileNames) [0x00076] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:100 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.Main (System.String[] args) [0x00155] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:64 

Unhandled Exception:
System.NotImplementedException: The requested feature is not implemented.
  at Microsoft.Boogie.Model+Element.AsInt () [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.GetThreadOne (Microsoft.Boogie.Model model, Boolean withSpaces) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.GetThreadsAndGroupsFromModel (Microsoft.Boogie.Model model, System.String& thread1, System.String& thread2, System.String& group1, System.String& group2, Boolean withSpaces) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportThreadSpecificFailure (Microsoft.Boogie.AssertCounterexample err, System.String messagePrefix) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportFailingBadPointerAccess (Microsoft.Boogie.AssertCounterexample err) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportCounterexample (Microsoft.Boogie.Counterexample error) [0x00000] in <filename unknown>:0 
  at GPUVerify.KernelAnalyser.ProcessOutcome (Microsoft.Boogie.Program program, System.String implName, Outcome outcome, System.Collections.Generic.List`1 errors, System.String timeIndication, System.Int32& errorCount, System.Int32& verified, System.Int32& inconclusives, System.Int32& timeOuts, System.Int32& outOfMemories) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.VerifyProgram (Microsoft.Boogie.Program program) [0x001d2] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:162 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.VerifyFiles (System.Collections.Generic.List`1 fileNames) [0x00076] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:100 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.Main (System.String[] args) [0x00155] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:64 
[ERROR] FATAL UNHANDLED EXCEPTION: System.NotImplementedException: The requested feature is not implemented.
  at Microsoft.Boogie.Model+Element.AsInt () [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.GetThreadOne (Microsoft.Boogie.Model model, Boolean withSpaces) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.GetThreadsAndGroupsFromModel (Microsoft.Boogie.Model model, System.String& thread1, System.String& thread2, System.String& group1, System.String& group2, Boolean withSpaces) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportThreadSpecificFailure (Microsoft.Boogie.AssertCounterexample err, System.String messagePrefix) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportFailingBadPointerAccess (Microsoft.Boogie.AssertCounterexample err) [0x00000] in <filename unknown>:0 
  at GPUVerify.GPUVerifyErrorReporter.ReportCounterexample (Microsoft.Boogie.Counterexample error) [0x00000] in <filename unknown>:0 
  at GPUVerify.KernelAnalyser.ProcessOutcome (Microsoft.Boogie.Program program, System.String implName, Outcome outcome, System.Collections.Generic.List`1 errors, System.String timeIndication, System.Int32& errorCount, System.Int32& verified, System.Int32& inconclusives, System.Int32& timeOuts, System.Int32& outOfMemories) [0x00000] in <filename unknown>:0 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.VerifyProgram (Microsoft.Boogie.Program program) [0x001d2] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:162 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.VerifyFiles (System.Collections.Generic.List`1 fileNames) [0x00076] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:100 
  at Microsoft.Boogie.GPUVerifyBoogieDriver.Main (System.String[] args) [0x00155] in /home/gv/gpuverify/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs:64 
Closed Dec 2, 2014 at 9:51 AM by jketema
Fixed after the latest commit

comments

jketema wrote Oct 28, 2014 at 10:30 PM

Two questions:
  • Does the current version of Boogie work with this Z3 version. Last I know (but that info is at least half a year old) it didn't?
  • Any idea if "solver" been replaced by something else, or has it been dropped completely?
If (preferably) renaming and possibly dropping the options from the GPUVerify script solver the problem, then how does the performance compare to 4.3.1 on our full invariant benchmark set?

jketema wrote Nov 29, 2014 at 4:22 PM

I've a potential fix for this. I'm still doing some regression testing on our whole benchmark suite.

I'm not able to check whether Boogie's Z3api interface works. I'm not sure how to tell Boogie where the library it is that it needs to load on Mac OS X.

danliew wrote Dec 1, 2014 at 8:56 AM

My guess is you would need to put the built z3.dll file into the Binaries folder. By the way that dll is not built by default when you build Z3 so you have to go ahead and build it manually. I also found I needed to be very careful with the Z3 shared library. When I first tried to use z3.dll it crashed because I had an older version of the Z3 shared library installed and mono picked that library first. I used the strace program to see what library mono was trying to use.

However I don't know if anyone uses the "Z3api" build configuration for Boogie. I've never used it.