Convert references more consistently #1696

fbrausse · 2024-02-21T08:54:46Z

I believe this PR is quite ready now. It does 3 things:

The clang-cpp frontend unconditionally converts constructor calls including the implicit this parameter now. Before, it had been added (only in some cases, leading to bugs) by the adjustment phase.
The conversion between references (modelled as pointers with a #reference or #rvalue_reference flag set) and the concrete values are now done during the implicit casts performed by c_typecast. The effect is that for almost all¹ case, member accesses now work as they are expected to by the clang-c frontend, which the clang-cpp one derives from.
References to C++ union/struct/class members of reference type are now always dereferenced. This is in line with the interface the clang-c frontend set up.

¹ There is one corner case that doesn't work, yet: initialization of a member of reference type with another reference. With this PR, both are dereferenced and assigned. This is not intentional and will be addressed soon.

As a summary, 271 KNOWNBUGs have been fixed, but 5 new ones were added:

One for Solidity, this is Contract members appear to be interpreted as static and not as instance variables #1723
regression/esbmc-cpp/gcc-template-tests/qualttp16: dereference failure: Object accessed with illegal offset
(this is a logic error in the dereference module about zero-sized structs)
regression/esbmc-cpp/list/list_sort
regression/esbmc-cpp/template/template_sort_string: ERROR: Can't construct rvalue reference to array type during dereference (It isn't allowed by C anyway)
regression/esbmc-cpp/vector/ch10_5 has a huge amount of c_link warnings about duplicate symbols and now fails when constructing an address_of of an address_of expression

Additionally, I've disabled one of the unit tests, which was also constructing an address_of of ~~an address_of~~ a constant. This is not supported: addresses only exist for symbols or dereferenced expressions.

Edit: Oh, and some bugs have been fixed in <vector>, <iterator> and <string_view> OMs.

lucasccordeiro · 2024-02-21T11:01:49Z

Very nice PR :-)

fbrausse · 2024-02-22T11:09:21Z

@XLiZHI you worked on the CUDA OMs in the past. Could I ask whether you have an insight into why the CUDA tests are failing here or how to produce a reduced version of a failing test case? As these are C++-frontend changes I don't expect interleavings to play any role, so ideally a failing CUDA test case with just a single thread would be great to have.

XLiZHI · 2024-02-22T11:24:13Z

Could I ask whether you have an insight into why the CUDA tests are failing here

Hi @fbrausse ,

The counterexample seem to be array out of bounds problem, I suggest that we can start from the TCs of C++, such as regression/esbmc - cpp11 / constructors/MoveConstructor and regression/esbmc-cpp11/reference/Reference4

I think maybe fixing these TCs will solve the problems in the CUDA TCs.

fbrausse · 2024-02-27T00:19:13Z

OK, I'm reasonably happy so far, but 3 issues remain with this PR, as far as I can see:

The cuda (and string_view1) tests fail, because the pointer to the symbol being constructed is not passed as first argument to the constructor (__dim3 here).
The init_anon_symbol() call added for converting the clang::MaterializeTemporaryExpr does fix a bunch of cases with references (since we can now properly take the address of that symbol), but it causes the control flow generated by the conversion to go haywire, also in cuda, see the --goto-functions-only for assignIndexes(), that's where the wrong out-of-bounds comes from. Edit: I briefly tried using the new make_temporary() instead, but it didn't work. Don't know why, might be worth investigating as it has a very similar purpose.
In one of the tests we're running into an infinite recursion. That's why the CI is failing now. Here are the results for a local ctest run as of now (0cf6492): ctest8.txt

Besides that, the changes (mainly: treating conversions between references (modelled as pointers) and the actual values as implicit via gen_typecast()) do introduce a lot of *&var and &*ptr constructs, which ideally should be removed somewhere, probably in the GOTO processing.

As I've got to turn my attention to other things, I would be happy if someone could give me a hand in fixing these remaining issues.

fbrausse · 2024-02-27T00:46:36Z

Update: this is the current list of failing tests: ctest8.1.txt

lucasccordeiro · 2024-02-28T08:39:14Z

@fbrausse: try to liaise with @XLiZHI to check whether he can continue working on this PR; otherwise, IMHO, we should break this PR into smaller PRs; for the bit you need help, we could open an issue for someone else to work on it.

fbrausse · 2024-02-28T09:29:03Z

@fbrausse: try to liaise with @XLiZHI to check whether he can continue working on this PR; otherwise, IMHO, we should break this PR into smaller PRs; for the bit you need help, we could open an issue for someone else to work on it.

Thanks, Lucas. It's not clear to me how to split this PR into smaller parts right now, except for the OMs. I believe the above mentioned issues are fixed now. Let's see what the CI says.

For some reason symbolic types now arrive in the dereference module. Might be because of the temporary_object expressions, not sure, yet. It's easy to work-around via ns.follow(), though.

lucasccordeiro · 2024-02-28T09:40:31Z

That's great. Thanks, @fbrausse.

I think @XLiZHI is in Shangai to apply for his visa to come to the UK; he should be back soon to work with you on this PR if needed.

This is in order to be able to take the address.

…to deref

