Skip to content

Commit ac26fe2

Browse files
tautschnigtautschnig
committed
Re-enable users of {expr,nondet}_initializer to do their own error reporting
With d5535a9 {expr,nondet}_initializer would fail an invariant when an expression of the chosen type could not be generated. As user input code can reasonably trigger this case (see included regression test), the caller should be able to do error handling as appropriate in a given context.
1 parent c3b78c9 commit ac26fe2

18 files changed

+238
-209
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -708,12 +708,14 @@ void java_bytecode_convert_classt::convert(
708708
new_symbol.type.set(ID_C_access, ID_default);
709709

710710
const namespacet ns(symbol_table);
711-
new_symbol.value=
712-
zero_initializer(
713-
field_type,
714-
class_symbol.location,
715-
ns,
716-
get_message_handler());
711+
const auto value = zero_initializer(field_type, class_symbol.location, ns);
712+
if(!value.has_value())
713+
{
714+
error().source_location = class_symbol.location;
715+
error() << "failed to zero-initialize " << f.name << eom;
716+
throw 0;
717+
}
718+
new_symbol.value = *value;
717719

718720
// Load annotations
719721
if(!f.annotations.empty())

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2974,8 +2974,15 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
29742974
if(return_type.id() == ID_empty)
29752975
return {};
29762976

2977-
return zero_initializer(
2978-
return_type, location, namespacet(symbol_table), get_message_handler());
2977+
const auto value =
2978+
zero_initializer(return_type, location, namespacet(symbol_table));
2979+
if(!value.has_value())
2980+
{
2981+
error().source_location = location;
2982+
error() << "failed to zero-initialize return type" << eom;
2983+
throw 0;
2984+
}
2985+
return value;
29792986
}
29802987

29812988
void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(

‎jbmc/src/java_bytecode/java_entry_point.cpp‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -200,14 +200,19 @@ static void java_static_lifetime_init(
200200
// First initialize the object as prior to a constructor:
201201
namespacet ns(symbol_table);
202202

203-
exprt zero_object =
204-
zero_initializer(
205-
sym.type, source_locationt(), ns, message_handler);
203+
auto zero_object = zero_initializer(sym.type, source_locationt(), ns);
204+
if(!zero_object.has_value())
205+
{
206+
messaget message(message_handler);
207+
message.error() << "failed to zero-initialize " << sym.name
208+
<< messaget::eom;
209+
throw 0;
210+
}
206211
set_class_identifier(
207-
to_struct_expr(zero_object), ns, to_symbol_type(sym.type));
212+
to_struct_expr(*zero_object), ns, to_symbol_type(sym.type));
208213

209214
code_block.copy_to_operands(
210-
code_assignt(sym.symbol_expr(), zero_object));
215+
code_assignt(sym.symbol_expr(), *zero_object));
211216

212217
// Then call the init function:
213218
code_block.move_to_operands(initializer_call);

‎jbmc/src/java_bytecode/java_object_factory.cpp‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1034,19 +1034,17 @@ void java_object_factoryt::gen_nondet_struct_init(
10341034
// passes can easily recognise leaves no uninitialised state behind.
10351035

10361036
// This code mirrors the `remove_java_new` pass:
1037-
null_message_handlert nullout;
1038-
exprt initial_object =
1039-
zero_initializer(
1040-
struct_type, source_locationt(), ns, nullout);
1037+
auto initial_object = zero_initializer(struct_type, source_locationt(), ns);
1038+
CHECK_RETURN(initial_object.has_value());
10411039
irep_idt qualified_clsid = "java::" + id2string(class_identifier);
10421040
set_class_identifier(
1043-
to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid));
1041+
to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));
10441042

10451043
// If the initialised type is a special-cased String type (one with length
10461044
// and data fields introduced by string-library preprocessing), initialise
10471045
// those fields with nondet values:
10481046
skip_special_string_fields = initialize_nondet_string_fields(
1049-
to_struct_expr(initial_object),
1047+
to_struct_expr(*initial_object),
10501048
assignments,
10511049
object_factory_parameters.min_nondet_string_length,
10521050
object_factory_parameters.max_nondet_string_length,
@@ -1055,8 +1053,7 @@ void java_object_factoryt::gen_nondet_struct_init(
10551053
symbol_table,
10561054
object_factory_parameters.string_printable);
10571055

1058-
assignments.copy_to_operands(
1059-
code_assignt(expr, initial_object));
1056+
assignments.copy_to_operands(code_assignt(expr, *initial_object));
10601057
}
10611058

10621059
for(const auto &component : components)

‎jbmc/src/java_bytecode/java_string_literals.cpp‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,10 @@ symbol_exprt get_or_create_string_literal_symbol(
192192
// Other members of JDK's java.lang.String we don't understand
193193
// without string-refinement. Just zero-init them; consider using
194194
// test-gen-like nondet object trees instead.
195-
literal_init.copy_to_operands(
196-
zero_initializer(comp.type(), string_expr.source_location(), ns));
195+
const auto init =
196+
zero_initializer(comp.type(), string_expr.source_location(), ns);
197+
CHECK_RETURN(init.has_value());
198+
literal_init.copy_to_operands(*init);
197199
}
198200
new_symbol.value = literal_init;
199201
}

