AssertionFailingException: Incorrect number of arguments

[sebastian-kunze]

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?

[delcypher]

@sekunze The problem you are observing here is that unfortunately the solver backend doesn't know how to handle multi arity maps.

i.e.

type IntHeap = [Ref, Int] int;

The solver backend does know how to handle nested single arity maps.

type IntHeap = [Ref][Int] int;

however.

This is an unfortunate limitation which I never hit before because the benchmarks I used only single arity maps (sometimes nested). Fixing this would be a matter teaching the SMTLIBQueryPrinter to encode multi arity maps like it encodes nested maps. Unfortunately Symbooglix's solver backend is a bit of a mess so this might not be very easy.

As for your question on traces Symbooglix doesn't current record execution traces. This could and should be implemented though as this is a very basic and useful feature. At what granularity do you need a trace? When sketched out the idea I imagined the trace should be a trie of basic block labels so try and keep memory usage as low as possible. Alternatively the trace could be a sequence of branch decisions.

[sebastian-kunze]

I am mostly interested in how methods interact with each other, i.e., what call sequences uncover a certain behaviour. Therefore, a tree structure would be most qualified.