…onref

…alizers This is being taken care of by c_typecast now.

…ion" This reverts commit b8afb21.

…s reference See also <https://cplusplus.github.io/LWG/issue1280>. Fixes (at least) - regression/esbmc-cpp/cpp/ch21_19

This reverts commit 4350f66.

lucasccordeiro

I'm impressed by the number of regression tests that you have enabled with this PR! Well done!

Thanks for submitting this PR, @fbrausse.

fbrausse · 2024-02-29T19:04:09Z

Thanks, as a note of caution though: I had to disable one of @kunjsong01's optimizations, which means we now create more symbols for temporary values (such as the C++ constructors are using). This may lead to a slow-down for C++/Solidity, but I gathered it's better to be more correct than fast here.

lucasccordeiro · 2024-02-29T19:09:10Z

This may lead to a slow-down for C++/Solidity, but I gathered it's better to be more correct than fast here.

Yes, I fully support this.

lucasccordeiro · 2024-02-29T19:10:00Z

BTW, can I ask you to start an SV-COMP run here, @fbrausse?

fbrausse · 2024-03-01T02:24:51Z

Master:

Statistics:          23805 Files
  correct:           13965
    correct true:     7709
    correct false:    6256
  incorrect:            31
    incorrect true:     13
    incorrect false:    18
  unknown:            9809
  Score:             20970 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/8102075164

This PR:

Statistics:          23805 Files
  correct:           13955
    correct true:     7681
    correct false:    6274
  incorrect:            33
    incorrect true:     13
    incorrect false:    20
  unknown:            9817
  Score:             20900 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/81015176924

The 2 new incorrect are in no-data-race:

timeout -> incorrect (is also incorrect on master), timeout noise
unknown -> incorrect on master fails with
```
ERROR: Symbolic type id in size_typet::size_bits
symbol
* symbol_name : tag-struct s
```
This got fixed by adding the ns.follow() in dereference(). Seems like we had symbolic types arriving in dereference already before this PR.

Interestingly, there are also unknown -> correct (and unknown -> timeout) ones in no-data-race, that had the same problem on master.

Besides that, there are 6 timeout -> out-of-memory ones in unreach-call (while all the other benchmarks don't seem to have significantly different memory usage):

c/loops/heavy-1.c
c/loops-crafted-1/nested3-1.c
c/loops-crafted-1/nested3-1_abstracted.c
c/loops-crafted-1/nested3-2.c
c/loops-crafted-1/nested3-2_abstracted.c
c/loops-crafted-1/nested5-2.c

I'll check whether those are noise.

lucasccordeiro · 2024-03-01T06:16:47Z

Many thanks, @fbrausse. This PR is a great addition to the ESBMC project.

These results are great! If there are still further improvements, we could write small PRs.

XLiZHI · 2024-03-04T07:10:38Z

src/util/c_typecast.cpp

+        "implicit typecast of reference to incompatible non-reference type?");
+    }
+  }
+  else if (dest_type.id() == "pointer")


We used the else if here, which allows us to skip the subsequent adjustments, which I think is why we encountered ERROR: Can't construct rvalue reference to array type during dereference (It isn't allowed by C anyway).

Update: Until cc23115 esbmc did not appear this error, it affects some OM TCs at present, for example stack.

struct B { }; struct list { B list[10]; }; int main () { list mylist; return 0; }

XLiZHI · 2024-03-04T07:13:05Z

src/cpp/library/new

+void *operator new(std::size_t count, void *ptr)
+{
+  return ptr;
+}


why we need placement new?

fbrausse added the C++ Anything related to C++ verification label Feb 21, 2024

fbrausse linked an issue Feb 21, 2024 that may be closed by this pull request

[C++ frontend] ERROR: Unrecognized address_of operand #1694

Closed

fbrausse force-pushed the fb/fix-1694 branch 2 times, most recently from 1af1a5d to 62b20d4 Compare February 21, 2024 10:40

fbrausse force-pushed the fb/fix-1694 branch 3 times, most recently from d74df91 to ebd52b9 Compare February 26, 2024 14:41

fbrausse mentioned this pull request Feb 29, 2024

Contract members appear to be interpreted as static and not as instance variables #1723

Open

fbrausse force-pushed the fb/fix-1694 branch from c2d4d89 to 4120e6c Compare February 29, 2024 07:10

fbrausse removed a link to an issue Feb 29, 2024

[C++ frontend] ERROR: Unrecognized address_of operand #1694

Closed

fbrausse added 12 commits February 29, 2024 10:01

[clang-c] convert: move init of anon symbol to separate function

83c0fc4

[clang-cpp] convert: dereference reference-typed VarDecls

88c54c7

[clang-cpp] convert: intro new anon symbol for materialized temporaries

80db274

This is in order to be able to take the address.

[regression] fix 77 cases, 3 new bugs

4ac7787

[regression] add simplified case from #1694

771afc2

[clang] skip intermediate reference types when getting a reference type

f74d7bb

[clang-cpp] simplify

bd74f61

[clang] take reference return type into account for function calls

6738706

[clang-cpp] unify code structure in get_decl_ref() + add annotations …

