viktormalik / 2ls Goto Github PK

When trying to analyze the following example:

#include <stdlib.h>

extern int __VERIFIER_nondet_int(void);

struct list{
	struct list* next;
};

int main()
{
	struct list *p,*q;
	p = malloc(sizeof(struct list));
	q = malloc(sizeof(struct list));
	
	p->next = malloc(sizeof(struct list));
	p = q;

	while(__VERIFIER_nondet_int) {
		q = p->next;
		q->next = malloc(sizeof(struct list));
		p->next = q->next;
	}

	return 1;
}

2ls ends up with this assertion error:
2ls: strategy_solver_heap.cpp:141: virtual bool strategy_solver_heapt::iterate(strategy_solver_baset::invariantt&): Assertion `to_address_of_expr(ptr_value).object().id()==ID_symbol' failed.

• currently, we transform an assignment with memory access at right hand side into SSA as follows:
  a = p->next (original assignment in C/GOTO program)
  a#cur-loc == p'obj.next#last-loc (SSA equality where cur-loc is the current location and last-loc is the location of the last assignment of p'obj.next)

• this transformation is done by method local_SSAt::build_transfer
  we check whether p'obj.next has been defined before (function all_symbolic_deref_called at line 469 in local_ssa.cpp)

• but we also need to check whether p has not changed since last assignment of p'obj.next, because that would make p'obj.next invalid
  in that case, we would have to use actual abstract object on the heap (dynamic_object$0.next) instead - this can be obtained by calling the function local_SSAt::dereference on p->next

• I'd suggest including this check into build_transfer function
  maybe it would be enough to check whether last definition of pointer p is before the last definition o p'obj.next - this information can be retrieved from ssa_analysis, for inspiration see all_symbolic_deref_defined (question is, is this really sound?)
  retrieving pointer p from object p'obj should be possible using functions from ssa_pointed_objects.h, particularly get_pointer

• merge into heap branch