Skip to content

Commit 449b771

Browse files
qinhepingqinheping
committed
Fix regression tests
1 parent 7e30d2c commit 449b771

File tree

4 files changed

+147
-137
lines changed

4 files changed

+147
-137
lines changed

‎regression/cbmc/Quantifiers1/quantifier-with-function-call.desc‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11
CORE
22
quantifier-with-function-call.c
33

4-
^EXIT=134$
4+
^EXIT=6$
55
^SIGNAL=0$
6-
^Invariant check failed
7-
^Reason: quantifier must not contain side effects
6+
quantifier must not contain function calls
87
--
98
^warning: ignoring

‎regression/validate-trace-xml-schema/check.py‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,8 @@
7474
# the SAT back-end only
7575
['integer-assignments1', 'test.desc'],
7676
# this test is expected to abort, thus producing invalid XML
77-
['String_Abstraction17', 'test.desc']
77+
['String_Abstraction17', 'test.desc'],
78+
['Quantifiers1', 'quantifier-with-function-call.desc']
7879
]))
7980

8081
# TODO maybe consider looking them up on PATH, but direct paths are

‎src/ansi-c/c_typecheck_expr.cpp‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -316,10 +316,16 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
316316
}
317317
}
318318

319-
if(expr.id() == ID_lambda && has_subexpr(where, ID_side_effect))
319+
if(has_subexpr(
320+
where,
321+
[&](const exprt &subexpr)
322+
{
323+
return can_cast_expr<side_effect_exprt>(subexpr) &&
324+
can_cast_expr<side_effect_expr_function_callt>(subexpr);
325+
}))
320326
{
321327
error().source_location = expr.source_location();
322-
error() << "lambda expressions must not contain side effects" << eom;
328+
error() << "quantifier must not contain function calls" << eom;
323329
throw 0;
324330
}
325331

‎src/ansi-c/goto-conversion/goto_clean_expr.cpp‎

Lines changed: 135 additions & 131 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,140 @@ static symbol_exprt find_base_symbol(const exprt &expr)
4848
}
4949
}
5050