f1e2bb6

…to deref

[util] c_typecast: handle both directions of implicit conv. ref <-> n…

f9ad7db

…onref

[clang-cpp] adjust code: rm unnecessary adjustment of reference initi…

05aacd0

…alizers This is being taken care of by c_typecast now.

[regression] fix 54 more KNOWNBUG

6af42e1

fbrausse added 5 commits February 29, 2024 10:01

[regression] revert falsely fixing 5 KNOWNBUG

203b1eb

Revert "[clang-c] convert: move init of anon symbol to separate funct…

40f0a5c

…ion" This reverts commit b8afb21.

[regression] add KNOWNBUG, this is #1723

dd29145

[cpp] fix <string_view>: includes + avoid unsupported nullptr

87e974c

[regression] pass --cppstd 17 to string_view TCs

0d2634f

fbrausse force-pushed the fb/fix-1694 branch from 6b376e8 to 0d2634f Compare February 29, 2024 09:01

fbrausse added 7 commits February 29, 2024 13:47

[cpp] fix ostream_iterator: store pointer to stream + post-inc return…

fdf9bfd

…s reference See also <https://cplusplus.github.io/LWG/issue1280>. Fixes (at least) - regression/esbmc-cpp/cpp/ch21_19

[regression] fixed 4 KNOWNBUG

7a1b604

Revert "[regression] fixed 1 KNOWNBUG"

51588f3

This reverts commit 4350f66.

[regression] fixed 1 KNOWNBUG

9d96e8d

[regression] fixed 4 KNOWNBUG

6b1b933

[unit] disable test leading to an invalid addr_of of an addr_of

b3fcbd6

[regression] add 4 new KNOWNBUG

654be36

fbrausse requested review from lucasccordeiro, kunjsong01 and XLiZHI February 29, 2024 18:50

fbrausse marked this pull request as ready for review February 29, 2024 18:50

lucasccordeiro approved these changes Feb 29, 2024

View reviewed changes

fbrausse added the needs-svcomp-run label Feb 29, 2024

fbrausse removed the needs-svcomp-run label Mar 1, 2024

lucasccordeiro merged commit ddf073a into master Mar 1, 2024
14 checks passed

lucasccordeiro deleted the fb/fix-1694 branch March 1, 2024 06:15

XLiZHI reviewed Mar 4, 2024

View reviewed changes

XLiZHI mentioned this pull request Mar 4, 2024

[C++ Verification] ERROR: Can't construct rvalue reference to array type during dereference #1729

Closed

XLiZHI mentioned this pull request Mar 28, 2024

[C++ frontend] ERROR: Unrecognized address_of operand #1694

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Convert references more consistently #1696

Convert references more consistently #1696

fbrausse commented Feb 21, 2024 •

edited

Loading

lucasccordeiro commented Feb 21, 2024

fbrausse commented Feb 22, 2024

XLiZHI commented Feb 22, 2024 •

edited

Loading

fbrausse commented Feb 27, 2024 •

edited

Loading

fbrausse commented Feb 27, 2024

lucasccordeiro commented Feb 28, 2024

fbrausse commented Feb 28, 2024

lucasccordeiro commented Feb 28, 2024

lucasccordeiro left a comment

fbrausse commented Feb 29, 2024 •

edited

Loading

lucasccordeiro commented Feb 29, 2024

lucasccordeiro commented Feb 29, 2024

fbrausse commented Mar 1, 2024

lucasccordeiro commented Mar 1, 2024

XLiZHI Mar 4, 2024 •

edited

Loading

XLiZHI Mar 4, 2024 •

edited

Loading

XLiZHI Mar 4, 2024

Convert references more consistently #1696

Convert references more consistently #1696

Conversation

fbrausse commented Feb 21, 2024 • edited Loading

lucasccordeiro commented Feb 21, 2024

fbrausse commented Feb 22, 2024

XLiZHI commented Feb 22, 2024 • edited Loading

fbrausse commented Feb 27, 2024 • edited Loading

fbrausse commented Feb 27, 2024

lucasccordeiro commented Feb 28, 2024

fbrausse commented Feb 28, 2024

lucasccordeiro commented Feb 28, 2024

lucasccordeiro left a comment

Choose a reason for hiding this comment

fbrausse commented Feb 29, 2024 • edited Loading

lucasccordeiro commented Feb 29, 2024

lucasccordeiro commented Feb 29, 2024

fbrausse commented Mar 1, 2024

lucasccordeiro commented Mar 1, 2024

XLiZHI Mar 4, 2024 • edited Loading

Choose a reason for hiding this comment

XLiZHI Mar 4, 2024 • edited Loading

Choose a reason for hiding this comment

XLiZHI Mar 4, 2024

Choose a reason for hiding this comment

fbrausse commented Feb 21, 2024 •

edited

Loading

XLiZHI commented Feb 22, 2024 •

edited

Loading

fbrausse commented Feb 27, 2024 •

edited

Loading

fbrausse commented Feb 29, 2024 •

edited

Loading

XLiZHI Mar 4, 2024 •

edited

Loading

XLiZHI Mar 4, 2024 •

edited

Loading