Skip to content

introduce binding_exprt [blocks: #4510] #4931

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 6, 2019
Merged

introduce binding_exprt [blocks: #4510] #4931

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4dd483a
introduce binding_exprt
Jul 20, 2019
c4f7a89
quantifiers are variable bindings
Jul 20, 2019
0983a0c
make return type of get_quantifier_var_min obvious
Aug 5, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 57 additions & 43 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,30 +290,37 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
else if(expr.id()==ID_forall ||
expr.id()==ID_exists)
{
// op0 is a declaration,
// op1 the bound expression
expr.type()=bool_typet();
// These have two operands.
// op0 is a tuple with declarations,
// op1 is the bound expression
auto &binary_expr = to_binary_expr(expr);
auto &bindings = binary_expr.op0().operands();
auto &where = binary_expr.op1();

if(binary_expr.op0().get(ID_statement) != ID_decl)
for(const auto &binding : bindings)
{
error().source_location = expr.source_location();
error() << "expected declaration as operand of quantifier" << eom;
throw 0;
if(binding.get(ID_statement) != ID_decl)
{
error().source_location = expr.source_location();
error() << "expected declaration as operand of quantifier" << eom;
throw 0;
}
}

if(has_subexpr(binary_expr.op1(), ID_side_effect))
if(has_subexpr(where, ID_side_effect))
{
error().source_location = expr.source_location();
error() << "quantifier must not contain side effects" << eom;
throw 0;
}

// replace declaration by symbol expression
symbol_exprt bound = to_code_decl(to_code(binary_expr.op0())).symbol();
binary_expr.op0().swap(bound);
expr.type() = bool_typet();

implicit_typecast_bool(binary_expr.op1());
// replace declarations by symbol expressions
for(auto &binding : bindings)
binding = to_code_decl(to_code(binding)).symbol();

implicit_typecast_bool(where);
}
else if(expr.id()==ID_label)
{
Expand Down Expand Up @@ -710,48 +717,55 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
}
else if(expr.id()==ID_forall || expr.id()==ID_exists)
{
// These introduce new symbols, which need to be added to the symbol table
// before the second operand is typechecked.

auto &binary_expr = to_binary_expr(expr);
auto &bindings = binary_expr.op0().operands();

ansi_c_declarationt &declaration = to_ansi_c_declaration(binary_expr.op0());
for(auto &binding : bindings)
{
ansi_c_declarationt &declaration = to_ansi_c_declaration(binding);

typecheck_declaration(declaration);
typecheck_declaration(declaration);

if(declaration.declarators().size()!=1)
{
error().source_location = expr.source_location();
error() << "expected one declarator exactly" << eom;
throw 0;
}
if(declaration.declarators().size() != 1)
{
error().source_location = expr.source_location();
error() << "forall/exists expects one declarator exactly" << eom;
throw 0;
}

irep_idt identifier=
declaration.declarators().front().get_name();
irep_idt identifier = declaration.declarators().front().get_name();

// look it up
symbol_tablet::symbolst::const_iterator s_it=
symbol_table.symbols.find(identifier);
// look it up
symbol_tablet::symbolst::const_iterator s_it =
symbol_table.symbols.find(identifier);

if(s_it==symbol_table.symbols.end())
{
error().source_location = expr.source_location();
error() << "failed to find decl symbol '" << identifier
<< "' in symbol table" << eom;
throw 0;
}
if(s_it == symbol_table.symbols.end())
{
error().source_location = expr.source_location();
error() << "failed to find bound symbol `" << identifier
<< "' in symbol table" << eom;
throw 0;
}

const symbolt &symbol=s_it->second;
const symbolt &symbol = s_it->second;

if(symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
!is_complete_type(symbol.type) || symbol.type.id()==ID_code)
{
error().source_location = expr.source_location();
error() << "unexpected quantified symbol" << eom;
throw 0;
}
if(
symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
!is_complete_type(symbol.type) || symbol.type.id() == ID_code)
{
error().source_location = expr.source_location();
error() << "unexpected quantified symbol" << eom;
throw 0;
}

code_declt decl(symbol.symbol_expr());
decl.add_source_location()=declaration.source_location();
code_declt decl(symbol.symbol_expr());
decl.add_source_location() = declaration.source_location();

binary_expr.op0() = decl;
binding = decl;
}

typecheck_expr(binary_expr.op1());
}
Expand Down
20 changes: 12 additions & 8 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -791,20 +791,21 @@ std::string expr2ct::convert_trinary(
}

std::string expr2ct::convert_quantifier(
const exprt &src,
const quantifier_exprt &src,
const std::string &symbol,
unsigned precedence)
{
if(src.operands().size()!=2)
// our made-up syntax can only do one symbol
if(src.op0().operands().size() != 1)
return convert_norep(src, precedence);

unsigned p0, p1;

std::string op0=convert_with_precedence(src.op0(), p0);
std::string op1=convert_with_precedence(src.op1(), p1);
std::string op0 = convert_with_precedence(src.symbol(), p0);
std::string op1 = convert_with_precedence(src.where(), p1);

std::string dest=symbol+" { ";
dest+=convert(src.op0().type());
dest += convert(src.symbol().type());
dest+=" "+op0+"; ";
dest+=op1;
dest+=" }";
Expand Down Expand Up @@ -3720,13 +3721,16 @@ std::string expr2ct::convert_with_precedence(
return convert_trinary(to_if_expr(src), "?", ":", precedence = 3);

else if(src.id()==ID_forall)
return convert_quantifier(src, "forall", precedence=2);
return convert_quantifier(
to_quantifier_expr(src), "forall", precedence = 2);

else if(src.id()==ID_exists)
return convert_quantifier(src, "exists", precedence=2);
return convert_quantifier(
to_quantifier_expr(src), "exists", precedence = 2);

else if(src.id()==ID_lambda)
return convert_quantifier(src, "LAMBDA", precedence=2);
return convert_quantifier(
to_quantifier_expr(src), "LAMBDA", precedence = 2);

else if(src.id()==ID_with)
return convert_with(src, precedence=16);
Expand Down
3 changes: 2 additions & 1 deletion src/ansi-c/expr2c_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,8 @@ class expr2ct
const exprt &src, unsigned &precedence);

std::string convert_quantifier(
const exprt &src, const std::string &symbol,
const quantifier_exprt &,
const std::string &symbol,
unsigned precedence);

std::string convert_with(
Expand Down
10 changes: 6 additions & 4 deletions src/ansi-c/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ extern char *yyansi_ctext;

#include "ansi_c_y.tab.h"

#include <util/mathematical_expr.h>

#ifdef _MSC_VER
// possible loss of data
#pragma warning(disable:4242)
Expand Down Expand Up @@ -469,15 +471,15 @@ quantifier_expression:
{
$$=$1;
set($$, ID_forall);
mto($$, $4);
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
mto($$, $5);
PARSER.pop_scope();
}
| TOK_EXISTS compound_scope '{' declaration comma_expression '}'
{
$$=$1;
set($$, ID_exists);
mto($$, $4);
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
mto($$, $5);
PARSER.pop_scope();
}
Expand Down Expand Up @@ -810,15 +812,15 @@ ACSL_binding_expression:
{
$$=$1;
set($$, ID_forall);
mto($$, $3);
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
mto($$, $4);
PARSER.pop_scope();
}
| TOK_ACSL_EXISTS compound_scope declaration ACSL_binding_expression
{
$$=$1;
set($$, ID_exists);
mto($$, $3);
parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
mto($$, $4);
PARSER.pop_scope();
}
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/flattening/boolbv_quantifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,8 +140,8 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
return re;
}

const auto min_i = get_quantifier_var_min(var_expr, re);
const auto max_i = get_quantifier_var_max(var_expr, re);
const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);

if(!min_i.has_value() || !max_i.has_value())
return nullopt;
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1807,7 +1807,7 @@ void smt2_convt::convert_expr(const exprt &expr)
else if(quantifier_expr.id() == ID_exists)
out << "(exists ";

exprt bound=expr.op0();
exprt bound = quantifier_expr.symbol();

out << "((";
convert_expr(bound);
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/smt2/smt2_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -283,7 +283,7 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
// go backwards, build quantified expression
for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
{
binary_predicate_exprt quantifier(*r_it, id, result);
quantifier_exprt quantifier(id, *r_it, result);
result=quantifier;
}

Expand Down
68 changes: 55 additions & 13 deletions src/util/mathematical_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -271,26 +271,34 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
return ret;
}

/// \brief A base class for quantifier expressions
class quantifier_exprt : public binary_predicate_exprt
/// \brief A base class for variable bindings (quantifiers, let, lambda)
class binding_exprt : public binary_exprt
{
public:
quantifier_exprt(
const irep_idt &_id,
const symbol_exprt &_symbol,
const exprt &_where)
: binary_predicate_exprt(_symbol, _id, _where)
using variablest = std::vector<symbol_exprt>;

/// construct the binding expression
binding_exprt(
irep_idt _id,
const variablest &_variables,
exprt _where,
typet _type)
: binary_exprt(
tuple_exprt((const operandst &)_variables),
_id,
std::move(_where),
std::move(_type))
{
}

symbol_exprt &symbol()
variablest &variables()
{
return static_cast<symbol_exprt &>(op0());
return (variablest &)static_cast<tuple_exprt &>(op0()).operands();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Quite likely this isn't the only such place, but this clearly makes USE_LIST no longer possible -- but in this case without causing compilation errors. So should we really get rid of USE_LIST right now?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be possible to make this work with USE_LIST. Is USE_LIST sill useful?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code wouldn't actually compile with USE_LIST. If USE_LIST were to work, we could change irept to have only a single container and some cursor(s) into that. Whether that's more efficient or not I can't tell, because it wouldn't compile...

}

const symbol_exprt &symbol() const
const variablest &variables() const
{
return static_cast<const symbol_exprt &>(op0());
return (variablest &)static_cast<const tuple_exprt &>(op0()).operands();
}

exprt &where()
Expand All @@ -304,6 +312,39 @@ class quantifier_exprt : public binary_predicate_exprt
}
};

/// \brief A base class for quantifier expressions
class quantifier_exprt : public binding_exprt
{
public:
/// constructor for single variable
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
: binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
{
}

/// constructor for multiple variables
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
: binding_exprt(_id, _variables, std::move(_where), bool_typet())
{
}

// for the special case of one variable
symbol_exprt &symbol()
{
auto &variables = this->variables();
PRECONDITION(variables.size() == 1);
return variables.front();
}

// for the special case of one variable
const symbol_exprt &symbol() const
{
auto &variables = this->variables();
PRECONDITION(variables.size() == 1);
return variables.front();
}
};

template <>
inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
{
Expand All @@ -313,8 +354,9 @@ inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
inline void validate_expr(const quantifier_exprt &value)
{
validate_operands(value, 2, "quantifier expressions must have two operands");
DATA_INVARIANT(
value.op0().id() == ID_symbol, "quantified variable shall be a symbol");
for(auto &op : value.variables())
DATA_INVARIANT(
op.id() == ID_symbol, "quantified variable shall be a symbol");
}

/// \brief Cast an exprt to a \ref quantifier_exprt
Expand Down