‎jbmc/src/java_bytecode/remove_java_new.cpp‎

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -93,12 +93,12 @@ goto_programt::targett remove_java_newt::lower_java_new(
9393

9494
// zero-initialize the object
9595
dereference_exprt deref(lhs, object_type);
96-
exprt zero_object =
97-
zero_initializer(object_type, location, ns, get_message_handler());
96+
auto zero_object = zero_initializer(object_type, location, ns);
97+
CHECK_RETURN(zero_object.has_value());
9898
set_class_identifier(
99-
to_struct_expr(zero_object), ns, to_symbol_type(object_type));
99+
to_struct_expr(*zero_object), ns, to_symbol_type(object_type));
100100
goto_programt::targett t_i = dest.insert_after(target);
101-
t_i->make_assignment(code_assignt(deref, zero_object));
101+
t_i->make_assignment(code_assignt(deref, *zero_object));
102102
t_i->source_location = location;
103103

104104
return t_i;
@@ -153,12 +153,12 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
153153

154154
// Init base class:
155155
dereference_exprt deref(lhs, object_type);
156-
exprt zero_object =
157-
zero_initializer(object_type, location, ns, get_message_handler());
156+
auto zero_object = zero_initializer(object_type, location, ns);
157+
CHECK_RETURN(zero_object.has_value());
158158
set_class_identifier(
159-
to_struct_expr(zero_object), ns, to_symbol_type(object_type));
159+
to_struct_expr(*zero_object), ns, to_symbol_type(object_type));
160160
goto_programt::targett t_i = dest.insert_before(next);
161-
t_i->make_assignment(code_assignt(deref, zero_object));
161+
t_i->make_assignment(code_assignt(deref, *zero_object));
162162
t_i->source_location = location;
163163

164164
// if it's an array, we need to set the length field
@@ -232,10 +232,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
232232
// zero-initialize the data
233233
if(!rhs.get_bool(ID_skip_initialize))
234234
{
235-
exprt zero_element = zero_initializer(
236-
data.type().subtype(), location, ns, get_message_handler());
235+
const auto zero_element =
236+
zero_initializer(data.type().subtype(), location, ns);
237+
CHECK_RETURN(zero_element.has_value());
237238
codet array_set(ID_array_set);
238-
array_set.copy_to_operands(new_array_data_symbol, zero_element);
239+
array_set.copy_to_operands(new_array_data_symbol, *zero_element);
239240
goto_programt::targett t_d = dest.insert_before(next);
240241
t_d->make_other(array_set);
241242
t_d->source_location = location;

‎regression/ansi-c/array_initialization4/main.c‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int foo(unsigned n)
4+
{
5+
assert(n > 0);
6+
int A[n] = {1};
7+
return A[0];
8+
}
9+
10+
int main()
11+
{
12+
assert(foo(1) == 1);
13+
}

‎regression/ansi-c/array_initialization4/test.desc‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=(1|64)$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring

‎src/ansi-c/c_typecheck_initializer.cpp‎

Lines changed: 68 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -114,13 +114,16 @@ exprt c_typecheck_baset::do_initializer_rec(
114114
{
115115
// fill up
116116
tmp.type()=type;
117-
exprt zero=
118-
zero_initializer(
119-
full_type.subtype(),
120-
value.source_location(),
121-
*this,
122-
get_message_handler());
123-
tmp.operands().resize(integer2size_t(array_size), zero);
117+
const auto zero =
118+
zero_initializer(full_type.subtype(), value.source_location(), *this);
119+
if(!zero.has_value())
120+
{
121+
err_location(value);
122+
error() << "cannot zero-initialize array with subtype `"
123+
<< to_string(full_type.subtype()) << "'" << eom;
124+
throw 0;
125+
}
126+
tmp.operands().resize(integer2size_t(array_size), *zero);
124127
}
125128
}
126129

@@ -171,13 +174,16 @@ exprt c_typecheck_baset::do_initializer_rec(
171174
{
172175
// fill up
173176
tmp2.type()=type;
174-
exprt zero=
175-
zero_initializer(
176-
full_type.subtype(),
177-
value.source_location(),
178-
*this,
179-
get_message_handler());
180-
tmp2.operands().resize(integer2size_t(array_size), zero);
177+
const auto zero =
178+
zero_initializer(full_type.subtype(), value.source_location(), *this);
179+
if(!zero.has_value())
180+
{
181+
err_location(value);
182+
error() << "cannot zero-initialize array with subtype `"
183+
<< to_string(full_type.subtype()) << "'" << eom;
184+
throw 0;
185+
}
186+
tmp2.operands().resize(integer2size_t(array_size), *zero);
181187
}
182188
}
183189

@@ -395,13 +401,16 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
395401
to_array_type(full_type).size().is_nil()))
396402
{
397403
// we are willing to grow an incomplete or zero-sized array
398-
exprt zero=
399-
zero_initializer(
400-
full_type.subtype(),
401-
value.source_location(),
402-
*this,
403-
get_message_handler());
404-
dest->operands().resize(integer2size_t(index)+1, zero);
404+
const auto zero = zero_initializer(
405+
full_type.subtype(), value.source_location(), *this);
406+
if(!zero.has_value())
407+
{
408+
err_location(value);
409+
error() << "cannot zero-initialize array with subtype `"
410+
<< to_string(full_type.subtype()) << "'" << eom;
411+
throw 0;
412+
}
413+
dest->operands().resize(integer2size_t(index) + 1, *zero);
405414

406415
// todo: adjust type!
407416
}
@@ -461,15 +470,17 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
461470
{
462471
// Note that gcc issues a warning if the union component is switched.
463472
// Build a union expression from given component.
464-
union_exprt union_expr(type);
465-
union_expr.op()=
466-
zero_initializer(
467-
component.type(),
468-
value.source_location(),
469-
*this,
470-
get_message_handler());
473+
const auto zero =
474+
zero_initializer(component.type(), value.source_location(), *this);
475+
if(!zero.has_value())
476+
{
477+
err_location(value);
478+
error() << "cannot zero-initialize union component of type `"
479+
<< to_string(component.type()) << "'" << eom;
480+
throw 0;
481+
}
482+
union_exprt union_expr(component.get_name(), *zero, type);
471483
union_expr.add_source_location()=value.source_location();
472-
union_expr.set_component_name(component.get_name());
473484
*dest=union_expr;
474485
}
475486

