Skip to content

Commit bcf33c1

Browse files
tautschnigtautschnig
committed
Use constant_exprt::is_{true,false,zero,one}
Avoids use of the now-deprecated exprt methods.
1 parent 870cefd commit bcf33c1

File tree

136 files changed

+1002
-529
lines changed

Some content is hidden

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

136 files changed

+1002
-529
lines changed

‎jbmc/src/java_bytecode/java_object_factory.cpp

+5-1
Original file line numberDiff line numberDiff line change
@@ -1087,8 +1087,12 @@ void java_object_factoryt::gen_nondet_init(
10871087
else
10881088
{
10891089
exprt within_bounds = interval.make_contains_expr(expr);
1090-
if(!within_bounds.is_true())
1090+
if(
1091+
!within_bounds.is_constant() ||
1092+
!to_constant_expr(within_bounds).is_true())
1093+
{
10911094
assignments.add(code_assumet(std::move(within_bounds)));
1095+
}
10921096
}
10931097

10941098
if(

‎jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

+10-6
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,8 @@ static bool is_call_to(
6969

7070
static bool is_assume_false(goto_programt::const_targett inst)
7171
{
72-
return inst->is_assume() && inst->condition().is_false();
72+
return inst->is_assume() && inst->condition().is_constant() &&
73+
to_constant_expr(inst->condition()).is_false();
7374
}
7475

7576
/// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,17 +91,20 @@ static goto_programt::const_targett interpret_classid_comparison(
9091
{
9192
exprt guard = pc->condition();
9293
guard = resolve_classid_test(guard, actual_class_id, ns);
93-
if(guard.is_true())
94+
if(!guard.is_constant())
95+
{
96+
// Can't resolve the test, so exit here:
97+
return pc;
98+
}
99+
else if(to_constant_expr(guard).is_true())
94100
{
95101
REQUIRE(pc->targets.begin() != pc->targets.end());
96102
pc = *(pc->targets.begin());
97103
}
98-
else if(guard.is_false())
99-
++pc;
100104
else
101105
{
102-
// Can't resolve the test, so exit here:
103-
return pc;
106+
CHECK_RETURN(to_constant_expr(guard).is_false());
107+
++pc;
104108
}
105109
}
106110
else if(pc->type() == SKIP)

‎src/analyses/constant_propagator.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -183,8 +183,8 @@ void constant_propagator_domaint::transform(
183183
else
184184
g = not_exprt(from->condition());
185185
partial_evaluate(values, g, ns);
186-
if(g.is_false())
187-
values.set_to_bottom();
186+
if(g.is_constant() && to_constant_expr(g).is_false())
187+
values.set_to_bottom();
188188
else
189189
two_way_propagate_rec(g, ns, cp);
190190
}
@@ -376,7 +376,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
376376

377377
// x != FALSE ==> x == TRUE
378378

379-
if(rhs.is_zero() || rhs.is_false())
379+
if(to_constant_expr(rhs).is_zero() || to_constant_expr(rhs).is_false())
380380
rhs = from_integer(1, rhs.type());
381381
else
382382
rhs = from_integer(0, rhs.type());

‎src/analyses/custom_bitvector_analysis.cpp

+9-9
Original file line numberDiff line numberDiff line change
@@ -530,7 +530,7 @@ void custom_bitvector_domaint::transform(
530530

531531
const exprt result2 = simplify_expr(eval(guard, cba), ns);
532532

533-
if(result2.is_false())
533+
if(result2.is_constant() && to_constant_expr(result2).is_false())
534534
make_bottom();
535535
}
536536
break;
@@ -814,12 +814,12 @@ void custom_bitvector_analysist::check(
814814
if(use_xml)
815815
{
816816
out << "<result status=\"";
817-
if(result.is_true())
817+
if(!result.is_constant())
818+
out << "UNKNOWN";
819+
else if(to_constant_expr(result).is_true())
818820
out << "SUCCESS";
819-
else if(result.is_false())
820-
out << "FAILURE";
821821
else
822-
out << "UNKNOWN";
822+
out << "FAILURE";
823823
out << "\">\n";
824824
out << xml(i_it->source_location());
825825
out << "<description>"
@@ -838,12 +838,12 @@ void custom_bitvector_analysist::check(
838838
out << '\n';
839839
}
840840

841-
if(result.is_true())
841+
if(!result.is_constant())
842+
unknown++;
843+
else if(to_constant_expr(result).is_true())
842844
pass++;
843-
else if(result.is_false())
844-
fail++;
845845
else
846-
unknown++;
846+
fail++;
847847
}
848848

849849
if(!use_xml)

‎src/analyses/goto_rw.cpp

+10-10
Original file line numberDiff line numberDiff line change
@@ -116,17 +116,17 @@ void rw_range_sett::get_objects_if(
116116
const range_spect &range_start,
117117
const range_spect &size)
118118
{
119-
if(if_expr.cond().is_false())
120-
get_objects_rec(mode, if_expr.false_case(), range_start, size);
121-
else if(if_expr.cond().is_true())
122-
get_objects_rec(mode, if_expr.true_case(), range_start, size);
123-
else
119+
if(!if_expr.cond().is_constant())
124120
{
125121
get_objects_rec(get_modet::READ, if_expr.cond());
126122

127123
get_objects_rec(mode, if_expr.false_case(), range_start, size);
128124
get_objects_rec(mode, if_expr.true_case(), range_start, size);
129125
}
126+
else if(to_constant_expr(if_expr.cond()).is_false())
127+
get_objects_rec(mode, if_expr.false_case(), range_start, size);
128+
else
129+
get_objects_rec(mode, if_expr.true_case(), range_start, size);
130130
}
131131

132132
void rw_range_sett::get_objects_dereference(
@@ -735,11 +735,7 @@ void rw_guarded_range_set_value_sett::get_objects_if(
735735
const range_spect &range_start,
736736
const range_spect &size)
737737
{
738-
if(if_expr.cond().is_false())
739-
get_objects_rec(mode, if_expr.false_case(), range_start, size);
740-
else if(if_expr.cond().is_true())
741-
get_objects_rec(mode, if_expr.true_case(), range_start, size);
742-
else
738+
if(!if_expr.cond().is_constant())
743739
{
744740
get_objects_rec(get_modet::READ, if_expr.cond());
745741

@@ -753,6 +749,10 @@ void rw_guarded_range_set_value_sett::get_objects_if(
753749
get_objects_rec(mode, if_expr.true_case(), range_start, size);
754750
guard = std::move(copy);
755751
}
752+
else if(to_constant_expr(if_expr.cond()).is_false())
753+
get_objects_rec(mode, if_expr.false_case(), range_start, size);
754+
else
755+
get_objects_rec(mode, if_expr.true_case(), range_start, size);
756756
}
757757

758758
void rw_guarded_range_set_value_sett::add(

‎src/analyses/guard_bdd.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ exprt guard_bddt::guard_expr(exprt expr) const
4444
}
4545
else
4646
{
47-
if(expr.is_false())
47+
if(expr.is_constant() && to_constant_expr(expr).is_false())
4848
{
4949
return boolean_negate(as_expr());
5050
}

‎src/analyses/guard_expr.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ exprt guard_exprt::guard_expr(exprt expr) const
2424
}
2525
else
2626
{
27-
if(expr.is_false())
27+
if(expr.is_constant() && to_constant_expr(expr).is_false())
2828
{
2929
return boolean_negate(as_expr());
3030
}
@@ -39,9 +39,10 @@ void guard_exprt::add(const exprt &expr)
3939
{
4040
PRECONDITION(expr.is_boolean());
4141

42-
if(is_false() || expr.is_true())
42+
if(is_false() || (expr.is_constant() && to_constant_expr(expr).is_true()))
4343
return;
44-
else if(is_true() || expr.is_false())
44+
else if(
45+
is_true() || (expr.is_constant() && to_constant_expr(expr).is_false()))
4546
{
4647
this->expr = expr;
4748

@@ -198,7 +199,9 @@ guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
198199

199200
if(tmp != and_expr1)
200201
{
201-
if(and_expr1.is_true() || and_expr2.is_true())
202+
if(
203+
(and_expr1.is_constant() && to_constant_expr(and_expr1).is_true()) ||
204+
(and_expr2.is_constant() && to_constant_expr(and_expr2).is_true()))
202205
{
203206
}
204207
else

‎src/analyses/guard_expr.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_ANALYSES_GUARD_EXPR_H
1313
#define CPROVER_ANALYSES_GUARD_EXPR_H
1414

15-
#include <util/expr.h>
15+
#include <util/std_expr.h>
1616

1717
/// This is unused by this implementation of guards, but can be used by other
1818
/// implementations of the same interface.
@@ -59,12 +59,12 @@ class guard_exprt
5959

6060
bool is_true() const
6161
{
62-
return expr.is_true();
62+
return expr.is_constant() && to_constant_expr(expr).is_true();
6363
}
6464

6565
bool is_false() const
6666
{
67-
return expr.is_false();
67+
return expr.is_constant() && to_constant_expr(expr).is_false();
6868
}
6969

7070
friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);

‎src/analyses/interval_analysis.cpp

+5-2
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,10 @@ void instrument_intervals(
4646
{
4747
goto_programt::const_targett previous = std::prev(i_it);
4848

49-
if(previous->is_goto() && !previous->condition().is_true())
49+
if(
50+
previous->is_goto() &&
51+
(!previous->condition().is_constant() ||
52+
!to_constant_expr(previous->condition()).is_true()))
5053
{
5154
// we follow a branch, instrument
5255
}
@@ -69,7 +72,7 @@ void instrument_intervals(
6972
for(const auto &symbol_expr : symbols)
7073
{
7174
exprt tmp=d.make_expression(symbol_expr);
72-
if(!tmp.is_true())
75+
if(!tmp.is_constant() || !to_constant_expr(tmp).is_true())
7376
assertion.push_back(tmp);
7477
}
7578

‎src/analyses/interval_domain.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -501,7 +501,8 @@ bool interval_domaint::ai_simplify(
501501
// of when condition is true
502502
if(!a.join(d)) // If d (this) is included in a...
503503
{ // Then the condition is always true
504-
unchanged=condition.is_true();
504+
unchanged =
505+
condition.is_constant() && to_constant_expr(condition).is_true();
505506
condition = true_exprt();
506507
}
507508
}
@@ -514,7 +515,8 @@ bool interval_domaint::ai_simplify(
514515
d.assume(not_exprt(condition), ns); // Restrict to when condition is false
515516
if(d.is_bottom()) // If there there are none...
516517
{ // Then the condition is always true
517-
unchanged=condition.is_true();
518+
unchanged =
519+
condition.is_constant() && to_constant_expr(condition).is_true();
518520
condition = true_exprt();
519521
}
520522
}

‎src/analyses/invariant_set.cpp

+22-16
Original file line numberDiff line numberDiff line change
@@ -394,14 +394,17 @@ void invariant_sett::strengthen_rec(const exprt &expr)
394394
return;
395395
}
396396

397-
if(expr.is_true())
398-
{
399-
// do nothing, it's useless
400-
}
401-
else if(expr.is_false())
397+
if(expr.is_constant())
402398
{
403-
// wow, that's strong
404-
make_false();
399+
if(to_constant_expr(expr).is_true())
400+
{
401+
// do nothing, it's useless
402+
}
403+
else
404+
{
405+
// wow, that's strong
406+
make_false();
407+
}
405408
}
406409
else if(expr.id()==ID_not)
407410
{
@@ -596,7 +599,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
596599
if(is_false) // can't get any stronger
597600
return tvt(true);
598601

599-
if(expr.is_true())
602+
if(expr.is_constant() && to_constant_expr(expr).is_true())
600603
return tvt(true);
601604
else if(expr.id()==ID_not)
602605
{
@@ -701,15 +704,18 @@ void invariant_sett::nnf(exprt &expr, bool negate)
701704
if(!expr.is_boolean())
702705
throw "nnf: non-Boolean expression";
703706

704-
if(expr.is_true())
705-
{
706-
if(negate)
707-
expr=false_exprt();
708-
}
709-
else if(expr.is_false())
707+
if(expr.is_constant())
710708
{
711-
if(negate)
712-
expr=true_exprt();
709+
if(to_constant_expr(expr).is_true())
710+
{
711+
if(negate)
712+
expr = false_exprt();
713+
}
714+
else
715+
{
716+
if(negate)
717+
expr = true_exprt();
718+
}
713719
}
714720
else if(expr.id()==ID_not)
715721
{

‎src/analyses/local_bitvector_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
115115
{
116116
if(rhs.is_constant())
117117
{
118-
if(rhs.is_zero())
118+
if(to_constant_expr(rhs).is_zero())
119119
return flagst::mk_null();
120120
else
121121
return flagst::mk_integer_address();

‎src/analyses/local_cfg.cpp

+5-1
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,12 @@ void local_cfgt::build(const goto_programt &goto_program)
3535
switch(instruction.type())
3636
{
3737
case GOTO:
38-
if(!instruction.condition().is_true())
38+
if(
39+
!instruction.condition().is_constant() ||
40+
!to_constant_expr(instruction.condition()).is_true())
41+
{
3942
node.successors.push_back(loc_nr+1);
43+
}
4044

4145
for(const auto &target : instruction.targets)
4246
{

‎src/analyses/local_may_alias.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ void local_may_aliast::get_rec(
171171
{
172172
if(rhs.is_constant())
173173
{
174-
if(rhs.is_zero())
174+
if(to_constant_expr(rhs).is_zero())
175175
dest.insert(objects.number(exprt(ID_null_object)));
176176
else
177177
dest.insert(objects.number(exprt(ID_integer_address_object)));

‎src/analyses/variable-sensitivity/abstract_environment.cpp

+5-5
Original file line numberDiff line numberDiff line change
@@ -269,7 +269,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
269269
// Should be of the right type
270270
INVARIANT(assumption.is_boolean(), "simplification preserves type");
271271

272-
if(assumption.is_false())
272+
if(assumption.is_constant() && to_constant_expr(assumption).is_false())
273273
{
274274
bool currently_bottom = is_bottom();
275275
make_bottom();
@@ -573,10 +573,10 @@ static auto inverse_operations =
573573

574574
static exprt invert_result(const exprt &result)
575575
{
576-
if(!result.is_boolean())
576+
if(!result.is_boolean() || !result.is_constant())
577577
return result;
578578

579-
if(result.is_true())
579+
if(to_constant_expr(result).is_true())
580580
return false_exprt();
581581
return true_exprt();
582582
}
@@ -634,7 +634,7 @@ exprt assume_and(
634634
for(auto const &operand : and_expr.operands())
635635
{
636636
auto result = env.do_assume(operand, ns);
637-
if(result.is_false())
637+
if(result.is_constant() && to_constant_expr(result).is_false())
638638
return result;
639639
nil |= result.is_nil();
640640
}
@@ -827,7 +827,7 @@ exprt assume_less_than(
827827
auto reduced_le_expr =
828828
binary_relation_exprt(left_lower, expr.id(), right_upper);
829829
auto result = env.eval(reduced_le_expr, ns)->to_constant();
830-
if(result.is_true())
830+
if(result.is_constant() && to_constant_expr(result).is_true())
831831
{
832832
if(is_assignable(operands.lhs))
833833
{

0 commit comments

Comments
 (0)