Skip to content

Commit 9a3ffde

Browse files
author
Daniel Kroening
authored
Merge pull request #4931 from diffblue/binding
introduce binding_exprt [blocks: #4510]
2 parents 7662ed0 + 0983a0c commit 9a3ffde

File tree

8 files changed

+136
-73
lines changed

8 files changed

+136
-73
lines changed

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 57 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -290,30 +290,37 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
290290
else if(expr.id()==ID_forall ||
291291
expr.id()==ID_exists)
292292
{
293-
// op0 is a declaration,
294-
// op1 the bound expression
295-
expr.type()=bool_typet();
293+
// These have two operands.
294+
// op0 is a tuple with declarations,
295+
// op1 is the bound expression
296296
auto &binary_expr = to_binary_expr(expr);
297+
auto &bindings = binary_expr.op0().operands();
298+
auto &where = binary_expr.op1();
297299

298-
if(binary_expr.op0().get(ID_statement) != ID_decl)
300+
for(const auto &binding : bindings)
299301
{
300-
error().source_location = expr.source_location();
301-
error() << "expected declaration as operand of quantifier" << eom;
302-
throw 0;
302+
if(binding.get(ID_statement) != ID_decl)
303+
{
304+
error().source_location = expr.source_location();
305+
error() << "expected declaration as operand of quantifier" << eom;
306+
throw 0;
307+
}
303308
}
304309

305-
if(has_subexpr(binary_expr.op1(), ID_side_effect))
310+
if(has_subexpr(where, ID_side_effect))
306311
{
307312
error().source_location = expr.source_location();
308313
error() << "quantifier must not contain side effects" << eom;
309314
throw 0;
310315
}
311316

312-
// replace declaration by symbol expression
313-
symbol_exprt bound = to_code_decl(to_code(binary_expr.op0())).symbol();
314-
binary_expr.op0().swap(bound);
317+
expr.type() = bool_typet();
315318

316-
implicit_typecast_bool(binary_expr.op1());
319+
// replace declarations by symbol expressions
320+
for(auto &binding : bindings)
321+
binding = to_code_decl(to_code(binding)).symbol();
322+
323+
implicit_typecast_bool(where);
317324
}
318325
else if(expr.id()==ID_label)
319326
{
@@ -710,48 +717,55 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
710717
}
711718
else if(expr.id()==ID_forall || expr.id()==ID_exists)
712719
{
720+
// These introduce new symbols, which need to be added to the symbol table
721+
// before the second operand is typechecked.
722+
713723
auto &binary_expr = to_binary_expr(expr);
724+
auto &bindings = binary_expr.op0().operands();
714725

715-
ansi_c_declarationt &declaration = to_ansi_c_declaration(binary_expr.op0());
726+
for(auto &binding : bindings)
727+
{
728+
ansi_c_declarationt &declaration = to_ansi_c_declaration(binding);
716729

717-
typecheck_declaration(declaration);
730+
typecheck_declaration(declaration);
718731

719-
if(declaration.declarators().size()!=1)
720-
{
721-
error().source_location = expr.source_location();
722-
error() << "expected one declarator exactly" << eom;
723-
throw 0;
724-
}
732+
if(declaration.declarators().size() != 1)
733+
{
734+
error().source_location = expr.source_location();
735+
error() << "forall/exists expects one declarator exactly" << eom;
736+
throw 0;
737+
}
725738

726-
irep_idt identifier=
727-
declaration.declarators().front().get_name();
739+
irep_idt identifier = declaration.declarators().front().get_name();
728740

729-
// look it up
730-
symbol_tablet::symbolst::const_iterator s_it=
731-
symbol_table.symbols.find(identifier);
741+
// look it up
742+
symbol_tablet::symbolst::const_iterator s_it =
743+
symbol_table.symbols.find(identifier);
732744

733-
if(s_it==symbol_table.symbols.end())
734-
{
735-
error().source_location = expr.source_location();
736-
error() << "failed to find decl symbol '" << identifier
737-
<< "' in symbol table" << eom;
738-
throw 0;
739-
}
745+
if(s_it == symbol_table.symbols.end())
746+
{
747+
error().source_location = expr.source_location();
748+
error() << "failed to find bound symbol `" << identifier
749+
<< "' in symbol table" << eom;
750+
throw 0;
751+
}
740752

741-
const symbolt &symbol=s_it->second;
753+
const symbolt &symbol = s_it->second;
742754

743-
if(symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
744-
!is_complete_type(symbol.type) || symbol.type.id()==ID_code)
745-
{
746-
error().source_location = expr.source_location();
747-
error() << "unexpected quantified symbol" << eom;
748-
throw 0;
749-
}
755+
if(
756+
symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
757+
!is_complete_type(symbol.type) || symbol.type.id() == ID_code)
758+
{
759+
error().source_location = expr.source_location();
760+
error() << "unexpected quantified symbol" << eom;
761+
throw 0;
762+
}
750763

751-
code_declt decl(symbol.symbol_expr());
752-
decl.add_source_location()=declaration.source_location();
764+
code_declt decl(symbol.symbol_expr());
765+
decl.add_source_location() = declaration.source_location();
753766

754-
binary_expr.op0() = decl;
767+
binding = decl;
768+
}
755769

756770
typecheck_expr(binary_expr.op1());
757771
}

‎src/ansi-c/expr2c.cpp

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -791,20 +791,21 @@ std::string expr2ct::convert_trinary(
791791
}
792792

793793
std::string expr2ct::convert_quantifier(
794-
const exprt &src,
794+
const quantifier_exprt &src,
795795
const std::string &symbol,
796796
unsigned precedence)
797797
{
798-
if(src.operands().size()!=2)
798+
// our made-up syntax can only do one symbol
799+
if(src.op0().operands().size() != 1)
799800
return convert_norep(src, precedence);
800801

801802
unsigned p0, p1;
802803

803-
std::string op0=convert_with_precedence(src.op0(), p0);
804-
std::string op1=convert_with_precedence(src.op1(), p1);
804+
std::string op0 = convert_with_precedence(src.symbol(), p0);
805+
std::string op1 = convert_with_precedence(src.where(), p1);
805806

806807
std::string dest=symbol+" { ";
807-
dest+=convert(src.op0().type());
808+
dest += convert(src.symbol().type());
808809
dest+=" "+op0+"; ";
809810
dest+=op1;
810811
dest+=" }";
@@ -3720,13 +3721,16 @@ std::string expr2ct::convert_with_precedence(
37203721
return convert_trinary(to_if_expr(src), "?", ":", precedence = 3);
37213722

37223723
else if(src.id()==ID_forall)
3723-
return convert_quantifier(src, "forall", precedence=2);
3724+
return convert_quantifier(
3725+
to_quantifier_expr(src), "forall", precedence = 2);
37243726

37253727
else if(src.id()==ID_exists)
3726-
return convert_quantifier(src, "exists", precedence=2);
3728+
return convert_quantifier(
3729+
to_quantifier_expr(src), "exists", precedence = 2);
37273730

37283731
else if(src.id()==ID_lambda)
3729-
return convert_quantifier(src, "LAMBDA", precedence=2);
3732+
return convert_quantifier(
3733+
to_quantifier_expr(src), "LAMBDA", precedence = 2);
37303734

37313735
else if(src.id()==ID_with)
37323736
return convert_with(src, precedence=16);

‎src/ansi-c/expr2c_class.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,8 @@ class expr2ct
128128
const exprt &src, unsigned &precedence);
129129

130130
std::string convert_quantifier(
131-
const exprt &src, const std::string &symbol,
131+
const quantifier_exprt &,
132+
const std::string &symbol,
132133
unsigned precedence);
133134

134135
std::string convert_with(

‎src/ansi-c/parser.y

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,8 @@ extern char *yyansi_ctext;
2626

2727
#include "ansi_c_y.tab.h"
2828

29+
#include <util/mathematical_expr.h>
30+
2931
#ifdef _MSC_VER
3032
// possible loss of data
3133
#pragma warning(disable:4242)
@@ -469,15 +471,15 @@ quantifier_expression:
469471
{
470472
$$=$1;
471473
set($$, ID_forall);
472-
mto($$, $4);
474+
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
473475
mto($$, $5);
474476
PARSER.pop_scope();
475477
}
476478
| TOK_EXISTS compound_scope '{' declaration comma_expression '}'
477479
{
478480
$$=$1;
479481
set($$, ID_exists);
480-
mto($$, $4);
482+
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
481483
mto($$, $5);
482484
PARSER.pop_scope();
483485
}
@@ -810,15 +812,15 @@ ACSL_binding_expression:
810812
{
811813
$$=$1;
812814
set($$, ID_forall);
813-
mto($$, $3);
815+
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
814816
mto($$, $4);
815817
PARSER.pop_scope();
816818
}
817819
| TOK_ACSL_EXISTS compound_scope declaration ACSL_binding_expression
818820
{
819821
$$=$1;
820822
set($$, ID_exists);
821-
mto($$, $3);
823+
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
822824
mto($$, $4);
823825
PARSER.pop_scope();
824826
}

‎src/solvers/flattening/boolbv_quantifier.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -140,8 +140,8 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
140140
return re;
141141
}
142142

143-
const auto min_i = get_quantifier_var_min(var_expr, re);
144-
const auto max_i = get_quantifier_var_max(var_expr, re);
143+
const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
144+
const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);
145145

146146
if(!min_i.has_value() || !max_i.has_value())
147147
return nullopt;

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1807,7 +1807,7 @@ void smt2_convt::convert_expr(const exprt &expr)
18071807
else if(quantifier_expr.id() == ID_exists)
18081808
out << "(exists ";
18091809

1810-
exprt bound=expr.op0();
1810+
exprt bound = quantifier_expr.symbol();
18111811

18121812
out << "((";
18131813
convert_expr(bound);

‎src/solvers/smt2/smt2_parser.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -283,7 +283,7 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
283283
// go backwards, build quantified expression
284284
for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
285285
{
286-
binary_predicate_exprt quantifier(*r_it, id, result);
286+
quantifier_exprt quantifier(id, *r_it, result);
287287
result=quantifier;
288288
}
289289

‎src/util/mathematical_expr.h

Lines changed: 55 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -271,26 +271,34 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
271271
return ret;
272272
}
273273

