Skip to content

Commit 1739299

Browse files
committed
Add side_effect_expr_overflowt
Introduce a new expression to handle GCC's __builtin_X_overflow in the middle-end (during goto conversion) instead of directly encoding the semantics during type checking.
1 parent de4557f commit 1739299

File tree

4 files changed

+179
-46
lines changed

4 files changed

+179
-46
lines changed

src/ansi-c/c_expr.h

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,4 +107,97 @@ inline shuffle_vector_exprt &to_shuffle_vector_expr(exprt &expr)
107107
return ret;
108108
}
109109

110+
/// \brief A Boolean expression returning true, iff the result of performing
111+
/// operation \c kind on operands \c lhs and \c rhs in infinite-precision
112+
/// arithmetic cannot be represented in the type of the object that \c result
113+
/// points to.
114+
/// If \c result is a pointer, the result of the operation is stored in the
115+
/// object pointed to by \c result.
116+
class side_effect_expr_overflowt : public side_effect_exprt
117+
{
118+
public:
119+
side_effect_expr_overflowt(
120+
const irep_idt &kind,
121+
exprt _lhs,
122+
exprt _rhs,
123+
exprt _result,
124+
const source_locationt &loc)
125+
: side_effect_exprt(
126+
"overflow-" + id2string(kind),
127+
{std::move(_lhs), std::move(_rhs), std::move(_result)},
128+
bool_typet{},
129+
loc)
130+
{
131+
}
132+
133+
exprt &lhs()
134+
{
135+
return op0();
136+
}
137+
138+
const exprt &lhs() const
139+
{
140+
return op0();
141+
}
142+
143+
exprt &rhs()
144+
{
145+
return op1();
146+
}
147+
148+
const exprt &rhs() const
149+
{
150+
return op1();
151+
}
152+
153+
exprt &result()
154+
{
155+
return op2();
156+
}
157+
158+
const exprt &result() const
159+
{
160+
return op2();
161+
}
162+
};
163+
164+
template <>
165+
inline bool can_cast_expr<side_effect_expr_overflowt>(const exprt &base)
166+
{
167+
if(base.id() != ID_side_effect)
168+
return false;
169+
170+
const irep_idt &statement = to_side_effect_expr(base).get_statement();
171+
return statement == ID_overflow_plus || statement == ID_overflow_mult ||
172+
statement == ID_overflow_minus;
173+
}
174+
175+
/// \brief Cast an exprt to a \ref side_effect_expr_overflowt
176+
///
177+
/// \a expr must be known to be \ref side_effect_expr_overflowt.
178+
///
179+
/// \param expr: Source expression
180+
/// \return Object of type \ref side_effect_expr_overflowt
181+
inline const side_effect_expr_overflowt &
182+
to_side_effect_expr_overflow(const exprt &expr)
183+
{
184+
const auto &side_effect_expr = to_side_effect_expr(expr);
185+
PRECONDITION(
186+
side_effect_expr.get_statement() == ID_overflow_plus ||
187+
side_effect_expr.get_statement() == ID_overflow_mult ||
188+
side_effect_expr.get_statement() == ID_overflow_minus);
189+
return static_cast<const side_effect_expr_overflowt &>(side_effect_expr);
190+
}
191+
192+
/// \copydoc to_side_effect_expr_overflow(const exprt &)
193+
inline side_effect_expr_overflowt &to_side_effect_expr_overflow(exprt &expr)
194+
{
195+
auto &side_effect_expr = to_side_effect_expr(expr);
196+
PRECONDITION(
197+
side_effect_expr.get_statement() == ID_overflow_plus ||
198+
side_effect_expr.get_statement() == ID_overflow_mult ||
199+
side_effect_expr.get_statement() == ID_overflow_minus);
200+
return static_cast<side_effect_expr_overflowt &>(side_effect_expr);
201+
}
202+
110203
#endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 13 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
3434

3535
#include "anonymous_member.h"
3636
#include "builtin_factory.h"
37+
#include "c_expr.h"
3738
#include "c_qualifiers.h"
3839
#include "c_typecast.h"
3940
#include "expr2c.h"
@@ -3023,14 +3024,12 @@ exprt c_typecheck_baset::do_special_functions(
30233024
throw invalid_source_file_exceptiont{error_message.str()};
30243025
}
30253026

3027+
typecheck_function_call_arguments(expr);
3028+
30263029
auto lhs = expr.arguments()[0];
30273030
auto rhs = expr.arguments()[1];
30283031
auto result_ptr = expr.arguments()[2];
30293032

