From f7d25b936e9b83bb199511758fc97455abdff070 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 10 Feb 2025 11:50:51 +0000 Subject: [PATCH] SMV: separate type checking and type propagation This splits up type checking (language semantics) from type propagation (an optimisation). --- regression/smv/boolean/boolean_expected1.desc | 2 +- regression/smv/boolean/boolean_expected2.desc | 2 +- regression/smv/boolean/boolean_expected3.desc | 2 +- regression/smv/boolean/boolean_expected4.desc | 2 +- src/smvlang/Makefile | 10 +- src/smvlang/smv_range.cpp | 14 + src/smvlang/smv_range.h | 24 +- src/smvlang/smv_typecheck.cpp | 398 ++++++------------ 8 files changed, 166 insertions(+), 288 deletions(-) create mode 100644 src/smvlang/smv_range.cpp diff --git a/regression/smv/boolean/boolean_expected1.desc b/regression/smv/boolean/boolean_expected1.desc index 7386134a1..890efe432 100644 --- a/regression/smv/boolean/boolean_expected1.desc +++ b/regression/smv/boolean/boolean_expected1.desc @@ -1,7 +1,7 @@ CORE boolean_expected1.smv -^file boolean_expected1\.smv line 3: expected 0 or 1 here, but got 10$ +^file boolean_expected1\.smv line 3: Expected expression of type `boolean', but got expression `10', which is of type `10..10'$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/boolean/boolean_expected2.desc b/regression/smv/boolean/boolean_expected2.desc index 37d6faafe..71b5338e7 100644 --- a/regression/smv/boolean/boolean_expected2.desc +++ b/regression/smv/boolean/boolean_expected2.desc @@ -1,7 +1,7 @@ CORE boolean_expected2.smv -^file boolean_expected2\.smv line 5: expected 0 or 1 here, but got 5$ +^file boolean_expected2\.smv line 5: Expected expression of type `boolean', but got expression `5', which is of type `5..5'$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/boolean/boolean_expected3.desc b/regression/smv/boolean/boolean_expected3.desc index b3ff245d8..261cc12d5 100644 --- a/regression/smv/boolean/boolean_expected3.desc +++ b/regression/smv/boolean/boolean_expected3.desc @@ -1,7 +1,7 @@ CORE boolean_expected3.smv -^file boolean_expected3\.smv line 3: expected 0 or 1 here, but got 3$ +^file boolean_expected3\.smv line 3: Expected expression of type `boolean', but got expression `3', which is of type `3..3'$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/boolean/boolean_expected4.desc b/regression/smv/boolean/boolean_expected4.desc index c598aad30..bb7009001 100644 --- a/regression/smv/boolean/boolean_expected4.desc +++ b/regression/smv/boolean/boolean_expected4.desc @@ -1,7 +1,7 @@ CORE boolean_expected4.smv -^file boolean_expected4\.smv line 6: expected 0 or 1 here, but got 5$ +^file boolean_expected4\.smv line 6: Expected expression of type `boolean', but got expression `5', which is of type `5..5'$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/src/smvlang/Makefile b/src/smvlang/Makefile index b8e0cb7eb..c3d01c4b9 100644 --- a/src/smvlang/Makefile +++ b/src/smvlang/Makefile @@ -1,5 +1,11 @@ -SRC = smv_language.cpp smv_parser.cpp smv_typecheck.cpp expr2smv.cpp \ - smv_y.tab.cpp lex.yy.cpp smv_parse_tree.cpp +SRC = smv_language.cpp \ + smv_parser.cpp \ + smv_typecheck.cpp \ + expr2smv.cpp \ + smv_y.tab.cpp \ + lex.yy.cpp \ + smv_parse_tree.cpp \ + smv_range.cpp include ../config.inc include ../common diff --git a/src/smvlang/smv_range.cpp b/src/smvlang/smv_range.cpp new file mode 100644 index 000000000..8ada89a1b --- /dev/null +++ b/src/smvlang/smv_range.cpp @@ -0,0 +1,14 @@ +/*******************************************************************\ + +Module: SMV Typechecking + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "smv_range.h" + +std::ostream &operator<<(std::ostream &out, const smv_ranget &range) +{ + return out << range.from << ".." << range.to; +} diff --git a/src/smvlang/smv_range.h b/src/smvlang/smv_range.h index 4fec77720..5d3bc750a 100644 --- a/src/smvlang/smv_range.h +++ b/src/smvlang/smv_range.h @@ -11,6 +11,8 @@ Author: Daniel Kroening, dkr@amazon.com #include +#include + class smv_ranget { public: @@ -58,32 +60,30 @@ class smv_ranget return from == to; } - smv_ranget &operator+(const smv_ranget &other) + smv_ranget operator+(const smv_ranget &other) const { - from += other.from; - to += other.to; - return *this; + return {from + other.from, to + other.to}; } - smv_ranget &operator-(const smv_ranget &other) + smv_ranget operator-(const smv_ranget &other) const { - from -= other.from; - to -= other.to; - return *this; + return {from - other.from, to - other.to}; } - smv_ranget &operator*(const smv_ranget &other) + smv_ranget operator*(const smv_ranget &other) const { mp_integer p1 = from * other.from; mp_integer p2 = from * other.to; mp_integer p3 = to * other.from; mp_integer p4 = to * other.to; - from = std::min(p1, std::min(p2, std::min(p3, p4))); - to = std::max(p1, std::max(p2, std::max(p3, p4))); + mp_integer from = std::min(p1, std::min(p2, std::min(p3, p4))); + mp_integer to = std::max(p1, std::max(p2, std::max(p3, p4))); - return *this; + return {std::move(from), std::move(to)}; } + + friend std::ostream &operator<<(std::ostream &, const smv_ranget &); }; #endif // CPROVER_SMV_RANGE_H diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 474026d18..240cade9f 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -63,8 +63,10 @@ class smv_typecheckt:public typecheckt typedef enum { NORMAL, NEXT } expr_modet; void convert(exprt &, expr_modet); - void typecheck(exprt &, const typet &, modet); - void typecheck_op(exprt &, const typet &, modet); + void typecheck(exprt &expr, modet mode) + { + typecheck_expr_rec(expr, mode); + } void typecheck() override; @@ -81,7 +83,8 @@ class smv_typecheckt:public typecheckt smv_ranget convert_type(const typet &); void convert(smv_parse_treet::modulet::itemt &); void typecheck(smv_parse_treet::modulet::itemt &); - void typecheck_expr_rec(exprt &, const typet &, modet); + void typecheck_expr_rec(exprt &, modet); + void convert_expr_to(exprt &, const typet &dest); smv_parse_treet::modulet *modulep; @@ -320,7 +323,9 @@ void smv_typecheckt::instantiate( if(!symbol.value.is_nil()) { instantiate_rename(symbol.value, rename_map); - typecheck(symbol.value, symbol.type, OTHER); + typecheck(symbol.value, OTHER); + if(symbol.type.is_not_nil()) + convert_expr_to(symbol.value, symbol.type); } } @@ -408,49 +413,6 @@ void smv_typecheckt::instantiate_rename( /*******************************************************************\ -Function: smv_typecheckt::typecheck_op - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void smv_typecheckt::typecheck_op( - exprt &expr, - const typet &type, - modet mode) -{ - if(expr.operands().size()==0) - { - throw errort().with_location(expr.find_source_location()) - << "Expected operands for " << expr.id() << " operator"; - } - - for(auto &op : expr.operands()) - typecheck_expr_rec(op, type, mode); - - expr.type()=type; - - // type fixed? - - if(type.is_nil()) - { - // figure out types - - for(const auto &op : expr.operands()) - if(!op.type().is_nil()) - { - expr.type() = op.type(); - break; - } - } -} - -/*******************************************************************\ - Function: smv_typecheckt::convert_type Inputs: @@ -556,26 +518,6 @@ typet smv_typecheckt::type_union( /*******************************************************************\ -Function: smv_typecheckt::typecheck - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void smv_typecheckt::typecheck( - exprt &expr, - const typet &type, - modet mode) -{ - typecheck_expr_rec(expr, type, mode); -} - -/*******************************************************************\ - Function: smv_typecheckt::typecheck_expr_rec Inputs: @@ -586,13 +528,8 @@ Function: smv_typecheckt::typecheck_expr_rec \*******************************************************************/ -void smv_typecheckt::typecheck_expr_rec( - exprt &expr, - const typet &dest_type, - modet mode) +void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) { - const auto static nil_type = static_cast(get_nil_irep()); - if(expr.id()==ID_symbol || expr.id()==ID_next_symbol) { @@ -628,22 +565,32 @@ void smv_typecheckt::typecheck_expr_rec( expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_xor || expr.id() == ID_not) { - typecheck_op(expr, bool_typet(), mode); + expr.type() = bool_typet{}; + + for(auto &op : expr.operands()) + { + typecheck_expr_rec(op, mode); + convert_expr_to(op, expr.type()); + } } else if(expr.id() == ID_smv_iff) { - typecheck_op(expr, bool_typet(), mode); + expr.type() = bool_typet{}; + + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + + convert_expr_to(binary_expr.lhs(), expr.type()); + convert_expr_to(binary_expr.rhs(), expr.type()); + expr.set(ID_C_smv_iff, true); expr.id(ID_equal); } - else if(expr.id()==ID_nondet_symbol) - { - if(!dest_type.is_nil()) - expr.type() = dest_type; - } else if(expr.id()==ID_constraint_select_one) { - typecheck_op(expr, dest_type, mode); + for(auto &op : expr.operands()) + typecheck_expr_rec(op, mode); typet op_type; op_type.make_nil(); @@ -655,108 +602,100 @@ void smv_typecheckt::typecheck_expr_rec( } for(auto &op : expr.operands()) - typecheck_expr_rec(op, op_type, mode); + convert_expr_to(op, op_type); expr.type()=op_type; } else if(expr.id()==ID_implies) { - if(expr.operands().size()!=2) - { - throw errort().with_location(expr.find_source_location()) - << "Expected two operands for -> operator"; - } + expr.type() = bool_typet{}; - typecheck_op(expr, bool_typet(), mode); + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + + convert_expr_to(binary_expr.lhs(), expr.type()); + convert_expr_to(binary_expr.rhs(), expr.type()); } else if(expr.id()==ID_equal || expr.id()==ID_notequal || expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) { - for(auto &op : expr.operands()) - typecheck_expr_rec(op, static_cast(get_nil_irep()), mode); - - if(expr.operands().size()!=2) - { - throw errort().with_location(expr.find_source_location()) - << "Expected two operands for " << expr.id(); - } - - expr.type()=bool_typet(); + expr.type() = bool_typet{}; exprt &op0 = to_binary_expr(expr).op0(), &op1 = to_binary_expr(expr).op1(); - typet op_type=type_union(op0.type(), op1.type()); - - typecheck_expr_rec(op0, op_type, mode); - typecheck_expr_rec(op1, op_type, mode); + typecheck_expr_rec(op0, mode); + typecheck_expr_rec(op1, mode); - INVARIANT(op0.type() == op1.type(), "type of operands of relational operators"); + typet op_type = type_union(op0.type(), op1.type()); if(expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) { - if(op0.type().id()!=ID_range) + if(op_type.id() != ID_range) { throw errort().with_location(expr.find_source_location()) << "Expected number type for " << to_string(expr); } } + + convert_expr_to(op0, op_type); + convert_expr_to(op1, op_type); } else if(expr.id() == ID_if) // ?: { + for(auto &op : expr.operands()) + typecheck_expr_rec(op, mode); + auto &if_expr = to_if_expr(expr); + auto &cond = if_expr.cond(); auto &true_case = if_expr.true_case(); auto &false_case = if_expr.false_case(); - typecheck_expr_rec(if_expr.cond(), bool_typet{}, mode); - typecheck_expr_rec(true_case, dest_type, mode); - typecheck_expr_rec(false_case, dest_type, mode); - expr.type() = dest_type; + + typet op_type = type_union(true_case.type(), false_case.type()); + + convert_expr_to(cond, bool_typet{}); + convert_expr_to(true_case, op_type); + convert_expr_to(false_case, op_type); + + expr.type() = op_type; } else if(expr.id()==ID_plus || expr.id()==ID_minus || expr.id()==ID_mult || expr.id()==ID_div || expr.id()==ID_mod) { - typecheck_op(expr, dest_type, mode); + exprt &op0 = to_binary_expr(expr).op0(), &op1 = to_binary_expr(expr).op1(); - if(expr.operands().size()!=2) - { - throw errort().with_location(expr.find_source_location()) - << "Expected two operands for " << expr.id(); - } + typecheck_expr_rec(op0, mode); + typecheck_expr_rec(op1, mode); + + // find proper type for precise arithmetic + smv_ranget new_range; + + smv_ranget smv_range0 = convert_type(op0.type()); + smv_ranget smv_range1 = convert_type(op1.type()); + + if(expr.id() == ID_plus) + new_range = smv_range0 + smv_range1; + else if(expr.id() == ID_minus) + new_range = smv_range0 - smv_range1; + else if(expr.id() == ID_mult) + new_range = smv_range0 * smv_range1; + else if(expr.id() == ID_div) + new_range = smv_range0; + else if(expr.id() == ID_mod) + new_range = smv_range1; + else + assert(false); - if(dest_type.is_nil()) - { - if(expr.type().id()==ID_range || - expr.type().id()==ID_bool) - { - // find proper type for precise arithmetic - smv_ranget new_range; - - smv_ranget smv_range0 = convert_type(to_binary_expr(expr).op0().type()); - smv_ranget smv_range1 = convert_type(to_binary_expr(expr).op1().type()); - - if(expr.id()==ID_plus) - new_range=smv_range0+smv_range1; - else if(expr.id()==ID_minus) - new_range=smv_range0-smv_range1; - else if(expr.id()==ID_mult) - new_range=smv_range0*smv_range1; - else if(expr.id()==ID_div) - new_range=smv_range0; - else if(expr.id()==ID_mod) - new_range=smv_range1; - else - assert(false); + new_range.make_union(smv_range0); + new_range.make_union(smv_range1); - new_range.to_type(expr.type()); - } - } - else if(dest_type.id() != ID_range) - { - throw errort().with_location(expr.find_source_location()) - << "Expected number type for " << to_string(expr); - } + new_range.to_type(expr.type()); + + convert_expr_to(op0, expr.type()); + convert_expr_to(op1, expr.type()); } else if(expr.id()==ID_constant) { @@ -765,131 +704,42 @@ void smv_typecheckt::typecheck_expr_rec( const std::string &value=expr.get_string(ID_value); mp_integer int_value=string2integer(value); - if(dest_type.is_nil()) - { - expr.type()=typet(ID_range); - expr.type().set(ID_from, integer2string(int_value)); - expr.type().set(ID_to, integer2string(int_value)); - } - else - { - expr.type() = dest_type; - - if(dest_type.id() == ID_bool) - { - if(int_value==0) - expr=false_exprt(); - else if(int_value==1) - expr=true_exprt(); - else - { - throw errort().with_location(expr.find_source_location()) - << "expected 0 or 1 here, but got " << value; - } - } - else if(dest_type.id() == ID_range) - { - smv_ranget smv_range = convert_type(dest_type); - - if(int_valuesmv_range.to) - { - throw errort().with_location(expr.find_source_location()) - << "expected " << smv_range.from << ".." << smv_range.to - << " here, but got " << value; - } - } - else - { - throw errort().with_location(expr.find_source_location()) - << "Unexpected constant: " << value; - } - } + expr.type() = typet(ID_range); + expr.type().set(ID_from, integer2string(int_value)); + expr.type().set(ID_to, integer2string(int_value)); } else if(expr.type().id()==ID_enumeration) { - if(dest_type.id() == ID_enumeration) - { - if(to_enumeration_type(expr.type()).elements().empty()) - expr.type() = dest_type; - } - } - else if(dest_type.is_not_nil() && dest_type != expr.type()) - { - // already done, but maybe need to change the type - mp_integer int_value; - bool have_int_value=false; - - if(expr.type().id()==ID_bool) - { - int_value=expr.is_true()?1:0; - have_int_value=true; - } - else if(expr.type().id()==ID_range) - { - int_value=string2integer(expr.get_string(ID_value)); - have_int_value=true; - } - - if(have_int_value) - { - if(dest_type.id() == ID_bool) - { - if(int_value==0) - expr=false_exprt(); - else if(int_value==1) - expr=true_exprt(); - } - else if(dest_type.id() == ID_range) - { - mp_integer from = string2integer(dest_type.get_string(ID_from)), - to = string2integer(dest_type.get_string(ID_to)); - - if(int_value>=from && int_value<=to) - { - expr = exprt(ID_constant, dest_type); - expr.set(ID_value, integer2string(int_value)); - } - } - } } } else if(expr.id()==ID_cond) { - if(dest_type.is_nil()) - { - bool condition=true; - - expr.type().make_nil(); + for(auto &op : expr.operands()) + typecheck_expr_rec(op, mode); - for(auto &op : expr.operands()) - { - if(condition) - typecheck_expr_rec(op, bool_typet(), mode); - else - { - typecheck_expr_rec( - op, static_cast(get_nil_irep()), mode); - expr.type() = type_union(expr.type(), op.type()); - } + bool condition = true; + typet result_type; + result_type.make_nil(); - condition=!condition; - } - } - else + for(auto &op : expr.operands()) { - expr.type() = dest_type; + if(!condition) + result_type = type_union(result_type, op.type()); - bool condition=true; + condition = !condition; + } - for(auto &op : expr.operands()) - { - if(condition) - typecheck_expr_rec(op, bool_typet(), mode); - else - typecheck_expr_rec(op, expr.type(), mode); + expr.type() = result_type; - condition=!condition; - } + condition = true; + for(auto &op : expr.operands()) + { + if(condition) + convert_expr_to(op, bool_typet{}); + else + convert_expr_to(op, result_type); + + condition = !condition; } } else if( @@ -900,7 +750,9 @@ void smv_typecheckt::typecheck_expr_rec( throw errort().with_location(expr.source_location()) << "CTL operator not permitted here"; expr.type() = bool_typet(); - typecheck_expr_rec(to_unary_expr(expr).op(), expr.type(), mode); + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + convert_expr_to(op, expr.type()); } else if(expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G) { @@ -908,7 +760,9 @@ void smv_typecheckt::typecheck_expr_rec( throw errort().with_location(expr.source_location()) << "LTL operator not permitted here"; expr.type() = bool_typet(); - typecheck_expr_rec(to_unary_expr(expr).op(), expr.type(), mode); + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + convert_expr_to(op, expr.type()); } else if( expr.id() == ID_EU || expr.id() == ID_ER || expr.id() == ID_AU || @@ -919,8 +773,10 @@ void smv_typecheckt::typecheck_expr_rec( << "CTL operator not permitted here"; auto &binary_expr = to_binary_expr(expr); expr.type() = bool_typet(); - typecheck_expr_rec(binary_expr.lhs(), expr.type(), mode); - typecheck_expr_rec(binary_expr.rhs(), expr.type(), mode); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + convert_expr_to(binary_expr.lhs(), expr.type()); + convert_expr_to(binary_expr.rhs(), expr.type()); } else if(expr.id() == ID_U || expr.id() == ID_R) { @@ -929,8 +785,10 @@ void smv_typecheckt::typecheck_expr_rec( << "LTL operator not permitted here"; auto &binary_expr = to_binary_expr(expr); expr.type() = bool_typet(); - typecheck_expr_rec(binary_expr.lhs(), expr.type(), mode); - typecheck_expr_rec(binary_expr.rhs(), expr.type(), mode); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + convert_expr_to(binary_expr.lhs(), expr.type()); + convert_expr_to(binary_expr.rhs(), expr.type()); } else if(expr.id()==ID_typecast) { @@ -948,9 +806,6 @@ void smv_typecheckt::typecheck_expr_rec( throw errort().with_location(expr.find_source_location()) << "No type checking for " << expr.id(); } - - if(!dest_type.is_nil()) - convert_expr_to(expr, dest_type); } /*******************************************************************\ @@ -1206,7 +1061,8 @@ void smv_typecheckt::typecheck( mode=OTHER; } - typecheck(item.expr, bool_typet(), mode); + typecheck(item.expr, mode); + convert_expr_to(item.expr, bool_typet{}); } /*******************************************************************\ @@ -1358,9 +1214,11 @@ void smv_typecheckt::convert_define(const irep_idt &identifier) symbolt &symbol=*it; d.in_progress=true; - - typecheck(d.value, symbol.type, OTHER); - + + typecheck(d.value, OTHER); + if(symbol.type.is_not_nil()) + convert_expr_to(d.value, symbol.type); + d.in_progress=false; d.typechecked=true;