Just as a heads-up, this is not the right fix: The rules regarding type promotion in ?: are different for C and C++. If this fixes only some C++ test cases, I'm pretty sure C ones will fail.

Just as a heads-up, this is not the right fix: The rules regarding type promotion in ?: are different for C and C++. If this fixes only some C++ test cases, I'm pretty sure C ones will fail.

Hi @fbrausse ,

Thanks for your suggestion.

Should I handle ?: in C++ frontend instead of C?

Should I handle ?: in C++ frontend instead of C?

If possible, yes. I tried your change earlier as well, that's how I know. See, e.g., "Usual arithmetic conversions" for C and "Conditional operator" for C++.

See, e.g., "Usual arithmetic conversions" for C and "Conditional operator" for C++.

Thanks for the reference. For C++, I think maybe we don't need to do something like "Usual arithmetic conversions". With Clang C++ AST I think we've got enough information. See the results for CI, where we failed one TC for C and fixed several for C++.

	979 - regression/esbmc/memset-const-no-simpl (Failed)
	1775 - regression/k-induction/cpp_stack_top_bug (Failed)
	2378 - regression/esbmc-cpp/cpp/ch2_5 (Failed)
	2503 - regression/esbmc-cpp/cpp/cpp_stack_top_bug (Failed)
	2551 - regression/esbmc-cpp/cpp/llbmc_stack-test (Failed)
	3291 - regression/esbmc-cpp/deque/deque_empty (Failed)
	3292 - regression/esbmc-cpp/deque/deque_empty_bug (Failed)
	3611 - regression/esbmc-cpp/stack/stack_empty_bug (Failed)
	3612 - regression/esbmc-cpp/stack/stack_pop (Failed)
	3613 - regression/esbmc-cpp/stack/stack_pop_bug (Failed)
	3615 - regression/esbmc-cpp/stack/stack_push_bug (Failed)
	3669 - regression/esbmc-cpp/vector/ch11_16 (Failed)
	3677 - regression/esbmc-cpp/vector/ch11_24 (Failed)
	3687 - regression/esbmc-cpp/vector/ch21_10 (Failed)
	3726 - regression/esbmc-cpp/vector/vector30 (Failed)
	3748 - regression/esbmc-cpp/vector/vector50 (Failed)

For now, I think we can implement adjusting if in a C++ front-end, what do you think?

For C++, I think maybe we don't need to do something like "Usual arithmetic conversions".

I think we do, see 6.2):

However, 6.1) says that, if they have the same type, then something special happens. Only otherwise the usual arith. conv. are being performed.

For now, I think we can implement adjusting if in a C++ front-end, what do you think?

That would be great, yeah. Maybe you can put the C handling of ?: into a virtual method and override it in the C++ frontend?

Edit: In particular item 6.1) is missing for C, so even in cond ? (char)1 : (char)2 both sides should be typecast to int.

see 6.2):

oh, I see. thanks.

However, 6.1) says that, if they have the same type, then something special happens. Only otherwise the usual arith. conv. are being performed.

I would like to ask is the implicit typecast provided in the AST not available? I think maybe we can use the information in the AST directly? Isn't that accurate information?

Do you have a cpp test case where this is failing? I'm surprised that clang doesn't abort before even generating the ast

Do you have a cpp test case where this is failing? I'm surprised that clang doesn't abort before even generating the ast

Hi @mikhailramalho ,

int main ()
{
  int b = 1;
  int *p = &b;
  int *a = 1? p: &b;
}

or

int main ()
{
 const char* a = true? "b":"c";
}

Can you double-check it?

I'm using esbmc fe3125b and it works just fine:

$ cat main1.cpp
#include <cassert>

int main ()
{
  int b = 1;
  int *p = &b;
  int *a = 1? p: &b;
  assert(a == &b);
}

$ esbmc main1.cpp
ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main1.cpp
Converting
Generating GOTO Program
GOTO program creation time: 0.126s
GOTO program processing time: 0.000s
Starting Bounded Model Checking
Symex completed in: 0.001s (16 assignments)
Slicing time: 0.000s (removed 15 assignments)
Generated 1 VCC(s), 1 remaining after simplification (1 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.3
Runtime decision procedure: 0.000s
BMC program time: 0.001s

VERIFICATION SUCCESSFUL

Can you double-check it?

oh, I thought you wanted the code for the AST above, I just gave an example to see that the AST provides type information.

Please use this code:

int main ()
{
 const char* a = true? "b":"c";
}

ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main.cpp
Converting
Generating GOTO Program
esbmc: /home/lucas/ESBMC_Project/esbmc/src/irep2/irep2_expr.h:1959: if2t::if2t(const type2tc&, const expr2tc&, const expr2tc&, const expr2tc&): Assertion `type->type_id == trueval->type->type_id' failed.
Aborted

I got the crash now, but surprisingly esbmc doesn't crash in release builds, i.e., our backend manages to handle this code just fine... Is the assertion too restrictive? Although I agree that we are missing a cast there.

Also, the goto program is weird:

        // 21 file main1.cpp line 3 column 2 function main
        a=&(true ? &"b"[0] : &"c"[0])[0];

I would like to ask is the implicit typecast provided in the AST not available? I think maybe we can use the information in the AST directly? Isn't that accurate information?

The problem is not accuracy but what later stages of the verification expect. In an ideal world, we would convert the clang AST and everything would work just fine (or better still, we could use clang AST directly), but in reality, it is not that simple.

Although I agree that we are missing a cast there.

I don't think we're missing cast, instead it's doing extra cast.

I'm a little confused about why the type returned here is ptr.

Also, the goto program is weird

This is because Clang AST generates char[2] as the type:

Where is the extra cast you mentioned in the goto code?

This is the failed assertion:

(gdb) p type->dump()
array
* subtype : signedbv
    * width : 8
* array_size : constant_int
    * value : 2
    * type : unsignedbv
      * width : 64
* size_is_infinite : false
$1 = void

(gdb) p trueval->type->dump()
type : pointer
* subtype : signedbv
    * width : 8
$2 = void

either we are missing the implicit cast from pointer to array or the assertion is being too restrictive. I vaguely remember we had an is_implicit_convertible check somewhere, maybe we should use that in the irep2 assertion

On line 133, a type cast is performed. turn op1 and op2's array into pointer.

I have some questions about this assertion, since we are comparing the type generated by Clang AST as the correct type, why don't we just cast to this type.

Master:

Statistics:          23805 Files
  correct:           13829
    correct true:     7618
    correct false:    6211
  incorrect:            24
    incorrect true:     13
    incorrect false:    11
  unknown:            9952
  Score:             20855
  
  https://github.com/esbmc/esbmc/actions/runs/7979388958/job/21787274434

This PR:

Statistics:          23805 Files
  correct:           13837
    correct true:     7621
    correct false:    6216
  incorrect:            24
    incorrect true:     13
    incorrect false:    11
  unknown:            9944
  Score:             20866 (max: 38482)
  
  https://github.com/esbmc/esbmc/actions/runs/7979387573/job/21787263854

I only applied the changes in the C++ frontend, I think this PR has no impact on C verification.

I have some questions about this assertion, since we are comparing the type generated by Clang AST as the correct type, why don't we just cast to this type.

Valid point. Parse trees for 0 ? (char)1 : (char)2 in C:

and in C++:

Clang is already giving us correctly-cast operands to ?:. Could it be that the adjuster itself is modifying the operands such that there is a need for typecasts afterwards?