3030-
typecheck_expr(lhs);
3031-
typecheck_expr(rhs);
3032-
typecheck_expr(result_ptr);
3033-
30343033
{
30353034
auto const raise_wrong_argument_error =
30363035
[this,
@@ -3061,48 +3060,16 @@ exprt c_typecheck_baset::do_special_functions(
30613060
}
30623061
}
30633062

3064-
// actual logic implementing the operators
3065-
auto const make_operation = [&identifier](exprt lhs, exprt rhs) -> exprt {
3066-
if(identifier == "__builtin_add_overflow")
3067-
{
3068-
return plus_exprt{lhs, rhs};
3069-
}
3070-
else if(identifier == "__builtin_sub_overflow")
3071-
{
3072-
return minus_exprt{lhs, rhs};
3073-
}
3074-
else
3075-
{
3076-
INVARIANT(
3077-
identifier == "__builtin_mul_overflow",
3078-
"the three overflow operations are add, sub and mul");
3079-
return mult_exprt{lhs, rhs};
3080-
}
3081-
};
3082-
3083-
// we’re basically generating this expression
3084-
// (*result = (result_type)((integer)lhs OP (integer)rhs)),
3085-
// ((integer)result == (integer)lhs OP (integer)rhs)
3086-
// i.e. perform the operation (+, -, *) on arbitrary length integer,
3087-
// cast to result type, check if the casted result is still equivalent
3088-
// to the arbitrary length result.
3089-
auto operation = make_operation(
3090-
typecast_exprt{lhs, integer_typet{}},
3091-
typecast_exprt{rhs, integer_typet{}});
3092-
3093-
auto operation_result =
3094-
typecast_exprt{operation, result_ptr.type().subtype()};
3095-
typecheck_expr_typecast(operation_result);
3096-
auto overflow_check = notequal_exprt{
3097-
typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}},
3098-
operation};
3099-
typecheck_expr(overflow_check);
3100-
return exprt{ID_comma,
3101-
bool_typet{},
3102-
{side_effect_expr_assignt{dereference_exprt{result_ptr},
3103-
operation_result,
3104-
expr.source_location()},
3105-
overflow_check}};
3063+
irep_idt kind =
3064+
(identifier == "__builtin_add_overflow")
3065+
? ID_plus
3066+
: (identifier == "__builtin_sub_overflow") ? ID_minus : ID_mult;
3067+
3068+
return side_effect_expr_overflowt{kind,
3069+
std::move(lhs),
3070+
std::move(rhs),
3071+
std::move(result_ptr),
3072+
expr.source_location()};
31063073
}
31073074
else
31083075
return nil_exprt();

src/goto-programs/goto_convert_class.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]
2525
#include "goto_program.h"
2626
#include "destructor_tree.h"
2727

28+
class side_effect_expr_overflowt;
29+
2830
class goto_convertt:public messaget
2931
{
3032
public:
@@ -150,6 +152,11 @@ class goto_convertt:public messaget
150152
exprt &expr,
151153
goto_programt &dest,
152154
const irep_idt &mode);
155+
void remove_overflow(
156+
side_effect_expr_overflowt &expr,
157+
goto_programt &dest,
158+
bool result_is_used,
159+
const irep_idt &mode);
153160

154161
virtual void do_cpp_new(
155162
const exprt &lhs,

src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
2121

2222
#include <util/c_types.h>
2323

24+
#include <ansi-c/c_expr.h>
25+
2426
bool goto_convertt::has_function_call(const exprt &expr)
2527
{
2628
forall_operands(it, expr)
@@ -588,6 +590,63 @@ void goto_convertt::remove_statement_expression(
588590
static_cast<exprt &>(expr)=tmp_symbol_expr;
589591
}
590592

593+
void goto_convertt::remove_overflow(
594+
side_effect_expr_overflowt &expr,
595+
goto_programt &dest,
596+
bool result_is_used,
597+
const irep_idt &mode)
598+
{
599+
const irep_idt &statement = expr.get_statement();
600+
const exprt &lhs = expr.lhs();
601+
const exprt &rhs = expr.rhs();
602+
const exprt &result_ptr = expr.result();
603+
604+
// actual logic implementing the operators
605+
auto const make_operation = [&statement](exprt lhs, exprt rhs) -> exprt {
606+
if(statement == ID_overflow_plus)
607+
{
608+
return plus_exprt{lhs, rhs};
609+
}
610+
else if(statement == ID_overflow_minus)
611+
{
612+
return minus_exprt{lhs, rhs};
613+
}
614+
else
615+
{
616+
INVARIANT(
617+
statement == ID_overflow_mult,
618+
"the three overflow operations are add, sub and mul");
619+
return mult_exprt{lhs, rhs};
620+
}
621+
};
622+
623+
// we’re basically generating this expression
624+
// (*result = (result_type)((integer)lhs OP (integer)rhs)),
625+
// ((integer)result == (integer)lhs OP (integer)rhs)
626+
// i.e. perform the operation (+, -, *) on arbitrary length integer,
627+
// cast to result type, check if the casted result is still equivalent
628+
// to the arbitrary length result.
629+
auto operation = make_operation(
630+
typecast_exprt{lhs, integer_typet{}}, typecast_exprt{rhs, integer_typet{}});
631+
632+
typecast_exprt operation_result{operation, result_ptr.type().subtype()};
633+
634+
code_assignt assign{dereference_exprt{result_ptr},
635+
std::move(operation_result),
636+
expr.source_location()};
637+
convert_assign(assign, dest, mode);
638+
639+
if(result_is_used)
640+
{
641+
notequal_exprt overflow_check{
642+
typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}},
643+
operation};
644+
expr.swap(overflow_check);
645+
}
646+
else
647+
expr.make_nil();
648+
}
649+
591650
void goto_convertt::remove_side_effect(
592651
side_effect_exprt &expr,
593652
goto_programt &dest,
@@ -651,6 +710,13 @@ void goto_convertt::remove_side_effect(
651710
// the result can't be used, these are void
652711
expr.make_nil();
653712
}
713+
else if(
714+
statement == ID_overflow_plus || statement == ID_overflow_minus ||
715+
statement == ID_overflow_mult)
716+
{
717+
remove_overflow(
718+
to_side_effect_expr_overflow(expr), dest, result_is_used, mode);
719+
}
654720
else
655721
{
656722
UNREACHABLE;

0 commit comments

Comments
 (0)