Null forking

[tjausm]

Idea 1: true lazy

Add special LazyReference(ref, class) type to Symbolic expression:

LazyRef implements:

• release() -> Result<Option<Reference>, Error>, if reference could be null return error. If path is unfeasible return None, otherwise return reference.
• initialize() -> Result<Option<Reference>, Error>, if reference could be null return error. If path is unfeasible return None, otherwise initialize lazy object on heap and return reference.

problem: how do we prevent lazyref from being instantiated in one place and not being instantiated in another? Is this even a problem?

solution: is not a problem. If one is initiated there must be a constraint indicating that ref is not null. Thus lazy refs will resolve to actual ref during constraint solving.

Implementation:

• expr_to_str -> encode LazyRef(ref, class) as name with assertion prepended: (xor (= name == ref) (= name == null)) (generate name from reference).
• access_object -> initialize()
• access_array -> return lazy reference
• stack_get -> if we want the reference: release()

Idea 2: on declaration

fork only happens when initializing lazy objects as arguments of main(), accessing fields of lazy objects or when accessing arrays with lazy objects. Let those functions fork as follows:

Initializing lazy object Forks state, happens in init_lazy_object() -> (Reference, Reference, SymMemory) returning a null reference and a

accessing fields If we access a field of reference r that is null we push r == null to pc, call pc.conjunct() and if expression_unsatisfiable holds we drop path, otherwise return error.

Accessing Object Generates Fork if field is a lazy object

• return null
• return ref to initialized lazy object

accessing arrays Generates Fork if it is array of lazy objects:

• return null
• return ref to initialized lazy object

Forking routine:

1. Use a type Fork<a> = No a | Yes a (Vec<State>)
2. implement a straighten(queue) method on the Fork type that returns a and possibly pushes new state(s) to front of queue
3. save initial state init_state each time when inspecting CFG node in SEE
4. when entering a function that could fork, pass &init_state to it, and call straighten on the result

[tjausm]

access_array, access_object & stack_get are implemented. Still need to implement release and initialise and correct encoding of LazyReferences in smtlib

[tjausm]

Add LazyReference to simplifier