Two problems after modifying CFA
15 views
Skip to first unread message
Liangchen
Nov 5, 2023, 9:20:37 AM11/5/23
to CPAchecker Users
Dear Developers,
I have modified mutableCFA and then transfer to CFA in CFACreator.java, just like picture 1. But after executing, I found output CFA is still original CFA, it's now my modified CFA. And I try to debug output function, just like picture 2(line 55) and picture 3, I found the object cfa is my modified CFA, but object dotGenerator is still original CFA. I wonder why I have modified CFA when it was MutableCFA, but it can't output.
By the way, After I modified CFA when it was MutableCFA, but it can't be used to verify.Just like picture 4, I found object cfa in line 327 is my modified CFA, such as edge[17] is "[a<3]",but this CFA wasn't used to verifiy, CPAchecker still use original CFA to verify. I want to know how to let CPAchecker use modified CFA to verify.
Thanks very much,
Yours,Liangchen
Liangchen
Nov 5, 2023, 9:25:08 AM11/5/23
to CPAchecker Users
Sorry, the order of pictures is wrong, picture 1 I mentioned is the third picture, picture 2 and 3 is the first and second. Picture 4 is in right position
Philipp Wendler
Nov 6, 2023, 9:45:37 AM11/6/23
to cpacheck...@googlegroups.com
Dear Liangchen,
Am 05.11.23 um 15:20 schrieb Liangchen:
in your CFA modification and how exactly you do that.
Note that MutableCFA is *not* a general-purpose data structure for a CFA
that allows arbitrary modifications. MutableCFA is a temporary data
structure used during CFA creation while we may still make *some*
modifications.
So if you change something, you must take care on your own that all
relevant invariants still hold, as MutableCFA may or may not contain
code that updates them. For example, all the various data structures
inside MutableCFA need to updated accordingly, and the data structure
that is formed out of the CFANodes and CFAEdges (via their attributes)
also needs to match that. If you just change something, the existing
code does not provide a guarantee that the CFA is kept consistent.
Furthermore, also pay close attention to the comment that is there where
you inserted the code. If you do any modifications in this place, it is
your responsibility to ensure that any data in stuff like the loop
structure and the post-order ids is kept consistent with the new CFA.
My recommendation would be to think hard if you really need to modify
the CFA. In many cases, our experience shows that one doesn't and that
it is easier to do something during the analysis rather than during CFA
construction. For example, it seems that you want to reduce the CFA
somewhat. If you do that in order to optimize out irrelevant parts, then
note that we have that already but that we do it later during the
analysis, where we can just skip edges that are irrelevant. This keeps
the CFA intact, is much easier to handle, and creates much fewer problems.
If you want to somehow change what the CFA looks for specific program
constructs, then it should be easier to do that right during the
creation of the respective edges in the first place.
If you do need to mutate the CFA, I recommend to do it before most
post-processing steps are done, i.e., in step 2 of CFACreator.
Btw: Please never use screenshots for code, this just doesn't make
sense. Code is plain text, but text in pixel pictures is just
unnecessarily hard to read due to scaling, color schemes, font choices,
etc., it is not accessible, not searchable, has lots of irrelevant
details such as the rest of your IDE window, and blows up the email
size. See for example also these StackOverflow guidelines:
https://meta.stackoverflow.com/a/285557/396730
Or this blog post: https://jakeworth.com/on-code-screenshots/
Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
Am 05.11.23 um 15:20 schrieb Liangchen:
> I have modified mutableCFA and then transfer to CFA in CFACreator.java,
> just like picture 1. But after executing, I found output CFA is still
> original CFA, it's now my modified CFA. And I try to debug output function,
> just like picture 2(line 55) and picture 3, I found the object cfa is my
> modified CFA, but object dotGenerator is still original CFA. I wonder why I
> have modified CFA when it was MutableCFA, but it can't output.
> By the way, After I modified CFA when it was MutableCFA, but it can't be
> used to verify.Just like picture 4, I found object cfa in line 327 is my
> modified CFA, such as edge[17] is "[a<3]",but this CFA wasn't used to
> verifiy, CPAchecker still use original CFA to verify. I want to know how to
> let CPAchecker use modified CFA to verify.
This is not possible to answer for us, because it depends on what you do
> just like picture 1. But after executing, I found output CFA is still
> original CFA, it's now my modified CFA. And I try to debug output function,
> just like picture 2(line 55) and picture 3, I found the object cfa is my
> modified CFA, but object dotGenerator is still original CFA. I wonder why I
> have modified CFA when it was MutableCFA, but it can't output.
> By the way, After I modified CFA when it was MutableCFA, but it can't be
> used to verify.Just like picture 4, I found object cfa in line 327 is my
> modified CFA, such as edge[17] is "[a<3]",but this CFA wasn't used to
> verifiy, CPAchecker still use original CFA to verify. I want to know how to
> let CPAchecker use modified CFA to verify.
in your CFA modification and how exactly you do that.
Note that MutableCFA is *not* a general-purpose data structure for a CFA
that allows arbitrary modifications. MutableCFA is a temporary data
structure used during CFA creation while we may still make *some*
modifications.
So if you change something, you must take care on your own that all
relevant invariants still hold, as MutableCFA may or may not contain
code that updates them. For example, all the various data structures
inside MutableCFA need to updated accordingly, and the data structure
that is formed out of the CFANodes and CFAEdges (via their attributes)
also needs to match that. If you just change something, the existing
code does not provide a guarantee that the CFA is kept consistent.
Furthermore, also pay close attention to the comment that is there where
you inserted the code. If you do any modifications in this place, it is
your responsibility to ensure that any data in stuff like the loop
structure and the post-order ids is kept consistent with the new CFA.
My recommendation would be to think hard if you really need to modify
the CFA. In many cases, our experience shows that one doesn't and that
it is easier to do something during the analysis rather than during CFA
construction. For example, it seems that you want to reduce the CFA
somewhat. If you do that in order to optimize out irrelevant parts, then
note that we have that already but that we do it later during the
analysis, where we can just skip edges that are irrelevant. This keeps
the CFA intact, is much easier to handle, and creates much fewer problems.
If you want to somehow change what the CFA looks for specific program
constructs, then it should be easier to do that right during the
creation of the respective edges in the first place.
If you do need to mutate the CFA, I recommend to do it before most
post-processing steps are done, i.e., in step 2 of CFACreator.
Btw: Please never use screenshots for code, this just doesn't make
sense. Code is plain text, but text in pixel pictures is just
unnecessarily hard to read due to scaling, color schemes, font choices,
etc., it is not accessible, not searchable, has lots of irrelevant
details such as the rest of your IDE window, and blows up the email
size. See for example also these StackOverflow guidelines:
https://meta.stackoverflow.com/a/285557/396730
Or this blog post: https://jakeworth.com/on-code-screenshots/
Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
Reply all
Reply to author
Forward
0 new messages