Clang-15+ based frontends cause regressions about esbmc HOT 4 CLOSED

Hi @fbrausse , It is not clear to me why the Clang version or C++ version affects the results. Maybe the AST has changed?

Their AST changes with different versions. Usually not much, like between versions 11 and 14 there are barely any changes affecting us. However, in this case, if you just compile against Clang/LLVM-15 instead, the three examples above will get parsed into a slightly different AST. As far as I can tell, this mainly affects std::move.

Could you please update the BUILDING.md about Clang-16 after this PR was merged? Or can you provide goto functions for them?

I'm not sure what you want me to do here. Just use a different version of Clang. I don't have pre-compiled packages, but Ubuntu has them.

Edit: Note, this is Clang-15, not 16. It's independent of my PR.

from esbmc.

Hi @fbrausse , It is not clear to me why the Clang version or C++ version affects the results. Maybe the AST has changed?

Could you please update the BUILDING.md about Clang-16 after this PR was merged? Or can you provide goto functions for them?

from esbmc.

https://releases.llvm.org/15.0.0/tools/clang/docs/ReleaseNotes.html

Improved -O0 code generation for calls to std::move, std::forward, std::move_if_noexcept, std::addressof, and std::as_const. These are now treated as compiler builtins and implemented directly, rather than instantiating the definition from the standard library.

I spent a day looking into this issue, since clang 15 the std::move function has been omitted and will be implemented directly in the compiler, I tried the following patch and it worked.

Hi @fbrausse, may I have your opinion?

diff --git a/src/clang-c-frontend/clang_c_convert.cpp b/src/clang-c-frontend/clang_c_convert.cpp
index 2cf2adf08..74e8cc63e 100644
--- a/src/clang-c-frontend/clang_c_convert.cpp
+++ b/src/clang-c-frontend/clang_c_convert.cpp
@@ -1766,6 +1766,16 @@ bool clang_c_convertert::get_expr(const clang::Stmt &stmt, exprt &new_expr)

     const clang::Stmt *callee = function_call.getCallee();

+#if CLANG_VERSION_MAJOR > 14
+    if (function_call.isCallToStdMove())
+    {
+      if (get_expr(*function_call.getArg(0), new_expr))
+        return true;
+
+      break;
+    }
+#endif
+
     exprt callee_expr;
     if (get_expr(*callee, callee_expr))
       return true;

from esbmc.

Hi @XLiZHI. Many thanks for looking into it! This seems like a good fix indeed. Could you open a PR? We should see the number of failing tests for clang-16 go down from 6 to 3 or maybe even to zero.

from esbmc.