-
Notifications
You must be signed in to change notification settings - Fork 88
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Help needed] [clang-cpp] Support ArrayInitLoopExpr #1793
base: master
Are you sure you want to change the base?
[Help needed] [clang-cpp] Support ArrayInitLoopExpr #1793
Conversation
This is used in copy/move ctors for arrays, lambdas that capture arrays by value and decomposition expressions.
Looks to me like this is generating a I also noticed you keep an empty |
symbolt source_array_symbol = tmp_symbol.new_symbol( | ||
context, array_element_ptr_type, "array_init_loop_expr_tmp"); | ||
context.add(source_array_symbol); | ||
source_array_symbol.lvalue = true; | ||
source_array_symbol.value = source_array_expr; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The .new_symbol() call already registers the symbol with the context (hence it returns a reference), no need to add it again. In fact, it should be accessed by reference, otherwise you're modifying a copy outside of the context with the last 2 statements.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
hey @intrigus-lgtm I think we need to take a step back here and check if this is the correct approach. TBH, the adjust code seems a bit over-engineered.
Whenever we work on the frontend I always suggest we first check if the feature works in the old frontend, then on cbmc. If it does in either of them, half of the work is done.
For this one, cbmc does support the feature, so it's very likely that if we create an irep similar to the one there, the rest of esbmc will process it properly, in this case, the irep is:
0: code
* type: empty
* statement: decl_block
0: code
* type: empty
* #source_location:
* file: main2.cpp
* line: 8
* function: main
* statement: decl
0: symbol
* type: struct_tag
* identifier: tag-a
* identifier: main::1::d
* #lvalue: 1
1: struct
* type: struct_tag
* identifier: tag-a
* #source_location:
* file: main2.cpp
* line: 8
* function: main
0: array
* type: array
* #member_name: tag-a
* size: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 3
0: signedbv
* width: 32
* #c_type: signed_int
* #source_location:
* file: main2.cpp
* line: 8
* function: main
0: constant
* type: signedbv
* width: 32
* #c_type: signed_int
* #source_location:
* file: main2.cpp
* line: 8
* function: main
* value: 0
1: constant
* type: signedbv
* width: 32
* #c_type: signed_int
* #source_location:
* file: main2.cpp
* line: 8
* function: main
* value: 0
2: constant
* type: signedbv
* width: 32
* #c_type: signed_int
* #source_location:
* file: main2.cpp
* line: 8
* function: main
* value: 0
Can you try to create a similar irep on the convert file?
Bear in mind that esbmc has some different names for stuff (e.g, location instead of source_location), so you'll probably need to take a look around to see what's used in esbmc. |
For reference, this is the symbol table of CBMC. Symbol......: main
Pretty name.: main()
Module......: main8
Base name...: main
Mode........: C
Type........: signed int (void)
Value.......: {
struct a d={ .a::b={ 0, 0, 0 } };
struct a e;
e = d;
}
Flags.......:
Location....: file main8.cpp line 5
Symbol......: main::1::d
Pretty name.: main::1::d
Module......: main8
Base name...: d
Mode........: cpp
Type........: struct a
Value.......: { .b={ 0, 0, 0 } }
Flags.......: lvalue thread_local file_local
Location....: file main8.cpp line 7 function main
Symbol......: main::1::e
Pretty name.: main::1::e
Module......: main8
Base name...: e
Mode........: cpp
Type........: struct a
Value.......:
Flags.......: lvalue thread_local file_local
Location....: file main8.cpp line 8 function main |
@mikhailramalho struct a { int b[3]; };
struct a d={};
struct a e;
e = d; // THIS
e.b = d.b // Hypothetical syntax I could also not get my example to work with the old c++ frontend; it seems that it doesn't like aggregate inits. Wouldn't it be better to try to represent the clang ast as faithfully as possible instead of assuming that it will always have a certain shape? |
hey, so cbmc also verifies cpp files, so just create a foo.cpp file and paste your code there. To print the symbol table, run cbmc with --show-symbol-table. I also use this patch to print the ireps:
cbmc doesn't handle the cassert header either, so you'll need to use __CPROVER_assert instead. The symbol table and irep for:
is
|
Wow, I didn't know that. Thank you very much! I'll try to look into this a bit more later this week/next week. |
@intrigus-lgtm: Can I ask you whether you had a chance to advance with this PR? Please let us know if you need further support. |
@lucasccordeiro: sorry, I was super busy the last two weeks with (co-)organizing GPN CTF. |
This PR tries to fix #1792.
Unfortunately I could not get this to really work.
My proof of concept (basically: 6bad2dd#diff-784347884400427356b283749ef36cc6e458d4d4df4f8e3a2a4007244a637b1eR1057-R1176) which I implemented in
clang_cpp_convert.cpp
actually successfully verified the test case, however I would assume that this would be the wrong place for the code.I was thinking that
clang_cpp_adjust_expr.cpp
would be a better place, so I tried to move my code there.However it fails with
migrate expr failed
.I would really appreciate if someone could take a look at this or guide me because I feel like this should be pretty simple to implement for someone that is more familiar with the code.
The high level goal of the PR is to support code like this:
When copying
d
toe
, the arrayb
also has to be copied.Clang represents that using an
ArrayInitLoopExpr
.So basically this should compile to this code:
Currently it looks like this (maybe that is the problem?):
(The
dag_match_replace_helper
stuff can be moved elsewhere if needed)