@@ -524,15 +535,17 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
524535
const union_typet::componentt &component=
525536
union_type.components().front();
526537

527-
union_exprt union_expr(type);
528-
union_expr.op()=
529-
zero_initializer(
530-
component.type(),
531-
value.source_location(),
532-
*this,
533-
get_message_handler());
538+
const auto zero =
539+
zero_initializer(component.type(), value.source_location(), *this);
540+
if(!zero.has_value())
541+
{
542+
err_location(value);
543+
error() << "cannot zero-initialize union component of type `"
544+
<< to_string(component.type()) << "'" << eom;
545+
throw 0;
546+
}
547+
union_exprt union_expr(component.get_name(), *zero, type);
534548
union_expr.add_source_location()=value.source_location();
535-
union_expr.set_component_name(component.get_name());
536549
*dest=union_expr;
537550
}
538551
}
@@ -830,9 +843,15 @@ exprt c_typecheck_baset::do_initializer_list(
830843
full_type.id()==ID_vector)
831844
{
832845
// start with zero everywhere
833-
result=
834-
zero_initializer(
835-
type, value.source_location(), *this, get_message_handler());
846+
const auto zero = zero_initializer(type, value.source_location(), *this);
847+
if(!zero.has_value())
848+
{
849+
err_location(value.source_location());
850+
error() << "cannot zero-initialize `" << to_string(full_type) << "'"
851+
<< eom;
852+
throw 0;
853+
}
854+
result = *zero;
836855
}
837856
else if(full_type.id()==ID_array)
838857
{
@@ -845,9 +864,15 @@ exprt c_typecheck_baset::do_initializer_list(
845864
else
846865
{
847866
// start with zero everywhere
848-
result=
849-
zero_initializer(
850-
type, value.source_location(), *this, get_message_handler());
867+
const auto zero = zero_initializer(type, value.source_location(), *this);
868+
if(!zero.has_value())
869+
{
870+
err_location(value.source_location());
871+
error() << "cannot zero-initialize `" << to_string(full_type) << "'"
872+
<< eom;
873+
throw 0;
874+
}
875+
result = *zero;
851876
}
852877

853878
// 6.7.9, 14: An array of character type may be initialized by a character

‎src/cpp/cpp_typecheck_expr.cpp‎

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -870,15 +870,18 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr)
870870
{
871871
// Default value, e.g., int()
872872
typecheck_type(expr.type());
873-
exprt new_expr=
874-
::zero_initializer(
875-
expr.type(),
876-
expr.find_source_location(),
877-
*this,
878-
get_message_handler());
879-
880-
new_expr.add_source_location()=expr.source_location();
881-
expr=new_expr;
873+
auto new_expr =
874+
::zero_initializer(expr.type(), expr.find_source_location(), *this);
875+
if(!new_expr.has_value())
876+
{
877+
err_location(expr.find_source_location());
878+
error() << "cannot zero-initialize `" << to_string(expr.type()) << "'"
879+
<< eom;
880+
throw 0;
881+
}
882+
883+
new_expr->add_source_location() = expr.source_location();
884+
expr = *new_expr;
882885
}
883886
else if(expr.operands().size()==1)
884887
{

0 commit comments

Comments
 (0)