Skip to content

Commit 8ed5e40

Browse files
tautschnigtautschnig
authored
Merge pull request #6754 from tautschnig/cleanup/assert-to-invariant
Replace assert(...) by macros from invariant.h [blocks: #6749]
2 parents 837cd1b + f901919 commit 8ed5e40

File tree

108 files changed

+613
-544
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

108 files changed

+613
-544
lines changed

‎jbmc/src/java_bytecode/character_refine_preprocess.cpp

+7-7
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ codet character_refine_preprocesst::convert_char_function(
2929
conversion_inputt &target)
3030
{
3131
const code_function_callt &function_call=target;
32-
assert(function_call.arguments().size()==1);
32+
PRECONDITION(function_call.arguments().size() == 1);
3333
const exprt &arg=function_call.arguments()[0];
3434
const exprt &result=function_call.lhs();
3535
const typet &type=result.type();
@@ -113,7 +113,7 @@ codet character_refine_preprocesst::convert_char_value(
113113
codet character_refine_preprocesst::convert_compare(conversion_inputt &target)
114114
{
115115
const code_function_callt &function_call=target;
116-
assert(function_call.arguments().size()==2);
116+
PRECONDITION(function_call.arguments().size() == 2);
117117
const exprt &char1=function_call.arguments()[0];
118118
const exprt &char2=function_call.arguments()[1];
119119
const exprt &result=function_call.lhs();
@@ -225,7 +225,7 @@ codet character_refine_preprocesst::convert_digit_int(conversion_inputt &target)
225225
codet character_refine_preprocesst::convert_for_digit(conversion_inputt &target)
226226
{
227227
const code_function_callt &function_call=target;
228-
assert(function_call.arguments().size()==2);
228+
PRECONDITION(function_call.arguments().size() == 2);
229229
const exprt &digit=function_call.arguments()[0];
230230
const exprt &result=function_call.lhs();
231231
const typet &type=result.type();
@@ -588,7 +588,7 @@ codet character_refine_preprocesst::convert_is_ideographic(
588588
conversion_inputt &target)
589589
{
590590
const code_function_callt &function_call=target;
591-
assert(function_call.arguments().size()==1);
591+
PRECONDITION(function_call.arguments().size() == 1);
592592
const exprt &arg=function_call.arguments()[0];
593593
const exprt &result=function_call.lhs();
594594
exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
@@ -602,7 +602,7 @@ codet character_refine_preprocesst::convert_is_ISO_control_char(
602602
conversion_inputt &target)
603603
{
604604
const code_function_callt &function_call=target;
605-
assert(function_call.arguments().size()==1);
605+
PRECONDITION(function_call.arguments().size() == 1);
606606
const exprt &arg=function_call.arguments()[0];
607607
const exprt &result=function_call.lhs();
608608
or_exprt iso(
@@ -760,7 +760,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate(
760760
conversion_inputt &target)
761761
{
762762
const code_function_callt &function_call=target;
763-
assert(function_call.arguments().size()==1);
763+
PRECONDITION(function_call.arguments().size() == 1);
764764
const exprt &arg=function_call.arguments()[0];
765765
const exprt &result=function_call.lhs();
766766
exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
@@ -897,7 +897,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair(
897897
conversion_inputt &target)
898898
{
899899
const code_function_callt &function_call=target;
900-
assert(function_call.arguments().size()==2);
900+
PRECONDITION(function_call.arguments().size() == 2);
901901
const exprt &arg0=function_call.arguments()[0];
902902
const exprt &arg1=function_call.arguments()[1];
903903
const exprt &result=function_call.lhs();

‎jbmc/src/java_bytecode/expr2java.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,9 @@ std::string expr2javat::convert_struct(
117117
const struct_typet::componentst &components=
118118
struct_type.components();
119119

120-
assert(components.size()==src.operands().size());
120+
DATA_INVARIANT(
121+
components.size() == src.operands().size(),
122+
"inconsistent number of components");
121123

122124
exprt::operandst::const_iterator o_it=src.operands().begin();
123125

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -763,8 +763,8 @@ void java_bytecode_convert_classt::convert(
763763
if(s_it!=symbol_table.symbols.end())
764764
symbol_table.erase(s_it); // erase, we stubbed it
765765

766-
if(symbol_table.add(new_symbol))
767-
assert(false && "failed to add static field symbol");
766+
const bool failed = symbol_table.add(new_symbol);
767+
CHECK_RETURN_WITH_DIAGNOSTICS(!failed, "failed to add static field symbol");
768768
}
769769
else
770770
{

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+29-25
Original file line numberDiff line numberDiff line change
@@ -773,20 +773,20 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
773773
bool allow_merge)
774774
{
775775
// Check the tree shape invariant:
776-
assert(tree.branch.size()==tree.branch_addresses.size());
776+
PRECONDITION(tree.branch.size() == tree.branch_addresses.size());
777777

778778
// If there are no child blocks, return this.
779779
if(tree.leaf)
780780
return this_block;
781-
assert(!tree.branch.empty());
781+
PRECONDITION(!tree.branch.empty());
782782

783783
// Find child block starting > address_start:
784784
const auto afterstart=
785785
std::upper_bound(
786786
tree.branch_addresses.begin(),
787787
tree.branch_addresses.end(),
788788
address_start);
789-
assert(afterstart!=tree.branch_addresses.begin());
789+
CHECK_RETURN(afterstart != tree.branch_addresses.begin());
790790
auto findstart=afterstart;
791791
--findstart;
792792
auto child_offset=
@@ -814,9 +814,9 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
814814
while(child_iter != this_block.statements().end() &&
815815
child_iter->get_statement() == ID_decl)
816816
++child_iter;
817-
assert(child_iter != this_block.statements().end());
817+
CHECK_RETURN(child_iter != this_block.statements().end());
818818
std::advance(child_iter, child_offset);
819-
assert(child_iter != this_block.statements().end());
819+
CHECK_RETURN(child_iter != this_block.statements().end());
820820
auto &child_label=to_code_label(*child_iter);
821821
auto &child_block=to_code_block(child_label.code());
822822

@@ -848,7 +848,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
848848
// Check for incoming control-flow edges targeting non-header
849849
// blocks of the new proposed block range:
850850
auto checkit=amap.find(*findstart);
851-
assert(checkit!=amap.end());
851+
CHECK_RETURN(checkit != amap.end());
852852
++checkit; // Skip the header, which can have incoming edges from outside.
853853
for(;
854854
checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
@@ -880,15 +880,15 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
880880
code_labelt newlabel(child_label_name, code_blockt());
881881
code_blockt &newblock=to_code_block(newlabel.code());
882882
auto nblocks=std::distance(findstart, findlim);
883-
assert(nblocks>=2);
883+
CHECK_RETURN(nblocks >= 2);
884884
log.debug() << "Generating codet: combining "
885885
<< std::distance(findstart, findlim) << " blocks for addresses "
886886
<< (*findstart) << "-" << findlim_block_start_address
887887
<< messaget::eom;
888888

889889
// Make a new block containing every child of interest:
890890
auto &this_block_children = this_block.statements();
891-
assert(tree.branch.size()==this_block_children.size());
891+
CHECK_RETURN(tree.branch.size() == this_block_children.size());
892892
for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
893893
blockidx!=blocklim;
894894
++blockidx)
@@ -918,7 +918,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
918918
++branchstart;
919919
tree.branch.erase(branchstart, branchlim);
920920

921-
assert(tree.branch.size()==this_block_children.size());
921+
CHECK_RETURN(tree.branch.size() == this_block_children.size());
922922

923923
auto branchaddriter=tree.branch_addresses.begin();
924924
std::advance(branchaddriter, child_offset);
@@ -934,7 +934,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
934934

935935
tree.branch[child_offset]=std::move(newnode);
936936

937-
assert(tree.branch.size()==tree.branch_addresses.size());
937+
CHECK_RETURN(tree.branch.size() == tree.branch_addresses.size());
938938

939939
return
940940
to_code_block(
@@ -1074,10 +1074,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
10741074
converted_instructiont ins=converted_instructiont(i_it, code_skipt());
10751075
std::pair<address_mapt::iterator, bool> a_entry=
10761076
address_map.insert(std::make_pair(i_it->address, ins));
1077-
assert(a_entry.second);
1077+
CHECK_RETURN(a_entry.second);
10781078
// addresses are strictly increasing, hence we must have inserted
10791079
// a new maximal key
1080-
assert(a_entry.first==--address_map.end());
1080+
CHECK_RETURN(a_entry.first == --address_map.end());
10811081

10821082
const auto bytecode = i_it->bytecode;
10831083
const std::string statement = bytecode_info[i_it->bytecode].mnemonic;
@@ -1217,9 +1217,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
12171217
instruction.stack.clear();
12181218
codet &c = instruction.code;
12191219

1220-
assert(
1220+
INVARIANT(
12211221
stack.empty() || instruction.predecessors.size() <= 1 ||
1222-
has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
1222+
has_prefix(stack.front().get_string(ID_C_base_name), "$stack"),
1223+
"inconsistent stack");
12231224

12241225
exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
12251226
exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
@@ -1288,7 +1289,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
12881289

12891290
if(bytecode == BC_aconst_null)
12901291
{
1291-
assert(results.size()==1);
1292+
PRECONDITION(results.size() == 1);
12921293
results[0] = null_pointer_exprt(java_reference_type(java_void_type()));
12931294
}
12941295
else if(bytecode == BC_athrow)
@@ -1428,23 +1429,23 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
14281429
// and write something like:
14291430
// if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
14301431
PRECONDITION(op.empty() && results.empty());
1431-
assert(!jsr_ret_targets.empty());
1432+
PRECONDITION(!jsr_ret_targets.empty());
14321433
c = convert_ret(
14331434
jsr_ret_targets, arg0, i_it->source_location, i_it->address);
14341435
}
14351436
else if(bytecode == BC_iconst_m1)
14361437
{
1437-
assert(results.size()==1);
1438+
CHECK_RETURN(results.size() == 1);
14381439
results[0]=from_integer(-1, java_int_type());
14391440
}
14401441
else if(bytecode == patternt("?const_?"))
14411442
{
1442-
assert(results.size()==1);
1443+
CHECK_RETURN(results.size() == 1);
14431444
results = convert_const(statement, to_constant_expr(arg0), results);
14441445
}
14451446
else if(bytecode == patternt("?ipush"))
14461447
{
1447-
PRECONDITION(results.size()==1);
1448+
CHECK_RETURN(results.size() == 1);
14481449
DATA_INVARIANT(
14491450
arg0.id()==ID_constant,
14501451
"ipush argument expected to be constant");
@@ -1737,7 +1738,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
17371738
numeric_cast_v<std::size_t>(to_constant_expr(arg1));
17381739

17391740
op=pop(dimension);
1740-
assert(results.size()==1);
1741+
CHECK_RETURN(results.size() == 1);
17411742
c = convert_multianewarray(i_it->source_location, arg0, op, results);
17421743
}
17431744
else if(bytecode == BC_arraylength)
@@ -1848,7 +1849,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
18481849
stackt::const_iterator os_it=a_it2->second.stack.begin();
18491850
for(auto &expr : stack)
18501851
{
1851-
assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
1852+
INVARIANT(
1853+
has_prefix(os_it->get_string(ID_C_base_name), "$stack"),
1854+
"invalid base name");
18521855
symbol_exprt lhs=to_symbol_expr(*os_it);
18531856
code_assignt a(lhs, expr);
18541857
more_code.add(a);
@@ -1917,7 +1920,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
19171920
for(const auto &address_pair : address_map)
19181921
{
19191922
const method_offsett address = address_pair.first;
1920-
assert(address_pair.first==address_pair.second.source->address);
1923+
CHECK_RETURN(address_pair.first == address_pair.second.source->address);
19211924
const codet &c=address_pair.second.code;
19221925

19231926
// Start a new lexical block if this is a branch target:
@@ -1946,9 +1949,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
19461949
root_block.add(
19471950
code_labelt{label(std::to_string(address)), code_blockt{}});
19481951
root.branch.push_back(block_tree_nodet::get_leaf());
1949-
assert((root.branch_addresses.empty() ||
1950-
root.branch_addresses.back()<address) &&
1951-
"Block addresses should be unique and increasing");
1952+
INVARIANT(
1953+
(root.branch_addresses.empty() ||
1954+
root.branch_addresses.back() < address),
1955+
"Block addresses should be unique and increasing");
19521956
root.branch_addresses.push_back(address);
19531957
}
19541958

‎jbmc/src/java_bytecode/java_bytecode_typecheck.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ std::string java_bytecode_typecheckt::to_string(const typet &type)
2525

2626
void java_bytecode_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
2727
{
28-
assert(!symbol.is_type);
28+
PRECONDITION(!symbol.is_type);
2929
typecheck_type(symbol.type);
3030
typecheck_expr(symbol.value);
3131
}

‎jbmc/src/java_bytecode/java_class_loader_limit.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ void java_class_loader_limitt::setup_class_load_limit(
6262
}
6363
else
6464
{
65-
assert(java_cp_include_files.length()>1);
65+
PRECONDITION(java_cp_include_files.length() > 1);
6666
jsont json_cp_config;
6767
if(parse_json(
6868
java_cp_include_files.substr(1),
@@ -76,7 +76,7 @@ void java_class_loader_limitt::setup_class_load_limit(
7676
throw "the JSON file has a wrong format";
7777
for(const jsont &file_entry : to_json_array(include_files))
7878
{
79-
assert(file_entry.is_string());
79+
PRECONDITION(file_entry.is_string());
8080
set_matcher.insert(file_entry.value);
8181
}
8282
}

‎jbmc/src/java_bytecode/java_entry_point.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -621,7 +621,7 @@ bool java_entry_point(
621621
return true;
622622
symbolt symbol=res.main_function;
623623

624-
assert(symbol.type.id()==ID_code);
624+
DATA_INVARIANT(symbol.type.id() == ID_code, "expected code-typed symbol");
625625

626626
return generate_java_start_function(
627627
symbol,

‎jbmc/src/java_bytecode/java_local_variable_table.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -488,7 +488,7 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator(
488488
++domit;
489489
++repeats;
490490
}
491-
assert(repeats<=merge_vars.size());
491+
INVARIANT(repeats <= merge_vars.size(), "out of bounds");
492492
if(repeats==merge_vars.size())
493493
return dom;
494494
}

‎jbmc/src/java_bytecode/java_pointer_casts.cpp

+5-5
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ bool find_superclass_with_type(
3434
const typet &target_type,
3535
const namespacet &ns)
3636
{
37-
assert(ptr.type().id()==ID_pointer);
37+
PRECONDITION(ptr.type().id() == ID_pointer);
3838
while(true)
3939
{
4040
const typet ptr_base = ns.follow(to_pointer_type(ptr.type()).base_type());
@@ -93,15 +93,15 @@ exprt make_clean_pointer_cast(
9393
exprt bare_ptr=ptr;
9494
while(bare_ptr.id()==ID_typecast)
9595
{
96-
assert(
97-
bare_ptr.type().id()==ID_pointer &&
96+
INVARIANT(
97+
bare_ptr.type().id() == ID_pointer,
9898
"Non-pointer in make_clean_pointer_cast?");
9999
if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
100100
bare_ptr = to_typecast_expr(bare_ptr).op();
101101
}
102102

103-
assert(
104-
bare_ptr.type().id()==ID_pointer &&
103+
INVARIANT(
104+
bare_ptr.type().id() == ID_pointer,
105105
"Non-pointer in make_clean_pointer_cast?");
106106

107107
if(bare_ptr.type()==target_type)

‎jbmc/src/java_bytecode/java_types.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -581,13 +581,13 @@ class java_class_typet:public class_typet
581581

582582
inline const java_class_typet &to_java_class_type(const typet &type)
583583
{
584-
assert(type.id()==ID_struct);
584+
PRECONDITION(type.id() == ID_struct);
585585
return static_cast<const java_class_typet &>(type);
586586
}
587587

588588
inline java_class_typet &to_java_class_type(typet &type)
589589
{
590-
assert(type.id()==ID_struct);
590+
PRECONDITION(type.id() == ID_struct);
591591
return static_cast<java_class_typet &>(type);
592592
}
593593

‎src/analyses/custom_bitvector_analysis.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -579,7 +579,7 @@ void custom_bitvector_domaint::output(
579579
for(unsigned i=0; b!=0; i++, b>>=1)
580580
if(b&1)
581581
{
582-
assert(i<cba.bits.size());
582+
INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
583583
out << ' '
584584
<< cba.bits[i];
585585
}
@@ -595,7 +595,7 @@ void custom_bitvector_domaint::output(
595595
for(unsigned i=0; b!=0; i++, b>>=1)
596596
if(b&1)
597597
{
598-
assert(i<cba.bits.size());
598+
INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
599599
out << ' '
600600
<< cba.bits[i];
601601
}

0 commit comments

Comments
 (0)