search

boogie-org / symbooglix

Symbolic Execution Engine for Boogie
MIT License
27 stars 4 forks source link

Throwing System.ArgumentNullException #32

Closed zvonimir closed 6 years ago

zvonimir commented 7 years ago

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
zvonimir commented 7 years ago

@delcypher : Have you maybe had a chance to take a peek at this one? Thx!

delcypher commented 7 years ago

@zvonimir I had a very quick look and manage to reproduce the failure but I haven't had time to debug it. The crash is actually happening in Boogie code rather than in Symbooglix's code so this might be a bit tricky as I'm not that familiar with some of Boogie's code.

zvonimir commented 6 years ago

@delcypher : Hey, we are back and stuck on this one. We are trying to use symbooglix on SVCOMP benchmarks with SMACK, and it is failing on most of them due to this particular problem. Any chance you'll have time to take a look at this any time soon?

delcypher commented 6 years ago

@zvonimir I'm a bit busy right now but I should be able to take a look at this on Wednesday.

zvonimir commented 6 years ago

That works. Thanks @delcypher!

zvonimir commented 6 years ago

Hey @delcypher. Sorry for bugging you again, but did you have a chance to look into this? Also, congrats!

zvonimir commented 6 years ago

@delcypher : Just checking about this. I know that you kind of moved on, but I am still curious if you would still be able to take a look at this?