Skip to content

Commit 4e2e372

Browse files
tautschnigtautschnig
authored
Merge pull request #5912 from tautschnig/refactor-expr2c
Refactor expr2ct::convert_with_precedence to avoid MSVC limitation
2 parents 551ac6e + a4ef885 commit 4e2e372

File tree

2 files changed

+58
-120
lines changed

2 files changed

+58
-120
lines changed

‎src/ansi-c/expr2c.cpp

Lines changed: 55 additions & 120 deletions
Original file line numberDiff line numberDiff line change
@@ -3415,21 +3415,6 @@ std::string expr2ct::convert_with_precedence(
34153415
else if(src.id()==ID_unary_plus)
34163416
return convert_unary(to_unary_expr(src), "+", precedence = 15);
34173417

3418-
else if(src.id()==ID_floatbv_plus)
3419-
return convert_function(src, "FLOAT+");
3420-
3421-
else if(src.id()==ID_floatbv_minus)
3422-
return convert_function(src, "FLOAT-");
3423-
3424-
else if(src.id()==ID_floatbv_mult)
3425-
return convert_function(src, "FLOAT*");
3426-
3427-
else if(src.id()==ID_floatbv_div)
3428-
return convert_function(src, "FLOAT/");
3429-
3430-
else if(src.id()==ID_floatbv_rem)
3431-
return convert_function(src, "FLOAT%");
3432-
34333418
else if(src.id()==ID_floatbv_typecast)
34343419
{
34353420
const auto &floatbv_typecast = to_floatbv_typecast_expr(src);
@@ -3479,21 +3464,6 @@ std::string expr2ct::convert_with_precedence(
34793464
return convert_function(src, "__builtin_popcount");
34803465
}
34813466

3482-
else if(src.id() == ID_r_ok)
3483-
return convert_function(src, "R_OK");
3484-
3485-
else if(src.id() == ID_w_ok)
3486-
return convert_function(src, "W_OK");
3487-
3488-
else if(src.id() == ID_is_invalid_pointer)
3489-
return convert_function(src, "IS_INVALID_POINTER");
3490-
3491-
else if(src.id()==ID_good_pointer)
3492-
return convert_function(src, "GOOD_POINTER");
3493-
3494-
else if(src.id()==ID_object_size)
3495-
return convert_function(src, "OBJECT_SIZE");
3496-
34973467
else if(src.id()=="pointer_arithmetic")
34983468
return convert_pointer_arithmetic(src, precedence=16);
34993469

@@ -3511,85 +3481,18 @@ std::string expr2ct::convert_with_precedence(
35113481
return id2string(src.id());
35123482
}
35133483

3514-
else if(src.id()==ID_infinity)
3515-
return convert_function(src, "INFINITY");
3516-
35173484
else if(src.id()=="builtin-function")
35183485
return src.get_string(ID_identifier);
35193486

3520-
else if(src.id()==ID_pointer_object)
3521-
return convert_function(src, "POINTER_OBJECT");
3522-
3523-
else if(src.id() == ID_get_must)
3524-
return convert_function(src, CPROVER_PREFIX "get_must");
3525-
3526-
else if(src.id() == ID_get_may)
3527-
return convert_function(src, CPROVER_PREFIX "get_may");
3528-
3529-
else if(src.id()=="object_value")
3530-
return convert_function(src, "OBJECT_VALUE");
3531-
35323487
else if(src.id()==ID_array_of)
35333488
return convert_array_of(src, precedence=16);
35343489

3535-
else if(src.id()==ID_pointer_offset)
3536-
return convert_function(src, "POINTER_OFFSET");
3537-
3538-
else if(src.id()=="pointer_base")
3539-
return convert_function(src, "POINTER_BASE");
3540-
3541-
else if(src.id()=="pointer_cons")
3542-
return convert_function(src, "POINTER_CONS");
3543-
3544-
else if(src.id() == ID_is_invalid_pointer)
3545-
return convert_function(src, CPROVER_PREFIX "is_invalid_pointer");
3546-
3547-
else if(src.id() == ID_dynamic_object)
3548-
return convert_function(src, "DYNAMIC_OBJECT");
3549-
3550-
else if(src.id() == ID_is_dynamic_object)
3551-
return convert_function(src, "IS_DYNAMIC_OBJECT");
3552-
3553-
else if(src.id()=="is_zero_string")
3554-
return convert_function(src, "IS_ZERO_STRING");
3555-
3556-
else if(src.id()=="zero_string")
3557-
return convert_function(src, "ZERO_STRING");
3558-
3559-
else if(src.id()=="zero_string_length")
3560-
return convert_function(src, "ZERO_STRING_LENGTH");
3561-
3562-
else if(src.id()=="buffer_size")
3563-
return convert_function(src, "BUFFER_SIZE");
3564-
3565-
else if(src.id()==ID_isnan)
3566-
return convert_function(src, "isnan");
3567-
3568-
else if(src.id()==ID_isfinite)
3569-
return convert_function(src, "isfinite");
3570-
3571-
else if(src.id()==ID_isinf)
3572-
return convert_function(src, "isinf");
3573-
35743490
else if(src.id()==ID_bswap)
35753491
return convert_function(
35763492
src,
35773493
"__builtin_bswap" + integer2string(*pointer_offset_bits(
35783494
to_unary_expr(src).op().type(), ns)));
35793495

3580-
else if(src.id()==ID_isnormal)
3581-
return convert_function(src, "isnormal");
3582-
3583-
else if(src.id()==ID_builtin_offsetof)
3584-
return convert_function(src, "builtin_offsetof");
3585-
3586-
else if(src.id()==ID_gcc_builtin_va_arg)
3587-
return convert_function(src, "gcc_builtin_va_arg");
3588-
3589-
else if(src.id()==ID_alignof)
3590-
// C uses "_Alignof", C++ uses "alignof"
3591-
return convert_function(src, "alignof");
3592-
35933496
else if(has_prefix(src.id_string(), "byte_extract"))
35943497
return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);
35953498

@@ -3734,27 +3637,6 @@ std::string expr2ct::convert_with_precedence(
37343637
else if(src.id()==ID_equal)
37353638
return convert_binary(to_equal_expr(src), "==", precedence = 9, true);
37363639

3737-
else if(src.id()==ID_ieee_float_equal)
3738-
return convert_function(src, "IEEE_FLOAT_EQUAL");
3739-
3740-
else if(src.id()==ID_width)
3741-
return convert_function(src, "WIDTH");
3742-
3743-
else if(src.id()==ID_concatenation)
3744-
return convert_function(src, "CONCATENATION");
3745-
3746-
else if(src.id()==ID_ieee_float_notequal)
3747-
return convert_function(src, "IEEE_FLOAT_NOTEQUAL");
3748-
3749-
else if(src.id()==ID_abs)
3750-
return convert_function(src, "abs");
3751-
3752-
else if(src.id()==ID_complex_real)
3753-
return convert_function(src, "__real__");
3754-
3755-
else if(src.id()==ID_complex_imag)
3756-
return convert_function(src, "__imag__");
3757-
37583640
else if(src.id()==ID_complex)
37593641
return convert_complex(src, precedence=16);
37603642

@@ -3915,13 +3797,66 @@ std::string expr2ct::convert_with_precedence(
39153797
else if(src.id()==ID_type)
39163798
return convert(src.type());
39173799

3918-
else if(src.id() == ID_count_leading_zeros)
3919-
return convert_function(src, "__builtin_clz");
3800+
auto function_string_opt = convert_function(src);
3801+
if(function_string_opt.has_value())
3802+
return *function_string_opt;
39203803

39213804
// no C language expression for internal representation
39223805
return convert_norep(src, precedence);
39233806
}
39243807

3808+
optionalt<std::string> expr2ct::convert_function(const exprt &src)
3809+
{
3810+
static const std::map<irep_idt, std::string> function_names = {
3811+
{"buffer_size", "BUFFER_SIZE"},
3812+
{"is_zero_string", "IS_ZERO_STRING"},
3813+
{"object_value", "OBJECT_VALUE"},
3814+
{"pointer_base", "POINTER_BASE"},
3815+
{"pointer_cons", "POINTER_CONS"},
3816+
{"zero_string", "ZERO_STRING"},
3817+
{"zero_string_length", "ZERO_STRING_LENGTH"},
3818+
{ID_abs, "abs"},
3819+
{ID_alignof, "alignof"}, // C uses "_Alignof", C++ uses "alignof"
3820+
{ID_builtin_offsetof, "builtin_offsetof"},
3821+
{ID_complex_imag, "__imag__"},
3822+
{ID_complex_real, "__real__"},
3823+
{ID_concatenation, "CONCATENATION"},
3824+
{ID_count_leading_zeros, "__builtin_clz"},
3825+
{ID_dynamic_object, "DYNAMIC_OBJECT"},
3826+
{ID_floatbv_div, "FLOAT/"},
3827+
{ID_floatbv_minus, "FLOAT-"},
3828+
{ID_floatbv_mult, "FLOAT*"},
3829+
{ID_floatbv_plus, "FLOAT+"},
3830+
{ID_floatbv_rem, "FLOAT%"},
3831+
{ID_gcc_builtin_va_arg, "gcc_builtin_va_arg"},
3832+
{ID_get_may, CPROVER_PREFIX "get_may"},
3833+
{ID_get_must, CPROVER_PREFIX "get_must"},
3834+
{ID_good_pointer, "GOOD_POINTER"},
3835+
{ID_ieee_float_equal, "IEEE_FLOAT_EQUAL"},
3836+
{ID_ieee_float_notequal, "IEEE_FLOAT_NOTEQUAL"},
3837+
{ID_infinity, "INFINITY"},
3838+
{ID_is_dynamic_object, "IS_DYNAMIC_OBJECT"},
3839+
{ID_is_invalid_pointer, "IS_INVALID_POINTER"},
3840+
{ID_is_invalid_pointer, CPROVER_PREFIX "is_invalid_pointer"},
3841+
{ID_isfinite, "isfinite"},
3842+
{ID_isinf, "isinf"},
3843+
{ID_isnan, "isnan"},
3844+
{ID_isnormal, "isnormal"},
3845+
{ID_object_size, "OBJECT_SIZE"},
3846+
{ID_pointer_object, "POINTER_OBJECT"},
3847+
{ID_pointer_offset, "POINTER_OFFSET"},
3848+
{ID_r_ok, "R_OK"},
3849+
{ID_w_ok, "W_OK"},
3850+
{ID_width, "WIDTH"},
3851+
};
3852+
3853+
const auto function_entry = function_names.find(src.id());
3854+
if(function_entry == function_names.end())
3855+
return nullopt;
3856+
3857+
return convert_function(src, function_entry->second);
3858+
}
3859+
39253860
std::string expr2ct::convert(const exprt &src)
39263861
{
39273862
unsigned precedence;

‎src/ansi-c/expr2c_class.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,9 @@ class expr2ct
169169
const exprt &src, const std::string &symbol,
170170
unsigned precedence);
171171

172+
/// Returns a string if \p src is a function with a known conversion, else
173+
/// returns nullopt.
174+
optionalt<std::string> convert_function(const exprt &src);
172175
std::string convert_function(const exprt &src, const std::string &symbol);
173176

174177
std::string convert_complex(

0 commit comments

Comments
 (0)