missing axiom definition in constraints

[sebastian-kunze]

I have two version of a program, which are are almost identical except that one program features an additional procedure. This additional procedure involves an axiom, which is present in both versions but used only in one version of them. Executing the equivalent procedure in both versions generates different constraints though. See the following example for details:

Version A: For procedure someMethodWeWantToExecuteSymbolically in version A, the constraint: [Cmd] assume {:partition} localBoolean; is generated. No information about the axiom is available.

// ---------------------------------------------------------------
// ---------------------------- HEAP -----------------------------
// ---------------------------------------------------------------
type Ref;

type Int;
type Bool;

type BoolHeap = [Ref][Bool] bool;
type IntHeap  = [Ref][Int]  int;
type ObjHeap  = [Ref][Ref]  Ref;

var boolHeap : BoolHeap;
var intHeap  : IntHeap;
var objHeap  : ObjHeap;

var null : Ref;

// ---------------------------------------------------------------
// ---------------------------- CODE -----------------------------
// ---------------------------------------------------------------

// FIELDS

var globalBooleanArray$array : [int] Bool;
var globalBooleanArray$field : Ref;

const globalBooleanArray$size : int;
axiom globalBooleanArray$size == 5;

// METHODS

procedure someMethodWeWantToExecuteSymbolically()
 modifies boolHeap, intHeap, objHeap;
{
 // INIT
 var localBoolean : bool;

 // BODY
 if (localBoolean) {
  localBoolean := false;
 }
}

Version B Executing procedure someMethodWeWantToExecuteSymbolically in version B, generated the constraints [Cmd] assume {:partition} localBoolean; and [Axiom] globalBooleanArray$size == 5.

// ---------------------------------------------------------------
// ---------------------------- HEAP -----------------------------
// ---------------------------------------------------------------
type Ref;

type Int;
type Bool;

type BoolHeap = [Ref][Bool] bool;
type IntHeap  = [Ref][Int]  int;
type ObjHeap  = [Ref][Ref]  Ref;

var boolHeap : BoolHeap;
var intHeap  : IntHeap;
var objHeap  : ObjHeap;

var null : Ref;

// ---------------------------------------------------------------
// ---------------------------- CODE -----------------------------
// ---------------------------------------------------------------

// FIELDS

var glbalBooleanArray$array : [int] Bool;
var globalBooleanArray$field : Ref;

const globalBooleanArray$size : int;
axiom globalBooleanArray$size == 5;

// METHODS

procedure someMethodWeWantToExecuteSymbolically()
 modifies boolHeap, intHeap, objHeap;
{
 // INIT
 var localBoolean : bool;

 // BODY
 if (localBoolean) {
  localBoolean := false;
 }
}

procedure someOtherMethodWeDoNotWantToExecuteSymbolically()
 modifies boolHeap, intHeap, objHeap;
{
 // INIT

 // BODY
 if (globalBooleanArray$size > 0) {

 }
}

Is this the desired behaviour? Shouldn't the information about the axiom be present in both version of the program?

[delcypher]

@sebkunze This is intentional. Symbooglix will deliberately remove global declarations (functions, axioms and variables) that it can statically prove will never be used. This is achieved using the GlobalDeadDeclEliminationPass. You can disable running this pass by passing --globaldde=0 to the sbx.exe tool.