274-
/// \brief A base class for quantifier expressions
275-
class quantifier_exprt : public binary_predicate_exprt
274+
/// \brief A base class for variable bindings (quantifiers, let, lambda)
275+
class binding_exprt : public binary_exprt
276276
{
277277
public:
278-
quantifier_exprt(
279-
const irep_idt &_id,
280-
const symbol_exprt &_symbol,
281-
const exprt &_where)
282-
: binary_predicate_exprt(_symbol, _id, _where)
278+
using variablest = std::vector<symbol_exprt>;
279+
280+
/// construct the binding expression
281+
binding_exprt(
282+
irep_idt _id,
283+
const variablest &_variables,
284+
exprt _where,
285+
typet _type)
286+
: binary_exprt(
287+
tuple_exprt((const operandst &)_variables),
288+
_id,
289+
std::move(_where),
290+
std::move(_type))
283291
{
284292
}
285293

286-
symbol_exprt &symbol()
294+
variablest &variables()
287295
{
288-
return static_cast<symbol_exprt &>(op0());
296+
return (variablest &)static_cast<tuple_exprt &>(op0()).operands();
289297
}
290298

291-
const symbol_exprt &symbol() const
299+
const variablest &variables() const
292300
{
293-
return static_cast<const symbol_exprt &>(op0());
301+
return (variablest &)static_cast<const tuple_exprt &>(op0()).operands();
294302
}
295303

296304
exprt &where()
@@ -304,6 +312,39 @@ class quantifier_exprt : public binary_predicate_exprt
304312
}
305313
};
306314

