Handle multi-arity maps correctly

[sebastian-kunze]

I run symbooglix on a programs, i.e., Example.bpl.txt, which abstracts a heap representation. The program looks fine when running it with boogie but throws the following exception related to my heap abstraction and a type mismatching when verifying it using symbooglix.

Symbooglix.ExprTypeCheckException: Type mismatch at index 0 expected type Ref but was type Field int
  at Symbooglix.MapProxy.TypeCheckIndices (IList`1 indices) <0x46bcb98 + 0x0028f> in <filename unknown>:0 
  at Symbooglix.MapProxy.ReadMapAt (IList`1 indices) <0x46bc988 + 0x00023> in <filename unknown>:0 
  at Symbooglix.SimpleVariableStore.ReadMap (Microsoft.Boogie.Variable mapVariable, IList`1 indicies) <0x46bc888 + 0x0006b> in <filename unknown>:0 
  at Symbooglix.ExecutionState.ReadMapVariableInScopeAt (Microsoft.Boogie.Variable v, IList`1 indices) <0x46bc7a8 + 0x00080> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x46bb1e8 + 0x00327> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x2df1e00 + 0x0001a> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x2f16808 + 0x00017> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x46a4c28 + 0x00017> in <filename unknown>:0 
  at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x46bb658 + 0x000a0> in <filename unknown>:0 
  at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x46bb1e8 + 0x00343> in <filename unknown>:0 
  at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x2df1e00 + 0x0001a> in <filename unknown>:0 
  at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x2f16808 + 0x00017> in <filename unknown>:0 
  at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x46a4c28 + 0x00017> in <filename unknown>:0 
  at Symbooglix.Executor.Handle (Microsoft.Boogie.AssignCmd c) <0x46ba000 + 0x0097e> 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) <0x4400000 + 0x00425> in <filename unknown>:0 
  at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
  at Symbooglix.Executor.ExecuteInstruction () <0x43f0718 + 0x001b4> in <filename unknown>:0 
  at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2f13b48 + 0x004eb> in <filename unknown>:0 
  at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x2f13770 + 0x000c3> in <filename unknown>:0 

[delcypher]

@sekunze Thanks for giving Symbooglix a try. The problem here is your use of type constructors. This is a feature I completely ignored during the design of Symbooglix because

• None of the benchmarks I had used them
• They don't seem to be well documented (just like the rest of Boogie 😭, feel free to update the docs so the world can actually understand these features ) so I don't have a good understanding of them.

// ######################################
// #         HEAP INITIALISATION        #
// ######################################
type Ref;
type Field a;
type Heap = <a> [Ref, Field a] a;

const unique null : Ref;
const unique alloc : Field bool;

var heap : Heap;

what I found really surprising here is that the variable heap has type Heap not Heap<int> so there's a free type parameter there which I didn't realise was legal (I thought <a> was like a generic parameter that you would specify when using the type) which means reading from heap can return different types depending on the map arguments. Symbooglix's current handling of maps cannot deal with this. I would need to some time to think about to handle this but really I need a much better understanding of type constructors before I can do this.

@afd have you seen this before?

@sekunze In the short term avoiding the use of maps with free type variables is what you need to do for your Boogie programs to work with Symbooglix right now. In your case I think having a heap for each data type would work. Although syntactically that's a bit displeasing it's worth noting that Boogie is meant to be an intermediate language so it doesn't matter if you are generating the Boogie code.

[sebastian-kunze]

@delcypher I removed the generic type and introduced an exclusive heap for type int. When calling my procedure, which simply accesses a value of type int and performs a subtraction, the same exception is thrown. The problem seems to be not specifically related to the generic types.

// ######################################
// #         HEAP INITIALISATION        #
// ######################################
type Ref;
type Field;
type Heap = [Ref, Field] int;

var heap : Heap;

// ######################################    
// #          LOCAL VARIABLES           #
// ######################################

var this : Ref;
var time : Field;

// ######################################    
// #             SYMBOOGLIX             #
// ######################################

procedure main(i : int)
{
 var o : int;
 call o := getElapsedTime(i);
}

// ######################################    
// #              METHODS               #
// ######################################

procedure getElapsedTime(t : int) returns (r : int)
 ensures heap == old(heap);
{
 r := heap[this,time] - t;
}

[afd]

@delcypher no, I'm not familiar with type constructors and type parameters in Boogie - haven't needed them for anything I've worked on so far.

[delcypher]

@sekunze Sorry for the delay. It seems I didn't get a notification when you replied. The example you give with the monomorphic map shouldn't fail. I'll take a look tomorrow and see if I can figure out what's wrong.

[delcypher]

@sekunze Okay curiosity got the better of me. I've found the issue. The problem is that Symbooglix does the wrong thing when working with multi-arity maps. This is something that was never tested properly because none of the benchmarks I had write maps this way.

The following change fixes running your example

--- a/src/Symbooglix/Executor/MapExecutionStateVariablesDuplicator.cs
+++ b/src/Symbooglix/Executor/MapExecutionStateVariablesDuplicator.cs
@@ -90,7 +90,7 @@ public override Expr VisitNAryExpr(NAryExpr node)
                 Expr firstArg = null;
                 do
                 {
-                    for (int index=1; index < asMapSelect.Args.Count; ++index)
+                    for (int index= asMapSelect.Args.Count -1; index >=1; --index)
                     {
                         // Don't do index variable mapping here because we might
                         // need to throw away what we've done

I won't be in a position to commit to Symbooglix's code until mid August so I can't land a fix (along with tests) into the master branch yet. There may be other bugs lurking related to multiple arity maps.

Hopefully this will get you started though. Sorry again for the delayed response.

[delcypher]

@sekunze @afd This is now fixed is master so I'm closing this issue.