51+
static exprt convert_statement_expression(
52+
const quantifier_exprt &qex,
53+
const code_expressiont &code,
54+
const irep_idt &mode,
55+
goto_convertt &converter)
56+
{
57+
goto_programt where;
58+
converter.goto_convert(code, where, mode);
59+
where.compute_location_numbers();
60+
61+
natural_loops_mutablet natural_loops(where);
62+
INVARIANT(
63+
natural_loops.loop_map.size() == 0,
64+
"quantifier must not contain side effects");
65+
66+
// `last` is the instruction corresponding to the last expression in the
67+
// statement expression.
68+
goto_programt::const_targett last;
69+
for(goto_programt::const_targett it = where.instructions.begin();
70+
it != where.instructions.end();
71+
++it)
72+
{
73+
// `last` is an other-instruction.
74+
if(it->is_other())
75+
{
76+
last = it;
77+
}
78+
}
79+
auto last_expr =
80+
expr_try_dynamic_cast<code_expressiont>(last->get_other())->expression();
81+
82+
// `pathes` contains all the `targett` we are iterating over.
83+
std::vector<goto_programt::const_targett> pathes;
84+
pathes.push_back(where.instructions.begin());
85+
std::vector<std::pair<exprt, replace_symbolt>> path_conditions_and_value_maps;
86+
path_conditions_and_value_maps.push_back(
87+
std::make_pair(true_exprt(), replace_symbolt()));
88+
89+
std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
90+
// All bounded variables are local.
91+
declared_symbols.insert(qex.variables().begin(), qex.variables().end());
92+
93+
exprt res = true_exprt();
94+
95+
// Visit the quantifeir body along `pathes`.
96+
while(!pathes.empty())
97+
{
98+
auto &current_it = pathes.back();
99+
auto &path_condition = path_conditions_and_value_maps.back().first;
100+
auto &value_map = path_conditions_and_value_maps.back().second;
101+
INVARIANT(
102+
current_it != where.instructions.end(),
103+
"Quantifier body must have a unique end expression.");
104+
105+
// Add all local-declared symbols into `declared_symbols`.
106+
if(current_it->is_decl())
107+
{
108+
declared_symbols.insert(current_it->decl_symbol());
109+
}
110+
// ASSIGN lhs := rhs
111+
// Add the replace lhr <- value_map(rhs) to the current value_map.
112+
if(current_it->is_assign())
113+
{
114+
// Check that if lhs is a declared symbol.
115+
auto lhs = current_it->assign_lhs();
116+
INVARIANT(
117+
declared_symbols.count(find_base_symbol(lhs)),
118+
"quantifier must not contain side effects");
119+
exprt rhs = current_it->assign_rhs();
120+
INVARIANT(
121+
!has_subexpr(rhs, ID_function_call),
122+
"quantifier must not contain side effects");
123+
value_map.replace(rhs);
124+
value_map.set(to_symbol_expr(current_it->assign_lhs()), rhs);
125+
}
126+
// GOTO label
127+
// -----------
128+
// Move the current targett to label.
129+
// or
130+
// IF cond GOTO label
131+
// ----------
132+
// Move the current targett to targett+1 with path condition
133+
// path_condition && !cond;
134+
// and add a new path starting from label with path condition
135+
// path_condition && cond.
136+
if(current_it->is_goto())
137+
{
138+
if(current_it->has_condition())
139+
{
140+
auto next_it = current_it->targets.front();
141+
exprt copy_path_condition = path_condition;
142+
replace_symbolt copy_symbol_map = value_map;
143+
path_condition =
144+
and_exprt(path_condition, not_exprt(current_it->condition()));
145+
path_conditions_and_value_maps.push_back(std::make_pair(
146+
and_exprt(copy_path_condition, current_it->condition()),
147+
copy_symbol_map));
148+
current_it++;
149+
pathes.push_back(next_it);
150+
}
151+
else
152+
{
153+
current_it = current_it->targets.front();
154+
}
155+
continue;
156+
}
157+
// EXPRESSION(expr)
158+
// The last instruction is an exression statement.
159+
// We add the predicate path_condition ==> value_map(expr) to res.
160+
if(current_it == last)
161+
{
162+
exprt copy_of_last_expr = last_expr;
163+
value_map.replace(copy_of_last_expr);
164+
res = and_exprt(res, implies_exprt(path_condition, copy_of_last_expr));
165+
path_conditions_and_value_maps.pop_back();
166+
pathes.pop_back();
167+
continue;
168+
}
169+
// DEAD symbol
170+
// Remove symbol from declared_symbols.
171+
if(current_it->is_dead())
172+
{
173+
declared_symbols.erase(current_it->decl_symbol());
174+
}
175+
// Unsupported instructions.
176+
if(current_it->is_function_call())
177+
{
178+
UNREACHABLE;
179+
}
180+
current_it++;
181+
}
182+
return res;
183+
}
184+
51185
symbol_exprt goto_convertt::make_compound_literal(
52186
const exprt &expr,
53187
goto_programt &dest,
@@ -491,137 +625,7 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
491625
code.operands()[0].get_named_sub()[ID_statement].id() ==
492626
ID_statement_expression)
493627
{
494-
goto_programt where;
495-
goto_convert(code, where, mode);
496-
where.compute_location_numbers();
497-
498-
natural_loops_mutablet natural_loops(where);
499-
INVARIANT(
500-
natural_loops.loop_map.size() == 0,
501-
"quantifier must not contain side effects");
502-
503-
// `last` is the instruction corresponding to the last expression in the
504-
// statement expression.
505-
goto_programt::const_targett last;
506-
for(goto_programt::const_targett it = where.instructions.begin();
507-
it != where.instructions.end();
508-
++it)
509-
{
510-
// `last` is an other-instruction.
511-
if(it->is_other())
512-
{
513-
last = it;
514-
}
515-
}
516-
auto last_expr =
517-
expr_try_dynamic_cast<code_expressiont>(last->get_other())
518-
->expression();
519-
520-
// `pathes` contains all the `targett` we are iterating over.
521-
std::vector<goto_programt::const_targett> pathes;
522-
pathes.push_back(where.instructions.begin());
523-
std::vector<std::pair<exprt, replace_symbolt>>
524-
path_conditions_and_value_maps;
525-
path_conditions_and_value_maps.push_back(
526-
std::make_pair(true_exprt(), replace_symbolt()));
527-
528-
std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
529-
// All bounded variables are local.
530-
declared_symbols.insert(qex.variables().begin(), qex.variables().end());
531-
532-
exprt res = true_exprt();
533-
534-
// Visit the quantifeir body along `pathes`.
535-
while(!pathes.empty())
536-
{
537-
auto &current_it = pathes.back();
538-
auto &path_condition = path_conditions_and_value_maps.back().first;
539-
auto &value_map = path_conditions_and_value_maps.back().second;
540-
INVARIANT(
541-
current_it != where.instructions.end(),
542-
"Quantifier body must have a unique end expression.");
543-
544-
// Add all local-declared symbols into `declared_symbols`.
545-
if(current_it->is_decl())
546-
{
547-
declared_symbols.insert(current_it->decl_symbol());
548-
}
549-
// ASSIGN lhs := rhs
550-
// Add the replace lhr <- value_map(rhs) to the current value_map.
551-
if(current_it->is_assign())
552-
{
553-
// Check that if lhs is a declared symbol.
554-
auto lhs = current_it->assign_lhs();
555-
INVARIANT(
556-
declared_symbols.count(find_base_symbol(lhs)),
557-
"quantifier must not contain side effects");
558-
exprt rhs = current_it->assign_rhs();
559-
INVARIANT(
560-
!has_subexpr(rhs, ID_function_call),
561-
"quantifier must not contain side effects");
562-
value_map.replace(rhs);
563-
value_map.set(to_symbol_expr(current_it->assign_lhs()), rhs);
564-
}
565-
// GOTO label
566-
// -----------
567-
// Move the current targett to label.
568-
// or
569-
// IF cond GOTO label
570-
// ----------
571-
// Move the current targett to targett+1 with path condition
572-
// path_condition && !cond;
573-
// and add a new path starting from label with path condition
574-
// path_condition && cond.
575-
if(current_it->is_goto())
576-
{
577-
if(current_it->has_condition())
578-
{
579-
auto next_it = current_it->targets.front();
580-
exprt copy_path_condition = path_condition;
581-
replace_symbolt copy_symbol_map = value_map;
582-
path_condition = simplify_expr(
583-
and_exprt(path_condition, not_exprt(current_it->condition())),
584-
ns);
585-
path_conditions_and_value_maps.push_back(std::make_pair(
586-
simplify_expr(
587-
and_exprt(copy_path_condition, current_it->condition()), ns),
588-
copy_symbol_map));
589-
current_it++;
590-
pathes.push_back(next_it);
591-
}
592-
else
593-
{
594-
current_it = current_it->targets.front();
595-
}
596-
continue;
597-
}
598-
// EXPRESSION(expr)
599-
// The last instruction is an exression statement.
600-
// We add the predicate path_condition ==> value_map(expr) to res.
601-
if(current_it == last)
602-
{
603-
exprt copy_of_last_expr = last_expr;
604-
value_map.replace(copy_of_last_expr);
605-
res =
606-
and_exprt(res, implies_exprt(path_condition, copy_of_last_expr));
607-
path_conditions_and_value_maps.pop_back();
608-
pathes.pop_back();
609-
continue;
610-
}
611-
// DEAD symbol
612-
// Remove symbol from declared_symbols.
613-
if(current_it->is_dead())
614-
{
615-
declared_symbols.erase(current_it->decl_symbol());
616-
}
617-
// Unsupported instructions.
618-
if(current_it->is_function_call())
619-
{
620-
UNREACHABLE;
621-
}
622-
current_it++;
623-
}
624-
628+
auto res = convert_statement_expression(qex, code, mode, *this);
625629
qex.where() = res;
626630
return clean_expr(res, mode, result_is_used);
627631
}

0 commit comments

Comments
 (0)