Comments (12)
martinhruska
commented on July 17, 2024
Is there any easy way how to print out the resulting ssa form of program?
from 2ls.
martinhruska
commented on July 17, 2024
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?
from 2ls.
viktormalik
commented on July 17, 2024
you can print the ssa using local_SSAt::output function
you can print any exprt expression using debug() << from_expr(...) -> see usage somewhere
from 2ls.
viktormalik
commented on July 17, 2024
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
from 2ls.
martinhruska
commented on July 17, 2024
OK and when we define it?
p = malloc();
p->next = ...;
p = ....;
while() {
x = p->next;
p->next = y;
}
from 2ls.
viktormalik
commented on July 17, 2024
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
from 2ls.
martinhruska
commented on July 17, 2024
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?
from 2ls.
viktormalik
commented on July 17, 2024
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.
from 2ls.
peterschrammel
commented on July 17, 2024
@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)?
from 2ls.
martinhruska
commented on July 17, 2024
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
from 2ls.
peterschrammel
commented on July 17, 2024
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
from 2ls.
martinhruska
commented on July 17, 2024
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.
from 2ls.
Related Issues (2)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from 2ls.