Skip to content

Heap Configuration Syntax

Jump to bottom
thnoll edited this page Mar 28, 2018 · 8 revisions

Initial heap configurations can be manually specified as an input for Attestor. They have to be given in JSON format as further specified below.

Hypergraph Object

Heap configurations are JSON-Objects with the attributes

{
  "nodes":[ NodeObject ],
  "external":[ Number ] ,
  "variables":[ VariableObject ],
  "selectors":[ SelectorObject ],
  "hyperedges":[ HyperedgeObject ]
}

For details on the individual objects, please confer

A complete example is found at the bottom of this page.

Nodes

Nodes are specified by node objects with attributes

{
  "type": String,
  "number": Number
}

Type may assume either "NULL", "int_0", "int_1" or "int_-1" for nodes referring to the respective constants or the class of the object this node will model (see Type).

number specifies the number of nodes of the given type that are created.

Skip example

Example

The following example merely underlines the use of number:

[{
  "type":"someType",
  "number":2
}]

is equal to

[{
  "type":"someType",
  "number":1
},{
  "type":"someType",
  "number":1
}]

The next example shows how different node types can be combined:

"nodes":[
{
  "type":"int_0",
  "number":1
},{
  "type":"NULL",
  "number":1
},{
  "type":"List",
  "number":2
}]

creates one node representing the constant 0 one representing null and two nodes representing List-objects.

Externals

External nodes are specified by an array of node identifiers.

Skip example

Example

The following snippet specifies the node referenced by 0 as the first external node and the node referenced by 1 as the second external node.

"externals":[0,1]

Variables

Variables are specified as an array of variable objects which have the form

{
  "name":String,
  "target":Number
}

The name is either a constant (null, true, false, -1, 0, or 1) or a parameter reference ("@parameterX:" with X being the index in the parameter list of the top-level method or "@this").

The target is the identifier of the node representing the object or constant this variable should point to.

Note: Any constants you do not specify manually will be inserted automatically by Attestor (so you only need to include constants if you want to reference them). Furthermore, Attestor requires that the constants true and 1 (false and 0 respectively) point to the same node. However, Attestor is not able to identify the correct node by its type if there is no constant-variable pointing to it.

Skip example

Examples

The following specification is not valid, since false and 0 do not point to the same node.

"variables":[
{
  "name":"false",
  "target":0
},{
  "name":"0",
  "target":1
}
]

The next example is valid, but Attestor would create a new node of type NULL for constant null probably leading to unexpected behaviour:

"nodes":[{
   "type":"NULL",
   "number":1
}],
"variables":[]
...

Instead you have to specify

"nodes":[{
  "type":"NULL",
  "number":1
}],
"variables":[{
  "name":"null",
  "target":0
}],
...

However, the next example is valid. It specifies that the first parameter given to the method analysed is false (or 0 - as Attestor cannot distinguish them) and the this-reference is some other object (represented by the node 2). Note, that we do not need to specify the constant 0, as it will be inserted automatically so that it points to the same node as false.

"variables":[
{
  "name":"false",
  "target":0
},{
  "name":"null",
  "target":1
},{
  "name":"@parameter0:",
  "target":0
},{
  "name":"@this:",
  "target":2
}
]

Selectors

Selector edges are specified by an array of selector objects which have the form

{
  "label":String,
  "annotation":String,
  "origin":Number,
  "target":Number
}

The label specifies the field modeled by this selector edge. The field annotation to specify an annotation is optional. The origin should be set to the node representing the object this field belongs to and target to the node representing the object or constant this field points to.

Skip example

Examples

"selectors":[
  {
    "label":"left",
    "annotation":"0",
    "origin":3,
    "target":1
  }
]

specifies a single selector edge left [0] from node 3 to node 1.

"selectors":[
 {
    "label":"next",
    "origin":2,
    "target":3
 }
]

specifies a single selector edge next without annotation pointing from 2 to 3.

Hyperedges

Nonterminal edges are specified by an array of hyperedge objects which have the form

{
  "label":String,
  "index":[String],
  "tentacles":[Number]
}

where the field index to specify the index of a nonterminal edge is optional. See here how to specify indices. The tentacles of the hyperedge are specified as an array of node references.

Skip example

Examples

"hyperedges":[
  {
    "label":"AVLTree",
    "index":["s","()"],
    "tentacles":[0,1,2,3,8]
  }
]

Above you see an example of an indexed nonterminal edge AVLTree [s,()] with adjacent nodes 0,1,2,3 and 8, whereas the example below shows a nonterminal edge List without index and adjacent nodes 3 and 1:

"hyperedges":[{
  "label":"List",
  "tentacles":[3,1]
}]

Node References

Nodes are referenced by an integer number referring to the order they were inserted, beginning with 0.

Examples

"nodes":[
 {
    "type":"NULL",
    "number":1
 },{
   "type":"List",
   "number":2
 }
]

In the example above the NULL-node is referenced by the number 0 whereas 1 and 2 each refer to a node of type List.

Complete Example

The following code combines some of the example snippets from the sections above:

{
  "nodes":[
    {
      "type":"int_0",
      "number":1
    },{
      "type":"NULL",
      "number":1
    },{
      "type":"List",
      "number":2
    }
  ],
  "externals":[0,1],
  "variables":[
  {
    "name":"false",
    "target":0
  },{
    "name":"@parameter0:",
    "target":0
  },{
    "name":"@this",
    "target":2
  }
  ],
  "selectors":[
  {
    "label":"next",
    "origin":2,
    "target":3
  }
 ],
 "hyperedges":[
  {
    "label":"List",
    "tentacles":[3,1]
  }
 ]
}
Clone this wiki locally