315+
/// \brief A base class for quantifier expressions
316+
class quantifier_exprt : public binding_exprt
317+
{
318+
public:
319+
/// constructor for single variable
320+
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
321+
: binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
322+
{
323+
}
324+
325+
/// constructor for multiple variables
326+
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
327+
: binding_exprt(_id, _variables, std::move(_where), bool_typet())
328+
{
329+
}
330+
331+
// for the special case of one variable
332+
symbol_exprt &symbol()
333+
{
334+
auto &variables = this->variables();
335+
PRECONDITION(variables.size() == 1);
336+
return variables.front();
337+
}
338+
339+
// for the special case of one variable
340+
const symbol_exprt &symbol() const
341+
{
342+
auto &variables = this->variables();
343+
PRECONDITION(variables.size() == 1);
344+
return variables.front();
345+
}
346+
};
347+
307348
template <>
308349
inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
309350
{
@@ -313,8 +354,9 @@ inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
313354
inline void validate_expr(const quantifier_exprt &value)
314355
{
315356
validate_operands(value, 2, "quantifier expressions must have two operands");
316-
DATA_INVARIANT(
317-
value.op0().id() == ID_symbol, "quantified variable shall be a symbol");
357+
for(auto &op : value.variables())
358+
DATA_INVARIANT(
359+
op.id() == ID_symbol, "quantified variable shall be a symbol");
318360
}
319361

320362
/// \brief Cast an exprt to a \ref quantifier_exprt

0 commit comments

Comments
 (0)