Symbolic Engine | Simple Objects Support - extended symbolic tracking

[ilebrero]

Details

First part of the references support for the symbolic engine (without supporting privater fields or sub classes). This PR focuses on extending the symbolic grammar and adding some general structure for the implementation of references in the symbolic engine.

Notes

• Private Fields and sub classes will be added at some point in the future

Future PRs

• Extend utils for creating reference related statements (probably there's something already done in this part)
• Add encoding in the solver side
• Translate the symbolic state of the references to the solver's encoding
• Complete the test case updater algorithm

Main idea

Instances

Enumerate the instances found along the execution. 0 is reserved for null and 1 for Object.

Types

Enumerate types found during execution. 0 is reserved for Object

Constraints

just == or != between references.

Encoding

• Will be added in a future PR

Test case update

• Added basic structure for the algorithm to reconstruct the object based on a solution from the solver

Documentation

• Implementation doc
• Trello board -> "Complex Objects Support" list

Changes

Grammar

• Extended grammar for expressing extra elements.

  • New one
    • ReferenceExpression = ReferenceVariable | ReferenceConstrant
    • ReferenceConstant = NullReferenceConstant | NonNullReferenceConstant
    • NonNullReferenceConstant = ClassReferenceConstant | ArrayConstant
    • ReferenceVariable = ClassReferenceVariable | ArrayVariable
    • ArrayVariable = Same as the one explained in the arrays implementation
    • ArrayConstant = Same as the one explained in the arrays implementation

• Added reference constraints for equals and not equals.

Instances

• Execution preparation
  • Added conversion to a symbolic variable for new instances created outside the SUT in the SymbolicObserver
• Added statistics
• Extended the symbolic grammar as mentioned above as well as all the processing related to the new expressions
• Cleaned up instance tracking in the SymbolicHeap

Types

• Extended the symbolic grammar as mentioned above as well as all the processing related to the new expressions
• Cleaned up type tracking in the SymbolicHeap

Constraints

• Added new constraints for references
• Extended the processing of constraints for the new constraints
• Added constraint tracking to the related byte-code instructions

Results processing

• Baseline for creating and updating test cases using the solver results

Test Cases

• Checked test cases for possible regressions
• Fixed broken test
• Fixed type utils