Skip to content

Commit fbabfd2

Browse files
committed
Add conversion for rol and ror operators to c output
This adds conversion for the rol and ror operators from CBMC internals into C code. This is done by bit-twiddling the values to achieve the outcome. Fixes #6241
1 parent d5c9ef8 commit fbabfd2

File tree

1 file changed

+29
-0
lines changed

1 file changed

+29
-0
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3794,6 +3794,35 @@ std::string expr2ct::convert_with_precedence(
37943794
else if(src.id()==ID_type)
37953795
return convert(src.type());
37963796

3797+
else if(src.id() == ID_rol)
3798+
{
3799+
// AAAA rol n == (AAAA << n) | (AAAA >> (width(AAAA) - n))
3800+
auto bin_expr = to_binary_expr(src);
3801+
auto lhs = "(" + convert_binary(bin_expr, "<<", precedence = 11, true) + ")";
3802+
const exprt &op0 = bin_expr.op0();
3803+
const exprt &op1 = bin_expr.op1();
3804+
irep_idt width_val = op0.type().get("width");
3805+
auto width = constant_exprt(width_val, op1.type());
3806+
auto complement_expr = minus_exprt(width, op1);
3807+
auto rhs_expr = binary_exprt(op0, ID_shr, complement_expr);
3808+
auto rhs = "(" + convert_binary(rhs_expr, ">>", precedence = 11, true) + ")";
3809+
return "(" + lhs + " | " + rhs + ")";
3810+
}
3811+
else if(src.id() == ID_ror)
3812+
{
3813+
// AAAA ror n == (AAAA >> n) | (AAAA << (width(AAAA) - n))
3814+
auto bin_expr = to_binary_expr(src);
3815+
auto lhs = "(" + convert_binary(bin_expr, ">>", precedence = 11, true) + ")";
3816+
const exprt &op0 = bin_expr.op0();
3817+
const exprt &op1 = bin_expr.op1();
3818+
irep_idt width_val = op0.type().get("width");
3819+
auto width = constant_exprt(width_val, op1.type());
3820+
auto complement_expr = minus_exprt(width, op1);
3821+
auto rhs_expr = binary_exprt(op0, ID_shl, complement_expr);
3822+
auto rhs = "(" + convert_binary(rhs_expr, "<<", precedence = 11, true) + ")";
3823+
return "(" + lhs + " | " + rhs + ")";
3824+
}
3825+
37973826
auto function_string_opt = convert_function(src);
37983827
if(function_string_opt.has_value())
37993828
return *function_string_opt;

0 commit comments

Comments
 (0)