Checking validity of heap object concretisation (p'obj.next).

[viktormalik]

• 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

[martinhruska]

Is there any easy way how to print out the resulting ssa form of program?

[martinhruska]

If we checked only the last definition of p wouldn't it be a problem in the following case:
p = malloc();
while() {
x = p->next;
p->next = y;
}

Couldn't this lead to the unsoundness the we have experienced before?

[viktormalik]

you can print the ssa using local_SSAt::output function
you can print any exprt expression using debug() << from_expr(...) -> see usage somewhere

[viktormalik]

in that case since p->next was not defined before when first used, it would not be transformed into p'obj.next, but into approriate dynamic_object.next

[martinhruska]

OK and when we define it?

p = malloc();
p->next = ...;
p = ....;
while() {
x = p->next;
p->next = y;
}

[viktormalik]

then we probably would, yes

I think this is a conceptual problem - dynamic_object is an abstraction and thus it might not cover all options in combination with the SSA form that we use

maybe we could solve this by defining p'obj.next in case it has not been defined since last assignment to p - we could get the value to be assigned to p'obj.next from dereferencing p - this way we would have p'obj.next as a concretised object which is assigned all possible values of actual abstract dynamic_objects that p might point to

[martinhruska]

So we would concretise p'obj.next to all possible values which p->next may have?

I think about another solution. Could not we stay with the current state but create for each point p set of the dependent objects P={p'obj.sel | sel is from set of all selectors of p}. Then once p is defined we invalidate all objects from P. Would this work?

[viktormalik]

That would work but in the last example you provided, you would invalidate p'obj.next for p = ...; and thus when transforming x = p->next, you can't use p'obj.next (since it is invalidated) and you have to use dynamic_object.next, which might again bring unsoundness.

I definitely agree with the idea of having dependent objects, but I think we will also have to introduce a mechanism to "concretise" object when reading it (when it appears on the right hand side) because currently we do that when it is written.

[peterschrammel]

@martinhruska, can you please paste here the current SSA as produced by the tool for your example above (fill in the ... with something that makes sense)?

[martinhruska]

So consider the following (a little bit artificial :) C code:

#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));
	q->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;
}

The following SSA form is produced:

(E) $guard#0 == TRUE

(E) __CPROVER_dead_object#2 == NULL

(E) __CPROVER_deallocated#3 == NULL

(E) __CPROVER_malloc_is_new_array#4 == FALSE

(E) __CPROVER_malloc_object#5 == NULL

(E) __CPROVER_malloc_size#6 == 0ul

(E) __CPROVER_memory_leak#7 == NULL

(E) __CPROVER_next_thread_id#8 == 0ul

(E) __CPROVER_pipe_count#9 == 0u

(E) __CPROVER_rounding_mode#10 == 0

(E) __CPROVER_thread_id#11 == 0ul

(E) __CPROVER_threads_exited#12 == ARRAY_OF(FALSE)

(E) malloc_size#20 == sizeof(struct list) /*8ul*/ 

(E) malloc_value$1#24 == (void *)&dynamic_object$24

(E) malloc_res#25 == malloc_value$1#24

(E) __CPROVER_deallocated#26 == (malloc_res#25 == __CPROVER_deallocated#3 ? NULL : __CPROVER_deallocated#3)

(E) __CPROVER_malloc_object#28 == (record_malloc#27 ? malloc_res#25 : __CPROVER_malloc_object#5)

(E) __CPROVER_malloc_size#29 == (record_malloc#27 ? malloc_size#20 : __CPROVER_malloc_size#6)

(E) __CPROVER_malloc_is_new_array#30 == (!record_malloc#27 && __CPROVER_malloc_is_new_array#4)

(E) __CPROVER_memory_leak#32 == (record_may_leak#31 ? malloc_res#25 : __CPROVER_memory_leak#7)

(E) malloc#return_value#33 == malloc_res#25

(E) return_value_malloc$1#40 == malloc#return_value#33

(E) p#42 == (struct list *)return_value_malloc$1#40

(E) malloc_size#46 == sizeof(struct list) /*8ul*/ 

(E) malloc_value$1#50 == (void *)&dynamic_object$50

(E) malloc_res#51 == malloc_value$1#50

(E) __CPROVER_deallocated#52 == (malloc_res#51 == __CPROVER_deallocated#26 ? NULL : __CPROVER_deallocated#26)

(E) __CPROVER_malloc_object#54 == (record_malloc#53 ? malloc_res#51 : __CPROVER_malloc_object#28)

(E) __CPROVER_malloc_size#55 == (record_malloc#53 ? malloc_size#46 : __CPROVER_malloc_size#29)

(E) __CPROVER_malloc_is_new_array#56 == (!record_malloc#53 && __CPROVER_malloc_is_new_array#30)

(E) __CPROVER_memory_leak#58 == (record_may_leak#57 ? malloc_res#51 : __CPROVER_memory_leak#32)

(E) malloc#return_value#59 == malloc_res#51

(E) return_value_malloc$2#66 == malloc#return_value#59

(E) q#68 == (struct list *)return_value_malloc$2#66

(E) malloc_size#72 == sizeof(struct list) /*8ul*/ 

(E) malloc_value$1#76 == (void *)&dynamic_object$76

(E) malloc_res#77 == malloc_value$1#76

(E) __CPROVER_deallocated#78 == (malloc_res#77 == __CPROVER_deallocated#52 ? NULL : __CPROVER_deallocated#52)

(E) __CPROVER_malloc_object#80 == (record_malloc#79 ? malloc_res#77 : __CPROVER_malloc_object#54)

(E) __CPROVER_malloc_size#81 == (record_malloc#79 ? malloc_size#72 : __CPROVER_malloc_size#55)

(E) __CPROVER_malloc_is_new_array#82 == (!record_malloc#79 && __CPROVER_malloc_is_new_array#56)

(E) __CPROVER_memory_leak#84 == (record_may_leak#83 ? malloc_res#77 : __CPROVER_memory_leak#58)

(E) malloc#return_value#85 == malloc_res#77

(E) return_value_malloc$3#92 == malloc#return_value#85

(E) dynamic_object$24.next#94 == (struct list *)return_value_malloc$3#92

(E) malloc_size#98 == sizeof(struct list) /*8ul*/ 

(E) malloc_value$1#102 == (void *)&dynamic_object$102

(E) malloc_res#103 == malloc_value$1#102

(E) __CPROVER_deallocated#104 == (malloc_res#103 == __CPROVER_deallocated#78 ? NULL : __CPROVER_deallocated#78)

(E) __CPROVER_malloc_object#106 == (record_malloc#105 ? malloc_res#103 : __CPROVER_malloc_object#80)

(E) __CPROVER_malloc_size#107 == (record_malloc#105 ? malloc_size#98 : __CPROVER_malloc_size#81)

(E) __CPROVER_malloc_is_new_array#108 == (!record_malloc#105 && __CPROVER_malloc_is_new_array#82)

(E) __CPROVER_memory_leak#110 == (record_may_leak#109 ? malloc_res#103 : __CPROVER_memory_leak#84)

(E) malloc#return_value#111 == malloc_res#103

(E) return_value_malloc$4#118 == malloc#return_value#111

(E) dynamic_object$50.next#120 == (struct list *)return_value_malloc$4#118

(E) p#121 == q#68

(E) __CPROVER_deallocated#phi122 == ($guard#ls152 ? __CPROVER_deallocated#lb152 : __CPROVER_deallocated#104)
(E) __CPROVER_malloc_object#phi122 == ($guard#ls152 ? __CPROVER_malloc_object#lb152 : __CPROVER_malloc_object#106)
(E) __CPROVER_malloc_size#phi122 == ($guard#ls152 ? __CPROVER_malloc_size#lb152 : __CPROVER_malloc_size#107)
(E) __CPROVER_malloc_is_new_array#phi122 == ($guard#ls152 ? __CPROVER_malloc_is_new_array#lb152 : __CPROVER_malloc_is_new_array#108)
(E) __CPROVER_memory_leak#phi122 == ($guard#ls152 ? __CPROVER_memory_leak#lb152 : __CPROVER_memory_leak#110)
(E) q#phi122 == ($guard#ls152 ? q#lb152 : q#68)
(E) dynamic_object$50.next#phi122 == ($guard#ls152 ? dynamic_object$50.next#lb152 : dynamic_object$50.next#120)
(E) dynamic_object$102.next#phi122 == ($guard#ls152 ? dynamic_object$102.next#lb152 : dynamic_object$102.next)
(E) dynamic_object$131.next#phi122 == ($guard#ls152 ? dynamic_object$131.next#lb152 : dynamic_object$131.next)
(E) $cond#122 == FALSE
(E) $guard#122 == (FALSE || $guard#0 && TRUE)

(E) q#123 == dynamic_object$50.next#phi122
(E) $guard#123 == ($guard#122 && !$cond#122)

(E) malloc_size#127 == sizeof(struct list) /*8ul*/ 

(E) malloc_value$1#131 == (void *)&dynamic_object$131

(E) malloc_res#132 == malloc_value$1#131

(E) __CPROVER_deallocated#133 == (malloc_res#132 == __CPROVER_deallocated#phi122 ? NULL : __CPROVER_deallocated#phi122)

(E) __CPROVER_malloc_object#135 == (record_malloc#134 ? malloc_res#132 : __CPROVER_malloc_object#phi122)

(E) __CPROVER_malloc_size#136 == (record_malloc#134 ? malloc_size#127 : __CPROVER_malloc_size#phi122)

(E) __CPROVER_malloc_is_new_array#137 == (!record_malloc#134 && __CPROVER_malloc_is_new_array#phi122)

(E) __CPROVER_memory_leak#139 == (record_may_leak#138 ? malloc_res#132 : __CPROVER_memory_leak#phi122)

(E) malloc#return_value#140 == malloc_res#132

(E) return_value_malloc$5#147 == malloc#return_value#140

(E) dynamic_object$131.next#149 == (q#123 == &dynamic_object$131 ? (struct list *)return_value_malloc$5#147 : dynamic_object$131.next#phi122)
(E) dynamic_object$102.next#149 == (struct list *)return_value_malloc$5#147

(E) dynamic_object$50.next#150 == (q#123 == &dynamic_object$131 ? dynamic_object$131.next#149 : dynamic_object$102.next#149)

(E) $cond#152 == TRUE

(E) main#return_value#153 == 1
(E) $guard#153 == ($guard#122 && $cond#122)

(E) return'#161 == main#return_value#153

[peterschrammel]

Ok, so, removing unnecessary stuff, we have:

(E) $guard#0 == TRUE

(E) return_value_malloc$1#40 == (void *)&dynamic_object$24
(E) p#42 == (struct list *)return_value_malloc$1#40

(E) return_value_malloc$2#66 == (void *)&dynamic_object$50
(E) q#68 == (struct list *)return_value_malloc$2#66

(E) return_value_malloc$3#92 == (void *)&dynamic_object$76
(E) dynamic_object$24.next#94 == (struct list *)return_value_malloc$3#92

(E) return_value_malloc$4#118 == (void *)&dynamic_object$102
(E) dynamic_object$50.next#120 == (struct list *)return_value_malloc$4#118

(E) p#121 == q#68

LOOP HEAD:

(E) q#phi122 == ($guard#ls152 ? q#lb152 : q#68)
(E) dynamic_object$50.next#phi122 == ($guard#ls152 ? dynamic_object$50.next#lb152 : dynamic_object$50.next#120)
(E) dynamic_object$102.next#phi122 == ($guard#ls152 ? dynamic_object$102.next#lb152 : dynamic_object$102.next)
(E) dynamic_object$131.next#phi122 == ($guard#ls152 ? dynamic_object$131.next#lb152 : dynamic_object$131.next)
(E) $cond#122 == FALSE
(E) $guard#122 == (FALSE || $guard#0 && TRUE)

(E) q#123 == dynamic_object$50.next#phi122
(E) $guard#123 == ($guard#122 && !$cond#122)

(E) return_value_malloc$5#147 == (void *)&dynamic_object$131

(E) dynamic_object$131.next#149 == (q#123 == &dynamic_object$131 ? (struct list *)return_value_malloc$5#147 : dynamic_object$131.next#phi122)
(E) dynamic_object$102.next#149 == (struct list *)return_value_malloc$5#147

(E) dynamic_object$50.next#150 == (q#123 == &dynamic_object$131 ? dynamic_object$131.next#149 : dynamic_object$102.next#149)

(E) $cond#152 == TRUE

END OF LOOP

(E) main#return_value#153 == 1
(E) $guard#153 == ($guard#122 && $cond#122)

(E) return'#161 == main#return_value#153

[martinhruska]

The described problem should be solved by pull request #3. However, we will probably need to concretize also the dereferences in assertions to make the analysis more precise.